author | berghofe |
Tue, 22 May 2001 15:10:06 +0200 | |
changeset 11325 | a5e0289dd56c |
parent 11003 | ee0838d89deb |
child 11436 | 3f74b80d979f |
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) |
5 |
||
6 |
Setup packages for inductive sets and types etc. |
|
7700 | 7 |
*) |
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/induct_method.ML") |
12 |
("Tools/inductive_package.ML") |
|
13 |
("Tools/datatype_aux.ML") |
|
14 |
("Tools/datatype_prop.ML") |
|
15 |
("Tools/datatype_rep_proofs.ML") |
|
16 |
("Tools/datatype_abs_proofs.ML") |
|
17 |
("Tools/datatype_package.ML") |
|
18 |
("Tools/primrec_package.ML"): |
|
19 |
||
10727 | 20 |
|
21 |
(* handling of proper rules *) |
|
22 |
||
10402 | 23 |
constdefs |
24 |
forall :: "('a => bool) => bool" |
|
25 |
"forall P == \<forall>x. P x" |
|
26 |
implies :: "bool => bool => bool" |
|
27 |
"implies A B == A --> B" |
|
10434 | 28 |
equal :: "'a => 'a => bool" |
29 |
"equal x y == x = y" |
|
10727 | 30 |
conj :: "bool => bool => bool" |
31 |
"conj A B == A & B" |
|
10402 | 32 |
|
33 |
lemma forall_eq: "(!!x. P x) == Trueprop (forall (\<lambda>x. P x))" |
|
10434 | 34 |
by (simp only: atomize_all forall_def) |
6437 | 35 |
|
10402 | 36 |
lemma implies_eq: "(A ==> B) == Trueprop (implies A B)" |
10434 | 37 |
by (simp only: atomize_imp implies_def) |
38 |
||
39 |
lemma equal_eq: "(x == y) == Trueprop (equal x y)" |
|
40 |
by (simp only: atomize_eq equal_def) |
|
10402 | 41 |
|
10727 | 42 |
lemma forall_conj: "forall (\<lambda>x. conj (A x) (B x)) = conj (forall A) (forall B)" |
43 |
by (unfold forall_def conj_def) blast |
|
44 |
||
45 |
lemma implies_conj: "implies C (conj A B) = conj (implies C A) (implies C B)" |
|
46 |
by (unfold implies_def conj_def) blast |
|
47 |
||
48 |
lemma conj_curry: "(conj A B ==> C) == (A ==> B ==> C)" |
|
49 |
by (simp only: atomize_imp atomize_eq conj_def) (rule equal_intr_rule, blast+) |
|
10434 | 50 |
|
51 |
lemmas inductive_atomize = forall_eq implies_eq equal_eq |
|
52 |
lemmas inductive_rulify1 = inductive_atomize [symmetric, standard] |
|
10727 | 53 |
lemmas inductive_rulify2 = forall_def implies_def equal_def conj_def |
54 |
lemmas inductive_conj = forall_conj implies_conj conj_curry |
|
55 |
||
56 |
hide const forall implies equal conj |
|
57 |
||
58 |
||
59 |
(* setup packages *) |
|
10402 | 60 |
|
61 |
use "Tools/induct_method.ML" |
|
8303 | 62 |
setup InductMethod.setup |
10402 | 63 |
|
64 |
use "Tools/inductive_package.ML" |
|
6437 | 65 |
setup InductivePackage.setup |
10402 | 66 |
|
67 |
use "Tools/datatype_aux.ML" |
|
68 |
use "Tools/datatype_prop.ML" |
|
69 |
use "Tools/datatype_rep_proofs.ML" |
|
70 |
use "Tools/datatype_abs_proofs.ML" |
|
71 |
use "Tools/datatype_package.ML" |
|
7700 | 72 |
setup DatatypePackage.setup |
10402 | 73 |
|
74 |
use "Tools/primrec_package.ML" |
|
8482 | 75 |
setup PrimrecPackage.setup |
7700 | 76 |
|
10312 | 77 |
theorems basic_monos [mono] = |
11003 | 78 |
subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2 |
10727 | 79 |
Collect_mono in_mono vimage_mono |
80 |
imp_conv_disj not_not de_Morgan_disj de_Morgan_conj |
|
81 |
not_all not_ex |
|
82 |
Ball_def Bex_def |
|
83 |
inductive_rulify2 |
|
84 |
||
6437 | 85 |
end |