Theory NEMonad

section ‹Nondeterminism Error Monad›

text ‹
  The NE monad used as basis for the state-error monad in our LLVM semantics.
  Note: for abstract programs, we use an (equivalent) monad (nres), defined in
  the original Monadic Refinement Framework. 
  That's for legacy reasons, and needs to be unified at some point!
›

theory NEMonad
imports "../Basic_Imports" Flat_CCPO
begin

  subsection ‹Additions to Partial Function›
  context partial_function_definitions
  begin
    lemma monotoneI:
      "(⋀x. mono_body (λf. F f x)) ⟹ monotone le_fun le_fun F"
      by (auto simp: monotone_def fun_ord_def)

    lemma fp_unfold:
      assumes "f ≡ fixp_fun F"
      assumes "(⋀x. mono_body (λf. F f x))"
      shows "f x = F f x"
      using assms mono_body_fixp[of F] by auto

  end

  lemma fun_ordD: "fun_ord le f g ⟹ le (f x) (g x)"
    by (auto simp: fun_ord_def)

  lemma fun_ord_mono_alt: "monotone le (fun_ord le') f ⟷ (∀x. monotone le le' (λy. f y x))"
    by (metis (mono_tags, lifting) fun_ord_def monotone_def)



  method_setup pf_mono_prover = ‹Scan.succeed (SIMPLE_METHOD' o Subgoal.FOCUS_PREMS (fn {context=ctxt,...} => CHANGED (ALLGOALS (Partial_Function.mono_tac ctxt))))›

  ML ‹
    fun discharge_monos ctxt thm = let
      fun aux ctxt thm = let
        val prems = Thm.prems_of thm

        fun prove_simple tac t ctxt = Goal.prove ctxt [] [] t (fn {context=ctxt, ...} => ALLGOALS (tac ctxt))


        (*val mono_tac = Subgoal.FOCUS (fn {context=ctxt,...} => CHANGED (ALLGOALS (Partial_Function.mono_tac ctxt)))*)
        fun mono_tac ctxt = CHANGED o (Partial_Function.mono_tac ctxt)

        fun cinst (t as @{mpat "⋀_. monotone (fun_ord _) _ _"}) = the_default asm_rl (try (prove_simple mono_tac t) ctxt)
          | cinst _ = asm_rl

        val insts = map cinst prems

        val thm = thm OF insts
      in
        thm
      end
    in
      (* Avoid surprises with schematic variables being instantiated *)
      singleton (Variable.trade (map o aux) ctxt) thm
    end

  ›

  attribute_setup discharge_monos
    = ‹Scan.succeed (Thm.rule_attribute [] (discharge_monos o Context.proof_of))›
    ‹Try to discharge monotonicity premises›



  subsection ‹Type Definition›
  text ‹
    The result of a nondeterministic computation
  ›
  datatype 'a neM = 
    SPEC (the_spec: "'a ⇒ bool") ― ‹May return any value that satisfies a predicate›
  | FAIL ("fail⇩n⇩e")  ― ‹May fail›

  fun map_neM where
    "map_neM f (SPEC P) = SPEC (λy. ∃x. P x ∧ y=f x)"
  | "map_neM _ FAIL = FAIL"  
  
  
  
  subsection ‹Pointwise Reasoning›
  text ‹Many theorems about the result monad can easily be 
    solved by transforming them to pointwise proposition over
    possible results.›
  
  definition "is_fail m ⟷ m=FAIL"
  definition "is_res m x ⟷ (m≠FAIL ∧ the_spec m x)"
    
  lemma pw_basic:
    "is_res (SPEC P) x ⟷ P x"
    "¬is_res FAIL x"
    "is_fail m ⟷ m=FAIL"
    unfolding is_res_def is_fail_def by auto
  
  lemma pw_eq_iff: "m=m' ⟷ ((is_fail m ⟷ is_fail m') ∧ (∀x. is_res m x ⟷ is_res m' x))"
    by (cases m; cases m'; auto simp add: pw_basic)
        

  subsubsection ‹Automation›
  text ‹We first rewrite with initialization rules, that convert
    a property to a pointwise property, and then with 
    simplification rules, which syntactically decompose pointwise 
    properties.
  ›

  named_theorems pw_init ‹Pointwise reasoning: initialization›
  named_theorems pw_simp ‹Pointwise reasoning: simplification›

  lemmas [pw_simp] = pw_basic
  lemmas [pw_init] = pw_eq_iff
  
  method pw = ((simp only: pw_init)?; auto simp: pw_simp)
  method pw' = ((simp only: pw_init)?; simp add: pw_simp)
      
  
  lemma pw_map_neM[pw_simp]:
    "map_neM f m = FAIL ⟷ is_fail m"
    "is_res (map_neM f m) y ⟷ (∃x. is_res m x ∧ y=f x)"
    apply (cases m; auto simp: is_fail_def is_res_def)
    apply (cases m; auto simp: is_fail_def is_res_def)
    done
  
  lemma pw_Let[pw_simp]:
    "Let x f = FAIL ⟷ is_fail (f x)"  
    "is_res (Let x f) r ⟷ is_res (f x) r"  
    by pw+
    
    
  subsection ‹Basic Combinators›

  subsubsection ‹Return and Bind›
  text ‹Deterministically return a result›
  definition "RETURN x ≡ SPEC (λr. r=x)"
  
  text ‹Sequential composition: apply ‹f› to every possible result of ‹m›.›
  definition "BIND m f ≡ case m of 
    SPEC P ⇒ (if ∃x. P x ∧ f x = FAIL then FAIL
              else SPEC (λr. ∃x Q. P x ∧ f x = SPEC Q ∧ Q r))
  | FAIL ⇒ FAIL"

  
  text ‹Parallel composition: pair of results. 
    Note, this is subtly different from sequential composition and returning the pair,
    in case that the first result is empty, and the second one fails!
  ›
  definition "PAR m⇩1 m⇩2 ≡ case (m⇩1,m⇩2) of
    (SPEC P⇩1, SPEC P⇩2) ⇒ SPEC (pred_prod P⇩1 P⇩2)
  | _ ⇒ FAIL  
  "
  
  
  lemma BIND_simps:
    "BIND FAIL f = FAIL"
    "BIND (SPEC P) f = (
      if ∃x. P x ∧ f x = FAIL then FAIL
      else SPEC (λr. ∃x Q. P x ∧ f x = SPEC Q ∧ Q r)
    )"  
    unfolding BIND_def by auto
  
  
  lemma pw_RETURN[pw_simp]:
    "RETURN x ≠ FAIL"
    "is_res (RETURN x) y ⟷ x=y"
    unfolding RETURN_def by pw+

  lemma pw_BIND[pw_simp]:
    "BIND m f = FAIL ⟷ is_fail m ∨ (∃y. is_res m y ∧ is_fail (f y))"
    "is_res (BIND m f) x ⟷ (∀y. is_res m y ⟶ ¬is_fail (f y)) ∧ (∃y. is_res m y ∧ is_res (f y) x)"
    unfolding BIND_def
    apply (auto simp: pw_simp is_fail_def split: neM.split)
    by (meson is_res_def neM.exhaust_sel)

    
  lemma pw_PAR[pw_simp]:
    "PAR m⇩1 m⇩2 = FAIL ⟷ is_fail m⇩1 ∨ is_fail m⇩2"
    "is_res (PAR m⇩1 m⇩2) rr ⟷ (case rr of (r⇩1,r⇩2) ⇒ is_res m⇩1 r⇩1 ∧ is_res m⇩2 r⇩2)"
    unfolding PAR_def is_fail_def is_res_def
    apply (cases m⇩1; cases m⇩2; auto)
    apply (cases m⇩1; cases m⇩2; auto)
    done
    
    

  text ‹\<^const>‹RETURN› and \<^const>‹BIND› satisfy the monad laws:›  
  lemma return_bind[simp]: "BIND (RETURN x) f = f x"
    by pw
  
  lemma bind_return[simp]: "BIND m RETURN = m"  
    by pw

  lemma bind_bind[simp]: "BIND (BIND m f) g = BIND m (λx. BIND (f x) g)"
    by pw

  text ‹There are also laws for the interaction of \<^const>‹BIND› and \<^const>‹FAIL››
  lemma fail_bind[simp]: "BIND FAIL f = FAIL" by pw
  
  text ‹Note that \<^term>‹SPEC (λ_. False)› is special, in that it specifies a program
    with no possible results. It's the dual to \<^const>‹FAIL›. We call it ‹EMPTY›: ›
  abbreviation "EMPTY ≡ SPEC (λ_. False)"  
    
  text ‹\<^const>‹EMPTY› can be an un-intuitive corner-case for some rules, 
    like the following, that only holds for \<^term>‹m≠EMPTY›:›  
  lemma bind_fail: "BIND m (λ_. FAIL) = FAIL ⟷ m≠EMPTY" by pw

  lemma bind_empty[simp]: "BIND EMPTY f = EMPTY" by pw

  text ‹Parallel can be expressed by sequential composition, except for the extreme case where
    the first component is empty, and the second one fails. 
    In this case, due to the sequential nature of BIND, the failing component will never be executed,
    and the result will be empty. For parallel composition, though, both components will be executed,
    and the failure will propagate.
  ›
  lemma PAR_as_BIND_iff: "PAR m⇩1 m⇩2 = BIND m⇩1 (λr⇩1. BIND m⇩2 (λr⇩2. RETURN (r⇩1,r⇩2))) ⟷ (m⇩1≠EMPTY ∨ m⇩2≠FAIL)"
    by pw
  
  lemma PAR_as_BIND: "m⇩1≠EMPTY ∨ m⇩2≠FAIL ⟹ PAR m⇩1 m⇩2 = BIND m⇩1 (λr⇩1. BIND m⇩2 (λr⇩2. RETURN (r⇩1,r⇩2)))"
    by pw

  text ‹The parallel composition operator is commutative›    
  lemma PAR_commute: "PAR m⇩1 m⇩2 = map_neM prod.swap (PAR m⇩2 m⇩1)"
    by pw

    
  subsubsection ‹Syntax›  

  text ‹We establish some syntax›
    
  (*abbreviation (input) bind_doI where "bind_doI m (λx. f x) ≡ BIND m (λx. f x)"*)
  abbreviation then_doI where "then_doI m f ≡ BIND m (λ_. f)"

  nonterminal doI_binds and doI_bind
  syntax
    "_doI_block" :: "doI_binds ⇒ 'a" ("do⇩n⇩e {//(2  _)//}" [12] 62)
    "_doI_bind"  :: "[pttrn, 'a] ⇒ doI_bind" ("(2_ ←/ _)" 13)
    "_doI_let" :: "[pttrn, 'a] ⇒ doI_bind" ("(2let _ =/ _)" [1000, 13] 13)
    "_doI_then" :: "'a ⇒ doI_bind" ("_" [14] 13)
    "_doI_final" :: "'a ⇒ doI_binds" ("_")
    "_doI_cons" :: "[doI_bind, doI_binds] ⇒ doI_binds" ("_;//_" [13, 12] 12)
    (*"_thenM" :: "['a, 'b] ⇒ 'c" (infixr "⪢" 54)*)

  syntax (ASCII)
    "_doI_bind" :: "[pttrn, 'a] ⇒ doI_bind" ("(2_ <-/ _)" 13)
    (*"_thenM" :: "['a, 'b] ⇒ 'c" (infixr ">>" 54)*)

  translations
    "_doI_block (_doI_cons (_doI_then t) (_doI_final e))"
      ⇌ "CONST then_doI t e"

    "_doI_block (_doI_cons (_doI_bind p t) (_doI_final e))"
      ⇌ "CONST BIND t (λp. e)"

    "_doI_block (_doI_cons (_doI_let p t) bs)"
      ⇌ "let p = t in _doI_block bs"

    "_doI_block (_doI_cons b (_doI_cons c cs))"
      ⇌ "_doI_block (_doI_cons b (_doI_final (_doI_block (_doI_cons c cs))))"

    "_doI_cons (_doI_let p t) (_doI_final s)"
      ⇌ "_doI_final (let p = t in s)"

    "_doI_block (_doI_final e)" ⇀ "e"
  
    "(CONST then_doI m n)" ⇀ "(CONST BIND m (λ_. n))"
    
   
  notation RETURN ("return⇩n⇩e _" 20)
  notation SPEC (binder "spec⇩n⇩e " 10)
  notation PAR (infixr "∥⇩n⇩e" 50)
  
      
  subsubsection ‹Assert›    
  text ‹An assertion returns unit if the predicate holds, and fails otherwise.
    Note that returning unit is the functional way of having a function with no return value (e.g. void in C/C++).
  ›
  definition "ASSERT P ≡ if P then return⇩n⇩e () else FAIL"
  
  lemma pw_ASSERT[pw_simp]: 
    "ASSERT P = FAIL ⟷ ¬P"  
    "is_res (ASSERT P) x ⟷ P"
    unfolding ASSERT_def
    apply pw+
    done
      
  notation ASSERT ("assert⇩n⇩e _" 20)

  definition "ASSUME P ≡ if P then return⇩n⇩e () else EMPTY"
  
  lemma pw_ASSUME[pw_simp]: 
    "ASSUME P ≠ FAIL"  
    "is_res (ASSUME P) x ⟷ P"
    unfolding ASSUME_def
    apply pw+
    done
      
  notation ASSUME ("assume⇩n⇩e _" 20)
  

  subsubsection ‹Recursion›  
  text ‹For recursion, we define a fixed-point combinator 
    utilizing a chain-complete partial order (CCPO).
    While CCPO's are advanced material, we try to capture the intuition
    below.
  ›
  

  
  context
  begin
    interpretation FR: flat_rec FAIL .
  
  (*    
    text ‹The recursion combinator models recursive functions. 
      The recursive call is the first parameter to the function body, and
      the argument is the second parameter.
    ›
    definition REC :: "(('a ⇒ 'b neM) ⇒ 'a ⇒ 'b neM) ⇒ 'a ⇒ 'b neM" where "REC ≡ FR.REC"
  *)
        
    text ‹The function body must be monotone. Intuitively, this means that 
      it terminates at less arguments if the recursive call terminates at less arguments.
    ›
    
    abbreviation "nres_mono' ≡ gen_is_mono' FR.le FR.le"
    
    
    (*
    definition nres_mono :: "(('a ⇒ 'b neM) ⇒ 'a ⇒ 'b neM) ⇒ bool" where "nres_mono = FR.mono"
    *)
(*    
    text ‹A recursive function can be unfolded, i.e., the body is inlined once.›
    lemma REC_unfold: "nres_mono F ⟹ REC F = F (REC F)"
      unfolding REC_def nres_mono_def using FR.REC_unfold .

    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: "nres_mono 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 nres_mono_def REC_def 
      using FR.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:  
      assumes BOT: "⋀x. P x FAIL"
      assumes STEP: "⋀D x. (⋀y. P y (D y)) ⟹ P x (F D x)"
      shows "P x (REC F x)"
      using assms REC_def
      using FR.REC_pointwise_induct by metis
  *)      
  
    subsubsection ‹Monotonicity›  
    text ‹Function bodies have to be monotone, i.e., when invoked with a recursive call 
      that terminates at less arguments, it must terminate at less arguments.
      
      This property can be established syntactically for the standard combinators
      programs are build from.
    ›
    
    (*
    named_theorems mono ‹Monotonicity theorems for nres› 
    
    ML ‹
      structure NE_Mono_Prover = struct
        fun mono_tac ctxt = let
          val rules = Named_Theorems.get ctxt @{named_theorems mono}
        in 
          REPEAT_ALL_NEW (match_tac ctxt rules ORELSE' assume_tac ctxt)
        end
      end
    ›
    
    method_setup ne_mono = ‹Scan.succeed (SIMPLE_METHOD' o NE_Mono_Prover.mono_tac)›
    *)
    
    definition "flat_le ≡ FR.le"
    
    lemma pw_flat_le[pw_init]: "flat_le m m' ⟷ is_fail m ∨ (¬is_fail m' ∧ (∀x. is_res m x ⟷ is_res m' x))"  
      apply (cases m; cases m'; auto simp: pw_simp)
      apply (auto simp: flat_le_def FR.le_def)
      done
    
    (*  
    lemma mono_alt: "nres_mono F = (∀x y. fun_ord flat_le x y ⟶ fun_ord flat_le (F x) (F y))"
      unfolding nres_mono_def monotone_def FR.le_def flat_le_def ..
    
    definition nres_mono' :: "(('a ⇒ 'b neM) ⇒ 'c neM) ⇒ bool"
      where "nres_mono' F ≡ ∀D D'. fun_ord flat_le D D' ⟶ flat_le (F D) (F D')"
    *)
      
    (*
    lemma nres_monoI[mono]: 
      assumes "⋀x. nres_mono' (λD. F D x)"
      shows "nres_mono F"
      using assms unfolding mono_alt nres_mono'_def fun_ord_def
      by simp
    
    lemma nres_monoD: "nres_mono F ⟹ nres_mono' (λD. F D x)"
      unfolding mono_alt nres_mono'_def fun_ord_def
      by simp
    *)
      
    (*
    lemma mono_If[mono]: "
      nres_mono' (λD. F D) ⟹ nres_mono' (λD. G D) ⟹
      nres_mono' (λD. if b then F D else G D)"  
      unfolding nres_mono'_def fun_ord_def
      apply pw
      done
    *)

    thm partial_function_mono
          
    lemma mono_BIND[partial_function_mono]: "
      nres_mono' (λD. F D) ⟹ 
      (⋀y. nres_mono' (λD. G y D)) ⟹ 
      nres_mono' (λD. BIND (F D) (λy. G y D))"  
      unfolding monotone_def fun_ord_def flat_le_def[symmetric]
      apply pw
      apply blast
      apply (smt (verit, ccfv_threshold))
      apply (smt (verit, ccfv_threshold))
      apply (smt (verit, ccfv_threshold))
      done
      
    lemma mono_PAR[partial_function_mono]: "
      nres_mono' (λD. F D) ⟹ 
      nres_mono' (λD. G D) ⟹ 
      nres_mono' (λD. PAR (F D) (G D))"
      unfolding monotone_def fun_ord_def flat_le_def[symmetric]
      by (pw; blast)
     
      
      
    (*
    lemma mono_REC[mono]: 
      assumes "⋀D. nres_mono (F D)"
      assumes "⋀DD x. nres_mono' (λD. F D DD x)"
      shows "nres_mono' (λD. REC (F D) x)"  
      using assms
      unfolding nres_mono'_def flat_le_def REC_def
      apply clarsimp
      subgoal for D D'
        apply (rule FR.REC_mono[of F D D', unfolded fun_ord_def, rule_format])
        subgoal by (simp add: fun_ord_def nres_mono_def monotone_def)
        subgoal by blast
        done
      done
    *)  

    (*      
    lemma mono_case_prod[mono]:
      assumes "⋀a b. nres_mono' (λD. F D a b)"
      shows "nres_mono' (λD. case p of (a,b) ⇒ F D a b)"
      using assms
      apply (cases p) by simp
    
    lemma mono_Let[mono]:
      assumes "⋀x. nres_mono' (λD. F D x)"
      shows "nres_mono' (λD. let x=v in F D x)"
      using assms
      by simp
    *)  
            
  end
    
  
  subsection ‹Weakest Precondition›
  
  text ‹Weakest precondition: ‹m› does not fail, and all possible results satisfy postcondition ‹Q››
  definition [pw_init]: "wp m Q ⟷ ¬is_fail m ∧ (∀x. is_res m x ⟶ Q x)"

  text ‹Weakest liberal precondition: if ‹m› does not fail, all possible results satisfy postcondition ‹Q››
  definition [pw_init]: "wlp m Q ⟷ (¬is_fail m ⟶ (∀x. is_res m x ⟶ Q x))"
  
  
  text ‹Consequence rule: weaken postcondition ›  
  lemma wp_cons: "wp m Q ⟹ (⋀x. Q x ⟹ Q' x) ⟹ wp m Q'"
    by pw

  lemma wlp_cons: "wlp m Q ⟹ (⋀x. Q x ⟹ Q' x) ⟹ wlp m Q'"
    by pw
    
  lemma wp_imp_wlp: "wp m Q ⟹ wlp m Q" by pw  
    
    
  subsection ‹Wp-Calculus›  
  text ‹Syntactic rules for weakest precondition›      
  named_theorems wp_rule ‹Syntactic rules for wp›
  
  lemma wp_RETURN_iff: "wp (RETURN x) Q ⟷ Q x"
    by pw
  
  lemma wp_BIND_iff: "wp (BIND m f) Q ⟷ wp m (λx. wp (f x) Q)"  
    by pw

  lemma wp_PAR_iff: "wp (PAR m⇩1 m⇩2) Q ⟷ (∃Q⇩1 Q⇩2. wp m⇩1 Q⇩1 ∧ wp m⇩2 Q⇩2 ∧ (∀r⇩1 r⇩2. Q⇩1 r⇩1 ∧ Q⇩2 r⇩2 ⟶ Q (r⇩1,r⇩2)))"  
    by pw
    
  lemma wlp_PAR_iff: "wlp (PAR m⇩1 m⇩2) Q ⟷ (∃Q⇩1 Q⇩2. wlp m⇩1 Q⇩1 ∧ wlp m⇩2 Q⇩2 ∧ (∀r⇩1 r⇩2. Q⇩1 r⇩1 ∧ Q⇩2 r⇩2 ⟶ Q (r⇩1,r⇩2)))"  
    by pw
    
  lemmas [wp_rule] = 
    wp_RETURN_iff[THEN iffD2]  
    wp_BIND_iff[THEN iffD2]  

  text ‹We do not include these in wp-rules by default,
    as they will create schematic postconditions›  
  lemma wp_PAR:  
    assumes "wp m⇩1 Q⇩1" 
    assumes "wp m⇩2 Q⇩2" 
    assumes "⋀r⇩1 r⇩2. Q⇩1 r⇩1 ⟹ Q⇩2 r⇩2 ⟹ Q (r⇩1,r⇩2)"
    shows "wp (PAR m⇩1 m⇩2) Q"
    using assms by pw
    
  lemma wlp_PAR:  
    assumes "wlp m⇩1 Q⇩1" 
    assumes "wlp m⇩2 Q⇩2" 
    assumes "⋀r⇩1 r⇩2. Q⇩1 r⇩1 ⟹ Q⇩2 r⇩2 ⟹ Q (r⇩1,r⇩2)"
    shows "wlp (PAR m⇩1 m⇩2) Q"
    using assms by pw
    
    
  lemma wp_ASSERT[wp_rule]: "P ⟹ Q () ⟹ wp (ASSERT P) Q"  
    by pw

  lemma wp_ASSUME[wp_rule]: "(P ⟹ Q ()) ⟹ wp (ASSUME P) Q"  
    by pw
    
            
  lemma wp_SPEC[wp_rule]: "(⋀x. P x ⟹ Q x) ⟹ wp (SPEC P) Q"  
    by pw
    
  lemma wp_Let[wp_rule]: "(⋀x. x=v ⟹ wp (f x) Q) ⟹ wp (let x=v in f x) Q"  
    by pw
    
    
  lemma wp_if[wp_rule]: "⟦ b ⟹ wp m Q; ¬b ⟹ wp m' Q ⟧ ⟹ wp (if b then m else m') Q" by simp 
    
    
  lemma wp_if_ext[wp_rule]: "⟦b ⟹ P; ¬b⟹Q⟧ ⟹ if b then P else Q"   by simp
    
  lemma wp_prod_case[wp_rule]: "⟦⋀a b. p=(a,b) ⟹ wp (f a b) Q⟧ ⟹ wp (case p of (a,b) ⇒ f a b) Q"
    by (cases p) auto
  
  (*
  lemma wp_REC: 
    fixes x :: 'a and V :: "'a rel"
    assumes WF: "wf V"
    assumes MONO: "nres_mono F"
    assumes INIT: "P x"
    assumes STEP: "⋀x D. (⋀y. (y, x) ∈ V ⟹ P y ⟹ wp (D y) (Q y)) ⟹ P x ⟹ wp (F D x) (Q x)"
    shows "wp (REC F x) (Q x)"  
  proof -
    have "P x ⟶ wp (REC F x) (Q x)"
      apply (rule REC_wf_induct[OF WF MONO])
      apply (blast intro: STEP)
      done
    with INIT show ?thesis by blast
  qed  
  *)  
    
  lemma wlp_FAIL[wp_rule]: "wlp FAIL Q" 
    by pw
  
  lemma wlp_RETURN_iff: "wlp (RETURN x) Q ⟷ Q x"
    by pw

    (*
  lemma wlp_BIND_iff: "wlp (BIND m f) Q ⟷ wlp m (λx. wlp (f x) Q)"  
    oops
    *)
      
  lemma wlp_BIND[wp_rule]: "wlp m (λx. wlp (f x) Q) ⟹ wlp (BIND m f) Q"  
    by pw
    
  lemmas [wp_rule] = 
    wlp_RETURN_iff[THEN iffD2]  

  lemma wlp_ASSERT[wp_rule]: "⟦P⟹ Q()⟧ ⟹ wlp (ASSERT P) Q"  
    by pw

  lemma wlp_ASSUME[wp_rule]: "(P ⟹ Q ()) ⟹ wlp (ASSUME P) Q"  
    by pw
    
            
  lemma wlp_SPEC[wp_rule]: "(⋀x. P x ⟹ Q x) ⟹ wlp (SPEC P) Q"  
    by pw
    
  lemma wlp_Let[wp_rule]: "(⋀x. x=v ⟹ wlp (f x) Q) ⟹ wlp (let x=v in f x) Q"  
    by pw
    
    
  lemma wlp_if[wp_rule]: "⟦ b ⟹ wlp m Q; ¬b ⟹ wlp m' Q ⟧ ⟹ wlp (if b then m else m') Q" by simp 
    
    
  lemma wlp_if_ext[wp_rule]: "⟦b ⟹ P; ¬b⟹Q⟧ ⟹ if b then P else Q"   by simp
    
  lemma wlp_prod_case[wp_rule]: "⟦⋀a b. p=(a,b) ⟹ wlp (f a b) Q⟧ ⟹ wlp (case p of (a,b) ⇒ f a b) Q"
    by (cases p) auto
  
  (*
  lemma wlp_REC: 
    fixes x :: 'a
    assumes INIT: "P x"
    assumes STEP: "⋀x D. (⋀y. P y ⟹ wlp (D y) (Q y)) ⟹ P x ⟹ wlp (F D x) (Q x)"
    shows "wlp (REC F x) (Q x)"  
  proof -
    thm REC_pointwise_induct
    note R = REC_pointwise_induct[where P="λx m. P x ⟶ wlp m (Q x)"]
    have "P x ⟶ wlp (REC F x) (Q x)"
      apply (rule R)
      apply pw
      using STEP by blast
    with INIT show ?thesis by blast
  qed  
  *)  
    
    
    
      
  (*    
  subsection ‹Invariant Annotation›
  text ‹We annotate variants and invariants to WHILE-loops and recursions,
    such that we can automatically generate verification conditions.
    ›
  
  definition WHILEI :: "'a rel ⇒ ('a ⇒ bool) ⇒ ('a ⇒ bool neM) ⇒ ('a ⇒ 'a neM) ⇒ 'a ⇒ 'a neM"
    where 
    "WHILEI V I b f s ≡ WHILE (λs. do⇩n⇩e { assert⇩n⇩e I s; b s }) (λs. do⇩n⇩e { assert⇩n⇩e I s; f s }) s"
  
  lemma wp_WHILEI[wp_rule]:
    assumes "wf V"
    assumes "I s"
    assumes STEP: "⋀s. ⟦ I s ⟧ ⟹ wp (b s) (λr. if r then wp (f s) (λs'. I s' ∧ (s',s)∈V) else Q s)"
    shows "wp (WHILEI V I b f s) Q"
    using assms(1,2)
    unfolding WHILEI_def
    apply (intro wp_rule wp_WHILE[where I=I] STEP[THEN wp_cons])
    apply assumption+
    apply simp_all
    done
  
  lemma mono_WHILEI[mono]: 
    assumes "⋀DD x. nres_mono' (λD. b D x)"
    assumes "⋀DD x y. nres_mono' (λD. f D x)"
    shows "nres_mono' (λD. WHILEI V I (b D) (f D) s)"
    unfolding WHILEI_def
    by (intro mono assms)
             
  definition RECI :: "'a rel ⇒ ('a ⇒ bool) ⇒ 
    (('a ⇒ 'b nres) ⇒ 'a ⇒ 'b nres) ⇒ 'a ⇒ 'b nres" where 
    "RECI V P F ≡ REC (λD x. do {assert P x; F D x})"  
    
  lemma wp_RECI[wp_rule]: 
    fixes x :: 'a and V :: "'a rel"
    assumes WF: "wf V"
    assumes MONO: "nres_mono F"
    assumes INIT: "P x"
    assumes STEP: "⋀x D. (⋀y. (y, x) ∈ V ⟹ P y ⟹ wp (D y) (Q y)) ⟹ P x ⟹ wp (F D x) (Q x)"
    shows "wp (RECI V P F x) (Q x)"  
    unfolding RECI_def
    apply (rule wp_REC[of V _ P])
    apply fact
    apply (intro mono MONO[THEN nres_monoD])
    apply fact
    apply (intro wp_rule STEP)
    .

    
  lemma mono_RECI[mono]: 
    assumes "⋀D. nres_mono (F D)"
    assumes "⋀DD x. nres_mono' (λD. F D DD x)"
    shows "nres_mono' (λD. RECI V P (F D) x)"  
    unfolding RECI_def
    by (intro mono assms(1)[THEN nres_monoD] assms(2))
  *)  
    
  subsection ‹Automation›  
  
  named_theorems wp_recursion_rule ‹Rule to trigger resolution with premises›
  
  method wp_basic_step = 
    rule wp_rule 
  | rule wp_recursion_rule,(assumption|rprems)
  | pf_mono_prover
  
  method wp_step = find_goal ‹wp_basic_step›
  method wp = wp_step+

  
  lemmas [wp_recursion_rule] = wp_cons
      

  subsection ‹Syntax Bundle›
  bundle monad_syntax_ne
  begin
    syntax
      "_doI_block" :: "doI_binds ⇒ 'a" ("do {//(2  _)//}" [12] 62)

    notation FAIL ("fail")  
    notation RETURN ("return _" 20)
    notation SPEC (binder "spec " 10)
    notation ASSERT ("assert _" 20)
    notation ASSUME ("assume _" 20)
    notation PAR (infixr "∥" 50)
      
  end
  
    
  subsection ‹Summary›
  text ‹
    We shallowly embed a basic non-deterministic PL.
    The basic combinators are
    
    ▪ \<^term>‹SPEC P›: Specify any result that satisfies predicate ‹P›. 
      Special cases:
      ▪ \<^term>‹EMPTY = SPEC (λ_. False)›: specifies a program with no results.
      ▪ \<^term>‹RETURN x = SPEC (λr. r=x)›: specifies a program with the only result ‹x›.
          Syntax for return, with low binding priority: \<^term>‹return⇩n⇩e x+1›.
    ▪ \<^term>‹FAIL›: Specifies a failing program. Failure may be due 
      to non-termination or failed assertions.
    ▪ \<^term>‹BIND m f›: Sequential composition. Syntax: \<^term>‹do⇩n⇩e { x←m; f x }›
    ▪ \<^term>‹PAR m⇩1 m⇩2›: Parallel composition. Syntax: \<^term>‹m⇩1 ∥⇩n⇩e m⇩2›
    
  
    Any combinator from HOL can be used. We provide support (automation, etc.)
    for the following:
    ▪ \<^term>‹if b then m⇩1 else m⇩2›
    ▪ \<^term>‹let x=v in f x›
    ▪ \<^term>‹case p of (a,b) ⇒ f a b›
    
    Moreover, we support the following derived combinators:
    ▪ \<^term>‹ASSERT P = (if P then return⇩n⇩e () else FAIL)›. 
      Syntax with lower binding priority: \<^term>‹assert⇩n⇩e P∧Q›
    
    For each combinator, we need to provide:
      ▪ wp-rule
      ▪ mono-rule (if higher-order)
      ▪ pw-rule (if non-recursive)
      ▪ refinement rule (see later theory on refinement)
    
  ›
  
    
end