equal
deleted
inserted
replaced
99 and TallXH: "a : TALL X. B(X) <-> (ALL X. a:B(X))" |
99 and TallXH: "a : TALL X. B(X) <-> (ALL X. a:B(X))" |
100 and TexXH: "a : TEX X. B(X) <-> (EX X. a:B(X))" |
100 and TexXH: "a : TEX X. B(X) <-> (EX X. a:B(X))" |
101 unfolding simp_type_defs by blast+ |
101 unfolding simp_type_defs by blast+ |
102 |
102 |
103 ML {* |
103 ML {* |
104 bind_thms ("case_rls", XH_to_Es @{thms XHs}); |
104 ML_Thms.bind_thms ("case_rls", XH_to_Es @{thms XHs}); |
105 *} |
105 *} |
106 |
106 |
107 |
107 |
108 subsection {* Canonical Type Rules *} |
108 subsection {* Canonical Type Rules *} |
109 |
109 |
260 unfolding ind_data_defs |
260 unfolding ind_data_defs |
261 by (rule ind_type_eqs [THEN XHlemma1], blast intro!: canTs elim!: case_rls)+ |
261 by (rule ind_type_eqs [THEN XHlemma1], blast intro!: canTs elim!: case_rls)+ |
262 |
262 |
263 lemmas iXHs = NatXH ListXH |
263 lemmas iXHs = NatXH ListXH |
264 |
264 |
265 ML {* bind_thms ("icase_rls", XH_to_Es @{thms iXHs}) *} |
265 ML {* ML_Thms.bind_thms ("icase_rls", XH_to_Es @{thms iXHs}) *} |
266 |
266 |
267 |
267 |
268 subsection {* Type Rules *} |
268 subsection {* Type Rules *} |
269 |
269 |
270 lemma zeroT: "zero : Nat" |
270 lemma zeroT: "zero : Nat" |
338 |
338 |
339 (* General theorem proving ignores non-canonical term-formers, *) |
339 (* General theorem proving ignores non-canonical term-formers, *) |
340 (* - intro rules are type rules for canonical terms *) |
340 (* - intro rules are type rules for canonical terms *) |
341 (* - elim rules are case rules (no non-canonical terms appear) *) |
341 (* - elim rules are case rules (no non-canonical terms appear) *) |
342 |
342 |
343 ML {* bind_thms ("XHEs", XH_to_Es @{thms XHs}) *} |
343 ML {* ML_Thms.bind_thms ("XHEs", XH_to_Es @{thms XHs}) *} |
344 |
344 |
345 lemmas [intro!] = SubtypeI canTs icanTs |
345 lemmas [intro!] = SubtypeI canTs icanTs |
346 and [elim!] = SubtypeE XHEs |
346 and [elim!] = SubtypeE XHEs |
347 |
347 |
348 |
348 |