merged
authorwenzelm
Fri, 05 Oct 2012 14:51:33 +0200
changeset 49721 519cf2ac6c0e
parent 49720 6279490e0438 (diff)
parent 49712 a1bd8fe5131b (current diff)
child 49722 c91419b3a425
merged
--- 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)