# HG changeset patch
# User paulson
# Date 1503612287 -3600
# Node ID c1d8ab323d858b5cc938c3eede56e0313ac7a61b
# Parent  5a42eddc11c1aadbef1289d2cb8f95a83f7ec33e# Parent  b81e1d194e4ce722cf3815c7e7dbe220594f6d5a
merged

diff -r b81e1d194e4c -r c1d8ab323d85 src/HOL/Algebra/Complete_Lattice.thy
--- a/src/HOL/Algebra/Complete_Lattice.thy	Thu Aug 24 23:04:33 2017 +0100
+++ b/src/HOL/Algebra/Complete_Lattice.thy	Thu Aug 24 23:04:47 2017 +0100
@@ -7,7 +7,7 @@
 *)
 
 theory Complete_Lattice
-imports Lattice
+imports Lattice Group
 begin
 
 section \<open>Complete Lattices\<close>
@@ -1192,8 +1192,43 @@
   then show "EX i. greatest ?L i (Lower ?L B)" ..
 qed
 
-text \<open>Another example, that of the lattice of subgroups of a group,
-  can be found in Group theory (Section~\ref{sec:subgroup-lattice}).\<close>
+theorem (in group) subgroups_complete_lattice:
+  "complete_lattice \<lparr>carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq>\<rparr>"
+    (is "complete_lattice ?L")
+proof (rule partial_order.complete_lattice_criterion1)
+  show "partial_order ?L" by (rule subgroups_partial_order)
+next
+  have "greatest ?L (carrier G) (carrier ?L)"
+    by (unfold greatest_def) (simp add: subgroup.subset subgroup_self)
+  then show "\<exists>G. greatest ?L G (carrier ?L)" ..
+next
+  fix A
+  assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}"
+  then have Int_subgroup: "subgroup (\<Inter>A) G"
+    by (fastforce intro: subgroups_Inter)
+  have "greatest ?L (\<Inter>A) (Lower ?L A)" (is "greatest _ ?Int _")
+  proof (rule greatest_LowerI)
+    fix H
+    assume H: "H \<in> A"
+    with L have subgroupH: "subgroup H G" by auto
+    from subgroupH have groupH: "group (G \<lparr>carrier := H\<rparr>)" (is "group ?H")
+      by (rule subgroup_imp_group)
+    from groupH have monoidH: "monoid ?H"
+      by (rule group.is_monoid)
+    from H have Int_subset: "?Int \<subseteq> H" by fastforce
+    then show "le ?L ?Int H" by simp
+  next
+    fix H
+    assume H: "H \<in> Lower ?L A"
+    with L Int_subgroup show "le ?L H ?Int"
+      by (fastforce simp: Lower_def intro: Inter_greatest)
+  next
+    show "A \<subseteq> carrier ?L" by (rule L)
+  next
+    show "?Int \<in> carrier ?L" by simp (rule Int_subgroup)
+  qed
+  then show "\<exists>I. greatest ?L I (Lower ?L A)" ..
+qed
 
 
 subsection \<open>Limit preserving functions\<close>
diff -r b81e1d194e4c -r c1d8ab323d85 src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Thu Aug 24 23:04:33 2017 +0100
+++ b/src/HOL/Algebra/Divisibility.thy	Thu Aug 24 23:04:47 2017 +0100
@@ -6,7 +6,7 @@
 section \<open>Divisibility in monoids and rings\<close>
 
 theory Divisibility
-  imports "HOL-Library.Permutation" Coset Group
+  imports "HOL-Library.Permutation" Coset Group Lattice
 begin
 
 section \<open>Factorial Monoids\<close>
diff -r b81e1d194e4c -r c1d8ab323d85 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Thu Aug 24 23:04:33 2017 +0100
+++ b/src/HOL/Algebra/Group.thy	Thu Aug 24 23:04:47 2017 +0100
@@ -5,7 +5,7 @@
 *)
 
 theory Group
-imports Complete_Lattice "HOL-Library.FuncSet"
+imports Order "HOL-Library.FuncSet"
 begin
 
 section \<open>Monoids and Groups\<close>
@@ -817,42 +817,4 @@
   show "x \<otimes> y \<in> \<Inter>A" by blast
 qed
 
-theorem (in group) subgroups_complete_lattice:
-  "complete_lattice \<lparr>carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq>\<rparr>"
-    (is "complete_lattice ?L")
-proof (rule partial_order.complete_lattice_criterion1)
-  show "partial_order ?L" by (rule subgroups_partial_order)
-next
-  have "greatest ?L (carrier G) (carrier ?L)"
-    by (unfold greatest_def) (simp add: subgroup.subset subgroup_self)
-  then show "\<exists>G. greatest ?L G (carrier ?L)" ..
-next
-  fix A
-  assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}"
-  then have Int_subgroup: "subgroup (\<Inter>A) G"
-    by (fastforce intro: subgroups_Inter)
-  have "greatest ?L (\<Inter>A) (Lower ?L A)" (is "greatest _ ?Int _")
-  proof (rule greatest_LowerI)
-    fix H
-    assume H: "H \<in> A"
-    with L have subgroupH: "subgroup H G" by auto
-    from subgroupH have groupH: "group (G \<lparr>carrier := H\<rparr>)" (is "group ?H")
-      by (rule subgroup_imp_group)
-    from groupH have monoidH: "monoid ?H"
-      by (rule group.is_monoid)
-    from H have Int_subset: "?Int \<subseteq> H" by fastforce
-    then show "le ?L ?Int H" by simp
-  next
-    fix H
-    assume H: "H \<in> Lower ?L A"
-    with L Int_subgroup show "le ?L H ?Int"
-      by (fastforce simp: Lower_def intro: Inter_greatest)
-  next
-    show "A \<subseteq> carrier ?L" by (rule L)
-  next
-    show "?Int \<in> carrier ?L" by simp (rule Int_subgroup)
-  qed
-  then show "\<exists>I. greatest ?L I (Lower ?L A)" ..
-qed
-
 end
diff -r b81e1d194e4c -r c1d8ab323d85 src/HOL/Algebra/Multiplicative_Group.thy
--- a/src/HOL/Algebra/Multiplicative_Group.thy	Thu Aug 24 23:04:33 2017 +0100
+++ b/src/HOL/Algebra/Multiplicative_Group.thy	Thu Aug 24 23:04:47 2017 +0100
@@ -141,7 +141,7 @@
 definition phi' :: "nat => nat"
   where "phi' m = card {x. 1 \<le> x \<and> x \<le> m \<and> gcd x m = 1}"
 
-notation (latex_output)
+notation (latex output)
   phi' ("\<phi> _")
 
 lemma phi'_nonzero :
diff -r b81e1d194e4c -r c1d8ab323d85 src/HOL/Data_Structures/Base_FDS.thy
--- a/src/HOL/Data_Structures/Base_FDS.thy	Thu Aug 24 23:04:33 2017 +0100
+++ b/src/HOL/Data_Structures/Base_FDS.thy	Thu Aug 24 23:04:47 2017 +0100
@@ -11,8 +11,7 @@
 of different parameters.
 
 To alert the reader whenever such a more subtle termination proof is taking place
-the lemma is not enabled all the time but only locally in a \<open>context\<close> block
-around such function definitions.
+the lemma is not enabled all the time but only when it is needed.
 \<close>
 
 lemma size_prod_measure: 
diff -r b81e1d194e4c -r c1d8ab323d85 src/HOL/Data_Structures/Leftist_Heap.thy
--- a/src/HOL/Data_Structures/Leftist_Heap.thy	Thu Aug 24 23:04:33 2017 +0100
+++ b/src/HOL/Data_Structures/Leftist_Heap.thy	Thu Aug 24 23:04:47 2017 +0100
@@ -10,8 +10,6 @@
   Complex_Main
 begin
 
-unbundle pattern_aliases
-
 fun mset_tree :: "('a,'b) tree \<Rightarrow> 'a multiset" where
 "mset_tree Leaf = {#}" |
 "mset_tree (Node _ l a r) = {#a#} + mset_tree l + mset_tree r"
@@ -46,16 +44,16 @@
 fun get_min :: "'a lheap \<Rightarrow> 'a" where
 "get_min(Node n l a r) = a"
 
-text\<open>Explicit termination argument: sum of sizes\<close>
+text \<open>For function \<open>merge\<close>:\<close>
+unbundle pattern_aliases
+declare size_prod_measure[measure_function]
 
-function merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
+fun merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
 "merge Leaf t2 = t2" |
 "merge t1 Leaf = t1" |
 "merge (Node n1 l1 a1 r1 =: t1) (Node n2 l2 a2 r2 =: t2) =
    (if a1 \<le> a2 then node l1 a1 (merge r1 t2)
     else node l2 a2 (merge r2 t1))"
-by pat_completeness auto
-termination by (relation "measure (\<lambda>(t1,t2). size t1 + size t2)") auto
 
 lemma merge_code: "merge t1 t2 = (case (t1,t2) of
   (Leaf, _) \<Rightarrow> t2 |
@@ -180,14 +178,12 @@
 
 text\<open>Explicit termination argument: sum of sizes\<close>
 
-function t_merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> nat" where
+fun t_merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> nat" where
 "t_merge Leaf t2 = 1" |
 "t_merge t2 Leaf = 1" |
 "t_merge (Node n1 l1 a1 r1 =: t1) (Node n2 l2 a2 r2 =: t2) =
   (if a1 \<le> a2 then 1 + t_merge r1 t2
    else 1 + t_merge r2 t1)"
-by pat_completeness auto
-termination by (relation "measure (\<lambda>(t1,t2). size t1 + size t2)") auto
 
 definition t_insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> nat" where
 "t_insert x t = t_merge (Node 1 Leaf x Leaf) t"