ConcurrentIMP, ConcurrentGC: address more of Makarius's comments from 2015-05.

Thu, 16 May 2019 01:37:39 +1000

author
Peter Gammie <peteg42@gmail.com>
date
Thu, 16 May 2019 01:37:39 +1000
changeset 10421
37a3fb78148c
parent 10420
a56916696df0
child 10422
4246e7e4c778
child 10423
093ccf72bdbe

ConcurrentIMP, ConcurrentGC: address more of Makarius's comments from 2015-05.

thys/ConcurrentGC/Handshakes.thy file | annotate | diff | comparison | revisions
thys/ConcurrentGC/MarkObject.thy file | annotate | diff | comparison | revisions
thys/ConcurrentGC/Model.thy file | annotate | diff | comparison | revisions
thys/ConcurrentGC/Proofs.thy file | annotate | diff | comparison | revisions
thys/ConcurrentGC/Proofs_basis.thy file | annotate | diff | comparison | revisions
thys/ConcurrentGC/StrongTricolour.thy file | annotate | diff | comparison | revisions
thys/ConcurrentGC/TSO.thy file | annotate | diff | comparison | revisions
thys/ConcurrentGC/Tactics.thy file | annotate | diff | comparison | revisions
thys/ConcurrentIMP/CIMP.thy file | annotate | diff | comparison | revisions
--- a/thys/ConcurrentGC/Handshakes.thy	Wed May 15 16:25:22 2019 +0100
+++ b/thys/ConcurrentGC/Handshakes.thy	Thu May 16 01:37:39 2019 +1000
@@ -77,69 +77,69 @@
 
 \<close>
 
-locset_definition "hp_Idle_locs \<equiv>
+locset_definition "hp_Idle_locs =
   (prefixed ''idle_noop'' - { ''idle_noop_mfence'', ''idle_noop_init_type'' })
 \<union> { ''idle_read_fM'', ''idle_invert_fM'', ''idle_write_fM'', ''idle_flip_noop_mfence'', ''idle_flip_noop_init_type'' }"
 
-locset_definition "hp_IdleInit_locs \<equiv>
+locset_definition "hp_IdleInit_locs =
     (prefixed ''idle_flip_noop'' - { ''idle_flip_noop_mfence'', ''idle_flip_noop_init_type'' })
   \<union> { ''idle_phase_init'', ''init_noop_mfence'', ''init_noop_init_type'' }"
 
-locset_definition "hp_InitMark_locs \<equiv>
+locset_definition "hp_InitMark_locs =
   (prefixed ''init_noop'' - { ''init_noop_mfence'', ''init_noop_init_type'' })
 \<union> { ''init_phase_mark'', ''mark_read_fM'', ''mark_write_fA'', ''mark_noop_mfence'', ''mark_noop_init_type'' }"
 
-locset_definition "hp_IdleMarkSweep_locs \<equiv>
+locset_definition "hp_IdleMarkSweep_locs =
      { ''idle_noop_mfence'', ''idle_noop_init_type'', ''mark_end'' }
   \<union>  sweep_locs
   \<union> (mark_loop_locs - { ''mark_loop_get_roots_init_type'' })"
 
-locset_definition "hp_Mark_locs \<equiv>
+locset_definition "hp_Mark_locs =
     (prefixed ''mark_noop'' - { ''mark_noop_mfence'', ''mark_noop_init_type'' })
   \<union> { ''mark_loop_get_roots_init_type'' }"
 
 abbreviation
   "hs_noop_prefixes \<equiv> {''idle_noop'', ''idle_flip_noop'', ''init_noop'', ''mark_noop'' }"
 
-locset_definition "hs_noop_locs \<equiv>
-  \<Union>l \<in> hs_noop_prefixes. prefixed l - (suffixed ''_noop_mfence'' \<union> suffixed ''_noop_init_type'')"
+locset_definition "hs_noop_locs =
+  (\<Union>l \<in> hs_noop_prefixes. prefixed l - (suffixed ''_noop_mfence'' \<union> suffixed ''_noop_init_type''))"
 
-locset_definition "hs_get_roots_locs \<equiv>
+locset_definition "hs_get_roots_locs =
   prefixed ''mark_loop_get_roots'' - {''mark_loop_get_roots_init_type''}"
 
-locset_definition "hs_get_work_locs \<equiv>
+locset_definition "hs_get_work_locs =
   prefixed ''mark_loop_get_work'' - {''mark_loop_get_work_init_type''}"
 
 abbreviation "hs_prefixes \<equiv>
   hs_noop_prefixes \<union> { ''mark_loop_get_roots'', ''mark_loop_get_work'' }"
 
-locset_definition "hs_init_loop_locs \<equiv> \<Union>l \<in> hs_prefixes. prefixed (l @ ''_init_loop'')"
+locset_definition "hs_init_loop_locs = (\<Union>l \<in> hs_prefixes. prefixed (l @ ''_init_loop''))"
 
-locset_definition "hs_done_loop_locs \<equiv> \<Union>l \<in> hs_prefixes. prefixed (l @ ''_done_loop'')"
+locset_definition "hs_done_loop_locs = (\<Union>l \<in> hs_prefixes. prefixed (l @ ''_done_loop''))"
 
-locset_definition "hs_done_locs \<equiv> \<Union>l \<in> hs_prefixes. prefixed (l @ ''_done'')"
+locset_definition "hs_done_locs = (\<Union>l \<in> hs_prefixes. prefixed (l @ ''_done''))"
 
-locset_definition "hs_none_pending_locs \<equiv> - (hs_init_loop_locs \<union> hs_done_locs)"
+locset_definition "hs_none_pending_locs = - (hs_init_loop_locs \<union> hs_done_locs)"
 
-locset_definition "hs_in_sync_locs \<equiv>
+locset_definition "hs_in_sync_locs =
   (- ( (\<Union>l \<in> hs_prefixes. prefixed (l @ ''_init'')) \<union> hs_done_locs ))
   \<union> (\<Union>l \<in> hs_prefixes. {l @ ''_init_type''})"
 
-locset_definition "hs_out_of_sync_locs \<equiv>
-  \<Union>l \<in> hs_prefixes. {l @ ''_init_muts''}"
+locset_definition "hs_out_of_sync_locs =
+  (\<Union>l \<in> hs_prefixes. {l @ ''_init_muts''})"
 
-locset_definition "hs_mut_in_muts_locs \<equiv>
-  \<Union>l \<in> hs_prefixes. {l @ ''_init_loop_set_pending'', l @ ''_init_loop_done''}"
+locset_definition "hs_mut_in_muts_locs =
+  (\<Union>l \<in> hs_prefixes. {l @ ''_init_loop_set_pending'', l @ ''_init_loop_done''})"
 
-locset_definition "hs_init_loop_done_locs \<equiv>
-  \<Union>l \<in> hs_prefixes. {l @ ''_init_loop_done''}"
+locset_definition "hs_init_loop_done_locs =
+  (\<Union>l \<in> hs_prefixes. {l @ ''_init_loop_done''})"
 
-locset_definition "hs_init_loop_not_done_locs \<equiv>
-  hs_init_loop_locs - (\<Union>l \<in> hs_prefixes. {l @ ''_init_loop_done''})"
+locset_definition "hs_init_loop_not_done_locs =
+  (hs_init_loop_locs - (\<Union>l \<in> hs_prefixes. {l @ ''_init_loop_done''}))"
 
-definition (in gc) handshake_invL :: "('field, 'mut, 'ref) gc_pred" where
-[inv]: "handshake_invL \<equiv>
-      atS_gc hs_noop_locs         (sys_handshake_type \<^bold>= \<langle>ht_NOOP\<rangle>)
+inv_definition (in gc) handshake_invL :: "('field, 'mut, 'ref) gc_pred" where
+  "handshake_invL =
+     (atS_gc hs_noop_locs         (sys_handshake_type \<^bold>= \<langle>ht_NOOP\<rangle>)
     \<^bold>\<and> atS_gc hs_get_roots_locs    (sys_handshake_type \<^bold>= \<langle>ht_GetRoots\<rangle>)
     \<^bold>\<and> atS_gc hs_get_work_locs     (sys_handshake_type \<^bold>= \<langle>ht_GetWork\<rangle>)
 
@@ -148,23 +148,23 @@
                                                                   \<^bold>\<or> sys_ghost_handshake_in_sync m)
     \<^bold>\<and> atS_gc hs_init_loop_not_done_locs (\<^bold>\<forall>m.   \<langle>m\<rangle> \<^bold>\<in> gc_muts \<^bold>\<longrightarrow> \<^bold>\<not>(sys_handshake_pending m)
                                                                  \<^bold>\<and> \<^bold>\<not>(sys_ghost_handshake_in_sync m))
-  \<^bold>\<and> atS_gc hs_init_loop_done_locs     ( (sys_handshake_pending \<^bold>$ gc_mut
+    \<^bold>\<and> atS_gc hs_init_loop_done_locs     ( (sys_handshake_pending \<^bold>$ gc_mut
                                         \<^bold>\<or> sys_ghost_handshake_in_sync \<^bold>$ gc_mut)
                                       \<^bold>\<and> (\<^bold>\<forall>m. \<langle>m\<rangle> \<^bold>\<in> gc_muts \<^bold>\<and> \<langle>m\<rangle> \<^bold>\<noteq> gc_mut
                                                                  \<^bold>\<longrightarrow> \<^bold>\<not>(sys_handshake_pending m)
                                                                    \<^bold>\<and> \<^bold>\<not>(sys_ghost_handshake_in_sync m)) )
-  \<^bold>\<and> atS_gc hs_done_locs       (\<^bold>\<forall>m. sys_handshake_pending m \<^bold>\<or> sys_ghost_handshake_in_sync m)
-  \<^bold>\<and> atS_gc hs_done_loop_locs  (\<^bold>\<forall>m. \<^bold>\<not>(\<langle>m\<rangle> \<^bold>\<in> gc_muts) \<^bold>\<longrightarrow> \<^bold>\<not>(sys_handshake_pending m))
-  \<^bold>\<and> atS_gc hs_none_pending_locs (\<^bold>\<forall>m. \<^bold>\<not>(sys_handshake_pending m))
-  \<^bold>\<and> atS_gc hs_in_sync_locs      (\<^bold>\<forall>m. sys_ghost_handshake_in_sync m)
-  \<^bold>\<and> atS_gc hs_out_of_sync_locs  (\<^bold>\<forall>m. \<^bold>\<not>(sys_handshake_pending m)
-                                       \<^bold>\<and> \<^bold>\<not>(sys_ghost_handshake_in_sync m))
+    \<^bold>\<and> atS_gc hs_done_locs       (\<^bold>\<forall>m. sys_handshake_pending m \<^bold>\<or> sys_ghost_handshake_in_sync m)
+    \<^bold>\<and> atS_gc hs_done_loop_locs  (\<^bold>\<forall>m. \<^bold>\<not>(\<langle>m\<rangle> \<^bold>\<in> gc_muts) \<^bold>\<longrightarrow> \<^bold>\<not>(sys_handshake_pending m))
+    \<^bold>\<and> atS_gc hs_none_pending_locs (\<^bold>\<forall>m. \<^bold>\<not>(sys_handshake_pending m))
+    \<^bold>\<and> atS_gc hs_in_sync_locs      (\<^bold>\<forall>m. sys_ghost_handshake_in_sync m)
+    \<^bold>\<and> atS_gc hs_out_of_sync_locs  (\<^bold>\<forall>m. \<^bold>\<not>(sys_handshake_pending m)
+                                         \<^bold>\<and> \<^bold>\<not>(sys_ghost_handshake_in_sync m))
 
-  \<^bold>\<and> atS_gc hp_Idle_locs          (sys_ghost_handshake_phase \<^bold>= \<langle>hp_Idle\<rangle>)
-  \<^bold>\<and> atS_gc hp_IdleInit_locs      (sys_ghost_handshake_phase \<^bold>= \<langle>hp_IdleInit\<rangle>)
-  \<^bold>\<and> atS_gc hp_InitMark_locs      (sys_ghost_handshake_phase \<^bold>= \<langle>hp_InitMark\<rangle>)
-  \<^bold>\<and> atS_gc hp_IdleMarkSweep_locs (sys_ghost_handshake_phase \<^bold>= \<langle>hp_IdleMarkSweep\<rangle>)
-  \<^bold>\<and> atS_gc hp_Mark_locs          (sys_ghost_handshake_phase \<^bold>= \<langle>hp_Mark\<rangle>)"
+    \<^bold>\<and> atS_gc hp_Idle_locs          (sys_ghost_handshake_phase \<^bold>= \<langle>hp_Idle\<rangle>)
+    \<^bold>\<and> atS_gc hp_IdleInit_locs      (sys_ghost_handshake_phase \<^bold>= \<langle>hp_IdleInit\<rangle>)
+    \<^bold>\<and> atS_gc hp_InitMark_locs      (sys_ghost_handshake_phase \<^bold>= \<langle>hp_InitMark\<rangle>)
+    \<^bold>\<and> atS_gc hp_IdleMarkSweep_locs (sys_ghost_handshake_phase \<^bold>= \<langle>hp_IdleMarkSweep\<rangle>)
+    \<^bold>\<and> atS_gc hp_Mark_locs          (sys_ghost_handshake_phase \<^bold>= \<langle>hp_Mark\<rangle>))"
 (*<*)
 
 lemma hs_get_roots_locs_subseteq_hp_IdleMarkSweep_locs:
@@ -209,17 +209,17 @@
 
 \<close>
 
-locset_definition "mut_no_pending_mutates_locs \<equiv>
+locset_definition "mut_no_pending_mutates_locs =
     (prefixed ''hs_noop'' - { ''hs_noop'', ''hs_noop_mfence'' })
   \<union> (prefixed ''hs_get_roots'' - { ''hs_get_roots'', ''hs_get_roots_mfence'' })
   \<union> (prefixed ''hs_get_work'' - { ''hs_get_work'', ''hs_get_work_mfence'' })"
 
-definition (in mut_m) handshake_invL :: "('field, 'mut, 'ref) gc_pred" where
-[inv]: "handshake_invL \<equiv>
-    atS_mut (prefixed ''hs_noop_'')     (sys_handshake_type \<^bold>= \<langle>ht_NOOP\<rangle> \<^bold>\<and> sys_handshake_pending m)
+inv_definition (in mut_m) handshake_invL :: "('field, 'mut, 'ref) gc_pred" where
+  "handshake_invL =
+   (atS_mut (prefixed ''hs_noop_'')     (sys_handshake_type \<^bold>= \<langle>ht_NOOP\<rangle> \<^bold>\<and> sys_handshake_pending m)
  \<^bold>\<and> atS_mut (prefixed ''hs_get_roots_'') (sys_handshake_type \<^bold>= \<langle>ht_GetRoots\<rangle> \<^bold>\<and> sys_handshake_pending m)
  \<^bold>\<and> atS_mut (prefixed ''hs_get_work_'')  (sys_handshake_type \<^bold>= \<langle>ht_GetWork\<rangle> \<^bold>\<and> sys_handshake_pending m)
- \<^bold>\<and> atS_mut mut_no_pending_mutates_locs  (LIST_NULL (tso_pending_mutate (mutator m)))"
+ \<^bold>\<and> atS_mut mut_no_pending_mutates_locs  (LIST_NULL (tso_pending_mutate (mutator m))))"
 (*<*)
 
 lemma (in mut_m) handshake_invL_eq_imp:
@@ -318,13 +318,13 @@
      \<union> (init_locs - { ''init_noop_mfence'' })
      \<union> (mark_locs - { ''mark_read_fM'', ''mark_write_fA'', ''mark_noop_mfence'' })"
 
-definition (in gc) phase_invL :: "('field, 'mut, 'ref) gc_pred" where
-[inv]: "phase_invL \<equiv>
-      atS_gc idle_locs             (gc_phase \<^bold>= \<langle>ph_Idle\<rangle>)
+inv_definition (in gc) phase_invL :: "('field, 'mut, 'ref) gc_pred" where
+  "phase_invL =
+     (atS_gc idle_locs             (gc_phase \<^bold>= \<langle>ph_Idle\<rangle>)
   \<^bold>\<and> atS_gc init_locs             (gc_phase \<^bold>= \<langle>ph_Init\<rangle>)
   \<^bold>\<and> atS_gc mark_locs             (gc_phase \<^bold>= \<langle>ph_Mark\<rangle>)
   \<^bold>\<and> atS_gc sweep_locs            (gc_phase \<^bold>= \<langle>ph_Sweep\<rangle>)
-  \<^bold>\<and> atS_gc no_pending_phase_locs (LIST_NULL (tso_pending_phase gc))"
+  \<^bold>\<and> atS_gc no_pending_phase_locs (LIST_NULL (tso_pending_phase gc)))"
 (*<*)
 
 lemma (in gc) phase_invL_eq_imp:
@@ -359,8 +359,7 @@
   shows "\<lbrace> LSTP (phase_rel_inv \<^bold>\<and> tso_writes_inv) \<rbrace> sys \<lbrace> LSTP phase_rel_inv \<rbrace>"
 apply vcg_jackhammer
 apply (simp add: phase_rel_def p_not_sys split: if_splits)
-apply (elim disjE)
-    apply (auto split: if_splits)
+apply (elim disjE; auto split: if_splits)
 done
 
 lemma (in mut_m) phase_rel_inv[intro]:
@@ -410,9 +409,9 @@
 definition fA_rel_inv :: "('field, 'mut, 'ref) lsts_pred" where
   "fA_rel_inv = ((\<^bold>\<forall>m. sys_ghost_handshake_in_sync m) \<^bold>\<otimes> sys_ghost_handshake_phase \<^bold>\<otimes> sys_fA \<^bold>\<otimes> gc_fM \<^bold>\<otimes> tso_pending_fA gc \<^bold>\<in> \<langle>fA_rel\<rangle>)"
 
-locset_definition "fM_eq_locs \<equiv> (- { ''idle_write_fM'', ''idle_flip_noop_mfence'' })"
-locset_definition "fM_tso_empty_locs \<equiv> (- { ''idle_flip_noop_mfence'' })"
-locset_definition "fA_tso_empty_locs \<equiv> (- { ''mark_noop_mfence'' })"
+locset_definition "fM_eq_locs = (- { ''idle_write_fM'', ''idle_flip_noop_mfence'' })"
+locset_definition "fM_tso_empty_locs = (- { ''idle_flip_noop_mfence'' })"
+locset_definition "fA_tso_empty_locs = (- { ''mark_noop_mfence'' })"
 
 locset_definition
   "fA_eq_locs \<equiv> { ''idle_read_fM'', ''idle_invert_fM'' }
@@ -425,9 +424,9 @@
                \<union> prefixed ''idle_flip_noop''
                \<union> init_locs"
 
-definition (in gc) fM_fA_invL :: "('field, 'mut, 'ref) gc_pred" where
-[inv]: "fM_fA_invL \<equiv>
-    atS_gc fM_eq_locs                    (sys_fM  \<^bold>= gc_fM)
+inv_definition (in gc) fM_fA_invL :: "('field, 'mut, 'ref) gc_pred" where
+  "fM_fA_invL =
+   (atS_gc fM_eq_locs                    (sys_fM  \<^bold>= gc_fM)
   \<^bold>\<and> at_gc ''idle_write_fM''              (sys_fM \<^bold>\<noteq> gc_fM)
   \<^bold>\<and> at_gc ''idle_flip_noop_mfence''      (sys_fM \<^bold>\<noteq> gc_fM \<^bold>\<longrightarrow> (\<^bold>\<not>(LIST_NULL (tso_pending_fM gc))))
   \<^bold>\<and> atS_gc fM_tso_empty_locs             (LIST_NULL (tso_pending_fM gc))
@@ -435,7 +434,7 @@
   \<^bold>\<and> atS_gc fA_eq_locs                    (sys_fA  \<^bold>= gc_fM)
   \<^bold>\<and> atS_gc fA_neq_locs                   (sys_fA \<^bold>\<noteq> gc_fM)
   \<^bold>\<and> at_gc ''mark_noop_mfence''           (sys_fA \<^bold>\<noteq> gc_fM \<^bold>\<longrightarrow> (\<^bold>\<not>(LIST_NULL (tso_pending_fA gc))))
-  \<^bold>\<and> atS_gc fA_tso_empty_locs             (LIST_NULL (tso_pending_fA gc))"
+  \<^bold>\<and> atS_gc fA_tso_empty_locs             (LIST_NULL (tso_pending_fA gc)))"
 (*<*)
 
 lemmas fM_rel_invD = iffD1[OF fun_cong[OF fM_rel_inv_def[simplified atomize_eq]]]
@@ -508,13 +507,9 @@
  apply (clarsimp simp: fM_rel_inv_def fM_rel_def split: if_splits)
 apply (clarsimp simp: fM_rel_inv_def fM_rel_def filter_empty_conv)
 
-apply (erule disjE)
- apply clarsimp
-apply clarsimp
+apply (erule disjE; clarsimp)
 
-apply (rule conjI)
- apply (clarsimp simp: fM_rel_inv_def fM_rel_def split: if_splits)
-apply (clarsimp simp: fM_rel_inv_def fM_rel_def split: if_splits)
+apply (rule conjI; clarsimp simp: fM_rel_inv_def fM_rel_def split: if_splits)
 
 apply (clarsimp split: if_splits)
 
--- a/thys/ConcurrentGC/MarkObject.thy	Wed May 15 16:25:22 2019 +0100
+++ b/thys/ConcurrentGC/MarkObject.thy	Thu May 16 01:37:39 2019 +1000
@@ -594,23 +594,23 @@
 
 \<close>
 
-locset_definition "mut_hs_get_roots_loop_locs \<equiv> prefixed ''hs_get_roots_loop''"
-locset_definition "mut_hs_get_roots_loop_mo_locs \<equiv>
+locset_definition "mut_hs_get_roots_loop_locs = prefixed ''hs_get_roots_loop''"
+locset_definition "mut_hs_get_roots_loop_mo_locs =
   prefixed ''hs_get_roots_loop_mo'' \<union> {''hs_get_roots_loop_done''}"
 
 abbreviation "mut_async_mark_object_prefixes \<equiv> { ''store_del'', ''store_ins'' }"
 
-locset_definition "mut_hs_not_hp_Idle_locs \<equiv>
+locset_definition "mut_hs_not_hp_Idle_locs =
   (\<Union>pref\<in>mut_async_mark_object_prefixes.
      \<Union>l\<in>{''mo_co_lock'', ''mo_co_cmark'', ''mo_co_ctest'', ''mo_co_mark'', ''mo_co_unlock'', ''mo_co_won'', ''mo_co_W''}. {pref @ ''_'' @ l})"
 
-locset_definition "mut_async_mo_ptest_locs \<equiv>
+locset_definition "mut_async_mo_ptest_locs =
   (\<Union>pref\<in>mut_async_mark_object_prefixes. {pref @ ''_mo_ptest''})"
 
-locset_definition "mut_mo_ptest_locs \<equiv>
+locset_definition "mut_mo_ptest_locs =
   (\<Union>pref\<in>mut_async_mark_object_prefixes. {pref @ ''_mo_ptest''})"
 
-locset_definition "mut_mo_valid_ref_locs \<equiv>
+locset_definition "mut_mo_valid_ref_locs =
   (prefixed ''store_del'' \<union> prefixed ''store_ins'' \<union> { ''deref_del'', ''lop_store_ins''})"
 (*<*)
 
@@ -642,7 +642,10 @@
 can locally guarantee that it, in the relevant phases, will insert
 only marked references. Less often can it be sure that the reference
 it is overwriting is marked. We also need to consider writes pending
-in TSO buffers.
+in TSO buffers: it is key that after the \<open>''init_noop''\<close>
+handshake there are no pending white insertions
+(mutations that insert unmarked references). This ensures the deletion barrier
+does its job.
 
 \<close>
 
@@ -651,8 +654,12 @@
      - (\<Union>pref\<in>{ ''mark_loop'', ''hs_get_roots_loop'', ''store_del'', ''store_ins'' }.
         \<Union>l\<in>{ ''mo_co_unlock'', ''mo_co_won'', ''mo_co_W'' }. {pref @ ''_'' @ l})"
 
-definition (in mut_m) mark_object_invL :: "('field, 'mut, 'ref) gc_pred" where
-[inv]: "mark_object_invL \<equiv>
+locset_definition
+  "ghost_honorary_root_empty_locs \<equiv>
+     - (prefixed ''store_del'' \<union> {''lop_store_ins''} \<union> prefixed ''store_ins'')"
+
+inv_definition (in mut_m) mark_object_invL :: "('field, 'mut, 'ref) gc_pred" where
+  "mark_object_invL =
    (atS_mut mut_hs_get_roots_loop_locs    (mut_refs \<^bold>\<subseteq> mut_roots \<^bold>\<and> (\<^bold>\<forall>r. \<langle>r\<rangle> \<^bold>\<in> mut_roots \<^bold>- mut_refs \<^bold>\<longrightarrow> marked r))
   \<^bold>\<and> atS_mut mut_hs_get_roots_loop_mo_locs (\<^bold>\<not>(NULL mut_ref) \<^bold>\<and> mut_the_ref \<^bold>\<in> mut_roots)
   \<^bold>\<and> at_mut ''hs_get_roots_loop_done''     (marked \<^bold>$ mut_the_ref)
@@ -691,7 +698,11 @@
                                             ( (mut_ghost_handshake_phase \<^bold>= \<langle>hp_Mark\<rangle>
                                              \<^bold>\<or> (mut_ghost_handshake_phase \<^bold>= \<langle>hp_IdleMarkSweep\<rangle> \<^bold>\<and> sys_phase \<^bold>\<noteq> \<langle>ph_Idle\<rangle>))
                                           \<^bold>\<and> (\<lambda>s. \<forall>opt_r'. \<not>tso_pending_write (mutator m) (mw_Mutate (mut_tmp_ref s) (mut_field s) opt_r') s)
-                                          \<^bold>\<longrightarrow> (\<lambda>s. obj_at_field_on_heap (\<lambda>r'. marked r' s) (mut_tmp_ref s) (mut_field s) s) ))"
+                                          \<^bold>\<longrightarrow> (\<lambda>s. obj_at_field_on_heap (\<lambda>r'. marked r' s) (mut_tmp_ref s) (mut_field s) s) )
+\<comment>\<open>after \<open>''init_noop''\<close>\<close>
+  \<^bold>\<and> at_mut ''load''         (mut_tmp_ref \<^bold>\<in> mut_roots)
+  \<^bold>\<and> at_mut ''hs_noop_done'' (LIST_NULL (tso_pending_mutate (mutator m))) \<comment>\<open> key: no pending white insertions \<close>
+  \<^bold>\<and> atS_mut ghost_honorary_root_empty_locs (EMPTY mut_ghost_honorary_root) )"
 (*<*)
 
 lemma get_roots_get_work_subseteq_ghost_honorary_grey_empty_locs:
@@ -809,18 +820,17 @@
    \<lbrace> mut_store_ins.mark_object_invL m \<rbrace>"
 apply (vcg_ni simp: not_blocked_def)
 
-subgoal by (fastforce simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
-subgoal by (fastforce simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
-subgoal by (fastforce simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
-subgoal by (fastforce simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
-subgoal by (fastforce simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
-subgoal by (fastforce simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
-subgoal by (fastforce simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
-subgoal by (fastforce simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
-subgoal by (fastforce simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
-subgoal by (fastforce simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
-subgoal by (fastforce simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
-
+subgoal by (auto simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
+subgoal by (auto simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
+subgoal by (auto simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
+subgoal by (auto simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
+subgoal by (auto simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
+subgoal by (auto simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
+subgoal by (auto simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
+subgoal by (auto simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
+subgoal by (auto simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
+subgoal by (auto simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
+subgoal by (auto simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
 done
 
 lemma (in sys) mut_get_roots_mark_object_invL[intro]:
@@ -835,18 +845,28 @@
 apply (vcg_ni simp: not_blocked_def p_not_sys
              dest!: mut_m.handshake_phase_invD[where m=m])
 
-subgoal by (fastforce simp: do_write_action_def fM_rel_inv_def fM_rel_def hp_step_rel_def split: mem_write_action.split if_splits obj_at_splits)
-subgoal by (fastforce simp: do_write_action_def fM_rel_inv_def fM_rel_def hp_step_rel_def split: mem_write_action.split if_splits obj_at_splits)
-subgoal by (fastforce simp: do_write_action_def fM_rel_inv_def fM_rel_def hp_step_rel_def split: mem_write_action.split if_splits obj_at_splits)
-subgoal by (fastforce simp: do_write_action_def fM_rel_inv_def fM_rel_def hp_step_rel_def split: mem_write_action.split if_splits obj_at_splits)
-subgoal by (fastforce simp: do_write_action_def fM_rel_inv_def fM_rel_def hp_step_rel_def split: mem_write_action.split if_splits obj_at_splits)
-subgoal by (fastforce simp: do_write_action_def fM_rel_inv_def fM_rel_def hp_step_rel_def split: mem_write_action.split if_splits obj_at_splits)
-subgoal by (fastforce simp: do_write_action_def fM_rel_inv_def fM_rel_def hp_step_rel_def split: mem_write_action.split if_splits obj_at_splits)
-subgoal by (fastforce simp: do_write_action_def fM_rel_inv_def fM_rel_def hp_step_rel_def split: mem_write_action.split if_splits obj_at_splits)
-subgoal by (fastforce simp: do_write_action_def fM_rel_inv_def fM_rel_def hp_step_rel_def split: mem_write_action.split if_splits obj_at_splits)
-subgoal by (fastforce simp: do_write_action_def fM_rel_inv_def fM_rel_def hp_step_rel_def split: mem_write_action.split if_splits obj_at_splits)
-subgoal by (fastforce simp: do_write_action_def fM_rel_inv_def fM_rel_def hp_step_rel_def split: mem_write_action.split if_splits obj_at_splits)
-
+subgoal by (auto simp: do_write_action_def fM_rel_inv_def fM_rel_def hp_step_rel_def filter_empty_conv
+                split: mem_write_action.splits if_splits obj_at_splits)
+subgoal by (auto simp: do_write_action_def fM_rel_inv_def fM_rel_def hp_step_rel_def filter_empty_conv
+                split: mem_write_action.splits if_splits obj_at_splits)
+subgoal by (auto simp: do_write_action_def fM_rel_inv_def fM_rel_def hp_step_rel_def filter_empty_conv
+                split: mem_write_action.splits if_splits obj_at_splits)
+subgoal by (auto simp: do_write_action_def fM_rel_inv_def fM_rel_def hp_step_rel_def filter_empty_conv
+                split: mem_write_action.splits if_splits obj_at_splits)
+subgoal by (auto simp: do_write_action_def fM_rel_inv_def fM_rel_def hp_step_rel_def filter_empty_conv
+                split: mem_write_action.splits if_splits obj_at_splits)
+subgoal by (auto simp: do_write_action_def fM_rel_inv_def fM_rel_def hp_step_rel_def filter_empty_conv
+                split: mem_write_action.splits if_splits obj_at_splits)
+subgoal by (auto simp: do_write_action_def fM_rel_inv_def fM_rel_def hp_step_rel_def filter_empty_conv
+                split: mem_write_action.splits if_splits obj_at_splits)
+subgoal by (auto simp: do_write_action_def fM_rel_inv_def fM_rel_def hp_step_rel_def filter_empty_conv
+                split: mem_write_action.splits if_splits obj_at_splits)
+subgoal by (auto simp: do_write_action_def fM_rel_inv_def fM_rel_def hp_step_rel_def filter_empty_conv
+                split: mem_write_action.splits if_splits obj_at_splits)
+subgoal by (auto simp: do_write_action_def fM_rel_inv_def fM_rel_def hp_step_rel_def filter_empty_conv
+                split: mem_write_action.splits if_splits obj_at_splits)
+subgoal by (auto simp: do_write_action_def fM_rel_inv_def fM_rel_def hp_step_rel_def filter_empty_conv
+                split: mem_write_action.splits if_splits obj_at_splits)
 done
 
 lemma (in sys) mut_store_del_mark_object_invL[intro]:
@@ -861,18 +881,17 @@
    \<lbrace> mut_store_del.mark_object_invL m \<rbrace>"
 apply (vcg_ni simp: not_blocked_def)
 
-subgoal by (fastforce simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
-subgoal by (fastforce simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
-subgoal by (fastforce simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
-subgoal by (fastforce simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
-subgoal by (fastforce simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
+subgoal by (auto simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
+subgoal by (auto simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
+subgoal by (auto simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
+subgoal by (auto simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
 subgoal by (fastforce simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
-subgoal by (fastforce simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
-subgoal by (fastforce simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
-subgoal by (fastforce simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
-subgoal by (fastforce simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
-subgoal by (fastforce simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
-
+subgoal by (auto simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
+subgoal by (auto simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
+subgoal by (auto simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
+subgoal by (auto simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
+subgoal by (auto simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
+subgoal by (auto simp: do_write_action_def split: mem_write_action.splits obj_at_splits)
 done
 
 lemma (in mut_m) mut_store_del_mark_object_invL[intro]:
@@ -946,8 +965,8 @@
      { ''mark_loop_mark_object_loop'', ''mark_loop_mark_choose_field'', ''mark_loop_mark_deref'', ''mark_loop_mark_field_done'', ''mark_loop_blacken'' }
    \<union> prefixed ''mark_loop_mo''"
 
-definition (in gc) obj_fields_marked_invL :: "('field, 'mut, 'ref) gc_pred" where
-[inv]: "obj_fields_marked_invL \<equiv>
+inv_definition (in gc) obj_fields_marked_invL :: "('field, 'mut, 'ref) gc_pred" where
+  "obj_fields_marked_invL \<equiv>
     (atS_gc obj_fields_marked_locs       (obj_fields_marked_inv \<^bold>\<and> gc_tmp_ref \<^bold>\<in> gc_W)
   \<^bold>\<and> atS_gc (prefixed ''mark_loop_mo'' \<union> { ''mark_loop_mark_field_done'' })
                                           (\<lambda>s. obj_at_field_on_heap (\<lambda>r. gc_ref s = Some r \<or> marked r s) (gc_tmp_ref s) (gc_field s) s)
@@ -1041,39 +1060,39 @@
    \<lbrace> gc_mark.mark_object_invL \<rbrace>"
 apply vcg_ni
 
-subgoal by (force dest!: valid_W_invD2
-              simp: do_write_action_def not_blocked_def fM_rel_def filter_empty_conv p_not_sys
-             split: mem_write_action.split if_splits)
-subgoal by (force dest!: valid_W_invD2
-              simp: do_write_action_def not_blocked_def fM_rel_def filter_empty_conv p_not_sys
-             split: mem_write_action.split if_splits)
-subgoal by (force dest!: valid_W_invD2
-              simp: do_write_action_def not_blocked_def fM_rel_def filter_empty_conv p_not_sys
-             split: mem_write_action.split if_splits)
-subgoal by (force dest!: valid_W_invD2
-              simp: do_write_action_def not_blocked_def fM_rel_def filter_empty_conv p_not_sys
-             split: mem_write_action.split if_splits)
-subgoal by (force dest!: valid_W_invD2
-              simp: do_write_action_def not_blocked_def fM_rel_def filter_empty_conv p_not_sys
-             split: mem_write_action.split if_splits)
-subgoal by (force dest!: valid_W_invD2
-              simp: do_write_action_def not_blocked_def fM_rel_def filter_empty_conv p_not_sys
-             split: mem_write_action.split if_splits)
-subgoal by (force dest!: valid_W_invD2
-              simp: do_write_action_def not_blocked_def fM_rel_def filter_empty_conv p_not_sys
-             split: mem_write_action.split if_splits)
-subgoal by (force dest!: valid_W_invD2
-              simp: do_write_action_def not_blocked_def fM_rel_def filter_empty_conv p_not_sys
-             split: mem_write_action.split if_splits)
-subgoal by (force dest!: valid_W_invD2
-              simp: do_write_action_def not_blocked_def fM_rel_def filter_empty_conv p_not_sys
-             split: mem_write_action.split if_splits)
-subgoal by (force dest!: valid_W_invD2
-              simp: do_write_action_def not_blocked_def fM_rel_def filter_empty_conv p_not_sys
-             split: mem_write_action.split if_splits)
-subgoal by (force dest!: valid_W_invD2
-              simp: do_write_action_def not_blocked_def fM_rel_def filter_empty_conv p_not_sys
-             split: mem_write_action.split if_splits)
+subgoal by (auto dest!: valid_W_invD2
+                  simp: do_write_action_def not_blocked_def fM_rel_def filter_empty_conv p_not_sys
+                 split: mem_write_action.split if_splits)
+subgoal by (auto dest!: valid_W_invD2
+                  simp: do_write_action_def not_blocked_def fM_rel_def filter_empty_conv p_not_sys
+                 split: mem_write_action.split if_splits)
+subgoal by (auto dest!: valid_W_invD2
+                  simp: do_write_action_def not_blocked_def fM_rel_def filter_empty_conv p_not_sys
+                 split: mem_write_action.split if_splits)
+subgoal by (auto dest!: valid_W_invD2
+                  simp: do_write_action_def not_blocked_def fM_rel_def filter_empty_conv p_not_sys
+                 split: mem_write_action.split if_splits)
+subgoal by (auto dest!: valid_W_invD2
+                  simp: do_write_action_def not_blocked_def fM_rel_def filter_empty_conv p_not_sys
+                 split: mem_write_action.split if_splits)
+subgoal by (auto dest!: valid_W_invD2
+                  simp: do_write_action_def not_blocked_def fM_rel_def filter_empty_conv p_not_sys
+                 split: mem_write_action.split if_splits)
+subgoal by (auto dest!: valid_W_invD2
+                  simp: do_write_action_def not_blocked_def fM_rel_def filter_empty_conv p_not_sys
+                 split: mem_write_action.split if_splits)
+subgoal by (auto dest!: valid_W_invD2
+                  simp: do_write_action_def not_blocked_def fM_rel_def filter_empty_conv p_not_sys
+                 split: mem_write_action.split if_splits)
+subgoal by (auto dest!: valid_W_invD2
+                  simp: do_write_action_def not_blocked_def fM_rel_def filter_empty_conv p_not_sys
+                 split: mem_write_action.split if_splits)
+subgoal by (auto dest!: valid_W_invD2
+                  simp: do_write_action_def not_blocked_def fM_rel_def filter_empty_conv p_not_sys
+                 split: mem_write_action.split if_splits)
+subgoal by (auto dest!: valid_W_invD2
+                  simp: do_write_action_def not_blocked_def fM_rel_def filter_empty_conv p_not_sys
+                 split: mem_write_action.split if_splits)
 done
 
 (*>*)
--- a/thys/ConcurrentGC/Model.thy	Wed May 15 16:25:22 2019 +0100
+++ b/thys/ConcurrentGC/Model.thy	Thu May 16 01:37:39 2019 +1000
@@ -279,7 +279,7 @@
 Both the mutators and the garbage collector mark references, which
 indicates that a reference is live in the current round of
 collection. This operation is defined in @{cite [cite_macro=citet]
-\<open>Figure~2.8\<close> "{Pizlo201xPhd"}. These definitions are
+\<open>Figure~2.8\<close> "Pizlo201xPhd"}. These definitions are
 parameterised by the name of the process.
 
 \<close>
--- a/thys/ConcurrentGC/Proofs.thy	Wed May 15 16:25:22 2019 +0100
+++ b/thys/ConcurrentGC/Proofs.thy	Thu May 16 01:37:39 2019 +1000
@@ -33,8 +33,7 @@
 
 definition (in mut_m) invsL :: "('field, 'mut, 'ref) gc_pred" where
   "invsL \<equiv>
-    load_invL
-  \<^bold>\<and> mark_object_invL
+    mark_object_invL
   \<^bold>\<and> mut_get_roots.mark_object_invL m
   \<^bold>\<and> mut_store_ins.mark_object_invL m
   \<^bold>\<and> mut_store_del.mark_object_invL m
@@ -262,7 +261,7 @@
                       valid_refs_imp_reachable_snapshot_inv
                       mut_m.invsL_def inv
                       mut_m.mark_object_invL_def
-                      mut_m.handshake_invL_def mut_m.load_invL_def mut_m.tso_lock_invL_def
+                      mut_m.handshake_invL_def mut_m.tso_lock_invL_def
                       mut_m.marked_deletions_def mut_m.marked_insertions_def
                       loc atS_simps)
 done
--- a/thys/ConcurrentGC/Proofs_basis.thy	Wed May 15 16:25:22 2019 +0100
+++ b/thys/ConcurrentGC/Proofs_basis.thy	Thu May 16 01:37:39 2019 +1000
@@ -206,11 +206,11 @@
 
 subsection\<open> Garbage collector locations \<close>
 
-locset_definition "idle_locs \<equiv> prefixed ''idle''"
-locset_definition "init_locs \<equiv> prefixed ''init''"
-locset_definition "mark_locs \<equiv> prefixed ''mark''"
-locset_definition "mark_loop_locs \<equiv> prefixed ''mark_loop''"
-locset_definition "sweep_locs \<equiv> prefixed ''sweep''"
+locset_definition "idle_locs = prefixed ''idle''"
+locset_definition "init_locs = prefixed ''init''"
+locset_definition "mark_locs = prefixed ''mark''"
+locset_definition "mark_loop_locs = prefixed ''mark_loop''"
+locset_definition "sweep_locs = prefixed ''sweep''"
 
 (*<*)
 
--- a/thys/ConcurrentGC/StrongTricolour.thy	Wed May 15 16:25:22 2019 +0100
+++ b/thys/ConcurrentGC/StrongTricolour.thy	Thu May 16 01:37:39 2019 +1000
@@ -887,39 +887,7 @@
 
 (*>*)
 
-subsection\<open>Lonely mutator assertions\<close>
-
-text\<open>
-
-The second assertion is key: after the \<open>''init_noop''\<close>
-handshake, we need to know that there are no pending white insertions
-(mutations that insert unmarked references) for the deletion barrier
-to work.
-
-\<close>
-
-locset_definition
-  "ghost_honorary_root_empty_locs \<equiv>
-     - (prefixed ''store_del'' \<union> {''lop_store_ins''} \<union> prefixed ''store_ins'')"
-
-definition (in mut_m) load_invL :: "('field, 'mut, 'ref) gc_pred" where
-[inv]: "load_invL \<equiv>
-    at_mut ''load''         (mut_tmp_ref \<^bold>\<in> mut_roots)
-  \<^bold>\<and> at_mut ''hs_noop_done'' (LIST_NULL (tso_pending_mutate (mutator m)))
-  \<^bold>\<and> atS_mut ghost_honorary_root_empty_locs (EMPTY mut_ghost_honorary_root)"
-(*<*)
-
-lemma (in mut_m) load_invL[intro]: "\<lbrace> load_invL \<rbrace> mutator m"
-by vcg_jackhammer
-
-lemma (in gc) load_invL[intro]: "\<lbrace> mut_m.load_invL m \<rbrace> gc"
-unfolding mut_m.load_invL_def by vcg_jackhammer
-
-lemma (in mut_m') load_invL[intro]: "\<lbrace> load_invL \<rbrace> mutator m'"
-by vcg_jackhammer
-
-lemma (in sys) load_invL[intro]: "\<lbrace> mut_m.load_invL m \<rbrace> sys"
-unfolding mut_m.load_invL_def by (vcg_jackhammer split: if_splits)
+subsection\<open> Mutator proofs \<close>
 
 lemma (in mut_m) reachable_snapshot_inv_hs_get_roots_done[simp]:
   assumes sti: "strong_tricolour_inv s"
@@ -1030,7 +998,7 @@
 by (clarsimp simp: reachable_snapshot_inv_def in_snapshot_def grey_protects_white_def)
 
 lemma (in mut_m) mutator_phase_inv[intro]:
-  "\<lbrace> handshake_invL \<^bold>\<and> load_invL
+  "\<lbrace> handshake_invL
        \<^bold>\<and> mark_object_invL
        \<^bold>\<and> mut_get_roots.mark_object_invL m
        \<^bold>\<and> mut_store_del.mark_object_invL m
@@ -1061,9 +1029,7 @@
   apply clarsimp
   apply (erule marked_insertions_store_ins)
   apply (drule phase_rel_invD)
-  apply (fastforce simp: phase_rel_def hp_step_rel_def
-                   dest: reachable_blackD
-                   elim: blackD)
+  apply (clarsimp simp: phase_rel_def hp_step_rel_def; elim disjE; fastforce dest: reachable_blackD elim: blackD)
  apply clarsimp
  apply (rule marked_deletions_store_ins, assumption) (* FIXME as above *)
  apply clarsimp
@@ -1608,11 +1574,11 @@
      \<union> prefixed ''mark_loop_get_roots''
      \<union> prefixed ''mark_loop_get_work''"
 
-locset_definition "black_heap_locs \<equiv> { ''sweep_idle'', ''idle_noop_mfence'', ''idle_noop_init_type'' }"
-locset_definition "no_grey_refs_locs \<equiv> black_heap_locs \<union> sweep_locs \<union> {''mark_end''}"
-
-definition (in gc) gc_W_empty_invL :: "('field, 'mut, 'ref) gc_pred" where
-[inv]: "gc_W_empty_invL =
+locset_definition "black_heap_locs = { ''sweep_idle'', ''idle_noop_mfence'', ''idle_noop_init_type'' }"
+locset_definition "no_grey_refs_locs = black_heap_locs \<union> sweep_locs \<union> {''mark_end''}"
+
+inv_definition (in gc) gc_W_empty_invL :: "('field, 'mut, 'ref) gc_pred" where
+  "gc_W_empty_invL =
    (atS_gc (hs_get_roots_locs \<union> hs_get_work_locs)  (\<^bold>\<forall>m. mut_m.gc_W_empty_mut_inv m)
   \<^bold>\<and> at_gc ''mark_loop_get_roots_load_W''          (EMPTY sys_W \<^bold>\<longrightarrow> no_grey_refs)
   \<^bold>\<and> at_gc ''mark_loop_get_work_load_W''           (EMPTY sys_W \<^bold>\<longrightarrow> no_grey_refs)
@@ -1905,10 +1871,10 @@
 
 subsection\<open>Sweep loop invariants\<close>
 
-locset_definition "sweep_loop_locs \<equiv> prefixed ''sweep_loop''"
-
-definition (in gc) sweep_loop_invL :: "('field, 'mut, 'ref) gc_pred" where
-[inv]: "sweep_loop_invL =
+locset_definition "sweep_loop_locs = prefixed ''sweep_loop''"
+
+inv_definition (in gc) sweep_loop_invL :: "('field, 'mut, 'ref) gc_pred" where
+  "sweep_loop_invL =
    (at_gc ''sweep_loop_check''        ( (\<^bold>\<not>(NULL gc_mark) \<^bold>\<longrightarrow> (\<lambda>s. obj_at (\<lambda>obj. Some (obj_mark obj) = gc_mark s) (gc_tmp_ref s) s))
                                       \<^bold>\<and> (  NULL gc_mark \<^bold>\<longrightarrow> valid_ref \<^bold>$ gc_tmp_ref \<^bold>\<longrightarrow> marked \<^bold>$ gc_tmp_ref ) )
   \<^bold>\<and> at_gc ''sweep_loop_free''         ( \<^bold>\<not>(NULL gc_mark) \<^bold>\<and> the \<circ> gc_mark \<^bold>\<noteq> gc_fM \<^bold>\<and> (\<lambda>s. obj_at (\<lambda>obj. Some (obj_mark obj) = gc_mark s) (gc_tmp_ref s) s) )
@@ -2876,7 +2842,7 @@
   notes mut_m_get_roots_no_fM_write[where m=m, simp]
   notes mut_m_get_roots_no_phase_write[where m=m, simp]
   notes mut_m_ghost_handshake_phase_not_hp_Idle[where m=m, simp]
-  notes atS_simps[simp]
+  notes atS_simps[simp] filter_empty_conv[simp]
   shows "\<lbrace> mut_m.handshake_invL m \<^bold>\<and> mut_m.mark_object_invL m
              \<^bold>\<and> LSTP (fA_rel_inv \<^bold>\<and> fM_rel_inv \<^bold>\<and> handshake_phase_inv \<^bold>\<and> mutators_phase_inv \<^bold>\<and> phase_rel_inv \<^bold>\<and> valid_refs_inv \<^bold>\<and> valid_W_inv \<^bold>\<and> tso_writes_inv) \<rbrace>
            sys
@@ -2933,7 +2899,7 @@
   apply (drule mp, erule atS_mono[OF _ subseteq_mut_mo_valid_ref_locs])
   apply ((thin_tac "atS p ls s \<longrightarrow> Q" for p ls s Q)+)[1]
   apply ((thin_tac "at p ls s \<longrightarrow> Q" for p ls s Q)+)[1]
-  apply (clarsimp simp: do_write_action_def filter_empty_conv p_not_sys loc
+  apply (clarsimp simp: do_write_action_def p_not_sys loc
                  split: mem_write_action.splits if_splits)
        apply (drule (1) valid_W_invD2)
        apply (erule obj_at_field_on_heap_weakenE)
@@ -2949,7 +2915,7 @@
      apply (clarsimp split: obj_at_splits option.splits)
       apply force
      apply (frule (1) marked_insertionsD)
-     apply (auto split: obj_at_splits)[1]
+     apply (auto split: obj_at_splits; fail)[1]
     apply (erule disjE) (* super messy case *)
      apply force
     apply (rule conjI)
@@ -2962,31 +2928,29 @@
     apply (frule spec[where x=m])
     apply (drule_tac x=ma in spec)
     apply (clarsimp simp: hp_step_rel_def)
-    apply (elim disjE, auto simp: phase_rel_def dest: marked_insertionsD)[1]
-   apply (erule disjE)
-    apply (drule mut_m.handshake_phase_invD[where m=m])
-    apply (clarsimp simp: fM_rel_inv_def fM_rel_def hp_step_rel_def)
-   apply force
-  apply (erule disjE)
+    apply (elim disjE, auto simp: phase_rel_def dest: marked_insertionsD; fail)[1]
+   apply (erule disjE; clarsimp)
    apply (drule mut_m.handshake_phase_invD[where m=m])
-   apply (drule phase_rel_invD)
-   apply (clarsimp simp: hp_step_rel_def phase_rel_def)
-  apply force
+   apply (clarsimp simp: fM_rel_inv_def fM_rel_def hp_step_rel_def)
+   apply (metis (no_types, lifting) handshake_phase.distinct(5) handshake_phase.distinct(7))
+  apply (erule disjE; clarsimp)
+  apply (drule mut_m.handshake_phase_invD[where m=m])
+  apply (drule phase_rel_invD)
+  apply (clarsimp simp: hp_step_rel_def phase_rel_def)
   done
 
 subgoal for s s' p w ws y
-  apply (clarsimp simp: do_write_action_def filter_empty_conv p_not_sys
+  apply (clarsimp simp: do_write_action_def p_not_sys
                  split: mem_write_action.splits if_splits)
-    apply (auto split: obj_at_splits)[1]
-   apply (erule disjE)
-    apply (drule mut_m.handshake_phase_invD[where m=m])
-    apply (clarsimp simp: fM_rel_inv_def fM_rel_def hp_step_rel_def)
-   apply force
-  apply (erule disjE)
+    apply (auto split: obj_at_splits; fail)[1]
+   apply (erule disjE; clarsimp)
    apply (drule mut_m.handshake_phase_invD[where m=m])
-   apply (drule phase_rel_invD)
-   apply (clarsimp simp: hp_step_rel_def phase_rel_def)
-  apply force
+   apply (clarsimp simp: fM_rel_inv_def fM_rel_def hp_step_rel_def)
+   apply (metis (no_types, lifting) handshake_phase.distinct(5) handshake_phase.distinct(7))
+  apply (erule disjE; clarsimp)
+  apply (drule mut_m.handshake_phase_invD[where m=m])
+  apply (drule phase_rel_invD)
+  apply (clarsimp simp: hp_step_rel_def phase_rel_def)
   done
 
 subgoal for s s' p w ws
@@ -2995,7 +2959,7 @@
   apply ((thin_tac "at p ls s \<longrightarrow> Q" for p ls s Q)+)[1]
   apply (subst do_write_action_fM[where m=m], simp_all)[1]
    apply (elim disjE, simp_all)[1]
-  apply (clarsimp simp: do_write_action_def filter_empty_conv p_not_sys
+  apply (clarsimp simp: do_write_action_def p_not_sys
                  split: mem_write_action.splits if_splits)
       apply (erule obj_at_field_on_heap_weakenE, auto)[1]
      apply (erule obj_at_field_on_heap_weakenE, auto split: obj_at_splits)[1]
@@ -3027,6 +2991,7 @@
    apply (clarsimp simp: hp_step_rel_def phase_rel_def)
   apply force
   done
+
 done
 
 lemma (in gc) mut_mark_object_invL[intro]:
@@ -3040,49 +3005,51 @@
          \<lbrace> mut_m.mark_object_invL m \<rbrace>"
 apply vcg_nihe
 apply vcg_ni
-  subgoal
-   apply (drule (1) mut_m_handshake_invL_get_roots)
-   apply clarsimp
-   done
-
- subgoal by (simp add: mut_m.handshake_invL_def)
-
- subgoal by (fastforce simp: fM_rel_inv_def fM_rel_def hp_step_rel_def split: obj_at_splits)
-
- subgoal
-   apply (drule mut_m.handshake_phase_invD[where m=m])
-   apply (drule spec[where x=m])
-   apply (clarsimp simp: valid_null_ref_def hp_step_rel_def conj_disj_distribR[symmetric] split: option.splits)
-   apply (drule (1) mut_m.reachable_blackD)
-    apply blast
-   apply (clarsimp split: obj_at_splits)
-   done
-
- subgoal
-   apply (drule mp, erule atS_mono[OF _ subseteq_mut_mo_valid_ref_locs])
-   apply ((thin_tac "atS p ls s \<longrightarrow> Q" for p ls s Q)+)[1]
-   apply ((thin_tac "at p ls s \<longrightarrow> Q" for p ls s Q)+)[1]
-   apply (drule mut_m.handshake_phase_invD[where m=m])
-   apply (drule spec[where x=m])
-   apply (clarsimp simp: valid_null_ref_def hp_step_rel_def conj_disj_distribR[symmetric] split: option.splits)
-   apply (drule (1) mut_m.reachable_blackD)
-    apply blast
-   apply (auto simp: obj_at_field_on_heap_def black_def split: obj_at_splits option.splits)[1]
-   done
-
- subgoal by (clarsimp split: obj_at_splits)
-
- subgoal
-   apply (drule mp, erule atS_mono[OF _ subseteq_mut_mo_valid_ref_locs2])
-   apply ((thin_tac "atS p ls s \<longrightarrow> Q" for p ls s Q)+)[1]
-   apply ((thin_tac "at p ls s \<longrightarrow> Q" for p ls s Q)+)[1]
-   apply (drule mut_m.handshake_phase_invD[where m=m])
-   apply (drule spec[where x=m])
-   apply (clarsimp simp: valid_null_ref_def hp_step_rel_def conj_disj_distribR[symmetric] split: option.splits)
-   apply (drule (1) mut_m.reachable_blackD)
-    apply blast
-   apply (auto simp: obj_at_field_on_heap_def black_def split: obj_at_splits option.splits)[1]
-  done
+
+subgoal
+ apply (drule (1) mut_m_handshake_invL_get_roots)
+ apply clarsimp
+ done
+
+subgoal by (simp add: mut_m.handshake_invL_def)
+
+subgoal by (fastforce simp: fM_rel_inv_def fM_rel_def hp_step_rel_def split: obj_at_splits)
+
+subgoal
+ apply (drule mut_m.handshake_phase_invD[where m=m])
+ apply (drule spec[where x=m])
+ apply (clarsimp simp: valid_null_ref_def hp_step_rel_def conj_disj_distribR[symmetric] split: option.splits)
+ apply (drule (1) mut_m.reachable_blackD)
+  apply blast
+ apply (clarsimp split: obj_at_splits)
+ done
+
+subgoal
+ apply (drule mp, erule atS_mono[OF _ subseteq_mut_mo_valid_ref_locs])
+ apply ((thin_tac "atS p ls s \<longrightarrow> Q" for p ls s Q)+)[1]
+ apply ((thin_tac "at p ls s \<longrightarrow> Q" for p ls s Q)+)[1]
+ apply (drule mut_m.handshake_phase_invD[where m=m])
+ apply (drule spec[where x=m])
+ apply (clarsimp simp: valid_null_ref_def hp_step_rel_def conj_disj_distribR[symmetric] split: option.splits)
+ apply (drule (1) mut_m.reachable_blackD)
+  apply blast
+ apply (auto simp: obj_at_field_on_heap_def black_def split: obj_at_splits option.splits)[1]
+ done
+
+subgoal by (clarsimp split: obj_at_splits)
+
+subgoal
+ apply (drule mp, erule atS_mono[OF _ subseteq_mut_mo_valid_ref_locs2])
+ apply ((thin_tac "atS p ls s \<longrightarrow> Q" for p ls s Q)+)[1]
+ apply ((thin_tac "at p ls s \<longrightarrow> Q" for p ls s Q)+)[1]
+ apply (drule mut_m.handshake_phase_invD[where m=m])
+ apply (drule spec[where x=m])
+ apply (clarsimp simp: valid_null_ref_def hp_step_rel_def conj_disj_distribR[symmetric] split: option.splits)
+ apply (drule (1) mut_m.reachable_blackD)
+  apply blast
+ apply (auto simp: obj_at_field_on_heap_def black_def split: obj_at_splits option.splits)[1]
+done
+
 done
 
 lemma (in gc) mut_store_old_mark_object_invL[intro]:
@@ -3376,8 +3343,7 @@
 by (clarsimp simp: valid_refs_inv_def)
 
 lemma (in mut_m) valid_refs_inv[intro]:
-  "\<lbrace> load_invL
-       \<^bold>\<and> mark_object_invL
+  "\<lbrace> mark_object_invL
        \<^bold>\<and> mut_get_roots.mark_object_invL m
        \<^bold>\<and> mut_store_del.mark_object_invL m
        \<^bold>\<and> mut_store_ins.mark_object_invL m
--- a/thys/ConcurrentGC/TSO.thy	Wed May 15 16:25:22 2019 +0100
+++ b/thys/ConcurrentGC/TSO.thy	Thu May 16 01:37:39 2019 +1000
@@ -113,12 +113,7 @@
 lemma (in sys) tso_gc_writes_inv[intro]:
   "\<lbrace> LSTP tso_writes_inv \<rbrace> sys"
 apply (vcg_jackhammer simp: tso_writes_inv_def)
-apply (rule conjI)
- apply force
-apply clarsimp
-apply (rename_tac x xa)
-apply (drule_tac x=x in spec) (* why??? *)
-apply simp
+apply (metis (no_types) list.set_intros(2))
 done
 
 lemma (in gc) tso_writes_inv[intro]:
@@ -143,10 +138,11 @@
 locset_definition gc_tso_lock_locs :: "location set" where
   "gc_tso_lock_locs \<equiv> \<Union>l\<in>{ ''mo_co_cmark'', ''mo_co_ctest'', ''mo_co_mark'', ''mo_co_unlock'' }. suffixed l"
 
-definition (in gc) tso_lock_invL :: "('field, 'mut, 'ref) gc_pred" where
-[inv]: "tso_lock_invL \<equiv>
+inv_definition (in gc) tso_lock_invL :: "('field, 'mut, 'ref) gc_pred" where
+  "tso_lock_invL \<equiv>
      atS_gc gc_tso_lock_locs (tso_locked_by gc)
    \<^bold>\<and> atS_gc (- gc_tso_lock_locs) (\<^bold>\<not> (tso_locked_by gc))"
+
 (*<*)
 
 lemma (in gc) tso_lock_invL[intro]:
@@ -171,13 +167,13 @@
 
 \<close>
 
-locset_definition "mut_tso_lock_locs \<equiv>
-  \<Union>l\<in>{ ''mo_co_cmark'', ''mo_co_ctest'', ''mo_co_mark'', ''mo_co_unlock'' }. suffixed l"
+locset_definition "mut_tso_lock_locs =
+  (\<Union>l\<in>{ ''mo_co_cmark'', ''mo_co_ctest'', ''mo_co_mark'', ''mo_co_unlock'' }. suffixed l)"
 
-definition (in mut_m) tso_lock_invL :: "('field, 'mut, 'ref) gc_pred" where
-[inv]: "tso_lock_invL \<equiv>
-     atS_mut mut_tso_lock_locs     (tso_locked_by (mutator m))
-   \<^bold>\<and> atS_mut (- mut_tso_lock_locs) (\<^bold>\<not>(tso_locked_by (mutator m)))"
+inv_definition (in mut_m) tso_lock_invL :: "('field, 'mut, 'ref) gc_pred" where
+  "tso_lock_invL =
+    (atS_mut mut_tso_lock_locs     (tso_locked_by (mutator m))
+   \<^bold>\<and> atS_mut (- mut_tso_lock_locs) (\<^bold>\<not>(tso_locked_by (mutator m))))"
 (*<*)
 
 lemma (in mut_m) tso_lock_invL[intro]:
--- a/thys/ConcurrentGC/Tactics.thy	Wed May 15 16:25:22 2019 +0100
+++ b/thys/ConcurrentGC/Tactics.thy	Thu May 16 01:37:39 2019 +1000
@@ -83,7 +83,6 @@
 
 subsection\<open>Tactics\<close>
 
-named_theorems inv "Location-sensitive invariant definitions"
 named_theorems nie "Non-interference elimination rules"
 
 text\<open>
@@ -247,6 +246,7 @@
              THEN' asm_full_simp_tac (ss_only (@{thms loc_simps} @ Named_Theorems.get ctxt @{named_theorems loc}) ctxt)
              THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (Rule_Insts.thin_tac ctxt "True" [])) (* FIXME weird, must be a standard way to do this. Leaving them in can cause simp to diverge ?? *)
              THEN_ALL_NEW clarsimp_tac (ctxt addsimps (Named_Theorems.get ctxt @{named_theorems loc} @ @{thms atS_simps})) (* FIXME smelly *)
+             THEN_ALL_NEW Rule_Insts.thin_tac ctxt "AT _ = _" [] (* FIXME discard \<open>AT s = s'(funupd)\<close> fact *)
              THEN_ALL_NEW TRY o terminal_tac ctxt)))
 
 val _ =
@@ -275,6 +275,7 @@
       THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (Tactic.ematch_tac ctxt @{thms thin_locs} THEN' REPEAT1 o assume_tac ctxt))
       THEN_ALL_NEW asm_full_simp_tac (ss_only (@{thms loc_simps} @ Named_Theorems.get ctxt @{named_theorems loc}) ctxt)
       THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (Rule_Insts.thin_tac ctxt "True" [])) (* FIXME weird, must be a standard way to do this. Leaving them in can cause simp to diverge ?? *)
+(*      THEN_ALL_NEW Rule_Insts.thin_tac ctxt "AT _ = _" [] (* FIXME discard \<open>AT s = s'(funupd)\<close> fact *) doesn't work when processes communicate! see gc_sweep_loop_invL *)
       THEN_ALL_NEW clarsimp_tac ctxt))
 
 fun vcg_nihe_tac ctxt =
--- a/thys/ConcurrentIMP/CIMP.thy	Wed May 15 16:25:22 2019 +0100
+++ b/thys/ConcurrentIMP/CIMP.thy	Thu May 16 01:37:39 2019 +1000
@@ -16,7 +16,7 @@
   CIMP_vcg
   "HOL-Library.Sublist"
 keywords
-  "locset_definition" :: thy_defn
+  "inv_definition" "locset_definition" :: thy_defn
 begin
 
 text\<open>
@@ -27,6 +27,7 @@
 \<close>
 
 named_theorems com "Command definitions"
+named_theorems inv "Location-sensitive invariant definitions"
 named_theorems loc "Location set membership cache"
 
 ML\<open>
@@ -35,7 +36,10 @@
 sig
     val com_locs_fold : (term -> 'b -> 'b) -> 'b -> term -> 'b
     val com_locs_map : (term -> 'b) -> term -> 'b list
-    val locset : thm -> local_theory -> local_theory
+    val com_locs_fold_no_response : (term -> 'b -> 'b) -> 'b -> term -> 'b
+    val com_locs_map_no_response : (term -> 'b) -> term -> 'b list
+    val def_inv : thm -> local_theory -> local_theory
+    val def_locset : thm -> local_theory -> local_theory
 end;
 
 structure Cimp : CIMP =
@@ -54,6 +58,19 @@
 
 fun com_locs_map f com = com_locs_fold (fn l => fn acc => f l :: acc) [] com
 
+fun com_locs_fold_no_response f x (Const (@{const_name Request}, _) $ l $ _ $ _ )    = f l x
+  | com_locs_fold_no_response _ x (Const (@{const_name Response}, _) $ _ $ _)        = x (* can often ignore \<open>Response\<close> *)
+  | com_locs_fold_no_response f x (Const (@{const_name LocalOp}, _) $ l $ _)         = f l x
+  | com_locs_fold_no_response f x (Const (@{const_name Cond1}, _) $ l $ _ $ c)       = com_locs_fold_no_response f (f l x) c
+  | com_locs_fold_no_response f x (Const (@{const_name Cond2}, _) $ l $ _ $ c1 $ c2) = com_locs_fold_no_response f (com_locs_fold_no_response f (f l x) c1) c2
+  | com_locs_fold_no_response f x (Const (@{const_name Loop}, _) $ c)                = com_locs_fold_no_response f x c
+  | com_locs_fold_no_response f x (Const (@{const_name While}, _) $ l $ _ $ c)       = com_locs_fold_no_response f (f l x) c
+  | com_locs_fold_no_response f x (Const (@{const_name Seq}, _) $ c1 $ c2)           = com_locs_fold_no_response f (com_locs_fold_no_response f x c1) c2
+  | com_locs_fold_no_response f x (Const (@{const_name Choose}, _) $ c1 $ c2)        = com_locs_fold_no_response f (com_locs_fold_no_response f x c1) c2
+  | com_locs_fold_no_response _ x _ = x;
+
+fun com_locs_map_no_response f com = com_locs_fold_no_response (fn l => fn acc => f l :: acc) [] com
+
 (* Cache location set membership facts.
 
 Decide membership in the given set for each label in the CIMP programs
@@ -61,42 +78,56 @@
 
 If the label set and com types differ, we probably get a nasty error.
 
-No need to consider locations of @{const "Response"}s; could tweak
-@{text "com_locs_fold"} to reflect this.
-
 *)
 
-fun locset thm ctxt =
+fun def_locset thm ctxt =
   let
-    val set_name = thm |> Thm.cprop_of |> Thm.dest_equals |> fst |> Thm.term_of (* FIXME how do we handle HOL (=) as well? maybe rule_format? *)
+    val set_name = thm
+                   |> Local_Defs.meta_rewrite_rule ctxt (* handle `=` or `\<equiv>` *)
+                   |> Thm.cprop_of |> Thm.dest_equals |> fst |> Thm.term_of
     val set_typ = set_name |> type_of
     val elt_typ = case set_typ of Type ("Set.set", [t]) => t | _ => raise Fail "thm should define a set"
-    val set_name_str = case set_name of Const (c, _) => c | Free (c, _) => c | _ => raise Fail "FIXME not a constant XXX" (* FIXME `definition` spits out a thm with a Free in it *)
-    val thm_name = set_name_str |> Long_Name.base_name |> (fn def => def ^ "_membs")
+    val set_name_str = case set_name of Const (c, _) => c | Free (c, _) => c | _ => error ("Not an equation of the form x = set: " ^ Thm.string_of_thm ctxt thm)
+    val thm_name = Binding.qualify true set_name_str (Binding.name "memb")
     fun mk_memb l = Thm.cterm_of ctxt (Const (@{const_name "Set.member"}, elt_typ --> set_typ --> @{typ "bool"}) $ l $ set_name)
     val rewrite_tac = Simplifier.rewrite (ctxt addsimps ([thm] @ Named_Theorems.get ctxt @{named_theorems "loc"})) (* probably want the ambient simpset + some stuff *)
     val coms = Named_Theorems.get ctxt @{named_theorems "com"} |> map (Thm.cprop_of #> Thm.dest_equals #> snd #> Thm.term_of)
     val attrs = [(* Attrib.internal (K (Clasimp.iff_add)), *) Attrib.internal (K (Named_Theorems.add @{named_theorems "loc"}))]
 (* Parallel *)
-    fun mk_thms coms = Par_List.map rewrite_tac (maps (com_locs_map mk_memb) coms)
+    fun mk_thms coms = Par_List.map rewrite_tac (maps (com_locs_map_no_response mk_memb) coms)
 (* Sequential *)
 (*    fun mk_thms coms = List.foldl (fn (c, thms) => com_locs_fold (fn l => fn thms => rewrite_tac (mk_memb l) :: thms) thms c) [] coms *)
   in
     ctxt
-    |> (Local_Theory.note ((Binding.name thm_name, attrs), mk_thms coms) #>> snd)
+    |> Local_Theory.note ((thm_name, attrs), mk_thms coms)
+    |> snd
+  end;
+
+(* FIXME later need to rewrite using interned labels (fold defs). *)
+fun def_inv thm ctxt : local_theory =
+  let
+    val attrs = [Attrib.internal (K (Named_Theorems.add @{named_theorems "inv"}))]
+  in
+    ctxt
+    |> Local_Theory.note ((Binding.empty, attrs), [thm])
     |> snd
   end;
 
 end;
 
-(* `definition` + `locset` *)
+val _ =
+  Outer_Syntax.local_theory' \<^command_keyword>\<open>inv_definition\<close> "constant definition for invariants"
+    (Scan.option Parse_Spec.constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop) --
+      Parse_Spec.if_assumes -- Parse.for_fixes >> (fn (((decl, spec), prems), params) => fn b => fn lthy =>
+        Specification.definition_cmd decl params prems spec b lthy
+        |> (fn ((_, (_, thm)), lthy) => (thm, lthy)) |> uncurry Cimp.def_inv));
+
 val _ =
   Outer_Syntax.local_theory' \<^command_keyword>\<open>locset_definition\<close> "constant definition for sets of locations"
     (Scan.option Parse_Spec.constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop) --
       Parse_Spec.if_assumes -- Parse.for_fixes >> (fn (((decl, spec), prems), params) => fn b => fn lthy =>
         Specification.definition_cmd decl params prems spec b lthy
-        |> (fn ((_, (_, thm)), lthy) => (thm, lthy)) |> uncurry Cimp.locset));
-
+        |> (fn ((_, (_, thm)), lthy) => (thm, lthy)) |> uncurry Cimp.def_locset));
 \<close>
 
 end

mercurial