author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46953  2b6e55924af3 
child 58860  fee7cfa69c50 
permissions  rwrr 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26056
diff
changeset

1 
(* Title: ZF/List_ZF.thy 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

3 
Copyright 1994 University of Cambridge 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

4 
*) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

5 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

6 
header{*Lists in ZermeloFraenkel Set Theory*} 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

7 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

8 
theory List_ZF imports Datatype_ZF ArithSimp begin 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

9 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

10 
consts 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

11 
list :: "i=>i" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

12 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

13 
datatype 
46953  14 
"list(A)" = Nil  Cons ("a \<in> A", "l \<in> list(A)") 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

15 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

16 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

17 
syntax 
35425  18 
"_Nil" :: i ("[]") 
19 
"_List" :: "is => i" ("[(_)]") 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

20 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

21 
translations 
35068  22 
"[x, xs]" == "CONST Cons(x, [xs])" 
23 
"[x]" == "CONST Cons(x, [])" 

24 
"[]" == "CONST Nil" 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

25 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

26 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

27 
consts 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

28 
length :: "i=>i" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

29 
hd :: "i=>i" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

30 
tl :: "i=>i" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

31 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

32 
primrec 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

33 
"length([]) = 0" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

34 
"length(Cons(a,l)) = succ(length(l))" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

35 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

36 
primrec 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

37 
"hd([]) = 0" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

38 
"hd(Cons(a,l)) = a" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

39 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

40 
primrec 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

41 
"tl([]) = []" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

42 
"tl(Cons(a,l)) = l" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

43 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

44 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

45 
consts 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

46 
map :: "[i=>i, i] => i" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

47 
set_of_list :: "i=>i" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

48 
app :: "[i,i]=>i" (infixr "@" 60) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

49 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

50 
(*map is a binding operator  it applies to metalevel functions, not 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

51 
objectlevel functions. This simplifies the final form of term_rec_conv, 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

52 
although complicating its derivation.*) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

53 
primrec 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

54 
"map(f,[]) = []" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

55 
"map(f,Cons(a,l)) = Cons(f(a), map(f,l))" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

56 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

57 
primrec 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

58 
"set_of_list([]) = 0" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

59 
"set_of_list(Cons(a,l)) = cons(a, set_of_list(l))" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

60 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

61 
primrec 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

62 
app_Nil: "[] @ ys = ys" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

63 
app_Cons: "(Cons(a,l)) @ ys = Cons(a, l @ ys)" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

64 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

65 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

66 
consts 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

67 
rev :: "i=>i" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

68 
flat :: "i=>i" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

69 
list_add :: "i=>i" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

70 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

71 
primrec 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

72 
"rev([]) = []" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

73 
"rev(Cons(a,l)) = rev(l) @ [a]" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

74 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

75 
primrec 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

76 
"flat([]) = []" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

77 
"flat(Cons(l,ls)) = l @ flat(ls)" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

78 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

79 
primrec 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

80 
"list_add([]) = 0" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

81 
"list_add(Cons(a,l)) = a #+ list_add(l)" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

82 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

83 
consts 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

84 
drop :: "[i,i]=>i" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

85 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

86 
primrec 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

87 
drop_0: "drop(0,l) = l" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

88 
drop_succ: "drop(succ(i), l) = tl (drop(i,l))" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

89 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

90 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

91 
(*** Thanks to Sidi Ehmety for the following ***) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

92 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

93 
definition 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

94 
(* Function `take' returns the first n elements of a list *) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

95 
take :: "[i,i]=>i" where 
46820  96 
"take(n, as) == list_rec(\<lambda>n\<in>nat. [], 
97 
%a l r. \<lambda>n\<in>nat. nat_case([], %m. Cons(a, r`m), n), as)`n" 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

98 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

99 
definition 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

100 
nth :: "[i, i]=>i" where 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

101 
{*returns the (n+1)th element of a list, or 0 if the 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

102 
list is too short.*} 
46820  103 
"nth(n, as) == list_rec(\<lambda>n\<in>nat. 0, 
104 
%a l r. \<lambda>n\<in>nat. nat_case(a, %m. r`m, n), as) ` n" 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

105 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

106 
definition 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

107 
list_update :: "[i, i, i]=>i" where 
46820  108 
"list_update(xs, i, v) == list_rec(\<lambda>n\<in>nat. Nil, 
109 
%u us vs. \<lambda>n\<in>nat. nat_case(Cons(v, us), %m. Cons(u, vs`m), n), xs)`i" 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

110 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

111 
consts 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

112 
filter :: "[i=>o, i] => i" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

113 
upt :: "[i, i] =>i" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

114 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

115 
primrec 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

116 
"filter(P, Nil) = Nil" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

117 
"filter(P, Cons(x, xs)) = 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

118 
(if P(x) then Cons(x, filter(P, xs)) else filter(P, xs))" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

119 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

120 
primrec 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

121 
"upt(i, 0) = Nil" 
46820  122 
"upt(i, succ(j)) = (if i \<le> j then upt(i, j)@[j] else Nil)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

123 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

124 
definition 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

125 
min :: "[i,i] =>i" where 
46820  126 
"min(x, y) == (if x \<le> y then x else y)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

127 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

128 
definition 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

129 
max :: "[i, i] =>i" where 
46820  130 
"max(x, y) == (if x \<le> y then y else x)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

131 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

132 
(*** Aspects of the datatype definition ***) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

133 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

134 
declare list.intros [simp,TC] 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

135 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

136 
(*An elimination rule, for typechecking*) 
46820  137 
inductive_cases ConsE: "Cons(a,l) \<in> list(A)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

138 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

139 
lemma Cons_type_iff [simp]: "Cons(a,l) \<in> list(A) \<longleftrightarrow> a \<in> A & l \<in> list(A)" 
46820  140 
by (blast elim: ConsE) 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

141 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

142 
(*Proving freeness results*) 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

143 
lemma Cons_iff: "Cons(a,l)=Cons(a',l') \<longleftrightarrow> a=a' & l=l'" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

144 
by auto 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

145 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

146 
lemma Nil_Cons_iff: "~ Nil=Cons(a,l)" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

147 
by auto 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

148 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

149 
lemma list_unfold: "list(A) = {0} + (A * list(A))" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

150 
by (blast intro!: list.intros [unfolded list.con_defs] 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

151 
elim: list.cases [unfolded list.con_defs]) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

152 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

153 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

154 
(** Lemmas to justify using "list" in other recursive type definitions **) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

155 

46820  156 
lemma list_mono: "A<=B ==> list(A) \<subseteq> list(B)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

157 
apply (unfold list.defs ) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

158 
apply (rule lfp_mono) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

159 
apply (simp_all add: list.bnd_mono) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

160 
apply (assumption  rule univ_mono basic_monos)+ 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

161 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

162 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

163 
(*There is a similar proof by list induction.*) 
46820  164 
lemma list_univ: "list(univ(A)) \<subseteq> univ(A)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

165 
apply (unfold list.defs list.con_defs) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

166 
apply (rule lfp_lowerbound) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

167 
apply (rule_tac [2] A_subset_univ [THEN univ_mono]) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

168 
apply (blast intro!: zero_in_univ Inl_in_univ Inr_in_univ Pair_in_univ) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

169 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

170 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

171 
(*These two theorems justify datatypes involving list(nat), list(A), ...*) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

172 
lemmas list_subset_univ = subset_trans [OF list_mono list_univ] 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

173 

46953  174 
lemma list_into_univ: "[ l \<in> list(A); A \<subseteq> univ(B) ] ==> l \<in> univ(B)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

175 
by (blast intro: list_subset_univ [THEN subsetD]) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

176 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

177 
lemma list_case_type: 
46953  178 
"[ l \<in> list(A); 
179 
c \<in> C(Nil); 

180 
!!x y. [ x \<in> A; y \<in> list(A) ] ==> h(x,y): C(Cons(x,y)) 

46820  181 
] ==> list_case(c,h,l) \<in> C(l)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

182 
by (erule list.induct, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

183 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

184 
lemma list_0_triv: "list(0) = {Nil}" 
46820  185 
apply (rule equalityI, auto) 
186 
apply (induct_tac x, auto) 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

187 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

188 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

189 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

190 
(*** List functions ***) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

191 

46953  192 
lemma tl_type: "l \<in> list(A) ==> tl(l) \<in> list(A)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

193 
apply (induct_tac "l") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

194 
apply (simp_all (no_asm_simp) add: list.intros) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

195 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

196 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

197 
(** drop **) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

198 

46953  199 
lemma drop_Nil [simp]: "i \<in> nat ==> drop(i, Nil) = Nil" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

200 
apply (induct_tac "i") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

201 
apply (simp_all (no_asm_simp)) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

202 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

203 

46953  204 
lemma drop_succ_Cons [simp]: "i \<in> nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

205 
apply (rule sym) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

206 
apply (induct_tac "i") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

207 
apply (simp (no_asm)) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

208 
apply (simp (no_asm_simp)) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

209 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

210 

46953  211 
lemma drop_type [simp,TC]: "[ i \<in> nat; l \<in> list(A) ] ==> drop(i,l) \<in> list(A)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

212 
apply (induct_tac "i") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

213 
apply (simp_all (no_asm_simp) add: tl_type) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

214 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

215 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

216 
declare drop_succ [simp del] 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

217 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

218 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

219 
(** Type checking  proved by induction, as usual **) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

220 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

221 
lemma list_rec_type [TC]: 
46953  222 
"[ l \<in> list(A); 
223 
c \<in> C(Nil); 

224 
!!x y r. [ x \<in> A; y \<in> list(A); r \<in> C(y) ] ==> h(x,y,r): C(Cons(x,y)) 

46820  225 
] ==> list_rec(c,h,l) \<in> C(l)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

226 
by (induct_tac "l", auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

227 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

228 
(** map **) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

229 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

230 
lemma map_type [TC]: 
46953  231 
"[ l \<in> list(A); !!x. x \<in> A ==> h(x): B ] ==> map(h,l) \<in> list(B)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

232 
apply (simp add: map_list_def) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

233 
apply (typecheck add: list.intros list_rec_type, blast) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

234 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

235 

46953  236 
lemma map_type2 [TC]: "l \<in> list(A) ==> map(h,l) \<in> list({h(u). u \<in> A})" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

237 
apply (erule map_type) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

238 
apply (erule RepFunI) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

239 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

240 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

241 
(** length **) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

242 

46953  243 
lemma length_type [TC]: "l \<in> list(A) ==> length(l) \<in> nat" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

244 
by (simp add: length_list_def) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

245 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

246 
lemma lt_length_in_nat: 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

247 
"[x < length(xs); xs \<in> list(A)] ==> x \<in> nat" 
46820  248 
by (frule lt_nat_in_nat, typecheck) 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

249 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

250 
(** app **) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

251 

46820  252 
lemma app_type [TC]: "[ xs: list(A); ys: list(A) ] ==> xs@ys \<in> list(A)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

253 
by (simp add: app_list_def) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

254 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

255 
(** rev **) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

256 

46820  257 
lemma rev_type [TC]: "xs: list(A) ==> rev(xs) \<in> list(A)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

258 
by (simp add: rev_list_def) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

259 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

260 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

261 
(** flat **) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

262 

46820  263 
lemma flat_type [TC]: "ls: list(list(A)) ==> flat(ls) \<in> list(A)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

264 
by (simp add: flat_list_def) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

265 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

266 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

267 
(** set_of_list **) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

268 

46953  269 
lemma set_of_list_type [TC]: "l \<in> list(A) ==> set_of_list(l) \<in> Pow(A)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

270 
apply (unfold set_of_list_list_def) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

271 
apply (erule list_rec_type, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

272 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

273 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

274 
lemma set_of_list_append: 
46820  275 
"xs: list(A) ==> set_of_list (xs@ys) = set_of_list(xs) \<union> set_of_list(ys)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

276 
apply (erule list.induct) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

277 
apply (simp_all (no_asm_simp) add: Un_cons) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

278 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

279 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

280 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

281 
(** list_add **) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

282 

46820  283 
lemma list_add_type [TC]: "xs: list(nat) ==> list_add(xs) \<in> nat" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

284 
by (simp add: list_add_list_def) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

285 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

286 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

287 
(*** theorems about map ***) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

288 

46953  289 
lemma map_ident [simp]: "l \<in> list(A) ==> map(%u. u, l) = l" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

290 
apply (induct_tac "l") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

291 
apply (simp_all (no_asm_simp)) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

292 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

293 

46953  294 
lemma map_compose: "l \<in> list(A) ==> map(h, map(j,l)) = map(%u. h(j(u)), l)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

295 
apply (induct_tac "l") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

296 
apply (simp_all (no_asm_simp)) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

297 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

298 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

299 
lemma map_app_distrib: "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

300 
apply (induct_tac "xs") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

301 
apply (simp_all (no_asm_simp)) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

302 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

303 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

304 
lemma map_flat: "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

305 
apply (induct_tac "ls") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

306 
apply (simp_all (no_asm_simp) add: map_app_distrib) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

307 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

308 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

309 
lemma list_rec_map: 
46953  310 
"l \<in> list(A) ==> 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

311 
list_rec(c, d, map(h,l)) = 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

312 
list_rec(c, %x xs r. d(h(x), map(h,xs), r), l)" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

313 
apply (induct_tac "l") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

314 
apply (simp_all (no_asm_simp)) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

315 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

316 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

317 
(** theorems about list(Collect(A,P))  used in Induct/Term.thy **) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

318 

46820  319 
(* @{term"c \<in> list(Collect(B,P)) ==> c \<in> list"} *) 
45602  320 
lemmas list_CollectD = Collect_subset [THEN list_mono, THEN subsetD] 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

321 

46953  322 
lemma map_list_Collect: "l \<in> list({x \<in> A. h(x)=j(x)}) ==> map(h,l) = map(j,l)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

323 
apply (induct_tac "l") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

324 
apply (simp_all (no_asm_simp)) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

325 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

326 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

327 
(*** theorems about length ***) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

328 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

329 
lemma length_map [simp]: "xs: list(A) ==> length(map(h,xs)) = length(xs)" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

330 
by (induct_tac "xs", simp_all) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

331 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

332 
lemma length_app [simp]: 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

333 
"[ xs: list(A); ys: list(A) ] 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

334 
==> length(xs@ys) = length(xs) #+ length(ys)" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

335 
by (induct_tac "xs", simp_all) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

336 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

337 
lemma length_rev [simp]: "xs: list(A) ==> length(rev(xs)) = length(xs)" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

338 
apply (induct_tac "xs") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

339 
apply (simp_all (no_asm_simp) add: length_app) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

340 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

341 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

342 
lemma length_flat: 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

343 
"ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

344 
apply (induct_tac "ls") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

345 
apply (simp_all (no_asm_simp) add: length_app) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

346 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

347 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

348 
(** Length and drop **) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

349 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

350 
(*Lemma for the inductive step of drop_length*) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

351 
lemma drop_length_Cons [rule_format]: 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

352 
"xs: list(A) ==> 
46820  353 
\<forall>x. \<exists>z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

354 
by (erule list.induct, simp_all) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

355 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

356 
lemma drop_length [rule_format]: 
46953  357 
"l \<in> list(A) ==> \<forall>i \<in> length(l). (\<exists>z zs. drop(i,l) = Cons(z,zs))" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

358 
apply (erule list.induct, simp_all, safe) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

359 
apply (erule drop_length_Cons) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

360 
apply (rule natE) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

361 
apply (erule Ord_trans [OF asm_rl length_type Ord_nat], assumption, simp_all) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

362 
apply (blast intro: succ_in_naturalD length_type) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

363 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

364 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

365 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

366 
(*** theorems about app ***) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

367 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

368 
lemma app_right_Nil [simp]: "xs: list(A) ==> xs@Nil=xs" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

369 
by (erule list.induct, simp_all) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

370 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

371 
lemma app_assoc: "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

372 
by (induct_tac "xs", simp_all) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

373 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

374 
lemma flat_app_distrib: "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

375 
apply (induct_tac "ls") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

376 
apply (simp_all (no_asm_simp) add: app_assoc) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

377 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

378 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

379 
(*** theorems about rev ***) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

380 

46953  381 
lemma rev_map_distrib: "l \<in> list(A) ==> rev(map(h,l)) = map(h,rev(l))" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

382 
apply (induct_tac "l") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

383 
apply (simp_all (no_asm_simp) add: map_app_distrib) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

384 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

385 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

386 
(*Simplifier needs the premises as assumptions because rewriting will not 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

387 
instantiate the variable ?A in the rules' typing conditions; note that 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

388 
rev_type does not instantiate ?A. Only the premises do. 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

389 
*) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

390 
lemma rev_app_distrib: 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

391 
"[ xs: list(A); ys: list(A) ] ==> rev(xs@ys) = rev(ys)@rev(xs)" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

392 
apply (erule list.induct) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

393 
apply (simp_all add: app_assoc) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

394 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

395 

46953  396 
lemma rev_rev_ident [simp]: "l \<in> list(A) ==> rev(rev(l))=l" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

397 
apply (induct_tac "l") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

398 
apply (simp_all (no_asm_simp) add: rev_app_distrib) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

399 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

400 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

401 
lemma rev_flat: "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

402 
apply (induct_tac "ls") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

403 
apply (simp_all add: map_app_distrib flat_app_distrib rev_app_distrib) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

404 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

405 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

406 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

407 
(*** theorems about list_add ***) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

408 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

409 
lemma list_add_app: 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

410 
"[ xs: list(nat); ys: list(nat) ] 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

411 
==> list_add(xs@ys) = list_add(ys) #+ list_add(xs)" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

412 
apply (induct_tac "xs", simp_all) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

413 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

414 

46953  415 
lemma list_add_rev: "l \<in> list(nat) ==> list_add(rev(l)) = list_add(l)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

416 
apply (induct_tac "l") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

417 
apply (simp_all (no_asm_simp) add: list_add_app) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

418 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

419 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

420 
lemma list_add_flat: 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

421 
"ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

422 
apply (induct_tac "ls") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

423 
apply (simp_all (no_asm_simp) add: list_add_app) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

424 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

425 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

426 
(** New induction rules **) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

427 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

428 
lemma list_append_induct [case_names Nil snoc, consumes 1]: 
46953  429 
"[ l \<in> list(A); 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

430 
P(Nil); 
46953  431 
!!x y. [ x \<in> A; y \<in> list(A); P(y) ] ==> P(y @ [x]) 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

432 
] ==> P(l)" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

433 
apply (subgoal_tac "P(rev(rev(l)))", simp) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

434 
apply (erule rev_type [THEN list.induct], simp_all) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

435 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

436 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

437 
lemma list_complete_induct_lemma [rule_format]: 
46820  438 
assumes ih: 
439 
"\<And>l. [ l \<in> list(A); 

440 
\<forall>l' \<in> list(A). length(l') < length(l) \<longrightarrow> P(l')] 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

441 
==> P(l)" 
46820  442 
shows "n \<in> nat ==> \<forall>l \<in> list(A). length(l) < n \<longrightarrow> P(l)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

443 
apply (induct_tac n, simp) 
46820  444 
apply (blast intro: ih elim!: leE) 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

445 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

446 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

447 
theorem list_complete_induct: 
46820  448 
"[ l \<in> list(A); 
449 
\<And>l. [ l \<in> list(A); 

450 
\<forall>l' \<in> list(A). length(l') < length(l) \<longrightarrow> P(l')] 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

451 
==> P(l) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

452 
] ==> P(l)" 
46820  453 
apply (rule list_complete_induct_lemma [of A]) 
454 
prefer 4 apply (rule le_refl, simp) 

455 
apply blast 

456 
apply simp 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

457 
apply assumption 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

458 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

459 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

460 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

461 
(*** Thanks to Sidi Ehmety for these results about min, take, etc. ***) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

462 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

463 
(** min FIXME: replace by Int! **) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

464 
(* Min theorems are also true for i, j ordinals *) 
46953  465 
lemma min_sym: "[ i \<in> nat; j \<in> nat ] ==> min(i,j)=min(j,i)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

466 
apply (unfold min_def) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

467 
apply (auto dest!: not_lt_imp_le dest: lt_not_sym intro: le_anti_sym) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

468 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

469 

46953  470 
lemma min_type [simp,TC]: "[ i \<in> nat; j \<in> nat ] ==> min(i,j):nat" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

471 
by (unfold min_def, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

472 

46953  473 
lemma min_0 [simp]: "i \<in> nat ==> min(0,i) = 0" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

474 
apply (unfold min_def) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

475 
apply (auto dest: not_lt_imp_le) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

476 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

477 

46953  478 
lemma min_02 [simp]: "i \<in> nat ==> min(i, 0) = 0" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

479 
apply (unfold min_def) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

480 
apply (auto dest: not_lt_imp_le) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

481 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

482 

46953  483 
lemma lt_min_iff: "[ i \<in> nat; j \<in> nat; k \<in> nat ] ==> i<min(j,k) \<longleftrightarrow> i<j & i<k" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

484 
apply (unfold min_def) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

485 
apply (auto dest!: not_lt_imp_le intro: lt_trans2 lt_trans) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

486 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

487 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

488 
lemma min_succ_succ [simp]: 
46953  489 
"[ i \<in> nat; j \<in> nat ] ==> min(succ(i), succ(j))= succ(min(i, j))" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

490 
apply (unfold min_def, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

491 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

492 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

493 
(*** more theorems about lists ***) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

494 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

495 
(** filter **) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

496 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

497 
lemma filter_append [simp]: 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

498 
"xs:list(A) ==> filter(P, xs@ys) = filter(P, xs) @ filter(P, ys)" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

499 
by (induct_tac "xs", auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

500 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

501 
lemma filter_type [simp,TC]: "xs:list(A) ==> filter(P, xs):list(A)" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

502 
by (induct_tac "xs", auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

503 

46820  504 
lemma length_filter: "xs:list(A) ==> length(filter(P, xs)) \<le> length(xs)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

505 
apply (induct_tac "xs", auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

506 
apply (rule_tac j = "length (l) " in le_trans) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

507 
apply (auto simp add: le_iff) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

508 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

509 

46820  510 
lemma filter_is_subset: "xs:list(A) ==> set_of_list(filter(P,xs)) \<subseteq> set_of_list(xs)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

511 
by (induct_tac "xs", auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

512 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

513 
lemma filter_False [simp]: "xs:list(A) ==> filter(%p. False, xs) = Nil" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

514 
by (induct_tac "xs", auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

515 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

516 
lemma filter_True [simp]: "xs:list(A) ==> filter(%p. True, xs) = xs" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

517 
by (induct_tac "xs", auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

518 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

519 
(** length **) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

520 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

521 
lemma length_is_0_iff [simp]: "xs:list(A) ==> length(xs)=0 \<longleftrightarrow> xs=Nil" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

522 
by (erule list.induct, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

523 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

524 
lemma length_is_0_iff2 [simp]: "xs:list(A) ==> 0 = length(xs) \<longleftrightarrow> xs=Nil" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

525 
by (erule list.induct, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

526 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

527 
lemma length_tl [simp]: "xs:list(A) ==> length(tl(xs)) = length(xs) # 1" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

528 
by (erule list.induct, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

529 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

530 
lemma length_greater_0_iff: "xs:list(A) ==> 0<length(xs) \<longleftrightarrow> xs \<noteq> Nil" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

531 
by (erule list.induct, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

532 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

533 
lemma length_succ_iff: "xs:list(A) ==> length(xs)=succ(n) \<longleftrightarrow> (\<exists>y ys. xs=Cons(y, ys) & length(ys)=n)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

534 
by (erule list.induct, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

535 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

536 
(** more theorems about append **) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

537 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

538 
lemma append_is_Nil_iff [simp]: 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

539 
"xs:list(A) ==> (xs@ys = Nil) \<longleftrightarrow> (xs=Nil & ys = Nil)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

540 
by (erule list.induct, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

541 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

542 
lemma append_is_Nil_iff2 [simp]: 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

543 
"xs:list(A) ==> (Nil = xs@ys) \<longleftrightarrow> (xs=Nil & ys = Nil)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

544 
by (erule list.induct, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

545 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

546 
lemma append_left_is_self_iff [simp]: 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

547 
"xs:list(A) ==> (xs@ys = xs) \<longleftrightarrow> (ys = Nil)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

548 
by (erule list.induct, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

549 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

550 
lemma append_left_is_self_iff2 [simp]: 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

551 
"xs:list(A) ==> (xs = xs@ys) \<longleftrightarrow> (ys = Nil)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

552 
by (erule list.induct, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

553 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

554 
(*TOO SLOW as a default simprule!*) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

555 
lemma append_left_is_Nil_iff [rule_format]: 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

556 
"[ xs:list(A); ys:list(A); zs:list(A) ] ==> 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

557 
length(ys)=length(zs) \<longrightarrow> (xs@ys=zs \<longleftrightarrow> (xs=Nil & ys=zs))" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

558 
apply (erule list.induct) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

559 
apply (auto simp add: length_app) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

560 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

561 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

562 
(*TOO SLOW as a default simprule!*) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

563 
lemma append_left_is_Nil_iff2 [rule_format]: 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

564 
"[ xs:list(A); ys:list(A); zs:list(A) ] ==> 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

565 
length(ys)=length(zs) \<longrightarrow> (zs=ys@xs \<longleftrightarrow> (xs=Nil & ys=zs))" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

566 
apply (erule list.induct) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

567 
apply (auto simp add: length_app) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

568 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

569 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

570 
lemma append_eq_append_iff [rule_format,simp]: 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

571 
"xs:list(A) ==> \<forall>ys \<in> list(A). 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

572 
length(xs)=length(ys) \<longrightarrow> (xs@us = ys@vs) \<longleftrightarrow> (xs=ys & us=vs)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

573 
apply (erule list.induct) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

574 
apply (simp (no_asm_simp)) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

575 
apply clarify 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

576 
apply (erule_tac a = ys in list.cases, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

577 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

578 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

579 
lemma append_eq_append [rule_format]: 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

580 
"xs:list(A) ==> 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

581 
\<forall>ys \<in> list(A). \<forall>us \<in> list(A). \<forall>vs \<in> list(A). 
46820  582 
length(us) = length(vs) \<longrightarrow> (xs@us = ys@vs) \<longrightarrow> (xs=ys & us=vs)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

583 
apply (induct_tac "xs") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

584 
apply (force simp add: length_app, clarify) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

585 
apply (erule_tac a = ys in list.cases, simp) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

586 
apply (subgoal_tac "Cons (a, l) @ us =vs") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

587 
apply (drule rev_iffD1 [OF _ append_left_is_Nil_iff], simp_all, blast) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

588 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

589 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

590 
lemma append_eq_append_iff2 [simp]: 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

591 
"[ xs:list(A); ys:list(A); us:list(A); vs:list(A); length(us)=length(vs) ] 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

592 
==> xs@us = ys@vs \<longleftrightarrow> (xs=ys & us=vs)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

593 
apply (rule iffI) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

594 
apply (rule append_eq_append, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

595 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

596 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

597 
lemma append_self_iff [simp]: 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

598 
"[ xs:list(A); ys:list(A); zs:list(A) ] ==> xs@ys=xs@zs \<longleftrightarrow> ys=zs" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

599 
by simp 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

600 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

601 
lemma append_self_iff2 [simp]: 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

602 
"[ xs:list(A); ys:list(A); zs:list(A) ] ==> ys@xs=zs@xs \<longleftrightarrow> ys=zs" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

603 
by simp 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

604 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

605 
(* Can also be proved from append_eq_append_iff2, 
46953  606 
but the proof requires two more hypotheses: x \<in> A and y \<in> A *) 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

607 
lemma append1_eq_iff [rule_format,simp]: 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

608 
"xs:list(A) ==> \<forall>ys \<in> list(A). xs@[x] = ys@[y] \<longleftrightarrow> (xs = ys & x=y)" 
46820  609 
apply (erule list.induct) 
610 
apply clarify 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

611 
apply (erule list.cases) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

612 
apply simp_all 
46820  613 
txt{*Inductive step*} 
614 
apply clarify 

615 
apply (erule_tac a=ys in list.cases, simp_all) 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

616 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

617 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

618 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

619 
lemma append_right_is_self_iff [simp]: 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

620 
"[ xs:list(A); ys:list(A) ] ==> (xs@ys = ys) \<longleftrightarrow> (xs=Nil)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

621 
by (simp (no_asm_simp) add: append_left_is_Nil_iff) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

622 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

623 
lemma append_right_is_self_iff2 [simp]: 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

624 
"[ xs:list(A); ys:list(A) ] ==> (ys = xs@ys) \<longleftrightarrow> (xs=Nil)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

625 
apply (rule iffI) 
46820  626 
apply (drule sym, auto) 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

627 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

628 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

629 
lemma hd_append [rule_format,simp]: 
46820  630 
"xs:list(A) ==> xs \<noteq> Nil \<longrightarrow> hd(xs @ ys) = hd(xs)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

631 
by (induct_tac "xs", auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

632 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

633 
lemma tl_append [rule_format,simp]: 
46820  634 
"xs:list(A) ==> xs\<noteq>Nil \<longrightarrow> tl(xs @ ys) = tl(xs)@ys" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

635 
by (induct_tac "xs", auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

636 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

637 
(** rev **) 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

638 
lemma rev_is_Nil_iff [simp]: "xs:list(A) ==> (rev(xs) = Nil \<longleftrightarrow> xs = Nil)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

639 
by (erule list.induct, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

640 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

641 
lemma Nil_is_rev_iff [simp]: "xs:list(A) ==> (Nil = rev(xs) \<longleftrightarrow> xs = Nil)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

642 
by (erule list.induct, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

643 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

644 
lemma rev_is_rev_iff [rule_format,simp]: 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

645 
"xs:list(A) ==> \<forall>ys \<in> list(A). rev(xs)=rev(ys) \<longleftrightarrow> xs=ys" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

646 
apply (erule list.induct, force, clarify) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

647 
apply (erule_tac a = ys in list.cases, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

648 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

649 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

650 
lemma rev_list_elim [rule_format]: 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

651 
"xs:list(A) ==> 
46820  652 
(xs=Nil \<longrightarrow> P) \<longrightarrow> (\<forall>ys \<in> list(A). \<forall>y \<in> A. xs =ys@[y] \<longrightarrow>P)\<longrightarrow>P" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

653 
by (erule list_append_induct, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

654 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

655 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

656 
(** more theorems about drop **) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

657 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

658 
lemma length_drop [rule_format,simp]: 
46953  659 
"n \<in> nat ==> \<forall>xs \<in> list(A). length(drop(n, xs)) = length(xs) # n" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

660 
apply (erule nat_induct) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

661 
apply (auto elim: list.cases) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

662 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

663 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

664 
lemma drop_all [rule_format,simp]: 
46953  665 
"n \<in> nat ==> \<forall>xs \<in> list(A). length(xs) \<le> n \<longrightarrow> drop(n, xs)=Nil" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

666 
apply (erule nat_induct) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

667 
apply (auto elim: list.cases) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

668 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

669 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

670 
lemma drop_append [rule_format]: 
46953  671 
"n \<in> nat ==> 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

672 
\<forall>xs \<in> list(A). drop(n, xs@ys) = drop(n,xs) @ drop(n # length(xs), ys)" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

673 
apply (induct_tac "n") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

674 
apply (auto elim: list.cases) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

675 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

676 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

677 
lemma drop_drop: 
46953  678 
"m \<in> nat ==> \<forall>xs \<in> list(A). \<forall>n \<in> nat. drop(n, drop(m, xs))=drop(n #+ m, xs)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

679 
apply (induct_tac "m") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

680 
apply (auto elim: list.cases) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

681 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

682 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

683 
(** take **) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

684 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

685 
lemma take_0 [simp]: "xs:list(A) ==> take(0, xs) = Nil" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

686 
apply (unfold take_def) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

687 
apply (erule list.induct, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

688 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

689 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

690 
lemma take_succ_Cons [simp]: 
46953  691 
"n \<in> nat ==> take(succ(n), Cons(a, xs)) = Cons(a, take(n, xs))" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

692 
by (simp add: take_def) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

693 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

694 
(* Needed for proving take_all *) 
46953  695 
lemma take_Nil [simp]: "n \<in> nat ==> take(n, Nil) = Nil" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

696 
by (unfold take_def, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

697 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

698 
lemma take_all [rule_format,simp]: 
46953  699 
"n \<in> nat ==> \<forall>xs \<in> list(A). length(xs) \<le> n \<longrightarrow> take(n, xs) = xs" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

700 
apply (erule nat_induct) 
46820  701 
apply (auto elim: list.cases) 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

702 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

703 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

704 
lemma take_type [rule_format,simp,TC]: 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

705 
"xs:list(A) ==> \<forall>n \<in> nat. take(n, xs):list(A)" 
46820  706 
apply (erule list.induct, simp, clarify) 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

707 
apply (erule natE, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

708 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

709 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

710 
lemma take_append [rule_format,simp]: 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

711 
"xs:list(A) ==> 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

712 
\<forall>ys \<in> list(A). \<forall>n \<in> nat. take(n, xs @ ys) = 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

713 
take(n, xs) @ take(n # length(xs), ys)" 
46820  714 
apply (erule list.induct, simp, clarify) 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

715 
apply (erule natE, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

716 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

717 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

718 
lemma take_take [rule_format]: 
46820  719 
"m \<in> nat ==> 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

720 
\<forall>xs \<in> list(A). \<forall>n \<in> nat. take(n, take(m,xs))= take(min(n, m), xs)" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

721 
apply (induct_tac "m", auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

722 
apply (erule_tac a = xs in list.cases) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

723 
apply (auto simp add: take_Nil) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

724 
apply (erule_tac n=n in natE) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

725 
apply (auto intro: take_0 take_type) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

726 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

727 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

728 
(** nth **) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

729 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

730 
lemma nth_0 [simp]: "nth(0, Cons(a, l)) = a" 
46820  731 
by (simp add: nth_def) 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

732 

46953  733 
lemma nth_Cons [simp]: "n \<in> nat ==> nth(succ(n), Cons(a,l)) = nth(n,l)" 
46820  734 
by (simp add: nth_def) 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

735 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

736 
lemma nth_empty [simp]: "nth(n, Nil) = 0" 
46820  737 
by (simp add: nth_def) 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

738 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

739 
lemma nth_type [rule_format,simp,TC]: 
46820  740 
"xs:list(A) ==> \<forall>n. n < length(xs) \<longrightarrow> nth(n,xs) \<in> A" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

741 
apply (erule list.induct, simp, clarify) 
46820  742 
apply (subgoal_tac "n \<in> nat") 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

743 
apply (erule natE, auto dest!: le_in_nat) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

744 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

745 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

746 
lemma nth_eq_0 [rule_format]: 
46820  747 
"xs:list(A) ==> \<forall>n \<in> nat. length(xs) \<le> n \<longrightarrow> nth(n,xs) = 0" 
748 
apply (erule list.induct, simp, clarify) 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

749 
apply (erule natE, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

750 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

751 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

752 
lemma nth_append [rule_format]: 
46820  753 
"xs:list(A) ==> 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

754 
\<forall>n \<in> nat. nth(n, xs @ ys) = (if n < length(xs) then nth(n,xs) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

755 
else nth(n # length(xs), ys))" 
46820  756 
apply (induct_tac "xs", simp, clarify) 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

757 
apply (erule natE, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

758 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

759 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

760 
lemma set_of_list_conv_nth: 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

761 
"xs:list(A) 
46953  762 
==> set_of_list(xs) = {x \<in> A. \<exists>i\<in>nat. i<length(xs) & x = nth(i,xs)}" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

763 
apply (induct_tac "xs", simp_all) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

764 
apply (rule equalityI, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

765 
apply (rule_tac x = 0 in bexI, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

766 
apply (erule natE, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

767 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

768 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

769 
(* Other theorems about lists *) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

770 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

771 
lemma nth_take_lemma [rule_format]: 
46953  772 
"k \<in> nat ==> 
46820  773 
\<forall>xs \<in> list(A). (\<forall>ys \<in> list(A). k \<le> length(xs) \<longrightarrow> k \<le> length(ys) \<longrightarrow> 
774 
(\<forall>i \<in> nat. i<k \<longrightarrow> nth(i,xs) = nth(i,ys))\<longrightarrow> take(k,xs) = take(k,ys))" 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

775 
apply (induct_tac "k") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

776 
apply (simp_all (no_asm_simp) add: lt_succ_eq_0_disj all_conj_distrib) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

777 
apply clarify 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

778 
(*Both lists are nonempty*) 
46820  779 
apply (erule_tac a=xs in list.cases, simp) 
780 
apply (erule_tac a=ys in list.cases, clarify) 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

781 
apply (simp (no_asm_use) ) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

782 
apply clarify 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

783 
apply (simp (no_asm_simp)) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

784 
apply (rule conjI, force) 
46820  785 
apply (rename_tac y ys z zs) 
786 
apply (drule_tac x = zs and x1 = ys in bspec [THEN bspec], auto) 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

787 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

788 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

789 
lemma nth_equalityI [rule_format]: 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

790 
"[ xs:list(A); ys:list(A); length(xs) = length(ys); 
46820  791 
\<forall>i \<in> nat. i < length(xs) \<longrightarrow> nth(i,xs) = nth(i,ys) ] 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

792 
==> xs = ys" 
46820  793 
apply (subgoal_tac "length (xs) \<le> length (ys) ") 
794 
apply (cut_tac k="length(xs)" and xs=xs and ys=ys in nth_take_lemma) 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

795 
apply (simp_all add: take_all) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

796 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

797 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

798 
(*The famous takelemma*) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

799 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

800 
lemma take_equalityI [rule_format]: 
46820  801 
"[ xs:list(A); ys:list(A); (\<forall>i \<in> nat. take(i, xs) = take(i,ys)) ] 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

802 
==> xs = ys" 
46820  803 
apply (case_tac "length (xs) \<le> length (ys) ") 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

804 
apply (drule_tac x = "length (ys) " in bspec) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

805 
apply (drule_tac [3] not_lt_imp_le) 
46820  806 
apply (subgoal_tac [5] "length (ys) \<le> length (xs) ") 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

807 
apply (rule_tac [6] j = "succ (length (ys))" in le_trans) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

808 
apply (rule_tac [6] leI) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

809 
apply (drule_tac [5] x = "length (xs) " in bspec) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

810 
apply (simp_all add: take_all) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

811 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

812 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

813 
lemma nth_drop [rule_format]: 
46953  814 
"n \<in> nat ==> \<forall>i \<in> nat. \<forall>xs \<in> list(A). nth(i, drop(n, xs)) = nth(n #+ i, xs)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

815 
apply (induct_tac "n", simp_all, clarify) 
46820  816 
apply (erule list.cases, auto) 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

817 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

818 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

819 
lemma take_succ [rule_format]: 
46820  820 
"xs\<in>list(A) 
821 
==> \<forall>i. i < length(xs) \<longrightarrow> take(succ(i), xs) = take(i,xs) @ [nth(i, xs)]" 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

822 
apply (induct_tac "xs", auto) 
46820  823 
apply (subgoal_tac "i\<in>nat") 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

824 
apply (erule natE) 
46820  825 
apply (auto simp add: le_in_nat) 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

826 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

827 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

828 
lemma take_add [rule_format]: 
46820  829 
"[xs\<in>list(A); j\<in>nat] 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

830 
==> \<forall>i\<in>nat. take(i #+ j, xs) = take(i,xs) @ take(j, drop(i,xs))" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

831 
apply (induct_tac "xs", simp_all, clarify) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

832 
apply (erule_tac n = i in natE, simp_all) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

833 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

834 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

835 
lemma length_take: 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

836 
"l\<in>list(A) ==> \<forall>n\<in>nat. length(take(n,l)) = min(n, length(l))" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

837 
apply (induct_tac "l", safe, simp_all) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

838 
apply (erule natE, simp_all) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

839 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

840 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

841 
subsection{*The function zip*} 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

842 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

843 
text{*Crafty definition to eliminate a type argument*} 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

844 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

845 
consts 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

846 
zip_aux :: "[i,i]=>i" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

847 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

848 
primrec (*explicit lambda is required because both arguments of "un" vary*) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

849 
"zip_aux(B,[]) = 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

850 
(\<lambda>ys \<in> list(B). list_case([], %y l. [], ys))" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

851 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

852 
"zip_aux(B,Cons(x,l)) = 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

853 
(\<lambda>ys \<in> list(B). 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

854 
list_case(Nil, %y zs. Cons(<x,y>, zip_aux(B,l)`zs), ys))" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

855 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

856 
definition 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

857 
zip :: "[i, i]=>i" where 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

858 
"zip(xs, ys) == zip_aux(set_of_list(ys),xs)`ys" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

859 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

860 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

861 
(* zip equations *) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

862 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

863 
lemma list_on_set_of_list: "xs \<in> list(A) ==> xs \<in> list(set_of_list(xs))" 
46820  864 
apply (induct_tac xs, simp_all) 
865 
apply (blast intro: list_mono [THEN subsetD]) 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

866 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

867 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

868 
lemma zip_Nil [simp]: "ys:list(A) ==> zip(Nil, ys)=Nil" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

869 
apply (simp add: zip_def list_on_set_of_list [of _ A]) 
46820  870 
apply (erule list.cases, simp_all) 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

871 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

872 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

873 
lemma zip_Nil2 [simp]: "xs:list(A) ==> zip(xs, Nil)=Nil" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

874 
apply (simp add: zip_def list_on_set_of_list [of _ A]) 
46820  875 
apply (erule list.cases, simp_all) 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

876 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

877 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

878 
lemma zip_aux_unique [rule_format]: 
46820  879 
"[B<=C; xs \<in> list(A)] 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

880 
==> \<forall>ys \<in> list(B). zip_aux(C,xs) ` ys = zip_aux(B,xs) ` ys" 
46820  881 
apply (induct_tac xs) 
882 
apply simp_all 

883 
apply (blast intro: list_mono [THEN subsetD], clarify) 

884 
apply (erule_tac a=ys in list.cases, auto) 

885 
apply (blast intro: list_mono [THEN subsetD]) 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

886 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

887 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

888 
lemma zip_Cons_Cons [simp]: 
46953  889 
"[ xs:list(A); ys:list(B); x \<in> A; y \<in> B ] ==> 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

890 
zip(Cons(x,xs), Cons(y, ys)) = Cons(<x,y>, zip(xs, ys))" 
46820  891 
apply (simp add: zip_def, auto) 
892 
apply (rule zip_aux_unique, auto) 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

893 
apply (simp add: list_on_set_of_list [of _ B]) 
46820  894 
apply (blast intro: list_on_set_of_list list_mono [THEN subsetD]) 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

895 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

896 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

897 
lemma zip_type [rule_format,simp,TC]: 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

898 
"xs:list(A) ==> \<forall>ys \<in> list(B). zip(xs, ys):list(A*B)" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

899 
apply (induct_tac "xs") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

900 
apply (simp (no_asm)) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

901 
apply clarify 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

902 
apply (erule_tac a = ys in list.cases, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

903 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

904 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

905 
(* zip length *) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

906 
lemma length_zip [rule_format,simp]: 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

907 
"xs:list(A) ==> \<forall>ys \<in> list(B). length(zip(xs,ys)) = 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

908 
min(length(xs), length(ys))" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

909 
apply (unfold min_def) 
46820  910 
apply (induct_tac "xs", simp_all, clarify) 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

911 
apply (erule_tac a = ys in list.cases, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

912 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

913 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

914 
lemma zip_append1 [rule_format]: 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

915 
"[ ys:list(A); zs:list(B) ] ==> 
46820  916 
\<forall>xs \<in> list(A). zip(xs @ ys, zs) = 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

917 
zip(xs, take(length(xs), zs)) @ zip(ys, drop(length(xs),zs))" 
46820  918 
apply (induct_tac "zs", force, clarify) 
919 
apply (erule_tac a = xs in list.cases, simp_all) 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

920 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

921 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

922 
lemma zip_append2 [rule_format]: 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

923 
"[ xs:list(A); zs:list(B) ] ==> \<forall>ys \<in> list(B). zip(xs, ys@zs) = 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

924 
zip(take(length(ys), xs), ys) @ zip(drop(length(ys), xs), zs)" 
46820  925 
apply (induct_tac "xs", force, clarify) 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

926 
apply (erule_tac a = ys in list.cases, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

927 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

928 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

929 
lemma zip_append [simp]: 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

930 
"[ length(xs) = length(us); length(ys) = length(vs); 
46820  931 
xs:list(A); us:list(B); ys:list(A); vs:list(B) ] 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

932 
==> zip(xs@ys,us@vs) = zip(xs, us) @ zip(ys, vs)" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

933 
by (simp (no_asm_simp) add: zip_append1 drop_append diff_self_eq_0) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

934 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

935 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

936 
lemma zip_rev [rule_format,simp]: 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

937 
"ys:list(B) ==> \<forall>xs \<in> list(A). 
46820  938 
length(xs) = length(ys) \<longrightarrow> zip(rev(xs), rev(ys)) = rev(zip(xs, ys))" 
939 
apply (induct_tac "ys", force, clarify) 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

940 
apply (erule_tac a = xs in list.cases) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

941 
apply (auto simp add: length_rev) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

942 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

943 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

944 
lemma nth_zip [rule_format,simp]: 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

945 
"ys:list(B) ==> \<forall>i \<in> nat. \<forall>xs \<in> list(A). 
46820  946 
i < length(xs) \<longrightarrow> i < length(ys) \<longrightarrow> 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

947 
nth(i,zip(xs, ys)) = <nth(i,xs),nth(i, ys)>" 
46820  948 
apply (induct_tac "ys", force, clarify) 
949 
apply (erule_tac a = xs in list.cases, simp) 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

950 
apply (auto elim: natE) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

951 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

952 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

953 
lemma set_of_list_zip [rule_format]: 
46953  954 
"[ xs:list(A); ys:list(B); i \<in> nat ] 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

955 
==> set_of_list(zip(xs, ys)) = 
46820  956 
{<x, y>:A*B. \<exists>i\<in>nat. i < min(length(xs), length(ys)) 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

957 
& x = nth(i, xs) & y = nth(i, ys)}" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

958 
by (force intro!: Collect_cong simp add: lt_min_iff set_of_list_conv_nth) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

959 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

960 
(** list_update **) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

961 

46953  962 
lemma list_update_Nil [simp]: "i \<in> nat ==>list_update(Nil, i, v) = Nil" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

963 
by (unfold list_update_def, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

964 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

965 
lemma list_update_Cons_0 [simp]: "list_update(Cons(x, xs), 0, v)= Cons(v, xs)" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

966 
by (unfold list_update_def, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

967 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

968 
lemma list_update_Cons_succ [simp]: 
46953  969 
"n \<in> nat ==> 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

970 
list_update(Cons(x, xs), succ(n), v)= Cons(x, list_update(xs, n, v))" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

971 
apply (unfold list_update_def, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

972 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

973 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

974 
lemma list_update_type [rule_format,simp,TC]: 
46953  975 
"[ xs:list(A); v \<in> A ] ==> \<forall>n \<in> nat. list_update(xs, n, v):list(A)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

976 
apply (induct_tac "xs") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

977 
apply (simp (no_asm)) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

978 
apply clarify 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

979 
apply (erule natE, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

980 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

981 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

982 
lemma length_list_update [rule_format,simp]: 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

983 
"xs:list(A) ==> \<forall>i \<in> nat. length(list_update(xs, i, v))=length(xs)" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

984 
apply (induct_tac "xs") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

985 
apply (simp (no_asm)) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

986 
apply clarify 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

987 
apply (erule natE, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

988 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

989 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

990 
lemma nth_list_update [rule_format]: 
46820  991 
"[ xs:list(A) ] ==> \<forall>i \<in> nat. \<forall>j \<in> nat. i < length(xs) \<longrightarrow> 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

992 
nth(j, list_update(xs, i, x)) = (if i=j then x else nth(j, xs))" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

993 
apply (induct_tac "xs") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

994 
apply simp_all 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

995 
apply clarify 
46820  996 
apply (rename_tac i j) 
997 
apply (erule_tac n=i in natE) 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

998 
apply (erule_tac [2] n=j in natE) 
46820  999 
apply (erule_tac n=j in natE, simp_all, force) 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1000 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1001 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1002 
lemma nth_list_update_eq [simp]: 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1003 
"[ i < length(xs); xs:list(A) ] ==> nth(i, list_update(xs, i,x)) = x" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1004 
by (simp (no_asm_simp) add: lt_length_in_nat nth_list_update) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1005 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1006 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1007 
lemma nth_list_update_neq [rule_format,simp]: 
46820  1008 
"xs:list(A) ==> 
1009 
\<forall>i \<in> nat. \<forall>j \<in> nat. i \<noteq> j \<longrightarrow> nth(j, list_update(xs,i,x)) = nth(j,xs)" 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1010 
apply (induct_tac "xs") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1011 
apply (simp (no_asm)) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1012 
apply clarify 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1013 
apply (erule natE) 
46820  1014 
apply (erule_tac [2] natE, simp_all) 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1015 
apply (erule natE, simp_all) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1016 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1017 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1018 
lemma list_update_overwrite [rule_format,simp]: 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1019 
"xs:list(A) ==> \<forall>i \<in> nat. i < length(xs) 
46820  1020 
\<longrightarrow> list_update(list_update(xs, i, x), i, y) = list_update(xs, i,y)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1021 
apply (induct_tac "xs") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1022 
apply (simp (no_asm)) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1023 
apply clarify 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1024 
apply (erule natE, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1025 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1026 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1027 
lemma list_update_same_conv [rule_format]: 
46820  1028 
"xs:list(A) ==> 
1029 
\<forall>i \<in> nat. i < length(xs) \<longrightarrow> 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

1030 
(list_update(xs, i, x) = xs) \<longleftrightarrow> (nth(i, xs) = x)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1031 
apply (induct_tac "xs") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1032 
apply (simp (no_asm)) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1033 
apply clarify 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1034 
apply (erule natE, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1035 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1036 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1037 
lemma update_zip [rule_format]: 
46820  1038 
"ys:list(B) ==> 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1039 
\<forall>i \<in> nat. \<forall>xy \<in> A*B. \<forall>xs \<in> list(A). 
46820  1040 
length(xs) = length(ys) \<longrightarrow> 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1041 
list_update(zip(xs, ys), i, xy) = zip(list_update(xs, i, fst(xy)), 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1042 
list_update(ys, i, snd(xy)))" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1043 
apply (induct_tac "ys") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1044 
apply auto 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1045 
apply (erule_tac a = xs in list.cases) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1046 
apply (auto elim: natE) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1047 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1048 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1049 
lemma set_update_subset_cons [rule_format]: 
46820  1050 
"xs:list(A) ==> 
1051 
\<forall>i \<in> nat. set_of_list(list_update(xs, i, x)) \<subseteq> cons(x, set_of_list(xs))" 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1052 
apply (induct_tac "xs") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1053 
apply simp 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1054 
apply (rule ballI) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1055 
apply (erule natE, simp_all, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1056 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1057 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1058 
lemma set_of_list_update_subsetI: 
46953  1059 
"[ set_of_list(xs) \<subseteq> A; xs:list(A); x \<in> A; i \<in> nat] 
46820  1060 
==> set_of_list(list_update(xs, i,x)) \<subseteq> A" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1061 
apply (rule subset_trans) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1062 
apply (rule set_update_subset_cons, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1063 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1064 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1065 
(** upt **) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1066 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1067 
lemma upt_rec: 
46953  1068 
"j \<in> nat ==> upt(i,j) = (if i<j then Cons(i, upt(succ(i), j)) else Nil)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1069 
apply (induct_tac "j", auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1070 
apply (drule not_lt_imp_le) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1071 
apply (auto simp: lt_Ord intro: le_anti_sym) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1072 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1073 

46953  1074 
lemma upt_conv_Nil [simp]: "[ j \<le> i; j \<in> nat ] ==> upt(i,j) = Nil" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1075 
apply (subst upt_rec, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1076 
apply (auto simp add: le_iff) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1077 
apply (drule lt_asym [THEN notE], auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1078 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1079 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1080 
(*Only needed if upt_Suc is deleted from the simpset*) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1081 
lemma upt_succ_append: 
46953  1082 
"[ i \<le> j; j \<in> nat ] ==> upt(i,succ(j)) = upt(i, j)@[j]" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1083 
by simp 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1084 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1085 
lemma upt_conv_Cons: 
46953  1086 
"[ i<j; j \<in> nat ] ==> upt(i,j) = Cons(i,upt(succ(i),j))" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1087 
apply (rule trans) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1088 
apply (rule upt_rec, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1089 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1090 

46953  1091 
lemma upt_type [simp,TC]: "j \<in> nat ==> upt(i,j):list(nat)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1092 
by (induct_tac "j", auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1093 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1094 
(*LOOPS as a simprule, since j<=j*) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1095 
lemma upt_add_eq_append: 
46953  1096 
"[ i \<le> j; j \<in> nat; k \<in> nat ] ==> upt(i, j #+k) = upt(i,j)@upt(j,j#+k)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1097 
apply (induct_tac "k") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1098 
apply (auto simp add: app_assoc app_type) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1099 
apply (rule_tac j = j in le_trans, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1100 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1101 

46953  1102 
lemma length_upt [simp]: "[ i \<in> nat; j \<in> nat ] ==>length(upt(i,j)) = j # i" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1103 
apply (induct_tac "j") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1104 
apply (rule_tac [2] sym) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1105 
apply (auto dest!: not_lt_imp_le simp add: diff_succ diff_is_0_iff) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1106 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1107 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1108 
lemma nth_upt [rule_format,simp]: 
46953  1109 
"[ i \<in> nat; j \<in> nat; k \<in> nat ] ==> i #+ k < j \<longrightarrow> nth(k, upt(i,j)) = i #+ k" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1110 
apply (induct_tac "j", simp) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1111 
apply (simp add: nth_append le_iff) 
46820  1112 
apply (auto dest!: not_lt_imp_le 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1113 
simp add: nth_append less_diff_conv add_commute) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1114 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1115 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1116 
lemma take_upt [rule_format,simp]: 
46953  1117 
"[ m \<in> nat; n \<in> nat ] ==> 
46820  1118 
\<forall>i \<in> nat. i #+ m \<le> n \<longrightarrow> take(m, upt(i,n)) = upt(i,i#+m)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1119 
apply (induct_tac "m") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1120 
apply (simp (no_asm_simp) add: take_0) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1121 
apply clarify 
46820  1122 
apply (subst upt_rec, simp) 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1123 
apply (rule sym) 
46820  1124 
apply (subst upt_rec, simp) 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1125 
apply (simp_all del: upt.simps) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1126 
apply (rule_tac j = "succ (i #+ x) " in lt_trans2) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1127 
apply auto 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1128 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1129 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1130 
lemma map_succ_upt: 
46953  1131 
"[ m \<in> nat; n \<in> nat ] ==> map(succ, upt(m,n))= upt(succ(m), succ(n))" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1132 
apply (induct_tac "n") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1133 
apply (auto simp add: map_app_distrib) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1134 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1135 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1136 
lemma nth_map [rule_format,simp]: 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1137 
"xs:list(A) ==> 
46820  1138 
\<forall>n \<in> nat. n < length(xs) \<longrightarrow> nth(n, map(f, xs)) = f(nth(n, xs))" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1139 
apply (induct_tac "xs", simp) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1140 
apply (rule ballI) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1141 
apply (induct_tac "n", auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1142 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1143 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1144 
lemma nth_map_upt [rule_format]: 
46953  1145 
"[ m \<in> nat; n \<in> nat ] ==> 
46820  1146 
\<forall>i \<in> nat. i < n # m \<longrightarrow> nth(i, map(f, upt(m,n))) = f(m #+ i)" 
1147 
apply (rule_tac n = m and m = n in diff_induct, typecheck, simp, simp) 

1148 
apply (subst map_succ_upt [symmetric], simp_all, clarify) 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1149 
apply (subgoal_tac "i < length (upt (0, x))") 
46820  1150 
prefer 2 
1151 
apply (simp add: less_diff_conv) 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1152 
apply (rule_tac j = "succ (i #+ y) " in lt_trans2) 
46820  1153 
apply simp 
1154 
apply simp 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1155 
apply (subgoal_tac "i < length (upt (y, x))") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1156 
apply (simp_all add: add_commute less_diff_conv) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1157 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1158 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1159 
(** sublist (a generalization of nth to sets) **) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1160 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1161 
definition 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1162 
sublist :: "[i, i] => i" where 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1163 
"sublist(xs, A)== 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1164 
map(fst, (filter(%p. snd(p): A, zip(xs, upt(0,length(xs))))))" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1165 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1166 
lemma sublist_0 [simp]: "xs:list(A) ==>sublist(xs, 0) =Nil" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1167 
by (unfold sublist_def, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1168 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1169 
lemma sublist_Nil [simp]: "sublist(Nil, A) = Nil" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1170 
by (unfold sublist_def, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1171 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1172 
lemma sublist_shift_lemma: 
46953  1173 
"[ xs:list(B); i \<in> nat ] ==> 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1174 
map(fst, filter(%p. snd(p):A, zip(xs, upt(i,i #+ length(xs))))) = 
46953  1175 
map(fst, filter(%p. snd(p):nat & snd(p) #+ i \<in> A, zip(xs,upt(0,length(xs)))))" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1176 
apply (erule list_append_induct) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1177 
apply (simp (no_asm_simp)) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1178 
apply (auto simp add: add_commute length_app filter_append map_app_distrib) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1179 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1180 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1181 
lemma sublist_type [simp,TC]: 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1182 
"xs:list(B) ==> sublist(xs, A):list(B)" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1183 
apply (unfold sublist_def) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1184 
apply (induct_tac "xs") 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1185 
apply (auto simp add: filter_append map_app_distrib) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1186 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1187 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1188 
lemma upt_add_eq_append2: 
46953  1189 
"[ i \<in> nat; j \<in> nat ] ==> upt(0, i #+ j) = upt(0, i) @ upt(i, i #+ j)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1190 
by (simp add: upt_add_eq_append [of 0] nat_0_le) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1191 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1192 
lemma sublist_append: 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1193 
"[ xs:list(B); ys:list(B) ] ==> 
46953  1194 
sublist(xs@ys, A) = sublist(xs, A) @ sublist(ys, {j \<in> nat. j #+ length(xs): A})" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1195 
apply (unfold sublist_def) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1196 
apply (erule_tac l = ys in list_append_induct, simp) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1197 
apply (simp (no_asm_simp) add: upt_add_eq_append2 app_assoc [symmetric]) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1198 
apply (auto simp add: sublist_shift_lemma length_type map_app_distrib app_assoc) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1199 
apply (simp_all add: add_commute) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1200 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1201 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1202 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1203 
lemma sublist_Cons: 
46953  1204 
"[ xs:list(B); x \<in> B ] ==> 
46820  1205 
sublist(Cons(x, xs), A) = 
46953  1206 
(if 0 \<in> A then [x] else []) @ sublist(xs, {j \<in> nat. succ(j) \<in> A})" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1207 
apply (erule_tac l = xs in list_append_induct) 
46820  1208 
apply (simp (no_asm_simp) add: sublist_def) 
1209 
apply (simp del: app_Cons add: app_Cons [symmetric] sublist_append, simp) 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1210 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1211 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1212 
lemma sublist_singleton [simp]: 
46820  1213 
"sublist([x], A) = (if 0 \<in> A then [x] else [])" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1214 
by (simp add: sublist_Cons) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1215 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1216 
lemma sublist_upt_eq_take [rule_format, simp]: 
46820  1217 
"xs:list(A) ==> \<forall>n\<in>nat. sublist(xs,n) = take(n,xs)" 
1218 
apply (erule list.induct, simp) 

1219 
apply (clarify ); 

1220 
apply (erule natE) 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1221 
apply (simp_all add: nat_eq_Collect_lt Ord_mem_iff_lt sublist_Cons) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1222 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1223 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1224 
lemma sublist_Int_eq: 
46820  1225 
"xs \<in> list(B) ==> sublist(xs, A \<inter> nat) = sublist(xs, A)" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1226 
apply (erule list.induct) 
46820  1227 
apply (simp_all add: sublist_Cons) 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1228 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1229 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1230 
text{*Repetition of a List Element*} 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1231 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1232 
consts repeat :: "[i,i]=>i" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1233 
primrec 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1234 
"repeat(a,0) = []" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1235 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1236 
"repeat(a,succ(n)) = Cons(a,repeat(a,n))" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1237 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1238 
lemma length_repeat: "n \<in> nat ==> length(repeat(a,n)) = n" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1239 
by (induct_tac n, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1240 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1241 
lemma repeat_succ_app: "n \<in> nat ==> repeat(a,succ(n)) = repeat(a,n) @ [a]" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1242 
apply (induct_tac n) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1243 
apply (simp_all del: app_Cons add: app_Cons [symmetric]) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1244 
done 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1245 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1246 
lemma repeat_type [TC]: "[a \<in> A; n \<in> nat] ==> repeat(a,n) \<in> list(A)" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1247 
by (induct_tac n, auto) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1248 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1249 
end 