theory week08A_sol
  imports Main
begin

-- "Syntax and State Space"

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)


-- "Example Program"

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"

-- "Execution"

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\<^isub>1,s) \<Rightarrow> s''; (c\<^isub>2,s'') \<Rightarrow> s' \<rbrakk> \<Longrightarrow> (c\<^isub>1;; c\<^isub>2, s) \<Rightarrow> s'"
|
  IfTrue: 
  "\<lbrakk> b s; (c\<^isub>1,s) \<Rightarrow> s' \<rbrakk> \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> s'"
|
  IfFalse: 
  "\<lbrakk> \<not>b s; (c\<^isub>2,s) \<Rightarrow> s' \<rbrakk> \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>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'"

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

thm eval_induct

inductive_cases
  skip [elim!]:   "(SKIP, s) \<Rightarrow> s'" and
  assign [elim!]: "(x :== a, s) \<Rightarrow> s'" and
  semi [elim!]:   "(c\<^isub>1;; c\<^isub>2, s) \<Rightarrow> s'" and
  "if" [elim!]:   "(IF b THEN c\<^isub>1 ELSE c\<^isub>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



-- ---------------------------------------------------------------------
-- "Example Proof"

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

lemma factorial':
  "(WHILE \<lambda>s. 0 < s A DO B :== (\<lambda>s. s B * s A) ;; A :== (\<lambda>s. s A - Suc 0)  OD, s(B := n)) \<Rightarrow> s' \<Longrightarrow>
    s' B = n * fac (s A)"
  apply (induct "s A" arbitrary: s n)
   apply clarsimp
   apply (erule while)
    apply clarsimp
   apply simp
  apply (erule while)
   apply clarsimp
  apply clarsimp
  apply (drule_tac x="s (A := s A - Suc 0)" in meta_spec)
  apply clarsimp
  apply (drule sym)
  apply clarsimp
  apply (subgoal_tac "s(B := n + n * x, A := x) = s(A := x, B := n + n * x)")
   apply simp
   apply (simp add: add_mult_distrib2 add_mult_distrib)
  apply auto
  done

lemma factorial_correct:
  "(factorial, s) \<Rightarrow> s' \<Longrightarrow> s' B = fac (s A)"
  apply (unfold factorial_def)
  apply clarsimp
  apply (auto simp: factorial')
  done


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


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\<^isub>1 {R}; \<turnstile> {R} c\<^isub>2 {Q} \<rbrakk> \<Longrightarrow> \<turnstile> {P} c\<^isub>1;;c\<^isub>2 {Q}"
|
  h_if: 
  "\<lbrakk> \<turnstile> {\<lambda>s. P s \<and> b s} c\<^isub>1 {Q}; \<turnstile> {\<lambda>s. P s \<and> \<not>b s} c\<^isub>2 {Q} \<rbrakk> \<Longrightarrow>
  \<turnstile> {P} IF b THEN c\<^isub>1 ELSE c\<^isub>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}"


-- "Soundness Proof"

thm eval_induct

lemma invariant':
  assumes inv: "\<forall>s s'. P s \<and> b s \<longrightarrow> (c,s) \<Rightarrow> s' \<longrightarrow> P s'"
  shows "\<lbrakk> (w, s) \<Rightarrow> s'; w = WHILE b DO c OD; P s \<rbrakk> \<Longrightarrow> P s' \<and> \<not>b s'"
  apply (induct rule: eval_induct)
        apply simp_all
  apply clarsimp
  apply (insert inv)
  apply blast
  done

lemma invariant:
  assumes inv: "\<forall>s. P s \<and> b s \<longrightarrow> (\<forall>s'. (c,s) \<Rightarrow> s' \<longrightarrow> P s')"
  shows "\<lbrakk> (WHILE b DO c OD, s) \<Rightarrow> s';  P s \<rbrakk> \<Longrightarrow> P s' \<and> \<not>b s'"
  apply (rule invariant')
  apply (auto simp: inv)
  done

theorem hoare_sound:
  assumes deriv: "\<turnstile> {P} c {Q}" 
  shows "\<Turnstile> {P} c {Q}" 
  using deriv
  apply induct
       apply (simp add: hoare_valid_def)
      apply (simp add: hoare_valid_def)
     apply (simp add: hoare_valid_def)
     apply clarsimp
     apply blast
    apply (clarsimp simp: hoare_valid_def)
    apply blast
   apply (clarsimp simp: hoare_valid_def)
   apply (drule (2) invariant)
   apply clarsimp
  apply (clarsimp simp: hoare_valid_def)
  apply blast
  done


-- --------------------------------------------------------------------------------------
-- "derived rules"

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)
   prefer 2
   apply clarify
  apply blast
  done


-- "example proof"

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")
    apply simp
   apply simp
   apply (simp add: add_mult_distrib2 add_mult_distrib)
  apply clarsimp
  apply (rule h_ass)
  apply clarsimp
  done


end