src/HOL/Inductive.thy
 changeset 10727 2ccafccb81c0 parent 10434 6ea4735c3955 child 11003 ee0838d89deb
```--- a/src/HOL/Inductive.thy	Fri Dec 22 18:20:55 2000 +0100
+++ b/src/HOL/Inductive.thy	Fri Dec 22 18:23:41 2000 +0100
@@ -1,6 +1,9 @@
(*  Title:      HOL/Inductive.thy
ID:         \$Id\$
Author:     Markus Wenzel, TU Muenchen
+
+Setup packages for inductive sets and types etc.
*)

theory Inductive = Gfp + Sum_Type + NatDef
@@ -14,6 +17,9 @@
("Tools/datatype_package.ML")
("Tools/primrec_package.ML"):

+
+(* handling of proper rules *)
+
constdefs
forall :: "('a => bool) => bool"
"forall P == \<forall>x. P x"
@@ -21,6 +27,8 @@
"implies A B == A --> B"
equal :: "'a => 'a => bool"
"equal x y == x = y"
+  conj :: "bool => bool => bool"
+  "conj A B == A & B"

lemma forall_eq: "(!!x. P x) == Trueprop (forall (\<lambda>x. P x))"
by (simp only: atomize_all forall_def)
@@ -31,11 +39,24 @@
lemma equal_eq: "(x == y) == Trueprop (equal x y)"
by (simp only: atomize_eq equal_def)

-hide const forall implies equal
+lemma forall_conj: "forall (\<lambda>x. conj (A x) (B x)) = conj (forall A) (forall B)"
+  by (unfold forall_def conj_def) blast
+
+lemma implies_conj: "implies C (conj A B) = conj (implies C A) (implies C B)"
+  by (unfold implies_def conj_def) blast
+
+lemma conj_curry: "(conj A B ==> C) == (A ==> B ==> C)"
+  by (simp only: atomize_imp atomize_eq conj_def) (rule equal_intr_rule, blast+)

lemmas inductive_atomize = forall_eq implies_eq equal_eq
lemmas inductive_rulify1 = inductive_atomize [symmetric, standard]
-lemmas inductive_rulify2 = forall_def implies_def equal_def
+lemmas inductive_rulify2 = forall_def implies_def equal_def conj_def
+lemmas inductive_conj = forall_conj implies_conj conj_curry
+
+hide const forall implies equal conj
+
+
+(* setup packages *)

use "Tools/induct_method.ML"
setup InductMethod.setup
@@ -54,11 +75,13 @@
setup PrimrecPackage.setup

theorems basic_monos [mono] =
-   subset_refl imp_refl disj_mono conj_mono ex_mono all_mono
-   Collect_mono in_mono vimage_mono
-   imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
-   not_all not_ex
-   Ball_def Bex_def
+  subset_refl imp_refl disj_mono conj_mono ex_mono all_mono
+  Collect_mono in_mono vimage_mono
+  imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
+  not_all not_ex
+  Ball_def Bex_def
+  inductive_rulify2
+

(*belongs to theory Transitive_Closure*)
declare rtrancl_induct [induct set: rtrancl]```