28 HTTgen_def: |
27 HTTgen_def: |
29 "HTTgen(R) == {t. t=true | t=false | (EX a b. t=<a,b> & a : R & b : R) | |
28 "HTTgen(R) == {t. t=true | t=false | (EX a b. t=<a,b> & a : R & b : R) | |
30 (EX f. t=lam x. f(x) & (ALL x. f(x) : R))}" |
29 (EX f. t=lam x. f(x) & (ALL x. f(x) : R))}" |
31 HTT_def: "HTT == gfp(HTTgen)" |
30 HTT_def: "HTT == gfp(HTTgen)" |
32 |
31 |
33 ML {* use_legacy_bindings (the_context ()) *} |
32 |
|
33 subsection {* Hereditary Termination *} |
|
34 |
|
35 lemma HTTgen_mono: "mono(%X. HTTgen(X))" |
|
36 apply (unfold HTTgen_def) |
|
37 apply (rule monoI) |
|
38 apply blast |
|
39 done |
|
40 |
|
41 lemma HTTgenXH: |
|
42 "t : HTTgen(A) <-> t=true | t=false | (EX a b. t=<a,b> & a : A & b : A) | |
|
43 (EX f. t=lam x. f(x) & (ALL x. f(x) : A))" |
|
44 apply (unfold HTTgen_def) |
|
45 apply blast |
|
46 done |
|
47 |
|
48 lemma HTTXH: |
|
49 "t : HTT <-> t=true | t=false | (EX a b. t=<a,b> & a : HTT & b : HTT) | |
|
50 (EX f. t=lam x. f(x) & (ALL x. f(x) : HTT))" |
|
51 apply (rule HTTgen_mono [THEN HTT_def [THEN def_gfp_Tarski], THEN XHlemma1, unfolded HTTgen_def]) |
|
52 apply blast |
|
53 done |
|
54 |
|
55 |
|
56 subsection {* Introduction Rules for HTT *} |
|
57 |
|
58 lemma HTT_bot: "~ bot : HTT" |
|
59 by (blast dest: HTTXH [THEN iffD1]) |
|
60 |
|
61 lemma HTT_true: "true : HTT" |
|
62 by (blast intro: HTTXH [THEN iffD2]) |
|
63 |
|
64 lemma HTT_false: "false : HTT" |
|
65 by (blast intro: HTTXH [THEN iffD2]) |
|
66 |
|
67 lemma HTT_pair: "<a,b> : HTT <-> a : HTT & b : HTT" |
|
68 apply (rule HTTXH [THEN iff_trans]) |
|
69 apply blast |
|
70 done |
|
71 |
|
72 lemma HTT_lam: "lam x. f(x) : HTT <-> (ALL x. f(x) : HTT)" |
|
73 apply (rule HTTXH [THEN iff_trans]) |
|
74 apply auto |
|
75 done |
|
76 |
|
77 lemmas HTT_rews1 = HTT_bot HTT_true HTT_false HTT_pair HTT_lam |
|
78 |
|
79 lemma HTT_rews2: |
|
80 "one : HTT" |
|
81 "inl(a) : HTT <-> a : HTT" |
|
82 "inr(b) : HTT <-> b : HTT" |
|
83 "zero : HTT" |
|
84 "succ(n) : HTT <-> n : HTT" |
|
85 "[] : HTT" |
|
86 "x$xs : HTT <-> x : HTT & xs : HTT" |
|
87 by (simp_all add: data_defs HTT_rews1) |
|
88 |
|
89 lemmas HTT_rews = HTT_rews1 HTT_rews2 |
|
90 |
|
91 |
|
92 subsection {* Coinduction for HTT *} |
|
93 |
|
94 lemma HTT_coinduct: "[| t : R; R <= HTTgen(R) |] ==> t : HTT" |
|
95 apply (erule HTT_def [THEN def_coinduct]) |
|
96 apply assumption |
|
97 done |
|
98 |
|
99 ML {* |
|
100 local val HTT_coinduct = thm "HTT_coinduct" |
|
101 in fun HTT_coinduct_tac s i = res_inst_tac [("R", s)] HTT_coinduct i end |
|
102 *} |
|
103 |
|
104 lemma HTT_coinduct3: |
|
105 "[| t : R; R <= HTTgen(lfp(%x. HTTgen(x) Un R Un HTT)) |] ==> t : HTT" |
|
106 apply (erule HTTgen_mono [THEN [3] HTT_def [THEN def_coinduct3]]) |
|
107 apply assumption |
|
108 done |
|
109 |
|
110 ML {* |
|
111 local |
|
112 val HTT_coinduct3 = thm "HTT_coinduct3" |
|
113 val HTTgen_def = thm "HTTgen_def" |
|
114 in |
|
115 |
|
116 val HTT_coinduct3_raw = rewrite_rule [HTTgen_def] HTT_coinduct3 |
|
117 |
|
118 fun HTT_coinduct3_tac s i = res_inst_tac [("R",s)] HTT_coinduct3 i |
|
119 |
|
120 val HTTgenIs = |
|
121 map (mk_genIs (the_context ()) (thms "data_defs") (thm "HTTgenXH") (thm "HTTgen_mono")) |
|
122 ["true : HTTgen(R)", |
|
123 "false : HTTgen(R)", |
|
124 "[| a : R; b : R |] ==> <a,b> : HTTgen(R)", |
|
125 "[| !!x. b(x) : R |] ==> lam x. b(x) : HTTgen(R)", |
|
126 "one : HTTgen(R)", |
|
127 "a : lfp(%x. HTTgen(x) Un R Un HTT) ==> inl(a) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))", |
|
128 "b : lfp(%x. HTTgen(x) Un R Un HTT) ==> inr(b) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))", |
|
129 "zero : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))", |
|
130 "n : lfp(%x. HTTgen(x) Un R Un HTT) ==> succ(n) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))", |
|
131 "[] : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))", |
|
132 "[| h : lfp(%x. HTTgen(x) Un R Un HTT); t : lfp(%x. HTTgen(x) Un R Un HTT) |] ==> h$t : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"] |
34 |
133 |
35 end |
134 end |
|
135 *} |
|
136 |
|
137 ML {* bind_thms ("HTTgenIs", HTTgenIs) *} |
|
138 |
|
139 |
|
140 subsection {* Formation Rules for Types *} |
|
141 |
|
142 lemma UnitF: "Unit <= HTT" |
|
143 by (simp add: subsetXH UnitXH HTT_rews) |
|
144 |
|
145 lemma BoolF: "Bool <= HTT" |
|
146 by (fastsimp simp: subsetXH BoolXH iff: HTT_rews) |
|
147 |
|
148 lemma PlusF: "[| A <= HTT; B <= HTT |] ==> A + B <= HTT" |
|
149 by (fastsimp simp: subsetXH PlusXH iff: HTT_rews) |
|
150 |
|
151 lemma SigmaF: "[| A <= HTT; !!x. x:A ==> B(x) <= HTT |] ==> SUM x:A. B(x) <= HTT" |
|
152 by (fastsimp simp: subsetXH SgXH HTT_rews) |
|
153 |
|
154 |
|
155 (*** Formation Rules for Recursive types - using coinduction these only need ***) |
|
156 (*** exhaution rule for type-former ***) |
|
157 |
|
158 (*Proof by induction - needs induction rule for type*) |
|
159 lemma "Nat <= HTT" |
|
160 apply (simp add: subsetXH) |
|
161 apply clarify |
|
162 apply (erule Nat_ind) |
|
163 apply (fastsimp iff: HTT_rews)+ |
|
164 done |
|
165 |
|
166 lemma NatF: "Nat <= HTT" |
|
167 apply clarify |
|
168 apply (erule HTT_coinduct3) |
|
169 apply (fast intro: HTTgenIs elim!: HTTgen_mono [THEN ci3_RI] dest: NatXH [THEN iffD1]) |
|
170 done |
|
171 |
|
172 lemma ListF: "A <= HTT ==> List(A) <= HTT" |
|
173 apply clarify |
|
174 apply (erule HTT_coinduct3) |
|
175 apply (fast intro!: HTTgenIs elim!: HTTgen_mono [THEN ci3_RI] |
|
176 subsetD [THEN HTTgen_mono [THEN ci3_AI]] |
|
177 dest: ListXH [THEN iffD1]) |
|
178 done |
|
179 |
|
180 lemma ListsF: "A <= HTT ==> Lists(A) <= HTT" |
|
181 apply clarify |
|
182 apply (erule HTT_coinduct3) |
|
183 apply (fast intro!: HTTgenIs elim!: HTTgen_mono [THEN ci3_RI] |
|
184 subsetD [THEN HTTgen_mono [THEN ci3_AI]] dest: ListsXH [THEN iffD1]) |
|
185 done |
|
186 |
|
187 lemma IListsF: "A <= HTT ==> ILists(A) <= HTT" |
|
188 apply clarify |
|
189 apply (erule HTT_coinduct3) |
|
190 apply (fast intro!: HTTgenIs elim!: HTTgen_mono [THEN ci3_RI] |
|
191 subsetD [THEN HTTgen_mono [THEN ci3_AI]] dest: IListsXH [THEN iffD1]) |
|
192 done |
|
193 |
|
194 end |