--- a/src/HOL/HoareParallel/RG_Hoare.thy Wed Jul 11 11:13:08 2007 +0200
+++ b/src/HOL/HoareParallel/RG_Hoare.thy Wed Jul 11 11:14:51 2007 +0200
@@ -11,36 +11,31 @@
stable :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool"
"stable \<equiv> \<lambda>f g. (\<forall>x y. x \<in> f \<longrightarrow> (x, y) \<in> g \<longrightarrow> y \<in> f)"
-consts rghoare :: "('a rgformula) set"
-syntax
- "_rghoare" :: "['a com, 'a set, ('a \<times> 'a) set, ('a \<times> 'a) set, 'a set] \<Rightarrow> bool"
- ("\<turnstile> _ sat [_, _, _, _]" [60,0,0,0,0] 45)
-translations
- "\<turnstile> P sat [pre, rely, guar, post]" \<rightleftharpoons> "(P, pre, rely, guar, post) \<in> rghoare"
-
-inductive rghoare
-intros
+inductive
+ rghoare :: "['a com, 'a set, ('a \<times> 'a) set, ('a \<times> 'a) set, 'a set] \<Rightarrow> bool"
+ ("\<turnstile> _ sat [_, _, _, _]" [60,0,0,0,0] 45)
+where
Basic: "\<lbrakk> pre \<subseteq> {s. f s \<in> post}; {(s,t). s \<in> pre \<and> (t=f s \<or> t=s)} \<subseteq> guar;
stable pre rely; stable post rely \<rbrakk>
\<Longrightarrow> \<turnstile> Basic f sat [pre, rely, guar, post]"
- Seq: "\<lbrakk> \<turnstile> P sat [pre, rely, guar, mid]; \<turnstile> Q sat [mid, rely, guar, post] \<rbrakk>
+| Seq: "\<lbrakk> \<turnstile> P sat [pre, rely, guar, mid]; \<turnstile> Q sat [mid, rely, guar, post] \<rbrakk>
\<Longrightarrow> \<turnstile> Seq P Q sat [pre, rely, guar, post]"
- Cond: "\<lbrakk> stable pre rely; \<turnstile> P1 sat [pre \<inter> b, rely, guar, post];
+| Cond: "\<lbrakk> stable pre rely; \<turnstile> P1 sat [pre \<inter> b, rely, guar, post];
\<turnstile> P2 sat [pre \<inter> -b, rely, guar, post]; \<forall>s. (s,s)\<in>guar \<rbrakk>
\<Longrightarrow> \<turnstile> Cond b P1 P2 sat [pre, rely, guar, post]"
- While: "\<lbrakk> stable pre rely; (pre \<inter> -b) \<subseteq> post; stable post rely;
+| While: "\<lbrakk> stable pre rely; (pre \<inter> -b) \<subseteq> post; stable post rely;
\<turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s,s)\<in>guar \<rbrakk>
\<Longrightarrow> \<turnstile> While b P sat [pre, rely, guar, post]"
- Await: "\<lbrakk> stable pre rely; stable post rely;
+| 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>
\<Longrightarrow> \<turnstile> Await b P sat [pre, rely, guar, post]"
- Conseq: "\<lbrakk> pre \<subseteq> pre'; rely \<subseteq> rely'; guar' \<subseteq> guar; post' \<subseteq> post;
+| Conseq: "\<lbrakk> pre \<subseteq> pre'; rely \<subseteq> rely'; guar' \<subseteq> guar; post' \<subseteq> post;
\<turnstile> P sat [pre', rely', guar', post'] \<rbrakk>
\<Longrightarrow> \<turnstile> P sat [pre, rely, guar, post]"
@@ -60,14 +55,10 @@
types 'a par_rgformula = "('a rgformula) list \<times> 'a set \<times> ('a \<times> 'a) set \<times> ('a \<times> 'a) set \<times> 'a set"
-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)
-translations
- "\<turnstile> Ps SAT [pre, rely, guar, post]" \<rightleftharpoons> "(Ps, pre, rely, guar, post) \<in> par_rghoare"
-
-inductive par_rghoare
-intros
+inductive
+ 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)
+where
Parallel:
"\<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);
(\<Union>j\<in>{j. j<length xs}. Guar(xs!j)) \<subseteq> guar;
@@ -113,22 +104,22 @@
lemma takecptn_is_cptn [rule_format, elim!]:
"\<forall>j. c \<in> cptn \<longrightarrow> take (Suc j) c \<in> cptn"
apply(induct "c")
- apply(force elim: cptn.elims)
+ apply(force elim: cptn.cases)
apply clarify
apply(case_tac j)
apply simp
apply(rule CptnOne)
apply simp
-apply(force intro:cptn.intros elim:cptn.elims)
+apply(force intro:cptn.intros elim:cptn.cases)
done
lemma dropcptn_is_cptn [rule_format,elim!]:
"\<forall>j<length c. c \<in> cptn \<longrightarrow> drop j c \<in> cptn"
apply(induct "c")
- apply(force elim: cptn.elims)
+ apply(force elim: cptn.cases)
apply clarify
apply(case_tac j,simp+)
-apply(erule cptn.elims)
+apply(erule cptn.cases)
apply simp
apply force
apply force
@@ -137,20 +128,20 @@
lemma takepar_cptn_is_par_cptn [rule_format,elim]:
"\<forall>j. c \<in> par_cptn \<longrightarrow> take (Suc j) c \<in> par_cptn"
apply(induct "c")
- apply(force elim: cptn.elims)
+ apply(force elim: cptn.cases)
apply clarify
apply(case_tac j,simp)
apply(rule ParCptnOne)
-apply(force intro:par_cptn.intros elim:par_cptn.elims)
+apply(force intro:par_cptn.intros elim:par_cptn.cases)
done
lemma droppar_cptn_is_par_cptn [rule_format]:
"\<forall>j<length c. c \<in> par_cptn \<longrightarrow> drop j c \<in> par_cptn"
apply(induct "c")
- apply(force elim: par_cptn.elims)
+ apply(force elim: par_cptn.cases)
apply clarify
apply(case_tac j,simp+)
-apply(erule par_cptn.elims)
+apply(erule par_cptn.cases)
apply simp
apply force
apply force
@@ -165,16 +156,16 @@
"\<forall>s. (None, s)#xs \<in> cptn \<longrightarrow> (\<forall>i<length xs. ((None, s)#xs)!i -e\<rightarrow> xs!i)"
apply(induct xs,simp+)
apply clarify
-apply(erule cptn.elims,simp)
+apply(erule cptn.cases,simp)
apply simp
apply(case_tac i,simp)
apply(rule Env)
apply simp
-apply(force elim:ctran.elims)
+apply(force elim:ctran.cases)
done
lemma cptn_not_empty [simp]:"[] \<notin> cptn"
-apply(force elim:cptn.elims)
+apply(force elim:cptn.cases)
done
lemma etran_or_ctran [rule_format]:
@@ -183,7 +174,7 @@
\<longrightarrow> x!i -e\<rightarrow> x!Suc i"
apply(induct x,simp)
apply clarify
-apply(erule cptn.elims,simp)
+apply(erule cptn.cases,simp)
apply(case_tac i,simp)
apply(rule Env)
apply simp
@@ -202,10 +193,10 @@
apply(induct x)
apply simp
apply clarify
-apply(erule cptn.elims,simp)
+apply(erule cptn.cases,simp)
apply(case_tac i,simp+)
apply(case_tac i,simp)
- apply(force elim:etran.elims)
+ apply(force elim:etran.cases)
apply simp
done
@@ -221,7 +212,7 @@
"\<lbrakk> (None, s) # xs \<in>cptn; i<length xs\<rbrakk> \<Longrightarrow> \<not> ((None, s) # xs) ! i -c\<rightarrow> xs ! i"
apply(frule not_ctran_None,simp)
apply(case_tac i,simp)
- apply(force elim:etran.elims)
+ apply(force elim:etranE)
apply simp
apply(rule etran_or_ctran2_disjI2,simp_all)
apply(force intro:tl_of_cptn_is_cptn)
@@ -241,9 +232,9 @@
(\<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
- apply(force elim:cptn.elims)
+ apply(force elim:cptn.cases)
apply clarify
-apply(erule cptn.elims,simp)
+apply(erule cptn.cases,simp)
apply simp
apply(case_tac k,simp,simp)
apply(case_tac j,simp)
@@ -274,7 +265,7 @@
apply(case_tac k,simp,simp)
apply(case_tac j)
apply(erule_tac x=0 and P="\<lambda>j. (?H j) \<longrightarrow> (?J j)\<in>etran" in allE,simp)
- apply(erule etran.elims,simp)
+ apply(erule etran.cases,simp)
apply(erule_tac x="nata" in allE)
apply(erule_tac x="nat" and P="\<lambda>j. (?s\<le>j) \<longrightarrow> (?J j)" in allE,simp)
apply(subgoal_tac "(\<forall>i. i < length xs \<longrightarrow> ((Q, t) # xs) ! i -e\<rightarrow> xs ! i \<longrightarrow> (snd (((Q, t) # xs) ! i), snd (xs ! i)) \<in> rely)")
@@ -295,7 +286,7 @@
apply(induct x,simp)
apply simp
apply clarify
-apply(erule cptn.elims,simp)
+apply(erule cptn.cases,simp)
apply(case_tac i,simp+)
apply clarify
apply(case_tac j,simp)
@@ -305,12 +296,12 @@
apply simp
apply(case_tac i)
apply(case_tac j,simp,simp)
- apply(erule ctran.elims,simp_all)
+ apply(erule ctran.cases,simp_all)
apply(force elim: not_ctran_None)
-apply(ind_cases "((Some (Basic f), sa), Q, t) \<in> ctran")
+apply(ind_cases "((Some (Basic f), sa), Q, t) \<in> ctran" for sa Q t)
apply simp
apply(drule_tac i=nat in not_ctran_None,simp)
-apply(erule etran.elims,simp)
+apply(erule etranE,simp)
done
lemma exists_ctran_Basic_None [rule_format]:
@@ -319,7 +310,7 @@
apply(induct x,simp)
apply simp
apply clarify
-apply(erule cptn.elims,simp)
+apply(erule cptn.cases,simp)
apply(case_tac i,simp,simp)
apply(erule_tac x=nat in allE,simp)
apply clarify
@@ -349,7 +340,7 @@
apply clarify
apply(drule_tac s="Some (Basic f)" in sym,simp)
apply(thin_tac "\<forall>j. ?H j")
- apply(force elim:ctran.elims)
+ apply(force elim:ctran.cases)
apply clarify
apply(simp add:cp_def)
apply clarify
@@ -368,7 +359,7 @@
apply simp
apply(drule_tac s="Some (Basic f)" in sym,simp)
apply(case_tac "x!Suc j",simp)
-apply(rule ctran.elims,simp)
+apply(rule ctran.cases,simp)
apply(simp_all)
apply(drule_tac c=sa in subsetD,simp)
apply clarify
@@ -389,7 +380,7 @@
(\<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)
+apply(erule cptn.cases,simp)
apply(case_tac i,simp+)
apply clarify
apply(case_tac j,simp)
@@ -399,11 +390,11 @@
apply simp
apply(case_tac i)
apply(case_tac j,simp,simp)
- apply(erule ctran.elims,simp_all)
+ apply(erule ctran.cases,simp_all)
apply(force elim: not_ctran_None)
-apply(ind_cases "((Some (Await b c), sa), Q, t) \<in> ctran",simp)
+apply(ind_cases "((Some (Await b c), sa), Q, t) \<in> ctran" for sa Q t,simp)
apply(drule_tac i=nat in not_ctran_None,simp)
-apply(erule etran.elims,simp)
+apply(erule etranE,simp)
done
lemma exists_ctran_Await_None [rule_format]:
@@ -411,7 +402,7 @@
\<longrightarrow> i<length x \<longrightarrow> fst(x!i)=None \<longrightarrow> (\<exists>j<i. x!j -c\<rightarrow> x!Suc j)"
apply(induct x,simp+)
apply clarify
-apply(erule cptn.elims,simp)
+apply(erule cptn.cases,simp)
apply(case_tac i,simp+)
apply(erule_tac x=nat in allE,simp)
apply clarify
@@ -440,7 +431,7 @@
apply force
apply(simp add:cp_def)
apply(case_tac l)
- apply(force elim:cptn.elims)
+ apply(force elim:cptn.cases)
apply simp
apply(erule CptnComp)
apply clarify
@@ -466,7 +457,7 @@
apply(erule_tac i=i in unique_ctran_Await,force,simp_all)
apply(simp add:cp_def)
--{* here starts the different part. *}
- apply(erule ctran.elims,simp_all)
+ apply(erule ctran.cases,simp_all)
apply(drule Star_imp_cptn)
apply clarify
apply(erule_tac x=sa in allE)
@@ -476,7 +467,7 @@
apply (simp add:cp_def)
apply clarify
apply(erule_tac x=ia and P="\<lambda>i. ?H i \<longrightarrow> (?J i,?I i)\<in>ctran" in allE,simp)
- apply(erule etran.elims,simp)
+ apply(erule etranE,simp)
apply simp
apply clarify
apply(simp add:cp_def)
@@ -496,7 +487,7 @@
apply simp
apply(drule_tac s="Some (Await b P)" in sym,simp)
apply(case_tac "x!Suc j",simp)
-apply(rule ctran.elims,simp)
+apply(rule ctran.cases,simp)
apply(simp_all)
apply(drule Star_imp_cptn)
apply clarify
@@ -507,7 +498,7 @@
apply (simp add:cp_def)
apply clarify
apply(erule_tac x=i and P="\<lambda>i. ?H i \<longrightarrow> (?J i,?I i)\<in>ctran" in allE,simp)
- apply(erule etran.elims,simp)
+ apply(erule etranE,simp)
apply simp
apply clarify
apply(frule_tac j="Suc j" and k="length x - 1" and p=post in stability,simp_all)
@@ -544,7 +535,7 @@
apply (simp add:assum_def)
apply(frule_tac j=0 and k="m" and p=pre in stability,simp+)
apply(erule_tac m="Suc m" in etran_or_ctran,simp+)
-apply(erule ctran.elims,simp_all)
+apply(erule ctran.cases,simp_all)
apply(erule_tac x="sa" in allE)
apply(drule_tac c="drop (Suc m) x" in subsetD)
apply simp
@@ -616,7 +607,7 @@
apply(simp (no_asm_use) add:lift_def)
apply clarify
apply(erule_tac x="Suc i" in allE, simp)
- apply(ind_cases "((Some (Seq Pa Q), sa), None, t) \<in> ctran")
+ apply(ind_cases "((Some (Seq Pa Q), sa), None, t) \<in> ctran" for Pa sa t)
apply(rule_tac x="(Some P, sa) # xs" in exI, simp add:cptn_iff_cptn_mod lift_def)
apply(erule_tac x="length xs" in allE, simp)
apply(simp only:Cons_lift_append)
@@ -649,7 +640,7 @@
apply(rule conjI,erule CptnEnv)
apply(simp (no_asm_use) add:lift_def)
apply(rule_tac x=ys in exI,simp)
-apply(ind_cases "((Some (Seq Pa Q), sa), t) \<in> ctran")
+apply(ind_cases "((Some (Seq Pa Q), sa), t) \<in> ctran" for Pa sa t)
apply simp
apply(rule_tac x="(Some Pa, sa)#[(None, ta)]" in exI,simp)
apply(rule conjI)
@@ -724,7 +715,7 @@
apply(erule_tac P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE,erule impE, assumption)
apply(simp add:snd_lift)
apply(erule mp)
- apply(force elim:etran.elims intro:Env simp add:lift_def)
+ apply(force elim:etranE intro:Env simp add:lift_def)
apply(simp add:comm_def)
apply(rule conjI)
apply clarify
@@ -766,7 +757,7 @@
back
apply(simp add:snd_lift)
apply(erule mp)
- apply(force elim:etran.elims intro:Env simp add:lift_def)
+ apply(force elim:etranE intro:Env simp add:lift_def)
apply simp
apply clarify
apply(erule_tac x="snd(xs!m)" in allE)
@@ -786,7 +777,7 @@
apply (case_tac i, (simp add:snd_lift)+)
apply(erule mp)
apply(case_tac "xs!m")
- apply(force elim:etran.elims intro:Env simp add:lift_def)
+ apply(force elim:etran.cases intro:Env simp add:lift_def)
apply simp
apply simp
apply clarify
@@ -866,7 +857,7 @@
apply simp
apply(simp add:Cons_lift_append nth_append snd_lift del:map.simps)
apply(erule mp)
- apply(erule etran.elims,simp)
+ apply(erule etranE,simp)
apply(case_tac "fst(((Some P, s) # xs) ! i)")
apply(force intro:Env simp add:lift_def)
apply(force intro:Env simp add:lift_def)
@@ -900,7 +891,7 @@
apply(erule mp)
apply(erule tl_of_assum_in_assum,simp)
--{* While-None *}
-apply(ind_cases "((Some (While b P), s), None, t) \<in> ctran")
+apply(ind_cases "((Some (While b P), s), None, t) \<in> ctran" for s t)
apply(simp add:comm_def)
apply(simp add:cptn_iff_cptn_mod [THEN sym])
apply(rule conjI,clarify)
@@ -909,7 +900,7 @@
apply(rule conjI, clarify)
apply(case_tac i,simp,simp)
apply(force simp add:not_ctran_None2)
-apply(subgoal_tac "\<forall>i. Suc i < length ((None, sa) # xs) \<longrightarrow> (((None, sa) # xs) ! i, ((None, sa) # xs) ! Suc i)\<in> etran")
+apply(subgoal_tac "\<forall>i. Suc i < length ((None, t) # xs) \<longrightarrow> (((None, t) # xs) ! i, ((None, t) # xs) ! Suc i)\<in> etran")
prefer 2
apply clarify
apply(rule_tac m="length ((None, s) # xs)" in etran_or_ctran,simp+)
@@ -934,7 +925,7 @@
apply(case_tac "fst(((Some P, sa) # xs) ! i)")
apply(case_tac "((Some P, sa) # xs) ! i")
apply (simp add:lift_def)
- apply(ind_cases "(Some (While b P), ba) -c\<rightarrow> t")
+ apply(ind_cases "(Some (While b P), ba) -c\<rightarrow> t" for ba t)
apply simp
apply simp
apply(simp add:snd_lift del:map.simps)
@@ -946,9 +937,9 @@
apply(erule_tac x="Suc ia" in allE,simp add:snd_lift del:map.simps)
apply(erule mp)
apply(case_tac "fst(((Some P, sa) # xs) ! ia)")
- apply(erule etran.elims,simp add:lift_def)
+ apply(erule etranE,simp add:lift_def)
apply(rule Env)
- apply(erule etran.elims,simp add:lift_def)
+ apply(erule etranE,simp add:lift_def)
apply(rule Env)
apply (simp add:comm_def del:map.simps)
apply clarify
@@ -986,7 +977,7 @@
apply(case_tac "fst(((Some P, sa) # xs) ! i)")
apply(case_tac "((Some P, sa) # xs) ! i")
apply (simp add:lift_def del:last.simps)
- apply(ind_cases "(Some (While b P), ba) -c\<rightarrow> t")
+ apply(ind_cases "(Some (While b P), ba) -c\<rightarrow> t" for ba t)
apply simp
apply simp
apply(simp add:snd_lift del:map.simps last.simps)
@@ -998,9 +989,9 @@
apply clarify
apply(erule_tac x="Suc ia" in allE,simp add:nth_append snd_lift del:map.simps last.simps, erule mp)
apply(case_tac "fst(((Some P, sa) # xs) ! ia)")
- apply(erule etran.elims,simp add:lift_def)
+ apply(erule etranE,simp add:lift_def)
apply(rule Env)
- apply(erule etran.elims,simp add:lift_def)
+ apply(erule etranE,simp add:lift_def)
apply(rule Env)
apply (simp add:comm_def del:map.simps)
apply clarify
@@ -1158,9 +1149,9 @@
--{* a c-tran in some @{text "\<sigma>_{ib}"} *}
apply clarify
apply(case_tac "i=ib",simp)
- apply(erule etran.elims,simp)
+ apply(erule etranE,simp)
apply(erule_tac x="ib" and P="\<lambda>i. ?H i \<longrightarrow> (?I i) \<or> (?J i)" in allE)
- apply (erule etran.elims)
+ apply (erule etranE)
apply(case_tac "ia=m",simp)
apply simp
apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (\<forall> i. ?P i j)" in allE)
@@ -1198,7 +1189,7 @@
apply(force simp add:same_state_def par_assum_def)
apply clarify
apply(case_tac "i=ia",simp)
- apply(erule etran.elims,simp)
+ apply(erule etranE,simp)
apply(erule_tac x="ia" and P="\<lambda>i. ?H i \<longrightarrow> (?I i) \<or> (?J i)" in allE,simp)
apply(erule_tac x=j and P="\<lambda>j. \<forall>i. ?S j i \<longrightarrow> (?I j i, ?H j i)\<in> ctran \<longrightarrow> (?P i j)" in allE)
apply(erule_tac x=ia and P="\<lambda>j. ?S j \<longrightarrow> (?I j, ?H j)\<in> ctran \<longrightarrow> (?P j)" in allE)
@@ -1237,7 +1228,7 @@
apply clarify
apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> fst(?I j)=(?J j)" in all_dupE)
apply(erule_tac x="Suc i" and P="\<lambda>j. ?H j \<longrightarrow> fst(?I j)=(?J j)" in allE)
-apply(erule par_ctran.elims,simp)
+apply(erule par_ctranE,simp)
apply(erule_tac x=i and P="\<lambda>j. \<forall>i. ?S j i \<longrightarrow> (?I j i, ?H j i)\<in> ctran \<longrightarrow> (?P i j)" in allE)
apply(erule_tac x=ia and P="\<lambda>j. ?S j \<longrightarrow> (?I j, ?H j)\<in> ctran \<longrightarrow> (?P j)" in allE)
apply(rule_tac x=ia in exI)
@@ -1255,7 +1246,7 @@
done
lemma parcptn_not_empty [simp]:"[] \<notin> par_cptn"
-apply(force elim:par_cptn.elims)
+apply(force elim:par_cptn.cases)
done
lemma five:
@@ -1336,12 +1327,12 @@
apply(case_tac list,simp,simp)
apply(case_tac i)
apply(simp add:par_cp_def ParallelCom_def)
- apply(erule par_ctran.elims,simp)
+ apply(erule par_ctranE,simp)
apply(simp add:par_cp_def ParallelCom_def)
apply clarify
-apply(erule par_cptn.elims,simp)
+apply(erule par_cptn.cases,simp)
apply simp
-apply(erule par_ctran.elims)
+apply(erule par_ctranE)
back
apply simp
done