# HG changeset patch # User oheimb # Date 856025299 -3600 # Node ID 4b30dbe4a0209af807600c5504ceefa170c20628 # Parent 835820c1591d99a5dc9a5df1e5f3dcb6a3f375e7 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), diff -r 835820c1591d -r 4b30dbe4a020 src/HOL/simpdata.ML --- a/src/HOL/simpdata.ML Sat Feb 15 17:45:08 1997 +0100 +++ b/src/HOL/simpdata.ML Sat Feb 15 17:48:19 1997 +0100 @@ -10,27 +10,6 @@ open Simplifier; -(*** Integration of simplifier with classical reasoner ***) - -(*Add a simpset to a classical set!*) -infix 4 addss; -fun cs addss ss = cs addbefore asm_full_simp_tac ss 1; - -fun Addss ss = (claset := !claset addbefore asm_full_simp_tac ss 1); - -(*Designed to be idempotent, except if best_tac instantiates variables - in some of the subgoals*) -fun auto_tac (cs,ss) = - ALLGOALS (asm_full_simp_tac ss) THEN - REPEAT (safe_tac cs THEN ALLGOALS (asm_full_simp_tac ss)) THEN - REPEAT (FIRSTGOAL (best_tac (cs addss ss))) THEN - prune_params_tac; - -fun Auto_tac() = auto_tac (!claset, !simpset); - -fun auto() = by (Auto_tac()); - - (*** Addition of rules to simpsets and clasets simultaneously ***) (*Takes UNCONDITIONAL theorems of the form A<->B to @@ -126,10 +105,12 @@ "(! x. x=t --> P(x)) = P(t)", "(! x. t=x --> P(x)) = P(t)" ]; (*Add congruence rules for = (instead of ==) *) -infix 4 addcongs; +infix 4 addcongs delcongs; fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection]); +fun ss delcongs congs = ss deleqcongs (congs RL [eq_reflection]); fun Addcongs congs = (simpset := !simpset addcongs congs); +fun Delcongs congs = (simpset := !simpset delcongs congs); fun mksimps pairs = map mk_meta_eq o atomize pairs o gen_all; @@ -307,24 +288,24 @@ ("All", [spec]), ("True", []), ("False", []), ("If", [if_bool_eq RS iffD1])]; -val HOL_base_ss = empty_ss - setmksimps (mksimps mksimps_pairs) - setsubgoaler asm_simp_tac; - -val HOL_min_ss = HOL_base_ss setsolver (fn ps => - FIRST'[resolve_tac (TrueI::refl::ps), atac, etac FalseE]); +fun unsafe_solver prems = FIRST'[resolve_tac (TrueI::refl::prems), + atac, etac FalseE]; +(*No premature instantiation of variables during simplification*) +fun safe_solver prems = FIRST'[match_tac (TrueI::refl::prems), + eq_assume_tac, ematch_tac [FalseE]]; -val HOL_safe_min_ss = HOL_base_ss setsolver (fn ps => - FIRST'[match_tac (TrueI::refl::ps), eq_assume_tac, ematch_tac[FalseE]]); +val HOL_basic_ss = empty_ss setsubgoaler asm_simp_tac + setSSolver safe_solver + setSolver unsafe_solver + setmksimps (mksimps mksimps_pairs); -val HOL_ss = HOL_min_ss - addsimps ([triv_forall_equality, (* prunes params *) - if_True, if_False, if_cancel, - o_apply, imp_disjL, conj_assoc, disj_assoc, - de_Morgan_conj, de_Morgan_disj, not_all, not_ex, cases_simp] - @ ex_simps @ all_simps @ simp_thms) - addcongs [imp_cong]; - +val HOL_ss = HOL_basic_ss addsimps ([triv_forall_equality, (* prunes params *) + if_True, if_False, if_cancel, + o_apply, imp_disjL, conj_assoc, disj_assoc, + de_Morgan_conj, de_Morgan_disj, + not_all, not_ex, cases_simp] + @ ex_simps @ all_simps @ simp_thms) + addcongs [imp_cong]; qed_goal "if_distrib" HOL.thy "f(if c then x else y) = (if c then f x else f y)" @@ -373,3 +354,78 @@ add_thy_reader_file "thy_data.ML"; + + + + +(*** Integration of simplifier with classical reasoner ***) + +(* rot_eq_tac rotates the first equality premise of subgoal i to the front, + fails if there is no equaliy or if an equality is already at the front *) +fun rot_eq_tac i = let + fun is_eq (Const ("Trueprop", _) $ (Const("op =",_) $ _ $ _)) = true + | is_eq _ = false; + fun find_eq n [] = None + | find_eq n (t :: ts) = if (is_eq t) then Some n else find_eq (n + 1) ts; + fun rot_eq state = let val (_, _, Bi, _) = dest_state (state, i) in + (case find_eq 0 (Logic.strip_assums_hyp Bi) of + None => no_tac + | Some 0 => no_tac + | Some n => rotate_tac n i) end; +in STATE rot_eq end; + +(*an unsatisfactory fix for the incomplete asm_full_simp_tac! + better: asm_really_full_simp_tac, a yet to be implemented version of + asm_full_simp_tac that applies all equalities in the + premises to all the premises *) +fun safe_asm_more_full_simp_tac ss = TRY o rot_eq_tac THEN' + safe_asm_full_simp_tac ss; + +(*Add a simpset to a classical set!*) +infix 4 addss; +fun cs addss ss = cs addSaltern (CHANGED o (safe_asm_more_full_simp_tac ss)); +(*old version, for compatibility with unstable old proofs*) +infix 4 unsafe_addss; +fun cs unsafe_addss ss = cs addbefore asm_full_simp_tac ss; + +fun Addss ss = (claset := !claset addss ss); +(*old version, for compatibility with unstable old proofs*) +fun Unsafe_Addss ss = (claset := !claset unsafe_addss ss); + +(*Designed to be idempotent, except if best_tac instantiates variables + in some of the subgoals*) +(*old version, for compatibility with unstable old proofs*) +fun unsafe_auto_tac (cs,ss) = + ALLGOALS (asm_full_simp_tac ss) THEN + REPEAT (safe_tac cs THEN ALLGOALS (asm_full_simp_tac ss)) THEN + REPEAT (FIRSTGOAL (best_tac (cs addss ss))) THEN + prune_params_tac; + +type clasimpset = (claset * simpset); + +val HOL_css = (HOL_cs, HOL_ss); + +fun pair_upd1 f ((a,b),x) = (f(a,x), b); +fun pair_upd2 f ((a,b),x) = (a, f(b,x)); + +infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2 + addsimps2 delsimps2 addcongs2 delcongs2; +val op addSIs2 = pair_upd1 (op addSIs); +val op addSEs2 = pair_upd1 (op addSEs); +val op addSDs2 = pair_upd1 (op addSDs); +val op addIs2 = pair_upd1 (op addIs ); +val op addEs2 = pair_upd1 (op addEs ); +val op addDs2 = pair_upd1 (op addDs ); +val op addsimps2 = pair_upd2 (op addsimps); +val op delsimps2 = pair_upd2 (op delsimps); +val op addcongs2 = pair_upd2 (op addcongs); +val op delcongs2 = pair_upd2 (op delcongs); + +fun auto_tac (cs,ss) = let val cs' = cs addss ss in +EVERY [ TRY (safe_tac cs'), + REPEAT (FIRSTGOAL (fast_tac cs')), + prune_params_tac] end; + +fun Auto_tac () = auto_tac (!claset, !simpset); + +fun auto () = by (Auto_tac ());