# HG changeset patch
# User wenzelm
# Date 1135207714 -3600
# Node ID 8cc35e95450a42f12cbb776b76770faad20e90e5
# Parent  b293c1087f1dddf47d5b2a4189f2470f61da5b3f
updated auxiliary facts for induct method;

diff -r b293c1087f1d -r 8cc35e95450a src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Wed Dec 21 17:00:57 2005 +0100
+++ b/src/FOL/FOL.thy	Thu Dec 22 00:28:34 2005 +0100
@@ -5,12 +5,12 @@
 
 header {* Classical first-order logic *}
 
-theory FOL 
+theory FOL
 imports IFOL
 uses ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML")
       ("eqrule_FOL_data.ML")
       ("~~/src/Provers/eqsubst.ML")
-begin  
+begin
 
 
 subsection {* The classical axiom *}
@@ -93,33 +93,32 @@
 text {* Proper handling of non-atomic rule statements. *}
 
 constdefs
-  induct_forall :: "('a => o) => o"
-  "induct_forall(P) == \<forall>x. P(x)"
-  induct_implies :: "o => o => o"
-  "induct_implies(A, B) == A --> B"
-  induct_equal :: "'a => 'a => o"
-  "induct_equal(x, y) == x = y"
+  induct_forall where "induct_forall(P) == \<forall>x. P(x)"
+  induct_implies where "induct_implies(A, B) == A \<longrightarrow> B"
+  induct_equal where "induct_equal(x, y) == x = y"
+  induct_conj where "induct_conj(A, B) == A \<and> B"
 
 lemma induct_forall_eq: "(!!x. P(x)) == Trueprop(induct_forall(\<lambda>x. P(x)))"
-  by (simp only: atomize_all induct_forall_def)
+  by (unfold atomize_all induct_forall_def)
 
 lemma induct_implies_eq: "(A ==> B) == Trueprop(induct_implies(A, B))"
-  by (simp only: atomize_imp induct_implies_def)
+  by (unfold atomize_imp induct_implies_def)
 
 lemma induct_equal_eq: "(x == y) == Trueprop(induct_equal(x, y))"
-  by (simp only: atomize_eq induct_equal_def)
+  by (unfold atomize_eq induct_equal_def)
 
-lemma induct_impliesI: "(A ==> B) ==> induct_implies(A, B)"
-  by (simp add: induct_implies_def)
+lemma induct_conj_eq:
+  includes meta_conjunction_syntax
+  shows "(A && B) == Trueprop(induct_conj(A, B))"
+  by (unfold atomize_conj induct_conj_def)
 
-lemmas induct_atomize = atomize_conj induct_forall_eq induct_implies_eq induct_equal_eq
-lemmas induct_rulify1 [symmetric, standard] = induct_forall_eq induct_implies_eq induct_equal_eq
-lemmas induct_rulify2 = induct_forall_def induct_implies_def induct_equal_def
+lemmas induct_atomize_old = induct_forall_eq induct_implies_eq induct_equal_eq atomize_conj
+lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
+lemmas induct_rulify [symmetric, standard] = induct_atomize
+lemmas induct_rulify_fallback =
+  induct_forall_def induct_implies_def induct_equal_def induct_conj_def
 
-lemma all_conj_eq: "(ALL x. P(x)) & (ALL y. Q(y)) == (ALL x y. P(x) & Q(y))"
-  by simp
-
-hide const induct_forall induct_implies induct_equal
+hide const induct_forall induct_implies induct_equal induct_conj
 
 
 text {* Method setup. *}
@@ -127,15 +126,11 @@
 ML {*
   structure InductMethod = InductMethodFun
   (struct
-    val dest_concls = FOLogic.dest_concls;
     val cases_default = thm "case_split";
-    val local_impI = thm "induct_impliesI";
-    val conjI = thm "conjI";
+    val atomize_old = thms "induct_atomize_old";
     val atomize = thms "induct_atomize";
-    val rulify1 = thms "induct_rulify1";
-    val rulify2 = thms "induct_rulify2";
-    val localize = [Thm.symmetric (thm "induct_implies_def"),
-      Thm.symmetric (thm "atomize_all"), thm "all_conj_eq"];
+    val rulify = thms "induct_rulify";
+    val rulify_fallback = thms "induct_rulify_fallback";
   end);
 *}
 
diff -r b293c1087f1d -r 8cc35e95450a src/HOL/Extraction.thy
--- a/src/HOL/Extraction.thy	Wed Dec 21 17:00:57 2005 +0100
+++ b/src/HOL/Extraction.thy	Thu Dec 22 00:28:34 2005 +0100
@@ -49,12 +49,12 @@
 *}
 
 lemmas [extraction_expand] =
-  atomize_eq atomize_all atomize_imp
+  atomize_eq atomize_all atomize_imp atomize_conj
   allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2
   notE' impE' impE iffE imp_cong simp_thms
-  induct_forall_eq induct_implies_eq induct_equal_eq
-  induct_forall_def induct_implies_def induct_impliesI
-  induct_atomize induct_rulify1 induct_rulify2
+  induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
+  induct_forall_def induct_implies_def induct_equal_def induct_conj_def
+  induct_atomize induct_atomize_old induct_rulify induct_rulify_fallback
 
 datatype sumbool = Left | Right
 
diff -r b293c1087f1d -r 8cc35e95450a src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Wed Dec 21 17:00:57 2005 +0100
+++ b/src/HOL/Inductive.thy	Thu Dec 22 00:28:34 2005 +0100
@@ -67,7 +67,7 @@
   imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
   not_all not_ex
   Ball_def Bex_def
-  induct_rulify2
+  induct_rulify_fallback
 
 
 subsection {* Inductive datatypes and primitive recursion *}