# HG changeset patch # User haftmann # Date 1160571084 -7200 # Node ID 0b8e436ed071e0b91e364e09b55158dcb7cafbce # Parent db0425645cc71d1a298c92a02cf1688de2d73de0 cleaned up HOL bootstrap diff -r db0425645cc7 -r 0b8e436ed071 src/HOL/HOL.ML --- a/src/HOL/HOL.ML Wed Oct 11 10:49:36 2006 +0200 +++ b/src/HOL/HOL.ML Wed Oct 11 14:51:24 2006 +0200 @@ -1,6 +1,24 @@ (* legacy ML bindings *) +val HOL_cs = HOL.claset; +val HOL_basic_ss = HOL.simpset_basic; +val HOL_ss = HOL.simpset; +val HOL_css = (HOL.claset, HOL.simpset); +val hol_simplify = HOL.simplify; + +val split_tac = Splitter.split_tac; +val split_inside_tac = Splitter.split_inside_tac; +val split_asm_tac = Splitter.split_asm_tac; +val op addsplits = Splitter.addsplits; +val op delsplits = Splitter.delsplits; +val Addsplits = Splitter.Addsplits; +val Delsplits = Splitter.Delsplits; + open HOL; +val claset = Classical.claset; +val simpset = Simplifier.simpset; +val simplify = Simplifier.simplify; +open Clasimp; val ext = thm "ext" val True_def = thm "True_def" diff -r db0425645cc7 -r 0b8e436ed071 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Wed Oct 11 10:49:36 2006 +0200 +++ b/src/HOL/HOL.thy Wed Oct 11 14:51:24 2006 +0200 @@ -227,7 +227,7 @@ subsection {* Fundamental rules *} -subsubsection {*Equality*} +subsubsection {* Equality *} text {* Thanks to Stephan Merz *} lemma subst: @@ -862,12 +862,11 @@ "\X. \ x=x; PROP W \ \ PROP W" . use "cladata.ML" -ML {* val HOL_cs = HOL.cs *} setup Hypsubst.hypsubst_setup setup {* ContextRules.addSWrapper (fn tac => HOL.hyp_subst_tac' ORELSE' tac) *} setup Classical.setup setup ResAtpset.setup -setup {* fn thy => (Classical.change_claset_of thy (K HOL.cs); thy) *} +setup {* fn thy => (Classical.change_claset_of thy (K HOL.claset); thy) *} lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P" apply (erule swap) @@ -881,7 +880,7 @@ and [elim?] = ex1_implies_ex (*Better then ex1E for classical reasoner: needs no quantifier duplication!*) -lemma alt_ex1E: +lemma alt_ex1E [elim!]: assumes major: "\!x. P x" and prem: "\x. \ P x; \y y'. P y \ P y' \ y = y' \ \ R" shows R @@ -1197,11 +1196,54 @@ use "simpdata.ML" setup "Simplifier.method_setup Splitter.split_modifiers" -setup simpsetup +setup "(fn thy => (change_simpset_of thy (fn _ => HOL.simpset_simprocs); thy))" setup Splitter.setup setup Clasimp.setup setup EqSubst.setup +declare triv_forall_equality [simp] (*prunes params*) + and True_implies_equals [simp] (*prune asms `True'*) + and if_True [simp] + and if_False [simp] + and if_cancel [simp] + and if_eq_cancel [simp] + and imp_disjL [simp] + (*In general it seems wrong to add distributive laws by default: they + might cause exponential blow-up. But imp_disjL has been in for a while + and cannot be removed without affecting existing proofs. Moreover, + rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the + grounds that it allows simplification of R in the two cases.*) + and conj_assoc [simp] + and disj_assoc [simp] + and de_Morgan_conj [simp] + and de_Morgan_disj [simp] + and imp_disj1 [simp] + and imp_disj2 [simp] + and not_imp [simp] + and disj_not1 [simp] + and not_all [simp] + and not_ex [simp] + and cases_simp [simp] + and the_eq_trivial [simp] + and the_sym_eq_trivial [simp] + and ex_simps [simp] + and all_simps [simp] + and simp_thms [simp] + and imp_cong [cong] + and simp_implies_cong [cong] + and split_if [split] + +ML {* +structure HOL = +struct + +open HOL; + +val simpset = Simplifier.simpset_of (the_context ()); + +end; +*} + text {* Simplifies x assuming c and y assuming ~c *} lemma if_cong: assumes "b = c" diff -r db0425645cc7 -r 0b8e436ed071 src/HOL/blastdata.ML --- a/src/HOL/blastdata.ML Wed Oct 11 10:49:36 2006 +0200 +++ b/src/HOL/blastdata.ML Wed Oct 11 14:51:24 2006 +0200 @@ -1,5 +1,3 @@ -Classical.AddSEs [thm "alt_ex1E"]; - structure Blast_Data = struct type claset = Classical.claset diff -r db0425645cc7 -r 0b8e436ed071 src/HOL/cladata.ML --- a/src/HOL/cladata.ML Wed Oct 11 10:49:36 2006 +0200 +++ b/src/HOL/cladata.ML Wed Oct 11 14:51:24 2006 +0200 @@ -9,7 +9,7 @@ structure Hypsubst_Data = struct structure Simplifier = Simplifier - fun dest_eq (Const ("op =", T) $ t $ u) = (t, u, domain_type T) + val dest_eq = HOLogic.dest_eq_typ val dest_Trueprop = HOLogic.dest_Trueprop val dest_imp = HOLogic.dest_imp val eq_reflection = HOL.eq_reflection @@ -52,7 +52,7 @@ addSEs [HOL.conjE, HOL.disjE, HOL.impCE, HOL.FalseE, HOL.iffCE]; (*Quantifier rules*) -val cs = prop_cs addSIs [HOL.allI, HOL.ex_ex1I] addIs [HOL.exI, HOL.the_equality] +val claset = prop_cs addSIs [HOL.allI, HOL.ex_ex1I] addIs [HOL.exI, HOL.the_equality] addSEs [HOL.exE] addEs [HOL.allE]; end; diff -r db0425645cc7 -r 0b8e436ed071 src/HOL/hologic.ML --- a/src/HOL/hologic.ML Wed Oct 11 10:49:36 2006 +0200 +++ b/src/HOL/hologic.ML Wed Oct 11 14:51:24 2006 +0200 @@ -39,6 +39,7 @@ val Collect_const: typ -> term val mk_eq: term * term -> term val dest_eq: term -> term * term + val dest_eq_typ: term -> (term * term) * typ val mk_all: string * typ * term -> term val list_all: (string * typ) list * term -> term val mk_exists: string * typ * term -> term @@ -158,6 +159,9 @@ fun dest_eq (Const ("op =", _) $ lhs $ rhs) = (lhs, rhs) | dest_eq t = raise TERM ("dest_eq", [t]) +fun dest_eq_typ (Const ("op =", T) $ lhs $ rhs) = ((lhs, rhs), domain_type T) + | dest_eq_typ t = raise TERM ("dest_eq_typ", [t]) + fun all_const T = Const ("All", [T --> boolT] ---> boolT); fun mk_all (x, T, P) = all_const T $ absfree (x, T, P); fun list_all (vs,x) = foldr (fn ((x, T), P) => all_const T $ Abs (x, T, P)) x vs; diff -r db0425645cc7 -r 0b8e436ed071 src/HOL/simpdata.ML --- a/src/HOL/simpdata.ML Wed Oct 11 10:49:36 2006 +0200 +++ b/src/HOL/simpdata.ML Wed Oct 11 14:51:24 2006 +0200 @@ -6,40 +6,16 @@ Instantiation of the generic simplifier for HOL. *) -(* legacy ML bindings - FIXME get rid of this *) - -val Eq_FalseI = thm "Eq_FalseI"; -val Eq_TrueI = thm "Eq_TrueI"; -val de_Morgan_conj = thm "de_Morgan_conj"; -val de_Morgan_disj = thm "de_Morgan_disj"; -val iff_conv_conj_imp = thm "iff_conv_conj_imp"; -val imp_cong = thm "imp_cong"; -val imp_conv_disj = thm "imp_conv_disj"; -val imp_disj1 = thm "imp_disj1"; -val imp_disj2 = thm "imp_disj2"; -val imp_disjL = thm "imp_disjL"; -val simp_impliesI = thm "simp_impliesI"; -val simp_implies_cong = thm "simp_implies_cong"; -val simp_implies_def = thm "simp_implies_def"; - -local - val uncurry = thm "uncurry" - val iff_allI = thm "iff_allI" - val iff_exI = thm "iff_exI" - val all_comm = thm "all_comm" - val ex_comm = thm "ex_comm" -in - -(*** make simplification procedures for quantifier elimination ***) +(** tools setup **) structure Quantifier1 = Quantifier1Fun (struct (*abstract syntax*) - fun dest_eq((c as Const("op =",_)) $ s $ t) = SOME(c,s,t) + fun dest_eq ((c as Const("op =",_)) $ s $ t) = SOME (c, s, t) | dest_eq _ = NONE; - fun dest_conj((c as Const("op &",_)) $ s $ t) = SOME(c,s,t) + fun dest_conj ((c as Const("op &",_)) $ s $ t) = SOME (c, s, t) | dest_conj _ = NONE; - fun dest_imp((c as Const("op -->",_)) $ s $ t) = SOME(c,s,t) + fun dest_imp ((c as Const("op -->",_)) $ s $ t) = SOME (c, s, t) | dest_imp _ = NONE; val conj = HOLogic.conj val imp = HOLogic.imp @@ -51,32 +27,162 @@ val conjE= HOL.conjE val impI = HOL.impI val mp = HOL.mp - val uncurry = uncurry + val uncurry = thm "uncurry" val exI = HOL.exI val exE = HOL.exE - val iff_allI = iff_allI - val iff_exI = iff_exI - val all_comm = all_comm - val ex_comm = ex_comm + 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 HOL = +struct + +open HOL; + +val Eq_FalseI = thm "Eq_FalseI"; +val Eq_TrueI = thm "Eq_TrueI"; +val simp_implies_def = thm "simp_implies_def"; +val simp_impliesI = thm "simp_impliesI"; + +fun mk_meta_eq r = r RS eq_reflection; +fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r; + +fun mk_eq thm = case concl_of thm + (*expects Trueprop if not == *) + of Const ("==",_) $ _ $ _ => thm + | _ $ (Const ("op =", _) $ _ $ _) => mk_meta_eq thm + | _ $ (Const ("Not", _) $ _) => thm RS Eq_FalseI + | _ => thm RS Eq_TrueI; + +fun mk_eq_True r = + SOME (r RS meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => NONE; + +(* Produce theorems of the form + (P1 =simp=> ... =simp=> Pn => x == y) ==> (P1 =simp=> ... =simp=> Pn => x = y) +*) +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 + else + let + val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j); + fun mk_simp_implies Q = foldr (fn (R, S) => + Const ("HOL.simp_implies", propT --> propT --> propT) $ R $ S) Q Ps + val aT = TFree ("'a", HOLogic.typeS); + val x = Free ("x", aT); + val y = Free ("y", aT) + in Goal.prove_global (Thm.theory_of_thm st) [] + [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)]) + end + end; + +(*Congruence rules for = (instead of ==)*) +fun mk_meta_cong rl = zero_var_indexes + (let val rl' = Seq.hd (TRYALL (fn i => fn st => + rtac (lift_meta_eq_to_obj_eq i st) i st) rl) + in mk_meta_eq rl' handle THM _ => + if can Logic.dest_equals (concl_of rl') then rl' + else error "Conclusion of congruence rules must be =-equality" + end); + +(* +val mk_atomize: (string * thm list) list -> thm -> thm list +looks too specific to move it somewhere else +*) +fun mk_atomize pairs = + let + fun atoms thm = case concl_of thm + of Const("Trueprop", _) $ p => (case head_of p + of Const(a, _) => (case AList.lookup (op =) pairs a + of SOME rls => maps atoms ([thm] RL rls) + | NONE => [thm]) + | _ => [thm]) + | _ => [thm] + in atoms end; + +fun mksimps pairs = + (map_filter (try mk_eq) o mk_atomize pairs o gen_all); + +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]; +val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac; + +(*No premature instantiation of variables during simplification*) +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]]; +val safe_solver = mk_solver "HOL safe" safe_solver_tac; + end; -val defEX_regroup = - Simplifier.simproc (the_context ()) - "defined EX" ["EX x. P x"] Quantifier1.rearrange_ex; +structure SplitterData = +struct + structure Simplifier = Simplifier + val mk_eq = HOL.mk_eq + val meta_eq_to_iff = HOL.meta_eq_to_obj_eq + val iffD = HOL.iffD2 + val disjE = HOL.disjE + val conjE = HOL.conjE + val exE = HOL.exE + val contrapos = HOL.contrapos_nn + val contrapos2 = HOL.contrapos_pp + val notnotD = HOL.notnotD +end; + +structure Splitter = SplitterFun(SplitterData); + +(* integration of simplifier with classical reasoner *) + +structure Clasimp = ClasimpFun + (structure Simplifier = Simplifier and Splitter = Splitter + and Classical = Classical and Blast = Blast + val iffD1 = HOL.iffD1 val iffD2 = HOL.iffD2 val notE = HOL.notE); -val defALL_regroup = - Simplifier.simproc (the_context ()) - "defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all; +structure HOL = +struct + +open HOL; + +val mksimps_pairs = + [("op -->", [mp]), ("op &", [thm "conjunct1", thm "conjunct2"]), + ("All", [spec]), ("True", []), ("False", []), + ("HOL.If", [thm "if_bool_eq_conj" RS iffD1])]; +val simpset_basic = + Simplifier.theory_context (the_context ()) empty_ss + setsubgoaler asm_simp_tac + setSSolver safe_solver + setSolver unsafe_solver + setmksimps (mksimps mksimps_pairs) + setmkeqTrue mk_eq_True + setmkcong mk_meta_cong; + +fun simplify rews = Simplifier.full_simplify (simpset_basic addsimps rews); + +fun unfold_tac ths = + let val ss0 = Simplifier.clear_ss simpset_basic addsimps ths + in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end; + +(** simprocs **) (* simproc for proving "(y = x) == False" from premise "~(x = y)" *) val use_neq_simproc = ref true; local - val neq_to_EQ_False = thm "not_sym" RS Eq_FalseI; + val thy = the_context (); + val neq_to_EQ_False = thm "not_sym" RS HOL.Eq_FalseI; fun neq_prover sg ss (eq $ lhs $ rhs) = let fun test thm = (case #prop (rep_thm thm) of @@ -91,10 +197,9 @@ end in -val neq_simproc = Simplifier.simproc (the_context ()) - "neq_simproc" ["x = y"] neq_prover; +val neq_simproc = Simplifier.simproc thy "neq_simproc" ["x = y"] neq_prover; -end; +end; (*local*) (* Simproc for Let *) @@ -102,23 +207,24 @@ val use_let_simproc = ref true; local + val thy = the_context (); val Let_folded = thm "Let_folded"; val Let_unfold = thm "Let_unfold"; - val (f_Let_unfold,x_Let_unfold) = + val (f_Let_unfold, x_Let_unfold) = let val [(_$(f$x)$_)] = prems_of Let_unfold - in (cterm_of (the_context ()) f,cterm_of (the_context ()) x) end - val (f_Let_folded,x_Let_folded) = + in (cterm_of thy f, cterm_of thy x) end + val (f_Let_folded, x_Let_folded) = let val [(_$(f$x)$_)] = prems_of Let_folded - in (cterm_of (the_context ()) f, cterm_of (the_context ()) x) end; + in (cterm_of thy f, cterm_of thy x) end; val g_Let_folded = - let val [(_$_$(g$_))] = prems_of Let_folded in cterm_of (the_context ()) g end; + let val [(_$_$(g$_))] = prems_of Let_folded in cterm_of thy g end; in val let_simproc = - Simplifier.simproc (the_context ()) "let_simp" ["Let x f"] + Simplifier.simproc thy "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; + val ([t'], ctxt') = Variable.import_terms false [t] ctxt; in Option.map (hd o Variable.export ctxt' ctxt o single) (case t' of (Const ("Let",_)$x$f) => (* x and f are already in normal form *) if not (!use_let_simproc) then NONE @@ -153,192 +259,9 @@ | _ => NONE) end) -end - -(*** Case splitting ***) - -(*Make meta-equalities. The operator below is Trueprop*) - -fun mk_meta_eq r = r RS HOL.eq_reflection; -fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r; - -fun mk_eq th = case concl_of th of - Const("==",_)$_$_ => th - | _$(Const("op =",_)$_$_) => mk_meta_eq th - | _$(Const("Not",_)$_) => th RS Eq_FalseI - | _ => th RS Eq_TrueI; -(* Expects Trueprop(.) if not == *) - -fun mk_eq_True r = - SOME (r RS HOL.meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => NONE; - -(* Produce theorems of the form - (P1 =simp=> ... =simp=> Pn => x == y) ==> (P1 =simp=> ... =simp=> Pn => x = y) -*) -fun lift_meta_eq_to_obj_eq i st = - let - val {sign, ...} = rep_thm st; - 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 HOL.meta_eq_to_obj_eq - else - let - val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j); - fun mk_simp_implies Q = foldr (fn (R, S) => - Const ("HOL.simp_implies", propT --> propT --> propT) $ R $ S) Q Ps - val aT = TFree ("'a", HOLogic.typeS); - val x = Free ("x", aT); - val y = Free ("y", aT) - in Goal.prove_global (Thm.theory_of_thm st) [] - [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 (HOL.meta_eq_to_obj_eq :: map (rewrite_rule [simp_implies_def]) prems) 1)]) - end - end; - -(*Congruence rules for = (instead of ==)*) -fun mk_meta_cong rl = zero_var_indexes - (let val rl' = Seq.hd (TRYALL (fn i => fn st => - rtac (lift_meta_eq_to_obj_eq i st) i st) rl) - in mk_meta_eq rl' handle THM _ => - if can Logic.dest_equals (concl_of rl') then rl' - else error "Conclusion of congruence rules must be =-equality" - end); - -structure SplitterData = -struct - structure Simplifier = Simplifier - val mk_eq = mk_eq - val meta_eq_to_iff = HOL.meta_eq_to_obj_eq - val iffD = HOL.iffD2 - val disjE = HOL.disjE - val conjE = HOL.conjE - val exE = HOL.exE - val contrapos = HOL.contrapos_nn - val contrapos2 = HOL.contrapos_pp - val notnotD = HOL.notnotD -end; - -structure Splitter = SplitterFun(SplitterData); - -val split_tac = Splitter.split_tac; -val split_inside_tac = Splitter.split_inside_tac; -val split_asm_tac = Splitter.split_asm_tac; -val op addsplits = Splitter.addsplits; -val op delsplits = Splitter.delsplits; -val Addsplits = Splitter.Addsplits; -val Delsplits = Splitter.Delsplits; - -val mksimps_pairs = - [("op -->", [HOL.mp]), ("op &", [thm "conjunct1", thm "conjunct2"]), - ("All", [HOL.spec]), ("True", []), ("False", []), - ("HOL.If", [thm "if_bool_eq_conj" RS HOL.iffD1])]; +end; (*local*) -(* -val mk_atomize: (string * thm list) list -> thm -> thm list -looks too specific to move it somewhere else -*) -fun mk_atomize pairs = - let fun atoms th = - (case concl_of th of - Const("Trueprop",_) $ p => - (case head_of p of - Const(a,_) => - (case AList.lookup (op =) pairs a of - SOME(rls) => List.concat (map atoms ([th] RL rls)) - | NONE => [th]) - | _ => [th]) - | _ => [th]) - in atoms end; - -fun mksimps pairs = - (List.mapPartial (try mk_eq) o mk_atomize pairs o gen_all); - -fun unsafe_solver_tac prems = - (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN' - FIRST'[resolve_tac(reflexive_thm :: HOL.TrueI :: HOL.refl :: prems), atac, etac HOL.FalseE]; -val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac; - -(*No premature instantiation of variables during simplification*) -fun safe_solver_tac prems = - (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN' - FIRST'[match_tac(reflexive_thm :: HOL.TrueI :: HOL.refl :: prems), - eq_assume_tac, ematch_tac [HOL.FalseE]]; -val safe_solver = mk_solver "HOL safe" safe_solver_tac; - -val HOL_basic_ss = - Simplifier.theory_context (the_context ()) empty_ss - setsubgoaler asm_simp_tac - setSSolver safe_solver - setSolver unsafe_solver - setmksimps (mksimps mksimps_pairs) - setmkeqTrue mk_eq_True - setmkcong mk_meta_cong; - -fun unfold_tac ths = - let val ss0 = Simplifier.clear_ss HOL_basic_ss addsimps ths - in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end; - -(*In general it seems wrong to add distributive laws by default: they - might cause exponential blow-up. But imp_disjL has been in for a while - and cannot be removed without affecting existing proofs. Moreover, - rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the - grounds that it allows simplification of R in the two cases.*) - -local - val ex_simps = thms "ex_simps"; - val all_simps = thms "all_simps"; - val simp_thms = thms "simp_thms"; - val cases_simp = thm "cases_simp"; - val conj_assoc = thm "conj_assoc"; - val if_False = thm "if_False"; - val if_True = thm "if_True"; - val disj_assoc = thm "disj_assoc"; - val disj_not1 = thm "disj_not1"; - val if_cancel = thm "if_cancel"; - val if_eq_cancel = thm "if_eq_cancel"; - val True_implies_equals = thm "True_implies_equals"; -in - -val HOL_ss = - HOL_basic_ss addsimps - ([triv_forall_equality, (* prunes params *) - True_implies_equals, (* prune asms `True' *) - if_True, if_False, if_cancel, if_eq_cancel, - imp_disjL, conj_assoc, disj_assoc, - de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, thm "not_imp", - disj_not1, thm "not_all", thm "not_ex", cases_simp, - thm "the_eq_trivial", HOL.the_sym_eq_trivial] - @ ex_simps @ all_simps @ simp_thms) - addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc] - addcongs [imp_cong, simp_implies_cong] - addsplits [thm "split_if"]; - -end; - -fun hol_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews); - -(* default simpset *) -val simpsetup = - (fn thy => (change_simpset_of thy (fn _ => HOL_ss); thy)); - - -(*** integration of simplifier with classical reasoner ***) - -structure Clasimp = ClasimpFun - (structure Simplifier = Simplifier and Splitter = Splitter - and Classical = Classical and Blast = Blast - val iffD1 = HOL.iffD1 val iffD2 = HOL.iffD2 val notE = HOL.notE); -open Clasimp; - -val HOL_css = (HOL_cs, HOL_ss); - - - -(*** A general refutation procedure ***) +(* A general refutation procedure *) (* Parameters: @@ -361,7 +284,7 @@ val nnf_simpset = empty_ss setmkeqTrue mk_eq_True setmksimps (mksimps mksimps_pairs) - addsimps [imp_conv_disj,iff_conv_conj_imp,de_Morgan_disj,de_Morgan_conj, + 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; @@ -369,13 +292,27 @@ fun refute_tac test prep_tac ref_tac = let val refute_prems_tac = REPEAT_DETERM - (eresolve_tac [HOL.conjE, HOL.exE] 1 ORELSE + (eresolve_tac [conjE, exE] 1 ORELSE filter_prems_tac test 1 ORELSE - etac HOL.disjE 1) THEN - ((etac HOL.notE 1 THEN eq_assume_tac 1) ORELSE + etac disjE 1) THEN + ((etac notE 1 THEN eq_assume_tac 1) ORELSE ref_tac 1); in EVERY'[TRY o filter_prems_tac test, - REPEAT_DETERM o etac HOL.rev_mp, prep_tac, rtac HOL.ccontr, prem_nnf_tac, + REPEAT_DETERM o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac, SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)] end; -end; +end; (*local*) + +val defALL_regroup = + Simplifier.simproc (the_context ()) + "defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all; + +val defEX_regroup = + Simplifier.simproc (the_context ()) + "defined EX" ["EX x. P x"] Quantifier1.rearrange_ex; + + +val simpset_simprocs = simpset_basic + addsimprocs [defALL_regroup, defEX_regroup, neq_simproc, let_simproc] + +end; (*struct*) \ No newline at end of file