--- a/src/HOL/UNITY/Extend.ML Mon Aug 06 15:54:29 2001 +0200
+++ b/src/HOL/UNITY/Extend.ML Mon Aug 06 16:43:40 2001 +0200
@@ -753,14 +753,11 @@
by (auto_tac (claset(), simpset() addsimps [ok_def]));
qed "ok_extend_iff";
-Unify.search_bound := 40;
-Unify.trace_bound := 40;
-
-Goal "OK I (%i. extend h (F i)) = (OK I F)";
-by (auto_tac (claset(), simpset() addsimps [OK_def]));
+Goalw [OK_def] "OK I (%i. extend h (F i)) = (OK I F)";
+by Safe_tac;
by (dres_inst_tac [("x","i")] bspec 1);
-by (dres_inst_tac [("x","j")] bspec 2);
-by Auto_tac;
+by (dres_inst_tac [("x","j")] bspec 2);
+by (REPEAT (Force_tac 1));
qed "OK_extend_iff";
Goal "F : X guarantees Y ==> \
--- a/src/HOL/UNITY/Lift_prog.ML Mon Aug 06 15:54:29 2001 +0200
+++ b/src/HOL/UNITY/Lift_prog.ML Mon Aug 06 16:43:40 2001 +0200
@@ -309,7 +309,7 @@
Goal "(insert_map j t f)(i := s) = \
\ (if i=j then insert_map i s f \
\ else if i<j then insert_map j t (f(i:=s)) \
-\ else insert_map j t (f(i-1:=s)))";
+\ else insert_map j t (f(i-1' := s)))";
by (rtac ext 1);
by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
by (ALLGOALS arith_tac);
@@ -341,7 +341,7 @@
by (dtac subsetD 1);
by (Blast_tac 1);
by Auto_tac;
-ren "s f uu s' f' uu'" 1;
+by (rename_tac "s f uu s' f' uu'" 1);
by (subgoal_tac "f'=f & uu'=uu" 1);
by (force_tac (claset() addSDs [preserves_imp_eq], simpset()) 2);
by Auto_tac;
--- a/src/HOL/UNITY/Simple/Network.ML Mon Aug 06 15:54:29 2001 +0200
+++ b/src/HOL/UNITY/Simple/Network.ML Mon Aug 06 16:43:40 2001 +0200
@@ -14,11 +14,11 @@
\ !! m. F : stable {s. s(Aproc,Rcvd) <= s(Bproc,Sent)}; \
\ !! m proc. F : stable {s. m <= s(proc,Sent)}; \
\ !! n proc. F : stable {s. n <= s(proc,Rcvd)}; \
-\ !! m proc. F : {s. s(proc,Idle) = 1 & s(proc,Rcvd) = m} co \
-\ {s. s(proc,Rcvd) = m --> s(proc,Idle) = 1}; \
-\ !! n proc. F : {s. s(proc,Idle) = 1 & s(proc,Sent) = n} co \
+\ !! m proc. F : {s. s(proc,Idle) = 1' & s(proc,Rcvd) = m} co \
+\ {s. s(proc,Rcvd) = m --> s(proc,Idle) = 1'}; \
+\ !! n proc. F : {s. s(proc,Idle) = 1' & s(proc,Sent) = n} co \
\ {s. s(proc,Sent) = n} \
-\ |] ==> F : stable {s. s(Aproc,Idle) = 1 & s(Bproc,Idle) = 1 & \
+\ |] ==> F : stable {s. s(Aproc,Idle) = 1' & s(Bproc,Idle) = 1' & \
\ s(Aproc,Sent) = s(Bproc,Rcvd) & \
\ s(Bproc,Sent) = s(Aproc,Rcvd) & \
\ s(Aproc,Rcvd) = m & s(Bproc,Rcvd) = n}";
--- a/src/HOL/UNITY/Simple/Reachability.ML Mon Aug 06 15:54:29 2001 +0200
+++ b/src/HOL/UNITY/Simple/Reachability.ML Mon Aug 06 16:43:40 2001 +0200
@@ -162,7 +162,7 @@
Goalw [nmsg_gte_def, nmsg_lte_def,nmsg_gt_def, nmsg_eq_def]
- "((nmsg_gte 0 (v,w) Int nmsg_lte 1 (v,w)) Int (- nmsg_gt 0 (v,w) Un A)) \
+ "((nmsg_gte 0 (v,w) Int nmsg_lte 1' (v,w)) Int (- nmsg_gt 0 (v,w) Un A)) \
\ <= A Un nmsg_eq 0 (v,w)";
by Auto_tac;
qed "lemma4";
@@ -170,7 +170,7 @@
Goalw [nmsg_gte_def,nmsg_lte_def,nmsg_gt_def, nmsg_eq_def]
"reachable v Int nmsg_eq 0 (v,w) = \
-\ ((nmsg_gte 0 (v,w) Int nmsg_lte 1 (v,w)) Int \
+\ ((nmsg_gte 0 (v,w) Int nmsg_lte 1' (v,w)) Int \
\ (reachable v Int nmsg_lte 0 (v,w)))";
by Auto_tac;
qed "lemma5";
--- a/src/HOL/UNITY/Simple/Reachability.thy Mon Aug 06 15:54:29 2001 +0200
+++ b/src/HOL/UNITY/Simple/Reachability.thy Mon Aug 06 16:43:40 2001 +0200
@@ -60,7 +60,7 @@
MA4 "[|(v,w) : E|] ==> F : Always (-(reachable v) Un (nmsg_gt 0 (v,w)) Un (reachable w))"
- MA5 "[|v:V;w:V|] ==> F : Always (nmsg_gte 0 (v,w) Int nmsg_lte 1 (v,w))"
+ MA5 "[|v:V;w:V|] ==> F : Always (nmsg_gte 0 (v,w) Int nmsg_lte 1' (v,w))"
MA6 "[|v:V|] ==> F : Stable (reachable v)"
--- a/src/HOL/UNITY/Union.ML Mon Aug 06 15:54:29 2001 +0200
+++ b/src/HOL/UNITY/Union.ML Mon Aug 06 16:43:40 2001 +0200
@@ -352,7 +352,7 @@
bind_thm ("ok_sym", ok_commute RS iffD1);
-Goal "OK {(0,F),(1,G),(2,H)} snd = (F ok G & (F Join G) ok H)";
+Goal "OK {(#0::int,F),(#1,G),(#2,H)} snd = (F ok G & (F Join G) ok H)";
by (asm_full_simp_tac
(simpset() addsimps [Ball_def, conj_disj_distribR, ok_def, Join_def,
OK_def, insert_absorb, all_conj_distrib, eq_commute]) 1);