removed the combine_coeff simproc because linear arith does not handle
authorpaulson
Fri Jul 23 17:31:51 1999 +0200 (1999-07-23)
changeset 7079eec20608c791
parent 7078 4e64b2bd10ce
child 7080 b551a5a8966c
removed the combine_coeff simproc because linear arith does not handle
coefficients yet
src/HOL/UNITY/Lift.ML
     1.1 --- a/src/HOL/UNITY/Lift.ML	Fri Jul 23 17:30:27 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Lift.ML	Fri Jul 23 17:31:51 1999 +0200
     1.3 @@ -254,6 +254,11 @@
     1.4  by (Blast_tac 1);
     1.5  qed "E_thm16a";
     1.6  
     1.7 +(*Must sometimes delete them because they introduce multiplication*)
     1.8 +val metric_ss = simpset() delsimprocs [Int_CC.sum_conv, Int_CC.rel_conv]
     1.9 +                          addsimps metric_simps;
    1.10 +
    1.11 +
    1.12  (*lem_lift_5_1 has ~goingup instead of goingdown*)
    1.13  Goal "#0<N ==>   \
    1.14  \     Lift : (closed Int Req n Int {s. metric n s = N} Int goingdown) LeadsTo \
    1.15 @@ -262,16 +267,15 @@
    1.16  by (ensures_tac "req_down" 1);
    1.17  by Auto_tac;
    1.18  by (REPEAT_FIRST (eresolve_tac mov_metrics));
    1.19 -by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps @ zcompare_rls)));
    1.20 +by (ALLGOALS (asm_simp_tac (metric_ss addsimps zcompare_rls)));
    1.21  by (Blast_tac 1);
    1.22  qed "E_thm16b";
    1.23  
    1.24  
    1.25 -
    1.26  (*lem_lift_5_0 proves an intersection involving ~goingup and goingup,
    1.27    i.e. the trivial disjunction, leading to an asymmetrical proof.*)
    1.28  Goal "#0<N ==> Req n Int {s. metric n s = N} <= goingup Un goingdown";
    1.29 -by (asm_simp_tac (simpset() addsimps metric_simps) 1);
    1.30 +by (asm_simp_tac metric_ss 1);
    1.31  by (force_tac (claset() delrules [impCE] addEs [impCE], 
    1.32  	       simpset() addsimps conj_comms) 1);
    1.33  qed "E_thm16c";
    1.34 @@ -294,7 +298,7 @@
    1.35  Goal "[| metric n s = #0;  Min <= floor s;  floor s <= Max |] ==> floor s = n";
    1.36  by (etac rev_mp 1);
    1.37  (*force simplification of "metric..." while in conclusion part*)
    1.38 -by (asm_simp_tac (simpset() addsimps metric_simps) 1);
    1.39 +by (asm_simp_tac metric_ss 1);
    1.40  qed "metric_eq_0D";
    1.41  
    1.42  AddDs [metric_eq_0D];
    1.43 @@ -309,7 +313,7 @@
    1.44  qed "E_thm11";
    1.45  
    1.46  val metric_tac = REPEAT (FIRSTGOAL (eresolve_tac mov_metrics))
    1.47 -                 THEN auto_tac (claset(), simpset() addsimps metric_simps);
    1.48 +                 THEN auto_tac (claset(), metric_ss);
    1.49  
    1.50  (*lem_lift_3_5*)
    1.51  Goal