Library ZFlist
Require Import Wf_nat.
Require Import ZF ZFpairs ZFnats.
Require Import ZFrepl ZFord ZFfix.
Section ListDefs.
Variable A : set.
Definition Nil := empty.
Definition Cons := couple.
Definition LISTf (X:set) := singl empty ∪ prodcart A X.
Instance LISTf_mono : Proper (incl_set ==> incl_set) LISTf.
Qed.
Instance LISTf_morph : Proper (eq_set ==> eq_set) LISTf.
Qed.
Lemma LISTf_ind : ∀ X (P : set -> Prop),
Proper (eq_set ==> iff) P ->
P Nil ->
(∀ x l, x ∈ A -> l ∈ X -> P (Cons x l)) ->
∀ a, a ∈ LISTf X -> P a.
Lemma Nil_typ0 : ∀ X, Nil ∈ LISTf X.
Lemma Cons_typ0 : ∀ X x l,
x ∈ A -> l ∈ X -> Cons x l ∈ LISTf X.
Definition LIST_case l f g :=
cond_set (l == Nil) f ∪ cond_set (l == Cons (fst l) (snd l)) g.
Global Instance LIST_case_morph : Proper (eq_set==>eq_set==>eq_set==>eq_set) LIST_case.
Qed.
Lemma LIST_case_Nil f g : LIST_case Nil f g == f.
Lemma LIST_case_Cons x l f g : LIST_case (Cons x l) f g == g.
Definition Lstn n := TI LISTf (nat2ordset n).
Lemma Lstn_incl_succ : ∀ k, Lstn k ⊆ Lstn (S k).
Lemma Lstn_eq : ∀ k, Lstn (S k) == LISTf (Lstn k).
Lemma Lstn_incl : ∀ k k', (k <= k')%nat -> Lstn k ⊆ Lstn k'.
Definition List := TI LISTf omega.
Lemma List_intro : ∀ k, Lstn k ⊆ List.
Lemma List_elim : ∀ x,
x ∈ List -> exists k, x ∈ Lstn k.
Lemma Lstn_case : ∀ k (P : set -> Prop),
Proper (eq_set ==> iff) P ->
P Nil ->
(∀ x l k', (k' < k)%nat -> x ∈ A -> l ∈ Lstn k' -> P (Cons x l)) ->
∀ a, a ∈ Lstn k -> P a.
Lemma List_fix : ∀ (P:set->Prop),
(∀ k,
(∀ k' x, (k' < k)%nat -> x ∈ Lstn k' -> P x) ->
(∀ x, x ∈ Lstn k -> P x)) ->
∀ x, x ∈ List -> P x.
Lemma List_ind : ∀ P : set -> Prop,
Proper (eq_set ==> iff) P ->
P Nil ->
(∀ x l, x ∈ A -> l ∈ List -> P l -> P (Cons x l)) ->
∀ a, a ∈ List -> P a.
Lemma List_eqn : List == LISTf List.
Lemma Nil_typ : Nil ∈ List.
Lemma Cons_typ : ∀ x l,
x ∈ A -> l ∈ List -> Cons x l ∈ List.
End ListDefs.
Instance List_mono : Proper (incl_set ==> incl_set) List.
Qed.
Instance List_morph : morph1 List.
Qed.
Require Import ZF ZFpairs ZFnats.
Require Import ZFrepl ZFord ZFfix.
Section ListDefs.
Variable A : set.
Definition Nil := empty.
Definition Cons := couple.
Definition LISTf (X:set) := singl empty ∪ prodcart A X.
Instance LISTf_mono : Proper (incl_set ==> incl_set) LISTf.
Qed.
Instance LISTf_morph : Proper (eq_set ==> eq_set) LISTf.
Qed.
Lemma LISTf_ind : ∀ X (P : set -> Prop),
Proper (eq_set ==> iff) P ->
P Nil ->
(∀ x l, x ∈ A -> l ∈ X -> P (Cons x l)) ->
∀ a, a ∈ LISTf X -> P a.
Lemma Nil_typ0 : ∀ X, Nil ∈ LISTf X.
Lemma Cons_typ0 : ∀ X x l,
x ∈ A -> l ∈ X -> Cons x l ∈ LISTf X.
Definition LIST_case l f g :=
cond_set (l == Nil) f ∪ cond_set (l == Cons (fst l) (snd l)) g.
Global Instance LIST_case_morph : Proper (eq_set==>eq_set==>eq_set==>eq_set) LIST_case.
Qed.
Lemma LIST_case_Nil f g : LIST_case Nil f g == f.
Lemma LIST_case_Cons x l f g : LIST_case (Cons x l) f g == g.
Definition Lstn n := TI LISTf (nat2ordset n).
Lemma Lstn_incl_succ : ∀ k, Lstn k ⊆ Lstn (S k).
Lemma Lstn_eq : ∀ k, Lstn (S k) == LISTf (Lstn k).
Lemma Lstn_incl : ∀ k k', (k <= k')%nat -> Lstn k ⊆ Lstn k'.
Definition List := TI LISTf omega.
Lemma List_intro : ∀ k, Lstn k ⊆ List.
Lemma List_elim : ∀ x,
x ∈ List -> exists k, x ∈ Lstn k.
Lemma Lstn_case : ∀ k (P : set -> Prop),
Proper (eq_set ==> iff) P ->
P Nil ->
(∀ x l k', (k' < k)%nat -> x ∈ A -> l ∈ Lstn k' -> P (Cons x l)) ->
∀ a, a ∈ Lstn k -> P a.
Lemma List_fix : ∀ (P:set->Prop),
(∀ k,
(∀ k' x, (k' < k)%nat -> x ∈ Lstn k' -> P x) ->
(∀ x, x ∈ Lstn k -> P x)) ->
∀ x, x ∈ List -> P x.
Lemma List_ind : ∀ P : set -> Prop,
Proper (eq_set ==> iff) P ->
P Nil ->
(∀ x l, x ∈ A -> l ∈ List -> P l -> P (Cons x l)) ->
∀ a, a ∈ List -> P a.
Lemma List_eqn : List == LISTf List.
Lemma Nil_typ : Nil ∈ List.
Lemma Cons_typ : ∀ x l,
x ∈ A -> l ∈ List -> Cons x l ∈ List.
End ListDefs.
Instance List_mono : Proper (incl_set ==> incl_set) List.
Qed.
Instance List_morph : morph1 List.
Qed.