--- 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
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
+
+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]