--- a/src/HOL/Finite_Set.thy Tue May 02 19:23:48 2006 +0200
+++ b/src/HOL/Finite_Set.thy Tue May 02 20:42:30 2006 +0200
@@ -803,6 +803,10 @@
setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
"setsum f A == if finite A then fold (op +) f 0 A else 0"
+abbreviation
+ Setsum ("\<Sum>_" [1000] 999)
+ "\<Sum>A == setsum (%x. x) A"
+
text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
written @{text"\<Sum>x\<in>A. e"}. *}
@@ -831,31 +835,18 @@
"SUM x|P. t" => "setsum (%x. t) {x. P}"
"\<Sum>x|P. t" => "setsum (%x. t) {x. P}"
-text{* Finally we abbreviate @{term"\<Sum>x\<in>A. x"} by @{text"\<Sum>A"}. *}
-
-syntax
- "_Setsum" :: "'a set => 'a::comm_monoid_mult" ("\<Sum>_" [1000] 999)
-
-parse_translation {*
- let
- fun Setsum_tr [A] = Syntax.const "setsum" $ Term.absdummy (dummyT, Bound 0) $ A
- in [("_Setsum", Setsum_tr)] end;
-*}
-
print_translation {*
let
- fun setsum_tr' [Abs(_,_,Bound 0), A] = Syntax.const "_Setsum" $ A
- | setsum_tr' [Abs(x,Tx,t), Const ("Collect",_) $ Abs(y,Ty,P)] =
- if x<>y then raise Match
- else let val x' = Syntax.mark_bound x
- val t' = subst_bound(x',t)
- val P' = subst_bound(x',P)
- in Syntax.const "_qsetsum" $ Syntax.mark_bound x $ P' $ t' end
-in
-[("setsum", setsum_tr')]
-end
+ fun setsum_tr' [Abs(x,Tx,t), Const ("Collect",_) $ Abs(y,Ty,P)] =
+ if x<>y then raise Match
+ else let val x' = Syntax.mark_bound x
+ val t' = subst_bound(x',t)
+ val P' = subst_bound(x',P)
+ in Syntax.const "_qsetsum" $ Syntax.mark_bound x $ P' $ t' end
+in [("setsum", setsum_tr')] end
*}
+
lemma setsum_empty [simp]: "setsum f {} = 0"
by (simp add: setsum_def)
@@ -995,10 +986,11 @@
(* By Jeremy Siek: *)
lemma setsum_diff_nat:
- assumes finB: "finite B"
- shows "B \<subseteq> A \<Longrightarrow> (setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
-using finB
-proof (induct)
+ assumes "finite B"
+ and "B \<subseteq> A"
+ shows "(setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
+ using prems
+proof induct
show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
next
fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
@@ -1026,15 +1018,15 @@
proof -
from le have finiteB: "finite B" using finite_subset by auto
show ?thesis using finiteB le
- proof (induct)
- case empty
- thus ?case by auto
- next
- case (insert x F)
- thus ?case using le finiteB
- by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
- qed
+ proof (induct)
+ case empty
+ thus ?case by auto
+ next
+ case (insert x F)
+ thus ?case using le finiteB
+ by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
qed
+qed
lemma setsum_mono:
assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, pordered_ab_semigroup_add}))"
@@ -1042,13 +1034,12 @@
proof (cases "finite K")
case True
thus ?thesis using le
- proof (induct)
+ proof induct
case empty
thus ?case by simp
next
case insert
- thus ?case using add_mono
- by force
+ thus ?case using add_mono by fastsimp
qed
next
case False
@@ -1057,10 +1048,11 @@
qed
lemma setsum_strict_mono:
-fixes f :: "'a \<Rightarrow> 'b::{pordered_cancel_ab_semigroup_add,comm_monoid_add}"
-assumes fin_ne: "finite A" "A \<noteq> {}"
-shows "(!!x. x:A \<Longrightarrow> f x < g x) \<Longrightarrow> setsum f A < setsum g A"
-using fin_ne
+ fixes f :: "'a \<Rightarrow> 'b::{pordered_cancel_ab_semigroup_add,comm_monoid_add}"
+ assumes "finite A" "A \<noteq> {}"
+ and "!!x. x:A \<Longrightarrow> f x < g x"
+ shows "setsum f A < setsum g A"
+ using prems
proof (induct rule: finite_ne_induct)
case singleton thus ?case by simp
next
@@ -1068,7 +1060,7 @@
qed
lemma setsum_negf:
- "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
+ "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
proof (cases "finite A")
case True thus ?thesis by (induct set: Finites, auto)
next
@@ -1076,8 +1068,8 @@
qed
lemma setsum_subtractf:
- "setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
- setsum f A - setsum g A"
+ "setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
+ setsum f A - setsum g A"
proof (cases "finite A")
case True thus ?thesis by (simp add: diff_minus setsum_addf setsum_negf)
next
@@ -1085,27 +1077,33 @@
qed
lemma setsum_nonneg:
-assumes nn: "\<forall>x\<in>A. (0::'a::{pordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
-shows "0 \<le> setsum f A"
+ assumes nn: "\<forall>x\<in>A. (0::'a::{pordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
+ shows "0 \<le> setsum f A"
proof (cases "finite A")
case True thus ?thesis using nn
- apply (induct set: Finites, auto)
- apply (subgoal_tac "0 + 0 \<le> f x + setsum f F", simp)
- apply (blast intro: add_mono)
- done
+ proof (induct)
+ case empty then show ?case by simp
+ next
+ case (insert x F)
+ then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono)
+ with insert show ?case by simp
+ qed
next
case False thus ?thesis by (simp add: setsum_def)
qed
lemma setsum_nonpos:
-assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{pordered_ab_semigroup_add,comm_monoid_add})"
-shows "setsum f A \<le> 0"
+ assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{pordered_ab_semigroup_add,comm_monoid_add})"
+ shows "setsum f A \<le> 0"
proof (cases "finite A")
case True thus ?thesis using np
- apply (induct set: Finites, auto)
- apply (subgoal_tac "f x + setsum f F \<le> 0 + 0", simp)
- apply (blast intro: add_mono)
- done
+ proof (induct)
+ case empty then show ?case by simp
+ next
+ case (insert x F)
+ then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono)
+ with insert show ?case by simp
+ qed
next
case False thus ?thesis by (simp add: setsum_def)
qed
@@ -1277,6 +1275,10 @@
setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult"
"setprod f A == if finite A then fold (op *) f 1 A else 1"
+abbreviation
+ Setprod ("\<Prod>_" [1000] 999)
+ "\<Prod>A == setprod (%x. x) A"
+
syntax
"_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(3PROD _:_. _)" [0, 51, 10] 10)
syntax (xsymbols)
@@ -1302,24 +1304,6 @@
"PROD x|P. t" => "setprod (%x. t) {x. P}"
"\<Prod>x|P. t" => "setprod (%x. t) {x. P}"
-text{* Finally we abbreviate @{term"\<Prod>x\<in>A. x"} by @{text"\<Prod>A"}. *}
-
-syntax
- "_Setprod" :: "'a set => 'a::comm_monoid_mult" ("\<Prod>_" [1000] 999)
-
-parse_translation {*
- let
- fun Setprod_tr [A] = Syntax.const "setprod" $ Abs ("", dummyT, Bound 0) $ A
- in [("_Setprod", Setprod_tr)] end;
-*}
-print_translation {*
-let fun setprod_tr' [Abs(x,Tx,t), A] =
- if t = Bound 0 then Syntax.const "_Setprod" $ A else raise Match
-in
-[("setprod", setprod_tr')]
-end
-*}
-
lemma setprod_empty [simp]: "setprod f {} = 1"
by (auto simp add: setprod_def)
--- a/src/HOL/Integ/IntDef.thy Tue May 02 19:23:48 2006 +0200
+++ b/src/HOL/Integ/IntDef.thy Tue May 02 20:42:30 2006 +0200
@@ -5,7 +5,7 @@
*)
-header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*}
+header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*}
theory IntDef
imports Equiv_Relations NatArith
@@ -108,10 +108,10 @@
qed
lemma zminus_zminus: "- (- z) = (z::int)"
-by (cases z, simp add: minus)
+ by (cases z) (simp add: minus)
lemma zminus_0: "- 0 = (0::int)"
-by (simp add: int_def Zero_int_def minus)
+ by (simp add: int_def Zero_int_def minus)
subsection{*Integer Addition*}
@@ -129,13 +129,13 @@
qed
lemma zminus_zadd_distrib: "- (z + w) = (- z) + (- w::int)"
-by (cases z, cases w, simp add: minus add)
+ by (cases z, cases w) (simp add: minus add)
lemma zadd_commute: "(z::int) + w = w + z"
-by (cases z, cases w, simp add: add_ac add)
+ by (cases z, cases w) (simp add: add_ac add)
lemma zadd_assoc: "((z1::int) + z2) + z3 = z1 + (z2 + z3)"
-by (cases z1, cases z2, cases z3, simp add: add add_assoc)
+ by (cases z1, cases z2, cases z3) (simp add: add add_assoc)
(*For AC rewriting*)
lemma zadd_left_commute: "x + (y + z) = y + ((x + z) ::int)"
@@ -149,13 +149,13 @@
lemmas zmult_ac = OrderedGroup.mult_ac
lemma zadd_int: "(int m) + (int n) = int (m + n)"
-by (simp add: int_def add)
+ by (simp add: int_def add)
lemma zadd_int_left: "(int m) + (int n + z) = int (m + n) + z"
-by (simp add: zadd_int zadd_assoc [symmetric])
+ by (simp add: zadd_int zadd_assoc [symmetric])
lemma int_Suc: "int (Suc m) = 1 + (int m)"
-by (simp add: One_int_def zadd_int)
+ by (simp add: One_int_def zadd_int)
(*also for the instance declaration int :: comm_monoid_add*)
lemma zadd_0: "(0::int) + z = z"
@@ -564,10 +564,12 @@
subsection{*The Set of Natural Numbers*}
constdefs
- Nats :: "'a::comm_semiring_1_cancel set"
- "Nats == range of_nat"
+ Nats :: "'a::comm_semiring_1_cancel set"
+ "Nats == range of_nat"
-syntax (xsymbols) Nats :: "'a set" ("\<nat>")
+abbreviation (xsymbols)
+ Nats1 ("\<nat>")
+ "\<nat> == Nats"
lemma of_nat_in_Nats [simp]: "of_nat n \<in> Nats"
by (simp add: Nats_def)
@@ -686,22 +688,22 @@
lemma of_int_eq_id [simp]: "of_int = (id :: int => int)"
proof
- fix z
- show "of_int z = id z"
- by (cases z,
- simp add: of_int add minus int_eq_of_nat [symmetric] int_def diff_minus)
+ fix z
+ show "of_int z = id z"
+ by (cases z)
+ (simp add: of_int add minus int_eq_of_nat [symmetric] int_def diff_minus)
qed
subsection{*The Set of Integers*}
constdefs
- Ints :: "'a::comm_ring_1 set"
- "Ints == range of_int"
+ Ints :: "'a::comm_ring_1 set"
+ "Ints == range of_int"
-
-syntax (xsymbols)
- Ints :: "'a set" ("\<int>")
+abbreviation (xsymbols)
+ Ints1 ("\<int>")
+ "\<int> == Ints"
lemma Ints_0 [simp]: "0 \<in> Ints"
apply (simp add: Ints_def)
@@ -746,11 +748,14 @@
lemma of_int_int_eq [simp]: "of_int (int n) = of_nat n"
by (simp add: int_eq_of_nat)
-lemma Ints_cases [case_names of_int, cases set: Ints]:
- "q \<in> \<int> ==> (!!z. q = of_int z ==> C) ==> C"
-proof (simp add: Ints_def)
- assume "!!z. q = of_int z ==> C"
- assume "q \<in> range of_int" thus C ..
+lemma Ints_cases [cases set: Ints]:
+ assumes "q \<in> \<int>"
+ obtains (of_int) z where "q = of_int z"
+ unfolding Ints_def
+proof -
+ from `q \<in> \<int>` have "q \<in> range of_int" unfolding Ints_def .
+ then obtain z where "q = of_int z" ..
+ then show thesis ..
qed
lemma Ints_induct [case_names of_int, induct set: Ints]:
@@ -768,12 +773,12 @@
lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
- apply (case_tac "finite A")
+ apply (cases "finite A")
apply (erule finite_induct, auto)
done
lemma of_int_setsum: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
- apply (case_tac "finite A")
+ apply (cases "finite A")
apply (erule finite_induct, auto)
done
@@ -781,12 +786,12 @@
by (simp add: int_eq_of_nat of_nat_setsum)
lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
- apply (case_tac "finite A")
+ apply (cases "finite A")
apply (erule finite_induct, auto)
done
lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
- apply (case_tac "finite A")
+ apply (cases "finite A")
apply (erule finite_induct, auto)
done
--- a/src/HOL/Product_Type.thy Tue May 02 19:23:48 2006 +0200
+++ b/src/HOL/Product_Type.thy Tue May 02 20:42:30 2006 +0200
@@ -85,7 +85,7 @@
local
-subsubsection {* Abstract constants and syntax *}
+subsubsection {* Definitions *}
global
@@ -100,6 +100,30 @@
local
+defs
+ Pair_def: "Pair a b == Abs_Prod (Pair_Rep a b)"
+ fst_def: "fst p == THE a. EX b. p = Pair a b"
+ snd_def: "snd p == THE b. EX a. p = Pair a b"
+ split_def: "split == (%c p. c (fst p) (snd p))"
+ curry_def: "curry == (%c x y. c (Pair x y))"
+ prod_fun_def: "prod_fun f g == split (%x y. Pair (f x) (g y))"
+ Sigma_def: "Sigma A B == UN x:A. UN y:B x. {Pair x y}"
+
+abbreviation
+ Times :: "['a set, 'b set] => ('a * 'b) set" (infixr "<*>" 80)
+ "A <*> B == Sigma A (%_. B)"
+
+abbreviation (xsymbols)
+ Times1 (infixr "\<times>" 80)
+ "Times1 == Times"
+
+abbreviation (HTML output)
+ Times2 (infixr "\<times>" 80)
+ "Times2 == Times"
+
+
+subsubsection {* Concrete syntax *}
+
text {*
Patterns -- extends pre-defined type @{typ pttrn} used in
abstractions.
@@ -116,7 +140,6 @@
"" :: "pttrn => patterns" ("_")
"_patterns" :: "[pttrn, patterns] => patterns" ("_,/ _")
"@Sigma" ::"[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" 10)
- "@Times" ::"['a set, 'a => 'b set] => ('a * 'b) set" (infixr "<*>" 80)
translations
"(x, y)" == "Pair x y"
@@ -126,9 +149,7 @@
"_abs (Pair x y) t" => "%(x,y).t"
(* The last rule accommodates tuples in `case C ... (x,y) ... => ...'
The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *)
-
- "SIGMA x:A. B" => "Sigma A (%x. B)"
- "A <*> B" => "Sigma A (%_. B)"
+ "SIGMA x:A. B" == "Sigma A (%x. B)"
(* reconstructs pattern from (nested) splits, avoiding eta-contraction of body*)
(* works best with enclosing "let", if "let" does not avoid eta-contraction *)
@@ -157,7 +178,6 @@
end
*}
-
(* print "split f" as "\<lambda>(x,y). f x y" and "split (\<lambda>x. f x)" as "\<lambda>(x,y). f x y" *)
typed_print_translation {*
let
@@ -184,33 +204,11 @@
end
*}
-text{*Deleted x-symbol and html support using @{text"\<Sigma>"} (Sigma) because of the danger of confusion with Sum.*}
-
-syntax (xsymbols)
- "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \<times> _" [81, 80] 80)
-
-syntax (HTML output)
- "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \<times> _" [81, 80] 80)
-
-print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *}
-
-
-subsubsection {* Definitions *}
-
-defs
- Pair_def: "Pair a b == Abs_Prod(Pair_Rep a b)"
- fst_def: "fst p == THE a. EX b. p = (a, b)"
- snd_def: "snd p == THE b. EX a. p = (a, b)"
- split_def: "split == (%c p. c (fst p) (snd p))"
- curry_def: "curry == (%c x y. c (x,y))"
- prod_fun_def: "prod_fun f g == split(%x y.(f(x), g(y)))"
- Sigma_def: "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
-
subsubsection {* Lemmas and proof tool setup *}
lemma ProdI: "Pair_Rep a b : Prod"
- by (unfold Prod_def) blast
+ unfolding Prod_def by blast
lemma Pair_Rep_inject: "Pair_Rep a b = Pair_Rep a' b' ==> a = a' & b = b'"
apply (unfold Pair_Rep_def)
@@ -235,10 +233,10 @@
by (blast elim!: Pair_inject)
lemma fst_conv [simp]: "fst (a, b) = a"
- by (unfold fst_def) blast
+ unfolding fst_def by blast
lemma snd_conv [simp]: "snd (a, b) = b"
- by (unfold snd_def) blast
+ unfolding snd_def by blast
lemma fst_eqD: "fst (x, y) = a ==> x = a"
by simp
@@ -255,7 +253,7 @@
done
lemma PairE [cases type: *]: "(!!x y. p = (x, y) ==> Q) ==> Q"
- by (insert PairE_lemma [of p]) blast
+ using PairE_lemma [of p] by blast
ML {*
local val PairE = thm "PairE" in
@@ -281,12 +279,11 @@
proof
fix a b
assume "!!x. PROP P x"
- thus "PROP P (a, b)" .
+ then show "PROP P (a, b)" .
next
fix x
assume "!!a b. PROP P (a, b)"
- hence "PROP P (fst x, snd x)" .
- thus "PROP P x" by simp
+ from `PROP P (fst x, snd x)` show "PROP P x" by simp
qed
lemmas split_tupled_all = split_paired_all unit_all_eq2