# HG changeset patch
# User haftmann
# Date 1364331236 -3600
# Node ID 2e26df807dc724da57ead9b920813bf8c7b58fbd
# Parent  6f6012f430fca7715294e84aac015d522cf4d2ae
more uniform style for interpretation and sublocale declarations

diff -r 6f6012f430fc -r 2e26df807dc7 src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Tue Mar 26 20:55:21 2013 +0100
+++ b/src/HOL/Big_Operators.thy	Tue Mar 26 21:53:56 2013 +0100
@@ -325,12 +325,11 @@
 
 sublocale comm_monoid_add < setsum!: comm_monoid_set plus 0
 where
-  "setsum.F = setsum"
+  "comm_monoid_set.F plus 0 = setsum"
 proof -
   show "comm_monoid_set plus 0" ..
   then interpret setsum!: comm_monoid_set plus 0 .
-  show "setsum.F = setsum"
-    by (simp only: setsum_def)
+  from setsum_def show "comm_monoid_set.F plus 0 = setsum" by rule
 qed
 
 abbreviation
@@ -1048,12 +1047,11 @@
 
 sublocale comm_monoid_mult < setprod!: comm_monoid_set times 1
 where
-  "setprod.F = setprod"
+  "comm_monoid_set.F times 1 = setprod"
 proof -
   show "comm_monoid_set times 1" ..
   then interpret setprod!: comm_monoid_set times 1 .
-  show "setprod.F = setprod"
-    by (simp only: setprod_def)
+  from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
 qed
 
 abbreviation
@@ -1743,22 +1741,20 @@
 
 sublocale semilattice_inf < Inf_fin!: semilattice_order_set inf less_eq less
 where
-  "Inf_fin.F = Inf_fin"
+  "semilattice_set.F inf = Inf_fin"
 proof -
   show "semilattice_order_set inf less_eq less" ..
   then interpret Inf_fin!: semilattice_order_set inf less_eq less.
-  show "Inf_fin.F = Inf_fin"
-    by (fact Inf_fin_def [symmetric])
+  from Inf_fin_def show "semilattice_set.F inf = Inf_fin" by rule
 qed
 
 sublocale semilattice_sup < Sup_fin!: semilattice_order_set sup greater_eq greater
 where
-  "Sup_fin.F = Sup_fin"
+  "semilattice_set.F sup = Sup_fin"
 proof -
   show "semilattice_order_set sup greater_eq greater" ..
   then interpret Sup_fin!: semilattice_order_set sup greater_eq greater .
-  show "Sup_fin.F = Sup_fin"
-    by (fact Sup_fin_def [symmetric])
+  from Sup_fin_def show "semilattice_set.F sup = Sup_fin" by rule
 qed
 
 
@@ -1910,12 +1906,6 @@
 
 subsection {* Minimum and Maximum over non-empty sets *}
 
-text {*
-  This case is already setup by the @{text min_max} sublocale dependency from above.  But note
-  that this yields irregular prefixes, e.g.~@{text min_max.Inf_fin.insert} instead
-  of @{text Max.insert}.
-*}
-
 context linorder
 begin
 
diff -r 6f6012f430fc -r 2e26df807dc7 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Mar 26 20:55:21 2013 +0100
+++ b/src/HOL/Finite_Set.thy	Tue Mar 26 21:53:56 2013 +0100
@@ -1107,11 +1107,11 @@
 
 interpretation card!: folding "\<lambda>_. Suc" 0
 where
-  "card.F = card"
+  "folding.F (\<lambda>_. Suc) 0 = card"
 proof -
   show "folding (\<lambda>_. Suc)" by default rule
   then interpret card!: folding "\<lambda>_. Suc" 0 .
-  show "card.F = card" by (simp only: card_def)
+  from card_def show "folding.F (\<lambda>_. Suc) 0 = card" by rule
 qed
 
 lemma card_infinite:
diff -r 6f6012f430fc -r 2e26df807dc7 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Tue Mar 26 20:55:21 2013 +0100
+++ b/src/HOL/Groups.thy	Tue Mar 26 21:53:56 2013 +0100
@@ -91,8 +91,8 @@
   fixes z :: 'a ("1")
   assumes comm_neutral: "a * 1 = a"
 
-sublocale comm_monoid < monoid proof
-qed (simp_all add: commute comm_neutral)
+sublocale comm_monoid < monoid
+  by default (simp_all add: commute comm_neutral)
 
 
 subsection {* Generic operations *}
@@ -151,14 +151,14 @@
 class semigroup_add = plus +
   assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b + c)"
 
-sublocale semigroup_add < add!: semigroup plus proof
-qed (fact add_assoc)
+sublocale semigroup_add < add!: semigroup plus
+  by default (fact add_assoc)
 
 class ab_semigroup_add = semigroup_add +
   assumes add_commute [algebra_simps, field_simps]: "a + b = b + a"
 
-sublocale ab_semigroup_add < add!: abel_semigroup plus proof
-qed (fact add_commute)
+sublocale ab_semigroup_add < add!: abel_semigroup plus
+  by default (fact add_commute)
 
 context ab_semigroup_add
 begin
@@ -174,14 +174,14 @@
 class semigroup_mult = times +
   assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)"
 
-sublocale semigroup_mult < mult!: semigroup times proof
-qed (fact mult_assoc)
+sublocale semigroup_mult < mult!: semigroup times
+  by default (fact mult_assoc)
 
 class ab_semigroup_mult = semigroup_mult +
   assumes mult_commute [algebra_simps, field_simps]: "a * b = b * a"
 
-sublocale ab_semigroup_mult < mult!: abel_semigroup times proof
-qed (fact mult_commute)
+sublocale ab_semigroup_mult < mult!: abel_semigroup times
+  by default (fact mult_commute)
 
 context ab_semigroup_mult
 begin
@@ -198,8 +198,8 @@
   assumes add_0_left: "0 + a = a"
     and add_0_right: "a + 0 = a"
 
-sublocale monoid_add < add!: monoid plus 0 proof
-qed (fact add_0_left add_0_right)+
+sublocale monoid_add < add!: monoid plus 0
+  by default (fact add_0_left add_0_right)+
 
 lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0"
 by (rule eq_commute)
@@ -207,11 +207,11 @@
 class comm_monoid_add = zero + ab_semigroup_add +
   assumes add_0: "0 + a = a"
 
-sublocale comm_monoid_add < add!: comm_monoid plus 0 proof
-qed (insert add_0, simp add: ac_simps)
+sublocale comm_monoid_add < add!: comm_monoid plus 0
+  by default (insert add_0, simp add: ac_simps)
 
-subclass (in comm_monoid_add) monoid_add proof
-qed (fact add.left_neutral add.right_neutral)+
+subclass (in comm_monoid_add) monoid_add
+  by default (fact add.left_neutral add.right_neutral)+
 
 class comm_monoid_diff = comm_monoid_add + minus +
   assumes diff_zero [simp]: "a - 0 = a"
@@ -268,8 +268,8 @@
   assumes mult_1_left: "1 * a  = a"
     and mult_1_right: "a * 1 = a"
 
-sublocale monoid_mult < mult!: monoid times 1 proof
-qed (fact mult_1_left mult_1_right)+
+sublocale monoid_mult < mult!: monoid times 1
+  by default (fact mult_1_left mult_1_right)+
 
 lemma one_reorient: "1 = x \<longleftrightarrow> x = 1"
 by (rule eq_commute)
@@ -277,11 +277,11 @@
 class comm_monoid_mult = one + ab_semigroup_mult +
   assumes mult_1: "1 * a = a"
 
-sublocale comm_monoid_mult < mult!: comm_monoid times 1 proof
-qed (insert mult_1, simp add: ac_simps)
+sublocale comm_monoid_mult < mult!: comm_monoid times 1
+  by default (insert mult_1, simp add: ac_simps)
 
-subclass (in comm_monoid_mult) monoid_mult proof
-qed (fact mult.left_neutral mult.right_neutral)+
+subclass (in comm_monoid_mult) monoid_mult
+  by default (fact mult.left_neutral mult.right_neutral)+
 
 class cancel_semigroup_add = semigroup_add +
   assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
diff -r 6f6012f430fc -r 2e26df807dc7 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Tue Mar 26 20:55:21 2013 +0100
+++ b/src/HOL/Lattices.thy	Tue Mar 26 21:53:56 2013 +0100
@@ -471,25 +471,23 @@
 class bounded_semilattice_inf_top = semilattice_inf + top
 
 sublocale bounded_semilattice_inf_top < inf_top!: semilattice_neutr inf top
+  + inf_top!: semilattice_neutr_order inf top less_eq less
 proof
   fix x
   show "x \<sqinter> \<top> = x"
     by (rule inf_absorb1) simp
 qed
 
-sublocale bounded_semilattice_inf_top < inf_top!: semilattice_neutr_order inf top less_eq less ..
-
 class bounded_semilattice_sup_bot = semilattice_sup + bot
 
 sublocale bounded_semilattice_sup_bot < sup_bot!: semilattice_neutr sup bot
+  + sup_bot!: semilattice_neutr_order sup bot greater_eq greater
 proof
   fix x
   show "x \<squnion> \<bottom> = x"
     by (rule sup_absorb1) simp
 qed
 
-sublocale bounded_semilattice_sup_bot < sup_bot!: semilattice_neutr_order sup bot greater_eq greater ..
-
 class bounded_lattice_bot = lattice + bot
 begin
 
diff -r 6f6012f430fc -r 2e26df807dc7 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Tue Mar 26 20:55:21 2013 +0100
+++ b/src/HOL/Orderings.thy	Tue Mar 26 21:53:56 2013 +0100
@@ -197,10 +197,7 @@
 
 end
 
-sublocale order < order!: ordering less_eq less
-  by default (auto intro: antisym order_trans simp add: less_le)
-
-sublocale order < dual_order!: ordering greater_eq greater
+sublocale order < order!: ordering less_eq less +  dual_order!: ordering greater_eq greater
   by default (auto intro: antisym order_trans simp add: less_le)
 
 context order
@@ -210,7 +207,7 @@
 
 lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x = y"
     -- {* NOT suitable for iff, since it can cause PROOF FAILED. *}
-by (simp add: less_le) blast
+by (fact order.order_iff_strict)
 
 lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x = y"
 unfolding less_le by blast
@@ -228,10 +225,10 @@
 text {* Transitivity rules for calculational reasoning *}
 
 lemma neq_le_trans: "a \<noteq> b \<Longrightarrow> a \<le> b \<Longrightarrow> a < b"
-by (simp add: less_le)
+by (fact order.not_eq_order_implies_strict)
 
 lemma le_neq_trans: "a \<le> b \<Longrightarrow> a \<noteq> b \<Longrightarrow> a < b"
-by (simp add: less_le)
+by (rule order.not_eq_order_implies_strict)
 
 
 text {* Asymmetry. *}
@@ -243,7 +240,7 @@
 by (blast intro: antisym)
 
 lemma less_imp_neq: "x < y \<Longrightarrow> x \<noteq> y"
-by (erule contrapos_pn, erule subst, rule less_irrefl)
+by (fact order.strict_implies_not_eq)
 
 
 text {* Least value operator *}
@@ -1168,7 +1165,6 @@
 by (simp add: max_def)
 
 
-
 subsection {* (Unique) top and bottom elements *}
 
 class bot = order +
@@ -1176,8 +1172,7 @@
   assumes bot_least: "\<bottom> \<le> a"
 
 sublocale bot < bot!: ordering_top greater_eq greater bot
-proof
-qed (fact bot_least)
+  by default (fact bot_least)
 
 context bot
 begin
@@ -1205,8 +1200,7 @@
   assumes top_greatest: "a \<le> \<top>"
 
 sublocale top < top!: ordering_top less_eq less top
-proof
-qed (fact top_greatest)
+  by default (fact top_greatest)
 
 context top
 begin
@@ -1316,6 +1310,7 @@
 
 class dense_linorder = inner_dense_linorder + no_top + no_bot
 
+
 subsection {* Wellorders *}
 
 class wellorder = linorder +