# HG changeset patch
# User prensani
# Date 1015348751 -3600
# Node ID b115b305612f53fa8eaefa43618a59912204d0ba
# Parent  cd0075346431ac83730f8db5a1c7f842d1278c00
New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)

diff -r cd0075346431 -r b115b305612f src/HOL/HoareParallel/Gar_Coll.thy
--- a/src/HOL/HoareParallel/Gar_Coll.thy	Tue Mar 05 17:14:11 2002 +0100
+++ b/src/HOL/HoareParallel/Gar_Coll.thy	Tue Mar 05 18:19:11 2002 +0100
@@ -654,7 +654,7 @@
  apply force
 apply (simp add:BtoW_def)
 apply force
---{* 1 subgoals left *}
+--{* 1 subgoal left *}
 apply(simp add:abbrev)
 done
 
@@ -757,7 +757,7 @@
 apply(rule conjI)
  apply(erule disjE, erule disjI1, rule disjI2,erule subset_trans, erule Graph9) 
 apply(simp add:nth_list_update)
---{* 1 subgoals left *}
+--{* 1 subgoal left *}
 apply(clarify, simp add:abbrev Graph7 Graph8 Graph12,
       erule disjE, erule disjI1, rule disjI2,erule subset_trans, erule Graph9)
 done
diff -r cd0075346431 -r b115b305612f src/HOL/HoareParallel/Graph.thy
--- a/src/HOL/HoareParallel/Graph.thy	Tue Mar 05 17:14:11 2002 +0100
+++ b/src/HOL/HoareParallel/Graph.thy	Tue Mar 05 18:19:11 2002 +0100
@@ -42,7 +42,7 @@
 lemmas Graph_defs= Blacks_def Proper_Roots_def Proper_Edges_def BtoW_def
 declare Graph_defs [simp]
 
-subsubsection{* Graph 1. *}
+subsubsection{* Graph 1 *}
 
 lemma Graph1_aux [rule_format]: 
   "\<lbrakk> Roots\<subseteq>Blacks M; \<forall>i<length E. \<not>BtoW(E!i,M)\<rbrakk>
@@ -89,7 +89,7 @@
 apply auto
 done
 
-subsubsection{* Graph 2. *}
+subsubsection{* Graph 2 *}
 
 lemma Ex_first_occurrence [rule_format]: 
   "P (n::nat) \<longrightarrow> (\<exists>m. P m \<and> (\<forall>i. i<m \<longrightarrow> \<not> P i))";
@@ -196,7 +196,7 @@
 done
 
 
-subsubsection{* Graph 3. *}
+subsubsection{* Graph 3 *}
 
 lemma Graph3: 
   "\<lbrakk> T\<in>Reach E; R<length E \<rbrakk> \<Longrightarrow> Reach(E[R:=(fst(E!R),T)]) \<subseteq> Reach E"
@@ -281,7 +281,7 @@
 apply(force simp add: nth_list_update)
 done
 
-subsubsection{* Graph 4. *}
+subsubsection{* Graph 4 *}
 
 lemma Graph4: 
   "\<lbrakk>T \<in> Reach E; Roots\<subseteq>Blacks M; I\<le>length E; T<length M; R<length E; 
@@ -322,7 +322,7 @@
 apply force
 done
 
-subsubsection {* Graph 5. *}
+subsubsection {* Graph 5 *}
 
 lemma Graph5: 
   "\<lbrakk> T \<in> Reach E ; Roots \<subseteq> Blacks M; \<forall>i<R. \<not>BtoW(E!i,M); T<length M; 
@@ -366,7 +366,7 @@
 apply force
 done
 
-subsubsection {* Graph 6, 7, 8. *}
+subsubsection {* Other lemmas about graphs *}
 
 lemma Graph6: 
  "\<lbrakk>Proper_Edges(M,E); R<length E ; T<length M\<rbrakk> \<Longrightarrow> Proper_Edges(M,E[R:=(fst(E!R),T)])"
diff -r cd0075346431 -r b115b305612f src/HOL/HoareParallel/Mul_Gar_Coll.thy
--- a/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Tue Mar 05 17:14:11 2002 +0100
+++ b/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Tue Mar 05 18:19:11 2002 +0100
@@ -294,7 +294,7 @@
 apply(erule less_SucE)
  apply force
 apply (simp add:BtoW_def)
---{* 1 subgoals left *}
+--{* 1 subgoal left *}
 apply clarify
 apply simp
 apply(disjE_tac)
@@ -388,7 +388,7 @@
 apply (force simp add:Blacks_def)
 --{* 2 subgoals left *}
 apply force
---{* 1 subgoals left *}
+--{* 1 subgoal left *}
 apply clarify
 apply(drule le_imp_less_or_eq)
 apply(disjE_tac)
@@ -777,7 +777,7 @@
  apply(rule disjI1, erule less_le_trans)
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
 apply force
---{* 1 subgoals left *} 
+--{* 1 subgoal left *} 
 apply clarify
 apply(disjE_tac)
   apply(simp_all add:Graph6)
@@ -908,7 +908,7 @@
 apply(rule conjI)
  apply(rule disjI2,rule disjI1, erule subset_psubset_trans,simp add:Graph11) 
 apply (force simp add:nth_list_update)
---{* 1 subgoals left *}
+--{* 1 subgoal left *}
 apply clarify
 apply (simp add:mul_collector_defs Mul_PBInv_def Graph7 Graph8 Graph12)
 apply(case_tac "M x!(T (Muts x!j))=Black")
@@ -1023,7 +1023,7 @@
   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)
  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)
 apply(simp add:Graph6)
---{* 1 subgoals left *}
+--{* 1 subgoal left *}
 apply(simp add:mul_mutator_defs nth_list_update)
 done
 
@@ -1114,7 +1114,7 @@
 apply(rule conjI)
  apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
 apply (simp add: nth_list_update)
---{* 1 subgoals left *}
+--{* 1 subgoal left *}
 apply clarify
 apply disjE_tac
   apply (simp add: Graph7 Graph8 Graph12)
diff -r cd0075346431 -r b115b305612f src/HOL/HoareParallel/OG_Examples.thy
--- a/src/HOL/HoareParallel/OG_Examples.thy	Tue Mar 05 17:14:11 2002 +0100
+++ b/src/HOL/HoareParallel/OG_Examples.thy	Tue Mar 05 18:19:11 2002 +0100
@@ -461,9 +461,10 @@
 
 subsubsection {* Set Elements of an Array to Zero *}
 
-record scheme1_vars =
+record Example1 =
   a :: "nat \<Rightarrow> nat"
-lemma scheme1: 
+
+lemma Example1: 
  "\<parallel>- .{True}.
    COBEGIN SCHEME [0\<le>i<n] .{True}. \<acute>a:=\<acute>a (i:=0) .{\<acute>a i=0}. COEND 
   .{\<forall>i < n. \<acute>a i = 0}."
@@ -472,14 +473,14 @@
 done
 
 text {* Same example with lists as auxiliary variables. *}
-record scheme1_list_vars =
-  a :: "nat list"
-lemma scheme1_list: 
- "\<parallel>- .{n < length \<acute>a}. 
+record Example1_list =
+  A :: "nat list"
+lemma Example1_list: 
+ "\<parallel>- .{n < length \<acute>A}. 
    COBEGIN 
-     SCHEME [0\<le>i<n] .{n < length \<acute>a}. \<acute>a:=\<acute>a[i:=0] .{\<acute>a!i=0}. 
+     SCHEME [0\<le>i<n] .{n < length \<acute>A}. \<acute>A:=\<acute>A[i:=0] .{\<acute>A!i=0}. 
    COEND 
-    .{\<forall>i < n. \<acute>a!i = 0}."
+    .{\<forall>i < n. \<acute>A!i = 0}."
 apply oghoare
 apply simp_all
   apply force+
@@ -492,13 +493,13 @@
 text {* First some lemmas about summation properties. Summation is
 defined in PreList. *}
 
-lemma scheme2_lemma1: "!!b. j<n \<Longrightarrow> (\<Sum>i<n. b i) = (0::nat) \<Longrightarrow> b j = 0 "
+lemma Example2_lemma1: "!!b. j<n \<Longrightarrow> (\<Sum>i<n. b i) = (0::nat) \<Longrightarrow> b j = 0 "
 apply(induct n)
  apply simp_all
 apply(force simp add: less_Suc_eq)
 done
 
-lemma scheme2_lemma2_aux: "!!b. j<n \<Longrightarrow> 
+lemma Example2_lemma2_aux: "!!b. j<n \<Longrightarrow> 
  (\<Sum>i<n. (b i::nat)) = (\<Sum>i<j. b i) + b j + (\<Sum>i<n-(Suc j) . b (Suc j + i))"
 apply(induct n)
  apply simp_all
@@ -509,36 +510,38 @@
 apply arith
 done 
 
-lemma scheme2_lemma2_aux2: "!!b. j\<le> s \<Longrightarrow> (\<Sum>i<j. (b (s:=t)) i) = (\<Sum>i<j. b i)"
+lemma Example2_lemma2_aux2: 
+  "!!b. j\<le> s \<Longrightarrow> (\<Sum>i<j. (b (s:=t)) i) = (\<Sum>i<j. b i)"
 apply(induct j)
  apply simp_all
 done
 
-lemma scheme2_lemma2 [rule_format]: 
+lemma Example2_lemma2: 
  "!!b. \<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i< n. b i)=(\<Sum>i< n. (b (j := Suc 0)) i)"
-apply(frule_tac b="(b (j:=(Suc 0)))" in scheme2_lemma2_aux)
+apply(frule_tac b="(b (j:=(Suc 0)))" in Example2_lemma2_aux)
 apply(erule_tac  t="Summation (b(j := (Suc 0))) n" in ssubst)
-apply(frule_tac b=b in scheme2_lemma2_aux)
+apply(frule_tac b=b in Example2_lemma2_aux)
 apply(erule_tac  t="Summation b n" in ssubst)
 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)))")
 apply(rotate_tac -1)
 apply(erule ssubst)
 apply(subgoal_tac "j\<le>j")
- apply(drule_tac b="b" and t="(Suc 0)" in scheme2_lemma2_aux2)
+ apply(drule_tac b="b" and t="(Suc 0)" in Example2_lemma2_aux2)
 apply(rotate_tac -1)
 apply(erule ssubst)
 apply simp_all
 done
 
-lemma scheme2_lemma3: "!!b. \<forall>i< n. b i = (Suc 0) \<Longrightarrow> (\<Sum>i<n. b i)= n"
+lemma Example2_lemma3: "!!b. \<forall>i< n. b i = (Suc 0) \<Longrightarrow> (\<Sum>i<n. b i)= n"
 apply (induct n)
 apply auto
 done
 
-record scheme2_vars = 
+record Example2 = 
  c :: "nat \<Rightarrow> nat" 
  x :: nat
-lemma scheme_2: "0<n \<Longrightarrow> 
+
+lemma Example_2: "0<n \<Longrightarrow> 
  \<parallel>- .{\<acute>x=0 \<and> (\<Sum>i< n. \<acute>c i)=0}.  
  COBEGIN 
    SCHEME [0\<le>i<n] 
@@ -551,14 +554,14 @@
 apply simp_all
 apply (tactic {* ALLGOALS Clarify_tac *})
 apply simp_all
-    apply(force elim:scheme2_lemma1)
-   apply(erule scheme2_lemma2)
+    apply(force elim:Example2_lemma1)
+   apply(erule Example2_lemma2)
    apply simp
-  apply(erule scheme2_lemma2)
+  apply(erule Example2_lemma2)
   apply simp
- apply(erule scheme2_lemma2)
+ apply(erule Example2_lemma2)
  apply simp
-apply(force intro: scheme2_lemma3)
+apply(force intro: Example2_lemma3)
 done
 
 end
\ No newline at end of file
diff -r cd0075346431 -r b115b305612f src/HOL/HoareParallel/OG_Syntax.thy
--- a/src/HOL/HoareParallel/OG_Syntax.thy	Tue Mar 05 17:14:11 2002 +0100
+++ b/src/HOL/HoareParallel/OG_Syntax.thy	Tue Mar 05 18:19:11 2002 +0100
@@ -1,7 +1,5 @@
 
-header {* \section{Concrete Syntax} *}
-
-theory OG_Syntax = Quote_Antiquote + OG_Tactics:
+theory OG_Syntax = OG_Tactics + Quote_Antiquote:
 
 text{* Syntax for commands and for assertions and boolean expressions in 
  commands @{text com} and annotated commands @{text ann_com}. *}
diff -r cd0075346431 -r b115b305612f src/HOL/HoareParallel/RG_Hoare.thy
--- a/src/HOL/HoareParallel/RG_Hoare.thy	Tue Mar 05 17:14:11 2002 +0100
+++ b/src/HOL/HoareParallel/RG_Hoare.thy	Tue Mar 05 18:19:11 2002 +0100
@@ -34,7 +34,8 @@
           \<Longrightarrow> \<turnstile> While b P sat [pre, rely, guar, post]"
 
   Await: "\<lbrakk> stable pre rely; stable post rely; 
-            \<forall>V. \<turnstile> P sat [pre \<inter> b \<inter> {V}, {(s, t). s = t}, UNIV, {s. (V, s) \<in> guar} \<inter> post] \<rbrakk>
+            \<forall>V. \<turnstile> P sat [pre \<inter> b \<inter> {V}, {(s, t). s = t}, 
+                UNIV, {s. (V, s) \<in> guar} \<inter> post] \<rbrakk>
            \<Longrightarrow> \<turnstile> Await b P sat [pre, rely, guar, post]"
   
   Conseq: "\<lbrakk> pre \<subseteq> pre'; rely \<subseteq> rely'; guar' \<subseteq> guar; post' \<subseteq> post;
@@ -59,8 +60,7 @@
 
 consts par_rghoare :: "('a par_rgformula) set" 
 syntax 
-  "_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)
+  "_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)
 translations 
   "\<turnstile> Ps SAT [pre, rely, guar, post]" \<rightleftharpoons> "(Ps, pre, rely, guar, post) \<in> par_rghoare"
 
@@ -177,7 +177,8 @@
 
 lemma etran_or_ctran [rule_format]: 
   "\<forall>m i. x\<in>cptn \<longrightarrow> m \<le> length x 
-  \<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"
+   \<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"
 apply(induct x,simp)
 apply clarify
 apply(erule cptn.elims,simp)
@@ -233,7 +234,8 @@
  
 lemma stability [rule_format]: 
   "\<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>
-  (\<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> 
+  (\<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> 
   (\<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)"
 apply(induct x)
  apply clarify
@@ -286,7 +288,8 @@
 
 lemma unique_ctran_Basic [rule_format]: 
   "\<forall>s i. x \<in> cptn \<longrightarrow> x ! 0 = (Some (Basic f), s) \<longrightarrow> 
-  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)"
+  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)"
 apply(induct x,simp)
 apply simp
 apply clarify
@@ -383,7 +386,8 @@
 
 lemma unique_ctran_Await [rule_format]: 
   "\<forall>s i. x \<in> cptn \<longrightarrow> x ! 0 = (Some (Await b c), s) \<longrightarrow> 
-  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)"
+  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)"
 apply(induct x,simp+)
 apply clarify
 apply(erule cptn.elims,simp)
@@ -445,8 +449,10 @@
  
 lemma Await_sound: 
   "\<lbrakk>stable pre rely; stable post rely;
-  \<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>
-  \<Turnstile> P sat [pre \<inter> b \<inter> {s. s = V}, {(s, t). s = t}, UNIV, {s. (V, s) \<in> guar} \<inter> post] \<rbrakk>
+  \<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>
+  \<Turnstile> P sat [pre \<inter> b \<inter> {s. s = V}, {(s, t). s = t}, 
+                 UNIV, {s. (V, s) \<in> guar} \<inter> post] \<rbrakk>
   \<Longrightarrow> \<Turnstile> Await b P sat [pre, rely, guar, post]"
 apply(unfold com_validity_def)
 apply clarify
@@ -683,9 +689,11 @@
 done
 
 lemma Seq_sound2 [rule_format]: 
-  "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>
+  "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>
   (\<forall>j<i. fst(x!j)\<noteq>(Some Q)) \<longrightarrow>
-  (\<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)"
+  (\<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)"
 apply(erule cptn.induct)
 apply(unfold cp_def)
 apply safe
@@ -910,9 +918,11 @@
 
 lemma assum_after_body: 
   "\<lbrakk> \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; 
-  (Some P, s) # xs \<in> cptn_mod; fst (((Some P, s) # xs)!length xs) = None; s \<in> b;
-  (Some (While b P), s) # (Some (Seq P (While b P)), s) # map (lift (While b P)) xs @ ys \<in> assum (pre, rely)\<rbrakk>
-  \<Longrightarrow> (Some (While b P), snd (((Some P, s) # xs)!length xs)) # ys \<in> assum (pre, rely)"
+  (Some P, s) # xs \<in> cptn_mod; fst (((Some P, s) # xs)!length xs) = None; 
+   s \<in> b;  (Some (While b P), s) # (Some (Seq P (While b P)), s) # 
+            map (lift (While b P)) xs @ ys \<in> assum (pre, rely)\<rbrakk>
+  \<Longrightarrow> (Some (While b P), snd (((Some P, s) # xs)!length xs)) # ys 
+      \<in> assum (pre, rely)"
 apply(simp add:assum_def com_validity_def cp_def cptn_iff_cptn_mod)
 apply clarify
 apply(erule_tac x=s in allE)
@@ -948,8 +958,8 @@
 lemma assum_after_body: 
   "\<lbrakk> \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; 
   (Some P, s) # xs \<in> cptn_mod; fst (last ((Some P, s) # xs)) = None; s \<in> b;
-  (Some (While b P), s) # (Some (Seq P (While b P)), s) # map (lift (While b P)) xs @ ys 
-   \<in> assum (pre, rely)\<rbrakk>
+  (Some (While b P), s) # (Some (Seq P (While b P)), s) # 
+   map (lift (While b P)) xs @ ys \<in> assum (pre, rely)\<rbrakk>
   \<Longrightarrow> (Some (While b P), snd (last ((Some P, s) # xs))) # ys \<in> assum (pre, rely)"
 apply(simp add:assum_def com_validity_def cp_def cptn_iff_cptn_mod)
 apply clarify
@@ -1214,10 +1224,12 @@
   "ParallelCom Ps \<equiv> map (Some \<circ> fst) Ps" 
 
 lemma two: 
-  "\<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);
-  pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i));
-  \<forall>i<length xs. \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
-  length xs=length clist; x \<in> par_cp (ParallelCom xs) s; x\<in>par_assum(pre, rely);
+  "\<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);
+   pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i));
+   \<forall>i<length xs. 
+   \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
+   length xs=length clist; x \<in> par_cp (ParallelCom xs) s; x\<in>par_assum(pre, rely);
   \<forall>i<length clist. clist!i\<in>cp (Some(Com(xs!i))) s; x \<propto> clist \<rbrakk>
   \<Longrightarrow> \<forall>j i. i<length clist \<and> Suc j<length x \<longrightarrow> (clist!i!j) -c\<rightarrow> (clist!i!Suc j) 
   \<longrightarrow> (snd(clist!i!j), snd(clist!i!Suc j)) \<in> Guar(xs!i)"
@@ -1291,10 +1303,12 @@
 done
 
 lemma three [rule_format]: 
-  "\<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);
-  pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i));
-  \<forall>i<length xs. \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
-  length xs=length clist; x \<in> par_cp (ParallelCom xs) s; x\<in>par_assum(pre, rely);
+  "\<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);
+   pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i));
+   \<forall>i<length xs. 
+    \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
+   length xs=length clist; x \<in> par_cp (ParallelCom xs) s; x \<in> par_assum(pre, rely);
   \<forall>i<length clist. clist!i\<in>cp (Some(Com(xs!i))) s; x \<propto> clist \<rbrakk>
   \<Longrightarrow> \<forall>j i. i<length clist \<and> Suc j<length x \<longrightarrow> (clist!i!j) -e\<rightarrow> (clist!i!Suc j) 
   \<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))"
@@ -1325,10 +1339,14 @@
 done
 
 lemma four: 
-  "\<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);
-  (\<Union>j\<in>{j. j < length xs}. Guar (xs ! j)) \<subseteq> guar; pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i));
-  \<forall>i < length xs. \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
-  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>
+  "\<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);
+   (\<Union>j\<in>{j. j < length xs}. Guar (xs ! j)) \<subseteq> guar; 
+   pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i));
+   \<forall>i < length xs.
+    \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
+   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>
   \<Longrightarrow> (snd (x ! i), snd (x ! Suc i)) \<in> guar"
 apply(simp add: ParallelCom_def)
 apply(subgoal_tac "(map (Some \<circ> fst) xs)\<noteq>[]")
@@ -1372,11 +1390,14 @@
 done
 
 lemma five: 
-  "\<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);
-  pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i)); (\<Inter>i\<in>{i. i < length xs}. Post (xs ! i)) \<subseteq> post;
-  \<forall>i < length xs. \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
-  x \<in> par_cp (ParallelCom xs) s; x \<in> par_assum (pre, rely); All_None (fst (last x)) \<rbrakk>
-  \<Longrightarrow> snd (last x) \<in> post"
+  "\<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);
+   pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i)); 
+   (\<Inter>i\<in>{i. i < length xs}. Post (xs ! i)) \<subseteq> post;
+   \<forall>i < length xs.
+    \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
+    x \<in> par_cp (ParallelCom xs) s; x \<in> par_assum (pre, rely); 
+   All_None (fst (last x)) \<rbrakk> \<Longrightarrow> snd (last x) \<in> post"
 apply(simp add: ParallelCom_def)
 apply(subgoal_tac "(map (Some \<circ> fst) xs)\<noteq>[]")
  prefer 2
@@ -1459,7 +1480,8 @@
 done
 
 theorem par_rgsound: 
-  "\<turnstile> c SAT [pre, rely, guar, post] \<Longrightarrow> \<Turnstile> (ParallelCom c) SAT [pre, rely, guar, post]"
+  "\<turnstile> c SAT [pre, rely, guar, post] \<Longrightarrow> 
+   \<Turnstile> (ParallelCom c) SAT [pre, rely, guar, post]"
 apply(erule par_rghoare.induct)
 apply(case_tac xs,simp)
  apply(simp add:par_com_validity_def par_comm_def)
diff -r cd0075346431 -r b115b305612f src/HOL/HoareParallel/RG_Syntax.thy
--- a/src/HOL/HoareParallel/RG_Syntax.thy	Tue Mar 05 17:14:11 2002 +0100
+++ b/src/HOL/HoareParallel/RG_Syntax.thy	Tue Mar 05 18:19:11 2002 +0100
@@ -1,7 +1,5 @@
 
-header {* \section{Concrete Syntax} *}
-
-theory RG_Syntax = Quote_Antiquote + RG_Hoare:
+theory RG_Syntax = RG_Hoare + Quote_Antiquote:
 
 syntax
   "_Assign"    :: "idt \<Rightarrow> 'b \<Rightarrow> 'a com"                     ("(\<acute>_ :=/ _)" [70, 65] 61)
diff -r cd0075346431 -r b115b305612f src/HOL/HoareParallel/RG_Tran.thy
--- a/src/HOL/HoareParallel/RG_Tran.thy	Tue Mar 05 17:14:11 2002 +0100
+++ b/src/HOL/HoareParallel/RG_Tran.thy	Tue Mar 05 18:19:11 2002 +0100
@@ -407,8 +407,8 @@
         c!i -pc\<rightarrow> c!Suc i \<longrightarrow> (snd(c!i), snd(c!Suc i)) \<in> guar) \<and> 
          (All_None (fst (last c)) \<longrightarrow> snd( last c) \<in> post)}"
 
-  par_com_validity :: "'a  par_com \<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)
+  par_com_validity :: "'a  par_com \<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)
   "\<Turnstile> Ps SAT [pre, rely, guar, post] \<equiv> 
    \<forall>s. par_cp Ps s \<inter> par_assum(pre, rely) \<subseteq> par_comm(guar, post)"
 
@@ -429,7 +429,7 @@
   compat_label :: "'a par_confs \<Rightarrow> ('a confs) list \<Rightarrow> bool"
   "compat_label c clist \<equiv> (\<forall>j. Suc j<length c \<longrightarrow> 
          (c!j -pc\<rightarrow> c!Suc j \<and> (\<exists>i<length clist. (clist!i)!j -c\<rightarrow> (clist!i)! Suc j \<and> 
-                              (\<forall>l<length clist. l\<noteq>i \<longrightarrow> (clist!l)!j -e\<rightarrow> (clist!l)! Suc j))) \<or> 
+                       (\<forall>l<length clist. l\<noteq>i \<longrightarrow> (clist!l)!j -e\<rightarrow> (clist!l)! Suc j))) \<or> 
          (c!j -pe\<rightarrow> c!Suc j \<and> (\<forall>i<length clist. (clist!i)!j -e\<rightarrow> (clist!i)! Suc j)))"
 
   conjoin :: "'a par_confs \<Rightarrow> ('a confs) list \<Rightarrow> bool"  ("_ \<propto> _" [65,65] 64)
@@ -437,7 +437,8 @@
 
 subsubsection {* Some previous lemmas *}
 
-lemma list_eq_if [rule_format]: "\<forall>ys. xs=ys \<longrightarrow> (length xs = length ys) \<longrightarrow> (\<forall>i<length xs. xs!i=ys!i)"
+lemma list_eq_if [rule_format]: 
+  "\<forall>ys. xs=ys \<longrightarrow> (length xs = length ys) \<longrightarrow> (\<forall>i<length xs. xs!i=ys!i)"
 apply (induct xs)
  apply simp
 apply clarify
@@ -523,7 +524,8 @@
 apply(force elim:cptn.elims)
 done
 
-lemma tl_zero[rule_format]: "P (ys!Suc j) \<longrightarrow> Suc j<length ys \<longrightarrow> ys\<noteq>[] \<longrightarrow> P (tl(ys)!j)"
+lemma tl_zero[rule_format]: 
+  "P (ys!Suc j) \<longrightarrow> Suc j<length ys \<longrightarrow> ys\<noteq>[] \<longrightarrow> P (tl(ys)!j)"
 apply(induct ys)
  apply simp_all
 done