theory Loading
imports Main

begin

ML {* quick_and_dirty := true *}

consts
  load_list_basic :: "nat \<Rightarrow> nat \<Rightarrow> nat list"

lemma load_list_basic_app [simp]:
  "load_list_basic (Suc n) p = p # load_list_basic n (p + 1)"
  sorry

lemma smbaL_load_list_basic2:
  assumes lens: "length bs = sz"
  assumes pmap: "P p sz bs"
  shows "load_list_basic sz p = Z"
using lens pmap proof (induct sz arbitrary: bs p)
  case 0 thus ?case sorry
next
  case (Suc sz)
  hence IH: "\<And>bs p. \<lbrakk>length bs = sz; P p sz bs\<rbrakk>
                      \<Longrightarrow> load_list_basic sz p = Z"
    by auto

  show ?case
    apply -
    apply simp
    apply (subst IH)
    sorry
qed

end