Theory Impl_List_Set

section ‹\isaheader{List Based Sets}›
theory Impl_List_Set
imports
  "../../Iterator/Iterator" 
  "../Intf/Intf_Set" 
begin
  (* TODO: Move *)
  lemma list_all2_refl_conv:
    "list_all2 P xs xs ⟷ (∀x∈set xs. P x x)"
    by (induct xs) auto

  primrec glist_member :: "('a⇒'a⇒bool) ⇒ 'a ⇒ 'a list ⇒ bool" where
    "glist_member eq x [] ⟷ False"
  | "glist_member eq x (y#ys) ⟷ eq x y ∨ glist_member eq x ys"

  lemma param_glist_member[param]: 
    "(glist_member,glist_member)∈(Ra→Ra→Id) → Ra → ⟨Ra⟩list_rel → Id"
    unfolding glist_member_def
    by (parametricity)

  lemma list_member_alt: "List.member = (λl x. glist_member (=) x l)"
  proof (intro ext)
    fix x l
    show "List.member l x = glist_member (=) x l"
      by (induct l) (auto simp: List.member_rec)
  qed

  thm List.insert_def
  definition 
    "glist_insert eq x xs = (if glist_member eq x xs then xs else x#xs)" 

  lemma param_glist_insert[param]:
    "(glist_insert, glist_insert) ∈ (R→R→Id) → R → ⟨R⟩list_rel → ⟨R⟩list_rel"
    unfolding glist_insert_def[abs_def]
    by (parametricity)


  primrec rev_append where
    "rev_append [] ac = ac"
  | "rev_append (x#xs) ac = rev_append xs (x#ac)"

  lemma rev_append_eq: "rev_append l ac = rev l @ ac"
    by (induct l arbitrary: ac) auto

  (*
  primrec glist_delete_aux1 :: "('a⇒'a⇒bool) ⇒ 'a ⇒ 'a list ⇒ 'a list" where
    "glist_delete_aux1 eq x [] = []"
  | "glist_delete_aux1 eq x (y#ys) = (
      if eq x y then 
        ys 
      else y#glist_delete_aux1 eq x ys)"

  primrec glist_delete_aux2 :: "('a⇒'a⇒_) ⇒ _" where
    "glist_delete_aux2 eq ac x [] = ac"
  | "glist_delete_aux2 eq ac x (y#ys) = (if eq x y then rev_append ys ac else
      glist_delete_aux2 eq (y#ac) x ys
    )"

  lemma glist_delete_aux2_eq1:
    "glist_delete_aux2 eq ac x l = rev (glist_delete_aux1 eq x l) @ ac"
    by (induct l arbitrary: ac) (auto simp: rev_append_eq)

  definition "glist_delete eq x l = glist_delete_aux2 eq [] x l"
  *)

  primrec glist_delete_aux :: "('a ⇒ 'a ⇒ bool) ⇒ _" where
    "glist_delete_aux eq x [] as = as"
  | "glist_delete_aux eq x (y#ys) as = (
      if eq x y then rev_append as ys 
      else glist_delete_aux eq x ys (y#as)
    )"

  definition glist_delete where 
    "glist_delete eq x l ≡ glist_delete_aux eq x l []"

  lemma param_glist_delete[param]:
    "(glist_delete, glist_delete) ∈ (R→R→Id) → R → ⟨R⟩list_rel → ⟨R⟩list_rel"
    unfolding glist_delete_def[abs_def]
      glist_delete_aux_def
      rev_append_def
    by (parametricity)


lemma list_rel_Range:
    "∀x'∈set l'. x' ∈ Range R ⟹ l' ∈ Range (⟨R⟩list_rel)"
proof (induction l')
  case Nil thus ?case by force
next
  case (Cons x' xs')
    then obtain xs where "(xs,xs') ∈ ⟨R⟩ list_rel" by force
    moreover from Cons.prems obtain x where "(x,x') ∈ R" by force
    ultimately have "(x#xs, x'#xs') ∈ ⟨R⟩ list_rel" by simp
    thus ?case ..
qed

  text ‹All finite sets can be represented›
  lemma list_set_rel_range:
    "Range (⟨R⟩list_set_rel) = { S. finite S ∧ S⊆Range R }"
      (is "?A = ?B")
  proof (intro equalityI subsetI)
    fix s' assume "s' ∈ ?A"
    then obtain l l' where A: "(l,l') ∈ ⟨R⟩list_rel" and
       B: "s' = set l'" and C: "distinct l'"
        unfolding list_set_rel_def br_def by blast
    moreover have "set l' ⊆ Range R"
        by (induction rule: list_rel_induct[OF A], auto)
    ultimately show "s' ∈ ?B" by simp
  next
    fix s' assume A: "s' ∈ ?B"
    then obtain l' where B: "set l' = s'" and C: "distinct l'"
        using finite_distinct_list by blast
    hence "(l',s') ∈ br set distinct" by (simp add: br_def)
    
    moreover from A and B have "∀x∈set l'. x ∈ Range R" by blast
    from list_rel_Range[OF this] obtain l
        where "(l,l') ∈ ⟨R⟩list_rel" by blast

    ultimately show "s' ∈ ?A" unfolding list_set_rel_def by fast
  qed

  lemmas [autoref_rel_intf] = REL_INTFI[of list_set_rel i_set]

  lemma list_set_rel_finite[autoref_ga_rules]:
    "finite_set_rel (⟨R⟩list_set_rel)"
    unfolding finite_set_rel_def list_set_rel_def
    by (auto simp: br_def)

  lemma list_set_rel_sv[relator_props]:
    "single_valued R ⟹ single_valued (⟨R⟩list_set_rel)"
    unfolding list_set_rel_def
    by tagged_solver
    
  (* TODO: Move to Misc *)
  lemma Id_comp_Id: "Id O Id = Id" by simp

  lemma glist_member_id_impl: 
    "(glist_member (=), (∈)) ∈ Id → br set distinct → Id"
  proof (intro fun_relI, goal_cases)
    case (1 x x' l s') thus ?case
      by (induct l arbitrary: s') (auto simp: br_def)
  qed

  lemma glist_insert_id_impl:
    "(glist_insert (=), Set.insert) ∈ Id → br set distinct → br set distinct"
  proof -
    have IC: "⋀x s. insert x s = (if x∈s then s else insert x s)" by auto

    show ?thesis
      apply (intro fun_relI)
      apply (subst IC)
      unfolding glist_insert_def
      apply (parametricity add: glist_member_id_impl)
      apply (auto simp: br_def)
      done
  qed

  lemma glist_delete_id_impl:
    "(glist_delete (=), λx s. s-{x})
    ∈ Id→br set distinct → br set distinct"
  proof (intro fun_relI)
    fix x x':: 'a and s and s' :: "'a set"
    assume XREL: "(x, x') ∈ Id" and SREL: "(s, s') ∈ br set distinct"
    from XREL have [simp]: "x'=x" by simp

    {
      fix a and a' :: "'a set"
      assume "(a,a')∈br set distinct" and "s' ∩ a' = {}"
      hence "(glist_delete_aux (=) x s a, s'-{x'} ∪ a')∈br set distinct"
        using SREL
      proof (induction s arbitrary: a s' a')
        case Nil thus ?case by (simp add: br_def)
      next
        case (Cons y s) 
        show ?case proof (cases "x=y")
          case True with Cons show ?thesis 
            by (auto simp add: br_def rev_append_eq)
        next
          case False
          have "glist_delete_aux (=) x (y # s) a 
            = glist_delete_aux (=) x s (y#a)" by (simp add: False)
          also have "(…,set s - {x'} ∪ insert y a')∈br set distinct"
            apply (rule Cons.IH[of "y#a" "insert y a'" "set s"])
            using Cons.prems by (auto simp: br_def)
          also have "set s - {x'} ∪ insert y a' = (s' - {x'}) ∪ a'"
          proof -
            from Cons.prems have [simp]: "s' = insert y (set s)"
              by (auto simp: br_def)
            show ?thesis using False by auto
          qed
          finally show ?thesis .
        qed
      qed
    }
    from this[of "[]" "{}"]     
    show "(glist_delete (=) x s, s' - {x'}) ∈ br set distinct"
      unfolding glist_delete_def
      by (simp add: br_def)
  qed
    
  lemma list_set_autoref_empty[autoref_rules]:
    "([],{})∈⟨R⟩list_set_rel"
    by (auto simp: list_set_rel_def br_def)

  lemma list_set_autoref_member[autoref_rules]:
    assumes "GEN_OP eq (=) (R→R→Id)"
    shows "(glist_member eq,(∈)) ∈ R → ⟨R⟩list_set_rel → Id"
    using assms
    apply (intro fun_relI)
    unfolding list_set_rel_def
    apply (erule relcompE)
    apply (simp del: pair_in_Id_conv)
    apply (subst Id_comp_Id[symmetric])
    apply (rule relcompI[rotated])
    apply (rule glist_member_id_impl[param_fo])
    apply (rule IdI)
    apply assumption
    apply parametricity
    done

  lemma list_set_autoref_insert[autoref_rules]:
    assumes "GEN_OP eq (=) (R→R→Id)"
    shows "(glist_insert eq,Set.insert) 
      ∈ R → ⟨R⟩list_set_rel → ⟨R⟩list_set_rel"
    using assms
    apply (intro fun_relI)
    unfolding list_set_rel_def
    apply (erule relcompE)
    apply (simp del: pair_in_Id_conv)
    apply (rule relcompI[rotated])
    apply (rule glist_insert_id_impl[param_fo])
    apply (rule IdI)
    apply assumption
    apply parametricity
    done

  lemma list_set_autoref_delete[autoref_rules]:
    assumes "GEN_OP eq (=) (R→R→Id)"
    shows "(glist_delete eq,op_set_delete) 
      ∈ R → ⟨R⟩list_set_rel → ⟨R⟩list_set_rel"
    using assms
    apply (intro fun_relI)
    unfolding list_set_rel_def
    apply (erule relcompE)
    apply (simp del: pair_in_Id_conv)
    apply (rule relcompI[rotated])
    apply (rule glist_delete_id_impl[param_fo])
    apply (rule IdI)
    apply assumption
    apply parametricity
    done
 
  lemma list_set_autoref_to_list[autoref_ga_rules]: 
    shows "is_set_to_sorted_list (λ_ _. True) R list_set_rel id"
    unfolding is_set_to_list_def is_set_to_sorted_list_def
      it_to_sorted_list_def list_set_rel_def br_def
    by auto

  lemma list_set_it_simp[refine_transfer_post_simp]:
    "foldli (id l) = foldli l" by simp

  lemma glist_insert_dj_id_impl:
    "⟦ x∉s; (l,s)∈br set distinct ⟧ ⟹ (x#l,insert x s)∈br set distinct"
    by (auto simp: br_def)

context begin interpretation autoref_syn .
  lemma list_set_autoref_insert_dj[autoref_rules]:
    assumes "PRIO_TAG_OPTIMIZATION"
    assumes "SIDE_PRECOND_OPT (x'∉s')"
    assumes "(x,x')∈R"
    assumes "(s,s')∈⟨R⟩list_set_rel"
    shows "(x#s,
      (OP Set.insert ::: R → ⟨R⟩list_set_rel → ⟨R⟩list_set_rel) $ x' $ s') 
      ∈ ⟨R⟩list_set_rel"
    using assms
    unfolding autoref_tag_defs
    unfolding list_set_rel_def
    apply -
    apply (erule relcompE)
    apply (simp del: pair_in_Id_conv)
    apply (rule relcompI[rotated])
    apply (rule glist_insert_dj_id_impl)
    apply assumption
    apply assumption
    apply parametricity
    done
end

  subsection ‹More Operations›
  lemma list_set_autoref_isEmpty[autoref_rules]:
    "(is_Nil,op_set_isEmpty) ∈ ⟨R⟩list_set_rel → bool_rel"
    by (auto simp: list_set_rel_def br_def split: list.split_asm)

  lemma list_set_autoref_filter[autoref_rules]:
    "(filter,op_set_filter) 
      ∈ (R → bool_rel) → ⟨R⟩list_set_rel → ⟨R⟩list_set_rel"
  proof -
    have "(filter, op_set_filter) 
      ∈ (Id → bool_rel) → ⟨Id⟩list_set_rel → ⟨Id⟩list_set_rel"
      by (auto simp: list_set_rel_def br_def)
    note this[param_fo]
    moreover have "(filter,filter)∈(R → bool_rel) → ⟨R⟩list_rel → ⟨R⟩list_rel"
      unfolding List.filter_def
      by parametricity
    note this[param_fo]
    ultimately show ?thesis
      unfolding list_set_rel_def
      apply (intro fun_relI)
      apply (erule relcompE, simp)
      apply (rule relcompI)
      apply (rprems, assumption+)
      apply (rprems, simp+)
      done
  qed


  context begin interpretation autoref_syn .
  lemma list_set_autoref_inj_image[autoref_rules]:
    assumes "PRIO_TAG_OPTIMIZATION"
    assumes INJ: "SIDE_PRECOND_OPT (inj_on f s)"
    assumes [param]: "(fi,f)∈Ra→Rb"
    assumes LP: "(l,s)∈⟨Ra⟩list_set_rel"
    shows "(map fi l, 
      (OP (`) ::: (Ra→Rb) → ⟨Ra⟩list_set_rel → ⟨Rb⟩list_set_rel)$f$s) 
      ∈ ⟨Rb⟩list_set_rel"
  proof -
    from LP obtain l' where 
      [param]: "(l,l')∈⟨Ra⟩list_rel" and L'S: "(l',s)∈br set distinct"
      unfolding list_set_rel_def by auto

    have "(map fi l, map f l')∈⟨Rb⟩list_rel" by parametricity
    also from INJ L'S have "(map f l',f`s)∈br set distinct"
      apply (induction l' arbitrary: s)
      apply (auto simp: br_def dest: injD)
      done
    finally (relcompI) show ?thesis 
      unfolding autoref_tag_defs list_set_rel_def .
  qed

  end


  lemma list_set_cart_autoref[autoref_rules]:
    fixes Rx :: "('xi × 'x) set"
    fixes Ry :: "('yi × 'y) set"
    shows "(λxl yl. [ (x,y). x←xl, y←yl], op_set_cart) 
    ∈ ⟨Rx⟩list_set_rel → ⟨Ry⟩list_set_rel → ⟨Rx ×⇩r Ry⟩list_set_rel"
  proof (intro fun_relI)
    fix xl xs yl ys
    assume "(xl, xs) ∈ ⟨Rx⟩list_set_rel" "(yl, ys) ∈ ⟨Ry⟩list_set_rel"
    then obtain xl' :: "'x list" and yl' :: "'y list" where 
      [param]: "(xl,xl')∈⟨Rx⟩list_rel" "(yl,yl')∈⟨Ry⟩list_rel"
      and XLS: "(xl',xs)∈br set distinct" and YLS: "(yl',ys)∈br set distinct"
      unfolding list_set_rel_def 
      by auto

    have "([ (x,y). x←xl, y←yl ], [ (x,y). x←xl', y←yl' ]) 
      ∈ ⟨Rx ×⇩r Ry⟩list_rel"
      by parametricity
    also have "([ (x,y). x←xl', y←yl' ], xs × ys) ∈ br set distinct"
      using XLS YLS
      apply (auto simp: br_def)
      apply hypsubst_thin
      apply (induction xl')
      apply simp
      apply (induction yl')
      apply simp
      apply auto []
      apply (metis (lifting) concat_map_maps distinct.simps(2) 
        distinct_singleton maps_simps(2))
      done
    finally (relcompI) 
    show "([ (x,y). x←xl, y←yl ], op_set_cart xs ys) ∈ ⟨Rx ×⇩r Ry⟩list_set_rel"
      unfolding list_set_rel_def by simp
  qed


  subsection ‹Optimizations›
  lemma glist_delete_hd: "eq x y ⟹ glist_delete eq x (y#s) = s"
    by (simp add: glist_delete_def)

  text ‹Hack to ensure specific ordering. Note that ordering has no meaning
    abstractly›
  definition [simp]: "LIST_SET_REV_TAG ≡ λx. x"
  
  lemma LIST_SET_REV_TAG_autoref[autoref_rules]: 
    "(rev,LIST_SET_REV_TAG) ∈ ⟨R⟩list_set_rel → ⟨R⟩list_set_rel"
    unfolding list_set_rel_def
    apply (intro fun_relI)
    apply (elim relcompE)
    apply (clarsimp simp: br_def)
    apply (rule relcompI)
    apply (rule param_rev[param_fo], assumption)
    apply auto
    done
  
  



end