# HG changeset patch
# User haftmann
# Date 1235421525 -3600
# Node ID c5920259850c3e7559c7600b34bc76bb30d52ce0
# Parent  ff5b4900d9a5b111774b3d6a3a7f4a31b569ea14# Parent  f3043dafef5faccad1ac2a6d3468d0eb78615ed8
merged

diff -r f3043dafef5f -r c5920259850c src/HOL/Fact.thy
--- a/src/HOL/Fact.thy	Mon Feb 23 21:38:36 2009 +0100
+++ b/src/HOL/Fact.thy	Mon Feb 23 21:38:45 2009 +0100
@@ -7,7 +7,7 @@
 header{*Factorial Function*}
 
 theory Fact
-imports Nat
+imports Main
 begin
 
 consts fact :: "nat => nat"
diff -r f3043dafef5f -r c5920259850c src/HOL/Library/Euclidean_Space.thy
--- a/src/HOL/Library/Euclidean_Space.thy	Mon Feb 23 21:38:36 2009 +0100
+++ b/src/HOL/Library/Euclidean_Space.thy	Mon Feb 23 21:38:45 2009 +0100
@@ -1010,11 +1010,6 @@
 
 lemma dist_le_0: "dist x y <= 0 \<longleftrightarrow> x = y" by norm 
 
-instantiation "^" :: (monoid_add,type) monoid_add
-begin
-  instance by (intro_classes)
-end
-
 lemma setsum_eq: "setsum f S = (\<chi> i. setsum (\<lambda>x. (f x)$i ) S)"
   apply vector
   apply auto
diff -r f3043dafef5f -r c5920259850c src/HOL/Library/Inner_Product.thy
--- a/src/HOL/Library/Inner_Product.thy	Mon Feb 23 21:38:36 2009 +0100
+++ b/src/HOL/Library/Inner_Product.thy	Mon Feb 23 21:38:45 2009 +0100
@@ -21,19 +21,10 @@
 begin
 
 lemma inner_zero_left [simp]: "inner 0 x = 0"
-proof -
-  have "inner 0 x = inner (0 + 0) x" by simp
-  also have "\<dots> = inner 0 x + inner 0 x" by (rule inner_left_distrib)
-  finally show "inner 0 x = 0" by simp
-qed
+  using inner_left_distrib [of 0 0 x] by simp
 
 lemma inner_minus_left [simp]: "inner (- x) y = - inner x y"
-proof -
-  have "inner (- x) y + inner x y = inner (- x + x) y"
-    by (rule inner_left_distrib [symmetric])
-  also have "\<dots> = - inner x y + inner x y" by simp
-  finally show "inner (- x) y = - inner x y" by simp
-qed
+  using inner_left_distrib [of x "- x" y] by simp
 
 lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z"
   by (simp add: diff_minus inner_left_distrib)
diff -r f3043dafef5f -r c5920259850c src/HOL/Library/Permutations.thy
--- a/src/HOL/Library/Permutations.thy	Mon Feb 23 21:38:36 2009 +0100
+++ b/src/HOL/Library/Permutations.thy	Mon Feb 23 21:38:45 2009 +0100
@@ -6,7 +6,7 @@
 header {* Permutations, both general and specifically on finite sets.*}
 
 theory Permutations
-imports Main Finite_Cartesian_Product Parity 
+imports Main Finite_Cartesian_Product Parity Fact
 begin
 
   (* Why should I import Main just to solve the Typerep problem! *)
diff -r f3043dafef5f -r c5920259850c src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Mon Feb 23 21:38:36 2009 +0100
+++ b/src/HOL/Library/Polynomial.thy	Mon Feb 23 21:38:45 2009 +0100
@@ -1020,6 +1020,16 @@
 lemma mod_smult_left: "(smult a x) mod y = smult a (x mod y)"
   by (rule mod_poly_eq, rule pdivmod_rel_smult_left, rule pdivmod_rel)
 
+lemma poly_div_minus_left [simp]:
+  fixes x y :: "'a::field poly"
+  shows "(- x) div y = - (x div y)"
+  using div_smult_left [of "- 1::'a"] by simp
+
+lemma poly_mod_minus_left [simp]:
+  fixes x y :: "'a::field poly"
+  shows "(- x) mod y = - (x mod y)"
+  using mod_smult_left [of "- 1::'a"] by simp
+
 lemma pdivmod_rel_smult_right:
   "\<lbrakk>a \<noteq> 0; pdivmod_rel x y q r\<rbrakk>
     \<Longrightarrow> pdivmod_rel x (smult a y) (smult (inverse a) q) r"
@@ -1032,6 +1042,17 @@
 lemma mod_smult_right: "a \<noteq> 0 \<Longrightarrow> x mod (smult a y) = x mod y"
   by (rule mod_poly_eq, erule pdivmod_rel_smult_right, rule pdivmod_rel)
 
+lemma poly_div_minus_right [simp]:
+  fixes x y :: "'a::field poly"
+  shows "x div (- y) = - (x div y)"
+  using div_smult_right [of "- 1::'a"]
+  by (simp add: nonzero_inverse_minus_eq)
+
+lemma poly_mod_minus_right [simp]:
+  fixes x y :: "'a::field poly"
+  shows "x mod (- y) = x mod y"
+  using mod_smult_right [of "- 1::'a"] by simp
+
 lemma pdivmod_rel_mult:
   "\<lbrakk>pdivmod_rel x y q r; pdivmod_rel q z q' r'\<rbrakk>
     \<Longrightarrow> pdivmod_rel x (y * z) q' (y * r' + r)"
diff -r f3043dafef5f -r c5920259850c src/HOL/Plain.thy
--- a/src/HOL/Plain.thy	Mon Feb 23 21:38:36 2009 +0100
+++ b/src/HOL/Plain.thy	Mon Feb 23 21:38:45 2009 +0100
@@ -1,7 +1,7 @@
 header {* Plain HOL *}
 
 theory Plain
-imports Datatype FunDef Record Extraction Divides Fact
+imports Datatype FunDef Record Extraction Divides
 begin
 
 text {*
diff -r f3043dafef5f -r c5920259850c src/HOL/RealVector.thy
--- a/src/HOL/RealVector.thy	Mon Feb 23 21:38:36 2009 +0100
+++ b/src/HOL/RealVector.thy	Mon Feb 23 21:38:45 2009 +0100
@@ -46,8 +46,10 @@
 
 locale vector_space =
   fixes scale :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b"
-  assumes scale_right_distrib: "scale a (x + y) = scale a x + scale a y"
-  and scale_left_distrib: "scale (a + b) x = scale a x + scale b x"
+  assumes scale_right_distrib [algebra_simps]:
+    "scale a (x + y) = scale a x + scale a y"
+  and scale_left_distrib [algebra_simps]:
+    "scale (a + b) x = scale a x + scale b x"
   and scale_scale [simp]: "scale a (scale b x) = scale (a * b) x"
   and scale_one [simp]: "scale 1 x = x"
 begin
@@ -58,7 +60,8 @@
 
 lemma scale_zero_left [simp]: "scale 0 x = 0"
   and scale_minus_left [simp]: "scale (- a) x = - (scale a x)"
-  and scale_left_diff_distrib: "scale (a - b) x = scale a x - scale b x"
+  and scale_left_diff_distrib [algebra_simps]:
+        "scale (a - b) x = scale a x - scale b x"
 proof -
   interpret s: additive "\<lambda>a. scale a x"
     proof qed (rule scale_left_distrib)
@@ -69,7 +72,8 @@
 
 lemma scale_zero_right [simp]: "scale a 0 = 0"
   and scale_minus_right [simp]: "scale a (- x) = - (scale a x)"
-  and scale_right_diff_distrib: "scale a (x - y) = scale a x - scale a y"
+  and scale_right_diff_distrib [algebra_simps]:
+        "scale a (x - y) = scale a x - scale a y"
 proof -
   interpret s: additive "\<lambda>x. scale a x"
     proof qed (rule scale_right_distrib)
@@ -135,21 +139,11 @@
 
 end
 
-instantiation real :: scaleR
-begin
-
-definition
-  real_scaleR_def [simp]: "scaleR a x = a * x"
-
-instance ..
-
-end
-
 class real_vector = scaleR + ab_group_add +
   assumes scaleR_right_distrib: "scaleR a (x + y) = scaleR a x + scaleR a y"
   and scaleR_left_distrib: "scaleR (a + b) x = scaleR a x + scaleR b x"
-  and scaleR_scaleR [simp]: "scaleR a (scaleR b x) = scaleR (a * b) x"
-  and scaleR_one [simp]: "scaleR 1 x = x"
+  and scaleR_scaleR: "scaleR a (scaleR b x) = scaleR (a * b) x"
+  and scaleR_one: "scaleR 1 x = x"
 
 interpretation real_vector!:
   vector_space "scaleR :: real \<Rightarrow> 'a \<Rightarrow> 'a::real_vector"
@@ -185,15 +179,16 @@
 
 class real_field = real_div_algebra + field
 
-instance real :: real_field
-apply (intro_classes, unfold real_scaleR_def)
-apply (rule right_distrib)
-apply (rule left_distrib)
-apply (rule mult_assoc [symmetric])
-apply (rule mult_1_left)
-apply (rule mult_assoc)
-apply (rule mult_left_commute)
-done
+instantiation real :: real_field
+begin
+
+definition
+  real_scaleR_def [simp]: "scaleR a x = a * x"
+
+instance proof
+qed (simp_all add: algebra_simps)
+
+end
 
 interpretation scaleR_left!: additive "(\<lambda>a. scaleR a x::'a::real_vector)"
 proof qed (rule scaleR_left_distrib)
@@ -307,7 +302,7 @@
 
 definition
   Reals :: "'a::real_algebra_1 set" where
-  [code del]: "Reals \<equiv> range of_real"
+  [code del]: "Reals = range of_real"
 
 notation (xsymbols)
   Reals  ("\<real>")
@@ -421,16 +416,6 @@
 class norm =
   fixes norm :: "'a \<Rightarrow> real"
 
-instantiation real :: norm
-begin
-
-definition
-  real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>"
-
-instance ..
-
-end
-
 class sgn_div_norm = scaleR + norm + sgn +
   assumes sgn_div_norm: "sgn x = x /\<^sub>R norm x"
 
@@ -462,7 +447,13 @@
   thus "norm (1::'a) = 1" by simp
 qed
 
-instance real :: real_normed_field
+instantiation real :: real_normed_field
+begin
+
+definition
+  real_norm_def [simp]: "norm r = \<bar>r\<bar>"
+
+instance
 apply (intro_classes, unfold real_norm_def real_scaleR_def)
 apply (simp add: real_sgn_def)
 apply (rule abs_ge_zero)
@@ -472,6 +463,8 @@
 apply (rule abs_mult)
 done
 
+end
+
 lemma norm_zero [simp]: "norm (0::'a::real_normed_vector) = 0"
 by simp
 
diff -r f3043dafef5f -r c5920259850c src/Tools/code/code_wellsorted.ML
--- a/src/Tools/code/code_wellsorted.ML	Mon Feb 23 21:38:36 2009 +0100
+++ b/src/Tools/code/code_wellsorted.ML	Mon Feb 23 21:38:45 2009 +0100
@@ -166,11 +166,13 @@
   in
     vardeps_data
     |> (apsnd o apsnd) (insert (op =) inst)
+    |> fold_index (fn (k, classes) =>
+         apfst (Vargraph.new_node ((Inst (class, tyco), k), ([] ,[])))
+         ) classess
     |> fold (fn superclass => assert_inst thy arities eqngr (superclass, tyco)) superclasses
     |> fold (assert_fun thy arities eqngr) inst_params
     |> fold_index (fn (k, classes) =>
-         apfst (Vargraph.new_node ((Inst (class, tyco), k), ([] ,[])))
-         #> add_classes thy arities eqngr (Inst (class, tyco), k) classes
+         add_classes thy arities eqngr (Inst (class, tyco), k) classes
          #> fold (fn superclass =>
              add_dep thy arities eqngr (Inst (superclass, tyco), k)
              (Inst (class, tyco), k)) superclasses