Theory InductiveSeq_ZF

theory InductiveSeq_ZF
imports FiniteSeq_ZF
(* 
    This file is a part of IsarMathLib - 
    a library of formalized mathematics for Isabelle/Isar.

    Copyright (C) 2007  Slawomir Kolodynski

    This program is free software; Redistribution and use in source and binary forms, 
    with or without modification, are permitted provided that the following conditions are met:

   1. Redistributions of source code must retain the above copyright notice, 
   this list of conditions and the following disclaimer.
   2. Redistributions in binary form must reproduce the above copyright notice, 
   this list of conditions and the following disclaimer in the documentation and/or 
   other materials provided with the distribution.
   3. The name of the author may not be used to endorse or promote products 
   derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED 
WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF 
MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. 
IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, 
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, 
PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; 
OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, 
WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR 
OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, 
EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

*)
header{*\isaheader{InductiveSeq\_ZF.thy}*}

theory InductiveSeq_ZF imports Nat_ZF_IML FiniteSeq_ZF

begin

text{*In this theory we discuss sequences defined by conditions of the form
  $a_0 = x,\  a_{n+1} = f(a_n)$ and similar.*}

section{*Sequences defined by induction*}

text{*One way of defining a sequence (that is a function $a:\mathbb{N}\rightarrow X$)
  is to provide the first element of the sequence and a function to find the next 
  value when we have the current one. This is usually called "defining a sequence
  by induction". In this section we set up the notion of
  a sequence defined by induction and prove the theorems needed to use it.*}

text{*First we define a helper notion of the sequence defined inductively up to a 
  given natural number $n$. *}

definition
  "InductiveSequenceN(x,f,n) ≡ 
  THE a. a: succ(n) -> domain(f) ∧ a`(0) = x ∧ (∀k∈n. a`(succ(k)) = f`(a`(k)))"

text{*From that we define the inductive sequence on the 
  whole set of natural numbers. Recall that in Isabelle/ZF the set of natural numbers
  is denoted @{text "nat"}.*}

definition
  "InductiveSequence(x,f) ≡ \<Union>n∈nat. InductiveSequenceN(x,f,n)"

text{*First we will consider the question of existence and uniqueness 
  of finite inductive sequences. The proof
  is by induction and the next lemma is the $P(0)$ step. To understand the notation
  recall that for natural numbers in set theory we have $n = \{0,1,..,n-1\}$ and
  @{text "succ(n)"}$ = \{0,1,..,n\}$.*}

lemma indseq_exun0: assumes A1: "f: X->X" and A2: "x∈X"
  shows 
  "∃! a. a: succ(0) -> X ∧ a`(0) = x ∧ ( ∀k∈0. a`(succ(k)) = f`(a`(k)) )"
proof
  fix a b
  assume A3:  
    "a: succ(0) -> X ∧ a`(0) = x ∧ ( ∀k∈0. a`(succ(k)) = f`(a`(k)) )"
    "b: succ(0) -> X ∧ b`(0) = x ∧ ( ∀k∈0. b`(succ(k)) = f`(b`(k)) )"
  moreover have "succ(0) = {0}" by auto
  ultimately have "a: {0} -> X"  "b: {0} -> X" by auto
  then have "a = {⟨0, a`(0)⟩}"   "b = {⟨0, b`(0)⟩}" using func_singleton_pair
    by auto
  with A3 show "a=b" by simp
next 
  let ?a = "{⟨0,x⟩}"
  have "?a : {0} -> {x}" using singleton_fun by simp
  moreover from A1 A2 have "{x} ⊆ X" by simp
  ultimately have "?a : {0} -> X"
    using func1_1_L1B by blast
  moreover have "{0} = succ(0)" by auto
  ultimately have "?a : succ(0) -> X" by simp
  with A1 show 
    "∃ a. a: succ(0) -> X ∧ a`(0) = x ∧ (∀k∈0. a`(succ(k)) = f`(a`(k)))"
    using singleton_apply by auto
qed

text{*A lemma about restricting finite sequences needed for the proof of
  the inductive step of the existence and uniqueness of finite inductive seqences.*}

lemma indseq_restrict: 
  assumes A1: "f: X->X" and A2: "x∈X" and A3: "n ∈ nat" and
  A4: "a: succ(succ(n))-> X ∧ a`(0) = x ∧ (∀k∈succ(n). a`(succ(k)) = f`(a`(k)))"
  and A5: "ar = restrict(a,succ(n))"
  shows 
  "ar: succ(n) -> X ∧ ar`(0) = x ∧ ( ∀k∈n. ar`(succ(k)) = f`(ar`(k)) )"
proof -
  from A3 have "succ(n) ⊆ succ(succ(n))" by auto
  with A4 A5 have "ar: succ(n) -> X" using restrict_type2 by auto
  moreover
  from A3 have "0 ∈ succ(n)" using empty_in_every_succ by simp
  with A4 A5 have "ar`(0) = x" using restrict_if by simp
  moreover from A3 A4 A5 have "∀k∈n. ar`(succ(k)) = f`(ar`(k))"
    using succ_ineq restrict_if by auto
  ultimately show ?thesis by simp
qed

  
text{*Existence and uniqueness of finite inductive sequences. The proof
  is by induction and the next lemma is the inductive step.*}

lemma indseq_exun_ind: 
  assumes A1: "f: X->X" and A2: "x∈X" and A3: "n ∈ nat" and 
  A4: "∃! a. a: succ(n) -> X ∧ a`(0) = x ∧ (∀k∈n. a`(succ(k)) = f`(a`(k)))"
  shows 
  "∃! a. a: succ(succ(n)) -> X ∧ a`(0) = x ∧ 
  ( ∀k∈succ(n). a`(succ(k)) = f`(a`(k)) )"
proof
  fix a b assume
    A5: "a: succ(succ(n)) -> X ∧ a`(0) = x ∧ 
    ( ∀k∈succ(n). a`(succ(k)) = f`(a`(k)) )" and
    A6: "b: succ(succ(n)) -> X ∧ b`(0) = x ∧ 
    ( ∀k∈succ(n). b`(succ(k)) = f`(b`(k)) )"
  show "a = b"
  proof -
    let ?ar = "restrict(a,succ(n))"
    let ?br = "restrict(b,succ(n))"
    note A1 A2 A3 A5
    moreover have "?ar = restrict(a,succ(n))" by simp
    ultimately have I:
      "?ar: succ(n) -> X ∧ ?ar`(0) = x ∧ ( ∀k∈n. ?ar`(succ(k)) = f`(?ar`(k)) )"
      by (rule indseq_restrict)
    note A1 A2 A3 A6
    moreover have "?br = restrict(b,succ(n))" by simp
    ultimately have
      "?br: succ(n) -> X ∧ ?br`(0) = x ∧ ( ∀k∈n. ?br`(succ(k)) = f`(?br`(k)) )"
      by (rule indseq_restrict)
    with A4 I have II: "?ar = ?br" by blast
    from A3 have "succ(n) ∈ nat" by simp
    moreover from A5 A6 have 
      "a: succ(succ(n)) -> X" and "b: succ(succ(n)) -> X"
      by auto
    moreover note II
    moreover 
    have T: "n ∈ succ(n)" by simp
    then have "?ar`(n) = a`(n)" and "?br`(n) = b`(n)" using restrict
      by auto
    with A5 A6 II T have "a`(succ(n)) = b`(succ(n))" by simp
    ultimately show "a = b" by (rule finseq_restr_eq)
  qed
next show 
    "∃ a. a: succ(succ(n)) -> X ∧ a`(0) = x ∧ 
    ( ∀k∈succ(n). a`(succ(k)) = f`(a`(k)) )"
  proof -
    from A4 obtain a where III: "a: succ(n) -> X" and IV: "a`(0) = x" 
      and V: "∀k∈n. a`(succ(k)) = f`(a`(k))" by auto
    let ?b = "a ∪ {⟨succ(n), f`(a`(n))⟩}"
    from A1 III have
      VI: "?b : succ(succ(n)) -> X" and
      VII: "∀k ∈ succ(n). ?b`(k) = a`(k)" and 
      VIII: "?b`(succ(n)) = f`(a`(n))" 
      using apply_funtype finseq_extend by auto
    from A3 have "0 ∈ succ(n)" using empty_in_every_succ by simp
    with IV VII have IX: "?b`(0) = x" by auto
    { fix k assume "k ∈ succ(n)"
      then have "k∈n ∨ k = n" by auto
      moreover
      { assume A7: "k ∈ n"
	with A3 VII have "?b`(succ(k)) = a`(succ(k))"
	  using succ_ineq by auto
	also from A7 V VII have "a`(succ(k)) = f`(?b`(k))" by simp
	finally have "?b`(succ(k)) =  f`(?b`(k))" by simp }
      moreover
      { assume A8: "k = n"
	with VIII have "?b`(succ(k)) =  f`(a`(k))" by simp
	with A8 VII VIII have "?b`(succ(k)) =  f`(?b`(k))" by simp }
      ultimately have "?b`(succ(k)) =  f`(?b`(k))" by auto
    } then have "∀k ∈ succ(n). ?b`(succ(k)) =  f`(?b`(k))" by simp
    with VI IX show ?thesis by auto
  qed
qed

text{*The next lemma combines @{text "indseq_exun0"} and @{text "indseq_exun_ind"} 
  to show the existence and uniqueness of finite sequences defined by induction.*}

lemma indseq_exun: 
  assumes A1: "f: X->X" and A2: "x∈X" and A3: "n ∈ nat"
  shows 
  "∃! a. a: succ(n) -> X ∧ a`(0) = x ∧ (∀k∈n. a`(succ(k)) = f`(a`(k)))"
proof -
  note A3
  moreover from A1 A2 have
    "∃! a. a: succ(0) -> X ∧ a`(0) = x ∧ ( ∀k∈0. a`(succ(k)) = f`(a`(k)) )"
    using indseq_exun0 by simp
  moreover from A1 A2 have "∀k ∈ nat.
    ( ∃! a. a: succ(k) -> X ∧ a`(0) = x ∧ 
    ( ∀i∈k. a`(succ(i)) = f`(a`(i)) )) -->
    ( ∃! a. a: succ(succ(k)) -> X ∧ a`(0) = x ∧ 
    ( ∀i∈succ(k). a`(succ(i)) = f`(a`(i)) ) )"
    using indseq_exun_ind by simp
  ultimately show
    "∃! a. a: succ(n) -> X ∧ a`(0) = x ∧ ( ∀k∈n. a`(succ(k)) = f`(a`(k)) )"
    by (rule ind_on_nat)
qed
  
text{*We are now ready to prove the main theorem about finite inductive sequences.*}

theorem fin_indseq_props: 
  assumes A1: "f: X->X" and A2: "x∈X" and A3: "n ∈ nat" and
  A4: "a = InductiveSequenceN(x,f,n)"
  shows
  "a: succ(n) -> X"
  "a`(0) = x"
  "∀k∈n. a`(succ(k)) = f`(a`(k))"
proof -
  let ?i = "THE a. a: succ(n) -> X ∧ a`(0) = x ∧ 
    ( ∀k∈n. a`(succ(k)) = f`(a`(k)) )"
  from A1 A2 A3 have 
    "∃! a. a: succ(n) -> X ∧ a`(0) = x ∧ ( ∀k∈n. a`(succ(k)) = f`(a`(k)) )"
    using indseq_exun by simp
  then have 
    "?i: succ(n) -> X ∧ ?i`(0) = x ∧ ( ∀k∈n. ?i`(succ(k)) = f`(?i`(k)) )"
    by (rule theI)
  moreover from A1 A4 have "a = ?i"
    using InductiveSequenceN_def func1_1_L1 by simp
  ultimately show 
    "a: succ(n) -> X"   "a`(0) = x"   "∀k∈n. a`(succ(k)) = f`(a`(k))"
    by auto
qed

text{*A corollary about the domain of a finite inductive sequence.*}

corollary fin_indseq_domain: 
  assumes A1: "f: X->X" and A2: "x∈X" and A3: "n ∈ nat" 
  shows "domain(InductiveSequenceN(x,f,n)) = succ(n)"
proof -
  from assms have "InductiveSequenceN(x,f,n) : succ(n) -> X"
    using fin_indseq_props by simp
  then show ?thesis using func1_1_L1 by simp
qed

text{*The collection of finite sequences defined by induction is consistent
  in the sense that the restriction of the sequence defined on a larger
  set to the smaller set is the same as the sequence defined on the smaller set.*}

lemma indseq_consistent: assumes A1: "f: X->X" and A2: "x∈X" and 
  A3: "i ∈ nat"  "j ∈ nat" and A4: "i ⊆ j"
  shows 
  "restrict(InductiveSequenceN(x,f,j),succ(i)) = InductiveSequenceN(x,f,i)"
proof -
  let ?a = "InductiveSequenceN(x,f,j)"
  let ?b = "restrict(InductiveSequenceN(x,f,j),succ(i))"
  let ?c = "InductiveSequenceN(x,f,i)"
  from A1 A2 A3 have 
    "?a: succ(j) -> X"  "?a`(0) = x"   "∀k∈j. ?a`(succ(k)) = f`(?a`(k))"
    using fin_indseq_props by auto
  with A3 A4 have
    "?b: succ(i) -> X ∧ ?b`(0) = x ∧ ( ∀k∈i. ?b`(succ(k)) = f`(?b`(k)))"
    using succ_subset restrict_type2 empty_in_every_succ restrict succ_ineq
    by auto
  moreover from A1 A2 A3 have
    "?c: succ(i) -> X ∧ ?c`(0) = x ∧ ( ∀k∈i. ?c`(succ(k)) = f`(?c`(k)))"
    using fin_indseq_props by simp
  moreover from A1 A2 A3 have
    "∃! a. a: succ(i) -> X ∧ a`(0) = x ∧ ( ∀k∈i. a`(succ(k)) = f`(a`(k)) )"
    using indseq_exun by simp
  ultimately show "?b = ?c" by blast
qed

text{*For any two natural numbers one of the corresponding inductive sequences
  is contained in the other.*}

lemma indseq_subsets: assumes A1: "f: X->X" and A2: "x∈X" and 
  A3: "i ∈ nat"  "j ∈ nat" and 
  A4: "a = InductiveSequenceN(x,f,i)"  "b = InductiveSequenceN(x,f,j)"
  shows "a ⊆ b ∨ b ⊆ a"
proof -
  from A3 have "i⊆j ∨ j⊆i" using nat_incl_total by simp
  moreover
  { assume "i⊆j"
    with A1 A2 A3 A4 have "restrict(b,succ(i)) = a" 
      using indseq_consistent by simp
    moreover have "restrict(b,succ(i)) ⊆ b" 
      using restrict_subset by simp
    ultimately have "a ⊆ b ∨ b ⊆ a" by simp }
  moreover
  { assume "j⊆i"
    with A1 A2 A3 A4 have "restrict(a,succ(j)) = b" 
      using indseq_consistent by simp
    moreover have "restrict(a,succ(j)) ⊆ a" 
      using restrict_subset by simp
    ultimately have "a ⊆ b ∨ b ⊆ a" by simp }
  ultimately show  "a ⊆ b ∨ b ⊆ a" by auto
qed

text{*The first theorem about properties of infinite inductive sequences:
  inductive sequence is a indeed a sequence (i.e. a function on the set of 
  natural numbers. *}

theorem indseq_seq: assumes  A1: "f: X->X" and A2: "x∈X"
  shows "InductiveSequence(x,f) : nat -> X"
proof -
  let ?S = "{InductiveSequenceN(x,f,n). n ∈ nat}"
  { fix a assume "a∈?S"
    then obtain n where "n ∈ nat" and "a =  InductiveSequenceN(x,f,n)"
      by auto
    with A1 A2 have "a : succ(n)->X" using fin_indseq_props
      by simp
    then have "∃A B. a:A->B" by auto
  } then have "∀a ∈ ?S. ∃A B. a:A->B" by auto
  moreover
  { fix a b assume "a∈?S"   "b∈?S"
    then obtain i j where "i∈nat"  "j∈nat" and
      "a = InductiveSequenceN(x,f,i)"   "b = InductiveSequenceN(x,f,j)"
      by auto
    with A1 A2 have "a⊆b ∨ b⊆a" using indseq_subsets by simp
  } then have "∀a∈?S. ∀b∈?S. a⊆b ∨ b⊆a" by auto
  ultimately have "\<Union>?S : domain(\<Union>?S) -> range(\<Union>?S)"
    using fun_Union by simp
  with A1 A2 have I: "\<Union>?S : nat -> range(\<Union>?S)"
    using domain_UN fin_indseq_domain nat_union_succ by simp
  moreover
  { fix k assume A3: "k ∈ nat"
    let ?y = "(\<Union>?S)`(k)"
    note I A3
    moreover have "?y = (\<Union>?S)`(k)" by simp
    ultimately have "⟨k,?y⟩ ∈ (\<Union>?S)" by (rule func1_1_L5A)
    then obtain n where "n ∈ nat" and II: "⟨k,?y⟩ ∈ InductiveSequenceN(x,f,n)"
      by auto
    with A1 A2 have "InductiveSequenceN(x,f,n): succ(n) -> X" 
      using fin_indseq_props by simp
    with II have "?y ∈ X" using func1_1_L5 by blast
  } then have "∀k ∈ nat.  (\<Union>?S)`(k) ∈ X" by simp
  ultimately have "\<Union>?S : nat -> X" using func1_1_L1A
    by blast
  then show "InductiveSequence(x,f) : nat -> X"
    using InductiveSequence_def by simp
qed

text{*Restriction of an inductive sequence to a finite domain
  is the corresponding finite inductive sequence.*}

lemma indseq_restr_eq: 
  assumes A1: "f: X->X" and A2: "x∈X" and A3: "n ∈ nat"
  shows 
  "restrict(InductiveSequence(x,f),succ(n)) = InductiveSequenceN(x,f,n)"
proof -
  let ?a = "InductiveSequence(x,f)"
  let ?b = "InductiveSequenceN(x,f,n)"
  let ?S = "{InductiveSequenceN(x,f,n). n ∈ nat}"
  from A1 A2 A3 have 
    I: "?a : nat -> X"  and "succ(n) ⊆ nat"
    using indseq_seq succnat_subset_nat by auto
  then have "restrict(?a,succ(n)) : succ(n) -> X"
    using restrict_type2 by simp
  moreover from A1 A2 A3 have "?b : succ(n) -> X"
    using fin_indseq_props by simp
  moreover
  { fix k assume A4: "k ∈ succ(n)"
    from A1 A2 A3 I have
      "\<Union>?S : nat -> X"   "?b ∈ ?S"  "?b : succ(n) -> X"
      using InductiveSequence_def fin_indseq_props by auto
    with A4 have "restrict(?a,succ(n))`(k) = ?b`(k)"
      using fun_Union_apply InductiveSequence_def restrict_if
      by simp
  } then have "∀k ∈ succ(n). restrict(?a,succ(n))`(k) = ?b`(k)" 
    by simp
  ultimately show ?thesis by (rule func_eq)
qed

text{*The first element of the inductive sequence starting at $x$ and generated by $f$
  is indeed $x$. *}

theorem indseq_valat0: assumes A1: "f: X->X" and A2: "x∈X"
  shows "InductiveSequence(x,f)`(0) = x"
proof -
  let ?a = "InductiveSequence(x,f)"
  let ?b = "InductiveSequenceN(x,f,0)"
  have T: "0∈nat"  "0 ∈ succ(0)" by auto
  with A1 A2 have "?b`(0) = x" 
    using fin_indseq_props by simp
  moreover from T have "restrict(?a,succ(0))`(0) = ?a`(0)"
    using restrict_if by simp
  moreover from A1 A2 T have 
    "restrict(?a,succ(0)) = ?b"
    using indseq_restr_eq by simp
  ultimately show "?a`(0) = x" by simp
qed

text{*An infinite inductive sequence satisfies the 
  inductive relation that defines it.*}
  
theorem indseq_vals: 
  assumes A1: "f: X->X" and A2: "x∈X"  and A3: "n ∈ nat"
  shows 
  "InductiveSequence(x,f)`(succ(n)) = f`(InductiveSequence(x,f)`(n))"
proof -
  let ?a = "InductiveSequence(x,f)"
  let ?b = "InductiveSequenceN(x,f,succ(n))"
  from A3 have T: 
    "succ(n) ∈ succ(succ(n))"  
    "succ(succ(n)) ∈ nat" 
    "n ∈ succ(succ(n))"
    by auto    
  then have "?a`(succ(n)) = restrict(?a,succ(succ(n)))`(succ(n))"
    using restrict_if by simp
  also from A1 A2 T have "… = f`(restrict(?a,succ(succ(n)))`(n))"
    using indseq_restr_eq fin_indseq_props by simp
  also from T have "… = f`(?a`(n))" using restrict_if by simp
  finally show "?a`(succ(n)) = f`(?a`(n))" by simp
qed

section{*Images of inductive sequences*}

text{*In this section we consider the properties of sets that are
  images of inductive sequences, that is are of the form
  $\{f^{(n)} (x) : n \in N\}$ for some $x$ in the domain of $f$,
  where $f^{(n)}$ denotes the $n$'th
  iteration of the function $f$. For a function $f:X\rightarrow X$ and
  a point $x\in X$ such set is set is sometimes called 
  the orbit of $x$ generated by $f$.*}

text{*The basic properties of orbits.*}

theorem ind_seq_image: assumes A1: "f: X->X" and A2: "x∈X"  and 
  A3: "A = InductiveSequence(x,f)``(nat)"
  shows "x∈A" and "∀y∈A. f`(y) ∈ A" 
proof -
  let ?a = "InductiveSequence(x,f)"
  from A1 A2 have "?a : nat -> X" using indseq_seq
    by simp
  with A3 have I: "A = {?a`(n). n ∈ nat}" using func_imagedef
    by auto hence "?a`(0) ∈ A" by auto
  with A1 A2 show "x∈A" using indseq_valat0 by simp
  { fix y assume "y∈A"
    with I obtain n where II: "n ∈ nat" and III: "y = ?a`(n)"
      by auto
    with A1 A2 have "?a`(succ(n)) = f`(y)"
      using indseq_vals by simp
    moreover from I II have "?a`(succ(n)) ∈ A" by auto
    ultimately have "f`(y) ∈ A" by simp
  } then show "∀y∈A. f`(y) ∈ A" by simp
qed

section{*Subsets generated by a binary operation*}

text{* In algebra we often talk about sets "generated" by an element,
  that is sets of the form (in multiplicative notation) $\{a^n | n\in Z\}$.
  This is a related to a general notion of "power" 
  (as in $a^n = a\cdot a \cdot .. \cdot a$ ) or multiplicity $n\cdot a = a+a+..+a$.
  The intuitive meaning of such notions is obvious, but we need to do some
  work to be able to use it in the formalized setting. This sections is devoted
  to sequences that are created by repeatedly applying a binary operation with the 
  second argument fixed to some constant.*}

text{*Basic propertes of sets generated by binary operations.*}

theorem binop_gen_set: 
  assumes A1: "f: X×Y -> X" and A2: "x∈X"  "y∈Y" and
  A3: "a = InductiveSequence(x,Fix2ndVar(f,y))"
  shows
  "a : nat -> X"
  "a``(nat) ∈ Pow(X)"
  "x ∈ a``(nat)"
  "∀z ∈ a``(nat). Fix2ndVar(f,y)`(z) ∈ a``(nat)"
proof -
  let ?g = "Fix2ndVar(f,y)"
  from A1 A2 have I: "?g : X->X"
    using fix_2nd_var_fun by simp
  with A2 A3 show "a : nat -> X"
    using indseq_seq by simp
  then show "a``(nat) ∈ Pow(X)" using func1_1_L6 by simp
  from A2 A3 I show "x ∈ a``(nat)" using ind_seq_image by blast
  from A2 A3 I have
    "?g : X->X"  "x∈X"  "a``(nat) = InductiveSequence(x,?g)``(nat)"
    by auto
  then show "∀z ∈ a``(nat). Fix2ndVar(f,y)`(z) ∈ a``(nat)"
    by (rule ind_seq_image)
qed

text{*A simple corollary to the theorem @{text "binop_gen_set"}: a set
  that contains all iterations of the application of a binary operation
  exists.*}

lemma binop_gen_set_ex: assumes A1: "f: X×Y -> X" and A2: "x∈X"  "y∈Y"
  shows "{A ∈ Pow(X). x∈A ∧ (∀z ∈ A. f`⟨z,y⟩ ∈ A) } ≠ 0"
proof -
  let ?a = "InductiveSequence(x,Fix2ndVar(f,y))" 
  let ?A = "?a``(nat)"
  from A1 A2 have I: "?A ∈ Pow(X)" and "x ∈ ?A" using binop_gen_set 
    by auto
  moreover
  { fix z assume T: "z∈?A"
    with A1 A2 have "Fix2ndVar(f,y)`(z) ∈ ?A"
      using binop_gen_set by simp
    moreover
    from I T have "z ∈ X" by auto
    with A1 A2 have "Fix2ndVar(f,y)`(z) = f`⟨z,y⟩"
      using fix_var_val by simp
    ultimately have "f`⟨z,y⟩ ∈ ?A" by simp
  } then have "∀z ∈ ?A. f`⟨z,y⟩ ∈ ?A" by simp
  ultimately show ?thesis by auto
qed

text{*A more general version of @{text " binop_gen_set"} where the generating
  binary operation acts on a larger set.*}

theorem binop_gen_set1: assumes A1: "f: X×Y -> X" and 
  A2: "X1 ⊆ X" and A3: "x∈X1"  "y∈Y" and
  A4: "∀t∈X1. f`⟨t,y⟩ ∈ X1" and 
  A5: "a = InductiveSequence(x,Fix2ndVar(restrict(f,X1×Y),y))"
shows 
  "a : nat -> X1"
  "a``(nat) ∈ Pow(X1)"
  "x ∈ a``(nat)"
  "∀z ∈ a``(nat). Fix2ndVar(f,y)`(z) ∈ a``(nat)"
  "∀z ∈ a``(nat). f`⟨z,y⟩ ∈ a``(nat)"
proof -
  let ?h = "restrict(f,X1×Y)"
  let ?g = "Fix2ndVar(?h,y)"
  from A2 have "X1×Y ⊆ X×Y" by auto
  with A1 have I: "?h : X1×Y -> X"
    using restrict_type2 by simp
  with A3 have II: "?g: X1 -> X" using fix_2nd_var_fun by simp
  from A3 A4 I have "∀t∈X1. ?g`(t) ∈ X1"
    using restrict fix_var_val by simp
  with II have III: "?g : X1 -> X1" using func1_1_L1A by blast
  with A3 A5 show "a : nat -> X1" using indseq_seq by simp
  then show IV: "a``(nat) ∈ Pow(X1)" using func1_1_L6 by simp
  from A3 A5 III show "x ∈ a``(nat)" using ind_seq_image by blast
  from A3 A5 III have 
    "?g : X1 -> X1"   "x∈X1"  "a``(nat) =  InductiveSequence(x,?g)``(nat)"
    by auto
  then have "∀z ∈ a``(nat). Fix2ndVar(?h,y)`(z) ∈ a``(nat)" 
    by (rule ind_seq_image)
  moreover
  { fix z assume "z ∈ a``(nat)"
    with IV have "z ∈ X1" by auto
    with A1 A2 A3 have "?g`(z) = Fix2ndVar(f,y)`(z)"
      using fix_2nd_var_restr_comm restrict by simp
  } then have "∀z ∈ a``(nat). ?g`(z) = Fix2ndVar(f,y)`(z)" by simp
  ultimately show "∀z ∈ a``(nat). Fix2ndVar(f,y)`(z) ∈ a``(nat)" by simp
  moreover
  { fix z assume "z ∈ a``(nat)"
    with A2 IV have "z∈X" by auto
    with A1 A3 have "Fix2ndVar(f,y)`(z) = f`⟨z,y⟩"
      using fix_var_val by simp
  } then have "∀z ∈ a``(nat). Fix2ndVar(f,y)`(z) = f`⟨z,y⟩"
    by simp
  ultimately show "∀z ∈ a``(nat). f`⟨z,y⟩ ∈ a``(nat)"
    by simp
qed

text{*A generalization of @{text " binop_gen_set_ex"} that applies when the binary
  operation acts on a larger set. This is used in our Metamath translation
  to prove the existence of the set of real natural numbers. 
  Metamath defines the real natural numbers as the smallest set that cantains
  $1$ and is closed with respect to operation of adding $1$.*}

lemma binop_gen_set_ex1: assumes A1: "f: X×Y -> X" and 
  A2: "X1 ⊆ X" and A3: "x∈X1"  "y∈Y" and
  A4: "∀t∈X1. f`⟨t,y⟩ ∈ X1"
  shows "{A ∈ Pow(X1). x∈A ∧ (∀z ∈ A. f`⟨z,y⟩ ∈ A) } ≠ 0"
proof -
  let ?a = "InductiveSequence(x,Fix2ndVar(restrict(f,X1×Y),y))"
  let ?A = "?a``(nat)"
  from A1 A2 A3 A4 have 
    "?A ∈ Pow(X1)"   "x ∈ ?A"   "∀z ∈ ?A. f`⟨z,y⟩ ∈ ?A"
    using binop_gen_set1 by auto
  thus ?thesis by auto
qed

section{*Inductive sequences with changing generating function*}

text{*A seemingly more general form of a sequence defined by induction 
  is a sequence generated by the difference equation $x_{n+1} = f_{n} (x_n)$
  where $n\mapsto f_n$ is a given sequence of functions such 
  that each maps $X$ into inself. 
  For example when 
  $f_n (x) := x + x_n$ then the equation $S_{n+1} = f_{n} (S_n)$ describes
  the sequence $n \mapsto S_n = s_0 +\sum_{i=0}^n x_n$, i.e. the sequence of 
  partial sums of the sequence $\{s_0, x_0, x_1, x_3,..\}$. 
  *}

text{*The situation where the function that we iterate changes with $n$ can be 
  derived from the simpler case if we define the generating function appropriately.
  Namely, we replace the generating function in the definitions of 
  @{text "InductiveSequenceN"} by the function $f: X\times n \rightarrow X\times n$, 
  $f\langle x,k\rangle = \langle f_k(x), k+1 \rangle$ if $k < n$,  
  $\langle f_k(x), k \rangle$ otherwise. The first notion defines the expression 
  we will use to define the generating function. 
  To understand the notation recall that in standard Isabelle/ZF
  for a pair $s=\langle x,n \rangle$ we have @{text "fst"}$(s)=x$ and 
  @{text "snd"}$(s)=n$. *}

definition
  "StateTransfFunNMeta(F,n,s) ≡ 
  if (snd(s) ∈ n) then ⟨F`(snd(s))`(fst(s)), succ(snd(s))⟩ else s"

text{* Then we define the actual generating function on sets of pairs
  from $X\times \{0,1, .. ,n\}$. *}

definition
  "StateTransfFunN(X,F,n) ≡ {⟨s, StateTransfFunNMeta(F,n,s)⟩. s ∈ X×succ(n)}"

text{*Having the generating function we can define the expression
  that we cen use to define the inductive sequence generates.*}

definition
  "StatesSeq(x,X,F,n) ≡ 
  InductiveSequenceN(⟨x,0⟩, StateTransfFunN(X,F,n),n)"

text{*Finally we can define the sequence given by a initial point $x$,
  and a sequence $F$ of $n$ functions.*}

definition
  "InductiveSeqVarFN(x,X,F,n) ≡ {⟨k,fst(StatesSeq(x,X,F,n)`(k))⟩. k ∈ succ(n)}"

text{*The state transformation function (@{text "StateTransfFunN"} is 
  a function that transforms $X\times n$ into itself.*}

lemma state_trans_fun: assumes A1: "n ∈ nat" and A2: "F: n -> (X->X)"
  shows "StateTransfFunN(X,F,n): X×succ(n) -> X×succ(n)"
proof -
  { fix s assume A3: "s ∈ X×succ(n)"
    let ?x = "fst(s)"
    let ?k = "snd(s)"
    let ?S = "StateTransfFunNMeta(F,n,s)"
    from A3 have T: "?x ∈ X"  "?k ∈ succ(n)" and "⟨?x,?k⟩ = s" by auto
    { assume A4: "?k ∈ n"
      with A1 have "succ(?k) ∈ succ(n)" using succ_ineq by simp
      with A2 T A4 have "?S ∈ X×succ(n)"
	using apply_funtype StateTransfFunNMeta_def by simp }
    with A2 A3 T have "?S ∈ X×succ(n)"
      using apply_funtype StateTransfFunNMeta_def by auto
  } then have "∀s ∈ X×succ(n). StateTransfFunNMeta(F,n,s) ∈ X×succ(n)"
    by simp
  then have 
    "{⟨s, StateTransfFunNMeta(F,n,s)⟩. s ∈ X×succ(n)} : X×succ(n) -> X×succ(n)"
    by (rule ZF_fun_from_total)
  then show "StateTransfFunN(X,F,n): X×succ(n) -> X×succ(n)"
    using StateTransfFunN_def by simp
qed

text{*We can apply @{text "fin_indseq_props"} to the sequence used in the
  definition of @{text "InductiveSeqVarFN"} to get the properties of the sequence
  of states generated by the @{text "StateTransfFunN"}.*}

lemma states_seq_props:
  assumes A1: "n ∈ nat" and A2: "F: n -> (X->X)" and A3: "x∈X" and 
  A4: "b = StatesSeq(x,X,F,n)"
  shows
  "b : succ(n) -> X×succ(n)"
  "b`(0) = ⟨x,0⟩"
  "∀k ∈ succ(n). snd(b`(k)) = k"  
  "∀k∈n. b`(succ(k)) = ⟨F`(k)`(fst(b`(k))), succ(k)⟩"
proof -
  let ?f = "StateTransfFunN(X,F,n)"
  from A1 A2 have I: "?f : X×succ(n) -> X×succ(n)"
    using state_trans_fun by simp
  moreover from A1 A3 have II: "⟨x,0⟩ ∈ X×succ(n)"
    using empty_in_every_succ by simp
  moreover note A1
  moreover from A4 have III: "b = InductiveSequenceN(⟨x,0⟩,?f,n)"
    using StatesSeq_def by simp
  ultimately show IV: "b : succ(n) -> X×succ(n)"
    by (rule fin_indseq_props)
  from I II A1 III show V: "b`(0) = ⟨x,0⟩"
    by (rule fin_indseq_props)
  from I II A1 III have VI: "∀k∈n. b`(succ(k)) = ?f`(b`(k))"
    by (rule fin_indseq_props)
  { fix k 
    note I
    moreover
    assume A5: "k ∈ n" hence "k ∈ succ(n)" by auto
    with IV have "b`(k) ∈  X×succ(n)" using apply_funtype by simp
    moreover have "?f = {⟨s, StateTransfFunNMeta(F,n,s)⟩. s ∈ X×succ(n)}"
      using StateTransfFunN_def by simp
    ultimately have "?f`(b`(k)) =  StateTransfFunNMeta(F,n,b`(k))"
      by (rule ZF_fun_from_tot_val)
  } then have VII: "∀k ∈ n. ?f`(b`(k)) =  StateTransfFunNMeta(F,n,b`(k))"
    by simp
  { fix k assume A5: "k ∈ succ(n)"
    note A1 A5
    moreover from V have " snd(b`(0)) = 0" by simp
    moreover from VI VII have 
      "∀j∈n. snd(b`(j)) = j --> snd(b`(succ(j))) = succ(j)"
      using StateTransfFunNMeta_def by auto
    ultimately have "snd(b`(k)) = k" by (rule fin_nat_ind)
  } then show "∀k ∈ succ(n). snd(b`(k)) = k" by simp
  with VI VII show "∀k∈n. b`(succ(k)) = ⟨F`(k)`(fst(b`(k))), succ(k)⟩"
    using StateTransfFunNMeta_def by auto
qed

text{*Basic properties of sequences defined by equation $x_{n+1}=f_n (x_n)$.*}

theorem fin_indseq_var_f_props: 
  assumes A1: "n ∈ nat" and A2: "x∈X" and A3: "F: n -> (X->X)" and 
  A4: "a = InductiveSeqVarFN(x,X,F,n)"
  shows
  "a: succ(n) -> X"
  "a`(0) = x"
  "∀k∈n. a`(succ(k)) = F`(k)`(a`(k))"
proof -
  let ?f = "StateTransfFunN(X,F,n)"
  let ?b = "StatesSeq(x,X,F,n)"
  from A1 A2 A3 have "?b : succ(n) -> X×succ(n)"
    using states_seq_props by simp
  then have "∀k ∈ succ(n). ?b`(k) ∈ X×succ(n)"
    using apply_funtype by simp
  hence "∀k ∈ succ(n). fst(?b`(k)) ∈ X" by auto
  then have I: "{⟨k,fst(?b`(k))⟩. k ∈ succ(n)} : succ(n) -> X"
    by (rule ZF_fun_from_total)
  with A4 show II: "a: succ(n) -> X" using InductiveSeqVarFN_def
    by simp
  moreover from A1 have "0 ∈ succ(n)" using empty_in_every_succ
    by simp
  moreover from A4 have III: 
    "a = {⟨k,fst(StatesSeq(x,X,F,n)`(k))⟩. k ∈ succ(n)}"
    using InductiveSeqVarFN_def by simp
  ultimately have "a`(0) = fst(?b`(0))"
    by (rule ZF_fun_from_tot_val)
  with A1 A2 A3 show "a`(0) = x" using states_seq_props by auto
  { fix k
    assume A5: "k ∈ n"
    with A1 have T1: "succ(k) ∈ succ(n)" and T2: "k ∈ succ(n)"
      using succ_ineq by auto
    from II T1 III have "a`(succ(k)) = fst(?b`(succ(k)))"
      by (rule ZF_fun_from_tot_val)
    with A1 A2 A3 A5 have "a`(succ(k)) = F`(k)`(fst(?b`(k)))"
      using states_seq_props by simp
    moreover from II T2 III have "a`(k) = fst(?b`(k))"
      by (rule ZF_fun_from_tot_val)
    ultimately have "a`(succ(k)) =  F`(k)`(a`(k))"
      by simp
  } then show "∀k∈n. a`(succ(k)) = F`(k)`(a`(k))"
    by simp
qed

text{*A consistency condition: if we make the sequence of 
  generating functions shorter, then we get a shorter inductive 
  sequence with the same values as in the original sequence. *}

lemma fin_indseq_var_f_restrict: assumes 
  A1: "n ∈ nat"  "i ∈ nat"  "x∈X"  "F: n -> (X->X)"   "G: i -> (X->X)"
  and A2: "i ⊆ n" and  A3: "∀j∈i. G`(j) = F`(j)" and A4: "k ∈ succ(i)"
  shows "InductiveSeqVarFN(x,X,G,i)`(k) = InductiveSeqVarFN(x,X,F,n)`(k)"
proof -
  let ?a = "InductiveSeqVarFN(x,X,F,n)"
  let ?b = "InductiveSeqVarFN(x,X,G,i)"
  from A1 A4 have "i ∈ nat"  "k ∈ succ(i)" by auto
  moreover from A1 have "?b`(0) = ?a`(0)"
    using fin_indseq_var_f_props by simp
  moreover from A1 A2 A3 have
    "∀j∈i. ?b`(j) = ?a`(j) --> ?b`(succ(j)) = ?a`(succ(j))"
    using fin_indseq_var_f_props by auto
  ultimately show "?b`(k) = ?a`(k)"
    by (rule fin_nat_ind)
qed
  

(*text{*If we make the sequence of generating funtions shorter, the resulting
  sequence will be shorter.*}

lemma fin_indseq_var_f_restrict:
  assumes A1: "n ∈ nat" and A2: "x∈X" and 
  A3: "F: n -> (X->X)" and A4: "k ≤ n" and
  A5: "a = restrict(InductiveSeqVarFN(x,X,F,n),k)" and
  A6: "b = InductiveSeqVarFN(x,X,restrict(F,k),k)"
  shows "a = b"
proof -*)
  
end