author | wenzelm |
Thu, 04 Oct 2001 15:43:17 +0200 | |
changeset 11688 | 56833637db2a |
parent 11439 | 9aaab1a160a5 |
child 11825 | ef7d619e2c88 |
permissions | -rw-r--r-- |
7700 | 1 |
(* Title: HOL/Inductive.thy |
2 |
ID: $Id$ |
|
10402 | 3 |
Author: Markus Wenzel, TU Muenchen |
10727 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
11688 | 5 |
*) |
10727 | 6 |
|
11688 | 7 |
header {* Support for inductive sets and types *} |
1187 | 8 |
|
11325
a5e0289dd56c
Inductive definitions are now introduced earlier in the theory hierarchy.
berghofe
parents:
11003
diff
changeset
|
9 |
theory Inductive = Gfp + Sum_Type + Relation |
7700 | 10 |
files |
10402 | 11 |
("Tools/inductive_package.ML") |
12 |
("Tools/datatype_aux.ML") |
|
13 |
("Tools/datatype_prop.ML") |
|
14 |
("Tools/datatype_rep_proofs.ML") |
|
15 |
("Tools/datatype_abs_proofs.ML") |
|
16 |
("Tools/datatype_package.ML") |
|
17 |
("Tools/primrec_package.ML"): |
|
18 |
||
10727 | 19 |
|
11688 | 20 |
subsection {* Proof by cases and induction *} |
21 |
||
22 |
text {* Proper handling of non-atomic rule statements. *} |
|
10727 | 23 |
|
10402 | 24 |
constdefs |
25 |
forall :: "('a => bool) => bool" |
|
26 |
"forall P == \<forall>x. P x" |
|
27 |
implies :: "bool => bool => bool" |
|
28 |
"implies A B == A --> B" |
|
10434 | 29 |
equal :: "'a => 'a => bool" |
30 |
"equal x y == x = y" |
|
10727 | 31 |
conj :: "bool => bool => bool" |
32 |
"conj A B == A & B" |
|
10402 | 33 |
|
34 |
lemma forall_eq: "(!!x. P x) == Trueprop (forall (\<lambda>x. P x))" |
|
10434 | 35 |
by (simp only: atomize_all forall_def) |
6437 | 36 |
|
10402 | 37 |
lemma implies_eq: "(A ==> B) == Trueprop (implies A B)" |
10434 | 38 |
by (simp only: atomize_imp implies_def) |
39 |
||
40 |
lemma equal_eq: "(x == y) == Trueprop (equal x y)" |
|
41 |
by (simp only: atomize_eq equal_def) |
|
10402 | 42 |
|
10727 | 43 |
lemma forall_conj: "forall (\<lambda>x. conj (A x) (B x)) = conj (forall A) (forall B)" |
44 |
by (unfold forall_def conj_def) blast |
|
45 |
||
46 |
lemma implies_conj: "implies C (conj A B) = conj (implies C A) (implies C B)" |
|
47 |
by (unfold implies_def conj_def) blast |
|
48 |
||
49 |
lemma conj_curry: "(conj A B ==> C) == (A ==> B ==> C)" |
|
50 |
by (simp only: atomize_imp atomize_eq conj_def) (rule equal_intr_rule, blast+) |
|
10434 | 51 |
|
52 |
lemmas inductive_atomize = forall_eq implies_eq equal_eq |
|
53 |
lemmas inductive_rulify1 = inductive_atomize [symmetric, standard] |
|
10727 | 54 |
lemmas inductive_rulify2 = forall_def implies_def equal_def conj_def |
55 |
lemmas inductive_conj = forall_conj implies_conj conj_curry |
|
56 |
||
57 |
hide const forall implies equal conj |
|
58 |
||
59 |
||
11688 | 60 |
text {* Method setup. *} |
61 |
||
62 |
ML {* |
|
63 |
structure InductMethod = InductMethodFun |
|
64 |
(struct |
|
65 |
val dest_concls = HOLogic.dest_concls; |
|
66 |
val cases_default = thm "case_split"; |
|
67 |
val conjI = thm "conjI"; |
|
68 |
val atomize = thms "inductive_atomize"; |
|
69 |
val rulify1 = thms "inductive_rulify1"; |
|
70 |
val rulify2 = thms "inductive_rulify2"; |
|
71 |
end); |
|
72 |
*} |
|
73 |
||
74 |
setup InductMethod.setup |
|
75 |
||
76 |
||
77 |
subsection {* Inductive sets *} |
|
78 |
||
79 |
text {* Inversion of injective functions. *} |
|
11436 | 80 |
|
81 |
constdefs |
|
82 |
myinv :: "('a => 'b) => ('b => 'a)" |
|
83 |
"myinv (f :: 'a => 'b) == \<lambda>y. THE x. f x = y" |
|
84 |
||
85 |
lemma myinv_f_f: "inj f ==> myinv f (f x) = x" |
|
86 |
proof - |
|
87 |
assume "inj f" |
|
88 |
hence "(THE x'. f x' = f x) = (THE x'. x' = x)" |
|
89 |
by (simp only: inj_eq) |
|
90 |
also have "... = x" by (rule the_eq_trivial) |
|
11439 | 91 |
finally show ?thesis by (unfold myinv_def) |
11436 | 92 |
qed |
93 |
||
94 |
lemma f_myinv_f: "inj f ==> y \<in> range f ==> f (myinv f y) = y" |
|
95 |
proof (unfold myinv_def) |
|
96 |
assume inj: "inj f" |
|
97 |
assume "y \<in> range f" |
|
98 |
then obtain x where "y = f x" .. |
|
99 |
hence x: "f x = y" .. |
|
100 |
thus "f (THE x. f x = y) = y" |
|
101 |
proof (rule theI) |
|
102 |
fix x' assume "f x' = y" |
|
103 |
with x have "f x' = f x" by simp |
|
104 |
with inj show "x' = x" by (rule injD) |
|
105 |
qed |
|
106 |
qed |
|
107 |
||
108 |
hide const myinv |
|
109 |
||
110 |
||
11688 | 111 |
text {* Package setup. *} |
10402 | 112 |
|
113 |
use "Tools/inductive_package.ML" |
|
6437 | 114 |
setup InductivePackage.setup |
10402 | 115 |
|
11688 | 116 |
theorems basic_monos [mono] = |
117 |
subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2 |
|
118 |
Collect_mono in_mono vimage_mono |
|
119 |
imp_conv_disj not_not de_Morgan_disj de_Morgan_conj |
|
120 |
not_all not_ex |
|
121 |
Ball_def Bex_def |
|
122 |
inductive_rulify2 |
|
123 |
||
124 |
||
125 |
subsubsection {* Inductive datatypes and primitive recursion *} |
|
126 |
||
10402 | 127 |
use "Tools/datatype_aux.ML" |
128 |
use "Tools/datatype_prop.ML" |
|
129 |
use "Tools/datatype_rep_proofs.ML" |
|
130 |
use "Tools/datatype_abs_proofs.ML" |
|
131 |
use "Tools/datatype_package.ML" |
|
7700 | 132 |
setup DatatypePackage.setup |
10402 | 133 |
|
134 |
use "Tools/primrec_package.ML" |
|
8482 | 135 |
setup PrimrecPackage.setup |
7700 | 136 |
|
6437 | 137 |
end |