make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests
authorhuffman
Fri Jul 20 10:53:25 2012 +0200 (2012-07-20)
changeset 48372868dc809c8a2
parent 48371 3a5a5a992519
child 48374 623607c5a40f
make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests
src/HOL/Tools/arith_data.ML
src/HOL/Tools/nat_arith.ML
src/HOL/ex/Simproc_Tests.thy
src/Provers/Arith/cancel_sums.ML
     1.1 --- a/src/HOL/Tools/arith_data.ML	Thu Jul 19 22:21:59 2012 +0200
     1.2 +++ b/src/HOL/Tools/arith_data.ML	Fri Jul 20 10:53:25 2012 +0200
     1.3 @@ -112,7 +112,8 @@
     1.4  
     1.5  fun simp_all_tac rules =
     1.6    let val ss0 = HOL_ss addsimps rules
     1.7 -  in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
     1.8 +      val safe_simp_tac = generic_simp_tac true (false, false, false)
     1.9 +  in fn ss => ALLGOALS (safe_simp_tac (Simplifier.inherit_context ss ss0)) end;
    1.10  
    1.11  fun simplify_meta_eq rules =
    1.12    let val ss0 = HOL_basic_ss addsimps rules |> Simplifier.add_eqcong @{thm eq_cong2}
     2.1 --- a/src/HOL/Tools/nat_arith.ML	Thu Jul 19 22:21:59 2012 +0200
     2.2 +++ b/src/HOL/Tools/nat_arith.ML	Fri Jul 20 10:53:25 2012 +0200
     2.3 @@ -49,13 +49,11 @@
     2.4  struct
     2.5    val mk_sum = mk_norm_sum;
     2.6    val dest_sum = dest_sum;
     2.7 -  val prove_conv = Arith_Data.prove_conv2;
     2.8 +  val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
     2.9    val norm_tac1 = Arith_Data.simp_all_tac [@{thm add_Suc}, @{thm add_Suc_right},
    2.10      @{thm Nat.add_0}, @{thm Nat.add_0_right}];
    2.11    val norm_tac2 = Arith_Data.simp_all_tac @{thms add_ac};
    2.12    fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
    2.13 -  fun gen_uncancel_tac rule = let val rule' = rule RS @{thm subst_equals}
    2.14 -    in fn ct => rtac (instantiate' [] [NONE, SOME ct] rule') 1 end;
    2.15  end;
    2.16  
    2.17  structure EqCancelSums = CancelSumsFun
    2.18 @@ -63,7 +61,7 @@
    2.19    open CommonCancelSums;
    2.20    val mk_bal = HOLogic.mk_eq;
    2.21    val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT;
    2.22 -  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel"};
    2.23 +  val cancel_rule = mk_meta_eq @{thm nat_add_left_cancel};
    2.24  end);
    2.25  
    2.26  structure LessCancelSums = CancelSumsFun
    2.27 @@ -71,7 +69,7 @@
    2.28    open CommonCancelSums;
    2.29    val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less};
    2.30    val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT;
    2.31 -  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
    2.32 +  val cancel_rule = mk_meta_eq @{thm nat_add_left_cancel_less};
    2.33  end);
    2.34  
    2.35  structure LeCancelSums = CancelSumsFun
    2.36 @@ -79,7 +77,7 @@
    2.37    open CommonCancelSums;
    2.38    val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq};
    2.39    val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT;
    2.40 -  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
    2.41 +  val cancel_rule = mk_meta_eq @{thm nat_add_left_cancel_le};
    2.42  end);
    2.43  
    2.44  structure DiffCancelSums = CancelSumsFun
    2.45 @@ -87,7 +85,7 @@
    2.46    open CommonCancelSums;
    2.47    val mk_bal = HOLogic.mk_binop @{const_name Groups.minus};
    2.48    val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} HOLogic.natT;
    2.49 -  val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"};
    2.50 +  val cancel_rule = mk_meta_eq @{thm diff_cancel};
    2.51  end);
    2.52  
    2.53  val nat_cancel_sums_add =
     3.1 --- a/src/HOL/ex/Simproc_Tests.thy	Thu Jul 19 22:21:59 2012 +0200
     3.2 +++ b/src/HOL/ex/Simproc_Tests.thy	Fri Jul 20 10:53:25 2012 +0200
     3.3 @@ -5,14 +5,14 @@
     3.4  header {* Testing of arithmetic simprocs *}
     3.5  
     3.6  theory Simproc_Tests
     3.7 -imports (*Main*) "../Numeral_Simprocs"
     3.8 +imports Main
     3.9  begin
    3.10  
    3.11  text {*
    3.12 -  This theory tests the various simprocs defined in
    3.13 -  @{file "~~/src/HOL/Numeral_Simprocs.thy"}. Many of the tests
    3.14 -  are derived from commented-out code originally found in
    3.15 -  @{file "~~/src/HOL/Tools/numeral_simprocs.ML"}.
    3.16 +  This theory tests the various simprocs defined in @{file
    3.17 +  "~~/src/HOL/Nat.thy"} and @{file "~~/src/HOL/Numeral_Simprocs.thy"}.
    3.18 +  Many of the tests are derived from commented-out code originally
    3.19 +  found in @{file "~~/src/HOL/Tools/numeral_simprocs.ML"}.
    3.20  *}
    3.21  
    3.22  subsection {* ML bindings *}
    3.23 @@ -21,6 +21,29 @@
    3.24    fun test ps = CHANGED (asm_simp_tac (HOL_basic_ss addsimprocs ps) 1)
    3.25  *}
    3.26  
    3.27 +subsection {* Cancellation simprocs from @{text Nat.thy} *}
    3.28 +
    3.29 +notepad begin
    3.30 +  fix a b c d :: nat
    3.31 +  {
    3.32 +    assume "b = Suc c" have "a + b = Suc (c + a)"
    3.33 +      by (tactic {* test [nth Nat_Arith.nat_cancel_sums 0] *}) fact
    3.34 +  next
    3.35 +    assume "b < Suc c" have "a + b < Suc (c + a)"
    3.36 +      by (tactic {* test [nth Nat_Arith.nat_cancel_sums 1] *}) fact
    3.37 +  next
    3.38 +    assume "b \<le> Suc c" have "a + b \<le> Suc (c + a)"
    3.39 +      by (tactic {* test [nth Nat_Arith.nat_cancel_sums 2] *}) fact
    3.40 +  next
    3.41 +    assume "b - Suc c = d" have "a + b - Suc (c + a) = d"
    3.42 +      by (tactic {* test [nth Nat_Arith.nat_cancel_sums 3] *}) fact
    3.43 +  }
    3.44 +end
    3.45 +
    3.46 +schematic_lemma "\<And>(y::?'b::size). size (?x::?'a::size) \<le> size y + size ?x"
    3.47 +  by (tactic {* test [nth Nat_Arith.nat_cancel_sums 2] *}) (rule le0)
    3.48 +(* TODO: test more simprocs with schematic variables *)
    3.49 +
    3.50  subsection {* Abelian group cancellation simprocs *}
    3.51  
    3.52  notepad begin
     4.1 --- a/src/Provers/Arith/cancel_sums.ML	Thu Jul 19 22:21:59 2012 +0200
     4.2 +++ b/src/Provers/Arith/cancel_sums.ML	Fri Jul 20 10:53:25 2012 +0200
     4.3 @@ -13,12 +13,12 @@
     4.4    (*abstract syntax*)
     4.5    val mk_sum: term list -> term
     4.6    val dest_sum: term -> term list
     4.7 +  val mk_plus: term * term -> term
     4.8    val mk_bal: term * term -> term
     4.9    val dest_bal: term -> term * term
    4.10    (*rules*)
    4.11 -  val prove_conv: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
    4.12    val norm_tac: simpset -> tactic            (*AC0 etc.*)
    4.13 -  val uncancel_tac: cterm -> tactic          (*apply A ~~ B  ==  x + A ~~ x + B*)
    4.14 +  val cancel_rule: thm                       (* x + A ~~ x + B == A ~~ B *)
    4.15  end;
    4.16  
    4.17  signature CANCEL_SUMS =
    4.18 @@ -46,14 +46,6 @@
    4.19        | GREATER => cons2 u (cancel (t :: ts) us vs));
    4.20  
    4.21  
    4.22 -(* uncancel *)
    4.23 -
    4.24 -fun uncancel_sums_tac _ [] = all_tac
    4.25 -  | uncancel_sums_tac thy (t :: ts) =
    4.26 -      Data.uncancel_tac (Thm.cterm_of thy t) THEN
    4.27 -      uncancel_sums_tac thy ts;
    4.28 -
    4.29 -
    4.30  (* the simplification procedure *)
    4.31  
    4.32  fun proc ss t =
    4.33 @@ -66,9 +58,21 @@
    4.34          val (ts', us', vs) = cancel ts us [];
    4.35        in
    4.36          if null vs then NONE
    4.37 -        else SOME
    4.38 -          (Data.prove_conv (uncancel_sums_tac thy vs) Data.norm_tac ss
    4.39 -            (t, Data.mk_bal (Data.mk_sum ts', Data.mk_sum us')))
    4.40 +        else
    4.41 +          let
    4.42 +            val cert = Thm.cterm_of thy
    4.43 +            val t' = Data.mk_sum ts'
    4.44 +            val u' = Data.mk_sum us'
    4.45 +            val v = Data.mk_sum vs
    4.46 +            val t1 = Data.mk_bal (Data.mk_plus (v, t'), Data.mk_plus (v, u'))
    4.47 +            val t2 = Data.mk_bal (t', u')
    4.48 +            val goal1 = Thm.cterm_of thy (Logic.mk_equals (t, t1))
    4.49 +            val goal2 = Thm.cterm_of thy (Logic.mk_equals (t1, t2))
    4.50 +            val thm1 = Goal.prove_internal [] goal1 (K (Data.norm_tac ss))
    4.51 +            val thm2 = Goal.prove_internal [] goal2 (K (rtac Data.cancel_rule 1))
    4.52 +          in
    4.53 +            SOME (Thm.transitive thm1 thm2)
    4.54 +          end
    4.55        end);
    4.56  
    4.57  end;