author  haftmann 
Fri, 17 Jun 2005 16:12:49 +0200  
changeset 16417  9bc16273c2d4 
parent 13612  55d32e76ef4e 
child 19736  d8d0f8f51d69 
permissions  rwrr 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

1 
(* Title: HOL/LList.thy 
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 
Copyright 1997 University of Cambridge 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

5 
*) 
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:
9101
diff
changeset

7 
header {*The "filter" functional for coinductive lists 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

8 
defined by a combination of induction and coinduction*} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

9 

16417  10 
theory LFilter imports LList begin 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

11 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

12 
consts 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

13 
findRel :: "('a => bool) => ('a llist * 'a llist)set" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

14 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

15 
inductive "findRel p" 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

16 
intros 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

17 
found: "p x ==> (LCons x l, LCons x l) \<in> findRel p" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

18 
seek: "[ ~p x; (l,l') \<in> findRel p ] ==> (LCons x l, l') \<in> findRel p" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

19 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

20 
declare findRel.intros [intro] 
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 
constdefs 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

23 
find :: "['a => bool, 'a llist] => 'a llist" 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

24 
"find p l == @l'. (l,l'): findRel p  (l' = LNil & l ~: Domain(findRel p))" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

25 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

26 
lfilter :: "['a => bool, 'a llist] => 'a llist" 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

27 
"lfilter p l == llist_corec l (%l. case find p l of 
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
3120
diff
changeset

28 
LNil => None 
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
3120
diff
changeset

29 
 LCons y z => Some(y,z))" 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

30 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

31 

13107  32 
subsection {* @{text findRel}: basic laws *} 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

33 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

34 
inductive_cases 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

35 
findRel_LConsE [elim!]: "(LCons x l, l'') \<in> findRel p" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

36 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

37 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

38 
lemma findRel_functional [rule_format]: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

39 
"(l,l'): findRel p ==> (l,l''): findRel p > l'' = l'" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

40 
by (erule findRel.induct, auto) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

41 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

42 
lemma findRel_imp_LCons [rule_format]: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

43 
"(l,l'): findRel p ==> \<exists>x l''. l' = LCons x l'' & p x" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

44 
by (erule findRel.induct, auto) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

45 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

46 
lemma findRel_LNil [elim!]: "(LNil,l): findRel p ==> R" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

47 
by (blast elim: findRel.cases) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

48 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

49 

13107  50 
subsection {* Properties of @{text "Domain (findRel p)"} *} 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

51 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

52 
lemma LCons_Domain_findRel [simp]: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

53 
"LCons x l \<in> Domain(findRel p) = (p x  l \<in> Domain(findRel p))" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

54 
by auto 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

55 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

56 
lemma Domain_findRel_iff: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

57 
"(l \<in> Domain (findRel p)) = (\<exists>x l'. (l, LCons x l') \<in> findRel p & p x)" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

58 
by (blast dest: findRel_imp_LCons) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

59 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

60 
lemma Domain_findRel_mono: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

61 
"[ !!x. p x ==> q x ] ==> Domain (findRel p) <= Domain (findRel q)" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

62 
apply clarify 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

63 
apply (erule findRel.induct, blast+) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

64 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

65 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

66 

13107  67 
subsection {* @{text find}: basic equations *} 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

68 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

69 
lemma find_LNil [simp]: "find p LNil = LNil" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

70 
by (unfold find_def, blast) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

71 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

72 
lemma findRel_imp_find [simp]: "(l,l') \<in> findRel p ==> find p l = l'" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

73 
apply (unfold find_def) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

74 
apply (blast dest: findRel_functional) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

75 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

76 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

77 
lemma find_LCons_found: "p x ==> find p (LCons x l) = LCons x l" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

78 
by (blast intro: findRel_imp_find) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

79 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

80 
lemma diverge_find_LNil [simp]: "l ~: Domain(findRel p) ==> find p l = LNil" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

81 
by (unfold find_def, blast) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

82 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

83 
lemma find_LCons_seek: "~ (p x) ==> find p (LCons x l) = find p l" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

84 
apply (case_tac "LCons x l \<in> Domain (findRel p) ") 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

85 
apply auto 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

86 
apply (blast intro: findRel_imp_find) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

87 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

88 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

89 
lemma find_LCons [simp]: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

90 
"find p (LCons x l) = (if p x then LCons x l else find p l)" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

91 
by (simp add: find_LCons_seek find_LCons_found) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

92 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

93 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

94 

13107  95 
subsection {* @{text lfilter}: basic equations *} 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

96 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

97 
lemma lfilter_LNil [simp]: "lfilter p LNil = LNil" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

98 
by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

99 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

100 
lemma diverge_lfilter_LNil [simp]: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

101 
"l ~: Domain(findRel p) ==> lfilter p l = LNil" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

102 
by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

103 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

104 
lemma lfilter_LCons_found: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

105 
"p x ==> lfilter p (LCons x l) = LCons x (lfilter p l)" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

106 
by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

107 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

108 
lemma findRel_imp_lfilter [simp]: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

109 
"(l, LCons x l') \<in> findRel p ==> lfilter p l = LCons x (lfilter p l')" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

110 
by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

111 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

112 
lemma lfilter_LCons_seek: "~ (p x) ==> lfilter p (LCons x l) = lfilter p l" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

113 
apply (rule lfilter_def [THEN def_llist_corec, THEN trans], simp) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

114 
apply (case_tac "LCons x l \<in> Domain (findRel p) ") 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

115 
apply (simp add: Domain_findRel_iff, auto) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

116 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

117 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

118 
lemma lfilter_LCons [simp]: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

119 
"lfilter p (LCons x l) = 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

120 
(if p x then LCons x (lfilter p l) else lfilter p l)" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

121 
by (simp add: lfilter_LCons_found lfilter_LCons_seek) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

122 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

123 
declare llistD_Fun_LNil_I [intro!] llistD_Fun_LCons_I [intro!] 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

124 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

125 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

126 
lemma lfilter_eq_LNil: "lfilter p l = LNil ==> l ~: Domain(findRel p)" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

127 
apply (auto iff: Domain_findRel_iff) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

128 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

129 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

130 
lemma lfilter_eq_LCons [rule_format]: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

131 
"lfilter p l = LCons x l' > 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

132 
(\<exists>l''. l' = lfilter p l'' & (l, LCons x l'') \<in> findRel p)" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

133 
apply (subst lfilter_def [THEN def_llist_corec]) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

134 
apply (case_tac "l \<in> Domain (findRel p) ") 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

135 
apply (auto iff: Domain_findRel_iff) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

136 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

137 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

138 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

139 
lemma lfilter_cases: "lfilter p l = LNil  
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

140 
(\<exists>y l'. lfilter p l = LCons y (lfilter p l') & p y)" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

141 
apply (case_tac "l \<in> Domain (findRel p) ") 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

142 
apply (auto iff: Domain_findRel_iff) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

143 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

144 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

145 

13107  146 
subsection {* @{text lfilter}: simple facts by coinduction *} 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

147 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

148 
lemma lfilter_K_True: "lfilter (%x. True) l = l" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

149 
by (rule_tac l = "l" in llist_fun_equalityI, simp_all) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

150 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

151 
lemma lfilter_idem: "lfilter p (lfilter p l) = lfilter p l" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

152 
apply (rule_tac l = "l" in llist_fun_equalityI, simp_all) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

153 
apply safe 
13107  154 
txt{*Cases: @{text "p x"} is true or false*} 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

155 
apply (rule lfilter_cases [THEN disjE]) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

156 
apply (erule ssubst, auto) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

157 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

158 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

159 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

160 
subsection {* Numerous lemmas required to prove @{text lfilter_conj} *} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

161 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

162 
lemma findRel_conj_lemma [rule_format]: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

163 
"(l,l') \<in> findRel q 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

164 
==> l' = LCons x l'' > p x > (l,l') \<in> findRel (%x. p x & q x)" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

165 
by (erule findRel.induct, auto) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

166 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

167 
lemmas findRel_conj = findRel_conj_lemma [OF _ refl] 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

168 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

169 
lemma findRel_not_conj_Domain [rule_format]: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

170 
"(l,l'') \<in> findRel (%x. p x & q x) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

171 
==> (l, LCons x l') \<in> findRel q > ~ p x > 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

172 
l' \<in> Domain (findRel (%x. p x & q x))" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

173 
by (erule findRel.induct, auto) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

174 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

175 
lemma findRel_conj2 [rule_format]: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

176 
"(l,lxx) \<in> findRel q 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

177 
==> lxx = LCons x lx > (lx,lz) \<in> findRel(%x. p x & q x) > ~ p x 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

178 
> (l,lz) \<in> findRel (%x. p x & q x)" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

179 
by (erule findRel.induct, auto) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

180 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

181 
lemma findRel_lfilter_Domain_conj [rule_format]: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

182 
"(lx,ly) \<in> findRel p 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

183 
==> \<forall>l. lx = lfilter q l > l \<in> Domain (findRel(%x. p x & q x))" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

184 
apply (erule findRel.induct) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

185 
apply (blast dest!: sym [THEN lfilter_eq_LCons] intro: findRel_conj, auto) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

186 
apply (drule sym [THEN lfilter_eq_LCons], auto) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

187 
apply (drule spec) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

188 
apply (drule refl [THEN rev_mp]) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

189 
apply (blast intro: findRel_conj2) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

190 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

191 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

192 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

193 
lemma findRel_conj_lfilter [rule_format]: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

194 
"(l,l'') \<in> findRel(%x. p x & q x) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

195 
==> l'' = LCons y l' > 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

196 
(lfilter q l, LCons y (lfilter q l')) \<in> findRel p" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

197 
by (erule findRel.induct, auto) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

198 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

199 
lemma lfilter_conj_lemma: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

200 
"(lfilter p (lfilter q l), lfilter (%x. p x & q x) l) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

201 
\<in> llistD_Fun (range (%u. (lfilter p (lfilter q u), 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

202 
lfilter (%x. p x & q x) u)))" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

203 
apply (case_tac "l \<in> Domain (findRel q)") 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

204 
apply (subgoal_tac [2] "l ~: Domain (findRel (%x. p x & q x))") 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

205 
prefer 3 apply (blast intro: rev_subsetD [OF _ Domain_findRel_mono]) 
13107  206 
txt{*There are no @{text qs} in @{text l}: both lists are @{text LNil}*} 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

207 
apply (simp_all add: Domain_findRel_iff, clarify) 
13107  208 
txt{*case @{text "q x"}*} 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

209 
apply (case_tac "p x") 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

210 
apply (simp_all add: findRel_conj [THEN findRel_imp_lfilter]) 
13107  211 
txt{*case @{text "q x"} and @{text "~(p x)"} *} 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

212 
apply (case_tac "l' \<in> Domain (findRel (%x. p x & q x))") 
13107  213 
txt{*subcase: there is no @{text "p & q"} in @{text l'} and therefore none in @{text l}*} 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

214 
apply (subgoal_tac [2] "l ~: Domain (findRel (%x. p x & q x))") 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

215 
prefer 3 apply (blast intro: findRel_not_conj_Domain) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

216 
apply (subgoal_tac [2] "lfilter q l' ~: Domain (findRel p) ") 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

217 
prefer 3 apply (blast intro: findRel_lfilter_Domain_conj) 
13107  218 
txt{* {\dots} and therefore too, no @{text p} in @{text "lfilter q l'"}. 
219 
Both results are @{text LNil}*} 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

220 
apply (simp_all add: Domain_findRel_iff, clarify) 
13107  221 
txt{*subcase: there is a @{text "p & q"} in @{text l'} and therefore also one in @{text l} *} 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

222 
apply (subgoal_tac " (l, LCons xa l'a) \<in> findRel (%x. p x & q x) ") 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

223 
prefer 2 apply (blast intro: findRel_conj2) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

224 
apply (subgoal_tac " (lfilter q l', LCons xa (lfilter q l'a)) \<in> findRel p") 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

225 
apply simp 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

226 
apply (blast intro: findRel_conj_lfilter) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

227 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

228 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

229 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

230 
lemma lfilter_conj: "lfilter p (lfilter q l) = lfilter (%x. p x & q x) l" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

231 
apply (rule_tac l = "l" in llist_fun_equalityI, simp_all) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

232 
apply (blast intro: lfilter_conj_lemma rev_subsetD [OF _ llistD_Fun_mono]) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

233 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

234 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

235 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

236 
subsection {* Numerous lemmas required to prove ??: 
13107  237 
@{text "lfilter p (lmap f l) = lmap f (lfilter (%x. p(f x)) l)"} 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

238 
*} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

239 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

240 
lemma findRel_lmap_Domain: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

241 
"(l,l') \<in> findRel(%x. p (f x)) ==> lmap f l \<in> Domain(findRel p)" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

242 
by (erule findRel.induct, auto) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

243 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

244 
lemma lmap_eq_LCons [rule_format]: "lmap f l = LCons x l' > 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

245 
(\<exists>y l''. x = f y & l' = lmap f l'' & l = LCons y l'')" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

246 
apply (subst lmap_def [THEN def_llist_corec]) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

247 
apply (rule_tac l = "l" in llistE, auto) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

248 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

249 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

250 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

251 
lemma lmap_LCons_findRel_lemma [rule_format]: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

252 
"(lx,ly) \<in> findRel p 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

253 
==> \<forall>l. lmap f l = lx > ly = LCons x l' > 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

254 
(\<exists>y l''. x = f y & l' = lmap f l'' & 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

255 
(l, LCons y l'') \<in> findRel(%x. p(f x)))" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

256 
apply (erule findRel.induct, simp_all) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

257 
apply (blast dest!: lmap_eq_LCons)+ 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

258 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

259 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

260 
lemmas lmap_LCons_findRel = lmap_LCons_findRel_lemma [OF _ refl refl] 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

261 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

262 
lemma lfilter_lmap: "lfilter p (lmap f l) = lmap f (lfilter (p o f) l)" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

263 
apply (rule_tac l = "l" in llist_fun_equalityI, simp_all) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

264 
apply safe 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

265 
apply (case_tac "lmap f l \<in> Domain (findRel p)") 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

266 
apply (simp add: Domain_findRel_iff, clarify) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

267 
apply (frule lmap_LCons_findRel, force) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

268 
apply (subgoal_tac "l ~: Domain (findRel (%x. p (f x)))", simp) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

269 
apply (blast intro: findRel_lmap_Domain) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

270 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
9101
diff
changeset

271 

3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

272 
end 