src/HOL/simpdata.ML
changeset 4640 ac6cf9f18653
parent 4633 d4a074973715
child 4651 70dd492a1698
     1.1 --- a/src/HOL/simpdata.ML	Fri Feb 20 17:33:14 1998 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Fri Feb 20 17:56:39 1998 +0100
     1.3 @@ -52,6 +52,9 @@
     1.4  val DelIffs = seq delIff
     1.5  end;
     1.6  
     1.7 +qed_goal "meta_eq_to_obj_eq" HOL.thy "x==y ==> x=y"
     1.8 +  (fn [prem] => [rewtac prem, rtac refl 1]);
     1.9 +
    1.10  local
    1.11  
    1.12    fun prover s = prove_goal HOL.thy s (K [blast_tac HOL_cs 1]);
    1.13 @@ -95,7 +98,7 @@
    1.14   [ "(x=x) = True",
    1.15     "(~True) = False", "(~False) = True", "(~ ~ P) = P",
    1.16     "(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))",
    1.17 -   "(True=P) = P", "(P=True) = P",
    1.18 +   "(True=P) = P", "(P=True) = P", "(False=P) = (~P)", "(P=False) = (~P)",
    1.19     "(True --> P) = P", "(False --> P) = True", 
    1.20     "(P --> True) = True", "(P --> P) = True",
    1.21     "(P --> False) = (~P)", "(P --> ~P) = (~P)",
    1.22 @@ -115,11 +118,15 @@
    1.23  
    1.24  (*Add congruence rules for = (instead of ==) *)
    1.25  infix 4 addcongs delcongs;
    1.26 -fun ss addcongs congs = ss addeqcongs 
    1.27 -                        (map standard (congs RL [eq_reflection]));
    1.28  
    1.29 -fun ss delcongs congs = ss deleqcongs 
    1.30 -                        (map standard (congs RL [eq_reflection]));
    1.31 +fun mk_meta_cong rl =
    1.32 +  standard(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl))
    1.33 +  handle THM _ =>
    1.34 +  error("Premises and conclusion of congruence rules must be =-equalities");
    1.35 +
    1.36 +fun ss addcongs congs = ss addeqcongs (map mk_meta_cong congs);
    1.37 +
    1.38 +fun ss delcongs congs = ss deleqcongs (map mk_meta_cong congs);
    1.39  
    1.40  fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
    1.41  fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
    1.42 @@ -241,9 +248,6 @@
    1.43  qed_goalw "o_apply" HOL.thy [o_def] "(f o g) x = f (g x)"
    1.44   (K [rtac refl 1]);
    1.45  
    1.46 -qed_goal "meta_eq_to_obj_eq" HOL.thy "x==y ==> x=y"
    1.47 -  (fn [prem] => [rewtac prem, rtac refl 1]);
    1.48 -
    1.49  qed_goalw "if_True" HOL.thy [if_def] "(if True then x else y) = x"
    1.50   (K [Blast_tac 1]);
    1.51  
    1.52 @@ -370,10 +374,10 @@
    1.53     ("All", [spec]), ("True", []), ("False", []),
    1.54     ("If", [if_bool_eq RS iffD1])];
    1.55  
    1.56 -fun unsafe_solver prems = FIRST'[resolve_tac (TrueI::refl::prems),
    1.57 +fun unsafe_solver prems = FIRST'[resolve_tac (reflexive_thm::TrueI::refl::prems),
    1.58  				 atac, etac FalseE];
    1.59  (*No premature instantiation of variables during simplification*)
    1.60 -fun   safe_solver prems = FIRST'[match_tac (TrueI::refl::prems),
    1.61 +fun   safe_solver prems = FIRST'[match_tac (reflexive_thm::TrueI::prems),
    1.62  				 eq_assume_tac, ematch_tac [FalseE]];
    1.63  
    1.64  val HOL_basic_ss = empty_ss setsubgoaler asm_simp_tac