Added setup for simplification of equality constraints in induction rules.
authorberghofe
Sun Jan 10 18:03:20 2010 +0100 (2010-01-10)
changeset 34908d546e75631bb
parent 34907 b0aaec87751c
child 34909 a799687944af
Added setup for simplification of equality constraints in induction rules.
src/HOL/HOL.thy
     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.57 +    addsimprocs
    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