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 09

This is the task corresponding to homework 09.

## Resources

### Definitions File

```theory Defs
imports "IMP2.Examples"
begin

lemma [named_ss vcg_bb]:
"lhsv (Inline c) = lhsv c"
unfolding Inline_def ..

lemma lran_split:
"lran a l h = lran a l p @ lran a p h" if "l \<le> p" "p \<le> h"
using that by (induction p; simp; simp add: lran.simps)

lemma lran_eq_iff':
"lran a l h = as @ bs \<longleftrightarrow> (\<exists> i. l \<le> i \<and> i \<le> h \<and> as = lran a l i \<and> bs = lran a i h)" if "l \<le> h"
apply safe
subgoal
using that
proof (induction as arbitrary: l)
case Nil
then show ?case
by auto
next
case (Cons x as)
from this(2-) have "lran a (l + 1) h = as @ bs" "a l = x" "l + 1 \<le> h"
apply -
subgoal
by simp
subgoal
by (smt append_Cons list.inject lran.simps lran_append1)
subgoal
done
from Cons.IH[OF this(1,3)] guess i by safe
note IH = this
with \<open>a l = x\<close> show ?case
apply (intro exI[where x = i])
apply auto
by (smt IH(3) lran_prepend1)
qed
apply (subst lran_split; simp)
done

end```

### Template File

```theory Submission
imports Defs
begin

theorem array_assign: "(x[] ::= a;; a[] ::= x) \<sim> (x[] ::= a)"
sorry

theorem
"(x[i] ::= Vidx a j;; a[j] ::= Vidx x i) \<sim> (x[i] ::= Vidx a j)"
oops

program_spec partition
assumes "l\<le>h"
ensures "mset_ran a {l\<^sub>0..<i} = filter_mset (\<lambda>x. x \<ge> 0) (mset_ran a\<^sub>0 {l\<^sub>0..<h\<^sub>0})
\<and> mset_ran a {i..<h\<^sub>0} = filter_mset (\<lambda>x. x < 0) (mset_ran a\<^sub>0 {l\<^sub>0..<h\<^sub>0})"
defines
\<open>
a[] = a;
i = 0;
j = l;
i = h;
temp = i
\<close>
sorry

program_spec substring_final
assumes "l \<le> h \<and> 0 \<le> len"
ensures "match = 1 \<longleftrightarrow> (\<exists>as bs. lran a l\<^sub>0 h\<^sub>0 = as @ lran b 0 len @ bs)"
for l h len match a[] b[]
defines \<open>
match = 1
\<close>
sorry

end```

### Check File

```theory Check
imports Submission
begin

theorem array_assign: "(x[] ::= a;; a[] ::= x) \<sim> (x[] ::= a)"
by (rule Submission.array_assign)

theorem partition_spec:
"HT_mods {''j'', ''a'', ''i'', ''temp''} (\<lambda>\<ss>. VAR (\<ss> ''l'' 0) (\<lambda>l. VAR (\<ss> ''h'' 0) (\<lambda>s. BB_PROTECT (l \<le> s)))) partition
(\<lambda>\<ss>\<^sub>0 \<ss>.
VAR (\<ss>\<^sub>0 ''l'' 0)
(\<lambda>l\<^sub>0. VAR (\<ss>\<^sub>0 ''h'' 0)
(\<lambda>h\<^sub>0. VAR (\<ss>\<^sub>0 ''a'')
(\<lambda>a\<^sub>0. VAR (\<ss> ''i'' 0)
(\<lambda>i. VAR (\<ss> ''a'')
(\<lambda>a. BB_PROTECT
(mset_ran a {l\<^sub>0..<i} = filter_mset ((\<le>) 0) (mset_ran a\<^sub>0 {l\<^sub>0..<h\<^sub>0}) \<and>
mset_ran a {i..<h\<^sub>0} = {#x \<in># mset_ran a\<^sub>0 {l\<^sub>0..<h\<^sub>0}. x < 0#})))))))"
by (rule Submission.partition_spec)

end```

Terms and Conditions