src/HOL/simpdata.ML
changeset 16633 208ebc9311f2
parent 16587 b34c8aa657a5
child 16999 307b2ec590ff
     1.1 --- a/src/HOL/simpdata.ML	Fri Jul 01 13:51:11 2005 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Fri Jul 01 13:54:12 2005 +0200
     1.3 @@ -69,6 +69,10 @@
     1.4  val not_imp = thm "not_imp";
     1.5  val not_not = thm "not_not";
     1.6  val rev_conj_cong = thm "rev_conj_cong";
     1.7 +val simp_impliesE = thm "simp_impliesI";
     1.8 +val simp_impliesI = thm "simp_impliesI";
     1.9 +val simp_implies_cong = thm "simp_implies_cong";
    1.10 +val simp_implies_def = thm "simp_implies_def";
    1.11  val simp_thms = thms "simp_thms";
    1.12  val split_if = thm "split_if";
    1.13  val split_if_asm = thm "split_if_asm";
    1.14 @@ -198,11 +202,40 @@
    1.15  fun mk_eq_True r =
    1.16    SOME (r RS meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => NONE;
    1.17  
    1.18 +(* Produce theorems of the form
    1.19 +  (P1 =simp=> ... =simp=> Pn => x == y) ==> (P1 =simp=> ... =simp=> Pn => x = y)
    1.20 +*)
    1.21 +fun lift_meta_eq_to_obj_eq i st =
    1.22 +  let
    1.23 +    val {sign, ...} = rep_thm st;
    1.24 +    fun count_imp (Const ("HOL.simp_implies", _) $ P $ Q) = 1 + count_imp Q
    1.25 +      | count_imp _ = 0;
    1.26 +    val j = count_imp (Logic.strip_assums_concl (List.nth (prems_of st, i - 1)))
    1.27 +  in if j = 0 then meta_eq_to_obj_eq
    1.28 +    else
    1.29 +      let
    1.30 +        val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j);
    1.31 +        fun mk_simp_implies Q = foldr (fn (R, S) =>
    1.32 +          Const ("HOL.simp_implies", propT --> propT --> propT) $ R $ S) Q Ps
    1.33 +        val aT = TFree ("'a", HOLogic.typeS);
    1.34 +        val x = Free ("x", aT);
    1.35 +        val y = Free ("y", aT)
    1.36 +      in prove_goalw_cterm [simp_implies_def]
    1.37 +        (cterm_of sign (Logic.mk_implies
    1.38 +          (mk_simp_implies (Logic.mk_equals (x, y)),
    1.39 +           mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y))))))
    1.40 +        (fn hyps => [REPEAT (ares_tac (meta_eq_to_obj_eq :: hyps) 1)])
    1.41 +      end
    1.42 +  end;
    1.43 +  
    1.44  (*Congruence rules for = (instead of ==)*)
    1.45 -fun mk_meta_cong rl =
    1.46 -  zero_var_indexes(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl))
    1.47 -  handle THM _ =>
    1.48 -  error("Premises and conclusion of congruence rules must be =-equalities");
    1.49 +fun mk_meta_cong rl = zero_var_indexes
    1.50 +  (let val rl' = Seq.hd (TRYALL (fn i => fn st =>
    1.51 +     rtac (lift_meta_eq_to_obj_eq i st) i st) rl)
    1.52 +   in mk_meta_eq rl' handle THM _ =>
    1.53 +     if Logic.is_equals (concl_of rl') then rl'
    1.54 +     else error "Conclusion of congruence rules must be =-equality"
    1.55 +   end);
    1.56  
    1.57  (* Elimination of True from asumptions: *)
    1.58  
    1.59 @@ -263,11 +296,13 @@
    1.60    (List.mapPartial (try mk_eq) o mk_atomize pairs o gen_all);
    1.61  
    1.62  fun unsafe_solver_tac prems =
    1.63 +  (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN'
    1.64    FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems), atac, etac FalseE];
    1.65  val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
    1.66  
    1.67  (*No premature instantiation of variables during simplification*)
    1.68  fun safe_solver_tac prems =
    1.69 +  (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN'
    1.70    FIRST'[match_tac(reflexive_thm::TrueI::refl::prems),
    1.71           eq_assume_tac, ematch_tac [FalseE]];
    1.72  val safe_solver = mk_solver "HOL safe" safe_solver_tac;
    1.73 @@ -298,7 +333,7 @@
    1.74         thm "the_eq_trivial", the_sym_eq_trivial]
    1.75       @ ex_simps @ all_simps @ simp_thms)
    1.76       addsimprocs [defALL_regroup,defEX_regroup,let_simproc]
    1.77 -     addcongs [imp_cong]
    1.78 +     addcongs [imp_cong, simp_implies_cong]
    1.79       addsplits [split_if];
    1.80  
    1.81  fun hol_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews);