Quelle  MonadSE.thy

(*****************************************************************************
 * Clean
 *                                                                            
 * HOL-TestGen --- theorem-prover based test case generation
 *                 http://www.brucker.ch/projects/hol-testgen/
 *                                                                            
 * Copyright (c) 2005-2007 ETH Zurich, Switzerland
 *               2009-2017 Univ. Paris-Sud, France 
 *               2009-2012 Achim D. Brucker, Germany
 *               2015-2017 University Sheffield, UK
 *               2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 ******************************************************************************)

(*
 * Monads --- a base testing theory for sequential computations.
 * This file is part of HOL-TestGen.
 *)

theory MonadSE
  imports Main
begin
        
section‹Definition : Standard State Exception Monads›
text‹State exception monads in our sense are a direct, pure formulation
  automata with a partial transition function.›

subsection‹Definition : Core Types and Operators›

type_synonym ('o, 'σ) MON_SE = "'σ ⇀ ('o × 'σ)" (* = '\<sigma> \<Rightarrow> ('o \<times> '\<sigma>)option *)       
      
definition bind_SE :: "('o,'σ)MON_SE ==> ('o ==> ('o','σ)MON_SE) ==> ('o','σ)MON_SE" 
where     "bind_SE f g = (λσ. case f σ of None ==> None
                                        | Some (out, σ') ==> g out σ')"

notation bind_SE (‹bind_SE›)

syntax    (xsymbols)
          "_bind_SE" :: "[pttrn,('o,'σ)MON_SE,('o','σ)MON_SE] ==> ('o','σ)MON_SE" 
          (‹(2 _ ← _; _)› [5,8,8]8)
translations 
          "x ← f; g" == "CONST bind_SE f (% x . g)"

definition unit_SE :: "'o ==> ('o, 'σ)MON_SE"   (‹(result _)› 8) 
where     "unit_SE e = (λσ. Some(e,σ))"
notation   unit_SE (‹unit_SE›)

text‹In the following, we prove the required Monad-laws›

lemma bind_right_unit[simp]: "(x ← m; result x) = m"
  apply (simp add:  unit_SE_def bind_SE_def)
  apply (rule ext)
  apply (case_tac "m σ", simp_all)
  done

lemma bind_left_unit [simp]: "(x ← result c; P x) = P c"
  by (simp add: unit_SE_def bind_SE_def)
  
lemma bind_assoc[simp]: "(y ← (x ← m; k x); h y) = (x ← m; (y ← k x; h y))"
  apply (simp add: unit_SE_def bind_SE_def, rule ext)
  apply (case_tac "m σ", simp_all)
  apply (case_tac "a", simp_all)
  done
    
subsection‹Definition : More Operators and their Properties›

definition fail_SE :: "('o, 'σ)MON_SE"
where     "fail_SE = (λσ. None)" 
notation   fail_SE (‹fail_SE›)

definition assert_SE :: "('σ ==> bool) ==> (bool, 'σ)MON_SE"
where     "assert_SE P = (λσ. if P σ then Some(True,σ) else None)"
notation   assert_SE (‹assert_SE›)

definition assume_SE :: "('σ ==> bool) ==> (unit, 'σ)MON_SE"
where     "assume_SE P = (λσ. if ∃σ . P σ then Some((), SOME σ . P σ) else None)"
notation   assume_SE (‹assume_SE›)


lemma bind_left_fail_SE[simp] : "(x ← fail_SE; P x) = fail_SE"
  by (simp add: fail_SE_def bind_SE_def)


text‹We also provide a "Pipe-free" - variant of the bind operator.
  a "standard" programming sequential operator without output frills.›
(* TODO: Eliminate/Modify this. Is a consequence of the Monad-Instantiation. *)


definition bind_SE' :: "('α, 'σ)MON_SE ==> ('β, 'σ)MON_SE ==> ('β, 'σ)MON_SE" (infixr ‹;-› 10)
where     "(f ;- g) = (_ ← f ; g)"

lemma bind_assoc'[simp]: "((m ;- k);- h ) = (m;- (k;- h))"
by(simp add:bind_SE'_def)


lemma bind_left_unit' [simp]: "((result c);- P) = P"
  by (simp add:  bind_SE'_def)
  

lemma bind_left_fail_SE'[simp]: "(fail_SE;- P) = fail_SE"
  by (simp add: bind_SE'_def)

lemma bind_right_unit'[simp]: "(m;- (result ())) = m"
  by (simp add:  bind_SE'_def)
          
text‹The bind-operator in the state-exception monad yields already
 a semantics for the concept of an input sequence on the meta-level:›
lemma     syntax_test: "(o1 ← f1 ; o2 ← f2; result (post o1 o2)) = X"
oops
  
definition yield_C :: "('a ==> 'b) ==> ('b,'a ) MON_SE"
    where "yield_C f ≡ (λσ. Some(f σ, σ))"


definition try_SE :: "('o,'σ) MON_SE ==> ('o option,'σ) MON_SE" (‹try_SE›)
where     "try_SE ioprog = (λσ. case ioprog σ of
                                      None ==> Some(None, σ)
                                    | Some(outs, σ') ==> Some(Some outs, σ'))" 
text‹In contrast, mbind as a failure safe operator can roughly be seen
 as a foldr on bind - try:
 m1 ; try m2 ; try m3; ... Note, that the rough equivalence only holds for
 certain predicates in the sequence - length equivalence modulo None,
 for example. However, if a conditional is added, the equivalence
 can be made precise:›
  
text‹On this basis, a symbolic evaluation scheme can be established
 that reduces mbind-code to try\_SE\_code and ite-cascades.›

definition alt_SE :: "[('o, 'σ)MON_SE, ('o, 'σ)MON_SE] ==> ('o, 'σ)MON_SE"   (infixl ‹⊓_SE› 10)
where     "(f ⊓_SE g) = (λ σ. case f σ of None ==> g σ
                                      | Some H ==> Some H)"

definition malt_SE :: "('o, 'σ)MON_SE list ==> ('o, 'σ)MON_SE"
where     "malt_SE S = foldr alt_SE S fail_SE"
notation   malt_SE (‹⊓_SE›)

lemma malt_SE_mt [simp]: "⊓_SE [] = fail_SE"
by(simp add: malt_SE_def)

lemma malt_SE_cons [simp]: "⊓_SE (a # S) = (a ⊓_SE (⊓_SE S))"
by(simp add: malt_SE_def)


subsection‹Definition : Programming Operators and their Properties›

definition  "skip_SE = unit_SE ()"

definition if_SE :: "['σ ==> bool, ('α, 'σ)MON_SE, ('α, 'σ)MON_SE] ==> ('α, 'σ)MON_SE"
where     "if_SE c E F = (λσ. if c σ then E σ else F σ)" 

syntax    (xsymbols)
          "_if_SE" :: "['σ ==> bool,('o,'σ)MON_SE,('o','σ)MON_SE] ==> ('o','σ)MON_SE" 
          (‹(if_SE _ then _ else _fi)› [5,8,8]8)
translations 
          "(if_SE cond then T1 else T2 fi)" == "CONST if_SE cond T1 T2"


subsection‹Theory of a Monadic While›

text‹Prerequisites›
fun replicator :: "[('a, 'σ)MON_SE, nat] ==> (unit, 'σ)MON_SE" (infixr ‹^^^› 60)
where     "f ^^^ 0 = (result ())"
        | "f ^^^ (Suc n) = (f ;- f ^^^ n)"


fun replicator2 :: "[('a, 'σ)MON_SE, nat, ('b, 'σ)MON_SE] ==> ('b, 'σ)MON_SE" (infixr ‹^:^› 60)
where     "(f ^:^ 0) M = (M )"
        | "(f ^:^ (Suc n)) M = (f ;- ((f ^:^ n) M))"


text‹First Step : Establishing an embedding between partial functions and relations›
(* plongement *)
definition Mon2Rel :: "(unit, 'σ)MON_SE ==> ('σ × 'σ) set"
where "Mon2Rel f = {(x, y). (f x = Some((), y))}"
(* ressortir *)
definition Rel2Mon :: " ('σ × 'σ) set ==> (unit, 'σ)MON_SE "
where "Rel2Mon S = (λ σ. if ∃σ'. (σ, σ') ∈ S then Some((), SOME σ'. (σ, σ') ∈ S) else None)"

lemma Mon2Rel_Rel2Mon_id: assumes det:"single_valued R" shows "(Mon2Rel ∘ Rel2Mon) R = R"
apply (simp add: comp_def Mon2Rel_def Rel2Mon_def,auto)
apply (case_tac "∃σ'. (a, σ') ∈ R", auto)
apply (subst (2) some_eq_ex) 
using det[simplified single_valued_def] by auto


lemma Rel2Mon_Id: "(Rel2Mon ∘ Mon2Rel) x = x"
apply (rule ext)
apply (auto simp: comp_def Mon2Rel_def Rel2Mon_def)
apply (erule contrapos_pp, drule HOL.not_sym, simp)
done

lemma single_valued_Mon2Rel: "single_valued (Mon2Rel B)"
by (auto simp: single_valued_def Mon2Rel_def)

text‹Second Step : Proving an induction principle allowing to establish that lfp remains
 deterministic›


(* A little complete partial order theory due to Tobias Nipkow *)
definition chain :: "(nat ==> 'a set) ==> bool" 
where     "chain S = (∀i. S i ⊆ S(Suc i))"

lemma chain_total: "chain S ==> S i ≤ S j ∨ S j ≤ S i"
by (metis chain_def le_cases lift_Suc_mono_le)

definition cont :: "('a set => 'b set) => bool" 
where     "cont f = (∀S. chain S ⟶ f(UN n. S n) = (UN n. f(S n)))"

lemma mono_if_cont: fixes f :: "'a set ==> 'b set"
  assumes "cont f" shows "mono f"
proof
  fix a b :: "'a set" assume "a ⊆ b"
  let ?S = "λn::nat. if n=0 then a else b"
  have "chain ?S" using ‹a ⊆ b› by(auto simp: chain_def)
  hence "f(UN n. ?S n) = (UN n. f(?S n))"
    using assms by (metis cont_def)
  moreover have "(UN n. ?S n) = b" using ‹a ⊆ b› by (auto split: if_splits)
  moreover have "(UN n. f(?S n)) = f a ∪ f b" by (auto split: if_splits)
  ultimately show "f a ⊆ f b" by (metis Un_upper1)
qed

lemma chain_iterates: fixes f :: "'a set ==> 'a set"
  assumes "mono f" shows "chain(λn. (f^^n) {})"
proof-
  { fix n have "(f ^^ n) {} ⊆ (f ^^ Suc n) {}" using assms
    by(induction n) (auto simp: mono_def) }
  thus ?thesis by(auto simp: chain_def)
qed

theorem lfp_if_cont:
  assumes "cont f" shows "lfp f = (∪n. (f ^^ n) {})" (is "_ = ?U")
proof
  show "lfp f ⊆ ?U"
  proof (rule lfp_lowerbound)
    have "f ?U = (UN n. (f^^Suc n){})"
      using chain_iterates[OF mono_if_cont[OF assms]] assms
      by(simp add: cont_def)
    also have "… = (f^^0){} ∪ …" by simp
    also have "… = ?U"
      apply(auto simp del: funpow.simps)
      by (metis empty_iff funpow_0 old.nat.exhaust)
    finally show "f ?U ⊆ ?U" by simp
  qed
next
  { fix n p assume "f p ⊆ p"
    have "(f^^n){} ⊆ p"
    proof(induction n)
      case 0 show ?case by simp
    next
      case Suc
      from monoD[OF mono_if_cont[OF assms] Suc] ‹f p ⊆ p›
      show ?case by simp
    qed
  }
  thus "?U ⊆ lfp f" by(auto simp: lfp_def)
qed


lemma single_valued_UN_chain:
  assumes "chain S" "(!!n. single_valued (S n))"
  shows "single_valued(UN n. S n)"
proof(auto simp: single_valued_def)
  fix m n x y z assume "(x, y) ∈ S m" "(x, z) ∈ S n"
  with chain_total[OF assms(1), of m n] assms(2)
  show "y = z" by (auto simp: single_valued_def)
qed

lemma single_valued_lfp: 
fixes f :: "('a × 'a) set ==> ('a × 'a) set"
assumes "cont f" "∧r. single_valued r ==> single_valued (f r)"
shows "single_valued(lfp f)"
unfolding lfp_if_cont[OF assms(1)]
proof(rule single_valued_UN_chain[OF chain_iterates[OF mono_if_cont[OF assms(1)]]])
  fix n show "single_valued ((f ^^ n) {})"
  by(induction n)(auto simp: assms(2))
qed


text‹Third Step: Definition of the Monadic While ‹ ››
definition Γ :: "['σ ==> bool,('σ × 'σ) set] ==> (('σ × 'σ) set ==> ('σ × 'σ) set)" 
where     "Γ b cd = (λcw. {(s,t). if b s then (s, t) ∈ cd O cw else s = t})"


definition while_SE :: "['σ ==> bool, (unit, 'σ)MON_SE] ==> (unit, 'σ)MON_SE"
where     "while_SE c B ≡ (Rel2Mon(lfp(Γ c (Mon2Rel B))))"

syntax    (xsymbols)
          "_while_SE" :: "['σ ==> bool, (unit, 'σ)MON_SE] ==> (unit, 'σ)MON_SE" 
          (‹(while_SE _ do _ od)› [8,8]8)
translations 
          "while_SE c do b od" == "CONST while_SE c b"

lemma cont_Γ: "cont (Γ c b)"
by (auto simp: cont_def Γ_def)

text‹The fixpoint theory now allows us to establish that the lfp constructed over
 @{term Mon2Rel} remains deterministic›

theorem single_valued_lfp_Mon2Rel: "single_valued (lfp(Γ c (Mon2Rel B)))"
apply(rule single_valued_lfp, simp_all add: cont_Γ)
apply(auto simp: Γ_def single_valued_def)
apply(metis single_valued_Mon2Rel[of "B"] single_valued_def)
done


lemma Rel2Mon_if:
  "Rel2Mon {(s, t). if b s then (s, t) ∈ Mon2Rel c O lfp (Γ b (Mon2Rel c)) else s = t} σ =
  (if b σ then Rel2Mon (Mon2Rel c O lfp (Γ b (Mon2Rel c))) σ else Some ((), σ))"
by (simp add: Rel2Mon_def)

lemma Rel2Mon_homomorphism:
  assumes determ_X: "single_valued X" and determ_Y: "single_valued Y"
  shows   "Rel2Mon (X O Y) = ((Rel2Mon X) ;- (Rel2Mon Y))"
proof - 
    have relational_partial_next_in_O: "∧x E F. (∃y. (x, y) ∈ (E O F)) ==> (∃y. (x, y) ∈ E)" 
                        by (auto)
    have some_eq_intro: "∧ X x y . single_valued X ==> (x, y) ∈ X ==> (SOME y. (x, y) ∈ X) = y"
                        by (auto simp: single_valued_def)

    show ?thesis
apply (simp add: Rel2Mon_def bind_SE'_def bind_SE_def)
apply (rule ext, rename_tac "σ")
apply (case_tac " ∃ σ'. (σ, σ') ∈ X O Y")
apply (simp only: HOL.if_True)
apply (frule relational_partial_next_in_O)
apply (auto simp: single_valued_relcomp some_eq_intro determ_X determ_Y relcomp.relcompI)
by blast
qed



text‹Putting everything together, the theory of embedding and the invariance of
 determinism of the while-body, gives us the usual unfold-theorem:›
theorem while_SE_unfold:
"(while_SE b do c od) = (if_SE b then (c ;- (while_SE b do c od)) else result () fi)"
apply (simp add: if_SE_def bind_SE'_def while_SE_def unit_SE_def)
apply (subst lfp_unfold [OF mono_if_cont, OF cont_Γ])
apply (rule ext)
apply (subst Γ_def)
apply (auto simp: Rel2Mon_if Rel2Mon_homomorphism bind_SE'_def Rel2Mon_Id [simplified comp_def] 
                  single_valued_Mon2Rel single_valued_lfp_Mon2Rel )
done
  

lemma bind_cong : " f σ = g σ ==> (x ← f ; M x)σ = (x ← g ; M x)σ"
  unfolding bind_SE'_def bind_SE_def  by simp

lemma bind'_cong : " f σ = g σ ==> (f ;- M )σ = (g ;- M )σ"
  unfolding bind_SE'_def bind_SE_def  by simp

  
  
lemma if_{SE_True} [simp]: "(if_SE (λ x. True) then c else d fi) = c" 
  apply(rule ext) by (simp add: MonadSE.if_SE_def) 

lemma if_{SE_False} [simp]: "(if_SE (λ x. False) then c else d fi) = d" 
  apply(rule ext) by (simp add: MonadSE.if_SE_def) 
  
    
lemma if_{SE_cond_cong} : "f σ = g σ ==>
                           (if_SE f then c else d fi) σ =
                           (if_SE g then c else d fi) σ"
  unfolding if_SE_def  by simp
 
lemma while_{SE_skip}[simp] : "(while_SE (λ x. False) do c od) = skip_SE" 
  apply(rule ext,subst MonadSE.while_SE_unfold)
  by (simp add: MonadSE.if_SE_def skip_{SE_def})
  
    
end