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 10

This is the task corresponding to homework 10.

Resources

Download Files

Definitions File

theory Defs
  imports "HOL-IMP.Big_Step" "HOL-Library.Extended_Nat"
begin

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

declare [[syntax_ambiguity_warning = false]]

code_pred big_step_t .

declare big_step_t.intros[intro]

thm big_step_t.induct

lemmas big_step_t_induct = big_step_t.induct[split_format(complete)]
thm big_step_t_induct

inductive_cases Skip_tE[elim!]: "(SKIP,s) \<Rightarrow>^x t"
inductive_cases Assign_tE[elim!]: "(x ::= a,s) \<Rightarrow>^p t"
inductive_cases Seq_tE[elim!]: "(c\<^sub>1;;c\<^sub>2,s\<^sub>1) \<Rightarrow>^p s\<^sub>3"
inductive_cases If_tE[elim!]: "(IF b THEN c\<^sub>1 ELSE c\<^sub>2,s) \<Rightarrow>^x t"
inductive_cases While_tE[elim]: "(WHILE b DO c,s) \<Rightarrow>^x t"

type_synonym assn = "state \<Rightarrow> bool"
type_synonym qassn = "state \<Rightarrow> enat"

fun emb :: "bool \<Rightarrow> enat" ("\<down>") where
   "emb False = \<infinity>"
 | "emb True = 0"


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



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

inductive hoareQ :: "qassn \<Rightarrow> com \<Rightarrow> qassn \<Rightarrow> bool" ("\<turnstile>\<^sub>Q ({(1_)}/ (_)/ {(1_)})" 50) where

SkipQ:  "\<turnstile>\<^sub>Q {\<lambda>s. eSuc (P s)} SKIP {P}"  |
AssignQ:  "\<turnstile>\<^sub>Q {\<lambda>s. eSuc (P (s[a/x]))} x::=a {P}"  |

IfQ: "\<lbrakk> \<turnstile>\<^sub>Q {\<lambda>s. P s + \<down>( bval b s)} c\<^sub>1 {Q};
       \<turnstile>\<^sub>Q {\<lambda>s. P s + \<down>(\<not> bval b s)} c\<^sub>2 {Q} \<rbrakk>
  \<Longrightarrow> \<turnstile>\<^sub>Q {\<lambda>s. eSuc (P s)} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}"  |

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

WhileQ:
  "\<turnstile>\<^sub>Q {\<lambda>s. I s + \<down>(bval b s)} c {\<lambda>t. I t + 1}
   \<Longrightarrow> \<turnstile>\<^sub>Q {\<lambda>s. I s + 1} WHILE b DO c {\<lambda>s. I s + \<down>(\<not> bval b s)}" |

conseqQ: "\<lbrakk> \<turnstile>\<^sub>Q {P} c {Q}; \<And>s. P s \<le> P' s; \<And>s. Q' s \<le> Q s \<rbrakk> \<Longrightarrow>
           \<turnstile>\<^sub>Q {P'} c {Q'}"

lemma strengthen_pre: "\<lbrakk> \<forall>s. P s \<le> P' s;  \<turnstile>\<^sub>Q {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>Q {P'} c {Q}"
  using conseqQ by blast

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


definition wsum :: com where
"wsum =
  ''y'' ::= N 0;;
  WHILE Less (N 0) (V ''x'')
  DO (''y'' ::= Plus (V ''y'') (V ''x'');;
      ''x'' ::= Plus (V ''x'') (N (- 1)))"

end

Template File

theory Submission
  imports Defs
begin

value "3::enat" \<comment>\<open>3\<close>
value "\<infinity>::enat" \<comment>\<open>\<open>\<infinity>\<close>\<close>
value "(3::enat) + 4" \<comment>\<open>7\<close>
value "(3::enat) + \<infinity>" \<comment>\<open>\<open>\<infinity>\<close>\<close>
value "eSuc 3" \<comment>\<open>4\<close>
value "eSuc \<infinity>" \<comment>\<open>\<open>\<infinity>\<close>\<close>


theorem wsum: "\<turnstile>\<^sub>Q {\<lambda>s. enat (2 + 3*n) + \<down> (s ''x'' = int n)} wsum {\<lambda>s. 0}"
unfolding wsum_def
apply(rule SeqQ[rotated])
 apply(rule conseqQ)
   apply(rule WhileQ[where I="\<lambda>s. enat (3 * nat (s ''x''))"])
sorry



lemma Skip_sound: "\<Turnstile>\<^sub>Q {\<lambda>a. eSuc (P a)} SKIP {P}"
unfolding hoare_Qvalid_def proof (safe)
  fix s assume "eSuc (P s) < \<infinity>"
  then have "(SKIP, s) \<Rightarrow>^1 s \<and> enat 1 + P s \<le> eSuc (P s)"
    using Skip  eSuc_def by (auto split: enat.splits)
  thus "\<exists>t n. (SKIP, s) \<Rightarrow>^n t \<and> enat n + P t \<le> eSuc (P s)"
    by blast
qed


theorem Assign_sound: "\<Turnstile>\<^sub>Q {\<lambda>b. eSuc (P (b[a/x]))} x::=a {P}"
  sorry

theorem conseq_sound:
    assumes hypP: "\<And>s. P s \<le> P' s"
      and hypQ: "\<And>s. Q' s \<le> Q s"
      and IH: "\<Turnstile>\<^sub>Q {P} c {Q}"
  shows "\<Turnstile>\<^sub>Q {P'} c {Q'}"
  sorry

theorem If_sound:
    assumes "\<Turnstile>\<^sub>Q {\<lambda>a. P a + \<down> (bval b a)} c\<^sub>1 {Q}"
      and " \<Turnstile>\<^sub>Q {\<lambda>a. P a + \<down> (\<not> bval b a)} c\<^sub>2 {Q}"
  shows "\<Turnstile>\<^sub>Q {\<lambda>a. eSuc (P a)} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}"
  sorry

theorem Seq_sound:
    assumes "\<Turnstile>\<^sub>Q {P\<^sub>1} c\<^sub>1 {P\<^sub>2}"
      and "\<Turnstile>\<^sub>Q {P\<^sub>2} c\<^sub>2 {P\<^sub>3}"
  shows "\<Turnstile>\<^sub>Q {P\<^sub>1} c\<^sub>1;;c\<^sub>2 {P\<^sub>3}"
  sorry

theorem While_sound: 
    assumes "\<Turnstile>\<^sub>Q {\<lambda>s. INV s + \<down>(bval b s)} c {\<lambda>t. INV t + 1}"
  shows "\<Turnstile>\<^sub>Q {\<lambda>s. INV s + 1} WHILE b DO c {\<lambda>s. INV s + \<down>(\<not> bval b s)}"
  sorry

end

Check File

theory Check
  imports Submission
begin

theorem wsum: "\<turnstile>\<^sub>Q {\<lambda>s. enat (2 + 3*n) + \<down> (s ''x'' = int n)} wsum {\<lambda>s. 0}"
  by (rule Submission.wsum)

theorem Assign_sound: "\<Turnstile>\<^sub>Q {\<lambda>b. eSuc (P (b[a/x]))} x::=a {P}"
  by (rule Submission.Assign_sound)

theorem conseq_sound: "(\<And>s. P s \<le> P' s) \<Longrightarrow> (\<And>s. Q' s \<le> Q s) \<Longrightarrow> (\<Turnstile>\<^sub>Q {P} c {Q}) \<Longrightarrow> \<Turnstile>\<^sub>Q {P'} c {Q'}"
  by (rule Submission.conseq_sound)

theorem If_sound: "(\<Turnstile>\<^sub>Q {\<lambda>a. P a + \<down> (bval b a)} c\<^sub>1 {Q}) \<Longrightarrow> ( \<Turnstile>\<^sub>Q {\<lambda>a. P a + \<down> (\<not> bval b a)} c\<^sub>2 {Q}) \<Longrightarrow> \<Turnstile>\<^sub>Q {\<lambda>a. eSuc (P a)} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}"
  by (rule Submission.If_sound)

theorem Seq_sound: "(\<Turnstile>\<^sub>Q {P\<^sub>1} c\<^sub>1 {P\<^sub>2}) \<Longrightarrow> (\<Turnstile>\<^sub>Q {P\<^sub>2} c\<^sub>2 {P\<^sub>3}) \<Longrightarrow> \<Turnstile>\<^sub>Q {P\<^sub>1} c\<^sub>1;;c\<^sub>2 {P\<^sub>3}"
  by (rule Submission.Seq_sound)

theorem While_sound: "(\<Turnstile>\<^sub>Q {\<lambda>s. INV s + \<down>(bval b s)} c {\<lambda>t. INV t + 1}) \<Longrightarrow> \<Turnstile>\<^sub>Q {\<lambda>s. INV s + 1} WHILE b DO c {\<lambda>s. INV s + \<down>(\<not> bval b s)}"
  by (rule Submission.While_sound)

end

Terms and Conditions