added delcongs, Delcongs, unsafe_solver, safe_solver, HOL_basic_ss,
authoroheimb
Sat Feb 15 17:48:19 1997 +0100 (1997-02-15)
changeset 26364b30dbe4a020
parent 2635 835820c1591d
child 2637 e9b203f854ae
added delcongs, Delcongs, unsafe_solver, safe_solver, HOL_basic_ss,
safe_asm_more_full_simp_ta, clasimpset HOL_css with modification functions
new addss (old version retained as unsafe_addss),
new Addss (old version retained as Unsafe_Addss),
new auto_tac (old version retained as unsafe_auto_tac),
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Sat Feb 15 17:45:08 1997 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Sat Feb 15 17:48:19 1997 +0100
     1.3 @@ -10,27 +10,6 @@
     1.4  
     1.5  open Simplifier;
     1.6  
     1.7 -(*** Integration of simplifier with classical reasoner ***)
     1.8 -
     1.9 -(*Add a simpset to a classical set!*)
    1.10 -infix 4 addss;
    1.11 -fun cs addss ss = cs addbefore asm_full_simp_tac ss 1;
    1.12 -
    1.13 -fun Addss ss = (claset := !claset addbefore asm_full_simp_tac ss 1);
    1.14 -
    1.15 -(*Designed to be idempotent, except if best_tac instantiates variables
    1.16 -  in some of the subgoals*)
    1.17 -fun auto_tac (cs,ss) = 
    1.18 -    ALLGOALS (asm_full_simp_tac ss) THEN
    1.19 -    REPEAT (safe_tac cs THEN ALLGOALS (asm_full_simp_tac ss)) THEN
    1.20 -    REPEAT (FIRSTGOAL (best_tac (cs addss ss))) THEN
    1.21 -    prune_params_tac;
    1.22 -
    1.23 -fun Auto_tac() = auto_tac (!claset, !simpset);
    1.24 -
    1.25 -fun auto() = by (Auto_tac());
    1.26 -
    1.27 -
    1.28  (*** Addition of rules to simpsets and clasets simultaneously ***)
    1.29  
    1.30  (*Takes UNCONDITIONAL theorems of the form A<->B to 
    1.31 @@ -126,10 +105,12 @@
    1.32     "(! x. x=t --> P(x)) = P(t)", "(! x. t=x --> P(x)) = P(t)" ];
    1.33  
    1.34  (*Add congruence rules for = (instead of ==) *)
    1.35 -infix 4 addcongs;
    1.36 +infix 4 addcongs delcongs;
    1.37  fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection]);
    1.38 +fun ss delcongs congs = ss deleqcongs (congs RL [eq_reflection]);
    1.39  
    1.40  fun Addcongs congs = (simpset := !simpset addcongs congs);
    1.41 +fun Delcongs congs = (simpset := !simpset delcongs congs);
    1.42  
    1.43  fun mksimps pairs = map mk_meta_eq o atomize pairs o gen_all;
    1.44  
    1.45 @@ -307,24 +288,24 @@
    1.46     ("All", [spec]), ("True", []), ("False", []),
    1.47     ("If", [if_bool_eq RS iffD1])];
    1.48  
    1.49 -val HOL_base_ss = empty_ss
    1.50 -      setmksimps (mksimps mksimps_pairs)
    1.51 -      setsubgoaler asm_simp_tac;
    1.52 -
    1.53 -val HOL_min_ss = HOL_base_ss setsolver (fn ps => 
    1.54 -	FIRST'[resolve_tac (TrueI::refl::ps), atac, etac FalseE]);
    1.55 +fun unsafe_solver prems = FIRST'[resolve_tac (TrueI::refl::prems),
    1.56 +				 atac, etac FalseE];
    1.57 +(*No premature instantiation of variables during simplification*)
    1.58 +fun   safe_solver prems = FIRST'[match_tac (TrueI::refl::prems),
    1.59 +				 eq_assume_tac, ematch_tac [FalseE]];
    1.60  
    1.61 -val HOL_safe_min_ss = HOL_base_ss setsolver (fn ps => 
    1.62 -	FIRST'[match_tac (TrueI::refl::ps), eq_assume_tac, ematch_tac[FalseE]]);
    1.63 +val HOL_basic_ss = empty_ss setsubgoaler asm_simp_tac
    1.64 +			    setSSolver   safe_solver
    1.65 +			    setSolver  unsafe_solver
    1.66 +			    setmksimps (mksimps mksimps_pairs);
    1.67  
    1.68 -val HOL_ss = HOL_min_ss
    1.69 -      addsimps ([triv_forall_equality, (* prunes params *)
    1.70 -                 if_True, if_False, if_cancel,
    1.71 -		 o_apply, imp_disjL, conj_assoc, disj_assoc,
    1.72 -                 de_Morgan_conj, de_Morgan_disj, not_all, not_ex, cases_simp]
    1.73 -        @ ex_simps @ all_simps @ simp_thms)
    1.74 -      addcongs [imp_cong];
    1.75 -
    1.76 +val HOL_ss = HOL_basic_ss addsimps ([triv_forall_equality, (* prunes params *)
    1.77 +				     if_True, if_False, if_cancel,
    1.78 +				     o_apply, imp_disjL, conj_assoc, disj_assoc,
    1.79 +				     de_Morgan_conj, de_Morgan_disj, 
    1.80 +				     not_all, not_ex, cases_simp]
    1.81 +				    @ ex_simps @ all_simps @ simp_thms)
    1.82 +			  addcongs [imp_cong];
    1.83  
    1.84  qed_goal "if_distrib" HOL.thy
    1.85    "f(if c then x else y) = (if c then f x else f y)" 
    1.86 @@ -373,3 +354,78 @@
    1.87  
    1.88  
    1.89  add_thy_reader_file "thy_data.ML";
    1.90 +
    1.91 +
    1.92 +
    1.93 +
    1.94 +(*** Integration of simplifier with classical reasoner ***)
    1.95 +
    1.96 +(* rot_eq_tac rotates the first equality premise of subgoal i to the front,
    1.97 +   fails if there is no equaliy or if an equality is already at the front *)
    1.98 +fun rot_eq_tac i = let
    1.99 +  fun is_eq (Const ("Trueprop", _) $ (Const("op =",_) $ _ $ _)) = true
   1.100 +  |   is_eq _ = false;
   1.101 +  fun find_eq n [] = None
   1.102 +  |   find_eq n (t :: ts) = if (is_eq t) then Some n else find_eq (n + 1) ts;
   1.103 +  fun rot_eq state = let val (_, _, Bi, _) = dest_state (state, i) in
   1.104 +	    (case find_eq 0 (Logic.strip_assums_hyp Bi) of
   1.105 +	      None   => no_tac
   1.106 +	    | Some 0 => no_tac
   1.107 +	    | Some n => rotate_tac n i) end;
   1.108 +in STATE rot_eq end;
   1.109 +
   1.110 +(*an unsatisfactory fix for the incomplete asm_full_simp_tac!
   1.111 +  better: asm_really_full_simp_tac, a yet to be implemented version of
   1.112 +			asm_full_simp_tac that applies all equalities in the
   1.113 +			premises to all the premises *)
   1.114 +fun safe_asm_more_full_simp_tac ss = TRY o rot_eq_tac THEN' 
   1.115 +				     safe_asm_full_simp_tac ss;
   1.116 +
   1.117 +(*Add a simpset to a classical set!*)
   1.118 +infix 4 addss;
   1.119 +fun cs addss ss = cs addSaltern (CHANGED o (safe_asm_more_full_simp_tac ss));
   1.120 +(*old version, for compatibility with unstable old proofs*)
   1.121 +infix 4 unsafe_addss;
   1.122 +fun cs unsafe_addss ss = cs addbefore asm_full_simp_tac ss;
   1.123 +
   1.124 +fun Addss ss = (claset := !claset addss ss);
   1.125 +(*old version, for compatibility with unstable old proofs*)
   1.126 +fun Unsafe_Addss ss = (claset := !claset unsafe_addss ss);
   1.127 +
   1.128 +(*Designed to be idempotent, except if best_tac instantiates variables
   1.129 +  in some of the subgoals*)
   1.130 +(*old version, for compatibility with unstable old proofs*)
   1.131 +fun unsafe_auto_tac (cs,ss) = 
   1.132 +    ALLGOALS (asm_full_simp_tac ss) THEN
   1.133 +    REPEAT   (safe_tac cs THEN ALLGOALS (asm_full_simp_tac ss)) THEN
   1.134 +    REPEAT   (FIRSTGOAL (best_tac (cs addss ss))) THEN
   1.135 +    prune_params_tac;
   1.136 +
   1.137 +type clasimpset = (claset * simpset);
   1.138 +
   1.139 +val HOL_css = (HOL_cs, HOL_ss);
   1.140 +
   1.141 +fun pair_upd1 f ((a,b),x) = (f(a,x), b);
   1.142 +fun pair_upd2 f ((a,b),x) = (a, f(b,x));
   1.143 +
   1.144 +infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2
   1.145 +	addsimps2 delsimps2 addcongs2 delcongs2;
   1.146 +val op addSIs2   = pair_upd1 (op addSIs);
   1.147 +val op addSEs2   = pair_upd1 (op addSEs);
   1.148 +val op addSDs2   = pair_upd1 (op addSDs);
   1.149 +val op addIs2    = pair_upd1 (op addIs );
   1.150 +val op addEs2    = pair_upd1 (op addEs );
   1.151 +val op addDs2    = pair_upd1 (op addDs );
   1.152 +val op addsimps2 = pair_upd2 (op addsimps);
   1.153 +val op delsimps2 = pair_upd2 (op delsimps);
   1.154 +val op addcongs2 = pair_upd2 (op addcongs);
   1.155 +val op delcongs2 = pair_upd2 (op delcongs);
   1.156 +
   1.157 +fun auto_tac (cs,ss) = let val cs' = cs addss ss in
   1.158 +EVERY [	TRY (safe_tac cs'),
   1.159 +	REPEAT (FIRSTGOAL (fast_tac cs')),
   1.160 +	prune_params_tac] end;
   1.161 +
   1.162 +fun Auto_tac () = auto_tac (!claset, !simpset);
   1.163 +
   1.164 +fun auto () = by (Auto_tac ());