1.1 --- a/src/HOL/Groups.thy Thu Nov 21 08:43:38 2013 +0100
1.2 +++ b/src/HOL/Groups.thy Thu Nov 21 09:18:22 2013 +0100
1.3 @@ -82,8 +82,6 @@
1.4
1.5 end
1.6
1.7 -print_locale! abel_semigroup
1.8 -
1.9 locale monoid = semigroup +
1.10 fixes z :: 'a ("1")
1.11 assumes left_neutral [simp]: "1 * a = a"
1.12 @@ -93,8 +91,8 @@
1.13 fixes z :: 'a ("1")
1.14 assumes comm_neutral: "a * 1 = a"
1.15
1.16 -sublocale comm_monoid < monoid proof
1.17 -qed (simp_all add: commute comm_neutral)
1.18 +sublocale comm_monoid < monoid
1.19 + by default (simp_all add: commute comm_neutral)
1.20
1.21
1.22 subsection {* Generic operations *}
1.23 @@ -123,15 +121,13 @@
1.24 simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc
1.25 simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
1.26
1.27 -typed_print_translation (advanced) {*
1.28 +typed_print_translation {*
1.29 let
1.30 fun tr' c = (c, fn ctxt => fn T => fn ts =>
1.31 - if not (null ts) orelse T = dummyT orelse
1.32 - not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T
1.33 - then raise Match
1.34 - else
1.35 + if null ts andalso Printer.type_emphasis ctxt T then
1.36 Syntax.const @{syntax_const "_constrain"} $ Syntax.const c $
1.37 - Syntax_Phases.term_of_typ ctxt T);
1.38 + Syntax_Phases.term_of_typ ctxt T
1.39 + else raise Match);
1.40 in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
1.41 *} -- {* show types that are presumably too general *}
1.42
1.43 @@ -153,21 +149,14 @@
1.44 class semigroup_add = plus +
1.45 assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b + c)"
1.46
1.47 -sublocale (*!class*) semigroup_add < (*1*) add!: (*locale*) semigroup (*class*) plus proof
1.48 -qed (fact (*..isar.ref.p.121*) add_assoc)
1.49 -(*(*1*) FROM ABOVE... setup {* Reorient_Proc.add*)
1.50 -thm add_assoc
1.51 +sublocale semigroup_add < add!: semigroup plus
1.52 + by default (fact add_assoc)
1.53
1.54 class ab_semigroup_add = semigroup_add +
1.55 assumes add_commute [algebra_simps, field_simps]: "a + b = b + a"
1.56
1.57 -sublocale ab_semigroup_add < add!: abel_semigroup plus proof
1.58 -qed (fact add_commute)
1.59 -(*... sublocales rearrange the locales hierarchy, see locales.pdf.p.6*)
1.60 -
1.61 -(*thm left_commute ...Unknown fact "left_commute"*)
1.62 -(*thm add_left_commute ...Unknown fact "left_commute"*)
1.63 -thm add.left_commute --{*?b + (?a + ?c) = ?a + (?b + ?c)*}
1.64 +sublocale ab_semigroup_add < add!: abel_semigroup plus
1.65 + by default (fact add_commute)
1.66
1.67 context ab_semigroup_add
1.68 begin
1.69 @@ -178,22 +167,19 @@
1.70
1.71 end
1.72
1.73 -thm ab_semigroup_add.add_ac --{* 3 thms*}
1.74 -print_locale! ab_semigroup_add
1.75 -
1.76 theorems add_ac = add_assoc add_commute add_left_commute
1.77
1.78 class semigroup_mult = times +
1.79 assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)"
1.80
1.81 -sublocale semigroup_mult < mult!: semigroup times proof
1.82 -qed (fact mult_assoc)
1.83 +sublocale semigroup_mult < mult!: semigroup times
1.84 + by default (fact mult_assoc)
1.85
1.86 class ab_semigroup_mult = semigroup_mult +
1.87 assumes mult_commute [algebra_simps, field_simps]: "a * b = b * a"
1.88
1.89 -sublocale ab_semigroup_mult < mult!: abel_semigroup times proof
1.90 -qed (fact mult_commute)
1.91 +sublocale ab_semigroup_mult < mult!: abel_semigroup times
1.92 + by default (fact mult_commute)
1.93
1.94 context ab_semigroup_mult
1.95 begin
1.96 @@ -210,8 +196,8 @@
1.97 assumes add_0_left: "0 + a = a"
1.98 and add_0_right: "a + 0 = a"
1.99
1.100 -sublocale monoid_add < add!: monoid plus 0 proof
1.101 -qed (fact add_0_left add_0_right)+
1.102 +sublocale monoid_add < add!: monoid plus 0
1.103 + by default (fact add_0_left add_0_right)+
1.104
1.105 lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0"
1.106 by (rule eq_commute)
1.107 @@ -219,11 +205,11 @@
1.108 class comm_monoid_add = zero + ab_semigroup_add +
1.109 assumes add_0: "0 + a = a"
1.110
1.111 -sublocale comm_monoid_add < add!: comm_monoid plus 0 proof
1.112 -qed (insert add_0, simp add: ac_simps)
1.113 +sublocale comm_monoid_add < add!: comm_monoid plus 0
1.114 + by default (insert add_0, simp add: ac_simps)
1.115
1.116 -subclass (in comm_monoid_add) monoid_add proof
1.117 -qed (fact add.left_neutral add.right_neutral)+
1.118 +subclass (in comm_monoid_add) monoid_add
1.119 + by default (fact add.left_neutral add.right_neutral)+
1.120
1.121 class comm_monoid_diff = comm_monoid_add + minus +
1.122 assumes diff_zero [simp]: "a - 0 = a"
1.123 @@ -280,8 +266,8 @@
1.124 assumes mult_1_left: "1 * a = a"
1.125 and mult_1_right: "a * 1 = a"
1.126
1.127 -sublocale monoid_mult < mult!: monoid times 1 proof
1.128 -qed (fact mult_1_left mult_1_right)+
1.129 +sublocale monoid_mult < mult!: monoid times 1
1.130 + by default (fact mult_1_left mult_1_right)+
1.131
1.132 lemma one_reorient: "1 = x \<longleftrightarrow> x = 1"
1.133 by (rule eq_commute)
1.134 @@ -289,11 +275,11 @@
1.135 class comm_monoid_mult = one + ab_semigroup_mult +
1.136 assumes mult_1: "1 * a = a"
1.137
1.138 -sublocale comm_monoid_mult < mult!: comm_monoid times 1 proof
1.139 -qed (insert mult_1, simp add: ac_simps)
1.140 +sublocale comm_monoid_mult < mult!: comm_monoid times 1
1.141 + by default (insert mult_1, simp add: ac_simps)
1.142
1.143 -subclass (in comm_monoid_mult) monoid_mult proof
1.144 -qed (fact mult.left_neutral mult.right_neutral)+
1.145 +subclass (in comm_monoid_mult) monoid_mult
1.146 + by default (fact mult.left_neutral mult.right_neutral)+
1.147
1.148 class cancel_semigroup_add = semigroup_add +
1.149 assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
1.150 @@ -672,6 +658,68 @@
1.151
1.152 end
1.153
1.154 +class ordered_cancel_comm_monoid_diff = comm_monoid_diff + ordered_ab_semigroup_add_imp_le +
1.155 + assumes le_iff_add: "a \<le> b \<longleftrightarrow> (\<exists>c. b = a + c)"
1.156 +begin
1.157 +
1.158 +context
1.159 + fixes a b
1.160 + assumes "a \<le> b"
1.161 +begin
1.162 +
1.163 +lemma add_diff_inverse:
1.164 + "a + (b - a) = b"
1.165 + using `a \<le> b` by (auto simp add: le_iff_add)
1.166 +
1.167 +lemma add_diff_assoc:
1.168 + "c + (b - a) = c + b - a"
1.169 + using `a \<le> b` by (auto simp add: le_iff_add add_left_commute [of c])
1.170 +
1.171 +lemma add_diff_assoc2:
1.172 + "b - a + c = b + c - a"
1.173 + using `a \<le> b` by (auto simp add: le_iff_add add_assoc)
1.174 +
1.175 +lemma diff_add_assoc:
1.176 + "c + b - a = c + (b - a)"
1.177 + using `a \<le> b` by (simp add: add_commute add_diff_assoc)
1.178 +
1.179 +lemma diff_add_assoc2:
1.180 + "b + c - a = b - a + c"
1.181 + using `a \<le> b`by (simp add: add_commute add_diff_assoc)
1.182 +
1.183 +lemma diff_diff_right:
1.184 + "c - (b - a) = c + a - b"
1.185 + by (simp add: add_diff_inverse add_diff_cancel_left [of a c "b - a", symmetric] add_commute)
1.186 +
1.187 +lemma diff_add:
1.188 + "b - a + a = b"
1.189 + by (simp add: add_commute add_diff_inverse)
1.190 +
1.191 +lemma le_add_diff:
1.192 + "c \<le> b + c - a"
1.193 + by (auto simp add: add_commute diff_add_assoc2 le_iff_add)
1.194 +
1.195 +lemma le_imp_diff_is_add:
1.196 + "a \<le> b \<Longrightarrow> b - a = c \<longleftrightarrow> b = c + a"
1.197 + by (auto simp add: add_commute add_diff_inverse)
1.198 +
1.199 +lemma le_diff_conv2:
1.200 + "c \<le> b - a \<longleftrightarrow> c + a \<le> b" (is "?P \<longleftrightarrow> ?Q")
1.201 +proof
1.202 + assume ?P
1.203 + then have "c + a \<le> b - a + a" by (rule add_right_mono)
1.204 + then show ?Q by (simp add: add_diff_inverse add_commute)
1.205 +next
1.206 + assume ?Q
1.207 + then have "a + c \<le> a + (b - a)" by (simp add: add_diff_inverse add_commute)
1.208 + then show ?P by simp
1.209 +qed
1.210 +
1.211 +end
1.212 +
1.213 +end
1.214 +
1.215 +
1.216 subsection {* Support for reasoning about signs *}
1.217
1.218 class ordered_comm_monoid_add =
1.219 @@ -1311,14 +1359,8 @@
1.220 by (auto intro: add_strict_right_mono add_strict_left_mono
1.221 add_less_le_mono add_le_less_mono add_strict_mono)
1.222
1.223 -code_modulename SML
1.224 - Groups Arith
1.225 -
1.226 -code_modulename OCaml
1.227 - Groups Arith
1.228 -
1.229 -code_modulename Haskell
1.230 - Groups Arith
1.231 +code_identifier
1.232 + code_module Groups \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
1.233
1.234
1.235 text {* Legacy *}
2.1 --- a/src/Pure/thm.ML Thu Nov 21 08:43:38 2013 +0100
2.2 +++ b/src/Pure/thm.ML Thu Nov 21 09:18:22 2013 +0100
2.3 @@ -40,7 +40,7 @@
2.4 type deriv (*WN*)
2.5 val rep_thm_G:(*WN*) thm ->
2.6 deriv *
2.7 - {thy_ref: theory_ref, (*new since 2002*)
2.8 + {thy: theory, (*new since 2002, updated 2013-1*)
2.9 tags: Properties.T, (*new since 2002*)
2.10 maxidx: int,
2.11 shyps: sort Ord_List.T,
2.12 @@ -65,7 +65,7 @@
2.13 val cprem_of: thm -> int -> cterm
2.14 val make_thm:(*WN*) cterm -> thm
2.15 val assbl_thm:(*WN*) deriv ->
2.16 - theory_ref ->
2.17 + theory ->
2.18 Properties.T ->
2.19 int ->
2.20 sort Ord_List.T ->
2.21 @@ -672,13 +672,13 @@
2.22 prop = prop})
2.23 end;
2.24 fun make_thm raw_ct = (*WN ---vvv *)
2.25 - let val Cterm {thy_ref, t = prop, T, maxidx, sorts} = adjust_maxidx_cterm ~1 raw_ct in
2.26 + let val Cterm {thy, t = prop, T, maxidx, sorts} = adjust_maxidx_cterm ~1 raw_ct in
2.27 if T <> propT then
2.28 - raise THM ("assume: prop", 0, [])
2.29 + raise THM ("make_thm: prop", 0, [])
2.30 (*else if maxidx <> ~1 then (*WN true with matches (?b * v_ = 0)..*)
2.31 - raise THM ("assume: variables", maxidx, [])*)
2.32 + raise THM ("make_thm: variables", maxidx, [])*)
2.33 else Thm (deriv_rule0 (Proofterm.Hyp prop),
2.34 - {thy_ref = thy_ref,
2.35 + {thy = thy,
2.36 tags = [],
2.37 maxidx = ~1,
2.38 shyps = sorts,
2.39 @@ -686,8 +686,8 @@
2.40 tpairs = [],
2.41 prop = prop})
2.42 end; (*WN ---^^^ *)
2.43 -fun assbl_thm deriv thy_ref tags maxidx shyps hyps tpairs prop = (*WN*)
2.44 - Thm (deriv, {thy_ref=thy_ref, tags=tags, maxidx=maxidx,
2.45 +fun assbl_thm deriv thy tags maxidx shyps hyps tpairs prop = (*WN*)
2.46 + Thm (deriv, {thy=thy, tags=tags, maxidx=maxidx,
2.47 shyps=shyps, hyps=hyps, tpairs=tpairs, prop=prop});
2.48
2.49 (*Implication introduction