src/HOL/HoareParallel/RG_Hoare.thy

 apply clarify
 apply(case_tac i,simp,simp)
 apply(rule_tac x=0 in exI,simp)
 done
 
-lemma Basic_sound:
+lemma Basic_sound: 
   " \<lbrakk>pre \<subseteq> {s. f s \<in> post}; {(s, t). s \<in> pre \<and> t = f s} \<subseteq> guar; 
   stable pre rely; stable post rely\<rbrakk>
   \<Longrightarrow> \<Turnstile> Basic f sat [pre, rely, guar, post]"
 apply(unfold com_validity_def)
 apply clarify

 apply clarify
 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(simp_all)
+apply(simp_all)
 apply(drule_tac c=sa in subsetD,simp)
 apply clarify
 apply(frule_tac j="Suc j" and k="length x - 1" and p=post in stability,simp_all)
-  apply(case_tac x,simp+)
+ apply(case_tac x,simp+)
  apply(erule_tac x=i in allE)
- apply(erule_tac i=j and f=f in unique_ctran_Basic,simp_all)
+apply(erule_tac i=j and f=f in unique_ctran_Basic,simp_all)
+  apply arith+
 apply(case_tac x)
- apply(simp add:last_length)+
+apply(simp add:last_length)+
 done
 
 subsubsection{* Soundness of the Await rule *}
 
 lemma unique_ctran_Await [rule_format]: 

 apply clarify
 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(simp_all)
+apply(simp_all)
 apply(drule Star_imp_cptn) 
 apply clarify
 apply(erule_tac x=sa in allE)
 apply clarify
 apply(erule_tac x=sa in allE)

  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 simp
 apply clarify
 apply(frule_tac j="Suc j" and k="length x - 1" and p=post in stability,simp_all)
-  apply(case_tac x,simp+)
+ apply(case_tac x,simp+)
  apply(erule_tac x=i in allE)
- apply(erule_tac i=j in unique_ctran_Await,force,simp_all)
+apply(erule_tac i=j in unique_ctran_Await,force,simp_all)
+ apply arith+
 apply(case_tac x)
- apply(simp add:last_length)+
+apply(simp add:last_length)+
 done
 
 subsubsection{* Soundness of the Conditional rule *}
-
-ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
 
 lemma Cond_sound: 
   "\<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]"

  apply(frule_tac j="0" and k="length x - 1" and p=pre in stability,simp+)
      apply(case_tac x,simp+)
     apply(simp add:assum_def)
    apply(simp add:assum_def)
   apply(erule_tac m="length x" in etran_or_ctran,simp+)
-  apply(case_tac x,simp+)
  apply(case_tac x, (simp add:last_length)+)
 apply(erule exE)
 apply(drule_tac n=i and P="\<lambda>i. ?H i \<and> (?J i,?I i)\<in> ctran" in Ex_first_occurrence)
 apply clarify
 apply (simp add:assum_def)

  apply(erule_tac m="Suc m" in etran_or_ctran,simp+)
 apply(erule ctran.elims,simp_all)
  apply(erule_tac x="sa" in allE)
  apply(drule_tac c="drop (Suc m) x" in subsetD)
   apply simp
-  apply(rule conjI)
-   apply force
   apply clarify
-  apply(subgoal_tac "(Suc m) + i \<le> length x")
-   apply(subgoal_tac "(Suc m) + (Suc i) \<le> length x")
-    apply(rotate_tac -2)
-    apply simp
-    apply(erule_tac x="Suc (m + i)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE)
-    apply(subgoal_tac "Suc (Suc (m + i)) < length x",simp)
-    apply arith
-   apply arith
-  apply arith
  apply simp
  apply clarify
  apply(case_tac "i\<le>m")
   apply(drule le_imp_less_or_eq)
   apply(erule disjE)
    apply(erule_tac x=i in allE, erule impE, assumption)
    apply simp+
  apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
-  apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
-   apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
-    apply(rotate_tac -2)
-    apply simp
-    apply(erule mp)
-    apply arith
-   apply arith
-  apply arith
-  apply(case_tac "length (drop (Suc m) x)",simp)
-  apply(erule_tac x="sa" in allE)
-  back
-  apply(drule_tac c="drop (Suc m) x" in subsetD,simp)
-   apply(rule conjI)
-    apply force
-   apply clarify
-   apply(subgoal_tac "(Suc m) + i \<le> length x")
-    apply(subgoal_tac "(Suc m) + (Suc i) \<le> length x")
-     apply(rotate_tac -2)
-     apply simp
-     apply(erule_tac x="Suc (m + i)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE)
-     apply(subgoal_tac "Suc (Suc (m + i)) < length x")
-      apply simp
-     apply arith
-    apply arith
-   apply arith
-  apply simp
-  apply clarify
-  apply(case_tac "i\<le>m")
-   apply(drule le_imp_less_or_eq)
-   apply(erule disjE)
-    apply(erule_tac x=i in allE, erule impE, assumption)
-    apply simp
+ apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
+  apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
+   apply(rotate_tac -2)
    apply simp
-  apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
-  apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
-   apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
-    apply(rotate_tac -2)
-    apply simp
-    apply(erule mp)
-   apply arith
   apply arith
  apply arith
-done
-
-ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
+apply(case_tac "length (drop (Suc m) x)",simp)
+apply(erule_tac x="sa" in allE)
+back
+apply(drule_tac c="drop (Suc m) x" in subsetD,simp)
+ apply clarify
+apply simp
+apply clarify
+apply(case_tac "i\<le>m")
+ apply(drule le_imp_less_or_eq)
+ apply(erule disjE)
+  apply(erule_tac x=i in allE, erule impE, assumption)
+  apply simp
+ apply simp
+apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
+apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
+ apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
+  apply(rotate_tac -2)
+  apply simp
+ apply arith
+apply arith
+done
 
 subsubsection{* Soundness of the Sequential rule *}
 
 inductive_cases Seq_cases [elim!]: "(Some (Seq P Q), s) -c\<rightarrow> t"
 

  apply(simp only :nth_append length_map last_length nth_map)
  apply(case_tac "last((Some P, sa) # xs)")
  apply(simp add:lift_def)
 apply simp
 done
-
 declare map_eq_Cons_conv [simp del] Cons_eq_map_conv [simp del]
 
 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>

  apply(rule nth_tl_if)
    apply force
   apply simp+
 apply(simp add:lift_def)
 done
-
 (*
 lemma last_lift_not_None3: "fst (last (map (lift Q) (x#xs))) \<noteq> None"
 apply(simp only:last_length [THEN sym])
 apply(subgoal_tac "length xs<length (x # xs)")
  apply(drule_tac Q=Q in  lift_nth)

  apply(erule ssubst)
  apply (simp add:lift_def)
  apply(case_tac "(x # xs) ! length xs",simp)
 apply simp
 done
-
-ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
 
 lemma Seq_sound: 
   "\<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]"
 apply(unfold com_validity_def)

    apply(rule tl_zero)
      apply (subgoal_tac "i-m=Suc(i-Suc m)")
       apply simp
       apply(erule mp)
       apply(case_tac ys,simp+)
-     apply arith
-    apply arith
    apply force
   apply arith
  apply force
 apply clarify
 apply(case_tac "(map (lift Q) xs @ tl ys)\<noteq>[]")

  apply(rule conjI,clarify)
   apply(case_tac ys,simp+)
  apply clarify
  apply(case_tac ys,simp+)
 done
-
-ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
 
 subsubsection{* Soundness of the While rule *}
 
 lemma last_append[rule_format]:
   "\<forall>xs. ys\<noteq>[] \<longrightarrow> ((xs@ys)!(length (xs@ys) - (Suc 0)))=(ys!(length ys - (Suc 0)))"

  apply(erule mp)
  apply(case_tac "last xs")
  apply(simp add:lift_def)
 apply(simp add:Cons_lift_append nth_append snd_lift del:map.simps)
 done
-
-ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
 
 lemma While_sound_aux [rule_format]: 
   "\<lbrakk> pre \<inter> - b \<subseteq> post; \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s, s) \<in> guar;
    stable pre rely;  stable post rely; x \<in> cptn_mod \<rbrakk> 
   \<Longrightarrow>  \<forall>s xs. x=(Some(While b P),s)#xs \<longrightarrow> x\<in>assum(pre, rely) \<longrightarrow> x \<in> comm (guar, post)"

   apply (simp del:map.simps last.simps)
  apply simp
 apply simp
 done
 
-ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
-
 lemma While_sound: 
   "\<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]"
 apply(unfold com_validity_def)