author berghofe Fri Jul 01 13:54:12 2005 +0200 (2005-07-01) changeset 16633 208ebc9311f2 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 file | annotate | diff | revisions src/HOL/simpdata.ML file | annotate | diff | revisions
```     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)