Theory DeclSemAsNDInterpFSet

section "Declarative semantics as a non-deterministic interpreter"
  
theory DeclSemAsNDInterpFSet
  imports Lambda ValuesFSet
begin
  
subsection "Non-determinism monad"

type_synonym 'a M = "'a set"

definition set_bind :: "'a M  ('a  'b M)  'b M" where
  "set_bind m f  { v.  v'. v'  m  v  f v' }"
declare set_bind_def[simp]

syntax "_set_bind" :: "[pttrns,'a M,'b]  'c" ("(_  _;//_)" 0)
translations "P  E; F"  "CONST set_bind E (λP. F)"

definition return :: "'a  'a M" where
  "return v  {v}"
declare return_def[simp]

definition zero :: "'a M" where
  "zero  {}"
declare zero_def[simp]

no_notation "binomial" (infixl "choose" 65)

definition choose :: "'a set  'a M" where
  "choose S  S"
declare choose_def[simp]
 
definition down :: "val  val M" where
  "down v  (v'  UNIV; if v'  v then return v' else zero)"
declare down_def[simp]

definition mapM :: "'a fset  ('a  'b M)  ('b fset) M" where
  "mapM as f  ffold (λa. λr. (b  f a; bs  r; return (finsert b bs))) (return ({||})) as"
  
subsection "Non-deterministic interpreter"

abbreviation apply_fun :: "val M  val M  val M" where
  "apply_fun V1 V2  (v1  V1; v2  V2;
                       case v1 of VFun f  
                          (v2',v3')  choose (fset f);
                          if v2'  v2 then return v3' else zero
                       | _  zero)"

fun E :: "exp  env  val set" where
  Enat2: "E (ENat n) ρ = return (VNat n)" |
  Evar2: "E (EVar x) ρ = (case lookup ρ x of None  zero | Some v  down v)" |
  Elam2: "E (ELam x e) ρ = (vs  choose UNIV; 
                           t  mapM vs (λ v. (v'  E e ((x,v)#ρ); return (v, v')));
                           return (VFun t))" |
  Eapp2: "E (EApp e1 e2) ρ = apply_fun (E e1 ρ) (E e2 ρ)" |
  Eprim2: "E (EPrim f e1 e2) ρ = (v1  E e1 ρ; v2  E e2 ρ;
                                 case (v1,v2) of
                                   (VNat n1, VNat n2)  return (VNat (f n1 n2))
                                | (VNat n1, VFun t2)  zero
                                | (VFun t1, v2)  zero)" |
  Eif2[eta_contract = false]: "E (EIf e1 e2 e3) ρ = (v1  E e1 ρ;
                              case v1 of
                                (VNat n)  if n  0 then E e2 ρ else E e3 ρ
                              | (VFun t)  zero)"

end