(* Examples for Simpl VCG in part from $AFP/Simpl/ex/VcgEx.thy. 
   License: LGPL *)

theory week11A_demo imports Vcg begin

-- ---------------------------------------------------------------------

subsection {* State Spaces *}

text {*
  The state space for the example programs below. The record lists
  all global and local variables that will occur. Each name has
  the postfix @{text "_'"} so program variable names don't clutter 
  the Isabelle name space. Hoare logic syntax and VCG rely on this
  naming scheme.
*}

record 'g vars = "'g state" +
  A_' :: nat
  I_' :: nat
  M_' :: nat
  N_' :: nat
  R_' :: nat
  S_' :: nat
  Abr_':: string
  B_' :: bool


subsection {* Basic Examples *}

text {*
  Basic Hoare triples have a procedure environment @{text \<Gamma>}, a 
  precondition, a command, and a postcondition. To distinguish
  them from normal sets, pre/post conditions use 
  @{text "{|"} and @{text "|}"} instead of @{text "{"} and @{text "}"}. 
  Unicode symbols are @{text "\<lbrace>"} and @{text "\<rbrace>"}.
*}

lemma "\<Gamma> \<turnstile> {| \<acute>N = 5 |}  \<acute>N :== 2 * \<acute>N  {| \<acute>N = 10 |}"
  apply (rule HoarePartial.Basic) 
  apply simp
  done

text {*
  Program variables referring to the current state are prefixed by 
  the @{text "\<acute>"} (acute) symbol. 

  This distinguishes them from normal, logical Isabelle names.
*}


text {*
  We usually do not apply Hoare logic rules directly, but use the VCG 
  instead. It performs very basic simplification, and also tries to leave
  goals that don't explicitly refer to the state.
*}

lemma "\<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>N :== 10 \<lbrace>\<acute>N = 10\<rbrace>"
  by vcg

lemma "\<Gamma>\<turnstile> \<lbrace>2 * \<acute>N = 10\<rbrace> \<acute>N :== 2 * \<acute>N \<lbrace>\<acute>N = 10\<rbrace>"
  by vcg


-- "Note the difference to the Hoare rule application above, N becomes
    an Isabelle bound name, not a record function of the state."
lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>N = 5\<rbrace> \<acute>N :== 2 * \<acute>N \<lbrace>\<acute>N = 10\<rbrace>"
  apply vcg
  apply simp
  done

-- "This triple hs the weakest precondition, so vcg solves it directly"
lemma "\<Gamma>\<turnstile> \<lbrace>a = a \<and> b = b\<rbrace> \<acute>M :== a;; \<acute>N :== b \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace>"
  by vcg
  
-- "Usually the vcg will leave implications to solve"
lemma "\<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>M :== a;; \<acute>N :== b \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace>"
  apply vcg 
  apply simp
  done

-- "Slightly more complex example"
lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace>
          \<acute>I :== \<acute>M;; \<acute>M :== \<acute>N;; \<acute>N :== \<acute>I
          \<lbrace>\<acute>M = b \<and> \<acute>N = a\<rbrace>"
  apply vcg
  apply simp
  done

-- "Single stepping for debugging:"
lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace>
          \<acute>I :== \<acute>M;; \<acute>M :== \<acute>N;; \<acute>N :== \<acute>I
          \<lbrace>\<acute>M = b \<and> \<acute>N = a\<rbrace>"
  apply vcg_step
  apply vcg_step
  apply vcg_step
  apply vcg_step
  apply simp
  done


subsection {* While loops *}

-- "Loop invariants are specified inline:" 

lemma while_sum:
      "\<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0 \<rbrace>
          WHILE \<acute>M \<noteq> a
          INV \<lbrace>\<acute>S = \<acute>M * b \<rbrace>
          DO \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 OD
          \<lbrace>\<acute>S = a * b \<rbrace>"
  apply vcg 
  apply auto
  done

-- "We actually proved a statement about a program schema for any a and b:"
thm while_sum


-- "Factorial:"

primrec fac:: "nat \<Rightarrow> nat" where
"fac 0 = 1" |
"fac (Suc n) = (Suc n) * fac n"

lemma fac_simp [simp]: "0 < i \<Longrightarrow>  fac i = i * fac (i - 1)"
  by (cases i) simp_all

lemma fac_sound:
"\<Gamma> \<turnstile> {| \<acute>N = n |}
     \<acute>M :== 1;;
     WHILE \<acute>N \<noteq> 0 INV {| fac n = \<acute>M * fac \<acute>N |} DO
       \<acute>M :== \<acute>M * \<acute>N;;
       \<acute>N :== \<acute>N - 1
     OD
     {| \<acute>M = fac n |}"
apply vcg
apply auto
done

-- ---------------------------------------------------------------------

subsection "More control flow"

-- "Exceptions"

lemma 
  "\<Gamma>\<turnstile> \<lbrace>\<acute>N = 0\<rbrace> Throw \<lbrace>False\<rbrace>,\<lbrace>\<acute>N = 0\<rbrace>"
  by vcg

lemma 
  "\<Gamma>\<turnstile> \<lbrace>True\<rbrace> 
      TRY
        IF \<acute>A = 0 THEN THROW ELSE \<acute>N :== 1 FI
      CATCH
        \<acute>N :== 42;;
        THROW
      END
      \<lbrace>\<acute>N = 1\<rbrace>,\<lbrace>\<acute>N = 42\<rbrace>"
   apply vcg
   apply simp
   done


-- "Break/continue"

lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
          TRY       
            WHILE True
            INV \<lbrace>\<acute>S = \<acute>M * b\<rbrace>
            DO IF \<acute>M = a THEN THROW ELSE \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 FI OD
          CATCH
            SKIP
          END
          \<lbrace>\<acute>S = a * b\<rbrace>"
apply vcg
apply auto
done

lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
          TRY       
            WHILE True
            INV \<lbrace>\<acute>S = \<acute>M * b\<rbrace>
            DO IF \<acute>M = a THEN \<acute>Abr :== ''Break'';;THROW 
               ELSE \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 
               FI 
            OD
          CATCH
            IF \<acute>Abr = ''Break'' THEN SKIP ELSE Throw FI
          END
          \<lbrace>\<acute>S = a * b\<rbrace>"
apply vcg
apply auto
done


-- {* SWITCH *}

lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>N = 5\<rbrace> SWITCH \<acute>B 
                        {True} \<Rightarrow> \<acute>N :== 6
                      | {False} \<Rightarrow> \<acute>N :== 7
                     END
          \<lbrace>\<acute>N > 5\<rbrace>"
apply vcg
apply simp
done

lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>N = 5\<rbrace> SWITCH \<acute>N 
                        {v. v < 5} \<Rightarrow> \<acute>N :== 6
                      | {v. v \<ge> 5} \<Rightarrow> \<acute>N :== 7
                     END
          \<lbrace>\<acute>N > 5\<rbrace>"
apply vcg
apply simp
done


-- ---------------------------------------------------------------------

subsection {* Procedures *}

text {* Parameters are on the left  of the |, 
        result parameters are on the right. *}

procedures
  Add (N,M|R) = "\<acute>R :== \<acute>N + \<acute>M;; \<acute>N :== 0"

text {*
  The procedures command sets up a locale (named context with set of 
  assumptions) for the name and implementation of Add.
*}

context Add_impl
begin

thm Add_impl Add_body_def

lemma "\<Gamma> \<turnstile> \<lbrace> True \<rbrace> 
           \<acute>N :== n;; 
           \<acute>I :== CALL Add(\<acute>N,\<acute>N)
           \<lbrace> \<acute>I = 2 * \<acute>N \<and> \<acute>N = n\<rbrace>"
  -- "formal parameters are replaced with actual, I gets the value of R,
      the change of N is local to Add"
  apply vcg
  apply simp
  done

end

-- {* Recursion: *}

text {* Recursive version of factorial. *}

procedures
  Fac (N|R) = "IF \<acute>N = 0 THEN \<acute>R :== 1
                       ELSE \<acute>R :== CALL Fac(\<acute>N - 1);;
                            \<acute>R :== \<acute>N * \<acute>R
                       FI"

context Fac_impl
begin

thm Fac_impl Fac_body_def

text {*
  For recursive procedures, we carry around another environment \<Theta> for
  procedure specifications. Similarly to induction, we need to quantify
  n if we want to use a different value n in the recursive call. 
*}

lemma "\<forall>n. \<Gamma>,\<Theta>\<turnstile>\<lbrace>\<acute>N=n\<rbrace> PROC Fac(\<acute>N,\<acute>R) \<lbrace>\<acute>R = fac n\<rbrace>"
  apply (hoare_rule HoarePartial.ProcRec1)
  apply vcg
  apply simp
  done


-- "single stepping, \<Theta> does not really need to be named explicitly."
lemma "\<forall>n. \<Gamma>\<turnstile>\<lbrace>\<acute>N=n\<rbrace> \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac n\<rbrace>"
  apply (hoare_rule HoarePartial.ProcRec1)
  apply vcg_step
  apply   vcg_step
  apply  vcg_step
  apply vcg_step
  apply vcg_step
  apply simp
  done

end (* of context Fac_Impl *)

end