--- a/src/HOL/Finite_Set.thy Tue Feb 08 09:46:00 2005 +0100
+++ b/src/HOL/Finite_Set.thy Tue Feb 08 15:11:30 2005 +0100
@@ -437,8 +437,9 @@
inductive "foldSet f g z"
intros
emptyI [intro]: "({}, z) : foldSet f g z"
-insertI [intro]: "\<lbrakk> x \<notin> A; (A, y) : foldSet f g z \<rbrakk>
- \<Longrightarrow> (insert x A, f (g x) y) : foldSet f g z"
+insertI [intro]:
+ "\<lbrakk> x \<notin> A; (A, y) : foldSet f g z \<rbrakk>
+ \<Longrightarrow> (insert x A, f (g x) y) : foldSet f g z"
inductive_cases empty_foldSetE [elim!]: "({}, x) : foldSet f g z"
@@ -538,7 +539,7 @@
show "u \<in> ?r"
proof cases
assume "i\<^isub>u < n"
- thus ?thesis using unotb by(fastsimp)
+ thus ?thesis using unotb by fastsimp
next
assume "\<not> i\<^isub>u < n"
with below have [simp]: "i\<^isub>u = n" by arith
@@ -597,7 +598,7 @@
show ?thesis
proof (rule foldSet.cases[OF Afoldx])
assume "(A, x) = ({}, z)" --{*fold of a singleton set*}
- thus "x' = x" using Afoldy by (auto)
+ thus "x' = x" using Afoldy by auto
next
fix B b y
assume eq1: "(A, x) = (insert b B, g b \<cdot> y)"
@@ -630,7 +631,7 @@
with A1 have "finite ?D" by simp
then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g z"
using finite_imp_foldSet by rules
- moreover have cinB: "c \<in> B" using B by(auto)
+ moreover have cinB: "c \<in> B" using B by auto
ultimately have "(B,g c \<cdot> d) \<in> foldSet f g z"
by(rule Diff1_foldSet)
hence "g c \<cdot> d = y" by(rule IH[OF lessB y])
@@ -667,7 +668,7 @@
show ?thesis
proof (rule foldSet.cases[OF Afoldx])
assume "(A, x) = ({}, e)"
- thus "x' = x" using Afoldy by (auto)
+ thus "x' = x" using Afoldy by auto
next
fix B b y
assume eq1: "(A, x) = (insert b B, g b \<cdot> y)"
@@ -697,7 +698,7 @@
have "finite ?D" using finA A1 by simp
then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g e"
using finite_imp_foldSet by rules
- moreover have cinB: "c \<in> B" using B by(auto)
+ moreover have cinB: "c \<in> B" using B by auto
ultimately have "(B,g c \<cdot> d) \<in> foldSet f g e"
by(rule Diff1_foldSet)
hence "g c \<cdot> d = y" by(rule IH[OF less y])
@@ -752,9 +753,6 @@
cong add: conj_cong simp add: fold_def [symmetric] fold_equality)
done
-declare
- empty_foldSetE [rule del] foldSet.intros [rule del]
- -- {* Delete rules to do with @{text foldSet} relation. *}
text{* A simplified version for idempotent functions: *}
@@ -770,7 +768,7 @@
from finA A have finB: "finite B" by(blast intro: finite_subset)
have "fold f g z (insert a A) = fold f g z (insert a B)" using A by simp
also have "\<dots> = (g a) \<cdot> (fold f g z B)"
- using finB disj by(simp)
+ using finB disj by simp
also have "\<dots> = g a \<cdot> fold f g z A"
using A finB disj by(simp add:idem assoc[symmetric])
finally show ?thesis .
@@ -807,7 +805,7 @@
lemma (in ACf) fold_reindex:
assumes fin: "finite A"
shows "inj_on h A \<Longrightarrow> fold f g z (h ` A) = fold f (g \<circ> h) z A"
-using fin apply (induct)
+using fin apply induct
apply simp
apply simp
done
@@ -838,6 +836,18 @@
apply (simp add: fold_Un_disjoint)
done
+text{*Fusion theorem, as described in
+Graham Hutton's paper,
+A Tutorial on the Universality and Expressiveness of Fold,
+JFP 9:4 (355-372), 1999.*}
+lemma (in ACf) fold_fusion:
+ includes ACf g
+ shows
+ "finite A ==>
+ (!!x y. h (g x y) = f x (h y)) ==>
+ h (fold g j w A) = fold f j (h w) A"
+ by (induct set: Finites, simp_all)
+
lemma (in ACf) fold_cong:
"finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold f g z A = fold f h z A"
apply (subgoal_tac "ALL C. C <= A --> (ALL x:C. g x = h x) --> fold f g z C = fold f h z C")
@@ -858,22 +868,17 @@
fold f (%x. fold f (g x) e (B x)) e A =
fold f (split g) e (SIGMA x:A. B x)"
apply (subst Sigma_def)
-apply (subst fold_UN_disjoint)
- apply assumption
- apply simp
+apply (subst fold_UN_disjoint, assumption, simp)
apply blast
apply (erule fold_cong)
-apply (subst fold_UN_disjoint)
- apply simp
- apply simp
+apply (subst fold_UN_disjoint, simp, simp)
apply blast
-apply (simp)
+apply simp
done
lemma (in ACe) fold_distrib: "finite A \<Longrightarrow>
fold f (%x. f (g x) (h x)) e A = f (fold f g e A) (fold f h e A)"
-apply (erule finite_induct)
- apply simp
+apply (erule finite_induct, simp)
apply (simp add:AC)
done
@@ -1441,8 +1446,7 @@
lemma card_0_eq [simp]: "finite A ==> (card A = 0) = (A = {})"
apply auto
- apply (drule_tac a = x in mk_disjoint_insert, clarify)
- apply (auto)
+ apply (drule_tac a = x in mk_disjoint_insert, clarify, auto)
done
lemma card_eq_0_iff: "(card A = 0) = (A = {} | ~ finite A)"
@@ -1591,8 +1595,7 @@
lemma eq_card_imp_inj_on:
"[| finite A; card(f ` A) = card A |] ==> inj_on f A"
-apply(induct rule:finite_induct)
- apply simp
+apply (induct rule:finite_induct, simp)
apply(frule card_image_le[where f = f])
apply(simp add:card_insert_if split:if_splits)
done
@@ -1739,181 +1742,148 @@
text{* Does not require start value. *}
+(*FIXME: many of the proofs below are too messy!*)
+
consts
- foldSet1 :: "('a => 'a => 'a) => ('a set \<times> 'a) set"
+ fold1Set :: "('a => 'a => 'a) => ('a set \<times> 'a) set"
-inductive "foldSet1 f"
+inductive "fold1Set f"
intros
-foldSet1_singletonI [intro]: "({a}, a) : foldSet1 f"
-foldSet1_insertI [intro]:
- "\<lbrakk> (A, x) : foldSet1 f; a \<notin> A; A \<noteq> {} \<rbrakk>
- \<Longrightarrow> (insert a A, f a x) : foldSet1 f"
+ fold1Set_insertI [intro]:
+ "\<lbrakk> (A,x) \<in> foldSet f id a; a \<notin> A \<rbrakk> \<Longrightarrow> (insert a A, x) \<in> fold1Set f"
constdefs
fold1 :: "('a => 'a => 'a) => 'a set => 'a"
- "fold1 f A == THE x. (A, x) : foldSet1 f"
+ "fold1 f A == THE x. (A, x) : fold1Set f"
+
+lemma fold1Set_nonempty:
+ "(A, x) : fold1Set f \<Longrightarrow> A \<noteq> {}"
+by(erule fold1Set.cases, simp_all)
+
-lemma foldSet1_nonempty:
- "(A, x) : foldSet1 f \<Longrightarrow> A \<noteq> {}"
-by(erule foldSet1.cases, simp_all)
+inductive_cases empty_fold1SetE [elim!]: "({}, x) : fold1Set f"
+
+inductive_cases insert_fold1SetE [elim!]: "(insert a X, x) : fold1Set f"
+
+
+lemma fold1Set_sing [iff]: "(({a},b) : fold1Set f) = (a = b)"
+ by (blast intro: foldSet.intros elim: foldSet.cases)
-inductive_cases empty_foldSet1E [elim!]: "({}, x) : foldSet1 f"
+subsubsection{* Determinacy for @{term fold1Set} *}
+
+text{*First, some lemmas about @{term foldSet}.*}
-lemma foldSet1_sing[iff]: "(({a},b) : foldSet1 f) = (a = b)"
-apply(rule iffI)
- prefer 2 apply fast
-apply (erule foldSet1.cases)
- apply blast
-apply (erule foldSet1.cases)
- apply blast
+lemma (in ACf) foldSet_insert_swap [rule_format]:
+ "(A,y) \<in> foldSet f id b ==> ALL z. z \<notin> A --> b \<notin> A --> z \<noteq> b -->
+ (insert b A, z \<cdot> y) \<in> foldSet f id z"
+apply (erule foldSet.induct)
+apply (simp add: fold_insert_aux)
+apply (force simp add: commute, auto)
+apply (drule_tac x=z in spec, simp)
+apply (subgoal_tac "(insert x (insert b A), x \<cdot> (z \<cdot> y)) \<in> foldSet f (\<lambda>u. u) z")
+prefer 2;
+apply force
+apply (simp add: insert_commute AC)
+done
+
+
+lemma (in ACf) foldSet_permute_diff [rule_format]:
+ "[|(A,x) \<in> foldSet f id b |]
+ ==> ALL a. a \<in> A --> b \<notin> A --> a \<noteq> b --> (insert b (A-{a}), x) \<in> foldSet f id a"
+apply (erule foldSet.induct, simp, clarify, auto) --{*somehow id gets unfolded??*}
+apply (blast intro: foldSet_insert_swap [unfolded id_def])
+apply (drule_tac x=a in spec, simp)
+apply (subgoal_tac "(insert x (insert b (A - {a})), x \<cdot> y) \<in> foldSet f (%u. u) a")
+prefer 2;
+apply force
+apply (subgoal_tac "insert x (insert b (A - {a})) =insert b (insert x A - {a})")
+apply simp
apply blast
done
-lemma Diff1_foldSet1:
- "(A - {x}, y) : foldSet1 f ==> x: A ==> (A, f x y) : foldSet1 f"
-by (erule insert_Diff [THEN subst], rule foldSet1.intros,
- auto dest!:foldSet1_nonempty)
-
-lemma foldSet1_imp_finite: "(A, x) : foldSet1 f ==> finite A"
- by (induct set: foldSet1) auto
-
-lemma finite_nonempty_imp_foldSet1:
- "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> EX x. (A, x) : foldSet1 f"
- by (induct set: Finites) auto
+lemma (in ACf) foldSet_permute:
+ "[|(insert a A, x) \<in> foldSet f id b; a \<notin> A; b \<notin> A|]
+ ==> (insert b A, x) \<in> foldSet f id a"
+apply (case_tac "a=b")
+apply (auto dest: foldSet_permute_diff)
+done
-lemma (in ACf) foldSet1_determ_aux:
- "!!A x y. \<lbrakk> card A < n; (A, x) : foldSet1 f; (A, y) : foldSet1 f \<rbrakk> \<Longrightarrow> y = x"
-proof (induct n)
- case 0 thus ?case by simp
-next
- case (Suc n)
- have IH: "!!A x y. \<lbrakk>card A < n; (A, x) \<in> foldSet1 f; (A, y) \<in> foldSet1 f\<rbrakk>
- \<Longrightarrow> y = x" and card: "card A < Suc n"
- and Afoldx: "(A, x) \<in> foldSet1 f" and Afoldy: "(A, y) \<in> foldSet1 f" .
- from card have "card A < n \<or> card A = n" by arith
- thus ?case
- proof
- assume less: "card A < n"
- show ?thesis by(rule IH[OF less Afoldx Afoldy])
+lemma (in ACf) fold1Set_determ:
+ "(A, x) \<in> fold1Set f ==> (A, y) \<in> fold1Set f ==> y = x"
+proof (clarify elim!: fold1Set.cases)
+ fix A x B y a b
+ assume Ax: "(A, x) \<in> foldSet f id a"
+ assume By: "(B, y) \<in> foldSet f id b"
+ assume anotA: "a \<notin> A"
+ assume bnotB: "b \<notin> B"
+ assume eq: "insert a A = insert b B"
+ show "y=x"
+ proof cases
+ assume same: "a=b"
+ hence "A=B" using anotA bnotB eq by (blast elim!: equalityE)
+ thus ?thesis using Ax By same by (blast intro: foldSet_determ)
next
- assume cardA: "card A = n"
- show ?thesis
- proof (rule foldSet1.cases[OF Afoldx])
- fix a assume "(A, x) = ({a}, a)"
- thus "y = x" using Afoldy by (simp add:foldSet1_sing)
- next
- fix Ax ax x'
- assume eq1: "(A, x) = (insert ax Ax, ax \<cdot> x')"
- and x': "(Ax, x') \<in> foldSet1 f" and notinx: "ax \<notin> Ax"
- and Axnon: "Ax \<noteq> {}"
- hence A1: "A = insert ax Ax" and x: "x = ax \<cdot> x'" by auto
- show ?thesis
- proof (rule foldSet1.cases[OF Afoldy])
- fix ay assume "(A, y) = ({ay}, ay)"
- thus ?thesis using eq1 x' Axnon notinx
- by (fastsimp simp:foldSet1_sing)
- next
- fix Ay ay y'
- assume eq2: "(A, y) = (insert ay Ay, ay \<cdot> y')"
- and y': "(Ay, y') \<in> foldSet1 f" and notiny: "ay \<notin> Ay"
- and Aynon: "Ay \<noteq> {}"
- hence A2: "A = insert ay Ay" and y: "y = ay \<cdot> y'" by auto
- have finA: "finite A" by(rule foldSet1_imp_finite[OF Afoldx])
- with cardA A1 notinx have less: "card Ax < n" by simp
- show ?thesis
- proof cases
- assume "ax = ay"
- then moreover have "Ax = Ay" using A1 A2 notinx notiny by auto
- ultimately show ?thesis using IH[OF less x'] y' eq1 eq2 by auto
- next
- assume diff: "ax \<noteq> ay"
- let ?B = "Ax - {ay}"
- have Ax: "Ax = insert ay ?B" and Ay: "Ay = insert ax ?B"
- using A1 A2 notinx notiny diff by(blast elim!:equalityE)+
- show ?thesis
- proof cases
- assume "?B = {}"
- with Ax Ay show ?thesis using x' y' x y by(simp add:commute)
- next
- assume Bnon: "?B \<noteq> {}"
- moreover have "finite ?B" using finA A1 by simp
- ultimately obtain b where Bfoldb: "(?B,b) \<in> foldSet1 f"
- using finite_nonempty_imp_foldSet1 by(blast)
- moreover have ayinAx: "ay \<in> Ax" using Ax by(auto)
- ultimately have "(Ax,ay\<cdot>b) \<in> foldSet1 f" by(rule Diff1_foldSet1)
- hence "ay\<cdot>b = x'" by(rule IH[OF less x'])
- moreover have "ax\<cdot>b = y'"
- proof (rule IH[OF _ y'])
- show "card Ay < n" using Ay cardA A1 notinx finA ayinAx
- by(auto simp:card_Diff1_less)
- next
- show "(Ay,ax\<cdot>b) \<in> foldSet1 f" using Ay notinx Bfoldb Bnon
- by fastsimp
- qed
- ultimately show ?thesis using x y by(auto simp:AC)
- qed
- qed
- qed
- qed
+ assume diff: "a\<noteq>b"
+ let ?D = "B - {a}"
+ have B: "B = insert a ?D" and A: "A = insert b ?D"
+ and aB: "a \<in> B" and bA: "b \<in> A"
+ using eq anotA bnotB diff by (blast elim!:equalityE)+
+ with aB bnotB By
+ have "(insert b ?D, y) \<in> foldSet f id a"
+ by (auto intro: foldSet_permute simp add: insert_absorb)
+ moreover
+ have "(insert b ?D, x) \<in> foldSet f id a"
+ by (simp add: A [symmetric] Ax)
+ ultimately show ?thesis by (blast intro: foldSet_determ)
qed
qed
-
-lemma (in ACf) foldSet1_determ:
- "(A, x) : foldSet1 f ==> (A, y) : foldSet1 f ==> y = x"
-by (blast intro: foldSet1_determ_aux [rule_format])
-
-lemma (in ACf) foldSet1_equality: "(A, y) : foldSet1 f ==> fold1 f A = y"
- by (unfold fold1_def) (blast intro: foldSet1_determ)
-
lemma fold1_singleton[simp]: "fold1 f {a} = a"
by (unfold fold1_def) blast
-lemma (in ACf) foldSet1_insert_aux: "x \<notin> A ==> A \<noteq> {} \<Longrightarrow>
- ((insert x A, v) : foldSet1 f) =
- (EX y. (A, y) : foldSet1 f & v = f x y)"
-apply auto
-apply (rule_tac A1 = A and f1 = f in finite_nonempty_imp_foldSet1 [THEN exE])
- apply (fastsimp dest: foldSet1_imp_finite)
- apply blast
-apply (blast intro: foldSet1_determ)
+lemma finite_nonempty_imp_fold1Set:
+ "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> EX x. (A, x) : fold1Set f"
+apply (induct A rule: finite_induct)
+apply (auto dest: finite_imp_foldSet [of _ f id])
+done
+
+lemma (in ACf) fold1Set_equality: "(A, y) : fold1Set f ==> fold1 f A = y"
+ by (unfold fold1_def) (blast intro: fold1Set_determ)
+
+lemma (in ACf) fold1_eq_fold:
+ "[|finite A; a \<notin> A|] ==> fold1 f (insert a A) = fold f id a A"
+apply (simp add: fold1_def fold_def)
+apply (rule the_equality)
+apply (best intro: foldSet_determ theI dest: finite_imp_foldSet [of _ f id])
+apply (rule sym, clarify)
+apply (case_tac "Aa=A")
+ apply (best intro: the_equality foldSet_determ)
+apply (subgoal_tac "(A,x) \<in> foldSet f id a")
+ apply (best intro: the_equality foldSet_determ)
+apply (subgoal_tac "insert aa (Aa - {a}) = A")
+ prefer 2 apply (blast elim: equalityE)
+apply (auto dest: foldSet_permute_diff [where a=a])
done
lemma (in ACf) fold1_insert:
"finite A ==> x \<notin> A ==> A \<noteq> {} \<Longrightarrow> fold1 f (insert x A) = f x (fold1 f A)"
-apply (unfold fold1_def)
-apply (simp add: foldSet1_insert_aux)
-apply (rule the_equality)
-apply (auto intro: finite_nonempty_imp_foldSet1
- cong add: conj_cong simp add: fold1_def [symmetric] foldSet1_equality)
+apply (induct A rule: finite_induct, force)
+apply (simp only: insert_commute, simp)
+apply (erule conjE)
+apply (simp add: fold1_eq_fold)
+apply (subst fold1_eq_fold, auto)
done
-lemma (in ACIf) fold1_insert2[simp]:
-assumes finA: "finite A" and nonA: "A \<noteq> {}"
-shows "fold1 f (insert a A) = f a (fold1 f A)"
-proof cases
- assume "a \<in> A"
- then obtain B where A: "A = insert a B" and disj: "a \<notin> B"
- by(blast dest: mk_disjoint_insert)
- show ?thesis
- proof cases
- assume "B = {}"
- thus ?thesis using A by(simp add:idem fold1_singleton)
- next
- assume nonB: "B \<noteq> {}"
- from finA A have finB: "finite B" by(blast intro: finite_subset)
- have "fold1 f (insert a A) = fold1 f (insert a B)" using A by simp
- also have "\<dots> = f a (fold1 f B)"
- using finB nonB disj by(simp add: fold1_insert)
- also have "\<dots> = f a (fold1 f A)"
- using A finB nonB disj by(simp add:idem fold1_insert assoc[symmetric])
- finally show ?thesis .
- qed
-next
- assume "a \<notin> A"
- with finA nonA show ?thesis by(simp add:fold1_insert)
-qed
+lemma (in ACIf) fold1_insert2 [simp]:
+ "finite A ==> A \<noteq> {} \<Longrightarrow> fold1 f (insert x A) = f x (fold1 f A)"
+apply (induct A rule: finite_induct, force)
+apply (case_tac "xa=x")
+ prefer 2 apply (simp add: insert_commute fold1_eq_fold fold_insert2)
+apply (case_tac "F={}")
+apply (simp add: idem)
+apply (simp add: fold1_insert assoc [symmetric] idem)
+done
text{* Now the recursion rules for definitions: *}
@@ -1928,6 +1898,10 @@
"\<lbrakk> g \<equiv> fold1 f; finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (g A)"
by(simp add:fold1_insert2)
+declare
+ empty_foldSetE [rule del] foldSet.intros [rule del]
+ empty_fold1SetE [rule del] insert_fold1SetE [rule del]
+ -- {* No more proves involve these relations. *}
subsubsection{* Semi-Lattices *}
@@ -2026,7 +2000,7 @@
shows "fold1 f A \<in> A"
using A
proof (induct rule:finite_ne_induct)
- case singleton thus ?case by(simp)
+ case singleton thus ?case by simp
next
case insert thus ?case using elem by (force simp add:fold1_insert)
qed
@@ -2354,8 +2328,7 @@
done
lemma Lattice_min_max: "Lattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max"
-apply(rule Lattice.intro)
-apply simp
+apply (rule Lattice.intro, simp)
apply(erule (1) order_trans)
apply(erule (1) order_antisym)
apply(simp add:min_def max_def linorder_not_le order_less_imp_le)
@@ -2443,10 +2416,12 @@
lemma Min_le_Max:
"\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A \<le> Max A"
by(simp add: Min_def Max_def Lattice.Inf_le_Sup[OF Lattice_min_max])
+
(* FIXME
lemma max_Min2_distrib:
"\<lbrakk> finite A; A \<noteq> {}; finite B; B \<noteq> {} \<rbrakk> \<Longrightarrow>
max (Min A) (Min B) = Min{ max a b |a b. a \<in> A \<and> b \<in> B}"
by(simp add: Min_def Max_def Lattice.sup_Inf2_distrib[OF Lattice_min_max])
*)
+
end