# HG changeset patch # User wenzelm # Date 1185712189 -7200 # Node ID 74c032aea9ed073c3666eb635a34b5b433f4422b # Parent ef0789aa7cbe3028af70cac5edf88e9847e37b0d simplified ResAtpset via NamedThmsFun; proper simproc_setup for "neq", "let_simp"; diff -r ef0789aa7cbe -r 74c032aea9ed src/HOL/HOL.thy --- a/src/HOL/HOL.thy Sun Jul 29 14:29:48 2007 +0200 +++ b/src/HOL/HOL.thy Sun Jul 29 14:29:49 2007 +0200 @@ -24,7 +24,6 @@ "~~/src/Provers/eqsubst.ML" "~~/src/Provers/quantifier1.ML" ("simpdata.ML") - "Tools/res_atpset.ML" ("~~/src/HOL/Tools/recfun_codegen.ML") begin @@ -928,6 +927,8 @@ ML_Context.value_antiq "claset" (Scan.succeed ("claset", "Classical.local_claset_of (ML_Context.the_local_context ())")); + +structure ResAtpset = NamedThmsFun(val name = "atp" val description = "ATP rules"); *} setup {* @@ -1284,6 +1285,80 @@ #> EqSubst.setup *} +text {* Simproc for proving @{text "(y = x) == False"} from premise @{text "~(x = y)"}: *} + +simproc_setup neq ("x = y") = {* fn _ => +let + val neq_to_EQ_False = @{thm not_sym} RS @{thm Eq_FalseI}; + fun is_neq eq lhs rhs thm = + (case Thm.prop_of thm of + _ $ (Not $ (eq' $ l' $ r')) => + Not = HOLogic.Not andalso eq' = eq andalso + r' aconv lhs andalso l' aconv rhs + | _ => false); + fun proc ss ct = + (case Thm.term_of ct of + eq $ lhs $ rhs => + (case find_first (is_neq eq lhs rhs) (Simplifier.prems_of_ss ss) of + SOME thm => SOME (thm RS neq_to_EQ_False) + | NONE => NONE) + | _ => NONE); +in proc end; +*} + +simproc_setup let_simp ("Let x f") = {* +let + val (f_Let_unfold, x_Let_unfold) = + 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 @{thm Let_folded} + in (cterm_of @{theory} f, cterm_of @{theory} x) end; + val g_Let_folded = + let val [(_$_$(g$_))] = prems_of @{thm Let_folded} in cterm_of @{theory} g end; + + fun proc _ ss ct = + let + val ctxt = Simplifier.the_context ss; + val thy = ProofContext.theory_of ctxt; + val t = Thm.term_of ct; + 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 is_Free x orelse is_Bound x orelse is_Const x + then SOME @{thm Let_def} + else + let + val n = case f of (Abs (x,_,_)) => x | _ => "x"; + val cx = cterm_of thy x; + val {T=xT,...} = rep_cterm cx; + val cf = cterm_of thy f; + val fx_g = Simplifier.rewrite ss (Thm.capply cf cx); + val (_$_$g) = prop_of fx_g; + val g' = abstract_over (x,g); + in (if (g aconv g') + then + let + 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 + val abs_g'= Abs (n,xT,g'); + val g'x = abs_g'$x; + val g_g'x = symmetric (beta_conversion false (cterm_of thy g'x)); + val rl = cterm_instantiate + [(f_Let_folded,cterm_of thy f),(x_Let_folded,cx), + (g_Let_folded,cterm_of thy abs_g')] + @{thm Let_folded}; + in SOME (rl OF [transitive fx_g g_g'x]) + end) + end + | _ => NONE) + end +in proc end *} + + lemma True_implies_equals: "(True \ PROP P) \ PROP P" proof assume "True \ PROP P" diff -r ef0789aa7cbe -r 74c032aea9ed src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Sun Jul 29 14:29:48 2007 +0200 +++ b/src/HOL/Library/Multiset.thy Sun Jul 29 14:29:49 2007 +0200 @@ -238,16 +238,15 @@ apply (blast dest: sym) done -ML"reset use_neq_simproc" lemma add_eq_conv_diff: "(M + {#a#} = N + {#b#}) = (M = N \ a = b \ M = N - {#a#} + {#b#} \ N = M - {#b#} + {#a#})" + using [[simproc del: neq]] apply (unfold single_def union_def diff_def) apply (simp (no_asm) add: expand_fun_eq) apply (rule conjI, force, safe, simp_all) apply (simp add: eq_sym_conv) done -ML"set use_neq_simproc" declare Rep_multiset_inject [symmetric, simp del] diff -r ef0789aa7cbe -r 74c032aea9ed src/HOL/simpdata.ML --- a/src/HOL/simpdata.ML Sun Jul 29 14:29:48 2007 +0200 +++ b/src/HOL/simpdata.ML Sun Jul 29 14:29:49 2007 +0200 @@ -185,92 +185,7 @@ -(** 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 @{thm Eq_FalseI}; - fun neq_prover sg ss (eq $ lhs $ rhs) = - let - fun test thm = (case #prop (rep_thm thm) of - _ $ (Not $ (eq' $ l' $ r')) => - Not = HOLogic.Not andalso eq' = eq andalso - r' aconv lhs andalso l' aconv rhs - | _ => false) - in if !use_neq_simproc then case find_first test (prems_of_ss ss) - of NONE => NONE - | SOME thm => SOME (thm RS neq_to_EQ_False) - else NONE - end -in - -val neq_simproc = Simplifier.simproc @{theory} "neq_simproc" ["x = y"] neq_prover; - -end; - - -(* simproc for Let *) - -val use_let_simproc = ref true; - -local - val (f_Let_unfold, x_Let_unfold) = - 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 @{thm Let_folded} - in (cterm_of @{theory} f, cterm_of @{theory} x) end; - val g_Let_folded = - let val [(_$_$(g$_))] = prems_of @{thm Let_folded} in cterm_of @{theory} g end; -in - -val let_simproc = - Simplifier.simproc @{theory} "let_simp" ["Let x f"] - (fn thy => fn ss => fn t => - let val ctxt = Simplifier.the_context ss; - 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 - else if is_Free x orelse is_Bound x orelse is_Const x - then SOME @{thm Let_def} - else - let - val n = case f of (Abs (x,_,_)) => x | _ => "x"; - val cx = cterm_of thy x; - val {T=xT,...} = rep_cterm cx; - val cf = cterm_of thy f; - val fx_g = Simplifier.rewrite ss (Thm.capply cf cx); - val (_$_$g) = prop_of fx_g; - val g' = abstract_over (x,g); - in (if (g aconv g') - then - let - 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 - val abs_g'= Abs (n,xT,g'); - val g'x = abs_g'$x; - val g_g'x = symmetric (beta_conversion false (cterm_of thy g'x)); - val rl = cterm_instantiate - [(f_Let_folded,cterm_of thy f),(x_Let_folded,cx), - (g_Let_folded,cterm_of thy abs_g')] - @{thm Let_folded}; - in SOME (rl OF [transitive fx_g g_g'x]) - end) - end - | _ => NONE) - end) - -end; - - -(* generic refutation procedure *) +(** generic refutation procedure **) (* parameters: @@ -321,8 +236,7 @@ "defined EX" ["EX x. P x"] Quantifier1.rearrange_ex; -val simpset_simprocs = HOL_basic_ss - addsimprocs [defALL_regroup, defEX_regroup, neq_simproc, let_simproc] +val simpset_simprocs = HOL_basic_ss addsimprocs [defALL_regroup, defEX_regroup] end;