--- a/src/HOL/Hoare_Parallel/OG_Hoare.thy Sat Dec 27 19:51:55 2014 +0100
+++ b/src/HOL/Hoare_Parallel/OG_Hoare.thy Sat Dec 27 20:32:06 2014 +0100
@@ -1,4 +1,4 @@
-section {* The Proof System *}
+section \<open>The Proof System\<close>
theory OG_Hoare imports OG_Tran begin
@@ -8,14 +8,14 @@
| "assertions (AnnCond1 r b c1 c2) = {r} \<union> assertions c1 \<union> assertions c2"
| "assertions (AnnCond2 r b c) = {r} \<union> assertions c"
| "assertions (AnnWhile r b i c) = {r, i} \<union> assertions c"
-| "assertions (AnnAwait r b c) = {r}"
+| "assertions (AnnAwait r b c) = {r}"
primrec atomics :: "'a ann_com \<Rightarrow> ('a assn \<times> 'a com) set" where
"atomics (AnnBasic r f) = {(r, Basic f)}"
| "atomics (AnnSeq c1 c2) = atomics c1 \<union> atomics c2"
| "atomics (AnnCond1 r b c1 c2) = atomics c1 \<union> atomics c2"
| "atomics (AnnCond2 r b c) = atomics c"
-| "atomics (AnnWhile r b i c) = atomics c"
+| "atomics (AnnWhile r b i c) = atomics c"
| "atomics (AnnAwait r b c) = {(r \<inter> b, c)}"
primrec com :: "'a ann_triple_op \<Rightarrow> 'a ann_com_op" where
@@ -25,12 +25,12 @@
"post (c, q) = q"
definition interfree_aux :: "('a ann_com_op \<times> 'a assn \<times> 'a ann_com_op) \<Rightarrow> bool" where
- "interfree_aux \<equiv> \<lambda>(co, q, co'). co'= None \<or>
+ "interfree_aux \<equiv> \<lambda>(co, q, co'). co'= None \<or>
(\<forall>(r,a) \<in> atomics (the co'). \<parallel>= (q \<inter> r) a q \<and>
(co = None \<or> (\<forall>p \<in> assertions (the co). \<parallel>= (p \<inter> r) a p)))"
-definition interfree :: "(('a ann_triple_op) list) \<Rightarrow> bool" where
- "interfree Ts \<equiv> \<forall>i j. i < length Ts \<and> j < length Ts \<and> i \<noteq> j \<longrightarrow>
+definition interfree :: "(('a ann_triple_op) list) \<Rightarrow> bool" where
+ "interfree Ts \<equiv> \<forall>i j. i < length Ts \<and> j < length Ts \<and> i \<noteq> j \<longrightarrow>
interfree_aux (com (Ts!i), post (Ts!i), com (Ts!j)) "
inductive
@@ -40,26 +40,26 @@
AnnBasic: "r \<subseteq> {s. f s \<in> q} \<Longrightarrow> \<turnstile> (AnnBasic r f) q"
| AnnSeq: "\<lbrakk> \<turnstile> c0 pre c1; \<turnstile> c1 q \<rbrakk> \<Longrightarrow> \<turnstile> (AnnSeq c0 c1) q"
-
-| AnnCond1: "\<lbrakk> r \<inter> b \<subseteq> pre c1; \<turnstile> c1 q; r \<inter> -b \<subseteq> pre c2; \<turnstile> c2 q\<rbrakk>
+
+| AnnCond1: "\<lbrakk> r \<inter> b \<subseteq> pre c1; \<turnstile> c1 q; r \<inter> -b \<subseteq> pre c2; \<turnstile> c2 q\<rbrakk>
\<Longrightarrow> \<turnstile> (AnnCond1 r b c1 c2) q"
| AnnCond2: "\<lbrakk> r \<inter> b \<subseteq> pre c; \<turnstile> c q; r \<inter> -b \<subseteq> q \<rbrakk> \<Longrightarrow> \<turnstile> (AnnCond2 r b c) q"
-
-| AnnWhile: "\<lbrakk> r \<subseteq> i; i \<inter> b \<subseteq> pre c; \<turnstile> c i; i \<inter> -b \<subseteq> q \<rbrakk>
+
+| AnnWhile: "\<lbrakk> r \<subseteq> i; i \<inter> b \<subseteq> pre c; \<turnstile> c i; i \<inter> -b \<subseteq> q \<rbrakk>
\<Longrightarrow> \<turnstile> (AnnWhile r b i c) q"
-
+
| AnnAwait: "\<lbrakk> atom_com c; \<parallel>- (r \<inter> b) c q \<rbrakk> \<Longrightarrow> \<turnstile> (AnnAwait r b c) q"
-
+
| AnnConseq: "\<lbrakk>\<turnstile> c q; q \<subseteq> q' \<rbrakk> \<Longrightarrow> \<turnstile> c q'"
| Parallel: "\<lbrakk> \<forall>i<length Ts. \<exists>c q. Ts!i = (Some c, q) \<and> \<turnstile> c q; interfree Ts \<rbrakk>
- \<Longrightarrow> \<parallel>- (\<Inter>i\<in>{i. i<length Ts}. pre(the(com(Ts!i))))
- Parallel Ts
+ \<Longrightarrow> \<parallel>- (\<Inter>i\<in>{i. i<length Ts}. pre(the(com(Ts!i))))
+ Parallel Ts
(\<Inter>i\<in>{i. i<length Ts}. post(Ts!i))"
| Basic: "\<parallel>- {s. f s \<in>q} (Basic f) q"
-
+
| Seq: "\<lbrakk> \<parallel>- p c1 r; \<parallel>- r c2 q \<rbrakk> \<Longrightarrow> \<parallel>- p (Seq c1 c2) q "
| Cond: "\<lbrakk> \<parallel>- (p \<inter> b) c1 q; \<parallel>- (p \<inter> -b) c2 q \<rbrakk> \<Longrightarrow> \<parallel>- p (Cond b c1 c2) q"
@@ -68,7 +68,7 @@
| Conseq: "\<lbrakk> p' \<subseteq> p; \<parallel>- p c q ; q \<subseteq> q' \<rbrakk> \<Longrightarrow> \<parallel>- p' c q'"
-section {* Soundness *}
+section \<open>Soundness\<close>
(* In the version Isabelle-10-Sep-1999: HOL: The THEN and ELSE
parts of conditional expressions (if P then x else y) are no longer
simplified. (This allows the simplifier to unfold recursive
@@ -95,9 +95,9 @@
lemmas While = oghoare_ann_hoare.While
lemmas Conseq = oghoare_ann_hoare.Conseq
-subsection {* Soundness of the System for Atomic Programs *}
+subsection \<open>Soundness of the System for Atomic Programs\<close>
-lemma Basic_ntran [rule_format]:
+lemma Basic_ntran [rule_format]:
"(Basic f, s) -Pn\<rightarrow> (Parallel Ts, t) \<longrightarrow> All_None Ts \<longrightarrow> t = f s"
apply(induct "n")
apply(simp (no_asm))
@@ -109,33 +109,33 @@
apply(simp (no_asm) add: L3_5v_lemma3)
apply(simp (no_asm) add: L3_5iv L3_5ii Parallel_empty)
apply(rule conjI)
- apply (blast dest: L3_5i)
+ apply (blast dest: L3_5i)
apply(simp add: SEM_def sem_def id_def)
-apply (blast dest: Basic_ntran rtrancl_imp_UN_relpow)
+apply (blast dest: Basic_ntran rtrancl_imp_UN_relpow)
done
-lemma atom_hoare_sound [rule_format]:
+lemma atom_hoare_sound [rule_format]:
" \<parallel>- p c q \<longrightarrow> atom_com(c) \<longrightarrow> \<parallel>= p c q"
apply (unfold com_validity_def)
apply(rule oghoare_induct)
apply simp_all
---{*Basic*}
+--\<open>Basic\<close>
apply(simp add: SEM_def sem_def)
apply(fast dest: rtrancl_imp_UN_relpow Basic_ntran)
---{* Seq *}
+--\<open>Seq\<close>
apply(rule impI)
apply(rule subset_trans)
prefer 2 apply simp
apply(simp add: L3_5ii L3_5i)
---{* Cond *}
+--\<open>Cond\<close>
apply(simp add: L3_5iv)
---{* While *}
- apply (force simp add: L3_5v dest: SEM_fwhile)
---{* Conseq *}
+--\<open>While\<close>
+ apply (force simp add: L3_5v dest: SEM_fwhile)
+--\<open>Conseq\<close>
apply(force simp add: SEM_def sem_def)
done
-
-subsection {* Soundness of the System for Component Programs *}
+
+subsection \<open>Soundness of the System for Component Programs\<close>
inductive_cases ann_transition_cases:
"(None,s) -1\<rightarrow> (c', s')"
@@ -146,17 +146,17 @@
"(Some (AnnWhile r b I c), s) -1\<rightarrow> (c', s')"
"(Some (AnnAwait r b c),s) -1\<rightarrow> (c', s')"
-text {* Strong Soundness for Component Programs:*}
+text \<open>Strong Soundness for Component Programs:\<close>
lemma ann_hoare_case_analysis [rule_format]: "\<turnstile> C q' \<longrightarrow>
- ((\<forall>r f. C = AnnBasic r f \<longrightarrow> (\<exists>q. r \<subseteq> {s. f s \<in> q} \<and> q \<subseteq> q')) \<and>
- (\<forall>c0 c1. C = AnnSeq c0 c1 \<longrightarrow> (\<exists>q. q \<subseteq> q' \<and> \<turnstile> c0 pre c1 \<and> \<turnstile> c1 q)) \<and>
- (\<forall>r b c1 c2. C = AnnCond1 r b c1 c2 \<longrightarrow> (\<exists>q. q \<subseteq> q' \<and>
- r \<inter> b \<subseteq> pre c1 \<and> \<turnstile> c1 q \<and> r \<inter> -b \<subseteq> pre c2 \<and> \<turnstile> c2 q)) \<and>
- (\<forall>r b c. C = AnnCond2 r b c \<longrightarrow>
- (\<exists>q. q \<subseteq> q' \<and> r \<inter> b \<subseteq> pre c \<and> \<turnstile> c q \<and> r \<inter> -b \<subseteq> q)) \<and>
- (\<forall>r i b c. C = AnnWhile r b i c \<longrightarrow>
- (\<exists>q. q \<subseteq> q' \<and> r \<subseteq> i \<and> i \<inter> b \<subseteq> pre c \<and> \<turnstile> c i \<and> i \<inter> -b \<subseteq> q)) \<and>
+ ((\<forall>r f. C = AnnBasic r f \<longrightarrow> (\<exists>q. r \<subseteq> {s. f s \<in> q} \<and> q \<subseteq> q')) \<and>
+ (\<forall>c0 c1. C = AnnSeq c0 c1 \<longrightarrow> (\<exists>q. q \<subseteq> q' \<and> \<turnstile> c0 pre c1 \<and> \<turnstile> c1 q)) \<and>
+ (\<forall>r b c1 c2. C = AnnCond1 r b c1 c2 \<longrightarrow> (\<exists>q. q \<subseteq> q' \<and>
+ r \<inter> b \<subseteq> pre c1 \<and> \<turnstile> c1 q \<and> r \<inter> -b \<subseteq> pre c2 \<and> \<turnstile> c2 q)) \<and>
+ (\<forall>r b c. C = AnnCond2 r b c \<longrightarrow>
+ (\<exists>q. q \<subseteq> q' \<and> r \<inter> b \<subseteq> pre c \<and> \<turnstile> c q \<and> r \<inter> -b \<subseteq> q)) \<and>
+ (\<forall>r i b c. C = AnnWhile r b i c \<longrightarrow>
+ (\<exists>q. q \<subseteq> q' \<and> r \<subseteq> i \<and> i \<inter> b \<subseteq> pre c \<and> \<turnstile> c i \<and> i \<inter> -b \<subseteq> q)) \<and>
(\<forall>r b c. C = AnnAwait r b c \<longrightarrow> (\<exists>q. q \<subseteq> q' \<and> \<parallel>- (r \<inter> b) c q)))"
apply(rule ann_hoare_induct)
apply simp_all
@@ -169,16 +169,16 @@
apply force
done
-lemma Strong_Soundness_aux_aux [rule_format]:
- "(co, s) -1\<rightarrow> (co', t) \<longrightarrow> (\<forall>c. co = Some c \<longrightarrow> s\<in> pre c \<longrightarrow>
+lemma Strong_Soundness_aux_aux [rule_format]:
+ "(co, s) -1\<rightarrow> (co', t) \<longrightarrow> (\<forall>c. co = Some c \<longrightarrow> s\<in> pre c \<longrightarrow>
(\<forall>q. \<turnstile> c q \<longrightarrow> (if co' = None then t\<in>q else t \<in> pre(the co') \<and> \<turnstile> (the co') q )))"
apply(rule ann_transition_transition.induct [THEN conjunct1])
-apply simp_all
---{* Basic *}
+apply simp_all
+--\<open>Basic\<close>
apply clarify
apply(frule ann_hoare_case_analysis)
apply force
---{* Seq *}
+--\<open>Seq\<close>
apply clarify
apply(frule ann_hoare_case_analysis,simp)
apply(fast intro: AnnConseq)
@@ -189,21 +189,21 @@
apply force
apply(rule AnnSeq,simp)
apply(fast intro: AnnConseq)
---{* Cond1 *}
+--\<open>Cond1\<close>
apply clarify
apply(frule ann_hoare_case_analysis,simp)
apply(fast intro: AnnConseq)
apply clarify
apply(frule ann_hoare_case_analysis,simp)
apply(fast intro: AnnConseq)
---{* Cond2 *}
+--\<open>Cond2\<close>
apply clarify
apply(frule ann_hoare_case_analysis,simp)
apply(fast intro: AnnConseq)
apply clarify
apply(frule ann_hoare_case_analysis,simp)
apply(fast intro: AnnConseq)
---{* While *}
+--\<open>While\<close>
apply clarify
apply(frule ann_hoare_case_analysis,simp)
apply force
@@ -214,17 +214,17 @@
apply simp
apply(rule AnnWhile)
apply simp_all
---{* Await *}
+--\<open>Await\<close>
apply(frule ann_hoare_case_analysis,simp)
apply clarify
apply(drule atom_hoare_sound)
- apply simp
+ apply simp
apply(simp add: com_validity_def SEM_def sem_def)
apply(simp add: Help All_None_def)
apply force
done
-lemma Strong_Soundness_aux: "\<lbrakk> (Some c, s) -*\<rightarrow> (co, t); s \<in> pre c; \<turnstile> c q \<rbrakk>
+lemma Strong_Soundness_aux: "\<lbrakk> (Some c, s) -*\<rightarrow> (co, t); s \<in> pre c; \<turnstile> c q \<rbrakk>
\<Longrightarrow> if co = None then t \<in> q else t \<in> pre (the co) \<and> \<turnstile> (the co) q"
apply(erule rtrancl_induct2)
apply simp
@@ -235,7 +235,7 @@
apply simp_all
done
-lemma Strong_Soundness: "\<lbrakk> (Some c, s)-*\<rightarrow>(co, t); s \<in> pre c; \<turnstile> c q \<rbrakk>
+lemma Strong_Soundness: "\<lbrakk> (Some c, s)-*\<rightarrow>(co, t); s \<in> pre c; \<turnstile> c q \<rbrakk>
\<Longrightarrow> if co = None then t\<in>q else t \<in> pre (the co)"
apply(force dest:Strong_Soundness_aux)
done
@@ -247,9 +247,9 @@
apply simp_all
done
-subsection {* Soundness of the System for Parallel Programs *}
+subsection \<open>Soundness of the System for Parallel Programs\<close>
-lemma Parallel_length_post_P1: "(Parallel Ts,s) -P1\<rightarrow> (R', t) \<Longrightarrow>
+lemma Parallel_length_post_P1: "(Parallel Ts,s) -P1\<rightarrow> (R', t) \<Longrightarrow>
(\<exists>Rs. R' = (Parallel Rs) \<and> (length Rs) = (length Ts) \<and>
(\<forall>i. i<length Ts \<longrightarrow> post(Rs ! i) = post(Ts ! i)))"
apply(erule transition_cases)
@@ -259,8 +259,8 @@
apply simp+
done
-lemma Parallel_length_post_PStar: "(Parallel Ts,s) -P*\<rightarrow> (R',t) \<Longrightarrow>
- (\<exists>Rs. R' = (Parallel Rs) \<and> (length Rs) = (length Ts) \<and>
+lemma Parallel_length_post_PStar: "(Parallel Ts,s) -P*\<rightarrow> (R',t) \<Longrightarrow>
+ (\<exists>Rs. R' = (Parallel Rs) \<and> (length Rs) = (length Ts) \<and>
(\<forall>i. i<length Ts \<longrightarrow> post(Ts ! i) = post(Rs ! i)))"
apply(erule rtrancl_induct2)
apply(simp_all)
@@ -275,7 +275,7 @@
apply auto
done
-lemma interfree_aux1 [rule_format]:
+lemma interfree_aux1 [rule_format]:
"(c,s) -1\<rightarrow> (r,t) \<longrightarrow> (interfree_aux(c1, q1, c) \<longrightarrow> interfree_aux(c1, q1, r))"
apply (rule ann_transition_transition.induct [THEN conjunct1])
apply(safe)
@@ -285,13 +285,13 @@
apply force+
done
-lemma interfree_aux2 [rule_format]:
+lemma interfree_aux2 [rule_format]:
"(c,s) -1\<rightarrow> (r,t) \<longrightarrow> (interfree_aux(c, q, a) \<longrightarrow> interfree_aux(r, q, a) )"
apply (rule ann_transition_transition.induct [THEN conjunct1])
apply(force simp add:interfree_aux_def)+
done
-lemma interfree_lemma: "\<lbrakk> (Some c, s) -1\<rightarrow> (r, t);interfree Ts ; i<length Ts;
+lemma interfree_lemma: "\<lbrakk> (Some c, s) -1\<rightarrow> (r, t);interfree Ts ; i<length Ts;
Ts!i = (Some c, q) \<rbrakk> \<Longrightarrow> interfree (Ts[i:= (r, q)])"
apply(simp add: interfree_def)
apply clarify
@@ -302,10 +302,10 @@
apply(force elim: interfree_aux2 simp add:nth_list_update)
done
-text {* Strong Soundness Theorem for Parallel Programs:*}
+text \<open>Strong Soundness Theorem for Parallel Programs:\<close>
-lemma Parallel_Strong_Soundness_Seq_aux:
- "\<lbrakk>interfree Ts; i<length Ts; com(Ts ! i) = Some(AnnSeq c0 c1) \<rbrakk>
+lemma Parallel_Strong_Soundness_Seq_aux:
+ "\<lbrakk>interfree Ts; i<length Ts; com(Ts ! i) = Some(AnnSeq c0 c1) \<rbrakk>
\<Longrightarrow> interfree (Ts[i:=(Some c0, pre c1)])"
apply(simp add: interfree_def)
apply clarify
@@ -317,14 +317,14 @@
apply simp
done
-lemma Parallel_Strong_Soundness_Seq [rule_format (no_asm)]:
- "\<lbrakk> \<forall>i<length Ts. (if com(Ts!i) = None then b \<in> post(Ts!i)
- else b \<in> pre(the(com(Ts!i))) \<and> \<turnstile> the(com(Ts!i)) post(Ts!i));
- com(Ts ! i) = Some(AnnSeq c0 c1); i<length Ts; interfree Ts \<rbrakk> \<Longrightarrow>
- (\<forall>ia<length Ts. (if com(Ts[i:=(Some c0, pre c1)]! ia) = None
- then b \<in> post(Ts[i:=(Some c0, pre c1)]! ia)
- else b \<in> pre(the(com(Ts[i:=(Some c0, pre c1)]! ia))) \<and>
- \<turnstile> the(com(Ts[i:=(Some c0, pre c1)]! ia)) post(Ts[i:=(Some c0, pre c1)]! ia)))
+lemma Parallel_Strong_Soundness_Seq [rule_format (no_asm)]:
+ "\<lbrakk> \<forall>i<length Ts. (if com(Ts!i) = None then b \<in> post(Ts!i)
+ else b \<in> pre(the(com(Ts!i))) \<and> \<turnstile> the(com(Ts!i)) post(Ts!i));
+ com(Ts ! i) = Some(AnnSeq c0 c1); i<length Ts; interfree Ts \<rbrakk> \<Longrightarrow>
+ (\<forall>ia<length Ts. (if com(Ts[i:=(Some c0, pre c1)]! ia) = None
+ then b \<in> post(Ts[i:=(Some c0, pre c1)]! ia)
+ else b \<in> pre(the(com(Ts[i:=(Some c0, pre c1)]! ia))) \<and>
+ \<turnstile> the(com(Ts[i:=(Some c0, pre c1)]! ia)) post(Ts[i:=(Some c0, pre c1)]! ia)))
\<and> interfree (Ts[i:= (Some c0, pre c1)])"
apply(rule conjI)
apply safe
@@ -335,20 +335,20 @@
apply(fast elim: Parallel_Strong_Soundness_Seq_aux)
done
-lemma Parallel_Strong_Soundness_aux_aux [rule_format]:
- "(Some c, b) -1\<rightarrow> (co, t) \<longrightarrow>
- (\<forall>Ts. i<length Ts \<longrightarrow> com(Ts ! i) = Some c \<longrightarrow>
- (\<forall>i<length Ts. (if com(Ts ! i) = None then b\<in>post(Ts!i)
- else b\<in>pre(the(com(Ts!i))) \<and> \<turnstile> the(com(Ts!i)) post(Ts!i))) \<longrightarrow>
- interfree Ts \<longrightarrow>
- (\<forall>j. j<length Ts \<and> i\<noteq>j \<longrightarrow> (if com(Ts!j) = None then t\<in>post(Ts!j)
+lemma Parallel_Strong_Soundness_aux_aux [rule_format]:
+ "(Some c, b) -1\<rightarrow> (co, t) \<longrightarrow>
+ (\<forall>Ts. i<length Ts \<longrightarrow> com(Ts ! i) = Some c \<longrightarrow>
+ (\<forall>i<length Ts. (if com(Ts ! i) = None then b\<in>post(Ts!i)
+ else b\<in>pre(the(com(Ts!i))) \<and> \<turnstile> the(com(Ts!i)) post(Ts!i))) \<longrightarrow>
+ interfree Ts \<longrightarrow>
+ (\<forall>j. j<length Ts \<and> i\<noteq>j \<longrightarrow> (if com(Ts!j) = None then t\<in>post(Ts!j)
else t\<in>pre(the(com(Ts!j))) \<and> \<turnstile> the(com(Ts!j)) post(Ts!j))) )"
apply(rule ann_transition_transition.induct [THEN conjunct1])
apply safe
prefer 11
apply(rule TrueI)
apply simp_all
---{* Basic *}
+--\<open>Basic\<close>
apply(erule_tac x = "i" in all_dupE, erule (1) notE impE)
apply(erule_tac x = "j" in allE , erule (1) notE impE)
apply(simp add: interfree_def)
@@ -362,15 +362,15 @@
apply clarify
apply simp
apply(erule_tac x="pre y" in ballE)
- apply(force intro: converse_rtrancl_into_rtrancl
+ apply(force intro: converse_rtrancl_into_rtrancl
simp add: com_validity_def SEM_def sem_def All_None_def)
apply(simp add:assertions_lemma)
---{* Seqs *}
+--\<open>Seqs\<close>
apply(erule_tac x = "Ts[i:=(Some c0, pre c1)]" in allE)
apply(drule Parallel_Strong_Soundness_Seq,simp+)
apply(erule_tac x = "Ts[i:=(Some c0, pre c1)]" in allE)
apply(drule Parallel_Strong_Soundness_Seq,simp+)
---{* Await *}
+--\<open>Await\<close>
apply(rule_tac x = "i" in allE , assumption , erule (1) notE impE)
apply(erule_tac x = "j" in allE , erule (1) notE impE)
apply(simp add: interfree_def)
@@ -378,28 +378,28 @@
apply(erule_tac x = "i" in allE,simp)
apply(drule_tac t = "i" in not_sym)
apply(case_tac "com(Ts ! j)=None")
- apply(force intro: converse_rtrancl_into_rtrancl simp add: interfree_aux_def
+ apply(force intro: converse_rtrancl_into_rtrancl simp add: interfree_aux_def
com_validity_def SEM_def sem_def All_None_def Help)
apply(simp add:interfree_aux_def)
apply clarify
apply simp
apply(erule_tac x="pre y" in ballE)
- apply(force intro: converse_rtrancl_into_rtrancl
+ apply(force intro: converse_rtrancl_into_rtrancl
simp add: com_validity_def SEM_def sem_def All_None_def Help)
apply(simp add:assertions_lemma)
done
-lemma Parallel_Strong_Soundness_aux [rule_format]:
+lemma Parallel_Strong_Soundness_aux [rule_format]:
"\<lbrakk>(Ts',s) -P*\<rightarrow> (Rs',t); Ts' = (Parallel Ts); interfree Ts;
- \<forall>i. i<length Ts \<longrightarrow> (\<exists>c q. (Ts ! i) = (Some c, q) \<and> s\<in>(pre c) \<and> \<turnstile> c q ) \<rbrakk> \<Longrightarrow>
- \<forall>Rs. Rs' = (Parallel Rs) \<longrightarrow> (\<forall>j. j<length Rs \<longrightarrow>
- (if com(Rs ! j) = None then t\<in>post(Ts ! j)
+ \<forall>i. i<length Ts \<longrightarrow> (\<exists>c q. (Ts ! i) = (Some c, q) \<and> s\<in>(pre c) \<and> \<turnstile> c q ) \<rbrakk> \<Longrightarrow>
+ \<forall>Rs. Rs' = (Parallel Rs) \<longrightarrow> (\<forall>j. j<length Rs \<longrightarrow>
+ (if com(Rs ! j) = None then t\<in>post(Ts ! j)
else t\<in>pre(the(com(Rs ! j))) \<and> \<turnstile> the(com(Rs ! j)) post(Ts ! j))) \<and> interfree Rs"
apply(erule rtrancl_induct2)
apply clarify
---{* Base *}
+--\<open>Base\<close>
apply force
---{* Induction step *}
+--\<open>Induction step\<close>
apply clarify
apply(drule Parallel_length_post_PStar)
apply clarify
@@ -419,9 +419,9 @@
apply simp_all
done
-lemma Parallel_Strong_Soundness:
- "\<lbrakk>(Parallel Ts, s) -P*\<rightarrow> (Parallel Rs, t); interfree Ts; j<length Rs;
- \<forall>i. i<length Ts \<longrightarrow> (\<exists>c q. Ts ! i = (Some c, q) \<and> s\<in>pre c \<and> \<turnstile> c q) \<rbrakk> \<Longrightarrow>
+lemma Parallel_Strong_Soundness:
+ "\<lbrakk>(Parallel Ts, s) -P*\<rightarrow> (Parallel Rs, t); interfree Ts; j<length Rs;
+ \<forall>i. i<length Ts \<longrightarrow> (\<exists>c q. Ts ! i = (Some c, q) \<and> s\<in>pre c \<and> \<turnstile> c q) \<rbrakk> \<Longrightarrow>
if com(Rs ! j) = None then t\<in>post(Ts ! j) else t\<in>pre (the(com(Rs ! j)))"
apply(drule Parallel_Strong_Soundness_aux)
apply simp+
@@ -431,7 +431,7 @@
apply (unfold com_validity_def)
apply(rule oghoare_induct)
apply(rule TrueI)+
---{* Parallel *}
+--\<open>Parallel\<close>
apply(simp add: SEM_def sem_def)
apply(clarify, rename_tac x y i Ts')
apply(frule Parallel_length_post_PStar)
@@ -445,19 +445,19 @@
apply(drule_tac s = "length Rs" in sym)
apply(erule allE, erule impE, assumption)
apply(force dest: nth_mem simp add: All_None_def)
---{* Basic *}
+--\<open>Basic\<close>
apply(simp add: SEM_def sem_def)
apply(force dest: rtrancl_imp_UN_relpow Basic_ntran)
---{* Seq *}
+--\<open>Seq\<close>
apply(rule subset_trans)
prefer 2 apply assumption
apply(simp add: L3_5ii L3_5i)
---{* Cond *}
+--\<open>Cond\<close>
apply(simp add: L3_5iv)
---{* While *}
+--\<open>While\<close>
apply(simp add: L3_5v)
- apply (blast dest: SEM_fwhile)
---{* Conseq *}
+ apply (blast dest: SEM_fwhile)
+--\<open>Conseq\<close>
apply(auto simp add: SEM_def sem_def)
done