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