# HG changeset patch
# User eberlm
# Date 1464108411 -7200
# Node ID feea9cf343d99a035b5c773a5691e715ca0e8676
# Parent  8230358fab884f8cb3700fa580246bc161a1b559
Backed out changeset 8230358fab88

diff -r 8230358fab88 -r feea9cf343d9 src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Tue May 24 17:42:14 2016 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Tue May 24 18:46:51 2016 +0200
@@ -73,9 +73,6 @@
 lemma [code, code del]:
   "Lcm_eucl = Lcm_eucl" ..
 
-lemma [code, code del]:
-  "permutations_of_set = permutations_of_set" ..
-
 (*
   If the code generation ends with an exception with the following message:
   '"List.set" is not a constructor, on left hand side of equation: ...',
diff -r 8230358fab88 -r feea9cf343d9 src/HOL/Number_Theory/Factorial_Ring.thy
--- a/src/HOL/Number_Theory/Factorial_Ring.thy	Tue May 24 17:42:14 2016 +0200
+++ b/src/HOL/Number_Theory/Factorial_Ring.thy	Tue May 24 18:46:51 2016 +0200
@@ -24,104 +24,16 @@
 
 end
 
-context comm_semiring_1
-begin
-
-definition irreducible :: "'a \<Rightarrow> bool" where
-  "irreducible p \<longleftrightarrow> p \<noteq> 0 \<and> \<not>p dvd 1 \<and> (\<forall>a b. p = a * b \<longrightarrow> a dvd 1 \<or> b dvd 1)"
-  
-lemma not_irreducible_zero [simp]: "\<not>irreducible 0"
-  by (simp add: irreducible_def)
-
-lemma irreducible_not_unit: "irreducible p \<Longrightarrow> \<not>p dvd 1"
-  by (simp add: irreducible_def)
-  
-lemma irreducibleI: 
-  "p \<noteq> 0 \<Longrightarrow> \<not>p dvd 1 \<Longrightarrow> (\<And>a b. p = a * b \<Longrightarrow> a dvd 1 \<or> b dvd 1) \<Longrightarrow> irreducible p"
-  by (simp add: irreducible_def)
-  
-lemma irreducibleD: "irreducible p \<Longrightarrow> p = a * b \<Longrightarrow> a dvd 1 \<or> b dvd 1"
-  by (simp add: irreducible_def)
-
-definition is_prime :: "'a \<Rightarrow> bool" where
-  "is_prime p \<longleftrightarrow> p \<noteq> 0 \<and> \<not>p dvd 1 \<and> (\<forall>a b. p dvd (a * b) \<longrightarrow> p dvd a \<or> p dvd b)"
-
-lemma not_is_prime_zero [simp]: "\<not>is_prime 0"
-  by (simp add: is_prime_def)
-
-lemma is_prime_not_unit: "is_prime p \<Longrightarrow> \<not>p dvd 1"
-  by (simp add: is_prime_def)
-
-lemma is_primeI: 
-    "p \<noteq> 0 \<Longrightarrow> \<not>p dvd 1 \<Longrightarrow> (\<And>a b. p dvd (a * b) \<Longrightarrow> p dvd a \<or> p dvd b) \<Longrightarrow> is_prime p"
-  by (simp add: is_prime_def)
-
-lemma prime_divides_productD:
-    "is_prime p \<Longrightarrow> p dvd (a * b) \<Longrightarrow> p dvd a \<or> p dvd b"
-  by (simp add: is_prime_def)
-
-lemma prime_divides_product_iff:
-  "is_prime p \<Longrightarrow> p dvd (a * b) \<longleftrightarrow> p dvd a \<or> p dvd b"
-  by (auto simp: is_prime_def)
-
-end
-
-
-context algebraic_semidom
-begin
-
-lemma prime_imp_irreducible:
-  assumes "prime p"
-  shows   "irreducible p"
-proof -
-  
-lemma is_prime_mono: 
-  assumes "is_prime p" "\<not>q dvd 1" "q dvd p"
-  shows   "is_prime q"
-proof -
-  from \<open>q dvd p\<close> obtain r where r: "p = q * r" by (elim dvdE)
-  hence "p dvd q * r" by simp
-  with \<open>is_prime p\<close> have "p dvd q \<or> p dvd r" by (rule prime_divides_productD)
-  hence "p dvd q"
-  proof
-    assume "p dvd r"
-    then obtain s where s: "r = p * s" by (elim dvdE)
-    from r have "p * 1 = p * (q * s)" by (subst (asm) s) (simp add: mult_ac)
-    with \<open>is_prime p\<close> have "q dvd 1"
-      by (subst (asm) mult_cancel_left) auto
-    with \<open>\<not>q dvd 1\<close> show ?thesis by contradiction
-  qed
-  
-  show ?thesis
-  proof (rule is_primeI)
-    fix a b assume "q dvd (a * b)"
-    with \<open>p dvd q\<close> have "p dvd (a * b)" by (rule dvd_trans)
-    with \<open>is_prime p\<close> have "p dvd a \<or> p dvd b" by (rule prime_divides_productD)
-    with \<open>q dvd p\<close> show "q dvd a \<or> q dvd b" by (blast intro: dvd_trans)
-  qed (insert assms, auto)
-qed
-
-end
-
-
 class factorial_semiring = normalization_semidom +
   assumes finite_divisors: "a \<noteq> 0 \<Longrightarrow> finite {b. b dvd a \<and> normalize b = b}"
-  assumes irreducible_is_prime: "(\<And>b. b dvd a \<Longrightarrow>
-  assumes no_prime_divisorsI2: "(\<And>b. b dvd a \<Longrightarrow> \<not> is_prime b) \<Longrightarrow> is_unit a"
+  fixes is_prime :: "'a \<Rightarrow> bool"
+  assumes not_is_prime_zero [simp]: "\<not> is_prime 0"
+    and is_prime_not_unit: "is_prime p \<Longrightarrow> \<not> is_unit p"
+    and no_prime_divisorsI2: "(\<And>b. b dvd a \<Longrightarrow> \<not> is_prime b) \<Longrightarrow> is_unit a"
+  assumes is_primeI: "p \<noteq> 0 \<Longrightarrow> \<not> is_unit p \<Longrightarrow> (\<And>a. a dvd p \<Longrightarrow> \<not> is_unit a \<Longrightarrow> p dvd a) \<Longrightarrow> is_prime p"
+    and is_primeD: "is_prime p \<Longrightarrow> p dvd a * b \<Longrightarrow> p dvd a \<or> p dvd b"
 begin
 
-lemma is_primeI': 
-  assumes "p \<noteq> 0" "\<not> is_unit p" "\<And>a. a dvd p \<Longrightarrow> \<not> is_unit a \<Longrightarrow> p dvd a"
-  shows   "is_prime p"
-proof (rule ccontr)
-  assume "\<not>is_prime p"
-  with assms obtain a b where "p dvd (a * b)" "\<not>p dvd a" "\<not>p dvd b"
-    by (auto simp: is_prime_def)
-  
-  
-qed fact+
-
-
 lemma not_is_prime_one [simp]:
   "\<not> is_prime 1"
   by (auto dest: is_prime_not_unit)
diff -r 8230358fab88 -r feea9cf343d9 src/HOL/Probability/Random_Permutations.thy
--- a/src/HOL/Probability/Random_Permutations.thy	Tue May 24 17:42:14 2016 +0200
+++ b/src/HOL/Probability/Random_Permutations.thy	Tue May 24 18:46:51 2016 +0200
@@ -40,7 +40,7 @@
 text \<open>
   A generic fold function that takes a function, an initial state, and a set 
   and chooses a random order in which it then traverses the set in the same 
-  fashion as a left fold over a list.
+  fashion as a left-fold over a list.
     We first give a recursive definition.
 \<close>
 function fold_random_permutation :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b pmf" where