theory week08B_demo
  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)"
  (*TODO*)
  sorry

lemma factorial_partial_correct:
  "(factorial, s) \<Rightarrow> s' \<Longrightarrow> s' B = fac (s A)"
  (*TODO*)
  sorry

\<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}"

print_theorems

\<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'"
  (*TODO*)
  sorry
   
(* 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}"
  (*TODO*)
  sorry

theorem hoare_sound:
  "\<turnstile> {P} c {Q} \<Longrightarrow> \<Turnstile> {P} c {Q}" 
  (*TODO*)
  sorry

\<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}"
  sorry


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

lemma "\<turnstile> {\<lambda>s. True} x :== (\<lambda>s. 2) {\<lambda>s. s x = 2}"
  sorry

lemma 
  "\<turnstile> {\<lambda>s. s A = n} factorial {\<lambda>s. s B = fac n}"
  sorry

end