--- 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>
--- 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>
--- 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
--- 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 :
--- 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:
--- 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"