author | wenzelm |
Mon, 06 Nov 2000 22:49:16 +0100 | |
changeset 10402 | 5e82d6cafb5f |
parent 10312 | 4c5a03649af7 |
child 10434 | 6ea4735c3955 |
permissions | -rw-r--r-- |
7700 | 1 |
(* Title: HOL/Inductive.thy |
2 |
ID: $Id$ |
|
10402 | 3 |
Author: Markus Wenzel, TU Muenchen |
7700 | 4 |
*) |
1187 | 5 |
|
10212 | 6 |
theory Inductive = Gfp + Sum_Type + NatDef |
7700 | 7 |
files |
10402 | 8 |
("Tools/induct_method.ML") |
9 |
("Tools/inductive_package.ML") |
|
10 |
("Tools/datatype_aux.ML") |
|
11 |
("Tools/datatype_prop.ML") |
|
12 |
("Tools/datatype_rep_proofs.ML") |
|
13 |
("Tools/datatype_abs_proofs.ML") |
|
14 |
("Tools/datatype_package.ML") |
|
15 |
("Tools/primrec_package.ML"): |
|
16 |
||
17 |
constdefs |
|
18 |
forall :: "('a => bool) => bool" |
|
19 |
"forall P == \<forall>x. P x" |
|
20 |
implies :: "bool => bool => bool" |
|
21 |
"implies A B == A --> B" |
|
22 |
||
23 |
lemma forall_eq: "(!!x. P x) == Trueprop (forall (\<lambda>x. P x))" |
|
24 |
proof |
|
25 |
assume "!!x. P x" |
|
26 |
thus "forall (\<lambda>x. P x)" by (unfold forall_def) blast |
|
27 |
next |
|
28 |
fix x |
|
29 |
assume "forall (\<lambda>x. P x)" |
|
30 |
thus "P x" by (unfold forall_def) blast |
|
31 |
qed |
|
6437 | 32 |
|
10402 | 33 |
lemma implies_eq: "(A ==> B) == Trueprop (implies A B)" |
34 |
proof |
|
35 |
assume "A ==> B" |
|
36 |
thus "implies A B" by (unfold implies_def) blast |
|
37 |
next |
|
38 |
assume "implies A B" and A |
|
39 |
thus B by (unfold implies_def) blast |
|
40 |
qed |
|
41 |
||
42 |
lemmas inductive_atomize = forall_eq implies_eq |
|
43 |
lemmas inductive_rulify = inductive_atomize [symmetric, standard] |
|
44 |
hide const forall implies |
|
45 |
||
46 |
use "Tools/induct_method.ML" |
|
8303 | 47 |
setup InductMethod.setup |
10402 | 48 |
|
49 |
use "Tools/inductive_package.ML" |
|
6437 | 50 |
setup InductivePackage.setup |
10402 | 51 |
|
52 |
use "Tools/datatype_aux.ML" |
|
53 |
use "Tools/datatype_prop.ML" |
|
54 |
use "Tools/datatype_rep_proofs.ML" |
|
55 |
use "Tools/datatype_abs_proofs.ML" |
|
56 |
use "Tools/datatype_package.ML" |
|
7700 | 57 |
setup DatatypePackage.setup |
10402 | 58 |
|
59 |
use "Tools/primrec_package.ML" |
|
8482 | 60 |
setup PrimrecPackage.setup |
7700 | 61 |
|
10312 | 62 |
theorems basic_monos [mono] = |
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7700
diff
changeset
|
63 |
subset_refl imp_refl disj_mono conj_mono ex_mono all_mono |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7700
diff
changeset
|
64 |
Collect_mono in_mono vimage_mono |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7700
diff
changeset
|
65 |
imp_conv_disj not_not de_Morgan_disj de_Morgan_conj |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7700
diff
changeset
|
66 |
not_all not_ex |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7700
diff
changeset
|
67 |
Ball_def Bex_def |
6437 | 68 |
|
10312 | 69 |
(*belongs to theory Transitive_Closure*) |
70 |
declare rtrancl_induct [induct set: rtrancl] |
|
71 |
declare rtranclE [cases set: rtrancl] |
|
72 |
declare trancl_induct [induct set: trancl] |
|
73 |
declare tranclE [cases set: trancl] |
|
74 |
||
6437 | 75 |
end |