New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
authorprensani
Tue Mar 05 18:19:11 2002 +0100 (2002-03-05)
changeset 13022b115b305612f
parent 13021 cd0075346431
child 13023 f869b6822006
New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
src/HOL/HoareParallel/Gar_Coll.thy
src/HOL/HoareParallel/Graph.thy
src/HOL/HoareParallel/Mul_Gar_Coll.thy
src/HOL/HoareParallel/OG_Examples.thy
src/HOL/HoareParallel/OG_Syntax.thy
src/HOL/HoareParallel/RG_Hoare.thy
src/HOL/HoareParallel/RG_Syntax.thy
src/HOL/HoareParallel/RG_Tran.thy
     1.1 --- a/src/HOL/HoareParallel/Gar_Coll.thy	Tue Mar 05 17:14:11 2002 +0100
     1.2 +++ b/src/HOL/HoareParallel/Gar_Coll.thy	Tue Mar 05 18:19:11 2002 +0100
     1.3 @@ -654,7 +654,7 @@
     1.4   apply force
     1.5  apply (simp add:BtoW_def)
     1.6  apply force
     1.7 ---{* 1 subgoals left *}
     1.8 +--{* 1 subgoal left *}
     1.9  apply(simp add:abbrev)
    1.10  done
    1.11  
    1.12 @@ -757,7 +757,7 @@
    1.13  apply(rule conjI)
    1.14   apply(erule disjE, erule disjI1, rule disjI2,erule subset_trans, erule Graph9) 
    1.15  apply(simp add:nth_list_update)
    1.16 ---{* 1 subgoals left *}
    1.17 +--{* 1 subgoal left *}
    1.18  apply(clarify, simp add:abbrev Graph7 Graph8 Graph12,
    1.19        erule disjE, erule disjI1, rule disjI2,erule subset_trans, erule Graph9)
    1.20  done
     2.1 --- a/src/HOL/HoareParallel/Graph.thy	Tue Mar 05 17:14:11 2002 +0100
     2.2 +++ b/src/HOL/HoareParallel/Graph.thy	Tue Mar 05 18:19:11 2002 +0100
     2.3 @@ -42,7 +42,7 @@
     2.4  lemmas Graph_defs= Blacks_def Proper_Roots_def Proper_Edges_def BtoW_def
     2.5  declare Graph_defs [simp]
     2.6  
     2.7 -subsubsection{* Graph 1. *}
     2.8 +subsubsection{* Graph 1 *}
     2.9  
    2.10  lemma Graph1_aux [rule_format]: 
    2.11    "\<lbrakk> Roots\<subseteq>Blacks M; \<forall>i<length E. \<not>BtoW(E!i,M)\<rbrakk>
    2.12 @@ -89,7 +89,7 @@
    2.13  apply auto
    2.14  done
    2.15  
    2.16 -subsubsection{* Graph 2. *}
    2.17 +subsubsection{* Graph 2 *}
    2.18  
    2.19  lemma Ex_first_occurrence [rule_format]: 
    2.20    "P (n::nat) \<longrightarrow> (\<exists>m. P m \<and> (\<forall>i. i<m \<longrightarrow> \<not> P i))";
    2.21 @@ -196,7 +196,7 @@
    2.22  done
    2.23  
    2.24  
    2.25 -subsubsection{* Graph 3. *}
    2.26 +subsubsection{* Graph 3 *}
    2.27  
    2.28  lemma Graph3: 
    2.29    "\<lbrakk> T\<in>Reach E; R<length E \<rbrakk> \<Longrightarrow> Reach(E[R:=(fst(E!R),T)]) \<subseteq> Reach E"
    2.30 @@ -281,7 +281,7 @@
    2.31  apply(force simp add: nth_list_update)
    2.32  done
    2.33  
    2.34 -subsubsection{* Graph 4. *}
    2.35 +subsubsection{* Graph 4 *}
    2.36  
    2.37  lemma Graph4: 
    2.38    "\<lbrakk>T \<in> Reach E; Roots\<subseteq>Blacks M; I\<le>length E; T<length M; R<length E; 
    2.39 @@ -322,7 +322,7 @@
    2.40  apply force
    2.41  done
    2.42  
    2.43 -subsubsection {* Graph 5. *}
    2.44 +subsubsection {* Graph 5 *}
    2.45  
    2.46  lemma Graph5: 
    2.47    "\<lbrakk> T \<in> Reach E ; Roots \<subseteq> Blacks M; \<forall>i<R. \<not>BtoW(E!i,M); T<length M; 
    2.48 @@ -366,7 +366,7 @@
    2.49  apply force
    2.50  done
    2.51  
    2.52 -subsubsection {* Graph 6, 7, 8. *}
    2.53 +subsubsection {* Other lemmas about graphs *}
    2.54  
    2.55  lemma Graph6: 
    2.56   "\<lbrakk>Proper_Edges(M,E); R<length E ; T<length M\<rbrakk> \<Longrightarrow> Proper_Edges(M,E[R:=(fst(E!R),T)])"
     3.1 --- a/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Tue Mar 05 17:14:11 2002 +0100
     3.2 +++ b/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Tue Mar 05 18:19:11 2002 +0100
     3.3 @@ -294,7 +294,7 @@
     3.4  apply(erule less_SucE)
     3.5   apply force
     3.6  apply (simp add:BtoW_def)
     3.7 ---{* 1 subgoals left *}
     3.8 +--{* 1 subgoal left *}
     3.9  apply clarify
    3.10  apply simp
    3.11  apply(disjE_tac)
    3.12 @@ -388,7 +388,7 @@
    3.13  apply (force simp add:Blacks_def)
    3.14  --{* 2 subgoals left *}
    3.15  apply force
    3.16 ---{* 1 subgoals left *}
    3.17 +--{* 1 subgoal left *}
    3.18  apply clarify
    3.19  apply(drule le_imp_less_or_eq)
    3.20  apply(disjE_tac)
    3.21 @@ -777,7 +777,7 @@
    3.22   apply(rule disjI1, erule less_le_trans)
    3.23   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
    3.24  apply force
    3.25 ---{* 1 subgoals left *} 
    3.26 +--{* 1 subgoal left *} 
    3.27  apply clarify
    3.28  apply(disjE_tac)
    3.29    apply(simp_all add:Graph6)
    3.30 @@ -908,7 +908,7 @@
    3.31  apply(rule conjI)
    3.32   apply(rule disjI2,rule disjI1, erule subset_psubset_trans,simp add:Graph11) 
    3.33  apply (force simp add:nth_list_update)
    3.34 ---{* 1 subgoals left *}
    3.35 +--{* 1 subgoal left *}
    3.36  apply clarify
    3.37  apply (simp add:mul_collector_defs Mul_PBInv_def Graph7 Graph8 Graph12)
    3.38  apply(case_tac "M x!(T (Muts x!j))=Black")
    3.39 @@ -1023,7 +1023,7 @@
    3.40    apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
    3.41   apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
    3.42  apply(simp add:Graph6)
    3.43 ---{* 1 subgoals left *}
    3.44 +--{* 1 subgoal left *}
    3.45  apply(simp add:mul_mutator_defs nth_list_update)
    3.46  done
    3.47  
    3.48 @@ -1114,7 +1114,7 @@
    3.49  apply(rule conjI)
    3.50   apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
    3.51  apply (simp add: nth_list_update)
    3.52 ---{* 1 subgoals left *}
    3.53 +--{* 1 subgoal left *}
    3.54  apply clarify
    3.55  apply disjE_tac
    3.56    apply (simp add: Graph7 Graph8 Graph12)
     4.1 --- a/src/HOL/HoareParallel/OG_Examples.thy	Tue Mar 05 17:14:11 2002 +0100
     4.2 +++ b/src/HOL/HoareParallel/OG_Examples.thy	Tue Mar 05 18:19:11 2002 +0100
     4.3 @@ -461,9 +461,10 @@
     4.4  
     4.5  subsubsection {* Set Elements of an Array to Zero *}
     4.6  
     4.7 -record scheme1_vars =
     4.8 +record Example1 =
     4.9    a :: "nat \<Rightarrow> nat"
    4.10 -lemma scheme1: 
    4.11 +
    4.12 +lemma Example1: 
    4.13   "\<parallel>- .{True}.
    4.14     COBEGIN SCHEME [0\<le>i<n] .{True}. \<acute>a:=\<acute>a (i:=0) .{\<acute>a i=0}. COEND 
    4.15    .{\<forall>i < n. \<acute>a i = 0}."
    4.16 @@ -472,14 +473,14 @@
    4.17  done
    4.18  
    4.19  text {* Same example with lists as auxiliary variables. *}
    4.20 -record scheme1_list_vars =
    4.21 -  a :: "nat list"
    4.22 -lemma scheme1_list: 
    4.23 - "\<parallel>- .{n < length \<acute>a}. 
    4.24 +record Example1_list =
    4.25 +  A :: "nat list"
    4.26 +lemma Example1_list: 
    4.27 + "\<parallel>- .{n < length \<acute>A}. 
    4.28     COBEGIN 
    4.29 -     SCHEME [0\<le>i<n] .{n < length \<acute>a}. \<acute>a:=\<acute>a[i:=0] .{\<acute>a!i=0}. 
    4.30 +     SCHEME [0\<le>i<n] .{n < length \<acute>A}. \<acute>A:=\<acute>A[i:=0] .{\<acute>A!i=0}. 
    4.31     COEND 
    4.32 -    .{\<forall>i < n. \<acute>a!i = 0}."
    4.33 +    .{\<forall>i < n. \<acute>A!i = 0}."
    4.34  apply oghoare
    4.35  apply simp_all
    4.36    apply force+
    4.37 @@ -492,13 +493,13 @@
    4.38  text {* First some lemmas about summation properties. Summation is
    4.39  defined in PreList. *}
    4.40  
    4.41 -lemma scheme2_lemma1: "!!b. j<n \<Longrightarrow> (\<Sum>i<n. b i) = (0::nat) \<Longrightarrow> b j = 0 "
    4.42 +lemma Example2_lemma1: "!!b. j<n \<Longrightarrow> (\<Sum>i<n. b i) = (0::nat) \<Longrightarrow> b j = 0 "
    4.43  apply(induct n)
    4.44   apply simp_all
    4.45  apply(force simp add: less_Suc_eq)
    4.46  done
    4.47  
    4.48 -lemma scheme2_lemma2_aux: "!!b. j<n \<Longrightarrow> 
    4.49 +lemma Example2_lemma2_aux: "!!b. j<n \<Longrightarrow> 
    4.50   (\<Sum>i<n. (b i::nat)) = (\<Sum>i<j. b i) + b j + (\<Sum>i<n-(Suc j) . b (Suc j + i))"
    4.51  apply(induct n)
    4.52   apply simp_all
    4.53 @@ -509,36 +510,38 @@
    4.54  apply arith
    4.55  done 
    4.56  
    4.57 -lemma scheme2_lemma2_aux2: "!!b. j\<le> s \<Longrightarrow> (\<Sum>i<j. (b (s:=t)) i) = (\<Sum>i<j. b i)"
    4.58 +lemma Example2_lemma2_aux2: 
    4.59 +  "!!b. j\<le> s \<Longrightarrow> (\<Sum>i<j. (b (s:=t)) i) = (\<Sum>i<j. b i)"
    4.60  apply(induct j)
    4.61   apply simp_all
    4.62  done
    4.63  
    4.64 -lemma scheme2_lemma2 [rule_format]: 
    4.65 +lemma Example2_lemma2: 
    4.66   "!!b. \<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i< n. b i)=(\<Sum>i< n. (b (j := Suc 0)) i)"
    4.67 -apply(frule_tac b="(b (j:=(Suc 0)))" in scheme2_lemma2_aux)
    4.68 +apply(frule_tac b="(b (j:=(Suc 0)))" in Example2_lemma2_aux)
    4.69  apply(erule_tac  t="Summation (b(j := (Suc 0))) n" in ssubst)
    4.70 -apply(frule_tac b=b in scheme2_lemma2_aux)
    4.71 +apply(frule_tac b=b in Example2_lemma2_aux)
    4.72  apply(erule_tac  t="Summation b n" in ssubst)
    4.73  apply(subgoal_tac "Suc (Summation b j + b j + (\<Sum>i<n - Suc j. b (Suc j + i)))=(Summation b j + Suc (b j) + (\<Sum>i<n - Suc j. b (Suc j + i)))")
    4.74  apply(rotate_tac -1)
    4.75  apply(erule ssubst)
    4.76  apply(subgoal_tac "j\<le>j")
    4.77 - apply(drule_tac b="b" and t="(Suc 0)" in scheme2_lemma2_aux2)
    4.78 + apply(drule_tac b="b" and t="(Suc 0)" in Example2_lemma2_aux2)
    4.79  apply(rotate_tac -1)
    4.80  apply(erule ssubst)
    4.81  apply simp_all
    4.82  done
    4.83  
    4.84 -lemma scheme2_lemma3: "!!b. \<forall>i< n. b i = (Suc 0) \<Longrightarrow> (\<Sum>i<n. b i)= n"
    4.85 +lemma Example2_lemma3: "!!b. \<forall>i< n. b i = (Suc 0) \<Longrightarrow> (\<Sum>i<n. b i)= n"
    4.86  apply (induct n)
    4.87  apply auto
    4.88  done
    4.89  
    4.90 -record scheme2_vars = 
    4.91 +record Example2 = 
    4.92   c :: "nat \<Rightarrow> nat" 
    4.93   x :: nat
    4.94 -lemma scheme_2: "0<n \<Longrightarrow> 
    4.95 +
    4.96 +lemma Example_2: "0<n \<Longrightarrow> 
    4.97   \<parallel>- .{\<acute>x=0 \<and> (\<Sum>i< n. \<acute>c i)=0}.  
    4.98   COBEGIN 
    4.99     SCHEME [0\<le>i<n] 
   4.100 @@ -551,14 +554,14 @@
   4.101  apply simp_all
   4.102  apply (tactic {* ALLGOALS Clarify_tac *})
   4.103  apply simp_all
   4.104 -    apply(force elim:scheme2_lemma1)
   4.105 -   apply(erule scheme2_lemma2)
   4.106 +    apply(force elim:Example2_lemma1)
   4.107 +   apply(erule Example2_lemma2)
   4.108     apply simp
   4.109 -  apply(erule scheme2_lemma2)
   4.110 +  apply(erule Example2_lemma2)
   4.111    apply simp
   4.112 - apply(erule scheme2_lemma2)
   4.113 + apply(erule Example2_lemma2)
   4.114   apply simp
   4.115 -apply(force intro: scheme2_lemma3)
   4.116 +apply(force intro: Example2_lemma3)
   4.117  done
   4.118  
   4.119  end
   4.120 \ No newline at end of file
     5.1 --- a/src/HOL/HoareParallel/OG_Syntax.thy	Tue Mar 05 17:14:11 2002 +0100
     5.2 +++ b/src/HOL/HoareParallel/OG_Syntax.thy	Tue Mar 05 18:19:11 2002 +0100
     5.3 @@ -1,7 +1,5 @@
     5.4  
     5.5 -header {* \section{Concrete Syntax} *}
     5.6 -
     5.7 -theory OG_Syntax = Quote_Antiquote + OG_Tactics:
     5.8 +theory OG_Syntax = OG_Tactics + Quote_Antiquote:
     5.9  
    5.10  text{* Syntax for commands and for assertions and boolean expressions in 
    5.11   commands @{text com} and annotated commands @{text ann_com}. *}
     6.1 --- a/src/HOL/HoareParallel/RG_Hoare.thy	Tue Mar 05 17:14:11 2002 +0100
     6.2 +++ b/src/HOL/HoareParallel/RG_Hoare.thy	Tue Mar 05 18:19:11 2002 +0100
     6.3 @@ -34,7 +34,8 @@
     6.4            \<Longrightarrow> \<turnstile> While b P sat [pre, rely, guar, post]"
     6.5  
     6.6    Await: "\<lbrakk> stable pre rely; stable post rely; 
     6.7 -            \<forall>V. \<turnstile> P sat [pre \<inter> b \<inter> {V}, {(s, t). s = t}, UNIV, {s. (V, s) \<in> guar} \<inter> post] \<rbrakk>
     6.8 +            \<forall>V. \<turnstile> P sat [pre \<inter> b \<inter> {V}, {(s, t). s = t}, 
     6.9 +                UNIV, {s. (V, s) \<in> guar} \<inter> post] \<rbrakk>
    6.10             \<Longrightarrow> \<turnstile> Await b P sat [pre, rely, guar, post]"
    6.11    
    6.12    Conseq: "\<lbrakk> pre \<subseteq> pre'; rely \<subseteq> rely'; guar' \<subseteq> guar; post' \<subseteq> post;
    6.13 @@ -59,8 +60,7 @@
    6.14  
    6.15  consts par_rghoare :: "('a par_rgformula) set" 
    6.16  syntax 
    6.17 -  "_par_rghoare" :: "('a rgformula) list \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set
    6.18 -                  \<Rightarrow> bool"    ("\<turnstile> _ SAT [_, _, _, _]" [60,0,0,0,0] 45)
    6.19 +  "_par_rghoare" :: "('a rgformula) list \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set \<Rightarrow> bool"    ("\<turnstile> _ SAT [_, _, _, _]" [60,0,0,0,0] 45)
    6.20  translations 
    6.21    "\<turnstile> Ps SAT [pre, rely, guar, post]" \<rightleftharpoons> "(Ps, pre, rely, guar, post) \<in> par_rghoare"
    6.22  
    6.23 @@ -177,7 +177,8 @@
    6.24  
    6.25  lemma etran_or_ctran [rule_format]: 
    6.26    "\<forall>m i. x\<in>cptn \<longrightarrow> m \<le> length x 
    6.27 -  \<longrightarrow> (\<forall>i. Suc i < m \<longrightarrow> \<not> x!i -c\<rightarrow> x!Suc i) \<longrightarrow> Suc i < m \<longrightarrow> x!i -e\<rightarrow> x!Suc i"
    6.28 +   \<longrightarrow> (\<forall>i. Suc i < m \<longrightarrow> \<not> x!i -c\<rightarrow> x!Suc i) \<longrightarrow> Suc i < m 
    6.29 +   \<longrightarrow> x!i -e\<rightarrow> x!Suc i"
    6.30  apply(induct x,simp)
    6.31  apply clarify
    6.32  apply(erule cptn.elims,simp)
    6.33 @@ -233,7 +234,8 @@
    6.34   
    6.35  lemma stability [rule_format]: 
    6.36    "\<forall>j k. x \<in> cptn \<longrightarrow> stable p rely \<longrightarrow> j\<le>k \<longrightarrow> k<length x \<longrightarrow> snd(x!j)\<in>p  \<longrightarrow>
    6.37 -  (\<forall>i. (Suc i)<length x \<longrightarrow> (x!i -e\<rightarrow> x!(Suc i)) \<longrightarrow> (snd(x!i), snd(x!(Suc i))) \<in> rely) \<longrightarrow> 
    6.38 +  (\<forall>i. (Suc i)<length x \<longrightarrow> 
    6.39 +          (x!i -e\<rightarrow> x!(Suc i)) \<longrightarrow> (snd(x!i), snd(x!(Suc i))) \<in> rely) \<longrightarrow> 
    6.40    (\<forall>i. j\<le>i \<and> i<k \<longrightarrow> x!i -e\<rightarrow> x!Suc i) \<longrightarrow> snd(x!k)\<in>p \<and> fst(x!j)=fst(x!k)"
    6.41  apply(induct x)
    6.42   apply clarify
    6.43 @@ -286,7 +288,8 @@
    6.44  
    6.45  lemma unique_ctran_Basic [rule_format]: 
    6.46    "\<forall>s i. x \<in> cptn \<longrightarrow> x ! 0 = (Some (Basic f), s) \<longrightarrow> 
    6.47 -  Suc i<length x \<longrightarrow> x!i -c\<rightarrow> x!Suc i \<longrightarrow> (\<forall>j. Suc j<length x \<longrightarrow> i\<noteq>j \<longrightarrow> x!j -e\<rightarrow> x!Suc j)"
    6.48 +  Suc i<length x \<longrightarrow> x!i -c\<rightarrow> x!Suc i \<longrightarrow> 
    6.49 +  (\<forall>j. Suc j<length x \<longrightarrow> i\<noteq>j \<longrightarrow> x!j -e\<rightarrow> x!Suc j)"
    6.50  apply(induct x,simp)
    6.51  apply simp
    6.52  apply clarify
    6.53 @@ -383,7 +386,8 @@
    6.54  
    6.55  lemma unique_ctran_Await [rule_format]: 
    6.56    "\<forall>s i. x \<in> cptn \<longrightarrow> x ! 0 = (Some (Await b c), s) \<longrightarrow> 
    6.57 -  Suc i<length x \<longrightarrow> x!i -c\<rightarrow> x!Suc i \<longrightarrow> (\<forall>j. Suc j<length x \<longrightarrow> i\<noteq>j \<longrightarrow> x!j -e\<rightarrow> x!Suc j)"
    6.58 +  Suc i<length x \<longrightarrow> x!i -c\<rightarrow> x!Suc i \<longrightarrow> 
    6.59 +  (\<forall>j. Suc j<length x \<longrightarrow> i\<noteq>j \<longrightarrow> x!j -e\<rightarrow> x!Suc j)"
    6.60  apply(induct x,simp+)
    6.61  apply clarify
    6.62  apply(erule cptn.elims,simp)
    6.63 @@ -445,8 +449,10 @@
    6.64   
    6.65  lemma Await_sound: 
    6.66    "\<lbrakk>stable pre rely; stable post rely;
    6.67 -  \<forall>V. \<turnstile> P sat [pre \<inter> b \<inter> {s. s = V}, {(s, t). s = t}, UNIV, {s. (V, s) \<in> guar} \<inter> post] \<and>
    6.68 -  \<Turnstile> P sat [pre \<inter> b \<inter> {s. s = V}, {(s, t). s = t}, UNIV, {s. (V, s) \<in> guar} \<inter> post] \<rbrakk>
    6.69 +  \<forall>V. \<turnstile> P sat [pre \<inter> b \<inter> {s. s = V}, {(s, t). s = t}, 
    6.70 +                 UNIV, {s. (V, s) \<in> guar} \<inter> post] \<and>
    6.71 +  \<Turnstile> P sat [pre \<inter> b \<inter> {s. s = V}, {(s, t). s = t}, 
    6.72 +                 UNIV, {s. (V, s) \<in> guar} \<inter> post] \<rbrakk>
    6.73    \<Longrightarrow> \<Turnstile> Await b P sat [pre, rely, guar, post]"
    6.74  apply(unfold com_validity_def)
    6.75  apply clarify
    6.76 @@ -683,9 +689,11 @@
    6.77  done
    6.78  
    6.79  lemma Seq_sound2 [rule_format]: 
    6.80 -  "x \<in> cptn \<Longrightarrow> \<forall>s P i. x!0=(Some (Seq P Q), s) \<longrightarrow> i<length x \<longrightarrow> fst(x!i)=Some Q \<longrightarrow>
    6.81 +  "x \<in> cptn \<Longrightarrow> \<forall>s P i. x!0=(Some (Seq P Q), s) \<longrightarrow> i<length x 
    6.82 +  \<longrightarrow> fst(x!i)=Some Q \<longrightarrow>
    6.83    (\<forall>j<i. fst(x!j)\<noteq>(Some Q)) \<longrightarrow>
    6.84 -  (\<exists>xs ys. xs \<in> cp (Some P) s \<and> length xs=Suc i \<and> ys \<in> cp (Some Q) (snd(xs !i)) \<and> x=(map (lift Q) xs)@tl ys)"
    6.85 +  (\<exists>xs ys. xs \<in> cp (Some P) s \<and> length xs=Suc i 
    6.86 +   \<and> ys \<in> cp (Some Q) (snd(xs !i)) \<and> x=(map (lift Q) xs)@tl ys)"
    6.87  apply(erule cptn.induct)
    6.88  apply(unfold cp_def)
    6.89  apply safe
    6.90 @@ -910,9 +918,11 @@
    6.91  
    6.92  lemma assum_after_body: 
    6.93    "\<lbrakk> \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; 
    6.94 -  (Some P, s) # xs \<in> cptn_mod; fst (((Some P, s) # xs)!length xs) = None; s \<in> b;
    6.95 -  (Some (While b P), s) # (Some (Seq P (While b P)), s) # map (lift (While b P)) xs @ ys \<in> assum (pre, rely)\<rbrakk>
    6.96 -  \<Longrightarrow> (Some (While b P), snd (((Some P, s) # xs)!length xs)) # ys \<in> assum (pre, rely)"
    6.97 +  (Some P, s) # xs \<in> cptn_mod; fst (((Some P, s) # xs)!length xs) = None; 
    6.98 +   s \<in> b;  (Some (While b P), s) # (Some (Seq P (While b P)), s) # 
    6.99 +            map (lift (While b P)) xs @ ys \<in> assum (pre, rely)\<rbrakk>
   6.100 +  \<Longrightarrow> (Some (While b P), snd (((Some P, s) # xs)!length xs)) # ys 
   6.101 +      \<in> assum (pre, rely)"
   6.102  apply(simp add:assum_def com_validity_def cp_def cptn_iff_cptn_mod)
   6.103  apply clarify
   6.104  apply(erule_tac x=s in allE)
   6.105 @@ -948,8 +958,8 @@
   6.106  lemma assum_after_body: 
   6.107    "\<lbrakk> \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; 
   6.108    (Some P, s) # xs \<in> cptn_mod; fst (last ((Some P, s) # xs)) = None; s \<in> b;
   6.109 -  (Some (While b P), s) # (Some (Seq P (While b P)), s) # map (lift (While b P)) xs @ ys 
   6.110 -   \<in> assum (pre, rely)\<rbrakk>
   6.111 +  (Some (While b P), s) # (Some (Seq P (While b P)), s) # 
   6.112 +   map (lift (While b P)) xs @ ys \<in> assum (pre, rely)\<rbrakk>
   6.113    \<Longrightarrow> (Some (While b P), snd (last ((Some P, s) # xs))) # ys \<in> assum (pre, rely)"
   6.114  apply(simp add:assum_def com_validity_def cp_def cptn_iff_cptn_mod)
   6.115  apply clarify
   6.116 @@ -1214,10 +1224,12 @@
   6.117    "ParallelCom Ps \<equiv> map (Some \<circ> fst) Ps" 
   6.118  
   6.119  lemma two: 
   6.120 -  "\<lbrakk> \<forall>i<length xs. rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j)) \<subseteq> Rely (xs ! i);
   6.121 -  pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i));
   6.122 -  \<forall>i<length xs. \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
   6.123 -  length xs=length clist; x \<in> par_cp (ParallelCom xs) s; x\<in>par_assum(pre, rely);
   6.124 +  "\<lbrakk> \<forall>i<length xs. rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j)) 
   6.125 +     \<subseteq> Rely (xs ! i);
   6.126 +   pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i));
   6.127 +   \<forall>i<length xs. 
   6.128 +   \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
   6.129 +   length xs=length clist; x \<in> par_cp (ParallelCom xs) s; x\<in>par_assum(pre, rely);
   6.130    \<forall>i<length clist. clist!i\<in>cp (Some(Com(xs!i))) s; x \<propto> clist \<rbrakk>
   6.131    \<Longrightarrow> \<forall>j i. i<length clist \<and> Suc j<length x \<longrightarrow> (clist!i!j) -c\<rightarrow> (clist!i!Suc j) 
   6.132    \<longrightarrow> (snd(clist!i!j), snd(clist!i!Suc j)) \<in> Guar(xs!i)"
   6.133 @@ -1291,10 +1303,12 @@
   6.134  done
   6.135  
   6.136  lemma three [rule_format]: 
   6.137 -  "\<lbrakk> xs\<noteq>[]; \<forall>i<length xs. rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j)) \<subseteq> Rely (xs ! i);
   6.138 -  pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i));
   6.139 -  \<forall>i<length xs. \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
   6.140 -  length xs=length clist; x \<in> par_cp (ParallelCom xs) s; x\<in>par_assum(pre, rely);
   6.141 +  "\<lbrakk> xs\<noteq>[]; \<forall>i<length xs. rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j)) 
   6.142 +   \<subseteq> Rely (xs ! i);
   6.143 +   pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i));
   6.144 +   \<forall>i<length xs. 
   6.145 +    \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
   6.146 +   length xs=length clist; x \<in> par_cp (ParallelCom xs) s; x \<in> par_assum(pre, rely);
   6.147    \<forall>i<length clist. clist!i\<in>cp (Some(Com(xs!i))) s; x \<propto> clist \<rbrakk>
   6.148    \<Longrightarrow> \<forall>j i. i<length clist \<and> Suc j<length x \<longrightarrow> (clist!i!j) -e\<rightarrow> (clist!i!Suc j) 
   6.149    \<longrightarrow> (snd(clist!i!j), snd(clist!i!Suc j)) \<in> rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j))"
   6.150 @@ -1325,10 +1339,14 @@
   6.151  done
   6.152  
   6.153  lemma four: 
   6.154 -  "\<lbrakk>xs\<noteq>[]; \<forall>i < length xs. rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j)) \<subseteq> Rely (xs ! i);
   6.155 -  (\<Union>j\<in>{j. j < length xs}. Guar (xs ! j)) \<subseteq> guar; pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i));
   6.156 -  \<forall>i < length xs. \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
   6.157 -  x \<in> par_cp (ParallelCom xs) s; x \<in> par_assum (pre, rely); Suc i < length x; x ! i -pc\<rightarrow> x ! Suc i\<rbrakk>
   6.158 +  "\<lbrakk>xs\<noteq>[]; \<forall>i < length xs. rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j)) 
   6.159 +    \<subseteq> Rely (xs ! i);
   6.160 +   (\<Union>j\<in>{j. j < length xs}. Guar (xs ! j)) \<subseteq> guar; 
   6.161 +   pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i));
   6.162 +   \<forall>i < length xs.
   6.163 +    \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
   6.164 +   x \<in> par_cp (ParallelCom xs) s; x \<in> par_assum (pre, rely); Suc i < length x; 
   6.165 +   x ! i -pc\<rightarrow> x ! Suc i\<rbrakk>
   6.166    \<Longrightarrow> (snd (x ! i), snd (x ! Suc i)) \<in> guar"
   6.167  apply(simp add: ParallelCom_def)
   6.168  apply(subgoal_tac "(map (Some \<circ> fst) xs)\<noteq>[]")
   6.169 @@ -1372,11 +1390,14 @@
   6.170  done
   6.171  
   6.172  lemma five: 
   6.173 -  "\<lbrakk>xs\<noteq>[]; \<forall>i<length xs. rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j)) \<subseteq> Rely (xs ! i);
   6.174 -  pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i)); (\<Inter>i\<in>{i. i < length xs}. Post (xs ! i)) \<subseteq> post;
   6.175 -  \<forall>i < length xs. \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
   6.176 -  x \<in> par_cp (ParallelCom xs) s; x \<in> par_assum (pre, rely); All_None (fst (last x)) \<rbrakk>
   6.177 -  \<Longrightarrow> snd (last x) \<in> post"
   6.178 +  "\<lbrakk>xs\<noteq>[]; \<forall>i<length xs. rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j))
   6.179 +   \<subseteq> Rely (xs ! i);
   6.180 +   pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i)); 
   6.181 +   (\<Inter>i\<in>{i. i < length xs}. Post (xs ! i)) \<subseteq> post;
   6.182 +   \<forall>i < length xs.
   6.183 +    \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
   6.184 +    x \<in> par_cp (ParallelCom xs) s; x \<in> par_assum (pre, rely); 
   6.185 +   All_None (fst (last x)) \<rbrakk> \<Longrightarrow> snd (last x) \<in> post"
   6.186  apply(simp add: ParallelCom_def)
   6.187  apply(subgoal_tac "(map (Some \<circ> fst) xs)\<noteq>[]")
   6.188   prefer 2
   6.189 @@ -1459,7 +1480,8 @@
   6.190  done
   6.191  
   6.192  theorem par_rgsound: 
   6.193 -  "\<turnstile> c SAT [pre, rely, guar, post] \<Longrightarrow> \<Turnstile> (ParallelCom c) SAT [pre, rely, guar, post]"
   6.194 +  "\<turnstile> c SAT [pre, rely, guar, post] \<Longrightarrow> 
   6.195 +   \<Turnstile> (ParallelCom c) SAT [pre, rely, guar, post]"
   6.196  apply(erule par_rghoare.induct)
   6.197  apply(case_tac xs,simp)
   6.198   apply(simp add:par_com_validity_def par_comm_def)
     7.1 --- a/src/HOL/HoareParallel/RG_Syntax.thy	Tue Mar 05 17:14:11 2002 +0100
     7.2 +++ b/src/HOL/HoareParallel/RG_Syntax.thy	Tue Mar 05 18:19:11 2002 +0100
     7.3 @@ -1,7 +1,5 @@
     7.4  
     7.5 -header {* \section{Concrete Syntax} *}
     7.6 -
     7.7 -theory RG_Syntax = Quote_Antiquote + RG_Hoare:
     7.8 +theory RG_Syntax = RG_Hoare + Quote_Antiquote:
     7.9  
    7.10  syntax
    7.11    "_Assign"    :: "idt \<Rightarrow> 'b \<Rightarrow> 'a com"                     ("(\<acute>_ :=/ _)" [70, 65] 61)
     8.1 --- a/src/HOL/HoareParallel/RG_Tran.thy	Tue Mar 05 17:14:11 2002 +0100
     8.2 +++ b/src/HOL/HoareParallel/RG_Tran.thy	Tue Mar 05 18:19:11 2002 +0100
     8.3 @@ -407,8 +407,8 @@
     8.4          c!i -pc\<rightarrow> c!Suc i \<longrightarrow> (snd(c!i), snd(c!Suc i)) \<in> guar) \<and> 
     8.5           (All_None (fst (last c)) \<longrightarrow> snd( last c) \<in> post)}"
     8.6  
     8.7 -  par_com_validity :: "'a  par_com \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set
     8.8 -                  \<Rightarrow> bool"  ("\<Turnstile> _ SAT [_, _, _, _]" [60,0,0,0,0] 45)
     8.9 +  par_com_validity :: "'a  par_com \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set 
    8.10 +\<Rightarrow> 'a set \<Rightarrow> bool"  ("\<Turnstile> _ SAT [_, _, _, _]" [60,0,0,0,0] 45)
    8.11    "\<Turnstile> Ps SAT [pre, rely, guar, post] \<equiv> 
    8.12     \<forall>s. par_cp Ps s \<inter> par_assum(pre, rely) \<subseteq> par_comm(guar, post)"
    8.13  
    8.14 @@ -429,7 +429,7 @@
    8.15    compat_label :: "'a par_confs \<Rightarrow> ('a confs) list \<Rightarrow> bool"
    8.16    "compat_label c clist \<equiv> (\<forall>j. Suc j<length c \<longrightarrow> 
    8.17           (c!j -pc\<rightarrow> c!Suc j \<and> (\<exists>i<length clist. (clist!i)!j -c\<rightarrow> (clist!i)! Suc j \<and> 
    8.18 -                              (\<forall>l<length clist. l\<noteq>i \<longrightarrow> (clist!l)!j -e\<rightarrow> (clist!l)! Suc j))) \<or> 
    8.19 +                       (\<forall>l<length clist. l\<noteq>i \<longrightarrow> (clist!l)!j -e\<rightarrow> (clist!l)! Suc j))) \<or> 
    8.20           (c!j -pe\<rightarrow> c!Suc j \<and> (\<forall>i<length clist. (clist!i)!j -e\<rightarrow> (clist!i)! Suc j)))"
    8.21  
    8.22    conjoin :: "'a par_confs \<Rightarrow> ('a confs) list \<Rightarrow> bool"  ("_ \<propto> _" [65,65] 64)
    8.23 @@ -437,7 +437,8 @@
    8.24  
    8.25  subsubsection {* Some previous lemmas *}
    8.26  
    8.27 -lemma list_eq_if [rule_format]: "\<forall>ys. xs=ys \<longrightarrow> (length xs = length ys) \<longrightarrow> (\<forall>i<length xs. xs!i=ys!i)"
    8.28 +lemma list_eq_if [rule_format]: 
    8.29 +  "\<forall>ys. xs=ys \<longrightarrow> (length xs = length ys) \<longrightarrow> (\<forall>i<length xs. xs!i=ys!i)"
    8.30  apply (induct xs)
    8.31   apply simp
    8.32  apply clarify
    8.33 @@ -523,7 +524,8 @@
    8.34  apply(force elim:cptn.elims)
    8.35  done
    8.36  
    8.37 -lemma tl_zero[rule_format]: "P (ys!Suc j) \<longrightarrow> Suc j<length ys \<longrightarrow> ys\<noteq>[] \<longrightarrow> P (tl(ys)!j)"
    8.38 +lemma tl_zero[rule_format]: 
    8.39 +  "P (ys!Suc j) \<longrightarrow> Suc j<length ys \<longrightarrow> ys\<noteq>[] \<longrightarrow> P (tl(ys)!j)"
    8.40  apply(induct ys)
    8.41   apply simp_all
    8.42  done