theory Demo13 
imports Main
begin

-- "Syntax and State Space"



types 
  loc   = string
  state = "loc \<Rightarrow> nat"

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

datatype
  com = SKIP                    
      | Assign loc 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"
constdefs  
  A :: loc
  "A \<equiv> ''A''"

  B :: loc 
  "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)

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


-- "Execution"

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

print_theorems
inductive_cases
  skip [elim!]:   "\<langle>SKIP, \<sigma>\<rangle> \<longrightarrow> \<sigma>'" and
  assign [elim!]: "\<langle>x :== a, \<sigma>\<rangle> \<longrightarrow> \<sigma>'" and
  semi [elim!]:   "\<langle>c\<^isub>1;; c\<^isub>2, \<sigma>\<rangle> \<longrightarrow> \<sigma>'" and
  "if" [elim!]:    "\<langle>IF b THEN c\<^isub>1 ELSE c\<^isub>2, \<sigma>\<rangle> \<longrightarrow> \<sigma>'" and
  while:          "\<langle>WHILE b DO c OD, \<sigma>\<rangle> \<longrightarrow> \<sigma>'"

thm skip assign semi "if" while

lemma skip_eq [simp]: "\<langle>SKIP, \<sigma>\<rangle> \<longrightarrow> \<sigma>' = (\<sigma>' = \<sigma>)" by blast
lemma assign_eq [simp]: "\<langle>x :== a, \<sigma>\<rangle> \<longrightarrow> \<sigma>' = (\<sigma>' = \<sigma> (x := a \<sigma>))"  by blast



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

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


lemma factorial_helper:
  "\<langle>c,\<sigma>\<rangle> \<longrightarrow> \<sigma>' \<Longrightarrow> 
  (c = WHILE \<lambda>\<sigma>. 0 < \<sigma> A DO B :== (\<lambda>\<sigma>. \<sigma> B * \<sigma> A) ;; A :== (\<lambda>\<sigma>. \<sigma> A - Suc 0)  OD)
  \<longrightarrow> \<sigma>' B = (\<sigma> B) * fac (\<sigma> A)"
  apply (erule eval.induct)
  apply simp_all
   apply clarsimp
  apply clarsimp
  apply (erule notE)
  apply (case_tac "\<sigma> A")
   apply simp
  apply simp
  done

lemma factorial_partial_correct:
  "\<langle>factorial, \<sigma>\<rangle> \<longrightarrow> \<sigma>' \<Longrightarrow> \<sigma>' B = fac (\<sigma> A)"
  apply (unfold factorial_def)
  apply clarsimp
  apply (drule factorial_helper)
  apply simp
  done
  

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

term "x \<union> y"


inductive
  foo :: "nat => bool"
where
 "foo (Suc x)"

lemma "foo x ==> x \<noteq> 0"
  apply (erule foo.induct)
  apply simp
  done

types assn = "state => bool"

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


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


-- "Soundness Proof"

lemma invariant:
  assumes inv: "\<forall>\<sigma> \<sigma>'. P \<sigma> \<and> b \<sigma> \<longrightarrow> \<langle>c,\<sigma>\<rangle> \<longrightarrow> \<sigma>' \<longrightarrow> P \<sigma>'"
  shows "\<lbrakk> \<langle>WHILE b DO c OD,\<sigma>\<rangle> \<longrightarrow> \<sigma>';  P \<sigma> \<rbrakk> \<Longrightarrow> P \<sigma>' \<and> \<not>b \<sigma>'"
proof -
  { fix w assume "\<langle>w,\<sigma>\<rangle> \<longrightarrow> \<sigma>'"
    hence "w = WHILE b DO c OD \<longrightarrow> P \<sigma> \<longrightarrow> P \<sigma>' \<and> \<not>b \<sigma>'"
    proof induct
      case (WhileTrue b' \<sigma> c' \<sigma>'' \<sigma>')
      { assume "b = b'" and "c' = c" 
        with WhileTrue
        have ?case by simp (insert inv, blast) }      
      thus ?case by auto
    qed auto
  }
  thus "\<lbrakk> \<langle>WHILE b DO c OD,\<sigma>\<rangle> \<longrightarrow> \<sigma>';  P \<sigma> \<rbrakk> \<Longrightarrow> P \<sigma>' \<and> \<not>b \<sigma>'" by blast
qed

theorem hoare_sound:
  assumes deriv: "\<turnstile> {P} c {Q}" 
  shows "\<Turnstile> {P} c {Q}" 
using deriv proof induct
  case h_skip
  show ?case
    by (simp add: hoare_valid_def)
next
  fix P x a  
  have "\<forall>\<sigma> \<sigma>'. P (\<sigma>(x := a \<sigma>)) \<longrightarrow> \<langle>x :== a, \<sigma>\<rangle> \<longrightarrow> \<sigma>' \<longrightarrow> P \<sigma>'" by simp
  thus "\<Turnstile> { \<lambda>\<sigma>. P (\<sigma>(x := a \<sigma>)) } x :== a  {P}" by (unfold hoare_valid_def)
next
  fix P c\<^isub>1 c\<^isub>2 Q R
  assume "\<Turnstile> {P} c\<^isub>1 {R}" 
  hence "\<forall>\<sigma> \<sigma>'. P \<sigma> \<longrightarrow> \<langle>c\<^isub>1, \<sigma>\<rangle> \<longrightarrow> \<sigma>' \<longrightarrow> R \<sigma>'" by (unfold hoare_valid_def)
  moreover
  assume "\<Turnstile> {R} c\<^isub>2 {Q}" 
  hence "\<forall>\<sigma> \<sigma>'. R \<sigma> \<longrightarrow> \<langle>c\<^isub>2, \<sigma>\<rangle> \<longrightarrow> \<sigma>' \<longrightarrow> Q \<sigma>'" by (unfold hoare_valid_def)
  ultimately
  have "\<forall>\<sigma> \<sigma>'. P \<sigma> \<longrightarrow> \<langle>c\<^isub>1;;c\<^isub>2, \<sigma>\<rangle> \<longrightarrow> \<sigma>' \<longrightarrow> Q \<sigma>'" by blast
  thus "\<Turnstile> {P} c\<^isub>1;; c\<^isub>2 {Q}" by (unfold hoare_valid_def)
next
  case (h_if P b c\<^isub>1 Q c\<^isub>2)
  thus ?case by (unfold hoare_valid_def) (blast elim: "if")
next
  fix P b c Q
  assume "\<Turnstile> {\<lambda>\<sigma>. P \<sigma> \<and> b \<sigma>} c {P}"
  hence "\<forall>\<sigma> \<sigma>'. P \<sigma> \<and> b \<sigma> \<longrightarrow> \<langle>c,\<sigma>\<rangle> \<longrightarrow> \<sigma>' \<longrightarrow> P \<sigma>'" by (unfold hoare_valid_def)
  hence "\<And>\<sigma> \<sigma>'. \<lbrakk> \<langle>WHILE b DO c OD,\<sigma>\<rangle> \<longrightarrow> \<sigma>'; P \<sigma> \<rbrakk> \<Longrightarrow> P \<sigma>' \<and> \<not>b \<sigma>'" by (rule invariant)
  moreover
  assume "\<forall>\<sigma>. P \<sigma> \<and> \<not> b \<sigma> \<longrightarrow> Q \<sigma>"
  ultimately
  show "\<Turnstile> {P} WHILE b DO c OD {Q}" by (unfold hoare_valid_def) blast    
next
  case (conseq P P' c Q' Q)
  thus ?case by (unfold hoare_valid_def) blast
qed
  


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

lemma h_ass:
  "(\<And>\<sigma>. P \<sigma> \<Longrightarrow> Q (\<sigma>(x := a \<sigma>))) \<Longrightarrow> \<turnstile> {P} x :== a {Q}"
  apply (rule conseq)
    prefer 2
    apply (rule h_assign)
   prefer 2
   apply clarify
   apply assumption
  apply blast
  done


-- "example proof"

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

lemma 
  "\<turnstile> {\<lambda>\<sigma>. \<sigma> A = n} factorial {\<lambda>\<sigma>. \<sigma> B = fac n}"
  apply (unfold factorial_def)
  apply (rule h_semi)
   prefer 2 
   apply (rule_tac P="\<lambda>\<sigma>. fac n = (\<sigma> B) * fac (\<sigma> A)" in h_while)
    apply (rule h_semi)
     prefer 2
     apply (rule h_assign)
    apply (rule h_ass)
    apply clarsimp
    apply (erule notE)
    apply (case_tac "\<sigma> A")
     apply simp
    apply simp
   apply clarsimp
  apply (rule h_ass)
  apply simp
  done

  
end

