--- a/src/ZF/UNITY/GenPrefix.thy Tue Sep 27 13:34:54 2022 +0200
+++ b/src/ZF/UNITY/GenPrefix.thy Tue Sep 27 16:51:35 2022 +0100
@@ -17,7 +17,7 @@
definition (*really belongs in ZF/Trancl*)
part_order :: "[i, i] => o" where
- "part_order(A, r) == refl(A,r) & trans[A](r) & antisym(r)"
+ "part_order(A, r) \<equiv> refl(A,r) & trans[A](r) & antisym(r)"
consts
gen_prefix :: "[i, i] => i"
@@ -30,46 +30,46 @@
intros
Nil: "<[],[]>:gen_prefix(A, r)"
- prepend: "[| <xs,ys>:gen_prefix(A, r); <x,y>:r; x \<in> A; y \<in> A |]
- ==> <Cons(x,xs), Cons(y,ys)>: gen_prefix(A, r)"
+ prepend: "\<lbrakk><xs,ys>:gen_prefix(A, r); <x,y>:r; x \<in> A; y \<in> A\<rbrakk>
+ \<Longrightarrow> <Cons(x,xs), Cons(y,ys)>: gen_prefix(A, r)"
- append: "[| <xs,ys>:gen_prefix(A, r); zs:list(A) |]
- ==> <xs, ys@zs>:gen_prefix(A, r)"
+ append: "\<lbrakk><xs,ys>:gen_prefix(A, r); zs:list(A)\<rbrakk>
+ \<Longrightarrow> <xs, ys@zs>:gen_prefix(A, r)"
type_intros app_type list.Nil list.Cons
definition
prefix :: "i=>i" where
- "prefix(A) == gen_prefix(A, id(A))"
+ "prefix(A) \<equiv> gen_prefix(A, id(A))"
definition
strict_prefix :: "i=>i" where
- "strict_prefix(A) == prefix(A) - id(list(A))"
+ "strict_prefix(A) \<equiv> prefix(A) - id(list(A))"
(* less or equal and greater or equal over prefixes *)
abbreviation
pfixLe :: "[i, i] => o" (infixl \<open>pfixLe\<close> 50) where
- "xs pfixLe ys == <xs, ys>:gen_prefix(nat, Le)"
+ "xs pfixLe ys \<equiv> <xs, ys>:gen_prefix(nat, Le)"
abbreviation
pfixGe :: "[i, i] => o" (infixl \<open>pfixGe\<close> 50) where
- "xs pfixGe ys == <xs, ys>:gen_prefix(nat, Ge)"
+ "xs pfixGe ys \<equiv> <xs, ys>:gen_prefix(nat, Ge)"
lemma reflD:
- "[| refl(A, r); x \<in> A |] ==> <x,x>:r"
+ "\<lbrakk>refl(A, r); x \<in> A\<rbrakk> \<Longrightarrow> <x,x>:r"
apply (unfold refl_def, auto)
done
(*** preliminary lemmas ***)
-lemma Nil_gen_prefix: "xs \<in> list(A) ==> <[], xs> \<in> gen_prefix(A, r)"
+lemma Nil_gen_prefix: "xs \<in> list(A) \<Longrightarrow> <[], xs> \<in> gen_prefix(A, r)"
by (drule gen_prefix.append [OF gen_prefix.Nil], simp)
declare Nil_gen_prefix [simp]
-lemma gen_prefix_length_le: "<xs,ys> \<in> gen_prefix(A, r) ==> length(xs) \<le> length(ys)"
+lemma gen_prefix_length_le: "<xs,ys> \<in> gen_prefix(A, r) \<Longrightarrow> length(xs) \<le> length(ys)"
apply (erule gen_prefix.induct)
apply (subgoal_tac [3] "ys \<in> list (A) ")
apply (auto dest: gen_prefix.dom_subset [THEN subsetD]
@@ -78,8 +78,8 @@
lemma Cons_gen_prefix_aux:
- "[| <xs', ys'> \<in> gen_prefix(A, r) |]
- ==> (\<forall>x xs. x \<in> A \<longrightarrow> xs'= Cons(x,xs) \<longrightarrow>
+ "\<lbrakk><xs', ys'> \<in> gen_prefix(A, r)\<rbrakk>
+ \<Longrightarrow> (\<forall>x xs. x \<in> A \<longrightarrow> xs'= Cons(x,xs) \<longrightarrow>
(\<exists>y ys. y \<in> A & ys' = Cons(y,ys) &
<x,y>:r & <xs, ys> \<in> gen_prefix(A, r)))"
apply (erule gen_prefix.induct)
@@ -87,9 +87,9 @@
done
lemma Cons_gen_prefixE:
- "[| <Cons(x,xs), zs> \<in> gen_prefix(A, r);
- !!y ys. [|zs = Cons(y, ys); y \<in> A; x \<in> A; <x,y>:r;
- <xs,ys> \<in> gen_prefix(A, r) |] ==> P |] ==> P"
+ "\<lbrakk><Cons(x,xs), zs> \<in> gen_prefix(A, r);
+ \<And>y ys. \<lbrakk>zs = Cons(y, ys); y \<in> A; x \<in> A; <x,y>:r;
+ <xs,ys> \<in> gen_prefix(A, r)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
apply (frule gen_prefix.dom_subset [THEN subsetD], auto)
apply (blast dest: Cons_gen_prefix_aux)
done
@@ -104,7 +104,7 @@
(** Monotonicity of gen_prefix **)
-lemma gen_prefix_mono2: "r<=s ==> gen_prefix(A, r) \<subseteq> gen_prefix(A, s)"
+lemma gen_prefix_mono2: "r<=s \<Longrightarrow> gen_prefix(A, r) \<subseteq> gen_prefix(A, s)"
apply clarify
apply (frule gen_prefix.dom_subset [THEN subsetD], clarify)
apply (erule rev_mp)
@@ -112,7 +112,7 @@
apply (auto intro: gen_prefix.append)
done
-lemma gen_prefix_mono1: "A<=B ==>gen_prefix(A, r) \<subseteq> gen_prefix(B, r)"
+lemma gen_prefix_mono1: "A<=B \<Longrightarrow>gen_prefix(A, r) \<subseteq> gen_prefix(B, r)"
apply clarify
apply (frule gen_prefix.dom_subset [THEN subsetD], clarify)
apply (erule rev_mp)
@@ -126,7 +126,7 @@
intro: gen_prefix.append list_mono [THEN subsetD])
done
-lemma gen_prefix_mono: "[| A \<subseteq> B; r \<subseteq> s |] ==> gen_prefix(A, r) \<subseteq> gen_prefix(B, s)"
+lemma gen_prefix_mono: "\<lbrakk>A \<subseteq> B; r \<subseteq> s\<rbrakk> \<Longrightarrow> gen_prefix(A, r) \<subseteq> gen_prefix(B, s)"
apply (rule subset_trans)
apply (rule gen_prefix_mono1)
apply (rule_tac [2] gen_prefix_mono2, auto)
@@ -135,7 +135,7 @@
(*** gen_prefix order ***)
(* reflexivity *)
-lemma refl_gen_prefix: "refl(A, r) ==> refl(list(A), gen_prefix(A, r))"
+lemma refl_gen_prefix: "refl(A, r) \<Longrightarrow> refl(list(A), gen_prefix(A, r))"
apply (unfold refl_def, auto)
apply (induct_tac "x", auto)
done
@@ -144,7 +144,7 @@
(* Transitivity *)
(* A lemma for proving gen_prefix_trans_comp *)
-lemma append_gen_prefix [rule_format (no_asm)]: "xs \<in> list(A) ==>
+lemma append_gen_prefix [rule_format (no_asm)]: "xs \<in> list(A) \<Longrightarrow>
\<forall>zs. <xs @ ys, zs> \<in> gen_prefix(A, r) \<longrightarrow> <xs, zs>: gen_prefix(A, r)"
apply (erule list.induct)
apply (auto dest: gen_prefix.dom_subset [THEN subsetD])
@@ -153,7 +153,7 @@
(* Lemma proving transitivity and more*)
lemma gen_prefix_trans_comp [rule_format (no_asm)]:
- "<x, y>: gen_prefix(A, r) ==>
+ "<x, y>: gen_prefix(A, r) \<Longrightarrow>
(\<forall>z \<in> list(A). <y,z> \<in> gen_prefix(A, s)\<longrightarrow><x, z> \<in> gen_prefix(A, s O r))"
apply (erule gen_prefix.induct)
apply (auto elim: ConsE simp add: Nil_gen_prefix)
@@ -162,10 +162,10 @@
apply (drule_tac xs = ys and r = s in append_gen_prefix, auto)
done
-lemma trans_comp_subset: "trans(r) ==> r O r \<subseteq> r"
+lemma trans_comp_subset: "trans(r) \<Longrightarrow> r O r \<subseteq> r"
by (auto dest: transD)
-lemma trans_gen_prefix: "trans(r) ==> trans(gen_prefix(A,r))"
+lemma trans_gen_prefix: "trans(r) \<Longrightarrow> trans(gen_prefix(A,r))"
apply (simp (no_asm) add: trans_def)
apply clarify
apply (rule trans_comp_subset [THEN gen_prefix_mono2, THEN subsetD], assumption)
@@ -174,14 +174,14 @@
done
lemma trans_on_gen_prefix:
- "trans(r) ==> trans[list(A)](gen_prefix(A, r))"
+ "trans(r) \<Longrightarrow> trans[list(A)](gen_prefix(A, r))"
apply (drule_tac A = A in trans_gen_prefix)
apply (unfold trans_def trans_on_def, blast)
done
lemma prefix_gen_prefix_trans:
- "[| <x,y> \<in> prefix(A); <y, z> \<in> gen_prefix(A, r); r<=A*A |]
- ==> <x, z> \<in> gen_prefix(A, r)"
+ "\<lbrakk><x,y> \<in> prefix(A); <y, z> \<in> gen_prefix(A, r); r<=A*A\<rbrakk>
+ \<Longrightarrow> <x, z> \<in> gen_prefix(A, r)"
apply (unfold prefix_def)
apply (rule_tac P = "%r. <x,z> \<in> gen_prefix (A, r) " in right_comp_id [THEN subst])
apply (blast dest: gen_prefix_trans_comp gen_prefix.dom_subset [THEN subsetD])+
@@ -189,8 +189,8 @@
lemma gen_prefix_prefix_trans:
-"[| <x,y> \<in> gen_prefix(A,r); <y, z> \<in> prefix(A); r<=A*A |]
- ==> <x, z> \<in> gen_prefix(A, r)"
+"\<lbrakk><x,y> \<in> gen_prefix(A,r); <y, z> \<in> prefix(A); r<=A*A\<rbrakk>
+ \<Longrightarrow> <x, z> \<in> gen_prefix(A, r)"
apply (unfold prefix_def)
apply (rule_tac P = "%r. <x,z> \<in> gen_prefix (A, r) " in left_comp_id [THEN subst])
apply (blast dest: gen_prefix_trans_comp gen_prefix.dom_subset [THEN subsetD])+
@@ -198,10 +198,10 @@
(** Antisymmetry **)
-lemma nat_le_lemma [rule_format]: "n \<in> nat ==> \<forall>b \<in> nat. n #+ b \<le> n \<longrightarrow> b = 0"
+lemma nat_le_lemma [rule_format]: "n \<in> nat \<Longrightarrow> \<forall>b \<in> nat. n #+ b \<le> n \<longrightarrow> b = 0"
by (induct_tac "n", auto)
-lemma antisym_gen_prefix: "antisym(r) ==> antisym(gen_prefix(A, r))"
+lemma antisym_gen_prefix: "antisym(r) \<Longrightarrow> antisym(gen_prefix(A, r))"
apply (simp (no_asm) add: antisym_def)
apply (rule impI [THEN allI, THEN allI])
apply (erule gen_prefix.induct, blast)
@@ -225,12 +225,12 @@
(*** recursion equations ***)
-lemma gen_prefix_Nil: "xs \<in> list(A) ==> <xs, []> \<in> gen_prefix(A,r) \<longleftrightarrow> (xs = [])"
+lemma gen_prefix_Nil: "xs \<in> list(A) \<Longrightarrow> <xs, []> \<in> gen_prefix(A,r) \<longleftrightarrow> (xs = [])"
by (induct_tac "xs", auto)
declare gen_prefix_Nil [simp]
lemma same_gen_prefix_gen_prefix:
- "[| refl(A, r); xs \<in> list(A) |] ==>
+ "\<lbrakk>refl(A, r); xs \<in> list(A)\<rbrakk> \<Longrightarrow>
<xs@ys, xs@zs>: gen_prefix(A, r) \<longleftrightarrow> <ys,zs> \<in> gen_prefix(A, r)"
apply (unfold refl_def)
apply (induct_tac "xs")
@@ -238,14 +238,14 @@
done
declare same_gen_prefix_gen_prefix [simp]
-lemma gen_prefix_Cons: "[| xs \<in> list(A); ys \<in> list(A); y \<in> A |] ==>
+lemma gen_prefix_Cons: "\<lbrakk>xs \<in> list(A); ys \<in> list(A); y \<in> A\<rbrakk> \<Longrightarrow>
<xs, Cons(y,ys)> \<in> gen_prefix(A,r) \<longleftrightarrow>
(xs=[] | (\<exists>z zs. xs=Cons(z,zs) & z \<in> A & <z,y>:r & <zs,ys> \<in> gen_prefix(A,r)))"
apply (induct_tac "xs", auto)
done
-lemma gen_prefix_take_append: "[| refl(A,r); <xs,ys> \<in> gen_prefix(A, r); zs \<in> list(A) |]
- ==> <xs@zs, take(length(xs), ys) @ zs> \<in> gen_prefix(A, r)"
+lemma gen_prefix_take_append: "\<lbrakk>refl(A,r); <xs,ys> \<in> gen_prefix(A, r); zs \<in> list(A)\<rbrakk>
+ \<Longrightarrow> <xs@zs, take(length(xs), ys) @ zs> \<in> gen_prefix(A, r)"
apply (erule gen_prefix.induct)
apply (simp (no_asm_simp))
apply (frule_tac [!] gen_prefix.dom_subset [THEN subsetD], auto)
@@ -254,21 +254,21 @@
apply (simp_all (no_asm_simp) add: diff_is_0_iff [THEN iffD2] take_type)
done
-lemma gen_prefix_append_both: "[| refl(A, r); <xs,ys> \<in> gen_prefix(A,r);
- length(xs) = length(ys); zs \<in> list(A) |]
- ==> <xs@zs, ys @ zs> \<in> gen_prefix(A, r)"
+lemma gen_prefix_append_both: "\<lbrakk>refl(A, r); <xs,ys> \<in> gen_prefix(A,r);
+ length(xs) = length(ys); zs \<in> list(A)\<rbrakk>
+ \<Longrightarrow> <xs@zs, ys @ zs> \<in> gen_prefix(A, r)"
apply (drule_tac zs = zs in gen_prefix_take_append, assumption+)
apply (subgoal_tac "take (length (xs), ys) =ys")
apply (auto intro!: take_all dest: gen_prefix.dom_subset [THEN subsetD])
done
(*NOT suitable for rewriting since [y] has the form y#ys*)
-lemma append_cons_conv: "xs \<in> list(A) ==> xs @ Cons(y, ys) = (xs @ [y]) @ ys"
+lemma append_cons_conv: "xs \<in> list(A) \<Longrightarrow> xs @ Cons(y, ys) = (xs @ [y]) @ ys"
by (auto simp add: app_assoc)
lemma append_one_gen_prefix_lemma [rule_format]:
- "[| <xs,ys> \<in> gen_prefix(A, r); refl(A, r) |]
- ==> length(xs) < length(ys) \<longrightarrow>
+ "\<lbrakk><xs,ys> \<in> gen_prefix(A, r); refl(A, r)\<rbrakk>
+ \<Longrightarrow> length(xs) < length(ys) \<longrightarrow>
<xs @ [nth(length(xs), ys)], ys> \<in> gen_prefix(A, r)"
apply (erule gen_prefix.induct, blast)
apply (frule gen_prefix.dom_subset [THEN subsetD], clarify)
@@ -290,15 +290,15 @@
apply (auto elim: ConsE simp add: gen_prefix_append_both)
done
-lemma append_one_gen_prefix: "[| <xs,ys>: gen_prefix(A, r); length(xs) < length(ys); refl(A, r) |]
- ==> <xs @ [nth(length(xs), ys)], ys> \<in> gen_prefix(A, r)"
+lemma append_one_gen_prefix: "\<lbrakk><xs,ys>: gen_prefix(A, r); length(xs) < length(ys); refl(A, r)\<rbrakk>
+ \<Longrightarrow> <xs @ [nth(length(xs), ys)], ys> \<in> gen_prefix(A, r)"
apply (blast intro: append_one_gen_prefix_lemma)
done
(** Proving the equivalence with Charpentier's definition **)
-lemma gen_prefix_imp_nth_lemma [rule_format]: "xs \<in> list(A) ==>
+lemma gen_prefix_imp_nth_lemma [rule_format]: "xs \<in> list(A) \<Longrightarrow>
\<forall>ys \<in> list(A). \<forall>i \<in> nat. i < length(xs)
\<longrightarrow> <xs, ys>: gen_prefix(A, r) \<longrightarrow> <nth(i, xs), nth(i, ys)>:r"
apply (induct_tac "xs", simp, clarify)
@@ -306,14 +306,14 @@
apply (erule natE, auto)
done
-lemma gen_prefix_imp_nth: "[| <xs,ys> \<in> gen_prefix(A,r); i < length(xs)|]
- ==> <nth(i, xs), nth(i, ys)>:r"
+lemma gen_prefix_imp_nth: "\<lbrakk><xs,ys> \<in> gen_prefix(A,r); i < length(xs)\<rbrakk>
+ \<Longrightarrow> <nth(i, xs), nth(i, ys)>:r"
apply (cut_tac A = A in gen_prefix.dom_subset)
apply (rule gen_prefix_imp_nth_lemma)
apply (auto simp add: lt_nat_in_nat)
done
-lemma nth_imp_gen_prefix [rule_format]: "xs \<in> list(A) ==>
+lemma nth_imp_gen_prefix [rule_format]: "xs \<in> list(A) \<Longrightarrow>
\<forall>ys \<in> list(A). length(xs) \<le> length(ys)
\<longrightarrow> (\<forall>i. i < length(xs) \<longrightarrow> <nth(i, xs), nth(i,ys)>:r)
\<longrightarrow> <xs, ys> \<in> gen_prefix(A, r)"
@@ -363,7 +363,7 @@
(* Monotonicity of "set" operator WRT prefix *)
lemma set_of_list_prefix_mono:
-"<xs,ys> \<in> prefix(A) ==> set_of_list(xs) \<subseteq> set_of_list(ys)"
+"<xs,ys> \<in> prefix(A) \<Longrightarrow> set_of_list(xs) \<subseteq> set_of_list(ys)"
apply (unfold prefix_def)
apply (erule gen_prefix.induct)
@@ -374,7 +374,7 @@
(** recursion equations **)
-lemma Nil_prefix: "xs \<in> list(A) ==> <[],xs> \<in> prefix(A)"
+lemma Nil_prefix: "xs \<in> list(A) \<Longrightarrow> <[],xs> \<in> prefix(A)"
apply (unfold prefix_def)
apply (simp (no_asm_simp) add: Nil_gen_prefix)
@@ -398,7 +398,7 @@
declare Cons_prefix_Cons [iff]
lemma same_prefix_prefix:
-"xs \<in> list(A)==> <xs@ys,xs@zs> \<in> prefix(A) \<longleftrightarrow> (<ys,zs> \<in> prefix(A))"
+"xs \<in> list(A)\<Longrightarrow> <xs@ys,xs@zs> \<in> prefix(A) \<longleftrightarrow> (<ys,zs> \<in> prefix(A))"
apply (unfold prefix_def)
apply (subgoal_tac "refl (A,id (A))")
apply (simp (no_asm_simp))
@@ -406,21 +406,21 @@
done
declare same_prefix_prefix [simp]
-lemma same_prefix_prefix_Nil: "xs \<in> list(A) ==> <xs@ys,xs> \<in> prefix(A) \<longleftrightarrow> (<ys,[]> \<in> prefix(A))"
+lemma same_prefix_prefix_Nil: "xs \<in> list(A) \<Longrightarrow> <xs@ys,xs> \<in> prefix(A) \<longleftrightarrow> (<ys,[]> \<in> prefix(A))"
apply (rule_tac P = "%x. <u, x>:v \<longleftrightarrow> w(x)" for u v w in app_right_Nil [THEN subst])
apply (rule_tac [2] same_prefix_prefix, auto)
done
declare same_prefix_prefix_Nil [simp]
lemma prefix_appendI:
-"[| <xs,ys> \<in> prefix(A); zs \<in> list(A) |] ==> <xs,ys@zs> \<in> prefix(A)"
+"\<lbrakk><xs,ys> \<in> prefix(A); zs \<in> list(A)\<rbrakk> \<Longrightarrow> <xs,ys@zs> \<in> prefix(A)"
apply (unfold prefix_def)
apply (erule gen_prefix.append, assumption)
done
declare prefix_appendI [simp]
lemma prefix_Cons:
-"[| xs \<in> list(A); ys \<in> list(A); y \<in> A |] ==>
+"\<lbrakk>xs \<in> list(A); ys \<in> list(A); y \<in> A\<rbrakk> \<Longrightarrow>
<xs,Cons(y,ys)> \<in> prefix(A) \<longleftrightarrow>
(xs=[] | (\<exists>zs. xs=Cons(y,zs) & <zs,ys> \<in> prefix(A)))"
apply (unfold prefix_def)
@@ -428,8 +428,8 @@
done
lemma append_one_prefix:
- "[| <xs,ys> \<in> prefix(A); length(xs) < length(ys) |]
- ==> <xs @ [nth(length(xs),ys)], ys> \<in> prefix(A)"
+ "\<lbrakk><xs,ys> \<in> prefix(A); length(xs) < length(ys)\<rbrakk>
+ \<Longrightarrow> <xs @ [nth(length(xs),ys)], ys> \<in> prefix(A)"
apply (unfold prefix_def)
apply (subgoal_tac "refl (A, id (A))")
apply (simp (no_asm_simp) add: append_one_gen_prefix)
@@ -437,7 +437,7 @@
done
lemma prefix_length_le:
-"<xs,ys> \<in> prefix(A) ==> length(xs) \<le> length(ys)"
+"<xs,ys> \<in> prefix(A) \<Longrightarrow> length(xs) \<le> length(ys)"
apply (unfold prefix_def)
apply (blast dest: gen_prefix_length_le)
done
@@ -454,7 +454,7 @@
done
lemma strict_prefix_length_lt_aux:
- "<xs,ys> \<in> prefix(A) ==> xs\<noteq>ys \<longrightarrow> length(xs) < length(ys)"
+ "<xs,ys> \<in> prefix(A) \<Longrightarrow> xs\<noteq>ys \<longrightarrow> length(xs) < length(ys)"
apply (unfold prefix_def)
apply (erule gen_prefix.induct, clarify)
apply (subgoal_tac [!] "ys \<in> list(A) & xs \<in> list(A)")
@@ -467,7 +467,7 @@
done
lemma strict_prefix_length_lt:
- "<xs,ys>:strict_prefix(A) ==> length(xs) < length(ys)"
+ "<xs,ys>:strict_prefix(A) \<Longrightarrow> length(xs) < length(ys)"
apply (unfold strict_prefix_def)
apply (rule strict_prefix_length_lt_aux [THEN mp])
apply (auto dest: prefix_type [THEN subsetD])
@@ -493,7 +493,7 @@
done
lemma prefix_snoc:
-"[|xs \<in> list(A); ys \<in> list(A); y \<in> A |] ==>
+"\<lbrakk>xs \<in> list(A); ys \<in> list(A); y \<in> A\<rbrakk> \<Longrightarrow>
<xs, ys@[y]> \<in> prefix(A) \<longleftrightarrow> (xs = ys@[y] | <xs,ys> \<in> prefix(A))"
apply (simp (no_asm) add: prefix_iff)
apply (rule iffI, clarify)
@@ -503,7 +503,7 @@
done
declare prefix_snoc [simp]
-lemma prefix_append_iff [rule_format]: "zs \<in> list(A) ==> \<forall>xs \<in> list(A). \<forall>ys \<in> list(A).
+lemma prefix_append_iff [rule_format]: "zs \<in> list(A) \<Longrightarrow> \<forall>xs \<in> list(A). \<forall>ys \<in> list(A).
(<xs, ys@zs> \<in> prefix(A)) \<longleftrightarrow>
(<xs,ys> \<in> prefix(A) | (\<exists>us. xs = ys@us & <us,zs> \<in> prefix(A)))"
apply (erule list_append_induct, force, clarify)
@@ -518,14 +518,14 @@
(*Although the prefix ordering is not linear, the prefixes of a list
are linearly ordered.*)
-lemma common_prefix_linear_lemma [rule_format]: "[| zs \<in> list(A); xs \<in> list(A); ys \<in> list(A) |]
- ==> <xs, zs> \<in> prefix(A) \<longrightarrow> <ys,zs> \<in> prefix(A)
+lemma common_prefix_linear_lemma [rule_format]: "\<lbrakk>zs \<in> list(A); xs \<in> list(A); ys \<in> list(A)\<rbrakk>
+ \<Longrightarrow> <xs, zs> \<in> prefix(A) \<longrightarrow> <ys,zs> \<in> prefix(A)
\<longrightarrow><xs,ys> \<in> prefix(A) | <ys,xs> \<in> prefix(A)"
apply (erule list_append_induct, auto)
done
-lemma common_prefix_linear: "[|<xs, zs> \<in> prefix(A); <ys,zs> \<in> prefix(A) |]
- ==> <xs,ys> \<in> prefix(A) | <ys,xs> \<in> prefix(A)"
+lemma common_prefix_linear: "\<lbrakk><xs, zs> \<in> prefix(A); <ys,zs> \<in> prefix(A)\<rbrakk>
+ \<Longrightarrow> <xs,ys> \<in> prefix(A) | <ys,xs> \<in> prefix(A)"
apply (cut_tac prefix_type)
apply (blast del: disjCI intro: common_prefix_linear_lemma)
done
@@ -565,19 +565,19 @@
by (unfold part_order_def, auto)
declare part_order_Le [simp]
-lemma pfixLe_refl: "x \<in> list(nat) ==> x pfixLe x"
+lemma pfixLe_refl: "x \<in> list(nat) \<Longrightarrow> x pfixLe x"
by (blast intro: refl_gen_prefix [THEN reflD] refl_Le)
declare pfixLe_refl [simp]
-lemma pfixLe_trans: "[| x pfixLe y; y pfixLe z |] ==> x pfixLe z"
+lemma pfixLe_trans: "\<lbrakk>x pfixLe y; y pfixLe z\<rbrakk> \<Longrightarrow> x pfixLe z"
by (blast intro: trans_gen_prefix [THEN transD] trans_Le)
-lemma pfixLe_antisym: "[| x pfixLe y; y pfixLe x |] ==> x = y"
+lemma pfixLe_antisym: "\<lbrakk>x pfixLe y; y pfixLe x\<rbrakk> \<Longrightarrow> x = y"
by (blast intro: antisym_gen_prefix [THEN antisymE] antisym_Le)
lemma prefix_imp_pfixLe:
-"<xs,ys>:prefix(nat)==> xs pfixLe ys"
+"<xs,ys>:prefix(nat)\<Longrightarrow> xs pfixLe ys"
apply (unfold prefix_def)
apply (rule gen_prefix_mono [THEN subsetD], auto)
@@ -599,25 +599,25 @@
done
declare trans_Ge [iff]
-lemma pfixGe_refl: "x \<in> list(nat) ==> x pfixGe x"
+lemma pfixGe_refl: "x \<in> list(nat) \<Longrightarrow> x pfixGe x"
by (blast intro: refl_gen_prefix [THEN reflD])
declare pfixGe_refl [simp]
-lemma pfixGe_trans: "[| x pfixGe y; y pfixGe z |] ==> x pfixGe z"
+lemma pfixGe_trans: "\<lbrakk>x pfixGe y; y pfixGe z\<rbrakk> \<Longrightarrow> x pfixGe z"
by (blast intro: trans_gen_prefix [THEN transD])
-lemma pfixGe_antisym: "[| x pfixGe y; y pfixGe x |] ==> x = y"
+lemma pfixGe_antisym: "\<lbrakk>x pfixGe y; y pfixGe x\<rbrakk> \<Longrightarrow> x = y"
by (blast intro: antisym_gen_prefix [THEN antisymE])
lemma prefix_imp_pfixGe:
- "<xs,ys>:prefix(nat) ==> xs pfixGe ys"
+ "<xs,ys>:prefix(nat) \<Longrightarrow> xs pfixGe ys"
apply (unfold prefix_def Ge_def)
apply (rule gen_prefix_mono [THEN subsetD], auto)
done
(* Added by Sidi \<in> prefix and take *)
lemma prefix_imp_take:
-"<xs, ys> \<in> prefix(A) ==> xs = take(length(xs), ys)"
+"<xs, ys> \<in> prefix(A) \<Longrightarrow> xs = take(length(xs), ys)"
apply (unfold prefix_def)
apply (erule gen_prefix.induct)
@@ -630,17 +630,17 @@
apply (simp_all (no_asm_simp) add: diff_is_0_iff)
done
-lemma prefix_length_equal: "[|<xs,ys> \<in> prefix(A); length(xs)=length(ys)|] ==> xs = ys"
+lemma prefix_length_equal: "\<lbrakk><xs,ys> \<in> prefix(A); length(xs)=length(ys)\<rbrakk> \<Longrightarrow> xs = ys"
apply (cut_tac A = A in prefix_type)
apply (drule subsetD, auto)
apply (drule prefix_imp_take)
apply (erule trans, simp)
done
-lemma prefix_length_le_equal: "[|<xs,ys> \<in> prefix(A); length(ys) \<le> length(xs)|] ==> xs = ys"
+lemma prefix_length_le_equal: "\<lbrakk><xs,ys> \<in> prefix(A); length(ys) \<le> length(xs)\<rbrakk> \<Longrightarrow> xs = ys"
by (blast intro: prefix_length_equal le_anti_sym prefix_length_le)
-lemma take_prefix [rule_format]: "xs \<in> list(A) ==> \<forall>n \<in> nat. <take(n, xs), xs> \<in> prefix(A)"
+lemma take_prefix [rule_format]: "xs \<in> list(A) \<Longrightarrow> \<forall>n \<in> nat. <take(n, xs), xs> \<in> prefix(A)"
apply (unfold prefix_def)
apply (erule list.induct, simp, clarify)
apply (erule natE, auto)
@@ -654,21 +654,21 @@
apply (blast intro: take_prefix length_type)
done
-lemma prefix_imp_nth: "[| <xs,ys> \<in> prefix(A); i < length(xs)|] ==> nth(i,xs) = nth(i,ys)"
+lemma prefix_imp_nth: "\<lbrakk><xs,ys> \<in> prefix(A); i < length(xs)\<rbrakk> \<Longrightarrow> nth(i,xs) = nth(i,ys)"
by (auto dest!: gen_prefix_imp_nth simp add: prefix_def)
lemma nth_imp_prefix:
- "[|xs \<in> list(A); ys \<in> list(A); length(xs) \<le> length(ys);
- !!i. i < length(xs) ==> nth(i, xs) = nth(i,ys)|]
- ==> <xs,ys> \<in> prefix(A)"
+ "\<lbrakk>xs \<in> list(A); ys \<in> list(A); length(xs) \<le> length(ys);
+ \<And>i. i < length(xs) \<Longrightarrow> nth(i, xs) = nth(i,ys)\<rbrakk>
+ \<Longrightarrow> <xs,ys> \<in> prefix(A)"
apply (auto simp add: prefix_def nth_imp_gen_prefix)
apply (auto intro!: nth_imp_gen_prefix simp add: prefix_def)
apply (blast intro: nth_type lt_trans2)
done
-lemma length_le_prefix_imp_prefix: "[|length(xs) \<le> length(ys);
- <xs,zs> \<in> prefix(A); <ys,zs> \<in> prefix(A)|] ==> <xs,ys> \<in> prefix(A)"
+lemma length_le_prefix_imp_prefix: "\<lbrakk>length(xs) \<le> length(ys);
+ <xs,zs> \<in> prefix(A); <ys,zs> \<in> prefix(A)\<rbrakk> \<Longrightarrow> <xs,ys> \<in> prefix(A)"
apply (cut_tac A = A in prefix_type)
apply (rule nth_imp_prefix, blast, blast)
apply assumption