Theory SM.SM_Datastructures

theory SM_Datastructures
imports Main 
  CAVA_Base.CAVA_Base
  "../Lib/SOS_Misc_Add"
  DFS_Framework.Feedback_Arcs (* TODO: Only for oo-symbol !?*)

begin

  lemma [code_unfold]: "{(a,b). (a,b)X  P a b} = Set.filter (λ(a,b). P a b) X"
    by auto

  lemma in_dom_map_code[code_unfold]: 
    "xdom m = (case m x of None  False | _  True)"
    by (auto split: option.splits)

  (* TODO: Move to gen_set. Generic algorithm for set_of_list *)
  lemma set_by_fold: "set l = fold insert l {}"
  proof -
    {
      fix s
      have "fold insert l s = s  set l"
        by (induction l arbitrary: s) auto
    } from this[of "{}"] show ?thesis by simp
  qed

  context
  begin

    interpretation autoref_syn .

    lemma [autoref_itype]: "set ::i Iii_list i Iii_set" by simp

  end

  lemma gen_set[autoref_rules_raw]:
    fixes R :: "('c×'a)set" and Rs :: "('c×'a) set  (_×'a set) set"
    assumes [simplified,param]:
      "GEN_OP em {} (RRs)"
      "GEN_OP ins insert (R  RRs  RRs)"
    shows "(λli. fold ins li em,set)Rlist_rel  RRs"
      unfolding set_by_fold[abs_def]
      by parametricity

  schematic_goal
    shows "(?c,set [1,2,3::nat])nat_reldflt_ahs_rel"
      using [[autoref_trace_failed_id]]
      by (autoref (trace, keep_goal))

  (* TODO: Possibly, we can drop the
    find_min_idx_f - stuff, and formalize our ample-set 
    using the abstract LEAST, which is then implemented
    by collecti_index.
  *)

  text ‹Find minimum index and result where function returns non-none value›
  primrec find_min_idx_f :: "('a  'b)  'a list  (nat × 'b)" where
    "find_min_idx_f f [] = None"
  | "find_min_idx_f f (x#xs) = (
      case f x of 
        Some r  Some (0,r) 
      | None  map_option (map_prod Suc id) (find_min_idx_f f xs)
    )"
  
  lemma find_min_idx_f_None_conv: 
    "find_min_idx_f f l = None  (aset l. f a = None)"
    apply (induction l)
    apply (auto split: option.splits)
    done

  lemma find_min_idx_f_SomeD:
    "find_min_idx_f f l = Some (i,r)  f (l!i) = Some r  i < length l"
    by (induction l arbitrary: i) (auto split: if_split_asm option.splits)

  lemma find_min_idx_f_SomeD_complete: 
    "find_min_idx_f f l = Some (i,r) 
       (f (l!i) = Some r  i < length l  (j<i. f (l!j) = None))"
    apply (induction l arbitrary: i) 
    apply (auto split: if_split_asm option.splits)
    apply (case_tac j)
    apply auto
    done

  lemma find_min_idx_f_LEAST_eq: "find_min_idx_f f l = (
    if i<length l. f (l!i)  None then
      let i = LEAST i. i<length l  f (l!i)  None in Some (i,the (f (l!i)))
    else
      None
  )"
  proof (cases "find_min_idx_f f l")
    case None
    show ?thesis using None by (auto simp: find_min_idx_f_None_conv)
  next
    case (Some a)
    obtain i r where 1: "a = (i, r)" by force
    have 2: "f (l ! i) = Some r" "i < length l" " j < i. f (l ! j) = None"
      using find_min_idx_f_SomeD_complete[OF Some[unfolded 1]] by auto
    have 3: "(LEAST i. i < length l  ( y. f (l ! i) = Some y)) = i"
      using 2 linorder_neqE_nat by (force intro!: Least_equality)
    show ?thesis unfolding Some 1 using 2 3 by auto
  qed  

  primrec collect_indexr' :: "nat  (nat×'b) set  (nat  'a  'b set)  'a list  (nat×'b) set" where
    "collect_indexr' i a c [] = a"
  | "collect_indexr' i a c (x#xs) = (collect_indexr' (Suc i) (a({i} × c i x)) c xs)"  

  abbreviation "collect_indexr  collect_indexr' 0 {}"

  lemma collect_indexr'_collect: "collect_indexr' i0 a f l 
    = a  {(i0+i,x) | i x. i<length l  xf (i0+i) (l!i)}"
    apply (induction l arbitrary: i0 a)
    apply simp
    apply simp
    apply auto
    apply (case_tac i, auto)
    apply (case_tac i, auto)
    done

  lemma collect_indexr_collect: "collect_indexr f l 
    = {(i,x) | i x. i<length l  xf i (l!i)}"  
    by (simp add: collect_indexr'_collect)
  

  primrec collecti_index' :: "nat  (nat×'b) set  (nat  'a  (bool × 'b set))  'a list  (nat×'b) set" where
    "collecti_index' i a c [] = a"
  | "collecti_index' i a c (x#xs) = (case c i x of
      (False,s)  collecti_index' (Suc i) (a  {i}×s) c xs
    | (True,s)  {i}×s)"

  abbreviation "collecti_index  collecti_index' 0 {}"

  lemma collecti_index'_collect: "collecti_index' i0 a0 f l 
    = (
      if i<length l. fst (f (i0+i) (l!i)) then
        let i=LEAST i . i<length l  fst (f (i0+i) (l!i)) in {i0+i} × snd (f (i0+i) (l!i))
      else
        a0  {(i0+i,x) | i x. i<length l  xsnd (f (i0+i) (l!i))})"
  proof (cases "i<length l. fst (f (i0+i) (l!i))")
    case False
    note False[simp]
    hence "i<length l. ¬fst (f (i0+i) (l!i))" by blast
    hence "collecti_index' i0 a0 f l = collect_indexr' i0 a0 (snd oo f) l"
    proof (induction l arbitrary: i0 a0)
      case (Cons x l)
      from Cons.prems have "¬fst (f i0 x)" by auto
      hence [simp]: "v. f i0 x  (True,v)" by auto
      have "collecti_index' i0 a0 f (x#l) = 
        collecti_index' (Suc i0) (a0  {i0} × (snd (f i0 x))) f l" 
        by (simp split: prod.splits bool.splits)
      also have " = collect_indexr' (Suc i0) ((a0  {i0} × (snd (f i0 x)))) (snd oo f) l" 
        apply (subst Cons.IH)
        using Cons.prems
        by auto
      finally have 1: "collecti_index' i0 a0 f (x # l) =
        collect_indexr' (Suc i0) (a0  {i0} × snd (f i0 x)) (snd ∘∘ f) l" . 
      show ?case by (subst 1) simp
    qed simp
    also note collect_indexr'_collect
    finally show ?thesis by simp
  next
    case True
    note True[simp]
    define im where "im  λl (i0::nat). LEAST i . i<length l  fst (f (i0+i) (l!i))"
    from LeastI_ex[OF True] have 
      1: "im l i0<length l" "fst (f (i0+im l i0) (l!im l i0))" 
      unfolding im_def by (auto) 
    have 2: "i<im l i0. ¬ fst (f (i0+i) (l!i))"
    proof safe
      fix i
      assume A: "i<im l i0" with 1 have "i<length l" by simp
      moreover assume "fst (f (i0+i) (l!i))"
      ultimately have "im l i0  i"
        unfolding im_def by (auto intro: Least_le)
      with A show False by simp  
    qed  

    from 1 2 have "collecti_index' i0 a0 f l = {i0+im l i0} × snd (f (i0+im l i0) (l!im l i0))"
    proof (induction l arbitrary: i0 a0)
      case (Cons x l)
      show ?case proof (cases "fst (f i0 x)")
        case True
        hence [simp]: "y. f i0 x  (False,y)" by auto
        note [simp] = True        

        from Cons.prems(3) have [simp]: "im (x#l) i0 = 0"
          by auto

        thus ?thesis
          by (auto split: prod.splits bool.splits)
      next
        case False
        hence "im (x#l) i0 = Suc (im l (Suc i0))"
          unfolding im_def
          apply (subst Least_Suc)
          apply (rule conjI) 
          apply (rule Cons.prems)+
          apply simp
          apply simp
          done
        hence ims: "im (x#l) i0 > 0" "im l (Suc i0) = im (x#l) i0 - 1" 
          by simp_all

        from False have 1: "collecti_index' i0 a0 f (x # l) 
          = collecti_index' (Suc i0) (a0  {i0} × (snd (f i0 x))) f l"
          by (auto)

        show ?thesis
          apply (subst 1)
          apply (subst Cons.IH)
          using Cons.prems(1) ims apply (simp)
          using Cons.prems(2) ims apply simp
          using Cons.prems(3)
          apply (auto simp: ims nth_Cons less_diff_conv split: nat.splits) []
          using ims(1) apply (auto simp: ims(2))
          done
      qed
    qed simp
    thus ?thesis
      by (simp add: im_def)

  qed      

  lemma collecti_index_collect: "collecti_index f l 
    = (
      if i<length l. fst (f i (l!i)) then
        let i=LEAST i . i<length l  fst (f i (l!i)) in {i} × snd (f i (l!i))
      else
        {(i,x) | i x. i<length l  xsnd (f i (l!i))})"
    using collecti_index'_collect[of 0 "{}" f l]
    by (simp cong: if_cong)

  primrec collecti_index'_list :: "nat  (nat×'b) list  (nat  'a  (bool × 'b list))  'a list  (nat×'b) list" where
    "collecti_index'_list i a c [] = a"
  | "collecti_index'_list i a c (x#xs) = (case c i x of
      (False,s)  collecti_index'_list (Suc i) (a @ map (Pair i) s) c xs
    | (True,s)  map (Pair i) s)"

  abbreviation "collecti_index_list  collecti_index'_list 0 []"

  lemma collecti_index'_list_invar:
    assumes "i x b l. c i x = (b,l)  distinct l"
    assumes "fst`set a  {0..<i0}" "distinct a"
    shows "distinct (collecti_index'_list i0 a c l)"
    using assms
    apply (induction l arbitrary: i0 a)
    apply simp
    apply (auto split: prod.splits bool.splits simp: nth_Cons' distinct_map)
    apply rprems
    apply (auto simp: distinct_map)
    done

  lemma image_Pair_eq_prod_sng[simp]: "Pair x ` s = {x}×s" by auto  

  lemma collecti_index'_list_α: 
    assumes "i x b l. ci i x = (b,l)  c i x = (b,set l)"
    shows 
      "set (collecti_index'_list i0 ai ci l) = collecti_index' i0 (set ai) c l"
  proof -
    from assms have A: "i x b s. c i x = (b,s)  (l. ci i x = (b, l)  s=set l)"
      apply auto apply (case_tac "ci i x") apply auto done

    show ?thesis  
      apply (induction l arbitrary: i0 ai)
      apply simp
      apply simp
      apply (split prod.split, clarsimp)
      apply (split bool.split, clarsimp, intro allI impI conjI)
      apply (force simp add: A) []
  
      apply (simp split: prod.splits bool.splits add: A)
      apply safe
      apply simp_all
      apply blast
      done
  qed

  lemma collecti_index_list_refine:
    "(collecti_index_list,collecti_index)
       (nat_rel  Id  bool_rel ×r Idlist_set_rel)  Idlist_rel 
     nat_rel×rIdlist_set_rel"
    apply (intro fun_relI)
    apply (simp add: list_set_rel_def)
    apply (rule brI)

    apply (simp add: br_def)
    apply (rule collecti_index'_list_α[of _ _ 0 "[]", simplified, symmetric])
    apply (drule_tac x=i and x'=i in fun_relD, simp)
    apply (drule_tac x=x and x'=x in fun_relD, simp)
    apply (auto simp: prod_rel_def) []

    apply (rule collecti_index'_list_invar)
    apply auto
    apply (drule_tac x=i and x'=i in fun_relD, simp)
    apply (drule_tac x=x and x'=x in fun_relD, simp)
    apply (auto simp: prod_rel_def br_def) []
    done





end