Session Clean

Theory MonadSE

(*****************************************************************************
 * 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
of automata with a partial transition function.›

subsection‹Definition : Core Types and Operators›

type_synonym ('o, ) MONSE = "  ('o × )" (* = 'σ ⇒ ('o × 'σ)option *)       
      
definition bind_SE :: "('o,)MONSE  ('o  ('o',)MONSE)  ('o',)MONSE" 
where     "bind_SE f g = (λσ. case f σ of None  None 
                                        | Some (out, σ')  g out σ')"

notation bind_SE ("bindSE")

syntax    (xsymbols)
          "_bind_SE" :: "[pttrn,('o,)MONSE,('o',)MONSE]  ('o',)MONSE" 
          ("(2 _  _; _)" [5,8,8]8)
translations 
          "x  f; g" == "CONST bind_SE f (% x . g)"

definition unit_SE :: "'o  ('o, )MONSE"   ("(result _)" 8) 
where     "unit_SE e = (λσ. Some(e,σ))"
notation   unit_SE ("unitSE")

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, )MONSE"
where     "fail_SE = (λσ. None)" 
notation   fail_SE ("failSE")

definition assert_SE :: "(  bool)  (bool, )MONSE"
where     "assert_SE P = (λσ. if P σ then Some(True,σ) else None)"
notation   assert_SE ("assertSE")

definition assume_SE :: "(  bool)  (unit, )MONSE"
where     "assume_SE P = (λσ. if σ . P σ then Some((), SOME σ . P σ) else None)"
notation   assume_SE ("assumeSE")


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


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


definition bind_SE' :: "(, )MONSE  (, )MONSE  (, )MONSE" (infixr ";-" 60)
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]: "(failSE;- P) = failSE"
  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 yieldC :: "('a   'b)   ('b,'a ) MONSE"
    where "yieldC f  (λσ. Some(f σ, σ))"


definition try_SE :: "('o,) MONSE  ('o option,) MONSE" ("trySE")
where     "trySE 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, )MONSE, ('o, )MONSE]  ('o, )MONSE"   (infixl "SE" 10)
where     "(f SE g) = (λ σ. case f σ of None  g σ
                                      | Some H  Some H)"

definition malt_SE :: "('o, )MONSE list  ('o, )MONSE"
where     "malt_SE S = foldr alt_SE S failSE"
notation   malt_SE ("SE")

lemma malt_SE_mt [simp]: "SE [] = failSE"
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  "skipSE = unitSE ()"

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

syntax    (xsymbols)
          "_if_SE" :: "[  bool,('o,)MONSE,('o',)MONSE]  ('o',)MONSE" 
          ("(ifSE _ then _ else _fi)" [5,8,8]8)
translations 
          "(ifSE cond then T1 else T2 fi)" == "CONST if_SE cond T1 T2"


subsection‹Theory of a Monadic While›

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


fun replicator2 :: "[('a, )MONSE, nat, ('b, )MONSE]  ('b, )MONSE" (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, )MONSE  ( × ) set"
where "Mon2Rel f = {(x, y). (f x = Some((), y))}"
(* ressortir *)
definition Rel2Mon :: " ( × ) set  (unit, )MONSE "
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, )MONSE]  (unit, )MONSE"
where     "while_SE c B  (Rel2Mon(lfp(Γ c (Mon2Rel B))))"

syntax    (xsymbols)
          "_while_SE" :: "[  bool, (unit, )MONSE]  (unit, )MONSE" 
          ("(whileSE _ do _ od)" [8,8]8)
translations 
          "whileSE 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:
"(whileSE b do c od) = (ifSE b then (c ;- (whileSE 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 ifSE_True [simp]: "(ifSE (λ x. True) then c else d fi) = c" 
  apply(rule ext) by (simp add: MonadSE.if_SE_def) 

lemma ifSE_False [simp]: "(ifSE (λ x. False) then c else d fi) = d" 
  apply(rule ext) by (simp add: MonadSE.if_SE_def) 
  
    
lemma ifSE_cond_cong : "f σ = g σ  
                           (ifSE f then c else d fi) σ = 
                           (ifSE g then c else d fi) σ"
  unfolding if_SE_def  by simp
 
lemma whileSE_skip[simp] : "(whileSE (λ x. False) do c od) = skipSE" 
  apply(rule ext,subst MonadSE.while_SE_unfold)
  by (simp add: MonadSE.if_SE_def skipSE_def)
  
    
end
  

Theory Seq_MonadSE

(******************************************************************************
 * Clean
 *
 * Copyright (c) 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.
 ******************************************************************************)

theory Seq_MonadSE
  imports MonadSE
begin
  
subsection‹ Chaining Monadic Computations : Definitions of Multi-bind Operators ›

text‹  In order to express execution sequences inside \HOL --- rather
than arguing over a certain pattern of terms on the meta-level --- and
in order to make our theory amenable to formal reasoning over execution sequences, 
we represent them as lists of input and generalize the bind-operator
of the state-exception monad accordingly. The approach is straightforward,
but comes with a price: we have to encapsulate all input and output data
into one type, and restrict ourselves to  a uniform step function.
Assume that we have a typed interface to a module with
the operations $op_1$, $op_2$, \ldots, $op_n$ with the inputs 
$\iota_1$, $\iota_2$, \ldots, $\iota_n$ (outputs are treated analogously).
Then we can encode for this interface the general input - type:
\begin{displaymath}
\texttt{datatype}\ \texttt{in}\ =\ op_1\ ::\ \iota_1\ |\ ...\ |\ \iota_n
\end{displaymath}
Obviously, we loose some type-safety in this approach; we have to express
that in traces only \emph{corresponding} input and output belonging to the 
same operation will occur; this form of side-conditions have to be expressed
inside \HOL. From the user perspective, this will not make much difference,
since junk-data resulting from too weak typing can be ruled out by adopted
front-ends. 
›

text‹ Note that the subsequent notion of a test-sequence allows the io stepping 
function (and the special case of a program under test) to stop execution 
\emph{within} the sequence; such premature terminations are characterized by an 
output list which is shorter than the input list. 

Intuitively, mbind› corresponds to a sequence of operation calls, separated by
";", in Java. The operation calls may fail (raising an exception), which means that
the state is maintained and the exception can still be caught at the end of the 
execution sequence.

›

fun    mbind :: " list    (  ('o,) MONSE)  ('o list,) MONSE"  
where "mbind [] iostep σ = Some([], σ)"
    | "mbind (a#S) iostep σ = 
                (case iostep a σ of 
                     None    Some([], σ)
                  |  Some (out, σ')  (case mbind S iostep σ' of 
                                          None     Some([out],σ') 
                                        | Some(outs,σ'')  Some(out#outs,σ'')))"

notation mbind ("mbindFailSave") (* future name: mbindFailSave *)

text‹This definition is fail-safe; in case of an exception, the current state is maintained,
       the computation as a whole is marked as success.
       Compare to the fail-strict variant mbind'›:›

lemma mbind_unit [simp]: 
     "mbind [] f = (result [])"
      by(rule ext, simp add: unit_SE_def)

text‹The characteristic property of @{term mbind} --- which distinguishes it from 
       mbind› defined in the sequel --- is that it never fails; it ``swallows'' internal
       errors occuring during the computation.›    
lemma mbind_nofailure [simp]:
     "mbind S f σ  None"
      apply(rule_tac x=σ in spec)
      apply(induct S, auto simp:unit_SE_def)
      apply(case_tac "f a x", auto)
      apply(erule_tac x="b" in allE) 
      apply(erule exE, erule exE, simp)
      done

text‹In contrast, we define a fail-strict sequential execution operator.
He has more the characteristic to fail globally whenever one of its operation
steps fails.

Intuitively speaking, mbind'› corresponds to an execution of operations 
where a results in a System-Halt. Another interpretation of mbind'› is to
view it as a kind of @{term foldl} foldl over lists via @{term bindSE}.› 
 
fun    mbind' :: " list    (  ('o,) MONSE)  ('o list,) MONSE"
where "mbind' [] iostep σ = Some([], σ)" |
      "mbind' (a#S) iostep σ = 
                (case iostep a σ of 
                     None    None
                  |  Some (out, σ')  (case mbind' S iostep σ' of 
                                          None     None   ― ‹fail-strict› 
                                        | Some(outs,σ'')  Some(out#outs,σ'')))"
notation mbind' ("mbindFailStop") (* future name: mbindFailStop *)

lemma mbind'_unit [simp]: 
     "mbind' [] f = (result [])"
      by(rule ext, simp add: unit_SE_def)

lemma mbind'_bind [simp]: 
     "(x  mbind' (a#S) F; M x) = (a  (F a); (x  mbind' S F; M (a # x)))"
      by(rule ext, rename_tac "z",simp add: bind_SE_def split: option.split)

declare mbind'.simps[simp del] (* use only more abstract definitions *)

text‹The next mbind› sequential execution operator is called 
Fail-Purge. He has more the characteristic to never fail, just "stuttering" 
above operation steps that fail. Another alternative in modeling.› 

fun    mbind'' :: " list    (  ('o,) MONSE)  ('o list,) MONSE"
where "mbind'' [] iostep σ = Some([], σ)" |
      "mbind'' (a#S) iostep σ = 
                (case iostep a σ of 
                     None            mbind'' S iostep σ
                  |  Some (out, σ')  (case mbind'' S iostep σ' of 
                                          None     None   ― ‹does not occur› 
                                        | Some(outs,σ'')  Some(out#outs,σ'')))"

notation mbind'' ("mbindFailPurge") (* future name: mbindPurgeFail *)
declare  mbind''.simps[simp del] (* use only more abstract definitions *)


text‹mbind' as failure strict operator can be seen as a foldr on bind -
       if the types would match \ldots›

subsubsection‹Definition : Miscellaneous Operators and their Properties›

lemma mbind_try: 
  "(x  mbind (a#S) F; M x) = 
   (a'  trySE(F a); 
      if a' = None 
      then (M [])
      else (x  mbind S F; M (the a' # x)))"
apply(rule ext)
apply(simp add: bind_SE_def try_SE_def)
apply(case_tac "F a x", auto)
apply(simp add: bind_SE_def try_SE_def)
apply(case_tac "mbind S F b", auto)
done



  
end
  

Theory Symbex_MonadSE

(******************************************************************************
 * Clean
 *
 * Copyright (c) 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.
 ******************************************************************************)

theory Symbex_MonadSE
  imports Seq_MonadSE
begin
  


subsection‹Definition and Properties of Valid Execution Sequences›

text‹A key-notion in our framework is the \emph{valid} execution
sequence, \ie{} a sequence that:
\begin{enumerate}
\item terminates (not obvious since while),
\item results in a final @{term True},
\item does not fail globally (but recall the FailSave and FailPurge
      variants of @{term mbind}-operators, that handle local exceptions in
      one or another way).
\end{enumerate}
Seen from an automata perspective (where the monad - operations correspond to
the step function), valid execution sequences can be used to model ``feasible paths''
across an automaton.›

definition valid_SE :: "  (bool,) MONSE  bool" (infix "" 15)
where "(σ  m) = (m σ  None  fst(the (m σ)))"
text‹This notation consideres failures as valid -- a definition
inspired by I/O conformance.›

subsubsection‹Valid Execution Sequences and their Symbolic Execution›
lemma exec_unit_SE [simp]: "(σ  (result P)) = (P)"
by(auto simp: valid_SE_def unit_SE_def)

lemma exec_unit_SE' [simp]: "(σ0  (λσ. Some (f σ, σ))) = (f σ0)"
by(simp add: valid_SE_def )

lemma exec_fail_SE [simp]: "(σ  failSE) = False"
by(auto simp: valid_SE_def fail_SE_def)

lemma exec_fail_SE'[simp]: "¬(σ0  (λσ. None))"
by(simp add: valid_SE_def )

text‹The following the rules are in a sense the heart of the entire symbolic execution approach›
lemma  exec_bind_SE_failure:
"A σ = None  ¬(σ  ((s  A ; M s)))"
by(simp add: valid_SE_def unit_SE_def bind_SE_def)

lemma  exec_bind_SE_failure2:
"A σ = None  ¬(σ  ((A ;- M)))"
by(simp add: valid_SE_def unit_SE_def bind_SE_def bind_SE'_def)
  
  
lemma exec_bind_SE_success: 
"A σ = Some(b,σ')  (σ  ((s  A ; M s))) = (σ'  (M b))"
  by(simp add: valid_SE_def unit_SE_def bind_SE_def )
    
lemma exec_bind_SE_success2: 
"A σ = Some(b,σ')  (σ  ((A ;- M))) = (σ'  M)"
  by(simp add: valid_SE_def unit_SE_def bind_SE_def bind_SE'_def )
    

lemma exec_bind_SE_success': (* atomic boolean Monad "Query Functions" *) 
"M σ = Some(f σ,σ)   (σ  M) = f σ"
by(simp add: valid_SE_def unit_SE_def bind_SE_def )




lemma exec_bind_SE_success'':
"σ  ((s  A ; M s))    v σ'. the(A σ) = (v,σ')  σ'  (M v)"
apply(auto simp: valid_SE_def unit_SE_def bind_SE_def)
apply(cases "A σ", simp_all)
apply(drule_tac x="A σ" and f=the in arg_cong, simp)
apply(rule_tac x="fst aa" in exI)
apply(rule_tac x="snd aa" in exI, auto)
done


lemma exec_bind_SE_success''':
"σ  ((s  A ; M s))    a. (A σ) = Some a  (snd a)  (M (fst a))"
apply(auto simp: valid_SE_def unit_SE_def bind_SE_def)
apply(cases "A σ", simp_all)
apply(drule_tac x="A σ" and f=the in arg_cong, simp)
apply(rule_tac x="fst aa" in exI)
apply(rule_tac x="snd aa" in exI, auto)
done


lemma  exec_bind_SE_success'''' :
"σ  ((s  A ; M s))    v σ'. A σ = Some(v,σ')  σ'  (M v)"
apply(auto simp: valid_SE_def unit_SE_def bind_SE_def)
apply(cases "A σ", simp_all)
apply(drule_tac x="A σ" and f=the in arg_cong, simp)
apply(rule_tac x="fst aa" in exI)
apply(rule_tac x="snd aa" in exI, auto)
done


lemma valid_bind_cong : " f σ = g σ  (σ  (x  f ; M x)) = (σ  (x  g ; M x))"
  unfolding bind_SE'_def bind_SE_def valid_SE_def
    by simp
  
lemma valid_bind'_cong : " f σ = g σ  (σ  f ;- M) = (σ  g ;- M)"
  unfolding bind_SE'_def bind_SE_def valid_SE_def
    by simp


text‹Recall \verb+mbind_unit+ for the base case.›

lemma valid_mbind_mt : "(σ  ( s   mbindFailSave [] f; unitSE (P s))) = P [] " by simp
lemma valid_mbind_mtE: "σ  ( s  mbindFailSave [] f; unitSE (P s))  (P []  Q)  Q"
by(auto simp: valid_mbind_mt)

lemma valid_mbind'_mt : "(σ  ( s  mbindFailStop [] f; unitSE (P s))) = P [] " by simp
lemma valid_mbind'_mtE: "σ  ( s  mbindFailStop [] f; unitSE (P s))  (P []  Q)  Q"
by(auto simp: valid_mbind'_mt)

lemma valid_mbind''_mt : "(σ  ( s  mbindFailPurge [] f; unitSE (P s))) = P [] " 
by(simp add: mbind''.simps valid_SE_def bind_SE_def unit_SE_def)
lemma valid_mbind''_mtE: "σ  ( s  mbindFailPurge [] f; unitSE (P s))  (P []  Q)  Q"
by(auto simp: valid_mbind''_mt)


lemma exec_mbindFSave_failure: 
"ioprog a σ = None  
   (σ  (s  mbindFailSave (a#S) ioprog ; M s)) =  (σ  (M []))"
by(simp add: valid_SE_def unit_SE_def bind_SE_def)

lemma exec_mbindFStop_failure: 
"ioprog a σ = None  
   (σ  (s  mbindFailStop (a#S) ioprog ; M s)) =  (False)"
by(simp add: exec_bind_SE_failure)

lemma exec_mbindFPurge_failure: 
"ioprog a σ = None  
   (σ  (s  mbindFailPurge (a#S) ioprog ; M s)) = (σ  (s  mbindFailPurge (S) ioprog ; M s))" 
by(simp add: valid_SE_def unit_SE_def bind_SE_def mbind''.simps)


lemma exec_mbindFSave_success : 
"ioprog a σ = Some(b,σ')  
   (σ   (s  mbindFailSave (a#S) ioprog ; M s)) = 
   (σ'  (s  mbindFailSave S ioprog ; M (b#s)))"
unfolding valid_SE_def unit_SE_def bind_SE_def 
by(cases "mbindFailSave S ioprog σ'", auto)

lemma exec_mbindFStop_success : 
"ioprog a σ = Some(b,σ')  
   (σ   (s  mbindFailStop (a#S) ioprog ; M s)) = 
   (σ'  (s  mbindFailStop S ioprog ; M (b#s)))"
unfolding valid_SE_def unit_SE_def bind_SE_def 
by(cases "mbindFailStop S ioprog σ'", auto simp:  mbind'.simps)

lemma exec_mbindFPurge_success : 
"ioprog a σ = Some(b,σ')  
   (σ   (s  mbindFailPurge (a#S) ioprog ; M s)) = 
   (σ'  (s  mbindFailPurge S ioprog ; M (b#s)))"
unfolding valid_SE_def unit_SE_def bind_SE_def 
by(cases "mbindFailPurge S ioprog σ'", auto simp:  mbind''.simps)

lemma exec_mbindFSave:
"(σ  (s  mbindFailSave  (a#S) ioprog ; return (P s))) =
    (case ioprog a σ of
       None  (σ   (return (P [])))
     | Some(b,σ')  (σ'   (s  mbindFailSave  S ioprog ; return (P (b#s)))))"
apply(case_tac "ioprog a σ")
apply(auto simp: exec_mbindFSave_failure  exec_mbindFSave_success split: prod.splits)
done

lemma mbind_eq_sexec: 
assumes * : "b σ'. f a σ = Some(b,σ')  
             (os  mbindFailStop S f; P (b#os)) = (os  mbindFailStop S f; P' (b#os))"
shows       "( a  f a;  x  mbindFailStop S f; P (a # x)) σ = 
             ( a  f a;  x  mbindFailStop S f; P'(a # x)) σ"
  apply(cases "f a σ = None")
  apply(subst bind_SE_def, simp)
 apply(subst bind_SE_def, simp)
 apply auto
 apply(subst bind_SE_def, simp)
 apply(subst bind_SE_def, simp)
apply(simp add: *)
done


lemma mbind_eq_sexec': 
assumes * : "b σ'. f a σ = Some(b,σ')  
             (P (b))σ' = (P' (b))σ'"
shows       "( a  f a;  P (a)) σ = 
             ( a  f a;  P'(a)) σ"
 apply(cases "f a σ = None")
   apply(subst bind_SE_def, simp)
  apply(subst bind_SE_def, simp)
  apply auto
  apply(subst bind_SE_def, simp)
  apply(subst bind_SE_def, simp)
 apply(simp add: *)
done

lemma mbind'_concat:
"(os  mbindFailStop (S@T) f; P os) = (os  mbindFailStop S f; os'  mbindFailStop T f; P (os @ os'))"
proof (rule ext, rename_tac "σ", induct S arbitrary: σ P) 
   case Nil show ?case by simp
next
   case (Cons a S) show ?case 
        apply(insert Cons.hyps, simp)
        by(rule mbind_eq_sexec',simp)
qed

lemma assert_suffix_inv : 
              "σ  ( _  mbindFailStop xs istep; assertSE (P)) 
                σ. P σ  (σ  (_  istep x; assertSE (P)))
                σ  ( _  mbindFailStop (xs @ [x]) istep; assertSE (P))"
apply(subst mbind'_concat, simp)
unfolding bind_SE_def assert_SE_def valid_SE_def
apply(auto split: option.split option.split_asm)
apply(case_tac "aa",simp_all)
apply(case_tac "P bb",simp_all)
apply (metis option.distinct(1))
apply(case_tac "aa",simp_all)
apply(case_tac "P bb",simp_all)
by (metis option.distinct(1))



text‹Universal splitting and symbolic execution rule›
lemma exec_mbindFSave_E:
assumes seq : "(σ  (s  mbindFailSave (a#S) ioprog ;  (P s)))"
  and   none: "ioprog a σ = None  (σ  (P []))  Q"
  and   some: " b σ'. ioprog a σ = Some(b,σ')  (σ'  (s  mbindFailSave S ioprog;(P (b#s))))  Q "
shows   "Q"
using seq
proof(cases "ioprog a σ")  
   case None  assume ass:"ioprog a σ = None" show "Q" 
        apply(rule none[OF ass])
        apply(insert ass, erule_tac ioprog1=ioprog in exec_mbindFSave_failure[THEN iffD1],rule seq)
        done
next
   case (Some aa) assume ass:"ioprog a σ = Some aa" show "Q" 
        apply(insert ass,cases "aa",simp, rename_tac "out" "σ'")
        apply(erule some)
        apply(insert ass,simp)
        apply(erule_tac ioprog1=ioprog in exec_mbindFSave_success[THEN iffD1],rule seq)
        done
qed

text‹The next rule reveals the particular interest in deduction;
       as an elimination rule, it allows for a linear conversion of a validity judgement
       @{term "mbindFailStop"} over an input list @{term "S"} into a constraint system; without any 
       branching ... Symbolic execution can even be stopped tactically whenever 
       @{term "ioprog a σ = Some(b,σ')"} comes to a contradiction.›
lemma exec_mbindFStop_E:
assumes seq : "(σ  (s  mbindFailStop (a#S) ioprog ; (P s)))"
  and   some: "b σ'. ioprog a σ = Some(b,σ')  (σ' (s  mbindFailStop S ioprog;(P(b#s))))  Q"
shows   "Q"
using seq
proof(cases "ioprog a σ")  
   case None  assume ass:"ioprog a σ = None" show "Q" 
        apply(insert ass seq)
        apply(drule_tac σ=σ and S=S and M=P in exec_mbindFStop_failure, simp)
        done
next
   case (Some aa) assume ass:"ioprog a σ = Some aa" show "Q" 
        apply(insert ass,cases "aa",simp, rename_tac "out" "σ'")
        apply(erule some)
        apply(insert ass,simp)
        apply(erule_tac ioprog1=ioprog in exec_mbindFStop_success[THEN iffD1],rule seq)
        done
qed


lemma exec_mbindFPurge_E:
assumes seq : "(σ  (s  mbindFailPurge (a#S) ioprog ;  (P s)))"
  and   none: "ioprog a σ = None  (σ  (s  mbindFailPurge S ioprog;(P (s))))  Q"
  and   some: " b σ'. ioprog a σ = Some(b,σ')  (σ'  (s  mbindFailPurge S ioprog;(P (b#s))))  Q "
shows   "Q"
using seq
proof(cases "ioprog a σ")  
   case None  assume ass:"ioprog a σ = None" show "Q" 
        apply(rule none[OF ass])
        apply(insert ass, erule_tac ioprog1=ioprog in exec_mbindFPurge_failure[THEN iffD1],rule seq)
        done
next
   case (Some aa) assume ass:"ioprog a σ = Some aa" show "Q" 
        apply(insert ass,cases "aa",simp, rename_tac "out" "σ'")
        apply(erule some)
        apply(insert ass,simp)
        apply(erule_tac ioprog1=ioprog in exec_mbindFPurge_success[THEN iffD1],rule seq)
        done
qed


lemma assert_disch1 :" P σ  (σ  (x  assertSE P; M x)) = (σ  (M True))"
by(auto simp: bind_SE_def assert_SE_def valid_SE_def)

lemma assert_disch2 :" ¬ P σ  ¬ (σ  (x  assertSE P ; M s))"
by(auto simp: bind_SE_def assert_SE_def valid_SE_def)

lemma assert_disch3 :" ¬ P σ  ¬ (σ  (assertSE P))"
by(auto simp: bind_SE_def assert_SE_def valid_SE_def)

lemma assert_disch4 :" P σ   (σ  (assertSE P))"
by(auto simp: bind_SE_def assert_SE_def valid_SE_def)

lemma assert_simp : "(σ  assertSE P) = P σ"
by (meson assert_disch3 assert_disch4)

lemmas assert_D = assert_simp[THEN iffD1]  (* legacy *)

lemma assert_bind_simp : "(σ  (x  assertSE P; M x)) = (P σ  (σ  (M True)))"
by(auto simp: bind_SE_def assert_SE_def valid_SE_def split: HOL.if_split_asm)

lemmas assert_bindD = assert_bind_simp[THEN iffD1]  (* legacy *)


lemma assume_D : "(σ  (_  assumeSE P; M))   σ. (P σ  (σ  M) )"
apply(auto simp: bind_SE_def assume_SE_def valid_SE_def split: HOL.if_split_asm)
apply(rule_tac x="Eps P" in exI, auto)
apply(subst Hilbert_Choice.someI,assumption,simp)
done


lemma assume_E :
assumes *  : "σ  ( _  assumeSE P; M) "
and     ** : " σ. P σ  σ  M   Q"
shows  "Q"
apply(insert *)
by(insert *[THEN assume_D], auto intro: **)

lemma assume_E' :
assumes *  : "σ  assumeSE P ;- M"
and     ** : " σ. P σ  σ  M   Q"
shows  "Q"
by(insert *[simplified "bind_SE'_def", THEN assume_D], auto intro: **)


text‹These two rule prove that the SE Monad in connection with the notion of valid sequence
is actually sufficient for a representation of a Boogie-like language. The SBE monad with explicit
sets of states --- to be shown below --- is strictly speaking not necessary (and will therefore
be discontinued in the development).›

term "ifSE P then B1 else B2 fi"

lemma if_SE_D1 : "P σ  (σ  (ifSE P then B1 else B2 fi)) = (σ  B1)"
by(auto simp: if_SE_def valid_SE_def)

lemma if_SE_D1' : "P σ  (σ  (ifSE P then B1 else B2 fi);-M) = (σ  (B1;-M))"
by(auto simp: if_SE_def valid_SE_def bind_SE'_def bind_SE_def)


lemma if_SE_D2 : "¬ P σ  (σ  (ifSE P then B1 else B2 fi)) = (σ  B2)"
by(auto simp: if_SE_def valid_SE_def)

lemma if_SE_D2' : "¬ P σ  (σ  (ifSE P then B1 else B2 fi);-M) = (σ  B2;-M)"
by(auto simp: if_SE_def valid_SE_def bind_SE'_def bind_SE_def)


lemma if_SE_split_asm : 
"(σ  (ifSE P then B1 else B2 fi)) = ((P σ  (σ  B1))  (¬ P σ  (σ  B2)))"
by(cases "P σ",auto simp: if_SE_D1 if_SE_D2)

lemma if_SE_split_asm': 
"(σ  (ifSE P then B1 else B2 fi);-M) = ((P σ  (σ  B1;-M))  (¬ P σ  (σ  B2;-M)))"
by(cases "P σ",auto simp: if_SE_D1' if_SE_D2')


lemma if_SE_split: 
"(σ  (ifSE P then B1 else B2 fi)) = ((P σ  (σ  B1))  (¬ P σ  (σ  B2)))"
by(cases "P σ", auto simp: if_SE_D1 if_SE_D2)


lemma if_SE_split': 
"(σ  (ifSE P then B1 else B2 fi);-M) = ((P σ  (σ  B1;-M))  (¬ P σ  (σ  B2;-M)))"
by(cases "P σ", auto simp: if_SE_D1' if_SE_D2')

lemma if_SE_execE:
  assumes A: "σ  ((ifSE P then B1 else B2 fi))"
   and   B: "P σ   σ  (B1)  Q"
   and   C: "¬ P σ σ  (B2)  Q"
  shows  "Q"
by(insert A [simplified if_SE_split],cases  "P σ", simp_all, auto elim: B C)


lemma if_SE_execE':
  assumes A: "σ  ((ifSE P then B1 else B2 fi);-M)"
   and   B: "P σ   σ  (B1;-M)  Q"
   and   C: "¬ P σ σ  (B2;-M)  Q"
  shows  "Q"
by(insert A [simplified if_SE_split'],cases  "P σ", simp_all, auto elim: B C)


lemma exec_while : 
"(σ  ((whileSE b do c od) ;- M)) = 
 (σ  ((ifSE b then c ;- (whileSE b do c od) else unitSE ()fi) ;- M))"
apply(subst while_SE_unfold)
by(simp add: bind_SE'_def )

lemmas exec_whileD = exec_while[THEN iffD1]

lemma if_SE_execE'':
"σ  (ifSE P then B1 else B2 fi) ;- M 
 (P σ  σ  B1 ;- M  Q) 
 (¬ P σ  σ  B2 ;- M  Q) 
 Q"
by(auto elim: if_SE_execE')

definition "opaque (x::bool) = x"
lemma if_SE_execE''_pos:
"σ  (ifSE P then B1 else B2 fi) ;- M 
 (P σ  σ  B1 ;- M  Q) 
 (opaque (σ  (ifSE P then B1 else B2 fi) ;- M)  Q) 
 Q"
using opaque_def by auto


lemma [code]:
  "(σ  m) = (case (m σ) of None   False | (Some (x,y))   x)"
  apply(simp add: valid_SE_def)
  apply(cases "m σ = None", simp_all) 
  apply(insert not_None_eq, auto)
done

    
(* for the moment no good idea to state the case where the body eventually crashes. *)
lemma "P  σ  (_   assumeSE P ; x   M; assertSE (λσ.  (x=X)  Q x σ))"
oops

lemma "σ.  X. σ  (_   assumeSE P ; x   M; assertSE (λσ.  x=X  Q x σ))"
oops


lemma monadic_sequence_rule:
      " X σ1. (σ  (_   assumeSE (λσ'. (σ=σ')   P σ) ; x   M; assertSE (λσ.  (x=X)  (σ=σ1)  Q x σ)))
                
               (σ1  (_   assumeSE (λσ.  (σ=σ1)  Q x σ) ; y   M'; assertSE (λσ.  R x y σ)))
       
               σ  (_   assumeSE (λσ'. (σ=σ')   P σ) ; x   M; y   M'; assertSE (R x y))"
apply(elim exE impE conjE)
apply(drule assume_D) 
apply(elim exE impE conjE)
unfolding valid_SE_def assume_SE_def assert_SE_def bind_SE_def
apply(auto split: if_split HOL.if_split_asm Option.option.split Option.option.split_asm)
apply (metis (mono_tags, lifting) option.simps(3) someI_ex)
oops


  
lemma " X. σ  (_   assumeSE P ; x   M; assertSE (λσ.  x=X  Q x σ))
        
            σ  (_   assumeSE P ; x   M; assertSE (λσ. Q x σ))"
unfolding valid_SE_def assume_SE_def assert_SE_def bind_SE_def
by(auto split: if_split HOL.if_split_asm Option.option.split Option.option.split_asm)


lemma exec_skip:
"(σ  skipSE ;- M) = (σ  M)"
by (simp add: skipSE_def)

lemmas exec_skipD = exec_skip[THEN iffD1]


text‹Test-Refinements will be stated in terms of the failsave @{term mbind}, opting 
       more generality. The following lemma allows for an  optimization both in 
       test execution as well as in symbolic execution for an important special case of
       the post-codition: Whenever the latter has the constraint that the length of input and 
       output sequence equal each other (that is to say: no failure occured), failsave mbind
       can be reduced to failstop mbind ...›
lemma mbindFSave_vs_mbindFStop : 
  "(σ  (os  (mbindFailSave ιs ioprog); result(length ιs = length os  P ιs os))) = 
   (σ  (os  (mbindFailStop ιs ioprog); result(P ιs os)))"
  apply(rule_tac x=P in spec)
  apply(rule_tac x=σ in spec)
  proof(induct "ιs") 
     case Nil show ?case by(simp_all add: mbind_try try_SE_def del: Seq_MonadSE.mbind.simps)
     case (Cons a ιs) show ?case
          apply(rule allI, rename_tac "σ",rule allI, rename_tac "P")
          apply(insert Cons.hyps)
          apply(case_tac "ioprog a σ")
          apply(simp only: exec_mbindFSave_failure exec_mbindFStop_failure, simp)
          apply(simp add:  split_paired_all del: Seq_MonadSE.mbind.simps )
          apply(rename_tac "σ'") 
          apply(subst exec_mbindFSave_success, assumption)
          apply(subst (2) exec_bind_SE_success, assumption)
          apply(erule_tac x="σ'" in allE)
          apply(erule_tac x="λιs s. P (a # ιs) (aa # s)" in allE) (* heureka ! *)
          apply(simp)
      done
  qed


lemma mbindFailSave_vs_mbindFailStop:
assumes A: " ι σ. ioprog ι σ  None"
shows      "(σ  (os  (mbindFailSave ιs ioprog); P os)) = 
            (σ  (os  (mbindFailStop ιs ioprog); P os))" 
proof(induct "ιs") 
  case Nil show ?case by simp
next 
  case (Cons a ιs) 
       from Cons.hyps                           
       have B:" S f σ. mbindFailSave S f σ  None " by simp
       have C:"σ. mbindFailStop ιs ioprog σ = mbindFailSave ιs ioprog σ" 
               apply(induct ιs, simp)
               apply(rule allI,rename_tac "σ")
               apply(simp add: Seq_MonadSE.mbind'.simps(2))
               apply(insert A, erule_tac x="a" in allE)
               apply(erule_tac x="σ" and P="λσ . ioprog a σ  None" in allE)
               apply(auto split:option.split)
               done
       show ?case 
       apply(insert A,erule_tac x="a" in allE,erule_tac x="σ" in allE)
       apply(simp, elim exE)
       apply(rename_tac  "out" "σ'")
       apply(insert B, erule_tac x=ιs in allE, erule_tac x=ioprog in allE, erule_tac x=σ' in allE)
       apply(subst(asm) not_None_eq, elim exE)
       apply(subst  exec_bind_SE_success)
       apply(simp   split: option.split, auto)
       apply(rule_tac s="(λ a b c. a # (fst c)) out σ' (aa, b)" in trans, simp,rule refl)
       apply(rule_tac s="(λ a b c. (snd c)) out σ' (aa, b)" in trans, simp,rule refl)
       apply(simp_all)
       apply(subst  exec_bind_SE_success, assumption)
       apply(subst  exec_bind_SE_success)
       apply(rule_tac s="Some (aa, b)" in  trans,simp_all add:C)
       apply(subst(asm)  exec_bind_SE_success, assumption)
       apply(subst(asm)  exec_bind_SE_success)
       apply(rule_tac s="Some (aa, b)" in  trans,simp_all add:C)
    done
qed

subsection‹Miscellaneous›

no_notation unit_SE ("(result _)" 8)

end
  

Theory Clean

(******************************************************************************
 * Clean
 *
 * Copyright (c) 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.
 ******************************************************************************)

(*
 * Clean --- a basic abstract ("shallow") programming language for test and proof.
 * Burkhart Wolff, Frédéric Tuong and Chantal Keller, LRI, Univ. Paris-Saclay, France
 *)

chapter ‹The Clean Language›

theory Clean
  imports Symbex_MonadSE
  keywords "global_vars" "local_vars_test" :: thy_decl 
     and "returns" "pre" "post" "local_vars" "variant" 
     and "function_spec" :: thy_decl
     and "rec_function_spec"   :: thy_decl

begin

text‹Clean (pronounced as: ``C lean'' or ``Céline'' [selin]) is a minimalistic imperative language 
with C-like control-flow operators based on a shallow embedding into the ``State Exception Monads'' theory 
formalized in 🗏‹MonadSE.thy›. It strives for a type-safe notation of program-variables, an
incremental construction of the typed state-space in order to facilitate incremental verification
and open-world extensibility to new type definitions intertwined with the program
definition.

It comprises:
\begin{itemize}
\item C-like control flow with termbreak and termreturn,
\item global variables,
\item function calls (seen as monadic executions) with side-effects, recursion
      and local variables,
\item parameters are modeled via functional abstractions 
      (functions are monads); a passing of parameters to local variables
      might be added later,
\item direct recursive function calls,
\item cartouche syntax for λ›-lifted update operations supporting global and local variables.
\end{itemize}

Note that Clean in its current version is restricted to ‹monomorphic› global and local variables
as well as function parameters. This limitation will be overcome at a later stage. The construction
in itself, however, is deeply based on parametric polymorphism (enabling structured proofs over
extensible records as used in languages of the ML family
🌐‹http://www.cs.ioc.ee/tfp-icfp-gpce05/tfp-proc/21num.pdf›
and Haskell 🌐‹https://www.schoolofhaskell.com/user/fumieval/extensible-records›).
›

(*<*)
text@{footnote ‹sdf›}, @{file "$ISABELLE_HOME/src/Pure/ROOT.ML"} 
(*>*)

section‹A High-level Description of the Clean Memory Model›

subsection‹A Simple Typed Memory Model of Clean: An Introduction ›
text‹ Clean is based on a ``no-frills'' state-exception monad 
type_synonym ('o, ) MONSE = ‹'σ ⇀ ('o × 'σ)› with the 
usual definitions of termbind and termunit.
In this language, sequence operators, conditionals and loops can be integrated. ›

text‹From a concrete program, the underlying state  is ‹incrementally› constructed by a
sequence of extensible record definitions:
 Initially, an internal control state is defined to give semantics to termbreak and
 termreturn statements:
  \begin{isar}
        record control_state =  break_val  :: bool   return_val :: bool
  \end{isar}
  ‹control_state› represents the $\sigma_0$ state.
 Any global variable definition block with definitions $a_1 : \tau_1$ $\dots$ $a_n : \tau_n$  
  is translated into a record extension:
  \begin{isar}
        record σ$_{n+1}$ = σ$_n$    +    a$_1$ :: $\tau_1$; ...; $a_n$ :: $\tau_n$
  \end{isar}
 Any local variable definition block (as part of a procedure declaration) 
  with definitions $a_1 : \tau_1$ $\dots$ $a_n : \tau_n$ is translated into the record extension:
  \begin{isar}
        record σ$_{n+1}$ = σ$_n$    +    a$_1$ :: $\tau_1$ list; ...; $a_n$ :: $\tau_n$ list; result :: $\tau_{result-type}$ list; 
  \end{isar}
  where the typ_ list›-lifting is used to model a ‹stack› of local variable instances
  in case of direct recursions and the termresult_value used for the value of the termreturn
  statement.›

text ‹ The record package creates an  extensible record type 
 control_state_ext› where the  stands for extensions that are subsequently ``stuffed'' in
them. Furthermore, it generates definitions for the constructor, accessor and update functions and
automatically derives a number of theorems over them (e.g., ``updates on different fields commute'',
``accessors on a record are surjective'', ``accessors yield the value of the last update''). The
collection of these theorems constitutes the ‹memory model› of Clean, providing an incrementally 
extensible state-space for global and local program variables. In contrast to axiomatizations
of memory models, our generated state-spaces might be ``wrong'' in the sense that they do not 
reflect the operational behaviour of a particular compiler or a sufficiently large portion of the 
C language; however, it is by construction ‹logically consistent› since it is
impossible to derive falsity from the entire set of conservative extension schemes used in their
construction. A particular advantage of the incremental state-space construction is that it
supports incremental verification and interleaving of program definitions with theory development.›

subsection‹ Formally Modeling Control-States  ›

text‹The control state is the ``root'' of all extensions for local and global variable
spaces in Clean. It contains just the information of the current control-flow: a termbreak occurred
(meaning all commands till the end of the control block will be skipped) or a termreturn occurred
(meaning all commands till the end of the current function body will be skipped).›
  
record  control_state = 
            break_status  :: bool
            return_status :: bool

(* break quits innermost while or for, return quits an entire execution sequence. *)  
definition break :: "(unit, ('σ_ext) control_state_ext) MONSE"
  where   "break  (λ σ. Some((), σ  break_status := True ))"
  
definition unset_break_status :: "(unit, ('σ_ext) control_state_ext) MONSE"
  where   "unset_break_status  (λ σ. Some((), σ  break_status := False ))"

definition set_return_status :: " (unit, ('σ_ext) control_state_ext) MONSE"    
  where   "set_return_status = (λ σ. Some((), σ  return_status := True ))"
    
definition unset_return_status :: "(unit, ('σ_ext) control_state_ext) MONSE"    
  where   "unset_return_status  = (λ σ. Some((), σ  return_status := False ))"


definition exec_stop :: "('σ_ext) control_state_ext  bool"
  where   "exec_stop = (λ σ. break_status σ  return_status σ )"

lemma exec_stop1[simp] : "break_status σ  exec_stop σ" 
  unfolding exec_stop_def by simp

lemma exec_stop2[simp] : "return_status σ  exec_stop σ" 
  unfolding exec_stop_def by simp

text‹ On the basis of the control-state, assignments, conditionals and loops are reformulated
  into term‹break›-aware and termreturn-aware versions as shown in the definitions of
  termassign and termif_C (in this theory file, see below). ›

text‹For Reasoning over Clean programs, we need the notion of independance of an
     update from the control-block: ›


definition control_independence ::
                 "(('b'b)'a control_state_scheme  'a control_state_scheme)  bool"    ("")
           where " upd  (σ T b. break_status (upd T σ) = break_status σ 
                                  return_status (upd T σ) = return_status σ
                                  upd T (σ return_status := b ) = (upd T σ) return_status := b 
                                  upd T (σ break_status := b ) = (upd T σ) break_status := b ) "



lemma exec_stop_vs_control_independence [simp]:
  " upd  exec_stop (upd f σ) = exec_stop σ"
  unfolding control_independence_def exec_stop_def  by simp


lemma exec_stop_vs_control_independence' [simp]:
  " upd  (upd f (σ  return_status := b )) = (upd f σ) return_status := b "
  unfolding control_independence_def exec_stop_def by simp

lemma exec_stop_vs_control_independence'' [simp]:
  " upd  (upd f (σ  break_status := b )) = (upd f σ)  break_status := b "
  unfolding control_independence_def exec_stop_def  by simp




subsection‹An Example for Global Variable Declarations.›
text‹We present the above definition of the incremental construction of the state-space in more
detail via an example construction.

Consider a global variable A› representing an array of integer. This 
‹global variable declaration› corresponds to the effect of the following
record declaration:

record state0 = control_state + A :: "int list"

which is later extended by another global variable, say, B› representing a real
described in the Cauchy Sequence form @{typ "nat  (int × int)"} as follows:

record state1 = state0 + B :: "nat ⇒ (int × int)".

A further extension would be needed if a (potentially recursive) function f› with some local
variable tmp› is defined:
record state2 = state1 + tmp :: "nat stack" result_value :: "nat stack", where the stack›
needed for modeling recursive instances is just a synonym for list›.
›

subsection‹ The Assignment Operations (embedded in State-Exception Monad) ›
text‹Based on the global variable states, we define   term‹break›-aware and termreturn-aware 
version of the assignment. The trick to do this in a generic ‹and› type-safe way is to provide
the generated accessor and update functions (the ``lens'' representing this global variable,
cf. @{cite "Foster2009BidirectionalPL" and "DBLP:journals/toplas/FosterGMPS07" and
"DBLP:conf/ictac/FosterZW16"}) to the generic assign operators. This pair of accessor and update
carries all relevant semantic and type information of this particular variable and ‹characterizes›
this variable semantically. Specific syntactic support~‹via the Isabelle concept of
cartouche: 🌐‹https://isabelle.in.tum.de/doc/isar-ref.pdf› will hide away the syntactic overhead and permit a human-readable
form of assignments or expressions accessing the underlying state. ›


consts syntax_assign :: "(   int)  int  term" (infix ":=" 60)

definition assign :: "(('σ_ext) control_state_scheme   
                       ('σ_ext) control_state_scheme)  
                       (unit,('σ_ext) control_state_scheme)MONSE"
  where   "assign f = (λσ. if exec_stop σ then Some((), σ) else Some((), f σ))"


definition  assign_global :: "(('a   'a )  'σ_ext control_state_scheme  'σ_ext control_state_scheme)
                               ('σ_ext control_state_scheme   'a)
                               (unit,'σ_ext control_state_scheme) MONSE"
  where    "assign_global upd rhs = assign(λσ. ((upd) (λ_. rhs σ)) σ)"

text‹An update of the variable A› based on the state of the previous example is done 
by @{term [source = true] ‹assign_global A_upd (λσ. list_update (A σ) (i) (A σ ! j))}
representing A[i] = A[j]›; arbitrary nested updates can be constructed accordingly.›

text‹Local variable spaces work analogously; except that they are represented by a stack
in order to support individual instances in case of function recursion. This requires
automated generation of specific push- and pop operations used to model the effect of
entering or leaving a function block (to be discussed later).›


fun      map_hd :: "('a  'a)  'a list  'a list" 
  where "map_hd f [] = []"
      | "map_hd f (a#S) = f a # S"

lemma tl_map_hd [simp] :"tl (map_hd f S) = tl S"  by (metis list.sel(3) map_hd.elims) 

definition "map_nth = (λi f l. list_update l i (f (l ! i)))"

definition  assign_local :: "(('a list  'a list) 
                                  'σ_ext control_state_scheme  'σ_ext control_state_scheme)
                              ('σ_ext control_state_scheme   'a)
                              (unit,'σ_ext control_state_scheme) MONSE"
  where    "assign_local upd rhs = assign(λσ. ((upd o map_hd) (%_. rhs σ)) σ)"


text‹Semantically, the difference between ‹global› and ‹local› is rather unimpressive as the 
     following lemma shows. However, the distinction matters for the pretty-printing setup of Clean.›
lemma "assign_local upd rhs = assign_global (upd o map_hd) rhs "
      unfolding assign_local_def assign_global_def by simp

text‹The return› command in C-like languages is represented basically by an assignment to a local
variable result_value› (see below in the Clean-package generation), plus some setup of 
term‹return_status›. Note that a termreturn may appear after a term‹break› and should have no effect
in this case.›

definition returnC :: "(('a list  'a list)  'σ_ext control_state_scheme  'σ_ext control_state_scheme)
                       ('σ_ext control_state_scheme   'a)
                       (unit,'σ_ext control_state_scheme) MONSE"
  where   "returnC upd rhs =(λσ. if exec_stop σ then Some((), σ) 
                                                else (assign_local upd rhs ;- set_return_status) σ)" 

subsection‹Example for a Local Variable Space›
text‹Consider the usual operation swap› defined in some free-style syntax as follows:
@{cartouche [display] ‹
  function_spec swap (i::nat,j::nat)
  local_vars   tmp :: int 
  defines      " ‹ tmp  := A ! i› ;-
                 ‹ A[i] := A ! j› ;- 
                 ‹ A[j] := tmp› "›}

text‹ 
For the fantasy syntax  tmp := A ! i›, we can construct the following semantic code:
@{term [source = true] ‹assign_local tmp_update (λσ. (A σ) ! i )} where tmp_update› is the
update operation generated by the record-package, which is generated while treating local variables
of swap›. By the way, a stack for return›-values is also generated in order to give semantics
to a return› operation: it is syntactically equivalent to the assignment of 
the result variable  in the local state (stack). It sets the termreturn_val flag.

The management of the local state space requires function-specific push› and pop› operations,
for which suitable definitions are generated as well:

@{cartouche [display]
‹definition push_local_swap_state :: "(unit,'a local_swap_state_scheme) MONSE"
   where   "push_local_swap_state σ = 
                     Some((),σ⦇local_swap_state.tmp := undefined # local_swap_state.tmp σ,
                               local_swap_state.result_value := undefined # 
                                                                  local_swap_state.result_value σ  ⦈)"

 definition pop_local_swap_state :: "(unit,'a local_swap_state_scheme) MONSE"
   where   "pop_local_swap_state σ = 
                    Some(hd(local_swap_state.result_value σ), 
                         σ⦇local_swap_state.tmp:= tl( local_swap_state.tmp σ) ⦈)"›}
where result_value› is the stack for potential result values (not needed in the concrete
example swap›).
›


section‹ Global and Local State Management via Extensible Records ›

text‹In the sequel, we present the automation of the state-management as schematically discussed
in the previous section; the declarations of global and local variable blocks are constructed by 
subsequent extensions of @{typ "'a control_state_scheme"}, defined above.›
MLstructure StateMgt_core = 
struct

val control_stateT = Syntax.parse_typ @{context} "control_state"
val control_stateS = @{typ "('a)control_state_scheme"};

fun optionT t = Type(@{type_name "Option.option"},[t]);
fun MON_SE_T res state = state --> optionT(HOLogic.mk_prodT(res,state));

fun merge_control_stateS (@{typ "('a)control_state_scheme"},t) = t
   |merge_control_stateS (t, @{typ "('a)control_state_scheme"}) = t
   |merge_control_stateS (t, t') = if (t = t') then t else error"can not merge Clean state"

datatype var_kind = global_var of typ | local_var of typ

fun type_of(global_var t) = t | type_of(local_var t) = t

type state_field_tab = var_kind Symtab.table

structure Data = Generic_Data
(
  type T                      = (state_field_tab * typ (* current extensible record *)) 
  val  empty                  = (Symtab.empty,control_stateS)
  val  extend                 = I
  fun  merge((s1,t1),(s2,t2)) = (Symtab.merge (op =)(s1,s2),merge_control_stateS(t1,t2))
);


val get_data                   = Data.get o Context.Proof;
val map_data                   = Data.map;
val get_data_global            = Data.get o Context.Theory;
val map_data_global            = Context.theory_map o map_data;

val get_state_type             = snd o get_data
val get_state_type_global      = snd o get_data_global
val get_state_field_tab        = fst o get_data
val get_state_field_tab_global = fst o get_data_global
fun upd_state_type f           = map_data (fn (tab,t) => (tab, f t))
fun upd_state_type_global f    = map_data_global (fn (tab,t) => (tab, f t))

fun fetch_state_field (ln,X)   = let val a::b:: _  = rev (Long_Name.explode ln) in ((b,a),X) end;

fun filter_name name ln        = let val ((a,b),X) = fetch_state_field ln
                                 in  if a = name then SOME((a,b),X) else NONE end;

fun filter_attr_of name thy    = let val tabs = get_state_field_tab_global thy
                                 in  map_filter (filter_name name) (Symtab.dest tabs) end;

fun is_program_variable name thy = Symtab.defined((fst o get_data_global) thy) name

fun is_global_program_variable name thy = case Symtab.lookup((fst o get_data_global) thy) name of
                                             SOME(global_var _) => true
                                           | _ => false

fun is_local_program_variable name thy = case Symtab.lookup((fst o get_data_global) thy) name of
                                             SOME(local_var _) => true
                                           | _ => false

fun declare_state_variable_global f field thy  =  
             let val Const(name,ty) = Syntax.read_term_global thy field
             in  (map_data_global (apfst (Symtab.update_new(name,f ty))) (thy)
                 handle Symtab.DUP _ => error("multiple declaration of global var"))
             end;

fun declare_state_variable_local f field ctxt  = 
             let val Const(name,ty) = Syntax.read_term_global  (Context.theory_of ctxt) field
             in  (map_data (apfst (Symtab.update_new(name,f ty)))(ctxt)
                 handle Symtab.DUP _ => error("multiple declaration of global var"))
             end;

end

subsection‹Block-Structures›
text‹ On the managed local state-spaces, it is now straight-forward to define the semantics for 
a block› representing the necessary management of local variable instances:
›
definition blockC :: "  (unit, ('σ_ext) control_state_ext)MONSE
                      (unit, ('σ_ext) control_state_ext)MONSE  
                      (, ('σ_ext) control_state_ext)MONSE
                      (, ('σ_ext) control_state_ext)MONSE"
  where   "blockC push core pop  (          ― ‹assumes break and return unset › 
                                   push ;-   ― ‹create new instances of local variables › 
                                   core ;-   ― ‹execute the body ›
                                   unset_break_status ;-    ― ‹unset a potential break ›
                                   unset_return_status;-    ― ‹unset a potential return break ›
                                   (x  pop;           ― ‹restore previous local var instances ›
                                    unitSE(x)))"        ― ‹yield the return value ›

text‹ Based on this definition, the running swap› example is represented as follows:

@{cartouche [display]
‹definition swap_core :: "nat × nat ⇒  (unit,'a local_swap_state_scheme) MONSE"
    where "swap_core  ≡ (λ(i,j). ((assign_local tmp_update (λσ. A σ ! i ))   ;-
                            (assign_global A_update (λσ. list_update (A σ) (i) (A σ ! j))) ;- 
                            (assign_global A_update (λσ. list_update (A σ) (j) ((hd o tmp) σ)))))" 

definition swap :: "nat × nat ⇒  (unit,'a local_swap_state_scheme) MONSE"
  where   "swap ≡ λ(i,j). blockC push_local_swap_state (swap_core (i,j)) pop_local_swap_state"
›}

subsection‹Call Semantics›

text‹It is now straight-forward to define the semantics of a generic call --- 
which is simply a monad execution that is term‹break›-aware and termreturn-aware.›

definition callC :: "(   (, ('σ_ext) control_state_ext)MONSE) 
                       ((('σ_ext) control_state_ext)  )                         
                      (, ('σ_ext) control_state_ext)MONSE"
  where   "callC M A1 = (λσ. if exec_stop σ then Some(undefined, σ) else M (A1 σ) σ)"

text‹Note that this presentation assumes a uncurried format of the arguments. The 
question arises if this is the right approach to handle calls of operation with multiple arguments.
Is it better to go for an some appropriate currying principle? Here are 
 some more experimental variants for curried operations...
›

definition call_0C :: "(, ('σ_ext) control_state_ext)MONSE  (, ('σ_ext) control_state_ext)MONSE"
  where   "call_0C M = (λσ. if exec_stop σ then Some(undefined, σ) else M σ)"

text‹The generic version using tuples is identical with @{term call_1C}.›
definition call_1C :: "(   (, ('σ_ext) control_state_ext)MONSE) 
                       ((('σ_ext) control_state_ext)  )                         
                      (, ('σ_ext) control_state_ext)MONSE"                                                      
  where   "call_1C  = callC"

definition call_2C :: "(     (, ('σ_ext) control_state_ext)MONSE) 
                       ((('σ_ext) control_state_ext)  )                         
                       ((('σ_ext) control_state_ext)  )       
                      (, ('σ_ext) control_state_ext)MONSE"
  where   "call_2C M A1 A2 = (λσ. if exec_stop σ then Some(undefined, σ) else M (A1 σ) (A2 σ) σ)"

definition call_3C :: "(        (, ('σ_ext) control_state_ext)MONSE) 
                       ((('σ_ext) control_state_ext)  )                         
                       ((('σ_ext) control_state_ext)  )       
                       ((('σ_ext) control_state_ext)  )       
                      (, ('σ_ext) control_state_ext)MONSE"
  where   "call_3C M A1 A2 A3 = (λσ. if exec_stop σ then Some(undefined, σ) 
                                                   else M (A1 σ) (A2 σ) (A3 σ) σ)"

(* and 4 and 5 and ... *)                        
  

section‹ Some Term-Coding Functions ›

text‹In the following, we add a number of advanced HOL-term constructors in the style of 
@{ML_structure "HOLogic"} from the Isabelle/HOL libraries. They incorporate the construction
of types during term construction in a bottom-up manner. Consequently, the leafs of such
terms should always be typed, and anonymous loose-@{ML "Bound"} variables avoided.›

ML(* HOLogic extended *)

fun mk_None ty = let val none = const_name‹Option.option.None›
                     val none_ty = ty --> Type(type_name‹option›,[ty])
                in  Const(none, none_ty)
                end;

fun mk_Some t = let val some = const_name‹Option.option.Some› 
                    val ty = fastype_of t
                    val some_ty = ty --> Type(type_name‹option›,[ty])
                in  Const(some, some_ty) $ t
                end;

fun dest_listTy (Type(type_name‹List.list›, [T])) = T;

fun mk_hdT t = let val ty = fastype_of t 
               in  Const(const_name‹List.hd›, ty --> (dest_listTy ty)) $ t end

fun mk_tlT t = let val ty = fastype_of t 
               in  Const(const_name‹List.tl›, ty --> ty) $ t end


fun  mk_undefined (@{typ "unit"}) = Const (const_name‹Product_Type.Unity›, typ‹unit›)
    |mk_undefined t               = Const (const_name‹HOL.undefined›, t)

fun meta_eq_const T = Const (const_name‹Pure.eq›, T --> T --> propT);

fun mk_meta_eq (t, u) = meta_eq_const (fastype_of t) $ t $ u;

fun   mk_pat_tupleabs [] t = t
    | mk_pat_tupleabs [(s,ty)] t = absfree(s,ty)(t)
    | mk_pat_tupleabs ((s,ty)::R) t = HOLogic.mk_case_prod(absfree(s,ty)(mk_pat_tupleabs R t));

fun read_constname ctxt n = fst(dest_Const(Syntax.read_term ctxt n))

fun wfrecT order recs = 
    let val funT = domain_type (fastype_of recs)
        val aTy  = domain_type funT
        val ordTy = HOLogic.mk_setT(HOLogic.mk_prodT (aTy,aTy))
    in Const(const_name‹Wfrec.wfrec›, ordTy --> (funT --> funT) --> funT) $ order $ recs end

text‹And here comes the core of the ‹Clean›-State-Management: the module that provides the 
functionality for the commands keywords global_vars, local_vars  and local_vars_test.
Note that the difference between local_vars and local_vars_test is just a technical one:
local_vars can only be used inside a Clean function specification, made with the function_spec
command. On the other hand, local_vars_test is defined as a global Isar command for test purposes. 

A particular feature of the local-variable management is the provision of definitions for termpush
and termpop operations --- encoded as typ('o, ) MONSE operations --- which are vital for
the function specifications defined below.
›

MLstructure StateMgt = 
struct

open StateMgt_core

val result_name = "result_value"

fun get_result_value_conf name thy = 
        let val  S = filter_attr_of name thy
        in  hd(filter (fn ((_,b),_) => b = result_name) S) 
            handle Empty => error "internal error: get_result_value_conf " end; 


fun mk_lookup_result_value_term name sty thy =
    let val ((prefix,name),local_var(Type("fun", [_,ty]))) = get_result_value_conf name thy;
        val long_name = Sign.intern_const thy (prefix^"."^name)
        val term = Const(long_name, sty --> ty)
    in  mk_hdT (term $ Free("σ",sty)) end


fun  map_to_update sty is_pop thy ((struct_name, attr_name), local_var (Type("fun",[_,ty]))) term = 
       let val tlT = if is_pop then Const(const_name‹List.tl›, ty --> ty)
                     else Const(const_name‹List.Cons›, dest_listTy ty --> ty --> ty)
                          $ mk_undefined (dest_listTy ty)
           val update_name = Sign.intern_const  thy (struct_name^"."^attr_name^"_update")
       in (Const(update_name, (ty --> ty) --> sty --> sty) $ tlT) $ term end
   | map_to_update _ _ _ ((_, _),_) _ = error("internal error map_to_update")     

fun mk_local_state_name binding = 
       Binding.prefix_name "local_" (Binding.suffix_name "_state" binding)  
fun mk_global_state_name binding = 
       Binding.prefix_name "global_" (Binding.suffix_name "_state" binding)  

fun construct_update is_pop binding sty thy = 
       let val long_name = Binding.name_of( binding)
           val attrS = StateMgt_core.filter_attr_of long_name thy
       in  fold (map_to_update sty is_pop thy) (attrS) (Free("σ",sty)) end

fun cmd (decl, spec, prems, params) = #2 oo Specification.definition' decl params prems spec

fun mk_push_name binding = Binding.prefix_name "push_" binding

fun push_eq binding  name_op rty sty lthy = 
         let val mty = MON_SE_T rty sty 
             val thy = Proof_Context.theory_of lthy
             val term = construct_update false binding sty thy
         in  mk_meta_eq((Free(name_op, mty) $ Free("σ",sty)), 
                         mk_Some ( HOLogic.mk_prod (mk_undefined rty,term)))
                          
         end;

fun mk_push_def binding sty lthy =
    let val name_pushop =  mk_push_name binding
        val rty = typ‹unit›
        val eq = push_eq binding  (Binding.name_of name_pushop) rty sty lthy
        val mty = StateMgt_core.MON_SE_T rty sty 
        val args = (SOME(name_pushop, SOME mty, NoSyn), (Binding.empty_atts,eq),[],[])
    in cmd args true lthy  end;

fun mk_pop_name binding = Binding.prefix_name "pop_"  binding

fun pop_eq  binding name_op rty sty lthy = 
         let val mty = MON_SE_T rty sty 
             val thy = Proof_Context.theory_of lthy
             val res_access = mk_lookup_result_value_term (Binding.name_of binding) sty thy
             val term = construct_update true binding  sty thy                 
         in  mk_meta_eq((Free(name_op, mty) $ Free("σ",sty)), 
                         mk_Some ( HOLogic.mk_prod (res_access,term)))                          
         end;


fun mk_pop_def binding rty sty lthy = 
    let val mty = StateMgt_core.MON_SE_T rty sty 
        val name_op =  mk_pop_name binding
        val eq = pop_eq binding (Binding.name_of name_op) rty sty lthy
        val args = (SOME(name_op, SOME mty, NoSyn),(Binding.empty_atts,eq),[],[])
    in cmd args true lthy
    end;


fun read_parent NONE ctxt = (NONE, ctxt)
  | read_parent (SOME raw_T) ctxt =
       (case Proof_Context.read_typ_abbrev ctxt raw_T of
        Type (name, Ts) => (SOME (Ts, name), fold Variable.declare_typ Ts ctxt)
      | T => error ("Bad parent record specification: " ^ Syntax.string_of_typ ctxt T));


fun read_fields raw_fields ctxt =
  let
    val Ts = Syntax.read_typs ctxt (map (fn (_, raw_T, _) => raw_T) raw_fields);
    val fields = map2 (fn (x, _, mx) => fn T => (x, T, mx)) raw_fields Ts;
    val ctxt' = fold Variable.declare_typ Ts ctxt;
  in (fields, ctxt') end;

fun parse_typ_'a ctxt binding = 
  let val ty_bind =  Binding.prefix_name "'a " (Binding.suffix_name "_scheme" binding)
  in case Syntax.parse_typ ctxt (Binding.name_of ty_bind) of
       Type (s, _) => Type (s, [@{typ "'a::type"}])
     | _ => error ("Unexpected type" ^ Position.here )
  end

fun add_record_cmd0 read_fields overloaded is_global_kind raw_params binding raw_parent raw_fields thy =
  let
    val ctxt = Proof_Context.init_global thy;
    val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params;
    val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt;
    val (parent, ctxt2) = read_parent raw_parent ctxt1;
    val (fields, ctxt3) = read_fields raw_fields ctxt2;
    fun lift (a,b,c) =  (a, HOLogic.listT b, c)
    val fields' = if is_global_kind then fields else map lift fields
    val params' = map (Proof_Context.check_tfree ctxt3) params;
    val declare = StateMgt_core.declare_state_variable_global
    fun upd_state_typ thy = let val ctxt = Proof_Context.init_global thy
                                val ty = Syntax.parse_typ ctxt (Binding.name_of binding)
                            in  StateMgt_core.upd_state_type_global(K ty)(thy) end
    fun insert_var ((f,_,_), thy) =           
            if is_global_kind   
            then declare StateMgt_core.global_var (Binding.name_of f) thy
            else declare StateMgt_core.local_var  (Binding.name_of f) thy
    fun define_push_pop thy = 
            if not is_global_kind 
            then let val sty = parse_typ_'a (Proof_Context.init_global thy) binding;
                     val rty = dest_listTy (#2(hd(rev fields')))
                 in thy

                    |> Named_Target.theory_map (mk_push_def binding sty) 
                    |> Named_Target.theory_map (mk_pop_def  binding rty sty) 
                                                            
                 end
            else thy
  in thy |> Record.add_record overloaded (params', binding) parent fields' 
         |> (fn thy =>  List.foldr insert_var (thy) (fields'))
         |> upd_state_typ
         |> define_push_pop 
  end;



fun typ_2_string_raw (Type(s,[TFree _])) = if String.isSuffix "_scheme" s
                                            then Long_Name.base_name(unsuffix "_scheme" s)
                                            else Long_Name.base_name(unsuffix "_ext" s)
                                          
   |typ_2_string_raw (Type(s,_)) = 
                         error ("Illegal parameterized state type - not allowed in Clean:"  ^ s) 
   |typ_2_string_raw _ = error  "Illegal state type - not allowed in Clean." 
                                  
             
fun new_state_record0 add_record_cmd is_global_kind (((raw_params, binding), res_ty), raw_fields) thy =
    let val binding = if is_global_kind 
                      then mk_global_state_name binding
                      else mk_local_state_name binding
        val raw_parent = SOME(typ_2_string_raw (StateMgt_core.get_state_type_global thy))
        val pos = Binding.pos_of binding
        fun upd_state_typ thy =
          StateMgt_core.upd_state_type_global (K (parse_typ_'a (Proof_Context.init_global thy) binding)) thy
        val result_binding = Binding.make(result_name,pos)
        val raw_fields' = case res_ty of 
                            NONE => raw_fields
                          | SOME res_ty => raw_fields @ [(result_binding,res_ty, NoSyn)]
    in  thy |> add_record_cmd {overloaded = false} is_global_kind 
                              raw_params binding raw_parent raw_fields' 
            |> upd_state_typ 

    end

val add_record_cmd    = add_record_cmd0 read_fields;
val add_record_cmd'   = add_record_cmd0 pair;

val new_state_record  = new_state_record0 add_record_cmd
val new_state_record' = new_state_record0 add_record_cmd'

val _ =
  Outer_Syntax.command 
      command_keywordglobal_vars   
      "define global state record"
      ((Parse.type_args_constrained -- Parse.binding)
    -- Scan.succeed NONE
    -- Scan.repeat1 Parse.const_binding
    >> (Toplevel.theory o new_state_record true));
;

val _ =
  Outer_Syntax.command 
      command_keywordlocal_vars_test  
      "define local state record"
      ((Parse.type_args_constrained -- Parse.binding) 
    -- (Parse.typ >> SOME)
    -- Scan.repeat1 Parse.const_binding
    >> (Toplevel.theory o new_state_record false))
;
end

section‹Syntactic Sugar supporting λ›-lifting for Global and Local Variables ›

ML structure Clean_Syntax_Lift =
struct
  local
    fun mk_local_access X = Const (@{const_name "Fun.comp"}, dummyT) 
                            $ Const (@{const_name "List.list.hd"}, dummyT) $ X
  in
    fun app_sigma db tm ctxt = case tm of
        Const(name, _) => if StateMgt_core.is_global_program_variable name (Proof_Context.theory_of ctxt) 
                          then tm $ (Bound db) (* lambda lifting *)
                          else if StateMgt_core.is_local_program_variable name (Proof_Context.theory_of ctxt) 
                               then (mk_local_access tm) $ (Bound db) (* lambda lifting local *)
                               else tm              (* no lifting *)
      | Free _ => tm
      | Var _ => tm
      | Bound n => if n > db then Bound(n + 1) else Bound n 
      | Abs (x, ty, tm') => Abs(x, ty, app_sigma (db+1) tm' ctxt)
      | t1 $ t2 => (app_sigma db t1 ctxt) $ (app_sigma db t2 ctxt)

    fun scope_var name =
      Proof_Context.theory_of
      #> (fn thy =>
            if StateMgt_core.is_global_program_variable name thy then SOME true
            else if StateMgt_core.is_local_program_variable name thy then SOME false
            else NONE)

    fun assign_update var = var ^ Record.updateN

    fun transform_term0 abs scope_var tm =
      case tm of
         Const (@{const_name "Clean.syntax_assign"}, _)
         $ (t1 as Const ("_type_constraint_", _) $ Const (name, ty))
         $ t2 =>
            Const ( case scope_var name of
                      SOME true => @{const_name "assign_global"}
                    | SOME false => @{const_name "assign_local"}
                    | NONE => raise TERM ("mk_assign", [t1])
                  , dummyT)
            $ Const(assign_update name, ty)
            $ abs t2
       | _ => abs tm

    fun transform_term ctxt sty =
      transform_term0
        (fn tm => Abs ("σ", sty, app_sigma 0 tm ctxt))
        (fn name => scope_var name ctxt)

    fun transform_term' ctxt = transform_term ctxt dummyT

    fun string_tr ctxt content args =
      let fun err () = raise TERM ("string_tr", args)
      in
        (case args of
          [(Const (@{syntax_const "_constrain"}, _)) $ (Free (s, _)) $ p] =>
            (case Term_Position.decode_position p of
              SOME (pos, _) => Symbol_Pos.implode (content (s, pos))
                            |> Syntax.parse_term ctxt
                            |> transform_term ctxt (StateMgt_core.get_state_type ctxt)
                            |> Syntax.check_term ctxt
            | NONE => err ())
        | _ => err ())
      end
  end
end

syntax "_cartouche_string" :: "cartouche_position  string"  ("_")

parse_translation [(@{syntax_const "_cartouche_string"},
    (fn ctxt => Clean_Syntax_Lift.string_tr ctxt (Symbol_Pos.cartouche_content o Symbol_Pos.explode)))]

section‹Support for (direct recursive) Clean Function Specifications ›

text‹Based on the machinery for the State-Management and  implicitly cooperating with the 
cartouches for assignment syntax, the function-specification function_spec-package coordinates:
 the parsing and type-checking of parameters,
 the parsing and type-checking of pre and post conditions in MOAL notation
  (using λ›-lifting cartouches and implicit reference to parameters, pre and post states),
 the parsing local variable section with the local-variable space generation,
 the parsing of the body in this extended variable space,
 and optionally the support of measures for recursion proofs.

The reader interested in details is referred to the 🗏‹../examples/Quicksort_concept.thy›-example,
accompanying this distribution.
›

definition old :: "'a  'a" where "old x = x"


ML‹ 
›

ML structure Function_Specification_Parser  = 
  struct

    type funct_spec_src = {    
        binding:  binding,                         (* name *)
        params: (binding*string) list,             (* parameters and their type*)
        ret_type: string,                          (* return type; default unit *)
        locals: (binding*string*mixfix)list,       (* local variables *)
        pre_src: string,                           (* precondition src *)
        post_src: string,                          (* postcondition src *)
        variant_src: string option,                       (* variant src *)
        body_src: string * Position.T              (* body src *)
      }

    type funct_spec_sem = {    
        params: (binding*typ) list,                (* parameters and their type*)
        ret_ty: typ,                               (* return type *)
        pre: term,                                 (* precondition  *)
        post: term,                                (* postcondition  *)
        variant: term option                       (* variant  *)
      }


    val parse_arg_decl = Parse.binding -- (Parse.$$$ "::" |-- Parse.typ)

    val parse_param_decls = Args.parens (Parse.enum "," parse_arg_decl)
      
    val parse_returns_clause = Scan.optional (keywordreturns |--  Parse.typ) "unit"
 
    val locals_clause = (Scan.optional ( keywordlocal_vars 
                                        -- (Scan.repeat1 Parse.const_binding)) ("", []))
    
    val parse_proc_spec = (
          Parse.binding 
       -- parse_param_decls
       -- parse_returns_clause
       --| keywordpre             -- Parse.term 
       --| keywordpost            -- Parse.term 
       -- (Scan.option  ( keywordvariant |-- Parse.term))
       -- (Scan.optional( keywordlocal_vars |-- (Scan.repeat1 Parse.const_binding))([]))
       --| keyworddefines         -- (Parse.position (Parse.term)) 
      ) >> (fn ((((((((binding,params),ret_ty),pre_src),post_src),variant_src),locals)),body_src) => 
        {
          binding = binding, 
          params=params, 
          ret_type=ret_ty, 
          pre_src=pre_src, 
          post_src=post_src, 
          variant_src=variant_src,
          locals=locals,
          body_src=body_src} : funct_spec_src
        )

   fun read_params params ctxt =
     let
       val Ts = Syntax.read_typs ctxt (map snd params);
     in (Ts, fold Variable.declare_typ Ts ctxt) end;
   
   fun read_result ret_ty ctxt = 
          let val [ty] = Syntax.read_typs ctxt [ret_ty]
              val ctxt' = Variable.declare_typ ty ctxt           
          in  (ty, ctxt') end

   fun read_function_spec ({ params, ret_type, variant_src, ...} : funct_spec_src) ctxt =
       let val (params_Ts, ctxt') = read_params params ctxt
           val (rty, ctxt'') = read_result ret_type ctxt' 
           val variant = Option.map (Syntax.read_term ctxt'')  variant_src
       in ({params = (params, params_Ts), ret_ty = rty,variant = variant},ctxt'') end 


   fun check_absence_old term = 
            let fun test (s,ty) = if s = @{const_name "old"} andalso fst (dest_Type ty) = "fun"
                                  then error("the old notation is not allowed here!")  
                                  else false
            in  exists_Const test term end
   
   fun transform_old sty term = 
       let fun  transform_old0 (Const(@{const_name "old"}, Type ("fun", [_,_])) $ term ) 
                              = (case term of
                                  (Const(s,ty) $ Bound x) =>  (Const(s,ty) $ Bound (x+1))
                                | _ => error("illegal application of the old notation."))
               |transform_old0 (t1 $ t2) = transform_old0 t1 $ transform_old0 t2
               |transform_old0 (Abs(s,ty,term)) = Abs(s,ty,transform_old0 term) 
               |transform_old0 term = term
       in  Abs(pre", sty, transform_old0 term) end
   
   fun define_cond binding f_sty transform_old src_suff check_absence_old params src ctxt = 
       let val src' = case transform_old (Syntax.read_term ctxt src) of 
                        Abs(nn, sty_pre, term) => mk_pat_tupleabs (map (apsnd #2) params) (Abs(nn,sty_pre(* sty root ! !*),term))
                      | _ => error ("define abstraction for result" ^ Position.here )
           val bdg = Binding.suffix_name src_suff binding
           val _ = check_absence_old src'
           val eq =  mk_meta_eq(Free(Binding.name_of bdg, HOLogic.mk_tupleT(map (#2 o #2) params) --> f_sty HOLogic.boolT),src')
           val args = (SOME(bdg,NONE,NoSyn), (Binding.empty_atts,eq),[],[]) 
       in  StateMgt.cmd args true ctxt end

   fun define_precond binding sty =
     define_cond binding (fn boolT => sty --> boolT) I "_pre" check_absence_old

   fun define_postcond binding rty sty =
     define_cond binding (fn boolT => sty --> sty --> rty --> boolT) (transform_old sty) "_post" I

   fun define_body_core binding args_ty sty params body =
       let val bdg_core = Binding.suffix_name "_core" binding
           val bdg_core_name = Binding.name_of bdg_core

           val umty = args_ty --> StateMgt.MON_SE_T @{typ "unit"} sty

           val eq = mk_meta_eq(Free (bdg_core_name, umty),mk_pat_tupleabs(map(apsnd #2)params) body)
           val args_core =(SOME (bdg_core, SOME umty, NoSyn), (Binding.empty_atts, eq), [], [])

       in StateMgt.cmd args_core true
       end 
 
   fun define_body_main {recursive = x:bool} binding rty sty params variant_src _ ctxt = 
       let val push_name = StateMgt.mk_push_name (StateMgt.mk_local_state_name binding)
           val pop_name = StateMgt.mk_pop_name (StateMgt.mk_local_state_name binding)
           val bdg_core = Binding.suffix_name "_core" binding
           val bdg_core_name = Binding.name_of bdg_core
           val bdg_rec_name = Binding.name_of(Binding.suffix_name "_rec" binding)
           val bdg_ord_name = Binding.name_of(Binding.suffix_name "_order" binding)

           val args_ty = HOLogic.mk_tupleT (map (#2 o #2) params)
           val params' = map (apsnd #2) params
           val rmty = StateMgt_core.MON_SE_T rty sty 

           val umty = StateMgt.MON_SE_T @{typ "unit"} sty
           val argsProdT = HOLogic.mk_prodT(args_ty,args_ty)
           val argsRelSet = HOLogic.mk_setT argsProdT
           val measure_term = case variant_src of
                                 NONE => Free(bdg_ord_name,args_ty --> HOLogic.natT)
                               | SOME str => (Syntax.read_term ctxt str |> mk_pat_tupleabs params')
           val measure =  Const(@{const_name "Wellfounded.measure"}, (args_ty --> HOLogic.natT)
                                                                     --> argsRelSet )
                          $ measure_term
           val lhs_main = if x andalso is_none variant_src
                          then Free(Binding.name_of binding, (args_ty --> HOLogic.natT)
                                                                       --> args_ty --> rmty) $
                                         Free(bdg_ord_name, args_ty --> HOLogic.natT)
                          else Free(Binding.name_of binding, args_ty --> rmty)
           val rhs_main = mk_pat_tupleabs params'
                          (Const(@{const_name "Clean.blockC"}, umty --> umty  --> rmty --> rmty)
                          $ Const(read_constname ctxt (Binding.name_of push_name),umty)
                          $ (Const(read_constname ctxt bdg_core_name, args_ty --> umty)  
                             $ HOLogic.mk_tuple (map Free params'))
                          $ Const(read_constname ctxt (Binding.name_of pop_name),rmty))
           val rhs_main_rec = wfrecT 
                              measure 
                              (Abs(bdg_rec_name, (args_ty --> umty) , 
                                   mk_pat_tupleabs params'
                                   (Const(@{const_name "Clean.blockC"}, umty-->umty-->rmty-->rmty)
                                   $ Const(read_constname ctxt (Binding.name_of push_name),umty)
                                   $ (Const(read_constname ctxt bdg_core_name,
                                            (args_ty --> umty) --> args_ty --> umty)  
                                      $ (Bound (length params))
                                      $ HOLogic.mk_tuple (map Free params'))
                                   $ Const(read_constname ctxt (Binding.name_of pop_name),rmty))))
           val eq_main = mk_meta_eq(lhs_main, if x then rhs_main_rec else rhs_main )
           val args_main = (SOME(binding,NONE,NoSyn), (Binding.empty_atts,eq_main),[],[]) 
       in  ctxt |> StateMgt.cmd args_main true 
       end 


   fun checkNsem_function_spec {recursive = false} ({variant_src=SOME _, ...}) _ = 
                               error "No measure required in non-recursive call"
      |checkNsem_function_spec (isrec as {recursive = _:bool}) 
                               (args as {binding, ret_type, variant_src, locals, body_src, pre_src, post_src, ...} : funct_spec_src)
                               thy =
       let val (theory_map, thy') =
             Named_Target.theory_map_result
               (K (fn f => Named_Target.theory_map o f))
               (read_function_spec args
               #> uncurry (fn {params=(params, Ts),ret_ty,variant = _} =>
                            pair (fn f =>
                                  Proof_Context.add_fixes (map2 (fn (b, _) => fn T => (b, SOME T, NoSyn)) params Ts)
                                    (* this declares the parameters of a function specification
                                       as Free variables (overrides a possible constant declaration)
                                       and assigns the declared type to them *)
                                  #> uncurry (fn params' => f (@{map 3} (fn b' => fn (b, _) => fn T => (b',(b,T))) params' params Ts) ret_ty))))
                thy
       in  thy' |> theory_map
                     let val sty_old = StateMgt_core.get_state_type_global thy'
                     in fn params => fn ret_ty =>
                         define_precond binding sty_old params pre_src
                      #> define_postcond binding ret_ty sty_old params post_src end
                |> StateMgt.new_state_record false ((([],binding), SOME ret_type),locals)
                |> theory_map
                         (fn params => fn ret_ty => fn ctxt => 
                          let val sty = StateMgt_core.get_state_type ctxt
                              val args_ty = HOLogic.mk_tupleT (map (#2 o #2) params)
                              val mon_se_ty = StateMgt_core.MON_SE_T ret_ty sty
                              val ctxt' =
                                if #recursive isrec then
                                  Proof_Context.add_fixes 
                                    [(binding, SOME (args_ty --> mon_se_ty), NoSyn)] ctxt |> #2
                                else
                                  ctxt
                              val body = Syntax.read_term ctxt' (fst body_src)
                          in  ctxt' |> define_body_core binding args_ty sty params body
                          end)
                |> theory_map
                         (fn params => fn ret_ty => fn ctxt => 
                          let val sty = StateMgt_core.get_state_type ctxt
                              val body = Syntax.read_term ctxt (fst body_src)
                          in  ctxt |> define_body_main isrec binding ret_ty sty params variant_src body
                          end)
        end

  
   val _ =
     Outer_Syntax.command 
         command_keywordfunction_spec   
         "define Clean function specification"
         (parse_proc_spec >> (Toplevel.theory o checkNsem_function_spec {recursive = false}));
   
   val _ =
     Outer_Syntax.command 
         command_keywordrec_function_spec   
         "define recursive Clean function specification"
         (parse_proc_spec >> (Toplevel.theory o checkNsem_function_spec {recursive = true}));
       
  end

section‹The Rest of Clean: Break/Return aware Version of If, While, etc.›

definition if_C :: "[('σ_ext) control_state_ext  bool, 
                      (, ('σ_ext) control_state_ext)MONSE, 
                      (, ('σ_ext) control_state_ext)MONSE]  (, ('σ_ext) control_state_ext)MONSE"
  where   "if_C c E F = (λσ. if exec_stop σ 
                              then Some(undefined, σ)  ― ‹state unchanged, return arbitrary›
                              else if c σ then E σ else F σ)"     

syntax    (xsymbols)
          "_if_SECLEAN" :: "[  bool,('o,)MONSE,('o',)MONSE]  ('o',)MONSE" 
          ("(ifC _ then _ else _fi)" [5,8,8]8)
translations 
          "(ifC cond then T1 else T2 fi)" == "CONST Clean.if_C cond T1 T2"

          
          
definition while_C :: "(('σ_ext) control_state_ext  bool) 
                         (unit, ('σ_ext) control_state_ext)MONSE 
                         (unit, ('σ_ext) control_state_ext)MONSE"
  where   "while_C c B  (λσ. if exec_stop σ then Some((), σ)
                               else ((MonadSE.while_SE (λ σ. ¬exec_stop σ  c σ) B) ;- 
                                     unset_break_status) σ)"
  
syntax    (xsymbols)
          "_while_C" :: "[  bool, (unit, )MONSE]  (unit, )MONSE" 
          ("(whileC _ do _ od)" [8,8]8)
translations 
          "whileC c do b od" == "CONST Clean.while_C c b"

  

end

  
  

Theory Hoare_MonadSE

(******************************************************************************
 * Clean
 *
 * Copyright (c) 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.
 ******************************************************************************)

(*
 * Basic Hoare Calculus for the State Exception Monad 
 *
 * Authors : Burkhart Wolff
 *)

theory Hoare_MonadSE
  imports Symbex_MonadSE
begin
  


section‹Hoare›


definition hoare3 :: "(  bool)  (, )MONSE  (    bool)  bool" ("((1_)/ (_)/ (1_))" 50)
where   "P M Q  (σ. P σ  (case M σ of None => False | Some(x, σ') => Q x σ'))" 

definition hoare3' :: "(  bool)  (, )MONSE  bool" ("((1_)/ (_)/)" 50)
where   "P M   (σ. P σ  (case M σ of None => True | _ => False))" 

subsection‹Basic rules› 
  
lemma skip: " P skipSE λ_. P"
  unfolding hoare3_def skipSE_def unit_SE_def
  by auto
    
lemma fail: "P failSE "
  unfolding hoare3'_def fail_SE_def unit_SE_def by auto

lemma assert: "P assertSE P λ _ _. True"    
  unfolding hoare3_def assert_SE_def unit_SE_def
  by auto

lemma assert_conseq: "Collect P  Collect Q  P assertSE Q λ _ _. True"    
  unfolding hoare3_def assert_SE_def unit_SE_def
  by auto

lemma assume_conseq: 
  assumes " σ. Q σ"
  shows   "P assumeSE Q λ _ . Q"    
  unfolding hoare3_def assume_SE_def unit_SE_def
  apply (auto simp : someI2)
  using assms by auto

    
text ‹assignment missing in the calculus because this is viewed as a state specific  
       operation, definable for concrete instances of @{typ ""}.›  

subsection ‹Generalized and special sequence rules› 
text‹The decisive idea is to factor out the post-condition on the results of @{term M} :›
lemma sequence : 
  "    P M λx σ. xA  Q x σ
    xA. Q x M' x R 
    P x  M; M' x R" 
  unfolding hoare3_def bind_SE_def 
  by(auto,erule_tac x="σ" in allE, auto split: Option.option.split_asm Option.option.split)

lemma sequence_irpt_l : "P M    P x  M; M' x " 
  unfolding hoare3'_def bind_SE_def 
  by(auto,erule_tac x="σ" in allE, auto split: Option.option.split_asm Option.option.split)

lemma sequence_irpt_r : "P M λx σ. xA  Q x σ  xA. Q x M' x    P x  M; M' x " 
  unfolding hoare3'_def hoare3_def bind_SE_def 
  by(auto,erule_tac x="σ" in allE, auto split: Option.option.split_asm Option.option.split)
        
lemma sequence' : "P M λ_. Q   Q M' R  P M;- M' R"     
  unfolding hoare3_def hoare3_def bind_SE_def bind_SE'_def
  by(auto,erule_tac x="σ" in allE, auto split: Option.option.split_asm Option.option.split)

lemma sequence_irpt_l' : "P M   P M;- M' " 
  unfolding hoare3'_def bind_SE_def bind_SE'_def
  by(auto,erule_tac x="σ" in allE, auto split: Option.option.split_asm Option.option.split)
    
lemma sequence_irpt_r' : "P M λ_. Q   Q M'   P M;- M' " 
  unfolding hoare3'_def hoare3_def bind_SE_def bind_SE'_def
  by(auto,erule_tac x="σ" in allE, auto split: Option.option.split_asm Option.option.split)

subsection‹Generalized and special consequence rules›  
lemma consequence : 
  "    Collect P  Collect P'
    P' M λx σ. xA  Q' x σ 
     xA. Collect(Q' x)  Collect (Q x)
    P M λx σ. xA  Q x σ"
  unfolding hoare3_def bind_SE_def 
  by(auto,erule_tac x="σ" in allE,auto split: Option.option.split_asm Option.option.split)

lemma consequence_unit : 
  assumes "( σ. P σ  P' σ)" 
   and  "P' M λx::unit. λ σ.  Q' σ" 
   and  " ( σ. Q'  σ  Q  σ)" 
   shows "P M λx σ. Q σ"
proof -
  have * : "(λx σ. Q  σ) = (λx::unit. λ σ. xUNIV  Q  σ) " by auto
  show ?thesis
    apply(subst *)
    apply(rule_tac  P' = "P'" and Q' = "%_. Q'" in consequence)
    apply (simp add: Collect_mono assms(1))
    using assms(2) apply auto[1]
    by (simp add: Collect_mono assms(3))
qed


lemma consequence_irpt : 
  "    Collect P  Collect P'
    P' M 
    P  M "
  unfolding hoare3_def hoare3'_def bind_SE_def  
  by(auto)

lemma consequence_mt_swap : 
  "(λ_. False M ) = (λ_. False M P)" 
  unfolding hoare3_def hoare3'_def bind_SE_def 
  by auto
    
subsection‹Condition rules› 
  
lemma cond : 
  "    λσ. P σ  cond σ M Q
    λσ. P σ  ¬ cond σ M' Q  
    PifSE cond then M else M' fiQ"
  unfolding hoare3_def hoare3'_def bind_SE_def if_SE_def
  by auto
  
lemma cond_irpt : 
  "    λσ. P σ  cond σ M 
    λσ. P σ  ¬ cond σ M'   
    PifSE cond then M else M' fi "
  unfolding hoare3_def hoare3'_def bind_SE_def if_SE_def
  by auto

text‹ Note that the other four combinations can be directly derived via
       the @{thm consequence_mt_swap} rule.›
  
subsection‹While rules› 
text‹The only non-trivial proof is, of course, the while loop rule. Note
that non-terminating loops were mapped to @{term None} following the principle
that our monadic state-transformers represent partial functions in the mathematical 
sense.›
  
lemma while :
  assumes  * : "λσ. cond σ  P σ  M λ_. P"
  and measure: "σ. cond σ  P σ  M σ  None  f(snd(the(M σ))) < ((f σ)::nat) "
  shows        "PwhileSE cond do M od λ_ σ. ¬cond σ  P σ"

unfolding hoare3_def hoare3'_def bind_SE_def if_SE_def
proof auto
  have * : "n.  σ. P σ  f σ  n   
                     (case (whileSE cond do M od) σ of 
                          None  False
                        | Some (x, σ')  ¬ cond σ'  P σ')" (is "n. ?P n")
     proof (rule allI, rename_tac n, induct_tac n)
       fix n show "?P 0"
         apply(auto)
         apply(subst while_SE_unfold)
         by (metis (no_types, lifting) gr_implies_not0 if_SE_def  measure option.case_eq_if 
                     option.sel option.simps(3) prod.sel(2) split_def unit_SE_def)
     next
       fix n  show " ?P n  ?P (Suc n)"
        apply(auto,subst while_SE_unfold)
         apply(case_tac "¬cond σ")
        apply (simp add: if_SE_def unit_SE_def)
        apply(simp add: if_SE_def)
        apply(case_tac "M σ = None")
         using measure apply blast
        proof (auto simp: bind_SE'_def bind_SE_def)
          fix σ σ'
          assume 1 : "cond σ"
            and  2 : "M σ = Some ((), σ')"
            and  3 : " P σ"
            and  4 : " f σ  Suc n"
            and  hyp : "?P n"
          have 5 : "P σ'" 
            by (metis (no_types, lifting) * 1 2 3 case_prodD hoare3_def option.simps(5))
          have 6 : "snd(the(M σ)) = σ'" 
            by (simp add: 2)
          have 7 : "cond σ'  f σ'  n" 
            using 1 3 4 6 leD measure by auto
          show   "case (whileSE cond do M od) σ' of None  False
                                                  | Some (xa, σ')  ¬ cond σ'  P σ'"
          using 1 3 4 5 6 hyp measure by auto
        qed
      qed
  show "σ. P σ 
         case (whileSE cond do M od) σ of None  False
         | Some (x, σ')  ¬ cond σ'  P σ'"
  using "*" by blast
qed
  

lemma while_irpt :
  assumes  * : "λσ. cond σ  P σ  M λ_. P  λσ. cond σ  P σ  M  "
  and measure: "σ. cond σ  P σ  M σ = None  f(snd(the(M σ))) < ((f σ)::nat)"
  and enabled: "σ. P σ  cond σ"
  shows        "PwhileSE cond do M od "
unfolding hoare3_def hoare3'_def bind_SE_def if_SE_def
proof auto
  have * : "n.  σ. P σ  f σ  n   
                     (case (whileSE cond do M od) σ of None  True | Some a  False)" 
            (is "n. ?P n ")
    proof (rule allI, rename_tac n, induct_tac n)
      fix n 
         have 1 : "σ. P σ  cond σ" 
          by (simp add: enabled * )
      show "?P 0 "
        apply(auto,frule 1)
        by (metis assms(2) bind_SE'_def bind_SE_def gr_implies_not0 if_SE_def option.case(1) 
                           option.case_eq_if  while_SE_unfold)
    next
      fix k n 
      assume hyp : "?P n"
         have 1 : "σ. P σ  cond σ" 
          by (simp add: enabled * )
      show "?P (Suc n) "
        apply(auto, frule 1)
        apply(subst while_SE_unfold, auto simp: if_SE_def)
      proof(insert *,simp_all add: hoare3_def hoare3'_def, erule disjE)
        fix σ
        assume "P σ"
         and   "f σ  Suc n"
         and   "cond σ"
         and   ** : "σ. cond σ  P σ  (case M σ of None  False | Some (x, σ')  P σ')"
         obtain "(case M σ of None  False | Some (x, σ')  P σ')" 
               by (simp add: "**" P σ cond σ)
        then 
        show "case (M ;- (whileSE cond do M od)) σ of None  True | Some a  False"
             apply(case_tac "M σ", auto, rename_tac σ', simp add: bind_SE'_def bind_SE_def)
             proof - 
               fix σ' 
               assume "P σ'"
                and "M σ = Some ((), σ')"
                have "cond σ'"  by (simp add: P σ' enabled)
                have "f σ'  n" 
                  using M σ = Some ((), σ') P σ cond σ f σ  Suc n measure by fastforce   
               show "case (whileSE cond do M od) σ' of None  True | Some a  False"
                  using hyp  by (simp add: P σ' f σ'  n)
              qed
      next
        fix σ
        assume "P σ"
         and   "f σ  Suc n"
         and   "cond σ"  
         and * : "σ. cond σ  P σ  (case M σ of None  True | Some a  False)"
        obtain ** : "(case M σ of None  True | Some a  False)" 
          by (simp add: "*" P σ cond σ)
        have "M σ = None" 
          by (simp add: "**" option.disc_eq_case(1))
        show "case (M ;- (whileSE cond do M od)) σ of None  True | Some a  False"          
          by (simp add: M σ = None› bind_SE'_def bind_SE_def)
      qed      
    qed
show "σ. P σ  case (whileSE cond do M od) σ of None  True | Some a  False" using * by blast
qed
  

subsection‹Experimental Alternative Definitions (Transformer-Style Rely-Guarantee)›

definition  hoare1 :: "(  bool)  (, )MONSE  (    bool)  bool" ("1 ({(1_)}/ (_)/ {(1_)})" 50)
where  "(1{P} M {Q} ) = (σ. σ  (_   assumeSE P ; x   M; assertSE (Q x)))"

(* Problem: Severe Deviation for the case of an unsatisfyabke precondition *)

definition  hoare2 :: "(  bool)  (, )MONSE  (    bool)  bool" ("2 ({(1_)}/ (_)/ {(1_)})" 50)
where  "(2{P} M {Q} ) = (σ. P σ  (σ   (x  M; assertSE (Q x))))"

  
end
  

Theory Hoare_Clean

(******************************************************************************
 * Clean
 *
 * Copyright (c) 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.
 ******************************************************************************)

(*
 * A Hoare Calculus for Clean
 *
 * Authors : Burkhart Wolff
 *)

theory Hoare_Clean
  imports Hoare_MonadSE
          Clean
begin


subsection‹Clean Control Rules›

lemma break1: 
  "λσ.  P (σ  break_status := True )  break λr σ.  P σ  break_status σ "
  unfolding    hoare3_def break_def unit_SE_def by auto

lemma unset_break1: 
  "λσ.  P (σ  break_status := False )  unset_break_status λr σ. P σ  ¬ break_status σ "
  unfolding    hoare3_def unset_break_status_def unit_SE_def by auto

lemma set_return1: 
  "λσ.  P (σ  return_status := True )  set_return_status λr σ. P σ  return_status σ "
  unfolding    hoare3_def set_return_status_def unit_SE_def by auto

lemma unset_return1: 
  "λσ.  P (σ  return_status := False )  unset_return_status λr σ. P σ  ¬return_status σ "
  unfolding    hoare3_def unset_return_status_def unit_SE_def by auto


subsection‹Clean Skip Rules›

lemma assign_global_skip:
"λσ.   exec_stop σ  P σ   assign_global upd rhs  λr σ. exec_stop σ  P σ "
  unfolding    hoare3_def skipSE_def unit_SE_def
  by (simp add: assign_def assign_global_def)

lemma assign_local_skip:
"λσ.   exec_stop σ  P σ  assign_local upd rhs  λr σ. exec_stop σ  P σ "
  unfolding    hoare3_def skipSE_def unit_SE_def
  by (simp add: assign_def assign_local_def)

lemma return_skip:
"λσ.  exec_stop σ  P σ  returnC upd rhs λr σ. exec_stop σ  P σ "
  unfolding hoare3_def returnC_def unit_SE_def assign_local_def assign_def bind_SE'_def bind_SE_def
  by auto

lemma assign_clean_skip:
"λσ.   exec_stop σ  P σ   assign tr  λr σ. exec_stop σ  P σ "
  unfolding    hoare3_def skipSE_def unit_SE_def
  by (simp add: assign_def assign_def)

lemma if_clean_skip:
"λσ.   exec_stop σ  P σ   ifC C then E else F fi λr σ. exec_stop σ  P σ "
  unfolding    hoare3_def skipSE_def unit_SE_def if_SE_def
  by (simp add: if_C_def)

lemma while_clean_skip:
"λσ.   exec_stop σ  P σ   whileC cond do body od  λr σ. exec_stop σ  P σ "
  unfolding    hoare3_def skipSE_def unit_SE_def while_C_def 
  by auto

lemma if_opcall_skip:
"λσ.   exec_stop σ  P σ (callC M A1) λr σ. exec_stop σ  P σ"
  unfolding    hoare3_def skipSE_def unit_SE_def callC_def
  by simp

lemma if_funcall_skip:
"λσ. exec_stop σ  P σ(ptmp  callC fun E ; assign_local upd (λσ. ptmp)) λr σ. exec_stop σ  P σ"
  unfolding    hoare3_def skipSE_def unit_SE_def callC_def assign_local_def assign_def
  by (simp add: bind_SE_def)

lemma if_funcall_skip':
"λσ. exec_stop σ  P σ (ptmp  callC fun E ; assign_global upd (λσ. ptmp)) λr σ. exec_stop σ  P σ "
  unfolding    hoare3_def skipSE_def unit_SE_def callC_def assign_global_def assign_def
  by (simp add: bind_SE_def)




subsection‹Clean Assign Rules›


lemma assign_global:
  assumes * : " upd"
  shows "λσ. ¬exec_stop σ  P (upd (λ_. rhs σ) σ)  
         assign_global upd rhs 
         λr σ. ¬exec_stop σ  P σ "
  unfolding    hoare3_def skipSE_def unit_SE_def assign_global_def  assign_def
  by(auto simp: assms)

lemma assign_local:
  assumes * : " (upd  map_hd)"
  shows "λσ.  ¬ exec_stop σ  P ((upd  map_hd) (λ_. rhs σ) σ)   
          assign_local upd rhs  
         λr σ. ¬ exec_stop σ  P σ "
  unfolding    hoare3_def skipSE_def unit_SE_def assign_local_def  assign_def
  using assms exec_stop_vs_control_independence by fastforce

lemma return_assign:
  assumes * : " (upd  map_hd)"
  shows "λ σ. ¬ exec_stop σ  P ((upd  map_hd) (λ_. rhs σ) (σ  return_status := True )) 
          returnC upd rhs
         λr σ. P σ  return_status σ "
  unfolding returnC_def hoare3_def skipSE_def unit_SE_def assign_local_def assign_def 
            set_return_status_def bind_SE'_def bind_SE_def 
proof (auto)
  fix σ :: "'b control_state_scheme"
    assume a1: "P (upd (map_hd (λ_. rhs σ)) (σreturn_status := True))"
    assume "¬ exec_stop σ"
    show "P (upd (map_hd (λ_. rhs σ)) σreturn_status := True)"
      using a1 assms exec_stop_vs_control_independence' by fastforce
  qed
  (* do we need independence of rhs ? Not really. 'Normal' programs would never
     be control-state dependent, and 'artificial' ones would still be correct ...*)


subsection‹Clean Construct Rules›

lemma cond_clean : 
  "    λσ. ¬ exec_stop σ  P σ  cond σ M Q
    λσ. ¬ exec_stop σ  P σ  ¬ cond σ M' Q  
    λσ. ¬ exec_stop σ  P σ ifC cond then M else M' fiQ"
  unfolding hoare3_def hoare3'_def bind_SE_def if_SE_def
  by (simp add: if_C_def)


text‹There is a particular difficulty with a verification of (terminating) while rules
in a Hoare-logic for a language involving break. The first is, that break is not used
in the toplevel of a body of a loop (there might be breaks inside an inner loop, though).
This scheme is covered by the rule below, which is a generalisation of the classical 
while loop (as presented by @{thm while}.›


lemma while_clean_no_break :
  assumes  * : "λσ. ¬ break_status σ  cond σ  P σ  M λ_. λσ.  ¬ break_status σ  P σ "
  and measure: "σ. ¬ exec_stop σ  cond σ  P σ 
                     M σ  None  f(snd(the(M σ))) < ((f σ)::nat) "
               (is "σ. _  cond σ  P σ  ?decrease σ")
  shows        "λσ. ¬ exec_stop σ  P σ 
                whileC cond do M od 
                λ_ σ. (return_status σ  ¬ cond σ)  ¬ break_status σ  P σ"
                (is "?pre whileC cond do M od λ_ σ. ?post1 σ  ?post2 σ")  
  unfolding while_C_def hoare3_def hoare3'_def
  proof (simp add: hoare3_def[symmetric],rule sequence') 
    show "?pre 
          whileSE (λσ. ¬ exec_stop σ  cond σ) do M od
          λ_ σ. ¬ (¬ exec_stop σ  cond σ)  ¬ break_status σ  P σ"
          (is "?pre whileSE ?cond' do M od λ_ σ. ¬ ( ?cond' σ)  ?post2 σ")
      proof (rule consequence_unit) 
         fix σ show " ?pre σ  ?post2 σ"  using exec_stop1 by blast
      next
         show "?post2whileSE ?cond' do M odλx σ. ¬(?cond' σ)  ?post2 σ"
         proof (rule_tac f = "f" in while, rule consequence_unit)
           fix σ show "?cond' σ  ?post2 σ  ¬break_status σ  cond σ  P σ" by simp
         next
           show "λσ. ¬ break_status σ  cond σ  P σ M λx σ. ?post2 σ" using "*" by blast
         next 
           fix σ  show "?post2 σ  ?post2 σ" by blast
         next 
           show "σ.?cond' σ  ?post2 σ  ?decrease σ" using measure by blast
         qed
      next
         fix σ show " ¬?cond' σ  ?post2 σ  ¬?cond' σ  ?post2 σ"  by blast
      qed
  next
    show "λσ. ¬ (¬ exec_stop σ  cond σ)  ?post2 σ unset_break_status
          λ_ σ'. (return_status σ'  ¬ cond σ')  ?post2 σ'"
         (is "λσ. ¬ (?cond'' σ)  ?post2 σ unset_break_status λ_ σ'. ?post3 σ'  ?post2 σ' ")
      proof (rule consequence_unit) 
        fix σ  
        show "¬ ?cond'' σ  ?post2 σ  (λσ. P σ  ?post3 σ) (σbreak_status := False)"
              by (metis (full_types) exec_stop_def surjective update_convs(1))
      next
        show "λσ. (λσ. P σ  ?post3 σ) (σbreak_status := False)
              unset_break_status 
              λx σ. ?post3 σ  ¬ break_status σ  P σ"    
             apply(subst (2) conj_commute,subst conj_assoc,subst (2) conj_commute)
             by(rule unset_break1)
      next 
         fix σ show  "?post3 σ  ?post2 σ  ?post3 σ  ?post2 σ"  by simp
      qed
qed 


text‹In the following we present a version allowing a break inside the body, which implies that the 
     invariant has been established at the break-point and the condition is irrelevant. 
     A return may occur, but the @{term "break_status"} is guaranteed to be true
     after leaving the loop.›



lemma while_clean':
  assumes  M_inv   : "λσ. ¬ exec_stop σ  cond σ  P σ  M λ_. P"
  and cond_idpc    : "x σ.  (cond (σbreak_status := x)) = cond σ "
  and inv_idpc     : "x σ.  (P (σbreak_status := x)) = P σ "
  and f_is_measure : "σ. ¬ exec_stop σ  cond σ  P σ  
                       M σ  None  f(snd(the(M σ))) < ((f σ)::nat) "
shows    "λσ. ¬ exec_stop σ  P σ 
          whileC cond do M od 
          λ_ σ.  ¬ break_status σ  P σ"
  unfolding while_C_def hoare3_def hoare3'_def
  proof (simp add: hoare3_def[symmetric], rule sequence')
    show "λσ. ¬ exec_stop σ  P σ 
            whileSE (λσ. ¬ exec_stop σ  cond σ) do M od
          λ_ σ. P (σbreak_status := False)"
          apply(rule consequence_unit, rule impI, erule conjunct2)
          apply(rule_tac f = "f" in while)
          using M_inv f_is_measure inv_idpc by auto
  next
    show "λσ. P (σbreak_status := False) unset_break_status 
          λx σ. ¬ break_status σ  P σ"
          apply(subst conj_commute)
          by(rule  Hoare_Clean.unset_break1)
  qed


text‹Consequence and Sequence rules where inherited from the underlying Hoare-Monad theory.›


end





Theory Clean_Symbex

(******************************************************************************
 * Clean
 *
 * Copyright (c) 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.
 ******************************************************************************)

theory Clean_Symbex
  imports Clean
begin


section‹Clean Symbolic Execution Rules ›


subsection‹Basic NOP - Symbolic Execution Rules.  ›

text‹  As they are equalities, they can also
be used as program optimization rules. ›

lemma non_exec_assign  : 
assumes "¬ exec_stop σ"
shows "(σ  ( _  assign f; M)) = ((f σ)   M)"
by (simp add: assign_def assms exec_bind_SE_success)

lemma non_exec_assign'  : 
assumes "¬ exec_stop σ"
shows "(σ  (assign f;- M)) = ((f σ)   M)"
by (simp add: assign_def assms exec_bind_SE_success bind_SE'_def)

lemma exec_assign  : 
assumes "exec_stop σ"
shows "(σ  ( _  assign f; M)) = (σ  M)"
by (simp add: assign_def assms exec_bind_SE_success)     

lemma exec_assign'  : 
assumes "exec_stop σ"
shows "(σ  (assign f;- M)) = (σ  M)"
by (simp add: assign_def assms exec_bind_SE_success bind_SE'_def)     

subsection‹Assign Execution Rules.  ›

lemma non_exec_assign_global  : 
assumes "¬ exec_stop σ"
shows   "(σ  ( _  assign_global upd rhs; M)) = ((upd (λ_. rhs σ) σ)   M)"
by(simp add: assign_global_def non_exec_assign assms)

lemma non_exec_assign_global'  : 
assumes "¬ exec_stop σ"
shows   "(σ  (assign_global upd rhs;- M)) = ((upd (λ_. rhs σ) σ)   M)"
  by (metis (full_types) assms bind_SE'_def non_exec_assign_global)


lemma exec_assign_global  : 
assumes "exec_stop σ"
shows   "(σ  ( _  assign_global upd rhs; M)) = ( σ   M)"
  by (simp add: assign_global_def assign_def assms exec_bind_SE_success)

lemma exec_assign_global'  : 
assumes "exec_stop σ"
shows   "(σ  (assign_global upd rhs;- M)) = ( σ   M)"
  by (simp add: assign_global_def assign_def assms exec_bind_SE_success bind_SE'_def)

lemma non_exec_assign_local  : 
assumes "¬ exec_stop σ"
shows   "(σ  ( _  assign_local upd rhs; M)) = ((upd (map_hd (λ_. rhs σ)) σ)   M)"
  by(simp add: assign_local_def non_exec_assign assms)

lemma non_exec_assign_local'  : 
assumes "¬ exec_stop σ"
shows   "(σ  (assign_local upd rhs;- M)) = ((upd (map_hd (λ_. rhs σ)) σ)   M)"
  by (metis assms bind_SE'_def non_exec_assign_local)

lemmas non_exec_assign_localD'= non_exec_assign[THEN iffD1]

lemma exec_assign_local  : 
assumes "exec_stop σ"
shows   "(σ  ( _  assign_local upd rhs; M)) = ( σ   M)"
  by (simp add: assign_local_def assign_def assms exec_bind_SE_success)

lemma exec_assign_local'  : 
assumes "exec_stop σ"
shows   "(σ  ( assign_local upd rhs;- M)) = ( σ   M)" 
  unfolding assign_local_def assign_def 
  by (simp add: assms exec_bind_SE_success2)

lemmas exec_assignD = exec_assign[THEN iffD1]
thm exec_assignD

lemmas exec_assignD' = exec_assign'[THEN iffD1]
thm exec_assignD'

lemmas exec_assign_globalD =  exec_assign_global[THEN iffD1]

lemmas exec_assign_globalD' =  exec_assign_global'[THEN iffD1]

lemmas exec_assign_localD = exec_assign_local[THEN iffD1]
thm exec_assign_localD

lemmas exec_assign_localD' = exec_assign_local'[THEN iffD1]



subsection‹Basic Call Symbolic Execution Rules.  ›



lemma exec_call_0  : 
assumes "exec_stop σ"
shows   "(σ  ( _  call_0C M; M')) = (σ   M')"
  by (simp add: assms call_0C_def exec_bind_SE_success)

lemma exec_call_0'  : 
assumes "exec_stop σ"
shows   "(σ  (call_0C M;- M')) = (σ   M')"
  by (simp add: assms bind_SE'_def exec_call_0)



lemma exec_call_1  : 
assumes "exec_stop σ"
shows   "(σ  ( x  call_1C M A1; M' x)) = (σ   M' undefined)"
  by (simp add: assms call_1C_def callC_def exec_bind_SE_success)

lemma exec_call_1'  : 
assumes "exec_stop σ"
shows   "(σ  (call_1C M A1;- M')) = (σ   M')"
  by (simp add: assms bind_SE'_def exec_call_1)

lemma exec_call  : 
assumes "exec_stop σ"
shows   "(σ  ( x  callC M A1; M' x)) = (σ   M' undefined)"
  by (simp add: assms callC_def call_1C_def exec_bind_SE_success)

lemma exec_call'  : 
assumes "exec_stop σ"
shows   "(σ  (callC M A1;- M')) = (σ   M')"
  by (metis assms call_1C_def exec_call_1')

lemma exec_call_2  : 
assumes "exec_stop σ"
shows   "(σ  ( _  call_2C M A1 A2; M')) = (σ   M')"
  by (simp add: assms call_2C_def exec_bind_SE_success)

lemma exec_call_2'  : 
assumes "exec_stop σ"
shows   "(σ  (call_2C M A1 A2;- M')) = (σ  M')"
  by (simp add: assms bind_SE'_def exec_call_2)

subsection‹Basic Call Symbolic Execution Rules.  ›

lemma non_exec_call_0  : 
assumes "¬ exec_stop σ"
shows   "(σ  ( _  call_0C M; M')) = (σ  M;- M')"
  by (simp add: assms bind_SE'_def bind_SE_def call_0C_def valid_SE_def)

lemma non_exec_call_0'  : 
assumes "¬ exec_stop σ"
shows   "(σ  call_0C M;- M') = (σ  M;- M')"
  by (simp add: assms bind_SE'_def non_exec_call_0)

lemma non_exec_call_1  : 
assumes "¬ exec_stop σ"
shows   "(σ  ( x  (call_1C M A1); M' x)) = (σ  (x  M (A1 σ); M' x))"
  by (simp add: assms bind_SE'_def callC_def bind_SE_def call_1C_def valid_SE_def)

lemma non_exec_call_1'  : 
assumes "¬ exec_stop σ"
shows   "(σ  call_1C M A1;- M') = (σ   M (A1 σ);- M')"
  by (simp add: assms bind_SE'_def non_exec_call_1)


lemma non_exec_call  : 
assumes "¬ exec_stop σ"
shows   "(σ  ( x  (callC M A1); M' x)) = (σ  (x  M (A1 σ); M' x))"
  by (simp add: assms callC_def bind_SE'_def bind_SE_def call_1C_def valid_SE_def)

lemma non_exec_call'  : 
assumes "¬ exec_stop σ"
shows   "(σ  callC M A1;- M') = (σ   M (A1 σ);- M')"
  by (simp add: assms bind_SE'_def non_exec_call)


lemma non_exec_call_2  : 
assumes "¬ exec_stop σ"
shows   "(σ  ( _  (call_2C M A1 A2); M')) = (σ  M (A1 σ) (A2 σ);- M')"
  by (simp add: assms bind_SE'_def bind_SE_def call_2C_def valid_SE_def)

lemma non_exec_call_2'  : 
assumes "¬ exec_stop σ"
shows   "(σ  call_2C M A1 A2;- M') = (σ   M (A1 σ) (A2 σ);- M')"
  by (simp add: assms bind_SE'_def non_exec_call_2)


subsection‹Conditional.  ›

lemma exec_IfC_IfSE  : 
assumes "¬ exec_stop σ"
shows  " ((ifC P then B1 else B2 fi))σ = ((ifSE P then B1 else B2 fi)) σ "
  unfolding if_SE_def MonadSE.if_SE_def Symbex_MonadSE.valid_SE_def MonadSE.bind_SE'_def
  by (simp add: assms bind_SE_def if_C_def)
    
    
lemma valid_exec_IfC  : 
assumes "¬ exec_stop σ"
shows  "(σ  (ifC P then B1 else B2 fi);-M) = (σ  (ifSE P then B1 else B2 fi);-M)"
  by (meson assms exec_IfC_IfSE valid_bind'_cong)


      
lemma exec_IfC'  : 
assumes "exec_stop σ"
shows  "(σ  (ifC P then B1 else B2 fi);-M) = (σ  M)"    
  unfolding if_SE_def MonadSE.if_SE_def Symbex_MonadSE.valid_SE_def MonadSE.bind_SE'_def bind_SE_def
    by (simp add: assms if_C_def)
    
lemma exec_WhileC'  : 
assumes "exec_stop σ"
shows  "(σ  (whileC P do B1 od);-M) = (σ  M)"    
  unfolding while_C_def MonadSE.if_SE_def Symbex_MonadSE.valid_SE_def MonadSE.bind_SE'_def bind_SE_def
  apply simp using assms by blast    


    
    
lemma ifC_cond_cong : "f σ = g σ  
                           (ifC f then c else d fi) σ = 
                           (ifC g then c else d fi) σ"
  unfolding if_C_def
   by simp 
   
 
subsection‹Break - Rules.  ›

lemma break_assign_skip [simp]: "break ;- assign f = break"
  apply(rule ext)
  unfolding break_def assign_def exec_stop_def bind_SE'_def   bind_SE_def
  by auto



lemma break_if_skip [simp]: "break ;- (ifC b then c else d fi) = break"
  apply(rule ext)
  unfolding break_def assign_def exec_stop_def if_C_def bind_SE'_def   bind_SE_def
  by auto
    
                       
lemma break_while_skip [simp]: "break ;- (whileC b do c od) = break"
  apply(rule ext)
  unfolding while_C_def skipSE_def unit_SE_def bind_SE'_def bind_SE_def break_def exec_stop_def
  by simp

    
lemma unset_break_idem [simp] : 
 "( unset_break_status ;- unset_break_status ;- M) = (unset_break_status ;- M)"
  apply(rule ext)  unfolding unset_break_status_def bind_SE'_def bind_SE_def by auto

lemma return_cancel1_idem [simp] : 
 "( returnC X E ;- assign_global X E' ;- M) = ( returnC X E ;- M)"
  apply(rule ext, rename_tac "σ")  
  unfolding unset_break_status_def bind_SE'_def bind_SE_def
            assign_def returnC_def assign_global_def assign_local_def
  apply(case_tac "exec_stop σ")
  apply auto
  by (simp add: exec_stop_def set_return_status_def)
    
lemma return_cancel2_idem [simp] : 
 "( returnC X E ;- assign_local X E' ;- M) = ( returnC X E ;- M)"
    apply(rule ext, rename_tac "σ")  
  unfolding unset_break_status_def bind_SE'_def bind_SE_def
            assign_def returnC_def assign_global_def assign_local_def
  apply(case_tac "exec_stop σ")
   apply auto
  by (simp add: exec_stop_def set_return_status_def)


subsection‹While.  ›     

lemma whileC_skip [simp]: "(whileC (λ x. False) do c od) = skipSE"
  apply(rule ext)
  unfolding while_C_def skipSE_def unit_SE_def
  apply auto
  unfolding exec_stop_def skipSE_def unset_break_status_def bind_SE'_def unit_SE_def bind_SE_def
  by simp
 

txt‹ Various tactics for various coverage criteria ›

definition while_k :: "nat  (('σ_ext) control_state_ext  bool) 
                         (unit, ('σ_ext) control_state_ext)MONSE 
                         (unit, ('σ_ext) control_state_ext)MONSE"
where     "while_k _  while_C"


text‹Somewhat amazingly, this unfolding lemma crucial for symbolic execution still holds ... 
     Even in the presence of break or return...› 
lemma exec_whileC : 
"(σ  ((whileC b do c od) ;- M)) = 
 (σ  ((ifC b then c ;- ((whileC b do c od) ;- unset_break_status) else skipSE fi)  ;- M))"
proof (cases "exec_stop σ")
  case True
  then show ?thesis 
    by (simp add: True exec_IfC' exec_WhileC')
next
  case False
  then show ?thesis
    proof (cases "¬ b σ")
      case True
      then show ?thesis
        apply(subst valid_bind'_cong)
        using ¬ exec_stop σ apply simp_all
        apply (auto simp: skipSE_def unit_SE_def)
          apply(subst while_C_def, simp)
         apply(subst bind'_cong)
         apply(subst MonadSE.while_SE_unfold)
          apply(subst ifSE_cond_cong [of _ _ "λ_. False"])
          apply simp_all
        apply(subst ifC_cond_cong [of _ _ "λ_. False"], simp add: )
        apply(subst exec_IfC_IfSE,simp_all)
        by (simp add: exec_stop_def unset_break_status_def)
    next
      case False
      have * : "b σ"  using False by auto
      then show ?thesis
           unfolding while_k_def 
           apply(subst  while_C_def)
           apply(subst  if_C_def)
           apply(subst  valid_bind'_cong)
            apply (simp add: ¬ exec_stop σ)
           apply(subst  (2) valid_bind'_cong)
            apply (simp add: ¬ exec_stop σ)
            apply(subst MonadSE.while_SE_unfold)
            apply(subst valid_bind'_cong)
            apply(subst bind'_cong)
             apply(subst ifSE_cond_cong [of _ _ "λ_. True"])
              apply(simp_all add:   ¬ exec_stop σ )
            apply(subst bind_assoc', subst bind_assoc')
            proof(cases "c σ")
              case None
              then show "(σ  c;-((whileSE (λσ. ¬ exec_stop σ  b σ) do c od);-unset_break_status);-M) =
                         (σ  c;-(whileC b do c od) ;- unset_break_status ;- M)"
                by (simp add: bind_SE'_def exec_bind_SE_failure)
            next
              case (Some a)
              then show "(σ  c ;- ((whileSE (λσ. ¬ exec_stop σ  b σ) do c od);-unset_break_status);-M) =
                         (σ  c ;- (whileC b do c od) ;- unset_break_status ;- M)"
                apply(insert c σ = Some a, subst (asm) surjective_pairing[of a])
                apply(subst exec_bind_SE_success2, assumption)
                apply(subst exec_bind_SE_success2, assumption)
                proof(cases "exec_stop (snd a)")
                  case True
                  then show "(snd a ((whileSE (λσ. ¬ exec_stop σ  b σ) do c od);-unset_break_status);-M)=
                             (snd a  (whileC b do c od) ;- unset_break_status ;- M)"
                       by (metis (no_types, lifting) bind_assoc' exec_WhileC' exec_skip if_SE_D2' 
                                                  skipSE_def while_SE_unfold)
                next
                  case False
                  then show "(snd a  ((whileSE(λσ. ¬exec_stop σ  b σ) do c od);-unset_break_status);-M)=
                             (snd a  (whileC b do c od) ;- unset_break_status ;- M)"
                          unfolding  while_C_def
                          by(subst (2) valid_bind'_cong,simp)(simp)
                qed       
            qed  
    qed
qed
(* ... although it is, oh my god, amazingly complex to prove. *)


lemma while_k_SE : "while_C = while_k k"
by (simp only: while_k_def)


corollary exec_while_k : 
"(σ  ((while_k (Suc n) b c) ;- M)) = 
 (σ  ((ifC b then c ;- (while_k n b c) ;- unset_break_status else skipSE fi)  ;- M))"
  by (metis exec_whileC while_k_def)
    

txt‹ Necessary prerequisite: turning ematch and dmatch into a proper Isar Method. ›
(* TODO : this code shoud go to TestGen Method setups *)
MLlocal
fun method_setup b tac =
  Method.setup b
    (Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o K (tac ctxt rules))))
in
val _ =
  Theory.setup (   method_setup @{binding ematch} ematch_tac "fast elimination matching"
                #> method_setup @{binding dmatch} dmatch_tac "fast destruction matching"
                #> method_setup @{binding match} match_tac "resolution based on fast matching")
end

lemmas exec_while_kD = exec_while_k[THEN iffD1]

end

Theory Test_Clean

(******************************************************************************
 * Clean
 *
 * Copyright (c) 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.
 ******************************************************************************)

theory Test_Clean
  imports Clean_Symbex
          "HOL-Eisbach.Eisbach"

begin

named_theorems memory_theory

method memory_theory = (simp only: memory_theory MonadSE.bind_assoc')
method norm = (auto dest!: assert_D)


end

Theory Clean_Main

(******************************************************************************
 * Clean
 *
 * Copyright (c) 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.
 ******************************************************************************)

(*
 * Clean --- a basic abstract ("shallow") programming language for test and proof.
 * Authors : Burkhart Wolff, Frédéric Tuong
 *           Contributions by Chantal Keller
 *)

theory Clean_Main
  imports Clean Hoare_Clean Test_Clean
begin

end

Theory Quicksort_concept

(******************************************************************************
 * Clean
 *
 * Copyright (c) 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.
 ******************************************************************************)

(*
 * Quicksort Concept
 *
 * Authors : Burkhart Wolff, Frédéric Tuong
 *)

chapter ‹ Clean Semantics : A Coding-Concept Example›

text‹The following show-case introduces subsequently a non-trivial example involving
local and global variable declarations, declarations of operations with pre-post conditions as
well as direct-recursive operations (i.e. C-like functions with side-effects on global and
local variables. ›

theory Quicksort_concept
  imports Clean
          Hoare_MonadSE
begin

section‹The Quicksort Example›

text‹ We present the following quicksort algorithm in some conceptual, high-level notation:

\begin{isar}
algorithm (A,i,j) =
    tmp := A[i];
    A[i]:=A[j];
    A[j]:=tmp

algorithm partition(A, lo, hi) is
    pivot := A[hi]
    i := lo
    for j := lo to hi - 1 do
        if A[j] < pivot then
            swap A[i] with A[j]
            i := i + 1
    swap A[i] with A[hi]
    return i

algorithm quicksort(A, lo, hi) is
    if lo < hi then
        p := partition(A, lo, hi)
        quicksort(A, lo, p - 1)
        quicksort(A, p + 1, hi)

\end{isar}
›

text‹In the following, we will present the Quicksort program alternatingly in Clean high-level
notation and simulate its effect by an alternative formalisation representing the semantic
effects of the high-level notation on a step-buy-step basis. Note that Clean does not posses
the concept of call-by-reference parameters; consequently, the algorithm must be specialized
to a variant where @{term A} is just a global variable.›

section‹Clean Encoding of the Global State of Quicksort›

text‹We demonstrate the accumulating effect of some key Clean commands by highlighting the
changes of  Clean's state-management module state. At the beginning, the state-type of
the Clean state management is just the type of the @{typ "'a Clean.control_state.control_state_ext"},
while the table of global and local variables is empty.›

MLval Type(s,t) = StateMgt_core.get_state_type_global @{theory};
    StateMgt_core.get_state_field_tab_global @{theory};

text‹The global_vars› command, described and defined in ‹Clean.thy›,
declares the global variable ‹A›. This has the following effect:›

global_vars state
    A :: "int list"

text‹... which is reflected in Clean's state-management table:›
MLval Type("Quicksort_concept.global_state_state_scheme",t)
        = StateMgt_core.get_state_type_global @{theory};
    StateMgt_core.get_state_field_tab_global @{theory}
text‹Note that the state-management uses long-names for complete disambiguation.›


section ‹Encoding swap in Clean›

subsection ‹swap› in High-level Notation›

text‹Unfortunately, the name result› is already used in the logical context; we use local binders
instead.›
definition "i = ()" ― ‹check that termi can exist as a constant with an arbitrary type before treating function_spec
definition "j = ()" ― ‹check that termj can exist as a constant with an arbitrary type before treating function_spec

function_spec swap (i::nat,j::nat) ― ‹TODO: the hovering on parameters produces a number of report equal to the number of ML‹Proof_Context.add_fixes› called in MLFunction_Specification_Parser.checkNsem_function_spec
pre          "‹i < length A ∧ j < length A›"
post         "‹λres. length A = length(old A) ∧ res = ()›"
local_vars   tmp :: int
defines      " ‹ tmp := A ! i›  ;-
               ‹ A := list_update A i (A ! j)› ;-
               ‹ A := list_update A j tmp› "

text‹The body --- heavily using the λ›-lifting cartouche --- corresponds to the low level
term: ›

text@{cartouche [display=true]
‹‹defines " ((assign_local tmp_update (λσ. (A σ) ! i ))   ;-
            (assign_global A_update (λσ. list_update (A σ) (i) (A σ ! j))) ;-
            (assign_global A_update (λσ. list_update (A σ) (j) ((hd o tmp) σ))))"››}

text‹The effect of this statement is generation of the following definitions in the logical context:›
term "(i, j)" ― ‹check that term‹i› and term‹j› are pointing to the constants defined before treating function_spec
thm push_local_swap_state_def
thm pop_local_swap_state_def
thm swap_pre_def
thm swap_post_def
thm swap_core_def
thm swap_def

text‹The state-management is in the following configuration:›

MLval Type(s,t) = StateMgt_core.get_state_type_global @{theory};
    StateMgt_core.get_state_field_tab_global @{theory}

subsection ‹A Similation of ‹swap› in elementary specification constructs:›

text‹Note that we prime identifiers in order to avoid confusion with the definitions of the
previous section. The pre- and postconditions are just definitions of the following form:›

definition swap'_pre :: " nat × nat  'a global_state_state_scheme  bool"
  where "swap'_pre  λ(i, j) σ. i < length (A σ)  j < length (A σ)"
definition swap'_post :: "'a × 'b  'c global_state_state_scheme  'd global_state_state_scheme  unit  bool"
  where "swap'_post  λ(i, j) σpre σ res. length (A σ) = length (A σpre)  res = ()"
text‹The somewhat vacuous parameter res› for the result of the swap-computation is the conseqeuence
of the implicit definition of the return-type as @{typ "unit"}

text‹We simulate the effect of the local variable space declaration by the following command
     factoring out the functionality into the command local_vars_test›
(*
local_vars_test swap' "unit"
   tmp :: "int"

ML‹
val Type(s,t) = StateMgt_core.get_state_type_global @{theory};
val tab = StateMgt_core.get_state_field_tab_global @{theory};
@{term "A::('a local_swap_state_scheme⇒ int list)"}›

text‹This has already the effect of the definition:›
thm push_local_swap_state_def
thm pop_local_swap_state_def

text‹Again, we simulate the effect of this command by more elementary \HOL specification constructs:›
(* Thus, the internal functionality in ‹local_vars› is the construction of the two definitions *)
definition push_local_swap_state' :: "(unit,'a local_swap'_state_scheme) MONSE"
  where   "push_local_swap_state' σ =
                    Some((),σ⦇local_swap_state.tmp :=  undefined # local_swap_state.tmp σ ⦈)"

definition pop_local_swap_state' :: "(unit,'a local_swap'_state_scheme) MONSE"
  where   "pop_local_swap_state' σ =
                    Some(hd(local_swap_state.result_value σ),
                                ― ‹ recall : returns op value ›
                                ― ‹ which happens to be unit ›
                         σ⦇local_swap_state.tmp:= tl( local_swap_state.tmp σ) ⦈)"


definition swap'_core :: "nat × nat ⇒  (unit,'a local_swap'_state_scheme) MONSE"
    where "swap'_core  ≡ (λ(i,j). ((assign_local tmp_update (λσ. A σ ! i ))   ;-
                            (assign_global A_update (λσ. list_update (A σ) (i) (A σ ! j))) ;-
                            (assign_global A_update (λσ. list_update (A σ) (j) ((hd o tmp) σ)))))"

text‹ a block manages the "dynamically" created fresh instances for the local variables of swap ›
definition swap' :: "nat × nat ⇒  (unit,'a local_swap'_state_scheme) MONSE"
  where   "swap' ≡ λ(i,j). blockC push_local_swap_state' (swap_core (i,j)) pop_local_swap_state'"


text‹NOTE: If local variables were only used in single-assignment style, it is possible
   to drastically simplify the encoding. These variables were not stored in the state,
   just kept as part of the monadic calculation. The simplifications refer both to
   calculation as well as well as symbolic execution and deduction.›

text‹The could be represented by the following alternative, optimized version :›
definition swap_opt :: "nat × nat ⇒  (unit,'a global_state_state_scheme) MONSE"
    where "swap_opt ≡ λ(i,j). (tmp ←  yieldC (λσ. A σ ! i) ;
                          ((assign_global A_update (λσ. list_update (A σ) (i) (A σ ! j))) ;-
                           (assign_global A_update (λσ. list_update (A σ) (j) (tmp)))))"
text‹In case that all local variables are single-assigned in swap, the entire local var definition
   could be ommitted.›
*)

section ‹Encoding ‹partition› in Clean›

subsection ‹partition› in High-level Notation›

function_spec partition (lo::nat, hi::nat) returns nat
pre          "‹lo < length A ∧ hi < length A›"
post         "‹λres::nat. length A = length(old A) ∧ res = 3›"
local_vars   pivot  :: int
             i      :: nat
             j      :: nat
defines      " (‹pivot := A ! hi ›  ;- ‹i := lo › ;- ‹j := lo › ;-
               (whileC ‹j ≤ hi - 1 ›
                do (ifC ‹A ! j < pivot›
                    then  callC swap ‹(i , j) ›  ;-
                          ‹i := i + 1 ›
                    else skipSE
                    fi) ;-
                    ‹j := j + 1 ›
                od) ;-
                callC swap ‹(i, j)›  ;-
                returnC result_value_update ‹i›
               ) "

text‹ The body is a fancy syntax for :

@{cartouche [display=true]
‹‹defines      " ((assign_local pivot_update (λσ. A σ ! hi ))   ;-
               (assign_local i_update (λσ. lo )) ;-

               (assign_local j_update (λσ. lo )) ;-
               (whileC (λσ. (hd o j) σ ≤ hi - 1 )
                do (ifC (λσ. A σ ! (hd o j) σ < (hd o pivot)σ )
                    then  callC (swap) (λσ. ((hd o i) σ,  (hd o j) σ))  ;-
                          assign_local i_update (λσ. ((hd o i) σ) + 1)
                    else skipSE
                    fi) ;-
                    (assign_local j_update (λσ. ((hd o j) σ) + 1))
                od) ;-
                callC (swap) (λσ. ((hd o i) σ,  (hd o j) σ))  ;-
                assign_local result_value_update (λσ. (hd o i) σ)
                ― ‹ the meaning of the return stmt ›
               ) "››}


text‹The effect of this statement is generation of the following definitions in the logical context:›
thm partition_pre_def
thm partition_post_def
thm push_local_partition_state_def
thm pop_local_partition_state_def
thm partition_core_def
thm partition_def

text‹The state-management is in the following configuration:›

MLval Type(s,t) = StateMgt_core.get_state_type_global @{theory};
    StateMgt_core.get_state_field_tab_global @{theory}

subsection ‹A Similation of ‹partition› in elementary specification constructs:›

definition "partition'_pre  λ(lo, hi) σ. lo < length (A σ)  hi < length (A σ)"
definition "partition'_post  λ(lo, hi) σpre σ res. length (A σ) = length (A σpre)  res = 3"

text‹Recall: list-lifting is automatic in local_vars_test›:›

local_vars_test  partition' "nat"
    pivot  :: "int"
    i      :: "nat"
    j      :: "nat"

text‹ ... which results in the internal definition of the respective push and pop operations
for the @{term "partition'"} local variable space: ›

thm push_local_partition'_state_def
thm pop_local_partition'_state_def

(* equivalent to *)
definition push_local_partition_state' :: "(unit, 'a local_partition'_state_scheme) MONSE"
  where   "push_local_partition_state' σ = Some((),
                        σlocal_partition_state.pivot := undefined # local_partition_state.pivot σ,
                          local_partition_state.i     := undefined # local_partition_state.i σ,
                          local_partition_state.j     := undefined # local_partition_state.j σ,
                          local_partition_state.result_value
                                           := undefined # local_partition_state.result_value σ )"

definition pop_local_partition_state' :: "(nat,'a local_partition_state_scheme) MONSE"
  where   "pop_local_partition_state' σ = Some(hd(local_partition_state.result_value σ),
                       σlocal_partition_state.pivot := tl(local_partition_state.pivot σ),
                         local_partition_state.i     := tl(local_partition_state.i σ),
                         local_partition_state.j     := tl(local_partition_state.j σ),
                         local_partition_state.result_value :=
                                                        tl(local_partition_state.result_value σ) )"


definition partition'_core :: "nat × nat   (unit,'a local_partition'_state_scheme) MONSE"
  where   "partition'_core   λ(lo,hi).
              ((assign_local pivot_update (λσ. A σ ! hi ))   ;-
               (assign_local i_update (λσ. lo )) ;-

               (assign_local j_update (λσ. lo )) ;-
               (whileC (λσ. (hd o j) σ  hi - 1 )
                do (ifC (λσ. A σ ! (hd o j) σ < (hd o pivot)σ )
                    then  callC (swap) (λσ. ((hd o i) σ,  (hd o j) σ))  ;-
                          assign_local i_update (λσ. ((hd o i) σ) + 1)
                    else skipSE
                    fi)
                od) ;-
               (assign_local j_update (λσ. ((hd o j) σ) + 1)) ;-
                callC (swap) (λσ. ((hd o i) σ,  (hd o j) σ))  ;-
                assign_local result_value_update (λσ. (hd o i) σ)
                ― ‹ the meaning of the return stmt ›
               )"

thm partition_core_def

(* a block manages the "dynamically" created fresh instances for the local variables of swap *)
definition partition' :: "nat × nat   (nat,'a local_partition'_state_scheme) MONSE"
  where   "partition'   λ(lo,hi). blockC push_local_partition_state
                                   (partition_core (lo,hi))
                                   pop_local_partition_state"


section ‹Encoding the toplevel : ‹quicksort› in Clean›

subsection ‹quicksort› in High-level Notation›

rec_function_spec quicksort (lo::nat, hi::nat) returns unit
pre          "‹lo ≤ hi ∧ hi < length A›"
post         "‹λres::unit. ∀i∈{lo .. hi}. ∀j∈{lo .. hi}. i ≤ j ⟶ A!i ≤ A!j›"
variant      "hi - lo"
local_vars   p :: "nat"
defines      " ifC ‹lo < hi›
               then (ptmp  callC partition ‹(lo, hi)› ; assign_local p_update (λσ. ptmp)) ;-
                     callC quicksort ‹(lo, p - 1)› ;-
                     callC quicksort ‹(lo, p + 1)›
               else skipSE
               fi"


thm quicksort_core_def
thm quicksort_def
thm quicksort_pre_def
thm quicksort_post_def




subsection ‹A Similation of ‹quicksort› in elementary specification constructs:›

text‹This is the most complex form a Clean function may have: it may be directly
recursive. Two subcases are to be distinguished: either a measure is provided or not.›

text‹We start again with our simulation: First, we define the local variable p›.›
local_vars_test  quicksort' "unit"
    p  :: "nat"

MLval (x,y) = StateMgt_core.get_data_global @{theory};

thm pop_local_quicksort'_state_def
thm push_local_quicksort'_state_def

(* this implies the definitions : *)
definition push_local_quicksort_state' :: "(unit, 'a local_quicksort'_state_scheme) MONSE"
  where   "push_local_quicksort_state' σ =
                 Some((), σlocal_quicksort'_state.p := undefined # local_quicksort'_state.p σ,
                            local_quicksort'_state.result_value := undefined # local_quicksort'_state.result_value σ )"




definition pop_local_quicksort_state' :: "(unit,'a local_quicksort'_state_scheme) MONSE"
  where   "pop_local_quicksort_state' σ = Some(hd(local_quicksort'_state.result_value σ),
                       σlocal_quicksort'_state.p   := tl(local_quicksort'_state.p σ),
                         local_quicksort'_state.result_value :=
                                                      tl(local_quicksort'_state.result_value σ) )"

text‹We recall the structure of the direct-recursive call in Clean syntax:
@{cartouche [display=true]
‹
funct quicksort(lo::int, hi::int) returns unit
     pre  "True"
     post "True"
     local_vars p :: int
     ‹ifCLEAN ‹lo < hi› then
        p := partition(lo, hi) ;-
        quicksort(lo, p - 1) ;-
        quicksort(p + 1, hi)
      else Skip›
›}


definition quicksort'_pre :: "nat × nat  'a local_quicksort'_state_scheme    bool"
  where   "quicksort'_pre  λ(i,j). λσ.  True "

definition quicksort'_post :: "nat × nat  unit  'a local_quicksort'_state_scheme   bool"
  where   "quicksort'_post  λ(i,j). λ res. λσ.  True"


definition quicksort'_core :: "   (nat × nat  (unit,'a local_quicksort'_state_scheme) MONSE)
                               (nat × nat  (unit,'a local_quicksort'_state_scheme) MONSE)"
  where   "quicksort'_core quicksort_rec  λ(lo, hi).
                            ((ifC (λσ. lo < hi )
                              then (ptmp  callC partition (λσ. (lo, hi)) ;
                                    assign_local p_update (λσ. ptmp)) ;-
                                    callC quicksort_rec (λσ. (lo, (hd o p) σ - 1)) ;-
                                    callC quicksort_rec (λσ. ((hd o p) σ + 1, hi))
                              else skipSE
                              fi))"

term " ((quicksort'_core X) (lo,hi))"

definition quicksort' :: " ((nat × nat) × (nat × nat)) set 
                            (nat × nat  (unit,'a local_quicksort'_state_scheme) MONSE)"
  where   "quicksort' order  wfrec order (λX. λ(lo, hi). blockC push_local_quicksort'_state
                                                                 (quicksort'_core X (lo,hi))
                                                                 pop_local_quicksort'_state)"


subsection‹Setup for Deductive Verification›

text‹The coupling between the pre- and the post-condition state is done by the
     free variable (serving as a kind of ghost-variable) @{term "σpre"}. This coupling
     can also be used to express framing conditions; i.e. parts of the state which are
     independent and/or not affected by the computations to be verified. ›
lemma quicksort_correct :
  "λσ.   ¬exec_stop σ  quicksort_pre (lo, hi)(σ)  σ = σpre 
     quicksort (lo, hi)
   λr σ. ¬exec_stop σ  quicksort_post(lo, hi)(σpre)(σ)(r) "
   oops



end

Theory SquareRoot_concept

(******************************************************************************
 * Clean
 *
 * Copyright (c) 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.
 ******************************************************************************)

(*
 * SquareRoot_concept --- Example of monadic symbolic execution for a WHILE program.
 * Burkhart Wolff and Chantal Keller, LRI, Univ. Paris-Sud, France
 *)

section ‹ The Squareroot Example for Symbolic Execution ›

theory SquareRoot_concept
  imports Test_Clean
begin


subsection‹ The Conceptual Algorithm in Clean Notation›

text‹ In high-level notation, the algorithm we are investigating looks like this:

@{cartouche [display=true]
‹‹
function_spec sqrt (a::int) returns int
pre          "‹0 ≤ a›"
post         "‹λres::int.  (res + 1)2 > a ∧ a ≥ (res)2›"
defines      " (‹tm := 1› ;-
               ‹sqsum := 1› ;-
               ‹i := 0› ;-
               (whileSE ‹sqsum <= a› do
                  ‹i := i+1› ;-
                  ‹tm := tm + 2› ;-
                  ‹sqsum := tm + sqsum›
               od) ;-
               returnC result_value_update ‹i›
               )"
››}


subsection‹ Definition of the Global State ›

text‹The state is just a record; and the global variables correspond to fields in this
     record. This corresponds to typed, structured, non-aliasing states.
     Note that the types in the state can be arbitrary HOL-types - want to have
     sets of functions in a ghost-field ? No problem !
    ›

text‹ The state of the square-root program looks like this : ›

typ "Clean.control_state"

MLval Type(s,t) = StateMgt_core.get_state_type_global @{theory}
val Type(u,v) = @{typ unit}

(* could also be local variable, we flipped a coin and it became this way *)
global_vars state
   tm    :: int
   i     :: int
   sqsum :: int


MLval Type(s,t) = StateMgt_core.get_state_type_global @{theory}
val Type(u,v) = @{typ unit}


(* should be automatic *)
lemma tm_independent [simp]: " tm_update"
  unfolding control_independence_def  by auto

lemma i_independent [simp]: " i_update"
  unfolding control_independence_def  by auto

lemma sqsum_independent [simp]: " sqsum_update"
  unfolding control_independence_def  by auto





subsection‹ Setting for Symbolic Execution ›

text‹ Some lemmas to reason about memory›

lemma tm_simp : "tm (σtm := t) = t"
  using [[simp_trace]]  by simp
(* from trace:
   [1]Procedure "record" produced rewrite rule:
   tm (?r⦇tm := ?k⦈) ≡ ?k

   Unfortunately, this lemma is not exported ... It looks as if it is computed on the fly ...
   This could explain why this is slow for our purposes ...
*)
lemma tm_simp1 : "tm (σsqsum := s) = tm σ" by simp
lemma tm_simp2 : "tm (σi := s) = tm σ" by simp
lemma sqsum_simp : "sqsum (σsqsum := s) = s" by simp
lemma sqsum_simp1 : "sqsum (σtm := t) = sqsum σ" by simp
lemma sqsum_simp2 : "sqsum (σi := t) = sqsum σ" by simp
lemma i_simp : "i (σi := i') = i'" by simp
lemma i_simp1 : "i (σtm := i') = i σ" by simp
lemma i_simp2 : "i (σsqsum := i') = i σ" by simp

lemmas memory_theory =
  tm_simp tm_simp1 tm_simp2
  sqsum_simp sqsum_simp1 sqsum_simp2
  i_simp i_simp1 i_simp2


declare memory_theory [memory_theory]


lemma non_exec_assign_globalD':
  assumes " upd"
  shows   "σ  assign_global upd rhs ;- M ¬ exec_stop σ   upd (λ_. rhs σ) σ  M"
  apply(drule non_exec_assign_global'[THEN iffD1])
  using assms exec_stop_vs_control_independence apply blast
  by auto

lemmas non_exec_assign_globalD'_tm = non_exec_assign_globalD'[OF tm_independent]
lemmas non_exec_assign_globalD'_i = non_exec_assign_globalD'[OF i_independent]
lemmas non_exec_assign_globalD'_sqsum = non_exec_assign_globalD'[OF sqsum_independent]

text‹ Now we run a symbolic execution. We run match-tactics (rather than the Isabelle simplifier
  which would do the trick as well) in order to demonstrate a symbolic execution in Isabelle. ›


subsection‹ A Symbolic Execution Simulation ›


lemma
  assumes non_exec_stop[simp]: "¬ exec_stop σ0"
   and    pos : "0  (a::int)"
   and    annotated_program:
          "σ0  ‹tm := 1› ;-
                ‹sqsum := 1› ;-
                ‹i := 0› ;-
                (whileSE ‹sqsum <= a› do
                   ‹i := i+1› ;-
                   ‹tm := tm + 2› ;-
                   ‹sqsum := tm + sqsum›
                od) ;-
                assertSE(λσ. σ=σR)"

       shows "σR assertSE ‹i2  ≤ a ∧ a < (i + 1)2 "


  apply(insert annotated_program)

  apply(tactic "dmatch_tac @{context} [@{thm \"non_exec_assign_globalD'_tm\"}] 1",simp)
  apply(tactic "dmatch_tac @{context} [@{thm \"non_exec_assign_globalD'_sqsum\"}] 1",simp)
  apply(tactic "dmatch_tac @{context} [@{thm \"non_exec_assign_globalD'_i\"}] 1",simp)

  apply(tactic "dmatch_tac @{context} [@{thm \"exec_whileD\"}] 1")
  apply(tactic "ematch_tac @{context} [@{thm \"if_SE_execE''\"}] 1")
   apply(simp_all only: memory_theory MonadSE.bind_assoc')

   apply(tactic "dmatch_tac @{context} [@{thm \"non_exec_assign_globalD'_i\"}] 1",simp)
   apply(tactic "dmatch_tac @{context} [@{thm \"non_exec_assign_globalD'_tm\"}] 1",simp)
   apply(tactic "dmatch_tac @{context} [@{thm \"non_exec_assign_globalD'_sqsum\"}] 1",simp)

   apply(tactic "dmatch_tac @{context} [@{thm \"exec_whileD\"}] 1")
    apply(tactic "ematch_tac @{context} [@{thm \"if_SE_execE''\"}] 1")
    apply(simp_all only: memory_theory MonadSE.bind_assoc')

    apply(tactic "dmatch_tac @{context} [@{thm \"non_exec_assign_globalD'_i\"}] 1",simp)
    apply(tactic "dmatch_tac @{context} [@{thm \"non_exec_assign_globalD'_tm\"}] 1",simp)
    apply(tactic "dmatch_tac @{context} [@{thm \"non_exec_assign_globalD'_sqsum\"}] 1",simp)

    apply(tactic "dmatch_tac @{context} [@{thm \"exec_whileD\"}] 1")
    apply(tactic "ematch_tac @{context} [@{thm \"if_SE_execE''\"}] 1")
    apply(simp_all only: memory_theory MonadSE.bind_assoc')


    apply(tactic "dmatch_tac @{context} [@{thm \"non_exec_assign_globalD'_i\"}] 1",simp)
    apply(tactic "dmatch_tac @{context} [@{thm \"non_exec_assign_globalD'_tm\"}] 1",simp)
    apply(tactic "dmatch_tac @{context} [@{thm \"non_exec_assign_globalD'_sqsum\"}] 1",simp)
     apply(simp_all)

  text‹Here are all abstract test-cases explicit. Each subgoal correstponds to
       a path taken through the loop.›


  txt‹push away the test-hyp: postcond is true for programs with more than
    three loop traversals (criterion: all-paths(k). This reveals explicitly
    the three test-cases for  @{term "k<3"}. ›
   defer 1


(*
txt‹Instead of testing, we @{emph ‹prove›} that the test cases satisfy the
    post-condition for all @{term "k<3"} loop traversals and @{emph ‹all›}
    positive inputs @{term "a "}.›
   apply(auto  simp: assert_simp)
 *)
oops

text‹TODO: re-establish  automatic test-coverage tactics of @{cite "DBLP:conf/tap/Keller18"}.›

end