# HG changeset patch # User wenzelm # Date 1146595350 -7200 # Node ID e4fdeb32eadfc0fe1fb4960a643a13f247761799 # Parent 1724ec4032c5a1b4c2b9d031644f0cd5c99f2221 replaced syntax/translations by abbreviation; tuned proofs; tuned; diff -r 1724ec4032c5 -r e4fdeb32eadf src/HOL/Finite_Set.thy --- 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 ("\_" [1000] 999) + "\A == setsum (%x. x) A" + text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is written @{text"\x\A. e"}. *} @@ -831,31 +835,18 @@ "SUM x|P. t" => "setsum (%x. t) {x. P}" "\x|P. t" => "setsum (%x. t) {x. P}" -text{* Finally we abbreviate @{term"\x\A. x"} by @{text"\A"}. *} - -syntax - "_Setsum" :: "'a set => 'a::comm_monoid_mult" ("\_" [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 \ A \ (setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)" -using finB -proof (induct) + assumes "finite B" + and "B \ 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 \ 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: "\i. i\K \ f (i::'a) \ ((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 \ 'b::{pordered_cancel_ab_semigroup_add,comm_monoid_add}" -assumes fin_ne: "finite A" "A \ {}" -shows "(!!x. x:A \ f x < g x) \ setsum f A < setsum g A" -using fin_ne + fixes f :: "'a \ 'b::{pordered_cancel_ab_semigroup_add,comm_monoid_add}" + assumes "finite A" "A \ {}" + and "!!x. x:A \ 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: "\x\A. (0::'a::{pordered_ab_semigroup_add,comm_monoid_add}) \ f x" -shows "0 \ setsum f A" + assumes nn: "\x\A. (0::'a::{pordered_ab_semigroup_add,comm_monoid_add}) \ f x" + shows "0 \ setsum f A" proof (cases "finite A") case True thus ?thesis using nn - apply (induct set: Finites, auto) - apply (subgoal_tac "0 + 0 \ 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 \ 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: "\x\A. f x \ (0::'a::{pordered_ab_semigroup_add,comm_monoid_add})" -shows "setsum f A \ 0" + assumes np: "\x\A. f x \ (0::'a::{pordered_ab_semigroup_add,comm_monoid_add})" + shows "setsum f A \ 0" proof (cases "finite A") case True thus ?thesis using np - apply (induct set: Finites, auto) - apply (subgoal_tac "f x + setsum f F \ 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 \ 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 ("\_" [1000] 999) + "\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}" "\x|P. t" => "setprod (%x. t) {x. P}" -text{* Finally we abbreviate @{term"\x\A. x"} by @{text"\A"}. *} - -syntax - "_Setprod" :: "'a set => 'a::comm_monoid_mult" ("\_" [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) diff -r 1724ec4032c5 -r e4fdeb32eadf src/HOL/Integ/IntDef.thy --- 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" ("\") +abbreviation (xsymbols) + Nats1 ("\") + "\ == Nats" lemma of_nat_in_Nats [simp]: "of_nat n \ 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" ("\") +abbreviation (xsymbols) + Ints1 ("\") + "\ == Ints" lemma Ints_0 [simp]: "0 \ 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 \ \ ==> (!!z. q = of_int z ==> C) ==> C" -proof (simp add: Ints_def) - assume "!!z. q = of_int z ==> C" - assume "q \ range of_int" thus C .. +lemma Ints_cases [cases set: Ints]: + assumes "q \ \" + obtains (of_int) z where "q = of_int z" + unfolding Ints_def +proof - + from `q \ \` have "q \ 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) = (\x\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) = (\x\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) = (\x\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) = (\x\A. of_int(f x))" - apply (case_tac "finite A") + apply (cases "finite A") apply (erule finite_induct, auto) done diff -r 1724ec4032c5 -r e4fdeb32eadf src/HOL/Product_Type.thy --- 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 "\" 80) + "Times1 == Times" + +abbreviation (HTML output) + Times2 (infixr "\" 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 "\(x,y). f x y" and "split (\x. f x)" as "\(x,y). f x y" *) typed_print_translation {* let @@ -184,33 +204,11 @@ end *} -text{*Deleted x-symbol and html support using @{text"\"} (Sigma) because of the danger of confusion with Sum.*} - -syntax (xsymbols) - "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \ _" [81, 80] 80) - -syntax (HTML output) - "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \ _" [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