# Theory LList

Up to index of Isabelle/ZF/ex

theory LList
imports Main
begin

    (*  Title:      ZF/ex/LList.thy
        ID:         $Id: LList.thy,v 1.11 2005/06/17 14:15:11 haftmann Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1994  University of Cambridge

    Codatatype definition of Lazy Lists

    Equality for llist(A) as a greatest fixed point

    Functions for Lazy Lists

    STILL NEEDS:
    co_recursion for defining lconst, flip, etc.
    a typing rule for it, based on some notion of "productivity..."
    *)

    theory LList imports Main begin

    consts
      llist  :: "i=>i";

    codatatype
      "llist(A)" = LNil | LCons ("a ∈ A", "l ∈ llist(A)")

    (*Coinductive definition of equality*)
    consts
      lleq :: "i=>i"

    (*Previously used <*> in the domain and variant pairs as elements.  But
      standard pairs work just as well.  To use variant pairs, must change prefix
      a q/Q to the Sigma, Pair and converse rules.*)
    coinductive
      domains "lleq(A)" <= "llist(A) * llist(A)"
      intros
        LNil:  "<LNil, LNil> ∈ lleq(A)"
        LCons: "[| a ∈ A; <l,l'> ∈ lleq(A) |]
                ==> <LCons(a,l), LCons(a,l')> ∈ lleq(A)"
      type_intros  llist.intros

    (*Lazy list functions; flip is not definitional!*)
    consts
      lconst   :: "i => i"
      flip     :: "i => i"

    defs
      lconst_def:  "lconst(a) == lfp(univ(a), %l. LCons(a,l))"

    axioms
      flip_LNil:   "flip(LNil) = LNil"

      flip_LCons:  "[| x ∈ bool; l ∈ llist(bool) |]
                    ==> flip(LCons(x,l)) = LCons(not(x), flip(l))"

    (*These commands cause classical reasoning to regard the subset relation
      as primitive, not reducing it to membership*)

    declare subsetI [rule del]
            subsetCE [rule del]

    declare subset_refl [intro!]
            cons_subsetI [intro!]
            subset_consI [intro!]
            Union_least [intro!]
            UN_least [intro!]
            Un_least [intro!]
            Inter_greatest [intro!]
            Int_greatest [intro!]
            RepFun_subset [intro!]
            Un_upper1 [intro!]
            Un_upper2 [intro!]
            Int_lower1 [intro!]
            Int_lower2 [intro!]

    (*An elimination rule, for type-checking*)
    inductive_cases LConsE: "LCons(a,l) ∈ llist(A)"

    (*Proving freeness results*)
    lemma LCons_iff: "LCons(a,l)=LCons(a',l') <-> a=a' & l=l'"
    by auto

    lemma LNil_LCons_iff: "~ LNil=LCons(a,l)"
    by auto

    (*
    lemma llist_unfold: "llist(A) = {0} <+> (A <*> llist(A))";
    let open llist  val rew = rewrite_rule con_defs in
    by (fast_tac (claset() addSIs (subsetI ::map rew intros) addEs [rew elim]) 1)
    end
    done
    *)

    (*** Lemmas to justify using "llist" in other recursive type definitions ***)

    lemma llist_mono: "A ⊆ B ==> llist(A) ⊆ llist(B)"
    apply (unfold llist.defs )
    apply (rule gfp_mono)
    apply (rule llist.bnd_mono)
    apply (assumption | rule quniv_mono basic_monos)+
    done

    (** Closure of quniv(A) under llist -- why so complex?  Its a gfp... **)

    declare QPair_Int_Vset_subset_UN [THEN subset_trans, intro!]
            QPair_subset_univ [intro!]
            empty_subsetI [intro!]
            one_in_quniv [THEN qunivD, intro!]
    declare qunivD [dest!]
    declare Ord_in_Ord [elim!]

    lemma llist_quniv_lemma [rule_format]:
         "Ord(i) ==> ∀l ∈ llist(quniv(A)). l Int Vset(i) ⊆ univ(eclose(A))"
    apply (erule trans_induct)
    apply (rule ballI)
    apply (erule llist.cases)
    apply (simp_all add: QInl_def QInr_def llist.con_defs)
    (*LCons case: I simply can't get rid of the deepen_tac*)
    apply (tactic "deepen_tac (claset() addIs [Ord_trans] addIs [Int_lower1 RS subset_trans]) 2 1")
    done

    lemma llist_quniv: "llist(quniv(A)) ⊆ quniv(A)"
    apply (rule qunivI [THEN subsetI])
    apply (rule Int_Vset_subset)
    apply (assumption | rule llist_quniv_lemma)+
    done

    lemmas llist_subset_quniv =
           subset_trans [OF llist_mono llist_quniv]

    (*** Lazy List Equality: lleq ***)

    declare QPair_Int_Vset_subset_UN [THEN subset_trans, intro!]
            QPair_mono [intro!]

    declare Ord_in_Ord [elim!]

    (*Lemma for proving finality.  Unfold the lazy list; use induction hypothesis*)
    lemma lleq_Int_Vset_subset [rule_format]:
         "Ord(i) ==> ∀l l'. <l,l'> ∈ lleq(A) --> l Int Vset(i) ⊆ l'"
    apply (erule trans_induct)
    apply (intro allI impI)
    apply (erule lleq.cases)
    apply (unfold QInr_def llist.con_defs, safe)
    apply (fast elim!: Ord_trans bspec [elim_format])
    done

    (*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*)
    lemma lleq_symmetric: "<l,l'> ∈ lleq(A) ==> <l',l> ∈ lleq(A)"
    apply (erule lleq.coinduct [OF converseI])
    apply (rule lleq.dom_subset [THEN converse_type], safe)
    apply (erule lleq.cases, blast+)
    done

    lemma lleq_implies_equal: "<l,l'> ∈ lleq(A) ==> l=l'"
    apply (rule equalityI)
    apply (assumption | rule lleq_Int_Vset_subset [THEN Int_Vset_subset] |
           erule lleq_symmetric)+
    done

    lemma equal_llist_implies_leq:
         "[| l=l';  l ∈ llist(A) |] ==> <l,l'> ∈ lleq(A)"
    apply (rule_tac X = "{<l,l>. l ∈ llist (A) }" in lleq.coinduct)
    apply blast
    apply safe
    apply (erule_tac a=l in llist.cases, fast+)
    done

    (*** Lazy List Functions ***)

    (*Examples of coinduction for type-checking and to prove llist equations*)

    (*** lconst -- defined directly using lfp, but equivalent to a LList_corec ***)

    lemma lconst_fun_bnd_mono: "bnd_mono(univ(a), %l. LCons(a,l))"
    apply (unfold llist.con_defs )
    apply (rule bnd_monoI)
    apply (blast intro: A_subset_univ QInr_subset_univ)
    apply (blast intro: subset_refl QInr_mono QPair_mono)
    done

    (* lconst(a) = LCons(a,lconst(a)) *)
    lemmas lconst = def_lfp_unfold [OF lconst_def lconst_fun_bnd_mono]
    lemmas lconst_subset = lconst_def [THEN def_lfp_subset]
    lemmas member_subset_Union_eclose = arg_into_eclose [THEN Union_upper]

    lemma lconst_in_quniv: "a ∈ A ==> lconst(a) ∈ quniv(A)"
    apply (rule lconst_subset [THEN subset_trans, THEN qunivI])
    apply (erule arg_into_eclose [THEN eclose_subset, THEN univ_mono])
    done

    lemma lconst_type: "a ∈ A ==> lconst(a): llist(A)"
    apply (rule singletonI [THEN llist.coinduct])
    apply (erule lconst_in_quniv [THEN singleton_subsetI])
    apply (fast intro!: lconst)
    done

    (*** flip --- equations merely assumed; certain consequences proved ***)

    declare flip_LNil [simp]
            flip_LCons [simp]
            not_type [simp]

    lemma bool_Int_subset_univ: "b ∈ bool ==> b Int X ⊆ univ(eclose(A))"
    by (fast intro: Int_lower1 [THEN subset_trans] elim!: boolE)

    declare not_type [intro!]
    declare bool_Int_subset_univ [intro]

    (*Reasoning borrowed from lleq.ML; a similar proof works for all
      "productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*)
    lemma flip_llist_quniv_lemma [rule_format]:
         "Ord(i) ==> ∀l ∈ llist(bool). flip(l) Int Vset(i) ⊆ univ(eclose(bool))"
    apply (erule trans_induct)
    apply (rule ballI)
    apply (erule llist.cases, simp_all)
    apply (simp_all add: QInl_def QInr_def llist.con_defs)
    (*LCons case: I simply can't get rid of the deepen_tac*)
    apply (tactic "deepen_tac (claset() addIs [Ord_trans] addIs [Int_lower1 RS subset_trans]) 2 1")
    done

    lemma flip_in_quniv: "l ∈ llist(bool) ==> flip(l) ∈ quniv(bool)"
    by (rule flip_llist_quniv_lemma [THEN Int_Vset_subset, THEN qunivI], assumption+)

    lemma flip_type: "l ∈ llist(bool) ==> flip(l): llist(bool)"
    apply (rule_tac X = "{flip (l) . l ∈ llist (bool) }" in llist.coinduct)
    apply blast
    apply (fast intro!: flip_in_quniv)
    apply (erule RepFunE)
    apply (erule_tac a=la in llist.cases, auto)
    done

    lemma flip_flip: "l ∈ llist(bool) ==> flip(flip(l)) = l"
    apply (rule_tac X1 = "{<flip (flip (l)),l> . l ∈ llist (bool) }" in
           lleq.coinduct [THEN lleq_implies_equal])
    apply blast
    apply (fast intro!: flip_type)
    apply (erule RepFunE)
    apply (erule_tac a=la in llist.cases)
    apply (simp_all add: flip_type not_not)
    done

    end

lemmas LConsE:

      [| LCons(a, l) ∈ llist(A); [| a ∈ A; l ∈ llist(A) |] ==> Q |] ==> Q

lemma LCons_iff:

      LCons(a, l) = LCons(a', l') <-> a = a' ∧ l = l'

lemma LNil_LCons_iff:

      LNil ≠ LCons(a, l)

lemma llist_mono:

      A ⊆ B ==> llist(A) ⊆ llist(B)

lemma llist_quniv_lemma:

      [| Ord(i); l ∈ llist(quniv(A)) |] ==> l ∩ Vset(i) ⊆ univ(eclose(A))

lemma llist_quniv:

      llist(quniv(A)) ⊆ quniv(A)

lemmas llist_subset_quniv:

      A2 ⊆ quniv(A1) ==> llist(A2) ⊆ quniv(A1)

lemmas llist_subset_quniv:

      A2 ⊆ quniv(A1) ==> llist(A2) ⊆ quniv(A1)

lemma lleq_Int_Vset_subset:

      [| Ord(i); ⟨l, l'⟩ ∈ lleq(A) |] ==> l ∩ Vset(i) ⊆ l'

lemma lleq_symmetric:

      ⟨l, l'⟩ ∈ lleq(A) ==> ⟨l', l⟩ ∈ lleq(A)

lemma lleq_implies_equal:

      ⟨l, l'⟩ ∈ lleq(A) ==> l = l'

lemma equal_llist_implies_leq:

      [| l = l'; l ∈ llist(A) |] ==> ⟨l, l'⟩ ∈ lleq(A)

lemma lconst_fun_bnd_mono:

      bnd_mono(univ(a), %l. LCons(a, l))

lemmas lconst:

      lconst(a1) = LCons(a1, lconst(a1))

lemmas lconst:

      lconst(a1) = LCons(a1, lconst(a1))

lemmas lconst_subset:

      lconst(a1) ⊆ univ(a1)

lemmas lconst_subset:

      lconst(a1) ⊆ univ(a1)

lemmas member_subset_Union_eclose:

      B ∈ A1 ==> B ⊆ \<Union>eclose(A1)

lemmas member_subset_Union_eclose:

      B ∈ A1 ==> B ⊆ \<Union>eclose(A1)

lemma lconst_in_quniv:

      a ∈ A ==> lconst(a) ∈ quniv(A)

lemma lconst_type:

      a ∈ A ==> lconst(a) ∈ llist(A)

lemma bool_Int_subset_univ:

      b ∈ bool ==> b ∩ X ⊆ univ(eclose(A))

lemma flip_llist_quniv_lemma:

      [| Ord(i); l ∈ llist(bool) |] ==> flip(l) ∩ Vset(i) ⊆ univ(eclose(bool))

lemma flip_in_quniv:

      l ∈ llist(bool) ==> flip(l) ∈ quniv(bool)

lemma flip_type:

      l ∈ llist(bool) ==> flip(l) ∈ llist(bool)

lemma flip_flip:

      l ∈ llist(bool) ==> flip(flip(l)) = l