# HG changeset patch # User paulson # Date 932743911 -7200 # Node ID eec20608c791bd46c9bf583a2f70b15b963483d1 # Parent 4e64b2bd10cec5c94fad6bb92fb796866b4bc64f removed the combine_coeff simproc because linear arith does not handle coefficients yet diff -r 4e64b2bd10ce -r eec20608c791 src/HOL/UNITY/Lift.ML --- a/src/HOL/UNITY/Lift.ML Fri Jul 23 17:30:27 1999 +0200 +++ b/src/HOL/UNITY/Lift.ML Fri Jul 23 17:31:51 1999 +0200 @@ -254,6 +254,11 @@ by (Blast_tac 1); qed "E_thm16a"; +(*Must sometimes delete them because they introduce multiplication*) +val metric_ss = simpset() delsimprocs [Int_CC.sum_conv, Int_CC.rel_conv] + addsimps metric_simps; + + (*lem_lift_5_1 has ~goingup instead of goingdown*) Goal "#0 \ \ Lift : (closed Int Req n Int {s. metric n s = N} Int goingdown) LeadsTo \ @@ -262,16 +267,15 @@ by (ensures_tac "req_down" 1); by Auto_tac; by (REPEAT_FIRST (eresolve_tac mov_metrics)); -by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps @ zcompare_rls))); +by (ALLGOALS (asm_simp_tac (metric_ss addsimps zcompare_rls))); by (Blast_tac 1); qed "E_thm16b"; - (*lem_lift_5_0 proves an intersection involving ~goingup and goingup, i.e. the trivial disjunction, leading to an asymmetrical proof.*) Goal "#0 Req n Int {s. metric n s = N} <= goingup Un goingdown"; -by (asm_simp_tac (simpset() addsimps metric_simps) 1); +by (asm_simp_tac metric_ss 1); by (force_tac (claset() delrules [impCE] addEs [impCE], simpset() addsimps conj_comms) 1); qed "E_thm16c"; @@ -294,7 +298,7 @@ Goal "[| metric n s = #0; Min <= floor s; floor s <= Max |] ==> floor s = n"; by (etac rev_mp 1); (*force simplification of "metric..." while in conclusion part*) -by (asm_simp_tac (simpset() addsimps metric_simps) 1); +by (asm_simp_tac metric_ss 1); qed "metric_eq_0D"; AddDs [metric_eq_0D]; @@ -309,7 +313,7 @@ qed "E_thm11"; val metric_tac = REPEAT (FIRSTGOAL (eresolve_tac mov_metrics)) - THEN auto_tac (claset(), simpset() addsimps metric_simps); + THEN auto_tac (claset(), metric_ss); (*lem_lift_3_5*) Goal