# HG changeset patch
# User wenzelm
# Date 1445110938 -7200
# Node ID 79900ab5d50a5bd4c8ef76e7dcd4437c0fc8113e
# Parent  a4c0de1df3d8789da6774f71416fbdbd1295694a# Parent  d35ff80f27fb3c184daeffed76acf47f0fdea180
merged

diff -r d35ff80f27fb -r 79900ab5d50a src/Doc/Prog_Prove/Basics.thy
--- a/src/Doc/Prog_Prove/Basics.thy	Sat Oct 17 21:26:14 2015 +0200
+++ b/src/Doc/Prog_Prove/Basics.thy	Sat Oct 17 21:42:18 2015 +0200
@@ -87,7 +87,7 @@
 the formula
 @{text"A\<^sub>1 \<Longrightarrow> A\<^sub>2 \<Longrightarrow> A\<^sub>3"} means @{text "A\<^sub>1 \<Longrightarrow> (A\<^sub>2 \<Longrightarrow> A\<^sub>3)"}.
 The (Isabelle-specific\footnote{To display implications in this style in
-Isabelle/jedit you need to set Plugins $>$ Plugin Options $>$ Isabelle/General $>$ Print Mode to ``\texttt{brackets}'' and restart.}) notation \mbox{@{text"\<lbrakk> A\<^sub>1; \<dots>; A\<^sub>n \<rbrakk> \<Longrightarrow> A"}}
+Isabelle/jEdit you need to set Plugins $>$ Plugin Options $>$ Isabelle/General $>$ Print Mode to ``\texttt{brackets}'' and restart.}) notation \mbox{@{text"\<lbrakk> A\<^sub>1; \<dots>; A\<^sub>n \<rbrakk> \<Longrightarrow> A"}}
 is short for the iterated implication \mbox{@{text"A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> A"}}.
 Sometimes we also employ inference rule notation:
 \inferrule{\mbox{@{text "A\<^sub>1"}}\\ \mbox{@{text "\<dots>"}}\\ \mbox{@{text "A\<^sub>n"}}}
diff -r d35ff80f27fb -r 79900ab5d50a src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sat Oct 17 21:26:14 2015 +0200
+++ b/src/HOL/Divides.thy	Sat Oct 17 21:42:18 2015 +0200
@@ -813,6 +813,9 @@
 
 subsection \<open>Division on @{typ nat}\<close>
 
+context
+begin
+
 text \<open>
   We define @{const divide} and @{const mod} on @{typ nat} by means
   of a characteristic relation with two input arguments
@@ -827,7 +830,7 @@
 
 text \<open>@{const divmod_nat_rel} is total:\<close>
 
-lemma divmod_nat_rel_ex:
+qualified lemma divmod_nat_rel_ex:
   obtains q r where "divmod_nat_rel m n (q, r)"
 proof (cases "n = 0")
   case True  with that show thesis
@@ -860,7 +863,7 @@
 
 text \<open>@{const divmod_nat_rel} is injective:\<close>
 
-lemma divmod_nat_rel_unique:
+qualified lemma divmod_nat_rel_unique:
   assumes "divmod_nat_rel m n qr"
     and "divmod_nat_rel m n qr'"
   shows "qr = qr'"
@@ -887,10 +890,10 @@
   means of @{const divmod_nat_rel}:
 \<close>
 
-definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
+qualified definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
   "divmod_nat m n = (THE qr. divmod_nat_rel m n qr)"
 
-lemma divmod_nat_rel_divmod_nat:
+qualified lemma divmod_nat_rel_divmod_nat:
   "divmod_nat_rel m n (divmod_nat m n)"
 proof -
   from divmod_nat_rel_ex
@@ -899,63 +902,65 @@
   by (auto simp add: divmod_nat_def intro: theI elim: divmod_nat_rel_unique)
 qed
 
-lemma divmod_nat_unique:
+qualified lemma divmod_nat_unique:
   assumes "divmod_nat_rel m n qr"
   shows "divmod_nat m n = qr"
   using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
 
+qualified lemma divmod_nat_zero: "divmod_nat m 0 = (0, m)"
+  by (simp add: Divides.divmod_nat_unique divmod_nat_rel_def)
+
+qualified lemma divmod_nat_zero_left: "divmod_nat 0 n = (0, 0)"
+  by (simp add: Divides.divmod_nat_unique divmod_nat_rel_def)
+
+qualified lemma divmod_nat_base: "m < n \<Longrightarrow> divmod_nat m n = (0, m)"
+  by (simp add: divmod_nat_unique divmod_nat_rel_def)
+
+qualified lemma divmod_nat_step:
+  assumes "0 < n" and "n \<le> m"
+  shows "divmod_nat m n = apfst Suc (divmod_nat (m - n) n)"
+proof (rule divmod_nat_unique)
+  have "divmod_nat_rel (m - n) n (divmod_nat (m - n) n)"
+    by (fact divmod_nat_rel_divmod_nat)
+  then show "divmod_nat_rel m n (apfst Suc (divmod_nat (m - n) n))"
+    unfolding divmod_nat_rel_def using assms by auto
+qed
+
+end
+  
 instantiation nat :: semiring_div
 begin
 
 definition divide_nat where
-  div_nat_def: "m div n = fst (divmod_nat m n)"
+  div_nat_def: "m div n = fst (Divides.divmod_nat m n)"
 
 definition mod_nat where
-  "m mod n = snd (divmod_nat m n)"
+  "m mod n = snd (Divides.divmod_nat m n)"
 
 lemma fst_divmod_nat [simp]:
-  "fst (divmod_nat m n) = m div n"
+  "fst (Divides.divmod_nat m n) = m div n"
   by (simp add: div_nat_def)
 
 lemma snd_divmod_nat [simp]:
-  "snd (divmod_nat m n) = m mod n"
+  "snd (Divides.divmod_nat m n) = m mod n"
   by (simp add: mod_nat_def)
 
 lemma divmod_nat_div_mod:
-  "divmod_nat m n = (m div n, m mod n)"
+  "Divides.divmod_nat m n = (m div n, m mod n)"
   by (simp add: prod_eq_iff)
 
 lemma div_nat_unique:
   assumes "divmod_nat_rel m n (q, r)"
   shows "m div n = q"
-  using assms by (auto dest!: divmod_nat_unique simp add: prod_eq_iff)
+  using assms by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
 
 lemma mod_nat_unique:
   assumes "divmod_nat_rel m n (q, r)"
   shows "m mod n = r"
-  using assms by (auto dest!: divmod_nat_unique simp add: prod_eq_iff)
+  using assms by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
 
 lemma divmod_nat_rel: "divmod_nat_rel m n (m div n, m mod n)"
-  using divmod_nat_rel_divmod_nat by (simp add: divmod_nat_div_mod)
-
-lemma divmod_nat_zero: "divmod_nat m 0 = (0, m)"
-  by (simp add: divmod_nat_unique divmod_nat_rel_def)
-
-lemma divmod_nat_zero_left: "divmod_nat 0 n = (0, 0)"
-  by (simp add: divmod_nat_unique divmod_nat_rel_def)
-
-lemma divmod_nat_base: "m < n \<Longrightarrow> divmod_nat m n = (0, m)"
-  by (simp add: divmod_nat_unique divmod_nat_rel_def)
-
-lemma divmod_nat_step:
-  assumes "0 < n" and "n \<le> m"
-  shows "divmod_nat m n = (Suc ((m - n) div n), (m - n) mod n)"
-proof (rule divmod_nat_unique)
-  have "divmod_nat_rel (m - n) n ((m - n) div n, (m - n) mod n)"
-    by (rule divmod_nat_rel)
-  thus "divmod_nat_rel m n (Suc ((m - n) div n), (m - n) mod n)"
-    unfolding divmod_nat_rel_def using assms by auto
-qed
+  using Divides.divmod_nat_rel_divmod_nat by (simp add: divmod_nat_div_mod)
 
 text \<open>The ''recursion'' equations for @{const divide} and @{const mod}\<close>
 
@@ -963,25 +968,25 @@
   fixes m n :: nat
   assumes "m < n"
   shows "m div n = 0"
-  using assms divmod_nat_base by (simp add: prod_eq_iff)
+  using assms Divides.divmod_nat_base by (simp add: prod_eq_iff)
 
 lemma le_div_geq:
   fixes m n :: nat
   assumes "0 < n" and "n \<le> m"
   shows "m div n = Suc ((m - n) div n)"
-  using assms divmod_nat_step by (simp add: prod_eq_iff)
+  using assms Divides.divmod_nat_step by (simp add: prod_eq_iff)
 
 lemma mod_less [simp]:
   fixes m n :: nat
   assumes "m < n"
   shows "m mod n = m"
-  using assms divmod_nat_base by (simp add: prod_eq_iff)
+  using assms Divides.divmod_nat_base by (simp add: prod_eq_iff)
 
 lemma le_mod_geq:
   fixes m n :: nat
   assumes "n \<le> m"
   shows "m mod n = (m - n) mod n"
-  using assms divmod_nat_step by (cases "n = 0") (simp_all add: prod_eq_iff)
+  using assms Divides.divmod_nat_step by (cases "n = 0") (simp_all add: prod_eq_iff)
 
 instance proof
   fix m n :: nat
@@ -1003,10 +1008,10 @@
   thus "(m * n) div (m * q) = n div q" by (rule div_nat_unique)
 next
   fix n :: nat show "n div 0 = 0"
-    by (simp add: div_nat_def divmod_nat_zero)
+    by (simp add: div_nat_def Divides.divmod_nat_zero)
 next
   fix n :: nat show "0 div n = 0"
-    by (simp add: div_nat_def divmod_nat_zero_left)
+    by (simp add: div_nat_def Divides.divmod_nat_zero_left)
 qed
 
 end
@@ -1030,8 +1035,9 @@
   
 end
 
-lemma divmod_nat_if [code]: "divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
-  let (q, r) = divmod_nat (m - n) n in (Suc q, r))"
+lemma divmod_nat_if [code]:
+  "Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
+    let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
   by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
 
 text \<open>Simproc for cancelling @{const divide} and @{const mod}\<close>
@@ -1347,15 +1353,15 @@
   assume P: ?lhs
   then have "divmod_nat_rel m n (q, m - n * q)"
     unfolding divmod_nat_rel_def by (auto simp add: ac_simps)
-  with divmod_nat_rel_unique divmod_nat_rel [of m n]
-  have "(q, m - n * q) = (m div n, m mod n)" by auto
+  then have "m div n = q"
+    by (rule div_nat_unique)
   then show ?rhs by simp
 qed
 
 theorem split_div':
   "P ((m::nat) div n) = ((n = 0 \<and> P 0) \<or>
    (\<exists>q. (n * q \<le> m \<and> m < n * (Suc q)) \<and> P q))"
-  apply (case_tac "0 < n")
+  apply (cases "0 < n")
   apply (simp only: add: split_div_lemma)
   apply simp_all
   done
diff -r d35ff80f27fb -r 79900ab5d50a src/HOL/IMP/Abs_State.thy
--- a/src/HOL/IMP/Abs_State.thy	Sat Oct 17 21:26:14 2015 +0200
+++ b/src/HOL/IMP/Abs_State.thy	Sat Oct 17 21:42:18 2015 +0200
@@ -18,8 +18,9 @@
 "eq_st S1 S2 = (fun_rep S1 = fun_rep S2)"
 
 hide_type st  --"hide previous def to avoid long names"
+declare [[typedef_overloaded]] --"allow quotient types to depend on classes"
 
-quotient_type (overloaded) 'a st = "('a::top) st_rep" / eq_st
+quotient_type 'a st = "('a::top) st_rep" / eq_st
 morphisms rep_st St
 by (metis eq_st_def equivpI reflpI sympI transpI)
 
diff -r d35ff80f27fb -r 79900ab5d50a src/HOL/Library/Code_Binary_Nat.thy
--- a/src/HOL/Library/Code_Binary_Nat.thy	Sat Oct 17 21:26:14 2015 +0200
+++ b/src/HOL/Library/Code_Binary_Nat.thy	Sat Oct 17 21:42:18 2015 +0200
@@ -134,12 +134,12 @@
   by (simp_all add: nat_of_num_numeral)
 
 lemma [code, code del]:
-  "divmod_nat = divmod_nat" ..
+  "Divides.divmod_nat = Divides.divmod_nat" ..
   
 lemma divmod_nat_code [code]:
-  "divmod_nat (nat_of_num k) (nat_of_num l) = divmod k l"
-  "divmod_nat m 0 = (0, m)"
-  "divmod_nat 0 n = (0, 0)"
+  "Divides.divmod_nat (nat_of_num k) (nat_of_num l) = divmod k l"
+  "Divides.divmod_nat m 0 = (0, m)"
+  "Divides.divmod_nat 0 n = (0, 0)"
   by (simp_all add: prod_eq_iff nat_of_num_numeral)
 
 end
diff -r d35ff80f27fb -r 79900ab5d50a src/HOL/Library/Code_Target_Nat.thy
--- a/src/HOL/Library/Code_Target_Nat.thy	Sat Oct 17 21:26:14 2015 +0200
+++ b/src/HOL/Library/Code_Target_Nat.thy	Sat Oct 17 21:42:18 2015 +0200
@@ -111,7 +111,7 @@
 lemma (in semiring_1) of_nat_code_if:
   "of_nat n = (if n = 0 then 0
      else let
-       (m, q) = divmod_nat n 2;
+       (m, q) = Divides.divmod_nat n 2;
        m' = 2 * of_nat m
      in if q = 0 then m' else m' + 1)"
 proof -
diff -r d35ff80f27fb -r 79900ab5d50a src/HOL/Library/RBT_Impl.thy
--- a/src/HOL/Library/RBT_Impl.thy	Sat Oct 17 21:26:14 2015 +0200
+++ b/src/HOL/Library/RBT_Impl.thy	Sat Oct 17 21:42:18 2015 +0200
@@ -1166,7 +1166,7 @@
     else if n = 1 then
       case kvs of (k, v) # kvs' \<Rightarrow> 
         (Branch R Empty k v Empty, kvs')
-    else let (n', r) = divmod_nat n 2 in
+    else let (n', r) = Divides.divmod_nat n 2 in
       if r = 0 then
         case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
           apfst (Branch B t1 k v) (rbtreeify_g n' kvs')
@@ -1177,7 +1177,7 @@
 lemma rbtreeify_g_code [code]:
   "rbtreeify_g n kvs =
    (if n = 0 \<or> n = 1 then (Empty, kvs)
-    else let (n', r) = divmod_nat n 2 in
+    else let (n', r) = Divides.divmod_nat n 2 in
       if r = 0 then
         case rbtreeify_g n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
           apfst (Branch B t1 k v) (rbtreeify_g n' kvs')
diff -r d35ff80f27fb -r 79900ab5d50a src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Sat Oct 17 21:26:14 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Sat Oct 17 21:42:18 2015 +0200
@@ -140,8 +140,8 @@
   Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ())) f x
 
 fun hackish_string_of_term ctxt =
-  map_aterms (fn Free (s, T) => Free (if Name.is_internal s then "_" else s, T) | t => t)
-  #> with_vanilla_print_mode (Syntax.string_of_term ctxt)
+  (* FIXME: map_aterms (fn Free (s, T) => Free (if Name.is_internal s then "_" else s, T) | t => t)
+  #> *) with_vanilla_print_mode (Syntax.string_of_term ctxt)
   #> YXML.content_of
   #> simplify_spaces
 
diff -r d35ff80f27fb -r 79900ab5d50a src/HOL/ex/Parallel_Example.thy
--- a/src/HOL/ex/Parallel_Example.thy	Sat Oct 17 21:26:14 2015 +0200
+++ b/src/HOL/ex/Parallel_Example.thy	Sat Oct 17 21:42:18 2015 +0200
@@ -61,7 +61,7 @@
 function factorise_from :: "nat \<Rightarrow> nat \<Rightarrow> nat list" where
   "factorise_from k n = (if 1 < k \<and> k \<le> n
     then
-      let (q, r) = divmod_nat n k 
+      let (q, r) = Divides.divmod_nat n k 
       in if r = 0 then k # factorise_from k q
         else factorise_from (Suc k) n
     else [])" 
@@ -105,4 +105,3 @@
 value "computation_parallel ()"
 
 end
-