added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
authoroheimb
Sat Feb 15 17:43:27 1997 +0100 (1997-02-15)
changeset 263337c0b5a7ee5d
parent 2632 1612b99395d4
child 2634 b85c77b64c7a
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
safe_asm_more_full_simp_tac
new addss (old version retained as unsafe_addss),
new auto_tac (old version retained as unsafe_auto_tac),
clasimpset with modification functions
src/FOL/simpdata.ML
     1.1 --- a/src/FOL/simpdata.ML	Sat Feb 15 17:35:53 1997 +0100
     1.2 +++ b/src/FOL/simpdata.ML	Sat Feb 15 17:43:27 1997 +0100
     1.3 @@ -187,37 +187,15 @@
     1.4  
     1.5  open Simplifier Induction;
     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  (*Add congruence rules for = or <-> (instead of ==) *)
    1.29 -infix 4 addcongs;
    1.30 +infix 4 addcongs delcongs;
    1.31  fun ss addcongs congs =
    1.32          ss addeqcongs (congs RL [eq_reflection,iff_reflection]);
    1.33 +fun ss delcongs congs =
    1.34 +        ss deleqcongs (congs RL [eq_reflection,iff_reflection]);
    1.35  
    1.36  fun Addcongs congs = (simpset := !simpset addcongs congs);
    1.37 -
    1.38 -(*Add a simpset to a classical set!*)
    1.39 -infix 4 addss;
    1.40 -fun cs addss ss = cs addbefore asm_full_simp_tac ss 1;
    1.41 +fun Delcongs congs = (simpset := !simpset delcongs congs);
    1.42  
    1.43  val IFOL_simps =
    1.44     [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
    1.45 @@ -226,15 +204,19 @@
    1.46  val notFalseI = int_prove_fun "~False";
    1.47  val triv_rls = [TrueI,refl,iff_refl,notFalseI];
    1.48  
    1.49 -val IFOL_ss = 
    1.50 -  empty_ss 
    1.51 -  setmksimps (map mk_meta_eq o atomize o gen_all)
    1.52 -  setsolver  (fn prems => resolve_tac (triv_rls@prems) 
    1.53 -                          ORELSE' assume_tac
    1.54 -                          ORELSE' etac FalseE)
    1.55 -  setsubgoaler asm_simp_tac
    1.56 -  addsimps IFOL_simps
    1.57 -  addcongs [imp_cong];
    1.58 +fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls@prems),
    1.59 +				 atac, etac FalseE];
    1.60 +(*No premature instantiation of variables during simplification*)
    1.61 +fun   safe_solver prems = FIRST'[match_tac (triv_rls@prems),
    1.62 +				 eq_assume_tac, ematch_tac [FalseE]];
    1.63 +
    1.64 +val FOL_basic_ss = empty_ss setsubgoaler asm_simp_tac
    1.65 +			    setSSolver   safe_solver
    1.66 +			    setSolver  unsafe_solver
    1.67 +			    setmksimps (map mk_meta_eq o atomize o gen_all);
    1.68 +
    1.69 +val IFOL_ss = FOL_basic_ss addsimps IFOL_simps
    1.70 +			   addcongs [imp_cong];
    1.71  
    1.72  val cla_simps = 
    1.73      [de_Morgan_conj, de_Morgan_disj, not_all, not_ex, cases_simp] @
    1.74 @@ -267,3 +249,79 @@
    1.75  
    1.76  
    1.77  add_thy_reader_file "thy_data.ML";
    1.78 +
    1.79 +
    1.80 +
    1.81 +
    1.82 +(*** Integration of simplifier with classical reasoner ***)
    1.83 +
    1.84 +(* rot_eq_tac rotates the first equality premise of subgoal i to the front,
    1.85 +   fails if there is no equaliy or if an equality is already at the front *)
    1.86 +fun rot_eq_tac i = let
    1.87 +  fun is_eq (Const ("Trueprop", _) $ (Const("op ="  ,_) $ _ $ _)) = true
    1.88 +  |   is_eq (Const ("Trueprop", _) $ (Const("op <->",_) $ _ $ _)) = true
    1.89 +  |   is_eq _ = false;
    1.90 +  fun find_eq n [] = None
    1.91 +  |   find_eq n (t :: ts) = if (is_eq t) then Some n else find_eq (n + 1) ts;
    1.92 +  fun rot_eq state = let val (_, _, Bi, _) = dest_state (state, i) in
    1.93 +	    (case find_eq 0 (Logic.strip_assums_hyp Bi) of
    1.94 +	      None   => no_tac
    1.95 +	    | Some 0 => no_tac
    1.96 +	    | Some n => rotate_tac n i) end;
    1.97 +in STATE rot_eq end;
    1.98 +
    1.99 +
   1.100 +fun safe_asm_more_full_simp_tac ss = TRY o rot_eq_tac THEN' 
   1.101 +				     safe_asm_full_simp_tac ss;
   1.102 +(*an unsatisfactory fix for the incomplete asm_full_simp_tac!
   1.103 +  better: asm_really_full_simp_tac, a yet to be implemented version of
   1.104 +			asm_full_simp_tac that applies all equalities in the
   1.105 +			premises to all the premises *)
   1.106 +
   1.107 +(*Add a simpset to a classical set!*)
   1.108 +infix 4 addss;
   1.109 +fun cs addss ss = cs addSaltern (CHANGED o (safe_asm_more_full_simp_tac ss));
   1.110 +
   1.111 +(*old version, for compatibility with unstable old proofs*)
   1.112 +infix 4 unsafe_addss;
   1.113 +fun cs unsafe_addss ss = cs addbefore asm_full_simp_tac ss;
   1.114 +
   1.115 +fun Addss ss = (claset := !claset addss ss);
   1.116 +
   1.117 +(*Designed to be idempotent, except if best_tac instantiates variables
   1.118 +  in some of the subgoals*)
   1.119 +(*old version, for compatibility with unstable old proofs*)
   1.120 +fun unsafe_auto_tac (cs,ss) = 
   1.121 +    ALLGOALS (asm_full_simp_tac ss) THEN
   1.122 +    REPEAT (safe_tac cs THEN ALLGOALS (asm_full_simp_tac ss)) THEN
   1.123 +    REPEAT (FIRSTGOAL (best_tac (cs addss ss))) THEN
   1.124 +    prune_params_tac;
   1.125 +
   1.126 +type clasimpset = (claset * simpset);
   1.127 +
   1.128 +val FOL_css = (FOL_cs, FOL_ss);
   1.129 +
   1.130 +fun pair_upd1 f ((a,b),x) = (f(a,x), b);
   1.131 +fun pair_upd2 f ((a,b),x) = (a, f(b,x));
   1.132 +
   1.133 +infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2
   1.134 +	addsimps2 delsimps2 addcongs2 delcongs2;
   1.135 +val op addSIs2   = pair_upd1 (op addSIs);
   1.136 +val op addSEs2   = pair_upd1 (op addSEs);
   1.137 +val op addSDs2   = pair_upd1 (op addSDs);
   1.138 +val op addIs2    = pair_upd1 (op addIs );
   1.139 +val op addEs2    = pair_upd1 (op addEs );
   1.140 +val op addDs2    = pair_upd1 (op addDs );
   1.141 +val op addsimps2 = pair_upd2 (op addsimps);
   1.142 +val op delsimps2 = pair_upd2 (op delsimps);
   1.143 +val op addcongs2 = pair_upd2 (op addcongs);
   1.144 +val op delcongs2 = pair_upd2 (op delcongs);
   1.145 +
   1.146 +fun auto_tac (cs,ss) = let val cs' = cs addss ss in
   1.147 +EVERY [	TRY (safe_tac cs'),
   1.148 +	REPEAT (FIRSTGOAL (fast_tac cs')),
   1.149 +	prune_params_tac] end;
   1.150 +
   1.151 +fun Auto_tac () = auto_tac (!claset, !simpset);
   1.152 +
   1.153 +fun auto () = by (Auto_tac ());