tuned;
authorwenzelm
Mon Apr 06 12:37:21 2015 +0200 (2015-04-06)
changeset 59929a090551e5ec8
parent 59927 251fa1530de1
child 59930 bdbc4b761c31
tuned;
src/HOL/HOL.thy
src/Tools/induct.ML
     1.1 --- a/src/HOL/HOL.thy	Sat Apr 04 22:22:38 2015 +0200
     1.2 +++ b/src/HOL/HOL.thy	Mon Apr 06 12:37:21 2015 +0200
     1.3 @@ -1365,44 +1365,32 @@
     1.4  subsubsection {* Generic cases and induction *}
     1.5  
     1.6  text {* Rule projections: *}
     1.7 -
     1.8  ML {*
     1.9  structure Project_Rule = Project_Rule
    1.10  (
    1.11    val conjunct1 = @{thm conjunct1}
    1.12    val conjunct2 = @{thm conjunct2}
    1.13    val mp = @{thm mp}
    1.14 -)
    1.15 +);
    1.16  *}
    1.17  
    1.18 -definition induct_forall where
    1.19 -  "induct_forall P == \<forall>x. P x"
    1.20 -
    1.21 -definition induct_implies where
    1.22 -  "induct_implies A B == A \<longrightarrow> B"
    1.23 -
    1.24 -definition induct_equal where
    1.25 -  "induct_equal x y == x = y"
    1.26 +definition "induct_forall P \<equiv> \<forall>x. P x"
    1.27 +definition "induct_implies A B \<equiv> A \<longrightarrow> B"
    1.28 +definition "induct_equal x y \<equiv> x = y"
    1.29 +definition "induct_conj A B \<equiv> A \<and> B"
    1.30 +definition "induct_true \<equiv> True"
    1.31 +definition "induct_false \<equiv> False"
    1.32  
    1.33 -definition induct_conj where
    1.34 -  "induct_conj A B == A \<and> B"
    1.35 -
    1.36 -definition induct_true where
    1.37 -  "induct_true == True"
    1.38 -
    1.39 -definition induct_false where
    1.40 -  "induct_false == False"
    1.41 -
    1.42 -lemma induct_forall_eq: "(!!x. P x) == Trueprop (induct_forall (\<lambda>x. P x))"
    1.43 +lemma induct_forall_eq: "(\<And>x. P x) \<equiv> Trueprop (induct_forall (\<lambda>x. P x))"
    1.44    by (unfold atomize_all induct_forall_def)
    1.45  
    1.46 -lemma induct_implies_eq: "(A ==> B) == Trueprop (induct_implies A B)"
    1.47 +lemma induct_implies_eq: "(A \<Longrightarrow> B) \<equiv> Trueprop (induct_implies A B)"
    1.48    by (unfold atomize_imp induct_implies_def)
    1.49  
    1.50 -lemma induct_equal_eq: "(x == y) == Trueprop (induct_equal x y)"
    1.51 +lemma induct_equal_eq: "(x \<equiv> y) \<equiv> Trueprop (induct_equal x y)"
    1.52    by (unfold atomize_eq induct_equal_def)
    1.53  
    1.54 -lemma induct_conj_eq: "(A &&& B) == Trueprop (induct_conj A B)"
    1.55 +lemma induct_conj_eq: "(A &&& B) \<equiv> Trueprop (induct_conj A B)"
    1.56    by (unfold atomize_conj induct_conj_def)
    1.57  
    1.58  lemmas induct_atomize' = induct_forall_eq induct_implies_eq induct_conj_eq
    1.59 @@ -1413,7 +1401,6 @@
    1.60    induct_forall_def induct_implies_def induct_equal_def induct_conj_def
    1.61    induct_true_def induct_false_def
    1.62  
    1.63 -
    1.64  lemma induct_forall_conj: "induct_forall (\<lambda>x. induct_conj (A x) (B x)) =
    1.65      induct_conj (induct_forall A) (induct_forall B)"
    1.66    by (unfold induct_forall_def induct_conj_def) iprover
    1.67 @@ -1422,13 +1409,15 @@
    1.68      induct_conj (induct_implies C A) (induct_implies C B)"
    1.69    by (unfold induct_implies_def induct_conj_def) iprover
    1.70  
    1.71 -lemma induct_conj_curry: "(induct_conj A B ==> PROP C) == (A ==> B ==> PROP C)"
    1.72 +lemma induct_conj_curry: "(induct_conj A B \<Longrightarrow> PROP C) \<equiv> (A \<Longrightarrow> B \<Longrightarrow> PROP C)"
    1.73  proof
    1.74 -  assume r: "induct_conj A B ==> PROP C" and A B
    1.75 -  show "PROP C" by (rule r) (simp add: induct_conj_def `A` `B`)
    1.76 +  assume r: "induct_conj A B \<Longrightarrow> PROP C"
    1.77 +  assume ab: A B
    1.78 +  show "PROP C" by (rule r) (simp add: induct_conj_def ab)
    1.79  next
    1.80 -  assume r: "A ==> B ==> PROP C" and "induct_conj A B"
    1.81 -  show "PROP C" by (rule r) (simp_all add: `induct_conj A B` [unfolded induct_conj_def])
    1.82 +  assume r: "A \<Longrightarrow> B \<Longrightarrow> PROP C"
    1.83 +  assume ab: "induct_conj A B"
    1.84 +  show "PROP C" by (rule r) (simp_all add: ab [unfolded induct_conj_def])
    1.85  qed
    1.86  
    1.87  lemmas induct_conj = induct_forall_conj induct_implies_conj induct_conj_curry
    1.88 @@ -1484,52 +1473,54 @@
    1.89  
    1.90  text {* Pre-simplification of induction and cases rules *}
    1.91  
    1.92 -lemma [induct_simp]: "(!!x. induct_equal x t ==> PROP P x) == PROP P t"
    1.93 +lemma [induct_simp]: "(\<And>x. induct_equal x t \<Longrightarrow> PROP P x) \<equiv> PROP P t"
    1.94    unfolding induct_equal_def
    1.95  proof
    1.96 -  assume R: "!!x. x = t ==> PROP P x"
    1.97 -  show "PROP P t" by (rule R [OF refl])
    1.98 +  assume r: "\<And>x. x = t \<Longrightarrow> PROP P x"
    1.99 +  show "PROP P t" by (rule r [OF refl])
   1.100  next
   1.101 -  fix x assume "PROP P t" "x = t"
   1.102 +  fix x
   1.103 +  assume "PROP P t" "x = t"
   1.104    then show "PROP P x" by simp
   1.105  qed
   1.106  
   1.107 -lemma [induct_simp]: "(!!x. induct_equal t x ==> PROP P x) == PROP P t"
   1.108 +lemma [induct_simp]: "(\<And>x. induct_equal t x \<Longrightarrow> PROP P x) \<equiv> PROP P t"
   1.109    unfolding induct_equal_def
   1.110  proof
   1.111 -  assume R: "!!x. t = x ==> PROP P x"
   1.112 -  show "PROP P t" by (rule R [OF refl])
   1.113 +  assume r: "\<And>x. t = x \<Longrightarrow> PROP P x"
   1.114 +  show "PROP P t" by (rule r [OF refl])
   1.115  next
   1.116 -  fix x assume "PROP P t" "t = x"
   1.117 +  fix x
   1.118 +  assume "PROP P t" "t = x"
   1.119    then show "PROP P x" by simp
   1.120  qed
   1.121  
   1.122 -lemma [induct_simp]: "(induct_false ==> P) == Trueprop induct_true"
   1.123 +lemma [induct_simp]: "(induct_false \<Longrightarrow> P) \<equiv> Trueprop induct_true"
   1.124    unfolding induct_false_def induct_true_def
   1.125    by (iprover intro: equal_intr_rule)
   1.126  
   1.127 -lemma [induct_simp]: "(induct_true ==> PROP P) == PROP P"
   1.128 +lemma [induct_simp]: "(induct_true \<Longrightarrow> PROP P) \<equiv> PROP P"
   1.129    unfolding induct_true_def
   1.130  proof
   1.131 -  assume R: "True \<Longrightarrow> PROP P"
   1.132 -  from TrueI show "PROP P" by (rule R)
   1.133 +  assume "True \<Longrightarrow> PROP P"
   1.134 +  then show "PROP P" using TrueI .
   1.135  next
   1.136    assume "PROP P"
   1.137    then show "PROP P" .
   1.138  qed
   1.139  
   1.140 -lemma [induct_simp]: "(PROP P ==> induct_true) == Trueprop induct_true"
   1.141 +lemma [induct_simp]: "(PROP P \<Longrightarrow> induct_true) \<equiv> Trueprop induct_true"
   1.142    unfolding induct_true_def
   1.143    by (iprover intro: equal_intr_rule)
   1.144  
   1.145 -lemma [induct_simp]: "(!!x. induct_true) == Trueprop induct_true"
   1.146 +lemma [induct_simp]: "(\<And>x. induct_true) \<equiv> Trueprop induct_true"
   1.147    unfolding induct_true_def
   1.148    by (iprover intro: equal_intr_rule)
   1.149  
   1.150 -lemma [induct_simp]: "induct_implies induct_true P == P"
   1.151 +lemma [induct_simp]: "induct_implies induct_true P \<equiv> P"
   1.152    by (simp add: induct_implies_def induct_true_def)
   1.153  
   1.154 -lemma [induct_simp]: "(x = x) = True"
   1.155 +lemma [induct_simp]: "x = x \<longleftrightarrow> True"
   1.156    by (rule simp_thms)
   1.157  
   1.158  hide_const induct_forall induct_implies induct_equal induct_conj induct_true induct_false
     2.1 --- a/src/Tools/induct.ML	Sat Apr 04 22:22:38 2015 +0200
     2.2 +++ b/src/Tools/induct.ML	Mon Apr 06 12:37:21 2015 +0200
     2.3 @@ -162,7 +162,7 @@
     2.4  
     2.5  val rearrange_eqs_simproc =
     2.6    Simplifier.simproc_global Pure.thy "rearrange_eqs" ["Pure.all t"]
     2.7 -    (fn ctxt => fn t => mk_swap_rrule ctxt (Thm.global_cterm_of (Proof_Context.theory_of ctxt) t));
     2.8 +    (fn ctxt => fn t => mk_swap_rrule ctxt (Thm.cterm_of ctxt t));
     2.9  
    2.10  
    2.11  (* rotate k premises to the left by j, skipping over first j premises *)
    2.12 @@ -515,7 +515,7 @@
    2.13  
    2.14  (** induct method **)
    2.15  
    2.16 -val conjunction_congs = [@{thm Pure.all_conjunction}, @{thm imp_conjunction}];
    2.17 +val conjunction_congs = @{thms Pure.all_conjunction imp_conjunction};
    2.18  
    2.19  
    2.20  (* atomize *)
    2.21 @@ -549,7 +549,7 @@
    2.22    rewrite_goal_tac ctxt (Induct_Args.rulify @ conjunction_congs) THEN'
    2.23    rewrite_goal_tac ctxt Induct_Args.rulify_fallback THEN'
    2.24    Goal.conjunction_tac THEN_ALL_NEW
    2.25 -  (rewrite_goal_tac ctxt [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac ctxt);
    2.26 +  (rewrite_goal_tac ctxt @{thms Pure.conjunction_imp} THEN' Goal.norm_hhf_tac ctxt);
    2.27  
    2.28  
    2.29  (* prepare rule *)