Homework 09

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
        using add1_zle_eq by fastforce
      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