Converted 1 to 1'
authorpaulson
Mon Aug 06 16:43:40 2001 +0200 (2001-08-06)
changeset 114671064effe37f6
parent 11466 d64ccdeaf9ae
child 11468 02cd5d5bc497
Converted 1 to 1'
src/HOL/UNITY/Extend.ML
src/HOL/UNITY/Lift_prog.ML
src/HOL/UNITY/Simple/Network.ML
src/HOL/UNITY/Simple/Reachability.ML
src/HOL/UNITY/Simple/Reachability.thy
src/HOL/UNITY/Union.ML
     1.1 --- a/src/HOL/UNITY/Extend.ML	Mon Aug 06 15:54:29 2001 +0200
     1.2 +++ b/src/HOL/UNITY/Extend.ML	Mon Aug 06 16:43:40 2001 +0200
     1.3 @@ -753,14 +753,11 @@
     1.4  by (auto_tac (claset(), simpset() addsimps [ok_def]));  
     1.5  qed "ok_extend_iff";
     1.6  
     1.7 -Unify.search_bound := 40;
     1.8 -Unify.trace_bound  := 40;
     1.9 -
    1.10 -Goal "OK I (%i. extend h (F i)) = (OK I F)";
    1.11 -by (auto_tac (claset(), simpset() addsimps [OK_def]));  
    1.12 +Goalw [OK_def] "OK I (%i. extend h (F i)) = (OK I F)";
    1.13 +by Safe_tac;
    1.14  by (dres_inst_tac [("x","i")] bspec 1); 
    1.15 -by (dres_inst_tac [("x","j")] bspec 2); 
    1.16 -by Auto_tac;  
    1.17 +by (dres_inst_tac [("x","j")] bspec 2);  
    1.18 +by (REPEAT (Force_tac 1));
    1.19  qed "OK_extend_iff";
    1.20  
    1.21  Goal "F : X guarantees Y ==> \
     2.1 --- a/src/HOL/UNITY/Lift_prog.ML	Mon Aug 06 15:54:29 2001 +0200
     2.2 +++ b/src/HOL/UNITY/Lift_prog.ML	Mon Aug 06 16:43:40 2001 +0200
     2.3 @@ -309,7 +309,7 @@
     2.4  Goal "(insert_map j t f)(i := s) = \
     2.5  \     (if i=j then insert_map i s f \
     2.6  \      else if i<j then insert_map j t (f(i:=s)) \
     2.7 -\      else insert_map j t (f(i-1:=s)))";
     2.8 +\      else insert_map j t (f(i-1' := s)))";
     2.9  by (rtac ext 1);
    2.10  by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
    2.11  by (ALLGOALS arith_tac);
    2.12 @@ -341,7 +341,7 @@
    2.13  by (dtac subsetD 1);
    2.14  by (Blast_tac 1);
    2.15  by Auto_tac;
    2.16 -ren "s f uu s' f' uu'" 1;
    2.17 +by (rename_tac "s f uu s' f' uu'" 1);
    2.18  by (subgoal_tac "f'=f & uu'=uu" 1);
    2.19  by (force_tac (claset() addSDs [preserves_imp_eq], simpset()) 2);
    2.20  by Auto_tac;
     3.1 --- a/src/HOL/UNITY/Simple/Network.ML	Mon Aug 06 15:54:29 2001 +0200
     3.2 +++ b/src/HOL/UNITY/Simple/Network.ML	Mon Aug 06 16:43:40 2001 +0200
     3.3 @@ -14,11 +14,11 @@
     3.4  \      !! m. F : stable {s. s(Aproc,Rcvd) <= s(Bproc,Sent)};  \
     3.5  \      !! m proc. F : stable {s. m <= s(proc,Sent)};  \
     3.6  \      !! n proc. F : stable {s. n <= s(proc,Rcvd)};  \
     3.7 -\      !! m proc. F : {s. s(proc,Idle) = 1 & s(proc,Rcvd) = m} co \
     3.8 -\                                 {s. s(proc,Rcvd) = m --> s(proc,Idle) = 1}; \
     3.9 -\      !! n proc. F : {s. s(proc,Idle) = 1 & s(proc,Sent) = n} co \
    3.10 +\      !! m proc. F : {s. s(proc,Idle) = 1' & s(proc,Rcvd) = m} co \
    3.11 +\                                 {s. s(proc,Rcvd) = m --> s(proc,Idle) = 1'}; \
    3.12 +\      !! n proc. F : {s. s(proc,Idle) = 1' & s(proc,Sent) = n} co \
    3.13  \                                 {s. s(proc,Sent) = n} \
    3.14 -\   |] ==> F : stable {s. s(Aproc,Idle) = 1 & s(Bproc,Idle) = 1 & \
    3.15 +\   |] ==> F : stable {s. s(Aproc,Idle) = 1' & s(Bproc,Idle) = 1' & \
    3.16  \                         s(Aproc,Sent) = s(Bproc,Rcvd) & \
    3.17  \                         s(Bproc,Sent) = s(Aproc,Rcvd) & \
    3.18  \                         s(Aproc,Rcvd) = m & s(Bproc,Rcvd) = n}";
     4.1 --- a/src/HOL/UNITY/Simple/Reachability.ML	Mon Aug 06 15:54:29 2001 +0200
     4.2 +++ b/src/HOL/UNITY/Simple/Reachability.ML	Mon Aug 06 16:43:40 2001 +0200
     4.3 @@ -162,7 +162,7 @@
     4.4  
     4.5  
     4.6  Goalw [nmsg_gte_def, nmsg_lte_def,nmsg_gt_def, nmsg_eq_def]
     4.7 -     "((nmsg_gte 0 (v,w) Int nmsg_lte 1 (v,w)) Int (- nmsg_gt 0 (v,w) Un A)) \
     4.8 +     "((nmsg_gte 0 (v,w) Int nmsg_lte 1' (v,w)) Int (- nmsg_gt 0 (v,w) Un A)) \
     4.9  \     <= A Un nmsg_eq 0 (v,w)";
    4.10  by Auto_tac;
    4.11  qed "lemma4";
    4.12 @@ -170,7 +170,7 @@
    4.13  
    4.14  Goalw [nmsg_gte_def,nmsg_lte_def,nmsg_gt_def, nmsg_eq_def]
    4.15       "reachable v Int nmsg_eq 0 (v,w) = \
    4.16 -\     ((nmsg_gte 0 (v,w) Int nmsg_lte 1 (v,w)) Int \
    4.17 +\     ((nmsg_gte 0 (v,w) Int nmsg_lte 1' (v,w)) Int \
    4.18  \      (reachable v Int nmsg_lte 0 (v,w)))";
    4.19  by Auto_tac;
    4.20  qed "lemma5";
     5.1 --- a/src/HOL/UNITY/Simple/Reachability.thy	Mon Aug 06 15:54:29 2001 +0200
     5.2 +++ b/src/HOL/UNITY/Simple/Reachability.thy	Mon Aug 06 16:43:40 2001 +0200
     5.3 @@ -60,7 +60,7 @@
     5.4  
     5.5      MA4  "[|(v,w) : E|] ==> F : Always (-(reachable v) Un (nmsg_gt 0 (v,w)) Un (reachable w))"
     5.6  
     5.7 -    MA5  "[|v:V;w:V|] ==> F : Always (nmsg_gte 0 (v,w) Int nmsg_lte 1 (v,w))"
     5.8 +    MA5  "[|v:V;w:V|] ==> F : Always (nmsg_gte 0 (v,w) Int nmsg_lte 1' (v,w))"
     5.9  
    5.10      MA6  "[|v:V|] ==> F : Stable (reachable v)"
    5.11  
     6.1 --- a/src/HOL/UNITY/Union.ML	Mon Aug 06 15:54:29 2001 +0200
     6.2 +++ b/src/HOL/UNITY/Union.ML	Mon Aug 06 16:43:40 2001 +0200
     6.3 @@ -352,7 +352,7 @@
     6.4  
     6.5  bind_thm ("ok_sym", ok_commute RS iffD1);
     6.6  
     6.7 -Goal "OK {(0,F),(1,G),(2,H)} snd = (F ok G & (F Join G) ok H)";
     6.8 +Goal "OK {(#0::int,F),(#1,G),(#2,H)} snd = (F ok G & (F Join G) ok H)";
     6.9  by (asm_full_simp_tac
    6.10      (simpset() addsimps [Ball_def, conj_disj_distribR, ok_def, Join_def, 
    6.11                     OK_def, insert_absorb, all_conj_distrib, eq_commute]) 1);