Theory MMonad

section State-Exception-Nondeterminism Monad with Access Reports
theory MMonad
imports NEMonad Generic_Memory
begin

  (* TODO: Move *)
  lemma fresh_freed_not_valid[simp]:
    "is_FRESH s (addr.block a)  ¬is_valid_addr s a"
    "is_FREED s (addr.block a)  ¬is_valid_addr s a"
    "is_FRESH s (addr.block a)  ¬is_valid_ptr_addr s a"
    "is_FREED s (addr.block a)  ¬is_valid_ptr_addr s a"
    by (auto simp: is_valid_addr_def is_valid_ptr_addr_def split: addr.split)
  


  text We define this Monad directly over our memory model, 
    but still generic in the stored values.
    
    The definition of the operations is done in two layers: first, we define the operations in the 
    ne-monad, prove that they preserve the consistency and non-emptiness invariant, and then
    lift them to the subtype for the actual M-monad.
  


  subsection Invariant and Subtype
  text 
    Our monad requires the following invariants, which will be enforced by a subtype
  
     the reported ACC_REPORT is consistent with the observable changes on the state. 
      This is a sanity check property, which also enables us to show commutativity of par.
     each program returns at least one possible result.
      This is a sanity check property, which ensures that we don't accidentally verify a 
      'magic' program.
     the memory manager can choose any available addresses.
      This is required to give it enough flexibility to always leave non-conflicting choices
      for parallel composition.
  
  
  
  definition "consistentM m  s. wlp (m s) (λ(_,i,s'). acc_consistent s i s')"
  definition "consistentM_pw s m  wlp m (λ(_,i,s'). acc_consistent s i s')"
  
  definition "non_emptyM_pw s m  ¬is_fail m  
    (B. finite B  (x i s'. is_res m (x,i,s')  acc.a i  B = {} ))"
  definition "non_emptyM m  s. ¬is_fail (m s)  
    (B. finite B  (x i s'. is_res (m s) (x,i,s')  acc.a i  B = {} ))"
  
  lemma non_emptyM_pw: "non_emptyM m = (s. non_emptyM_pw s (m s))"
    unfolding non_emptyM_def non_emptyM_pw_def by simp
  
  lemma consistentM_pw: "consistentM m  (s. consistentM_pw s (m s))"
    unfolding consistentM_def consistentM_pw_def by auto
      
  definition "invarM m  consistentM m  non_emptyM m"  

  definition "invarM_pw s m  consistentM_pw s m  non_emptyM_pw s m"
  
  lemma invarM_pw: "invarM m = (s. invarM_pw s (m s))"
    unfolding invarM_def invarM_pw_def
    by (auto simp add: consistentM_pw non_emptyM_pw)
 
  (* For presentation in paper *)   
  lemma "invarM c = (μ P. c μ = SPEC P 
    (x ρ μ'. P (x,ρ,μ')  acc_consistent μ ρ μ')
   (B. finite B  (x ρ μ'. P (x,ρ,μ')  acc.a ρ  B = {} ))
  )"
    unfolding invarM_def consistentM_def non_emptyM_def wlp_def
    unfolding is_fail_def is_res_def
    apply (safe;clarsimp)
    apply (metis neM.sel neM.simps(3))
    by (metis neM.collapse)
    
  lemma 
    assumes "ρ=ACC_REPORT r w a f"  
    shows "acc_consistent μ ρ μ'  (
      (addrr  w. addr.block addr  a  is_valid_addr μ addr) 
      (addrr  w. addr.block addr  f  is_valid_addr μ' addr) 
      (b. valid_block_trans μ μ' b) 
      a = alloc_blocks μ μ' 
      f = freed_blocks μ μ'  
      (addr. is_valid_addr μ addr  is_valid_addr μ' addr  addr  w  get_addr μ addr = get_addr μ' addr))"  
    unfolding acc_consistent_def valid_block_trans_def alloc_blocks_def freed_blocks_def assms
    apply (clarsimp simp: is_ALLOC_conv)
    apply (safe)
    apply blast
    apply blast
    apply blast
    apply blast
    apply blast
    apply blast
    apply blast
    apply blast
    apply (smt (verit, best) UnI1 addr.case_eq_if block.disc(1) block.distinct(1) is_valid_addr_alt mem_Collect_eq)
    subgoal by (simp add: addr.case_eq_if is_valid_addr_alt)
    subgoal by (metis (no_types, lifting) UnI2 addr.case_eq_if block.disc(1) block.distinct(1) is_valid_addr_alt mem_Collect_eq)
    subgoal by (simp add: addr.case_eq_if is_valid_addr_alt)
    apply blast
    apply blast
    apply blast
    apply blast
    apply blast
    apply blast
    done
    
  lemma 
    assumes "ρ=ACC_REPORT r w a f"  
    shows "acc_consistent μ ρ μ'  (
      (addrr  w. addr.block addr  a  is_valid_addr μ addr) 
      (addrr  w. addr.block addr  f  is_valid_addr μ' addr) 
      (b. valid_block_trans μ μ' b) 
      a = alloc_blocks μ μ' 
      f = freed_blocks μ μ'  
      (addr. is_valid_addr μ addr  is_valid_addr μ' addr  addr  w  get_addr μ addr = get_addr μ' addr))"  
    unfolding acc_consistent_def valid_block_trans_def alloc_blocks_def freed_blocks_def assms
    apply (clarsimp simp: is_ALLOC_conv)
    apply (safe)
    apply blast
    apply blast
    apply blast
    apply blast
    apply blast
    apply blast
    apply blast
    apply blast
    apply (smt (verit, best) UnI1 addr.case_eq_if block.disc(1) block.distinct(1) is_valid_addr_alt mem_Collect_eq)
    subgoal by (simp add: addr.case_eq_if is_valid_addr_alt)
    subgoal by (metis (no_types, lifting) UnI2 addr.case_eq_if block.disc(1) block.distinct(1) is_valid_addr_alt mem_Collect_eq)
    subgoal by (simp add: addr.case_eq_if is_valid_addr_alt)
    apply blast
    apply blast
    apply blast
    apply blast
    apply blast
    apply blast
    done
    
    
  
  
      
  lemma consistentMI[intro?]:
    assumes "s. wlp (m s) (λ(_,i,s'). acc_consistent s i s')"
    shows "consistentM m"
    using assms unfolding consistentM_def ..
    
  lemma consistentMD:
    assumes "consistentM m"
    shows "wlp (m s) (λ(_,i,s'). acc_consistent s i s')"
    using assms unfolding consistentM_def ..

  lemma consistent_wlp: "consistentM m  (x i s'. acc_consistent s i s'  Q (x,i,s'))  (wlp (m s) Q)"  
    unfolding consistentM_def by pw

  lemma invarM_pw_FAIL[simp]: "invarM_pw s FAIL" 
    unfolding invarM_pw_def consistentM_pw_def non_emptyM_pw_def
    by pw
  
  subsubsection Subtype Definition
    
  typedef ('r,'v) M = "{m::'v memory  ('r×acc×'v memory) neM. invarM m}" 
    morphisms run Abs_M
    unfolding invarM_def consistentM_def non_emptyM_def
    by pw
    
  setup_lifting type_definition_M

  lemma invarM_run: "invarM (run m)"
    using run by force
    
  
  subsection Basic Monad Combinators
  context
    includes monad_syntax_ne
  begin

    qualified named_theorems invarM_lemmas Monad invariant preservation lemmas
      
    declare invarM_def[invarM_lemmas]      
  
  
    definition "preturn x s = (return (x,0::acc,s))"
    
    definition "pspec P s = (if Pbot then SPEC (λ(r,i,s'). P r  i=0  s'=s) else FAIL)"
    
    definition "pbind m f s  do {
      (x,i1,s)  m s;
      (r,i2,s)  f x s;
      return (r,i1+i2 ::acc,s)
    }"  

    lemma [invarM_lemmas]: "consistentM (preturn x)"
      unfolding consistentM_def preturn_def
      apply rule
      apply wp
      apply auto
      unfolding acc_consistent_def
      by (auto simp: )

    lemma [invarM_lemmas]: "consistentM (pspec P)"
      unfolding consistentM_def pspec_def
      apply rule
      apply wp
      apply auto
      unfolding acc_consistent_def
      apply (auto simp:  wlp_FAIL) (* TODO: wlp_FAIL should be applied by wp, but isn't! *)
      done
            
    lemma [invarM_lemmas]: "consistentM m  (x. consistentM (f x))  consistentM (pbind m f)"  
      supply [wp_recursion_rule] = consistent_wlp
      unfolding pbind_def
      apply rule
      apply wp
      apply (clarsimp simp: acc_consistent_trans)
      done
      
    
    lemma [invarM_lemmas]: "non_emptyM (preturn x)"  
      unfolding non_emptyM_def preturn_def
      by pw
      
    lemma [invarM_lemmas]: "non_emptyM (pspec P)"  
      unfolding non_emptyM_def pspec_def
      by pw
              
    lemma [invarM_lemmas]: "non_emptyM m  (x. non_emptyM (f x))  non_emptyM (pbind m f)"  
      unfolding non_emptyM_def pbind_def
      apply pw
      by (metis inf_sup_distrib2 acc_plus_simps(3) sup.idem)
      
    
      

    lift_definition Mreturn :: "'r  ('r,'v) M" is preturn by (simp add: invarM_lemmas)
    lift_definition Mspec :: "('rbool)  ('r,'v) M" is pspec by (simp add: invarM_lemmas)
    lift_definition Mbind :: "('x,'v) M  ('x  ('r,'v) M)  ('r,'v) M"
      is pbind by (auto simp add: invarM_lemmas intro!: invarM_pw[THEN iffD1])
    
        
  subsection Parallel Combinator
    
    
    definition "ppar m1 m2 s  do {
      ((r1,i1,s1),(r2,i2,s2))  m1 s  m2 s;
      assert acc_consistent s i1 s1  acc_consistent s i2 s2; ― ‹Ensure reported ACC_REPORT is 
        consistent with observable modifications on state. This will later be enforced by subtyping.
      assume spar_feasible i1 i2; ― ‹Filter out impossible combinations (where malloc did not sync)
      assert acc_norace i1 i2; ― ‹Fail on data races
      let s = combine_states s1 i2 s2; ― ‹Combine states
      return ((r1,r2),i1+i2,s) 
    }"
  
    lemma [invarM_lemmas]: "consistentM m1  consistentM m2  consistentM (ppar m1 m2)"    
      supply [wp_recursion_rule] = consistent_wlp
      supply [wp_rule] = wlp_PAR[OF consistentMD consistentMD]
      unfolding ppar_def
      apply rule
      apply wp
      apply clarsimp
      apply wp
      apply simp_all
      by (simp add: feasible_parallel_execution.consistent' feasible_parallel_execution.intro)
      
      
    text To show that our parallel combinator does not rule out all executions,
      we need to exploit that, for any finite set of blocks, we always find an execution 
      that does not allocate this set of blocks.
      
    lemma finite_alloc_blocks[simp, intro]: "finite (alloc_blocks s s')"  
      unfolding alloc_blocks_def
      by (simp add: finite_non_fresh)
      
    lemma [invarM_lemmas]: "non_emptyM m1; consistentM m1; non_emptyM m2; consistentM m2   non_emptyM (ppar m1 m2)"
      unfolding non_emptyM_def ppar_def
      apply pw
    proof goal_cases
      case (1 s A)
      
      obtain x1 i1 s1 where R1: "is_res (m1 s) (x1, i1, s1)" and I1: "acc.a i1  A = {}" using 1 by meson
      
      hence "acc_consistent s i1 s1" using consistentM m1 m1 s  FAIL
        unfolding consistentM_def wlp_def by pw 

      interpret c1: acc_consistent_loc s i1 s1 apply unfold_locales by fact 
                
      have "finite (alloc_blocks s s1  A)" using 1 by auto
      hence "finite (acc.a i1  A)"
        using c1.acc_a_alloc by presburger
      then obtain x2 i2 s2 where R2: "is_res (m2 s) (x2, i2, s2)" and I2: "acc.a i2  (acc.a i1  A) = {}"  
        using 1 by metis
      hence NF2: "m2 s  FAIL" using 1 by metis
      with R2 have "acc_consistent s i2 s2" using consistentM m2
        unfolding consistentM_def wlp_def by pw 
  
      interpret c2: acc_consistent_loc s i2 s2 apply unfold_locales by fact 
        
        
      from I2 have "spar_feasible i1 i2"
        unfolding spar_feasible_def by (auto simp: c1.acc_a_alloc c2.acc_a_alloc)
      
      with I1 I2 R1 R2 NF2 have NI: "acc_norace i1 i2" using 1
        by metis
        
      interpret valid_parallel_execution s s1 i1 s2 i2 apply unfold_locales by fact+
        
        
      show ?case
        apply (rule exI[where x=x1])
        apply (rule exI[where x=x2])
        apply (rule exI[where x="i1+i2"])
        
        apply (rule conjI)
        subgoal
          apply (intro exI conjI impI)
          apply fact
          apply fact
          apply (rule NI)
          apply fact
          apply fact
          apply (rule NI)
          apply fact
          apply fact
          apply simp
          apply simp
          apply simp
          done
        subgoal using I1 I2 by auto  
        done
        
    qed
  
    
    
    lift_definition Mpar :: "('x,'v) M  (('y,'v) M)  ('x×'y,'v) M"
      is ppar by (simp add: invarM_lemmas)
    
    
    subsection Memory Operations
  
    definition "malloc vs s = do {
      b  spec b. is_FRESH s b;
      return (b, acc_a b, addr_alloc vs b s)
    }"
    
    definition "mfree b s = do {
      assert is_ALLOC s b;
      return ((), acc_f b, addr_free b s)
    }"  

    definition "mvalid_addr a s = do {
      assert is_valid_addr s a;
      return ((), acc_r a, s)
    }"
        
    definition "mload a s = do {
      assert is_valid_addr s a;
      return (get_addr s a, acc_r a, s)
    }"
    
    definition "mstore a v s = do {
      assert is_valid_addr s a;
      return ((), acc_w a, put_addr s a v)
    }"
    
      
    lemma [invarM_lemmas]: "consistentM (malloc v)"
      unfolding consistentM_def malloc_def
      apply rule
      apply wp
      apply (auto simp: acc_consistent_def alloc_blocks_def freed_blocks_def)
      done
      
    lemma [invarM_lemmas]: "consistentM (mfree a)"
      unfolding consistentM_def mfree_def
      apply rule
      apply wp
      apply auto
      unfolding acc_consistent_def alloc_blocks_def freed_blocks_def
      by (auto)

    lemma [invarM_lemmas]: "consistentM (mvalid_addr a)"
      unfolding consistentM_def mvalid_addr_def
      apply rule
      apply wp
      apply auto
      unfolding acc_consistent_def
      by (auto)
      
    lemma [invarM_lemmas]: "consistentM (mload a)"
      unfolding consistentM_def mload_def
      apply rule
      apply wp
      apply auto
      unfolding acc_consistent_def
      by (auto simp: )
      
    lemma [invarM_lemmas]: "consistentM (mstore a v)"
      unfolding consistentM_def mstore_def
      apply rule
      apply wp
      apply auto
      unfolding acc_consistent_def alloc_blocks_def freed_blocks_def
      by (auto split: block.split)
      
    lemma [invarM_lemmas]: "non_emptyM (malloc v)"  
      unfolding non_emptyM_def malloc_def alloc_blocks_def
      apply pw
      using ex_fresh by fastforce
  
    lemma [invarM_lemmas]: "non_emptyM (mfree a)"  
      unfolding non_emptyM_def mfree_def alloc_blocks_def
      by pw

    lemma [invarM_lemmas]: "non_emptyM (mvalid_addr a)"  
      unfolding non_emptyM_def mvalid_addr_def alloc_blocks_def
      by pw
                  
    lemma [invarM_lemmas]: "non_emptyM (mload a)"  
      unfolding non_emptyM_def mload_def
      by pw
      
    lemma [invarM_lemmas]: "non_emptyM (mstore a v)"  
      unfolding non_emptyM_def mstore_def alloc_blocks_def
      by pw
    
    lift_definition Mmalloc :: "('v list)  (block_idx,'v) M" is malloc by (simp add: invarM_lemmas)
    lift_definition Mfree :: "block_idx  (unit,'v) M" is mfree by (simp add: invarM_lemmas)
    lift_definition Mvalid_addr :: "addr  (unit,'v) M" is mvalid_addr by (simp add: invarM_lemmas)
    (*lift_definition Mvalid_ptr_addr :: "addr ⇒ (unit,'v) M" is mvalid_ptr_addr by (simp add: invarM_lemmas)*)
    lift_definition Mload :: "addr  ('v,'v) M" is mload by (simp add: invarM_lemmas)
    lift_definition Mstore :: "addr  'v  (unit,'v) M" is mstore by (simp add: invarM_lemmas)
    
    
  end    


subsection Pointwise Reasoning Setup    

  lemma M_eq_iff[pw_init]: "m=m'  (s. run m s = run m' s)"
    apply transfer
    by auto
    
  lemma pw_Mreturn[pw_simp]:
    "run (Mreturn x) s  FAIL"  
    "is_res (run (Mreturn x) s) r  r=(x,0,s)"  
    by (transfer'; unfold preturn_def; pw)+

  lemma pw_Mspec[pw_simp]:
    "run (Mspec P) s = FAIL  P=bot"  
    "is_res (run (Mspec P) s) r  (x. r=(x,0,s)  P x)"  
    by (transfer'; unfold pspec_def; pw)+

  lemma pw_Mbind1[pw_simp]:
    "run (Mbind m f) s = FAIL  is_fail (run m s)  (x i s'. is_res (run m s) (x,i,s')  is_fail (run (f x) s'))"
    apply transfer
    unfolding pbind_def
    by pw
    
  lemma pw_Mbind2[pw_simp]:
    "is_res (run (Mbind m f) s) ris  (case ris of (r,i'',s'') 
        (x i s'. is_res (run m s) (x,i,s')  ¬is_fail (run (f x) s'))
         (x i i' s'. is_res (run m s) (x,i,s')  is_res (run (f x) s') (r,i',s'')  i''=i+i')
      )"
    apply transfer
    unfolding pbind_def
    apply pw 
    by blast
  
  lemma invarM_pw_iff: "invarM m  (s. 
      (r i s'. is_res (m s) (r,i,s')  acc_consistent s i s')
     non_emptyM_pw s (m s)
  )"  
    unfolding invarM_def consistentM_def non_emptyM_pw
    apply pw  
    by (metis is_res_def)
  

  lemma pw_Mpar1[pw_simp]:
    "run (Mpar m1 m2) s = FAIL  (is_fail (run m1 s)  is_fail (run m2 s) 
       (r1 i1 s1 r2 i2 s2. is_res (run m1 s) (r1,i1,s1)  is_res (run m2 s) (r2,i2,s2) 
           spar_feasible i1 i2  ¬acc_norace i1 i2 ))"
    apply transfer
    unfolding ppar_def invarM_pw_iff
    apply pw
    by blast+

  lemma pw_Mpar2[pw_simp]:
    "is_res (run (Mpar m1 m2) s) ris  (case ris of (r,i,s')  
        (r1 i1 s1 r2 i2 s2. is_res (run m1 s) (r1,i1,s1)  is_res (run m2 s) (r2,i2,s2)  spar_feasible i1 i2 
           acc_norace i1 i2)
       (r1 i1 s1 r2 i2 s2. is_res (run m1 s) (r1,i1,s1)  is_res (run m2 s) (r2,i2,s2) 
           spar_feasible i1 i2  r=(r1,r2)  i=i1+i2  s' = combine_states s1 i2 s2  ))"
    apply transfer
    unfolding ppar_def invarM_pw_iff
    apply pw
    apply blast+
    done

  lemma no_result_is_FAIL[pw_simp]: "(a b c. ¬is_res (run m s) (a,b,c))  run m s = FAIL"
    by (metis finite.emptyI invarM_pw_iff invarM_run is_fail_def is_res_def non_emptyM_pw_def)
        
  context    
    includes monad_syntax_ne
  begin
    lemma run_Mmalloc[pw_simp]: "run (Mmalloc vs) s = malloc vs s"  
      apply transfer ..

    lemma run_Mfree[pw_simp]: "run (Mfree a) s = mfree a s"  
      apply transfer ..

    lemma run_Mvalid_addr[pw_simp]: "run (Mvalid_addr a) s = mvalid_addr a s"  
      apply transfer ..

    (*lemma run_Mvalid_ptr_addr[pw_simp]: "run (Mvalid_ptr_addr a) s = mvalid_ptr_addr a s"  
      apply transfer ..*)
      
    lemma run_Mload[pw_simp]: "run (Mload a) s = mload a s"  
      apply transfer ..

    lemma run_Mstore[pw_simp]: "run (Mstore a v) s = mstore a v s"  
      apply transfer ..
              
  end
    
      
subsection Recursion Setup    
      
  lift_definition Mbot :: "('r,'v) M" is "λ_. FAIL"
    by (auto simp: invarM_pw)

  context
  begin
    interpretation FR: flat_rec FAIL .
    
    
    lift_definition Mle :: "('r,'v) M  ('r,'v) M  bool" 
      is "fun_ord FR.le" .
      
      
    definition "fun_chain  Complete_Partial_Order.chain (fun_ord FR.le)"  
    definition "fun_chain'  Complete_Partial_Order.chain Mle"  
      
    lemma [transfer_rule]: "(rel_fun (rel_set cr_M) (=)) fun_chain fun_chain'"
      unfolding fun_chain_def fun_chain'_def Complete_Partial_Order.chain_def
      (* TODP: clean up this proof *)
      apply (auto simp: rel_fun_def fun_ord_def rel_set_def)
      apply (metis (full_types) Mle.rep_eq cr_M_def fun_ord_def)
      by (metis (no_types, lifting) Mle.rep_eq cr_M_def fun_ord_def)
      
    
    
    lift_definition Mlub :: "('r,'v) M set  ('r,'v) M"
      is "λC. if fun_chain C then fun_lub FR.lub C else (λ_. FAIL)"
      unfolding invarM_pw
      apply rule
      subgoal for C s
        apply (auto simp: FR.fun_lub_apply fun_chain_def)
        apply (drule FR.chain_apply[where x=s])
        apply (erule FR.chain_cases)
        apply auto
        by force
      done
      
    lemma Mlub_empty_is_fail[pw_simp]: "run (Mlub {}) s = FAIL"  
      apply transfer
      by (auto simp: fun_lub_def)
      
    lemma M_ccpo: "class.ccpo Mlub Mle (mk_lt Mle)"
      apply intro_locales
      apply (rule preorder_mk_ltI)
      apply unfold_locales
      
      apply transfer apply (auto simp: fun_ord_def FR.le_def) []
      apply transfer apply (fastforce simp: fun_ord_def FR.le_def) []
      apply transfer apply (auto simp: fun_ord_def FR.le_def fun_eq_iff; metis) [] 
      
      apply (fold fun_chain'_def)
      
      apply transfer
      apply (clarsimp simp: fun_ord_def FR.fun_lub_apply fun_chain_def)
      subgoal for C f s
        apply (drule FR.chain_apply[where x=s])
        apply (erule FR.chain_cases)
        apply (auto simp: FR.le_def)
        done
        
      apply transfer
      apply (clarsimp simp: fun_ord_def FR.fun_lub_apply fun_chain_def)
      subgoal for C f s
        apply (drule FR.chain_apply[where x=s])
        apply (erule FR.chain_cases)
        apply (auto simp: FR.le_def)
        apply force
        apply force
        done
      done
  

    interpretation RS: ccpo Mlub Mle "mk_lt Mle"
      by (rule M_ccpo) 
    interpretation RS: rec_setup Mlub Mle "mk_lt Mle"
      by unfold_locales
      
    (* Adding one level of definitions. TODO: Maybe use global_interpretation?! *)  
      
    definition "REC  RS.REC"
    
    abbreviation "M_mono'  gen_is_mono' Mle Mle"
    abbreviation "M_mono_body  RS.is_mono_body"
    
    (*
    definition "M_mono ≡ RS.fmono"

    definition M_mono' where "M_mono' F ≡ ∀D D'. fun_ord Mle D D' ⟶ Mle (F D) (F D')"
    
    lemma M_monoI[mono]: 
      assumes "⋀x. M_mono' (λD. F D x)"
      shows "M_mono F"
      using assms unfolding M_mono'_def M_mono_def Complete_Partial_Order.monotone_def fun_ord_def
      by blast
    *)

    lemma REC_unfold: 
      assumes MONO: "RS.is_mono_body F"
      shows "REC F = F (REC F)"
      by (metis REC_def RS.REC_unfold assms)
      
    text Pointwise properties of recursive functions can be proved by well-founded induction 
      on the arguments.
    lemma REC_wf_induct: 
      assumes WF: "wf V"
      assumes MONO: "RS.is_mono_body F"
      assumes STEP: "x D. y. (y,x)V  P y (D y)   P x (F D x)"
      shows "P x (REC F x)"
      using assms unfolding REC_def 
      using RS.REC_wf_induct by metis

    text For pointwise properties, which hold at non-terminating arguments, we
      can use the following induction scheme, which does not require a well-founded ordering.
    lemma REC_pointwise_induct: 
      fixes P
      assumes BOT: "x s. P x s FAIL" 
      assumes STEP: "D x s. (y s. P y s (run (D y) s))  P x s (run (F D x) s)"
      shows "P x s (run (REC F x) s)"
    proof -
      have "s. P x s (run (REC F x) s)"
        unfolding REC_def
        supply R = RS.REC_pointwise_induct[where P="λx m. s. P x s (run m s)"]
        apply (rule R)
        subgoal for x
          apply (transfer fixing: P)
          apply (auto simp: fun_chain_def chain_empty fun_lub_def BOT)
          done
        subgoal for x
          unfolding ccpo.admissible_def fun_chain'_def[symmetric]
          apply (transfer fixing: P)
          apply (clarsimp simp: FR.fun_lub_apply)
          subgoal for x C s
            unfolding fun_chain_def
            apply (drule FR.chain_apply[where x=s])
            apply (erule FR.chain_cases)
            apply (auto simp: FR.le_def BOT) 
            by force
          done
        subgoal using STEP by blast 
        done
      thus ?thesis ..
    qed
    
subsubsection Monotonicity Prover Setup      

    qualified lemma Mle_alt: "Mle a b  (s. FR.le (run a s) (run b s))"  
      apply transfer
      by (auto simp: fun_ord_def)
      
    qualified lemma pw_FR_le: "FR.le a b  a=b  is_fail a"  
      unfolding FR.le_def is_fail_def by auto

    context
      notes [pw_init] = Mle_alt pw_FR_le
    begin  
    
      (*
      lemma mono_const[mono]: 
        "M_mono' (λ_. c)"  
        "M_mono' (λD. D y)"
        unfolding M_mono'_def fun_ord_def
        by auto 
        
      lemma mono_If[mono]: "
        M_mono' (λD. F D) ⟹ M_mono' (λD. G D) ⟹
        M_mono' (λD. if b then F D else G D)"  
        unfolding M_mono'_def
        by auto
      *)
        
      lemma mono_Mbind1: "
        M_mono' (λD. F D)  
        M_mono' (λD. Mbind (F D) (G))"  
        unfolding monotone_def fun_ord_def Mle_alt
        apply pw' 
        apply (safe; simp; blast)
        done

      lemma mono_Mbind2: "
        (y. M_mono' (λD. G y D))  
        M_mono' (λD. Mbind F (λy. G y D))"  
        unfolding monotone_def fun_ord_def Mle_alt
        apply pw
        apply blast
        apply metis
        apply blast
        apply blast
        done
                
      lemma mono_Mbind[partial_function_mono]: 
        assumes "M_mono' (λD. F D)" 
        assumes "y. M_mono' (λD. G y D)"
        shows "M_mono' (λD. Mbind (F D) (λy. G y D))"  
        using mono_Mbind1[OF assms(1)] mono_Mbind2[of G, OF assms(2)]
        unfolding monotone_def
        apply auto
        using RS.order.trans by blast

      lemma mono_Mpar1: "
        M_mono' (λD. F D)  
        M_mono' (λD. Mpar (F D) G)"  
        unfolding monotone_def fun_ord_def Mle_alt
        apply pw' 
        apply (safe; simp; blast)
        done
        
      lemma mono_Mpar2: "
        M_mono' (λD. G D)  
        M_mono' (λD. Mpar F (G D))"  
        unfolding monotone_def fun_ord_def Mle_alt
        apply pw' 
        apply (safe; simp; blast)
        done
        
      lemma mono_Mpar[partial_function_mono]: "
        M_mono' (λD. F D)  
        M_mono' (λD. G D)  
        M_mono' (λD. Mpar (F D) (G D))"  
        using mono_Mpar1 mono_Mpar2
        unfolding monotone_def
        apply auto
        using RS.order.trans by blast

      lemma mono_REC[partial_function_mono]: 
        assumes "D. RS.is_mono_body (F D)"
        assumes "DD x. M_mono' (λD. F D DD x)"
        shows "M_mono' (λD. REC (F D) x)"  
        using assms
        unfolding monotone_def REC_def
        apply clarsimp
        subgoal for D D'
          apply (rule RS.REC_mono[of F D D', unfolded fun_ord_def, rule_format])
          subgoal by (simp add: fun_ord_def monotone_def)
          subgoal by blast
          done
        done
        
    end          

    
subsection Partial Function Setup        
    
    lemmas M_partial_function = RS.partial_function_definitions
    
  end          

  
  interpretation RSPF: partial_function_definitions Mle Mlub
    by (rule M_partial_function)
  
  declaration Partial_Function.init "M" @{term RSPF.fixp_fun}
    @{term RSPF.mono_body} @{thm RSPF.fixp_rule_uc} @{thm RSPF.fixp_induct_uc}
    (NONE)
  
    
  subsection Symmetry of parallel    
      
  definition "mswap m  done { ((r1,r2),i,s)m; returnne ((r2,r1),i,s) }"  
  
  lemma pw_mswap[pw_simp]:
    "mswap m = FAIL  is_fail m"
    "is_res (mswap m) ab  (case ab of ((r1,r2),i,s)  is_res m ((r2,r1),i,s))"
    unfolding mswap_def 
    apply pw
    by (cases ab; pw)
    
    
  lemmas combine_states_sym = valid_parallel_execution.combine_states_sym[OF valid_parallel_execution.intro]  
    
  lemma ppar_sym: "invarM m1  invarM m2  ppar m1 m2 s = mswap (ppar m2 m1 s)"  
    unfolding ppar_def
    apply (cases "m1 s"; cases "m2 s"; simp)
    defer
    apply pw
    apply pw
    apply pw
    subgoal for P1 P2
      apply (subgoal_tac "invarM_pw s (SPEC P1)")
      apply (subgoal_tac "invarM_pw s (SPEC P2)")
      
      apply (thin_tac "invarM _")+
      apply (thin_tac "_=_")+
      subgoal
        apply pw
        using spar_feasible_sym acc_norace_sym
        apply -
        apply blast
        apply blast
        apply blast
        apply blast
        apply blast
        apply blast
        apply blast
        apply (smt (verit, best) add.commute combine_states_sym acc_consistent_loc.intro)
        apply blast
        by (smt (verit, best) add.commute combine_states_sym acc_consistent_loc.intro)
      apply (metis invarM_pw)
      apply (metis invarM_pw)
      done
    done
    
  lemma res_run_consistentI: "is_res (run m s) (x,i,s')  acc_consistent s i s'"  
    using invarM_pw_iff invarM_run by fastforce
        
    
  lemma Mpar_sym: "Mpar m1 m2 = Mbind (Mpar m2 m1) (λ(r1,r2). Mreturn (r2,r1))"  
    apply pw
    using spar_feasible_sym acc_norace_sym apply blast
    using spar_feasible_sym acc_norace_sym apply blast
    using spar_feasible_sym acc_norace_sym apply blast
    apply (metis (no_types, opaque_lifting) add.commute combine_states_sym spar_feasible_sym res_run_consistentI)
    using spar_feasible_sym acc_norace_sym apply blast
    apply (metis (no_types, opaque_lifting) add.commute combine_states_sym spar_feasible_sym res_run_consistentI)
    done
   
  lifting_update M.lifting  
  lifting_forget M.lifting  
     
  
  
subsection Syntax  
  
  (*abbreviation (input) bind_doI where "bind_doI m (λx. f x) ≡ BIND m (λx. f x)"*)
  abbreviation then_doM where "then_doM m f  Mbind m (λ_. f)"

  nonterminal doM_binds and doM_bind
  syntax
    "_doM_block" :: "doM_binds  'a" ("doM {//(2  _)//}" [12] 62)
    "_doM_bind"  :: "[pttrn, 'a]  doM_bind" ("(2_ / _)" 13)
    "_doM_let" :: "[pttrn, 'a]  doM_bind" ("(2let _ =/ _)" [1000, 13] 13)
    "_doM_then" :: "'a  doM_bind" ("_" [14] 13)
    "_doM_final" :: "'a  doM_binds" ("_")
    "_doM_cons" :: "[doM_bind, doM_binds]  doM_binds" ("_;//_" [13, 12] 12)
    (*"_thenM" :: "['a, 'b] ⇒ 'c" (infixr "⪢" 54)*)

  syntax (ASCII)
    "_doM_block" :: "doM_binds  'a" ("doM {//(2  _)//}" [12] 62)
    "_doM_bind" :: "[pttrn, 'a]  doM_bind" ("(2_ <-/ _)" 13)
    (*"_thenM" :: "['a, 'b] ⇒ 'c" (infixr ">>" 54)*)

  translations
    "_doM_block (_doM_cons (_doM_then t) (_doM_final e))"
       "CONST then_doM t e"

    "_doM_block (_doM_cons (_doM_bind p t) (_doM_final e))"
       "CONST Mbind t (λp. e)"

    "_doM_block (_doM_cons (_doM_let p t) bs)"
       "let p = t in _doM_block bs"

    "_doM_block (_doM_cons b (_doM_cons c cs))"
       "_doM_block (_doM_cons b (_doM_final (_doM_block (_doM_cons c cs))))"

    "_doM_cons (_doM_let p t) (_doM_final s)"
       "_doM_final (let p = t in s)"

    "_doM_block (_doM_final e)"  "e"
  
    "(CONST then_doM m n)"  "(CONST Mbind m (λ_. n))"
    
   
  notation Mreturn ("returnM _" 20)
  notation Mspec (binder "specM " 10)
  notation Mpar (infixr "M" 50)


subsection Monad Laws    
  
lemma M_monad_laws[simp]:
  "doM {xreturnM a; f x} = f a"
  "doM {xm; returnM x} = m"
  "doM {ydoM {xm; f x}; g y} = doM { xm; yf x; g y }"
  apply pw
  apply pw
  
  apply pw
  apply blast 
  apply blast 
  using group_cancel.add1 apply blast 
  by (metis (no_types, opaque_lifting) add.assoc)
  
  subsubsection Additional simp lemmas
  
  lemma Mreturn_inj[simp]: "(returnM a) = (returnM b)  a=b"
    by pw
  
  
  
subsection Derived Constructs  

  subsubsection Fail
  text We define fail via least upper bound of the empty set, and show that it behaves as expected
  definition Mfail ("failM") where "Mfail  Mlub {}"
  
  lemma run_Mfail[pw_simp]: "run Mfail s = FAIL"
    unfolding Mfail_def
    by pw

  lemma M_bind_fail[simp]:  
    "doM {m; failM} = failM"
    "doM {failM; m} = failM"
    by pw+

  lemma M_par_fail[simp]:  
    "(failM M m2) = failM"
    "(m1 M failM) = failM"
    by pw+
          
  subsubsection Assert

  definition Massert ("assertm _" 20) where "Massert P  if P then Mreturn () else Mfail"

  lemma run_assert[pw_simp]: "run (Massert P) s = done {assertne P; returnne ((),0,s)}"
    unfolding Massert_def by pw

  lemma assert_True[simp]: "Massert True = Mreturn ()" by pw
    
  subsubsection While
    
  definition "Mwhile b c  REC (λwhile s. doM {
    bb  b s;
    if bb then doM {
      s  c s;
      while s
    } else returnM s
  })"
    
  lemma Mwhile_unfold: "Mwhile b c s = doM {
    bb  b s;
    if bb then doM {
      s  c s;
      Mwhile b c s
    } else returnM s
  }" 
    unfolding Mwhile_def
    apply (subst REC_unfold)
    apply pf_mono_prover
    ..
    
  lemma Mwhile_mono[partial_function_mono]:      
    assumes "x. M_mono' (λf. b f x)"
    assumes "x. M_mono' (λf. c f x)"
    shows "M_mono' (λD. Mwhile (b D) (c D) σ)"
    unfolding Mwhile_def
    using assms by pf_mono_prover
    

subsection Syntax Bundle    
  bundle monad_syntax_M
  begin
    syntax
      "_doM_block" :: "doM_binds  'a" ("do {//(2  _)//}" [12] 62)

    notation Mfail ("fail")      
    notation Mreturn ("return _" 20)
    notation Mspec (binder "spec " 10)
    notation Massert ("assert _" 20)
    notation Mpar (infixr "" 50)
      
  end
  
    
    
    
      
  
end        
            
        
(* TODO:
    can we integrate independence of values not read into consistency?
    → will change admissibility proof, but should be OK!
    → will need a simulation relation spanning results, too. As results
      can contain pointers to changed memory layout.
      
*)