author  haftmann 
Fri, 17 Jun 2005 16:12:49 +0200  
changeset 16417  9bc16273c2d4 
parent 15944  9b00875e21f7 
child 17841  b1f10b98430d 
permissions  rwrr 
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  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  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  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  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  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  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  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  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  102 
subsubsection{* Sample function definitions. Itembased 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  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  158 
subsection{* Type checking by coinduction *} 
159 

160 
text {* 

161 
{\dots} using @{text list_Fun} THE COINDUCTIVE DEFINITION PACKAGE 

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  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  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  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  237 
text{*A typical use of coinduction to show membership in the @{text gfp}. 
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  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  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  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  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  285 
subsubsection{* Coinduction, using @{text LListD_Fun} *} 
286 

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  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  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  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  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  355 
text{*We must remove @{text Pair_eq} because it may turn an instance of reflexivity 
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  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  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 coinduction to show membership in the gfp. 
13107  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  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  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  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  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  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 typechecking 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  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  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  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  596 
subsubsection{* Alternative typechecking 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 coinduction: 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 coinduction: bisimulation and case analysis on one variable*} 
13524  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  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  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  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  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  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  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  676 
"r <= (llist A) <*> (llist A) 
677 
==> LListD_Fun (diag A) r <= (llist A) <*> (llist A)" 

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  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  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  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  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  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  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  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  799 
subsubsection{* Two lemmas about @{text "natrec n x (%m. g)"}, which is essentially 
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  813 
text{*The bisimulation consists of @{text "{(lmap(f)^n (h(u)), lmap(f)^n (iterates(f,u)))}"} 
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  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  866 
apply (rule rangeI) 
867 
apply (safe) 

15944  868 
apply (subst (1 2) iterates) 
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  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  887 
text{*Shorter proof of theorem above using @{text llist_equalityI} as strong coinduction*} 
13524  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  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 