theory week08B_demo_sol
  imports Main
begin


\<comment> \<open>Syntax and State Space\<close>

type_synonym
  vname   = string
type_synonym
  state = "vname \<Rightarrow> nat"

type_synonym
  aexp  = "state \<Rightarrow> nat"
type_synonym  
  bexp  = "state \<Rightarrow> bool"


datatype
  com = SKIP                    
      | Assign vname aexp       ("_ :== _ " [60,60] 60)
      | Semi   com com          ("_;; _"  [50, 51] 50)
      | Cond   bexp com com     ("IF _ THEN _ ELSE _"  [0,0,59] 60)
      | While  bexp com         ("WHILE _ DO _ OD"  [0,45] 60)


\<comment> \<open>Example Program\<close>

definition
  A :: vname where
  "A \<equiv> ''A''"

definition
  B :: vname  where
  "B \<equiv> ''B''"

lemma [simp]: "A \<noteq> B" by (simp add: A_def B_def)
lemma [simp]: "B \<noteq> A" by (simp add: A_def B_def)

definition
  factorial :: com where
  "factorial \<equiv>  B :== (\<lambda>s. 1);;
                WHILE (\<lambda>s. s A \<noteq> 0) DO
                   B :== (\<lambda>s. s B * s A);;
                   A :== (\<lambda>s. s A - 1)
                OD"

\<comment> \<open>Execution\<close>

inductive 
  eval :: "com \<times> state \<Rightarrow> state \<Rightarrow> bool" ("_/ \<Rightarrow> _" [60,60] 61)
where
  Skip [intro!,simp]:    
  "(SKIP, s) \<Rightarrow> s"
|
  Assign [intro!,simp]: 
  "(x :== a, s) \<Rightarrow> s (x := a s)"
|
  Semi [intro!]:
  "\<lbrakk> (c\<^sub>1,s) \<Rightarrow> s''; (c\<^sub>2,s'') \<Rightarrow> s' \<rbrakk> \<Longrightarrow> (c\<^sub>1;; c\<^sub>2, s) \<Rightarrow> s'"
|
  IfTrue: 
  "\<lbrakk> b s; (c\<^sub>1,s) \<Rightarrow> s' \<rbrakk> \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> s'"
|
  IfFalse: 
  "\<lbrakk> \<not>b s; (c\<^sub>2,s) \<Rightarrow> s' \<rbrakk> \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> s'"
|
  WhileFalse: 
  "\<not>b s \<Longrightarrow> (WHILE b DO c OD, s) \<Rightarrow> s"
|
  WhileTrue:  
  "\<lbrakk>b s; (c,s) \<Rightarrow> s''; (WHILE b DO c OD, s'') \<Rightarrow> s'\<rbrakk> \<Longrightarrow> (WHILE b DO c OD, s) \<Rightarrow> s'"


(* Isabelle provides eval.induct which allows the 
   elimination of terms cs \<Rightarrow> t.
   In practice, we will have cs as a tuple (c,s).
   To avoid to manually have to split cs every time,
   we can use split_format as below to define an induction
   rule that will work on terms of the form (c, s) \<Rightarrow> t.*)

thm eval.induct
lemmas eval_induct = eval.induct [split_format (complete)]
thm eval_induct


(* In practice, it is also useful to have elimination rules
   for precisely when e.g. c=SKIP, or c= c1;;c2, etc.
   (If c=SKIP, eval_induct has many useless cases).
   The command inductive_cases allows exactly this.*)

inductive_cases
  skip [elim!]:   "(SKIP, s) \<Rightarrow> s'" and
  assign [elim!]: "(x :== a, s) \<Rightarrow> s'" and
  semi [elim!]:   "(c\<^sub>1;; c\<^sub>2, s) \<Rightarrow> s'" and
  "if" [elim!]:   "(IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> s'" and
  while:          "(WHILE b DO c OD, s) \<Rightarrow> s'"

thm skip assign semi "if" while

lemma skip_eq [simp]: "(SKIP, s) \<Rightarrow> s' = (s' = s)" by blast
lemma assign_eq [simp]: "(x :== a, s) \<Rightarrow> s' = (s' = s (x := a s))"  by blast



\<comment> \<open>---------------------------------------------------------------------\<close>
\<comment> \<open>Example Proof\<close>

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

(* Need to relate the final state of B to values of A and B *at each iteration* 
   of the loop *)
lemma factorial_partial_correct_helper:
  "(prog, s) \<Rightarrow> s' \<Longrightarrow> 
    prog = WHILE \<lambda>s. 0 < s A DO B :== (\<lambda>s. s B * s A) ;; A :== (\<lambda>s. s A - Suc 0)  OD \<Longrightarrow>
    s' B = s B * fac (s A)"
  apply (induct rule: eval_induct)
        apply (simp_all)
  apply (case_tac "s A")
   apply (simp)
  apply clarsimp
  (*sledgehammer*)
  by (simp add: distrib_left distrib_right)
  
lemma factorial_partial_correct:
  "(factorial, s) \<Rightarrow> s' \<Longrightarrow> s' B = fac (s A)"
  apply (unfold factorial_def)
  apply clarsimp
  apply (clarsimp simp: factorial_partial_correct_helper)
  done
  
\<comment> \<open>---------------------------------------------------------------------\<close>


type_synonym assn = "state => bool"

definition
  hoare_valid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" 50) where
  "\<Turnstile> {P} c {Q} \<equiv> \<forall>s s'. P s \<longrightarrow> (c,s) \<Rightarrow> s' \<longrightarrow> Q s'"


inductive 
  hoare :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<turnstile> ({(1_)}/ (_)/ {(1_)})" 50)
where
  h_skip: 
  "\<turnstile> {P} SKIP {P}"
|
  h_assign:  
  "\<turnstile> {\<lambda>s. P (s(x:= a s))} x:==a {P}"
|
  h_semi: 
  "\<lbrakk> \<turnstile> {P} c\<^sub>1 {R}; \<turnstile> {R} c\<^sub>2 {Q} \<rbrakk> \<Longrightarrow> \<turnstile> {P} c\<^sub>1;;c\<^sub>2 {Q}"
|
  h_if: 
  "\<lbrakk> \<turnstile> {\<lambda>s. P s \<and> b s} c\<^sub>1 {Q}; \<turnstile> {\<lambda>s. P s \<and> \<not>b s} c\<^sub>2 {Q} \<rbrakk> \<Longrightarrow>
  \<turnstile> {P} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}"
|
  h_while: 
  "\<lbrakk> \<turnstile> {\<lambda>s. P s \<and> b s} c {P}; \<forall>s. P s \<and> \<not>b s \<longrightarrow> Q s \<rbrakk> \<Longrightarrow>
  \<turnstile> {P} WHILE b DO c OD {Q}"
|
  conseq: 
  "\<lbrakk> \<forall>s. P s \<longrightarrow> P' s; \<turnstile> {P'} c {Q'}; \<forall>s. Q' s \<longrightarrow> Q s \<rbrakk> \<Longrightarrow>
  \<turnstile> {P} c {Q}"


\<comment> \<open>Soundness Proof\<close>

(* When a while loop is fully executed to a state s', 
   then the loop condition is false in s' (otherwise there
   would have been another iteration). Moreover, if the loop
   satisfies an invariant P, then P is true when the loop exits. *)
lemma while_final:
  "\<lbrakk>(prog, s) \<Rightarrow> s';  \<forall>s. P s \<and> b s \<longrightarrow> (\<forall>s'. (c, s) \<Rightarrow> s' \<longrightarrow> P s');  P s;
    prog = WHILE b DO c OD\<rbrakk>  \<Longrightarrow> P s' \<and> \<not> b s'"
   apply (induct rule: eval_induct)
   apply (simp_all)
   done
   
(* To show that a postcondition Q holds after a While loop,
   we need to find a predicate P that is an invariant of the loop
   (i.e. preserved by the loop body at each iteration) and
   is "enough" to prove the postcondition when the proof exits.*)
lemma while_sound:
  "\<lbrakk>\<Turnstile> {\<lambda>a. P a \<and> b a} c {P}; \<forall>s. P s \<and> \<not> b s \<longrightarrow> Q s\<rbrakk> \<Longrightarrow> 
  \<Turnstile> {P} WHILE b DO c OD {Q}"
  apply (clarsimp simp: hoare_valid_def)
  apply (subgoal_tac "P s' \<and> \<not> b s'")
   apply blast
  apply (rule while_final)
  apply (simp_all)
  done

theorem hoare_sound:
  "\<turnstile> {P} c {Q} \<Longrightarrow> \<Turnstile> {P} c {Q}"
proof(induct rule: hoare.induct)
  case (h_while P b c Q)
  then show ?case by(rule_tac while_sound)
qed (auto simp add: hoare_valid_def)

(*OR*)
theorem hoare_sound2:
  "\<turnstile> {P} c {Q} \<Longrightarrow> \<Turnstile> {P} c {Q}" 
  apply (induct rule:hoare.induct)
  by (fastforce elim: while_sound simp: hoare_valid_def)+

  
\<comment> \<open>--------------------------------------------------------------------------------------\<close>
\<comment> \<open>derived rules\<close>

lemma h_ass:
  "(\<And>s. P s \<Longrightarrow> Q (s(x := a s))) \<Longrightarrow> \<turnstile> {P} x :== a {Q}"
  apply (rule_tac Q'=Q in conseq)
  prefer 2
  apply (rule h_assign)
  apply (blast)+
  done
 


\<comment> \<open>example proof\<close>

lemma "\<turnstile> {\<lambda>s. True} x :== (\<lambda>s. 2) {\<lambda>s. s x = 2}"
  apply (rule h_ass)
  apply simp
  done

lemma 
  "\<turnstile> {\<lambda>s. s A = n} factorial {\<lambda>s. s B = fac n}"
  apply (unfold factorial_def)
  apply (rule h_semi)
   prefer 2
   apply (rule_tac P="\<lambda>s. s B * fac (s A) = fac n" in h_while)
    apply (rule h_semi)
     prefer 2
     apply (rule h_assign)
    apply (rule h_ass)
    apply clarsimp
    apply (case_tac "s A", simp)
    apply clarsimp
    apply (simp add: add_mult_distrib2 comm_semiring_class.distrib)
   apply clarsimp
  apply (rule h_ass)
  apply clarsimp
  done

\<comment> \<open>Bonus content: completeness proof\<close>

(* This relation is used to state a loop invariant for the completeness proof.
   Intuitively, while_rel P c x1 s holds if, starting from a state satisfying P,
   s is an intermediate state that can be reached by running the loop

     WHILE x1 DO c OD

   n times (not necessarily to completion).
 *)
inductive while_rel where
  while_rel_base: "P s \<Longrightarrow> while_rel P c x1 s"
| while_rel_step: "\<lbrakk>while_rel P c x1 s; x1 s; (c,s) \<Rightarrow> s'\<rbrakk> \<Longrightarrow> while_rel P c x1 s'"

lemma while_rel_valid:
  assumes "\<Turnstile> {P} WHILE x1 DO c OD {Q}"
  shows "\<Turnstile> {while_rel P c x1} WHILE x1 DO c OD {Q}"
proof -
  (* The curly brackets begin what's called an _explicit proof block_,
     which is a way of proving an auxiliary result within an Isar proof
     without explicitly stating it. For example, the proof block

     { fix x y :: nat
       have "x + y = y + x" by simp
     }

     will create the following theorem:

      ?x + ?y = ?y + ?x

     note that the arbitrary but fixed (orange) variables in the proof block
     were exported from the block as schematic variables.
   *)
  { fix s s'
    assume "while_rel P c x1 s"
       and "(WHILE x1 DO c OD, s) \<Rightarrow> s'"
    hence "Q s'" using assms
    proof(induct rule: while_rel.induct)
      case (while_rel_base P s c x1)
      then show ?case
        by(auto simp add: hoare_valid_def)
    next
      case (while_rel_step P c x1 s s'')
      then show ?case
        apply clarsimp
        apply(erule meta_mp)
        by(rule WhileTrue)
    qed
  } \<comment> \<open> Put the cursor here to see the theorem that the proof block created. \<close>
  thus ?thesis
    by(force simp add: hoare_valid_def)
qed

theorem hoare_complete:
  assumes "\<Turnstile> {P} c {Q}"
  shows "\<turnstile> {P} c {Q}"
  using assms
 \<comment> \<open> Structural induction is fine here since the Hoare rules are syntax-directed.
      Besides, we don't have an inductive relation as a premise, so no sense trying
      rule induction. \<close>
proof(induct c arbitrary: P Q)
case SKIP
  then show ?case
    by(auto simp add: hoare_valid_def intro: h_skip conseq)
next
  case (Assign x1 x2)
  then show ?case
    by(force intro: h_ass simp add: hoare_valid_def)
next
  case (Semi c1 c2)
  (* thm Semi contains induction hypotheses + other premises inherited from the
     chained facts present when the induction started. These can be referred
     to separately:
   *)
  thm Semi
  thm Semi.prems
  thm Semi.hyps
  show ?case using Semi.prems
    by(force intro: Semi.hyps
                    h_semi[where R="\<lambda> s. (\<forall>s'. (c2, s) \<Rightarrow> s' \<longrightarrow> Q s')"]
             simp add: hoare_valid_def)
    (* force doesn't find the intermediate pre/post-condition on its own,
       so we give it a clue by giving it a pre-instantiated version of h_semi
       as an intro rule.
     *)
next
  case (Cond x1 c1 c2)
  show ?case using Cond.prems
    by(force intro: h_if Cond.hyps IfTrue IfFalse simp add: hoare_valid_def)+
next
  case (While x1 c)
  from While.prems have "\<Turnstile> {while_rel P c x1} WHILE x1 DO c OD {Q}"
    by(rule while_rel_valid)
  then show ?case
    apply -
    apply(rule conseq[where Q'=Q and P'="while_rel P c x1"])
      apply(force intro: while_rel.intros)
     apply(rule h_while)
      apply(rule While.hyps)
      apply(force intro: while_rel.intros simp add: hoare_valid_def)
     apply(force intro: WhileFalse simp add: hoare_valid_def)
    apply simp
    done
qed

end