Refined arith tactic.
authornipkow
Sat Jan 09 15:24:11 1999 +0100 (1999-01-09)
changeset 6073fba734ba6894
parent 6072 5583261db33d
child 6074 34242451bc91
Refined arith tactic.
src/HOL/Arith.ML
src/HOL/Divides.ML
src/HOL/Integ/Bin.ML
src/HOL/List.ML
src/HOL/MiniML/Type.ML
src/HOL/MiniML/W.ML
src/HOL/Ord.ML
src/HOL/Real/PNat.ML
src/HOL/ex/Primes.ML
src/HOLCF/Fix.ML
     1.1 --- a/src/HOL/Arith.ML	Fri Jan 08 14:02:04 1999 +0100
     1.2 +++ b/src/HOL/Arith.ML	Sat Jan 09 15:24:11 1999 +0100
     1.3 @@ -855,6 +855,13 @@
     1.4  val not_lessD = leI;
     1.5  val sym = sym;
     1.6  
     1.7 +fun mkEqTrue thm = thm RS (eqTrueI RS eq_reflection);
     1.8 +val mk_Trueprop = HOLogic.mk_Trueprop;
     1.9 +
    1.10 +fun neg_prop(TP$(Const("Not",_)$t)) = (TP$t, true)
    1.11 +  | neg_prop(TP$t) =
    1.12 +      (TP $ (Const("Not",HOLogic.boolT-->HOLogic.boolT)$t), false);
    1.13 +
    1.14  (* Turn term into list of summand * multiplicity plus a constant *)
    1.15  fun poly(Const("Suc",_)$t, (p,i)) = poly(t, (p,i+1))
    1.16    | poly(Const("op +",_) $ s $ t, pi) = poly(s,poly(t,pi))
    1.17 @@ -916,9 +923,29 @@
    1.18  
    1.19  structure Fast_Nat_Arith = Fast_Lin_Arith(Nat_LA_Data);
    1.20  
    1.21 -simpset_ref () := (simpset() addSolver Fast_Nat_Arith.cut_lin_arith_tac);
    1.22 +val fast_nat_arith_tac = Fast_Nat_Arith.lin_arith_tac;
    1.23 +
    1.24 +local
    1.25 +fun prep_pat s = Thm.read_cterm (sign_of Arith.thy) (s, HOLogic.boolT);
    1.26 +
    1.27 +val pats = map prep_pat
    1.28 +  ["(m::nat) < n","(m::nat) <= n", "~ (m::nat) < n","~ (m::nat) <= n",
    1.29 +   "(m::nat) = n"]
    1.30  
    1.31 -val fast_nat_arith_tac = Fast_Nat_Arith.lin_arith_tac;
    1.32 +in
    1.33 +val fast_nat_arith_simproc =
    1.34 +  mk_simproc "fast_nat_arith" pats Fast_Nat_Arith.lin_arith_prover;
    1.35 +end;
    1.36 +
    1.37 +Addsimprocs [fast_nat_arith_simproc];
    1.38 +
    1.39 +(* Because of fast_nat_arith_simproc, the arithmetic solver is really only
    1.40 +useful to detect inconsistencies among the premises for subgoals which are
    1.41 +*not* themselves (in)equalities, because the latter activate
    1.42 +fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
    1.43 +solver all the time rather than add the additional check. *)
    1.44 +
    1.45 +simpset_ref () := (simpset() addSolver Fast_Nat_Arith.cut_lin_arith_tac);
    1.46  
    1.47  (* Elimination of `-' on nat due to John Harrison *)
    1.48  Goal "P(a - b::nat) = (!d. (b = a + d --> P 0) & (a = b + d --> P d))";
     2.1 --- a/src/HOL/Divides.ML	Fri Jan 08 14:02:04 1999 +0100
     2.2 +++ b/src/HOL/Divides.ML	Sat Jan 09 15:24:11 1999 +0100
     2.3 @@ -189,14 +189,13 @@
     2.4  (* Antimonotonicity of div in second argument *)
     2.5  Goal "[| 0<m; m<=n |] ==> (k div n) <= (k div m)";
     2.6  by (subgoal_tac "0<n" 1);
     2.7 - by (Simp_tac 2);
     2.8 + by (Asm_simp_tac 2);
     2.9  by (res_inst_tac [("n","k")] less_induct 1);
    2.10 -by (Simp_tac 1);
    2.11  by (rename_tac "k" 1);
    2.12  by (case_tac "k<n" 1);
    2.13   by (asm_simp_tac (simpset() addsimps [div_less]) 1);
    2.14  by (subgoal_tac "~(k<m)" 1);
    2.15 - by (Simp_tac 2);
    2.16 + by (Asm_simp_tac 2);
    2.17  by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
    2.18  by (subgoal_tac "(k-n) div n <= (k-m) div n" 1);
    2.19  by (REPEAT (eresolve_tac [div_le_mono,diff_le_mono2] 2));
    2.20 @@ -209,19 +208,18 @@
    2.21  by (subgoal_tac "m div n <= m div 1" 1);
    2.22  by (Asm_full_simp_tac 1);
    2.23  by (rtac div_le_mono2 1);
    2.24 -by (ALLGOALS Simp_tac);
    2.25 +by (ALLGOALS Asm_simp_tac);
    2.26  qed "div_le_dividend";
    2.27  Addsimps [div_le_dividend];
    2.28  
    2.29  (* Similar for "less than" *)
    2.30  Goal "1<n ==> (0 < m) --> (m div n < m)";
    2.31  by (res_inst_tac [("n","m")] less_induct 1);
    2.32 -by (Simp_tac 1);
    2.33  by (rename_tac "m" 1);
    2.34  by (case_tac "m<n" 1);
    2.35   by (asm_full_simp_tac (simpset() addsimps [div_less]) 1);
    2.36  by (subgoal_tac "0<n" 1);
    2.37 - by (Simp_tac 2);
    2.38 + by (Asm_simp_tac 2);
    2.39  by (asm_full_simp_tac (simpset() addsimps [div_geq]) 1);
    2.40  by (case_tac "n<m" 1);
    2.41   by (subgoal_tac "(m-n) div n < (m-n)" 1);
    2.42 @@ -230,7 +228,7 @@
    2.43   by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1);
    2.44  (* case n=m *)
    2.45  by (subgoal_tac "m=n" 1);
    2.46 - by (Simp_tac 2);
    2.47 + by (Asm_simp_tac 2);
    2.48  by (asm_simp_tac (simpset() addsimps [div_less]) 1);
    2.49  qed_spec_mp "div_less_dividend";
    2.50  Addsimps [div_less_dividend];
     3.1 --- a/src/HOL/Integ/Bin.ML	Fri Jan 08 14:02:04 1999 +0100
     3.2 +++ b/src/HOL/Integ/Bin.ML	Sat Jan 09 15:24:11 1999 +0100
     3.3 @@ -410,6 +410,10 @@
     3.4  val not_lessD = zleI;
     3.5  val sym = sym;
     3.6  
     3.7 +val mk_Trueprop = Nat_LA_Data.mk_Trueprop;
     3.8 +val neg_prop = Nat_LA_Data.neg_prop;
     3.9 +val mkEqTrue = Nat_LA_Data.mkEqTrue;
    3.10 +
    3.11  val intT = Type("IntDef.int",[]);
    3.12  
    3.13  (* borrowed from Bin.thy: *)
     4.1 --- a/src/HOL/List.ML	Fri Jan 08 14:02:04 1999 +0100
     4.2 +++ b/src/HOL/List.ML	Sat Jan 09 15:24:11 1999 +0100
     4.3 @@ -906,20 +906,10 @@
     4.4  by(induct_tac "j" 1);
     4.5   by(Simp_tac 1);
     4.6  by(asm_simp_tac (simpset() addsimps [nth_append,less_diff_conv]@add_ac) 1);
     4.7 -br conjI 1;
     4.8 - by(Clarify_tac 1);
     4.9 - bd add_lessD1 1;
    4.10 - by(Simp_tac 1);
    4.11 -by(Clarify_tac 1);
    4.12 -br conjI 1;
    4.13 - by(Clarify_tac 1);
    4.14 - by(subgoal_tac "n=i+k" 1);
    4.15 -  by(Asm_full_simp_tac 1);
    4.16 - by(Simp_tac 1);
    4.17  by(Clarify_tac 1);
    4.18  by(subgoal_tac "n=i+k" 1);
    4.19 - by(Asm_full_simp_tac 1);
    4.20 -by(Simp_tac 1);
    4.21 + by(Asm_simp_tac 2);
    4.22 +by(Asm_simp_tac 1);
    4.23  qed_spec_mp "nth_upt";
    4.24  Addsimps [nth_upt];
    4.25  
     5.1 --- a/src/HOL/MiniML/Type.ML	Fri Jan 08 14:02:04 1999 +0100
     5.2 +++ b/src/HOL/MiniML/Type.ML	Sat Jan 09 15:24:11 1999 +0100
     5.3 @@ -530,15 +530,6 @@
     5.4  qed "new_tv_not_free_tv";
     5.5  Addsimps [new_tv_not_free_tv];
     5.6  
     5.7 -Goalw [max_def] "!!n::nat. m < n ==> m < max n n'";
     5.8 -by (Auto_tac);
     5.9 -qed "less_maxL";
    5.10 -
    5.11 -Goalw [max_def] "!!n::nat. m < n' ==> m < max n n'";
    5.12 -by (Simp_tac 1);
    5.13 -by (fast_tac (claset() addDs [not_leE] addIs [less_trans]) 1);
    5.14 -val less_maxR = result();
    5.15 -
    5.16  Goalw [new_tv_def] "!!t::typ. ? n. (new_tv n t)";
    5.17  by (induct_tac "t" 1);
    5.18  by (res_inst_tac [("x","Suc nat")] exI 1);
    5.19 @@ -546,8 +537,8 @@
    5.20  by (REPEAT (etac exE 1));
    5.21  by (rename_tac "n'" 1);
    5.22  by (res_inst_tac [("x","max n n'")] exI 1);
    5.23 -by (Simp_tac 1);
    5.24 -by (fast_tac (claset() addIs [less_maxR,less_maxL]) 1);
    5.25 +by (simp_tac (simpset() addsimps [less_max_iff_disj]) 1);
    5.26 +by (Blast_tac 1);
    5.27  qed "fresh_variable_types";
    5.28  
    5.29  Addsimps [fresh_variable_types];
    5.30 @@ -561,21 +552,12 @@
    5.31  by (REPEAT (etac exE 1));
    5.32  by (rename_tac "n'" 1);
    5.33  by (res_inst_tac [("x","max n n'")] exI 1);
    5.34 -by (Simp_tac 1);
    5.35 -by (fast_tac (claset() addIs [less_maxR,less_maxL]) 1);
    5.36 +by (simp_tac (simpset() addsimps [less_max_iff_disj]) 1);
    5.37 +by (Blast_tac 1);
    5.38  qed "fresh_variable_type_schemes";
    5.39  
    5.40  Addsimps [fresh_variable_type_schemes];
    5.41  
    5.42 -Goalw [max_def] "!!n::nat. n <= (max n n')";
    5.43 -by (Simp_tac 1);
    5.44 -val le_maxL = result();
    5.45 -
    5.46 -Goalw [max_def] "!!n'::nat. n' <= (max n n')";
    5.47 -by (Simp_tac 1);
    5.48 -by (fast_tac (claset() addDs [not_leE] addIs [less_or_eq_imp_le]) 1);
    5.49 -val le_maxR = result();
    5.50 -
    5.51  Goal "!!A::type_scheme list. ? n. (new_tv n A)";
    5.52  by (induct_tac "A" 1);
    5.53  by (Simp_tac 1);
    5.54 @@ -588,7 +570,7 @@
    5.55  by (subgoal_tac "n <= (max n n')" 1);
    5.56  by (subgoal_tac "n' <= (max n n')" 1);
    5.57  by (fast_tac (claset() addDs [new_tv_le]) 1);
    5.58 -by (ALLGOALS (simp_tac (simpset() addsimps [le_maxR,le_maxL])));
    5.59 +by (ALLGOALS (simp_tac (simpset() addsimps [le_max_iff_disj])));
    5.60  qed "fresh_variable_type_scheme_lists";
    5.61  
    5.62  Addsimps [fresh_variable_type_scheme_lists];
    5.63 @@ -600,7 +582,7 @@
    5.64  by (subgoal_tac "n1 <= max n1 n2" 1);
    5.65  by (subgoal_tac "n2 <= max n1 n2" 1);
    5.66  by (fast_tac (claset() addDs [new_tv_le]) 1);
    5.67 -by (ALLGOALS (simp_tac (simpset() addsimps [le_maxL,le_maxR])));
    5.68 +by (ALLGOALS (simp_tac (simpset() addsimps [le_max_iff_disj])));
    5.69  qed "make_one_new_out_of_two";
    5.70  
    5.71  Goal "!!(A::type_scheme list) (A'::type_scheme list) (t::typ) (t'::typ). \
    5.72 @@ -620,7 +602,8 @@
    5.73  by (rename_tac "n2 n1" 1);
    5.74  by (res_inst_tac [("x","(max n1 n2)")] exI 1);
    5.75  by (rewtac new_tv_def);
    5.76 -by (fast_tac (claset() addIs [less_maxL,less_maxR]) 1);
    5.77 +by (simp_tac (simpset() addsimps [less_max_iff_disj]) 1);
    5.78 +by (Blast_tac 1);
    5.79  qed "ex_fresh_variable";
    5.80  
    5.81  (* mgu does not introduce new type variables *)
     6.1 --- a/src/HOL/MiniML/W.ML	Fri Jan 08 14:02:04 1999 +0100
     6.2 +++ b/src/HOL/MiniML/W.ML	Sat Jan 09 15:24:11 1999 +0100
     6.3 @@ -62,10 +62,6 @@
     6.4  by (rtac add_le_mono 1);
     6.5   by (Simp_tac 1);
     6.6  by (simp_tac (simpset() addsimps [max_def]) 1);
     6.7 -by (strip_tac 1);
     6.8 -by (dtac not_leE 1);
     6.9 -by (rtac less_or_eq_imp_le 1);
    6.10 -by (Fast_tac 1);
    6.11  qed_spec_mp "new_tv_bound_typ_inst_sch";
    6.12  
    6.13  Addsimps [new_tv_bound_typ_inst_sch];
     7.1 --- a/src/HOL/Ord.ML	Fri Jan 08 14:02:04 1999 +0100
     7.2 +++ b/src/HOL/Ord.ML	Sat Jan 09 15:24:11 1999 +0100
     7.3 @@ -55,6 +55,13 @@
     7.4  (* [| n<m;  ~P ==> m<n |] ==> P *)
     7.5  bind_thm ("order_less_asym", order_less_not_sym RS swap);
     7.6  
     7.7 +(* Transitivity *)
     7.8 +
     7.9 +Goal "!!x::'a::order. [| x < y; y < z |] ==> x < z";
    7.10 +by (asm_full_simp_tac (simpset() addsimps [order_less_le]) 1);
    7.11 +by (blast_tac (claset() addIs [order_trans,order_antisym]) 1);
    7.12 +qed "order_less_trans";
    7.13 +
    7.14  
    7.15  (** Useful for simplification, but too risky to include by default. **)
    7.16  
    7.17 @@ -103,6 +110,12 @@
    7.18  by (blast_tac (claset() addIs [order_trans]) 1);
    7.19  qed "le_max_iff_disj";
    7.20  
    7.21 +Goalw [max_def] "!!z::'a::linorder. (z < max x y) = (z < x | z < y)";
    7.22 +by (simp_tac (simpset() addsimps [order_le_less]) 1);
    7.23 +by (cut_facts_tac [linorder_less_linear] 1);
    7.24 +by (blast_tac (claset() addIs [order_less_trans]) 1);
    7.25 +qed "less_max_iff_disj";
    7.26 +
    7.27  Goalw [max_def] "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)";
    7.28  by (Simp_tac 1);
    7.29  by (cut_facts_tac [linorder_linear] 1);
     8.1 --- a/src/HOL/Real/PNat.ML	Fri Jan 08 14:02:04 1999 +0100
     8.2 +++ b/src/HOL/Real/PNat.ML	Sat Jan 09 15:24:11 1999 +0100
     8.3 @@ -456,7 +456,6 @@
     8.4  Goal "m + k <= n --> m <= (n::pnat)";
     8.5  by (simp_tac (simpset() addsimps [pnat_le_iff_Rep_pnat_le,
     8.6      sum_Rep_pnat_sum RS sym]) 1);
     8.7 -by (fast_tac (claset() addIs [add_leD1]) 1);
     8.8  qed_spec_mp "pnat_add_leD1";
     8.9  
    8.10  Goal "!!n::pnat. m + k <= n ==> k <= n";
     9.1 --- a/src/HOL/ex/Primes.ML	Fri Jan 08 14:02:04 1999 +0100
     9.2 +++ b/src/HOL/ex/Primes.ML	Sat Jan 09 15:24:11 1999 +0100
     9.3 @@ -47,7 +47,6 @@
     9.4  Goal "0<n ==> gcd(m,n) = gcd (n, m mod n)";
     9.5  by (rtac (gcd_eq RS trans) 1);
     9.6  by (Asm_simp_tac 1);
     9.7 -by (Blast_tac 1);
     9.8  qed "gcd_non_0";
     9.9  
    9.10  Goal "gcd(m,1) = 1";
    10.1 --- a/src/HOLCF/Fix.ML	Fri Jan 08 14:02:04 1999 +0100
    10.2 +++ b/src/HOLCF/Fix.ML	Sat Jan 09 15:24:11 1999 +0100
    10.3 @@ -689,7 +689,7 @@
    10.4          ALLGOALS Asm_simp_tac
    10.5          ]);
    10.6  
    10.7 -  val adm_disj_lemma4 = prove_goal Nat.thy
    10.8 +  val adm_disj_lemma4 = prove_goal Arith.thy
    10.9    "!!Q. !j. i < j --> Q(Y(j))  ==> !n. Q( if n < Suc i then Y(Suc i) else Y n)"
   10.10   (fn _ =>
   10.11          [Asm_simp_tac 1]);
   10.12 @@ -701,10 +701,10 @@
   10.13          [
   10.14          safe_tac (HOL_cs addSIs [lub_equal2,adm_disj_lemma3]),
   10.15          atac 2,
   10.16 -        Asm_simp_tac 1,
   10.17          res_inst_tac [("x","i")] exI 1,
   10.18 -        strip_tac 1,
   10.19 -        Simp_tac 1
   10.20 +        Simp_tac 1,
   10.21 +	strip_tac 1,
   10.22 +        Asm_simp_tac 1
   10.23          ]);
   10.24  
   10.25    val adm_disj_lemma6 = prove_goal thy