wenzelm@7700: (* Title: HOL/Inductive.thy wenzelm@7700: ID: $Id$ wenzelm@10402: Author: Markus Wenzel, TU Muenchen wenzelm@10727: License: GPL (GNU GENERAL PUBLIC LICENSE) wenzelm@11688: *) wenzelm@10727: wenzelm@11688: header {* Support for inductive sets and types *} lcp@1187: berghofe@11325: theory Inductive = Gfp + Sum_Type + Relation wenzelm@7700: files wenzelm@10402: ("Tools/inductive_package.ML") berghofe@12437: ("Tools/inductive_codegen.ML") wenzelm@10402: ("Tools/datatype_aux.ML") wenzelm@10402: ("Tools/datatype_prop.ML") wenzelm@10402: ("Tools/datatype_rep_proofs.ML") wenzelm@10402: ("Tools/datatype_abs_proofs.ML") wenzelm@10402: ("Tools/datatype_package.ML") berghofe@12437: ("Tools/datatype_codegen.ML") berghofe@12437: ("Tools/recfun_codegen.ML") wenzelm@10402: ("Tools/primrec_package.ML"): wenzelm@10402: wenzelm@10727: wenzelm@11688: subsection {* Inductive sets *} wenzelm@11688: wenzelm@11688: text {* Inversion of injective functions. *} wenzelm@11436: wenzelm@11436: constdefs wenzelm@11436: myinv :: "('a => 'b) => ('b => 'a)" wenzelm@11436: "myinv (f :: 'a => 'b) == \y. THE x. f x = y" wenzelm@11436: wenzelm@11436: lemma myinv_f_f: "inj f ==> myinv f (f x) = x" wenzelm@11436: proof - wenzelm@11436: assume "inj f" wenzelm@11436: hence "(THE x'. f x' = f x) = (THE x'. x' = x)" wenzelm@11436: by (simp only: inj_eq) wenzelm@11436: also have "... = x" by (rule the_eq_trivial) wenzelm@11439: finally show ?thesis by (unfold myinv_def) wenzelm@11436: qed wenzelm@11436: wenzelm@11436: lemma f_myinv_f: "inj f ==> y \ range f ==> f (myinv f y) = y" wenzelm@11436: proof (unfold myinv_def) wenzelm@11436: assume inj: "inj f" wenzelm@11436: assume "y \ range f" wenzelm@11436: then obtain x where "y = f x" .. wenzelm@11436: hence x: "f x = y" .. wenzelm@11436: thus "f (THE x. f x = y) = y" wenzelm@11436: proof (rule theI) wenzelm@11436: fix x' assume "f x' = y" wenzelm@11436: with x have "f x' = f x" by simp wenzelm@11436: with inj show "x' = x" by (rule injD) wenzelm@11436: qed wenzelm@11436: qed wenzelm@11436: wenzelm@11436: hide const myinv wenzelm@11436: wenzelm@11436: wenzelm@11688: text {* Package setup. *} wenzelm@10402: wenzelm@10402: use "Tools/inductive_package.ML" wenzelm@6437: setup InductivePackage.setup wenzelm@10402: wenzelm@11688: theorems basic_monos [mono] = wenzelm@11688: subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2 wenzelm@11688: Collect_mono in_mono vimage_mono wenzelm@11688: imp_conv_disj not_not de_Morgan_disj de_Morgan_conj wenzelm@11688: not_all not_ex wenzelm@11688: Ball_def Bex_def wenzelm@11990: induct_rulify2 wenzelm@11688: wenzelm@11688: wenzelm@12023: subsection {* Inductive datatypes and primitive recursion *} wenzelm@11688: wenzelm@11825: text {* Package setup. *} wenzelm@11825: berghofe@12437: use "Tools/recfun_codegen.ML" berghofe@12437: setup RecfunCodegen.setup berghofe@12437: wenzelm@10402: use "Tools/datatype_aux.ML" wenzelm@10402: use "Tools/datatype_prop.ML" wenzelm@10402: use "Tools/datatype_rep_proofs.ML" wenzelm@10402: use "Tools/datatype_abs_proofs.ML" wenzelm@10402: use "Tools/datatype_package.ML" wenzelm@7700: setup DatatypePackage.setup wenzelm@10402: berghofe@12437: use "Tools/datatype_codegen.ML" berghofe@12437: setup DatatypeCodegen.setup berghofe@12437: berghofe@12437: use "Tools/inductive_codegen.ML" berghofe@12437: setup InductiveCodegen.setup berghofe@12437: wenzelm@10402: use "Tools/primrec_package.ML" wenzelm@7700: wenzelm@6437: end