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.
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
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
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