Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
authorberghofe
Fri Jul 01 13:54:12 2005 +0200 (2005-07-01)
changeset 16633208ebc9311f2
parent 16632 ad2895beef79
child 16634 f19d58cfb47a
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
of premises of congruence rules.
src/HOL/HOL.thy
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/HOL.thy	Fri Jul 01 13:51:11 2005 +0200
     1.2 +++ b/src/HOL/HOL.thy	Fri Jul 01 13:54:12 2005 +0200
     1.3 @@ -1122,6 +1122,53 @@
     1.4  lemma Let_unfold: "f x \<equiv> g \<Longrightarrow>  Let x f \<equiv> g"
     1.5    by (unfold Let_def)
     1.6  
     1.7 +text {*
     1.8 +The following copy of the implication operator is useful for
     1.9 +fine-tuning congruence rules.
    1.10 +*}
    1.11 +
    1.12 +consts
    1.13 +  simp_implies :: "[prop, prop] => prop"  ("(_/ =simp=> _)" [2, 1] 1)
    1.14 +defs simp_implies_def: "simp_implies \<equiv> op ==>"
    1.15 +
    1.16 +lemma simp_impliesI: 
    1.17 +  assumes PQ: "(PROP P \<Longrightarrow> PROP Q)"
    1.18 +  shows "PROP P =simp=> PROP Q"
    1.19 +  apply (unfold simp_implies_def)
    1.20 +  apply (rule PQ)
    1.21 +  apply assumption
    1.22 +  done
    1.23 +
    1.24 +lemma simp_impliesE:
    1.25 +  assumes PQ:"PROP P =simp=> PROP Q"
    1.26 +  and P: "PROP P"
    1.27 +  and QR: "PROP Q \<Longrightarrow> PROP R"
    1.28 +  shows "PROP R"
    1.29 +  apply (rule QR)
    1.30 +  apply (rule PQ [unfolded simp_implies_def])
    1.31 +  apply (rule P)
    1.32 +  done
    1.33 +
    1.34 +lemma simp_implies_cong:
    1.35 +  assumes PP' :"PROP P == PROP P'"
    1.36 +  and P'QQ': "PROP P' ==> (PROP Q == PROP Q')"
    1.37 +  shows "(PROP P =simp=> PROP Q) == (PROP P' =simp=> PROP Q')"
    1.38 +proof (unfold simp_implies_def, rule equal_intr_rule)
    1.39 +  assume PQ: "PROP P \<Longrightarrow> PROP Q"
    1.40 +  and P': "PROP P'"
    1.41 +  from PP' [symmetric] and P' have "PROP P"
    1.42 +    by (rule equal_elim_rule1)
    1.43 +  hence "PROP Q" by (rule PQ)
    1.44 +  with P'QQ' [OF P'] show "PROP Q'" by (rule equal_elim_rule1)
    1.45 +next
    1.46 +  assume P'Q': "PROP P' \<Longrightarrow> PROP Q'"
    1.47 +  and P: "PROP P"
    1.48 +  from PP' and P have P': "PROP P'" by (rule equal_elim_rule1)
    1.49 +  hence "PROP Q'" by (rule P'Q')
    1.50 +  with P'QQ' [OF P', symmetric] show "PROP Q"
    1.51 +    by (rule equal_elim_rule1)
    1.52 +qed
    1.53 +
    1.54  subsubsection {* Actual Installation of the Simplifier *}
    1.55  
    1.56  use "simpdata.ML"
     2.1 --- a/src/HOL/simpdata.ML	Fri Jul 01 13:51:11 2005 +0200
     2.2 +++ b/src/HOL/simpdata.ML	Fri Jul 01 13:54:12 2005 +0200
     2.3 @@ -69,6 +69,10 @@
     2.4  val not_imp = thm "not_imp";
     2.5  val not_not = thm "not_not";
     2.6  val rev_conj_cong = thm "rev_conj_cong";
     2.7 +val simp_impliesE = thm "simp_impliesI";
     2.8 +val simp_impliesI = thm "simp_impliesI";
     2.9 +val simp_implies_cong = thm "simp_implies_cong";
    2.10 +val simp_implies_def = thm "simp_implies_def";
    2.11  val simp_thms = thms "simp_thms";
    2.12  val split_if = thm "split_if";
    2.13  val split_if_asm = thm "split_if_asm";
    2.14 @@ -198,11 +202,40 @@
    2.15  fun mk_eq_True r =
    2.16    SOME (r RS meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => NONE;
    2.17  
    2.18 +(* Produce theorems of the form
    2.19 +  (P1 =simp=> ... =simp=> Pn => x == y) ==> (P1 =simp=> ... =simp=> Pn => x = y)
    2.20 +*)
    2.21 +fun lift_meta_eq_to_obj_eq i st =
    2.22 +  let
    2.23 +    val {sign, ...} = rep_thm st;
    2.24 +    fun count_imp (Const ("HOL.simp_implies", _) $ P $ Q) = 1 + count_imp Q
    2.25 +      | count_imp _ = 0;
    2.26 +    val j = count_imp (Logic.strip_assums_concl (List.nth (prems_of st, i - 1)))
    2.27 +  in if j = 0 then meta_eq_to_obj_eq
    2.28 +    else
    2.29 +      let
    2.30 +        val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j);
    2.31 +        fun mk_simp_implies Q = foldr (fn (R, S) =>
    2.32 +          Const ("HOL.simp_implies", propT --> propT --> propT) $ R $ S) Q Ps
    2.33 +        val aT = TFree ("'a", HOLogic.typeS);
    2.34 +        val x = Free ("x", aT);
    2.35 +        val y = Free ("y", aT)
    2.36 +      in prove_goalw_cterm [simp_implies_def]
    2.37 +        (cterm_of sign (Logic.mk_implies
    2.38 +          (mk_simp_implies (Logic.mk_equals (x, y)),
    2.39 +           mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y))))))
    2.40 +        (fn hyps => [REPEAT (ares_tac (meta_eq_to_obj_eq :: hyps) 1)])
    2.41 +      end
    2.42 +  end;
    2.43 +  
    2.44  (*Congruence rules for = (instead of ==)*)
    2.45 -fun mk_meta_cong rl =
    2.46 -  zero_var_indexes(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl))
    2.47 -  handle THM _ =>
    2.48 -  error("Premises and conclusion of congruence rules must be =-equalities");
    2.49 +fun mk_meta_cong rl = zero_var_indexes
    2.50 +  (let val rl' = Seq.hd (TRYALL (fn i => fn st =>
    2.51 +     rtac (lift_meta_eq_to_obj_eq i st) i st) rl)
    2.52 +   in mk_meta_eq rl' handle THM _ =>
    2.53 +     if Logic.is_equals (concl_of rl') then rl'
    2.54 +     else error "Conclusion of congruence rules must be =-equality"
    2.55 +   end);
    2.56  
    2.57  (* Elimination of True from asumptions: *)
    2.58  
    2.59 @@ -263,11 +296,13 @@
    2.60    (List.mapPartial (try mk_eq) o mk_atomize pairs o gen_all);
    2.61  
    2.62  fun unsafe_solver_tac prems =
    2.63 +  (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN'
    2.64    FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems), atac, etac FalseE];
    2.65  val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
    2.66  
    2.67  (*No premature instantiation of variables during simplification*)
    2.68  fun safe_solver_tac prems =
    2.69 +  (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN'
    2.70    FIRST'[match_tac(reflexive_thm::TrueI::refl::prems),
    2.71           eq_assume_tac, ematch_tac [FalseE]];
    2.72  val safe_solver = mk_solver "HOL safe" safe_solver_tac;
    2.73 @@ -298,7 +333,7 @@
    2.74         thm "the_eq_trivial", the_sym_eq_trivial]
    2.75       @ ex_simps @ all_simps @ simp_thms)
    2.76       addsimprocs [defALL_regroup,defEX_regroup,let_simproc]
    2.77 -     addcongs [imp_cong]
    2.78 +     addcongs [imp_cong, simp_implies_cong]
    2.79       addsplits [split_if];
    2.80  
    2.81  fun hol_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews);