1(* non-interactive mode
2*)
3open HolKernel Parse boolLib;
4val _ = new_theory "subtype";
5val _ = ParseExtras.temp_loose_equality()
6
7(* interactive mode
8show_assums := true;
9loadPath := union ["../ho_prover"] (!loadPath);
10app load
11  ["bossLib", "combinTheory", "pred_setTheory", "seqTheory", "HurdUseful",
12   "res_quanTheory", "ho_proverTools", "pairTheory"];
13*)
14
15open bossLib combinTheory pred_setTheory seqTheory hurdUtils
16     res_quanTheory ho_proverTools pairTheory;
17
18infixr 0 ++ << || THENC ORELSEC ORELSER ##;
19infix 1 >>;
20
21val op++ = op THEN;
22val op<< = op THENL;
23val op|| = op ORELSE;
24val op>> = op THEN1;
25
26(* ------------------------------------------------------------------------- *)
27(* Auxiliary theorems.                                                       *)
28(* ------------------------------------------------------------------------- *)
29
30val EQ_T_IMP = store_thm
31  ("EQ_T_IMP",
32   ``!x. x = T ==> x``,
33   PROVE_TAC []);
34
35val EQ_SUBSET_SUBSET = store_thm
36  ("EQ_SUBSET_SUBSET",
37   ``!(s : 'a -> bool) t. (s = t) ==> s SUBSET t /\ t SUBSET s``,
38   RW_TAC std_ss [SUBSET_DEF, EXTENSION]);
39
40val IN_EQ_UNIV_IMP = store_thm
41  ("IN_EQ_UNIV_IMP",
42   ``!s. (s = UNIV) ==> !v. (v : 'a) IN s``,
43   RW_TAC std_ss [IN_UNIV]);
44
45(* ------------------------------------------------------------------------- *)
46(* bool theory subtypes.                                                     *)
47(* ------------------------------------------------------------------------- *)
48
49(* Subtype definitions *)
50
51val _ = add_infix("->", 250, HOLgrammars.RIGHT);
52
53val _ = overload_on
54  ("->", ``FUNSET:('a->bool) -> ('b->bool) -> (('a->'b)->bool)``);
55val _ = overload_on
56  ("-->", ``DFUNSET : ('a->bool) -> ('a->'b->bool) -> (('a->'b)->bool)``);
57
58val pair_def = Define
59  `pair (X : 'a -> bool) (Y : 'b -> bool) = \ (x, y). x IN X /\ y IN Y`;
60
61val IN_PAIR = store_thm
62  ("IN_PAIR",
63   ``!(x : 'a # 'b) X Y. x IN pair X Y = FST x IN X /\ SND x IN Y``,
64   Cases
65   ++ RW_TAC std_ss [pair_def, SPECIFICATION]);
66
67(* Simplifications *)
68
69val PAIR_UNIV = store_thm
70  ("PAIR_UNIV",
71   ``pair UNIV UNIV = (UNIV : 'a # 'b -> bool)``,
72   RW_TAC std_ss [SET_EQ, IN_PAIR, IN_UNIV]);
73
74(* Subtypes *)
75
76val DEFAULT_SUBTYPE = store_thm
77  ("DEFAULT_SUBTYPE",
78   ``!x. x IN UNIV``,
79   RW_TAC std_ss [IN_UNIV]);
80
81val COMB_SUBTYPE = store_thm
82  ("COMB_SUBTYPE",
83   ``!(f : 'a -> 'b) a x y. f IN (x --> y) /\ a IN x ==> f a IN y a``,
84   RW_TAC std_ss [IN_DFUNSET]
85   ++ PROVE_TAC []);
86
87val ABS_SUBTYPE = store_thm
88  ("ABS_SUBTYPE",
89   ``!(f : 'a -> 'b) p. (!x. f x IN p x) ==> (\x. f x) IN (UNIV --> p)``,
90   CONV_TAC (DEPTH_CONV FUN_EQ_CONV)
91   ++ RW_TAC std_ss [IN_DFUNSET]);
92
93val COND_SUBTYPE = store_thm
94  ("COND_SUBTYPE",
95   ``!c (a:'a) b x.
96       (c ==> a IN x) /\
97       (~c ==> b IN x) ==>
98       COND c a b IN x``,
99   RW_TAC std_ss []);
100
101val RES_ABSTRACT_SUBTYPE = store_thm
102  ("RES_ABSTRACT_SUBTYPE",
103   ``!p (f : 'a -> 'b) q.
104       (!x. x IN p ==> (f x IN q x)) ==>
105       RES_ABSTRACT p f IN (p --> q)``,
106   RW_TAC std_ss [RES_FORALL, RES_ABSTRACT, IN_DFUNSET]);
107
108val UNCURRY_SUBTYPE = store_thm
109  ("UNCURRY_SUBTYPE",
110   ``!(f : 'a -> 'b -> 'c) p.
111       (!x y. f x y IN p x y) ==>
112       (UNCURRY f IN (UNIV --> UNCURRY p))``,
113    RW_TAC std_ss [IN_DFUNSET]
114    ++ Cases_on `x`
115    ++ RW_TAC std_ss []);
116
117(* ------------------------------------------------------------------------- *)
118(* The bool theory simplifier module.                                        *)
119(* ------------------------------------------------------------------------- *)
120
121(* Congruences *)
122
123val comb_cong = store_thm
124  ("comb_cong",
125   ``!(f : 'a -> 'b) f' a a'. (f = f') /\ (a = a') ==> (f a = f' a')``,
126   RW_TAC std_ss []);
127
128val abs_cong = store_thm
129  ("abs_cong",
130   ``!(f : 'a -> 'b) f'. (!x. f x = f' x) ==> ((\x. f x) = f')``,
131   CONV_TAC (DEPTH_CONV FUN_EQ_CONV)
132   ++ RW_TAC std_ss []);
133
134val conj_cong = store_thm
135  ("conj_cong",
136   ``!a a' b b'.
137       (b ==> (a = a')) /\
138       (a' ==> (b = b')) ==>
139       (a /\ b = a' /\ b')``,
140   RW_TAC std_ss []
141   ++ ho_PROVE_TAC []);
142
143val disj_cong = store_thm
144  ("disj_cong",
145   ``!a a' b b'.
146       (~b ==> (a = a')) /\
147       (~a' ==> (b = b')) ==>
148       (a \/ b = a' \/ b')``,
149   RW_TAC std_ss []
150   ++ ho_PROVE_TAC []);
151
152val imp_cong = store_thm
153  ("imp_cong",
154   ``!a a' b b'.
155       (a = a') /\
156       (a' ==> (b = b')) ==>
157       (a ==> b = a' ==> b')``,
158   RW_TAC std_ss []
159   ++ ho_PROVE_TAC []);
160
161val cond_cong = store_thm
162  ("cond_cong",
163   ``!c c' (a:'a) a' b b'.
164       (c = c') /\
165       (c' ==> (a = a')) /\
166       (~c' ==> (b = b')) ==>
167       (COND c a b = COND c' a' b')``,
168   RW_TAC std_ss []);
169
170val res_forall_cong = store_thm
171  ("res_forall_cong",
172   ``!(p : 'a -> bool) p' f f'.
173       (p = p') /\
174       (!x. x IN p' ==> (f x = f' x)) ==>
175       (RES_FORALL p f = RES_FORALL p' f')``,
176   RW_TAC std_ss [RES_FORALL]);
177
178val res_exists_cong = store_thm
179  ("res_exists_cong",
180   ``!(p : 'a -> bool) p' f f'.
181       (p = p') /\
182       (!x. x IN p' ==> (f x = f' x)) ==>
183       (RES_EXISTS p f = RES_EXISTS p' f')``,
184   RW_TAC std_ss [RES_EXISTS]
185   ++ ho_PROVE_TAC []);
186
187val res_select_cong = store_thm
188  ("res_select_cong",
189   ``!(p : 'a -> bool) p' f f'.
190       (p = p') /\
191       (!x. x IN p' ==> (f x = f' x)) ==>
192       (RES_SELECT p f = RES_SELECT p' f')``,
193   RW_TAC std_ss [RES_SELECT]
194   ++ Q_TAC SUFF_TAC `!x. x IN p /\ f x = x IN p /\ f' x` >> RW_TAC std_ss []
195   ++ ho_PROVE_TAC []);
196
197val res_abstract_cong = store_thm
198  ("res_abstract_cong",
199   ``!(p : 'a -> bool) p' f f'.
200       (p = p') /\
201       (!x. x IN p' ==> (f x = f' x)) ==>
202       (RES_ABSTRACT p f = RES_ABSTRACT p' f')``,
203   RW_TAC std_ss [RES_ABSTRACT_EQUAL]);
204
205val uncurry_cong = store_thm
206  ("uncurry_cong",
207   ``!(f : 'a -> 'b -> 'c) f'.
208        (!x y. f x y = f' x y) ==>
209        (UNCURRY f = UNCURRY f')``,
210   FUN_EQ_TAC
211   ++ RW_TAC std_ss []
212   ++ Cases_on `x`
213   ++ RW_TAC std_ss [UNCURRY_DEF]);
214
215(* Rewrites *)
216
217val PAIRED_BETA_THM = store_thm
218  ("PAIRED_BETA_THM",
219   ``!f z. UNCURRY f z = f (FST z) (SND z)``,
220   STRIP_TAC
221   ++ Cases
222   ++ RW_TAC std_ss []);
223
224(* non-interactive mode
225*)
226val _ = export_theory ();
227