merged

--- a/src/HOL/Fields.thy	Mon Feb 24 20:42:08 2014 +0100
+++ b/src/HOL/Fields.thy	Mon Feb 24 22:41:08 2014 +0100
@@ -1156,6 +1156,12 @@
   apply (simp add: order_less_imp_le)
 done
 
+lemma zero_le_divide_abs_iff [simp]: "(0 \<le> a / abs b) = (0 \<le> a | b = 0)" 
+by (auto simp: zero_le_divide_iff)
+
+lemma divide_le_0_abs_iff [simp]: "(a / abs b \<le> 0) = (a \<le> 0 | b = 0)" 
+by (auto simp: divide_le_0_iff)
+
 lemma field_le_mult_one_interval:
   assumes *: "\<And>z. \<lbrakk> 0 < z ; z < 1 \<rbrakk> \<Longrightarrow> z * x \<le> y"
   shows "x \<le> y"

--- a/src/HOL/Power.thy	Mon Feb 24 20:42:08 2014 +0100
+++ b/src/HOL/Power.thy	Mon Feb 24 22:41:08 2014 +0100
@@ -610,6 +610,11 @@
 
 subsection {* Miscellaneous rules *}
 
+lemma self_le_power:
+  fixes x::"'a::linordered_semidom" 
+  shows "1 \<le> x \<Longrightarrow> 0 < n \<Longrightarrow> x \<le> x ^ n"
+  by (metis gr_implies_not0 le_eq_less_or_eq less_one nat_le_linear power_increasing power_one_right)
+
 lemma power_eq_if: "p ^ m = (if m=0 then 1 else p * (p ^ (m - 1)))"
   unfolding One_nat_def by (cases m) simp_all
 

--- a/src/HOL/Real_Vector_Spaces.thy	Mon Feb 24 20:42:08 2014 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Mon Feb 24 22:41:08 2014 +0100
@@ -385,7 +385,7 @@
 apply (erule nonzero_of_real_inverse [symmetric])
 done
 
-lemma Reals_inverse [simp]:
+lemma Reals_inverse:
   fixes a :: "'a::{real_div_algebra, division_ring_inverse_zero}"
   shows "a \<in> Reals \<Longrightarrow> inverse a \<in> Reals"
 apply (auto simp add: Reals_def)
@@ -393,6 +393,11 @@
 apply (rule of_real_inverse [symmetric])
 done
 
+lemma Reals_inverse_iff [simp]: 
+  fixes x:: "'a :: {real_div_algebra, division_ring_inverse_zero}"
+  shows "inverse x \<in> \<real> \<longleftrightarrow> x \<in> \<real>"
+by (metis Reals_inverse inverse_inverse_eq)
+
 lemma nonzero_Reals_divide:
   fixes a b :: "'a::real_field"
   shows "\<lbrakk>a \<in> Reals; b \<in> Reals; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / b \<in> Reals"
@@ -427,6 +432,24 @@
   then show thesis ..
 qed
 
+lemma setsum_in_Reals: assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setsum f s \<in> \<real>"
+proof (cases "finite s")
+  case True then show ?thesis using assms
+    by (induct s rule: finite_induct) auto
+next
+  case False then show ?thesis using assms
+    by (metis Reals_0 setsum_infinite)
+qed
+
+lemma setprod_in_Reals: assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setprod f s \<in> \<real>"
+proof (cases "finite s")
+  case True then show ?thesis using assms
+    by (induct s rule: finite_induct) auto
+next
+  case False then show ?thesis using assms
+    by (metis Reals_1 setprod_infinite)
+qed
+
 lemma Reals_induct [case_names of_real, induct set: Reals]:
   "q \<in> \<real> \<Longrightarrow> (\<And>r. P (of_real r)) \<Longrightarrow> P q"
   by (rule Reals_cases) auto
@@ -719,6 +742,11 @@
   finally show ?thesis .
 qed
 
+lemma norm_triangle_mono: 
+  fixes a b :: "'a::real_normed_vector"
+  shows "\<lbrakk>norm a \<le> r; norm b \<le> s\<rbrakk> \<Longrightarrow> norm (a + b) \<le> r + s"
+by (metis add_mono_thms_linordered_semiring(1) norm_triangle_ineq order.trans)
+
 lemma abs_norm_cancel [simp]:
   fixes a :: "'a::real_normed_vector"
   shows "\<bar>norm a\<bar> = norm a"
@@ -802,6 +830,17 @@
   shows "norm (x ^ n) = norm x ^ n"
 by (induct n) (simp_all add: norm_mult)
 
+lemma setprod_norm:
+  fixes f :: "'a \<Rightarrow> 'b::{comm_semiring_1,real_normed_div_algebra}"
+  shows "setprod (\<lambda>x. norm(f x)) A = norm (setprod f A)"
+proof (cases "finite A")
+  case True then show ?thesis 
+    by (induct A rule: finite_induct) (auto simp: norm_mult)
+next
+  case False then show ?thesis
+    by (metis norm_one setprod.infinite) 
+qed
+
 
 subsection {* Metric spaces *}
 

--- a/src/HOL/Set_Interval.thy	Mon Feb 24 20:42:08 2014 +0100
+++ b/src/HOL/Set_Interval.thy	Mon Feb 24 22:41:08 2014 +0100
@@ -1459,6 +1459,14 @@
   finally show ?case .
 qed
 
+lemma setsum_last_plus: "n \<noteq> 0 \<Longrightarrow> (\<Sum>i = 0..n. f i) = f n + (\<Sum>i = 0..n - Suc 0. f i)"
+  using atLeastAtMostSuc_conv [of 0 "n - 1"]
+  by auto
+
+lemma nested_setsum_swap:
+     "(\<Sum>i = 0..n. (\<Sum>j = 0..<i. a i j)) = (\<Sum>j = 0..<n. \<Sum>i = Suc j..n. a i j)"
+  by (induction n) (auto simp: setsum_addf)
+
 
 subsection {* The formula for geometric sums *}
 
@@ -1565,6 +1573,14 @@
   show ?case by simp
 qed
 
+lemma nat_diff_setsum_reindex:
+  fixes x :: "'a::{comm_ring,monoid_mult}"
+  shows "(\<Sum>i=0..<n. f (n - Suc i)) = (\<Sum>i=0..<n. f i)"
+apply (subst setsum_reindex_cong [of "%i. n - Suc i" "{0..< n}"])
+apply (auto simp: inj_on_def)
+apply (rule_tac x="n - Suc x" in image_eqI, auto)
+done
+
 subsection {* Products indexed over intervals *}
 
 syntax
@@ -1649,4 +1665,15 @@
     by auto
 qed
 
+lemma setprod_power_distrib:
+  fixes f :: "'a \<Rightarrow> 'b::comm_semiring_1"
+  shows "setprod f A ^ n = setprod (\<lambda>x. (f x)^n) A"
+proof (cases "finite A") 
+  case True then show ?thesis 
+    by (induct A rule: finite_induct) (auto simp add: power_mult_distrib)
+next
+  case False then show ?thesis 
+    by (metis setprod_infinite power_one)
+qed
+
 end

--- a/src/HOL/Tools/Lifting/lifting_def.ML	Mon Feb 24 20:42:08 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Mon Feb 24 22:41:08 2014 +0100
@@ -265,7 +265,7 @@
     val unabs_def = unabs_all_def ctxt unfolded_def
   in  
     if body_type rty = body_type qty then 
-      SOME (simplify_code_eq ctxt unabs_def)
+      SOME (simplify_code_eq ctxt (unabs_def RS @{thm meta_eq_to_obj_eq}))
     else 
       let
         val thy = Proof_Context.theory_of ctxt
@@ -324,68 +324,74 @@
     simplify_code_eq ctxt abs_eq
   end
 
-fun define_code_using_abs_eq abs_eq_thm lthy =
-  if null (Logic.strip_imp_prems(prop_of abs_eq_thm)) then
-    (snd oo Local_Theory.note) ((Binding.empty, [Code.add_default_eqn_attrib]), [abs_eq_thm]) lthy
-  else
-    lthy
-  
-fun define_code_using_rep_eq opt_rep_eq_thm lthy = 
-  case opt_rep_eq_thm of
-    SOME rep_eq_thm =>   
-      let
-        val add_abs_eqn_attribute = 
-          Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abs_eqn thm) I)
-        val add_abs_eqn_attrib = Attrib.internal (K add_abs_eqn_attribute);
-      in
-        (snd oo Local_Theory.note) ((Binding.empty, [add_abs_eqn_attrib]), [rep_eq_thm]) lthy
-      end
-    | NONE => lthy
 
-fun has_constr ctxt quot_thm =
+fun register_code_eq_thy abs_eq_thm opt_rep_eq_thm (rty, qty) thy =
   let
-    val thy = Proof_Context.theory_of ctxt
-    val abs_fun = quot_thm_abs quot_thm
-  in
-    if is_Const abs_fun then
-      Code.is_constr thy ((fst o dest_Const) abs_fun)
-    else
-      false
-  end
+    fun no_abstr (t $ u) = no_abstr t andalso no_abstr u
+      | no_abstr (Abs (_, _, t)) = no_abstr t
+      | no_abstr (Const (name, _)) = not (Code.is_abstr thy name)
+      | no_abstr _ = true
+    fun is_valid_eq eqn = can (Code.assert_eqn thy) (mk_meta_eq eqn, true) 
+      andalso no_abstr (prop_of eqn)
+    fun is_valid_abs_eq abs_eq = can (Code.assert_abs_eqn thy NONE) (mk_meta_eq abs_eq)
 
-fun has_abstr ctxt quot_thm =
-  let
-    val thy = Proof_Context.theory_of ctxt
-    val abs_fun = quot_thm_abs quot_thm
   in
-    if is_Const abs_fun then
-      Code.is_abstr thy ((fst o dest_Const) abs_fun)
+    if is_valid_eq abs_eq_thm then
+      Code.add_default_eqn abs_eq_thm thy
     else
-      false
-  end
-
-fun define_code abs_eq_thm opt_rep_eq_thm (rty, qty) lthy =
-  let
-    val (rty_body, qty_body) = get_body_types (rty, qty)
-  in
-    if rty_body = qty_body then
-      if null (Logic.strip_imp_prems(prop_of abs_eq_thm)) then
-        (snd oo Local_Theory.note) ((Binding.empty, [Code.add_default_eqn_attrib]), [abs_eq_thm]) lthy
-      else
-        (snd oo Local_Theory.note) ((Binding.empty, [Code.add_default_eqn_attrib]), [the opt_rep_eq_thm]) lthy
-    else
-      let 
-        val body_quot_thm = Lifting_Term.prove_quot_thm lthy (rty_body, qty_body)
+      let
+        val (rty_body, qty_body) = get_body_types (rty, qty)
       in
-        if has_constr lthy body_quot_thm then
-          define_code_using_abs_eq abs_eq_thm lthy
-        else if has_abstr lthy body_quot_thm then
-          define_code_using_rep_eq opt_rep_eq_thm lthy
+        if rty_body = qty_body then
+         Code.add_default_eqn (the opt_rep_eq_thm) thy
         else
-          lthy
+          if is_some opt_rep_eq_thm andalso is_valid_abs_eq (the opt_rep_eq_thm)
+          then
+            Code.add_abs_eqn (the opt_rep_eq_thm) thy
+          else
+            thy
       end
   end
 
+local
+  fun encode_code_eq thy abs_eq opt_rep_eq (rty, qty) = 
+    let
+      fun mk_type typ = typ |> Logic.mk_type |> cterm_of thy |> Drule.mk_term
+    in
+      Conjunction.intr_balanced [abs_eq, (the_default TrueI opt_rep_eq), mk_type rty, mk_type qty]
+    end
+  
+  fun decode_code_eq thm =
+    let
+      val [abs_eq, rep_eq, rty, qty] = Conjunction.elim_balanced 4 thm
+      val opt_rep_eq = if Thm.eq_thm_prop (rep_eq, TrueI) then NONE else SOME rep_eq
+      fun dest_type typ = typ |> Drule.dest_term |> term_of |> Logic.dest_type
+    in
+      (abs_eq, opt_rep_eq, (dest_type rty, dest_type qty)) 
+    end
+  
+  fun register_encoded_code_eq thm thy =
+    let
+      val (abs_eq_thm, opt_rep_eq_thm, (rty, qty)) = decode_code_eq thm
+    in
+      register_code_eq_thy abs_eq_thm opt_rep_eq_thm (rty, qty) thy
+    end
+  
+  val register_code_eq_attribute = Thm.declaration_attribute
+    (fn thm => Context.mapping (register_encoded_code_eq thm) I)
+  val register_code_eq_attrib = Attrib.internal (K register_code_eq_attribute)
+in
+
+fun register_code_eq abs_eq_thm opt_rep_eq_thm (rty, qty) lthy =
+  let
+    val thy = Proof_Context.theory_of lthy
+    val encoded_code_eq = encode_code_eq thy abs_eq_thm opt_rep_eq_thm (rty, qty)
+  in
+    (snd oo Local_Theory.note) ((Binding.empty, [register_code_eq_attrib]), 
+      [encoded_code_eq]) lthy
+  end
+end
+            
 (*
   Defines an operation on an abstract type in terms of a corresponding operation 
     on a representation type.
@@ -434,7 +440,7 @@
       |> (case opt_rep_eq_thm of 
             SOME rep_eq_thm => (snd oo Local_Theory.note) ((rep_eq_thm_name, []), [rep_eq_thm])
             | NONE => I)
-      |> define_code abs_eq_thm opt_rep_eq_thm (rty_forced, qty)
+      |> register_code_eq abs_eq_thm opt_rep_eq_thm (rty_forced, qty)
   end
 
 fun mk_readable_rsp_thm_eq tm lthy =

--- a/src/HOL/Transcendental.thy	Mon Feb 24 20:42:08 2014 +0100
+++ b/src/HOL/Transcendental.thy	Mon Feb 24 22:41:08 2014 +0100
@@ -60,6 +60,23 @@
   apply (metis atLeastLessThan_iff diff_diff_cancel diff_less_Suc imageI le0 less_Suc_eq_le)
   done
 
+lemma power_diff_1_eq:
+  fixes x :: "'a::{comm_ring,monoid_mult}"
+  shows "n \<noteq> 0 \<Longrightarrow> x^n - 1 = (x - 1) * (\<Sum>i=0..<n. (x^i))"
+using lemma_realpow_diff_sumr2 [of x _ 1] 
+  by (cases n) auto
+
+lemma one_diff_power_eq':
+  fixes x :: "'a::{comm_ring,monoid_mult}"
+  shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i=0..<n. x^(n - Suc i))"
+using lemma_realpow_diff_sumr2 [of 1 _ x] 
+  by (cases n) auto
+
+lemma one_diff_power_eq:
+  fixes x :: "'a::{comm_ring,monoid_mult}"
+  shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i=0..<n. x^i)"
+by (metis one_diff_power_eq' [of n x] nat_diff_setsum_reindex)
+
 text{*Power series has a `circle` of convergence, i.e. if it sums for @{term
   x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*}
 

--- a/src/Pure/Isar/code.ML	Mon Feb 24 20:42:08 2014 +0100
+++ b/src/Pure/Isar/code.ML	Mon Feb 24 22:41:08 2014 +0100
@@ -24,6 +24,7 @@
   val mk_eqn: theory -> thm * bool -> thm * bool
   val mk_eqn_liberal: theory -> thm -> (thm * bool) option
   val assert_eqn: theory -> thm * bool -> thm * bool
+  val assert_abs_eqn: theory -> string option -> thm -> thm * string
   val const_typ_eqn: theory -> thm -> string * typ
   val expand_eta: theory -> int -> thm -> thm
   type cert
@@ -47,6 +48,8 @@
   val add_eqn: thm -> theory -> theory
   val add_nbe_eqn: thm -> theory -> theory
   val add_abs_eqn: thm -> theory -> theory
+  val add_abs_eqn_attribute: attribute
+  val add_abs_eqn_attrib: Attrib.src
   val add_default_eqn: thm -> theory -> theory
   val add_default_eqn_attribute: attribute
   val add_default_eqn_attrib: Attrib.src
@@ -546,7 +549,7 @@
       else error ("Type arguments do not satisfy sort constraints of abstype certificate.");
   in (thm, tyco) end;
 
-fun assert_eqn thy = error_thm (gen_assert_eqn thy true) thy;
+fun assert_eqn thy = gen_assert_eqn thy true;
 
 fun meta_rewrite thy = Local_Defs.meta_rewrite_rule (Proof_Context.init_global thy);
 
@@ -750,7 +753,7 @@
       let
         val thy = Proof_Context.theory_of ctxt;
         val eqns = burrow_fst (canonize_thms thy) raw_eqns;
-        val _ = map (assert_eqn thy) eqns;
+        val _ = map (error_thm (assert_eqn thy) thy) eqns;
         val (thms, propers) = split_list eqns;
         val _ = map (fn thm => if c = const_eqn thy thm then ()
           else error ("Wrong head of code equation,\nexpected constant "
@@ -1121,6 +1124,10 @@
 
 fun add_abs_eqn raw_thm thy = gen_add_abs_eqn (mk_abs_eqn thy raw_thm) thy;
 
+val add_abs_eqn_attribute = Thm.declaration_attribute
+  (fn thm => Context.mapping (add_abs_eqn thm) I);
+val add_abs_eqn_attrib = Attrib.internal (K add_abs_eqn_attribute);
+
 fun add_eqn_maybe_abs thm thy =
   case mk_eqn_maybe_abs thy thm
    of SOME (eqn, NONE) => gen_add_eqn false eqn thy