New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
--- 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
--- 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)])"
--- 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)
--- 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
--- 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}. *}
--- 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)
--- 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)
--- 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