src/HOL/Induct/LList.thy
author urbanc
Tue Jun 05 09:56:19 2007 +0200 (2007-06-05)
changeset 23243 a37d3e6e8323
parent 21404 eb85850d3eb7
child 23746 a455e69c31cc
permissions -rw-r--r--
included Class.thy in the compiling process for Nominal/Examples
     1 (*  Title:      HOL/Induct/LList.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4 
     5 Shares NIL, CONS, List_case with List.thy
     6 
     7 Still needs flatten function -- hard because it need
     8 bounds on the amount of lookahead required.
     9 
    10 Could try (but would it work for the gfp analogue of term?)
    11   LListD_Fun_def "LListD_Fun(A) == (%Z. diag({Numb(0)}) <++> diag(A) <**> Z)"
    12 
    13 A nice but complex example would be [ML for the Working Programmer, page 176]
    14   from(1) = enumerate (Lmap (Lmap(pack), makeqq(from(1),from(1))))
    15 
    16 Previous definition of llistD_Fun was explicit:
    17   llistD_Fun_def
    18    "llistD_Fun(r) ==    
    19        {(LNil,LNil)}  Un        
    20        (UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))`r)"
    21 *)
    22 
    23 header {*Definition of type llist by a greatest fixed point*}
    24 
    25 theory LList imports SList begin
    26 
    27 consts
    28 
    29   llist  :: "'a item set => 'a item set"
    30   LListD :: "('a item * 'a item)set => ('a item * 'a item)set"
    31 
    32 
    33 coinductive "llist(A)"
    34   intros
    35     NIL_I:  "NIL \<in> llist(A)"
    36     CONS_I:         "[| a \<in> A;  M \<in> llist(A) |] ==> CONS a M \<in> llist(A)"
    37 
    38 coinductive "LListD(r)"
    39   intros
    40     NIL_I:  "(NIL, NIL) \<in> LListD(r)"
    41     CONS_I:         "[| (a,b) \<in> r;  (M,N) \<in> LListD(r) |] 
    42                      ==> (CONS a M, CONS b N) \<in> LListD(r)"
    43 
    44 
    45 typedef (LList)
    46   'a llist = "llist(range Leaf) :: 'a item set"
    47   by (blast intro: llist.NIL_I)
    48 
    49 definition
    50   list_Fun   :: "['a item set, 'a item set] => 'a item set" where
    51     --{*Now used exclusively for abbreviating the coinduction rule*}
    52      "list_Fun A X = {z. z = NIL | (\<exists>M a. z = CONS a M & a \<in> A & M \<in> X)}"
    53 
    54 definition
    55   LListD_Fun :: 
    56       "[('a item * 'a item)set, ('a item * 'a item)set] => 
    57        ('a item * 'a item)set" where
    58     "LListD_Fun r X =   
    59        {z. z = (NIL, NIL) |   
    60            (\<exists>M N a b. z = (CONS a M, CONS b N) & (a, b) \<in> r & (M, N) \<in> X)}"
    61 
    62 definition
    63   LNil :: "'a llist" where
    64      --{*abstract constructor*}
    65     "LNil = Abs_LList NIL"
    66 
    67 definition
    68   LCons :: "['a, 'a llist] => 'a llist" where
    69      --{*abstract constructor*}
    70     "LCons x xs = Abs_LList(CONS (Leaf x) (Rep_LList xs))"
    71 
    72 definition
    73   llist_case :: "['b, ['a, 'a llist]=>'b, 'a llist] => 'b" where
    74     "llist_case c d l =
    75        List_case c (%x y. d (inv Leaf x) (Abs_LList y)) (Rep_LList l)"
    76 
    77 definition
    78   LList_corec_fun :: "[nat, 'a=> ('b item * 'a) option, 'a] => 'b item" where
    79     "LList_corec_fun k f ==
    80      nat_rec (%x. {})                         
    81              (%j r x. case f x of None    => NIL
    82                                 | Some(z,w) => CONS z (r w)) 
    83              k"
    84 
    85 definition
    86   LList_corec     :: "['a, 'a => ('b item * 'a) option] => 'b item" where
    87     "LList_corec a f = (\<Union>k. LList_corec_fun k f a)"
    88 
    89 definition
    90   llist_corec     :: "['a, 'a => ('b * 'a) option] => 'b llist" where
    91     "llist_corec a f =
    92        Abs_LList(LList_corec a 
    93                  (%z. case f z of None      => None
    94                                 | Some(v,w) => Some(Leaf(v), w)))"
    95 
    96 definition
    97   llistD_Fun :: "('a llist * 'a llist)set => ('a llist * 'a llist)set" where
    98     "llistD_Fun(r) =   
    99         prod_fun Abs_LList Abs_LList `         
   100                 LListD_Fun (diag(range Leaf))   
   101                             (prod_fun Rep_LList Rep_LList ` r)"
   102 
   103 
   104 
   105 text{* The case syntax for type @{text "'a llist"} *}
   106 syntax  (* FIXME proper case syntax!? *)
   107   LNil :: logic
   108   LCons :: logic
   109 translations
   110   "case p of LNil => a | LCons x l => b" == "CONST llist_case a (%x l. b) p"
   111 
   112 
   113 subsubsection{* Sample function definitions.  Item-based ones start with @{text L} *}
   114 
   115 definition
   116   Lmap       :: "('a item => 'b item) => ('a item => 'b item)" where
   117     "Lmap f M = LList_corec M (List_case None (%x M'. Some((f(x), M'))))"
   118 
   119 definition
   120   lmap       :: "('a=>'b) => ('a llist => 'b llist)" where
   121     "lmap f l = llist_corec l (%z. case z of LNil => None 
   122                                            | LCons y z => Some(f(y), z))"
   123 
   124 definition
   125   iterates   :: "['a => 'a, 'a] => 'a llist" where
   126     "iterates f a = llist_corec a (%x. Some((x, f(x))))"     
   127 
   128 definition
   129   Lconst     :: "'a item => 'a item" where
   130     "Lconst(M) == lfp(%N. CONS M N)"
   131 
   132 definition
   133   Lappend    :: "['a item, 'a item] => 'a item" where
   134    "Lappend M N = LList_corec (M,N)                                         
   135      (split(List_case (List_case None (%N1 N2. Some((N1, (NIL,N2))))) 
   136                       (%M1 M2 N. Some((M1, (M2,N))))))"
   137 
   138 definition
   139   lappend    :: "['a llist, 'a llist] => 'a llist" where
   140     "lappend l n = llist_corec (l,n)                                         
   141        (split(llist_case (llist_case None (%n1 n2. Some((n1, (LNil,n2))))) 
   142                          (%l1 l2 n. Some((l1, (l2,n))))))"
   143 
   144 
   145 text{*Append generates its result by applying f, where
   146     f((NIL,NIL))          = None
   147     f((NIL, CONS N1 N2))  = Some((N1, (NIL,N2))
   148     f((CONS M1 M2, N))    = Some((M1, (M2,N))
   149 *}
   150 
   151 text{*
   152 SHOULD @{text LListD_Fun_CONS_I}, etc., be equations (for rewriting)?
   153 *}
   154 
   155 lemmas UN1_I = UNIV_I [THEN UN_I, standard]
   156 
   157 subsubsection{* Simplification *}
   158 
   159 declare option.split [split]
   160 
   161 text{*This justifies using llist in other recursive type definitions*}
   162 lemma llist_mono: "A\<subseteq>B ==> llist(A) \<subseteq> llist(B)"
   163 apply (simp add: llist.defs)
   164 apply (rule gfp_mono)
   165 apply (assumption | rule basic_monos)+
   166 done
   167 
   168 
   169 lemma llist_unfold: "llist(A) = usum {Numb(0)} (uprod A (llist A))"
   170   by (fast intro!: llist.intros [unfolded NIL_def CONS_def]
   171            elim: llist.cases [unfolded NIL_def CONS_def])
   172 
   173 
   174 subsection{* Type checking by coinduction *}
   175 
   176 text {*
   177   {\dots} using @{text list_Fun} THE COINDUCTIVE DEFINITION PACKAGE
   178   COULD DO THIS!
   179 *}
   180 
   181 lemma llist_coinduct: 
   182     "[| M \<in> X;  X \<subseteq> list_Fun A (X Un llist(A)) |] ==>  M \<in> llist(A)"
   183 apply (simp add: list_Fun_def)
   184 apply (erule llist.coinduct)
   185 apply (blast intro: elim:); 
   186 done
   187 
   188 lemma list_Fun_NIL_I [iff]: "NIL \<in> list_Fun A X"
   189 by (simp add: list_Fun_def NIL_def)
   190 
   191 lemma list_Fun_CONS_I [intro!,simp]: 
   192     "[| M \<in> A;  N \<in> X |] ==> CONS M N \<in> list_Fun A X"
   193 by (simp add: list_Fun_def CONS_def)
   194 
   195 
   196 text{*Utilise the ``strong'' part, i.e. @{text "gfp(f)"}*}
   197 lemma list_Fun_llist_I: "M \<in> llist(A) ==> M \<in> list_Fun A (X Un llist(A))"
   198 apply (unfold llist.defs list_Fun_def)
   199 apply (rule gfp_fun_UnI2) 
   200 apply (rule monoI, auto)
   201 done
   202 
   203 subsection{* @{text LList_corec} satisfies the desired recurion equation *}
   204 
   205 text{*A continuity result?*}
   206 lemma CONS_UN1: "CONS M (\<Union>x. f(x)) = (\<Union>x. CONS M (f x))"
   207 apply (simp add: CONS_def In1_UN1 Scons_UN1_y)
   208 done
   209 
   210 lemma CONS_mono: "[| M\<subseteq>M';  N\<subseteq>N' |] ==> CONS M N \<subseteq> CONS M' N'"
   211 apply (simp add: CONS_def In1_mono Scons_mono)
   212 done
   213 
   214 declare LList_corec_fun_def [THEN def_nat_rec_0, simp]
   215         LList_corec_fun_def [THEN def_nat_rec_Suc, simp]
   216 
   217 
   218 subsubsection{* The directions of the equality are proved separately *}
   219 
   220 lemma LList_corec_subset1: 
   221     "LList_corec a f \<subseteq>  
   222      (case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f))"
   223 apply (unfold LList_corec_def)
   224 apply (rule UN_least)
   225 apply (case_tac k) 
   226 apply (simp_all (no_asm_simp))
   227 apply (rule allI impI subset_refl [THEN CONS_mono] UNIV_I [THEN UN_upper])+
   228 done
   229 
   230 lemma LList_corec_subset2: 
   231     "(case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f)) \<subseteq>  
   232      LList_corec a f"
   233 apply (simp add: LList_corec_def)
   234 apply (simp add: CONS_UN1, safe) 
   235 apply (rule_tac a="Suc(?k)" in UN_I, simp, simp)+ 
   236 done
   237 
   238 text{*the recursion equation for @{text LList_corec} -- NOT SUITABLE FOR REWRITING!*}
   239 lemma LList_corec:
   240      "LList_corec a f =   
   241       (case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f))"
   242 by (rule equalityI LList_corec_subset1 LList_corec_subset2)+
   243 
   244 text{*definitional version of same*}
   245 lemma def_LList_corec: 
   246      "[| !!x. h(x) = LList_corec x f |]      
   247       ==> h(a) = (case f a of None => NIL | Some(z,w) => CONS z (h w))"
   248 by (simp add: LList_corec)
   249 
   250 text{*A typical use of co-induction to show membership in the @{text gfp}. 
   251   Bisimulation is @{text "range(%x. LList_corec x f)"} *}
   252 lemma LList_corec_type: "LList_corec a f \<in> llist UNIV"
   253 apply (rule_tac X = "range (%x. LList_corec x ?g)" in llist_coinduct)
   254 apply (rule rangeI, safe)
   255 apply (subst LList_corec, simp)
   256 done
   257 
   258 
   259 subsection{* @{text llist} equality as a @{text gfp}; the bisimulation principle *}
   260 
   261 text{*This theorem is actually used, unlike the many similar ones in ZF*}
   262 lemma LListD_unfold: "LListD r = dsum (diag {Numb 0}) (dprod r (LListD r))"
   263   by (fast intro!: LListD.intros [unfolded NIL_def CONS_def]
   264            elim: LListD.cases [unfolded NIL_def CONS_def])
   265 
   266 lemma LListD_implies_ntrunc_equality [rule_format]:
   267      "\<forall>M N. (M,N) \<in> LListD(diag A) --> ntrunc k M = ntrunc k N"
   268 apply (induct_tac "k" rule: nat_less_induct) 
   269 apply (safe del: equalityI)
   270 apply (erule LListD.cases)
   271 apply (safe del: equalityI)
   272 apply (case_tac "n", simp)
   273 apply (rename_tac "n'")
   274 apply (case_tac "n'")
   275 apply (simp_all add: CONS_def less_Suc_eq)
   276 done
   277 
   278 text{*The domain of the @{text LListD} relation*}
   279 lemma Domain_LListD: 
   280     "Domain (LListD(diag A)) \<subseteq> llist(A)"
   281 apply (simp add: llist.defs NIL_def CONS_def)
   282 apply (rule gfp_upperbound)
   283 txt{*avoids unfolding @{text LListD} on the rhs*}
   284 apply (rule_tac P = "%x. Domain x \<subseteq> ?B" in LListD_unfold [THEN ssubst], auto) 
   285 done
   286 
   287 text{*This inclusion justifies the use of coinduction to show @{text "M = N"}*}
   288 lemma LListD_subset_diag: "LListD(diag A) \<subseteq> diag(llist(A))"
   289 apply (rule subsetI)
   290 apply (rule_tac p = x in PairE, safe)
   291 apply (rule diag_eqI)
   292 apply (rule LListD_implies_ntrunc_equality [THEN ntrunc_equality], assumption) 
   293 apply (erule DomainI [THEN Domain_LListD [THEN subsetD]])
   294 done
   295 
   296 
   297 subsubsection{* Coinduction, using @{text LListD_Fun} *}
   298 
   299 text {* THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS! *}
   300 
   301 lemma LListD_Fun_mono: "A\<subseteq>B ==> LListD_Fun r A \<subseteq> LListD_Fun r B"
   302 apply (simp add: LListD_Fun_def)
   303 apply (assumption | rule basic_monos)+
   304 done
   305 
   306 lemma LListD_coinduct: 
   307     "[| M \<in> X;  X \<subseteq> LListD_Fun r (X Un LListD(r)) |] ==>  M \<in> LListD(r)"
   308 apply (simp add: LListD_Fun_def)
   309 apply (erule LListD.coinduct)
   310 apply (auto ); 
   311 done
   312 
   313 lemma LListD_Fun_NIL_I: "(NIL,NIL) \<in> LListD_Fun r s"
   314 by (simp add: LListD_Fun_def NIL_def)
   315 
   316 lemma LListD_Fun_CONS_I: 
   317      "[| x\<in>A;  (M,N):s |] ==> (CONS x M, CONS x N) \<in> LListD_Fun (diag A) s"
   318 by (simp add: LListD_Fun_def CONS_def, blast)
   319 
   320 text{*Utilise the "strong" part, i.e. @{text "gfp(f)"}*}
   321 lemma LListD_Fun_LListD_I:
   322      "M \<in> LListD(r) ==> M \<in> LListD_Fun r (X Un LListD(r))"
   323 apply (unfold LListD.defs LListD_Fun_def)
   324 apply (rule gfp_fun_UnI2) 
   325 apply (rule monoI, auto)
   326 done
   327 
   328 
   329 text{*This converse inclusion helps to strengthen @{text LList_equalityI}*}
   330 lemma diag_subset_LListD: "diag(llist(A)) \<subseteq> LListD(diag A)"
   331 apply (rule subsetI)
   332 apply (erule LListD_coinduct)
   333 apply (rule subsetI)
   334 apply (erule diagE)
   335 apply (erule ssubst)
   336 apply (erule llist.cases)
   337 apply (simp_all add: diagI LListD_Fun_NIL_I LListD_Fun_CONS_I)
   338 done
   339 
   340 lemma LListD_eq_diag: "LListD(diag A) = diag(llist(A))"
   341 apply (rule equalityI LListD_subset_diag diag_subset_LListD)+
   342 done
   343 
   344 lemma LListD_Fun_diag_I: "M \<in> llist(A) ==> (M,M) \<in> LListD_Fun (diag A) (X Un diag(llist(A)))"
   345 apply (rule LListD_eq_diag [THEN subst])
   346 apply (rule LListD_Fun_LListD_I)
   347 apply (simp add: LListD_eq_diag diagI)
   348 done
   349 
   350 
   351 subsubsection{* To show two LLists are equal, exhibit a bisimulation! 
   352       [also admits true equality]
   353    Replace @{text A} by some particular set, like @{text "{x. True}"}??? *}
   354 lemma LList_equalityI:
   355      "[| (M,N) \<in> r;  r \<subseteq> LListD_Fun (diag A) (r Un diag(llist(A))) |] 
   356       ==>  M=N"
   357 apply (rule LListD_subset_diag [THEN subsetD, THEN diagE])
   358 apply (erule LListD_coinduct)
   359 apply (simp add: LListD_eq_diag, safe)
   360 done
   361 
   362 
   363 subsection{* Finality of @{text "llist(A)"}: Uniqueness of functions defined by corecursion *}
   364 
   365 text{*We must remove @{text Pair_eq} because it may turn an instance of reflexivity
   366   @{text "(h1 b, h2 b) = (h1 ?x17, h2 ?x17)"} into a conjunction! 
   367   (or strengthen the Solver?) 
   368 *}
   369 declare Pair_eq [simp del]
   370 
   371 text{*abstract proof using a bisimulation*}
   372 lemma LList_corec_unique:
   373  "[| !!x. h1(x) = (case f x of None => NIL | Some(z,w) => CONS z (h1 w));   
   374      !!x. h2(x) = (case f x of None => NIL | Some(z,w) => CONS z (h2 w)) |] 
   375   ==> h1=h2"
   376 apply (rule ext)
   377 txt{*next step avoids an unknown (and flexflex pair) in simplification*}
   378 apply (rule_tac A = UNIV and r = "range(%u. (h1 u, h2 u))" 
   379        in LList_equalityI)
   380 apply (rule rangeI, safe)
   381 apply (simp add: LListD_Fun_NIL_I UNIV_I [THEN LListD_Fun_CONS_I])
   382 done
   383 
   384 lemma equals_LList_corec:
   385  "[| !!x. h(x) = (case f x of None => NIL | Some(z,w) => CONS z (h w)) |]  
   386   ==> h = (%x. LList_corec x f)"
   387 by (simp add: LList_corec_unique LList_corec) 
   388 
   389 
   390 subsubsection{*Obsolete proof of @{text LList_corec_unique}: 
   391                complete induction, not coinduction *}
   392 
   393 lemma ntrunc_one_CONS [simp]: "ntrunc (Suc 0) (CONS M N) = {}"
   394 by (simp add: CONS_def ntrunc_one_In1)
   395 
   396 lemma ntrunc_CONS [simp]: 
   397     "ntrunc (Suc(Suc(k))) (CONS M N) = CONS (ntrunc k M) (ntrunc k N)"
   398 by (simp add: CONS_def)
   399 
   400 
   401 lemma
   402  assumes prem1:
   403           "!!x. h1 x = (case f x of None => NIL | Some(z,w) => CONS z (h1 w))"
   404      and prem2:
   405           "!!x. h2 x = (case f x of None => NIL | Some(z,w) => CONS z (h2 w))"
   406  shows "h1=h2"
   407 apply (rule ntrunc_equality [THEN ext])
   408 apply (rule_tac x = x in spec)
   409 apply (induct_tac "k" rule: nat_less_induct)
   410 apply (rename_tac "n")
   411 apply (rule allI)
   412 apply (subst prem1)
   413 apply (subst prem2, simp)
   414 apply (intro strip) 
   415 apply (case_tac "n") 
   416 apply (rename_tac [2] "m")
   417 apply (case_tac [2] "m", simp_all)
   418 done
   419 
   420 
   421 subsection{*Lconst: defined directly by @{text lfp} *}
   422 
   423 text{*But it could be defined by corecursion.*}
   424 
   425 lemma Lconst_fun_mono: "mono(CONS(M))"
   426 apply (rule monoI subset_refl CONS_mono)+
   427 apply assumption 
   428 done
   429 
   430 text{* @{text "Lconst(M) = CONS M (Lconst M)"} *}
   431 lemmas Lconst = Lconst_fun_mono [THEN Lconst_def [THEN def_lfp_unfold]]
   432 
   433 text{*A typical use of co-induction to show membership in the gfp.
   434   The containing set is simply the singleton @{text "{Lconst(M)}"}. *}
   435 lemma Lconst_type: "M\<in>A ==> Lconst(M): llist(A)"
   436 apply (rule singletonI [THEN llist_coinduct], safe)
   437 apply (rule_tac P = "%u. u \<in> ?A" in Lconst [THEN ssubst])
   438 apply (assumption | rule list_Fun_CONS_I singletonI UnI1)+
   439 done
   440 
   441 lemma Lconst_eq_LList_corec: "Lconst(M) = LList_corec M (%x. Some(x,x))"
   442 apply (rule equals_LList_corec [THEN fun_cong], simp)
   443 apply (rule Lconst)
   444 done
   445 
   446 text{*Thus we could have used gfp in the definition of Lconst*}
   447 lemma gfp_Lconst_eq_LList_corec: "gfp(%N. CONS M N) = LList_corec M (%x. Some(x,x))"
   448 apply (rule equals_LList_corec [THEN fun_cong], simp)
   449 apply (rule Lconst_fun_mono [THEN gfp_unfold])
   450 done
   451 
   452 
   453 subsection{* Isomorphisms *}
   454 
   455 lemma LListI: "x \<in> llist (range Leaf) ==> x \<in> LList"
   456 by (simp add: LList_def)
   457 
   458 lemma LListD: "x \<in> LList ==> x \<in> llist (range Leaf)"
   459 by (simp add: LList_def)
   460 
   461 
   462 subsubsection{* Distinctness of constructors *}
   463 
   464 lemma LCons_not_LNil [iff]: "~ LCons x xs = LNil"
   465 apply (simp add: LNil_def LCons_def)
   466 apply (subst Abs_LList_inject)
   467 apply (rule llist.intros CONS_not_NIL rangeI LListI Rep_LList [THEN LListD])+
   468 done
   469 
   470 lemmas LNil_not_LCons [iff] = LCons_not_LNil [THEN not_sym, standard]
   471 
   472 
   473 subsubsection{* llist constructors *}
   474 
   475 lemma Rep_LList_LNil: "Rep_LList LNil = NIL"
   476 apply (simp add: LNil_def)
   477 apply (rule llist.NIL_I [THEN LListI, THEN Abs_LList_inverse])
   478 done
   479 
   480 lemma Rep_LList_LCons: "Rep_LList(LCons x l) = CONS (Leaf x) (Rep_LList l)"
   481 apply (simp add: LCons_def)
   482 apply (rule llist.CONS_I [THEN LListI, THEN Abs_LList_inverse] 
   483             rangeI Rep_LList [THEN LListD])+
   484 done
   485 
   486 subsubsection{* Injectiveness of @{text CONS} and @{text LCons} *}
   487 
   488 lemma CONS_CONS_eq2: "(CONS M N=CONS M' N') = (M=M' & N=N')"
   489 apply (simp add: CONS_def)
   490 done
   491 
   492 lemmas CONS_inject = CONS_CONS_eq [THEN iffD1, THEN conjE, standard]
   493 
   494 
   495 text{*For reasoning about abstract llist constructors*}
   496 
   497 declare Rep_LList [THEN LListD, intro] LListI [intro]
   498 declare llist.intros [intro]
   499 
   500 lemma LCons_LCons_eq [iff]: "(LCons x xs=LCons y ys) = (x=y & xs=ys)"
   501 apply (simp add: LCons_def)
   502 apply (subst Abs_LList_inject)
   503 apply (auto simp add: Rep_LList_inject)
   504 done
   505 
   506 lemma CONS_D2: "CONS M N \<in> llist(A) ==> M \<in> A & N \<in> llist(A)"
   507 apply (erule llist.cases)
   508 apply (erule CONS_neq_NIL, fast)
   509 done
   510 
   511 
   512 subsection{* Reasoning about @{text "llist(A)"} *}
   513 
   514 text{*A special case of @{text list_equality} for functions over lazy lists*}
   515 lemma LList_fun_equalityI:
   516  "[| M \<in> llist(A); g(NIL): llist(A);                              
   517      f(NIL)=g(NIL);                                              
   518      !!x l. [| x\<in>A;  l \<in> llist(A) |] ==>                          
   519             (f(CONS x l),g(CONS x l)) \<in>                          
   520                 LListD_Fun (diag A) ((%u.(f(u),g(u)))`llist(A) Un   
   521                                     diag(llist(A)))              
   522   |] ==> f(M) = g(M)"
   523 apply (rule LList_equalityI)
   524 apply (erule imageI)
   525 apply (rule image_subsetI)
   526 apply (erule_tac aa=x in llist.cases)
   527 apply (erule ssubst, erule ssubst, erule LListD_Fun_diag_I, blast) 
   528 done
   529 
   530 
   531 subsection{* The functional @{text Lmap} *}
   532 
   533 lemma Lmap_NIL [simp]: "Lmap f NIL = NIL"
   534 by (rule Lmap_def [THEN def_LList_corec, THEN trans], simp)
   535 
   536 lemma Lmap_CONS [simp]: "Lmap f (CONS M N) = CONS (f M) (Lmap f N)"
   537 by (rule Lmap_def [THEN def_LList_corec, THEN trans], simp)
   538 
   539 
   540 
   541 text{*Another type-checking proof by coinduction*}
   542 lemma Lmap_type:
   543      "[| M \<in> llist(A);  !!x. x\<in>A ==> f(x):B |] ==> Lmap f M \<in> llist(B)"
   544 apply (erule imageI [THEN llist_coinduct], safe)
   545 apply (erule llist.cases, simp_all)
   546 done
   547 
   548 text{*This type checking rule synthesises a sufficiently large set for @{text f}*}
   549 lemma Lmap_type2: "M \<in> llist(A) ==> Lmap f M \<in> llist(f`A)"
   550 apply (erule Lmap_type)
   551 apply (erule imageI)
   552 done
   553 
   554 subsubsection{* Two easy results about @{text Lmap} *}
   555 
   556 lemma Lmap_compose: "M \<in> llist(A) ==> Lmap (f o g) M = Lmap f (Lmap g M)"
   557 apply (simp add: o_def)
   558 apply (drule imageI)
   559 apply (erule LList_equalityI, safe)
   560 apply (erule llist.cases, simp_all)
   561 apply (rule LListD_Fun_NIL_I imageI UnI1 rangeI [THEN LListD_Fun_CONS_I])+
   562 apply assumption  
   563 done
   564 
   565 lemma Lmap_ident: "M \<in> llist(A) ==> Lmap (%x. x) M = M"
   566 apply (drule imageI)
   567 apply (erule LList_equalityI, safe)
   568 apply (erule llist.cases, simp_all)
   569 apply (rule LListD_Fun_NIL_I imageI UnI1 rangeI [THEN LListD_Fun_CONS_I])+
   570 apply assumption 
   571 done
   572 
   573 
   574 subsection{* @{text Lappend} -- its two arguments cause some complications! *}
   575 
   576 lemma Lappend_NIL_NIL [simp]: "Lappend NIL NIL = NIL"
   577 apply (simp add: Lappend_def)
   578 apply (rule LList_corec [THEN trans], simp)
   579 done
   580 
   581 lemma Lappend_NIL_CONS [simp]: 
   582     "Lappend NIL (CONS N N') = CONS N (Lappend NIL N')"
   583 apply (simp add: Lappend_def)
   584 apply (rule LList_corec [THEN trans], simp)
   585 done
   586 
   587 lemma Lappend_CONS [simp]: 
   588     "Lappend (CONS M M') N = CONS M (Lappend M' N)"
   589 apply (simp add: Lappend_def)
   590 apply (rule LList_corec [THEN trans], simp)
   591 done
   592 
   593 declare llist.intros [simp] LListD_Fun_CONS_I [simp] 
   594         range_eqI [simp] image_eqI [simp]
   595 
   596 
   597 lemma Lappend_NIL [simp]: "M \<in> llist(A) ==> Lappend NIL M = M"
   598 by (erule LList_fun_equalityI, simp_all)
   599 
   600 lemma Lappend_NIL2: "M \<in> llist(A) ==> Lappend M NIL = M"
   601 by (erule LList_fun_equalityI, simp_all)
   602 
   603 
   604 subsubsection{* Alternative type-checking proofs for @{text Lappend} *}
   605 
   606 text{*weak co-induction: bisimulation and case analysis on both variables*}
   607 lemma Lappend_type: "[| M \<in> llist(A); N \<in> llist(A) |] ==> Lappend M N \<in> llist(A)"
   608 apply (rule_tac X = "\<Union>u\<in>llist (A) . \<Union>v \<in> llist (A) . {Lappend u v}" in llist_coinduct)
   609 apply fast
   610 apply safe
   611 apply (erule_tac aa = u in llist.cases)
   612 apply (erule_tac aa = v in llist.cases, simp_all, blast)
   613 done
   614 
   615 text{*strong co-induction: bisimulation and case analysis on one variable*}
   616 lemma Lappend_type': "[| M \<in> llist(A); N \<in> llist(A) |] ==> Lappend M N \<in> llist(A)"
   617 apply (rule_tac X = "(%u. Lappend u N) `llist (A)" in llist_coinduct)
   618 apply (erule imageI)
   619 apply (rule image_subsetI)
   620 apply (erule_tac aa = x in llist.cases)
   621 apply (simp add: list_Fun_llist_I, simp)
   622 done
   623 
   624 subsection{* Lazy lists as the type @{text "'a llist"} -- strongly typed versions of above *}
   625 
   626 subsubsection{* @{text llist_case}: case analysis for @{text "'a llist"} *}
   627 
   628 declare LListI [THEN Abs_LList_inverse, simp]
   629 declare Rep_LList_inverse [simp]
   630 declare Rep_LList [THEN LListD, simp]
   631 declare rangeI [simp] inj_Leaf [simp] 
   632 
   633 lemma llist_case_LNil [simp]: "llist_case c d LNil = c"
   634 by (simp add: llist_case_def LNil_def)
   635 
   636 lemma llist_case_LCons [simp]: "llist_case c d (LCons M N) = d M N"
   637 by (simp add: llist_case_def LCons_def)
   638 
   639 
   640 text{*Elimination is case analysis, not induction.*}
   641 lemma llistE: "[| l=LNil ==> P;  !!x l'. l=LCons x l' ==> P |] ==> P"
   642 apply (rule Rep_LList [THEN LListD, THEN llist.cases])
   643  apply (simp add: Rep_LList_LNil [symmetric] Rep_LList_inject, blast) 
   644 apply (erule LListI [THEN Rep_LList_cases], clarify)
   645 apply (simp add: Rep_LList_LCons [symmetric] Rep_LList_inject, blast) 
   646 done
   647 
   648 subsubsection{* @{text llist_corec}: corecursion for @{text "'a llist"} *}
   649 
   650 text{*Lemma for the proof of @{text llist_corec}*}
   651 lemma LList_corec_type2:
   652      "LList_corec a  
   653            (%z. case f z of None => None | Some(v,w) => Some(Leaf(v),w)) 
   654        \<in> llist(range Leaf)"
   655 apply (rule_tac X = "range (%x. LList_corec x ?g)" in llist_coinduct)
   656 apply (rule rangeI, safe)
   657 apply (subst LList_corec, force)
   658 done
   659 
   660 lemma llist_corec: 
   661     "llist_corec a f =   
   662      (case f a of None => LNil | Some(z,w) => LCons z (llist_corec w f))"
   663 apply (unfold llist_corec_def LNil_def LCons_def)
   664 apply (subst LList_corec)
   665 apply (case_tac "f a")
   666 apply (simp add: LList_corec_type2)
   667 apply (force simp add: LList_corec_type2)
   668 done
   669 
   670 text{*definitional version of same*}
   671 lemma def_llist_corec: 
   672      "[| !!x. h(x) = llist_corec x f |] ==>      
   673       h(a) = (case f a of None => LNil | Some(z,w) => LCons z (h w))"
   674 by (simp add: llist_corec)
   675 
   676 subsection{* Proofs about type @{text "'a llist"} functions *}
   677 
   678 subsection{* Deriving @{text llist_equalityI} -- @{text llist} equality is a bisimulation *}
   679 
   680 lemma LListD_Fun_subset_Times_llist: 
   681     "r \<subseteq> (llist A) <*> (llist A) 
   682      ==> LListD_Fun (diag A) r \<subseteq> (llist A) <*> (llist A)"
   683 by (auto simp add: LListD_Fun_def)
   684 
   685 lemma subset_Times_llist:
   686      "prod_fun Rep_LList Rep_LList ` r \<subseteq>  
   687      (llist(range Leaf)) <*> (llist(range Leaf))"
   688 by (blast intro: Rep_LList [THEN LListD])
   689 
   690 lemma prod_fun_lemma:
   691      "r \<subseteq> (llist(range Leaf)) <*> (llist(range Leaf)) 
   692       ==> prod_fun (Rep_LList o Abs_LList) (Rep_LList o Abs_LList) ` r \<subseteq> r"
   693 apply safe
   694 apply (erule subsetD [THEN SigmaE2], assumption)
   695 apply (simp add: LListI [THEN Abs_LList_inverse])
   696 done
   697 
   698 lemma prod_fun_range_eq_diag:
   699      "prod_fun Rep_LList  Rep_LList ` range(%x. (x, x)) =  
   700       diag(llist(range Leaf))"
   701 apply (rule equalityI, blast) 
   702 apply (fast elim: LListI [THEN Abs_LList_inverse, THEN subst])
   703 done
   704 
   705 text{*Used with @{text lfilter}*}
   706 lemma llistD_Fun_mono: 
   707     "A\<subseteq>B ==> llistD_Fun A \<subseteq> llistD_Fun B"
   708 apply (simp add: llistD_Fun_def prod_fun_def, auto)
   709 apply (rule image_eqI)
   710  prefer 2 apply (blast intro: rev_subsetD [OF _ LListD_Fun_mono], force)
   711 done
   712 
   713 subsubsection{* To show two llists are equal, exhibit a bisimulation! 
   714       [also admits true equality] *}
   715 lemma llist_equalityI: 
   716     "[| (l1,l2) \<in> r;  r \<subseteq> llistD_Fun(r Un range(%x.(x,x))) |] ==> l1=l2"
   717 apply (simp add: llistD_Fun_def)
   718 apply (rule Rep_LList_inject [THEN iffD1])
   719 apply (rule_tac r = "prod_fun Rep_LList Rep_LList `r" and A = "range (Leaf)" in LList_equalityI)
   720 apply (erule prod_fun_imageI)
   721 apply (erule image_mono [THEN subset_trans])
   722 apply (rule image_compose [THEN subst])
   723 apply (rule prod_fun_compose [THEN subst])
   724 apply (subst image_Un)
   725 apply (subst prod_fun_range_eq_diag)
   726 apply (rule LListD_Fun_subset_Times_llist [THEN prod_fun_lemma])
   727 apply (rule subset_Times_llist [THEN Un_least])
   728 apply (rule diag_subset_Times)
   729 done
   730 
   731 subsubsection{* Rules to prove the 2nd premise of @{text llist_equalityI} *}
   732 lemma llistD_Fun_LNil_I [simp]: "(LNil,LNil) \<in> llistD_Fun(r)"
   733 apply (simp add: llistD_Fun_def LNil_def)
   734 apply (rule LListD_Fun_NIL_I [THEN prod_fun_imageI])
   735 done
   736 
   737 lemma llistD_Fun_LCons_I [simp]: 
   738     "(l1,l2):r ==> (LCons x l1, LCons x l2) \<in> llistD_Fun(r)"
   739 apply (simp add: llistD_Fun_def LCons_def)
   740 apply (rule rangeI [THEN LListD_Fun_CONS_I, THEN prod_fun_imageI])
   741 apply (erule prod_fun_imageI)
   742 done
   743 
   744 text{*Utilise the "strong" part, i.e. @{text "gfp(f)"}*}
   745 lemma llistD_Fun_range_I: "(l,l) \<in> llistD_Fun(r Un range(%x.(x,x)))"
   746 apply (simp add: llistD_Fun_def)
   747 apply (rule Rep_LList_inverse [THEN subst])
   748 apply (rule prod_fun_imageI)
   749 apply (subst image_Un)
   750 apply (subst prod_fun_range_eq_diag)
   751 apply (rule Rep_LList [THEN LListD, THEN LListD_Fun_diag_I])
   752 done
   753 
   754 text{*A special case of @{text list_equality} for functions over lazy lists*}
   755 lemma llist_fun_equalityI:
   756      "[| f(LNil)=g(LNil);                                                 
   757          !!x l. (f(LCons x l),g(LCons x l)) 
   758                 \<in> llistD_Fun(range(%u. (f(u),g(u))) Un range(%v. (v,v)))    
   759       |] ==> f(l) = (g(l :: 'a llist) :: 'b llist)"
   760 apply (rule_tac r = "range (%u. (f (u),g (u)))" in llist_equalityI)
   761 apply (rule rangeI, clarify) 
   762 apply (rule_tac l = u in llistE)
   763 apply (simp_all add: llistD_Fun_range_I) 
   764 done
   765 
   766 
   767 subsection{* The functional @{text lmap} *}
   768 
   769 lemma lmap_LNil [simp]: "lmap f LNil = LNil"
   770 by (rule lmap_def [THEN def_llist_corec, THEN trans], simp)
   771 
   772 lemma lmap_LCons [simp]: "lmap f (LCons M N) = LCons (f M) (lmap f N)"
   773 by (rule lmap_def [THEN def_llist_corec, THEN trans], simp)
   774 
   775 
   776 subsubsection{* Two easy results about @{text lmap} *}
   777 
   778 lemma lmap_compose [simp]: "lmap (f o g) l = lmap f (lmap g l)"
   779 by (rule_tac l = l in llist_fun_equalityI, simp_all)
   780 
   781 lemma lmap_ident [simp]: "lmap (%x. x) l = l"
   782 by (rule_tac l = l in llist_fun_equalityI, simp_all)
   783 
   784 
   785 subsection{* iterates -- @{text llist_fun_equalityI} cannot be used! *}
   786 
   787 lemma iterates: "iterates f x = LCons x (iterates f (f x))"
   788 by (rule iterates_def [THEN def_llist_corec, THEN trans], simp)
   789 
   790 lemma lmap_iterates [simp]: "lmap f (iterates f x) = iterates f (f x)"
   791 apply (rule_tac r = "range (%u. (lmap f (iterates f u),iterates f (f u)))" in llist_equalityI)
   792 apply (rule rangeI, safe)
   793 apply (rule_tac x1 = "f (u)" in iterates [THEN ssubst])
   794 apply (rule_tac x1 = u in iterates [THEN ssubst], simp)
   795 done
   796 
   797 lemma iterates_lmap: "iterates f x = LCons x (lmap f (iterates f x))"
   798 apply (subst lmap_iterates)
   799 apply (rule iterates)
   800 done
   801 
   802 subsection{* A rather complex proof about iterates -- cf Andy Pitts *}
   803 
   804 subsubsection{* Two lemmas about @{text "natrec n x (%m. g)"}, which is essentially
   805   @{text "(g^n)(x)"} *}
   806 
   807 lemma fun_power_lmap: "nat_rec (LCons b l) (%m. lmap(f)) n =       
   808      LCons (nat_rec b (%m. f) n) (nat_rec l (%m. lmap(f)) n)"
   809 by (induct_tac "n", simp_all)
   810 
   811 lemma fun_power_Suc: "nat_rec (g x) (%m. g) n = nat_rec x (%m. g) (Suc n)"
   812 by (induct_tac "n", simp_all)
   813 
   814 lemmas Pair_cong = refl [THEN cong, THEN cong, of concl: Pair]
   815 
   816 
   817 text{*The bisimulation consists of @{text "{(lmap(f)^n (h(u)), lmap(f)^n (iterates(f,u)))}"}
   818   for all @{text u} and all @{text "n::nat"}.*}
   819 lemma iterates_equality:
   820      "(!!x. h(x) = LCons x (lmap f (h x))) ==> h = iterates(f)"
   821 apply (rule ext)
   822 apply (rule_tac 
   823        r = "\<Union>u. range (%n. (nat_rec (h u) (%m y. lmap f y) n, 
   824                              nat_rec (iterates f u) (%m y. lmap f y) n))" 
   825        in llist_equalityI)
   826 apply (rule UN1_I range_eqI Pair_cong nat_rec_0 [symmetric])+
   827 apply clarify
   828 apply (subst iterates, atomize)
   829 apply (drule_tac x=u in spec) 
   830 apply (erule ssubst) 
   831 apply (subst fun_power_lmap)
   832 apply (subst fun_power_lmap)
   833 apply (rule llistD_Fun_LCons_I)
   834 apply (rule lmap_iterates [THEN subst])
   835 apply (subst fun_power_Suc)
   836 apply (subst fun_power_Suc, blast)
   837 done
   838 
   839 
   840 subsection{* @{text lappend} -- its two arguments cause some complications! *}
   841 
   842 lemma lappend_LNil_LNil [simp]: "lappend LNil LNil = LNil"
   843 apply (simp add: lappend_def)
   844 apply (rule llist_corec [THEN trans], simp)
   845 done
   846 
   847 lemma lappend_LNil_LCons [simp]: 
   848     "lappend LNil (LCons l l') = LCons l (lappend LNil l')"
   849 apply (simp add: lappend_def)
   850 apply (rule llist_corec [THEN trans], simp)
   851 done
   852 
   853 lemma lappend_LCons [simp]: 
   854     "lappend (LCons l l') N = LCons l (lappend l' N)"
   855 apply (simp add: lappend_def)
   856 apply (rule llist_corec [THEN trans], simp)
   857 done
   858 
   859 lemma lappend_LNil [simp]: "lappend LNil l = l"
   860 by (rule_tac l = l in llist_fun_equalityI, simp_all)
   861 
   862 lemma lappend_LNil2 [simp]: "lappend l LNil = l"
   863 by (rule_tac l = l in llist_fun_equalityI, simp_all)
   864 
   865 
   866 text{*The infinite first argument blocks the second*}
   867 lemma lappend_iterates [simp]: "lappend (iterates f x) N = iterates f x"
   868 apply (rule_tac r = "range (%u. (lappend (iterates f u) N,iterates f u))" 
   869        in llist_equalityI)
   870  apply (rule rangeI, safe)
   871 apply (subst (1 2) iterates)
   872 apply simp 
   873 done
   874 
   875 subsubsection{* Two proofs that @{text lmap} distributes over lappend *}
   876 
   877 text{*Long proof requiring case analysis on both both arguments*}
   878 lemma lmap_lappend_distrib:
   879      "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)"
   880 apply (rule_tac r = "\<Union>n. range (%l. (lmap f (lappend l n),
   881                                       lappend (lmap f l) (lmap f n)))" 
   882        in llist_equalityI)
   883 apply (rule UN1_I)
   884 apply (rule rangeI, safe)
   885 apply (rule_tac l = l in llistE)
   886 apply (rule_tac l = n in llistE, simp_all)
   887 apply (blast intro: llistD_Fun_LCons_I) 
   888 done
   889 
   890 text{*Shorter proof of theorem above using @{text llist_equalityI} as strong coinduction*}
   891 lemma lmap_lappend_distrib':
   892      "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)"
   893 by (rule_tac l = l in llist_fun_equalityI, auto)
   894 
   895 text{*Without strong coinduction, three case analyses might be needed*}
   896 lemma lappend_assoc': "lappend (lappend l1 l2) l3 = lappend l1 (lappend l2 l3)"
   897 by (rule_tac l = l1 in llist_fun_equalityI, auto)
   898 
   899 end