diff -r 28df61d931e2 -r a455e69c31cc src/HOL/HoareParallel/OG_Hoare.thy
--- a/src/HOL/HoareParallel/OG_Hoare.thy	Wed Jul 11 11:13:08 2007 +0200
+++ b/src/HOL/HoareParallel/OG_Hoare.thy	Wed Jul 11 11:14:51 2007 +0200
@@ -36,46 +36,40 @@
   "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)) "
 
-consts ann_hoare :: "('a ann_com \<times> 'a assn) set" 
-syntax "_ann_hoare" :: "'a ann_com \<Rightarrow> 'a assn \<Rightarrow> bool"  ("(2\<turnstile> _// _)" [60,90] 45)
-translations "\<turnstile> c q" \<rightleftharpoons> "(c, q) \<in> ann_hoare"
-
-consts oghoare :: "('a assn \<times> 'a com \<times> 'a assn) set"
-syntax "_oghoare" :: "'a assn \<Rightarrow> 'a com \<Rightarrow> 'a assn \<Rightarrow> bool"  ("(3\<parallel>- _//_//_)" [90,55,90] 50)
-translations "\<parallel>- p c q" \<rightleftharpoons> "(p, c, q) \<in> oghoare"
-
-inductive oghoare ann_hoare
-intros
+inductive
+  oghoare :: "'a assn \<Rightarrow> 'a com \<Rightarrow> 'a assn \<Rightarrow> bool"  ("(3\<parallel>- _//_//_)" [90,55,90] 50)
+  and ann_hoare :: "'a ann_com \<Rightarrow> 'a assn \<Rightarrow> bool"  ("(2\<turnstile> _// _)" [60,90] 45)
+where
   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"
+| 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"
+| 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"
+| 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'"
+| 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>
+| 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 
                   (\<Inter>i\<in>{i. i<length Ts}. post(Ts!i))"
 
-  Basic:   "\<parallel>- {s. f s \<in>q} (Basic f) q"
+| 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 "
+| 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"
+| Cond:   "\<lbrakk> \<parallel>- (p \<inter> b) c1 q; \<parallel>- (p \<inter> -b) c2 q \<rbrakk> \<Longrightarrow> \<parallel>- p (Cond b c1 c2) q"
 
-  While:  "\<lbrakk> \<parallel>- (p \<inter> b) c p \<rbrakk> \<Longrightarrow> \<parallel>- p (While b i c) (p \<inter> -b)"
+| While:  "\<lbrakk> \<parallel>- (p \<inter> b) c p \<rbrakk> \<Longrightarrow> \<parallel>- p (While b i c) (p \<inter> -b)"
 
-  Conseq: "\<lbrakk> p' \<subseteq> p; \<parallel>- p c q ; q \<subseteq> q' \<rbrakk> \<Longrightarrow> \<parallel>- p' c q'"
+| Conseq: "\<lbrakk> p' \<subseteq> p; \<parallel>- p c q ; q \<subseteq> q' \<rbrakk> \<Longrightarrow> \<parallel>- p' c q'"
 					    
 section {* Soundness *}
 (* In the version Isabelle-10-Sep-1999: HOL: The THEN and ELSE
@@ -147,13 +141,13 @@
 subsection {* Soundness of the System for Component Programs *}
 
 inductive_cases ann_transition_cases:
-    "(None,s) -1\<rightarrow> t"
-    "(Some (AnnBasic r f),s) -1\<rightarrow> t"
-    "(Some (AnnSeq c1 c2), s) -1\<rightarrow> t" 
-    "(Some (AnnCond1 r b c1 c2), s) -1\<rightarrow> t"
-    "(Some (AnnCond2 r b c), s) -1\<rightarrow> t"
-    "(Some (AnnWhile r b I c), s) -1\<rightarrow> t"
-    "(Some (AnnAwait r b c),s) -1\<rightarrow> t"
+    "(None,s) -1\<rightarrow> (c', s')"
+    "(Some (AnnBasic r f),s) -1\<rightarrow> (c', s')"
+    "(Some (AnnSeq c1 c2), s) -1\<rightarrow> (c', s')"
+    "(Some (AnnCond1 r b c1 c2), s) -1\<rightarrow> (c', s')"
+    "(Some (AnnCond2 r b c), s) -1\<rightarrow> (c', s')"
+    "(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:*}
 
@@ -174,7 +168,7 @@
 apply(clarify,simp,clarify,rule_tac x=qa in exI,fast)
 done
 
-lemma Help: "(transition \<inter> {(v,v,u). True}) = (transition)"
+lemma Help: "(transition \<inter> {(x,y). True}) = (transition)"
 apply force
 done
 
@@ -412,7 +406,7 @@
 apply clarify
 apply(drule Parallel_length_post_PStar)
 apply clarify
-apply (ind_cases "(Parallel Ts, s) -P1\<rightarrow> (Parallel Rs, t)")
+apply (ind_cases "(Parallel Ts, s) -P1\<rightarrow> (Parallel Rs, t)" for Ts s Rs t)
 apply(rule conjI)
  apply clarify
  apply(case_tac "i=j")