Theory CoCallGraph-TTree

theory "CoCallGraph-TTree"
imports CoCallGraph "TTree-HOLCF"
begin

lemma interleave_ccFromList:
  "xs ∈ interleave ys zs ⟹ ccFromList xs = ccFromList ys ⊔ ccFromList zs ⊔ ccProd (set ys) (set zs)"
  by (induction rule: interleave_induct)
     (auto simp add: interleave_set ccProd_comm ccProd_insert2[where S' = "set xs" for xs]  ccProd_insert1[where S' = "set xs" for xs] )


lift_definition ccApprox :: "var ttree ⇒ CoCalls"
  is "λ xss .  lub (ccFromList ` xss)".

lemma ccApprox_paths: "ccApprox t = lub (ccFromList ` (paths t))" by transfer simp

lemma ccApprox_strict[simp]: "ccApprox ⊥ = ⊥"
  by (simp add: ccApprox_paths empty_is_bottom[symmetric])

lemma in_ccApprox: "(x--y∈(ccApprox t)) ⟷ (∃ xs ∈ paths t. (x--y∈(ccFromList xs)))"
  unfolding ccApprox_paths
  by transfer auto

lemma ccApprox_mono: "paths t ⊆ paths t' ⟹ ccApprox t ⊑ ccApprox t'"
  by (rule below_CoCallsI) (auto simp add: in_ccApprox)

lemma ccApprox_mono': "t ⊑  t' ⟹ ccApprox t ⊑ ccApprox t'"
  by (metis below_set_def ccApprox_mono paths_mono_iff)

lemma ccApprox_belowI: "(⋀ xs. xs ∈ paths t ⟹ ccFromList xs ⊑ G) ⟹ ccApprox t ⊑ G"
  unfolding ccApprox_paths
  by transfer auto

lemma ccApprox_below_iff: "ccApprox t ⊑ G ⟷ (∀ xs ∈ paths t. ccFromList xs ⊑ G)"
  unfolding ccApprox_paths by transfer auto

lemma cc_restr_ccApprox_below_iff: "cc_restr S (ccApprox t) ⊑ G ⟷ (∀ xs ∈ paths t. cc_restr S (ccFromList xs) ⊑ G)"
  unfolding ccApprox_paths cc_restr_lub
  by transfer auto

lemma ccFromList_below_ccApprox:
  "xs ∈ paths t ⟹ ccFromList xs ⊑ ccApprox t" 
by (rule below_CoCallsI)(auto simp add: in_ccApprox)

lemma ccApprox_nxt_below:
  "ccApprox (nxt t x) ⊑ ccApprox t"
by (rule below_CoCallsI)(auto simp add: in_ccApprox paths_nxt_eq elim!:  bexI[rotated])

lemma ccApprox_ttree_restr_nxt_below:
  "ccApprox (ttree_restr S (nxt t x)) ⊑ ccApprox (ttree_restr S t)"
by (rule below_CoCallsI)
   (auto simp add: in_ccApprox filter_paths_conv_free_restr[symmetric] paths_nxt_eq  elim!:  bexI[rotated])

lemma ccApprox_ttree_restr[simp]: "ccApprox (ttree_restr S t) = cc_restr S (ccApprox t)"
  by (rule CoCalls_eqI) (auto simp add: in_ccApprox filter_paths_conv_free_restr[symmetric] )

lemma ccApprox_both: "ccApprox (t ⊗⊗ t') = ccApprox t ⊔ ccApprox t' ⊔ ccProd (carrier t) (carrier t')"
proof (rule below_antisym)
  show "ccApprox (t ⊗⊗ t') ⊑ ccApprox t ⊔ ccApprox t' ⊔ ccProd (carrier t) (carrier t')"
  by (rule below_CoCallsI)
     (auto 4 4  simp add: in_ccApprox paths_both Union_paths_carrier[symmetric]  interleave_ccFromList)
next
  have "ccApprox t ⊑ ccApprox (t ⊗⊗ t')"
    by (rule ccApprox_mono[OF both_contains_arg1])
  moreover
  have "ccApprox t' ⊑ ccApprox (t ⊗⊗ t')"
    by (rule ccApprox_mono[OF both_contains_arg2])
  moreover
  have "ccProd (carrier t) (carrier t') ⊑ ccApprox (t ⊗⊗ t')"
  proof(rule ccProd_belowI)
    fix x y
    assume "x ∈ carrier t" and "y ∈ carrier t'"
    then obtain xs ys where "x ∈ set xs" and "y ∈ set ys"
      and "xs ∈ paths t" and "ys ∈ paths t'" by (auto simp add: Union_paths_carrier[symmetric])
    hence "xs @ ys ∈ paths (t ⊗⊗ t')" by (metis paths_both append_interleave)
    moreover
    from ‹x ∈ set xs› ‹y ∈ set ys›
    have "x--y∈(ccFromList (xs@ys))" by simp
    ultimately
    show "x--y∈(ccApprox (t ⊗⊗ t'))" by (auto simp add: in_ccApprox simp del: ccFromList_append)
  qed
  ultimately
  show "ccApprox t ⊔ ccApprox t' ⊔ ccProd (carrier t) (carrier t') ⊑ ccApprox (t ⊗⊗ t')"
    by (simp add: join_below_iff)
qed

lemma ccApprox_many_calls[simp]:
  "ccApprox (many_calls x) = ccProd {x} {x}"
  by transfer' (rule CoCalls_eqI, auto)

lemma ccApprox_single[simp]:
  "ccApprox (TTree.single y) = ⊥"
  by transfer' auto

lemma ccApprox_either[simp]: "ccApprox (t ⊕⊕ t') = ccApprox t ⊔ ccApprox t'"
  by transfer' (rule CoCalls_eqI, auto)

(* could work, but tricky
lemma ccApprox_lub_nxt: "ccApprox t = (⨆ x ∈UNIV. ccApprox (nxt t x) ⊔ (ccProd {x} (carrier (nxt t x))))"
*)

lemma wild_recursion:
  assumes "ccApprox  t ⊑ G"
  assumes "⋀ x. x ∉ S ⟹ f x = empty"
  assumes "⋀ x. x ∈ S ⟹ ccApprox (f x) ⊑ G"
  assumes "⋀ x. x ∈ S ⟹ ccProd (ccNeighbors x G) (carrier (f x)) ⊑ G"
  shows "ccApprox (ttree_restr (-S) (substitute f T t)) ⊑ G"
proof(rule ccApprox_belowI)
  fix xs
  define seen :: "var set" where "seen = {}"

  assume "xs ∈ paths (ttree_restr (- S) (substitute f T t))"
  then obtain xs' xs'' where "xs = [x←xs' . x ∉ S]" and "substitute'' f T xs'' xs'" and "xs'' ∈ paths t"
    by (auto simp add: filter_paths_conv_free_restr2[symmetric] substitute_substitute'')
 
  note this(2)
  moreover
  from ‹ccApprox t ⊑ G› and ‹xs'' ∈ paths t›
  have  "ccFromList xs'' ⊑ G"
    by (auto simp add: ccApprox_below_iff)
  moreover
  note assms(2)
  moreover
  from assms(3,4)
  have "⋀ x ys. x ∈ S ⟹ ys ∈ paths (f x) ⟹ ccFromList ys ⊑ G"
    and "⋀ x ys. x ∈ S ⟹ ys ∈ paths (f x) ⟹ ccProd (ccNeighbors x G) (set ys) ⊑ G"
    by (auto simp add: ccApprox_below_iff Union_paths_carrier[symmetric] cc_lub_below_iff)
  moreover
  have "ccProd seen (set xs'') ⊑ G" unfolding seen_def by simp
  ultimately 
  have "ccFromList [x←xs' . x ∉ S] ⊑ G ∧ ccProd (seen) (set xs') ⊑ G"
  proof(induction f T xs'' xs' arbitrary: seen rule: substitute''.induct[case_names Nil Cons])
  case Nil thus ?case by simp
  next
  case (Cons zs f x xs' xs T ys)
    
    have seen_x: "ccProd seen {x} ⊑ G"
      using ‹ccProd seen (set (x # xs)) ⊑ G›
      by (auto simp add: ccProd_insert2[where S' = "set xs" for xs] join_below_iff)

    show ?case
    proof(cases "x ∈ S")
      case True

      from ‹ccFromList (x # xs) ⊑ G›
      have "ccProd {x} (set xs) ⊑ G" by (auto simp add: join_below_iff)
      hence subset1: "set xs ⊆ ccNeighbors x G" by transfer auto

      from ‹ccProd seen (set (x # xs)) ⊑ G›
      have subset2: "seen  ⊆ ccNeighbors x G"
        by (auto simp add: subset_ccNeighbors ccProd_insert2[where S' = "set xs" for xs] join_below_iff ccProd_comm)

      from subset1 and subset2
      have "seen ∪ set xs ⊆ ccNeighbors x G" by auto
      hence "ccProd (seen ∪ set xs) (set zs) ⊑ ccProd (ccNeighbors x G) (set zs)"
        by (rule ccProd_mono1)
      also
      from ‹x ∈ S›  ‹zs ∈ paths (f x)›
      have "… ⊑ G"
        by (rule Cons.prems(4))
      finally
      have "ccProd (seen ∪ set xs) (set zs) ⊑ G" by this simp
     
      with ‹x ∈ S› Cons.prems Cons.hyps
      have "ccFromList [x←ys . x ∉ S] ⊑ G ∧ ccProd (seen) (set ys) ⊑ G"
          apply -
          apply (rule Cons.IH)
          apply (auto simp add: f_nxt_def  join_below_iff  interleave_ccFromList interleave_set  ccProd_insert2[where S' = "set xs" for xs]
                  split: if_splits)
          done
      with  ‹x ∈ S›  seen_x
      show "ccFromList [x←x # ys . x ∉ S] ⊑ G  ∧ ccProd seen (set (x#ys)) ⊑ G" 
          by (auto simp add: ccProd_insert2[where S' = "set xs" for xs] join_below_iff)
    next
      case False

      from False Cons.prems Cons.hyps
      have *: "ccFromList [x←ys . x ∉ S] ⊑ G ∧ ccProd ((insert x seen)) (set ys) ⊑ G"
        apply -
        apply (rule Cons.IH[where seen = "insert x seen"])
        apply (auto simp add: ccApprox_both join_below_iff ttree_restr_both interleave_ccFromList insert_Diff_if
                   simp add:  ccProd_insert2[where S' = "set xs" for xs]
                   simp add:  ccProd_insert1[where S' = "seen"])
        done
      moreover
      from False *
      have "ccProd {x} (set ys) ⊑  G"
        by (auto simp add: insert_Diff_if ccProd_insert1[where S' = "seen"] join_below_iff)
      hence "ccProd {x} {x ∈ set ys. x ∉ S} ⊑ G"
        by (rule below_trans[rotated, OF _ ccProd_mono2]) auto
      moreover
      note False seen_x
      ultimately
      show "ccFromList [x←x # ys . x ∉ S] ⊑ G ∧ ccProd (seen) (set (x # ys)) ⊑ G"
        by (auto simp add: join_below_iff  simp add: insert_Diff_if  ccProd_insert2[where S' = "set xs" for xs]   ccProd_insert1[where S' = "seen"])
    qed
  qed
  with ‹xs = _›
  show "ccFromList xs ⊑ G" by simp
qed

lemma wild_recursion_thunked:
  assumes "ccApprox  t ⊑ G"
  assumes "⋀ x. x ∉ S ⟹ f x = empty"
  assumes "⋀ x. x ∈ S ⟹ ccApprox (f x) ⊑ G"
  assumes "⋀ x. x ∈ S ⟹ ccProd (ccNeighbors x G - {x} ∩ T) (carrier (f x)) ⊑ G"
  shows "ccApprox (ttree_restr (-S) (substitute f T t)) ⊑ G"
proof(rule ccApprox_belowI)
  fix xs

  define seen :: "var set" where "seen = {}"
  define seen_T :: "var set" where "seen_T = {}"

  assume "xs ∈ paths (ttree_restr (- S) (substitute f T t))"
  then obtain xs' xs'' where "xs = [x←xs' . x ∉ S]" and "substitute'' f T xs'' xs'" and "xs'' ∈ paths t"
    by (auto simp add: filter_paths_conv_free_restr2[symmetric] substitute_substitute'')
 
  note this(2)
  moreover
  from ‹ccApprox t ⊑ G› and ‹xs'' ∈ paths t›
  have  "ccFromList xs'' ⊑ G"
    by (auto simp add: ccApprox_below_iff)
  hence  "ccFromList xs'' G|` (- seen_T) ⊑ G"
    by (rule rev_below_trans[OF _ cc_restr_below_arg])
  moreover
  note assms(2)
  moreover
  from assms(3,4)
  have "⋀ x ys. x ∈ S ⟹ ys ∈ paths (f x) ⟹ ccFromList ys ⊑ G"
    and "⋀ x ys. x ∈ S ⟹ ys ∈ paths (f x) ⟹ ccProd (ccNeighbors x G - {x} ∩ T) (set ys) ⊑ G"
    by (auto simp add: ccApprox_below_iff seen_T_def Union_paths_carrier[symmetric] cc_lub_below_iff)
  moreover
  have "ccProd seen (set xs'' - seen_T) ⊑ G" unfolding seen_def seen_T_def by simp
  moreover
  have "seen ∩ S = {}" unfolding seen_def by simp
  moreover
  have "seen_T ⊆ S" unfolding seen_T_def by simp
  moreover
  have "⋀ x. x ∈ seen_T ⟹ f x = empty"  unfolding seen_T_def by simp
  ultimately 
  have "ccFromList [x←xs' . x ∉ S] ⊑ G ∧ ccProd (seen) (set xs' - seen_T) ⊑ G"
  proof(induction f T xs'' xs' arbitrary: seen seen_T rule: substitute''.induct[case_names Nil Cons])
  case Nil thus ?case by simp
  next
  case (Cons zs f x xs' xs T ys)

    let  ?seen_T = "if x ∈ T then insert x seen_T else seen_T"
    have subset: "- insert x seen_T ⊆ - seen_T" by auto
    have subset2: "set xs ∩ - insert x seen_T ⊆ insert x (set xs) ∩ - seen_T" by auto
    have subset3: "set zs ∩ - insert x seen_T ⊆ set zs" by auto
    have subset4: "set xs ∩ - seen_T ⊆ insert x (set xs) ∩ - seen_T" by auto
    have subset5: "set zs ∩ - seen_T ⊆ set zs" by auto
    have subset6: "set ys - seen_T ⊆ (set ys - ?seen_T) ∪ {x}" by auto

    show ?case
    proof(cases "x ∈ seen_T")
      assume "x ∈ seen_T"
      
      have [simp]: "f x = empty" using ‹x ∈ seen_T› Cons.prems by auto
      have [simp]: "f_nxt f T x = f" by (auto simp add: f_nxt_def split:if_splits)
      have [simp]: "zs = []" using ‹zs ∈ paths (f x)› by simp
      have [simp]: "xs' = xs" using ‹xs' ∈ xs ⊗ zs› by simp
      have [simp]: "x ∈ S" using ‹x ∈ seen_T› Cons.prems by auto

      from Cons.hyps Cons.prems
      have "ccFromList [x←ys . x ∉ S] ⊑ G ∧ ccProd seen (set ys - seen_T) ⊑ G"
        apply -
        apply (rule Cons.IH[where seen_T = seen_T])
        apply (auto simp add: join_below_iff Diff_eq)
        apply (erule below_trans[OF ccProd_mono[OF order_refl subset4]])
        done
      thus ?thesis using ‹x ∈ seen_T› by simp
    next
      assume "x ∉ seen_T"

      have seen_x: "ccProd seen {x} ⊑ G"
        using ‹ccProd seen (set (x # xs) - seen_T) ⊑ G› ‹x ∉ seen_T›
        by (auto simp add: insert_Diff_if ccProd_insert2[where S' = "set xs - seen_T" for xs] join_below_iff)
  
      show ?case
      proof(cases "x ∈ S")
        case True
  
        from ‹cc_restr (- seen_T) (ccFromList (x # xs)) ⊑ G›
        have "ccProd {x} (set xs - seen_T) ⊑ G" using ‹x ∉ seen_T›  by (auto simp add: join_below_iff Diff_eq)
        hence "set xs - seen_T ⊆ ccNeighbors x G" by transfer auto
        moreover
        
        from seen_x
        have "seen  ⊆ ccNeighbors x G" by (simp add: subset_ccNeighbors   ccProd_comm)
        moreover
        have "x ∉ seen" using True ‹seen ∩ S = {}› by auto
  
        ultimately
        have "seen ∪ (set xs ∩ - ?seen_T) ⊆ ccNeighbors x G - {x}∩T" by auto
        hence "ccProd (seen ∪ (set xs ∩ - ?seen_T)) (set zs) ⊑ ccProd (ccNeighbors x G - {x}∩T) (set zs)"
          by (rule ccProd_mono1)
        also
        from ‹x ∈ S›  ‹zs ∈ paths (f x)›
        have "… ⊑ G"
          by (rule Cons.prems(4))
        finally
        have "ccProd (seen ∪ (set xs ∩ - ?seen_T)) (set zs) ⊑ G" by this simp
  
        with ‹x ∈ S› Cons.prems Cons.hyps(1,2)
        have "ccFromList [x←ys . x ∉ S] ⊑ G ∧ ccProd (seen) (set ys - ?seen_T) ⊑ G"
            apply -
            apply (rule Cons.IH[where seen_T = "?seen_T"])
            apply (auto simp add: Un_Diff Int_Un_distrib2 Diff_eq f_nxt_def  join_below_iff  interleave_ccFromList interleave_set  ccProd_insert2[where S' = "set xs" for xs]
                    split: if_splits)
            apply (erule below_trans[OF cc_restr_mono1[OF subset]])
            apply (rule below_trans[OF cc_restr_below_arg], simp)
            apply (erule below_trans[OF ccProd_mono[OF order_refl Int_lower1]])
            apply (rule below_trans[OF cc_restr_below_arg], simp)
            apply (erule below_trans[OF ccProd_mono[OF order_refl Int_lower1]])
            apply (erule below_trans[OF ccProd_mono[OF order_refl subset2]])
            apply (erule below_trans[OF ccProd_mono[OF order_refl subset3]])
            apply (erule below_trans[OF ccProd_mono[OF order_refl subset4]])
            apply (erule below_trans[OF ccProd_mono[OF order_refl subset5]])
            done
        with  ‹x ∈ S›  seen_x ‹x ∉ seen_T›
        show "ccFromList [x←x # ys . x ∉ S] ⊑ G  ∧ ccProd seen (set (x#ys) - seen_T) ⊑ G" 
            apply (auto simp add: insert_Diff_if ccProd_insert2[where S' = "set ys - seen_T" for xs] join_below_iff)
            apply (rule below_trans[OF ccProd_mono[OF order_refl subset6]])
            apply (subst ccProd_union2)
            apply (auto simp add: join_below_iff)
            done
      next
        case False
  
        from False Cons.prems Cons.hyps
        have *: "ccFromList [x←ys . x ∉ S] ⊑ G ∧ ccProd ((insert x seen)) (set ys - seen_T) ⊑ G"
          apply -
          apply (rule Cons.IH[where seen = "insert x seen" and seen_T = seen_T])
          apply (auto simp add: ‹x ∉ seen_T› Diff_eq ccApprox_both join_below_iff ttree_restr_both interleave_ccFromList insert_Diff_if
                     simp add:  ccProd_insert2[where S' = "set xs ∩ - seen_T" for xs]
                     simp add:  ccProd_insert1[where S' = "seen"])
          done
        moreover
        {
        from False *
        have "ccProd {x} (set ys - seen_T) ⊑  G"
          by (auto simp add: insert_Diff_if ccProd_insert1[where S' = "seen"] join_below_iff)
        hence "ccProd {x} {x ∈ set ys - seen_T. x ∉ S} ⊑ G"
          by (rule below_trans[rotated, OF _ ccProd_mono2]) auto
        also have "{x ∈ set ys - seen_T. x ∉ S} =  {x ∈ set ys. x ∉ S}"
          using ‹seen_T ⊆ S› by auto
        finally
        have "ccProd {x} {x ∈ set ys. x ∉ S} ⊑ G".
        }
        moreover
        note False seen_x
        ultimately
        show "ccFromList [x←x # ys . x ∉ S] ⊑ G ∧ ccProd (seen) (set (x # ys) - seen_T) ⊑ G"
          by (auto simp add: join_below_iff  simp add: insert_Diff_if  ccProd_insert2[where S' = "set ys - seen_T" for xs]   ccProd_insert1[where S' = "seen"])
      qed
    qed
  qed
  with ‹xs = _›
  show "ccFromList xs ⊑ G" by simp
qed


inductive_set valid_lists :: "var set ⇒ CoCalls ⇒ var list set"
  for S G
  where  "[] ∈ valid_lists S G"
  | "set xs ⊆ ccNeighbors x G ⟹ xs ∈ valid_lists S G ⟹ x ∈ S ⟹ x#xs ∈ valid_lists S G"

inductive_simps valid_lists_simps[simp]: "[] ∈ valid_lists S G" "(x#xs) ∈ valid_lists S G"
inductive_cases vald_lists_ConsE: "(x#xs) ∈ valid_lists S G"

lemma  valid_lists_downset_aux:
  "xs ∈ valid_lists S CoCalls ⟹ butlast xs ∈ valid_lists S CoCalls"
  by (induction xs) (auto dest: in_set_butlastD)

lemma valid_lists_subset: "xs ∈ valid_lists S G ⟹ set xs ⊆ S"
  by (induction rule: valid_lists.induct) auto

lemma valid_lists_mono1:
  assumes "S ⊆ S'"
  shows "valid_lists S G ⊆ valid_lists S' G"
proof
  fix xs
  assume "xs ∈ valid_lists S G"
  thus "xs ∈ valid_lists S' G"
    by (induction rule: valid_lists.induct) (auto dest: subsetD[OF assms])
qed

lemma valid_lists_chain1:
   assumes "chain Y" 
   assumes "xs ∈ valid_lists (⋃(Y ` UNIV)) G"
   shows "∃ i. xs ∈ valid_lists (Y i) G"
proof-
  note ‹chain Y›
  moreover
  from assms(2)
  have "set xs ⊆ ⋃(Y ` UNIV)" by (rule valid_lists_subset)
  moreover
  have "finite (set xs)" by simp
  ultimately
  have "∃i. set xs ⊆ Y i" by (rule finite_subset_chain)
  then obtain i where "set xs ⊆ Y i"..

  from assms(2) this
  have "xs ∈ valid_lists (Y i) G" by (induction rule:valid_lists.induct) auto
  thus ?thesis..
qed

lemma valid_lists_chain2:
   assumes "chain Y" 
   assumes "xs ∈ valid_lists S (⨆i. Y i)"
   shows "∃ i. xs ∈ valid_lists S  (Y i)"
using assms(2)
proof(induction rule:valid_lists.induct[case_names Nil Cons])
  case Nil thus ?case by simp
next
  case (Cons xs x)

  from ‹chain Y›
  have "chain (λ i. ccNeighbors x (Y i))"
    apply (rule ch2ch_monofun[OF monofunI, rotated])
    unfolding below_set_def
    by (rule ccNeighbors_mono)
  moreover
  from ‹set xs ⊆ ccNeighbors x (⨆ i. Y i)›
  have "set xs ⊆ (⋃ i. ccNeighbors x (Y i))"
    by (simp add:  lub_set)
  moreover
  have "finite (set xs)" by simp
  ultimately
  have "∃i. set xs ⊆ ccNeighbors x (Y i)" by (rule finite_subset_chain)
  then obtain i where i: "set xs ⊆ ccNeighbors x (Y i)"..

  from Cons.IH
  obtain j where j: "xs ∈ valid_lists S (Y j)"..

  from i
  have "set xs ⊆ ccNeighbors x (Y (max i j))"
    by (rule order_trans[OF _ ccNeighbors_mono[OF chain_mono[OF ‹chain Y› max.cobounded1]]])
  moreover
  from j
  have "xs ∈ valid_lists S (Y (max i j))" 
    by (induction rule: valid_lists.induct)
       (auto del: subsetI elim: order_trans[OF _ ccNeighbors_mono[OF chain_mono[OF ‹chain Y› max.cobounded2]]])
  moreover
  note ‹x ∈ S›
  ultimately
  have "x # xs ∈ valid_lists S (Y (max i j))" by rule
  thus ?case..
qed

lemma valid_lists_cc_restr: "valid_lists S G = valid_lists S (cc_restr S G)"
proof(rule set_eqI)
  fix xs
  show "(xs ∈ valid_lists S G) = (xs ∈ valid_lists S (cc_restr S G))"
    by (induction xs) (auto dest: subsetD[OF valid_lists_subset])
qed

lemma interleave_valid_list:
  "xs ∈ ys ⊗ zs ⟹ ys ∈ valid_lists S G ⟹ zs ∈ valid_lists S' G' ⟹ xs ∈ valid_lists (S ∪ S') (G ⊔ (G' ⊔ ccProd S S'))"
proof (induction rule:interleave_induct)
  case Nil
  show ?case by simp
next
  case (left ys zs xs x)

  from ‹x # ys ∈ valid_lists S G›
  have "x ∈ S" and "set ys ⊆ ccNeighbors x G" and "ys ∈ valid_lists S G"
    by auto
 
  from ‹xs ∈ ys ⊗ zs›
  have "set xs = set ys ∪ set zs" by (rule interleave_set)
  with ‹set ys ⊆ ccNeighbors x G› valid_lists_subset[OF ‹zs ∈ valid_lists S' G'›]
  have "set xs ⊆ ccNeighbors x (G ⊔ (G' ⊔ ccProd S S'))"
    by (auto simp add: ccNeighbors_ccProd ‹x ∈ S›)
  moreover
  from ‹ys ∈ valid_lists S G› ‹zs ∈ valid_lists S' G'›
  have "xs ∈ valid_lists (S ∪ S') (G ⊔ (G' ⊔ ccProd S S'))"
    by (rule left.IH)
  moreover
  from ‹x ∈ S›
  have "x ∈ S ∪ S'" by simp
  ultimately
  show ?case..
next
  case (right ys zs xs x)

  from ‹x # zs ∈ valid_lists S' G'›
  have "x ∈ S'" and "set zs ⊆ ccNeighbors x G'" and "zs ∈ valid_lists S' G'"
    by auto
 
  from ‹xs ∈ ys ⊗ zs›
  have "set xs = set ys ∪ set zs" by (rule interleave_set)
  with ‹set zs ⊆ ccNeighbors x G'› valid_lists_subset[OF ‹ys ∈ valid_lists S G›]
  have "set xs ⊆ ccNeighbors x (G ⊔ (G' ⊔ ccProd S S'))"
    by (auto simp add: ccNeighbors_ccProd ‹x ∈ S'›)
  moreover
  from ‹ys ∈ valid_lists S G› ‹zs ∈ valid_lists S' G'›
  have "xs ∈ valid_lists (S ∪ S') (G ⊔ (G' ⊔ ccProd S S'))"
    by (rule right.IH)
  moreover
  from ‹x ∈ S'›
  have "x ∈ S ∪ S'" by simp
  ultimately
  show ?case..
qed

lemma interleave_valid_list':
  "xs ∈ valid_lists (S ∪ S') G ⟹ ∃ ys zs. xs ∈ ys ⊗ zs ∧ ys ∈ valid_lists S G ∧ zs ∈ valid_lists S' G"
proof(induction rule: valid_lists.induct[case_names Nil Cons])
  case Nil show ?case by simp
next
  case (Cons xs x)
  then obtain ys zs where "xs ∈ ys ⊗ zs" "ys ∈ valid_lists S G" "zs ∈ valid_lists S' G" by auto

    from ‹xs ∈ ys ⊗ zs› have "set xs = set ys ∪ set zs" by (rule interleave_set)
    with ‹set xs ⊆ ccNeighbors x G› 
    have "set ys ⊆ ccNeighbors x G" and "set zs ⊆ ccNeighbors x G"  by auto
  
  from ‹x ∈ S ∪ S'›
  show ?case
  proof
    assume "x ∈ S"
    with ‹set ys ⊆ ccNeighbors x G› ‹ys ∈ valid_lists S G›
    have "x # ys ∈ valid_lists S G"
      by rule
    moreover
    from ‹xs ∈ ys ⊗ zs›
    have "x#xs ∈ x#ys ⊗ zs"..
    ultimately
    show ?thesis using ‹zs ∈ valid_lists S' G› by blast
  next
    assume "x ∈ S'"
    with ‹set zs ⊆ ccNeighbors x G› ‹zs ∈ valid_lists S' G›
    have "x # zs ∈ valid_lists S' G"
      by rule
    moreover
    from ‹xs ∈ ys ⊗ zs›
    have "x#xs ∈ ys ⊗ x#zs"..
    ultimately
    show ?thesis using ‹ys ∈ valid_lists S G› by blast
  qed
qed

lemma many_calls_valid_list:
  "xs ∈ valid_lists {x} (ccProd {x} {x}) ⟹ xs ∈ range (λn. replicate n x)"
  by (induction rule: valid_lists.induct) (auto, metis UNIV_I image_iff replicate_Suc)

lemma filter_valid_lists:
  "xs ∈ valid_lists S G ⟹ filter P xs ∈ valid_lists {a ∈ S. P a} G"
by (induction rule:valid_lists.induct) auto

lift_definition ccTTree :: "var set ⇒ CoCalls ⇒ var ttree" is "λ S G. valid_lists S G" 
  by (auto intro: valid_lists_downset_aux)

lemma paths_ccTTree[simp]: "paths (ccTTree S G) = valid_lists S G" by transfer auto

lemma carrier_ccTTree[simp]: "carrier (ccTTree S G) = S"
  apply transfer
  apply (auto dest: valid_lists_subset)
  apply (rule_tac x = "[x]" in bexI)
  apply auto
  done

lemma valid_lists_ccFromList:
  "xs ∈ valid_lists S G ⟹ ccFromList xs ⊑ cc_restr S G"
by (induction rule:valid_lists.induct)
   (auto simp add: join_below_iff subset_ccNeighbors ccProd_below_cc_restr elim: subsetD[OF valid_lists_subset])

lemma ccApprox_ccTTree[simp]: "ccApprox (ccTTree S G) = cc_restr S G"
proof (transfer' fixing: S G, rule below_antisym)
  show "lub (ccFromList ` valid_lists S G) ⊑ cc_restr S G"
    apply (rule is_lub_thelub_ex)
    apply (metis coCallsLub_is_lub)
    apply (rule is_ubI)
    apply clarify
    apply (erule valid_lists_ccFromList)
    done
next
  show "cc_restr S G ⊑ lub (ccFromList ` valid_lists S G)"
  proof (rule below_CoCallsI)
    fix x y
    have "x--y∈(ccFromList [y,x])" by simp
    moreover
    assume "x--y∈(cc_restr S G)"
    hence "[y,x] ∈ valid_lists S G"  by (auto simp add: elem_ccNeighbors)
    ultimately
    show "x--y∈(lub (ccFromList ` valid_lists S G))"
      by (rule in_CoCallsLubI[OF _ imageI])
  qed
qed

lemma below_ccTTreeI:
  assumes "carrier t ⊆ S" and "ccApprox t ⊑ G"
  shows "t ⊑ ccTTree S G"
unfolding paths_mono_iff[symmetric] below_set_def
proof
  fix xs
  assume "xs ∈ paths t"
  with assms
  have "xs ∈ valid_lists S G"
  proof(induction xs arbitrary : t)
  case Nil thus ?case by simp
  next
  case (Cons x xs)
    from ‹x # xs ∈ paths t›
    have "possible t x" and "xs ∈ paths (nxt t x)" by (auto simp add: Cons_path)

    have "ccProd {x} (set xs) ⊑ ccFromList (x # xs)" by simp
    also
    from ‹x # xs ∈ paths t› 
    have "… ⊑ ccApprox t"
      by (rule ccFromList_below_ccApprox)
    also
    note ‹ccApprox t ⊑ G›
    finally
    have "ccProd {x} (set xs) ⊑ G" by this simp_all
    hence "set xs ⊆ ccNeighbors x G" unfolding subset_ccNeighbors.
    moreover
    have "xs ∈ valid_lists S G"
    proof(rule Cons.IH)
      show "xs ∈ paths (nxt t x)" by fact
    next
      from ‹carrier t ⊆ S›
      show "carrier (nxt t x) ⊆ S" 
        by (rule order_trans[OF carrier_nxt_subset])
    next
      from ‹ccApprox t ⊑ G›
      show "ccApprox (nxt t x) ⊑ G" 
        by (rule below_trans[OF ccApprox_nxt_below])
    qed
    moreover
    from  ‹carrier t ⊆ S› and ‹possible t x›
    have "x ∈ S" by (rule carrier_possible_subset)
    ultimately
    show ?case..
  qed
    
  thus "xs ∈ paths (ccTTree S G)" by (metis paths_ccTTree)
qed    

lemma ccTTree_mono1:
  "S ⊆ S' ⟹ ccTTree S G ⊑ ccTTree S' G"
  by (rule below_ccTTreeI) (auto simp add:  cc_restr_below_arg)

lemma cont_ccTTree1:
  "cont (λ S. ccTTree S G)"
  apply (rule contI2)
  apply (rule monofunI)
  apply (erule ccTTree_mono1[folded below_set_def])
  
  apply (rule ttree_belowI)
  apply (simp add: paths_Either lub_set lub_is_either)
  apply (drule (1) valid_lists_chain1[rotated])
  apply simp
  done

lemma ccTTree_mono2:
  "G ⊑ G' ⟹ ccTTree S G ⊑ ccTTree S G'"
  apply (rule ttree_belowI)
  apply simp
  apply (induct_tac  rule:valid_lists.induct) apply assumption
  apply simp
  apply simp
  apply (erule (1) order_trans[OF _ ccNeighbors_mono])
  done

lemma ccTTree_mono:
  "S ⊆ S' ⟹ G ⊑ G' ⟹ ccTTree S G ⊑ ccTTree S' G'"
  by (metis below_trans[OF ccTTree_mono1 ccTTree_mono2])


lemma cont_ccTTree2:
  "cont (ccTTree S)"
  apply (rule contI2)
  apply (rule monofunI)
  apply (erule ccTTree_mono2)

  apply (rule ttree_belowI)
  apply (simp add: paths_Either lub_set lub_is_either)
  apply (drule (1) valid_lists_chain2)
  apply simp
  done

lemmas cont_ccTTree = cont_compose2[where c = ccTTree, OF cont_ccTTree1 cont_ccTTree2, simp, cont2cont]

lemma ccTTree_below_singleI:
  assumes "S ∩ S' = {}"
  shows "ccTTree S G ⊑ singles S'"
proof-
  {
  fix xs x
  assume "xs ∈ valid_lists S G" and "x ∈ S'"
  from this assms
  have "length [x'←xs . x' = x] ≤ Suc 0"
  by(induction rule: valid_lists.induct[case_names Nil Cons]) auto
  }
  thus ?thesis by transfer auto
qed


lemma ccTTree_cc_restr: "ccTTree S G = ccTTree S (cc_restr S G)"
  by transfer' (rule valid_lists_cc_restr)

lemma ccTTree_cong_below: "cc_restr S G ⊑ cc_restr S G' ⟹ ccTTree S G ⊑ ccTTree S G'"
  by (metis ccTTree_mono2 ccTTree_cc_restr)
  
lemma ccTTree_cong: "cc_restr S G = cc_restr S G' ⟹ ccTTree S G = ccTTree S G'"
  by (metis ccTTree_cc_restr)

lemma either_ccTTree:
  "ccTTree S G ⊕⊕ ccTTree S' G' ⊑ ccTTree (S ∪ S') (G ⊔ G')"
  by (auto intro!: either_belowI ccTTree_mono)
 

lemma interleave_ccTTree: 
   "ccTTree S G ⊗⊗ ccTTree S' G' ⊑ ccTTree (S ∪ S') (G ⊔ G' ⊔ ccProd S S')"
   by transfer' (auto, erule (2) interleave_valid_list)

lemma interleave_ccTTree': 
   "ccTTree (S ∪ S') G ⊑ ccTTree S G ⊗⊗ ccTTree S' G"
   by transfer' (auto dest!:  interleave_valid_list')

lemma many_calls_ccTTree:
  shows "many_calls x = ccTTree {x} (ccProd {x} {x})"
  apply(transfer')
  apply (auto intro: many_calls_valid_list)
  apply (induct_tac n)
  apply (auto simp add: ccNeighbors_ccProd)
  done

lemma filter_valid_lists':
  "xs ∈ valid_lists {x' ∈ S. P x'} G ⟹ xs ∈ filter P ` valid_lists S G"
proof (induction xs )
  case Nil thus ?case by auto  (metis filter.simps(1) image_iff valid_lists_simps(1))
next
  case (Cons x xs)
  from Cons.prems
  have "set xs ⊆ ccNeighbors x G" and "xs ∈ valid_lists {x' ∈ S. P x'} G" and "x ∈ S" and "P x" by auto

  from this(2) have "set xs ⊆ {x' ∈ S. P x'}" by (rule valid_lists_subset)
  hence "∀x ∈ set xs. P x" by auto
  hence [simp]: "filter P xs = xs" by (rule filter_True)
  
  from Cons.IH[OF ‹xs ∈ _›]
  have "xs ∈ filter P ` valid_lists S G".

  from  ‹xs ∈ valid_lists {x' ∈ S. P x'} G›
  have "xs ∈ valid_lists S G" by (rule subsetD[OF valid_lists_mono1, rotated]) auto

  from ‹set xs ⊆ ccNeighbors x G› this ‹x ∈ S›
  have "x # xs ∈ valid_lists S G" by rule

  hence "filter P (x # xs) ∈ filter P ` valid_lists S G" by (rule imageI)
  thus ?case using ‹P x› ‹filter P xs =xs› by simp
qed

lemma without_ccTTree[simp]:
   "without x (ccTTree S G) = ccTTree (S - {x}) G"
by (transfer' fixing: x) (auto dest: filter_valid_lists'  filter_valid_lists[where P = "(λ x'. x'≠ x)"]  simp add: set_diff_eq)

lemma ttree_restr_ccTTree[simp]:
   "ttree_restr S' (ccTTree S G) = ccTTree (S ∩ S') G"
by (transfer' fixing: S') (auto dest: filter_valid_lists'  filter_valid_lists[where P = "(λ x'. x' ∈ S')"]  simp add:Int_def)

lemma repeatable_ccTTree_ccSquare: "S ⊆ S' ⟹ repeatable (ccTTree S (ccSquare S'))"
   unfolding repeatable_def
   by transfer (auto simp add:ccNeighbors_ccSquare dest: subsetD[OF valid_lists_subset])


text ‹An alternative definition›

inductive valid_lists' :: "var set ⇒ CoCalls ⇒ var set ⇒ var list ⇒ bool"
  for S G
  where  "valid_lists' S G prefix []"
  | "prefix ⊆ ccNeighbors x G ⟹ valid_lists' S G (insert x prefix) xs ⟹ x ∈ S ⟹ valid_lists' S G prefix (x#xs)"

inductive_simps valid_lists'_simps[simp]: "valid_lists' S G prefix []" "valid_lists' S G prefix (x#xs)"
inductive_cases vald_lists'_ConsE: "valid_lists' S G prefix (x#xs)"

lemma valid_lists_valid_lists':
  "xs ∈ valid_lists S G ⟹ ccProd prefix (set xs) ⊑ G ⟹ valid_lists' S G prefix xs"
proof(induction arbitrary: prefix rule: valid_lists.induct[case_names Nil Cons])
  case Nil thus ?case by simp
next
  case (Cons xs x)

  from Cons.prems Cons.hyps Cons.IH[where prefix = "insert x prefix"]
  show ?case
  by (auto simp add: insert_is_Un[where A = "set xs"]  insert_is_Un[where A = prefix]
                     join_below_iff subset_ccNeighbors elem_ccNeighbors ccProd_comm simp del: Un_insert_left )
qed

lemma valid_lists'_valid_lists_aux:
  "valid_lists' S G prefix xs ⟹  x ∈ prefix ⟹ ccProd (set xs) {x} ⊑ G"
proof(induction  rule: valid_lists'.induct[case_names Nil Cons])
  case Nil thus ?case by simp
next
  case (Cons prefix x xs)
  thus ?case
    apply (auto simp add: ccProd_insert2[where S' = prefix] ccProd_insert1[where S' = "set xs"] join_below_iff subset_ccNeighbors)
    by (metis Cons.hyps(1) dual_order.trans empty_subsetI insert_subset subset_ccNeighbors)
qed

lemma valid_lists'_valid_lists:
  "valid_lists' S G prefix xs ⟹ xs ∈ valid_lists S G"
proof(induction  rule: valid_lists'.induct[case_names Nil Cons])
  case Nil thus ?case by simp
next
  case (Cons prefix x xs)
  thus ?case
    by (auto simp add: insert_is_Un[where A = "set xs"]  insert_is_Un[where A = prefix]
                   join_below_iff subset_ccNeighbors elem_ccNeighbors ccProd_comm simp del: Un_insert_left 
         intro: valid_lists'_valid_lists_aux)
qed

text ‹Yet another definition›

lemma valid_lists_characterization:
  "xs ∈ valid_lists S G ⟷ set xs ⊆ S ∧ (∀n. ccProd (set (take n xs)) (set (drop n xs)) ⊑ G)"
proof(safe)
  fix x
  assume "xs ∈ valid_lists S G"
  from  valid_lists_subset[OF this]
  show "x ∈ set xs ⟹ x ∈ S" by auto
next
  fix n
  assume "xs ∈ valid_lists S G"
  thus "ccProd (set (take n xs)) (set (drop n xs)) ⊑ G"
  proof(induction arbitrary: n rule: valid_lists.induct[case_names Nil Cons])
    case Nil thus ?case by simp
  next
    case (Cons xs x)
    show ?case
    proof(cases n)
      case 0 thus ?thesis by simp
    next
      case (Suc n)
      with Cons.hyps Cons.IH[where n = n]
      show ?thesis
      apply (auto simp add: ccProd_insert1[where S' = "set xs" for xs] join_below_iff subset_ccNeighbors)
      by (metis dual_order.trans set_drop_subset subset_ccNeighbors)
    qed
  qed
next
  assume "set xs ⊆ S"
  and "∀ n. ccProd (set (take n xs)) (set (drop n xs)) ⊑ G" 
  thus "xs ∈ valid_lists S G"
  proof (induction xs)
    case Nil thus ?case by simp
  next
    case (Cons x xs)
    from ‹∀n. ccProd (set (take n (x # xs))) (set (drop n (x # xs))) ⊑ G›
    have "∀n. ccProd (set (take n xs)) (set (drop n xs)) ⊑ G"
      by -(rule, erule_tac x = "Suc n" in allE, auto simp add: ccProd_insert1[where S' = "set xs" for xs] join_below_iff)
    from Cons.prems Cons.IH[OF _ this]
    have "xs ∈ valid_lists S G" by auto
    with Cons.prems(1)  spec[OF ‹∀n. ccProd (set (take n (x # xs))) (set (drop n (x # xs))) ⊑ G›, where x = 1]
    show ?case by (simp add: subset_ccNeighbors)
  qed
qed

end