src/HOL/HOL.thy
 changeset 59929 a090551e5ec8 parent 59864 c777743294e1 child 59940 087d81f5213e
```     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
```