--- a/src/HOL/BNF/Tools/bnf_comp.ML Fri Oct 05 14:32:56 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML Fri Oct 05 14:51:33 2012 +0200
@@ -13,10 +13,6 @@
type unfold_set
val empty_unfolds: unfold_set
- val map_unfolds_of: unfold_set -> thm list
- val rel_unfolds_of: unfold_set -> thm list
- val set_unfoldss_of: unfold_set -> thm list list
- val srel_unfolds_of: unfold_set -> thm list
val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) ->
((string * sort) list list -> (string * sort) list) -> typ -> unfold_set * Proof.context ->
@@ -64,11 +60,6 @@
add_to_unfolds (map_def_of_bnf bnf) (set_defs_of_bnf bnf) (rel_def_of_bnf bnf)
(srel_def_of_bnf bnf);
-val map_unfolds_of = #map_unfolds;
-val set_unfoldss_of = #set_unfoldss;
-val rel_unfolds_of = #rel_unfolds;
-val srel_unfolds_of = #srel_unfolds;
-
val bdTN = "bdT";
fun mk_killN n = "_kill" ^ string_of_int n;
@@ -185,7 +176,8 @@
else
map (fn goal =>
Skip_Proof.prove lthy [] [] goal
- (fn {context, ...} => (mk_comp_set_alt_tac context (collect_set_natural_of_bnf outer)))
+ (fn {context = ctxt, prems = _} =>
+ mk_comp_set_alt_tac ctxt (collect_set_natural_of_bnf outer))
|> Thm.close_derivation)
(map2 (curry (HOLogic.mk_Trueprop o HOLogic.mk_eq)) sets sets_alt);
@@ -206,8 +198,8 @@
val single_set_bd_thmss =
map ((fn f => map f (0 upto olive - 1)) o single_set_bd_thm) (0 upto ilive - 1);
in
- map2 (fn set_alt => fn single_set_bds => fn {context, ...} =>
- mk_comp_set_bd_tac context set_alt single_set_bds)
+ map2 (fn set_alt => fn single_set_bds => fn {context = ctxt, prems = _} =>
+ mk_comp_set_bd_tac ctxt set_alt single_set_bds)
set_alt_thms single_set_bd_thmss
end;
@@ -218,7 +210,7 @@
val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
in
Skip_Proof.prove lthy [] [] goal
- (fn {context, ...} => mk_comp_in_alt_tac context set_alt_thms)
+ (fn {context = ctxt, prems = _} => mk_comp_in_alt_tac ctxt set_alt_thms)
|> Thm.close_derivation
end;
@@ -264,7 +256,7 @@
|> minimize_wits
|> map (fn (frees, t) => fold absfree frees t);
- fun wit_tac {context = ctxt, ...} =
+ fun wit_tac {context = ctxt, prems = _} =
mk_comp_wit_tac ctxt (wit_thms_of_bnf outer) (collect_set_natural_of_bnf outer)
(maps wit_thms_of_bnf inners);
@@ -314,11 +306,11 @@
(Library.foldr1 (uncurry mk_csum) (map (mk_card_of o HOLogic.mk_UNIV) killedAs)) bnf_bd;
fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
- fun map_comp_tac {context, ...} =
- unfold_thms_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
+ fun map_comp_tac {context = ctxt, prems = _} =
+ unfold_thms_tac ctxt ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
rtac refl 1;
- fun map_cong_tac {context, ...} =
- mk_kill_map_cong_tac context n (live - n) (map_cong_of_bnf bnf);
+ fun map_cong_tac {context = ctxt, prems = _} =
+ mk_kill_map_cong_tac ctxt n (live - n) (map_cong_of_bnf bnf);
val set_natural_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_natural_of_bnf bnf));
fun bd_card_order_tac _ = mk_kill_bd_card_order_tac n (bd_card_order_of_bnf bnf);
fun bd_cinfinite_tac _ = mk_kill_bd_cinfinite_tac (bd_Cinfinite_of_bnf bnf);
@@ -408,11 +400,11 @@
val bd = mk_bd_of_bnf Ds As bnf;
fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
- fun map_comp_tac {context, ...} =
- unfold_thms_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
+ fun map_comp_tac {context = ctxt, prems = _} =
+ unfold_thms_tac ctxt ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
rtac refl 1;
- fun map_cong_tac {context, ...} =
- rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac context 1);
+ fun map_cong_tac {context = ctxt, prems = _} =
+ rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);
val set_natural_tacs =
if ! quick_and_dirty then
replicate (n + live) (K all_tac)
@@ -496,8 +488,8 @@
fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
fun map_comp_tac _ = rtac (map_comp_of_bnf bnf) 1;
- fun map_cong_tac {context, ...} =
- rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac context 1);
+ fun map_cong_tac {context = ctxt, prems = _} =
+ rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);
val set_natural_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_natural_of_bnf bnf));
fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1;
fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1;
@@ -603,10 +595,10 @@
val (Bs, _) = apfst (map TFree)
(Variable.invent_types (replicate live HOLogic.typeS) lthy1);
- val map_unfolds = map_unfolds_of unfold_set;
- val set_unfoldss = set_unfoldss_of unfold_set;
- val rel_unfolds = rel_unfolds_of unfold_set;
- val srel_unfolds = srel_unfolds_of unfold_set;
+ val map_unfolds = #map_unfolds unfold_set;
+ val set_unfoldss = #set_unfoldss unfold_set;
+ val rel_unfolds = #rel_unfolds unfold_set;
+ val srel_unfolds = #srel_unfolds unfold_set;
val expand_maps =
fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) map_unfolds);
--- a/src/HOL/Big_Operators.thy Fri Oct 05 14:32:56 2012 +0200
+++ b/src/HOL/Big_Operators.thy Fri Oct 05 14:51:33 2012 +0200
@@ -447,6 +447,15 @@
setsum f A + setsum f B - setsum f (A Int B)"
by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
+lemma setsum_Un2:
+ assumes "finite (A \<union> B)"
+ shows "setsum f (A \<union> B) = setsum f (A - B) + setsum f (B - A) + setsum f (A \<inter> B)"
+proof -
+ have "A \<union> B = A - B \<union> (B - A) \<union> A \<inter> B"
+ by auto
+ with assms show ?thesis by simp (subst setsum_Un_disjoint, auto)+
+qed
+
lemma (in comm_monoid_add) setsum_eq_general_reverses:
assumes fS: "finite S" and fT: "finite T"
and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
@@ -1087,6 +1096,15 @@
= setprod f A * setprod f B / setprod f (A Int B)"
by (subst setprod_Un_Int [symmetric], auto)
+lemma setprod_Un2:
+ assumes "finite (A \<union> B)"
+ shows "setprod f (A \<union> B) = setprod f (A - B) * setprod f (B - A) * setprod f (A \<inter> B)"
+proof -
+ have "A \<union> B = A - B \<union> (B - A) \<union> A \<inter> B"
+ by auto
+ with assms show ?thesis by simp (subst setprod_Un_disjoint, auto)+
+qed
+
lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
(setprod f (A - {a}) :: 'a :: {field}) =
(if a:A then setprod f A / f a else setprod f A)"
--- a/src/HOL/Library/Multiset.thy Fri Oct 05 14:32:56 2012 +0200
+++ b/src/HOL/Library/Multiset.thy Fri Oct 05 14:51:33 2012 +0200
@@ -872,6 +872,8 @@
qed
qed
+declare image_mset.identity [simp]
+
subsection {* Alternative representations *}
--- a/src/HOL/Number_Theory/UniqueFactorization.thy Fri Oct 05 14:32:56 2012 +0200
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy Fri Oct 05 14:51:33 2012 +0200
@@ -30,72 +30,52 @@
count M x > 0
*)
-
-(* useful facts *)
-
-lemma setsum_Un2: "finite (A Un B) \<Longrightarrow>
- setsum f (A Un B) = setsum f (A - B) + setsum f (B - A) +
- setsum f (A Int B)"
- apply (subgoal_tac "A Un B = (A - B) Un (B - A) Un (A Int B)")
- apply (erule ssubst)
- apply (subst setsum_Un_disjoint)
- apply auto
- apply (subst setsum_Un_disjoint)
- apply auto
- done
-
-lemma setprod_Un2: "finite (A Un B) \<Longrightarrow>
- setprod f (A Un B) = setprod f (A - B) * setprod f (B - A) *
- setprod f (A Int B)"
- apply (subgoal_tac "A Un B = (A - B) Un (B - A) Un (A Int B)")
- apply (erule ssubst)
- apply (subst setprod_Un_disjoint)
- apply auto
- apply (subst setprod_Un_disjoint)
- apply auto
- done
-
(* Here is a version of set product for multisets. Is it worth moving
to multiset.thy? If so, one should similarly define msetsum for abelian
semirings, using of_nat. Also, is it worth developing bounded quantifiers
"ALL i :# M. P i"?
*)
-definition msetprod :: "('a => ('b::{power,comm_monoid_mult})) => 'a multiset => 'b" where
- "msetprod f M == setprod (%x. (f x)^(count M x)) (set_of M)"
+definition (in comm_monoid_mult) msetprod :: "'a multiset \<Rightarrow> 'a"
+where
+ "msetprod M = setprod (\<lambda>x. x ^ count M x) (set_of M)"
+
+abbreviation (in comm_monoid_mult) msetprod_image :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b multiset \<Rightarrow> 'a"
+where
+ "msetprod_image f M \<equiv> msetprod (image_mset f M)"
syntax
- "_msetprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"
+ "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
("(3PROD _:#_. _)" [0, 51, 10] 10)
translations
- "PROD i :# A. b" == "CONST msetprod (%i. b) A"
+ "PROD i :# A. b" == "CONST msetprod_image (\<lambda>i. b) A"
-lemma msetprod_empty: "msetprod f {#} = 1"
+lemma msetprod_empty: "msetprod {#} = 1"
by (simp add: msetprod_def)
-lemma msetprod_singleton: "msetprod f {#x#} = f x"
+lemma msetprod_singleton: "msetprod {#x#} = x"
by (simp add: msetprod_def)
-lemma msetprod_Un: "msetprod f (A+B) = msetprod f A * msetprod f B"
+lemma msetprod_Un: "msetprod (A + B) = msetprod A * msetprod B"
apply (simp add: msetprod_def power_add)
apply (subst setprod_Un2)
apply auto
apply (subgoal_tac
- "(PROD x:set_of A - set_of B. f x ^ count A x * f x ^ count B x) =
- (PROD x:set_of A - set_of B. f x ^ count A x)")
+ "(PROD x:set_of A - set_of B. x ^ count A x * x ^ count B x) =
+ (PROD x:set_of A - set_of B. x ^ count A x)")
apply (erule ssubst)
apply (subgoal_tac
- "(PROD x:set_of B - set_of A. f x ^ count A x * f x ^ count B x) =
- (PROD x:set_of B - set_of A. f x ^ count B x)")
+ "(PROD x:set_of B - set_of A. x ^ count A x * x ^ count B x) =
+ (PROD x:set_of B - set_of A. x ^ count B x)")
apply (erule ssubst)
- apply (subgoal_tac "(PROD x:set_of A. f x ^ count A x) =
- (PROD x:set_of A - set_of B. f x ^ count A x) *
- (PROD x:set_of A Int set_of B. f x ^ count A x)")
+ apply (subgoal_tac "(PROD x:set_of A. x ^ count A x) =
+ (PROD x:set_of A - set_of B. x ^ count A x) *
+ (PROD x:set_of A Int set_of B. x ^ count A x)")
apply (erule ssubst)
- apply (subgoal_tac "(PROD x:set_of B. f x ^ count B x) =
- (PROD x:set_of B - set_of A. f x ^ count B x) *
- (PROD x:set_of A Int set_of B. f x ^ count B x)")
+ apply (subgoal_tac "(PROD x:set_of B. x ^ count B x) =
+ (PROD x:set_of B - set_of A. x ^ count B x) *
+ (PROD x:set_of A Int set_of B. x ^ count B x)")
apply (erule ssubst)
apply (subst setprod_timesf)
apply (force simp add: mult_ac)
@@ -222,7 +202,8 @@
apply (frule multiset_prime_factorization_exists)
apply clarify
apply (rule theI)
- apply (insert multiset_prime_factorization_unique, blast)+
+ apply (insert multiset_prime_factorization_unique)
+ apply auto
done
@@ -363,29 +344,32 @@
by auto
lemma prime_factorization_unique_nat:
- "S = { (p::nat) . f p > 0} \<Longrightarrow> finite S \<Longrightarrow> (ALL p : S. prime p) \<Longrightarrow>
- n = (PROD p : S. p^(f p)) \<Longrightarrow>
- S = prime_factors n & (ALL p. f p = multiplicity p n)"
- apply (subgoal_tac "multiset_prime_factorization n = Abs_multiset f")
- apply (unfold prime_factors_nat_def multiplicity_nat_def)
- apply (simp add: set_of_def Abs_multiset_inverse multiset_def)
- apply (unfold multiset_prime_factorization_def)
- apply (subgoal_tac "n > 0")
- prefer 2
- apply force
- apply (subst if_P, assumption)
- apply (rule the1_equality)
- apply (rule ex_ex1I)
- apply (rule multiset_prime_factorization_exists, assumption)
- apply (rule multiset_prime_factorization_unique)
- apply force
- apply force
- apply force
- unfolding set_of_def msetprod_def
- apply (subgoal_tac "f : multiset")
- apply (auto simp only: Abs_multiset_inverse)
- unfolding multiset_def apply force
- done
+ fixes f :: "nat \<Rightarrow> _"
+ assumes S_eq: "S = {p. 0 < f p}" and "finite S"
+ and "\<forall>p\<in>S. prime p" "n = (\<Prod>p\<in>S. p ^ f p)"
+ shows "S = prime_factors n \<and> (\<forall>p. f p = multiplicity p n)"
+proof -
+ from assms have "f \<in> multiset"
+ by (auto simp add: multiset_def)
+ moreover from assms have "n > 0" by force
+ ultimately have "multiset_prime_factorization n = Abs_multiset f"
+ apply (unfold multiset_prime_factorization_def)
+ apply (subst if_P, assumption)
+ apply (rule the1_equality)
+ apply (rule ex_ex1I)
+ apply (rule multiset_prime_factorization_exists, assumption)
+ apply (rule multiset_prime_factorization_unique)
+ apply force
+ apply force
+ apply force
+ using assms
+ apply (simp add: Abs_multiset_inverse set_of_def msetprod_def)
+ done
+ with `f \<in> multiset` have "count (multiset_prime_factorization n) = f"
+ by (simp add: Abs_multiset_inverse)
+ with S_eq show ?thesis
+ by (simp add: set_of_def multiset_def prime_factors_nat_def multiplicity_nat_def)
+qed
lemma prime_factors_characterization_nat: "S = {p. 0 < f (p::nat)} \<Longrightarrow>
finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
@@ -898,3 +882,4 @@
done
end
+
--- a/src/HOL/Tools/SMT/z3_interface.ML Fri Oct 05 14:32:56 2012 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML Fri Oct 05 14:51:33 2012 +0200
@@ -127,9 +127,10 @@
(** basic and additional constructors **)
-fun mk_builtin_typ _ (Sym ("bool", _)) = SOME @{typ bool}
+fun mk_builtin_typ _ (Sym ("Bool", _)) = SOME @{typ bool}
| mk_builtin_typ _ (Sym ("Int", _)) = SOME @{typ int}
- | mk_builtin_typ _ (Sym ("int", _)) = SOME @{typ int} (*FIXME: delete*)
+ | mk_builtin_typ _ (Sym ("bool", _)) = SOME @{typ bool} (*FIXME: legacy*)
+ | mk_builtin_typ _ (Sym ("int", _)) = SOME @{typ int} (*FIXME: legacy*)
| mk_builtin_typ ctxt sym = chained_mk_builtin_typ (get_mk_builtins ctxt) sym
fun mk_builtin_num _ i @{typ int} = SOME (Numeral.mk_cnumber @{ctyp int} i)