(* 
   This is a slightly modified and specialized version of the partial
   correctness logic presented in
      ABSTRACT HOARE LOGICS
        by Tobias Nipkow

   Modifications are done for educational reasons by
   Arnd Poetzsch-Heffter to show the relation to 
   other theories discussed in the lecture.
*)

theory MyHoare imports Main begin

datatype var = V nat  (".v_"  90)

type_synonym state = "var \<Rightarrow> int" 
type_synonym bexp = "state \<Rightarrow> bool"

datatype com = Do "(state \<Rightarrow> state set)"
             | Semi  com com            ("_; _"  [60, 60] 10)
             | Cond  bexp com com     ("IF _ THEN _ ELSE _"  60)
             | While bexp com           ("WHILE _ DO _"  60)
             | Local "(state \<Rightarrow> state)" com "(state \<Rightarrow> state \<Rightarrow> state)"
               ("LOCAL _; _; _" [0,0,60] 60)

inductive
  exec :: "state \<Rightarrow> com \<Rightarrow> state \<Rightarrow> bool" ("_/ -_\<rightarrow>/ _" [50,0,50] 50)
where
  Do:     "t \<in> f s \<Longrightarrow> s -Do f\<rightarrow> t"

| Semi:   "\<lbrakk> s0 -c1\<rightarrow> s1; s1 -c2\<rightarrow> s2 \<rbrakk> \<Longrightarrow> s0 -c1;c2\<rightarrow> s2"

| IfT:    "\<lbrakk>  b s; s -c1\<rightarrow> t \<rbrakk> \<Longrightarrow> s -IF b THEN c1 ELSE c2\<rightarrow> t"
| IfF:    "\<lbrakk> \<not>b s; s -c2\<rightarrow> t \<rbrakk> \<Longrightarrow> s -IF b THEN c1 ELSE c2\<rightarrow> t"

| WhileF: "\<not>b s \<Longrightarrow> s -WHILE b DO c\<rightarrow> s"
| WhileT: "\<lbrakk> b s; s -c\<rightarrow> t; t -WHILE b DO c\<rightarrow> u \<rbrakk> \<Longrightarrow> s -WHILE b DO c\<rightarrow> u"

| Local:  "f s -c\<rightarrow> t \<Longrightarrow> s -LOCAL f; c; g\<rightarrow> g s t"


lemma exec_Do_iff[iff]: "(s -Do f\<rightarrow> t) = (t \<in> f s)"
by(auto elim: exec.cases intro:exec.intros)


lemma [iff]: "(s -c;d\<rightarrow> u) = (\<exists>t. s -c\<rightarrow> t \<and> t -d\<rightarrow> u)"
by(best elim: exec.cases intro:exec.intros)


lemma [iff]: "(s -IF b THEN c ELSE d\<rightarrow> t) =
              (s -if b s then c else d\<rightarrow> t)"
apply auto
apply(blast elim: exec.cases intro:exec.intros)+
done


lemma [iff]: "(s -LOCAL f; c; g\<rightarrow> u) = (\<exists>t. f s -c\<rightarrow> t \<and> u = g s t)"
by(fastsimp elim: exec.cases intro:exec.intros)


lemma unfold_while:
 "(s -WHILE b DO c\<rightarrow> u) =
  (s -IF b THEN c;WHILE b DO c ELSE Do(\<lambda>s. {s})\<rightarrow> u)"
by(auto elim: exec.cases intro:exec.intros split:split_if_asm)


lemma while_lemma[rule_format]:
"s -w\<rightarrow> t \<Longrightarrow> \<forall>b c. w = WHILE b DO c \<and> P s \<and>
                    (\<forall>s s'. P s \<and> b s \<and> s -c\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P t \<and> \<not>b t"

apply(erule exec.induct)
apply clarify+
defer
apply clarify+
apply(subgoal_tac "P t")
apply blast
apply blast
done


lemma while_rule:
 "\<lbrakk>s -WHILE b DO c\<rightarrow> t; P s; \<forall>s s'. P s \<and> b s \<and> s -c\<rightarrow> s' \<longrightarrow> P s'\<rbrakk>
  \<Longrightarrow> P t \<and> \<not>b t"

apply(drule while_lemma)
prefer 2 apply assumption
apply blast
done



type_synonym assn = "state \<Rightarrow> bool"

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


inductive
  hoare :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<turnstile> ({(1_)}/ (_)/ {(1_)})" 50)
where
  Do:    "\<turnstile> {\<lambda>s. \<forall>t \<in> f s. P t} Do f {P}"

| Semi:  "\<lbrakk> \<turnstile> {P}c1{Q};  \<turnstile> {Q}c2{R} \<rbrakk>  \<Longrightarrow>  \<turnstile> {P} c1;c2 {R}"

| If:    "\<lbrakk> \<turnstile> {\<lambda>s. P s \<and> b s} c1 {Q};  \<turnstile> {\<lambda>s. P s \<and> \<not>b s} c2 {Q} \<rbrakk>
          \<Longrightarrow> \<turnstile> {P} IF b THEN c1 ELSE c2 {Q}"

| While: "\<turnstile> {\<lambda>s. P s \<and> b s} c {P}  \<Longrightarrow>  \<turnstile> {P} WHILE b DO c {\<lambda>s. P s \<and> \<not>b s}"

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

| Local: "\<lbrakk> \<And>s. P s \<Longrightarrow> P' s (f s); \<forall>s. \<turnstile> {P' s} c {Q \<circ> (g s)} \<rbrakk> \<Longrightarrow>
        \<turnstile> {P} LOCAL f;c;g {Q}"


lemma strengthen_pre: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile> {P}c{Q}  \<rbrakk> \<Longrightarrow> \<turnstile> {P'}c{Q}"

by(erule hoare.Conseq, assumption, blast)


lemma weaken_post: "\<lbrakk> \<turnstile> {P}c{Q}; \<forall>s. Q s \<longrightarrow> Q' s  \<rbrakk> \<Longrightarrow> \<turnstile> {P}c{Q'}"

apply(rule hoare.Conseq)
apply(fast, assumption, assumption)
done



(*
{ x >= 0 }
c := 0;
sq := 1;
while sq<=x (
c  := c+1;
sq := sq + (2*c+1)
*)

definition x  :: "var" where "x \<equiv> .v0"
definition c  :: "var"  where  "c == .v1"
definition sq :: "var"  where  "sq == .v2"
definition a1 :: "com"  where  "a1 == (Do (\<lambda>s.{s(c := (0::int))}))"
definition a2 :: "com"  where  "a2 == (Do (\<lambda>s.{s(sq := (1::int))}))"
definition a3 :: "com"  where  "a3 == (Do (\<lambda>s.{s(c := (s c) + (1::int))}))"
definition a4 :: "com"  where  "a4 == (Do (\<lambda>s.{s(sq := (s sq) + (2*(s c)+(1::int)))}))"
definition wb :: "com"  where  "wb == (a3 ; a4)"
definition w  :: "com"   where  "w == (WHILE ( \<lambda>s. (s sq) \<le> (s x) ) DO wb)"
definition c1 :: "com"  where  "c1 == (a2 ; w)"
definition c0 :: "com"   where "c0 == (a1 ; c1)"


lemmas var_def = x_def c_def sq_def

lemma a1Prop:
"\<turnstile> { \<lambda>s. (0 \<le> (s x))} a1 {\<lambda>s.(s c)*(s c) \<le> (s x) \<and>  1 = ((s c)+1)*((s c)+1)}"

apply (simp add: a1_def var_def)
thm hoare.Do
apply(rule strengthen_pre)
prefer 2
apply (rule hoare.Do)
apply simp
done


lemma a2Prop: 
"\<turnstile> {\<lambda>s.(s c)*(s c) \<le> (s x) \<and>  1 = ((s c)+1)*((s c)+1)} a2 
                                  {\<lambda>s.(s c)*(s c) \<le> (s x) \<and> (s sq) = ((s c)+1)*((s c)+1)}"

apply (simp add: a2_def var_def)
thm hoare.Do
apply(rule strengthen_pre)
prefer 2
apply (rule hoare.Do)
apply simp
done


lemma a3Prop: 
"\<turnstile> {\<lambda>s. (s sq) \<le> (s x) \<and> (s c)*(s c) \<le> (s x) \<and> (s sq) = ((s c)+1)*((s c)+1) } a3 
        {\<lambda>s. (s c)*(s c) \<le> (s x) \<and> (s sq) = (s c)*(s c)}"

apply (simp add: a3_def var_def)
thm hoare.Do
apply(rule strengthen_pre)
prefer 2
apply (rule hoare.Do)
apply simp
done


lemma a4Prop [rule_format]: 
"\<turnstile> { \<lambda>s. (s c)*(s c) \<le> (s x) \<and> (s sq)+(2*(s c)+1) = ((s c)+1)*((s c)+1) } a4
       { \<lambda>s. (s c)*(s c) \<le> (s x) \<and>  (s sq) = ((s c)+1)*((s c)+1) }"
apply (simp add: a4_def var_def)
thm hoare.Do
apply(rule strengthen_pre)
prefer 2
apply (rule hoare.Do)
apply simp
done


lemma binom1: 
"((i::int)+1)*(i+1) = i*i + 2*i + 1"
apply (simp add: add mult ring_distribs)
done


lemma a4StrengthProp: 
"\<turnstile> { \<lambda>s. (s c)*(s c) \<le> (s x) \<and> (s sq) = (s c)*(s c) } a4
       { \<lambda>s. (s c)*(s c) \<le> (s x) \<and>  (s sq) = ((s c)+1)*((s c)+1) }"
apply (rule strengthen_pre)
prefer 2
apply (rule a4Prop)
apply (insert binom1)
apply simp
done


lemma wbProp [rule_format]: 
"\<turnstile> {\<lambda>s. (s sq) \<le> (s x) \<and> (s c)*(s c) \<le> (s x) \<and> (s sq) = ((s c)+1)*((s c)+1) } wb
                        { \<lambda>s. (s c)*(s c) \<le> (s x) \<and>  (s sq) = ((s c)+1)*((s c)+1) }"
apply (simp (no_asm) add: wb_def )
thm hoare.Semi
apply (rule Semi)
apply (rule a3Prop)
apply (rule a4StrengthProp)
done



lemma wProp: 
"\<turnstile> {\<lambda>s. (s c)*(s c) \<le> (s x) \<and> (s sq) = ((s c)+1)*((s c)+1) } w
    {\<lambda>s. \<not>((s sq) \<le> (s x)) \<and> (s c)*(s c) \<le> (s x) \<and> (s sq) = ((s c)+1)*((s c)+1) }"

apply (unfold w_def )
thm While
apply (rule weaken_post)
apply (rule While)
prefer 2
apply blast
apply (rule strengthen_pre)
prefer 2
apply (rule wbProp)
apply simp
done


lemma wWeakProp: 
"\<turnstile> {\<lambda>s. (s c)*(s c) \<le> (s x) \<and> (s sq) = ((s c)+1)*((s c)+1) } w
    {\<lambda>s. (s c)*(s c) \<le> (s x) \<and> (s x) < ((s c)+1)*((s c)+1) }"

apply (rule weaken_post)
thm wProp
apply (rule wProp)
apply simp
done



lemma c1Prop: 
"\<turnstile> {\<lambda>s.(s c)*(s c) \<le> (s x) \<and>  1 = ((s c)+1)*((s c)+1)} c1
    {\<lambda>s. (s c)*(s c) \<le> (s x) \<and> (s x) < ((s c)+1)*((s c)+1) }"

apply (unfold c1_def )
thm hoare.Semi
apply (rule Semi)
apply (rule a2Prop)
apply (rule wWeakProp)
done


lemma c0Prop: 
  "\<turnstile> {\<lambda>s.(0 \<le> (s x))} c0 {\<lambda>s. (s c)*(s c) \<le> (s x) \<and> (s x) < ((s c)+1)*((s c)+1) }"

apply (unfold c0_def )
apply (rule Semi)
apply (rule a1Prop)
apply (rule c1Prop)
done


end