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