Partial conversion of UNITY to Isar new-style theories
authorpaulson
Fri Jan 24 14:06:49 2003 +0100 (2003-01-24)
changeset 13785e2fcd88be55d
parent 13784 b9f6154427a4
child 13786 ab8f39f48a6f
Partial conversion of UNITY to Isar new-style theories
src/HOL/IsaMakefile
src/HOL/UNITY/Detects.ML
src/HOL/UNITY/Detects.thy
src/HOL/UNITY/ROOT.ML
src/HOL/UNITY/Simple/Channel.ML
src/HOL/UNITY/Simple/Channel.thy
src/HOL/UNITY/Simple/Common.ML
src/HOL/UNITY/Simple/Common.thy
src/HOL/UNITY/Simple/Deadlock.ML
src/HOL/UNITY/Simple/Deadlock.thy
src/HOL/UNITY/Simple/Lift.ML
src/HOL/UNITY/Simple/Lift.thy
src/HOL/UNITY/Simple/Mutex.ML
src/HOL/UNITY/Simple/Mutex.thy
src/HOL/UNITY/Simple/Network.ML
src/HOL/UNITY/Simple/Network.thy
src/HOL/UNITY/Simple/Reach.ML
src/HOL/UNITY/Simple/Reach.thy
src/HOL/UNITY/Simple/Reachability.ML
src/HOL/UNITY/Simple/Reachability.thy
src/HOL/UNITY/Simple/Token.ML
src/HOL/UNITY/Simple/Token.thy
     1.1 --- a/src/HOL/IsaMakefile	Thu Jan 23 10:30:14 2003 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Fri Jan 24 14:06:49 2003 +0100
     1.3 @@ -381,8 +381,8 @@
     1.4  HOL-UNITY: HOL $(LOG)/HOL-UNITY.gz
     1.5  
     1.6  $(LOG)/HOL-UNITY.gz: $(OUT)/HOL Library/Multiset.thy UNITY/ROOT.ML \
     1.7 -  UNITY/Comp.ML UNITY/Comp.thy \
     1.8 -  UNITY/Detects.ML UNITY/Detects.thy \
     1.9 +  UNITY/UNITY_Main.thy UNITY/Comp.ML UNITY/Comp.thy \
    1.10 +  UNITY/Detects.thy \
    1.11    UNITY/ELT.ML UNITY/ELT.thy UNITY/Extend.ML \
    1.12    UNITY/Extend.thy UNITY/FP.ML UNITY/FP.thy UNITY/Follows.ML \
    1.13    UNITY/Follows.thy UNITY/GenPrefix.ML UNITY/GenPrefix.thy \
    1.14 @@ -395,16 +395,16 @@
    1.15    UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/UNITY.ML \
    1.16    UNITY/UNITY.thy UNITY/Union.ML UNITY/Union.thy UNITY/WFair.ML \
    1.17    UNITY/WFair.thy \
    1.18 -  UNITY/Simple/Channel.ML UNITY/Simple/Channel.thy  \
    1.19 -  UNITY/Simple/Common.ML UNITY/Simple/Common.thy  \
    1.20 -  UNITY/Simple/Deadlock.ML UNITY/Simple/Deadlock.thy  \
    1.21 -  UNITY/Simple/Lift.ML UNITY/Simple/Lift.thy  \
    1.22 -  UNITY/Simple/Mutex.ML UNITY/Simple/Mutex.thy  \
    1.23 +  UNITY/Simple/Channel.thy  \
    1.24 +  UNITY/Simple/Common.thy  \
    1.25 +  UNITY/Simple/Deadlock.thy  \
    1.26 +  UNITY/Simple/Lift.thy  \
    1.27 +  UNITY/Simple/Mutex.thy  \
    1.28    UNITY/Simple/NSP_Bad.ML UNITY/Simple/NSP_Bad.thy  \
    1.29 -  UNITY/Simple/Network.ML UNITY/Simple/Network.thy  \
    1.30 -  UNITY/Simple/Reach.ML UNITY/Simple/Reach.thy   \
    1.31 -  UNITY/Simple/Reachability.ML UNITY/Simple/Reachability.thy   \
    1.32 -  UNITY/Simple/Token.ML UNITY/Simple/Token.thy \
    1.33 +  UNITY/Simple/Network.thy  \
    1.34 +  UNITY/Simple/Reach.thy   \
    1.35 +  UNITY/Simple/Reachability.thy   \
    1.36 +  UNITY/Simple/Token.thy \
    1.37    UNITY/Comp/Alloc.ML UNITY/Comp/Alloc.thy \
    1.38    UNITY/Comp/AllocBase.ML UNITY/Comp/AllocBase.thy \
    1.39    UNITY/Comp/Client.ML UNITY/Comp/Client.thy \
     2.1 --- a/src/HOL/UNITY/Detects.ML	Thu Jan 23 10:30:14 2003 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,69 +0,0 @@
     2.4 -(*  Title:      HOL/UNITY/Detects
     2.5 -    ID:         $Id$
     2.6 -    Author:     Tanja Vos, Cambridge University Computer Laboratory
     2.7 -    Copyright   2000  University of Cambridge
     2.8 -
     2.9 -Detects definition (Section 3.8 of Chandy & Misra) using LeadsTo
    2.10 -*)
    2.11 -
    2.12 -(* Corollary from Sectiom 3.6.4 *)
    2.13 -
    2.14 -Goal "F: A LeadsTo B ==> F : Always (-((FP F) Int A Int -B))";
    2.15 -by (rtac LeadsTo_empty 1);
    2.16 -by (subgoal_tac "F : (FP F Int A Int - B) LeadsTo (B Int (FP F Int -B))" 1);
    2.17 -by (subgoal_tac "(FP F Int A Int - B) = (A Int (FP F Int -B))" 2);
    2.18 -by (subgoal_tac "(B Int (FP F Int -B)) = {}" 1);
    2.19 -by Auto_tac;
    2.20 -by (blast_tac (claset() addIs [PSP_Stable, stable_imp_Stable, 
    2.21 -			       stable_FP_Int]) 1);
    2.22 -qed "Always_at_FP";
    2.23 -
    2.24 -
    2.25 -Goalw [Detects_def, Int_def]
    2.26 -     "[| F : A Detects B; F : B Detects C |] ==> F : A Detects C";
    2.27 -by (Simp_tac 1);
    2.28 -by Safe_tac;
    2.29 -by (rtac LeadsTo_Trans 2);
    2.30 -by Auto_tac;
    2.31 -by (subgoal_tac "F : Always ((-A Un B) Int (-B Un C))" 1);
    2.32 -by (simp_tac (simpset() addsimps [Always_Int_distrib]) 2);
    2.33 -by Auto_tac;
    2.34 -by (blast_tac (claset() addIs [Always_weaken]) 1);
    2.35 -qed "Detects_Trans";
    2.36 -
    2.37 -
    2.38 -Goalw [Detects_def] "F : A Detects A";
    2.39 -by (simp_tac (simpset() addsimps [Un_commute, Compl_partition, 
    2.40 -				  subset_imp_LeadsTo]) 1);
    2.41 -qed "Detects_refl";
    2.42 -
    2.43 -Goalw [Equality_def] "(A<==>B) = (A Int B) Un (-A Int -B)";
    2.44 -by (Blast_tac 1);
    2.45 -qed "Detects_eq_Un";
    2.46 -
    2.47 -(*Not quite antisymmetry: sets A and B agree in all reachable states *)
    2.48 -Goalw [Detects_def, Equality_def]
    2.49 -     "[| F : A Detects B;  F : B Detects A|] ==> F : Always (A <==> B)";
    2.50 -by (asm_full_simp_tac (simpset() addsimps [Always_Int_I, Un_commute]) 1);
    2.51 -qed "Detects_antisym";
    2.52 -
    2.53 -
    2.54 -(* Theorem from Section 3.8 *)
    2.55 -
    2.56 -Goalw [Detects_def, Equality_def]
    2.57 -     "F : A Detects B ==> F : Always ((-(FP F)) Un (A <==> B))";
    2.58 -by (simp_tac (simpset() addsimps [Un_Int_distrib, Always_Int_distrib]) 1);
    2.59 -by (blast_tac (claset() addDs [Always_at_FP]
    2.60 -			addIs [Always_weaken]) 1);
    2.61 -qed "Detects_Always";
    2.62 -
    2.63 -(* Theorem from exercise 11.1 Section 11.3.1 *)
    2.64 -
    2.65 -Goalw [Detects_def, Equality_def]
    2.66 -     "F : A Detects B ==> F : UNIV LeadsTo (A <==> B)";
    2.67 -by (res_inst_tac [("B", "B")]  LeadsTo_Diff 1);
    2.68 -by (blast_tac (claset() addIs [Always_LeadsTo_weaken]) 2);
    2.69 -by (blast_tac (claset() addIs [Always_LeadsToI, subset_imp_LeadsTo]) 1);
    2.70 -qed "Detects_Imp_LeadstoEQ";
    2.71 -
    2.72 -
     3.1 --- a/src/HOL/UNITY/Detects.thy	Thu Jan 23 10:30:14 2003 +0100
     3.2 +++ b/src/HOL/UNITY/Detects.thy	Fri Jan 24 14:06:49 2003 +0100
     3.3 @@ -6,16 +6,78 @@
     3.4  Detects definition (Section 3.8 of Chandy & Misra) using LeadsTo
     3.5  *)
     3.6  
     3.7 -Detects = WFair + Reach + 
     3.8 -
     3.9 +theory Detects = FP + SubstAx:
    3.10  
    3.11  consts
    3.12     op_Detects  :: "['a set, 'a set] => 'a program set"  (infixl "Detects" 60)
    3.13     op_Equality :: "['a set, 'a set] => 'a set"          (infixl "<==>" 60)
    3.14     
    3.15  defs
    3.16 -  Detects_def "A Detects B == (Always (-A Un B)) Int (B LeadsTo A)"
    3.17 -  Equality_def "A <==> B == (-A Un B) Int (A Un -B)"
    3.18 +  Detects_def:  "A Detects B == (Always (-A Un B)) Int (B LeadsTo A)"
    3.19 +  Equality_def: "A <==> B == (-A Un B) Int (A Un -B)"
    3.20 +
    3.21 +
    3.22 +(* Corollary from Sectiom 3.6.4 *)
    3.23 +
    3.24 +lemma Always_at_FP: "F: A LeadsTo B ==> F : Always (-((FP F) Int A Int -B))"
    3.25 +apply (rule LeadsTo_empty)
    3.26 +apply (subgoal_tac "F : (FP F Int A Int - B) LeadsTo (B Int (FP F Int -B))")
    3.27 +apply (subgoal_tac [2] " (FP F Int A Int - B) = (A Int (FP F Int -B))")
    3.28 +apply (subgoal_tac "(B Int (FP F Int -B)) = {}")
    3.29 +apply auto
    3.30 +apply (blast intro: PSP_Stable stable_imp_Stable stable_FP_Int)
    3.31 +done
    3.32 +
    3.33 +
    3.34 +lemma Detects_Trans: 
    3.35 +     "[| F : A Detects B; F : B Detects C |] ==> F : A Detects C"
    3.36 +apply (unfold Detects_def Int_def)
    3.37 +apply (simp (no_asm))
    3.38 +apply safe
    3.39 +apply (rule_tac [2] LeadsTo_Trans)
    3.40 +apply auto
    3.41 +apply (subgoal_tac "F : Always ((-A Un B) Int (-B Un C))")
    3.42 + apply (blast intro: Always_weaken)
    3.43 +apply (simp add: Always_Int_distrib)
    3.44 +done
    3.45 +
    3.46 +lemma Detects_refl: "F : A Detects A"
    3.47 +apply (unfold Detects_def)
    3.48 +apply (simp (no_asm) add: Un_commute Compl_partition subset_imp_LeadsTo)
    3.49 +done
    3.50 +
    3.51 +lemma Detects_eq_Un: "(A<==>B) = (A Int B) Un (-A Int -B)"
    3.52 +apply (unfold Equality_def)
    3.53 +apply blast
    3.54 +done
    3.55 +
    3.56 +(*Not quite antisymmetry: sets A and B agree in all reachable states *)
    3.57 +lemma Detects_antisym: 
    3.58 +     "[| F : A Detects B;  F : B Detects A|] ==> F : Always (A <==> B)"
    3.59 +apply (unfold Detects_def Equality_def)
    3.60 +apply (simp add: Always_Int_I Un_commute)
    3.61 +done
    3.62 +
    3.63 +
    3.64 +(* Theorem from Section 3.8 *)
    3.65 +
    3.66 +lemma Detects_Always: 
    3.67 +     "F : A Detects B ==> F : Always ((-(FP F)) Un (A <==> B))"
    3.68 +apply (unfold Detects_def Equality_def)
    3.69 +apply (simp (no_asm) add: Un_Int_distrib Always_Int_distrib)
    3.70 +apply (blast dest: Always_at_FP intro: Always_weaken)
    3.71 +done
    3.72 +
    3.73 +(* Theorem from exercise 11.1 Section 11.3.1 *)
    3.74 +
    3.75 +lemma Detects_Imp_LeadstoEQ: 
    3.76 +     "F : A Detects B ==> F : UNIV LeadsTo (A <==> B)"
    3.77 +apply (unfold Detects_def Equality_def)
    3.78 +apply (rule_tac B = "B" in LeadsTo_Diff)
    3.79 +prefer 2 apply (blast intro: Always_LeadsTo_weaken)
    3.80 +apply (blast intro: Always_LeadsToI subset_imp_LeadsTo)
    3.81 +done
    3.82 +
    3.83  
    3.84  end
    3.85  
     4.1 --- a/src/HOL/UNITY/ROOT.ML	Thu Jan 23 10:30:14 2003 +0100
     4.2 +++ b/src/HOL/UNITY/ROOT.ML	Fri Jan 24 14:06:49 2003 +0100
     4.3 @@ -7,8 +7,7 @@
     4.4  *)
     4.5  
     4.6  (*Basic meta-theory*)
     4.7 -time_use_thy "FP";
     4.8 -time_use_thy "WFair";
     4.9 +time_use_thy "UNITY_Main";
    4.10  
    4.11  (*Simple examples: no composition*)
    4.12  time_use_thy "Simple/Deadlock";
     5.1 --- a/src/HOL/UNITY/Simple/Channel.ML	Thu Jan 23 10:30:14 2003 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,57 +0,0 @@
     5.4 -(*  Title:      HOL/UNITY/Channel
     5.5 -    ID:         $Id$
     5.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.7 -    Copyright   1998  University of Cambridge
     5.8 -
     5.9 -Unordered Channel
    5.10 -
    5.11 -From Misra, "A Logic for Concurrent Programming" (1994), section 13.3
    5.12 -*)
    5.13 -
    5.14 -(*None represents "infinity" while Some represents proper integers*)
    5.15 -Goalw [minSet_def] "minSet A = Some x --> x : A";
    5.16 -by (Simp_tac 1);
    5.17 -by (fast_tac (claset() addIs [LeastI]) 1);
    5.18 -qed_spec_mp "minSet_eq_SomeD";
    5.19 -
    5.20 -Goalw [minSet_def] " minSet{} = None";
    5.21 -by (Asm_simp_tac 1);
    5.22 -qed_spec_mp "minSet_empty";
    5.23 -Addsimps [minSet_empty];
    5.24 -
    5.25 -Goalw [minSet_def] "x:A ==> minSet A = Some (LEAST x. x: A)";
    5.26 -by Auto_tac;
    5.27 -qed_spec_mp "minSet_nonempty";
    5.28 -
    5.29 -Goal "F : (minSet -` {Some x}) leadsTo (minSet -` (Some`greaterThan x))";
    5.30 -by (rtac leadsTo_weaken 1);
    5.31 -by (res_inst_tac [("x1","x")] ([UC2, UC1] MRS psp) 1);
    5.32 -by Safe_tac;
    5.33 -by (auto_tac (claset() addDs [minSet_eq_SomeD], 
    5.34 -	      simpset() addsimps [linorder_neq_iff]));
    5.35 -qed "minSet_greaterThan";
    5.36 -
    5.37 -(*The induction*)
    5.38 -Goal "F : (UNIV-{{}}) leadsTo (minSet -` (Some`atLeast y))";
    5.39 -by (rtac leadsTo_weaken_R 1);
    5.40 -by (res_inst_tac  [("l", "y"), ("f", "the o minSet"), ("B", "{}")]
    5.41 -     greaterThan_bounded_induct 1);
    5.42 -by Safe_tac;
    5.43 -by (ALLGOALS Asm_simp_tac);
    5.44 -by (dtac minSet_nonempty 2);
    5.45 -by (Asm_full_simp_tac 2);
    5.46 -by (rtac (minSet_greaterThan RS leadsTo_weaken) 1);
    5.47 -by Safe_tac;
    5.48 -by (ALLGOALS Asm_full_simp_tac);
    5.49 -by (dtac minSet_nonempty 1);
    5.50 -by (Asm_full_simp_tac 1);
    5.51 -val lemma = result();
    5.52 -
    5.53 -
    5.54 -Goal "!!y::nat. F : (UNIV-{{}}) leadsTo {s. y ~: s}";
    5.55 -by (rtac (lemma RS leadsTo_weaken_R) 1);
    5.56 -by (Clarify_tac 1);
    5.57 -by (ftac minSet_nonempty 1);
    5.58 -by (auto_tac (claset() addDs [Suc_le_lessD, not_less_Least], 
    5.59 -	      simpset()));
    5.60 -qed "Channel_progress";
     6.1 --- a/src/HOL/UNITY/Simple/Channel.thy	Thu Jan 23 10:30:14 2003 +0100
     6.2 +++ b/src/HOL/UNITY/Simple/Channel.thy	Fri Jan 24 14:06:49 2003 +0100
     6.3 @@ -8,23 +8,65 @@
     6.4  From Misra, "A Logic for Concurrent Programming" (1994), section 13.3
     6.5  *)
     6.6  
     6.7 -Channel = WFair +
     6.8 +theory Channel = UNITY_Main:
     6.9  
    6.10 -types state = nat set
    6.11 +types state = "nat set"
    6.12  
    6.13  consts
    6.14 -  F :: state program
    6.15 +  F :: "state program"
    6.16  
    6.17  constdefs
    6.18 -  minSet :: nat set => nat option
    6.19 +  minSet :: "nat set => nat option"
    6.20      "minSet A == if A={} then None else Some (LEAST x. x:A)"
    6.21  
    6.22 -rules
    6.23 +axioms
    6.24  
    6.25 -  UC1  "F : (minSet -` {Some x}) co (minSet -` (Some`atLeast x))"
    6.26 +  UC1:  "F : (minSet -` {Some x}) co (minSet -` (Some`atLeast x))"
    6.27  
    6.28    (*  UC1  "F : {s. minSet s = x} co {s. x <= minSet s}"  *)
    6.29  
    6.30 -  UC2  "F : (minSet -` {Some x}) leadsTo {s. x ~: s}"
    6.31 +  UC2:  "F : (minSet -` {Some x}) leadsTo {s. x ~: s}"
    6.32 +
    6.33 +
    6.34 +(*None represents "infinity" while Some represents proper integers*)
    6.35 +lemma minSet_eq_SomeD: "minSet A = Some x ==> x : A"
    6.36 +apply (unfold minSet_def)
    6.37 +apply (simp split: split_if_asm)
    6.38 +apply (fast intro: LeastI)
    6.39 +done
    6.40 +
    6.41 +lemma minSet_empty [simp]: " minSet{} = None"
    6.42 +by (unfold minSet_def, simp)
    6.43 +
    6.44 +lemma minSet_nonempty: "x:A ==> minSet A = Some (LEAST x. x: A)"
    6.45 +by (unfold minSet_def, auto)
    6.46 +
    6.47 +lemma minSet_greaterThan:
    6.48 +     "F : (minSet -` {Some x}) leadsTo (minSet -` (Some`greaterThan x))"
    6.49 +apply (rule leadsTo_weaken)
    6.50 +apply (rule_tac x1=x in psp [OF UC2 UC1], safe)
    6.51 +apply (auto dest: minSet_eq_SomeD simp add: linorder_neq_iff)
    6.52 +done
    6.53 +
    6.54 +(*The induction*)
    6.55 +lemma Channel_progress_lemma:
    6.56 +     "F : (UNIV-{{}}) leadsTo (minSet -` (Some`atLeast y))"
    6.57 +apply (rule leadsTo_weaken_R)
    6.58 +apply (rule_tac l = y and f = "the o minSet" and B = "{}" 
    6.59 +       in greaterThan_bounded_induct, safe)
    6.60 +apply (simp_all (no_asm_simp))
    6.61 +apply (drule_tac [2] minSet_nonempty)
    6.62 + prefer 2 apply simp 
    6.63 +apply (rule minSet_greaterThan [THEN leadsTo_weaken], safe)
    6.64 +apply simp_all
    6.65 +apply (drule minSet_nonempty, simp)
    6.66 +done
    6.67 +
    6.68 +
    6.69 +lemma Channel_progress: "!!y::nat. F : (UNIV-{{}}) leadsTo {s. y ~: s}"
    6.70 +apply (rule Channel_progress_lemma [THEN leadsTo_weaken_R], clarify)
    6.71 +apply (frule minSet_nonempty)
    6.72 +apply (auto dest: Suc_le_lessD not_less_Least)
    6.73 +done
    6.74  
    6.75  end
     7.1 --- a/src/HOL/UNITY/Simple/Common.ML	Thu Jan 23 10:30:14 2003 +0100
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,90 +0,0 @@
     7.4 -(*  Title:      HOL/UNITY/Common
     7.5 -    ID:         $Id$
     7.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.7 -    Copyright   1998  University of Cambridge
     7.8 -
     7.9 -Common Meeting Time example from Misra (1994)
    7.10 -
    7.11 -The state is identified with the one variable in existence.
    7.12 -
    7.13 -From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
    7.14 -*)
    7.15 -
    7.16 -(*Misra's property CMT4: t exceeds no common meeting time*)
    7.17 -Goal "[| ALL m. F : {m} Co (maxfg m); n: common |] \
    7.18 -\     ==> F : Stable (atMost n)";
    7.19 -by (dres_inst_tac [("M", "{t. t<=n}")] Elimination_sing 1);
    7.20 -by (asm_full_simp_tac
    7.21 -    (simpset() addsimps [atMost_def, Stable_def, common_def, maxfg_def,
    7.22 -			 le_max_iff_disj]) 1);
    7.23 -by (etac Constrains_weaken_R 1);
    7.24 -by (blast_tac (claset() addIs [order_eq_refl, fmono, gmono, le_trans]) 1);
    7.25 -qed "common_stable";
    7.26 -
    7.27 -Goal "[| Init F <= atMost n;  \
    7.28 -\        ALL m. F : {m} Co (maxfg m); n: common |] \
    7.29 -\     ==> F : Always (atMost n)";
    7.30 -by (asm_simp_tac (simpset() addsimps [AlwaysI, common_stable]) 1);
    7.31 -qed "common_safety";
    7.32 -
    7.33 -
    7.34 -(*** Some programs that implement the safety property above ***)
    7.35 -
    7.36 -Goal "SKIP : {m} co (maxfg m)";
    7.37 -by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, le_max_iff_disj,
    7.38 -				  fasc]) 1);
    7.39 -result();
    7.40 -
    7.41 -(*This one is  t := ftime t || t := gtime t*)
    7.42 -Goal "mk_program (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}, UNIV) \
    7.43 -\      : {m} co (maxfg m)";
    7.44 -by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, 
    7.45 -				  le_max_iff_disj, fasc]) 1);
    7.46 -result();
    7.47 -
    7.48 -(*This one is  t := max (ftime t) (gtime t)*)
    7.49 -Goal "mk_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV) \
    7.50 -\      : {m} co (maxfg m)";
    7.51 -by (simp_tac 
    7.52 -    (simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1);
    7.53 -result();
    7.54 -
    7.55 -(*This one is  t := t+1 if t <max (ftime t) (gtime t) *)
    7.56 -Goal "mk_program  \
    7.57 -\         (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }, UNIV)  \
    7.58 -\      : {m} co (maxfg m)";
    7.59 -by (simp_tac 
    7.60 -    (simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1);
    7.61 -result();
    7.62 -
    7.63 -
    7.64 -(*It remans to prove that they satisfy CMT3': t does not decrease,
    7.65 -  and that CMT3' implies that t stops changing once common(t) holds.*)
    7.66 -
    7.67 -
    7.68 -(*** Progress under weak fairness ***)
    7.69 -
    7.70 -Addsimps [atMost_Int_atLeast];
    7.71 -
    7.72 -Goal "[| ALL m. F : {m} Co (maxfg m); \
    7.73 -\               ALL m: lessThan n. F : {m} LeadsTo (greaterThan m); \
    7.74 -\               n: common |]  \
    7.75 -\     ==> F : (atMost n) LeadsTo common";
    7.76 -by (rtac LeadsTo_weaken_R 1);
    7.77 -by (res_inst_tac [("f","id"), ("l","n")] GreaterThan_bounded_induct 1);
    7.78 -by (ALLGOALS Asm_simp_tac);
    7.79 -by (rtac subset_refl 2);
    7.80 -by (blast_tac (claset() addDs [PSP_Stable2] 
    7.81 -                        addIs [common_stable, LeadsTo_weaken_R]) 1);
    7.82 -val lemma = result();
    7.83 -
    7.84 -(*The "ALL m: -common" form echoes CMT6.*)
    7.85 -Goal "[| ALL m. F : {m} Co (maxfg m); \
    7.86 -\               ALL m: -common. F : {m} LeadsTo (greaterThan m); \
    7.87 -\               n: common |]  \
    7.88 -\            ==> F : (atMost (LEAST n. n: common)) LeadsTo common";
    7.89 -by (rtac lemma 1);
    7.90 -by (ALLGOALS Asm_simp_tac);
    7.91 -by (etac LeastI 2);
    7.92 -by (blast_tac (claset() addSDs [not_less_Least]) 1);
    7.93 -qed "leadsTo_common";
     8.1 --- a/src/HOL/UNITY/Simple/Common.thy	Thu Jan 23 10:30:14 2003 +0100
     8.2 +++ b/src/HOL/UNITY/Simple/Common.thy	Fri Jan 24 14:06:49 2003 +0100
     8.3 @@ -10,23 +10,96 @@
     8.4  From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
     8.5  *)
     8.6  
     8.7 -Common = SubstAx + 
     8.8 +theory Common = UNITY_Main:
     8.9  
    8.10  consts
    8.11 -  ftime,gtime :: nat=>nat
    8.12 +  ftime :: "nat=>nat"
    8.13 +  gtime :: "nat=>nat"
    8.14  
    8.15 -rules
    8.16 -  fmono "m <= n ==> ftime m <= ftime n"
    8.17 -  gmono "m <= n ==> gtime m <= gtime n"
    8.18 +axioms
    8.19 +  fmono: "m <= n ==> ftime m <= ftime n"
    8.20 +  gmono: "m <= n ==> gtime m <= gtime n"
    8.21  
    8.22 -  fasc  "m <= ftime n"
    8.23 -  gasc  "m <= gtime n"
    8.24 +  fasc:  "m <= ftime n"
    8.25 +  gasc:  "m <= gtime n"
    8.26  
    8.27  constdefs
    8.28 -  common :: nat set
    8.29 +  common :: "nat set"
    8.30      "common == {n. ftime n = n & gtime n = n}"
    8.31  
    8.32 -  maxfg :: nat => nat set
    8.33 +  maxfg :: "nat => nat set"
    8.34      "maxfg m == {t. t <= max (ftime m) (gtime m)}"
    8.35  
    8.36 +
    8.37 +(*Misra's property CMT4: t exceeds no common meeting time*)
    8.38 +lemma common_stable:
    8.39 +     "[| ALL m. F : {m} Co (maxfg m); n: common |]  
    8.40 +      ==> F : Stable (atMost n)"
    8.41 +apply (drule_tac M = "{t. t<=n}" in Elimination_sing)
    8.42 +apply (simp add: atMost_def Stable_def common_def maxfg_def le_max_iff_disj)
    8.43 +apply (erule Constrains_weaken_R)
    8.44 +apply (blast intro: order_eq_refl fmono gmono le_trans)
    8.45 +done
    8.46 +
    8.47 +lemma common_safety:
    8.48 +     "[| Init F <= atMost n;   
    8.49 +         ALL m. F : {m} Co (maxfg m); n: common |]  
    8.50 +      ==> F : Always (atMost n)"
    8.51 +by (simp add: AlwaysI common_stable)
    8.52 +
    8.53 +
    8.54 +(*** Some programs that implement the safety property above ***)
    8.55 +
    8.56 +lemma "SKIP : {m} co (maxfg m)"
    8.57 +by (simp add: constrains_def maxfg_def le_max_iff_disj fasc)
    8.58 +
    8.59 +(*This one is  t := ftime t || t := gtime t*)
    8.60 +lemma "mk_program (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}, UNIV)
    8.61 +       : {m} co (maxfg m)"
    8.62 +by (simp add: constrains_def maxfg_def le_max_iff_disj fasc)
    8.63 +
    8.64 +(*This one is  t := max (ftime t) (gtime t)*)
    8.65 +lemma  "mk_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV)  
    8.66 +       : {m} co (maxfg m)"
    8.67 +by (simp add: constrains_def maxfg_def max_def gasc)
    8.68 +
    8.69 +(*This one is  t := t+1 if t <max (ftime t) (gtime t) *)
    8.70 +lemma  "mk_program   
    8.71 +          (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }, UNIV)   
    8.72 +       : {m} co (maxfg m)"
    8.73 +by (simp add: constrains_def maxfg_def max_def gasc)
    8.74 +
    8.75 +
    8.76 +(*It remans to prove that they satisfy CMT3': t does not decrease,
    8.77 +  and that CMT3' implies that t stops changing once common(t) holds.*)
    8.78 +
    8.79 +
    8.80 +(*** Progress under weak fairness ***)
    8.81 +
    8.82 +declare atMost_Int_atLeast [simp]
    8.83 +
    8.84 +lemma leadsTo_common_lemma:
    8.85 +     "[| ALL m. F : {m} Co (maxfg m);  
    8.86 +         ALL m: lessThan n. F : {m} LeadsTo (greaterThan m);  
    8.87 +         n: common |]   
    8.88 +      ==> F : (atMost n) LeadsTo common"
    8.89 +apply (rule LeadsTo_weaken_R)
    8.90 +apply (rule_tac f = id and l = n in GreaterThan_bounded_induct)
    8.91 +apply (simp_all (no_asm_simp))
    8.92 +apply (rule_tac [2] subset_refl)
    8.93 +apply (blast dest: PSP_Stable2 intro: common_stable LeadsTo_weaken_R)
    8.94 +done
    8.95 +
    8.96 +(*The "ALL m: -common" form echoes CMT6.*)
    8.97 +lemma leadsTo_common:
    8.98 +     "[| ALL m. F : {m} Co (maxfg m);  
    8.99 +         ALL m: -common. F : {m} LeadsTo (greaterThan m);  
   8.100 +         n: common |]   
   8.101 +      ==> F : (atMost (LEAST n. n: common)) LeadsTo common"
   8.102 +apply (rule leadsTo_common_lemma)
   8.103 +apply (simp_all (no_asm_simp))
   8.104 +apply (erule_tac [2] LeastI)
   8.105 +apply (blast dest!: not_less_Least)
   8.106 +done
   8.107 +
   8.108  end
     9.1 --- a/src/HOL/UNITY/Simple/Deadlock.ML	Thu Jan 23 10:30:14 2003 +0100
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,78 +0,0 @@
     9.4 -(*  Title:      HOL/UNITY/Deadlock
     9.5 -    ID:         $Id$
     9.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.7 -    Copyright   1998  University of Cambridge
     9.8 -
     9.9 -Deadlock examples from section 5.6 of 
    9.10 -    Misra, "A Logic for Concurrent Programming", 1994
    9.11 -*)
    9.12 -
    9.13 -(*Trivial, two-process case*)
    9.14 -Goalw [constrains_def, stable_def]
    9.15 -    "[| F : (A Int B) co A;  F : (B Int A) co B |] ==> F : stable (A Int B)";
    9.16 -by (Blast_tac 1);
    9.17 -result();
    9.18 -
    9.19 -
    9.20 -(*a simplification step*)
    9.21 -Goal "(INT i: atMost n. A(Suc i) Int A i) = (INT i: atMost (Suc n). A i)";
    9.22 -by (induct_tac "n" 1);
    9.23 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [atMost_Suc])));
    9.24 -by Auto_tac;
    9.25 -qed "Collect_le_Int_equals";
    9.26 -
    9.27 -(*Dual of the required property.  Converse inclusion fails.*)
    9.28 -Goal "(UN i: lessThan n. A i) Int (- A n) <=  \
    9.29 -\     (UN i: lessThan n. (A i) Int (- A (Suc i)))";
    9.30 -by (induct_tac "n" 1);
    9.31 -by (Asm_simp_tac 1);
    9.32 -by (simp_tac (simpset() addsimps [lessThan_Suc]) 1);
    9.33 -by (Blast_tac 1);
    9.34 -qed "UN_Int_Compl_subset";
    9.35 -
    9.36 -
    9.37 -(*Converse inclusion fails.*)
    9.38 -Goal "(INT i: lessThan n. -A i Un A (Suc i))  <= \
    9.39 -\     (INT i: lessThan n. -A i) Un A n";
    9.40 -by (induct_tac "n" 1);
    9.41 -by (Asm_simp_tac 1);
    9.42 -by (asm_simp_tac (simpset() addsimps [lessThan_Suc]) 1);
    9.43 -by (Blast_tac 1);
    9.44 -qed "INT_Un_Compl_subset";
    9.45 -
    9.46 -
    9.47 -(*Specialized rewriting*)
    9.48 -Goal "A 0 Int (-(A n) Int (INT i: lessThan n. -A i Un A (Suc i))) = {}";
    9.49 -by (blast_tac (claset() addIs [gr0I]
    9.50 -		        addDs [impOfSubs INT_Un_Compl_subset]) 1);
    9.51 -val lemma = result();
    9.52 -
    9.53 -(*Reverse direction makes it harder to invoke the ind hyp*)
    9.54 -Goal "(INT i: atMost n. A i) = \
    9.55 -\         A 0 Int (INT i: lessThan n. -A i Un A(Suc i))";
    9.56 -by (induct_tac "n" 1);
    9.57 -by (Asm_simp_tac 1);
    9.58 -by (asm_simp_tac
    9.59 -    (simpset() addsimps Int_ac @ [Int_Un_distrib, Int_Un_distrib2, lemma,
    9.60 -				  lessThan_Suc, atMost_Suc]) 1);
    9.61 -qed "INT_le_equals_Int";
    9.62 -
    9.63 -Goal "(INT i: atMost (Suc n). A i) = \
    9.64 -\     A 0 Int (INT i: atMost n. -A i Un A(Suc i))";
    9.65 -by (simp_tac (simpset() addsimps [lessThan_Suc_atMost, INT_le_equals_Int]) 1);
    9.66 -qed "INT_le_Suc_equals_Int";
    9.67 -
    9.68 -
    9.69 -(*The final deadlock example*)
    9.70 -val [zeroprem, allprem] = Goalw [stable_def]
    9.71 -    "[| F : (A 0 Int A (Suc n)) co (A 0);  \
    9.72 -\       !!i. i: atMost n ==> F : (A(Suc i) Int A i) co (-A i Un A(Suc i)) |] \
    9.73 -\    ==> F : stable (INT i: atMost (Suc n). A i)";
    9.74 -by (rtac ([zeroprem, constrains_INT] MRS 
    9.75 -	  constrains_Int RS constrains_weaken) 1);
    9.76 -by (etac allprem 1);
    9.77 -by (simp_tac (simpset() addsimps [Collect_le_Int_equals, 
    9.78 -				  Int_assoc, INT_absorb]) 1);
    9.79 -by (simp_tac (simpset() addsimps [INT_le_Suc_equals_Int]) 1);
    9.80 -result();
    9.81 -
    10.1 --- a/src/HOL/UNITY/Simple/Deadlock.thy	Thu Jan 23 10:30:14 2003 +0100
    10.2 +++ b/src/HOL/UNITY/Simple/Deadlock.thy	Fri Jan 24 14:06:49 2003 +0100
    10.3 @@ -1,1 +1,82 @@
    10.4 -Deadlock = UNITY
    10.5 +(*  Title:      HOL/UNITY/Deadlock
    10.6 +    ID:         $Id$
    10.7 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    10.8 +    Copyright   1998  University of Cambridge
    10.9 +
   10.10 +Deadlock examples from section 5.6 of 
   10.11 +    Misra, "A Logic for Concurrent Programming", 1994
   10.12 +*)
   10.13 +
   10.14 +theory Deadlock = UNITY:
   10.15 +
   10.16 +(*Trivial, two-process case*)
   10.17 +lemma "[| F : (A Int B) co A;  F : (B Int A) co B |] ==> F : stable (A Int B)"
   10.18 +by (unfold constrains_def stable_def, blast)
   10.19 +
   10.20 +
   10.21 +(*a simplification step*)
   10.22 +lemma Collect_le_Int_equals:
   10.23 +     "(INT i: atMost n. A(Suc i) Int A i) = (INT i: atMost (Suc n). A i)"
   10.24 +apply (induct_tac "n")
   10.25 +apply (simp_all (no_asm_simp) add: atMost_Suc)
   10.26 +apply auto
   10.27 +done
   10.28 +
   10.29 +(*Dual of the required property.  Converse inclusion fails.*)
   10.30 +lemma UN_Int_Compl_subset:
   10.31 +     "(UN i: lessThan n. A i) Int (- A n) <=   
   10.32 +      (UN i: lessThan n. (A i) Int (- A (Suc i)))"
   10.33 +apply (induct_tac "n")
   10.34 +apply (simp (no_asm_simp))
   10.35 +apply (simp (no_asm) add: lessThan_Suc)
   10.36 +apply blast
   10.37 +done
   10.38 +
   10.39 +
   10.40 +(*Converse inclusion fails.*)
   10.41 +lemma INT_Un_Compl_subset:
   10.42 +     "(INT i: lessThan n. -A i Un A (Suc i))  <=  
   10.43 +      (INT i: lessThan n. -A i) Un A n"
   10.44 +apply (induct_tac "n")
   10.45 +apply (simp (no_asm_simp))
   10.46 +apply (simp (no_asm_simp) add: lessThan_Suc)
   10.47 +apply blast
   10.48 +done
   10.49 +
   10.50 +
   10.51 +(*Specialized rewriting*)
   10.52 +lemma INT_le_equals_Int_lemma:
   10.53 +     "A 0 Int (-(A n) Int (INT i: lessThan n. -A i Un A (Suc i))) = {}"
   10.54 +by (blast intro: gr0I dest: INT_Un_Compl_subset [THEN subsetD])
   10.55 +
   10.56 +(*Reverse direction makes it harder to invoke the ind hyp*)
   10.57 +lemma INT_le_equals_Int:
   10.58 +     "(INT i: atMost n. A i) =  
   10.59 +      A 0 Int (INT i: lessThan n. -A i Un A(Suc i))"
   10.60 +apply (induct_tac "n", simp)
   10.61 +apply (simp add: Int_ac Int_Un_distrib Int_Un_distrib2
   10.62 +                 INT_le_equals_Int_lemma lessThan_Suc atMost_Suc)
   10.63 +done
   10.64 +
   10.65 +lemma INT_le_Suc_equals_Int:
   10.66 +     "(INT i: atMost (Suc n). A i) =  
   10.67 +      A 0 Int (INT i: atMost n. -A i Un A(Suc i))"
   10.68 +by (simp add: lessThan_Suc_atMost INT_le_equals_Int)
   10.69 +
   10.70 +
   10.71 +(*The final deadlock example*)
   10.72 +lemma
   10.73 +  assumes zeroprem: "F : (A 0 Int A (Suc n)) co (A 0)"
   10.74 +      and allprem:
   10.75 +	    "!!i. i: atMost n ==> F : (A(Suc i) Int A i) co (-A i Un A(Suc i))"
   10.76 +  shows "F : stable (INT i: atMost (Suc n). A i)"
   10.77 +apply (unfold stable_def) 
   10.78 +apply (rule constrains_Int [THEN constrains_weaken])
   10.79 +   apply (rule zeroprem) 
   10.80 +  apply (rule constrains_INT) 
   10.81 +  apply (erule allprem)
   10.82 + apply (simp add: Collect_le_Int_equals Int_assoc INT_absorb)
   10.83 +apply (simp add: INT_le_Suc_equals_Int)
   10.84 +done
   10.85 +
   10.86 +end
    11.1 --- a/src/HOL/UNITY/Simple/Lift.ML	Thu Jan 23 10:30:14 2003 +0100
    11.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.3 @@ -1,317 +0,0 @@
    11.4 -(*  Title:      HOL/UNITY/Lift
    11.5 -    ID:         $Id$
    11.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    11.7 -    Copyright   1998  University of Cambridge
    11.8 -
    11.9 -The Lift-Control Example
   11.10 -*)
   11.11 -
   11.12 -Goal "[| x ~: A;  y : A |] ==> x ~= y";
   11.13 -by (Blast_tac 1);
   11.14 -qed "not_mem_distinct";
   11.15 -
   11.16 -
   11.17 -Addsimps [Lift_def RS def_prg_Init];
   11.18 -program_defs_ref := [Lift_def];
   11.19 -
   11.20 -Addsimps (map simp_of_act
   11.21 -	  [request_act_def, open_act_def, close_act_def,
   11.22 -	   req_up_def, req_down_def, move_up_def, move_down_def,
   11.23 -	   button_press_def]);
   11.24 -
   11.25 -(*The ALWAYS properties*)
   11.26 -Addsimps (map simp_of_set [above_def, below_def, queueing_def, 
   11.27 -			   goingup_def, goingdown_def, ready_def]);
   11.28 -
   11.29 -Addsimps [bounded_def, open_stop_def, open_move_def, stop_floor_def,
   11.30 -	  moving_up_def, moving_down_def];
   11.31 -
   11.32 -AddIffs [Min_le_Max];
   11.33 -
   11.34 -Goal "Lift : Always open_stop";
   11.35 -by (always_tac 1);
   11.36 -qed "open_stop";
   11.37 -
   11.38 -Goal "Lift : Always stop_floor";
   11.39 -by (always_tac 1);
   11.40 -qed "stop_floor";
   11.41 -
   11.42 -(*This one needs open_stop, which was proved above*)
   11.43 -Goal "Lift : Always open_move";
   11.44 -by (cut_facts_tac [open_stop] 1);
   11.45 -by (always_tac 1);
   11.46 -qed "open_move";
   11.47 -
   11.48 -Goal "Lift : Always moving_up";
   11.49 -by (always_tac 1);
   11.50 -by (auto_tac (claset() addDs [zle_imp_zless_or_eq],
   11.51 -	      simpset() addsimps [add1_zle_eq]));
   11.52 -qed "moving_up";
   11.53 -
   11.54 -Goal "Lift : Always moving_down";
   11.55 -by (always_tac 1);
   11.56 -by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1);
   11.57 -qed "moving_down";
   11.58 -
   11.59 -Goal "Lift : Always bounded";
   11.60 -by (cut_facts_tac [moving_up, moving_down] 1);
   11.61 -by (always_tac 1);
   11.62 -by Auto_tac;
   11.63 -by (ALLGOALS (dtac not_mem_distinct THEN' assume_tac));
   11.64 -by (ALLGOALS arith_tac);
   11.65 -qed "bounded";
   11.66 -
   11.67 -
   11.68 -
   11.69 -(*** Progress ***)
   11.70 -
   11.71 -
   11.72 -val abbrev_defs = [moving_def, stopped_def, 
   11.73 -		   opened_def, closed_def, atFloor_def, Req_def];
   11.74 -
   11.75 -Addsimps (map simp_of_set abbrev_defs);
   11.76 -
   11.77 -
   11.78 -(** The HUG'93 paper mistakenly omits the Req n from these! **)
   11.79 -
   11.80 -(** Lift_1 **)
   11.81 -
   11.82 -Goal "Lift : (stopped Int atFloor n) LeadsTo (opened Int atFloor n)";
   11.83 -by (cut_facts_tac [stop_floor] 1);
   11.84 -by (ensures_tac "open_act" 1);
   11.85 -qed "E_thm01";  (*lem_lift_1_5*)
   11.86 -
   11.87 -Goal "Lift : (Req n Int stopped - atFloor n) LeadsTo \
   11.88 -\                    (Req n Int opened - atFloor n)";
   11.89 -by (cut_facts_tac [stop_floor] 1);
   11.90 -by (ensures_tac "open_act" 1);
   11.91 -qed "E_thm02";  (*lem_lift_1_1*)
   11.92 -
   11.93 -Goal "Lift : (Req n Int opened - atFloor n) LeadsTo \
   11.94 -\                    (Req n Int closed - (atFloor n - queueing))";
   11.95 -by (ensures_tac "close_act" 1);
   11.96 -qed "E_thm03";  (*lem_lift_1_2*)
   11.97 -
   11.98 -Goal "Lift : (Req n Int closed Int (atFloor n - queueing))  \
   11.99 -\            LeadsTo (opened Int atFloor n)";
  11.100 -by (ensures_tac "open_act" 1);
  11.101 -qed "E_thm04";  (*lem_lift_1_7*)
  11.102 -
  11.103 -
  11.104 -(** Lift 2.  Statements of thm05a and thm05b were wrong! **)
  11.105 -
  11.106 -Open_locale "floor"; 
  11.107 -
  11.108 -val Min_le_n = thm "Min_le_n";
  11.109 -val n_le_Max = thm "n_le_Max";
  11.110 -
  11.111 -AddIffs [Min_le_n, n_le_Max];
  11.112 -
  11.113 -val le_MinD = Min_le_n RS order_antisym;
  11.114 -val Max_leD = n_le_Max RSN (2,order_antisym);
  11.115 -
  11.116 -val linorder_leI = linorder_not_less RS iffD1;
  11.117 -
  11.118 -AddSDs [le_MinD, linorder_leI RS le_MinD,
  11.119 -	Max_leD, linorder_leI RS Max_leD];
  11.120 -
  11.121 -(*lem_lift_2_0 
  11.122 -  NOT an ensures property, but a mere inclusion;
  11.123 -  don't know why script lift_2.uni says ENSURES*)
  11.124 -Goal "Lift : (Req n Int closed - (atFloor n - queueing))   \
  11.125 -\            LeadsTo ((closed Int goingup Int Req n)  Un \
  11.126 -\                     (closed Int goingdown Int Req n))";
  11.127 -by (auto_tac (claset() addSIs [subset_imp_LeadsTo] addSEs [int_neqE], 
  11.128 -		       simpset()));
  11.129 -qed "E_thm05c";
  11.130 -
  11.131 -(*lift_2*)
  11.132 -Goal "Lift : (Req n Int closed - (atFloor n - queueing))   \
  11.133 -\            LeadsTo (moving Int Req n)";
  11.134 -by (rtac ([E_thm05c, LeadsTo_Un] MRS LeadsTo_Trans) 1);
  11.135 -by (ensures_tac "req_down" 2);
  11.136 -by (ensures_tac "req_up" 1);
  11.137 -by Auto_tac;
  11.138 -qed "lift_2";
  11.139 -
  11.140 -
  11.141 -(** Towards lift_4 ***)
  11.142 - 
  11.143 -val metric_ss = simpset() addsplits [split_if_asm] 
  11.144 -                          addsimps  [metric_def, vimage_def];
  11.145 -
  11.146 -
  11.147 -(*lem_lift_4_1 *)
  11.148 -Goal "0 < N ==> \
  11.149 -\     Lift : (moving Int Req n Int {s. metric n s = N} Int \
  11.150 -\             {s. floor s ~: req s} Int {s. up s})   \
  11.151 -\            LeadsTo \
  11.152 -\              (moving Int Req n Int {s. metric n s < N})";
  11.153 -by (cut_facts_tac [moving_up] 1);
  11.154 -by (ensures_tac "move_up" 1);
  11.155 -by Safe_tac;
  11.156 -(*this step consolidates two formulae to the goal  metric n s' <= metric n s*)
  11.157 -by (etac (linorder_leI RS order_antisym RS sym) 1);
  11.158 -by (auto_tac (claset(), metric_ss));
  11.159 -qed "E_thm12a";
  11.160 -
  11.161 -
  11.162 -(*lem_lift_4_3 *)
  11.163 -Goal "0 < N ==> \
  11.164 -\     Lift : (moving Int Req n Int {s. metric n s = N} Int \
  11.165 -\             {s. floor s ~: req s} - {s. up s})   \
  11.166 -\            LeadsTo (moving Int Req n Int {s. metric n s < N})";
  11.167 -by (cut_facts_tac [moving_down] 1);
  11.168 -by (ensures_tac "move_down" 1);
  11.169 -by Safe_tac;
  11.170 -(*this step consolidates two formulae to the goal  metric n s' <= metric n s*)
  11.171 -by (etac (linorder_leI RS order_antisym RS sym) 1);
  11.172 -by (auto_tac (claset(), metric_ss));
  11.173 -qed "E_thm12b";
  11.174 -
  11.175 -(*lift_4*)
  11.176 -Goal "0<N ==> Lift : (moving Int Req n Int {s. metric n s = N} Int \
  11.177 -\                           {s. floor s ~: req s}) LeadsTo     \
  11.178 -\                          (moving Int Req n Int {s. metric n s < N})";
  11.179 -by (rtac ([subset_imp_LeadsTo, [E_thm12a, E_thm12b] MRS LeadsTo_Un] 
  11.180 -	  MRS LeadsTo_Trans) 1);
  11.181 -by Auto_tac;
  11.182 -qed "lift_4";
  11.183 -
  11.184 -
  11.185 -(** towards lift_5 **)
  11.186 -
  11.187 -(*lem_lift_5_3*)
  11.188 -Goal "0<N   \
  11.189 -\ ==> Lift : (closed Int Req n Int {s. metric n s = N} Int goingup) LeadsTo \
  11.190 -\            (moving Int Req n Int {s. metric n s < N})";
  11.191 -by (cut_facts_tac [bounded] 1);
  11.192 -by (ensures_tac "req_up" 1);
  11.193 -by (auto_tac (claset(), metric_ss));
  11.194 -qed "E_thm16a";
  11.195 -
  11.196 -
  11.197 -(*lem_lift_5_1 has ~goingup instead of goingdown*)
  11.198 -Goal "0<N ==>   \
  11.199 -\     Lift : (closed Int Req n Int {s. metric n s = N} Int goingdown) LeadsTo \
  11.200 -\                  (moving Int Req n Int {s. metric n s < N})";
  11.201 -by (cut_facts_tac [bounded] 1);
  11.202 -by (ensures_tac "req_down" 1);
  11.203 -by (auto_tac (claset(), metric_ss));
  11.204 -qed "E_thm16b";
  11.205 -
  11.206 -
  11.207 -(*lem_lift_5_0 proves an intersection involving ~goingup and goingup,
  11.208 -  i.e. the trivial disjunction, leading to an asymmetrical proof.*)
  11.209 -Goal "0<N ==> Req n Int {s. metric n s = N} <= goingup Un goingdown";
  11.210 -by (Clarify_tac 1);
  11.211 -by (force_tac (claset(), metric_ss) 1);
  11.212 -qed "E_thm16c";
  11.213 -
  11.214 -
  11.215 -(*lift_5*)
  11.216 -Goal "0<N ==> Lift : (closed Int Req n Int {s. metric n s = N}) LeadsTo   \
  11.217 -\                          (moving Int Req n Int {s. metric n s < N})";
  11.218 -by (rtac ([subset_imp_LeadsTo, [E_thm16a, E_thm16b] MRS LeadsTo_Un] 
  11.219 -	  MRS LeadsTo_Trans) 1);
  11.220 -by (dtac E_thm16c 1);
  11.221 -by Auto_tac;
  11.222 -qed "lift_5";
  11.223 -
  11.224 -
  11.225 -(** towards lift_3 **)
  11.226 -
  11.227 -(*lemma used to prove lem_lift_3_1*)
  11.228 -Goal "[| metric n s = 0;  Min <= floor s;  floor s <= Max |] ==> floor s = n";
  11.229 -by (auto_tac (claset(), metric_ss));
  11.230 -qed "metric_eq_0D";
  11.231 -
  11.232 -AddDs [metric_eq_0D];
  11.233 -
  11.234 -
  11.235 -(*lem_lift_3_1*)
  11.236 -Goal "Lift : (moving Int Req n Int {s. metric n s = 0}) LeadsTo   \
  11.237 -\                  (stopped Int atFloor n)";
  11.238 -by (cut_facts_tac [bounded] 1);
  11.239 -by (ensures_tac "request_act" 1);
  11.240 -by Auto_tac;
  11.241 -qed "E_thm11";
  11.242 -
  11.243 -(*lem_lift_3_5*)
  11.244 -Goal
  11.245 -  "Lift : (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
  11.246 -\ LeadsTo (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})";
  11.247 -by (ensures_tac "request_act" 1);
  11.248 -by (auto_tac (claset(), metric_ss));
  11.249 -qed "E_thm13";
  11.250 -
  11.251 -(*lem_lift_3_6*)
  11.252 -Goal "0 < N ==> \
  11.253 -\     Lift : \
  11.254 -\       (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
  11.255 -\       LeadsTo (opened Int Req n Int {s. metric n s = N})";
  11.256 -by (ensures_tac "open_act" 1);
  11.257 -by (auto_tac (claset(), metric_ss));
  11.258 -qed "E_thm14";
  11.259 -
  11.260 -(*lem_lift_3_7*)
  11.261 -Goal "Lift : (opened Int Req n Int {s. metric n s = N})  \
  11.262 -\            LeadsTo (closed Int Req n Int {s. metric n s = N})";
  11.263 -by (ensures_tac "close_act" 1);
  11.264 -by (auto_tac (claset(), metric_ss));
  11.265 -qed "E_thm15";
  11.266 -
  11.267 -
  11.268 -(** the final steps **)
  11.269 -
  11.270 -Goal "0 < N ==> \
  11.271 -\     Lift : \
  11.272 -\       (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s})   \
  11.273 -\       LeadsTo (moving Int Req n Int {s. metric n s < N})";
  11.274 -by (blast_tac (claset() addSIs [E_thm13, E_thm14, E_thm15, lift_5]
  11.275 -	                addIs [LeadsTo_Trans]) 1);
  11.276 -qed "lift_3_Req";
  11.277 -
  11.278 -
  11.279 -(*Now we observe that our integer metric is really a natural number*)
  11.280 -Goal "Lift : Always {s. 0 <= metric n s}";
  11.281 -by (rtac (bounded RS Always_weaken) 1);
  11.282 -by (auto_tac (claset(), metric_ss));
  11.283 -qed "Always_nonneg";
  11.284 -
  11.285 -val R_thm11 = [Always_nonneg, E_thm11] MRS Always_LeadsTo_weaken;
  11.286 -
  11.287 -Goal "Lift : (moving Int Req n) LeadsTo (stopped Int atFloor n)";
  11.288 -by (rtac (Always_nonneg RS integ_0_le_induct) 1);
  11.289 -by (case_tac "0 < z" 1);
  11.290 -(*If z <= 0 then actually z = 0*)
  11.291 -by (force_tac (claset() addIs [R_thm11, order_antisym], 
  11.292 -	       simpset() addsimps [linorder_not_less]) 2);
  11.293 -by (rtac ([asm_rl, Un_upper1] MRS LeadsTo_weaken_R) 1);
  11.294 -by (rtac ([subset_imp_LeadsTo, [lift_4, lift_3_Req] MRS LeadsTo_Un] 
  11.295 -	  MRS LeadsTo_Trans) 1);
  11.296 -by Auto_tac;
  11.297 -qed "lift_3";
  11.298 -
  11.299 -
  11.300 -val LeadsTo_Trans_Un' = rotate_prems 1 LeadsTo_Trans_Un;
  11.301 -(* [| Lift: B LeadsTo C; Lift: A LeadsTo B |] ==> Lift: (A Un B) LeadsTo C *)
  11.302 -
  11.303 -Goal "Lift : (Req n) LeadsTo (opened Int atFloor n)";
  11.304 -by (rtac LeadsTo_Trans 1);
  11.305 -by (rtac ([E_thm04, LeadsTo_Un_post] MRS LeadsTo_Un) 2);
  11.306 -by (rtac (E_thm01 RS LeadsTo_Trans_Un') 2);
  11.307 -by (rtac (lift_3 RS LeadsTo_Trans_Un') 2);
  11.308 -by (rtac (lift_2 RS LeadsTo_Trans_Un') 2);
  11.309 -by (rtac ([E_thm03,E_thm02] MRS LeadsTo_Trans_Un') 2);
  11.310 -by (rtac (open_move RS Always_LeadsToI) 1);
  11.311 -by (rtac ([open_stop, subset_imp_LeadsTo] MRS Always_LeadsToI) 1);
  11.312 -by (Clarify_tac 1);
  11.313 -(*The case split is not essential but makes Blast_tac much faster.
  11.314 -  Calling rotate_tac prevents simplification from looping*)
  11.315 -by (case_tac "open x" 1);
  11.316 -by (ALLGOALS (rotate_tac ~1));
  11.317 -by Auto_tac;
  11.318 -qed "lift_1";
  11.319 -
  11.320 -Close_locale "floor";
    12.1 --- a/src/HOL/UNITY/Simple/Lift.thy	Thu Jan 23 10:30:14 2003 +0100
    12.2 +++ b/src/HOL/UNITY/Simple/Lift.thy	Fri Jan 24 14:06:49 2003 +0100
    12.3 @@ -6,63 +6,63 @@
    12.4  The Lift-Control Example
    12.5  *)
    12.6  
    12.7 -Lift = SubstAx +
    12.8 +theory Lift = UNITY_Main:
    12.9  
   12.10  record state =
   12.11 -  floor :: int		(*current position of the lift*)
   12.12 -  open  :: bool		(*whether the door is open at floor*)
   12.13 -  stop  :: bool		(*whether the lift is stopped at floor*)
   12.14 -  req   :: int set	(*for each floor, whether the lift is requested*)
   12.15 -  up    :: bool		(*current direction of movement*)
   12.16 -  move  :: bool		(*whether moving takes precedence over opening*)
   12.17 +  floor :: "int"	    (*current position of the lift*)
   12.18 +  "open" :: "bool"	    (*whether the door is opened at floor*)
   12.19 +  stop  :: "bool"	    (*whether the lift is stopped at floor*)
   12.20 +  req   :: "int set"	    (*for each floor, whether the lift is requested*)
   12.21 +  up    :: "bool"	    (*current direction of movement*)
   12.22 +  move  :: "bool"	    (*whether moving takes precedence over opening*)
   12.23  
   12.24  consts
   12.25 -  Min, Max :: int       (*least and greatest floors*)
   12.26 +  Min :: "int"       (*least and greatest floors*)
   12.27 +  Max :: "int"       (*least and greatest floors*)
   12.28  
   12.29 -rules
   12.30 -  Min_le_Max  "Min <= Max"
   12.31 +axioms
   12.32 +  Min_le_Max [iff]: "Min <= Max"
   12.33    
   12.34  constdefs
   12.35    
   12.36    (** Abbreviations: the "always" part **)
   12.37    
   12.38 -  above :: state set
   12.39 +  above :: "state set"
   12.40      "above == {s. EX i. floor s < i & i <= Max & i : req s}"
   12.41  
   12.42 -  below :: state set
   12.43 +  below :: "state set"
   12.44      "below == {s. EX i. Min <= i & i < floor s & i : req s}"
   12.45  
   12.46 -  queueing :: state set
   12.47 +  queueing :: "state set"
   12.48      "queueing == above Un below"
   12.49  
   12.50 -  goingup :: state set
   12.51 +  goingup :: "state set"
   12.52      "goingup   == above Int  ({s. up s}  Un -below)"
   12.53  
   12.54 -  goingdown :: state set
   12.55 +  goingdown :: "state set"
   12.56      "goingdown == below Int ({s. ~ up s} Un -above)"
   12.57  
   12.58 -  ready :: state set
   12.59 +  ready :: "state set"
   12.60      "ready == {s. stop s & ~ open s & move s}"
   12.61 -
   12.62   
   12.63    (** Further abbreviations **)
   12.64  
   12.65 -  moving :: state set
   12.66 +  moving :: "state set"
   12.67      "moving ==  {s. ~ stop s & ~ open s}"
   12.68  
   12.69 -  stopped :: state set
   12.70 +  stopped :: "state set"
   12.71      "stopped == {s. stop s  & ~ open s & ~ move s}"
   12.72  
   12.73 -  opened :: state set
   12.74 +  opened :: "state set"
   12.75      "opened ==  {s. stop s  &  open s  &  move s}"
   12.76  
   12.77 -  closed :: state set  (*but this is the same as ready!!*)
   12.78 +  closed :: "state set"  (*but this is the same as ready!!*)
   12.79      "closed ==  {s. stop s  & ~ open s &  move s}"
   12.80  
   12.81 -  atFloor :: int => state set
   12.82 +  atFloor :: "int => state set"
   12.83      "atFloor n ==  {s. floor s = n}"
   12.84  
   12.85 -  Req :: int => state set
   12.86 +  Req :: "int => state set"
   12.87      "Req n ==  {s. n : req s}"
   12.88  
   12.89  
   12.90 @@ -118,7 +118,7 @@
   12.91  		        & Min <= n & n <= Max}"
   12.92  
   12.93  
   12.94 -  Lift :: state program
   12.95 +  Lift :: "state program"
   12.96      (*for the moment, we OMIT button_press*)
   12.97      "Lift == mk_program ({s. floor s = Min & ~ up s & move s & stop s &
   12.98  		          ~ open s & req s = {}},
   12.99 @@ -129,27 +129,27 @@
  12.100  
  12.101    (** Invariants **)
  12.102  
  12.103 -  bounded :: state set
  12.104 +  bounded :: "state set"
  12.105      "bounded == {s. Min <= floor s & floor s <= Max}"
  12.106  
  12.107 -  open_stop :: state set
  12.108 +  open_stop :: "state set"
  12.109      "open_stop == {s. open s --> stop s}"
  12.110    
  12.111 -  open_move :: state set
  12.112 +  open_move :: "state set"
  12.113      "open_move == {s. open s --> move s}"
  12.114    
  12.115 -  stop_floor :: state set
  12.116 +  stop_floor :: "state set"
  12.117      "stop_floor == {s. stop s & ~ move s --> floor s : req s}"
  12.118    
  12.119 -  moving_up :: state set
  12.120 +  moving_up :: "state set"
  12.121      "moving_up == {s. ~ stop s & up s -->
  12.122                     (EX f. floor s <= f & f <= Max & f : req s)}"
  12.123    
  12.124 -  moving_down :: state set
  12.125 +  moving_down :: "state set"
  12.126      "moving_down == {s. ~ stop s & ~ up s -->
  12.127                       (EX f. Min <= f & f <= floor s & f : req s)}"
  12.128    
  12.129 -  metric :: [int,state] => int
  12.130 +  metric :: "[int,state] => int"
  12.131      "metric ==
  12.132         %n s. if floor s < n then (if up s then n - floor s
  12.133  			          else (floor s - Min) + (n-Min))
  12.134 @@ -158,12 +158,310 @@
  12.135  		                  else floor s - n)
  12.136               else 0"
  12.137  
  12.138 -locale floor =
  12.139 -  fixes 
  12.140 -    n	:: int
  12.141 -  assumes
  12.142 -    Min_le_n    "Min <= n"
  12.143 -    n_le_Max    "n <= Max"
  12.144 -  defines
  12.145 +locale Floor =
  12.146 +  fixes n
  12.147 +  assumes Min_le_n [iff]: "Min <= n"
  12.148 +      and n_le_Max [iff]: "n <= Max"
  12.149 +
  12.150 +lemma not_mem_distinct: "[| x ~: A;  y : A |] ==> x ~= y"
  12.151 +by blast
  12.152 +
  12.153 +
  12.154 +declare Lift_def [THEN def_prg_Init, simp]
  12.155 +
  12.156 +declare request_act_def [THEN def_act_simp, simp]
  12.157 +declare open_act_def [THEN def_act_simp, simp]
  12.158 +declare close_act_def [THEN def_act_simp, simp]
  12.159 +declare req_up_def [THEN def_act_simp, simp]
  12.160 +declare req_down_def [THEN def_act_simp, simp]
  12.161 +declare move_up_def [THEN def_act_simp, simp]
  12.162 +declare move_down_def [THEN def_act_simp, simp]
  12.163 +declare button_press_def [THEN def_act_simp, simp]
  12.164 +
  12.165 +(*The ALWAYS properties*)
  12.166 +declare above_def [THEN def_set_simp, simp]
  12.167 +declare below_def [THEN def_set_simp, simp]
  12.168 +declare queueing_def [THEN def_set_simp, simp]
  12.169 +declare goingup_def [THEN def_set_simp, simp]
  12.170 +declare goingdown_def [THEN def_set_simp, simp]
  12.171 +declare ready_def [THEN def_set_simp, simp]
  12.172 +
  12.173 +(*Basic definitions*)
  12.174 +declare bounded_def [simp] 
  12.175 +        open_stop_def [simp] 
  12.176 +        open_move_def [simp] 
  12.177 +        stop_floor_def [simp]
  12.178 +        moving_up_def [simp]
  12.179 +        moving_down_def [simp]
  12.180 +
  12.181 +lemma open_stop: "Lift : Always open_stop"
  12.182 +apply (rule AlwaysI, force) 
  12.183 +apply (unfold Lift_def, constrains) 
  12.184 +done
  12.185 +
  12.186 +lemma stop_floor: "Lift : Always stop_floor"
  12.187 +apply (rule AlwaysI, force) 
  12.188 +apply (unfold Lift_def, constrains)
  12.189 +done
  12.190 +
  12.191 +(*This one needs open_stop, which was proved above*)
  12.192 +lemma open_move: "Lift : Always open_move"
  12.193 +apply (cut_tac open_stop)
  12.194 +apply (rule AlwaysI, force) 
  12.195 +apply (unfold Lift_def, constrains)
  12.196 +done
  12.197 +
  12.198 +lemma moving_up: "Lift : Always moving_up"
  12.199 +apply (rule AlwaysI, force) 
  12.200 +apply (unfold Lift_def, constrains)
  12.201 +apply (auto dest: zle_imp_zless_or_eq simp add: add1_zle_eq)
  12.202 +done
  12.203 +
  12.204 +lemma moving_down: "Lift : Always moving_down"
  12.205 +apply (rule AlwaysI, force) 
  12.206 +apply (unfold Lift_def, constrains)
  12.207 +apply (blast dest: zle_imp_zless_or_eq)
  12.208 +done
  12.209 +
  12.210 +lemma bounded: "Lift : Always bounded"
  12.211 +apply (cut_tac moving_up moving_down)
  12.212 +apply (rule AlwaysI, force) 
  12.213 +apply (unfold Lift_def, constrains, auto)
  12.214 +apply (drule not_mem_distinct, assumption, arith)+
  12.215 +done
  12.216 +
  12.217 +
  12.218 +subsection{*Progress*}
  12.219 +
  12.220 +declare moving_def [THEN def_set_simp, simp]
  12.221 +declare stopped_def [THEN def_set_simp, simp]
  12.222 +declare opened_def [THEN def_set_simp, simp]
  12.223 +declare closed_def [THEN def_set_simp, simp]
  12.224 +declare atFloor_def [THEN def_set_simp, simp]
  12.225 +declare Req_def [THEN def_set_simp, simp]
  12.226 +
  12.227 +
  12.228 +(** The HUG'93 paper mistakenly omits the Req n from these! **)
  12.229 +
  12.230 +(** Lift_1 **)
  12.231 +lemma E_thm01: "Lift : (stopped Int atFloor n) LeadsTo (opened Int atFloor n)"
  12.232 +apply (cut_tac stop_floor)
  12.233 +apply (unfold Lift_def, ensures_tac "open_act")
  12.234 +done  (*lem_lift_1_5*)
  12.235 +
  12.236 +lemma E_thm02: "Lift : (Req n Int stopped - atFloor n) LeadsTo  
  12.237 +                     (Req n Int opened - atFloor n)"
  12.238 +apply (cut_tac stop_floor)
  12.239 +apply (unfold Lift_def, ensures_tac "open_act")
  12.240 +done  (*lem_lift_1_1*)
  12.241 +
  12.242 +lemma E_thm03: "Lift : (Req n Int opened - atFloor n) LeadsTo  
  12.243 +                     (Req n Int closed - (atFloor n - queueing))"
  12.244 +apply (unfold Lift_def, ensures_tac "close_act")
  12.245 +done  (*lem_lift_1_2*)
  12.246 +
  12.247 +lemma E_thm04: "Lift : (Req n Int closed Int (atFloor n - queueing))   
  12.248 +             LeadsTo (opened Int atFloor n)"
  12.249 +apply (unfold Lift_def, ensures_tac "open_act")
  12.250 +done  (*lem_lift_1_7*)
  12.251 +
  12.252 +
  12.253 +(** Lift 2.  Statements of thm05a and thm05b were wrong! **)
  12.254 +
  12.255 +lemmas linorder_leI = linorder_not_less [THEN iffD1]
  12.256 +
  12.257 +lemmas (in Floor) le_MinD = Min_le_n [THEN order_antisym]
  12.258 +              and Max_leD = n_le_Max [THEN [2] order_antisym]
  12.259 +
  12.260 +declare (in Floor) le_MinD [dest!]
  12.261 +               and linorder_leI [THEN le_MinD, dest!]
  12.262 +               and Max_leD [dest!]
  12.263 +               and linorder_leI [THEN Max_leD, dest!]
  12.264 +
  12.265 +
  12.266 +(*lem_lift_2_0 
  12.267 +  NOT an ensures_tac property, but a mere inclusion
  12.268 +  don't know why script lift_2.uni says ENSURES*)
  12.269 +lemma (in Floor) E_thm05c: 
  12.270 +    "Lift : (Req n Int closed - (atFloor n - queueing))    
  12.271 +             LeadsTo ((closed Int goingup Int Req n)  Un  
  12.272 +                      (closed Int goingdown Int Req n))"
  12.273 +by (auto intro!: subset_imp_LeadsTo elim!: int_neqE)
  12.274 +
  12.275 +(*lift_2*)
  12.276 +lemma (in Floor) lift_2: "Lift : (Req n Int closed - (atFloor n - queueing))    
  12.277 +             LeadsTo (moving Int Req n)"
  12.278 +apply (rule LeadsTo_Trans [OF E_thm05c LeadsTo_Un])
  12.279 +apply (unfold Lift_def) 
  12.280 +apply (ensures_tac [2] "req_down")
  12.281 +apply (ensures_tac "req_up", auto)
  12.282 +done
  12.283 +
  12.284 +
  12.285 +(** Towards lift_4 ***)
  12.286 + 
  12.287 +declare split_if_asm [split]
  12.288 +
  12.289 +
  12.290 +(*lem_lift_4_1 *)
  12.291 +lemma (in Floor) E_thm12a:
  12.292 +     "0 < N ==>  
  12.293 +      Lift : (moving Int Req n Int {s. metric n s = N} Int  
  12.294 +              {s. floor s ~: req s} Int {s. up s})    
  12.295 +             LeadsTo  
  12.296 +               (moving Int Req n Int {s. metric n s < N})"
  12.297 +apply (cut_tac moving_up)
  12.298 +apply (unfold Lift_def, ensures_tac "move_up", safe)
  12.299 +(*this step consolidates two formulae to the goal  metric n s' <= metric n s*)
  12.300 +apply (erule linorder_leI [THEN order_antisym, symmetric])
  12.301 +apply (auto simp add: metric_def)
  12.302 +done
  12.303 +
  12.304 +
  12.305 +(*lem_lift_4_3 *)
  12.306 +lemma (in Floor) E_thm12b: "0 < N ==>  
  12.307 +      Lift : (moving Int Req n Int {s. metric n s = N} Int  
  12.308 +              {s. floor s ~: req s} - {s. up s})    
  12.309 +             LeadsTo (moving Int Req n Int {s. metric n s < N})"
  12.310 +apply (cut_tac moving_down)
  12.311 +apply (unfold Lift_def, ensures_tac "move_down", safe)
  12.312 +(*this step consolidates two formulae to the goal  metric n s' <= metric n s*)
  12.313 +apply (erule linorder_leI [THEN order_antisym, symmetric])
  12.314 +apply (auto simp add: metric_def)
  12.315 +done
  12.316 +
  12.317 +(*lift_4*)
  12.318 +lemma (in Floor) lift_4:
  12.319 +     "0<N ==> Lift : (moving Int Req n Int {s. metric n s = N} Int  
  12.320 +                            {s. floor s ~: req s}) LeadsTo      
  12.321 +                           (moving Int Req n Int {s. metric n s < N})"
  12.322 +apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo
  12.323 +                              LeadsTo_Un [OF E_thm12a E_thm12b]], auto)
  12.324 +done
  12.325 +
  12.326 +
  12.327 +(** towards lift_5 **)
  12.328 +
  12.329 +(*lem_lift_5_3*)
  12.330 +lemma (in Floor) E_thm16a: "0<N    
  12.331 +  ==> Lift : (closed Int Req n Int {s. metric n s = N} Int goingup) LeadsTo  
  12.332 +             (moving Int Req n Int {s. metric n s < N})"
  12.333 +apply (cut_tac bounded)
  12.334 +apply (unfold Lift_def, ensures_tac "req_up")
  12.335 +apply (auto simp add: metric_def)
  12.336 +done
  12.337 +
  12.338 +
  12.339 +(*lem_lift_5_1 has ~goingup instead of goingdown*)
  12.340 +lemma (in Floor) E_thm16b: "0<N ==>    
  12.341 +      Lift : (closed Int Req n Int {s. metric n s = N} Int goingdown) LeadsTo  
  12.342 +                   (moving Int Req n Int {s. metric n s < N})"
  12.343 +apply (cut_tac bounded)
  12.344 +apply (unfold Lift_def, ensures_tac "req_down")
  12.345 +apply (auto simp add: metric_def)
  12.346 +done
  12.347 +
  12.348 +
  12.349 +(*lem_lift_5_0 proves an intersection involving ~goingup and goingup,
  12.350 +  i.e. the trivial disjunction, leading to an asymmetrical proof.*)
  12.351 +lemma (in Floor) E_thm16c:
  12.352 +     "0<N ==> Req n Int {s. metric n s = N} <= goingup Un goingdown"
  12.353 +by (force simp add: metric_def)
  12.354 +
  12.355 +
  12.356 +(*lift_5*)
  12.357 +lemma (in Floor) lift_5:
  12.358 +     "0<N ==> Lift : (closed Int Req n Int {s. metric n s = N}) LeadsTo    
  12.359 +                     (moving Int Req n Int {s. metric n s < N})"
  12.360 +apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo
  12.361 +                              LeadsTo_Un [OF E_thm16a E_thm16b]])
  12.362 +apply (drule E_thm16c, auto)
  12.363 +done
  12.364 +
  12.365 +
  12.366 +(** towards lift_3 **)
  12.367 +
  12.368 +(*lemma used to prove lem_lift_3_1*)
  12.369 +lemma (in Floor) metric_eq_0D [dest]:
  12.370 +     "[| metric n s = 0;  Min <= floor s;  floor s <= Max |] ==> floor s = n"
  12.371 +by (force simp add: metric_def)
  12.372 +
  12.373 +
  12.374 +(*lem_lift_3_1*)
  12.375 +lemma (in Floor) E_thm11: "Lift : (moving Int Req n Int {s. metric n s = 0}) LeadsTo    
  12.376 +                       (stopped Int atFloor n)"
  12.377 +apply (cut_tac bounded)
  12.378 +apply (unfold Lift_def, ensures_tac "request_act", auto)
  12.379 +done
  12.380 +
  12.381 +(*lem_lift_3_5*)
  12.382 +lemma (in Floor) E_thm13: 
  12.383 +  "Lift : (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s})  
  12.384 +  LeadsTo (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})"
  12.385 +apply (unfold Lift_def, ensures_tac "request_act")
  12.386 +apply (auto simp add: metric_def)
  12.387 +done
  12.388 +
  12.389 +(*lem_lift_3_6*)
  12.390 +lemma (in Floor) E_thm14: "0 < N ==>  
  12.391 +      Lift :  
  12.392 +        (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})  
  12.393 +        LeadsTo (opened Int Req n Int {s. metric n s = N})"
  12.394 +apply (unfold Lift_def, ensures_tac "open_act")
  12.395 +apply (auto simp add: metric_def)
  12.396 +done
  12.397 +
  12.398 +(*lem_lift_3_7*)
  12.399 +lemma (in Floor) E_thm15: "Lift : (opened Int Req n Int {s. metric n s = N})   
  12.400 +             LeadsTo (closed Int Req n Int {s. metric n s = N})"
  12.401 +apply (unfold Lift_def, ensures_tac "close_act")
  12.402 +apply (auto simp add: metric_def)
  12.403 +done
  12.404 +
  12.405 +
  12.406 +(** the final steps **)
  12.407 +
  12.408 +lemma (in Floor) lift_3_Req: "0 < N ==>  
  12.409 +      Lift :  
  12.410 +        (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s})    
  12.411 +        LeadsTo (moving Int Req n Int {s. metric n s < N})"
  12.412 +apply (blast intro!: E_thm13 E_thm14 E_thm15 lift_5 intro: LeadsTo_Trans)
  12.413 +done
  12.414 +
  12.415 +
  12.416 +(*Now we observe that our integer metric is really a natural number*)
  12.417 +lemma (in Floor) Always_nonneg: "Lift : Always {s. 0 <= metric n s}"
  12.418 +apply (rule bounded [THEN Always_weaken])
  12.419 +apply (auto simp add: metric_def)
  12.420 +done
  12.421 +
  12.422 +lemmas (in Floor) R_thm11 = Always_LeadsTo_weaken [OF Always_nonneg E_thm11]
  12.423 +
  12.424 +lemma (in Floor) lift_3:
  12.425 +     "Lift : (moving Int Req n) LeadsTo (stopped Int atFloor n)"
  12.426 +apply (rule Always_nonneg [THEN integ_0_le_induct])
  12.427 +apply (case_tac "0 < z")
  12.428 +(*If z <= 0 then actually z = 0*)
  12.429 +prefer 2 apply (force intro: R_thm11 order_antisym simp add: linorder_not_less)
  12.430 +apply (rule LeadsTo_weaken_R [OF asm_rl Un_upper1])
  12.431 +apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo
  12.432 +                              LeadsTo_Un [OF lift_4 lift_3_Req]], auto)
  12.433 +done
  12.434 +
  12.435 +
  12.436 +lemma (in Floor) lift_1: "Lift : (Req n) LeadsTo (opened Int atFloor n)"
  12.437 +apply (rule LeadsTo_Trans)
  12.438 + prefer 2
  12.439 + apply (rule LeadsTo_Un [OF E_thm04 LeadsTo_Un_post])
  12.440 + apply (rule E_thm01 [THEN [2] LeadsTo_Trans_Un])
  12.441 + apply (rule lift_3 [THEN [2] LeadsTo_Trans_Un])
  12.442 + apply (rule lift_2 [THEN [2] LeadsTo_Trans_Un])
  12.443 + apply (rule LeadsTo_Trans_Un [OF E_thm02 E_thm03])
  12.444 +apply (rule open_move [THEN Always_LeadsToI])
  12.445 +apply (rule Always_LeadsToI [OF open_stop subset_imp_LeadsTo], clarify)
  12.446 +(*The case split is not essential but makes the proof much faster.*)
  12.447 +apply (case_tac "open x", auto)
  12.448 +done
  12.449 +
  12.450  
  12.451  end
    13.1 --- a/src/HOL/UNITY/Simple/Mutex.ML	Thu Jan 23 10:30:14 2003 +0100
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,166 +0,0 @@
    13.4 -(*  Title:      HOL/UNITY/Mutex
    13.5 -    ID:         $Id$
    13.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    13.7 -    Copyright   1998  University of Cambridge
    13.8 -
    13.9 -Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
   13.10 -*)
   13.11 -
   13.12 -Addsimps [Mutex_def RS def_prg_Init];
   13.13 -program_defs_ref := [Mutex_def];
   13.14 -
   13.15 -Addsimps (map simp_of_act
   13.16 -	  [U0_def, U1_def, U2_def, U3_def, U4_def, 
   13.17 -	   V0_def, V1_def, V2_def, V3_def, V4_def]);
   13.18 -
   13.19 -Addsimps (map simp_of_set [IU_def, IV_def, bad_IU_def]);
   13.20 -
   13.21 -
   13.22 -Goal "Mutex : Always IU";
   13.23 -by (always_tac 1);
   13.24 -qed "IU";
   13.25 -
   13.26 -Goal "Mutex : Always IV";
   13.27 -by (always_tac 1);
   13.28 -qed "IV";
   13.29 -
   13.30 -(*The safety property: mutual exclusion*)
   13.31 -Goal "Mutex : Always {s. ~ (m s = 3 & n s = 3)}";
   13.32 -by (rtac ([IU, IV] MRS Always_Int_I RS Always_weaken) 1);
   13.33 -by Auto_tac;
   13.34 -qed "mutual_exclusion";
   13.35 -
   13.36 -
   13.37 -(*The bad invariant FAILS in V1*)
   13.38 -Goal "Mutex : Always bad_IU";
   13.39 -by (always_tac 1);
   13.40 -by Auto_tac;
   13.41 -(*Resulting state: n=1, p=false, m=4, u=false.  
   13.42 -  Execution of V1 (the command of process v guarded by n=1) sets p:=true,
   13.43 -  violating the invariant!*)
   13.44 -(*Check that subgoals remain: proof failed.*)
   13.45 -getgoal 1;  
   13.46 -
   13.47 -
   13.48 -Goal "((1::int) <= i & i <= 3) = (i = 1 | i = 2 | i = 3)";
   13.49 -by (arith_tac 1);
   13.50 -qed "eq_123";
   13.51 -
   13.52 -
   13.53 -(*** Progress for U ***)
   13.54 -
   13.55 -Goalw [Unless_def] "Mutex : {s. m s=2} Unless {s. m s=3}";
   13.56 -by (constrains_tac 1);
   13.57 -qed "U_F0";
   13.58 -
   13.59 -Goal "Mutex : {s. m s=1} LeadsTo {s. p s = v s & m s = 2}";
   13.60 -by (ensures_tac "U1" 1);
   13.61 -qed "U_F1";
   13.62 -
   13.63 -Goal "Mutex : {s. ~ p s & m s = 2} LeadsTo {s. m s = 3}";
   13.64 -by (cut_facts_tac [IU] 1);
   13.65 -by (ensures_tac "U2" 1);
   13.66 -qed "U_F2";
   13.67 -
   13.68 -Goal "Mutex : {s. m s = 3} LeadsTo {s. p s}";
   13.69 -by (res_inst_tac [("B", "{s. m s = 4}")] LeadsTo_Trans 1);
   13.70 -by (ensures_tac "U4" 2);
   13.71 -by (ensures_tac "U3" 1);
   13.72 -qed "U_F3";
   13.73 -
   13.74 -Goal "Mutex : {s. m s = 2} LeadsTo {s. p s}";
   13.75 -by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] 
   13.76 -	  MRS LeadsTo_Diff) 1);
   13.77 -by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
   13.78 -by (auto_tac (claset() addSEs [less_SucE], simpset()));
   13.79 -val U_lemma2 = result();
   13.80 -
   13.81 -Goal "Mutex : {s. m s = 1} LeadsTo {s. p s}";
   13.82 -by (rtac ([U_F1 RS LeadsTo_weaken_R, U_lemma2] MRS LeadsTo_Trans) 1);
   13.83 -by (Blast_tac 1);
   13.84 -val U_lemma1 = result();
   13.85 -
   13.86 -Goal "Mutex : {s. 1 <= m s & m s <= 3} LeadsTo {s. p s}";
   13.87 -by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
   13.88 -				  U_lemma1, U_lemma2, U_F3] ) 1);
   13.89 -val U_lemma123 = result();
   13.90 -
   13.91 -(*Misra's F4*)
   13.92 -Goal "Mutex : {s. u s} LeadsTo {s. p s}";
   13.93 -by (rtac ([IU, U_lemma123] MRS Always_LeadsTo_weaken) 1);
   13.94 -by Auto_tac;
   13.95 -qed "u_Leadsto_p";
   13.96 -
   13.97 -
   13.98 -(*** Progress for V ***)
   13.99 -
  13.100 -
  13.101 -Goalw [Unless_def] "Mutex : {s. n s=2} Unless {s. n s=3}";
  13.102 -by (constrains_tac 1);
  13.103 -qed "V_F0";
  13.104 -
  13.105 -Goal "Mutex : {s. n s=1} LeadsTo {s. p s = (~ u s) & n s = 2}";
  13.106 -by (ensures_tac "V1" 1);
  13.107 -qed "V_F1";
  13.108 -
  13.109 -Goal "Mutex : {s. p s & n s = 2} LeadsTo {s. n s = 3}";
  13.110 -by (cut_facts_tac [IV] 1);
  13.111 -by (ensures_tac "V2" 1);
  13.112 -qed "V_F2";
  13.113 -
  13.114 -Goal "Mutex : {s. n s = 3} LeadsTo {s. ~ p s}";
  13.115 -by (res_inst_tac [("B", "{s. n s = 4}")] LeadsTo_Trans 1);
  13.116 -by (ensures_tac "V4" 2);
  13.117 -by (ensures_tac "V3" 1);
  13.118 -qed "V_F3";
  13.119 -
  13.120 -Goal "Mutex : {s. n s = 2} LeadsTo {s. ~ p s}";
  13.121 -by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] 
  13.122 -	  MRS LeadsTo_Diff) 1);
  13.123 -by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1);
  13.124 -by (auto_tac (claset() addSEs [less_SucE], simpset()));
  13.125 -val V_lemma2 = result();
  13.126 -
  13.127 -Goal "Mutex : {s. n s = 1} LeadsTo {s. ~ p s}";
  13.128 -by (rtac ([V_F1 RS LeadsTo_weaken_R, V_lemma2] MRS LeadsTo_Trans) 1);
  13.129 -by (Blast_tac 1);
  13.130 -val V_lemma1 = result();
  13.131 -
  13.132 -Goal "Mutex : {s. 1 <= n s & n s <= 3} LeadsTo {s. ~ p s}";
  13.133 -by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
  13.134 -				  V_lemma1, V_lemma2, V_F3] ) 1);
  13.135 -val V_lemma123 = result();
  13.136 -
  13.137 -
  13.138 -(*Misra's F4*)
  13.139 -Goal "Mutex : {s. v s} LeadsTo {s. ~ p s}";
  13.140 -by (rtac ([IV, V_lemma123] MRS Always_LeadsTo_weaken) 1);
  13.141 -by Auto_tac;
  13.142 -qed "v_Leadsto_not_p";
  13.143 -
  13.144 -
  13.145 -(** Absence of starvation **)
  13.146 -
  13.147 -(*Misra's F6*)
  13.148 -Goal "Mutex : {s. m s = 1} LeadsTo {s. m s = 3}";
  13.149 -by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
  13.150 -by (rtac U_F2 2);
  13.151 -by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
  13.152 -by (stac Un_commute 1);
  13.153 -by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
  13.154 -by (rtac ([v_Leadsto_not_p, U_F0] MRS PSP_Unless) 2);
  13.155 -by (rtac (U_F1 RS LeadsTo_weaken_R) 1);
  13.156 -by Auto_tac;
  13.157 -qed "m1_Leadsto_3";
  13.158 -
  13.159 -(*The same for V*)
  13.160 -Goal "Mutex : {s. n s = 1} LeadsTo {s. n s = 3}";
  13.161 -by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
  13.162 -by (rtac V_F2 2);
  13.163 -by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
  13.164 -by (stac Un_commute 1);
  13.165 -by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
  13.166 -by (rtac ([u_Leadsto_p, V_F0] MRS PSP_Unless) 2);
  13.167 -by (rtac (V_F1 RS LeadsTo_weaken_R) 1);
  13.168 -by Auto_tac;
  13.169 -qed "n1_Leadsto_3";
    14.1 --- a/src/HOL/UNITY/Simple/Mutex.thy	Thu Jan 23 10:30:14 2003 +0100
    14.2 +++ b/src/HOL/UNITY/Simple/Mutex.thy	Fri Jan 24 14:06:49 2003 +0100
    14.3 @@ -6,7 +6,7 @@
    14.4  Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
    14.5  *)
    14.6  
    14.7 -Mutex = SubstAx +
    14.8 +theory Mutex = UNITY_Main:
    14.9  
   14.10  record state =
   14.11    p :: bool
   14.12 @@ -53,7 +53,7 @@
   14.13    V4 :: command
   14.14      "V4 == {(s,s'). s' = s (|p:=False, n:=0|) & n s = 4}"
   14.15  
   14.16 -  Mutex :: state program
   14.17 +  Mutex :: "state program"
   14.18      "Mutex == mk_program ({s. ~ u s & ~ v s & m s = 0 & n s = 0},
   14.19  		 	  {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4},
   14.20  			  UNIV)"
   14.21 @@ -61,16 +61,166 @@
   14.22  
   14.23    (** The correct invariants **)
   14.24  
   14.25 -  IU :: state set
   14.26 +  IU :: "state set"
   14.27      "IU == {s. (u s = (1 <= m s & m s <= 3)) & (m s = 3 --> ~ p s)}"
   14.28  
   14.29 -  IV :: state set
   14.30 +  IV :: "state set"
   14.31      "IV == {s. (v s = (1 <= n s & n s <= 3)) & (n s = 3 --> p s)}"
   14.32  
   14.33    (** The faulty invariant (for U alone) **)
   14.34  
   14.35 -  bad_IU :: state set
   14.36 +  bad_IU :: "state set"
   14.37      "bad_IU == {s. (u s = (1 <= m s & m s <= 3)) &
   14.38  	           (3 <= m s & m s <= 4 --> ~ p s)}"
   14.39  
   14.40 +
   14.41 +declare Mutex_def [THEN def_prg_Init, simp]
   14.42 +
   14.43 +declare U0_def [THEN def_act_simp, simp]
   14.44 +declare U1_def [THEN def_act_simp, simp]
   14.45 +declare U2_def [THEN def_act_simp, simp]
   14.46 +declare U3_def [THEN def_act_simp, simp]
   14.47 +declare U4_def [THEN def_act_simp, simp]
   14.48 +declare V0_def [THEN def_act_simp, simp]
   14.49 +declare V1_def [THEN def_act_simp, simp]
   14.50 +declare V2_def [THEN def_act_simp, simp]
   14.51 +declare V3_def [THEN def_act_simp, simp]
   14.52 +declare V4_def [THEN def_act_simp, simp]
   14.53 +
   14.54 +declare IU_def [THEN def_set_simp, simp]
   14.55 +declare IV_def [THEN def_set_simp, simp]
   14.56 +declare bad_IU_def [THEN def_set_simp, simp]
   14.57 +
   14.58 +lemma IU: "Mutex : Always IU"
   14.59 +apply (rule AlwaysI, force) 
   14.60 +apply (unfold Mutex_def, constrains) 
   14.61 +done
   14.62 +
   14.63 +
   14.64 +lemma IV: "Mutex : Always IV"
   14.65 +apply (rule AlwaysI, force) 
   14.66 +apply (unfold Mutex_def, constrains)
   14.67 +done
   14.68 +
   14.69 +(*The safety property: mutual exclusion*)
   14.70 +lemma mutual_exclusion: "Mutex : Always {s. ~ (m s = 3 & n s = 3)}"
   14.71 +apply (rule Always_weaken) 
   14.72 +apply (rule Always_Int_I [OF IU IV], auto)
   14.73 +done
   14.74 +
   14.75 +
   14.76 +(*The bad invariant FAILS in V1*)
   14.77 +lemma "Mutex : Always bad_IU"
   14.78 +apply (rule AlwaysI, force) 
   14.79 +apply (unfold Mutex_def, constrains, auto)
   14.80 +(*Resulting state: n=1, p=false, m=4, u=false.  
   14.81 +  Execution of V1 (the command of process v guarded by n=1) sets p:=true,
   14.82 +  violating the invariant!*)
   14.83 +oops
   14.84 +
   14.85 +
   14.86 +lemma eq_123: "((1::int) <= i & i <= 3) = (i = 1 | i = 2 | i = 3)"
   14.87 +by arith
   14.88 +
   14.89 +
   14.90 +(*** Progress for U ***)
   14.91 +
   14.92 +lemma U_F0: "Mutex : {s. m s=2} Unless {s. m s=3}"
   14.93 +by (unfold Unless_def Mutex_def, constrains)
   14.94 +
   14.95 +lemma U_F1: "Mutex : {s. m s=1} LeadsTo {s. p s = v s & m s = 2}"
   14.96 +by (unfold Mutex_def, ensures_tac "U1")
   14.97 +
   14.98 +lemma U_F2: "Mutex : {s. ~ p s & m s = 2} LeadsTo {s. m s = 3}"
   14.99 +apply (cut_tac IU)
  14.100 +apply (unfold Mutex_def, ensures_tac U2)
  14.101 +done
  14.102 +
  14.103 +lemma U_F3: "Mutex : {s. m s = 3} LeadsTo {s. p s}"
  14.104 +apply (rule_tac B = "{s. m s = 4}" in LeadsTo_Trans)
  14.105 + apply (unfold Mutex_def)
  14.106 + apply (ensures_tac U3)
  14.107 +apply (ensures_tac U4)
  14.108 +done
  14.109 +
  14.110 +lemma U_lemma2: "Mutex : {s. m s = 2} LeadsTo {s. p s}"
  14.111 +apply (rule LeadsTo_Diff [OF LeadsTo_weaken_L
  14.112 +                             Int_lower2 [THEN subset_imp_LeadsTo]])
  14.113 +apply (rule LeadsTo_Trans [OF U_F2 U_F3], auto)
  14.114 +done
  14.115 +
  14.116 +lemma U_lemma1: "Mutex : {s. m s = 1} LeadsTo {s. p s}"
  14.117 +by (rule LeadsTo_Trans [OF U_F1 [THEN LeadsTo_weaken_R] U_lemma2], blast)
  14.118 +
  14.119 +lemma U_lemma123: "Mutex : {s. 1 <= m s & m s <= 3} LeadsTo {s. p s}"
  14.120 +by (simp add: eq_123 Collect_disj_eq LeadsTo_Un_distrib U_lemma1 U_lemma2 U_F3)
  14.121 +
  14.122 +(*Misra's F4*)
  14.123 +lemma u_Leadsto_p: "Mutex : {s. u s} LeadsTo {s. p s}"
  14.124 +by (rule Always_LeadsTo_weaken [OF IU U_lemma123], auto)
  14.125 +
  14.126 +
  14.127 +(*** Progress for V ***)
  14.128 +
  14.129 +
  14.130 +lemma V_F0: "Mutex : {s. n s=2} Unless {s. n s=3}"
  14.131 +by (unfold Unless_def Mutex_def, constrains)
  14.132 +
  14.133 +lemma V_F1: "Mutex : {s. n s=1} LeadsTo {s. p s = (~ u s) & n s = 2}"
  14.134 +by (unfold Mutex_def, ensures_tac "V1")
  14.135 +
  14.136 +lemma V_F2: "Mutex : {s. p s & n s = 2} LeadsTo {s. n s = 3}"
  14.137 +apply (cut_tac IV)
  14.138 +apply (unfold Mutex_def, ensures_tac "V2")
  14.139 +done
  14.140 +
  14.141 +lemma V_F3: "Mutex : {s. n s = 3} LeadsTo {s. ~ p s}"
  14.142 +apply (rule_tac B = "{s. n s = 4}" in LeadsTo_Trans)
  14.143 + apply (unfold Mutex_def)
  14.144 + apply (ensures_tac V3)
  14.145 +apply (ensures_tac V4)
  14.146 +done
  14.147 +
  14.148 +lemma V_lemma2: "Mutex : {s. n s = 2} LeadsTo {s. ~ p s}"
  14.149 +apply (rule LeadsTo_Diff [OF LeadsTo_weaken_L
  14.150 +                             Int_lower2 [THEN subset_imp_LeadsTo]])
  14.151 +apply (rule LeadsTo_Trans [OF V_F2 V_F3], auto) 
  14.152 +done
  14.153 +
  14.154 +lemma V_lemma1: "Mutex : {s. n s = 1} LeadsTo {s. ~ p s}"
  14.155 +by (rule LeadsTo_Trans [OF V_F1 [THEN LeadsTo_weaken_R] V_lemma2], blast)
  14.156 +
  14.157 +lemma V_lemma123: "Mutex : {s. 1 <= n s & n s <= 3} LeadsTo {s. ~ p s}"
  14.158 +by (simp add: eq_123 Collect_disj_eq LeadsTo_Un_distrib V_lemma1 V_lemma2 V_F3)
  14.159 +
  14.160 +
  14.161 +(*Misra's F4*)
  14.162 +lemma v_Leadsto_not_p: "Mutex : {s. v s} LeadsTo {s. ~ p s}"
  14.163 +by (rule Always_LeadsTo_weaken [OF IV V_lemma123], auto)
  14.164 +
  14.165 +
  14.166 +(** Absence of starvation **)
  14.167 +
  14.168 +(*Misra's F6*)
  14.169 +lemma m1_Leadsto_3: "Mutex : {s. m s = 1} LeadsTo {s. m s = 3}"
  14.170 +apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate])
  14.171 +apply (rule_tac [2] U_F2)
  14.172 +apply (simp add: Collect_conj_eq)
  14.173 +apply (subst Un_commute)
  14.174 +apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate])
  14.175 + apply (rule_tac [2] PSP_Unless [OF v_Leadsto_not_p U_F0])
  14.176 +apply (rule U_F1 [THEN LeadsTo_weaken_R], auto)
  14.177 +done
  14.178 +
  14.179 +(*The same for V*)
  14.180 +lemma n1_Leadsto_3: "Mutex : {s. n s = 1} LeadsTo {s. n s = 3}"
  14.181 +apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate])
  14.182 +apply (rule_tac [2] V_F2)
  14.183 +apply (simp add: Collect_conj_eq)
  14.184 +apply (subst Un_commute)
  14.185 +apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate])
  14.186 + apply (rule_tac [2] PSP_Unless [OF u_Leadsto_p V_F0])
  14.187 +apply (rule V_F1 [THEN LeadsTo_weaken_R], auto)
  14.188 +done
  14.189 +
  14.190  end
    15.1 --- a/src/HOL/UNITY/Simple/Network.ML	Thu Jan 23 10:30:14 2003 +0100
    15.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.3 @@ -1,59 +0,0 @@
    15.4 -(*  Title:      HOL/UNITY/Network
    15.5 -    ID:         $Id$
    15.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    15.7 -    Copyright   1998  University of Cambridge
    15.8 -
    15.9 -The Communication Network
   15.10 -
   15.11 -From Misra, "A Logic for Concurrent Programming" (1994), section 5.7
   15.12 -*)
   15.13 -
   15.14 -val [rsA, rsB, sent_nondec, rcvd_nondec, rcvd_idle, sent_idle] = 
   15.15 -Goalw [stable_def]
   15.16 -   "[| !! m. F : stable {s. s(Bproc,Rcvd) <= s(Aproc,Sent)};  \
   15.17 -\      !! m. F : stable {s. s(Aproc,Rcvd) <= s(Bproc,Sent)};  \
   15.18 -\      !! m proc. F : stable {s. m <= s(proc,Sent)};  \
   15.19 -\      !! n proc. F : stable {s. n <= s(proc,Rcvd)};  \
   15.20 -\      !! m proc. F : {s. s(proc,Idle) = Suc 0 & s(proc,Rcvd) = m} co \
   15.21 -\                                 {s. s(proc,Rcvd) = m --> s(proc,Idle) = Suc 0}; \
   15.22 -\      !! n proc. F : {s. s(proc,Idle) = Suc 0 & s(proc,Sent) = n} co \
   15.23 -\                                 {s. s(proc,Sent) = n} \
   15.24 -\   |] ==> F : stable {s. s(Aproc,Idle) = Suc 0 & s(Bproc,Idle) = Suc 0 & \
   15.25 -\                         s(Aproc,Sent) = s(Bproc,Rcvd) & \
   15.26 -\                         s(Bproc,Sent) = s(Aproc,Rcvd) & \
   15.27 -\                         s(Aproc,Rcvd) = m & s(Bproc,Rcvd) = n}";
   15.28 -
   15.29 -val sent_nondec_A = read_instantiate [("proc","Aproc")] sent_nondec;
   15.30 -val sent_nondec_B = read_instantiate [("proc","Bproc")] sent_nondec;
   15.31 -val rcvd_nondec_A = read_instantiate [("proc","Aproc")] rcvd_nondec;
   15.32 -val rcvd_nondec_B = read_instantiate [("proc","Bproc")] rcvd_nondec;
   15.33 -val rcvd_idle_A = read_instantiate [("proc","Aproc")] rcvd_idle;
   15.34 -val rcvd_idle_B = read_instantiate [("proc","Bproc")] rcvd_idle;
   15.35 -val sent_idle_A = read_instantiate [("proc","Aproc")] sent_idle;
   15.36 -val sent_idle_B = read_instantiate [("proc","Bproc")] sent_idle;
   15.37 -
   15.38 -val rs_AB = [rsA, rsB] MRS constrains_Int;
   15.39 -val sent_nondec_AB = [sent_nondec_A, sent_nondec_B] MRS constrains_Int;
   15.40 -val rcvd_nondec_AB = [rcvd_nondec_A, rcvd_nondec_B] MRS constrains_Int;
   15.41 -val rcvd_idle_AB = [rcvd_idle_A, rcvd_idle_B] MRS constrains_Int;
   15.42 -val sent_idle_AB = [sent_idle_A, sent_idle_B] MRS constrains_Int;
   15.43 -val nondec_AB = [sent_nondec_AB, rcvd_nondec_AB] MRS constrains_Int;
   15.44 -val idle_AB = [rcvd_idle_AB, sent_idle_AB] MRS constrains_Int;
   15.45 -val nondec_idle = [nondec_AB, idle_AB] MRS constrains_Int;
   15.46 -
   15.47 -by (rtac constrainsI 1);
   15.48 -by (dtac ([rs_AB, nondec_idle] MRS constrains_Int RS constrainsD) 1);
   15.49 -by (assume_tac 1);
   15.50 -by (ALLGOALS Asm_full_simp_tac);
   15.51 -by (blast_tac (HOL_cs addIs [order_refl]) 1);
   15.52 -by (Clarify_tac 1);
   15.53 -by (subgoals_tac ["s' (Aproc, Rcvd) = s (Aproc, Rcvd)",
   15.54 -		  "s' (Bproc, Rcvd) = s (Bproc, Rcvd)"] 1);
   15.55 -by (REPEAT 
   15.56 -    (blast_tac (claset() addIs [order_antisym, le_trans, eq_imp_le]) 2));
   15.57 -by (Asm_simp_tac 1);
   15.58 -result();
   15.59 -
   15.60 -
   15.61 -
   15.62 -
    16.1 --- a/src/HOL/UNITY/Simple/Network.thy	Thu Jan 23 10:30:14 2003 +0100
    16.2 +++ b/src/HOL/UNITY/Simple/Network.thy	Fri Jan 24 14:06:49 2003 +0100
    16.3 @@ -8,7 +8,7 @@
    16.4  From Misra, "A Logic for Concurrent Programming" (1994), section 5.7
    16.5  *)
    16.6  
    16.7 -Network = UNITY +
    16.8 +theory Network = UNITY:
    16.9  
   16.10  (*The state assigns a number to each process variable*)
   16.11  
   16.12 @@ -18,4 +18,53 @@
   16.13  
   16.14  types state = "pname * pvar => nat"
   16.15  
   16.16 +locale F_props =
   16.17 +  fixes F 
   16.18 +  assumes rsA: "F : stable {s. s(Bproc,Rcvd) <= s(Aproc,Sent)}"
   16.19 +      and rsB: "F : stable {s. s(Aproc,Rcvd) <= s(Bproc,Sent)}"
   16.20 +    and sent_nondec: "F : stable {s. m <= s(proc,Sent)}"
   16.21 +    and rcvd_nondec: "F : stable {s. n <= s(proc,Rcvd)}"
   16.22 +    and rcvd_idle: "F : {s. s(proc,Idle) = Suc 0 & s(proc,Rcvd) = m}
   16.23 +                        co {s. s(proc,Rcvd) = m --> s(proc,Idle) = Suc 0}"
   16.24 +    and sent_idle: "F : {s. s(proc,Idle) = Suc 0 & s(proc,Sent) = n}
   16.25 +                        co {s. s(proc,Sent) = n}"
   16.26 +  
   16.27 +
   16.28 +lemmas (in F_props) 
   16.29 +        sent_nondec_A = sent_nondec [of _ Aproc]
   16.30 +    and sent_nondec_B = sent_nondec [of _ Bproc]
   16.31 +    and rcvd_nondec_A = rcvd_nondec [of _ Aproc]
   16.32 +    and rcvd_nondec_B = rcvd_nondec [of _ Bproc]
   16.33 +    and rcvd_idle_A = rcvd_idle [of Aproc]
   16.34 +    and rcvd_idle_B = rcvd_idle [of Bproc]
   16.35 +    and sent_idle_A = sent_idle [of Aproc]
   16.36 +    and sent_idle_B = sent_idle [of Bproc]
   16.37 +
   16.38 +    and rs_AB = stable_Int [OF rsA rsB]
   16.39 +    and sent_nondec_AB = stable_Int [OF sent_nondec_A sent_nondec_B]
   16.40 +    and rcvd_nondec_AB = stable_Int [OF rcvd_nondec_A rcvd_nondec_B]
   16.41 +    and rcvd_idle_AB = constrains_Int [OF rcvd_idle_A rcvd_idle_B]
   16.42 +    and sent_idle_AB = constrains_Int [OF sent_idle_A sent_idle_B]
   16.43 +    and nondec_AB = stable_Int [OF sent_nondec_AB rcvd_nondec_AB]
   16.44 +    and idle_AB = constrains_Int [OF rcvd_idle_AB sent_idle_AB]
   16.45 +    and nondec_idle = constrains_Int [OF nondec_AB [unfolded stable_def] 
   16.46 +                                         idle_AB]
   16.47 +
   16.48 +lemma (in F_props)
   16.49 +  shows "F : stable {s. s(Aproc,Idle) = Suc 0 & s(Bproc,Idle) = Suc 0 &  
   16.50 +			s(Aproc,Sent) = s(Bproc,Rcvd) &  
   16.51 +			s(Bproc,Sent) = s(Aproc,Rcvd) &  
   16.52 +			s(Aproc,Rcvd) = m & s(Bproc,Rcvd) = n}"
   16.53 +apply (unfold stable_def) 
   16.54 +apply (rule constrainsI)
   16.55 +apply (drule constrains_Int [OF rs_AB [unfolded stable_def] nondec_idle, 
   16.56 +                             THEN constrainsD], assumption)
   16.57 +apply simp_all
   16.58 +apply (blast intro!: order_refl del: le0, clarify) 
   16.59 +apply (subgoal_tac "s' (Aproc, Rcvd) = s (Aproc, Rcvd)")
   16.60 +apply (subgoal_tac "s' (Bproc, Rcvd) = s (Bproc, Rcvd)") 
   16.61 +apply simp 
   16.62 +apply (blast intro: order_antisym le_trans eq_imp_le)+
   16.63 +done
   16.64 +
   16.65  end
    17.1 --- a/src/HOL/UNITY/Simple/Reach.ML	Thu Jan 23 10:30:14 2003 +0100
    17.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.3 @@ -1,142 +0,0 @@
    17.4 -(*  Title:      HOL/UNITY/Reach.thy
    17.5 -    ID:         $Id$
    17.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    17.7 -    Copyright   1998  University of Cambridge
    17.8 -
    17.9 -Reachability in Directed Graphs.  From Chandy and Misra, section 6.4.
   17.10 -	[ this example took only four days!]
   17.11 -*)
   17.12 -
   17.13 -(*TO SIMPDATA.ML??  FOR CLASET??  *)
   17.14 -val major::prems = goal thy 
   17.15 -    "[| if P then Q else R;    \
   17.16 -\       [| P;   Q |] ==> S;    \
   17.17 -\       [| ~ P; R |] ==> S |] ==> S";
   17.18 -by (cut_facts_tac [major] 1);
   17.19 -by (blast_tac (claset() addSDs [if_bool_eq_disj RS iffD1] addIs prems) 1);
   17.20 -qed "ifE";
   17.21 -
   17.22 -AddSEs [ifE];
   17.23 -
   17.24 -
   17.25 -Addsimps [Rprg_def RS def_prg_Init];
   17.26 -program_defs_ref := [Rprg_def];
   17.27 -
   17.28 -Addsimps [simp_of_act asgt_def];
   17.29 -
   17.30 -(*All vertex sets are finite*)
   17.31 -AddIffs [[subset_UNIV, finite_graph] MRS finite_subset];
   17.32 -
   17.33 -Addsimps [simp_of_set reach_invariant_def];
   17.34 -
   17.35 -Goal "Rprg : Always reach_invariant";
   17.36 -by (always_tac 1);
   17.37 -by (blast_tac (claset() addIs [rtrancl_trans]) 1);
   17.38 -qed "reach_invariant";
   17.39 -
   17.40 -
   17.41 -(*** Fixedpoint ***)
   17.42 -
   17.43 -(*If it reaches a fixedpoint, it has found a solution*)
   17.44 -Goalw [fixedpoint_def]
   17.45 -     "fixedpoint Int reach_invariant = { %v. (init, v) : edges^* }";
   17.46 -by (rtac equalityI 1);
   17.47 -by (auto_tac (claset() addSIs [ext], simpset()));
   17.48 -by (blast_tac (claset() addIs [rtrancl_trans]) 2);
   17.49 -by (etac rtrancl_induct 1);
   17.50 -by Auto_tac;
   17.51 -qed "fixedpoint_invariant_correct";
   17.52 -
   17.53 -Goalw [FP_def, fixedpoint_def, stable_def, constrains_def, Rprg_def]
   17.54 -     "FP Rprg <= fixedpoint";
   17.55 -by Auto_tac;
   17.56 -by (dtac bspec 1 THEN atac 1);
   17.57 -by (asm_full_simp_tac (simpset() addsimps [Image_singleton, image_iff]) 1);
   17.58 -by (dtac fun_cong 1);
   17.59 -by Auto_tac;
   17.60 -val lemma1 = result();
   17.61 -
   17.62 -Goalw [FP_def, fixedpoint_def, stable_def, constrains_def, Rprg_def]
   17.63 -     "fixedpoint <= FP Rprg";
   17.64 -by (auto_tac (claset() addSIs [ext], simpset()));
   17.65 -val lemma2 = result();
   17.66 -
   17.67 -Goal "FP Rprg = fixedpoint";
   17.68 -by (rtac ([lemma1,lemma2] MRS equalityI) 1);
   17.69 -qed "FP_fixedpoint";
   17.70 -
   17.71 -
   17.72 -(*If we haven't reached a fixedpoint then there is some edge for which u but
   17.73 -  not v holds.  Progress will be proved via an ENSURES assertion that the
   17.74 -  metric will decrease for each suitable edge.  A union over all edges proves
   17.75 -  a LEADSTO assertion that the metric decreases if we are not at a fixedpoint.
   17.76 -  *)
   17.77 -
   17.78 -Goal "- fixedpoint = (UN (u,v): edges. {s. s u & ~ s v})";
   17.79 -by (simp_tac (simpset() addsimps
   17.80 -	      [Compl_FP, UN_UN_flatten, FP_fixedpoint RS sym, Rprg_def]) 1);
   17.81 -by Auto_tac;
   17.82 -by (rtac fun_upd_idem 1);
   17.83 -by Auto_tac;
   17.84 -by (force_tac (claset() addSIs [rev_bexI], 
   17.85 -	       simpset() addsimps [fun_upd_idem_iff]) 1);
   17.86 -qed "Compl_fixedpoint";
   17.87 -
   17.88 -Goal "A - fixedpoint = (UN (u,v): edges. A Int {s. s u & ~ s v})";
   17.89 -by (simp_tac (simpset() addsimps [Diff_eq, Compl_fixedpoint]) 1);
   17.90 -by (Blast_tac 1);
   17.91 -qed "Diff_fixedpoint";
   17.92 -
   17.93 -
   17.94 -(*** Progress ***)
   17.95 -
   17.96 -Goalw [metric_def] "~ s x ==> Suc (metric (s(x:=True))) = metric s";
   17.97 -by (subgoal_tac "{v. ~ (s(x:=True)) v} = {v. ~ s v} - {x}" 1);
   17.98 -by (Force_tac 2);
   17.99 -by (asm_full_simp_tac (simpset() addsimps [card_Suc_Diff1]) 1);
  17.100 -qed "Suc_metric";
  17.101 -
  17.102 -Goal "~ s x ==> metric (s(x:=True)) < metric s";
  17.103 -by (etac (Suc_metric RS subst) 1);
  17.104 -by (Blast_tac 1);
  17.105 -qed "metric_less";
  17.106 -AddSIs [metric_less];
  17.107 -
  17.108 -Goal "metric (s(y:=s x | s y)) <= metric s";
  17.109 -by (case_tac "s x --> s y" 1);
  17.110 -by (auto_tac (claset() addIs [less_imp_le],
  17.111 -	      simpset() addsimps [fun_upd_idem]));
  17.112 -qed "metric_le";
  17.113 -
  17.114 -Goal "Rprg : ((metric-`{m}) - fixedpoint) LeadsTo (metric-`(lessThan m))";
  17.115 -by (simp_tac (simpset() addsimps [Diff_fixedpoint]) 1);
  17.116 -by (rtac LeadsTo_UN 1);
  17.117 -by Auto_tac;
  17.118 -by (ensures_tac "asgt a b" 1);
  17.119 -by (Blast_tac 2);
  17.120 -by (full_simp_tac (simpset() addsimps [not_less_iff_le]) 1);
  17.121 -by (dtac (metric_le RS order_antisym) 1);
  17.122 -by (auto_tac (claset() addEs [less_not_refl3 RSN (2, rev_notE)],
  17.123 -	      simpset()));
  17.124 -qed "LeadsTo_Diff_fixedpoint";
  17.125 -
  17.126 -Goal "Rprg : (metric-`{m}) LeadsTo (metric-`(lessThan m) Un fixedpoint)";
  17.127 -by (rtac ([LeadsTo_Diff_fixedpoint RS LeadsTo_weaken_R,
  17.128 -	   subset_imp_LeadsTo] MRS LeadsTo_Diff) 1);
  17.129 -by Auto_tac;
  17.130 -qed "LeadsTo_Un_fixedpoint";
  17.131 -
  17.132 -
  17.133 -(*Execution in any state leads to a fixedpoint (i.e. can terminate)*)
  17.134 -Goal "Rprg : UNIV LeadsTo fixedpoint";
  17.135 -by (rtac LessThan_induct 1);
  17.136 -by Auto_tac;
  17.137 -by (rtac LeadsTo_Un_fixedpoint 1);
  17.138 -qed "LeadsTo_fixedpoint";
  17.139 -
  17.140 -Goal "Rprg : UNIV LeadsTo { %v. (init, v) : edges^* }";
  17.141 -by (stac (fixedpoint_invariant_correct RS sym) 1);
  17.142 -by (rtac ([reach_invariant, LeadsTo_fixedpoint] 
  17.143 -	  MRS Always_LeadsTo_weaken) 1); 
  17.144 -by Auto_tac;
  17.145 -qed "LeadsTo_correct";
    18.1 --- a/src/HOL/UNITY/Simple/Reach.thy	Thu Jan 23 10:30:14 2003 +0100
    18.2 +++ b/src/HOL/UNITY/Simple/Reach.thy	Fri Jan 24 14:06:49 2003 +0100
    18.3 @@ -4,14 +4,14 @@
    18.4      Copyright   1998  University of Cambridge
    18.5  
    18.6  Reachability in Directed Graphs.  From Chandy and Misra, section 6.4.
    18.7 +	[this example took only four days!]
    18.8  *)
    18.9  
   18.10 -Reach = FP + SubstAx +
   18.11 +theory Reach = UNITY_Main:
   18.12  
   18.13 -types   vertex
   18.14 -        state = "vertex=>bool"
   18.15 +typedecl vertex
   18.16  
   18.17 -arities vertex :: type
   18.18 +types    state = "vertex=>bool"
   18.19  
   18.20  consts
   18.21    init ::  "vertex"
   18.22 @@ -23,21 +23,142 @@
   18.23    asgt  :: "[vertex,vertex] => (state*state) set"
   18.24      "asgt u v == {(s,s'). s' = s(v:= s u | s v)}"
   18.25  
   18.26 -  Rprg :: state program
   18.27 +  Rprg :: "state program"
   18.28      "Rprg == mk_program ({%v. v=init}, UN (u,v): edges. {asgt u v}, UNIV)"
   18.29  
   18.30 -  reach_invariant :: state set
   18.31 +  reach_invariant :: "state set"
   18.32      "reach_invariant == {s. (ALL v. s v --> (init, v) : edges^*) & s init}"
   18.33  
   18.34 -  fixedpoint :: state set
   18.35 +  fixedpoint :: "state set"
   18.36      "fixedpoint == {s. ALL (u,v): edges. s u --> s v}"
   18.37  
   18.38 -  metric :: state => nat
   18.39 +  metric :: "state => nat"
   18.40      "metric s == card {v. ~ s v}"
   18.41  
   18.42 -rules
   18.43 +
   18.44 +text{**We assume that the set of vertices is finite*}
   18.45 +axioms 
   18.46 +  finite_graph:  "finite (UNIV :: vertex set)"
   18.47 +  
   18.48 +
   18.49 +
   18.50 +
   18.51 +(*TO SIMPDATA.ML??  FOR CLASET??  *)
   18.52 +lemma ifE [elim!]:
   18.53 +    "[| if P then Q else R;     
   18.54 +        [| P;   Q |] ==> S;     
   18.55 +        [| ~ P; R |] ==> S |] ==> S"
   18.56 +by (simp split: split_if_asm) 
   18.57 +
   18.58 +
   18.59 +declare Rprg_def [THEN def_prg_Init, simp]
   18.60 +
   18.61 +declare asgt_def [THEN def_act_simp,simp]
   18.62 +
   18.63 +(*All vertex sets are finite*)
   18.64 +declare finite_subset [OF subset_UNIV finite_graph, iff]
   18.65 +
   18.66 +declare reach_invariant_def [THEN def_set_simp, simp]
   18.67 +
   18.68 +lemma reach_invariant: "Rprg : Always reach_invariant"
   18.69 +apply (rule AlwaysI, force) 
   18.70 +apply (unfold Rprg_def, constrains) 
   18.71 +apply (blast intro: rtrancl_trans)
   18.72 +done
   18.73 +
   18.74 +
   18.75 +(*** Fixedpoint ***)
   18.76 +
   18.77 +(*If it reaches a fixedpoint, it has found a solution*)
   18.78 +lemma fixedpoint_invariant_correct: 
   18.79 +     "fixedpoint Int reach_invariant = { %v. (init, v) : edges^* }"
   18.80 +apply (unfold fixedpoint_def)
   18.81 +apply (rule equalityI)
   18.82 +apply (auto intro!: ext)
   18.83 + prefer 2 apply (blast intro: rtrancl_trans)
   18.84 +apply (erule rtrancl_induct, auto)
   18.85 +done
   18.86 +
   18.87 +lemma lemma1: 
   18.88 +     "FP Rprg <= fixedpoint"
   18.89 +apply (unfold FP_def fixedpoint_def stable_def constrains_def Rprg_def, auto)
   18.90 +apply (drule bspec, assumption)
   18.91 +apply (simp add: Image_singleton image_iff)
   18.92 +apply (drule fun_cong, auto)
   18.93 +done
   18.94 +
   18.95 +lemma lemma2: 
   18.96 +     "fixedpoint <= FP Rprg"
   18.97 +apply (unfold FP_def fixedpoint_def stable_def constrains_def Rprg_def)
   18.98 +apply (auto intro!: ext)
   18.99 +done
  18.100 +
  18.101 +lemma FP_fixedpoint: "FP Rprg = fixedpoint"
  18.102 +by (rule equalityI [OF lemma1 lemma2])
  18.103 +
  18.104  
  18.105 -  (*We assume that the set of vertices is finite*)
  18.106 -  finite_graph "finite (UNIV :: vertex set)"
  18.107 -  
  18.108 +(*If we haven't reached a fixedpoint then there is some edge for which u but
  18.109 +  not v holds.  Progress will be proved via an ENSURES assertion that the
  18.110 +  metric will decrease for each suitable edge.  A union over all edges proves
  18.111 +  a LEADSTO assertion that the metric decreases if we are not at a fixedpoint.
  18.112 +  *)
  18.113 +
  18.114 +lemma Compl_fixedpoint: "- fixedpoint = (UN (u,v): edges. {s. s u & ~ s v})"
  18.115 +apply (simp add: Compl_FP UN_UN_flatten FP_fixedpoint [symmetric] Rprg_def, auto)
  18.116 + apply (rule fun_upd_idem, force)
  18.117 +apply (force intro!: rev_bexI simp add: fun_upd_idem_iff)
  18.118 +done
  18.119 +
  18.120 +lemma Diff_fixedpoint:
  18.121 +     "A - fixedpoint = (UN (u,v): edges. A Int {s. s u & ~ s v})"
  18.122 +apply (simp add: Diff_eq Compl_fixedpoint, blast)
  18.123 +done
  18.124 +
  18.125 +
  18.126 +(*** Progress ***)
  18.127 +
  18.128 +lemma Suc_metric: "~ s x ==> Suc (metric (s(x:=True))) = metric s"
  18.129 +apply (unfold metric_def)
  18.130 +apply (subgoal_tac "{v. ~ (s (x:=True)) v} = {v. ~ s v} - {x}")
  18.131 + prefer 2 apply force
  18.132 +apply (simp add: card_Suc_Diff1)
  18.133 +done
  18.134 +
  18.135 +lemma metric_less [intro!]: "~ s x ==> metric (s(x:=True)) < metric s"
  18.136 +by (erule Suc_metric [THEN subst], blast)
  18.137 +
  18.138 +lemma metric_le: "metric (s(y:=s x | s y)) <= metric s"
  18.139 +apply (case_tac "s x --> s y")
  18.140 +apply (auto intro: less_imp_le simp add: fun_upd_idem)
  18.141 +done
  18.142 +
  18.143 +lemma LeadsTo_Diff_fixedpoint:
  18.144 +     "Rprg : ((metric-`{m}) - fixedpoint) LeadsTo (metric-`(lessThan m))"
  18.145 +apply (simp (no_asm) add: Diff_fixedpoint Rprg_def)
  18.146 +apply (rule LeadsTo_UN, auto)
  18.147 +apply (ensures_tac "asgt a b")
  18.148 + prefer 2 apply blast
  18.149 +apply (simp (no_asm_use) add: not_less_iff_le)
  18.150 +apply (drule metric_le [THEN order_antisym]) 
  18.151 +apply (auto elim: less_not_refl3 [THEN [2] rev_notE])
  18.152 +done
  18.153 +
  18.154 +lemma LeadsTo_Un_fixedpoint:
  18.155 +     "Rprg : (metric-`{m}) LeadsTo (metric-`(lessThan m) Un fixedpoint)"
  18.156 +apply (rule LeadsTo_Diff [OF LeadsTo_Diff_fixedpoint [THEN LeadsTo_weaken_R]
  18.157 +                             subset_imp_LeadsTo], auto)
  18.158 +done
  18.159 +
  18.160 +
  18.161 +(*Execution in any state leads to a fixedpoint (i.e. can terminate)*)
  18.162 +lemma LeadsTo_fixedpoint: "Rprg : UNIV LeadsTo fixedpoint"
  18.163 +apply (rule LessThan_induct, auto)
  18.164 +apply (rule LeadsTo_Un_fixedpoint)
  18.165 +done
  18.166 +
  18.167 +lemma LeadsTo_correct: "Rprg : UNIV LeadsTo { %v. (init, v) : edges^* }"
  18.168 +apply (subst fixedpoint_invariant_correct [symmetric])
  18.169 +apply (rule Always_LeadsTo_weaken [OF reach_invariant LeadsTo_fixedpoint], auto)
  18.170 +done
  18.171 +
  18.172  end
    19.1 --- a/src/HOL/UNITY/Simple/Reachability.ML	Thu Jan 23 10:30:14 2003 +0100
    19.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.3 @@ -1,306 +0,0 @@
    19.4 -(*  Title:      HOL/UNITY/Reachability
    19.5 -    ID:         $Id$
    19.6 -    Author:     Tanja Vos, Cambridge University Computer Laboratory
    19.7 -    Copyright   2000  University of Cambridge
    19.8 -
    19.9 -Reachability in Graphs
   19.10 -
   19.11 -From Chandy and Misra, "Parallel Program Design" (1989), sections 6.2 and 11.3
   19.12 -*)
   19.13 -
   19.14 -bind_thm("E_imp_in_V_L", Graph2 RS conjunct1);
   19.15 -bind_thm("E_imp_in_V_R", Graph2 RS conjunct2);
   19.16 -
   19.17 -Goal "(v,w) : E ==> F : reachable v LeadsTo nmsg_eq 0 (v,w) Int reachable v";
   19.18 -by (rtac (MA7 RS PSP_Stable RS LeadsTo_weaken_L) 1);
   19.19 -by (rtac MA6 3);
   19.20 -by (auto_tac (claset(), simpset() addsimps [E_imp_in_V_L, E_imp_in_V_R]));
   19.21 -qed "lemma2";
   19.22 -
   19.23 -Goal "(v,w) : E ==> F : reachable v LeadsTo reachable w";
   19.24 -by (rtac (MA4 RS Always_LeadsTo_weaken) 1);
   19.25 -by (rtac lemma2 2);
   19.26 -by (auto_tac (claset(), simpset() addsimps [nmsg_eq_def, nmsg_gt_def]));
   19.27 -qed "Induction_base";
   19.28 -
   19.29 -Goal "(v,w) : REACHABLE ==> F : reachable v LeadsTo reachable w";
   19.30 -by (etac REACHABLE.induct 1);
   19.31 -by (rtac subset_imp_LeadsTo 1);
   19.32 -by (Blast_tac 1);
   19.33 -by (blast_tac (claset() addIs [LeadsTo_Trans, Induction_base]) 1);
   19.34 -qed "REACHABLE_LeadsTo_reachable";
   19.35 -
   19.36 -Goal "F : {s. (root,v) : REACHABLE} LeadsTo reachable v";
   19.37 -by (rtac single_LeadsTo_I 1);
   19.38 -by (full_simp_tac (simpset() addsplits [split_if_asm]) 1);
   19.39 -by (rtac (MA1 RS Always_LeadsToI) 1);
   19.40 -by (etac (REACHABLE_LeadsTo_reachable RS LeadsTo_weaken_L) 1);
   19.41 -by Auto_tac;
   19.42 -qed "Detects_part1";
   19.43 -
   19.44 -
   19.45 -Goalw [Detects_def]
   19.46 -     "v : V ==> F : (reachable v) Detects {s. (root,v) : REACHABLE}";
   19.47 -by Auto_tac;
   19.48 -by (blast_tac (claset() addIs [MA2 RS Always_weaken]) 2);
   19.49 -by (rtac (Detects_part1 RS LeadsTo_weaken_L) 1);
   19.50 -by (Blast_tac 1);
   19.51 -qed "Reachability_Detected";
   19.52 -
   19.53 -
   19.54 -Goal "v : V ==> F : UNIV LeadsTo (reachable v <==> {s. (root,v) : REACHABLE})";
   19.55 -by (etac (Reachability_Detected RS Detects_Imp_LeadstoEQ) 1);
   19.56 -qed "LeadsTo_Reachability";
   19.57 -
   19.58 -(* ------------------------------------ *)
   19.59 -
   19.60 -(* Some lemmas about <==> *)
   19.61 -
   19.62 -Goalw [Equality_def]
   19.63 -     "(reachable v <==> {s. (root,v) : REACHABLE}) = \
   19.64 -\     {s. ((s : reachable v) = ((root,v) : REACHABLE))}";
   19.65 -by (Blast_tac 1);
   19.66 -qed "Eq_lemma1";
   19.67 -
   19.68 -
   19.69 -Goalw [Equality_def]
   19.70 -     "(reachable v <==> (if (root,v) : REACHABLE then UNIV else {})) = \
   19.71 -\     {s. ((s : reachable v) = ((root,v) : REACHABLE))}";
   19.72 -by Auto_tac;
   19.73 -qed "Eq_lemma2";
   19.74 -
   19.75 -(* ------------------------------------ *)
   19.76 -
   19.77 -
   19.78 -(* Some lemmas about final (I don't need all of them!)  *)
   19.79 -
   19.80 -Goalw [final_def, Equality_def]
   19.81 -     "(INT v: V. INT w:V. {s. ((s : reachable v) = ((root,v) : REACHABLE)) & \
   19.82 -\                             s : nmsg_eq 0 (v,w)}) \
   19.83 -\     <= final";
   19.84 -by Auto_tac;
   19.85 -by (ftac E_imp_in_V_R 1);
   19.86 -by (ftac E_imp_in_V_L 1);
   19.87 -by (Blast_tac 1);
   19.88 -qed "final_lemma1";
   19.89 -
   19.90 -Goalw [final_def, Equality_def] 
   19.91 - "E~={} \
   19.92 -\ ==> (INT v: V. INT e: E. {s. ((s : reachable v) = ((root,v) : REACHABLE))} \
   19.93 -\                          Int nmsg_eq 0 e)    <=  final";
   19.94 -by (auto_tac (claset(), simpset() addsplits [split_if_asm]));
   19.95 -by (ftac E_imp_in_V_L 1);
   19.96 -by (Blast_tac 1);
   19.97 -qed "final_lemma2";
   19.98 -
   19.99 -Goal "E~={} \
  19.100 -\     ==> (INT v: V. INT e: E. \
  19.101 -\          (reachable v <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 e) \
  19.102 -\         <= final";
  19.103 -by (ftac final_lemma2 1);
  19.104 -by (full_simp_tac (simpset() addsimps [Eq_lemma2]) 1);
  19.105 -qed "final_lemma3";
  19.106 -
  19.107 -
  19.108 -Goal "E~={} \
  19.109 -\     ==> (INT v: V. INT e: E. \
  19.110 -\          {s. ((s : reachable v) = ((root,v) : REACHABLE))} Int nmsg_eq 0 e) \
  19.111 -\         = final";
  19.112 -by (rtac subset_antisym 1);
  19.113 -by (etac final_lemma2 1);
  19.114 -by (rewrite_goals_tac [final_def,Equality_def]);
  19.115 -by (Blast_tac 1); 
  19.116 -qed "final_lemma4";
  19.117 -
  19.118 -Goal "E~={} \
  19.119 -\     ==> (INT v: V. INT e: E. \
  19.120 -\          ((reachable v) <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 e) \
  19.121 -\         = final";
  19.122 -by (ftac final_lemma4 1);
  19.123 -by (full_simp_tac (simpset() addsimps [Eq_lemma2]) 1);
  19.124 -qed "final_lemma5";
  19.125 -
  19.126 -
  19.127 -Goal "(INT v: V. INT w: V. \
  19.128 -\      (reachable v <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 (v,w)) \
  19.129 -\     <= final";
  19.130 -by (simp_tac (simpset() addsimps [Eq_lemma2, Int_def]) 1);
  19.131 -by (rtac final_lemma1 1);
  19.132 -qed "final_lemma6";
  19.133 -
  19.134 -
  19.135 -Goalw [final_def] 
  19.136 -     "final = \
  19.137 -\     (INT v: V. INT w: V. \
  19.138 -\      ((reachable v) <==> {s. (root,v) : REACHABLE}) Int \
  19.139 -\      (-{s. (v,w) : E} Un (nmsg_eq 0 (v,w))))";
  19.140 -by (rtac subset_antisym 1);
  19.141 -by (Blast_tac 1); 
  19.142 -by (auto_tac (claset(), simpset() addsplits [split_if_asm])); 
  19.143 -by (ALLGOALS (blast_tac (claset() addDs [E_imp_in_V_L, E_imp_in_V_R]))); 
  19.144 -qed "final_lemma7"; 
  19.145 -
  19.146 -(* ------------------------------------ *)
  19.147 -
  19.148 -
  19.149 -(* ------------------------------------ *)
  19.150 -
  19.151 -(* Stability theorems *)
  19.152 -
  19.153 -
  19.154 -Goal "[| v : V; (root,v) ~: REACHABLE |] ==> F : Stable (- reachable v)";
  19.155 -by (dtac (MA2 RS AlwaysD) 1);
  19.156 -by Auto_tac;
  19.157 -qed "not_REACHABLE_imp_Stable_not_reachable";
  19.158 -
  19.159 -Goal "v : V ==> F : Stable (reachable v <==> {s. (root,v) : REACHABLE})";
  19.160 -by (simp_tac (simpset() addsimps [Equality_def, Eq_lemma2]) 1);
  19.161 -by (blast_tac (claset() addIs [MA6,not_REACHABLE_imp_Stable_not_reachable]) 1);
  19.162 -qed "Stable_reachable_EQ_R";
  19.163 -
  19.164 -
  19.165 -Goalw [nmsg_gte_def, nmsg_lte_def,nmsg_gt_def, nmsg_eq_def]
  19.166 -     "((nmsg_gte 0 (v,w) Int nmsg_lte (Suc 0) (v,w)) Int (- nmsg_gt 0 (v,w) Un A)) \
  19.167 -\     <= A Un nmsg_eq 0 (v,w)";
  19.168 -by Auto_tac;
  19.169 -qed "lemma4";
  19.170 -
  19.171 -
  19.172 -Goalw [nmsg_gte_def,nmsg_lte_def,nmsg_gt_def, nmsg_eq_def]
  19.173 -     "reachable v Int nmsg_eq 0 (v,w) = \
  19.174 -\     ((nmsg_gte 0 (v,w) Int nmsg_lte (Suc 0) (v,w)) Int \
  19.175 -\      (reachable v Int nmsg_lte 0 (v,w)))";
  19.176 -by Auto_tac;
  19.177 -qed "lemma5";
  19.178 -
  19.179 -Goalw [nmsg_gte_def,nmsg_lte_def,nmsg_gt_def, nmsg_eq_def]
  19.180 -     "- nmsg_gt 0 (v,w) Un reachable v <= nmsg_eq 0 (v,w) Un reachable v";
  19.181 -by Auto_tac;
  19.182 -qed "lemma6";
  19.183 -
  19.184 -Goal "[|v : V; w : V|] ==> F : Always (reachable v Un nmsg_eq 0 (v,w))";
  19.185 -by (rtac ([MA5, MA3] MRS Always_Int_I RS Always_weaken) 1);
  19.186 -by (rtac lemma4 5); 
  19.187 -by Auto_tac;
  19.188 -qed "Always_reachable_OR_nmsg_0";
  19.189 -
  19.190 -Goal "[|v : V; w : V|] ==> F : Stable (reachable v Int nmsg_eq 0 (v,w))";
  19.191 -by (stac lemma5 1);
  19.192 -by (blast_tac (claset() addIs [MA5, Always_imp_Stable RS Stable_Int, MA6b]) 1);
  19.193 -qed "Stable_reachable_AND_nmsg_0";
  19.194 -
  19.195 -Goal "[|v : V; w : V|] ==> F : Stable (nmsg_eq 0 (v,w) Un reachable v)";
  19.196 -by (blast_tac (claset() addSIs [Always_weaken RS Always_imp_Stable,
  19.197 -			       lemma6, MA3]) 1);
  19.198 -qed "Stable_nmsg_0_OR_reachable";
  19.199 -
  19.200 -Goal "[| v : V; w:V; (root,v) ~: REACHABLE |] \
  19.201 -\     ==> F : Stable (- reachable v Int nmsg_eq 0 (v,w))";
  19.202 -by (rtac ([MA2 RS Always_imp_Stable, Stable_nmsg_0_OR_reachable] MRS 
  19.203 -	  Stable_Int RS Stable_eq) 1);
  19.204 -by (Blast_tac 4);
  19.205 -by Auto_tac;
  19.206 -qed "not_REACHABLE_imp_Stable_not_reachable_AND_nmsg_0";
  19.207 -
  19.208 -Goal "[| v : V; w:V |] \
  19.209 -\     ==> F : Stable ((reachable v <==> {s. (root,v) : REACHABLE}) Int \
  19.210 -\                     nmsg_eq 0 (v,w))";
  19.211 -by (asm_simp_tac
  19.212 -    (simpset() addsimps [Equality_def, Eq_lemma2,
  19.213 -			 not_REACHABLE_imp_Stable_not_reachable_AND_nmsg_0,
  19.214 -			 Stable_reachable_AND_nmsg_0]) 1);
  19.215 -qed "Stable_reachable_EQ_R_AND_nmsg_0";
  19.216 -
  19.217 -
  19.218 -(* ------------------------------------ *)
  19.219 -
  19.220 -
  19.221 -(* LeadsTo final predicate (Exercise 11.2 page 274) *)
  19.222 -
  19.223 -Goal "UNIV <= (INT v: V. UNIV)";
  19.224 -by (Blast_tac 1);
  19.225 -val UNIV_lemma = result();
  19.226 -
  19.227 -val UNIV_LeadsTo_completion = 
  19.228 -    [Finite_stable_completion, UNIV_lemma] MRS LeadsTo_weaken_L;
  19.229 -
  19.230 -Goalw [final_def] "E={} ==> F : UNIV LeadsTo final";
  19.231 -by (Asm_full_simp_tac 1);
  19.232 -by (rtac UNIV_LeadsTo_completion 1);
  19.233 -by Safe_tac;
  19.234 -by (etac (simplify (simpset()) LeadsTo_Reachability) 1);
  19.235 -by (dtac Stable_reachable_EQ_R 1);
  19.236 -by (Asm_full_simp_tac 1);
  19.237 -qed "LeadsTo_final_E_empty";
  19.238 -
  19.239 -
  19.240 -Goal "[| v : V; w:V |] \
  19.241 -\  ==> F : UNIV LeadsTo \
  19.242 -\          ((reachable v <==> {s. (root,v): REACHABLE}) Int nmsg_eq 0 (v,w))";
  19.243 -by (rtac (LeadsTo_Reachability RS LeadsTo_Trans) 1);
  19.244 -by (Blast_tac 1);
  19.245 -by (subgoal_tac "F : (reachable v <==> {s. (root,v) : REACHABLE}) Int UNIV LeadsTo (reachable v <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 (v,w)" 1);
  19.246 -by (Asm_full_simp_tac 1);
  19.247 -by (rtac PSP_Stable2 1);
  19.248 -by (rtac MA7 1); 
  19.249 -by (rtac Stable_reachable_EQ_R 3);
  19.250 -by Auto_tac;
  19.251 -qed "Leadsto_reachability_AND_nmsg_0";
  19.252 -
  19.253 -
  19.254 -Goal "E~={} ==> F : UNIV LeadsTo final";
  19.255 -by (rtac ([LeadsTo_weaken_R, UNIV_lemma] MRS LeadsTo_weaken_L) 1);
  19.256 -by (rtac final_lemma6 2);
  19.257 -by (rtac Finite_stable_completion 1);
  19.258 -by (Blast_tac 1); 
  19.259 -by (rtac UNIV_LeadsTo_completion 1);
  19.260 -by (REPEAT
  19.261 -    (blast_tac (claset() addIs [Stable_INT,
  19.262 -				Stable_reachable_EQ_R_AND_nmsg_0,
  19.263 -				Leadsto_reachability_AND_nmsg_0]) 1));
  19.264 -qed "LeadsTo_final_E_NOT_empty";
  19.265 -
  19.266 -
  19.267 -Goal "F : UNIV LeadsTo final";
  19.268 -by (case_tac "E={}" 1);
  19.269 -by (rtac LeadsTo_final_E_NOT_empty 2);
  19.270 -by (rtac LeadsTo_final_E_empty 1);
  19.271 -by Auto_tac;
  19.272 -qed "LeadsTo_final";
  19.273 -
  19.274 -(* ------------------------------------ *)
  19.275 -
  19.276 -(* Stability of final (Exercise 11.2 page 274) *)
  19.277 -
  19.278 -Goalw [final_def] "E={} ==> F : Stable final";
  19.279 -by (Asm_full_simp_tac 1);
  19.280 -by (rtac Stable_INT 1); 
  19.281 -by (dtac Stable_reachable_EQ_R 1);
  19.282 -by (Asm_full_simp_tac 1);
  19.283 -qed "Stable_final_E_empty";
  19.284 -
  19.285 -
  19.286 -Goal "E~={} ==> F : Stable final";
  19.287 -by (stac final_lemma7 1); 
  19.288 -by (rtac Stable_INT 1); 
  19.289 -by (rtac Stable_INT 1); 
  19.290 -by (simp_tac (simpset() addsimps [Eq_lemma2]) 1);
  19.291 -by Safe_tac;
  19.292 -by (rtac Stable_eq 1);
  19.293 -by (subgoal_tac "({s. (s : reachable v) = ((root,v) : REACHABLE)} Int nmsg_eq 0 (v,w)) = \
  19.294 -\                ({s. (s : reachable v) = ((root,v) : REACHABLE)} Int (- UNIV Un nmsg_eq 0 (v,w)))" 2);
  19.295 -by (Blast_tac 2); by (Blast_tac 2);
  19.296 -by (rtac (simplify (simpset() addsimps [Eq_lemma2]) Stable_reachable_EQ_R_AND_nmsg_0) 1);
  19.297 -by (Blast_tac 1);by (Blast_tac 1);
  19.298 -by (rtac Stable_eq 1);
  19.299 -by (subgoal_tac "({s. (s : reachable v) = ((root,v) : REACHABLE)}) = ({s. (s : reachable v) = ((root,v) : REACHABLE)} Int (- {} Un nmsg_eq 0 (v,w)))" 2);
  19.300 -by (Blast_tac 2); by (Blast_tac 2);
  19.301 -by (rtac (simplify (simpset() addsimps [Eq_lemma2]) Stable_reachable_EQ_R) 1);
  19.302 -by Auto_tac;
  19.303 -qed "Stable_final_E_NOT_empty";
  19.304 -
  19.305 -Goal "F : Stable final";
  19.306 -by (case_tac "E={}" 1);
  19.307 -by (blast_tac (claset() addIs [Stable_final_E_NOT_empty]) 2);
  19.308 -by (blast_tac (claset() addIs [Stable_final_E_empty]) 1);
  19.309 -qed "Stable_final";
    20.1 --- a/src/HOL/UNITY/Simple/Reachability.thy	Thu Jan 23 10:30:14 2003 +0100
    20.2 +++ b/src/HOL/UNITY/Simple/Reachability.thy	Fri Jan 24 14:06:49 2003 +0100
    20.3 @@ -8,65 +8,367 @@
    20.4  From Chandy and Misra, "Parallel Program Design" (1989), sections 6.2 and 11.3
    20.5  *)
    20.6  
    20.7 -Reachability = Detects + 
    20.8 +theory Reachability = Detects + Reach:
    20.9  
   20.10  types  edge = "(vertex*vertex)"
   20.11  
   20.12  record state =
   20.13 -  reach :: vertex => bool
   20.14 -  nmsg  :: edge => nat
   20.15 +  reach :: "vertex => bool"
   20.16 +  nmsg  :: "edge => nat"
   20.17  
   20.18 -consts REACHABLE :: edge set
   20.19 -       root :: vertex
   20.20 -       E :: edge set
   20.21 -       V :: vertex set
   20.22 +consts REACHABLE :: "edge set"
   20.23 +       root :: "vertex"
   20.24 +       E :: "edge set"
   20.25 +       V :: "vertex set"
   20.26  
   20.27  inductive "REACHABLE"
   20.28 -  intrs
   20.29 -   base "v : V ==> ((v,v) : REACHABLE)"
   20.30 -   step "((u,v) : REACHABLE) & (v,w) : E ==> ((u,w) : REACHABLE)"
   20.31 +  intros
   20.32 +   base: "v : V ==> ((v,v) : REACHABLE)"
   20.33 +   step: "((u,v) : REACHABLE) & (v,w) : E ==> ((u,w) : REACHABLE)"
   20.34  
   20.35  constdefs
   20.36 -  reachable :: vertex => state set
   20.37 +  reachable :: "vertex => state set"
   20.38    "reachable p == {s. reach s p}"
   20.39  
   20.40 -  nmsg_eq :: nat => edge  => state set
   20.41 +  nmsg_eq :: "nat => edge  => state set"
   20.42    "nmsg_eq k == %e. {s. nmsg s e = k}"
   20.43  
   20.44 -  nmsg_gt :: nat => edge  => state set
   20.45 +  nmsg_gt :: "nat => edge  => state set"
   20.46    "nmsg_gt k  == %e. {s. k < nmsg s e}"
   20.47  
   20.48 -  nmsg_gte :: nat => edge => state set
   20.49 +  nmsg_gte :: "nat => edge => state set"
   20.50    "nmsg_gte k == %e. {s. k <= nmsg s e}"
   20.51  
   20.52 -  nmsg_lte  :: nat => edge => state set
   20.53 +  nmsg_lte  :: "nat => edge => state set"
   20.54    "nmsg_lte k  == %e. {s. nmsg s e <= k}"
   20.55  
   20.56    
   20.57  
   20.58 -  final :: state set
   20.59 +  final :: "state set"
   20.60    "final == (INTER V (%v. reachable v <==> {s. (root, v) : REACHABLE})) Int (INTER E (nmsg_eq 0))"
   20.61  
   20.62 -rules
   20.63 -    Graph1 "root : V"
   20.64 +axioms
   20.65 +
   20.66 +    Graph1: "root : V"
   20.67 +
   20.68 +    Graph2: "(v,w) : E ==> (v : V) & (w : V)"
   20.69 +
   20.70 +    MA1:  "F : Always (reachable root)"
   20.71 +
   20.72 +    MA2:  "v: V ==> F : Always (- reachable v Un {s. ((root,v) : REACHABLE)})"
   20.73 +
   20.74 +    MA3:  "[|v:V;w:V|] ==> F : Always (-(nmsg_gt 0 (v,w)) Un (reachable v))"
   20.75 +
   20.76 +    MA4:  "(v,w) : E ==> 
   20.77 +           F : Always (-(reachable v) Un (nmsg_gt 0 (v,w)) Un (reachable w))"
   20.78 +
   20.79 +    MA5:  "[|v:V; w:V|] 
   20.80 +           ==> F : Always (nmsg_gte 0 (v,w) Int nmsg_lte (Suc 0) (v,w))"
   20.81 +
   20.82 +    MA6:  "[|v:V|] ==> F : Stable (reachable v)"
   20.83 +
   20.84 +    MA6b: "[|v:V;w:W|] ==> F : Stable (reachable v Int nmsg_lte k (v,w))"
   20.85 +
   20.86 +    MA7:  "[|v:V;w:V|] ==> F : UNIV LeadsTo nmsg_eq 0 (v,w)"
   20.87 +
   20.88 +
   20.89 +lemmas E_imp_in_V_L = Graph2 [THEN conjunct1, standard]
   20.90 +lemmas E_imp_in_V_R = Graph2 [THEN conjunct2, standard]
   20.91 +
   20.92 +lemma lemma2:
   20.93 +     "(v,w) : E ==> F : reachable v LeadsTo nmsg_eq 0 (v,w) Int reachable v"
   20.94 +apply (rule MA7 [THEN PSP_Stable, THEN LeadsTo_weaken_L])
   20.95 +apply (rule_tac [3] MA6)
   20.96 +apply (auto simp add: E_imp_in_V_L E_imp_in_V_R)
   20.97 +done
   20.98 +
   20.99 +lemma Induction_base: "(v,w) : E ==> F : reachable v LeadsTo reachable w"
  20.100 +apply (rule MA4 [THEN Always_LeadsTo_weaken])
  20.101 +apply (rule_tac [2] lemma2)
  20.102 +apply (auto simp add: nmsg_eq_def nmsg_gt_def)
  20.103 +done
  20.104 +
  20.105 +lemma REACHABLE_LeadsTo_reachable:
  20.106 +     "(v,w) : REACHABLE ==> F : reachable v LeadsTo reachable w"
  20.107 +apply (erule REACHABLE.induct)
  20.108 +apply (rule subset_imp_LeadsTo, blast)
  20.109 +apply (blast intro: LeadsTo_Trans Induction_base)
  20.110 +done
  20.111 +
  20.112 +lemma Detects_part1: "F : {s. (root,v) : REACHABLE} LeadsTo reachable v"
  20.113 +apply (rule single_LeadsTo_I)
  20.114 +apply (simp split add: split_if_asm)
  20.115 +apply (rule MA1 [THEN Always_LeadsToI])
  20.116 +apply (erule REACHABLE_LeadsTo_reachable [THEN LeadsTo_weaken_L], auto)
  20.117 +done
  20.118 +
  20.119 +
  20.120 +lemma Reachability_Detected: 
  20.121 +     "v : V ==> F : (reachable v) Detects {s. (root,v) : REACHABLE}"
  20.122 +apply (unfold Detects_def, auto)
  20.123 + prefer 2 apply (blast intro: MA2 [THEN Always_weaken])
  20.124 +apply (rule Detects_part1 [THEN LeadsTo_weaken_L], blast)
  20.125 +done
  20.126 +
  20.127 +
  20.128 +lemma LeadsTo_Reachability:
  20.129 +     "v : V ==> F : UNIV LeadsTo (reachable v <==> {s. (root,v) : REACHABLE})"
  20.130 +by (erule Reachability_Detected [THEN Detects_Imp_LeadstoEQ])
  20.131 +
  20.132 +
  20.133 +(* ------------------------------------ *)
  20.134 +
  20.135 +(* Some lemmas about <==> *)
  20.136 +
  20.137 +lemma Eq_lemma1: 
  20.138 +     "(reachable v <==> {s. (root,v) : REACHABLE}) =  
  20.139 +      {s. ((s : reachable v) = ((root,v) : REACHABLE))}"
  20.140 +apply (unfold Equality_def, blast)
  20.141 +done
  20.142 +
  20.143  
  20.144 -    Graph2 "(v,w) : E ==> (v : V) & (w : V)"
  20.145 +lemma Eq_lemma2: 
  20.146 +     "(reachable v <==> (if (root,v) : REACHABLE then UNIV else {})) =  
  20.147 +      {s. ((s : reachable v) = ((root,v) : REACHABLE))}"
  20.148 +apply (unfold Equality_def, auto)
  20.149 +done
  20.150 +
  20.151 +(* ------------------------------------ *)
  20.152 +
  20.153 +
  20.154 +(* Some lemmas about final (I don't need all of them!)  *)
  20.155 +
  20.156 +lemma final_lemma1: 
  20.157 +     "(INT v: V. INT w:V. {s. ((s : reachable v) = ((root,v) : REACHABLE)) &  
  20.158 +                              s : nmsg_eq 0 (v,w)})  
  20.159 +      <= final"
  20.160 +apply (unfold final_def Equality_def, auto)
  20.161 +apply (frule E_imp_in_V_R)
  20.162 +apply (frule E_imp_in_V_L, blast)
  20.163 +done
  20.164 +
  20.165 +lemma final_lemma2: 
  20.166 + "E~={}  
  20.167 +  ==> (INT v: V. INT e: E. {s. ((s : reachable v) = ((root,v) : REACHABLE))}  
  20.168 +                           Int nmsg_eq 0 e)    <=  final"
  20.169 +apply (unfold final_def Equality_def)
  20.170 +apply (auto split add: split_if_asm)
  20.171 +apply (frule E_imp_in_V_L, blast)
  20.172 +done
  20.173 +
  20.174 +lemma final_lemma3:
  20.175 +     "E~={}  
  20.176 +      ==> (INT v: V. INT e: E.  
  20.177 +           (reachable v <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 e)  
  20.178 +          <= final"
  20.179 +apply (frule final_lemma2)
  20.180 +apply (simp (no_asm_use) add: Eq_lemma2)
  20.181 +done
  20.182 +
  20.183  
  20.184 -    MA1  "F : Always (reachable root)"
  20.185 +lemma final_lemma4:
  20.186 +     "E~={}  
  20.187 +      ==> (INT v: V. INT e: E.  
  20.188 +           {s. ((s : reachable v) = ((root,v) : REACHABLE))} Int nmsg_eq 0 e)  
  20.189 +          = final"
  20.190 +apply (rule subset_antisym)
  20.191 +apply (erule final_lemma2)
  20.192 +apply (unfold final_def Equality_def, blast)
  20.193 +done
  20.194 +
  20.195 +lemma final_lemma5:
  20.196 +     "E~={}  
  20.197 +      ==> (INT v: V. INT e: E.  
  20.198 +           ((reachable v) <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 e)  
  20.199 +          = final"
  20.200 +apply (frule final_lemma4)
  20.201 +apply (simp (no_asm_use) add: Eq_lemma2)
  20.202 +done
  20.203 +
  20.204  
  20.205 -    MA2  "[|v:V|] ==> F : Always (- reachable v Un {s. ((root,v) : REACHABLE)})"
  20.206 +lemma final_lemma6:
  20.207 +     "(INT v: V. INT w: V.  
  20.208 +       (reachable v <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 (v,w))  
  20.209 +      <= final"
  20.210 +apply (simp (no_asm) add: Eq_lemma2 Int_def)
  20.211 +apply (rule final_lemma1)
  20.212 +done
  20.213 +
  20.214 +
  20.215 +lemma final_lemma7: 
  20.216 +     "final =  
  20.217 +      (INT v: V. INT w: V.  
  20.218 +       ((reachable v) <==> {s. (root,v) : REACHABLE}) Int  
  20.219 +       (-{s. (v,w) : E} Un (nmsg_eq 0 (v,w))))"
  20.220 +apply (unfold final_def)
  20.221 +apply (rule subset_antisym, blast)
  20.222 +apply (auto split add: split_if_asm)
  20.223 +apply (blast dest: E_imp_in_V_L E_imp_in_V_R)+
  20.224 +done
  20.225 +
  20.226 +(* ------------------------------------ *)
  20.227  
  20.228 -    MA3  "[|v:V;w:V|] ==> F : Always (-(nmsg_gt 0 (v,w)) Un (reachable v))"
  20.229 +
  20.230 +(* ------------------------------------ *)
  20.231 +
  20.232 +(* Stability theorems *)
  20.233 +lemma not_REACHABLE_imp_Stable_not_reachable:
  20.234 +     "[| v : V; (root,v) ~: REACHABLE |] ==> F : Stable (- reachable v)"
  20.235 +apply (drule MA2 [THEN AlwaysD], auto)
  20.236 +done
  20.237 +
  20.238 +lemma Stable_reachable_EQ_R:
  20.239 +     "v : V ==> F : Stable (reachable v <==> {s. (root,v) : REACHABLE})"
  20.240 +apply (simp (no_asm) add: Equality_def Eq_lemma2)
  20.241 +apply (blast intro: MA6 not_REACHABLE_imp_Stable_not_reachable)
  20.242 +done
  20.243 +
  20.244 +
  20.245 +lemma lemma4: 
  20.246 +     "((nmsg_gte 0 (v,w) Int nmsg_lte (Suc 0) (v,w)) Int 
  20.247 +       (- nmsg_gt 0 (v,w) Un A))  
  20.248 +      <= A Un nmsg_eq 0 (v,w)"
  20.249 +apply (unfold nmsg_gte_def nmsg_lte_def nmsg_gt_def nmsg_eq_def, auto)
  20.250 +done
  20.251 +
  20.252 +
  20.253 +lemma lemma5: 
  20.254 +     "reachable v Int nmsg_eq 0 (v,w) =  
  20.255 +      ((nmsg_gte 0 (v,w) Int nmsg_lte (Suc 0) (v,w)) Int  
  20.256 +       (reachable v Int nmsg_lte 0 (v,w)))"
  20.257 +apply (unfold nmsg_gte_def nmsg_lte_def nmsg_gt_def nmsg_eq_def, auto)
  20.258 +done
  20.259 +
  20.260 +lemma lemma6: 
  20.261 +     "- nmsg_gt 0 (v,w) Un reachable v <= nmsg_eq 0 (v,w) Un reachable v"
  20.262 +apply (unfold nmsg_gte_def nmsg_lte_def nmsg_gt_def nmsg_eq_def, auto)
  20.263 +done
  20.264  
  20.265 -    MA4  "[|(v,w) : E|] ==> F : Always (-(reachable v) Un (nmsg_gt 0 (v,w)) Un (reachable w))"
  20.266 +lemma Always_reachable_OR_nmsg_0:
  20.267 +     "[|v : V; w : V|] ==> F : Always (reachable v Un nmsg_eq 0 (v,w))"
  20.268 +apply (rule Always_Int_I [OF MA5 MA3, THEN Always_weaken])
  20.269 +apply (rule_tac [5] lemma4, auto)
  20.270 +done
  20.271 +
  20.272 +lemma Stable_reachable_AND_nmsg_0:
  20.273 +     "[|v : V; w : V|] ==> F : Stable (reachable v Int nmsg_eq 0 (v,w))"
  20.274 +apply (subst lemma5)
  20.275 +apply (blast intro: MA5 Always_imp_Stable [THEN Stable_Int] MA6b)
  20.276 +done
  20.277 +
  20.278 +lemma Stable_nmsg_0_OR_reachable:
  20.279 +     "[|v : V; w : V|] ==> F : Stable (nmsg_eq 0 (v,w) Un reachable v)"
  20.280 +by (blast intro!: Always_weaken [THEN Always_imp_Stable] lemma6 MA3)
  20.281  
  20.282 -    MA5  "[|v:V;w:V|] ==> F : Always (nmsg_gte 0 (v,w) Int nmsg_lte (Suc 0) (v,w))"
  20.283 +lemma not_REACHABLE_imp_Stable_not_reachable_AND_nmsg_0:
  20.284 +     "[| v : V; w:V; (root,v) ~: REACHABLE |]  
  20.285 +      ==> F : Stable (- reachable v Int nmsg_eq 0 (v,w))"
  20.286 +apply (rule Stable_Int [OF MA2 [THEN Always_imp_Stable] 
  20.287 +                           Stable_nmsg_0_OR_reachable, 
  20.288 +            THEN Stable_eq])
  20.289 +   prefer 4 apply blast
  20.290 +apply auto
  20.291 +done
  20.292 +
  20.293 +lemma Stable_reachable_EQ_R_AND_nmsg_0:
  20.294 +     "[| v : V; w:V |]  
  20.295 +      ==> F : Stable ((reachable v <==> {s. (root,v) : REACHABLE}) Int  
  20.296 +                      nmsg_eq 0 (v,w))"
  20.297 +by (simp add: Equality_def Eq_lemma2  Stable_reachable_AND_nmsg_0
  20.298 +              not_REACHABLE_imp_Stable_not_reachable_AND_nmsg_0)
  20.299 +
  20.300 +
  20.301 +
  20.302 +(* ------------------------------------ *)
  20.303 +
  20.304 +
  20.305 +(* LeadsTo final predicate (Exercise 11.2 page 274) *)
  20.306 +
  20.307 +lemma UNIV_lemma: "UNIV <= (INT v: V. UNIV)"
  20.308 +by blast
  20.309  
  20.310 -    MA6  "[|v:V|] ==> F : Stable (reachable v)"
  20.311 +lemmas UNIV_LeadsTo_completion = 
  20.312 +    LeadsTo_weaken_L [OF Finite_stable_completion UNIV_lemma]
  20.313 +
  20.314 +lemma LeadsTo_final_E_empty: "E={} ==> F : UNIV LeadsTo final"
  20.315 +apply (unfold final_def, simp)
  20.316 +apply (rule UNIV_LeadsTo_completion)
  20.317 +  apply safe
  20.318 + apply (erule LeadsTo_Reachability [simplified])
  20.319 +apply (drule Stable_reachable_EQ_R, simp)
  20.320 +done
  20.321 +
  20.322 +
  20.323 +lemma Leadsto_reachability_AND_nmsg_0:
  20.324 +     "[| v : V; w:V |]  
  20.325 +      ==> F : UNIV LeadsTo  
  20.326 +             ((reachable v <==> {s. (root,v): REACHABLE}) Int nmsg_eq 0 (v,w))"
  20.327 +apply (rule LeadsTo_Reachability [THEN LeadsTo_Trans], blast)
  20.328 +apply (subgoal_tac
  20.329 +	 "F : (reachable v <==> {s. (root,v) : REACHABLE}) Int 
  20.330 +              UNIV LeadsTo (reachable v <==> {s. (root,v) : REACHABLE}) Int 
  20.331 +              nmsg_eq 0 (v,w) ")
  20.332 +apply simp
  20.333 +apply (rule PSP_Stable2)
  20.334 +apply (rule MA7)
  20.335 +apply (rule_tac [3] Stable_reachable_EQ_R, auto)
  20.336 +done
  20.337 +
  20.338 +lemma LeadsTo_final_E_NOT_empty: "E~={} ==> F : UNIV LeadsTo final"
  20.339 +apply (rule LeadsTo_weaken_L [OF LeadsTo_weaken_R UNIV_lemma])
  20.340 +apply (rule_tac [2] final_lemma6)
  20.341 +apply (rule Finite_stable_completion)
  20.342 +  apply blast
  20.343 + apply (rule UNIV_LeadsTo_completion)
  20.344 +   apply (blast intro: Stable_INT Stable_reachable_EQ_R_AND_nmsg_0
  20.345 +                    Leadsto_reachability_AND_nmsg_0)+
  20.346 +done
  20.347  
  20.348 -    MA6b "[|v:V;w:W|] ==> F : Stable (reachable v Int nmsg_lte k (v,w))"
  20.349 +lemma LeadsTo_final: "F : UNIV LeadsTo final"
  20.350 +apply (case_tac "E={}")
  20.351 +apply (rule_tac [2] LeadsTo_final_E_NOT_empty)
  20.352 +apply (rule LeadsTo_final_E_empty, auto)
  20.353 +done
  20.354 +
  20.355 +(* ------------------------------------ *)
  20.356 +
  20.357 +(* Stability of final (Exercise 11.2 page 274) *)
  20.358 +
  20.359 +lemma Stable_final_E_empty: "E={} ==> F : Stable final"
  20.360 +apply (unfold final_def, simp)
  20.361 +apply (rule Stable_INT)
  20.362 +apply (drule Stable_reachable_EQ_R, simp)
  20.363 +done
  20.364 +
  20.365  
  20.366 -    MA7  "[|v:V;w:V|] ==> F : UNIV LeadsTo nmsg_eq 0 (v,w)"
  20.367 +lemma Stable_final_E_NOT_empty: "E~={} ==> F : Stable final"
  20.368 +apply (subst final_lemma7)
  20.369 +apply (rule Stable_INT)
  20.370 +apply (rule Stable_INT)
  20.371 +apply (simp (no_asm) add: Eq_lemma2)
  20.372 +apply safe
  20.373 +apply (rule Stable_eq)
  20.374 +apply (subgoal_tac [2] "({s. (s : reachable v) = ((root,v) : REACHABLE) } Int nmsg_eq 0 (v,w)) = ({s. (s : reachable v) = ( (root,v) : REACHABLE) } Int (- UNIV Un nmsg_eq 0 (v,w))) ")
  20.375 +prefer 2 apply blast 
  20.376 +prefer 2 apply blast 
  20.377 +apply (rule Stable_reachable_EQ_R_AND_nmsg_0
  20.378 +            [simplified Eq_lemma2 Collect_const])
  20.379 +apply (blast, blast)
  20.380 +apply (rule Stable_eq)
  20.381 + apply (rule Stable_reachable_EQ_R [simplified Eq_lemma2 Collect_const])
  20.382 + apply simp
  20.383 +apply (subgoal_tac 
  20.384 +        "({s. (s : reachable v) = ((root,v) : REACHABLE) }) = 
  20.385 +         ({s. (s : reachable v) = ( (root,v) : REACHABLE) } Int
  20.386 +              (- {} Un nmsg_eq 0 (v,w)))")
  20.387 +apply blast+
  20.388 +done
  20.389 +
  20.390 +lemma Stable_final: "F : Stable final"
  20.391 +apply (case_tac "E={}")
  20.392 +prefer 2 apply (blast intro: Stable_final_E_NOT_empty)
  20.393 +apply (blast intro: Stable_final_E_empty)
  20.394 +done
  20.395  
  20.396  end
  20.397  
    21.1 --- a/src/HOL/UNITY/Simple/Token.ML	Thu Jan 23 10:30:14 2003 +0100
    21.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.3 @@ -1,101 +0,0 @@
    21.4 -(*  Title:      HOL/UNITY/Token
    21.5 -    ID:         $Id$
    21.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    21.7 -    Copyright   1998  University of Cambridge
    21.8 -
    21.9 -The Token Ring.
   21.10 -
   21.11 -From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.
   21.12 -*)
   21.13 -
   21.14 -val Token_defs = [HasTok_def, H_def, E_def, T_def];
   21.15 -
   21.16 -Goalw [HasTok_def] "[| s: HasTok i; s: HasTok j |] ==> i=j";
   21.17 -by Auto_tac;
   21.18 -qed "HasToK_partition";
   21.19 -
   21.20 -Goalw Token_defs "(s ~: E i) = (s : H i | s : T i)";
   21.21 -by (Simp_tac 1);
   21.22 -by (case_tac "proc s i" 1);
   21.23 -by Auto_tac;
   21.24 -qed "not_E_eq";
   21.25 -
   21.26 -Open_locale "Token";
   21.27 -
   21.28 -val TR2 = thm "TR2";
   21.29 -val TR3 = thm "TR3";
   21.30 -val TR4 = thm "TR4";
   21.31 -val TR5 = thm "TR5";
   21.32 -val TR6 = thm "TR6";
   21.33 -val TR7 = thm "TR7";
   21.34 -val nodeOrder_def = thm "nodeOrder_def";
   21.35 -val next_def = thm "next_def";
   21.36 -
   21.37 -AddIffs [thm "N_positive"];
   21.38 -
   21.39 -Goalw [stable_def] "F : stable (-(E i) Un (HasTok i))";
   21.40 -by (rtac constrains_weaken 1);
   21.41 -by (rtac ([[TR2, TR4] MRS constrains_Un, TR5] MRS constrains_Un) 1);
   21.42 -by (auto_tac (claset(), simpset() addsimps [not_E_eq]));
   21.43 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [H_def, E_def, T_def])));
   21.44 -qed "token_stable";
   21.45 -
   21.46 -
   21.47 -(*** Progress under weak fairness ***)
   21.48 -
   21.49 -Goalw [nodeOrder_def] "wf(nodeOrder j)";
   21.50 -by (rtac (wf_less_than RS wf_inv_image RS wf_subset) 1);
   21.51 -by (Blast_tac 1);
   21.52 -qed"wf_nodeOrder";
   21.53 -
   21.54 -Goalw [nodeOrder_def, next_def, inv_image_def]
   21.55 -    "[| i<N; j<N |] ==> ((next i, i) : nodeOrder j) = (i ~= j)";
   21.56 -by (auto_tac (claset(), simpset() addsimps [mod_Suc, mod_geq]));
   21.57 -by (auto_tac (claset(), 
   21.58 -              simpset() addsplits [nat_diff_split]
   21.59 -                        addsimps [linorder_neq_iff, mod_geq]));
   21.60 -qed "nodeOrder_eq";
   21.61 -
   21.62 -(*From "A Logic for Concurrent Programming", but not used in Chapter 4.
   21.63 -  Note the use of case_tac.  Reasoning about leadsTo takes practice!*)
   21.64 -Goal "[| i<N; j<N |] ==>   \
   21.65 -\     F : (HasTok i) leadsTo ({s. (token s, i) : nodeOrder j} Un HasTok j)";
   21.66 -by (case_tac "i=j" 1);
   21.67 -by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
   21.68 -by (rtac (TR7 RS leadsTo_weaken_R) 1);
   21.69 -by (auto_tac (claset(), simpset() addsimps [HasTok_def, nodeOrder_eq]));
   21.70 -qed "TR7_nodeOrder";
   21.71 -
   21.72 -
   21.73 -(*Chapter 4 variant, the one actually used below.*)
   21.74 -Goal "[| i<N; j<N; i~=j |]    \
   21.75 -\     ==> F : (HasTok i) leadsTo {s. (token s, i) : nodeOrder j}";
   21.76 -by (rtac (TR7 RS leadsTo_weaken_R) 1);
   21.77 -by (auto_tac (claset(), simpset() addsimps [HasTok_def, nodeOrder_eq]));
   21.78 -qed "TR7_aux";
   21.79 -
   21.80 -Goal "({s. token s < N} Int token -` {m}) = (if m<N then token -` {m} else {})";
   21.81 -by Auto_tac;
   21.82 -val token_lemma = result();
   21.83 -
   21.84 -
   21.85 -(*Misra's TR9: the token reaches an arbitrary node*)
   21.86 -Goal "j<N ==> F : {s. token s < N} leadsTo (HasTok j)";
   21.87 -by (rtac leadsTo_weaken_R 1);
   21.88 -by (res_inst_tac [("I", "-{j}"), ("f", "token"), ("B", "{}")]
   21.89 -     (wf_nodeOrder RS bounded_induct) 1);
   21.90 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [token_lemma, vimage_Diff,
   21.91 -						HasTok_def])));
   21.92 -by (Blast_tac 2);
   21.93 -by (Clarify_tac 1);
   21.94 -by (rtac (TR7_aux RS leadsTo_weaken) 1);
   21.95 -by (auto_tac (claset(), simpset() addsimps [HasTok_def, nodeOrder_def]));
   21.96 -qed "leadsTo_j";
   21.97 -
   21.98 -(*Misra's TR8: a hungry process eventually eats*)
   21.99 -Goal "j<N ==> F : ({s. token s < N} Int H j) leadsTo (E j)";
  21.100 -by (rtac (leadsTo_cancel1 RS leadsTo_Un_duplicate) 1);
  21.101 -by (rtac TR6 2);
  21.102 -by (rtac ([leadsTo_j, TR3] MRS psp RS leadsTo_weaken) 1);
  21.103 -by (ALLGOALS Blast_tac);
  21.104 -qed "token_progress";
    22.1 --- a/src/HOL/UNITY/Simple/Token.thy	Thu Jan 23 10:30:14 2003 +0100
    22.2 +++ b/src/HOL/UNITY/Simple/Token.thy	Fri Jan 24 14:06:49 2003 +0100
    22.3 @@ -9,58 +9,120 @@
    22.4  *)
    22.5  
    22.6  
    22.7 -Token = WFair + 
    22.8 +theory Token = WFair:
    22.9  
   22.10  (*process states*)
   22.11  datatype pstate = Hungry | Eating | Thinking
   22.12  
   22.13  record state =
   22.14 -  token :: nat
   22.15 -  proc  :: nat => pstate
   22.16 +  token :: "nat"
   22.17 +  proc  :: "nat => pstate"
   22.18  
   22.19  
   22.20  constdefs
   22.21 -  HasTok :: nat => state set
   22.22 +  HasTok :: "nat => state set"
   22.23      "HasTok i == {s. token s = i}"
   22.24  
   22.25 -  H :: nat => state set
   22.26 +  H :: "nat => state set"
   22.27      "H i == {s. proc s i = Hungry}"
   22.28  
   22.29 -  E :: nat => state set
   22.30 +  E :: "nat => state set"
   22.31      "E i == {s. proc s i = Eating}"
   22.32  
   22.33 -  T :: nat => state set
   22.34 +  T :: "nat => state set"
   22.35      "T i == {s. proc s i = Thinking}"
   22.36  
   22.37  
   22.38  locale Token =
   22.39 -  fixes
   22.40 -    N         :: nat	 (*number of nodes in the ring*)
   22.41 -    F         :: state program
   22.42 -    nodeOrder :: "nat => (nat*nat)set"
   22.43 -    next      :: nat => nat
   22.44 +  fixes N and F and nodeOrder and "next"   
   22.45 +  defines nodeOrder_def:
   22.46 +       "nodeOrder j == (inv_image less_than (%i. ((j+N)-i) mod N))  Int
   22.47 +	 	       (lessThan N <*> lessThan N)"
   22.48 +      and next_def:
   22.49 +       "next i == (Suc i) mod N"
   22.50 +  assumes N_positive [iff]: "0<N"
   22.51 +      and TR2:  "F : (T i) co (T i Un H i)"
   22.52 +      and TR3:  "F : (H i) co (H i Un E i)"
   22.53 +      and TR4:  "F : (H i - HasTok i) co (H i)"
   22.54 +      and TR5:  "F : (HasTok i) co (HasTok i Un -(E i))"
   22.55 +      and TR6:  "F : (H i Int HasTok i) leadsTo (E i)"
   22.56 +      and TR7:  "F : (HasTok i) leadsTo (HasTok (next i))"
   22.57 +
   22.58 +
   22.59 +lemma HasToK_partition: "[| s: HasTok i; s: HasTok j |] ==> i=j"
   22.60 +by (unfold HasTok_def, auto)
   22.61  
   22.62 -  assumes
   22.63 -    N_positive "0<N"
   22.64 +lemma not_E_eq: "(s ~: E i) = (s : H i | s : T i)"
   22.65 +apply (simp add: H_def E_def T_def)
   22.66 +apply (case_tac "proc s i", auto)
   22.67 +done
   22.68  
   22.69 -    TR2  "F : (T i) co (T i Un H i)"
   22.70 +lemma (in Token) token_stable: "F : stable (-(E i) Un (HasTok i))"
   22.71 +apply (unfold stable_def)
   22.72 +apply (rule constrains_weaken)
   22.73 +apply (rule constrains_Un [OF constrains_Un [OF TR2 TR4] TR5])
   22.74 +apply (auto simp add: not_E_eq)
   22.75 +apply (simp_all add: H_def E_def T_def)
   22.76 +done
   22.77  
   22.78 -    TR3  "F : (H i) co (H i Un E i)"
   22.79 +
   22.80 +(*** Progress under weak fairness ***)
   22.81 +
   22.82 +lemma (in Token) wf_nodeOrder: "wf(nodeOrder j)"
   22.83 +apply (unfold nodeOrder_def)
   22.84 +apply (rule wf_less_than [THEN wf_inv_image, THEN wf_subset], blast)
   22.85 +done
   22.86  
   22.87 -    TR4  "F : (H i - HasTok i) co (H i)"
   22.88 -
   22.89 -    TR5  "F : (HasTok i) co (HasTok i Un -(E i))"
   22.90 +lemma (in Token) nodeOrder_eq: 
   22.91 +     "[| i<N; j<N |] ==> ((next i, i) : nodeOrder j) = (i ~= j)"
   22.92 +apply (unfold nodeOrder_def next_def inv_image_def)
   22.93 +apply (auto simp add: mod_Suc mod_geq)
   22.94 +apply (auto split add: nat_diff_split simp add: linorder_neq_iff mod_geq)
   22.95 +done
   22.96  
   22.97 -    TR6  "F : (H i Int HasTok i) leadsTo (E i)"
   22.98 +(*From "A Logic for Concurrent Programming", but not used in Chapter 4.
   22.99 +  Note the use of case_tac.  Reasoning about leadsTo takes practice!*)
  22.100 +lemma (in Token) TR7_nodeOrder:
  22.101 +     "[| i<N; j<N |] ==>    
  22.102 +      F : (HasTok i) leadsTo ({s. (token s, i) : nodeOrder j} Un HasTok j)"
  22.103 +apply (case_tac "i=j")
  22.104 +apply (blast intro: subset_imp_leadsTo)
  22.105 +apply (rule TR7 [THEN leadsTo_weaken_R])
  22.106 +apply (auto simp add: HasTok_def nodeOrder_eq)
  22.107 +done
  22.108  
  22.109 -    TR7  "F : (HasTok i) leadsTo (HasTok (next i))"
  22.110 +
  22.111 +(*Chapter 4 variant, the one actually used below.*)
  22.112 +lemma (in Token) TR7_aux: "[| i<N; j<N; i~=j |]     
  22.113 +      ==> F : (HasTok i) leadsTo {s. (token s, i) : nodeOrder j}"
  22.114 +apply (rule TR7 [THEN leadsTo_weaken_R])
  22.115 +apply (auto simp add: HasTok_def nodeOrder_eq)
  22.116 +done
  22.117  
  22.118 -  defines
  22.119 -    nodeOrder_def
  22.120 -      "nodeOrder j == (inv_image less_than (%i. ((j+N)-i) mod N))  Int
  22.121 -		      (lessThan N <*> lessThan N)"
  22.122 +lemma (in Token) token_lemma:
  22.123 +     "({s. token s < N} Int token -` {m}) = (if m<N then token -` {m} else {})"
  22.124 +by auto
  22.125 +
  22.126  
  22.127 -    next_def
  22.128 -      "next i == (Suc i) mod N"
  22.129 +(*Misra's TR9: the token reaches an arbitrary node*)
  22.130 +lemma  (in Token) leadsTo_j: "j<N ==> F : {s. token s < N} leadsTo (HasTok j)"
  22.131 +apply (rule leadsTo_weaken_R)
  22.132 +apply (rule_tac I = "-{j}" and f = token and B = "{}" 
  22.133 +       in wf_nodeOrder [THEN bounded_induct])
  22.134 +apply (simp_all (no_asm_simp) add: token_lemma vimage_Diff HasTok_def)
  22.135 + prefer 2 apply blast
  22.136 +apply clarify
  22.137 +apply (rule TR7_aux [THEN leadsTo_weaken])
  22.138 +apply (auto simp add: HasTok_def nodeOrder_def)
  22.139 +done
  22.140 +
  22.141 +(*Misra's TR8: a hungry process eventually eats*)
  22.142 +lemma (in Token) token_progress:
  22.143 +     "j<N ==> F : ({s. token s < N} Int H j) leadsTo (E j)"
  22.144 +apply (rule leadsTo_cancel1 [THEN leadsTo_Un_duplicate])
  22.145 +apply (rule_tac [2] TR6)
  22.146 +apply (rule psp [OF leadsTo_j TR3, THEN leadsTo_weaken], blast+)
  22.147 +done
  22.148 +
  22.149  
  22.150  end