equal
deleted
inserted
replaced
1 (* Title: HOL/Induct/LList.thy |
1 (* Title: HOL/Induct/LList.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1994 University of Cambridge |
|
5 |
4 |
6 Shares NIL, CONS, List_case with List.thy |
5 Shares NIL, CONS, List_case with List.thy |
7 |
6 |
8 Still needs flatten function -- hard because it need |
7 Still needs flatten function -- hard because it need |
9 bounds on the amount of lookahead required. |
8 bounds on the amount of lookahead required. |
443 |
442 |
444 |
443 |
445 subsection{* Isomorphisms *} |
444 subsection{* Isomorphisms *} |
446 |
445 |
447 lemma inj_Rep_LList: "inj Rep_LList" |
446 lemma inj_Rep_LList: "inj Rep_LList" |
448 apply (rule inj_inverseI) |
447 apply (rule inj_on_inverseI) |
449 apply (rule Rep_LList_inverse) |
448 apply (rule Rep_LList_inverse) |
450 done |
449 done |
451 |
450 |
452 |
451 |
453 lemma LListI: "x \<in> llist (range Leaf) ==> x \<in> LList" |
452 lemma LListI: "x \<in> llist (range Leaf) ==> x \<in> LList" |