1 (* Title: CCL/Hered.ML |
|
2 ID: $Id$ |
|
3 Author: Martin Coen, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 *) |
|
6 |
|
7 fun type_of_terms (Const("Trueprop",_) $ (Const("op =",(Type ("fun", [t,_])))$_$_)) = t; |
|
8 |
|
9 (*** Hereditary Termination ***) |
|
10 |
|
11 Goalw [HTTgen_def] "mono(%X. HTTgen(X))"; |
|
12 by (rtac monoI 1); |
|
13 by (fast_tac set_cs 1); |
|
14 qed "HTTgen_mono"; |
|
15 |
|
16 Goalw [HTTgen_def] |
|
17 "t : HTTgen(A) <-> t=true | t=false | (EX a b. t=<a,b> & a : A & b : A) | \ |
|
18 \ (EX f. t=lam x. f(x) & (ALL x. f(x) : A))"; |
|
19 by (fast_tac set_cs 1); |
|
20 qed "HTTgenXH"; |
|
21 |
|
22 Goal |
|
23 "t : HTT <-> t=true | t=false | (EX a b. t=<a,b> & a : HTT & b : HTT) | \ |
|
24 \ (EX f. t=lam x. f(x) & (ALL x. f(x) : HTT))"; |
|
25 by (rtac (rewrite_rule [HTTgen_def] |
|
26 (HTTgen_mono RS (HTT_def RS def_gfp_Tarski) RS XHlemma1)) 1); |
|
27 by (fast_tac set_cs 1); |
|
28 qed "HTTXH"; |
|
29 |
|
30 (*** Introduction Rules for HTT ***) |
|
31 |
|
32 Goal "~ bot : HTT"; |
|
33 by (fast_tac (term_cs addDs [XH_to_D HTTXH]) 1); |
|
34 qed "HTT_bot"; |
|
35 |
|
36 Goal "true : HTT"; |
|
37 by (fast_tac (term_cs addIs [XH_to_I HTTXH]) 1); |
|
38 qed "HTT_true"; |
|
39 |
|
40 Goal "false : HTT"; |
|
41 by (fast_tac (term_cs addIs [XH_to_I HTTXH]) 1); |
|
42 qed "HTT_false"; |
|
43 |
|
44 Goal "<a,b> : HTT <-> a : HTT & b : HTT"; |
|
45 by (rtac (HTTXH RS iff_trans) 1); |
|
46 by (fast_tac term_cs 1); |
|
47 qed "HTT_pair"; |
|
48 |
|
49 Goal "lam x. f(x) : HTT <-> (ALL x. f(x) : HTT)"; |
|
50 by (rtac (HTTXH RS iff_trans) 1); |
|
51 by (simp_tac term_ss 1); |
|
52 by (safe_tac term_cs); |
|
53 by (asm_simp_tac term_ss 1); |
|
54 by (fast_tac term_cs 1); |
|
55 qed "HTT_lam"; |
|
56 |
|
57 local |
|
58 val raw_HTTrews = [HTT_bot,HTT_true,HTT_false,HTT_pair,HTT_lam]; |
|
59 fun mk_thm s = prove_goalw (the_context ()) data_defs s (fn _ => |
|
60 [simp_tac (term_ss addsimps raw_HTTrews) 1]); |
|
61 in |
|
62 val HTT_rews = raw_HTTrews @ |
|
63 map mk_thm ["one : HTT", |
|
64 "inl(a) : HTT <-> a : HTT", |
|
65 "inr(b) : HTT <-> b : HTT", |
|
66 "zero : HTT", |
|
67 "succ(n) : HTT <-> n : HTT", |
|
68 "[] : HTT", |
|
69 "x$xs : HTT <-> x : HTT & xs : HTT"]; |
|
70 end; |
|
71 |
|
72 val HTT_Is = HTT_rews @ (HTT_rews RL [iffD2]); |
|
73 |
|
74 (*** Coinduction for HTT ***) |
|
75 |
|
76 val prems = goal (the_context ()) "[| t : R; R <= HTTgen(R) |] ==> t : HTT"; |
|
77 by (rtac (HTT_def RS def_coinduct) 1); |
|
78 by (REPEAT (ares_tac prems 1)); |
|
79 qed "HTT_coinduct"; |
|
80 |
|
81 fun HTT_coinduct_tac s i = res_inst_tac [("R",s)] HTT_coinduct i; |
|
82 |
|
83 val prems = goal (the_context ()) |
|
84 "[| t : R; R <= HTTgen(lfp(%x. HTTgen(x) Un R Un HTT)) |] ==> t : HTT"; |
|
85 by (rtac (HTTgen_mono RSN(3,HTT_def RS def_coinduct3)) 1); |
|
86 by (REPEAT (ares_tac prems 1)); |
|
87 qed "HTT_coinduct3"; |
|
88 val HTT_coinduct3_raw = rewrite_rule [HTTgen_def] HTT_coinduct3; |
|
89 |
|
90 fun HTT_coinduct3_tac s i = res_inst_tac [("R",s)] HTT_coinduct3 i; |
|
91 |
|
92 val HTTgenIs = map (mk_genIs (the_context ()) data_defs HTTgenXH HTTgen_mono) |
|
93 ["true : HTTgen(R)", |
|
94 "false : HTTgen(R)", |
|
95 "[| a : R; b : R |] ==> <a,b> : HTTgen(R)", |
|
96 "[| !!x. b(x) : R |] ==> lam x. b(x) : HTTgen(R)", |
|
97 "one : HTTgen(R)", |
|
98 "a : lfp(%x. HTTgen(x) Un R Un HTT) ==> \ |
|
99 \ inl(a) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))", |
|
100 "b : lfp(%x. HTTgen(x) Un R Un HTT) ==> \ |
|
101 \ inr(b) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))", |
|
102 "zero : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))", |
|
103 "n : lfp(%x. HTTgen(x) Un R Un HTT) ==> \ |
|
104 \ succ(n) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))", |
|
105 "[] : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))", |
|
106 "[| h : lfp(%x. HTTgen(x) Un R Un HTT); t : lfp(%x. HTTgen(x) Un R Un HTT) |] ==>\ |
|
107 \ h$t : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"]; |
|
108 |
|
109 (*** Formation Rules for Types ***) |
|
110 |
|
111 Goal "Unit <= HTT"; |
|
112 by (simp_tac (CCL_ss addsimps ([subsetXH,UnitXH] @ HTT_rews)) 1); |
|
113 qed "UnitF"; |
|
114 |
|
115 Goal "Bool <= HTT"; |
|
116 by (simp_tac (CCL_ss addsimps ([subsetXH,BoolXH] @ HTT_rews)) 1); |
|
117 by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1); |
|
118 qed "BoolF"; |
|
119 |
|
120 val prems = goal (the_context ()) "[| A <= HTT; B <= HTT |] ==> A + B <= HTT"; |
|
121 by (simp_tac (CCL_ss addsimps ([subsetXH,PlusXH] @ HTT_rews)) 1); |
|
122 by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1); |
|
123 qed "PlusF"; |
|
124 |
|
125 val prems = goal (the_context ()) |
|
126 "[| A <= HTT; !!x. x:A ==> B(x) <= HTT |] ==> SUM x:A. B(x) <= HTT"; |
|
127 by (simp_tac (CCL_ss addsimps ([subsetXH,SgXH] @ HTT_rews)) 1); |
|
128 by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1); |
|
129 qed "SigmaF"; |
|
130 |
|
131 (*** Formation Rules for Recursive types - using coinduction these only need ***) |
|
132 (*** exhaution rule for type-former ***) |
|
133 |
|
134 (*Proof by induction - needs induction rule for type*) |
|
135 Goal "Nat <= HTT"; |
|
136 by (simp_tac (term_ss addsimps [subsetXH]) 1); |
|
137 by (safe_tac set_cs); |
|
138 by (etac Nat_ind 1); |
|
139 by (ALLGOALS (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])))); |
|
140 val NatF = result(); |
|
141 |
|
142 Goal "Nat <= HTT"; |
|
143 by (safe_tac set_cs); |
|
144 by (etac HTT_coinduct3 1); |
|
145 by (fast_tac (set_cs addIs HTTgenIs |
|
146 addSEs [HTTgen_mono RS ci3_RI] addEs [XH_to_E NatXH]) 1); |
|
147 qed "NatF"; |
|
148 |
|
149 val [prem] = goal (the_context ()) "A <= HTT ==> List(A) <= HTT"; |
|
150 by (safe_tac set_cs); |
|
151 by (etac HTT_coinduct3 1); |
|
152 by (fast_tac (set_cs addSIs HTTgenIs |
|
153 addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)] |
|
154 addEs [XH_to_E ListXH]) 1); |
|
155 qed "ListF"; |
|
156 |
|
157 val [prem] = goal (the_context ()) "A <= HTT ==> Lists(A) <= HTT"; |
|
158 by (safe_tac set_cs); |
|
159 by (etac HTT_coinduct3 1); |
|
160 by (fast_tac (set_cs addSIs HTTgenIs |
|
161 addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)] |
|
162 addEs [XH_to_E ListsXH]) 1); |
|
163 qed "ListsF"; |
|
164 |
|
165 val [prem] = goal (the_context ()) "A <= HTT ==> ILists(A) <= HTT"; |
|
166 by (safe_tac set_cs); |
|
167 by (etac HTT_coinduct3 1); |
|
168 by (fast_tac (set_cs addSIs HTTgenIs |
|
169 addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)] |
|
170 addEs [XH_to_E IListsXH]) 1); |
|
171 qed "IListsF"; |
|
172 |
|
173 (*** A possible use for this predicate is proving equality from pre-order ***) |
|
174 (*** but it seems as easy (and more general) to do this directly by coinduction ***) |
|
175 (* |
|
176 val prems = goal (the_context ()) "[| t : HTT; t [= u |] ==> u [= t"; |
|
177 by (po_coinduct_tac "{p. EX a b. p=<a,b> & b : HTT & b [= a}" 1); |
|
178 by (fast_tac (ccl_cs addIs prems) 1); |
|
179 by (safe_tac ccl_cs); |
|
180 by (dtac (poXH RS iffD1) 1); |
|
181 by (safe_tac (set_cs addSEs [HTT_bot RS notE])); |
|
182 by (REPEAT_SOME (rtac (POgenXH RS iffD2) ORELSE' etac rev_mp)); |
|
183 by (ALLGOALS (simp_tac (term_ss addsimps HTT_rews))); |
|
184 by (ALLGOALS (fast_tac ccl_cs)); |
|
185 qed "HTT_po_op"; |
|
186 |
|
187 val prems = goal (the_context ()) "[| t : HTT; t [= u |] ==> t = u"; |
|
188 by (REPEAT (ares_tac (prems @ [conjI RS (eq_iff RS iffD2),HTT_po_op]) 1)); |
|
189 qed "HTT_po_eq"; |
|
190 *) |
|