src/HOL/Inductive.thy
 author krauss Fri Nov 24 13:44:51 2006 +0100 (2006-11-24) changeset 21512 3786eb1b69d6 parent 21018 e6b8d6784792 child 22218 30a8890d2967 permissions -rw-r--r--
Lemma "fundef_default_value" uses predicate instead of set.
1 (*  Title:      HOL/Inductive.thy
2     ID:         \$Id\$
3     Author:     Markus Wenzel, TU Muenchen
4 *)
6 header {* Support for inductive sets and types *}
8 theory Inductive
9 imports FixedPoint Sum_Type Relation Record
10 uses
11   ("Tools/inductive_package.ML")
12   ("Tools/old_inductive_package.ML")
13   ("Tools/inductive_realizer.ML")
14   ("Tools/inductive_codegen.ML")
15   ("Tools/datatype_aux.ML")
16   ("Tools/datatype_prop.ML")
17   ("Tools/datatype_rep_proofs.ML")
18   ("Tools/datatype_abs_proofs.ML")
19   ("Tools/datatype_realizer.ML")
20   ("Tools/datatype_hooks.ML")
21   ("Tools/datatype_package.ML")
22   ("Tools/datatype_codegen.ML")
23   ("Tools/recfun_codegen.ML")
24   ("Tools/primrec_package.ML")
25 begin
27 subsection {* Inductive sets *}
29 text {* Inversion of injective functions. *}
31 constdefs
32   myinv :: "('a => 'b) => ('b => 'a)"
33   "myinv (f :: 'a => 'b) == \<lambda>y. THE x. f x = y"
35 lemma myinv_f_f: "inj f ==> myinv f (f x) = x"
36 proof -
37   assume "inj f"
38   hence "(THE x'. f x' = f x) = (THE x'. x' = x)"
39     by (simp only: inj_eq)
40   also have "... = x" by (rule the_eq_trivial)
41   finally show ?thesis by (unfold myinv_def)
42 qed
44 lemma f_myinv_f: "inj f ==> y \<in> range f ==> f (myinv f y) = y"
45 proof (unfold myinv_def)
46   assume inj: "inj f"
47   assume "y \<in> range f"
48   then obtain x where "y = f x" ..
49   hence x: "f x = y" ..
50   thus "f (THE x. f x = y) = y"
51   proof (rule theI)
52     fix x' assume "f x' = y"
53     with x have "f x' = f x" by simp
54     with inj show "x' = x" by (rule injD)
55   qed
56 qed
58 hide const myinv
61 text {* Package setup. *}
63 use "Tools/old_inductive_package.ML"
64 setup OldInductivePackage.setup
66 theorems basic_monos [mono] =
67   subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2
68   Collect_mono in_mono vimage_mono
69   imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
70   not_all not_ex
71   Ball_def Bex_def
72   induct_rulify_fallback
74 use "Tools/inductive_package.ML"
75 setup InductivePackage.setup
77 theorems [mono2] =
78   imp_refl disj_mono conj_mono ex_mono all_mono if_def2
79   imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
80   not_all not_ex
81   Ball_def Bex_def
82   induct_rulify_fallback
84 lemma False_meta_all:
85   "Trueprop False \<equiv> (\<And>P\<Colon>bool. P)"
86 proof
87   fix P
88   assume False
89   then show P ..
90 next
91   assume "\<And>P\<Colon>bool. P"
92   then show "False" ..
93 qed
95 lemma not_eq_False:
96   assumes not_eq: "x \<noteq> y"
97   and eq: "x == y"
98   shows False
99   using not_eq eq by auto
101 lemmas not_eq_quodlibet =
102   not_eq_False [simplified False_meta_all]
105 subsection {* Inductive datatypes and primitive recursion *}
107 text {* Package setup. *}
109 use "Tools/recfun_codegen.ML"
110 setup RecfunCodegen.setup
112 use "Tools/datatype_aux.ML"
113 use "Tools/datatype_prop.ML"
114 use "Tools/datatype_rep_proofs.ML"
115 use "Tools/datatype_abs_proofs.ML"
116 use "Tools/datatype_realizer.ML"
118 use "Tools/datatype_hooks.ML"
119 setup DatatypeHooks.setup
121 use "Tools/datatype_package.ML"
122 setup DatatypePackage.setup
124 use "Tools/datatype_codegen.ML"
125 setup DatatypeCodegen.setup
127 use "Tools/inductive_realizer.ML"
128 setup InductiveRealizer.setup
130 use "Tools/inductive_codegen.ML"
131 setup InductiveCodegen.setup
133 use "Tools/primrec_package.ML"
135 end