# HG changeset patch # User huffman # Date 1342774405 -7200 # Node ID 868dc809c8a21ee59046d4082eb253dc46442bb2 # Parent 3a5a5a992519c45124930e269a614011b38d73aa make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests diff -r 3a5a5a992519 -r 868dc809c8a2 src/HOL/Tools/arith_data.ML --- a/src/HOL/Tools/arith_data.ML Thu Jul 19 22:21:59 2012 +0200 +++ b/src/HOL/Tools/arith_data.ML Fri Jul 20 10:53:25 2012 +0200 @@ -112,7 +112,8 @@ fun simp_all_tac rules = let val ss0 = HOL_ss addsimps rules - in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end; + val safe_simp_tac = generic_simp_tac true (false, false, false) + in fn ss => ALLGOALS (safe_simp_tac (Simplifier.inherit_context ss ss0)) end; fun simplify_meta_eq rules = let val ss0 = HOL_basic_ss addsimps rules |> Simplifier.add_eqcong @{thm eq_cong2} diff -r 3a5a5a992519 -r 868dc809c8a2 src/HOL/Tools/nat_arith.ML --- a/src/HOL/Tools/nat_arith.ML Thu Jul 19 22:21:59 2012 +0200 +++ b/src/HOL/Tools/nat_arith.ML Fri Jul 20 10:53:25 2012 +0200 @@ -49,13 +49,11 @@ struct val mk_sum = mk_norm_sum; val dest_sum = dest_sum; - val prove_conv = Arith_Data.prove_conv2; + val mk_plus = HOLogic.mk_binop @{const_name Groups.plus}; val norm_tac1 = Arith_Data.simp_all_tac [@{thm add_Suc}, @{thm add_Suc_right}, @{thm Nat.add_0}, @{thm Nat.add_0_right}]; val norm_tac2 = Arith_Data.simp_all_tac @{thms add_ac}; fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss; - fun gen_uncancel_tac rule = let val rule' = rule RS @{thm subst_equals} - in fn ct => rtac (instantiate' [] [NONE, SOME ct] rule') 1 end; end; structure EqCancelSums = CancelSumsFun @@ -63,7 +61,7 @@ open CommonCancelSums; val mk_bal = HOLogic.mk_eq; val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT; - val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel"}; + val cancel_rule = mk_meta_eq @{thm nat_add_left_cancel}; end); structure LessCancelSums = CancelSumsFun @@ -71,7 +69,7 @@ open CommonCancelSums; val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less}; val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT; - val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"}; + val cancel_rule = mk_meta_eq @{thm nat_add_left_cancel_less}; end); structure LeCancelSums = CancelSumsFun @@ -79,7 +77,7 @@ open CommonCancelSums; val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq}; val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT; - val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"}; + val cancel_rule = mk_meta_eq @{thm nat_add_left_cancel_le}; end); structure DiffCancelSums = CancelSumsFun @@ -87,7 +85,7 @@ open CommonCancelSums; val mk_bal = HOLogic.mk_binop @{const_name Groups.minus}; val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} HOLogic.natT; - val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"}; + val cancel_rule = mk_meta_eq @{thm diff_cancel}; end); val nat_cancel_sums_add = diff -r 3a5a5a992519 -r 868dc809c8a2 src/HOL/ex/Simproc_Tests.thy --- a/src/HOL/ex/Simproc_Tests.thy Thu Jul 19 22:21:59 2012 +0200 +++ b/src/HOL/ex/Simproc_Tests.thy Fri Jul 20 10:53:25 2012 +0200 @@ -5,14 +5,14 @@ header {* Testing of arithmetic simprocs *} theory Simproc_Tests -imports (*Main*) "../Numeral_Simprocs" +imports Main begin text {* - This theory tests the various simprocs defined in - @{file "~~/src/HOL/Numeral_Simprocs.thy"}. Many of the tests - are derived from commented-out code originally found in - @{file "~~/src/HOL/Tools/numeral_simprocs.ML"}. + This theory tests the various simprocs defined in @{file + "~~/src/HOL/Nat.thy"} and @{file "~~/src/HOL/Numeral_Simprocs.thy"}. + Many of the tests are derived from commented-out code originally + found in @{file "~~/src/HOL/Tools/numeral_simprocs.ML"}. *} subsection {* ML bindings *} @@ -21,6 +21,29 @@ fun test ps = CHANGED (asm_simp_tac (HOL_basic_ss addsimprocs ps) 1) *} +subsection {* Cancellation simprocs from @{text Nat.thy} *} + +notepad begin + fix a b c d :: nat + { + assume "b = Suc c" have "a + b = Suc (c + a)" + by (tactic {* test [nth Nat_Arith.nat_cancel_sums 0] *}) fact + next + assume "b < Suc c" have "a + b < Suc (c + a)" + by (tactic {* test [nth Nat_Arith.nat_cancel_sums 1] *}) fact + next + assume "b \ Suc c" have "a + b \ Suc (c + a)" + by (tactic {* test [nth Nat_Arith.nat_cancel_sums 2] *}) fact + next + assume "b - Suc c = d" have "a + b - Suc (c + a) = d" + by (tactic {* test [nth Nat_Arith.nat_cancel_sums 3] *}) fact + } +end + +schematic_lemma "\(y::?'b::size). size (?x::?'a::size) \ size y + size ?x" + by (tactic {* test [nth Nat_Arith.nat_cancel_sums 2] *}) (rule le0) +(* TODO: test more simprocs with schematic variables *) + subsection {* Abelian group cancellation simprocs *} notepad begin diff -r 3a5a5a992519 -r 868dc809c8a2 src/Provers/Arith/cancel_sums.ML --- a/src/Provers/Arith/cancel_sums.ML Thu Jul 19 22:21:59 2012 +0200 +++ b/src/Provers/Arith/cancel_sums.ML Fri Jul 20 10:53:25 2012 +0200 @@ -13,12 +13,12 @@ (*abstract syntax*) val mk_sum: term list -> term val dest_sum: term -> term list + val mk_plus: term * term -> term val mk_bal: term * term -> term val dest_bal: term -> term * term (*rules*) - val prove_conv: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm val norm_tac: simpset -> tactic (*AC0 etc.*) - val uncancel_tac: cterm -> tactic (*apply A ~~ B == x + A ~~ x + B*) + val cancel_rule: thm (* x + A ~~ x + B == A ~~ B *) end; signature CANCEL_SUMS = @@ -46,14 +46,6 @@ | GREATER => cons2 u (cancel (t :: ts) us vs)); -(* uncancel *) - -fun uncancel_sums_tac _ [] = all_tac - | uncancel_sums_tac thy (t :: ts) = - Data.uncancel_tac (Thm.cterm_of thy t) THEN - uncancel_sums_tac thy ts; - - (* the simplification procedure *) fun proc ss t = @@ -66,9 +58,21 @@ val (ts', us', vs) = cancel ts us []; in if null vs then NONE - else SOME - (Data.prove_conv (uncancel_sums_tac thy vs) Data.norm_tac ss - (t, Data.mk_bal (Data.mk_sum ts', Data.mk_sum us'))) + else + let + val cert = Thm.cterm_of thy + val t' = Data.mk_sum ts' + val u' = Data.mk_sum us' + val v = Data.mk_sum vs + val t1 = Data.mk_bal (Data.mk_plus (v, t'), Data.mk_plus (v, u')) + val t2 = Data.mk_bal (t', u') + val goal1 = Thm.cterm_of thy (Logic.mk_equals (t, t1)) + val goal2 = Thm.cterm_of thy (Logic.mk_equals (t1, t2)) + val thm1 = Goal.prove_internal [] goal1 (K (Data.norm_tac ss)) + val thm2 = Goal.prove_internal [] goal2 (K (rtac Data.cancel_rule 1)) + in + SOME (Thm.transitive thm1 thm2) + end end); end;