author berghofe Sun Jan 10 18:03:20 2010 +0100 (2010-01-10) changeset 34908 d546e75631bb parent 34907 b0aaec87751c child 34909 a799687944af
Added setup for simplification of equality constraints in induction rules.
 src/HOL/HOL.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/HOL.thy	Sun Jan 10 18:01:04 2010 +0100
1.2 +++ b/src/HOL/HOL.thy	Sun Jan 10 18:03:20 2010 +0100
1.3 @@ -1398,6 +1398,8 @@
1.4    induct_implies where "induct_implies A B == A \<longrightarrow> B"
1.5    induct_equal where "induct_equal x y == x = y"
1.6    induct_conj where "induct_conj A B == A \<and> B"
1.7 +  induct_true where "induct_true == True"
1.8 +  induct_false where "induct_false == False"
1.9
1.10  lemma induct_forall_eq: "(!!x. P x) == Trueprop (induct_forall (\<lambda>x. P x))"
1.11    by (unfold atomize_all induct_forall_def)
1.12 @@ -1411,10 +1413,13 @@
1.13  lemma induct_conj_eq: "(A &&& B) == Trueprop (induct_conj A B)"
1.14    by (unfold atomize_conj induct_conj_def)
1.15
1.16 -lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
1.17 +lemmas induct_atomize' = induct_forall_eq induct_implies_eq induct_conj_eq
1.18 +lemmas induct_atomize = induct_atomize' induct_equal_eq
1.19 +lemmas induct_rulify' [symmetric, standard] = induct_atomize'
1.20  lemmas induct_rulify [symmetric, standard] = induct_atomize
1.21  lemmas induct_rulify_fallback =
1.22    induct_forall_def induct_implies_def induct_equal_def induct_conj_def
1.23 +  induct_true_def induct_false_def
1.24
1.25
1.26  lemma induct_forall_conj: "induct_forall (\<lambda>x. induct_conj (A x) (B x)) =
1.27 @@ -1436,7 +1441,8 @@
1.28
1.29  lemmas induct_conj = induct_forall_conj induct_implies_conj induct_conj_curry
1.30
1.31 -hide const induct_forall induct_implies induct_equal induct_conj
1.32 +lemma induct_trueI: "induct_true"
1.33 +  by (simp add: induct_true_def)
1.34
1.35  text {* Method setup. *}
1.36
1.37 @@ -1445,12 +1451,93 @@
1.38  (
1.39    val cases_default = @{thm case_split}
1.40    val atomize = @{thms induct_atomize}
1.41 -  val rulify = @{thms induct_rulify}
1.42 +  val rulify = @{thms induct_rulify'}
1.43    val rulify_fallback = @{thms induct_rulify_fallback}
1.44 +  fun dest_def (Const (@{const_name induct_equal}, _) \$ t \$ u) = SOME (t, u)
1.45 +    | dest_def _ = NONE
1.46 +  val trivial_tac = match_tac @{thms induct_trueI}
1.47  )
1.48  *}
1.49
1.50 -setup Induct.setup
1.51 +setup {*
1.52 +  Induct.setup #>
1.53 +  Context.theory_map (Induct.map_simpset (fn ss => ss
1.54 +    setmksimps (Simpdata.mksimps Simpdata.mksimps_pairs #>
1.55 +      map (Simplifier.rewrite_rule (map Thm.symmetric
1.56 +        @{thms induct_rulify_fallback induct_true_def induct_false_def})))
1.58 +      [Simplifier.simproc @{theory} "swap_induct_false"
1.59 +         ["induct_false ==> PROP P ==> PROP Q"]
1.60 +         (fn _ => fn _ =>
1.61 +            (fn _ \$ (P as _ \$ @{const induct_false}) \$ (_ \$ Q \$ _) =>
1.62 +                  if P <> Q then SOME Drule.swap_prems_eq else NONE
1.63 +              | _ => NONE)),
1.64 +       Simplifier.simproc @{theory} "induct_equal_conj_curry"
1.65 +         ["induct_conj P Q ==> PROP R"]
1.66 +         (fn _ => fn _ =>
1.67 +            (fn _ \$ (_ \$ P) \$ _ =>
1.68 +                let
1.69 +                  fun is_conj (@{const induct_conj} \$ P \$ Q) =
1.70 +                        is_conj P andalso is_conj Q
1.71 +                    | is_conj (Const (@{const_name induct_equal}, _) \$ _ \$ _) = true
1.72 +                    | is_conj @{const induct_true} = true
1.73 +                    | is_conj @{const induct_false} = true
1.74 +                    | is_conj _ = false
1.75 +                in if is_conj P then SOME @{thm induct_conj_curry} else NONE end
1.76 +              | _ => NONE))]))
1.77 +*}
1.78 +
1.79 +text {* Pre-simplification of induction and cases rules *}
1.80 +
1.81 +lemma [induct_simp]: "(!!x. induct_equal x t ==> PROP P x) == PROP P t"
1.82 +  unfolding induct_equal_def
1.83 +proof
1.84 +  assume R: "!!x. x = t ==> PROP P x"
1.85 +  show "PROP P t" by (rule R [OF refl])
1.86 +next
1.87 +  fix x assume "PROP P t" "x = t"
1.88 +  then show "PROP P x" by simp
1.89 +qed
1.90 +
1.91 +lemma [induct_simp]: "(!!x. induct_equal t x ==> PROP P x) == PROP P t"
1.92 +  unfolding induct_equal_def
1.93 +proof
1.94 +  assume R: "!!x. t = x ==> PROP P x"
1.95 +  show "PROP P t" by (rule R [OF refl])
1.96 +next
1.97 +  fix x assume "PROP P t" "t = x"
1.98 +  then show "PROP P x" by simp
1.99 +qed
1.100 +
1.101 +lemma [induct_simp]: "(induct_false ==> P) == Trueprop induct_true"
1.102 +  unfolding induct_false_def induct_true_def
1.103 +  by (iprover intro: equal_intr_rule)
1.104 +
1.105 +lemma [induct_simp]: "(induct_true ==> PROP P) == PROP P"
1.106 +  unfolding induct_true_def
1.107 +proof
1.108 +  assume R: "True \<Longrightarrow> PROP P"
1.109 +  from TrueI show "PROP P" by (rule R)
1.110 +next
1.111 +  assume "PROP P"
1.112 +  then show "PROP P" .
1.113 +qed
1.114 +
1.115 +lemma [induct_simp]: "(PROP P ==> induct_true) == Trueprop induct_true"
1.116 +  unfolding induct_true_def
1.117 +  by (iprover intro: equal_intr_rule)
1.118 +
1.119 +lemma [induct_simp]: "(!!x. induct_true) == Trueprop induct_true"
1.120 +  unfolding induct_true_def
1.121 +  by (iprover intro: equal_intr_rule)
1.122 +
1.123 +lemma [induct_simp]: "induct_implies induct_true P == P"
1.124 +  by (simp add: induct_implies_def induct_true_def)
1.125 +
1.126 +lemma [induct_simp]: "(x = x) = True"
1.127 +  by (rule simp_thms)
1.128 +
1.129 +hide const induct_forall induct_implies induct_equal induct_conj induct_true induct_false
1.130
1.131  use "~~/src/Tools/induct_tacs.ML"
1.132  setup InductTacs.setup
```