# HG changeset patch
# User berghofe
# Date 1210150761 -7200
# Node ID 067cceb36e2602f1e1a4719d8f2b115319b8a4de
# Parent  255a347eae4379a0601747915904d798019875dd
Rephrased proof of ann_hoare_case_analysis, to avoid problems with HO unification

diff -r 255a347eae43 -r 067cceb36e26 src/HOL/HoareParallel/OG_Hoare.thy
--- a/src/HOL/HoareParallel/OG_Hoare.thy	Wed May 07 10:59:20 2008 +0200
+++ b/src/HOL/HoareParallel/OG_Hoare.thy	Wed May 07 10:59:21 2008 +0200
@@ -151,7 +151,8 @@
 
 text {* Strong Soundness for Component Programs:*}
 
-lemma ann_hoare_case_analysis [rule_format]: "\<turnstile> C q' \<longrightarrow>  
+lemma ann_hoare_case_analysis [rule_format]: 
+  defines I: "I \<equiv> \<lambda>C q'.
   ((\<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>  
@@ -161,8 +162,9 @@
   (\<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)))"
+  shows "\<turnstile> C q' \<longrightarrow> I C q'"
 apply(rule ann_hoare_induct)
-apply simp_all
+apply (simp_all add: I)
  apply(rule_tac x=q in exI,simp)+
 apply(rule conjI,clarify,simp,clarify,rule_tac x=qa in exI,fast)+
 apply(clarify,simp,clarify,rule_tac x=qa in exI,fast)
@@ -439,7 +441,7 @@
       apply clarify
       apply(frule Parallel_length_post_PStar)
       apply clarify
-      apply(drule_tac j=i in Parallel_Strong_Soundness)
+      apply(drule_tac j=xa in Parallel_Strong_Soundness)
          apply clarify
         apply simp
        apply force