Theory FWLTS

(*  Title:      JinjaThreads/Framework/FWLTS.thy
    Author:     Andreas Lochbihler
*)

section ‹The multithreaded semantics as a labelled transition system›

theory FWLTS
imports
  FWProgressAux
  FWLifting
  LTS
begin

sublocale multithreaded_base < trsys "r t" for t .
sublocale multithreaded_base < mthr: trsys redT .

― ‹Move to FWSemantics?›
definition redT_upd_ε :: "('l,'t,'x,'m,'w) state  't  'x  'm  ('l,'t,'x,'m,'w) state"
where [simp]: "redT_upd_ε s t x' m' = (locks s, ((thr s)(t  (x', snd (the (thr s t)))), m'), wset s, interrupts s)"

lemma redT_upd_ε_redT_upd:
  "redT_upd s t ε x' m' (redT_upd_ε s t x' m')"
by(auto simp add: redT_updLns_def redT_updWs_def)

context multithreaded begin
  
sublocale trsys "r t" for t .
    
sublocale mthr: trsys redT .
    
end
  
subsection ‹The multithreaded semantics with internal actions›

type_synonym
  ('l,'t,'x,'m,'w,'o) τmoves =
    "'x × 'm  ('l,'t,'x,'m,'w,'o) thread_action  'x × 'm  bool"

text ‹pretty printing for τmoves›
print_translation let
    fun tr' [(Const (@{type_syntax "prod"}, _) $ x1 $ m1),
             (Const (@{type_syntax "fun"}, _) $
               (Const (@{type_syntax "prod"}, _) $ 
                 (Const (@{type_syntax "finfun"}, _) $ l $ 
                   (Const (@{type_syntax "list"}, _) $ Const (@{type_syntax "lock_action"}, _))) $
                 (Const (@{type_syntax "prod"},_) $ 
                   (Const (@{type_syntax "list"}, _) $ (Const (@{type_syntax "new_thread_action"}, _) $ t1 $ x2 $ m2)) $
                   (Const (@{type_syntax "prod"}, _) $ 
                     (Const (@{type_syntax "list"}, _) $ (Const (@{type_syntax "conditional_action"}, _) $ t2)) $
                     (Const (@{type_syntax "prod"}, _) $ 
                       (Const (@{type_syntax "list"}, _) $ (Const (@{type_syntax "wait_set_action"}, _) $ t3 $ w)) $
                       (Const (@{type_syntax prod}, _) $ 
                         (Const (@{type_syntax list}, _) $ (Const (@{type_syntax "interrupt_action"}, _) $ t4)) $
                         (Const (@{type_syntax "list"}, _) $ o1)))))) $
               (Const (@{type_syntax "fun"}, _) $ 
                 (Const (@{type_syntax "prod"}, _) $ x3 $ m3) $
                 (Const (@{type_syntax "bool"}, _))))] =
      if x1 = x2 andalso x1 = x3 andalso m1 = m2 andalso m1 = m3 andalso t1 = t2 andalso t2 = t3 andalso t3 = t4
      then Syntax.const (@{type_syntax "τmoves"}) $ l $ t1 $ x1 $ m1 $ w $ o1
      else raise Match;
  in [(@{type_syntax "fun"}, K tr')]
  end
typ "('l,'t,'x,'m,'w,'o) τmoves"

locale τmultithreaded = multithreaded_base +
  constrains final :: "'x  bool"
  and r :: "('l,'t,'x,'m,'w,'o) semantics"
  and convert_RA :: "'l released_locks  'o list"
  fixes τmove :: "('l,'t,'x,'m,'w,'o) τmoves"

sublocale τmultithreaded < τtrsys "r t" τmove for t .

context τmultithreaded begin

inductive mτmove :: "(('l,'t,'x,'m,'w) state, 't × ('l,'t,'x,'m,'w,'o) thread_action) trsys"
where
  " thr s t = (x, no_wait_locks); thr s' t = (x', ln'); τmove (x, shr s) ta (x', shr s') 
   mτmove s (t, ta) s'"

end

sublocale τmultithreaded < mthr: τtrsys redT mτmove .

context τmultithreaded begin

abbreviation τmredT :: "('l,'t,'x,'m,'w) state  ('l,'t,'x,'m,'w) state  bool"
where "τmredT == mthr.silent_move"

end

lemma (in multithreaded_base) τrtrancl3p_redT_thread_not_disappear:
  assumes "τtrsys.τrtrancl3p redT τmove s ttas s'" "thr s t  None"
  shows "thr s' t  None"
proof -
  interpret T: τtrsys redT τmove .
  show ?thesis
  proof
    assume "thr s' t = None"
    with τtrsys.τrtrancl3p redT τmove s ttas s' have "thr s t = None"
      by(induct rule: T.τrtrancl3p.induct)(auto simp add: split_paired_all dest: redT_thread_not_disappear)
    with thr s t  None show False by contradiction
  qed
qed

lemma mτmove_False: "τmultithreaded.mτmove (λs ta s'. False) = (λs ta s'. False)"
by(auto intro!: ext elim: τmultithreaded.mτmove.cases)

declare split_paired_Ex [simp del]

locale τmultithreaded_wf =
  τmultithreaded _ _ _ τmove +
  multithreaded final r convert_RA
  for τmove :: "('l,'t,'x,'m,'w,'o) τmoves" +
  assumes τmove_heap: " t  (x, m) -ta (x', m'); τmove (x, m) ta (x', m')   m = m'"
  assumes silent_tl: "τmove s ta s'  ta = ε"
begin

lemma mτmove_silentD: "mτmove s (t, ta) s'  ta = (K$ [], [], [], [], [], [])"
by(auto elim!: mτmove.cases dest: silent_tl)

lemma mτmove_heap: 
  assumes redT: "redT s (t, ta) s'"
  and mτmove: "mτmove s (t, ta) s'"
  shows "shr s' = shr s"
using mτmove redT
by cases(auto dest: τmove_heap elim!: redT.cases)

lemma τmredT_thread_preserved:
  "τmredT s s'  thr s t = None  thr s' t = None"
by(auto simp add: mthr.silent_move_iff elim!: redT.cases dest!: mτmove_silentD split: if_split_asm)

lemma τmRedT_thread_preserved:
  "τmredT^** s s'  thr s t = None  thr s' t = None"
by(induct rule: rtranclp.induct)(auto dest: τmredT_thread_preserved[where t=t])

lemma τmtRedT_thread_preserved:
  "τmredT^++ s s'  thr s t = None  thr s' t = None"
by(induct rule: tranclp.induct)(auto dest: τmredT_thread_preserved[where t=t])

lemma τmredT_add_thread_inv:
  assumes τred: "τmredT s s'" and tst: "thr s t = None"
  shows "τmredT (locks s, ((thr s)(t  xln), shr s), wset s, interrupts s) (locks s', ((thr s')(t  xln), shr s'), wset s', interrupts s')"
proof -
  obtain ls ts m ws "is" where s: "s = (ls, (ts, m), ws, is)" by(cases s) fastforce
  obtain ls' ts' m' ws' is' where s': "s' = (ls', (ts', m'), ws', is')" by(cases s') fastforce
  from τred s s' obtain t' where red: "(ls, (ts, m), ws, is) -t'ε (ls', (ts', m'), ws', is')"
    and τ: "mτmove (ls, (ts, m), ws, is) (t', ε) (ls', (ts', m'), ws', is')"
    by(auto simp add: mthr.silent_move_iff dest: mτmove_silentD)
  from red have "(ls, (ts(t  xln), m), ws, is) -t'ε (ls', (ts'(t  xln), m'), ws', is')"
  proof(cases rule: redT_elims)
    case (normal x x' m') with tst s show ?thesis
      by-(rule redT_normal, auto simp add: fun_upd_twist elim!: rtrancl3p_cases)
  next
    case (acquire x ln n)
    with tst s show ?thesis
      unfolding ε = (K$ [], [], [], [], [], convert_RA ln)
      by -(rule redT_acquire, auto intro: fun_upd_twist)
  qed
  moreover from red tst s have tt': "t  t'" by(cases) auto
  have "(λt''. (ts(t  xln)) t''  None  (ts(t  xln)) t''  (ts'(t  xln)) t'') =
        (λt''. ts t''  None  ts t''  ts' t'')" using tst s by(auto simp add: fun_eq_iff)
  with τ tst tt' have "mτmove (ls, (ts(t  xln), m), ws, is) (t', ε) (ls', (ts'(t  xln), m'), ws', is')"
    by cases(rule mτmove.intros, auto)
  ultimately show ?thesis unfolding s s' by auto
qed

lemma τmRedT_add_thread_inv:
  " τmredT^** s s'; thr s t = None 
   τmredT^** (locks s, ((thr s)(t  xln), shr s), wset s, interrupts s) (locks s', ((thr s')(t  xln), shr s'), wset s', interrupts s')"
apply(induct rule: rtranclp_induct)
apply(blast dest: τmRedT_thread_preserved[where t=t] τmredT_add_thread_inv[where xln=xln] intro: rtranclp.rtrancl_into_rtrancl)+
done

lemma τmtRed_add_thread_inv:
  " τmredT^++ s s'; thr s t = None 
   τmredT^++ (locks s, ((thr s)(t  xln), shr s), wset s, interrupts s) (locks s', ((thr s')(t  xln), shr s'), wset s', interrupts s')"
apply(induct rule: tranclp_induct)
apply(blast dest: τmtRedT_thread_preserved[where t=t] τmredT_add_thread_inv[where xln=xln] intro: tranclp.trancl_into_trancl)+
done

lemma silent_move_into_RedT_τ_inv:
  assumes move: "silent_move t (x, shr s) (x', m')"
  and state: "thr s t = (x, no_wait_locks)" "wset s t = None"
  shows "τmredT s (redT_upd_ε s t x' m')"
proof -
  from move obtain red: "t  (x, shr s) -ε (x', m')" and τ: "τmove (x, shr s) ε (x', m')"
    by(auto simp add: silent_move_iff dest: silent_tl)
  from red state have "s -tε redT_upd_ε s t x' m'"
    by -(rule redT_normal, auto simp add: redT_updLns_def o_def finfun_Diag_const2 redT_updWs_def)
  moreover from τ red state have "mτmove s (t, ε) (redT_upd_ε s t x' m')"
    by -(rule mτmove.intros, auto dest: τmove_heap simp add: redT_updLns_def)
  ultimately show ?thesis by auto
qed

lemma silent_moves_into_RedT_τ_inv:
  assumes major: "silent_moves t (x, shr s) (x', m')"
  and state: "thr s t = (x, no_wait_locks)" "wset s t = None"
  shows "τmredT^** s (redT_upd_ε s t x' m')"
using major
proof(induct rule: rtranclp_induct2)
  case refl with state show ?case by(cases s)(auto simp add: fun_upd_idem)
next
  case (step x' m' x'' m'')
  from silent_move t (x', m') (x'', m'') state
  have "τmredT (redT_upd_ε s t x' m') (redT_upd_ε (redT_upd_ε s t x' m') t x'' m'')"
    by -(rule silent_move_into_RedT_τ_inv, auto)
  hence "τmredT (redT_upd_ε s t x' m') (redT_upd_ε s t x'' m'')" by(simp)
  with τmredT^** s (redT_upd_ε s t x' m') show ?case ..
qed

lemma red_rtrancl_τ_heapD_inv:
  " silent_moves t s s'; wfs t s   snd s' = snd s"
proof(induct rule: rtranclp_induct)
  case base show ?case ..
next
  case (step s' s'')
  thus ?case by(cases s, cases s', cases s'')(auto dest: τmove_heap)
qed

lemma red_trancl_τ_heapD_inv:
  " silent_movet t s s'; wfs t s   snd s' = snd s"
proof(induct rule: tranclp_induct)
  case (base s') thus ?case by(cases s')(cases s, auto simp add: silent_move_iff dest: τmove_heap)
next
  case (step s' s'')
  thus ?case by(cases s, cases s', cases s'')(auto simp add: silent_move_iff dest: τmove_heap)
qed

lemma red_trancl_τ_into_RedT_τ_inv:
  assumes major: "silent_movet t (x, shr s) (x', m')"
  and state: "thr s t = (x, no_wait_locks)" "wset s t = None"
  shows "τmredT^++ s (redT_upd_ε s t x' m')"
using major
proof(induct rule: tranclp_induct2)
  case (base x' m')
  thus ?case using state
    by -(rule tranclp.r_into_trancl, rule silent_move_into_RedT_τ_inv, auto)
next
  case (step x' m' x'' m'')
  hence "τmredT^++ s (redT_upd_ε s t x' m')" by blast
  moreover from silent_move t (x', m') (x'', m'') state
  have "τmredT (redT_upd_ε s t x' m') (redT_upd_ε (redT_upd_ε s t x' m') t x'' m'')"
    by -(rule silent_move_into_RedT_τ_inv, auto simp add: redT_updLns_def)
  hence "τmredT (redT_upd_ε s t x' m') (redT_upd_ε s t x'' m'')"
    by(simp add: redT_updLns_def)
  ultimately show ?case ..
qed

lemma τdiverge_into_τmredT:
  assumes "τdiverge t (x, shr s)"
  and "thr s t = (x, no_wait_locks)" "wset s t = None"
  shows "mthr.τdiverge s"
using assms
proof(coinduction arbitrary: s x)
  case (τdiverge s x)
  note tst = thr s t = (x, no_wait_locks)
  from τdiverge t (x, shr s) obtain x' m' where "silent_move t (x, shr s) (x', m')" 
    and "τdiverge t (x', m')" by cases auto
  from silent_move t (x, shr s) (x', m') tst wset s t = None
  have "τmredT s (redT_upd_ε s t x' m')" by(rule silent_move_into_RedT_τ_inv)
  moreover have "thr (redT_upd_ε s t x' m') t = (x', no_wait_locks)"
    using tst by(auto simp add: redT_updLns_def)
  moreover have "wset (redT_upd_ε s t x' m') t = None" using wset s t = None by simp
  moreover from τdiverge t (x', m') have "τdiverge t (x', shr (redT_upd_ε s t x' m'))" by simp
  ultimately show ?case using τdiverge t (x', m') by blast
qed

lemma τdiverge_τmredTD:
  assumes div: "mthr.τdiverge s"
  and fin: "finite (dom (thr s))"
  shows "t x. thr s t = (x, no_wait_locks)  wset s t = None  τdiverge t (x, shr s)"
using fin div
proof(induct A"dom (thr s)" arbitrary: s rule: finite_induct)
  case empty
  from mthr.τdiverge s obtain s' where "τmredT s s'" by cases auto
  with {} = dom (thr s)[symmetric] have False by(auto elim!: mthr.silent_move.cases redT.cases)
  thus ?case ..
next
  case (insert t A)
  note IH = s.  A = dom (thr s); mthr.τdiverge s 
              t x. thr s t = (x, no_wait_locks)  wset s t = None  τdiverge t (x, shr s)
  from insert t A = dom (thr s)
  obtain x ln where tst: "thr s t = (x, ln)" by(fastforce simp add: dom_def)
  define s' where "s' = (locks s, ((thr s)(t := None), shr s), wset s, interrupts s)"
  show ?case
  proof(cases "ln = no_wait_locks  τdiverge t (x, shr s)  wset s t = None")
    case True
    with tst show ?thesis by blast
  next
    case False
    define xm where "xm = (x, shr s)"
    define xm' where "xm' = (x, shr s)"
    have "A = dom (thr s')" using t  A insert t A = dom (thr s)
      unfolding s'_def by auto
    moreover { 
      from xm'_def tst mthr.τdiverge s False
      have "s x. thr s t = (x, ln)  (ln  no_wait_locks  wset s t  None  ¬ τdiverge t xm') 
                  s' = (locks s, ((thr s)(t := None), shr s), wset s, interrupts s)  xm = (x, shr s)  
                  mthr.τdiverge s  silent_moves t xm' xm"
        unfolding s'_def xm_def by blast
      moreover
      from False have "wfP (if τdiverge t xm' then (λs s'. False) else flip (silent_move_from t xm'))"
        using τdiverge_neq_wfP_silent_move_from[of t "(x, shr s)"] unfolding xm'_def by(auto)
      ultimately have "mthr.τdiverge s'"
      proof(coinduct s' xm rule: mthr.τdiverge_trancl_measure_coinduct)
        case (τdiverge s' xm)
        then obtain s x where tst: "thr s t = (x, ln)"
          and blocked: "ln  no_wait_locks  wset s t  None  ¬ τdiverge t xm'"
          and s'_def: "s' = (locks s, ((thr s)(t := None), shr s), wset s, interrupts s)"
          and xm_def: "xm = (x, shr s)"
          and xmxm': "silent_moves t xm' (x, shr s)"
          and "mthr.τdiverge s" by blast
        from mthr.τdiverge s obtain s'' where "τmredT s s''" "mthr.τdiverge s''" by cases auto
        from τmredT s s'' obtain t' ta where "s -t'ta s''" and "mτmove s (t', ta) s''" by auto
        then obtain x' x'' m'' where red: "t'  x', shr s -ta x'', m''"
          and tst': "thr s t' = (x', no_wait_locks)" 
          and aoe: "actions_ok s t' ta"
          and s'': "redT_upd s t' ta x'' m'' s''"
          by cases(fastforce elim: mτmove.cases)+
        from mτmove s (t', ta) s'' have [simp]: "ta = ε"
          by(auto elim!: mτmove.cases dest!: silent_tl)
        hence wst': "wset s t' = None" using aoe by auto
        from mτmove s (t', ta) s'' tst' s''
        have "τmove (x', shr s) ε (x'', m'')" by(auto elim: mτmove.cases)
        show ?case
        proof(cases "t' = t")
          case False
          with tst' wst' have "thr s' t' = (x', no_wait_locks)"
            "wset s' t' = None" "shr s' = shr s" unfolding s'_def by auto
          with red have "s' -t'ε redT_upd_ε s' t' x'' m''"
            by -(rule redT_normal, auto simp add: redT_updLns_def o_def finfun_Diag_const2 redT_updWs_def)
          moreover from τmove (x', shr s) ε (x'', m'') thr s' t' = (x', no_wait_locks) shr s' = shr s
          have "mτmove s' (t', ta) (redT_upd_ε s' t' x'' m'')"
            by -(rule mτmove.intros, auto)
          ultimately have "τmredT s' (redT_upd_ε s' t' x'' m'')"
            unfolding ta = ε by(rule mthr.silent_move.intros)
          hence "τmredT^++ s' (redT_upd_ε s' t' x'' m'')" ..
          moreover have "thr s'' t = (x, ln)"
            using tst t'  t s'' by auto
          moreover from τmove (x', shr s) ε (x'', m'') red
          have [simp]: "m'' = shr s" by(auto dest: τmove_heap)
          hence "shr s = shr s''" using s'' by(auto)
          have "ln  no_wait_locks  wset s'' t  None  ¬ τdiverge t xm'"
            using blocked s'' by(auto simp add: redT_updWs_def elim!: rtrancl3p_cases)
          moreover have "redT_upd_ε s' t' x'' m'' = (locks s'', ((thr s'')(t := None), shr s''), wset s'', interrupts s'')"
            unfolding s'_def using tst s'' t'  t
            by(auto intro: ext elim!: rtrancl3p_cases simp add: redT_updLns_def redT_updWs_def)
          ultimately show ?thesis using mthr.τdiverge s'' xmxm'
            unfolding shr s = shr s'' by blast
        next
          case True
          with tst tst' wst' blocked have "¬ τdiverge t xm'"
            and [simp]: "x' = x" by auto
          moreover from red τmove (x', shr s) ε (x'', m'') True
          have "silent_move t (x, shr s) (x'', m'')" by auto
          with xmxm' have "silent_move_from t xm' (x, shr s) (x'', m'')"
            by(rule silent_move_fromI)
          ultimately have "(if τdiverge t xm' then λs s'. False else flip (silent_move_from t xm')) (x'', m'') xm"
            by(auto simp add: flip_conv xm_def)
          moreover have "thr s'' t = (x'', ln)" using tst True s''
            by(auto simp add: redT_updLns_def)
          moreover from τmove (x', shr s) ε (x'', m'') red
          have [simp]: "m'' = shr s" by(auto dest: τmove_heap)
          hence "shr s = shr s''" using s'' by auto
          have "s' = (locks s'', ((thr s'')(t := None), shr s''), wset s'', interrupts s'')"
            using True s'' unfolding s'_def 
            by(auto intro: ext elim!: rtrancl3p_cases simp add: redT_updLns_def redT_updWs_def)
          moreover have "(x'', m'') = (x'', shr s'')" using s'' by auto
          moreover from xmxm' silent_move t (x, shr s) (x'', m'')
          have "silent_moves t xm' (x'', shr s'')"
            unfolding m'' = shr s shr s = shr s'' by auto
          ultimately show ?thesis using ¬ τdiverge t xm' mthr.τdiverge s'' by blast
        qed
      qed }
    ultimately have "t x. thr s' t = (x, no_wait_locks)  wset s' t = None  τdiverge t (x, shr s')" by(rule IH)
    then obtain t' x' where "thr s' t' = (x', no_wait_locks)"
      and "wset s' t' = None" and "τdiverge t' (x', shr s')" by blast
    moreover with False have "t'  t" by(auto simp add: s'_def)
    ultimately have "thr s t' = (x', no_wait_locks)" "wset s t' = None" "τdiverge t' (x', shr s)"
      unfolding s'_def by auto
    thus ?thesis by blast
  qed
qed

lemma τmredT_preserves_final_thread:
  " τmredT s s'; final_thread s t   final_thread s' t"
by(auto elim: mthr.silent_move.cases intro: redT_preserves_final_thread)

lemma τmRedT_preserves_final_thread:
  " τmredT^** s s'; final_thread s t   final_thread s' t"
by(induct rule: rtranclp.induct)(blast intro: τmredT_preserves_final_thread)+

lemma silent_moves2_silentD:
  assumes "rtrancl3p mthr.silent_move2 s ttas s'"
  and "(t, ta)  set ttas"
  shows "ta = ε"
using assms
by(induct)(auto simp add: mthr.silent_move2_def dest: mτmove_silentD)

lemma inf_step_silentD:
  assumes step: "trsys.inf_step mthr.silent_move2 s ttas"
  and lset: "(t, ta)  lset ttas"
  shows "ta = ε"
using lset step
by(induct arbitrary: s rule: lset_induct)(fastforce elim: trsys.inf_step.cases simp add: mthr.silent_move2_def dest: mτmove_silentD)+

end

subsection ‹The multithreaded semantics with a well-founded relation on states›

locale multithreaded_base_measure = multithreaded_base +
  constrains final :: "'x  bool"
  and r :: "('l,'t,'x,'m,'w,'o) semantics"
  and convert_RA :: "'l released_locks  'o list"
  fixes μ :: "('x × 'm)  ('x × 'm)  bool"
begin

inductive mμt :: "'m  ('l,'t,'x) thread_info  ('l,'t,'x) thread_info  bool"
for m and ts and ts'
where
  mμtI:
  "ln.  finite (dom ts); ts t = (x, ln); ts' t = (x', ln'); μ (x, m) (x', m); t'. t'  t  ts t' = ts' t' 
   mμt m ts ts'"

definition  :: "('l,'t,'x,'m,'w) state  ('l,'t,'x,'m,'w) state  bool"
where " s s'  shr s = shr s'  mμt (shr s) (thr s) (thr s')"

lemma mμt_thr_dom_eq: "mμt m ts ts'  dom ts = dom ts'"
apply(erule mμt.cases)
apply(rule equalityI)
 apply(rule subsetI)
 apply(case_tac "xa = t")
  apply(auto)[2]
apply(rule subsetI)
apply(case_tac "xa = t")
apply auto
done

lemma mμ_finite_thrD:
  assumes "mμt m ts ts'"
  shows "finite (dom ts)" "finite (dom ts')"
using assms
by(simp_all add: mμt_thr_dom_eq[symmetric])(auto elim: mμt.cases)

end

locale multithreaded_base_measure_wf = multithreaded_base_measure +
  constrains final :: "'x  bool"
  and r :: "('l,'t,'x,'m,'w,'o) semantics"
  and convert_RA :: "'l released_locks  'o list"
  and μ :: "('x × 'm)  ('x × 'm)  bool"
  assumes wf_μ: "wfP μ"
begin

lemma wf_mμt: "wfP (mμt m)"
unfolding wfp_eq_minimal
proof(intro strip)
  fix Q :: "('l,'t,'x) thread_info set" and ts
  assume "ts  Q"
  show "zQ. y. mμt m y z  y  Q"
  proof(cases "finite (dom ts)")
    case False
    hence "y. mμt m y ts  y  Q" by(auto dest: mμ_finite_thrD)
    thus ?thesis using ts  Q by blast
  next
    case True
    thus ?thesis using ts  Q
    proof(induct A"dom ts" arbitrary: ts Q rule: finite_induct)
      case empty
      hence "dom ts = {}" by simp
      with ts  Q show ?case by(auto elim: mμt.cases)
    next
      case (insert t A)
      note IH = ts Q. A = dom ts; ts  Q  zQ. y. mμt m y z  y  Q
      define Q' where "Q' = {ts. ts t = None  (xln. ts(t  xln)  Q)}"
      let ?ts' = "ts(t := None)"
      from insert t A = dom ts t  A have "A = dom ?ts'" by auto
      moreover from insert t A = dom ts obtain xln where "ts t = xln" by(cases "ts t") auto
      hence "ts(t  xln) = ts" by(auto simp add: fun_eq_iff)
      with ts  Q have "ts(t  xln)  Q" by(auto)
      hence "?ts'  Q'" unfolding Q'_def by(auto simp del: split_paired_Ex)
      ultimately have "zQ'. y. mμt m y z  y  Q'" by(rule IH)
      then obtain ts' where "ts'  Q'" 
        and min: "ts''. mμt m ts'' ts'  ts''  Q'" by blast
      from ts'  Q' obtain x' ln' where "ts' t = None" "ts'(t  (x', ln'))  Q"
        unfolding Q'_def by auto
      define Q'' where "Q'' = {(x, m)|x. ln. ts'(t  (x, ln))  Q}"
      from ts'(t  (x', ln'))  Q have "(x', m)  Q''" unfolding Q''_def by blast
      hence "xm''Q''. xm'''. μ xm''' xm''  xm'''  Q''" by(rule wf_μ[unfolded wfp_eq_minimal, rule_format])
      then obtain xm'' where "xm''  Q''" and min': "xm'''. μ xm''' xm''  xm'''  Q''" by blast
      from xm''  Q'' obtain x'' ln'' where "xm'' = (x'', m)" "ts'(t  (x'', ln''))  Q" unfolding Q''_def by blast
      moreover {
        fix ts''
        assume "mμt m ts'' (ts'(t  (x'', ln'')))"
        then obtain T X'' LN'' X' LN'
          where "finite (dom ts'')" "ts'' T = (X'', LN'')" 
          and "(ts'(t  (x'', ln''))) T = (X', LN')" "μ (X'', m) (X', m)"
          and eq: "t'. t'  T  ts'' t' = (ts'(t  (x'', ln''))) t'" by(cases) blast
        have "ts''  Q"
        proof(cases "T = t")
          case True
          from True (ts'(t  (x'', ln''))) T = (X', LN') have "X' = x''" by simp
          with μ (X'', m) (X', m) have "(X'', m)  Q''" by(auto dest: min'[unfolded xm'' = (x'', m)])
          hence "ln. ts'(t  (X'', ln))  Q" by(simp add: Q''_def)
          moreover from ts' t = None eq True
          have "ts''(t := None) = ts'" by(auto simp add: fun_eq_iff)
          with ts'' T = (X'', LN'') True
          have ts'': "ts'' = ts'(t  (X'', LN''))" by(auto intro!: ext)
          ultimately show ?thesis by blast
        next
          case False
          from finite (dom ts'') have "finite (dom (ts''(t := None)))" by simp
          moreover from ts'' T = (X'', LN'') False
          have "(ts''(t := None)) T = (X'', LN'')" by simp
          moreover from (ts'(t  (x'', ln''))) T = (X', LN') False
          have "ts' T = (X', LN')" by simp
          ultimately have "mμt m (ts''(t := None)) ts'" using μ (X'', m) (X', m)
          proof(rule mμtI)
            fix t'
            assume "t'  T"
            with eq[OF False[symmetric]] eq[OF this] ts' t = None
            show "(ts''(t := None)) t' = ts' t'" by auto
          qed
          hence "ts''(t := None)  Q'" by(rule min)
          thus ?thesis
          proof(rule contrapos_nn)
            assume "ts''  Q"
            from eq[OF False[symmetric]] have "ts'' t = (x'', ln'')" by simp
            hence ts'': "ts''(t  (x'', ln'')) = ts''" by(auto simp add: fun_eq_iff)
            from ts''  Q have "ts''(t  (x'', ln''))  Q" unfolding ts'' .
            thus "ts''(t := None)  Q'" unfolding Q'_def by auto
          qed
        qed
      }
      ultimately show ?case by blast
    qed
  qed
qed

lemma wf_mμ: "wfP "
proof -
  have "wf (inv_image (same_fst (λm. True) (λm. {(ts, ts'). mμt m ts ts'})) (λs. (shr s, thr s)))"
    by(rule wf_inv_image)(rule wf_same_fst, rule wf_mμt[unfolded wfp_def])
  also have "inv_image (same_fst (λm. True) (λm. {(ts, ts'). mμt m ts ts'})) (λs. (shr s, thr s)) = {(s, s').  s s'}"
    by(auto simp add: mμ_def same_fst_def)
  finally show ?thesis by(simp add: wfp_def)
qed

end

end