theory Test
imports Main
begin

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

function f :: "nat \<Rightarrow> nat list \<Rightarrow> nat list"
     and foldr_f :: "[nat list, nat list] \<Rightarrow> nat list"
where
  "f k ks = (if k \<in> set ks then ks else foldr_f (g k) (k#ks))"
| "foldr_f [] a = a"
| "foldr_f (x#xs) a = f x (foldr_f xs a)"
by pat_completeness auto

consts lim :: "[nat, nat list] \<Rightarrow> nat set"
       --"lim takes the arguments of f and calculates all reachable nodes"

lemma lim_finite: "finite (lim k ks)"
sorry

lemma lim_eq: "lim k (k#ks) = lim k ks"
sorry

lemma lim_subset: "set ks \<subseteq> lim k ks" sorry

lemma lim_concat: "lim k (xs@ys) = lim k xs \<union> lim k ys" sorry

lemma lim_append: "lim k (x#xs) = lim k [x] \<union> lim k xs" using lim_concat[of k "[x]" xs] by auto

lemma lim_mem: "k\<in>set ks \<Longrightarrow> lim l (k#ks) = lim l ks" sorry


lemma subset_prop':
      "f_foldr_f_dom (Inl (k, a)) \<Longrightarrow> set a \<subseteq> set (f k a) \<and> lim l (f k a) = lim l (k#a)"
      "f_foldr_f_dom (Inr (ks, a)) \<Longrightarrow> set a \<subseteq> set (foldr_f ks a) \<and> lim l (foldr_f ks a) = lim l (ks@a)"
proof (induct a and a rule: f_foldr_f.pinduct)
  case goal1 thus ?case
  proof(cases "k\<in>set ks")
    case goal1 thus ?case using lim_mem by simp
  next
    case goal2
      hence "lim l (g k @ k # ks) = lim l (k#ks)" sorry
      --"This should be true, since lim should contain all 'child nodes' that are calculated by g."
      --"Therefore the right hand side should contain 'g k' implicitly."
      thus ?case using goal2 by simp
  qed
next
  case goal2 thus ?case by auto
next
  case (goal3 k' )
    have "lim l (k' # xs @ a) = lim l [k'] \<union> lim l (xs @ a)" using lim_append by blast
    moreover with goal3 have "\<dots> = lim l [k'] \<union> lim l (foldr_f xs a)" by auto
    moreover have "\<dots> = lim l (k' # foldr_f xs a)" using lim_append by blast
    moreover have "\<dots> = lim l (f k' (foldr_f xs a))" using goal3 by auto
    ultimately have "lim l (f k' (foldr_f xs a)) = lim l (k' # xs @ a)" by simp
    thus ?case using goal3 by auto
qed


lemma subset_prop: 
  assumes "f_foldr_f_dom (Inr (ks, a))"
    shows "set a \<subseteq> set (foldr_f ks a)"
      and "lim k (foldr_f ks a) = lim k (ks@a)"
using prems subset_prop' by auto


abbreviation
  "my_term_ord \<equiv>
     inv_image (finite_psubset <*lex*> less_than) (\<lambda>v. (case v of (Inr (ys, ks)) \<Rightarrow> (lim (hd ks) (ks@ys) - set ks, size ys)
                                                                | (Inl (k, ks)) \<Rightarrow> (lim k ks - set ks, 0) ))"


lemma in_finite_psubset[simp]:
  "((A, B) \<in> finite_psubset) = (A \<subset> B \<and> finite B)"
unfolding finite_psubset_def by simp


termination
proof (relation "my_term_ord")
  case goal1 thus ?case by (auto intro: wf_finite_psubset)
next
  case (goal2 k ks)
    hence "lim k (k#ks) - insert k (set ks) \<subset> lim k ks - set ks"
    unfolding lim_eq sorry --"easy to proof"
    moreover have "finite (lim k ks - set ks)" using lim_finite by auto
    moreover have "lim k (k # ks) = lim k (k # ks @ g k)" sorry --"see above"
    ultimately show ?case by simp
next
  case (goal3 k ks a) thus ?case apply simp sorry --"easy to proof"
next
  case (goal4 k ks a)
    hence "set a \<subseteq> set (foldr_f ks a)"
      and "lim k (foldr_f ks a) = lim k (ks@a)" using subset_prop by auto
    moreover have "lim (hd a) (a @ k # ks) = lim k (ks@a)" sorry -- "easy to proof"
    ultimately show ?case apply simp sorry -- "again easy, use the premise"
qed


end