Cookies disclaimer

I agree Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

Homework 11

This is the task corresponding to homework 11.

Resources

Download Files

Definitions File

theory Defs
  imports Main
begin

type_synonym vname = string
type_synonym val = int
type_synonym state = "vname \<Rightarrow> val"

datatype aexp
 = N int | V vname | Plus aexp aexp
 | Minus aexp aexp | Mul aexp aexp | Div aexp aexp

fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val" where
"aval (N n) s = n" |
"aval (V x) s = s x" |
"aval (Plus a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s + aval a\<^sub>2 s" |
"aval (Div a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s div aval a\<^sub>2 s" |
"aval (Mul a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s * aval a\<^sub>2 s" |
"aval (Minus a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s - aval a\<^sub>2 s"


definition null_state ("<>") where
  "null_state \<equiv> \<lambda>x. 0"
syntax
  "_State" :: "updbinds => 'a" ("<_>")
translations
  "_State ms" == "_Update <> ms"
  "_State (_updbinds b bs)" <= "_Update (_State b) bs"

datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp

fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
"bval (Bc v) s = v" |
"bval (Not b) s = (\<not> bval b s)" |
"bval (And b\<^sub>1 b\<^sub>2) s = (bval b\<^sub>1 s \<and> bval b\<^sub>2 s)" |
"bval (Less a\<^sub>1 a\<^sub>2) s = (aval a\<^sub>1 s < aval a\<^sub>2 s)"

datatype
  com = SKIP
      | Assign vname aexp       ("_ ::= _" [1000, 61] 61)
      | Seq    com  com         ("_;;/ _"  [60, 61] 60)
      | If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
      | While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)

inductive
  big_step :: "com \<times> state \<Rightarrow> state \<Rightarrow> bool" (infix "\<Rightarrow>" 55)
where
Skip: "(SKIP,s) \<Rightarrow> s" |
Assign: "(x ::= a,s) \<Rightarrow> s(x := aval a s)" |
Seq: "\<lbrakk> (c\<^sub>1,s\<^sub>1) \<Rightarrow> s\<^sub>2;  (c\<^sub>2,s\<^sub>2) \<Rightarrow> s\<^sub>3 \<rbrakk> \<Longrightarrow> (c\<^sub>1;;c\<^sub>2, s\<^sub>1) \<Rightarrow> s\<^sub>3" |
IfTrue: "\<lbrakk> bval b s;  (c\<^sub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> t" |
IfFalse: "\<lbrakk> \<not>bval b s;  (c\<^sub>2,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> t" |
WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s) \<Rightarrow> s" |
WhileTrue:
"\<lbrakk> bval b s\<^sub>1;  (c,s\<^sub>1) \<Rightarrow> s\<^sub>2;  (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3 \<rbrakk>
\<Longrightarrow> (WHILE b DO c, s\<^sub>1) \<Rightarrow> s\<^sub>3"

code_pred big_step .

declare big_step.intros [intro]
lemmas big_step_induct = big_step.induct[split_format(complete)]
thm big_step_induct

inductive_cases SkipE[elim!]: "(SKIP,s) \<Rightarrow> t"
thm SkipE
inductive_cases AssignE[elim!]: "(x ::= a,s) \<Rightarrow> t"
thm AssignE
inductive_cases SeqE[elim!]: "(c1;;c2,s1) \<Rightarrow> s3"
thm SeqE
inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \<Rightarrow> t"
thm IfE

inductive_cases WhileE[elim]: "(WHILE b DO c,s) \<Rightarrow> t"
thm WhileE

theorem big_step_determ: "\<lbrakk> (c,s) \<Rightarrow> t; (c,s) \<Rightarrow> u \<rbrakk> \<Longrightarrow> u = t"
  by (induction arbitrary: u rule: big_step.induct) blast+

abbreviation
  equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" (infix "\<sim>" 50) where
  "c \<sim> c' \<equiv> (\<forall>s t. (c,s) \<Rightarrow> t  =  (c',s) \<Rightarrow> t)"

lemma unfold_while:
  "(WHILE b DO c) \<sim> (IF b THEN c;; WHILE b DO c ELSE SKIP)" (is "?w \<sim> ?iw")
proof -
  have "(?iw, s) \<Rightarrow> t" if assm: "(?w, s) \<Rightarrow> t" for s t
  proof -
    from assm show ?thesis
    proof cases
      case WhileFalse
      thus ?thesis by blast
    next
      case WhileTrue
      from \<open>bval b s\<close> \<open>(?w, s) \<Rightarrow> t\<close> obtain s' where
        "(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
      hence "(c;; ?w, s) \<Rightarrow> t" by (rule Seq)
      with \<open>bval b s\<close> show ?thesis by (rule IfTrue)
    qed
  qed
  moreover
  have "(?w, s) \<Rightarrow> t" if assm: "(?iw, s) \<Rightarrow> t" for s t
  proof -
    from assm show ?thesis
    proof cases
      case IfFalse
      hence "s = t" using \<open>(?iw, s) \<Rightarrow> t\<close> by blast
      thus ?thesis using \<open>\<not>bval b s\<close> by blast
    next
      case IfTrue
      from \<open>(c;; ?w, s) \<Rightarrow> t\<close> obtain s' where
        "(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
      with \<open>bval b s\<close> show ?thesis by (rule WhileTrue)
    qed
  qed
  ultimately
  show ?thesis by blast
qed

paragraph "Hoare"

type_synonym assn = "state \<Rightarrow> bool"

abbreviation state_subst :: "state \<Rightarrow> aexp \<Rightarrow> vname \<Rightarrow> state"
  ("_[_'/_]" [1000,0,0] 999)
where "s[a/x] == s(x := aval a s)"

paragraph "Partial correctness"

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

inductive
  partial_hoare :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<turnstile> ({(1_)}/ (_)/ {(1_)})" 50)
where
partial_Skip: "\<turnstile> {P} SKIP {P}"  |

partial_Assign:  "\<turnstile> {\<lambda>s. P(s[a/x])} x::=a {P}"  |

partial_Seq: "\<lbrakk> \<turnstile> {P} c\<^sub>1 {Q};  \<turnstile> {Q} c\<^sub>2 {R} \<rbrakk>
      \<Longrightarrow> \<turnstile> {P} c\<^sub>1;;c\<^sub>2 {R}"  |

partial_If: "\<lbrakk> \<turnstile> {\<lambda>s. P s \<and> bval b s} c\<^sub>1 {Q};  \<turnstile> {\<lambda>s. P s \<and> \<not> bval b s} c\<^sub>2 {Q} \<rbrakk>
     \<Longrightarrow> \<turnstile> {P} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}"  |

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

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

lemmas [simp] = partial_hoare.partial_Skip partial_hoare.partial_Assign partial_hoare.partial_Seq partial_If

lemmas [intro!] = partial_hoare.partial_Skip partial_hoare.partial_Assign partial_hoare.partial_Seq partial_hoare.partial_If

lemma partial_strengthen_pre:
  "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s;  \<turnstile> {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile> {P'} c {Q}"
by (blast intro: partial_conseq)

lemma partial_weaken_post:
  "\<lbrakk> \<turnstile> {P} c {Q};  \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow>  \<turnstile> {P} c {Q'}"
  by (blast intro: partial_conseq)

lemma partial_Assign': "\<forall>s. P s \<longrightarrow> Q(s[a/x]) \<Longrightarrow> \<turnstile> {P} x ::= a {Q}"
by (simp add: partial_strengthen_pre[OF _ partial_Assign])

lemma partial_While':
assumes "\<turnstile> {\<lambda>s. P s \<and> bval b s} c {P}" and "\<forall>s. P s \<and> \<not> bval b s \<longrightarrow> Q s"
shows "\<turnstile> {P} WHILE b DO c {Q}"
by(rule partial_weaken_post[OF partial_While[OF assms(1)] assms(2)])


definition partial_wp :: "com \<Rightarrow> assn \<Rightarrow> assn" where
"partial_wp c Q = (\<lambda>s. \<forall>t. (c,s) \<Rightarrow> t  \<longrightarrow>  Q t)"

lemma partial_wp_SKIP[simp]: "partial_wp SKIP Q = Q"
by (rule ext) (auto simp: partial_wp_def)

lemma partial_wp_Ass[simp]: "partial_wp (x::=a) Q = (\<lambda>s. Q(s[a/x]))"
by (rule ext) (auto simp: partial_wp_def)

lemma partial_wp_partial_Seq[simp]: "partial_wp (c\<^sub>1;;c\<^sub>2) Q = partial_wp c\<^sub>1 (partial_wp c\<^sub>2 Q)"
by (rule ext) (auto simp: partial_wp_def)

lemma partial_wp_partial_If[simp]:
 "partial_wp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) Q =
 (\<lambda>s. if bval b s then partial_wp c\<^sub>1 Q s else partial_wp c\<^sub>2 Q s)"
by (rule ext) (auto simp: partial_wp_def)

lemma partial_wp_partial_While_partial_If:
 "partial_wp (WHILE b DO c) Q s =
  partial_wp (IF b THEN c;;WHILE b DO c ELSE SKIP) Q s"
unfolding partial_wp_def by (metis unfold_while)

lemma partial_wp_partial_While_True[simp]: "bval b s \<Longrightarrow>
  partial_wp (WHILE b DO c) Q s = partial_wp (c;; WHILE b DO c) Q s"
by(simp add: partial_wp_partial_While_partial_If)

lemma partial_wp_partial_While_False[simp]: "\<not> bval b s \<Longrightarrow> partial_wp (WHILE b DO c) Q s = Q s"
by(simp add: partial_wp_partial_While_partial_If)

lemma partial_wp_is_pre: "\<turnstile> {partial_wp c Q} c {Q}"
proof(induction c arbitrary: Q)
  case If thus ?case by(auto intro: partial_hoare.partial_conseq)
next
  case (While b c)
  let ?w = "WHILE b DO c"
  show "\<turnstile> {partial_wp ?w Q} ?w {Q}"
  proof(rule partial_While')
    show "\<turnstile> {\<lambda>s. partial_wp ?w Q s \<and> bval b s} c {partial_wp ?w Q}"
    proof(rule partial_strengthen_pre[OF _ While.IH])
      show "\<forall>s. partial_wp ?w Q s \<and> bval b s \<longrightarrow> partial_wp c (partial_wp ?w Q) s" by auto
    qed
    show "\<forall>s. partial_wp ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s" by auto
  qed
qed auto

lemma partial_hoare_complete: assumes "\<Turnstile> {P}c{Q}" shows "\<turnstile> {P}c{Q}"
proof(rule partial_strengthen_pre)
  show "\<forall>s. P s \<longrightarrow> partial_wp c Q s" using assms
    by (auto simp: partial_hoare_valid_def partial_wp_def)
  show "\<turnstile> {partial_wp c Q} c {Q}" by(rule partial_wp_is_pre)
qed

paragraph "Annotated commands"

datatype acom =
  Askip                  ("SKIP") |
  Aassign vname aexp     ("(_ ::= _)" [1000, 61] 61) |
  Aseq   acom acom       ("_;;/ _"  [60, 61] 60) |
  Aif bexp acom acom     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61) |
  Awhile assn bexp acom
    ("({_}/ WHILE _/ DO _)"  [0, 0, 61] 61)

bundle ACOM begin
no_notation SKIP ("SKIP")
no_notation Assign ("_ ::= _" [1000, 61] 61)
no_notation Seq    ("_;;/ _"  [60, 61] 60)
no_notation If ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
notation Askip ("SKIP")
notation Aassign ("(_ ::= _)" [1000, 61] 61)
notation Aseq ("_;;/ _"  [60, 61] 60)
notation Aif ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
end

bundle COM begin
no_notation Askip ("SKIP")
no_notation Aassign ("(_ ::= _)" [1000, 61] 61)
no_notation Aseq ("_;;/ _"  [60, 61] 60)
no_notation Aif ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
notation SKIP ("SKIP")
notation Assign ("_ ::= _" [1000, 61] 61)
notation Seq    ("_;;/ _"  [60, 61] 60)
notation If ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
end

unbundle ACOM

fun strip :: "acom \<Rightarrow> com" where
"strip SKIP = com.SKIP" |
"strip (x ::= a) = com.Assign x a" |
"strip (C\<^sub>1;; C\<^sub>2) = com.Seq (strip C\<^sub>1) (strip C\<^sub>2)" |
"strip (IF b THEN C\<^sub>1 ELSE C\<^sub>2) = com.If b (strip C\<^sub>1) (strip C\<^sub>2)" |
"strip ({_} WHILE b DO C) = com.While b (strip C)"

paragraph "VCG for partial correctness"

fun partial_pre :: "acom \<Rightarrow> assn \<Rightarrow> assn" where
"partial_pre SKIP Q = Q" |
"partial_pre (x ::= a) Q = (\<lambda>s. Q(s(x := aval a s)))" |
"partial_pre (C\<^sub>1;; C\<^sub>2) Q = partial_pre C\<^sub>1 (partial_pre C\<^sub>2 Q)" |
"partial_pre (IF b THEN C\<^sub>1 ELSE C\<^sub>2) Q =
  (\<lambda>s. if bval b s then partial_pre C\<^sub>1 Q s else partial_pre C\<^sub>2 Q s)" |
"partial_pre ({I} WHILE b DO C) Q = I"

fun vc :: "acom \<Rightarrow> assn \<Rightarrow> bool" where
"vc SKIP Q = True" |
"vc (x ::= a) Q = True" |
"vc (C\<^sub>1;; C\<^sub>2) Q = (vc C\<^sub>1 (partial_pre C\<^sub>2 Q) \<and> vc C\<^sub>2 Q)" |
"vc (IF b THEN C\<^sub>1 ELSE C\<^sub>2) Q = (vc C\<^sub>1 Q \<and> vc C\<^sub>2 Q)" |
"vc ({I} WHILE b DO C) Q =
  ((\<forall>s. (I s \<and> bval b s \<longrightarrow> partial_pre C I s) \<and>
        (I s \<and> \<not> bval b s \<longrightarrow> Q s)) \<and>
    vc C I)"

lemma vc_sound: "vc C Q \<Longrightarrow> \<turnstile> {partial_pre C Q} strip C {Q}"
proof(induction C arbitrary: Q)
  case (Awhile I b C)
  show ?case
  proof(simp, rule partial_While')
    from \<open>vc (Awhile I b C) Q\<close>
    have vc: "vc C I" and IQ: "\<forall>s. I s \<and> \<not> bval b s \<longrightarrow> Q s" and
         partial_pre: "\<forall>s. I s \<and> bval b s \<longrightarrow> partial_pre C I s" by simp_all
    have "\<turnstile> {partial_pre C I} strip C {I}" by(rule Awhile.IH[OF vc])
    with partial_pre show "\<turnstile> {\<lambda>s. I s \<and> bval b s} strip C {I}"
      by(rule partial_strengthen_pre)
    show "\<forall>s. I s \<and> \<not>bval b s \<longrightarrow> Q s" by(rule IQ)
  qed
qed (auto intro: partial_conseq)

corollary vc_sound':
  "\<lbrakk> vc C Q; \<forall>s. P s \<longrightarrow> partial_pre C Q s \<rbrakk> \<Longrightarrow> \<turnstile> {P} strip C {Q}"
by (metis partial_strengthen_pre vc_sound)

unbundle COM

paragraph "Total correctness"

definition hoare_tvalid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool"
  ("\<Turnstile>\<^sub>t {(1_)}/ (_)/ {(1_)}" 50) where
"\<Turnstile>\<^sub>t {P}c{Q}  \<longleftrightarrow>  (\<forall>s. P s \<longrightarrow> (\<exists>t. (c,s) \<Rightarrow> t \<and> Q t))"

inductive
  hoaret :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<turnstile>\<^sub>t ({(1_)}/ (_)/ {(1_)})" 50)
  where
Skip:  "\<turnstile>\<^sub>t {P} SKIP {P}"  |

Assign:  "\<turnstile>\<^sub>t {\<lambda>s. P(s[a/x])} x::=a {P}"  |

Seq: "\<lbrakk> \<turnstile>\<^sub>t {P\<^sub>1} c\<^sub>1 {P\<^sub>2}; \<turnstile>\<^sub>t {P\<^sub>2} c\<^sub>2 {P\<^sub>3} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P\<^sub>1} c\<^sub>1;;c\<^sub>2 {P\<^sub>3}"  |

If: "\<lbrakk> \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s} c\<^sub>1 {Q}; \<turnstile>\<^sub>t {\<lambda>s. P s \<and> \<not> bval b s} c\<^sub>2 {Q} \<rbrakk>
  \<Longrightarrow> \<turnstile>\<^sub>t {P} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}"  |

While:
  "(\<And>n::nat.
    \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> T s n} c {\<lambda>s. P s \<and> (\<exists>n'<n. T s n')})
   \<Longrightarrow> \<turnstile>\<^sub>t {\<lambda>s. P s \<and> (\<exists>n. T s n)} WHILE b DO c {\<lambda>s. P s \<and> \<not>bval b s}"  |

conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile>\<^sub>t {P}c{Q}; \<forall>s. Q s \<longrightarrow> Q' s  \<rbrakk> \<Longrightarrow>
           \<turnstile>\<^sub>t {P'}c{Q'}"

lemma While_fun:
  "\<lbrakk> \<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> n = f s} c {\<lambda>s. P s \<and> f s < n}\<rbrakk>
   \<Longrightarrow> \<turnstile>\<^sub>t {P} WHILE b DO c {\<lambda>s. P s \<and> \<not>bval b s}"
  by (rule While [where T="\<lambda>s n. n = f s", simplified])

lemma strengthen_pre:
  "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s;  \<turnstile>\<^sub>t {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P'} c {Q}"
by (metis conseq)

lemma weaken_post:
  "\<lbrakk> \<turnstile>\<^sub>t {P} c {Q};  \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow>  \<turnstile>\<^sub>t {P} c {Q'}"
by (metis conseq)

lemma Assign': "\<forall>s. P s \<longrightarrow> Q(s[a/x]) \<Longrightarrow> \<turnstile>\<^sub>t {P} x ::= a {Q}"
by (simp add: strengthen_pre[OF _ Assign])

lemma While_fun':
assumes "\<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> n = f s} c {\<lambda>s. P s \<and> f s < n}"
    and "\<forall>s. P s \<and> \<not> bval b s \<longrightarrow> Q s"
shows "\<turnstile>\<^sub>t {P} WHILE b DO c {Q}"
by(blast intro: assms(1) weaken_post[OF While_fun assms(2)])

theorem hoaret_sound: "\<turnstile>\<^sub>t {P}c{Q}  \<Longrightarrow>  \<Turnstile>\<^sub>t {P}c{Q}"
proof(unfold hoare_tvalid_def, induction rule: hoaret.induct)
  case (While P b T c)
  have "\<lbrakk> P s; T s n \<rbrakk> \<Longrightarrow> \<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P t \<and> \<not> bval b t" for s n
  proof(induction "n" arbitrary: s rule: less_induct)
    case (less n) thus ?case by (metis While.IH WhileFalse WhileTrue)
  qed
  thus ?case by auto
next
  case If thus ?case by auto blast
qed fastforce+

definition wpt :: "com \<Rightarrow> assn \<Rightarrow> assn" ("wp\<^sub>t") where
"wp\<^sub>t c Q  =  (\<lambda>s. \<exists>t. (c,s) \<Rightarrow> t \<and> Q t)"

lemma [simp]: "wp\<^sub>t SKIP Q = Q"
by(auto intro!: ext simp: wpt_def)

lemma [simp]: "wp\<^sub>t (x ::= e) Q = (\<lambda>s. Q(s(x := aval e s)))"
by(auto intro!: ext simp: wpt_def)

lemma [simp]: "wp\<^sub>t (c\<^sub>1;;c\<^sub>2) Q = wp\<^sub>t c\<^sub>1 (wp\<^sub>t c\<^sub>2 Q)"
unfolding wpt_def
apply(rule ext)
apply auto
done

lemma [simp]:
 "wp\<^sub>t (IF b THEN c\<^sub>1 ELSE c\<^sub>2) Q = (\<lambda>s. wp\<^sub>t (if bval b s then c\<^sub>1 else c\<^sub>2) Q s)"
apply(unfold wpt_def)
apply(rule ext)
apply auto
  done

inductive Its :: "bexp \<Rightarrow> com \<Rightarrow> state \<Rightarrow> nat \<Rightarrow> bool" where
Its_0: "\<not> bval b s \<Longrightarrow> Its b c s 0" |
Its_Suc: "\<lbrakk> bval b s;  (c,s) \<Rightarrow> s';  Its b c s' n \<rbrakk> \<Longrightarrow> Its b c s (Suc n)"

lemma Its_fun: "Its b c s n \<Longrightarrow> Its b c s n' \<Longrightarrow> n=n'"
proof(induction arbitrary: n' rule:Its.induct)
  case Its_0 thus ?case by(metis Its.cases)
next
  case Its_Suc thus ?case by(metis Its.cases big_step_determ)
qed

lemma WHILE_Its: "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> \<exists>n. Its b c s n"
proof(induction "WHILE b DO c" s t rule: big_step_induct)
  case WhileFalse thus ?case by (metis Its_0)
next
  case WhileTrue thus ?case by (metis Its_Suc)
qed

lemma wpt_is_pre: "\<turnstile>\<^sub>t {wp\<^sub>t c Q} c {Q}"
proof (induction c arbitrary: Q)
  case SKIP show ?case by (auto intro:hoaret.Skip)
next
  case Assign show ?case by (auto intro:hoaret.Assign)
next
  case Seq thus ?case by (auto intro:hoaret.Seq)
next
  case If thus ?case by (auto intro:hoaret.If hoaret.conseq)
next
  case (While b c)
  let ?w = "WHILE b DO c"
  let ?T = "Its b c"
  have 1: "\<forall>s. wp\<^sub>t ?w Q s \<longrightarrow> wp\<^sub>t ?w Q s \<and> (\<exists>n. Its b c s n)"
    unfolding wpt_def by (metis WHILE_Its)
  let ?R = "\<lambda>n s'. wp\<^sub>t ?w Q s' \<and> (\<exists>n'<n. ?T s' n')"
  have "\<forall>s. wp\<^sub>t ?w Q s \<and> bval b s \<and> ?T s n \<longrightarrow> wp\<^sub>t c (?R n) s" for n
  proof -
    have "wp\<^sub>t c (?R n) s" if "bval b s" and "?T s n" and "(?w, s) \<Rightarrow> t" and "Q t" for s t
    proof -
      from \<open>bval b s\<close> and \<open>(?w, s) \<Rightarrow> t\<close> obtain s' where
        "(c,s) \<Rightarrow> s'" "(?w,s') \<Rightarrow> t" by auto
      from \<open>(?w, s') \<Rightarrow> t\<close> obtain n' where "?T s' n'"
        by (blast dest: WHILE_Its)
      with \<open>bval b s\<close> and \<open>(c, s) \<Rightarrow> s'\<close> have "?T s (Suc n')" by (rule Its_Suc)
      with \<open>?T s n\<close> have "n = Suc n'" by (rule Its_fun)
      with \<open>(c,s) \<Rightarrow> s'\<close> and \<open>(?w,s') \<Rightarrow> t\<close> and \<open>Q t\<close> and \<open>?T s' n'\<close>
      show ?thesis by (auto simp: wpt_def)
    qed
    thus ?thesis
      unfolding wpt_def by auto
  qed
  note 2 = hoaret.While[OF strengthen_pre[OF this While.IH]]
  have "\<forall>s. wp\<^sub>t ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s"
    by (auto simp add:wpt_def)
  with 1 2 show ?case by (rule conseq)
qed

theorem hoaret_complete: "\<Turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<turnstile>\<^sub>t {P}c{Q}"
apply(rule strengthen_pre[OF _ wpt_is_pre])
apply(auto simp: hoare_tvalid_def wpt_def)
done

corollary hoaret_sound_complete: "\<turnstile>\<^sub>t {P}c{Q} \<longleftrightarrow> \<Turnstile>\<^sub>t {P}c{Q}"
by (metis hoaret_sound hoaret_complete)

paragraph "Extra:"

lemma total_imp_partial: "\<turnstile>\<^sub>t {P} c {Q} \<Longrightarrow> \<turnstile> {P} c {Q}"
proof -
  assume "\<turnstile>\<^sub>t {P} c {Q}"
  then have "\<Turnstile>\<^sub>t {P} c {Q}" by (auto simp: hoaret_sound_complete)
  then have "\<Turnstile> {P} c {Q}"
    unfolding partial_hoare_valid_def hoare_tvalid_def using big_step_determ by blast
  thus "\<turnstile> {P} c {Q}"
    by (simp add: partial_hoare_complete)
qed


paragraph \<open>Square Root Program\<close>

unbundle COM

definition "SQRT_vars \<equiv> {''L'',''R'',''M''}"

(*takes lower and upper bound for root*)
definition SQRT :: com where
"SQRT \<equiv>
  ''L'' ::= N 0;;
  ''R'' ::= Plus (V ''x'') (N 1);;
  WHILE (Less (Plus (V ''L'') (N 1)) (V ''R'')) DO (
    ''M'' ::= Div (Plus (V ''L'') (V ''R'')) (N 2);;
    IF (Less (V ''x'') (Mul (V ''M'') (V ''M'')))
    THEN (''R'' ::= V ''M'')
    ELSE (''L'' ::= V ''M''))"

unbundle ACOM

definition SQRT_annot :: "(state \<Rightarrow> assn) \<Rightarrow> state \<Rightarrow> acom" where
"SQRT_annot invar sorig \<equiv>
  ''L'' ::= N 0;;
  ''R'' ::= Plus (V ''x'') (N 1);;
  {invar sorig} WHILE (Less (Plus (V ''L'') (N 1)) (V ''R'')) DO (
    ''M'' ::= Div (Plus (V ''L'') (V ''R'')) (N 2);;
    IF (Less (V ''x'') (Mul (V ''M'') (V ''M'')))
    THEN (''R'' ::= V ''M'')
    ELSE (''L'' ::= V ''M''))"

unbundle COM

lemma SQRT_annot_strip: "strip (SQRT_annot invar sorig) = SQRT"
  unfolding SQRT_annot_def SQRT_def
  by auto



consts SQRT_invar :: "state \<Rightarrow> assn"

consts SQRT_measure :: "state \<Rightarrow> nat"


end

Template File

theory Submission
  imports Defs
begin

definition SQRT_invar :: "state \<Rightarrow> assn"  where
  "SQRT_invar _ _ = True"

theorem SQRT_partially_correct:
  "\<turnstile> {\<lambda>s. s=sorig \<and> 0 \<le> s ''x''}
    SQRT
    {\<lambda>s. (s ''L'')^2 \<le> s ''x'' \<and> s ''x'' < (s ''L'' + 1)^2 \<and> (\<forall>v. v \<notin> SQRT_vars \<longrightarrow> s v = sorig v)}"
  (*Do not changes these lines*)
  apply (subst SQRT_annot_strip[of SQRT_invar sorig, symmetric])
  apply (rule vc_sound')
  (*Complete the proof*)
sorry

definition SQRT_measure :: "state \<Rightarrow> nat"  where
  "SQRT_measure _ = 0"

lemma SQRT_measure_correct:
    assumes "s ''L'' + 1 < s ''R''"
  shows "s ''x'' < ((s ''L'' + s ''R'') div 2)^2 \<Longrightarrow>
    SQRT_measure (s(''M'' := (s ''L'' + s ''R'') div 2, ''R'' := (s ''L'' + s ''R'') div 2))
    < SQRT_measure s"
  and "\<not>(s ''x'' < ((s ''L'' + s ''R'') div 2)^2) \<Longrightarrow>
    SQRT_measure (s(''M'' := (s ''L'' + s ''R'') div 2, ''L'' := (s ''L'' + s ''R'') div 2))
    < SQRT_measure s"
sorry

end

Check File

theory Check
  imports Submission
begin

theorem SQRT_partially_correct: "\<turnstile> {\<lambda>s. s=sorig \<and> 0 \<le> s ''x''}
    SQRT
    {\<lambda>s. (s ''L'')^2 \<le> s ''x'' \<and> s ''x'' < (s ''L'' + 1)^2 \<and> (\<forall>v. v \<notin> SQRT_vars \<longrightarrow> s v = sorig v)}"
  by (rule Submission.SQRT_partially_correct)

lemma SQRT_measure_correct: "(s ''L'' + 1 < s ''R'') \<Longrightarrow> s ''x'' < ((s ''L'' + s ''R'') div 2)^2 \<Longrightarrow>
    SQRT_measure (s(''M'' := (s ''L'' + s ''R'') div 2, ''R'' := (s ''L'' + s ''R'') div 2))
    < SQRT_measure s"
  by (rule Submission.SQRT_measure_correct)

end

Terms and Conditions