src/HOL/Library/Coinductive_List.thy
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 34941 156925dd67af
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
     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 primrec
    57   LList_corec_aux :: "nat \<Rightarrow> ('a \<Rightarrow> ('b Datatype.item \<times> 'a) option) \<Rightarrow>
    58     'a \<Rightarrow> 'b Datatype.item" where
    59     "LList_corec_aux 0 f x = {}"
    60   | "LList_corec_aux (Suc k) f x =
    61       (case f x of
    62         None \<Rightarrow> NIL
    63       | Some (z, w) \<Rightarrow> CONS z (LList_corec_aux k f w))"
    64 
    65 definition "LList_corec a f = (\<Union>k. LList_corec_aux k f a)"
    66 
    67 text {*
    68   Note: the subsequent recursion equation for @{text LList_corec} may
    69   be used with the Simplifier, provided it operates in a non-strict
    70   fashion for case expressions (i.e.\ the usual @{text case}
    71   congruence rule needs to be present).
    72 *}
    73 
    74 lemma LList_corec:
    75   "LList_corec a f =
    76     (case f a of None \<Rightarrow> NIL | Some (z, w) \<Rightarrow> CONS z (LList_corec w f))"
    77   (is "?lhs = ?rhs")
    78 proof
    79   show "?lhs \<subseteq> ?rhs"
    80     apply (unfold LList_corec_def)
    81     apply (rule UN_least)
    82     apply (case_tac k)
    83      apply (simp_all (no_asm_simp) split: option.splits)
    84     apply (rule allI impI subset_refl [THEN CONS_mono] UNIV_I [THEN UN_upper])+
    85     done
    86   show "?rhs \<subseteq> ?lhs"
    87     apply (simp add: LList_corec_def split: option.splits)
    88     apply (simp add: CONS_UN1)
    89     apply safe
    90      apply (rule_tac a = "Suc ?k" in UN_I, simp, simp)+
    91     done
    92 qed
    93 
    94 lemma LList_corec_type: "LList_corec a f \<in> LList UNIV"
    95 proof -
    96   have "\<exists>x. LList_corec a f = LList_corec x f" by blast
    97   then show ?thesis
    98   proof coinduct
    99     case (LList L)
   100     then obtain x where L: "L = LList_corec x f" by blast
   101     show ?case
   102     proof (cases "f x")
   103       case None
   104       then have "LList_corec x f = NIL"
   105         by (simp add: LList_corec)
   106       with L have ?NIL by simp
   107       then show ?thesis ..
   108     next
   109       case (Some p)
   110       then have "LList_corec x f = CONS (fst p) (LList_corec (snd p) f)"
   111         by (simp add: LList_corec split: prod.split)
   112       with L have ?CONS by auto
   113       then show ?thesis ..
   114     qed
   115   qed
   116 qed
   117 
   118 
   119 subsection {* Abstract type definition *}
   120 
   121 typedef 'a llist = "LList (range Datatype.Leaf) :: 'a Datatype.item set"
   122 proof
   123   show "NIL \<in> ?llist" ..
   124 qed
   125 
   126 lemma NIL_type: "NIL \<in> llist"
   127   unfolding llist_def by (rule LList.NIL)
   128 
   129 lemma CONS_type: "a \<in> range Datatype.Leaf \<Longrightarrow>
   130     M \<in> llist \<Longrightarrow> CONS a M \<in> llist"
   131   unfolding llist_def by (rule LList.CONS)
   132 
   133 lemma llistI: "x \<in> LList (range Datatype.Leaf) \<Longrightarrow> x \<in> llist"
   134   by (simp add: llist_def)
   135 
   136 lemma llistD: "x \<in> llist \<Longrightarrow> x \<in> LList (range Datatype.Leaf)"
   137   by (simp add: llist_def)
   138 
   139 lemma Rep_llist_UNIV: "Rep_llist x \<in> LList UNIV"
   140 proof -
   141   have "Rep_llist x \<in> llist" by (rule Rep_llist)
   142   then have "Rep_llist x \<in> LList (range Datatype.Leaf)"
   143     by (simp add: llist_def)
   144   also have "\<dots> \<subseteq> LList UNIV" by (rule LList_mono) simp
   145   finally show ?thesis .
   146 qed
   147 
   148 definition "LNil = Abs_llist NIL"
   149 definition "LCons x xs = Abs_llist (CONS (Datatype.Leaf x) (Rep_llist xs))"
   150 
   151 code_datatype LNil LCons
   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   [code del]: "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 
   203 syntax  (* FIXME? *)
   204   LNil :: logic
   205   LCons :: logic
   206 translations
   207   "case p of XCONST LNil \<Rightarrow> a | XCONST 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, nitpick_simp]:
   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, nitpick_simp]: "lmap f LNil = LNil"
   660   and lmap_LCons [simp, nitpick_simp]:
   661   "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, nitpick_simp]: "lappend LNil LNil = LNil"
   733   and lappend_LNil_LCons [simp, nitpick_simp]: "lappend LNil (LCons l l') = LCons l (lappend LNil l')"
   734   and lappend_LCons [simp, nitpick_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 [nitpick_simp]: "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 setup {*
   852   Nitpick.register_codatatype @{typ "'a llist"} @{const_name llist_case}
   853     (map dest_Const [@{term LNil}, @{term LCons}])
   854 *}
   855 
   856 end