--- a/src/ZF/List.thy Tue Sep 27 16:51:35 2022 +0100
+++ b/src/ZF/List.thy Tue Sep 27 17:03:23 2022 +0100
@@ -136,11 +136,11 @@
(*An elimination rule, for type-checking*)
inductive_cases ConsE: "Cons(a,l) \<in> list(A)"
-lemma Cons_type_iff [simp]: "Cons(a,l) \<in> list(A) \<longleftrightarrow> a \<in> A & l \<in> list(A)"
+lemma Cons_type_iff [simp]: "Cons(a,l) \<in> list(A) \<longleftrightarrow> a \<in> A \<and> l \<in> list(A)"
by (blast elim: ConsE)
(*Proving freeness results*)
-lemma Cons_iff: "Cons(a,l)=Cons(a',l') \<longleftrightarrow> a=a' & l=l'"
+lemma Cons_iff: "Cons(a,l)=Cons(a',l') \<longleftrightarrow> a=a' \<and> l=l'"
by auto
lemma Nil_Cons_iff: "\<not> Nil=Cons(a,l)"
@@ -480,7 +480,7 @@
apply (auto dest: not_lt_imp_le)
done
-lemma lt_min_iff: "\<lbrakk>i \<in> nat; j \<in> nat; k \<in> nat\<rbrakk> \<Longrightarrow> i<min(j,k) \<longleftrightarrow> i<j & i<k"
+lemma lt_min_iff: "\<lbrakk>i \<in> nat; j \<in> nat; k \<in> nat\<rbrakk> \<Longrightarrow> i<min(j,k) \<longleftrightarrow> i<j \<and> i<k"
apply (unfold min_def)
apply (auto dest!: not_lt_imp_le intro: lt_trans2 lt_trans)
done
@@ -530,17 +530,17 @@
lemma length_greater_0_iff: "xs:list(A) \<Longrightarrow> 0<length(xs) \<longleftrightarrow> xs \<noteq> Nil"
by (erule list.induct, auto)
-lemma length_succ_iff: "xs:list(A) \<Longrightarrow> length(xs)=succ(n) \<longleftrightarrow> (\<exists>y ys. xs=Cons(y, ys) & length(ys)=n)"
+lemma length_succ_iff: "xs:list(A) \<Longrightarrow> length(xs)=succ(n) \<longleftrightarrow> (\<exists>y ys. xs=Cons(y, ys) \<and> length(ys)=n)"
by (erule list.induct, auto)
(** more theorems about append **)
lemma append_is_Nil_iff [simp]:
- "xs:list(A) \<Longrightarrow> (xs@ys = Nil) \<longleftrightarrow> (xs=Nil & ys = Nil)"
+ "xs:list(A) \<Longrightarrow> (xs@ys = Nil) \<longleftrightarrow> (xs=Nil \<and> ys = Nil)"
by (erule list.induct, auto)
lemma append_is_Nil_iff2 [simp]:
- "xs:list(A) \<Longrightarrow> (Nil = xs@ys) \<longleftrightarrow> (xs=Nil & ys = Nil)"
+ "xs:list(A) \<Longrightarrow> (Nil = xs@ys) \<longleftrightarrow> (xs=Nil \<and> ys = Nil)"
by (erule list.induct, auto)
lemma append_left_is_self_iff [simp]:
@@ -554,7 +554,7 @@
(*TOO SLOW as a default simprule!*)
lemma append_left_is_Nil_iff [rule_format]:
"\<lbrakk>xs:list(A); ys:list(A); zs:list(A)\<rbrakk> \<Longrightarrow>
- length(ys)=length(zs) \<longrightarrow> (xs@ys=zs \<longleftrightarrow> (xs=Nil & ys=zs))"
+ length(ys)=length(zs) \<longrightarrow> (xs@ys=zs \<longleftrightarrow> (xs=Nil \<and> ys=zs))"
apply (erule list.induct)
apply (auto simp add: length_app)
done
@@ -562,14 +562,14 @@
(*TOO SLOW as a default simprule!*)
lemma append_left_is_Nil_iff2 [rule_format]:
"\<lbrakk>xs:list(A); ys:list(A); zs:list(A)\<rbrakk> \<Longrightarrow>
- length(ys)=length(zs) \<longrightarrow> (zs=ys@xs \<longleftrightarrow> (xs=Nil & ys=zs))"
+ length(ys)=length(zs) \<longrightarrow> (zs=ys@xs \<longleftrightarrow> (xs=Nil \<and> ys=zs))"
apply (erule list.induct)
apply (auto simp add: length_app)
done
lemma append_eq_append_iff [rule_format]:
"xs:list(A) \<Longrightarrow> \<forall>ys \<in> list(A).
- length(xs)=length(ys) \<longrightarrow> (xs@us = ys@vs) \<longleftrightarrow> (xs=ys & us=vs)"
+ length(xs)=length(ys) \<longrightarrow> (xs@us = ys@vs) \<longleftrightarrow> (xs=ys \<and> us=vs)"
apply (erule list.induct)
apply (simp (no_asm_simp))
apply clarify
@@ -580,7 +580,7 @@
lemma append_eq_append [rule_format]:
"xs:list(A) \<Longrightarrow>
\<forall>ys \<in> list(A). \<forall>us \<in> list(A). \<forall>vs \<in> list(A).
- length(us) = length(vs) \<longrightarrow> (xs@us = ys@vs) \<longrightarrow> (xs=ys & us=vs)"
+ length(us) = length(vs) \<longrightarrow> (xs@us = ys@vs) \<longrightarrow> (xs=ys \<and> us=vs)"
apply (induct_tac "xs")
apply (force simp add: length_app, clarify)
apply (erule_tac a = ys in list.cases, simp)
@@ -590,7 +590,7 @@
lemma append_eq_append_iff2 [simp]:
"\<lbrakk>xs:list(A); ys:list(A); us:list(A); vs:list(A); length(us)=length(vs)\<rbrakk>
- \<Longrightarrow> xs@us = ys@vs \<longleftrightarrow> (xs=ys & us=vs)"
+ \<Longrightarrow> xs@us = ys@vs \<longleftrightarrow> (xs=ys \<and> us=vs)"
apply (rule iffI)
apply (rule append_eq_append, auto)
done
@@ -606,7 +606,7 @@
(* Can also be proved from append_eq_append_iff2,
but the proof requires two more hypotheses: x \<in> A and y \<in> A *)
lemma append1_eq_iff [rule_format]:
- "xs:list(A) \<Longrightarrow> \<forall>ys \<in> list(A). xs@[x] = ys@[y] \<longleftrightarrow> (xs = ys & x=y)"
+ "xs:list(A) \<Longrightarrow> \<forall>ys \<in> list(A). xs@[x] = ys@[y] \<longleftrightarrow> (xs = ys \<and> x=y)"
apply (erule list.induct)
apply clarify
apply (erule list.cases)
@@ -769,7 +769,7 @@
lemma set_of_list_conv_nth:
"xs:list(A)
- \<Longrightarrow> set_of_list(xs) = {x \<in> A. \<exists>i\<in>nat. i<length(xs) & x = nth(i,xs)}"
+ \<Longrightarrow> set_of_list(xs) = {x \<in> A. \<exists>i\<in>nat. i<length(xs) \<and> x = nth(i,xs)}"
apply (induct_tac "xs", simp_all)
apply (rule equalityI, auto)
apply (rule_tac x = 0 in bexI, auto)
@@ -968,7 +968,7 @@
"\<lbrakk>xs:list(A); ys:list(B); i \<in> nat\<rbrakk>
\<Longrightarrow> set_of_list(zip(xs, ys)) =
{<x, y>:A*B. \<exists>i\<in>nat. i < min(length(xs), length(ys))
- & x = nth(i, xs) & y = nth(i, ys)}"
+ \<and> x = nth(i, xs) \<and> y = nth(i, ys)}"
by (force intro!: Collect_cong simp add: lt_min_iff set_of_list_conv_nth)
(** list_update **)
@@ -1192,7 +1192,7 @@
lemma sublist_shift_lemma:
"\<lbrakk>xs:list(B); i \<in> nat\<rbrakk> \<Longrightarrow>
map(fst, filter(%p. snd(p):A, zip(xs, upt(i,i #+ length(xs))))) =
- map(fst, filter(%p. snd(p):nat & snd(p) #+ i \<in> A, zip(xs,upt(0,length(xs)))))"
+ map(fst, filter(%p. snd(p):nat \<and> snd(p) #+ i \<in> A, zip(xs,upt(0,length(xs)))))"
apply (erule list_append_induct)
apply (simp (no_asm_simp))
apply (auto simp add: add_commute length_app filter_append map_app_distrib)