clib: some proof compression

Signed-off-by: Michael McInerney <[email protected]>

lib/clib/CCorresLemmas.thy

@@ -1058,21 +1058,13 @@ lemma ccorres_While_Normal_helper:
   apply (simp add: isNormal_def)
   apply (elim exE)
   apply (simp add: image_def)
-  apply (erule exec_While_final_inv''[where C="{s'. cond_xf s' \<noteq> 0}" and B="B;; setter"])
-        apply fastforce
-       apply fastforce
-      apply clarsimp
-     apply clarsimp
+  apply (erule exec_While_final_inv''[where C="{s'. cond_xf s' \<noteq> 0}" and B="B;; setter"]; clarsimp)
      apply (frule intermediate_Normal_state[OF _ _ body_inv])
       apply fastforce
      apply clarsimp
      apply (rename_tac inter_t)
-     apply (frule hoarep_exec[OF _ _ body_inv, rotated])
-      apply fastforce
-     apply (frule_tac s=inter_t in hoarep_exec[rotated 2])
-       apply fastforce
-      apply fastforce
-     apply fastforce
+     apply (frule hoarep_exec[OF _ _ body_inv, rotated], fastforce)
+     apply (frule_tac s=inter_t in hoarep_exec[rotated 2], fastforce+)[1]
     apply (metis (mono_tags, lifting) HoarePartial.SeqSwap empty_iff exec_abrupt mem_Collect_eq)
    apply (metis (mono_tags, lifting) HoarePartial.SeqSwap exec_stuck mem_Collect_eq)
   apply (metis (mono_tags, lifting) HoarePartial.SeqSwap empty_iff exec_fault mem_Collect_eq)
@@ -1176,13 +1168,8 @@ proof -
       apply (insert setter_inv_cond)[1]
       apply (drule_tac x=s in meta_spec)
       apply (drule_tac x=r in meta_spec)
-      apply (rule_tac Q'="{s' \<in> G'. cond_xf s' \<noteq> 0 \<longrightarrow> s' \<in> C'}" in conseqPost)
-        apply fastforce
-       apply fastforce
-      apply fastforce
-     apply (rule hoarep_conj_lift_pre_fix)
-      apply (simp add: Collect_mono conseq_under_new_pre)
-     apply (simp add: Collect_mono conseq_under_new_pre)
+      apply (rule_tac Q'="{s' \<in> G'. cond_xf s' \<noteq> 0 \<longrightarrow> s' \<in> C'}" in conseqPost; fastforce)
+     apply (fastforce intro!: hoarep_conj_lift_pre_fix simp: Collect_mono conseq_under_new_pre)
     apply (insert setter_inv_cond)
     apply (drule_tac x=s in meta_spec)
     apply (drule_tac x=r in meta_spec)
@@ -1229,8 +1216,7 @@ proof -
       apply fastforce
      apply fastforce
     apply (case_tac xstate; clarsimp)
-    apply (frule intermediate_Normal_state[OF _ _ setter_hoarep])
-      apply fastforce
+    apply (frule intermediate_Normal_state[OF _ _ setter_hoarep]; assumption?)
      apply fastforce
     apply clarsimp
     apply (rename_tac inter_t)