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