Theory Indexed_Set

theory Indexed_Set
  imports Main FuncSet Previous
begin

section{*Indexed sets*}

text{*The next type definition, @{text iset}, represents the notion of an indexed set,
  which is a pair: a set and a function that goes from naturals to the set.*}

type_synonym ('a) iset = "'a set × (nat => 'a)"

text{*Now we define functions which make possible to separate an indexed set into the set
and the function and we add them to the simplifier, since they are only meant to be
abbreviations of the ``fst'' and ``snd'' operations:*}

definition iset_to_set :: "'a iset => 'a set"
  where "iset_to_set A = fst A"

definition iset_to_index :: "'a iset => (nat => 'a)"
  where "iset_to_index A = snd A"

lemmas [simp] = iset_to_set_def iset_to_index_def

text{*An indexing of a set will be any bijection between the set of the
  natural numbers less than its cardinality (because we start counting from @{term "0::nat"}) and the set.
  Note: we will always work with finite sets. By default, the definition of @{term card}
  assigns to an infinite set cardinality equal to @{term "0::nat"}.*}

definition indexing :: "('a iset) => bool"
  where "indexing A = bij_betw (iset_to_index A) 
  {..<card (iset_to_set A)} (iset_to_set A)"

text{*Once we have the definition of @{text indexing}, we are going to prove some properties of it:*}

text{*We introduce some lemmas presenting properties and alternative definitions of ``indexing''. For instance, whenever
we have an indexing $A=(iset\_to\_set \mbox{ } A,iset\_to\_index \mbox{ } A)$ the index function will map naturals in the
range $\{..<card(A)\}$ to elements of $iset\_to\_set \mbox{ } A$ and, moreover, the image set of the indexing function
in such range will be whole set $iset\_to\_set \mbox{ } A$.*}

lemma indexing_equiv_img:
  assumes  ob: "indexing A"
  shows "(iset_to_index A) 
  ∈ {..<(card (iset_to_set A))} -> (iset_to_set A) 
  ∧ (iset_to_index A) ` {..<(card (iset_to_set A))} 
  = (iset_to_set A)"
  using ob
  unfolding indexing_def
  unfolding bij_betw_def by auto

text{*The implication is also satisfied in the opposite direction:*}
lemma img_equiv_indexing:
  assumes f: "(iset_to_index A) 
  ∈ {..<(card (iset_to_set A))} -> (iset_to_set A) 
  ∧ (iset_to_index A) ` {..<(card (iset_to_set A))} 
  = (iset_to_set A)"
  shows "indexing A"
  proof -
  have "inj_on (iset_to_index A) {..<card (iset_to_set A)}"
    proof -
    have "card ((iset_to_index A) ` {..<(card (iset_to_set A))})
      =card (iset_to_set A)" using f by auto
    also have "...= card ({..<card (iset_to_set A)})" 
      using card_lessThan by auto
    finally have 1: 
      "card ( (iset_to_index A) ` {..<(card (iset_to_set A))}) 
      = card ({..<card (iset_to_set A)})" .
    have 2: "finite {..<card (iset_to_set A)}"
      by (metis finite_lessThan)
    show ?thesis using eq_card_imp_inj_on [OF 2 1] .
  qed
  moreover have " iset_to_index A ` {..<card (iset_to_set A)} 
    = iset_to_set A" using f by auto
  ultimately show ?thesis 
    unfolding indexing_def unfolding bij_betw_def 
    by simp
qed

text{*Now we present another alternative definition of indexing linking it with the notions of injectivity and surjectivity:*}

lemma indexing_inj_surj:
  assumes  ob: "indexing A"
  shows "inj_on (iset_to_index A) {..<(card (iset_to_set A))} 
    ∧ (iset_to_index A) ` {..<(card (iset_to_set A))} 
  = (iset_to_set A)"
  using ob
  unfolding indexing_def
  unfolding bij_betw_def .

lemma indexing_inj_surj_inv:
  assumes "inj_on (iset_to_index A) {..<(card (iset_to_set A))} 
  ∧ (iset_to_index A) ` {..<(card (iset_to_set A))} = (iset_to_set A)"
  shows "indexing A"
  unfolding indexing_def
  unfolding bij_betw_def by fact

text{*One basic property is that the empty set with any function of appropriate type is an @{text indexing}:*}
lemma indexing_empty:
  "indexing ({}, f)"
  unfolding indexing_def
  unfolding bij_betw_def by simp

text{*We can obtain an equivalent notion of previous lemma writing the property in the unfolded definition of 
  @{text indexing}.*}
lemma indexing_empty_inv:
  shows "inj_on (iset_to_index ({}, f)) {..<card (iset_to_set ({}, f))} 
  ∧ iset_to_index ({}, f) ` {..<card (iset_to_set ({}, f))} = iset_to_set ({}, f)" by simp

text{*Now we are proving a basic but useful lemma: if we have an @{text indexing} of a set, 
then the image of a natural less than the cardinality of the set is an element of the set.*}
lemma indexing_in_set:
  assumes "indexing (A,f)"
  and "n < card A"
  shows "f n ∈ A"
  using assms unfolding indexing_def bij_betw_def by auto

text{*We present two auxiliary lemmas about indexings and their behaviours as injective functions.
The first one claims that if we have an @{text indexing} and two naturals (less than the cardinality of the set) with
the same image, then the naturals are equal (which is a consequence of injectivity):.*}
lemma
  indexing_impl_eq_preimage:
  assumes i: "indexing (A, f)"
  and x: "x ∈ {..<card A}" and y: "y ∈ {..<card A}" 
  and f: "f x = f y"
  shows "x = y"
  apply (rule inj_onD [of f "{..<card A}"])
  using i
  unfolding indexing_def bij_betw_def
  by simp fact+

text{*On the contrary, if we have the same assumptions than before but we consider that the image of both naturals 
are different, then the numbers are distinct.*}
lemma
  indexing_impl_ndiff_image:
  assumes i: "indexing (A, f)"
  and x: "x ∈ {..<card A}" and y: "y ∈ {..<card A}" 
  and f: "x ≠ y"
  shows "f x ≠ f y"
proof (rule ccontr, simp)
  assume "f x = f y"
  hence "x = y" 
    using i 
    unfolding indexing_def bij_betw_def inj_on_def
    using x y by auto
  thus False using f by contradiction
qed

text{*The following lemma proves that for any finite set $A$, there exist a natural number $n$ and a function $f$
such that $f$ is an index function of $A$ with $\{..<n\}$ the collection of indexes. The prof is no constructive, is based on a lemma in the Isabelle library proving that every finite set is a mapping of a range of the naturals.*}
lemma finite_imp_nat_seg_image_inj_on_Pi:
  assumes f: "finite A"
  shows "(∃n::nat. ∃f∈{i. i < n} -> A.
  ((f ` {i. i < n} = A) ∧ inj_on f {i. i < n}))"
proof -
  obtain f and n
    where a1: "f ` {i. i < (n::nat)} = A ∧ inj_on f {i. i < n}"
    and a2: "f ∈ {i. i < n} -> A"
    using finite_imp_nat_seg_image_inj_on [OF f] by auto
  thus ?thesis by auto
qed
 
text{*The bijection is between the naturals up to card A and the set. Thanks to that we are giving to the set an indexation, we are representing a set more or less like a vector in C++:
  a structure with $card(A)$ components (from position $0$ to ($card(A) - 1$)). Each component $f(i)$ tallies with one
  element of the set.*}
text{*The following lemma extends the previous one, since we prove that $n$ in the previous lemma is actually $card(A)$.
The proof is carried out by induction on the finite set $A$, and the indexing function is explicitly given ($?f$ in
the proof below):*}
lemma finite_imp_nat_seg_image_inj_on_Pi_card:
  assumes f: "finite A"
  shows "(∃f ∈ {i. i < (card A)} -> A. ((f ` {i. i < (card A)} = A) 
  ∧ inj_on f {i. i < (card A)}))"
  using f proof (induct)
  case empty
  show ?case by auto
next
  case (insert b B)
  show "∃f∈{i::nat. i <
    card (insert b B)} -> insert b B.
    f ` {i::nat. i < card (insert b B)} = insert b B ∧
    inj_on f {i::nat. i < card (insert b B)}"
  proof -
    obtain g
      where g1: "g ∈ {i. i < (card B)} -> B"
      and g2: "g ` {i::nat. i < card B} = B ∧ inj_on g
      {i::nat. i < card B}"
      using insert.hyps (3) by auto
    let ?f = "(λn::nat. if n ∈ {i. i < card B} then g n
      else if n = card B then b else g n)"
    have f1: "?f ∈{i::nat. i < card (insert b B)}
      -> insert b B"
    proof
      fix x
      assume x_bounded: "x ∈ {i::nat. i < card (insert b B)}"
      show "(if x ∈ {i::nat. i < card B} then g x else if x
        = card B then b else g x) ∈ insert b B"
      proof (cases "x ∈ {i::nat. i < card B}")
        case True then show ?thesis using g1 unfolding Pi_def by simp
      next
        case False
        have "x = card B"
        proof -
          have "card (insert b B) = Suc (card B)" -- "To prove this we need that @{term b}
            won't be in @{term B} and that the set be finite"
            using insert.hyps (2)
            using insert.hyps (1) by simp
          thus ?thesis
            using False
            using x_bounded by simp
        qed
        thus ?thesis by simp
      qed
    qed
    have f2: "?f ` {i::nat. i < card (insert b B)} 
      = (insert b B) ∧ inj_on ?f {i::nat. i < card (insert b B)}"
    proof
      show "?f ` {i::nat. i < card (insert b B)} = insert b B"
      proof -
        have "?f ` {i::nat. i < card (insert b B)} =  ?f `
          ({i::nat. i < card B} ∪ {i. i = card B})"
          using insert.hyps (2)
          using insert.hyps (1) by auto
        also have "… =  ?f ` {i::nat. i < card B} ∪
          ?f ` {i. i = card B}"
          by (rule image_Un)
        also have "… = B  ∪ ?f ` {i. i = card B}"
          using g2 by auto
        also have "… = B ∪ {b}" by simp
        finally show ?thesis by simp
      qed
      show "inj_on ?f {i::nat. i < card (insert b B)}"
      proof -
        have "inj_on ?f {i::nat. i < card (insert b B)} = inj_on
          ?f (insert (card B) {i. i < (card B)})"
        proof -
          have "{i::nat. i < card (insert b B)} = insert (card
            B) {i. i < (card B)}"
            using insert.hyps (2)
            using insert.hyps (1) by auto
          thus ?thesis by simp
        qed
        also have "… = (inj_on ?f {i. i < (card B)} ∧ ?f
          (card B) ∉ ?f ` ({i. i < (card B)} - {card B}))"
          by (rule inj_on_insert)
        also have "… = (True ∧ ?f (card B) ∉ ?f `
          ({i. i < (card B)} - {card B}))"
          using g2 unfolding inj_on_def by auto
        also have "… = (True ∧ True)"
          using insert.hyps (2) using g2 by auto
        also have "… = True" by fast
        finally show ?thesis by fast
      qed
    qed
    show ?thesis
      using f1 f2 by auto
  qed
qed

text{*As a corollary, we prove that for each finite set there exists an indexing of it. This is the main theorem
of this section and it will be very useful in the future to assign an order to a finite set (we will need it
in future proofs).*}
corollary obtain_indexing: 
  assumes finite_A: "finite A"
  shows "∃f. indexing (A,f)"
proof (unfold indexing_def,unfold bij_betw_def,auto)
  from finite_A obtain f where surj: "f ` {i. i < (card A)} = A" and inj_on: "inj_on f {i. i < (card A)}"
    using finite_imp_nat_seg_image_inj_on_Pi_card[OF finite_A] by auto
  show  "∃f. inj_on f {..<card A} ∧ f ` {..<card A} = A" using surj and inj_on and lessThan_def[of "card A"]
    by auto
qed

text{*In addition, if we have an indexing we will know that the set is finite. 
  This lemma will allow us to remove the premise $finite$ $A$ whenever we have indexings. 
  This is because Isabelle assigns $0$ as the cardinality of an infinite set. Suppose that
  $A$ is infinite. If we have an $indexing(A,f)$, hence $f$ is a bijection between the set of naturals less than the
  cardinality of $A$ ($0$ due to the implementation) and $A$. Then, $A=f`\{..<card(A)\}=f`\{..<0\}=f`\{\}=\{\}$.
  However, we have supposed that $A$ was infinite and $\{\}$ is not, so we have a contradiction and $A$ is always finite.*}
lemma indexing_finite[simp]:
  assumes indexing_A: "indexing (A,f)"
  shows "finite A"
  by (metis bij_betw_finite finite_lessThan
    fst_conv indexing_def iset_to_set_def indexing_A)

text{*After introducing the notion of indexed set, we need to introduce two basic operations over indexed sets: insert and
  remove. They will be generic with respect to the position where an element can be inserted or removed. For instance,
  given an indexed set $\{(a,0),(b,1),(c,2)\}$ if we are to insert an element $d$, 
  we will admit indexing $\{(d,0),(a,1),(b,2),(c,3)\},\{(a,0),(d,1),(b,2),(c,3)\}$ and so on. 
  In other words, inserting an element in a sorted set preserves the order of the elements, but maybe not their positions.*}

text{*First we define the function which, for a given indexing $A$ and an element $a$ gives all possible indexings
for the set $insert$ $a$ $(iset\_to\_set$ $A)$ preserving $(iset\_to\_index$ $A)$:*}
text{*$n$ is the position where 'a' will be inserted. It shoul be a natural number between $0$ (first position) 
  and card A (last position).*}

definition indexing_ext :: "('a iset) => 'a => (nat => nat => 'a)"
  where
  "indexing_ext A a = 
  (%n. %k. if k < n then (iset_to_index A) k 
  else if k = n then a
  else (iset_to_index A) (k - 1))"


text{*Now we present a basic property (it will be useful to be applied in induction proofs):
  If one @{term indexing_ext} generated from an indexation @{term "F::'a iset"} and
  from one element @{term "a ∉ (index_to_set F)"} is good (is an indexing), then the indexation of
  @{term "F::'a iset"} is also good (an indexing).*}

text{*It is a long lemma (about 300 lines). The proof of injectivity must be separated in several different cases,
  depending on the position where we insert the element (after, before or exactly in the $nth$ position):*}

lemma indexing_indexing_ext:  
  assumes ob: 
  "indexing ((insert x (iset_to_set F)), (indexing_ext F x n))"
  and n1: "0 ≤ n"
  and n2: "n ≤ card (iset_to_set F)"
  and x_notin_F: "x ∉ (iset_to_set F)"
  shows "indexing F"
proof (unfold indexing_def bij_betw_def, intro conjI)
  let ?h = "iset_to_index F"
  let ?F = "iset_to_set F"
  show inj_on_h:"inj_on ?h {..<card ?F}"
  proof (unfold inj_on_def, rule ballI, rule ballI, rule impI)
    fix xa y
    assume xa: "xa ∈ {..<card ?F}" 
      and y: "y ∈ {..<card ?F}" and h: "?h xa = ?h y"
    show "xa = y"
    proof (rule inj_onD 
        [of "(indexing_ext F x n)" "{..<card (insert x ?F)}"])
      show "xa ∈ {..<card (insert x ?F)}"
         using xa 
        by (metis card_infinite card_insert_le gr_implies_not0 le_neq_implies_less 
          lessThan_iff less_or_eq_imp_le order_le_less_trans)
      show "y ∈ {..<card (insert x ?F)}"
        using y
        by (metis card_infinite card_insert_le gr_implies_not0 le_neq_implies_less 
          lessThan_iff less_or_eq_imp_le order_le_less_trans)
      show  "inj_on (indexing_ext F x n) {..<card (insert x ?F)}"
        using ob unfolding indexing_def bij_betw_def 
        by auto
    next
      show "indexing_ext F x n xa = indexing_ext F x n y"
      proof (cases "xa < n")
        case True note xa_l_n = True
        show ?thesis
        proof (cases "y < n")
          case True
          show ?thesis
            unfolding indexing_ext_def
            using xa_l_n True using h by simp
        next
          case False hence n_le_y: "n ≤ y" and xa_l_y: "xa < y" 
            using xa_l_n by simp_all
          have "?h xa = (indexing_ext F x n) xa"
            unfolding indexing_ext_def
            using xa_l_n by simp
          moreover have "?h y = (indexing_ext F x n) (Suc y)"
            using n_le_y
            unfolding indexing_ext_def by simp
          ultimately
          have eq: "(indexing_ext F x n) xa =  (indexing_ext F x n) (Suc y)" 
            using h by simp
          have "xa = Suc y"
          proof (rule inj_onD [of "indexing_ext F x n" "{..<card (insert x ?F)}"])
            show "inj_on (indexing_ext F x n) {..<card (insert x ?F)}"
              using ob
              unfolding indexing_def
              unfolding bij_betw_def by auto
            show "indexing_ext F x n xa = indexing_ext F x n (Suc y)"
              using eq .
            show "xa ∈ {..<card (insert x ?F)}"
              using xa
              by (metis card_infinite card_insert_disjoint lessThan_iff less_SucI less_zeroE x_notin_F)
            show "Suc y ∈ {..<card (insert x ?F)}"
              using x_notin_F using y
              by (metis Suc_mono card_infinite card_insert_disjoint lessThan_iff less_zeroE)
          qed
          hence False using xa_l_y by simp
          thus ?thesis by simp
        qed
      next
        case False
        hence n_le_xa: "n ≤ xa" using False by simp
        show ?thesis
        proof (cases "n = xa")
          case True note n_eq_xa = True
          show ?thesis
          proof (cases "y < n")
            case True
            have x_eq: "?h xa = indexing_ext F x n (Suc xa)"
              unfolding indexing_ext_def
              using n_eq_xa by simp
            moreover have y_eq: "?h y = indexing_ext F x n y"
              unfolding indexing_def
              using True unfolding indexing_ext_def by simp
            ultimately
            have eq: "(indexing_ext F x n) y =  (indexing_ext F x n) (Suc xa)"
              using h by simp
            have "y = Suc xa"
            proof (rule inj_onD [of "indexing_ext F x n" "{..<card (insert x ?F)}"])
              show "inj_on (indexing_ext F x n) {..<card (insert x ?F)}"
                using ob
                unfolding indexing_def
                unfolding bij_betw_def by auto
              show "indexing_ext F x n y = indexing_ext F x n (Suc xa)"
                using eq .
              show "y ∈ {..<card (insert x ?F)}"
                using y
                by (metis card_infinite card_insert_disjoint lessThan_iff less_SucI less_zeroE x_notin_F)
              show "Suc xa ∈ {..<card (insert x ?F)}"
                using x_notin_F using xa
                by (metis Suc_mono card_infinite card_insert_disjoint lessThan_iff less_zeroE)
            qed
            hence False using n_eq_xa True by simp
            thus ?thesis by simp
          next
            case False
            hence n_le_y: "n ≤ y" by simp
            show ?thesis
            proof (cases "n = y")
              case True note n_eq_y = True
              show ?thesis
                unfolding indexing_ext_def
                using n_eq_xa n_eq_y by simp
            next
              case False hence n_l_y: "n < y" using n_le_y by simp
              have x_eq: "?h xa = indexing_ext F x n (Suc xa)"
                unfolding indexing_ext_def
                using n_eq_xa by simp
              moreover have y_eq: "?h y = indexing_ext F x n (Suc y)"
                unfolding indexing_ext_def
                using n_l_y by simp
              ultimately
              have eq: "(indexing_ext F x n) (Suc y) = (indexing_ext F x n) (Suc xa)" 
                using h by simp
              have "Suc y = Suc xa"
              proof (rule inj_onD [of "indexing_ext F x n" "{..<card (insert x ?F)}"])
                show "inj_on (indexing_ext F x n) {..<card (insert x ?F)}"
                  using ob
                  unfolding indexing_def
                  unfolding bij_betw_def by auto
                show "indexing_ext F x n (Suc y) = indexing_ext F x n (Suc xa)"
                  using eq .
                show "Suc y ∈ {..<card (insert x ?F)}"
                  using y
                  by (metis Suc_mono card_infinite card_insert_disjoint lessThan_iff less_zeroE x_notin_F)
                show "Suc xa ∈ {..<card (insert x ?F)}"
                  using x_notin_F using xa
                  by (metis Suc_mono card_infinite card_insert_disjoint lessThan_iff less_zeroE)
              qed
              hence False using n_eq_xa n_l_y by simp
              thus ?thesis by simp
            qed
          qed
        next
          case False
          hence n_l_xa: "n < xa" using n_le_xa by simp
          show ?thesis
          proof (cases "y < n")
            case True note y_l_n = True
            have x_eq: "?h xa = indexing_ext F x n (Suc xa)"
              unfolding indexing_ext_def
              using n_l_xa by simp
            moreover have y_eq: "?h y = indexing_ext F x n y"
              unfolding indexing_ext_def
              using True by simp
            ultimately
            have eq: "(indexing_ext F x n) y =  (indexing_ext F x n) (Suc xa)" 
              using h by simp
            have "y = Suc xa"
            proof (rule inj_onD [of "indexing_ext F x n" "{..<card (insert x ?F)}"])
              show "inj_on (indexing_ext F x n) {..<card (insert x ?F)}"
                using ob
                unfolding indexing_def
                unfolding bij_betw_def by auto
              show "indexing_ext F x n y = indexing_ext F x n (Suc xa)"
                using eq .
              show "y ∈ {..<card (insert x ?F)}"
                using y
                by (metis card_infinite card_insert_disjoint lessThan_iff less_SucI less_zeroE x_notin_F)
              show "Suc xa ∈ {..<card (insert x ?F)}"
                using x_notin_F using xa
                by (metis Suc_mono card_infinite card_insert_disjoint lessThan_iff less_zeroE)
            qed
            hence False using n_l_xa True by simp
            thus ?thesis by simp
          next
            case False
            hence n_le_y: "n ≤ y" by simp
            show ?thesis
            proof (cases "n = y")
              case True note n_eq_y = True
              have "?h xa = (indexing_ext F x n) (Suc xa)"
                unfolding indexing_ext_def
                using n_l_xa by simp
              moreover have "?h y = (indexing_ext F x n) (Suc y)"
                using n_le_y
                unfolding indexing_ext_def by simp
              ultimately
              have eq: "(indexing_ext F x n) (Suc xa) =  (indexing_ext F x n) (Suc y)"
                using h by simp
              have "Suc xa = Suc y"
              proof (rule inj_onD [of "indexing_ext F x n" "{..<card (insert x ?F)}"])
                show "inj_on (indexing_ext F x n) {..<card (insert x ?F)}"
                  using ob
                  unfolding indexing_def
                  unfolding bij_betw_def by auto
                show "indexing_ext F x n (Suc xa) = indexing_ext F x n (Suc y)"
                  using eq .
                show "Suc xa ∈ {..<card (insert x ?F)}"
                  using xa 
                  by (metis Suc_mono card_infinite card_insert_disjoint lessThan_iff less_zeroE x_notin_F)
                show "Suc y ∈ {..<card (insert x ?F)}"
                  using x_notin_F using y
                  by (metis Suc_mono card_infinite card_insert_disjoint lessThan_iff less_zeroE)
              qed
              hence False using n_l_xa n_eq_y by simp
              thus ?thesis by simp
            next
              case False
              hence n_l_y: "n < y" using n_le_y by simp
              have "?h xa = (indexing_ext F x n) (Suc xa)"
                unfolding indexing_ext_def
                using n_l_xa by simp
              moreover have "?h y = (indexing_ext F x n) (Suc y)"
                using n_l_y
                unfolding indexing_ext_def by simp
              ultimately
              have eq: "(indexing_ext F x n) (Suc xa) =  (indexing_ext F x n) (Suc y)"
                using h by simp
              have "Suc xa = Suc y"
              proof (rule inj_onD [of "indexing_ext F x n" "{..<card (insert x ?F)}"])
                show "inj_on (indexing_ext F x n) {..<card (insert x ?F)}"
                  using ob
                  unfolding indexing_def
                  unfolding bij_betw_def by auto
                show "indexing_ext F x n (Suc xa) = indexing_ext F x n (Suc y)"
                  using eq .
                show "Suc xa ∈ {..<card (insert x ?F)}"
                  using xa
                  by (metis Suc_mono card_infinite card_insert_disjoint lessThan_iff less_zeroE x_notin_F)
                show "Suc y ∈ {..<card (insert x ?F)}"
                  using x_notin_F using y
                  by (metis Suc_mono card_infinite card_insert_disjoint lessThan_iff less_zeroE)
              qed
              thus ?thesis by simp
            qed
          qed
        qed
      qed
    qed
  qed
  show "?h ` {..<card ?F} = ?F"
  proof -
    have finite_iset_to_set_F: "finite (iset_to_set F)"
      by (metis bij_betw_finite finite_insert finite_lessThan fst_conv indexing_def iset_to_set_def ob)
    have surj_indexing: "(indexing_ext F x n) ` {..<card (insert x ?F)}=(insert x (?F))" 
      using ob unfolding indexing_def and bij_betw_def by auto
    have inj_on_indexing: "inj_on (indexing_ext F x n) {..<card (insert x ?F)}" 
      using ob unfolding indexing_def bij_betw_def by auto
    have descomposicion_conjunto: "{..<card (insert x ?F)}={..<n}∪{n}∪{n<..<card (insert x ?F)}" 
      using n1 and n2 and x_notin_F and card_insert_if and finite_iset_to_set_F 
      unfolding iset_to_set_def by auto
    have F_indexing_ext_desc:"(?F)=(indexing_ext F x n) ` {..<n} ∪ (indexing_ext F x n) ` {n<..<card (insert x ?F)}"
    proof -
      have descomposicion_conjuntos2: "{..<n} ∪ {n<..<card (insert x ?F)}={..<card (insert x ?F)}-{n}"
        using n2 and descomposicion_conjunto by auto
      have "(indexing_ext F x n) ` {..<n} ∪ (indexing_ext F x n) ` {n<..<card (insert x ?F)}
        =(indexing_ext F x n) ` ({..<n} ∪ {n<..<card (insert x ?F)})"
        by auto
      also have "...=indexing_ext F x n ` ({..<card (insert x ?F)}-{n})"
        using descomposicion_conjuntos2 by auto
      also have "...=indexing_ext F x n ` {..<card (insert x ?F)}-indexing_ext F x n `{n}"
      proof (rule inj_on_image_set_diff[OF inj_on_indexing])
        show "{..<card (insert x (iset_to_set F))} ⊆ {..<card (insert x (iset_to_set F))}" ..
        show "{n} ⊆ {..<card (insert x (iset_to_set F))}" using descomposicion_conjunto by auto
      qed
      also have "...= (insert x ?F) - {x}" using surj_indexing unfolding indexing_ext_def by auto
      also have "...=?F" using x_notin_F by auto
      finally show "?F= (indexing_ext F x n) ` {..<n} ∪ (indexing_ext F x n) ` {n<..<card (insert x ?F)}" by auto
    qed
    have card_insert_suc_eq: "card (insert x (?F))-Suc 0=card (?F)" 
      using card_insert_if and x_notin_F and finite_iset_to_set_F by auto
    have desc1: "(indexing_ext F x n) ` {..<n}=?h` {..<n}" unfolding indexing_ext_def by auto
    have desc2: "(indexing_ext F x n) ` {n<..<card (insert x ?F)}= ?h `{i. n≤i ∧ i<card (insert x (?F))-Suc 0}" 
      unfolding indexing_ext_def image_def Pi_def apply auto 
    proof -
      show "!!xa. [|n < xa; xa < card (insert x (fst F))|] 
        ==> ∃xb≥n. xb < card (insert x (fst F)) - Suc 0 ∧ snd F (xa - Suc 0) = snd F xb"
      proof -
        fix xa
        assume n_l_xa: "n < xa" and xa_l_card_xF: "xa < card (insert x (fst F))"
        show "∃xb≥n. xb < card (insert x (fst F)) - Suc 0 ∧ snd F (xa - Suc 0) = snd F xb"
        proof -
          let ?xb="xa-Suc 0"
          have "xa>0" using n1 and n_l_xa by auto
          hence 1:"?xb < card (insert x (fst F)) - Suc 0" using xa_l_card_xF by auto
          have 2:"snd F (xa - Suc 0) = snd F ?xb" ..
          have 3: "?xb≥n" using n_l_xa by auto
          show ?thesis using 1 and 2 and 3 by auto
        qed qed
      show "!!xa. [|n ≤ xa; xa < card (insert x (fst F)) - Suc 0|] 
        ==> ∃x∈{n<..<card (insert x (fst F))}. snd F xa = snd F (x - Suc 0)"
      proof -
        fix xa
        assume n_le_xa: "n ≤ xa" and xa_l_card_xF_suc: "xa < card (insert x (fst F)) - Suc 0"
        show "∃x∈{n<..<card (insert x (fst F))}. snd F xa = snd F (x - Suc 0)"
        proof (rule bexI[of _ "xa+Suc 0"])
          show " snd F xa = snd F (xa + Suc 0 - Suc 0)" by auto
          show "xa + Suc 0 ∈ {n<..<card (insert x (fst F))}" using n_le_xa and xa_l_card_xF_suc by auto
        qed qed qed
    have "?h ` {..<card ?F} = ?h`{..<n}∪?h`{i. n≤i ∧ i<card ?F}" using n2 by force
    also have "...=(indexing_ext F x n) ` {..<n} ∪ (indexing_ext F x n) ` {n<..<card (insert x ?F)}" 
      using desc1 and desc2 and card_insert_suc_eq by auto
    also have "...=?F" using F_indexing_ext_desc by simp
    finally show ?thesis . 
  qed 
qed


text{*From the above definitions we can define the operation insert for indexed sets.
  We don't assume that the new element (which is going to be inserted in the set) is not in
  the set, this will appear as a premise in the corresponding results.*}
text{*Given any indexed set $A$, an element $a$ and a position $n$, the operation $insert\_iset$ will introduce
$a$ in $iset\_to\_set$ $A$ in the position $n$ (modifying accordingly the original indexation $iset\_to\_index$ $A$).*}

definition insert_iset :: "'a iset => 'a => nat => 'a iset"
  where
  "insert_iset A a n 
  = (insert a (iset_to_set A), indexing_ext A a n)"

text{*Next lemma claims that if we insert an element in an @{text indexing}, we are increasing the cardinality of the set
in a unit.
Logically, we need to assume that the element which is going to be inserted is not in the set.*}
lemma insert_iset_increase_card:
  assumes indexing_A: "indexing (A,f)"
  and a_notin_A: "a ∉ A"
  shows "card (iset_to_set (insert_iset (A,f) a n) ) = card A + 1"
  by (metis a_notin_A card.insert fst_conv indexing_A indexing_finite insert_iset_def iset_to_set_def nat_add_commute)

text{*Given an indexing $(A,f)$, an element $a \notin A$ and a position $n\leq card (A)$, the result of inserting $a$
in $A$ in position $n$ will be an indexing:*}
lemma insert_iset_indexing:
  assumes indexing_A: "indexing (A,f)"
  and a_notin_A: "a ∉ A"
  and n2: "n ≤ (card A)"
  shows "indexing (insert_iset (A,f) a n)"
proof (unfold indexing_def,unfold bij_betw_def, rule conjI)
  have finite_A: "finite A" using indexing_finite[OF indexing_A] .
  have card_insert: "card (insert a A)=card A + 1" 
    using a_notin_A card_insert_if[OF finite_A] by force
  have descomposicion_conjunto: 
    "{..< card (insert a A)}={..<n}∪{n}∪{n<..<card (insert a A)}" 
    using n2
    by (metis Suc_eq_plus1 Un_commute Un_empty_right Un_insert_right 
      atLeastLessThanSuc_atLeastAtMost 
      atLeastSucAtMost_greaterThanAtMost 
      atLeastSucLessThan_greaterThanLessThan card_insert 
      ivl_disj_un(9) lessThan_Suc lessThan_Suc_atMost)
  show surj: "iset_to_index (insert_iset (A, f) a n) ` 
    {..<card (iset_to_set (insert_iset (A, f) a n))} 
    = iset_to_set (insert_iset (A, f) a n)"
  proof (unfold insert_iset_def, simp)
    have "∀x∈{..<n}. indexing_ext (A, f) a n x = f x" unfolding indexing_ext_def by auto
    hence ind_1: "indexing_ext (A, f) a n ` {..<n}= f `{..<n}" unfolding image_def by auto
    have "∀x∈{n<..< card (insert a A)}. indexing_ext (A, f) a n x = f (x - Suc 0)" unfolding indexing_ext_def by auto
    hence ind_2: "indexing_ext (A, f) a n ` {n<..< card (insert a A)} = f ` {i. n≤i ∧ i < card A}" unfolding image_def
    proof (auto)
      show "!!xa. [|∀x∈{n<..<card (insert a A)}. indexing_ext (A, f) a n x = f (x - Suc 0); n < xa; xa < card (insert a A)|]
        ==> ∃x≥n. x < card A ∧ f (xa - Suc 0) = f x"
      proof -
        fix xa
        assume n_l_xa: "n < xa" and xa_l_cardAa: "xa < card (insert a A)"
        show "∃x≥n. x < card A ∧ f (xa - Suc 0) = f x"
        proof - (*We can not use proof (rule bexI[of _ "xa - Suc 0"]) because it is not of the way: ∃?x ∈ ?A. *)
          let ?x="xa - Suc 0"
          have 1: "?x < card A" using xa_l_cardAa using card_insert 
            by (metis One_nat_def Suc_diff_1 Suc_eq_plus1 gr0I gr_implies_not0 
              less_diff_conv less_irrefl_nat linorder_neqE_nat n_l_xa xt1(9))
          have 2: "f (xa - Suc 0) = f ?x" by simp
          have 3: "?x≥n" using n_l_xa by simp
          show ?thesis using 1 and 2 and 3 by auto
        qed
      qed
      show "!!xa. [|∀x∈{n<..<card (insert a A)}. indexing_ext (A, f) a n x = f (x - Suc 0); n ≤ xa; xa < card A|]
        ==> ∃x∈{n<..<card (insert a A)}. f xa = f (x - Suc 0)"
      proof -
        fix xa
        assume n_le_xa: "n ≤ xa" and xa_l_cardA: "xa < card A"
        show "∃x∈{n<..<card (insert a A)}. f xa = f (x - Suc 0)"
        proof - 
          let ?x="xa + Suc 0"
          have 1: "f xa = f (?x - Suc 0)" by simp
          have 2: "?x∈{n<..<card (insert a A)}" using n_le_xa and xa_l_cardA card_insert by auto 
          show ?thesis using 1 and 2 by fast
        qed
      qed
    qed      
    have desc_indexing: "indexing_ext (A, f) a n ` {..<n} ∪ indexing_ext (A, f) a n ` {n<..<card (insert a A)} 
      = f`{..<card A}" 
      using ind_1 and ind_2 and n2 by force
    show "indexing_ext (A, f) a n ` {..<card (insert a A)} = insert a A"
    proof -
      have "indexing_ext (A, f) a n ` {..<card (insert a A)}
        = indexing_ext (A, f) a n ` {..<n}  ∪ indexing_ext (A, f) a n ` {n} 
        ∪ indexing_ext (A, f) a n ` {n<..<card (insert a A)}" using descomposicion_conjunto by blast
      also have "...= f`{..<card A} ∪ {a}" using desc_indexing unfolding indexing_ext_def by simp
      also have "...=insert a A" using indexing_A unfolding indexing_def bij_betw_def a_notin_A by force
      finally show ?thesis .
    qed
  qed
  show "inj_on (iset_to_index (insert_iset (A, f) a n)) 
    {..<card (iset_to_set (insert_iset (A, f) a n))}"
  proof (rule eq_card_imp_inj_on) --"We need to have proved previously the injectivity"
    show "finite {..<card (iset_to_set (insert_iset (A, f) a n))}" 
      unfolding insert_iset_def by simp
    show "card (iset_to_index (insert_iset (A, f) a n) ` {..<card (iset_to_set (insert_iset (A, f) a n))}) 
      = card {..<card (iset_to_set (insert_iset (A, f) a n))}" 
      using surj by simp
  qed
qed


text{*We introduce the definition of a generic function @{term remove_iset} which removes the
  $nth$ element of an indexed set. Logically, the position of the element which is going to be removed
  must be less than the cardinality of the set. The indexing must be also modified in such a way
  that every element above $n$ will decrease its position in one  unit. For instance, if we have the indexed set
  $\{(a,0),(b,1),(c,2)\}$ and we remove the position $0$, we will obtain $\{(b,0),(c,1)\}$.*}

definition remove_iset :: "'a iset => nat => 'a iset"
  where "remove_iset A n = (fst A - {(snd A) n},
  (λk. if k < n then (snd A) k  else (snd A) (Suc k)))"

text{*Here an equivalent definition to @{thm remove_iset_def}:*}

lemma remove_iset_def':
  "remove_iset (A, f) n = (A - {f n},  (λk. if k < n then f k  else f (Suc k)))"
  unfolding remove_iset_def by (auto simp add: fun_eq_iff)

text{*The following lemma proves that, for any indexing, the result of removing an element in a valid position will be
again an indexing. This is a long lemma (about 150 lines).*}
lemma
  indexing_remove_iset:
  assumes i: "indexing (B, h)"
  and n: "n < card B"
  shows "indexing (remove_iset (B, h) n)"
proof (unfold indexing_def bij_betw_def, intro conjI, simp)
  have fin_B: "finite B" using indexing_finite[OF i] .
  have h_n_in_B: "h n ∈ B" 
    using n i unfolding indexing_def bij_betw_def by auto
  have eq_i: "!!x y. [|x ∈ {..<card B}; y ∈ {..<card B}; h x = h y|] 
    ==> x = y"
    using i unfolding indexing_def bij_betw_def inj_on_def 
    by auto
  show "inj_on (snd (remove_iset (B, h) n)) 
    {..<card (fst (remove_iset (B, h) n))}"
    unfolding remove_iset_def
    unfolding inj_on_def
  proof (rule ballI, rule ballI, rule impI, unfold fst_conv snd_conv)
    fix x y
    assume x: "x ∈ {..<card (B - {h n})}" 
      and y: "y ∈ {..<card (B - {h n})}"
      and eq: "(if x < n then h x else h (Suc x)) = (if y < n then h y else h (Suc y))"
    show "x = y"
    proof (cases "x < n")
      case True note x_l_n = True
      show "x = y"
      proof (cases "y < n")
        case True
        show "x = y"
        proof (rule eq_i)
          show "x ∈ {..<card B}" using x 
            by (metis lessThan_iff less_or_eq_imp_le n order_le_less_trans x_l_n)
          show "y ∈ {..<card B}" using y 
            by (metis lessThan_iff less_or_eq_imp_le n order_le_less_trans True)
          show "h x = h y" using eq x_l_n True by simp
        qed
      next
        case False
        have "x ≠ (Suc y)" using x_l_n False by auto
        moreover have "x = (Suc y)"
        proof (rule eq_i)
          show "x ∈ {..<card B}" using x
            by (metis lessThan_iff less_or_eq_imp_le n order_le_less_trans x_l_n)
          show "(Suc y) ∈ {..<card B}" using y using h_n_in_B 
            by (metis Suc_eq_plus1  `x ∈ {..<card B}` card_Diff_singleton card_infinite 
              emptyE lessThan_0 lessThan_iff less_diff_conv) 
          show "h x = h (Suc y)" using eq x_l_n False by simp
        qed
        ultimately have False by contradiction
        thus ?thesis by fast
      qed
    next
      case False hence n_le_x: "n ≤ x" by arith
      show "x = y"
      proof (cases "y < n")
        case True
        have x_ne_y: "(Suc x) ≠ y" using n_le_x True by auto
        moreover have "(Suc x) = y"
        proof (rule eq_i)
          show "y ∈ {..<card B}" using y
            by (metis lessThan_iff less_or_eq_imp_le n order_le_less_trans True)
          show "(Suc x) ∈ {..<card B}" using x using h_n_in_B 
            by (metis Suc_eq_plus1  `y ∈ {..<card B}` card_Diff_singleton card_infinite 
              emptyE lessThan_0 lessThan_iff less_diff_conv)
          show "h (Suc x) = h y" using eq True n_le_x by simp
        qed
        ultimately have False by contradiction
        thus "x = y" by fast
      next
        case False
        have "Suc x = Suc y"
        proof (rule eq_i)
          show "Suc x ∈ {..<card B}"
            using x using card_Diff1_less [OF fin_B h_n_in_B] using h_n_in_B
            by (metis Suc_eq_plus1 card_Diff_singleton fin_B lessThan_iff less_diff_conv)
          show "Suc y ∈ {..<card B}"
            using y using card_Diff1_less [OF fin_B h_n_in_B] using h_n_in_B
            by (metis Suc_eq_plus1 card_Diff_singleton fin_B lessThan_iff less_diff_conv)
          show "h (Suc x) = h (Suc y)"
            using eq using False using n_le_x by simp
        qed
        thus "x = y" by simp
      qed
    qed
  qed
  have h_im: "h ` {..<card B} = B" using i unfolding indexing_def bij_betw_def by auto
  show "iset_to_index (remove_iset (B, h) n) ` 
    {..<card (iset_to_set (remove_iset (B, h) n))} 
    = iset_to_set (remove_iset (B, h) n)"
  proof (unfold remove_iset_def iset_to_index_def iset_to_set_def fst_conv snd_conv)
    show "(λk. if k < n then h k else h (Suc k)) ` {..<card (B - {h n})} = B - {h n}"
      (is "?h' ` {..<card (B - {h n})} = B - {h n}")
    proof -
      have "B - {h n} = h ` ({..<card B} - {n})"
        using bij_betw_image_minus [symmetric, of h "{..<card B}" B n]
        using n using i unfolding indexing_def bij_betw_def by simp
      also have "... = h ` ({..<n} ∪ {n<..<card B})" using n by auto
      also have "... = h ` {..<n} ∪ h ` {n<..<card B}" unfolding image_Un ..
      also have "... = ?h' ` {..<n} ∪ h ` {n<..<card B}" by auto
      also have "... = ?h' ` {..<n} ∪ ?h' ` {n..<card (B - {h n})}"
      proof -
        have "?h' ` {n..<card (B - {h n})} = h ` {n<..<card B}"
          unfolding image_def using fin_B h_n_in_B 
        proof (auto, force)
          fix xa
          assume n: "n < xa" and xa: "xa < card B"
          hence xa_n_0: "0 < xa" by simp
          show "∃x∈{n..<card B - Suc 0}. h xa = h (Suc x)"
            apply (rule bexI [of _ "xa - 1"])
            apply (metis Suc_diff_1 xa_n_0)
            using n xa xa_n_0 by force
        qed
        thus ?thesis by fast
      qed
      also have "... = ?h' ` ({..<n} ∪ {n..<card (B - {h n})})"
        by (rule image_Un [symmetric, of "?h'" "{..<n}" "{n..<card (B - {h n})}"]) 
      also have "... = ?h' ` {..<card (B - {h n})}" using n using fin_B h_n_in_B by auto
      finally show ?thesis by simp
    qed
  qed
qed

text{*The result of inserting an element in an indexed set in position $n$ and then removing the element in position
$n$ is the original indexed set.*}

lemma
  remove_iset_insert_iset_id:
  assumes x_notin_A: "x ∉ A"
  and n_l_c: "n < card A"
  shows "remove_iset (insert_iset (A, f) x n) n = (A, f)"
  unfolding insert_iset_def
  using x_notin_A
  unfolding indexing_ext_def
  unfolding remove_iset_def by (auto simp add: fun_eq_iff n_l_c)

(*
text{*Función para insertar el primer elemento de B en la última posición de A.
  Esta función no modifica el conjunto B, luego no nos vale para iterar.*}
definition insert_iset_last_position :: "'a iset => 'a iset => 'a iset"
  where 
  "insert_iset_last_position A B = 
  insert_iset A ((iset_to_index B) 0 ) (card (iset_to_set A))"

text{*Lo mismo que la anterior pero borrando de B el elemento que se
  inserta en A. Esta función la podremos iterar.*}
definition insert_iset_last_position_2 :: "'a iset => 'a iset 
  => ('a iset × 'a iset)"
  where 
  "insert_iset_last_position_2 A B = 
  (insert_iset_last_position A B,remove_iset B 0)"

lemma fst_in_insert_iset_last_position:
 shows "A ⊆ iset_to_set (fst (insert_iset_last_position_2 (A,f) (B,g)))"
 unfolding insert_iset_last_position_2_def
 insert_iset_last_position_def insert_iset_def by auto


lemma fst_insert_last_position:
shows "iset_to_set(insert_iset_last_position (A,f) (B,g))=A∪{g(0)}"
unfolding iset_to_set_def insert_iset_last_position_def insert_iset_def iset_to_index_def by auto

lemma fst_insert_last_position_2:
shows "iset_to_set (fst((insert_iset_last_position_2) (A,f) (B,g)))=A∪{g(0)}"
by (metis fst_conv fst_insert_last_position insert_iset_def 
insert_iset_last_position_2_def insert_iset_last_position_def iset_to_set_def)



lemma fst_insert_last_position_2_iterada:
assumes indexing_A_f: "indexing (A,f)"
and indexing_B_g: "indexing (B,g)"
 and disjuntos: "A∩B={}" 
-- "Añado otras dos que son necesarias"
 and B_not_empty: "B≠{}"
and finite_B: "finite B"
 shows "iset_to_set (fst((insert_iset_last_position_2 ^(card B)) (A,f) (B,g)))=A∪B"
proof (induct "card B")
 case 0 thus ?thesis using B_not_empty finite_B by simp
next
case Suc show ?thesis
proof - 
thm Suc.hyps
have "(insert_iset_last_position_2 ^ Suc x) (A, f) (B, g)=
  (insert_iset_last_position_2 ^ (x + Suc 0)) (A, f) (B, g)" by auto
 
--"No me deja porque la función devuelve algo (_,_) y tiene de entradas 
2 parámetros (es distinto A B que (A,B))"
also have "...=
  insert_iset_last_position_2 ((insert_iset_last_position_2 ^ x) (A, f) (B, g))"
also have "...=
  insert_iset_last_position_2 fst((insert_iset_last_position_2 ^ x) (A, f) (B, g)) snd((insert_iset_last_position_2 ^ x) (A, f) (B, g))"
...
qed


lemma indexing_insert_last_position:
assumes indexing_A_f: "indexing (A,f)"
and indexing_B_g: "indexing (B,g)"
and disjuntos: "A∩B={}"
shows "indexing (fst (insert_iset_last_position_2 (A,f) (B,g)))"
 using indexing_A_f indexing_B_g
using indexing_indexing_ext unfolding indexing_def unfolding insert_iset_last_position_2_def
 insert_iset_last_position_def unfolding insert_iset_def 
using disjuntos sorry 
*)


text{*Next lemma is a good example of proof by acumulation of facts, and it is ideal 
  to structure it using @{text "moreover"}  and finish it with @{term ultimately}. 
  However, we can use @{thm "conjI4"[no_vars]} to abridge it:*}

text{*The lemma claims that given an indexing $(X,f)$, there exists an indexing $(insert\mbox{ }x\mbox{ }X,h)$
which places $x$ in the last position (and keeps the elements of $X$ in their original places).*}
lemma indexation_x_union_X:
  assumes finite: "finite X" and x_not_in_X: "x ∉ X"
  and f_buena:"f ∈ {i. i < (card X)} -> X" and ordenFX: "f ` {i. i < (card X)} = X"
  shows  "∃h. (h ∈ {i. i < (card (insert x X))} -> (insert x X) 
  ∧ h`{i. i < (card (insert x X))} = (insert x X)
  ∧ h (card X) = x ∧ (∀i. i<card(X) --> h i = f i))"
proof (rule exI [of _ "(λi::nat. if i<(card X) then f(i) else x)"], rule conjI4)
  let ?h = "(λi::nat. if i<(card X) then f(i) else x)"
  show "?h ∈ {i. i < card (insert x X)} -> insert x X"
    using f_buena unfolding Pi_def by auto
  show "?h ` {i. i < card (insert x X)} = insert x X"
    using ordenFX
    unfolding card_insert_disjoint [OF finite x_not_in_X]
    unfolding less_than_Suc_union
    unfolding image_Un by auto
  show "(if card X < card X then f (card X) else x) = x" by simp
  show "(∀i<card X. (if i < card X then f i else x) = f i)" by simp
qed

(*The same proof but using moreover:*)
(*
lemma indexation_x_union_X:
  assumes finite: "finite X" 
  and x_not_in_X: "x ∉ X"
  and f_buena:"f ∈ {i. i < (card X)} -> X" 
  and ordenFX: "f ` {i. i < (card X)} = X"
  shows  "∃h. (h ∈ {i. i < (card (insert x X))} -> (insert x X) ∧
  h`{i. i < (card (insert x X))} = (insert x X)
  ∧ h (card X) = x ∧ (∀i. i<card(X) --> h i = f i))"
proof -
  let ?h = "(λi::nat. if i<(card X) then f(i) else x)"
  have h_f: "(∀i. i<card(X) --> ?h(i)=f(i))" by auto
  hence 0:"?h`{i. i < (card X)} = f`{i. i < (card X)}" by auto
  have ordenHX:"?h`{i. i < (card X)} = X" using ordenFX by auto
  moreover have h_cardX_x: "?h (card X) = x" by auto
  moreover have ordenH_xX: "?h`{i. i < (card (insert x X))} = (insert x X)"
  proof -
    have 1: "card (insert x X) = Suc(card X)" using card_insert_if and x_not_in_X and finite by auto
    hence 2:"{i. i < (card X)} ∪ {i. i=card(X)}= {i. i < (card (insert x X))}" by auto
    have "?h`({i. i < (card X)} ∪ {i. i=card(X)})=?h`({i. i < (card X)}) ∪ ?h`({i. i=card(X)})" by auto
    also have "…= (X ∪ {x})" using h_cardX_x and ordenHX by auto
    finally have 3:"?h`({i. i < (card X)} ∪ {i. i=card(X)})=(insert x X)" by auto
    have "?h`({i. i < (card X)} ∪ {i. i=card(X)})=?h` {i. i < (card (insert x X))}" using 2 by auto
    thus ?thesis using 3 by auto
  qed
  moreover hence h:"?h ∈ {i. i < (card (insert x X))} -> (insert x X)" unfolding Pi_def by auto
  ultimately show ?thesis by auto
qed
*)

text{*This is an indispensable lemma to prove the theorem that claims that an independent set
  can be completed to a basis. Given any pair of (disjoint) sets $A$ and $B$, there exists an indexing
  function $h$ which places the elements of $A$ in the first $card(A)$ positions and then the elements of $B$. In
  the proof, the indexing function is explicitly provided:*}

lemma indexing_union: 
  assumes disjuntos: "A∩B={}"
  and finite_A: "finite A"
  and A_not_empty: "A≠{}" --"If not the result is trivial."
  and finite_B: "finite B"
  shows "∃h. indexing (A∪B,h) ∧ h` {..<card(A)}= A 
  ∧ h` ({..<(card(A)+card(B))}-{..<card(A)})=B"
proof -
  have "∃f. indexing (A,f)" using obtain_indexing[OF finite_A] .
  from this obtain f where indexing_A_f: "indexing (A,f)" by auto
  have "∃g. indexing (B,g)" using obtain_indexing[OF finite_B] .
  from this obtain g where indexing_B_g:  "indexing (B,g)" by auto
  show ?thesis
  proof (rule exI[of _ "(λx. if x∈ {..<card(A)} 
      then f(x) else g(x-card(A)))"])
    let ?h="(λx. if x∈ {..<card(A)} then f(x) else g(x-card(A)))"
    have "∀x∈{..<card(A)}. f(x)= ?h (x)" by simp
    hence surj_h_A: "?h` {..<card(A)}=A" 
      using indexing_A_f unfolding indexing_def bij_betw_def by auto
    have "∀x∈{..<(card(A)+card(B))}-{..<card(A)}. g(x-card(A))=?h(x)" by auto
    hence "?h` ({..<(card(A)+card(B))}-{..<card(A)}) = g`{..<card(B)}"
      unfolding image_def
    proof (auto)
      fix xa
      assume xa_le_cardB: "xa < card B"
      show "∃x∈{..<card A + card B} - {..<card A}. g xa = g (x - card A)"
      proof (rule bexI[of _ "xa+card(A)"])
        have cardA_not_zero: "card A ≠ 0" using A_not_empty finite_A by auto
        thus "g xa = g (xa + card A - card A)" by auto
        show " xa + card A ∈ {..<card A + card B} - {..<card A}"
          by (metis DiffI diff_add_inverse lessThan_iff less_diff_conv not_add_less2 xa_le_cardB)
      qed
    qed
    hence surj_h_B: "?h` ({..<(card(A)+card(B))}-{..<card(A)})=B" 
      using indexing_B_g unfolding indexing_def and bij_betw_def by auto
    have indexing: "indexing (A∪B,?h)"
    proof (unfold indexing_def, simp,unfold  bij_betw_def)
      have 1: "?h ` {..<card (A ∪ B)} = A ∪ B"
      proof -
        have "card (A∪B)=card(A)+card(B)" using disjuntos and finite_A finite_B card_Un_disjoint by auto
        hence "{..<card (A ∪ B)}={..<card(A)+card(B)}" by simp
        also have "...={..<card(A)} ∪ ({..<(card(A)+card(B))}-{..<card(A)})" by auto
        finally have "?h` {..<card (A ∪ B)} = ?h ` {..<card(A)} ∪ ?h ` ({..<(card(A)+card(B))}-{..<card(A)})" by force
        thus ?thesis using surj_h_B and surj_h_A by auto
      qed
      have 2: "inj_on ?h {..<card (A ∪ B)}"
      proof (rule eq_card_imp_inj_on) 
        show "finite {..<card (A ∪ B)}" using finite_A and finite_B by auto
        show " card (?h ` {..<card (A ∪ B)}) = card {..<card (A ∪ B)}"
          using 1 and card_lessThan by auto
      qed
      show "inj_on (λx. if x < card A then f x else g (x - card A))
        {..<card (A ∪ B)} ∧
        (λx. if x < card A then f x else g (x - card A)) ` {..<card (A ∪ B)} =
        A ∪ B"
        using 1 and 2 by auto
    qed
    show "indexing(A ∪ B,?h) ∧
      ?h `{..<card A} = A ∧
      ?h `({..<card A + card B} - {..<card A}) =
      B" using indexing surj_h_A surj_h_B by auto 
  qed
qed

text{*Now we are going to define a new function which returns the position where an element @{term a} is in a set $A$.
  When we use this function it is very important to assume that @{term "a ∈ A"}, 
  since functions are total in HOL, and without the premise @{term "a ∈ A"} we would obtain an undefined value of the righ type.
  An alternative definition could be made writing LEAST instead of THE and then we could remove @{term "n < card A"}.
  Note that both THE and LEAST are based on the Hilbert's $\epsilon$ operator, 
  which, in general, places us out of a constructive setting.*}

text{*This function will be very important for the proof that each basis of a vector space has the same cardinality.*}

definition obtain_position :: "'c=>'c iset => nat"
  where "obtain_position a A = (THE n. (snd A) n = a 
  ∧ n < card (fst A))"
(*where "obtain_position a A = (LEAST n. (snd A) n = a)" *)

text{*Under the right premises, this natural number exists and is smaller than $card(A)$ which ensures that 
  @{text obtain_position} is well-defined.*}

lemma exists_n_obtain_position:
  assumes  a_in_A: "a ∈ A"
  and indexing_A: "indexing (A,f)"
  shows "∃n::nat. f n = a"
proof -
  have "A≠{}" using a_in_A by blast
  hence cardA_g_0: "card A > 0" using card_gt_0_iff and indexing_finite[OF indexing_A] by blast
  thus ?thesis using a_in_A indexing_A unfolding indexing_def bij_betw_def by force
qed

text{*We proof that exists someone that also verifies @{term "n < card A"}*}

lemma exists_n_and_less_card_obtain_position:
  assumes  a_in_A: "a ∈ A"
  and indexing_A: "indexing (A,f)"
  shows "∃n::nat. f n = a ∧ n < (card A)"
proof -
  have "A≠{}" using a_in_A by blast
  hence cardA_g_0: "card A > 0" 
    using card_gt_0_iff and indexing_finite[OF indexing_A] by blast
  thus ?thesis using a_in_A indexing_A unfolding indexing_def bij_betw_def by force
qed

text{*Thanks to the previous lemma and the injectivity of indexing functions, 
  we can prove the existence and the unicity of @{text obtain_position}:*}
lemma exists_n_and_is_unique_obtain_position:
  assumes  a_in_A: "a∈ A"
  and indexing_A: "indexing (A,f)"
  shows "∃!n::nat. f n = a ∧ n < (card A)"
proof (rule ex_ex1I)
  show "∃n. f n = a ∧ n < card A" 
    using exists_n_and_less_card_obtain_position 
    [OF a_in_A indexing_A] .
  show "!!n y. [|f n = a ∧ n < card A; f y = a ∧ y < card A|] 
    ==> n = y "
  proof -
    fix n and y
    assume hip_n: "f n = a ∧ n < card A" 
      and hip_y: "f y = a ∧ y < card A"
    show "n=y"
    proof -
      have inj_on: "inj_on f {..<card A}" 
        using indexing_A unfolding indexing_def bij_betw_def by simp
      show ?thesis using inj_on_eq_iff[OF inj_on _ _ ] using hip_n hip_y by auto
    qed
  qed
qed

text{*Now that we have proved that @{text obtain_position} is well defined, we prove that its result satisfies the required properties. The number which is returned by @{text obtain_position} is less than the cardinal of the set:*}

lemma obtain_position_less_card:
  assumes a_in_A: "a ∈ A"
  and indexing_A: "indexing (A,f)" 
  shows "(obtain_position a (A,f)) < card A" 
proof (unfold obtain_position_def)
  let ?P = "(λn. f n = a ∧ n < card A)"
  have exK: "(∃!k. ?P k)" 
    using exists_n_and_is_unique_obtain_position[OF a_in_A indexing_A] .
  have ex_THE: "?P (THE k. ?P k)"
    using theI' [OF exK] .
  def n≡"(THE k. ?P k)"
  have "n < card A" unfolding n_def
    by (metis ex_THE)
  thus "(THE n. snd (A, f) n = a ∧ n < card (fst (A, f))) < card A"
    by (metis ex_THE fst_conv n_def snd_conv)
qed

text{*The function really returns the position of the element.*}
lemma obtain_position_element:
  assumes a_in_A: "a ∈ A"
  and indexing_A: "indexing (A,f)" 
  shows "f (obtain_position a (A,f)) = a" 
proof (unfold obtain_position_def)
  let ?P = "(λn. f n = a ∧ n < card A)"
  have exK: "(∃!k. ?P k)" 
    using exists_n_and_is_unique_obtain_position[OF a_in_A indexing_A] .
  have ex_THE: "?P (THE k. ?P k)"
    using theI' [OF exK] .
  def n≡"(THE k. ?P k)"
  have "f n = a" unfolding n_def
    by (metis ex_THE)
  thus "f (THE n. snd (A, f) n = a ∧ n < card (fst (A, f))) = a"
    by (metis ex_THE fst_conv n_def snd_conv)
qed

text{*An element will not be in the set returned by the function @{text remove_iset} 
called with the position of that element.*}
lemma a_notin_remove_iset:
  assumes a_in_A: "a ∈ A"
  and indexing_A: "indexing (A,f)"
  shows "a ∉ fst (remove_iset (A,f) (obtain_position a (A,f)))"
  unfolding remove_iset_def 
  using obtain_position_element[OF a_in_A indexing_A] by simp


text{*Finally some important theorems to prove future properties of indexed sets. Isabelle has an induction rule to prove
  properties of finite sets. Unfortunately, this rule is of little help for proving properties 
  of indexed sets, since the set and the indexing function must behave accordingly 
  in the induction rule, and their inherent properties. Consequently,
  we have to introduce a special induction rule for indexed sets.*}

text{*First an auxiliary lemma:*}
lemma exists_indexing_ext: 
  assumes i: "indexing (insert x A, f)"
  shows "∃h. ∃n ∈ {..card A}. (f = (indexing_ext (A, h) x) n)" 
proof -
  have x_in_insert: "x ∈ (insert x A)" by simp
  from i obtain n where n_less_card_insert: "n < card (insert x A)" 
    and fn_x: "f n = x" using obtain_position_less_card[OF x_in_insert i] 
    and obtain_position_element[OF x_in_insert i]
    by blast
  show ?thesis 
  proof (rule exI, rule bexI[of _ "n"])
    have "finite (insert x A)" using indexing_finite[OF i] .
    thus "n ∈ {..card A}" using n_less_card_insert and x_in_insert
      by (metis atMost_iff card_insert_disjoint 
        finite_insert insert_absorb less_or_eq_imp_le linorder_not_le not_less_eq_eq)
    def h≡"(λx. if x < n then f x else f (x + 1))"
    show "f = indexing_ext (A, h) x n"
      unfolding indexing_ext_def unfolding h_def fun_eq_iff 
      using n_less_card_insert fn_x 
      by fastsimp
  qed 
qed

text{*The first one induction rule:*}
theorem
  indexed_set_induct:
  assumes "indexing (A, f)"
  and "finite A"
  and "!!f. indexing ({}, f) ==> P {} f"
  and step: "!!a A f n. [|a ∉ A; finite A; indexing (A, f); 
              0 ≤ n; n ≤ card A|] ==> P (insert a A) ((indexing_ext (A, f) a) n)"
  shows "P A f"
  using `finite A` and `indexing (A, f)`
proof (induct arbitrary: f)
  case empty
  show ?case using empty (1) by fact
next
  case (insert x F h')
  show ?case
  proof -
    obtain h n 
      where h'_def: "h' = (indexing_ext (F, h) x) n"
      and n1: "0 ≤ n"
      and n2: "n ≤ card F"
      using exists_indexing_ext[OF insert.prems] by blast
    show ?case
      unfolding h'_def
    proof (rule step)
      show "x ∉ F" by fact
      show "finite F" by fact
      show "indexing (F, h)"
        apply (rule indexing_indexing_ext [of x _ n])
        using insert.prems unfolding h'_def apply simp
        unfolding iset_to_set_def fst_conv by fact+
      show "0 ≤ n" using n1 .
      show "n ≤ card F" using n2 .
    qed
  qed
qed


text{*This induction rule is similar to the proper of finite sets,
  @{thm finite_induct[no_vars]}, but taking into account the indexing. Thus, if a property $P$ holds for the empty set
  and one of its indexing functions, and when it holds for a given set $A$ and an indexing function $f$, we now
  how to prove it for the pair $insert$ $a$ $A$ (with $a \notin A$) and any of the extensions of $f$, then $P$ holds
  for every indexing $(A,f)$. The proof of the property is completed by induction over the set $A$, but keeping $f$ free
  for later instantiation with the right indexing functions.*}

lemma
  indexed_set_induct2 [case_names indexing finite empty insert]:
  assumes "indexing (A, f)"
  and "finite A"
  and "!!f. indexing ({}, f) ==> P {} f"
  and step: "!!a A f n. [|a ∉ A; 
           [| indexing (A, f) |] ==> P A f; 
           finite (insert a A);
           indexing ((insert a A), (indexing_ext (A, f) a n));
           0 ≤ n; n ≤ card A |] ==> 
           P (insert a A) (indexing_ext (A, f) a n)"
  shows "P A f"
  using `finite A` and `indexing (A, f)`
proof (induct arbitrary: f)
  case empty
  show ?case using empty (1) by fact
next
  case (insert x F h')
  show ?case
  proof - 
    obtain n h
      where h'_def: "h' = (indexing_ext (F, h) x) n"
      and n1: "0 ≤ n"
      and n2: "n ≤ card F" using exists_indexing_ext[OF insert.prems] by blast
    show ?case
      unfolding h'_def
    proof (rule step)
      show "x ∉ F" by fact
      have i_F_h: "indexing (F, h)"
        apply (rule indexing_indexing_ext [of x "(F, h)" n])
        using insert.prems unfolding h'_def
        using n1 n2 insert.hyps (2) by simp_all
      show "P F h" by (rule insert.hyps (3)) (rule i_F_h)
      show "0 ≤ n" using n1 .
      show "n ≤ card F" using n2 .
      show "finite (insert x F)" using insert.hyps (1) by simp
      show "indexing (insert x F, indexing_ext (F, h) x n)"
        using insert.prems unfolding h'_def .
    qed
  qed
qed

end