converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
authorpaulson
Thu Jul 03 12:56:48 2003 +0200 (2003-07-03)
changeset 1408861bd46feb919
parent 14087 cb07c3948668
child 14089 7b34f58b1b81
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
src/HOL/IsaMakefile
src/HOL/UNITY/Comp/Counter.ML
src/HOL/UNITY/Comp/Counter.thy
src/HOL/UNITY/Comp/Counterc.ML
src/HOL/UNITY/Comp/Counterc.thy
src/HOL/UNITY/Comp/Priority.thy
src/HOL/UNITY/Comp/PriorityAux.ML
src/HOL/UNITY/Comp/PriorityAux.thy
     1.1 --- a/src/HOL/IsaMakefile	Thu Jul 03 10:37:25 2003 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Thu Jul 03 12:56:48 2003 +0200
     1.3 @@ -391,9 +391,8 @@
     1.4    UNITY/Comp/Alloc.ML UNITY/Comp/Alloc.thy \
     1.5    UNITY/Comp/AllocBase.thy \
     1.6    UNITY/Comp/Client.ML UNITY/Comp/Client.thy \
     1.7 -  UNITY/Comp/Counter.ML UNITY/Comp/Counter.thy \
     1.8 -  UNITY/Comp/Counterc.ML UNITY/Comp/Counterc.thy UNITY/Comp/Handshake.thy \
     1.9 -  UNITY/Comp/PriorityAux.ML UNITY/Comp/PriorityAux.thy \
    1.10 +  UNITY/Comp/Counter.thy UNITY/Comp/Counterc.thy UNITY/Comp/Handshake.thy \
    1.11 +  UNITY/Comp/PriorityAux.thy \
    1.12    UNITY/Comp/Priority.thy UNITY/Comp/Progress.thy \
    1.13    UNITY/Comp/TimerArray.thy
    1.14  	@$(ISATOOL) usedir $(OUT)/HOL UNITY
     2.1 --- a/src/HOL/UNITY/Comp/Counter.ML	Thu Jul 03 10:37:25 2003 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,113 +0,0 @@
     2.4 -(*  Title:      HOL/UNITY/Counter
     2.5 -    ID:         $Id$
     2.6 -    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     2.7 -    Copyright   2001  University of Cambridge
     2.8 -
     2.9 -A family of similar counters, version close to the original. 
    2.10 -
    2.11 -From Charpentier and Chandy,
    2.12 -Examples of Program Composition Illustrating the Use of Universal Properties
    2.13 -   In J. Rolim (editor), Parallel and Distributed Processing,
    2.14 -   Spriner LNCS 1586 (1999), pages 1215-1227.
    2.15 -*)
    2.16 -
    2.17 -Addsimps [Component_def RS def_prg_Init, simp_of_act a_def];
    2.18 -
    2.19 -(* Theorems about sum and sumj *)
    2.20 -Goal "\\<forall>n. I<n --> sum I (s(c n := x)) = sum I s";
    2.21 -by (induct_tac "I" 1);
    2.22 -by Auto_tac;
    2.23 -qed_spec_mp "sum_upd_gt";
    2.24 -
    2.25 -
    2.26 -Goal "sum I (s(c I := x)) = sum I s";
    2.27 -by (induct_tac "I" 1);
    2.28 -by Auto_tac;
    2.29 -by (simp_tac (simpset() 
    2.30 -    addsimps [rewrite_rule [fun_upd_def] sum_upd_gt]) 1);
    2.31 -qed "sum_upd_eq";
    2.32 -
    2.33 -Goal "sum I (s(C := x)) = sum I s";
    2.34 -by (induct_tac "I" 1);
    2.35 -by Auto_tac;
    2.36 -qed "sum_upd_C";
    2.37 -
    2.38 -Goal "sumj I i (s(c i := x)) = sumj I i s";
    2.39 -by (induct_tac "I" 1);
    2.40 -by Auto_tac;
    2.41 -by (simp_tac (simpset() addsimps 
    2.42 -    [rewrite_rule [fun_upd_def] sum_upd_eq]) 1);
    2.43 -qed "sumj_upd_ci";
    2.44 -
    2.45 -Goal "sumj I i (s(C := x)) = sumj I i s";
    2.46 -by (induct_tac "I" 1);
    2.47 -by Auto_tac;
    2.48 -by (simp_tac (simpset() 
    2.49 -    addsimps [rewrite_rule [fun_upd_def] sum_upd_C]) 1);
    2.50 -qed "sumj_upd_C";
    2.51 -
    2.52 -Goal "\\<forall>i. I<i--> (sumj I i s = sum I s)";
    2.53 -by (induct_tac "I" 1);
    2.54 -by Auto_tac;
    2.55 -qed_spec_mp  "sumj_sum_gt";
    2.56 -
    2.57 -Goal "(sumj I I s = sum I s)";
    2.58 -by (induct_tac "I" 1);
    2.59 -by Auto_tac;
    2.60 -by (simp_tac (simpset() addsimps [sumj_sum_gt]) 1);
    2.61 -qed "sumj_sum_eq";
    2.62 -
    2.63 -Goal "\\<forall>i. i<I-->(sum I s = s (c i) +  sumj I i s)";
    2.64 -by (induct_tac "I" 1);
    2.65 -by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff, sumj_sum_eq]));  
    2.66 -qed_spec_mp "sum_sumj";
    2.67 -
    2.68 -(* Correctness proofs for Components *)
    2.69 -(* p2 and p3 proofs *)
    2.70 -Goal "Component i \\<in> stable {s. s C = s (c i) + k}";
    2.71 -by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
    2.72 -by (constrains_tac 1);
    2.73 -qed "p2";
    2.74 -
    2.75 -Goal "Component i \\<in> stable {s. \\<forall>v. v~=c i & v~=C --> s v = k v}";
    2.76 -by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
    2.77 -by (constrains_tac 1);
    2.78 -qed "p3";
    2.79 -
    2.80 -
    2.81 -Goal 
    2.82 -"(\\<forall>k. Component i \\<in> stable ({s. s C = s (c i) + sumj I i k} \
    2.83 -\                  \\<inter> {s. \\<forall>v. v~=c i & v~=C --> s v = k v})) \
    2.84 -\  = (Component i \\<in> stable {s. s C = s (c i) + sumj I i s})";
    2.85 -by (asm_full_simp_tac (simpset() addsimps [Component_def, mk_total_program_def]) 1);
    2.86 -by (auto_tac (claset(), simpset() 
    2.87 -     addsimps [constrains_def, stable_def, sumj_upd_C, sumj_upd_ci]));
    2.88 -qed "p2_p3_lemma1";
    2.89 -
    2.90 -Goal 
    2.91 -"\\<forall>k. Component i \\<in> stable ({s. s C = s (c i) + sumj I i k} Int \
    2.92 -\                             {s. \\<forall>v. v~=c i & v~=C --> s v = k v})";
    2.93 -by (blast_tac (claset() addIs [[p2, p3] MRS stable_Int]) 1);
    2.94 -qed "p2_p3_lemma2";
    2.95 -
    2.96 -
    2.97 -Goal 
    2.98 -"Component i \\<in> stable {s.  s C = s (c i) + sumj I i s}";
    2.99 -by (auto_tac (claset() addSIs [p2_p3_lemma2],
   2.100 -              simpset() addsimps [p2_p3_lemma1 RS sym]));
   2.101 -qed "p2_p3";
   2.102 -
   2.103 -(* Compositional Proof *)
   2.104 -
   2.105 -Goal "(\\<forall>i. i < I --> s (c i) = 0) --> sum I s = 0";
   2.106 -by (induct_tac "I" 1);
   2.107 -by Auto_tac;
   2.108 -qed "sum_0'";
   2.109 -val sum0_lemma =  (sum_0' RS mp) RS sym;
   2.110 -
   2.111 -(* I could'nt be empty *)
   2.112 -Goalw [invariant_def] 
   2.113 -"!!I. 0<I ==> (\\<Squnion>i \\<in> {i. i<I}. Component i) \\<in> invariant {s. s C = sum I s}";
   2.114 -by (simp_tac (simpset() addsimps [JN_stable, sum_sumj]) 1);
   2.115 -by (force_tac (claset() addIs [p2_p3, sum0_lemma RS sym], simpset()) 1);
   2.116 -qed "safety";
     3.1 --- a/src/HOL/UNITY/Comp/Counter.thy	Thu Jul 03 10:37:25 2003 +0200
     3.2 +++ b/src/HOL/UNITY/Comp/Counter.thy	Thu Jul 03 12:56:48 2003 +0200
     3.3 @@ -11,11 +11,11 @@
     3.4     Spriner LNCS 1586 (1999), pages 1215-1227.
     3.5  *)
     3.6  
     3.7 -Counter = UNITY_Main +
     3.8 +theory Counter = UNITY_Main:
     3.9  
    3.10  (* Variables are names *)
    3.11  datatype name = C | c nat
    3.12 -types state = name=>int
    3.13 +types state = "name=>int"
    3.14  
    3.15  consts  
    3.16    sum  :: "[nat,state]=>int"
    3.17 @@ -38,6 +38,99 @@
    3.18    Component :: "nat => state program"
    3.19    "Component i ==
    3.20      mk_total_program({s. s C = 0 & s (c i) = 0}, {a i},
    3.21 -	             \\<Union>G \\<in> preserves (%s. s (c i)). Acts G)"
    3.22 +	             \<Union>G \<in> preserves (%s. s (c i)). Acts G)"
    3.23 +
    3.24 +
    3.25 +
    3.26 +declare Component_def [THEN def_prg_Init, simp]
    3.27 +declare a_def [THEN def_act_simp, simp]
    3.28 +
    3.29 +(* Theorems about sum and sumj *)
    3.30 +lemma sum_upd_gt [rule_format (no_asm)]: "\<forall>n. I<n --> sum I (s(c n := x)) = sum I s"
    3.31 +apply (induct_tac "I")
    3.32 +apply auto
    3.33 +done
    3.34 +
    3.35 +
    3.36 +lemma sum_upd_eq: "sum I (s(c I := x)) = sum I s"
    3.37 +apply (induct_tac "I")
    3.38 +apply (auto simp add: sum_upd_gt [unfolded fun_upd_def])
    3.39 +done
    3.40 +
    3.41 +lemma sum_upd_C: "sum I (s(C := x)) = sum I s"
    3.42 +apply (induct_tac "I")
    3.43 +apply auto
    3.44 +done
    3.45 +
    3.46 +lemma sumj_upd_ci: "sumj I i (s(c i := x)) = sumj I i s"
    3.47 +apply (induct_tac "I")
    3.48 +apply (auto simp add: sum_upd_eq [unfolded fun_upd_def])
    3.49 +done
    3.50 +
    3.51 +lemma sumj_upd_C: "sumj I i (s(C := x)) = sumj I i s"
    3.52 +apply (induct_tac "I")
    3.53 +apply (auto simp add: sum_upd_C [unfolded fun_upd_def])
    3.54 +done
    3.55 +
    3.56 +lemma sumj_sum_gt [rule_format (no_asm)]: "\<forall>i. I<i--> (sumj I i s = sum I s)"
    3.57 +apply (induct_tac "I")
    3.58 +apply auto
    3.59 +done
    3.60 +
    3.61 +lemma sumj_sum_eq: "(sumj I I s = sum I s)"
    3.62 +apply (induct_tac "I")
    3.63 +apply auto
    3.64 +apply (simp (no_asm) add: sumj_sum_gt)
    3.65 +done
    3.66 +
    3.67 +lemma sum_sumj [rule_format (no_asm)]: "\<forall>i. i<I-->(sum I s = s (c i) +  sumj I i s)"
    3.68 +apply (induct_tac "I")
    3.69 +apply (auto simp add: linorder_neq_iff sumj_sum_eq)
    3.70 +done
    3.71 +
    3.72 +(* Correctness proofs for Components *)
    3.73 +(* p2 and p3 proofs *)
    3.74 +lemma p2: "Component i \<in> stable {s. s C = s (c i) + k}"
    3.75 +apply (simp add: Component_def)
    3.76 +apply constrains
    3.77 +done
    3.78 +
    3.79 +lemma p3: "Component i \<in> stable {s. \<forall>v. v~=c i & v~=C --> s v = k v}"
    3.80 +apply (simp add: Component_def)
    3.81 +apply constrains
    3.82 +done
    3.83 +
    3.84 +
    3.85 +lemma p2_p3_lemma1: 
    3.86 +"(\<forall>k. Component i \<in> stable ({s. s C = s (c i) + sumj I i k}  
    3.87 +                   \<inter> {s. \<forall>v. v~=c i & v~=C --> s v = k v}))  
    3.88 +   = (Component i \<in> stable {s. s C = s (c i) + sumj I i s})"
    3.89 +apply (simp add: Component_def mk_total_program_def)
    3.90 +apply (auto simp add: constrains_def stable_def sumj_upd_C sumj_upd_ci)
    3.91 +done
    3.92 +
    3.93 +lemma p2_p3_lemma2: 
    3.94 +"\<forall>k. Component i \<in> stable ({s. s C = s (c i) + sumj I i k} Int  
    3.95 +                            {s. \<forall>v. v~=c i & v~=C --> s v = k v})"
    3.96 +by (blast intro: stable_Int [OF p2 p3])
    3.97 +
    3.98 +lemma p2_p3: "Component i \<in> stable {s.  s C = s (c i) + sumj I i s}"
    3.99 +apply (auto intro!: p2_p3_lemma2 simp add: p2_p3_lemma1 [symmetric])
   3.100 +done
   3.101 +
   3.102 +(* Compositional Proof *)
   3.103 +
   3.104 +lemma sum_0' [rule_format]: "(\<forall>i. i < I --> s (c i) = 0) --> sum I s = 0"
   3.105 +apply (induct_tac "I")
   3.106 +apply auto
   3.107 +done
   3.108 +
   3.109 +(* I could'nt be empty *)
   3.110 +lemma safety: 
   3.111 +"!!I. 0<I ==> (\<Squnion>i \<in> {i. i<I}. Component i) \<in> invariant {s. s C = sum I s}"
   3.112 +apply (unfold invariant_def)
   3.113 +apply (simp (no_asm) add: JN_stable sum_sumj)
   3.114 +apply (force intro: p2_p3 sum_0')
   3.115 +done
   3.116  
   3.117  end  
     4.1 --- a/src/HOL/UNITY/Comp/Counterc.ML	Thu Jul 03 10:37:25 2003 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,126 +0,0 @@
     4.4 -(*  Title:      HOL/UNITY/Counterc
     4.5 -    ID:         $Id$
     4.6 -    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     4.7 -    Copyright   2001  University of Cambridge
     4.8 -
     4.9 -A family of similar counters, version with a full use of "compatibility "
    4.10 -
    4.11 -From Charpentier and Chandy,
    4.12 -Examples of Program Composition Illustrating the Use of Universal Properties
    4.13 -   In J. Rolim (editor), Parallel and Distributed Processing,
    4.14 -   Spriner LNCS 1586 (1999), pages 1215-1227.
    4.15 -*)
    4.16 -
    4.17 -Addsimps [Component_def RS def_prg_Init, 
    4.18 -          Component_def RS def_prg_AllowedActs,
    4.19 -          simp_of_act a_def];
    4.20 -
    4.21 -(* Theorems about sum and sumj *)
    4.22 -Goal "\\<forall>i. I<i--> (sum I s = sumj I i s)";
    4.23 -by (induct_tac "I" 1);
    4.24 -by Auto_tac;
    4.25 -qed_spec_mp  "sum_sumj_eq1";
    4.26 -
    4.27 -Goal "i<I --> sum I s  = c s i + sumj I i s";
    4.28 -by (induct_tac "I" 1);
    4.29 -by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff, sum_sumj_eq1]));
    4.30 -qed_spec_mp "sum_sumj_eq2";
    4.31 -
    4.32 -Goal "(\\<forall>i. i<I --> c s' i = c s i) --> (sum I s' = sum I s)";
    4.33 -by (induct_tac "I" 1 THEN Auto_tac);
    4.34 -qed_spec_mp "sum_ext";
    4.35 -
    4.36 -Goal "(\\<forall>j. j<I & j~=i --> c s' j =  c s j) --> (sumj I i s' = sumj I i s)";
    4.37 -by (induct_tac "I" 1);
    4.38 -by Safe_tac;
    4.39 -by (auto_tac (claset() addSIs [sum_ext], simpset()));
    4.40 -qed_spec_mp "sumj_ext";
    4.41 -
    4.42 -
    4.43 -Goal "(\\<forall>i. i<I --> c s i = 0) -->  sum I s = 0";
    4.44 -by (induct_tac "I" 1);
    4.45 -by Auto_tac;
    4.46 -qed "sum0";
    4.47 -
    4.48 -
    4.49 -(* Safety properties for Components *)
    4.50 -
    4.51 -Goal "(Component i ok G) = \
    4.52 -\     (G \\<in> preserves (%s. c s i) & Component i \\<in> Allowed G)";
    4.53 -by (auto_tac (claset(), 
    4.54 -      simpset() addsimps [ok_iff_Allowed, Component_def RS def_total_prg_Allowed]));
    4.55 -qed "Component_ok_iff";
    4.56 -AddIffs [Component_ok_iff];
    4.57 -AddIffs [OK_iff_ok];
    4.58 -Addsimps [preserves_def];
    4.59 -
    4.60 -
    4.61 -Goal "Component i \\<in> stable {s. C s = (c s) i + k}";
    4.62 -by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
    4.63 -by (constrains_tac 1);
    4.64 -qed "p2";
    4.65 -
    4.66 -Goal "[| OK I Component; i\\<in>I |]  \
    4.67 -\     ==> Component i \\<in> stable {s. \\<forall>j\\<in>I. j~=i --> c s j = c k j}";
    4.68 -by (asm_full_simp_tac (simpset() addsimps []) 1); 
    4.69 -by (rewrite_goals_tac [Component_def, mk_total_program_def]);
    4.70 -by (full_simp_tac (simpset() addsimps [stable_def, constrains_def]) 1);
    4.71 -by (Blast_tac 1);
    4.72 -qed "p3";
    4.73 -
    4.74 -
    4.75 -Goal 
    4.76 -"[| OK {i. i<I} Component; i<I |] ==> \
    4.77 -\ \\<forall>k. Component i \\<in> stable ({s. C s = c s i + sumj I i k} Int \
    4.78 -\                             {s. \\<forall>j\\<in>{i. i<I}. j~=i --> c s j = c k j})";
    4.79 -by (blast_tac (claset() addIs [[p2, p3] MRS stable_Int]) 1);
    4.80 -qed "p2_p3_lemma1";
    4.81 -
    4.82 -
    4.83 -Goal "(\\<forall>k. F\\<in>stable ({s. C s = (c s) i + sumj I i k} Int \
    4.84 -\                       {s. \\<forall>j\\<in>{i. i<I}. j~=i --> c s j = c k j}))  \
    4.85 -\     ==> (F\\<in>stable {s. C s = c s i + sumj I i s})";
    4.86 -by (full_simp_tac (simpset() addsimps [constrains_def, stable_def]) 1);
    4.87 -by (force_tac (claset() addSIs [sumj_ext], simpset()) 1);
    4.88 -qed "p2_p3_lemma2";
    4.89 -
    4.90 -
    4.91 -Goal "[| OK {i. i<I} Component; i<I |] \
    4.92 -\     ==> Component i \\<in> stable {s. C s = c s i + sumj I i s}";
    4.93 -by (blast_tac (claset() addIs [p2_p3_lemma1 RS p2_p3_lemma2]) 1);
    4.94 -qed "p2_p3";
    4.95 -
    4.96 -
    4.97 -(* Compositional correctness *)
    4.98 -Goalw [invariant_def]
    4.99 -     "[| 0<I; OK {i. i<I} Component |]  \
   4.100 -\     ==> (\\<Squnion>i\\<in>{i. i<I}. (Component i)) \\<in> invariant {s. C s = sum I s}";
   4.101 -by (simp_tac (simpset() addsimps [JN_stable, sum_sumj_eq2]) 1);
   4.102 -by (auto_tac (claset() addSIs [sum0 RS mp, p2_p3], 
   4.103 -              simpset()));
   4.104 -qed "safety";
   4.105 -
   4.106 -
   4.107 -
   4.108 -
   4.109 -
   4.110 -
   4.111 -
   4.112 -
   4.113 -
   4.114 -
   4.115 -
   4.116 -
   4.117 -
   4.118 -
   4.119 -
   4.120 -
   4.121 -
   4.122 -
   4.123 -
   4.124 -
   4.125 - 
   4.126 -
   4.127 -
   4.128 -
   4.129 -
     5.1 --- a/src/HOL/UNITY/Comp/Counterc.thy	Thu Jul 03 10:37:25 2003 +0200
     5.2 +++ b/src/HOL/UNITY/Comp/Counterc.thy	Thu Jul 03 12:56:48 2003 +0200
     5.3 @@ -11,9 +11,9 @@
     5.4     Spriner LNCS 1586 (1999), pages 1215-1227.
     5.5  *)
     5.6  
     5.7 -Counterc =  UNITY_Main +
     5.8 +theory Counterc =  UNITY_Main:
     5.9  
    5.10 -types state
    5.11 +typedecl state
    5.12  arities state :: type
    5.13  
    5.14  consts
    5.15 @@ -41,5 +41,90 @@
    5.16    Component :: "nat => state program"
    5.17    "Component i == mk_total_program({s. C s = 0 & (c s) i = 0},
    5.18  				   {a i},
    5.19 - 	                           \\<Union>G \\<in> preserves (%s. (c s) i). Acts G)"
    5.20 + 	                           \<Union>G \<in> preserves (%s. (c s) i). Acts G)"
    5.21 +
    5.22 +
    5.23 +declare Component_def [THEN def_prg_Init, simp]
    5.24 +declare Component_def [THEN def_prg_AllowedActs, simp]
    5.25 +declare a_def [THEN def_act_simp, simp]
    5.26 +
    5.27 +(* Theorems about sum and sumj *)
    5.28 +lemma sum_sumj_eq1 [rule_format]: "\<forall>i. I<i--> (sum I s = sumj I i s)"
    5.29 +by (induct_tac "I", auto)
    5.30 +
    5.31 +lemma sum_sumj_eq2 [rule_format]: "i<I --> sum I s  = c s i + sumj I i s"
    5.32 +apply (induct_tac "I")
    5.33 +apply (auto simp add: linorder_neq_iff sum_sumj_eq1)
    5.34 +done
    5.35 +
    5.36 +lemma sum_ext [rule_format]:
    5.37 +     "(\<forall>i. i<I --> c s' i = c s i) --> (sum I s' = sum I s)"
    5.38 +by (induct_tac "I", auto)
    5.39 +
    5.40 +lemma sumj_ext [rule_format]:
    5.41 +     "(\<forall>j. j<I & j~=i --> c s' j =  c s j) --> (sumj I i s' = sumj I i s)"
    5.42 +apply (induct_tac "I", safe)
    5.43 +apply (auto intro!: sum_ext)
    5.44 +done
    5.45 +
    5.46 +
    5.47 +lemma sum0 [rule_format]: "(\<forall>i. i<I --> c s i = 0) -->  sum I s = 0"
    5.48 +by (induct_tac "I", auto)
    5.49 +
    5.50 +
    5.51 +(* Safety properties for Components *)
    5.52 +
    5.53 +lemma Component_ok_iff:
    5.54 +     "(Component i ok G) =  
    5.55 +      (G \<in> preserves (%s. c s i) & Component i \<in> Allowed G)"
    5.56 +apply (auto simp add: ok_iff_Allowed Component_def [THEN def_total_prg_Allowed])
    5.57 +done
    5.58 +declare Component_ok_iff [iff]
    5.59 +declare OK_iff_ok [iff]
    5.60 +declare preserves_def [simp]
    5.61 +
    5.62 +
    5.63 +lemma p2: "Component i \<in> stable {s. C s = (c s) i + k}"
    5.64 +by (simp add: Component_def, constrains)
    5.65 +
    5.66 +lemma p3:
    5.67 +     "[| OK I Component; i\<in>I |]   
    5.68 +      ==> Component i \<in> stable {s. \<forall>j\<in>I. j~=i --> c s j = c k j}"
    5.69 +apply simp
    5.70 +apply (unfold Component_def mk_total_program_def)
    5.71 +apply (simp (no_asm_use) add: stable_def constrains_def)
    5.72 +apply blast
    5.73 +done
    5.74 +
    5.75 +
    5.76 +lemma p2_p3_lemma1: 
    5.77 +     "[| OK {i. i<I} Component; i<I |] ==>  
    5.78 +      \<forall>k. Component i \<in> stable ({s. C s = c s i + sumj I i k} Int  
    5.79 +	 	                {s. \<forall>j\<in>{i. i<I}. j~=i --> c s j = c k j})"
    5.80 +by (blast intro: stable_Int [OF p2 p3])
    5.81 +
    5.82 +lemma p2_p3_lemma2:
    5.83 +     "(\<forall>k. F \<in> stable ({s. C s = (c s) i + sumj I i k} Int  
    5.84 +                        {s. \<forall>j\<in>{i. i<I}. j~=i --> c s j = c k j}))   
    5.85 +      ==> (F \<in> stable {s. C s = c s i + sumj I i s})"
    5.86 +apply (simp add: constrains_def stable_def)
    5.87 +apply (force intro!: sumj_ext)
    5.88 +done
    5.89 +
    5.90 +
    5.91 +lemma p2_p3:
    5.92 +     "[| OK {i. i<I} Component; i<I |]  
    5.93 +      ==> Component i \<in> stable {s. C s = c s i + sumj I i s}"
    5.94 +by (blast intro: p2_p3_lemma1 [THEN p2_p3_lemma2])
    5.95 +
    5.96 +
    5.97 +(* Compositional correctness *)
    5.98 +lemma safety: 
    5.99 +     "[| 0<I; OK {i. i<I} Component |]   
   5.100 +      ==> (\<Squnion>i\<in>{i. i<I}. (Component i)) \<in> invariant {s. C s = sum I s}"
   5.101 +apply (unfold invariant_def)
   5.102 +apply (simp (no_asm) add: JN_stable sum_sumj_eq2)
   5.103 +apply (auto intro!: sum0 p2_p3)
   5.104 +done
   5.105 +
   5.106  end  
     6.1 --- a/src/HOL/UNITY/Comp/Priority.thy	Thu Jul 03 10:37:25 2003 +0200
     6.2 +++ b/src/HOL/UNITY/Comp/Priority.thy	Thu Jul 03 12:56:48 2003 +0200
     6.3 @@ -2,8 +2,6 @@
     6.4      ID:         $Id$
     6.5      Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     6.6      Copyright   2001  University of Cambridge
     6.7 -
     6.8 -
     6.9  *)
    6.10  
    6.11  header{*The priority system*}
    6.12 @@ -128,17 +126,16 @@
    6.13  (* property 14: the 'above set' of a Component that hasn't got 
    6.14        priority doesn't increase *)
    6.15  lemma above_not_increase: 
    6.16 -     "\<forall>j. system \<in> -Highest i Int {s. j\<notin>above i s} co {s. j\<notin>above i s}"
    6.17 -apply clarify
    6.18 -apply (cut_tac i = j in reach_lemma)
    6.19 +     "system \<in> -Highest i Int {s. j\<notin>above i s} co {s. j\<notin>above i s}"
    6.20 +apply (insert reach_lemma [of concl: j])
    6.21  apply (simp add: system_def Component_def mk_total_program_def totalize_JN, 
    6.22         constrains)
    6.23 -apply (auto simp add: trancl_converse)
    6.24 +apply (simp add: trancl_converse, blast) 
    6.25  done
    6.26  
    6.27  lemma above_not_increase':
    6.28       "system \<in> -Highest i Int {s. above i s = x} co {s. above i s <= x}"
    6.29 -apply (cut_tac i = i in above_not_increase)
    6.30 +apply (insert above_not_increase [of i])
    6.31  apply (simp add: trancl_converse constrains_def, blast)
    6.32  done
    6.33  
    6.34 @@ -174,8 +171,7 @@
    6.35  
    6.36  (* property 17: original one is an invariant *)
    6.37  lemma Acyclic_Maximal_stable: "system \<in> stable (Acyclic Int Maximal)"
    6.38 -apply (simp add: Acyclic_subset_Maximal [THEN Int_absorb2] Acyclic_stable)
    6.39 -done
    6.40 +by (simp add: Acyclic_subset_Maximal [THEN Int_absorb2] Acyclic_stable)
    6.41  
    6.42  
    6.43  (* propert 5: existential property *)
    6.44 @@ -216,7 +212,7 @@
    6.45  apply (rule leadsTo_UN)
    6.46  apply (rule single_leadsTo_I, clarify)
    6.47  apply (rule_tac x2 = "above i x" in above_decreases_lemma)
    6.48 -apply (simp_all (no_asm_use) del: Highest_def add: Highest_iff_above0)
    6.49 +apply (simp_all (no_asm_use) add: Highest_iff_above0)
    6.50  apply blast+
    6.51  done
    6.52  
    6.53 @@ -249,7 +245,7 @@
    6.54  
    6.55  lemma Progress: "system \<in> Acyclic leadsTo Highest i"
    6.56  apply (rule_tac f = "%s. above i s" in finite_psubset_induct)
    6.57 -apply (simp del: Highest_def above_def
    6.58 +apply (simp del: above_def
    6.59              add: Highest_iff_above0 vimage_def finite_psubset_def, clarify)
    6.60  apply (case_tac "m={}")
    6.61  apply (rule Int_lower2 [THEN [2] leadsTo_weaken_L])
    6.62 @@ -265,4 +261,4 @@
    6.63  suffices that we start from a state which is finite and acyclic.*}
    6.64  
    6.65  
    6.66 -end
    6.67 \ No newline at end of file
    6.68 +end
     7.1 --- a/src/HOL/UNITY/Comp/PriorityAux.ML	Thu Jul 03 10:37:25 2003 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,116 +0,0 @@
     7.4 -(*  Title:      HOL/UNITY/PriorityAux
     7.5 -    ID:         $Id$
     7.6 -    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     7.7 -    Copyright   2001  University of Cambridge
     7.8 -
     7.9 -Auxiliary definitions needed in Priority.thy
    7.10 -*)
    7.11 -
    7.12 -Addsimps [derive_def, derive1_def, symcl_def, A_def, R_def,  
    7.13 -          above_def, reach_def, reverse_def, neighbors_def];
    7.14 -
    7.15 -(*All vertex sets are finite \\<dots>*)
    7.16 -AddIffs [[subset_UNIV, finite_vertex_univ] MRS finite_subset];
    7.17 -
    7.18 -(* and relatons over vertex are finite too *)
    7.19 -AddIffs [[subset_UNIV, [finite_vertex_univ, finite_vertex_univ] 
    7.20 -           MRS finite_Prod_UNIV] MRS finite_subset];
    7.21 -
    7.22 -
    7.23 -(* The equalities (above i r = {}) = (A i r = {}) 
    7.24 -   and (reach i r = {}) = (R i r) rely on the following theorem  *)
    7.25 -
    7.26 -Goal "((r^+)``{i} = {}) = (r``{i} = {})";
    7.27 -by Auto_tac;
    7.28 -by (etac trancl_induct 1);
    7.29 -by Auto_tac;
    7.30 -qed "image0_trancl_iff_image0_r";
    7.31 -
    7.32 -(* Another form usefull in some situation *)
    7.33 -Goal "(r``{i}={}) = (ALL x. ((i,x):r^+) = False)";
    7.34 -by Auto_tac;
    7.35 -by (dtac (image0_trancl_iff_image0_r RS ssubst) 1);
    7.36 -by Auto_tac;
    7.37 -qed "image0_r_iff_image0_trancl";
    7.38 -
    7.39 -
    7.40 -(* In finite universe acyclic coincides with wf *)
    7.41 -Goal 
    7.42 -"!!r::(vertex*vertex)set. acyclic r = wf r";
    7.43 -by (auto_tac (claset(), simpset() addsimps [wf_iff_acyclic_if_finite]));
    7.44 -qed "acyclic_eq_wf";
    7.45 -
    7.46 -(* derive and derive1 are equivalent *)
    7.47 -Goal "derive i r q = derive1 i r q";
    7.48 -by Auto_tac;
    7.49 -qed "derive_derive1_eq";
    7.50 -
    7.51 -(* Lemma 1 *)
    7.52 -Goalw [reach_def]
    7.53 -"[| x:reach i q; derive1 k r q |] ==> x~=k --> x:reach i r";
    7.54 -by (etac ImageE 1);
    7.55 -by (etac trancl_induct 1);
    7.56 -by (case_tac "i=k" 1);
    7.57 -by (auto_tac (claset() addIs [r_into_trancl], simpset()));
    7.58 -by (dres_inst_tac [("x", "y")] spec 1);
    7.59 -by (rotate_tac ~1 1);
    7.60 -by (dres_inst_tac [("x", "z")] spec 1);
    7.61 -by (auto_tac (claset() addDs [r_into_trancl] addIs [trancl_trans], simpset()));
    7.62 -qed "lemma1_a";
    7.63 -
    7.64 -Goal "ALL k r q. derive k r q -->(reach i q <= (reach i r Un {k}))";
    7.65 -by (REPEAT(rtac allI 1));
    7.66 -by (rtac impI 1);
    7.67 -by (rtac subsetI 1 THEN dtac lemma1_a 1);
    7.68 -by (auto_tac (claset(), simpset() addsimps [derive_derive1_eq]
    7.69 -                    delsimps [reach_def, derive_def, derive1_def]));
    7.70 -qed "reach_lemma";
    7.71 -
    7.72 -(* An other possible formulation of the above theorem based on
    7.73 -   the equivalence x:reach y r = y:above x r                  *)
    7.74 -Goal 
    7.75 -"(ALL i. reach i q <= (reach i r Un {k})) =\
    7.76 -\ (ALL x. x~=k --> (ALL i. i~:above x r --> i~:above x q))";
    7.77 -by (auto_tac (claset(), simpset() addsimps [trancl_converse]));
    7.78 -qed "reach_above_lemma";
    7.79 -
    7.80 -(* Lemma 2 *)
    7.81 -Goal 
    7.82 -"(z, i):r^+ ==> (ALL y. (y, z):r --> (y, i)~:r^+) = ((r^-1)``{z}={})";
    7.83 -by Auto_tac;
    7.84 -by (forw_inst_tac [("r", "r")] trancl_into_trancl2 1);
    7.85 -by Auto_tac;
    7.86 -qed "maximal_converse_image0";
    7.87 -
    7.88 -Goal
    7.89 - "acyclic r ==> A i r~={}-->(EX j:above i r. A j r = {})";
    7.90 -by (full_simp_tac (simpset() 
    7.91 -            addsimps [acyclic_eq_wf, wf_eq_minimal]) 1);
    7.92 -by (dres_inst_tac [("x", "((r^-1)^+)``{i}")] spec 1);
    7.93 -by Auto_tac;
    7.94 -by (rotate_tac ~1 1);
    7.95 -by (asm_full_simp_tac (simpset() 
    7.96 -        addsimps [maximal_converse_image0, trancl_converse]) 1);
    7.97 -qed "above_lemma_a";
    7.98 -
    7.99 -
   7.100 -Goal
   7.101 - "acyclic r ==> above i r~={}-->(EX j:above i r. above j r = {})";
   7.102 -by (dtac above_lemma_a 1);
   7.103 -by (auto_tac (claset(), simpset() 
   7.104 -        addsimps [image0_trancl_iff_image0_r]));
   7.105 -qed "above_lemma_b";
   7.106 -
   7.107 -
   7.108 -
   7.109 -
   7.110 -
   7.111 -
   7.112 -
   7.113 -
   7.114 -
   7.115 -
   7.116 -
   7.117 -
   7.118 -
   7.119 -
     8.1 --- a/src/HOL/UNITY/Comp/PriorityAux.thy	Thu Jul 03 10:37:25 2003 +0200
     8.2 +++ b/src/HOL/UNITY/Comp/PriorityAux.thy	Thu Jul 03 12:56:48 2003 +0200
     8.3 @@ -6,19 +6,19 @@
     8.4  Auxiliary definitions needed in Priority.thy
     8.5  *)
     8.6  
     8.7 -PriorityAux = UNITY_Main +
     8.8 +theory PriorityAux = UNITY_Main:
     8.9  
    8.10 -types vertex
    8.11 +typedecl vertex
    8.12  arities vertex :: type
    8.13    
    8.14  constdefs
    8.15    (* symmetric closure: removes the orientation of a relation *)
    8.16    symcl :: "(vertex*vertex)set=>(vertex*vertex)set"
    8.17 -  "symcl r == r Un (r^-1)"
    8.18 +  "symcl r == r \<union> (r^-1)"
    8.19  
    8.20    (* Neighbors of a vertex i *)
    8.21    neighbors :: "[vertex, (vertex*vertex)set]=>vertex set"
    8.22 - "neighbors i r == ((r Un r^-1)``{i}) - {i}"
    8.23 + "neighbors i r == ((r \<union> r^-1)``{i}) - {i}"
    8.24  
    8.25    R :: "[vertex, (vertex*vertex)set]=>vertex set"
    8.26    "R i r == r``{i}"
    8.27 @@ -34,20 +34,107 @@
    8.28    "above i r == ((r^-1)^+)``{i}"  
    8.29  
    8.30    reverse :: "[vertex, (vertex*vertex) set]=>(vertex*vertex)set"
    8.31 -  "reverse i r == (r - {(x,y). x=i | y=i} Int r) Un ({(x,y). x=i|y=i} Int r)^-1"
    8.32 +  "reverse i r == (r - {(x,y). x=i | y=i} \<inter> r) \<union> ({(x,y). x=i|y=i} \<inter> r)^-1"
    8.33  
    8.34    (* The original definition *)
    8.35    derive1 :: "[vertex, (vertex*vertex)set, (vertex*vertex)set]=>bool"
    8.36    "derive1 i r q == symcl r = symcl q &
    8.37 -                    (ALL k k'. k~=i & k'~=i -->((k,k'):r) = ((k,k'):q)) &
    8.38 +                    (\<forall>k k'. k\<noteq>i & k'\<noteq>i -->((k,k'):r) = ((k,k'):q)) &
    8.39                      A i r = {} & R i q = {}"
    8.40  
    8.41    (* Our alternative definition *)
    8.42    derive :: "[vertex, (vertex*vertex)set, (vertex*vertex)set]=>bool"
    8.43    "derive i r q == A i r = {} & (q = reverse i r)"
    8.44  
    8.45 -rules
    8.46 +axioms
    8.47    (* we assume that the universe of vertices is finite  *)
    8.48 -  finite_vertex_univ "finite (UNIV :: vertex set)"
    8.49 +  finite_vertex_univ:  "finite (UNIV :: vertex set)"
    8.50 +
    8.51 +declare derive_def [simp] derive1_def [simp] symcl_def [simp] 
    8.52 +        A_def [simp] R_def [simp] 
    8.53 +        above_def [simp] reach_def [simp] 
    8.54 +        reverse_def [simp] neighbors_def [simp]
    8.55 +
    8.56 +text{*All vertex sets are finite \<dots>*}
    8.57 +declare finite_subset [OF subset_UNIV finite_vertex_univ, iff]
    8.58 +
    8.59 +text{* and relatons over vertex are finite too *}
    8.60 +
    8.61 +lemmas finite_UNIV_Prod =
    8.62 +       finite_Prod_UNIV [OF finite_vertex_univ finite_vertex_univ] 
    8.63 +
    8.64 +declare finite_subset [OF subset_UNIV finite_UNIV_Prod, iff]
    8.65 +
    8.66 +
    8.67 +(* The equalities (above i r = {}) = (A i r = {}) 
    8.68 +   and (reach i r = {}) = (R i r) rely on the following theorem  *)
    8.69 +
    8.70 +lemma image0_trancl_iff_image0_r: "((r^+)``{i} = {}) = (r``{i} = {})"
    8.71 +apply auto
    8.72 +apply (erule trancl_induct, auto)
    8.73 +done
    8.74 +
    8.75 +(* Another form usefull in some situation *)
    8.76 +lemma image0_r_iff_image0_trancl: "(r``{i}={}) = (ALL x. ((i,x):r^+) = False)"
    8.77 +apply auto
    8.78 +apply (drule image0_trancl_iff_image0_r [THEN ssubst], auto)
    8.79 +done
    8.80 +
    8.81 +
    8.82 +(* In finite universe acyclic coincides with wf *)
    8.83 +lemma acyclic_eq_wf: "!!r::(vertex*vertex)set. acyclic r = wf r"
    8.84 +by (auto simp add: wf_iff_acyclic_if_finite)
    8.85 +
    8.86 +(* derive and derive1 are equivalent *)
    8.87 +lemma derive_derive1_eq: "derive i r q = derive1 i r q"
    8.88 +by auto
    8.89 +
    8.90 +(* Lemma 1 *)
    8.91 +lemma lemma1_a: 
    8.92 +     "[| x \<in> reach i q; derive1 k r q |] ==> x\<noteq>k --> x \<in> reach i r"
    8.93 +apply (unfold reach_def)
    8.94 +apply (erule ImageE)
    8.95 +apply (erule trancl_induct) 
    8.96 + apply (case_tac "i=k", simp_all) 
    8.97 +  apply (blast intro: r_into_trancl, blast, clarify) 
    8.98 +apply (drule_tac x = y in spec)
    8.99 +apply (drule_tac x = z in spec)
   8.100 +apply (blast dest: r_into_trancl intro: trancl_trans)
   8.101 +done
   8.102 +
   8.103 +lemma reach_lemma: "derive k r q ==> reach i q \<subseteq> (reach i r \<union> {k})"
   8.104 +apply clarify 
   8.105 +apply (drule lemma1_a)
   8.106 +apply (auto simp add: derive_derive1_eq 
   8.107 +            simp del: reach_def derive_def derive1_def)
   8.108 +done
   8.109 +
   8.110 +(* An other possible formulation of the above theorem based on
   8.111 +   the equivalence x \<in> reach y r = y \<in> above x r                  *)
   8.112 +lemma reach_above_lemma:
   8.113 +      "(\<forall>i. reach i q \<subseteq> (reach i r \<union> {k})) = 
   8.114 +       (\<forall>x. x\<noteq>k --> (\<forall>i. i \<notin> above x r --> i \<notin> above x q))"
   8.115 +by (auto simp add: trancl_converse)
   8.116 +
   8.117 +(* Lemma 2 *)
   8.118 +lemma maximal_converse_image0: 
   8.119 +     "(z, i):r^+ ==> (\<forall>y. (y, z):r --> (y,i) \<notin> r^+) = ((r^-1)``{z}={})"
   8.120 +apply auto
   8.121 +apply (frule_tac r = r in trancl_into_trancl2, auto)
   8.122 +done
   8.123 +
   8.124 +lemma above_lemma_a: 
   8.125 +     "acyclic r ==> A i r\<noteq>{}-->(\<exists>j \<in> above i r. A j r = {})"
   8.126 +apply (simp add: acyclic_eq_wf wf_eq_minimal) 
   8.127 +apply (drule_tac x = " ((r^-1) ^+) ``{i}" in spec)
   8.128 +apply auto
   8.129 +apply (simp add: maximal_converse_image0 trancl_converse)
   8.130 +done
   8.131 +
   8.132 +lemma above_lemma_b: 
   8.133 +     "acyclic r ==> above i r\<noteq>{}-->(\<exists>j \<in> above i r. above j r = {})";
   8.134 +apply (drule above_lemma_a)
   8.135 +apply (auto simp add: image0_trancl_iff_image0_r)
   8.136 +done
   8.137  
   8.138  end