--- a/src/HOL/Finite_Set.thy Sat Dec 09 18:06:17 2006 +0100
+++ b/src/HOL/Finite_Set.thy Sun Dec 10 07:12:26 2006 +0100
@@ -428,7 +428,7 @@
*}
consts
- foldSet :: "('a => 'b => 'b) => ('c => 'a) => 'b => ('c set \<times> 'b) set"
+ foldSet :: "('a => 'a => 'a) => ('b => 'a) => 'a => ('b set \<times> 'a) set"
inductive "foldSet f g z"
intros
@@ -440,7 +440,7 @@
inductive_cases empty_foldSetE [elim!]: "({}, x) : foldSet f g z"
constdefs
- fold :: "('a => 'b => 'b) => ('c => 'a) => 'b => 'c set => 'b"
+ fold :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a"
"fold f g z A == THE x. (A, x) : foldSet f g z"
text{*A tempting alternative for the definiens is
@@ -1211,7 +1211,7 @@
proof induct
case empty thus ?case by simp
next
- case (insert x A) thus ?case by (auto intro: order_trans)
+ case (insert x A) thus ?case by (auto simp: add_nonneg_nonneg)
qed
next
case False thus ?thesis by (simp add: setsum_def)
@@ -2213,7 +2213,7 @@
apply(rule ACIf.axioms[OF ACIf_inf])
apply(rule ACIfSL_axioms.intro)
apply(rule iffI)
- apply(blast intro: antisym inf_le1 inf_le2 inf_least refl)
+ apply(blast intro: antisym inf_le1 inf_le2 inf_greatest refl)
apply(erule subst)
apply(rule inf_le2)
done
@@ -2226,7 +2226,7 @@
apply(rule ACIf.axioms[OF ACIf_sup])
apply(rule ACIfSL_axioms.intro)
apply(rule iffI)
- apply(blast intro: antisym sup_ge1 sup_ge2 sup_greatest refl)
+ apply(blast intro: antisym sup_ge1 sup_ge2 sup_least refl)
apply(erule subst)
apply(rule sup_ge2)
done
@@ -2247,12 +2247,12 @@
lemma (in Lattice) sup_Inf_absorb[simp]:
"\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<squnion> \<Sqinter>A) = a"
apply(subst sup_commute)
-apply(simp add:Inf_def sup_absorb ACIfSL.fold1_belowI[OF ACIfSL_inf])
+apply(simp add:Inf_def sup_absorb2 ACIfSL.fold1_belowI[OF ACIfSL_inf])
done
lemma (in Lattice) inf_Sup_absorb[simp]:
"\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<sqinter> \<Squnion>A) = a"
-by(simp add:Sup_def inf_absorb ACIfSL.fold1_belowI[OF ACIfSL_sup])
+by(simp add:Sup_def inf_absorb1 ACIfSL.fold1_belowI[OF ACIfSL_sup])
lemma (in ACIf) hom_fold1_commute:
@@ -2289,7 +2289,7 @@
next
case (insert x A)
have finB: "finite {x \<squnion> b |b. b \<in> B}"
- by(fast intro: finite_surj[where f = "%b. x \<squnion> b", OF B(1)])
+ by(rule finite_surj[where f = "%b. x \<squnion> b", OF B(1)], auto)
have finAB: "finite {a \<squnion> b |a b. a \<in> A \<and> b \<in> B}"
proof -
have "{a \<squnion> b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {a \<squnion> b})"
@@ -2330,7 +2330,7 @@
next
case (insert x A)
have finB: "finite {x \<sqinter> b |b. b \<in> B}"
- by(fast intro: finite_surj[where f = "%b. x \<sqinter> b", OF B(1)])
+ by(rule finite_surj[where f = "%b. x \<sqinter> b", OF B(1)], auto)
have finAB: "finite {a \<sqinter> b |a b. a \<in> A \<and> b \<in> B}"
proof -
have "{a \<sqinter> b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {a \<sqinter> b})"