# HG changeset patch # User wenzelm # Date 1169394226 -3600 # Node ID f4ed4d940d44a02d1e521e91e78221b95d217955 # Parent d8cbb198e096e961dea9ec9314a29addcef07fcf simplified ML setup; diff -r d8cbb198e096 -r f4ed4d940d44 src/HOL/simpdata.ML --- a/src/HOL/simpdata.ML Sun Jan 21 16:43:45 2007 +0100 +++ b/src/HOL/simpdata.ML Sun Jan 21 16:43:46 2007 +0100 @@ -20,60 +20,47 @@ val conj = HOLogic.conj val imp = HOLogic.imp (*rules*) - val iff_reflection = thm "eq_reflection" - val iffI = thm "iffI" - val iff_trans = thm "trans" - val conjI= thm "conjI" - val conjE= thm "conjE" - val impI = thm "impI" - val mp = thm "mp" - val uncurry = thm "uncurry" - val exI = thm "exI" - val exE = thm "exE" - val iff_allI = thm "iff_allI" - val iff_exI = thm "iff_exI" - val all_comm = thm "all_comm" - val ex_comm = thm "ex_comm" + val iff_reflection = @{thm eq_reflection} + val iffI = @{thm iffI} + val iff_trans = @{thm trans} + val conjI= @{thm conjI} + val conjE= @{thm conjE} + val impI = @{thm impI} + val mp = @{thm mp} + val uncurry = @{thm uncurry} + val exI = @{thm exI} + val exE = @{thm exE} + val iff_allI = @{thm iff_allI} + val iff_exI = @{thm iff_exI} + val all_comm = @{thm all_comm} + val ex_comm = @{thm ex_comm} end); structure Simpdata = struct -local - val eq_reflection = thm "eq_reflection" -in fun mk_meta_eq r = r RS eq_reflection end; +fun mk_meta_eq r = r RS @{thm eq_reflection}; fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r; -local - val Eq_FalseI = thm "Eq_FalseI" - val Eq_TrueI = thm "Eq_TrueI" -in fun mk_eq th = case concl_of th +fun mk_eq th = case concl_of th (*expects Trueprop if not == *) of Const ("==",_) $ _ $ _ => th | _ $ (Const ("op =", _) $ _ $ _) => mk_meta_eq th - | _ $ (Const ("Not", _) $ _) => th RS Eq_FalseI - | _ => th RS Eq_TrueI -end; + | _ $ (Const ("Not", _) $ _) => th RS @{thm Eq_FalseI} + | _ => th RS @{thm Eq_TrueI} -local - val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq" - val Eq_TrueI = thm "Eq_TrueI" -in fun mk_eq_True r = - SOME (r RS meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => NONE; -end; +fun mk_eq_True r = + SOME (r RS @{thm meta_eq_to_obj_eq} RS @{thm Eq_TrueI}) handle Thm.THM _ => NONE; (* Produce theorems of the form (P1 =simp=> ... =simp=> Pn => x == y) ==> (P1 =simp=> ... =simp=> Pn => x = y) *) -local - val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq" - val simp_implies_def = thm "simp_implies_def" -in fun lift_meta_eq_to_obj_eq i st = +fun lift_meta_eq_to_obj_eq i st = let fun count_imp (Const ("HOL.simp_implies", _) $ P $ Q) = 1 + count_imp Q | count_imp _ = 0; val j = count_imp (Logic.strip_assums_concl (List.nth (prems_of st, i - 1))) - in if j = 0 then meta_eq_to_obj_eq + in if j = 0 then @{thm meta_eq_to_obj_eq} else let val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j); @@ -86,11 +73,11 @@ [mk_simp_implies (Logic.mk_equals (x, y))] (mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y)))) (fn prems => EVERY - [rewrite_goals_tac [simp_implies_def], - REPEAT (ares_tac (meta_eq_to_obj_eq :: map (rewrite_rule [simp_implies_def]) prems) 1)]) + [rewrite_goals_tac @{thms simp_implies_def}, + REPEAT (ares_tac (@{thm meta_eq_to_obj_eq} :: + map (rewrite_rule @{thms simp_implies_def}) prems) 1)]) end end; -end; (*Congruence rules for = (instead of ==)*) fun mk_meta_cong rl = zero_var_indexes @@ -123,42 +110,33 @@ fun mksimps pairs = map_filter (try mk_eq) o mk_atomize pairs o gen_all; -local - val simp_impliesI = thm "simp_impliesI" - val TrueI = thm "TrueI" - val FalseE = thm "FalseE" - val refl = thm "refl" -in fun unsafe_solver_tac prems = - (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN' - FIRST'[resolve_tac(reflexive_thm :: TrueI :: refl :: prems), atac, etac FalseE]; -end; +fun unsafe_solver_tac prems = + (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN' + FIRST' [resolve_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: prems), atac, + etac @{thm FalseE}]; + val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac; (*No premature instantiation of variables during simplification*) -local - val simp_impliesI = thm "simp_impliesI" - val TrueI = thm "TrueI" - val FalseE = thm "FalseE" - val refl = thm "refl" -in fun safe_solver_tac prems = - (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN' - FIRST'[match_tac(reflexive_thm :: TrueI :: refl :: prems), - eq_assume_tac, ematch_tac [FalseE]]; -end; +fun safe_solver_tac prems = + (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN' + FIRST' [match_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: prems), + eq_assume_tac, ematch_tac @{thms FalseE}]; + val safe_solver = mk_solver "HOL safe" safe_solver_tac; structure SplitterData = struct structure Simplifier = Simplifier val mk_eq = mk_eq - val meta_eq_to_iff = thm "meta_eq_to_obj_eq" - val iffD = thm "iffD2" - val disjE = thm "disjE" - val conjE = thm "conjE" - val exE = thm "exE" - val contrapos = thm "contrapos_nn" - val contrapos2 = thm "contrapos_pp" - val notnotD = thm "notnotD" + val meta_eq_to_iff = @{thm meta_eq_to_obj_eq} + val iffD = @{thm iffD2} + val disjE = @{thm disjE} + val conjE = @{thm conjE} + val exE = @{thm exE} + val contrapos = @{thm contrapos_nn} + val contrapos2 = @{thm contrapos_pp} + val notnotD = @{thm notnotD} end; structure Splitter = SplitterFun(SplitterData); @@ -177,19 +155,19 @@ structure Clasimp = ClasimpFun (structure Simplifier = Simplifier and Splitter = Splitter and Classical = Classical and Blast = Blast - val iffD1 = thm "iffD1" val iffD2 = thm "iffD2" val notE = thm "notE"); + val iffD1 = @{thm iffD1} val iffD2 = @{thm iffD2} val notE = @{thm notE}); open Clasimp; val _ = ML_Context.value_antiq "clasimpset" (Scan.succeed ("clasimpset", "Clasimp.local_clasimpset_of (ML_Context.the_local_context ())")); val mksimps_pairs = - [("op -->", [thm "mp"]), ("op &", [thm "conjunct1", thm "conjunct2"]), - ("All", [thm "spec"]), ("True", []), ("False", []), - ("HOL.If", [thm "if_bool_eq_conj" RS thm "iffD1"])]; + [("op -->", [@{thm mp}]), ("op &", [@{thm conjunct1}, @{thm conjunct2}]), + ("All", [@{thm spec}]), ("True", []), ("False", []), + ("HOL.If", [@{thm if_bool_eq_conj} RS @{thm iffD1}])]; val HOL_basic_ss = - Simplifier.theory_context (the_context ()) empty_ss + Simplifier.theory_context @{theory} empty_ss setsubgoaler asm_simp_tac setSSolver safe_solver setSolver unsafe_solver @@ -212,8 +190,7 @@ val use_neq_simproc = ref true; local - val thy = the_context (); - val neq_to_EQ_False = thm "not_sym" RS thm "Eq_FalseI"; + val neq_to_EQ_False = @{thm not_sym} RS @{thm Eq_FalseI}; fun neq_prover sg ss (eq $ lhs $ rhs) = let fun test thm = (case #prop (rep_thm thm) of @@ -228,7 +205,7 @@ end in -val neq_simproc = Simplifier.simproc thy "neq_simproc" ["x = y"] neq_prover; +val neq_simproc = Simplifier.simproc @{theory} "neq_simproc" ["x = y"] neq_prover; end; @@ -238,22 +215,18 @@ val use_let_simproc = ref true; local - val thy = the_context (); - val Let_folded = thm "Let_folded"; - val Let_unfold = thm "Let_unfold"; - val Let_def = thm "Let_def"; val (f_Let_unfold, x_Let_unfold) = - let val [(_$(f$x)$_)] = prems_of Let_unfold - in (cterm_of thy f, cterm_of thy x) end + let val [(_$(f$x)$_)] = prems_of @{thm Let_unfold} + in (cterm_of @{theory} f, cterm_of @{theory} x) end val (f_Let_folded, x_Let_folded) = - let val [(_$(f$x)$_)] = prems_of Let_folded - in (cterm_of thy f, cterm_of thy x) end; + let val [(_$(f$x)$_)] = prems_of @{thm Let_folded} + in (cterm_of @{theory} f, cterm_of @{theory} x) end; val g_Let_folded = - let val [(_$_$(g$_))] = prems_of Let_folded in cterm_of thy g end; + let val [(_$_$(g$_))] = prems_of @{thm Let_folded} in cterm_of @{theory} g end; in val let_simproc = - Simplifier.simproc thy "let_simp" ["Let x f"] + Simplifier.simproc @{theory} "let_simp" ["Let x f"] (fn sg => fn ss => fn t => let val ctxt = Simplifier.the_context ss; val ([t'], ctxt') = Variable.import_terms false [t] ctxt; @@ -261,7 +234,7 @@ (case t' of (Const ("Let",_)$x$f) => (* x and f are already in normal form *) if not (!use_let_simproc) then NONE else if is_Free x orelse is_Bound x orelse is_Const x - then SOME Let_def + then SOME @{thm Let_def} else let val n = case f of (Abs (x,_,_)) => x | _ => "x"; @@ -274,7 +247,8 @@ in (if (g aconv g') then let - val rl = cterm_instantiate [(f_Let_unfold,cf),(x_Let_unfold,cx)] Let_unfold; + val rl = + cterm_instantiate [(f_Let_unfold,cf),(x_Let_unfold,cx)] @{thm Let_unfold}; in SOME (rl OF [fx_g]) end else if Term.betapply (f,x) aconv g then NONE (*avoid identity conversion*) else let @@ -284,7 +258,7 @@ val rl = cterm_instantiate [(f_Let_folded,cterm_of sg f),(x_Let_folded,cx), (g_Let_folded,cterm_of sg abs_g')] - Let_folded; + @{thm Let_folded}; in SOME (rl OF [transitive fx_g g_g'x]) end) end @@ -314,40 +288,34 @@ *) local - val conjE = thm "conjE" - val exE = thm "exE" - val disjE = thm "disjE" - val notE = thm "notE" - val rev_mp = thm "rev_mp" - val ccontr = thm "ccontr" val nnf_simpset = empty_ss setmkeqTrue mk_eq_True setmksimps (mksimps mksimps_pairs) - addsimps [thm "imp_conv_disj", thm "iff_conv_conj_imp", thm "de_Morgan_disj", thm "de_Morgan_conj", - thm "not_all", thm "not_ex", thm "not_not"]; + addsimps [@{thm imp_conv_disj}, @{thm iff_conv_conj_imp}, @{thm de_Morgan_disj}, + @{thm de_Morgan_conj}, @{thm not_all}, @{thm not_ex}, @{thm not_not}]; fun prem_nnf_tac i st = full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st; in fun refute_tac test prep_tac ref_tac = let val refute_prems_tac = REPEAT_DETERM - (eresolve_tac [conjE, exE] 1 ORELSE + (eresolve_tac [@{thm conjE}, @{thm exE}] 1 ORELSE filter_prems_tac test 1 ORELSE - etac disjE 1) THEN - ((etac notE 1 THEN eq_assume_tac 1) ORELSE + etac @{thm disjE} 1) THEN + ((etac @{thm notE} 1 THEN eq_assume_tac 1) ORELSE ref_tac 1); in EVERY'[TRY o filter_prems_tac test, - REPEAT_DETERM o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac, + REPEAT_DETERM o etac @{thm rev_mp}, prep_tac, rtac @{thm ccontr}, prem_nnf_tac, SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)] end; end; val defALL_regroup = - Simplifier.simproc (the_context ()) + Simplifier.simproc @{theory} "defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all; val defEX_regroup = - Simplifier.simproc (the_context ()) + Simplifier.simproc @{theory} "defined EX" ["EX x. P x"] Quantifier1.rearrange_ex;