# HG changeset patch
# User wenzelm
# Date 1135207716 -3600
# Node ID 356a9f7118996b405071185dc22b69e411220ca9
# Parent  8cc35e95450a42f12cbb776b76770faad20e90e5
structure ProjectRule;
updated auxiliary facts for induct method;
tuned proofs;

diff -r 8cc35e95450a -r 356a9f711899 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Dec 22 00:28:34 2005 +0100
+++ b/src/HOL/HOL.thy	Thu Dec 22 00:28:36 2005 +0100
@@ -237,22 +237,18 @@
 
 subsection {*Equality*}
 
-lemma sym: "s=t ==> t=s"
-apply (erule subst)
-apply (rule refl)
-done
+lemma sym: "s = t ==> t = s"
+  by (erule subst) (rule refl)
 
-(*calling "standard" reduces maxidx to 0*)
-lemmas ssubst = sym [THEN subst, standard]
+lemma ssubst: "t = s ==> P s ==> P t"
+  by (drule sym) (erule subst)
 
 lemma trans: "[| r=s; s=t |] ==> r=t"
-apply (erule subst , assumption)
-done
+  by (erule subst)
 
-lemma def_imp_eq:  assumes meq: "A == B" shows "A = B"
-apply (unfold meq)
-apply (rule refl)
-done
+lemma def_imp_eq: assumes meq: "A == B" shows "A = B"
+  by (unfold meq) (rule refl)
+
 
 (*Useful with eresolve_tac for proving equalties from known equalities.
         a = b
@@ -303,18 +299,13 @@
 subsection {*Equality of booleans -- iff*}
 
 lemma iffI: assumes prems: "P ==> Q" "Q ==> P" shows "P=Q"
-apply (iprover intro: iff [THEN mp, THEN mp] impI prems)
-done
+  by (iprover intro: iff [THEN mp, THEN mp] impI prems)
 
 lemma iffD2: "[| P=Q; Q |] ==> P"
-apply (erule ssubst)
-apply assumption
-done
+  by (erule ssubst)
 
 lemma rev_iffD2: "[| Q; P=Q |] ==> P"
-apply (erule iffD2)
-apply assumption
-done
+  by (erule iffD2)
 
 lemmas iffD1 = sym [THEN iffD2, standard]
 lemmas rev_iffD1 = sym [THEN [2] rev_iffD2, standard]
@@ -322,19 +313,17 @@
 lemma iffE:
   assumes major: "P=Q"
       and minor: "[| P --> Q; Q --> P |] ==> R"
-  shows "R"
-by (iprover intro: minor impI major [THEN iffD2] major [THEN iffD1])
+  shows R
+  by (iprover intro: minor impI major [THEN iffD2] major [THEN iffD1])
 
 
 subsection {*True*}
 
 lemma TrueI: "True"
-apply (unfold True_def)
-apply (rule refl)
-done
+  by (unfold True_def) (rule refl)
 
 lemma eqTrueI: "P ==> P=True"
-by (iprover intro: iffI TrueI)
+  by (iprover intro: iffI TrueI)
 
 lemma eqTrueE: "P=True ==> P"
 apply (erule iffD2)
@@ -810,6 +799,15 @@
 
 theorems case_split = case_split_thm [case_names True False]
 
+ML {*
+structure ProjectRule = ProjectRuleFun
+(struct
+  val conjunct1 = thm "conjunct1";
+  val conjunct2 = thm "conjunct2";
+  val mp = thm "mp";
+end)
+*}
+
 
 subsubsection {* Intuitionistic Reasoning *}
 
@@ -1146,7 +1144,7 @@
   simp_implies :: "[prop, prop] => prop"  (infixr "=simp=>" 1)
   "simp_implies \<equiv> op ==>"
 
-lemma simp_impliesI: 
+lemma simp_impliesI:
   assumes PQ: "(PROP P \<Longrightarrow> PROP Q)"
   shows "PROP P =simp=> PROP Q"
   apply (unfold simp_implies_def)
@@ -1282,23 +1280,31 @@
 subsection {* Generic cases and induction *}
 
 constdefs
-  induct_forall :: "('a => bool) => bool"
-  "induct_forall P == \<forall>x. P x"
-  induct_implies :: "bool => bool => bool"
-  "induct_implies A B == A --> B"
-  induct_equal :: "'a => 'a => bool"
-  "induct_equal x y == x = y"
-  induct_conj :: "bool => bool => bool"
-  "induct_conj A B == A & B"
+  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_conj_eq:
+  includes meta_conjunction_syntax
+  shows "(A && B) == Trueprop (induct_conj A B)"
+  by (unfold atomize_conj induct_conj_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 induct_forall_conj: "induct_forall (\<lambda>x. induct_conj (A x) (B x)) =
     induct_conj (induct_forall A) (induct_forall B)"
@@ -1311,18 +1317,12 @@
 lemma induct_conj_curry: "(induct_conj A B ==> PROP C) == (A ==> B ==> PROP C)"
 proof
   assume r: "induct_conj A B ==> PROP C" and A B
-  show "PROP C" by (rule r) (simp! add: induct_conj_def)
+  show "PROP C" by (rule r) (simp add: induct_conj_def `A` `B`)
 next
   assume r: "A ==> B ==> PROP C" and "induct_conj A B"
-  show "PROP C" by (rule r) (simp! add: induct_conj_def)+
+  show "PROP C" by (rule r) (simp_all add: `induct_conj A B` [unfolded induct_conj_def])
 qed
 
-lemma induct_impliesI: "(A ==> B) ==> induct_implies A B"
-  by (simp add: induct_implies_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 induct_conj_def
 lemmas induct_conj = induct_forall_conj induct_implies_conj induct_conj_curry
 
 hide const induct_forall induct_implies induct_equal induct_conj
@@ -1333,24 +1333,22 @@
 ML {*
   structure InductMethod = InductMethodFun
   (struct
-    val dest_concls = HOLogic.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")]
+    val rulify = thms "induct_rulify"
+    val rulify_fallback = thms "induct_rulify_fallback"
   end);
 *}
 
 setup InductMethod.setup
 
-subsubsection{*Tags, for the ATP Linkup*}
+
+subsubsection {*Tags, for the ATP Linkup *}
 
 constdefs
   tag :: "bool => bool"
-   "tag P == P"
+  "tag P == P"
 
 text{*These label the distinguished literals of introduction and elimination
 rules.*}
@@ -1370,4 +1368,3 @@
 by (simp add: tag_def)
 
 end
-