src/HOL/Library/Coinductive_List.thy
author haftmann
Mon Jul 07 08:47:17 2008 +0200 (2008-07-07)
changeset 27487 c8a6ce181805
parent 27368 9f90ac19e32b
child 28693 a1294a197d12
permissions -rw-r--r--
absolute imports of HOL/*.thy theories
     1 (*  Title:      HOL/Library/Coinductive_Lists.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson and Makarius
     4 *)
     5 
     6 header {* Potentially infinite lists as greatest fixed-point *}
     7 
     8 theory Coinductive_List
     9 imports Plain "~~/src/HOL/List"
    10 begin
    11 
    12 subsection {* List constructors over the datatype universe *}
    13 
    14 definition "NIL = Datatype.In0 (Datatype.Numb 0)"
    15 definition "CONS M N = Datatype.In1 (Datatype.Scons M N)"
    16 
    17 lemma CONS_not_NIL [iff]: "CONS M N \<noteq> NIL"
    18   and NIL_not_CONS [iff]: "NIL \<noteq> CONS M N"
    19   and CONS_inject [iff]: "(CONS K M) = (CONS L N) = (K = L \<and> M = N)"
    20   by (simp_all add: NIL_def CONS_def)
    21 
    22 lemma CONS_mono: "M \<subseteq> M' \<Longrightarrow> N \<subseteq> N' \<Longrightarrow> CONS M N \<subseteq> CONS M' N'"
    23   by (simp add: CONS_def In1_mono Scons_mono)
    24 
    25 lemma CONS_UN1: "CONS M (\<Union>x. f x) = (\<Union>x. CONS M (f x))"
    26     -- {* A continuity result? *}
    27   by (simp add: CONS_def In1_UN1 Scons_UN1_y)
    28 
    29 definition "List_case c h = Datatype.Case (\<lambda>_. c) (Datatype.Split h)"
    30 
    31 lemma List_case_NIL [simp]: "List_case c h NIL = c"
    32   and List_case_CONS [simp]: "List_case c h (CONS M N) = h M N"
    33   by (simp_all add: List_case_def NIL_def CONS_def)
    34 
    35 
    36 subsection {* Corecursive lists *}
    37 
    38 coinductive_set LList for A
    39 where NIL [intro]:  "NIL \<in> LList A"
    40   | CONS [intro]: "a \<in> A \<Longrightarrow> M \<in> LList A \<Longrightarrow> CONS a M \<in> LList A"
    41 
    42 lemma LList_mono:
    43   assumes subset: "A \<subseteq> B"
    44   shows "LList A \<subseteq> LList B"
    45     -- {* This justifies using @{text LList} in other recursive type definitions. *}
    46 proof
    47   fix x
    48   assume "x \<in> LList A"
    49   then show "x \<in> LList B"
    50   proof coinduct
    51     case LList
    52     then show ?case using subset
    53       by cases blast+
    54   qed
    55 qed
    56 
    57 consts
    58   LList_corec_aux :: "nat \<Rightarrow> ('a \<Rightarrow> ('b Datatype.item \<times> 'a) option) \<Rightarrow>
    59     'a \<Rightarrow> 'b Datatype.item"
    60 primrec
    61   "LList_corec_aux 0 f x = {}"
    62   "LList_corec_aux (Suc k) f x =
    63     (case f x of
    64       None \<Rightarrow> NIL
    65     | Some (z, w) \<Rightarrow> CONS z (LList_corec_aux k f w))"
    66 
    67 definition "LList_corec a f = (\<Union>k. LList_corec_aux k f a)"
    68 
    69 text {*
    70   Note: the subsequent recursion equation for @{text LList_corec} may
    71   be used with the Simplifier, provided it operates in a non-strict
    72   fashion for case expressions (i.e.\ the usual @{text case}
    73   congruence rule needs to be present).
    74 *}
    75 
    76 lemma LList_corec:
    77   "LList_corec a f =
    78     (case f a of None \<Rightarrow> NIL | Some (z, w) \<Rightarrow> CONS z (LList_corec w f))"
    79   (is "?lhs = ?rhs")
    80 proof
    81   show "?lhs \<subseteq> ?rhs"
    82     apply (unfold LList_corec_def)
    83     apply (rule UN_least)
    84     apply (case_tac k)
    85      apply (simp_all (no_asm_simp) split: option.splits)
    86     apply (rule allI impI subset_refl [THEN CONS_mono] UNIV_I [THEN UN_upper])+
    87     done
    88   show "?rhs \<subseteq> ?lhs"
    89     apply (simp add: LList_corec_def split: option.splits)
    90     apply (simp add: CONS_UN1)
    91     apply safe
    92      apply (rule_tac a = "Suc ?k" in UN_I, simp, simp)+
    93     done
    94 qed
    95 
    96 lemma LList_corec_type: "LList_corec a f \<in> LList UNIV"
    97 proof -
    98   have "\<exists>x. LList_corec a f = LList_corec x f" by blast
    99   then show ?thesis
   100   proof coinduct
   101     case (LList L)
   102     then obtain x where L: "L = LList_corec x f" by blast
   103     show ?case
   104     proof (cases "f x")
   105       case None
   106       then have "LList_corec x f = NIL"
   107         by (simp add: LList_corec)
   108       with L have ?NIL by simp
   109       then show ?thesis ..
   110     next
   111       case (Some p)
   112       then have "LList_corec x f = CONS (fst p) (LList_corec (snd p) f)"
   113         by (simp add: LList_corec split: prod.split)
   114       with L have ?CONS by auto
   115       then show ?thesis ..
   116     qed
   117   qed
   118 qed
   119 
   120 
   121 subsection {* Abstract type definition *}
   122 
   123 typedef 'a llist = "LList (range Datatype.Leaf) :: 'a Datatype.item set"
   124 proof
   125   show "NIL \<in> ?llist" ..
   126 qed
   127 
   128 lemma NIL_type: "NIL \<in> llist"
   129   unfolding llist_def by (rule LList.NIL)
   130 
   131 lemma CONS_type: "a \<in> range Datatype.Leaf \<Longrightarrow>
   132     M \<in> llist \<Longrightarrow> CONS a M \<in> llist"
   133   unfolding llist_def by (rule LList.CONS)
   134 
   135 lemma llistI: "x \<in> LList (range Datatype.Leaf) \<Longrightarrow> x \<in> llist"
   136   by (simp add: llist_def)
   137 
   138 lemma llistD: "x \<in> llist \<Longrightarrow> x \<in> LList (range Datatype.Leaf)"
   139   by (simp add: llist_def)
   140 
   141 lemma Rep_llist_UNIV: "Rep_llist x \<in> LList UNIV"
   142 proof -
   143   have "Rep_llist x \<in> llist" by (rule Rep_llist)
   144   then have "Rep_llist x \<in> LList (range Datatype.Leaf)"
   145     by (simp add: llist_def)
   146   also have "\<dots> \<subseteq> LList UNIV" by (rule LList_mono) simp
   147   finally show ?thesis .
   148 qed
   149 
   150 definition "LNil = Abs_llist NIL"
   151 definition "LCons x xs = Abs_llist (CONS (Datatype.Leaf x) (Rep_llist xs))"
   152 
   153 lemma LCons_not_LNil [iff]: "LCons x xs \<noteq> LNil"
   154   apply (simp add: LNil_def LCons_def)
   155   apply (subst Abs_llist_inject)
   156     apply (auto intro: NIL_type CONS_type Rep_llist)
   157   done
   158 
   159 lemma LNil_not_LCons [iff]: "LNil \<noteq> LCons x xs"
   160   by (rule LCons_not_LNil [symmetric])
   161 
   162 lemma LCons_inject [iff]: "(LCons x xs = LCons y ys) = (x = y \<and> xs = ys)"
   163   apply (simp add: LCons_def)
   164   apply (subst Abs_llist_inject)
   165     apply (auto simp add: Rep_llist_inject intro: CONS_type Rep_llist)
   166   done
   167 
   168 lemma Rep_llist_LNil: "Rep_llist LNil = NIL"
   169   by (simp add: LNil_def add: Abs_llist_inverse NIL_type)
   170 
   171 lemma Rep_llist_LCons: "Rep_llist (LCons x l) =
   172     CONS (Datatype.Leaf x) (Rep_llist l)"
   173   by (simp add: LCons_def Abs_llist_inverse CONS_type Rep_llist)
   174 
   175 lemma llist_cases [cases type: llist]:
   176   obtains
   177     (LNil) "l = LNil"
   178   | (LCons) x l' where "l = LCons x l'"
   179 proof (cases l)
   180   case (Abs_llist L)
   181   from `L \<in> llist` have "L \<in> LList (range Datatype.Leaf)" by (rule llistD)
   182   then show ?thesis
   183   proof cases
   184     case NIL
   185     with Abs_llist have "l = LNil" by (simp add: LNil_def)
   186     with LNil show ?thesis .
   187   next
   188     case (CONS a K)
   189     then have "K \<in> llist" by (blast intro: llistI)
   190     then obtain l' where "K = Rep_llist l'" by cases
   191     with CONS and Abs_llist obtain x where "l = LCons x l'"
   192       by (auto simp add: LCons_def Abs_llist_inject)
   193     with LCons show ?thesis .
   194   qed
   195 qed
   196 
   197 
   198 definition
   199   "llist_case c d l =
   200     List_case c (\<lambda>x y. d (inv Datatype.Leaf x) (Abs_llist y)) (Rep_llist l)"
   201 
   202 syntax  (* FIXME? *)
   203   LNil :: logic
   204   LCons :: logic
   205 translations
   206   "case p of LNil \<Rightarrow> a | LCons x l \<Rightarrow> b" \<rightleftharpoons> "CONST llist_case a (\<lambda>x l. b) p"
   207 
   208 lemma llist_case_LNil [simp]: "llist_case c d LNil = c"
   209   by (simp add: llist_case_def LNil_def
   210     NIL_type Abs_llist_inverse)
   211 
   212 lemma llist_case_LCons [simp]: "llist_case c d (LCons M N) = d M N"
   213   by (simp add: llist_case_def LCons_def
   214     CONS_type Abs_llist_inverse Rep_llist Rep_llist_inverse inj_Leaf)
   215 
   216 
   217 definition
   218   "llist_corec a f =
   219     Abs_llist (LList_corec a
   220       (\<lambda>z.
   221         case f z of None \<Rightarrow> None
   222         | Some (v, w) \<Rightarrow> Some (Datatype.Leaf v, w)))"
   223 
   224 lemma LList_corec_type2:
   225   "LList_corec a
   226     (\<lambda>z. case f z of None \<Rightarrow> None
   227       | Some (v, w) \<Rightarrow> Some (Datatype.Leaf v, w)) \<in> llist"
   228   (is "?corec a \<in> _")
   229 proof (unfold llist_def)
   230   let "LList_corec a ?g" = "?corec a"
   231   have "\<exists>x. ?corec a = ?corec x" by blast
   232   then show "?corec a \<in> LList (range Datatype.Leaf)"
   233   proof coinduct
   234     case (LList L)
   235     then obtain x where L: "L = ?corec x" by blast
   236     show ?case
   237     proof (cases "f x")
   238       case None
   239       then have "?corec x = NIL"
   240         by (simp add: LList_corec)
   241       with L have ?NIL by simp
   242       then show ?thesis ..
   243     next
   244       case (Some p)
   245       then have "?corec x =
   246           CONS (Datatype.Leaf (fst p)) (?corec (snd p))"
   247         by (simp add: LList_corec split: prod.split)
   248       with L have ?CONS by auto
   249       then show ?thesis ..
   250     qed
   251   qed
   252 qed
   253 
   254 lemma llist_corec:
   255   "llist_corec a f =
   256     (case f a of None \<Rightarrow> LNil | Some (z, w) \<Rightarrow> LCons z (llist_corec w f))"
   257 proof (cases "f a")
   258   case None
   259   then show ?thesis
   260     by (simp add: llist_corec_def LList_corec LNil_def)
   261 next
   262   case (Some p)
   263 
   264   let "?corec a" = "llist_corec a f"
   265   let "?rep_corec a" =
   266     "LList_corec a
   267       (\<lambda>z. case f z of None \<Rightarrow> None
   268         | Some (v, w) \<Rightarrow> Some (Datatype.Leaf v, w))"
   269 
   270   have "?corec a = Abs_llist (?rep_corec a)"
   271     by (simp only: llist_corec_def)
   272   also from Some have "?rep_corec a =
   273       CONS (Datatype.Leaf (fst p)) (?rep_corec (snd p))"
   274     by (simp add: LList_corec split: prod.split)
   275   also have "?rep_corec (snd p) = Rep_llist (?corec (snd p))"
   276     by (simp only: llist_corec_def Abs_llist_inverse LList_corec_type2)
   277   finally have "?corec a = LCons (fst p) (?corec (snd p))"
   278     by (simp only: LCons_def)
   279   with Some show ?thesis by (simp split: prod.split)
   280 qed
   281 
   282 
   283 subsection {* Equality as greatest fixed-point -- the bisimulation principle *}
   284 
   285 coinductive_set EqLList for r
   286 where EqNIL: "(NIL, NIL) \<in> EqLList r"
   287   | EqCONS: "(a, b) \<in> r \<Longrightarrow> (M, N) \<in> EqLList r \<Longrightarrow>
   288       (CONS a M, CONS b N) \<in> EqLList r"
   289 
   290 lemma EqLList_unfold:
   291     "EqLList r = dsum (diag {Datatype.Numb 0}) (dprod r (EqLList r))"
   292   by (fast intro!: EqLList.intros [unfolded NIL_def CONS_def]
   293            elim: EqLList.cases [unfolded NIL_def CONS_def])
   294 
   295 lemma EqLList_implies_ntrunc_equality:
   296     "(M, N) \<in> EqLList (diag A) \<Longrightarrow> ntrunc k M = ntrunc k N"
   297   apply (induct k arbitrary: M N rule: nat_less_induct)
   298   apply (erule EqLList.cases)
   299    apply (safe del: equalityI)
   300   apply (case_tac n)
   301    apply simp
   302   apply (rename_tac n')
   303   apply (case_tac n')
   304    apply (simp_all add: CONS_def less_Suc_eq)
   305   done
   306 
   307 lemma Domain_EqLList: "Domain (EqLList (diag A)) \<subseteq> LList A"
   308   apply (rule subsetI)
   309   apply (erule LList.coinduct)
   310   apply (subst (asm) EqLList_unfold)
   311   apply (auto simp add: NIL_def CONS_def)
   312   done
   313 
   314 lemma EqLList_diag: "EqLList (diag A) = diag (LList A)"
   315   (is "?lhs = ?rhs")
   316 proof
   317   show "?lhs \<subseteq> ?rhs"
   318     apply (rule subsetI)
   319     apply (rule_tac p = x in PairE)
   320     apply clarify
   321     apply (rule diag_eqI)
   322      apply (rule EqLList_implies_ntrunc_equality [THEN ntrunc_equality],
   323        assumption)
   324     apply (erule DomainI [THEN Domain_EqLList [THEN subsetD]])
   325     done
   326   {
   327     fix M N assume "(M, N) \<in> diag (LList A)"
   328     then have "(M, N) \<in> EqLList (diag A)"
   329     proof coinduct
   330       case (EqLList M N)
   331       then obtain L where L: "L \<in> LList A" and MN: "M = L" "N = L" by blast
   332       from L show ?case
   333       proof cases
   334         case NIL with MN have ?EqNIL by simp
   335         then show ?thesis ..
   336       next
   337         case CONS with MN have ?EqCONS by (simp add: diagI)
   338         then show ?thesis ..
   339       qed
   340     qed
   341   }
   342   then show "?rhs \<subseteq> ?lhs" by auto
   343 qed
   344 
   345 lemma EqLList_diag_iff [iff]: "(p \<in> EqLList (diag A)) = (p \<in> diag (LList A))"
   346   by (simp only: EqLList_diag)
   347 
   348 
   349 text {*
   350   To show two LLists are equal, exhibit a bisimulation!  (Also admits
   351   true equality.)
   352 *}
   353 
   354 lemma LList_equalityI
   355   [consumes 1, case_names EqLList, case_conclusion EqLList EqNIL EqCONS]:
   356   assumes r: "(M, N) \<in> r"
   357     and step: "\<And>M N. (M, N) \<in> r \<Longrightarrow>
   358       M = NIL \<and> N = NIL \<or>
   359         (\<exists>a b M' N'.
   360           M = CONS a M' \<and> N = CONS b N' \<and> (a, b) \<in> diag A \<and>
   361             ((M', N') \<in> r \<or> (M', N') \<in> EqLList (diag A)))"
   362   shows "M = N"
   363 proof -
   364   from r have "(M, N) \<in> EqLList (diag A)"
   365   proof coinduct
   366     case EqLList
   367     then show ?case by (rule step)
   368   qed
   369   then show ?thesis by auto
   370 qed
   371 
   372 lemma LList_fun_equalityI
   373   [consumes 1, case_names NIL_type NIL CONS, case_conclusion CONS EqNIL EqCONS]:
   374   assumes M: "M \<in> LList A"
   375     and fun_NIL: "g NIL \<in> LList A"  "f NIL = g NIL"
   376     and fun_CONS: "\<And>x l. x \<in> A \<Longrightarrow> l \<in> LList A \<Longrightarrow>
   377             (f (CONS x l), g (CONS x l)) = (NIL, NIL) \<or>
   378             (\<exists>M N a b.
   379               (f (CONS x l), g (CONS x l)) = (CONS a M, CONS b N) \<and>
   380                 (a, b) \<in> diag A \<and>
   381                 (M, N) \<in> {(f u, g u) | u. u \<in> LList A} \<union> diag (LList A))"
   382       (is "\<And>x l. _ \<Longrightarrow> _ \<Longrightarrow> ?fun_CONS x l")
   383   shows "f M = g M"
   384 proof -
   385   let ?bisim = "{(f L, g L) | L. L \<in> LList A}"
   386   have "(f M, g M) \<in> ?bisim" using M by blast
   387   then show ?thesis
   388   proof (coinduct taking: A rule: LList_equalityI)
   389     case (EqLList M N)
   390     then obtain L where MN: "M = f L" "N = g L" and L: "L \<in> LList A" by blast
   391     from L show ?case
   392     proof (cases L)
   393       case NIL
   394       with fun_NIL and MN have "(M, N) \<in> diag (LList A)" by auto
   395       then have "(M, N) \<in> EqLList (diag A)" ..
   396       then show ?thesis by cases simp_all
   397     next
   398       case (CONS a K)
   399       from fun_CONS and `a \<in> A` `K \<in> LList A`
   400       have "?fun_CONS a K" (is "?NIL \<or> ?CONS") .
   401       then show ?thesis
   402       proof
   403         assume ?NIL
   404         with MN CONS have "(M, N) \<in> diag (LList A)" by auto
   405         then have "(M, N) \<in> EqLList (diag A)" ..
   406         then show ?thesis by cases simp_all
   407       next
   408         assume ?CONS
   409         with CONS obtain a b M' N' where
   410             fg: "(f L, g L) = (CONS a M', CONS b N')"
   411           and ab: "(a, b) \<in> diag A"
   412           and M'N': "(M', N') \<in> ?bisim \<union> diag (LList A)"
   413           by blast
   414         from M'N' show ?thesis
   415         proof
   416           assume "(M', N') \<in> ?bisim"
   417           with MN fg ab show ?thesis by simp
   418         next
   419           assume "(M', N') \<in> diag (LList A)"
   420           then have "(M', N') \<in> EqLList (diag A)" ..
   421           with MN fg ab show ?thesis by simp
   422         qed
   423       qed
   424     qed
   425   qed
   426 qed
   427 
   428 text {*
   429   Finality of @{text "llist A"}: Uniqueness of functions defined by corecursion.
   430 *}
   431 
   432 lemma equals_LList_corec:
   433   assumes h: "\<And>x. h x =
   434     (case f x of None \<Rightarrow> NIL | Some (z, w) \<Rightarrow> CONS z (h w))"
   435   shows "h x = (\<lambda>x. LList_corec x f) x"
   436 proof -
   437   def h' \<equiv> "\<lambda>x. LList_corec x f"
   438   then have h': "\<And>x. h' x =
   439       (case f x of None \<Rightarrow> NIL | Some (z, w) \<Rightarrow> CONS z (h' w))"
   440     unfolding h'_def by (simp add: LList_corec)
   441   have "(h x, h' x) \<in> {(h u, h' u) | u. True}" by blast
   442   then show "h x = h' x"
   443   proof (coinduct taking: UNIV rule: LList_equalityI)
   444     case (EqLList M N)
   445     then obtain x where MN: "M = h x" "N = h' x" by blast
   446     show ?case
   447     proof (cases "f x")
   448       case None
   449       with h h' MN have ?EqNIL by simp
   450       then show ?thesis ..
   451     next
   452       case (Some p)
   453       with h h' MN have "M = CONS (fst p) (h (snd p))"
   454 	and "N = CONS (fst p) (h' (snd p))"
   455         by (simp_all split: prod.split)
   456       then have ?EqCONS by (auto iff: diag_iff)
   457       then show ?thesis ..
   458     qed
   459   qed
   460 qed
   461 
   462 
   463 lemma llist_equalityI
   464   [consumes 1, case_names Eqllist, case_conclusion Eqllist EqLNil EqLCons]:
   465   assumes r: "(l1, l2) \<in> r"
   466     and step: "\<And>q. q \<in> r \<Longrightarrow>
   467       q = (LNil, LNil) \<or>
   468         (\<exists>l1 l2 a b.
   469           q = (LCons a l1, LCons b l2) \<and> a = b \<and>
   470             ((l1, l2) \<in> r \<or> l1 = l2))"
   471       (is "\<And>q. _ \<Longrightarrow> ?EqLNil q \<or> ?EqLCons q")
   472   shows "l1 = l2"
   473 proof -
   474   def M \<equiv> "Rep_llist l1" and N \<equiv> "Rep_llist l2"
   475   with r have "(M, N) \<in> {(Rep_llist l1, Rep_llist l2) | l1 l2. (l1, l2) \<in> r}"
   476     by blast
   477   then have "M = N"
   478   proof (coinduct taking: UNIV rule: LList_equalityI)
   479     case (EqLList M N)
   480     then obtain l1 l2 where
   481         MN: "M = Rep_llist l1" "N = Rep_llist l2" and r: "(l1, l2) \<in> r"
   482       by auto
   483     from step [OF r] show ?case
   484     proof
   485       assume "?EqLNil (l1, l2)"
   486       with MN have ?EqNIL by (simp add: Rep_llist_LNil)
   487       then show ?thesis ..
   488     next
   489       assume "?EqLCons (l1, l2)"
   490       with MN have ?EqCONS
   491         by (force simp add: Rep_llist_LCons EqLList_diag intro: Rep_llist_UNIV)
   492       then show ?thesis ..
   493     qed
   494   qed
   495   then show ?thesis by (simp add: M_def N_def Rep_llist_inject)
   496 qed
   497 
   498 lemma llist_fun_equalityI
   499   [case_names LNil LCons, case_conclusion LCons EqLNil EqLCons]:
   500   assumes fun_LNil: "f LNil = g LNil"
   501     and fun_LCons: "\<And>x l.
   502       (f (LCons x l), g (LCons x l)) = (LNil, LNil) \<or>
   503         (\<exists>l1 l2 a b.
   504           (f (LCons x l), g (LCons x l)) = (LCons a l1, LCons b l2) \<and>
   505             a = b \<and> ((l1, l2) \<in> {(f u, g u) | u. True} \<or> l1 = l2))"
   506       (is "\<And>x l. ?fun_LCons x l")
   507   shows "f l = g l"
   508 proof -
   509   have "(f l, g l) \<in> {(f l, g l) | l. True}" by blast
   510   then show ?thesis
   511   proof (coinduct rule: llist_equalityI)
   512     case (Eqllist q)
   513     then obtain l where q: "q = (f l, g l)" by blast
   514     show ?case
   515     proof (cases l)
   516       case LNil
   517       with fun_LNil and q have "q = (g LNil, g LNil)" by simp
   518       then show ?thesis by (cases "g LNil") simp_all
   519     next
   520       case (LCons x l')
   521       with `?fun_LCons x l'` q LCons show ?thesis by blast
   522     qed
   523   qed
   524 qed
   525 
   526 
   527 subsection {* Derived operations -- both on the set and abstract type *}
   528 
   529 subsubsection {* @{text Lconst} *}
   530 
   531 definition "Lconst M \<equiv> lfp (\<lambda>N. CONS M N)"
   532 
   533 lemma Lconst_fun_mono: "mono (CONS M)"
   534   by (simp add: monoI CONS_mono)
   535 
   536 lemma Lconst: "Lconst M = CONS M (Lconst M)"
   537   by (rule Lconst_def [THEN def_lfp_unfold]) (rule Lconst_fun_mono)
   538 
   539 lemma Lconst_type:
   540   assumes "M \<in> A"
   541   shows "Lconst M \<in> LList A"
   542 proof -
   543   have "Lconst M \<in> {Lconst (id M)}" by simp
   544   then show ?thesis
   545   proof coinduct
   546     case (LList N)
   547     then have "N = Lconst M" by simp
   548     also have "\<dots> = CONS M (Lconst M)" by (rule Lconst)
   549     finally have ?CONS using `M \<in> A` by simp
   550     then show ?case ..
   551   qed
   552 qed
   553 
   554 lemma Lconst_eq_LList_corec: "Lconst M = LList_corec M (\<lambda>x. Some (x, x))"
   555   apply (rule equals_LList_corec)
   556   apply simp
   557   apply (rule Lconst)
   558   done
   559 
   560 lemma gfp_Lconst_eq_LList_corec:
   561     "gfp (\<lambda>N. CONS M N) = LList_corec M (\<lambda>x. Some(x, x))"
   562   apply (rule equals_LList_corec)
   563   apply simp
   564   apply (rule Lconst_fun_mono [THEN gfp_unfold])
   565   done
   566 
   567 
   568 subsubsection {* @{text Lmap} and @{text lmap} *}
   569 
   570 definition
   571   "Lmap f M = LList_corec M (List_case None (\<lambda>x M'. Some (f x, M')))"
   572 definition
   573   "lmap f l = llist_corec l
   574     (\<lambda>z.
   575       case z of LNil \<Rightarrow> None
   576       | LCons y z \<Rightarrow> Some (f y, z))"
   577 
   578 lemma Lmap_NIL [simp]: "Lmap f NIL = NIL"
   579   and Lmap_CONS [simp]: "Lmap f (CONS M N) = CONS (f M) (Lmap f N)"
   580   by (simp_all add: Lmap_def LList_corec)
   581 
   582 lemma Lmap_type:
   583   assumes M: "M \<in> LList A"
   584     and f: "\<And>x. x \<in> A \<Longrightarrow> f x \<in> B"
   585   shows "Lmap f M \<in> LList B"
   586 proof -
   587   from M have "Lmap f M \<in> {Lmap f N | N. N \<in> LList A}" by blast
   588   then show ?thesis
   589   proof coinduct
   590     case (LList L)
   591     then obtain N where L: "L = Lmap f N" and N: "N \<in> LList A" by blast
   592     from N show ?case
   593     proof cases
   594       case NIL
   595       with L have ?NIL by simp
   596       then show ?thesis ..
   597     next
   598       case (CONS K a)
   599       with f L have ?CONS by auto
   600       then show ?thesis ..
   601     qed
   602   qed
   603 qed
   604 
   605 lemma Lmap_compose:
   606   assumes M: "M \<in> LList A"
   607   shows "Lmap (f o g) M = Lmap f (Lmap g M)"  (is "?lhs M = ?rhs M")
   608 proof -
   609   have "(?lhs M, ?rhs M) \<in> {(?lhs N, ?rhs N) | N. N \<in> LList A}"
   610     using M by blast
   611   then show ?thesis
   612   proof (coinduct taking: "range (\<lambda>N. N)" rule: LList_equalityI)
   613     case (EqLList L M)
   614     then obtain N where LM: "L = ?lhs N" "M = ?rhs N" and N: "N \<in> LList A" by blast
   615     from N show ?case
   616     proof cases
   617       case NIL
   618       with LM have ?EqNIL by simp
   619       then show ?thesis ..
   620     next
   621       case CONS
   622       with LM have ?EqCONS by auto
   623       then show ?thesis ..
   624     qed
   625   qed
   626 qed
   627 
   628 lemma Lmap_ident:
   629   assumes M: "M \<in> LList A"
   630   shows "Lmap (\<lambda>x. x) M = M"  (is "?lmap M = _")
   631 proof -
   632   have "(?lmap M, M) \<in> {(?lmap N, N) | N. N \<in> LList A}" using M by blast
   633   then show ?thesis
   634   proof (coinduct taking: "range (\<lambda>N. N)" rule: LList_equalityI)
   635     case (EqLList L M)
   636     then obtain N where LM: "L = ?lmap N" "M = N" and N: "N \<in> LList A" by blast
   637     from N show ?case
   638     proof cases
   639       case NIL
   640       with LM have ?EqNIL by simp
   641       then show ?thesis ..
   642     next
   643       case CONS
   644       with LM have ?EqCONS by auto
   645       then show ?thesis ..
   646     qed
   647   qed
   648 qed
   649 
   650 lemma lmap_LNil [simp]: "lmap f LNil = LNil"
   651   and lmap_LCons [simp]: "lmap f (LCons M N) = LCons (f M) (lmap f N)"
   652   by (simp_all add: lmap_def llist_corec)
   653 
   654 lemma lmap_compose [simp]: "lmap (f o g) l = lmap f (lmap g l)"
   655   by (coinduct l rule: llist_fun_equalityI) auto
   656 
   657 lemma lmap_ident [simp]: "lmap (\<lambda>x. x) l = l"
   658   by (coinduct l rule: llist_fun_equalityI) auto
   659 
   660 
   661 
   662 subsubsection {* @{text Lappend} *}
   663 
   664 definition
   665   "Lappend M N = LList_corec (M, N)
   666     (split (List_case
   667         (List_case None (\<lambda>N1 N2. Some (N1, (NIL, N2))))
   668         (\<lambda>M1 M2 N. Some (M1, (M2, N)))))"
   669 definition
   670   "lappend l n = llist_corec (l, n)
   671     (split (llist_case
   672         (llist_case None (\<lambda>n1 n2. Some (n1, (LNil, n2))))
   673         (\<lambda>l1 l2 n. Some (l1, (l2, n)))))"
   674 
   675 lemma Lappend_NIL_NIL [simp]:
   676     "Lappend NIL NIL = NIL"
   677   and Lappend_NIL_CONS [simp]:
   678     "Lappend NIL (CONS N N') = CONS N (Lappend NIL N')"
   679   and Lappend_CONS [simp]:
   680     "Lappend (CONS M M') N = CONS M (Lappend M' N)"
   681   by (simp_all add: Lappend_def LList_corec)
   682 
   683 lemma Lappend_NIL [simp]: "M \<in> LList A \<Longrightarrow> Lappend NIL M = M"
   684   by (erule LList_fun_equalityI) auto
   685 
   686 lemma Lappend_NIL2: "M \<in> LList A \<Longrightarrow> Lappend M NIL = M"
   687   by (erule LList_fun_equalityI) auto
   688 
   689 lemma Lappend_type:
   690   assumes M: "M \<in> LList A" and N: "N \<in> LList A"
   691   shows "Lappend M N \<in> LList A"
   692 proof -
   693   have "Lappend M N \<in> {Lappend u v | u v. u \<in> LList A \<and> v \<in> LList A}"
   694     using M N by blast
   695   then show ?thesis
   696   proof coinduct
   697     case (LList L)
   698     then obtain M N where L: "L = Lappend M N"
   699         and M: "M \<in> LList A" and N: "N \<in> LList A"
   700       by blast
   701     from M show ?case
   702     proof cases
   703       case NIL
   704       from N show ?thesis
   705       proof cases
   706         case NIL
   707         with L and `M = NIL` have ?NIL by simp
   708         then show ?thesis ..
   709       next
   710         case CONS
   711         with L and `M = NIL` have ?CONS by simp
   712         then show ?thesis ..
   713       qed
   714     next
   715       case CONS
   716       with L N have ?CONS by auto
   717       then show ?thesis ..
   718     qed
   719   qed
   720 qed
   721 
   722 lemma lappend_LNil_LNil [simp]: "lappend LNil LNil = LNil"
   723   and lappend_LNil_LCons [simp]: "lappend LNil (LCons l l') = LCons l (lappend LNil l')"
   724   and lappend_LCons [simp]: "lappend (LCons l l') m = LCons l (lappend l' m)"
   725   by (simp_all add: lappend_def llist_corec)
   726 
   727 lemma lappend_LNil1 [simp]: "lappend LNil l = l"
   728   by (coinduct l rule: llist_fun_equalityI) auto
   729 
   730 lemma lappend_LNil2 [simp]: "lappend l LNil = l"
   731   by (coinduct l rule: llist_fun_equalityI) auto
   732 
   733 lemma lappend_assoc: "lappend (lappend l1 l2) l3 = lappend l1 (lappend l2 l3)"
   734   by (coinduct l1 rule: llist_fun_equalityI) auto
   735 
   736 lemma lmap_lappend_distrib: "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)"
   737   by (coinduct l rule: llist_fun_equalityI) auto
   738 
   739 
   740 subsection{* iterates *}
   741 
   742 text {* @{text llist_fun_equalityI} cannot be used here! *}
   743 
   744 definition
   745   iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
   746   "iterates f a = llist_corec a (\<lambda>x. Some (x, f x))"
   747 
   748 lemma iterates: "iterates f x = LCons x (iterates f (f x))"
   749   apply (unfold iterates_def)
   750   apply (subst llist_corec)
   751   apply simp
   752   done
   753 
   754 lemma lmap_iterates: "lmap f (iterates f x) = iterates f (f x)"
   755 proof -
   756   have "(lmap f (iterates f x), iterates f (f x)) \<in>
   757     {(lmap f (iterates f u), iterates f (f u)) | u. True}" by blast
   758   then show ?thesis
   759   proof (coinduct rule: llist_equalityI)
   760     case (Eqllist q)
   761     then obtain x where q: "q = (lmap f (iterates f x), iterates f (f x))"
   762       by blast
   763     also have "iterates f (f x) = LCons (f x) (iterates f (f (f x)))"
   764       by (subst iterates) rule
   765     also have "iterates f x = LCons x (iterates f (f x))"
   766       by (subst iterates) rule
   767     finally have ?EqLCons by auto
   768     then show ?case ..
   769   qed
   770 qed
   771 
   772 lemma iterates_lmap: "iterates f x = LCons x (lmap f (iterates f x))"
   773   by (subst lmap_iterates) (rule iterates)
   774 
   775 
   776 subsection{* A rather complex proof about iterates -- cf.\ Andy Pitts *}
   777 
   778 lemma funpow_lmap:
   779   fixes f :: "'a \<Rightarrow> 'a"
   780   shows "(lmap f ^ n) (LCons b l) = LCons ((f ^ n) b) ((lmap f ^ n) l)"
   781   by (induct n) simp_all
   782 
   783 
   784 lemma iterates_equality:
   785   assumes h: "\<And>x. h x = LCons x (lmap f (h x))"
   786   shows "h = iterates f"
   787 proof
   788   fix x
   789   have "(h x, iterates f x) \<in>
   790       {((lmap f ^ n) (h u), (lmap f ^ n) (iterates f u)) | u n. True}"
   791   proof -
   792     have "(h x, iterates f x) = ((lmap f ^ 0) (h x), (lmap f ^ 0) (iterates f x))"
   793       by simp
   794     then show ?thesis by blast
   795   qed
   796   then show "h x = iterates f x"
   797   proof (coinduct rule: llist_equalityI)
   798     case (Eqllist q)
   799     then obtain u n where "q = ((lmap f ^ n) (h u), (lmap f ^ n) (iterates f u))"
   800         (is "_ = (?q1, ?q2)")
   801       by auto
   802     also have "?q1 = LCons ((f ^ n) u) ((lmap f ^ Suc n) (h u))"
   803     proof -
   804       have "?q1 = (lmap f ^ n) (LCons u (lmap f (h u)))"
   805         by (subst h) rule
   806       also have "\<dots> = LCons ((f ^ n) u) ((lmap f ^ n) (lmap f (h u)))"
   807         by (rule funpow_lmap)
   808       also have "(lmap f ^ n) (lmap f (h u)) = (lmap f ^ Suc n) (h u)"
   809         by (simp add: funpow_swap1)
   810       finally show ?thesis .
   811     qed
   812     also have "?q2 = LCons ((f ^ n) u) ((lmap f ^ Suc n) (iterates f u))"
   813     proof -
   814       have "?q2 = (lmap f ^ n) (LCons u (iterates f (f u)))"
   815         by (subst iterates) rule
   816       also have "\<dots> = LCons ((f ^ n) u) ((lmap f ^ n) (iterates f (f u)))"
   817         by (rule funpow_lmap)
   818       also have "(lmap f ^ n) (iterates f (f u)) = (lmap f ^ Suc n) (iterates f u)"
   819         by (simp add: lmap_iterates funpow_swap1)
   820       finally show ?thesis .
   821     qed
   822     finally have ?EqLCons by (auto simp del: funpow.simps)
   823     then show ?case ..
   824   qed
   825 qed
   826 
   827 lemma lappend_iterates: "lappend (iterates f x) l = iterates f x"
   828 proof -
   829   have "(lappend (iterates f x) l, iterates f x) \<in>
   830     {(lappend (iterates f u) l, iterates f u) | u. True}" by blast
   831   then show ?thesis
   832   proof (coinduct rule: llist_equalityI)
   833     case (Eqllist q)
   834     then obtain x where "q = (lappend (iterates f x) l, iterates f x)" by blast
   835     also have "iterates f x = LCons x (iterates f (f x))" by (rule iterates)
   836     finally have ?EqLCons by auto
   837     then show ?case ..
   838   qed
   839 qed
   840 
   841 end