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