src/HOL/Library/Coinductive_List.thy
author chaieb
Mon Feb 09 17:21:46 2009 +0000 (2009-02-09)
changeset 29847 af32126ee729
parent 28856 5e009a80fe6d
child 30198 922f944f03b2
permissions -rw-r--r--
added Determinants to Library
     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 code_datatype LNil LCons
   154 
   155 lemma LCons_not_LNil [iff]: "LCons x xs \<noteq> LNil"
   156   apply (simp add: LNil_def LCons_def)
   157   apply (subst Abs_llist_inject)
   158     apply (auto intro: NIL_type CONS_type Rep_llist)
   159   done
   160 
   161 lemma LNil_not_LCons [iff]: "LNil \<noteq> LCons x xs"
   162   by (rule LCons_not_LNil [symmetric])
   163 
   164 lemma LCons_inject [iff]: "(LCons x xs = LCons y ys) = (x = y \<and> xs = ys)"
   165   apply (simp add: LCons_def)
   166   apply (subst Abs_llist_inject)
   167     apply (auto simp add: Rep_llist_inject intro: CONS_type Rep_llist)
   168   done
   169 
   170 lemma Rep_llist_LNil: "Rep_llist LNil = NIL"
   171   by (simp add: LNil_def add: Abs_llist_inverse NIL_type)
   172 
   173 lemma Rep_llist_LCons: "Rep_llist (LCons x l) =
   174     CONS (Datatype.Leaf x) (Rep_llist l)"
   175   by (simp add: LCons_def Abs_llist_inverse CONS_type Rep_llist)
   176 
   177 lemma llist_cases [cases type: llist]:
   178   obtains
   179     (LNil) "l = LNil"
   180   | (LCons) x l' where "l = LCons x l'"
   181 proof (cases l)
   182   case (Abs_llist L)
   183   from `L \<in> llist` have "L \<in> LList (range Datatype.Leaf)" by (rule llistD)
   184   then show ?thesis
   185   proof cases
   186     case NIL
   187     with Abs_llist have "l = LNil" by (simp add: LNil_def)
   188     with LNil show ?thesis .
   189   next
   190     case (CONS a K)
   191     then have "K \<in> llist" by (blast intro: llistI)
   192     then obtain l' where "K = Rep_llist l'" by cases
   193     with CONS and Abs_llist obtain x where "l = LCons x l'"
   194       by (auto simp add: LCons_def Abs_llist_inject)
   195     with LCons show ?thesis .
   196   qed
   197 qed
   198 
   199 
   200 definition
   201   [code del]: "llist_case c d l =
   202     List_case c (\<lambda>x y. d (inv Datatype.Leaf x) (Abs_llist y)) (Rep_llist l)"
   203 
   204 syntax  (* FIXME? *)
   205   LNil :: logic
   206   LCons :: logic
   207 translations
   208   "case p of LNil \<Rightarrow> a | LCons x l \<Rightarrow> b" \<rightleftharpoons> "CONST llist_case a (\<lambda>x l. b) p"
   209 
   210 lemma llist_case_LNil [simp, code]: "llist_case c d LNil = c"
   211   by (simp add: llist_case_def LNil_def
   212     NIL_type Abs_llist_inverse)
   213 
   214 lemma llist_case_LCons [simp, code]: "llist_case c d (LCons M N) = d M N"
   215   by (simp add: llist_case_def LCons_def
   216     CONS_type Abs_llist_inverse Rep_llist Rep_llist_inverse inj_Leaf)
   217 
   218 lemma llist_case_cert:
   219   assumes "CASE \<equiv> llist_case c d"
   220   shows "(CASE LNil \<equiv> c) &&& (CASE (LCons M N) \<equiv> d M N)"
   221   using assms by simp_all
   222 
   223 setup {*
   224   Code.add_case @{thm llist_case_cert}
   225 *}
   226 
   227 definition
   228   [code del]: "llist_corec a f =
   229     Abs_llist (LList_corec a
   230       (\<lambda>z.
   231         case f z of None \<Rightarrow> None
   232         | Some (v, w) \<Rightarrow> Some (Datatype.Leaf v, w)))"
   233 
   234 lemma LList_corec_type2:
   235   "LList_corec a
   236     (\<lambda>z. case f z of None \<Rightarrow> None
   237       | Some (v, w) \<Rightarrow> Some (Datatype.Leaf v, w)) \<in> llist"
   238   (is "?corec a \<in> _")
   239 proof (unfold llist_def)
   240   let "LList_corec a ?g" = "?corec a"
   241   have "\<exists>x. ?corec a = ?corec x" by blast
   242   then show "?corec a \<in> LList (range Datatype.Leaf)"
   243   proof coinduct
   244     case (LList L)
   245     then obtain x where L: "L = ?corec x" by blast
   246     show ?case
   247     proof (cases "f x")
   248       case None
   249       then have "?corec x = NIL"
   250         by (simp add: LList_corec)
   251       with L have ?NIL by simp
   252       then show ?thesis ..
   253     next
   254       case (Some p)
   255       then have "?corec x =
   256           CONS (Datatype.Leaf (fst p)) (?corec (snd p))"
   257         by (simp add: LList_corec split: prod.split)
   258       with L have ?CONS by auto
   259       then show ?thesis ..
   260     qed
   261   qed
   262 qed
   263 
   264 lemma llist_corec [code]:
   265   "llist_corec a f =
   266     (case f a of None \<Rightarrow> LNil | Some (z, w) \<Rightarrow> LCons z (llist_corec w f))"
   267 proof (cases "f a")
   268   case None
   269   then show ?thesis
   270     by (simp add: llist_corec_def LList_corec LNil_def)
   271 next
   272   case (Some p)
   273 
   274   let "?corec a" = "llist_corec a f"
   275   let "?rep_corec a" =
   276     "LList_corec a
   277       (\<lambda>z. case f z of None \<Rightarrow> None
   278         | Some (v, w) \<Rightarrow> Some (Datatype.Leaf v, w))"
   279 
   280   have "?corec a = Abs_llist (?rep_corec a)"
   281     by (simp only: llist_corec_def)
   282   also from Some have "?rep_corec a =
   283       CONS (Datatype.Leaf (fst p)) (?rep_corec (snd p))"
   284     by (simp add: LList_corec split: prod.split)
   285   also have "?rep_corec (snd p) = Rep_llist (?corec (snd p))"
   286     by (simp only: llist_corec_def Abs_llist_inverse LList_corec_type2)
   287   finally have "?corec a = LCons (fst p) (?corec (snd p))"
   288     by (simp only: LCons_def)
   289   with Some show ?thesis by (simp split: prod.split)
   290 qed
   291 
   292 
   293 subsection {* Equality as greatest fixed-point -- the bisimulation principle *}
   294 
   295 coinductive_set EqLList for r
   296 where EqNIL: "(NIL, NIL) \<in> EqLList r"
   297   | EqCONS: "(a, b) \<in> r \<Longrightarrow> (M, N) \<in> EqLList r \<Longrightarrow>
   298       (CONS a M, CONS b N) \<in> EqLList r"
   299 
   300 lemma EqLList_unfold:
   301     "EqLList r = dsum (diag {Datatype.Numb 0}) (dprod r (EqLList r))"
   302   by (fast intro!: EqLList.intros [unfolded NIL_def CONS_def]
   303            elim: EqLList.cases [unfolded NIL_def CONS_def])
   304 
   305 lemma EqLList_implies_ntrunc_equality:
   306     "(M, N) \<in> EqLList (diag A) \<Longrightarrow> ntrunc k M = ntrunc k N"
   307   apply (induct k arbitrary: M N rule: nat_less_induct)
   308   apply (erule EqLList.cases)
   309    apply (safe del: equalityI)
   310   apply (case_tac n)
   311    apply simp
   312   apply (rename_tac n')
   313   apply (case_tac n')
   314    apply (simp_all add: CONS_def less_Suc_eq)
   315   done
   316 
   317 lemma Domain_EqLList: "Domain (EqLList (diag A)) \<subseteq> LList A"
   318   apply (rule subsetI)
   319   apply (erule LList.coinduct)
   320   apply (subst (asm) EqLList_unfold)
   321   apply (auto simp add: NIL_def CONS_def)
   322   done
   323 
   324 lemma EqLList_diag: "EqLList (diag A) = diag (LList A)"
   325   (is "?lhs = ?rhs")
   326 proof
   327   show "?lhs \<subseteq> ?rhs"
   328     apply (rule subsetI)
   329     apply (rule_tac p = x in PairE)
   330     apply clarify
   331     apply (rule diag_eqI)
   332      apply (rule EqLList_implies_ntrunc_equality [THEN ntrunc_equality],
   333        assumption)
   334     apply (erule DomainI [THEN Domain_EqLList [THEN subsetD]])
   335     done
   336   {
   337     fix M N assume "(M, N) \<in> diag (LList A)"
   338     then have "(M, N) \<in> EqLList (diag A)"
   339     proof coinduct
   340       case (EqLList M N)
   341       then obtain L where L: "L \<in> LList A" and MN: "M = L" "N = L" by blast
   342       from L show ?case
   343       proof cases
   344         case NIL with MN have ?EqNIL by simp
   345         then show ?thesis ..
   346       next
   347         case CONS with MN have ?EqCONS by (simp add: diagI)
   348         then show ?thesis ..
   349       qed
   350     qed
   351   }
   352   then show "?rhs \<subseteq> ?lhs" by auto
   353 qed
   354 
   355 lemma EqLList_diag_iff [iff]: "(p \<in> EqLList (diag A)) = (p \<in> diag (LList A))"
   356   by (simp only: EqLList_diag)
   357 
   358 
   359 text {*
   360   To show two LLists are equal, exhibit a bisimulation!  (Also admits
   361   true equality.)
   362 *}
   363 
   364 lemma LList_equalityI
   365   [consumes 1, case_names EqLList, case_conclusion EqLList EqNIL EqCONS]:
   366   assumes r: "(M, N) \<in> r"
   367     and step: "\<And>M N. (M, N) \<in> r \<Longrightarrow>
   368       M = NIL \<and> N = NIL \<or>
   369         (\<exists>a b M' N'.
   370           M = CONS a M' \<and> N = CONS b N' \<and> (a, b) \<in> diag A \<and>
   371             ((M', N') \<in> r \<or> (M', N') \<in> EqLList (diag A)))"
   372   shows "M = N"
   373 proof -
   374   from r have "(M, N) \<in> EqLList (diag A)"
   375   proof coinduct
   376     case EqLList
   377     then show ?case by (rule step)
   378   qed
   379   then show ?thesis by auto
   380 qed
   381 
   382 lemma LList_fun_equalityI
   383   [consumes 1, case_names NIL_type NIL CONS, case_conclusion CONS EqNIL EqCONS]:
   384   assumes M: "M \<in> LList A"
   385     and fun_NIL: "g NIL \<in> LList A"  "f NIL = g NIL"
   386     and fun_CONS: "\<And>x l. x \<in> A \<Longrightarrow> l \<in> LList A \<Longrightarrow>
   387             (f (CONS x l), g (CONS x l)) = (NIL, NIL) \<or>
   388             (\<exists>M N a b.
   389               (f (CONS x l), g (CONS x l)) = (CONS a M, CONS b N) \<and>
   390                 (a, b) \<in> diag A \<and>
   391                 (M, N) \<in> {(f u, g u) | u. u \<in> LList A} \<union> diag (LList A))"
   392       (is "\<And>x l. _ \<Longrightarrow> _ \<Longrightarrow> ?fun_CONS x l")
   393   shows "f M = g M"
   394 proof -
   395   let ?bisim = "{(f L, g L) | L. L \<in> LList A}"
   396   have "(f M, g M) \<in> ?bisim" using M by blast
   397   then show ?thesis
   398   proof (coinduct taking: A rule: LList_equalityI)
   399     case (EqLList M N)
   400     then obtain L where MN: "M = f L" "N = g L" and L: "L \<in> LList A" by blast
   401     from L show ?case
   402     proof (cases L)
   403       case NIL
   404       with fun_NIL and MN 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       case (CONS a K)
   409       from fun_CONS and `a \<in> A` `K \<in> LList A`
   410       have "?fun_CONS a K" (is "?NIL \<or> ?CONS") .
   411       then show ?thesis
   412       proof
   413         assume ?NIL
   414         with MN CONS have "(M, N) \<in> diag (LList A)" by auto
   415         then have "(M, N) \<in> EqLList (diag A)" ..
   416         then show ?thesis by cases simp_all
   417       next
   418         assume ?CONS
   419         with CONS obtain a b M' N' where
   420             fg: "(f L, g L) = (CONS a M', CONS b N')"
   421           and ab: "(a, b) \<in> diag A"
   422           and M'N': "(M', N') \<in> ?bisim \<union> diag (LList A)"
   423           by blast
   424         from M'N' show ?thesis
   425         proof
   426           assume "(M', N') \<in> ?bisim"
   427           with MN fg ab show ?thesis by simp
   428         next
   429           assume "(M', N') \<in> diag (LList A)"
   430           then have "(M', N') \<in> EqLList (diag A)" ..
   431           with MN fg ab show ?thesis by simp
   432         qed
   433       qed
   434     qed
   435   qed
   436 qed
   437 
   438 text {*
   439   Finality of @{text "llist A"}: Uniqueness of functions defined by corecursion.
   440 *}
   441 
   442 lemma equals_LList_corec:
   443   assumes h: "\<And>x. h x =
   444     (case f x of None \<Rightarrow> NIL | Some (z, w) \<Rightarrow> CONS z (h w))"
   445   shows "h x = (\<lambda>x. LList_corec x f) x"
   446 proof -
   447   def h' \<equiv> "\<lambda>x. LList_corec x f"
   448   then have h': "\<And>x. h' x =
   449       (case f x of None \<Rightarrow> NIL | Some (z, w) \<Rightarrow> CONS z (h' w))"
   450     unfolding h'_def by (simp add: LList_corec)
   451   have "(h x, h' x) \<in> {(h u, h' u) | u. True}" by blast
   452   then show "h x = h' x"
   453   proof (coinduct taking: UNIV rule: LList_equalityI)
   454     case (EqLList M N)
   455     then obtain x where MN: "M = h x" "N = h' x" by blast
   456     show ?case
   457     proof (cases "f x")
   458       case None
   459       with h h' MN have ?EqNIL by simp
   460       then show ?thesis ..
   461     next
   462       case (Some p)
   463       with h h' MN have "M = CONS (fst p) (h (snd p))"
   464 	and "N = CONS (fst p) (h' (snd p))"
   465         by (simp_all split: prod.split)
   466       then have ?EqCONS by (auto iff: diag_iff)
   467       then show ?thesis ..
   468     qed
   469   qed
   470 qed
   471 
   472 
   473 lemma llist_equalityI
   474   [consumes 1, case_names Eqllist, case_conclusion Eqllist EqLNil EqLCons]:
   475   assumes r: "(l1, l2) \<in> r"
   476     and step: "\<And>q. q \<in> r \<Longrightarrow>
   477       q = (LNil, LNil) \<or>
   478         (\<exists>l1 l2 a b.
   479           q = (LCons a l1, LCons b l2) \<and> a = b \<and>
   480             ((l1, l2) \<in> r \<or> l1 = l2))"
   481       (is "\<And>q. _ \<Longrightarrow> ?EqLNil q \<or> ?EqLCons q")
   482   shows "l1 = l2"
   483 proof -
   484   def M \<equiv> "Rep_llist l1" and N \<equiv> "Rep_llist l2"
   485   with r have "(M, N) \<in> {(Rep_llist l1, Rep_llist l2) | l1 l2. (l1, l2) \<in> r}"
   486     by blast
   487   then have "M = N"
   488   proof (coinduct taking: UNIV rule: LList_equalityI)
   489     case (EqLList M N)
   490     then obtain l1 l2 where
   491         MN: "M = Rep_llist l1" "N = Rep_llist l2" and r: "(l1, l2) \<in> r"
   492       by auto
   493     from step [OF r] show ?case
   494     proof
   495       assume "?EqLNil (l1, l2)"
   496       with MN have ?EqNIL by (simp add: Rep_llist_LNil)
   497       then show ?thesis ..
   498     next
   499       assume "?EqLCons (l1, l2)"
   500       with MN have ?EqCONS
   501         by (force simp add: Rep_llist_LCons EqLList_diag intro: Rep_llist_UNIV)
   502       then show ?thesis ..
   503     qed
   504   qed
   505   then show ?thesis by (simp add: M_def N_def Rep_llist_inject)
   506 qed
   507 
   508 lemma llist_fun_equalityI
   509   [case_names LNil LCons, case_conclusion LCons EqLNil EqLCons]:
   510   assumes fun_LNil: "f LNil = g LNil"
   511     and fun_LCons: "\<And>x l.
   512       (f (LCons x l), g (LCons x l)) = (LNil, LNil) \<or>
   513         (\<exists>l1 l2 a b.
   514           (f (LCons x l), g (LCons x l)) = (LCons a l1, LCons b l2) \<and>
   515             a = b \<and> ((l1, l2) \<in> {(f u, g u) | u. True} \<or> l1 = l2))"
   516       (is "\<And>x l. ?fun_LCons x l")
   517   shows "f l = g l"
   518 proof -
   519   have "(f l, g l) \<in> {(f l, g l) | l. True}" by blast
   520   then show ?thesis
   521   proof (coinduct rule: llist_equalityI)
   522     case (Eqllist q)
   523     then obtain l where q: "q = (f l, g l)" by blast
   524     show ?case
   525     proof (cases l)
   526       case LNil
   527       with fun_LNil and q have "q = (g LNil, g LNil)" by simp
   528       then show ?thesis by (cases "g LNil") simp_all
   529     next
   530       case (LCons x l')
   531       with `?fun_LCons x l'` q LCons show ?thesis by blast
   532     qed
   533   qed
   534 qed
   535 
   536 
   537 subsection {* Derived operations -- both on the set and abstract type *}
   538 
   539 subsubsection {* @{text Lconst} *}
   540 
   541 definition "Lconst M \<equiv> lfp (\<lambda>N. CONS M N)"
   542 
   543 lemma Lconst_fun_mono: "mono (CONS M)"
   544   by (simp add: monoI CONS_mono)
   545 
   546 lemma Lconst: "Lconst M = CONS M (Lconst M)"
   547   by (rule Lconst_def [THEN def_lfp_unfold]) (rule Lconst_fun_mono)
   548 
   549 lemma Lconst_type:
   550   assumes "M \<in> A"
   551   shows "Lconst M \<in> LList A"
   552 proof -
   553   have "Lconst M \<in> {Lconst (id M)}" by simp
   554   then show ?thesis
   555   proof coinduct
   556     case (LList N)
   557     then have "N = Lconst M" by simp
   558     also have "\<dots> = CONS M (Lconst M)" by (rule Lconst)
   559     finally have ?CONS using `M \<in> A` by simp
   560     then show ?case ..
   561   qed
   562 qed
   563 
   564 lemma Lconst_eq_LList_corec: "Lconst M = LList_corec M (\<lambda>x. Some (x, x))"
   565   apply (rule equals_LList_corec)
   566   apply simp
   567   apply (rule Lconst)
   568   done
   569 
   570 lemma gfp_Lconst_eq_LList_corec:
   571     "gfp (\<lambda>N. CONS M N) = LList_corec M (\<lambda>x. Some(x, x))"
   572   apply (rule equals_LList_corec)
   573   apply simp
   574   apply (rule Lconst_fun_mono [THEN gfp_unfold])
   575   done
   576 
   577 
   578 subsubsection {* @{text Lmap} and @{text lmap} *}
   579 
   580 definition
   581   "Lmap f M = LList_corec M (List_case None (\<lambda>x M'. Some (f x, M')))"
   582 definition
   583   "lmap f l = llist_corec l
   584     (\<lambda>z.
   585       case z of LNil \<Rightarrow> None
   586       | LCons y z \<Rightarrow> Some (f y, z))"
   587 
   588 lemma Lmap_NIL [simp]: "Lmap f NIL = NIL"
   589   and Lmap_CONS [simp]: "Lmap f (CONS M N) = CONS (f M) (Lmap f N)"
   590   by (simp_all add: Lmap_def LList_corec)
   591 
   592 lemma Lmap_type:
   593   assumes M: "M \<in> LList A"
   594     and f: "\<And>x. x \<in> A \<Longrightarrow> f x \<in> B"
   595   shows "Lmap f M \<in> LList B"
   596 proof -
   597   from M have "Lmap f M \<in> {Lmap f N | N. N \<in> LList A}" by blast
   598   then show ?thesis
   599   proof coinduct
   600     case (LList L)
   601     then obtain N where L: "L = Lmap f N" and N: "N \<in> LList A" by blast
   602     from N show ?case
   603     proof cases
   604       case NIL
   605       with L have ?NIL by simp
   606       then show ?thesis ..
   607     next
   608       case (CONS K a)
   609       with f L have ?CONS by auto
   610       then show ?thesis ..
   611     qed
   612   qed
   613 qed
   614 
   615 lemma Lmap_compose:
   616   assumes M: "M \<in> LList A"
   617   shows "Lmap (f o g) M = Lmap f (Lmap g M)"  (is "?lhs M = ?rhs M")
   618 proof -
   619   have "(?lhs M, ?rhs M) \<in> {(?lhs N, ?rhs N) | N. N \<in> LList A}"
   620     using M by blast
   621   then show ?thesis
   622   proof (coinduct taking: "range (\<lambda>N. N)" rule: LList_equalityI)
   623     case (EqLList L M)
   624     then obtain N where LM: "L = ?lhs N" "M = ?rhs N" and N: "N \<in> LList A" by blast
   625     from N show ?case
   626     proof cases
   627       case NIL
   628       with LM have ?EqNIL by simp
   629       then show ?thesis ..
   630     next
   631       case CONS
   632       with LM have ?EqCONS by auto
   633       then show ?thesis ..
   634     qed
   635   qed
   636 qed
   637 
   638 lemma Lmap_ident:
   639   assumes M: "M \<in> LList A"
   640   shows "Lmap (\<lambda>x. x) M = M"  (is "?lmap M = _")
   641 proof -
   642   have "(?lmap M, M) \<in> {(?lmap N, N) | N. N \<in> LList A}" using M by blast
   643   then show ?thesis
   644   proof (coinduct taking: "range (\<lambda>N. N)" rule: LList_equalityI)
   645     case (EqLList L M)
   646     then obtain N where LM: "L = ?lmap N" "M = N" and N: "N \<in> LList A" by blast
   647     from N show ?case
   648     proof cases
   649       case NIL
   650       with LM have ?EqNIL by simp
   651       then show ?thesis ..
   652     next
   653       case CONS
   654       with LM have ?EqCONS by auto
   655       then show ?thesis ..
   656     qed
   657   qed
   658 qed
   659 
   660 lemma lmap_LNil [simp]: "lmap f LNil = LNil"
   661   and lmap_LCons [simp]: "lmap f (LCons M N) = LCons (f M) (lmap f N)"
   662   by (simp_all add: lmap_def llist_corec)
   663 
   664 lemma lmap_compose [simp]: "lmap (f o g) l = lmap f (lmap g l)"
   665   by (coinduct l rule: llist_fun_equalityI) auto
   666 
   667 lemma lmap_ident [simp]: "lmap (\<lambda>x. x) l = l"
   668   by (coinduct l rule: llist_fun_equalityI) auto
   669 
   670 
   671 
   672 subsubsection {* @{text Lappend} *}
   673 
   674 definition
   675   "Lappend M N = LList_corec (M, N)
   676     (split (List_case
   677         (List_case None (\<lambda>N1 N2. Some (N1, (NIL, N2))))
   678         (\<lambda>M1 M2 N. Some (M1, (M2, N)))))"
   679 definition
   680   "lappend l n = llist_corec (l, n)
   681     (split (llist_case
   682         (llist_case None (\<lambda>n1 n2. Some (n1, (LNil, n2))))
   683         (\<lambda>l1 l2 n. Some (l1, (l2, n)))))"
   684 
   685 lemma Lappend_NIL_NIL [simp]:
   686     "Lappend NIL NIL = NIL"
   687   and Lappend_NIL_CONS [simp]:
   688     "Lappend NIL (CONS N N') = CONS N (Lappend NIL N')"
   689   and Lappend_CONS [simp]:
   690     "Lappend (CONS M M') N = CONS M (Lappend M' N)"
   691   by (simp_all add: Lappend_def LList_corec)
   692 
   693 lemma Lappend_NIL [simp]: "M \<in> LList A \<Longrightarrow> Lappend NIL M = M"
   694   by (erule LList_fun_equalityI) auto
   695 
   696 lemma Lappend_NIL2: "M \<in> LList A \<Longrightarrow> Lappend M NIL = M"
   697   by (erule LList_fun_equalityI) auto
   698 
   699 lemma Lappend_type:
   700   assumes M: "M \<in> LList A" and N: "N \<in> LList A"
   701   shows "Lappend M N \<in> LList A"
   702 proof -
   703   have "Lappend M N \<in> {Lappend u v | u v. u \<in> LList A \<and> v \<in> LList A}"
   704     using M N by blast
   705   then show ?thesis
   706   proof coinduct
   707     case (LList L)
   708     then obtain M N where L: "L = Lappend M N"
   709         and M: "M \<in> LList A" and N: "N \<in> LList A"
   710       by blast
   711     from M show ?case
   712     proof cases
   713       case NIL
   714       from N show ?thesis
   715       proof cases
   716         case NIL
   717         with L and `M = NIL` have ?NIL by simp
   718         then show ?thesis ..
   719       next
   720         case CONS
   721         with L and `M = NIL` have ?CONS by simp
   722         then show ?thesis ..
   723       qed
   724     next
   725       case CONS
   726       with L N have ?CONS by auto
   727       then show ?thesis ..
   728     qed
   729   qed
   730 qed
   731 
   732 lemma lappend_LNil_LNil [simp]: "lappend LNil LNil = LNil"
   733   and lappend_LNil_LCons [simp]: "lappend LNil (LCons l l') = LCons l (lappend LNil l')"
   734   and lappend_LCons [simp]: "lappend (LCons l l') m = LCons l (lappend l' m)"
   735   by (simp_all add: lappend_def llist_corec)
   736 
   737 lemma lappend_LNil1 [simp]: "lappend LNil l = l"
   738   by (coinduct l rule: llist_fun_equalityI) auto
   739 
   740 lemma lappend_LNil2 [simp]: "lappend l LNil = l"
   741   by (coinduct l rule: llist_fun_equalityI) auto
   742 
   743 lemma lappend_assoc: "lappend (lappend l1 l2) l3 = lappend l1 (lappend l2 l3)"
   744   by (coinduct l1 rule: llist_fun_equalityI) auto
   745 
   746 lemma lmap_lappend_distrib: "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)"
   747   by (coinduct l rule: llist_fun_equalityI) auto
   748 
   749 
   750 subsection{* iterates *}
   751 
   752 text {* @{text llist_fun_equalityI} cannot be used here! *}
   753 
   754 definition
   755   iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
   756   "iterates f a = llist_corec a (\<lambda>x. Some (x, f x))"
   757 
   758 lemma iterates: "iterates f x = LCons x (iterates f (f x))"
   759   apply (unfold iterates_def)
   760   apply (subst llist_corec)
   761   apply simp
   762   done
   763 
   764 lemma lmap_iterates: "lmap f (iterates f x) = iterates f (f x)"
   765 proof -
   766   have "(lmap f (iterates f x), iterates f (f x)) \<in>
   767     {(lmap f (iterates f u), iterates f (f u)) | u. True}" by blast
   768   then show ?thesis
   769   proof (coinduct rule: llist_equalityI)
   770     case (Eqllist q)
   771     then obtain x where q: "q = (lmap f (iterates f x), iterates f (f x))"
   772       by blast
   773     also have "iterates f (f x) = LCons (f x) (iterates f (f (f x)))"
   774       by (subst iterates) rule
   775     also have "iterates f x = LCons x (iterates f (f x))"
   776       by (subst iterates) rule
   777     finally have ?EqLCons by auto
   778     then show ?case ..
   779   qed
   780 qed
   781 
   782 lemma iterates_lmap: "iterates f x = LCons x (lmap f (iterates f x))"
   783   by (subst lmap_iterates) (rule iterates)
   784 
   785 
   786 subsection{* A rather complex proof about iterates -- cf.\ Andy Pitts *}
   787 
   788 lemma funpow_lmap:
   789   fixes f :: "'a \<Rightarrow> 'a"
   790   shows "(lmap f ^ n) (LCons b l) = LCons ((f ^ n) b) ((lmap f ^ n) l)"
   791   by (induct n) simp_all
   792 
   793 
   794 lemma iterates_equality:
   795   assumes h: "\<And>x. h x = LCons x (lmap f (h x))"
   796   shows "h = iterates f"
   797 proof
   798   fix x
   799   have "(h x, iterates f x) \<in>
   800       {((lmap f ^ n) (h u), (lmap f ^ n) (iterates f u)) | u n. True}"
   801   proof -
   802     have "(h x, iterates f x) = ((lmap f ^ 0) (h x), (lmap f ^ 0) (iterates f x))"
   803       by simp
   804     then show ?thesis by blast
   805   qed
   806   then show "h x = iterates f x"
   807   proof (coinduct rule: llist_equalityI)
   808     case (Eqllist q)
   809     then obtain u n where "q = ((lmap f ^ n) (h u), (lmap f ^ n) (iterates f u))"
   810         (is "_ = (?q1, ?q2)")
   811       by auto
   812     also have "?q1 = LCons ((f ^ n) u) ((lmap f ^ Suc n) (h u))"
   813     proof -
   814       have "?q1 = (lmap f ^ n) (LCons u (lmap f (h u)))"
   815         by (subst h) rule
   816       also have "\<dots> = LCons ((f ^ n) u) ((lmap f ^ n) (lmap f (h u)))"
   817         by (rule funpow_lmap)
   818       also have "(lmap f ^ n) (lmap f (h u)) = (lmap f ^ Suc n) (h u)"
   819         by (simp add: funpow_swap1)
   820       finally show ?thesis .
   821     qed
   822     also have "?q2 = LCons ((f ^ n) u) ((lmap f ^ Suc n) (iterates f u))"
   823     proof -
   824       have "?q2 = (lmap f ^ n) (LCons u (iterates f (f u)))"
   825         by (subst iterates) rule
   826       also have "\<dots> = LCons ((f ^ n) u) ((lmap f ^ n) (iterates f (f u)))"
   827         by (rule funpow_lmap)
   828       also have "(lmap f ^ n) (iterates f (f u)) = (lmap f ^ Suc n) (iterates f u)"
   829         by (simp add: lmap_iterates funpow_swap1)
   830       finally show ?thesis .
   831     qed
   832     finally have ?EqLCons by (auto simp del: funpow.simps)
   833     then show ?case ..
   834   qed
   835 qed
   836 
   837 lemma lappend_iterates: "lappend (iterates f x) l = iterates f x"
   838 proof -
   839   have "(lappend (iterates f x) l, iterates f x) \<in>
   840     {(lappend (iterates f u) l, iterates f u) | u. True}" by blast
   841   then show ?thesis
   842   proof (coinduct rule: llist_equalityI)
   843     case (Eqllist q)
   844     then obtain x where "q = (lappend (iterates f x) l, iterates f x)" by blast
   845     also have "iterates f x = LCons x (iterates f (f x))" by (rule iterates)
   846     finally have ?EqLCons by auto
   847     then show ?case ..
   848   qed
   849 qed
   850 
   851 end