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 haftmann@23708: imports FixedPoint Product_Type Sum_Type haftmann@16417: uses wenzelm@10402: ("Tools/inductive_package.ML") berghofe@23734: ("Tools/inductive_set_package.ML") berghofe@13705: ("Tools/inductive_realizer.ML") haftmann@24625: "Tools/dseq.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") berghofe@22783: ("Tools/datatype_case.ML") wenzelm@10402: ("Tools/datatype_package.ML") berghofe@12437: ("Tools/datatype_codegen.ML") nipkow@15131: ("Tools/primrec_package.ML") nipkow@15131: begin wenzelm@10727: berghofe@23734: subsection {* Inductive predicates and 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: berghofe@23734: theorems basic_monos = 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@23734: theorems [mono] = 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 \ (\P\bool. P)" haftmann@20604: proof haftmann@20604: fix P haftmann@20604: assume False haftmann@20604: then show P .. haftmann@20604: next haftmann@20604: assume "\P\bool. P" wenzelm@23389: then show False . haftmann@20604: qed haftmann@20604: haftmann@20604: lemma not_eq_False: haftmann@20604: assumes not_eq: "x \ y" haftmann@22886: 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: 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@22783: use "Tools/datatype_case.ML" berghofe@13469: use "Tools/datatype_realizer.ML" 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: berghofe@23734: use "Tools/inductive_set_package.ML" berghofe@23734: setup InductiveSetPackage.setup berghofe@23734: nipkow@23526: text{* Lambda-abstractions with pattern matching: *} nipkow@23526: nipkow@23526: syntax nipkow@23529: "_lam_pats_syntax" :: "cases_syn => 'a => 'b" ("(%_)" 10) nipkow@23526: syntax (xsymbols) nipkow@23529: "_lam_pats_syntax" :: "cases_syn => 'a => 'b" ("(\_)" 10) nipkow@23526: nipkow@23529: parse_translation (advanced) {* nipkow@23529: let nipkow@23529: fun fun_tr ctxt [cs] = nipkow@23529: let nipkow@23529: val x = Free (Name.variant (add_term_free_names (cs, [])) "x", dummyT); nipkow@24349: val ft = DatatypeCase.case_tr true DatatypePackage.datatype_of_constr nipkow@24349: ctxt [x, cs] nipkow@23529: in lambda x ft end nipkow@23529: in [("_lam_pats_syntax", fun_tr)] end nipkow@23526: *} nipkow@23526: nipkow@23526: end