wenzelm@7700: (*  Title:      HOL/Inductive.thy
wenzelm@7700:     ID:         $Id$
wenzelm@10402:     Author:     Markus Wenzel, TU Muenchen
wenzelm@11688: *)
wenzelm@10727: 
wenzelm@11688: header {* Support for inductive sets and types *}
lcp@1187: 
nipkow@15131: theory Inductive 
avigad@17009: imports FixedPoint Sum_Type Relation Record
haftmann@16417: uses
wenzelm@10402:   ("Tools/inductive_package.ML")
berghofe@21018:   ("Tools/old_inductive_package.ML")
berghofe@13705:   ("Tools/inductive_realizer.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")
berghofe@13469:   ("Tools/datatype_realizer.ML")
haftmann@19599:   ("Tools/datatype_hooks.ML")
wenzelm@10402:   ("Tools/datatype_package.ML")
berghofe@12437:   ("Tools/datatype_codegen.ML")
berghofe@12437:   ("Tools/recfun_codegen.ML")
nipkow@15131:   ("Tools/primrec_package.ML")
nipkow@15131: begin
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) == \<lambda>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 \<in> range f ==> f (myinv f y) = y"
wenzelm@11436: proof (unfold myinv_def)
wenzelm@11436:   assume inj: "inj f"
wenzelm@11436:   assume "y \<in> 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: 
berghofe@21018: use "Tools/old_inductive_package.ML"
berghofe@21018: setup OldInductivePackage.setup
wenzelm@10402: 
wenzelm@11688: theorems basic_monos [mono] =
haftmann@22218:   subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
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@18456:   induct_rulify_fallback
wenzelm@11688: 
berghofe@21018: use "Tools/inductive_package.ML"
berghofe@21018: setup InductivePackage.setup
berghofe@21018: 
berghofe@21018: theorems [mono2] =
haftmann@22218:   imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
berghofe@21018:   imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
berghofe@21018:   not_all not_ex
berghofe@21018:   Ball_def Bex_def
berghofe@21018:   induct_rulify_fallback
berghofe@21018: 
haftmann@20604: lemma False_meta_all:
haftmann@20604:   "Trueprop False \<equiv> (\<And>P\<Colon>bool. P)"
haftmann@20604: proof
haftmann@20604:   fix P
haftmann@20604:   assume False
haftmann@20604:   then show P ..
haftmann@20604: next
haftmann@20604:   assume "\<And>P\<Colon>bool. P"
haftmann@20604:   then show "False" ..
haftmann@20604: qed
haftmann@20604: 
haftmann@20604: lemma not_eq_False:
haftmann@20604:   assumes not_eq: "x \<noteq> y"
haftmann@20604:   and eq: "x == y"
haftmann@20604:   shows False
haftmann@20604:   using not_eq eq by auto
haftmann@20604: 
haftmann@20604: lemmas not_eq_quodlibet =
haftmann@20604:   not_eq_False [simplified False_meta_all]
haftmann@20604: 
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"
berghofe@13469: use "Tools/datatype_realizer.ML"
haftmann@19599: 
haftmann@19599: use "Tools/datatype_hooks.ML"
haftmann@19599: setup DatatypeHooks.setup
haftmann@19599: 
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@13705: use "Tools/inductive_realizer.ML"
berghofe@13705: setup InductiveRealizer.setup
berghofe@13705: 
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