--- a/NEWS Thu Mar 26 11:33:50 2009 -0700
+++ b/NEWS Thu Mar 26 20:09:58 2009 +0100
@@ -139,8 +139,8 @@
INCOMPATBILITY.
* Complete re-implementation of locales. INCOMPATIBILITY. The most
-important changes are listed below. See documentation (forthcoming)
-and tutorial (also forthcoming) for details.
+important changes are listed below. See the Tutorial on Locales for
+details.
- In locale expressions, instantiation replaces renaming. Parameters
must be declared in a for clause. To aid compatibility with previous
@@ -154,19 +154,23 @@
- More flexible mechanisms to qualify names generated by locale
expressions. Qualifiers (prefixes) may be specified in locale
-expressions. Available are normal qualifiers (syntax "name:") and
-strict qualifiers (syntax "name!:"). The latter must occur in name
-references and are useful to avoid accidental hiding of names, the
-former are optional. Qualifiers derived from the parameter names of a
-locale are no longer generated.
+expressions, and can be marked as mandatory (syntax: "name!:") or
+optional (syntax "name?:"). The default depends for plain "name:"
+depends on the situation where a locale expression is used: in
+commands 'locale' and 'sublocale' prefixes are optional, in
+'interpretation' and 'interpret' prefixes are mandatory. Old-style
+implicit qualifiers derived from the parameter names of a locale are
+no longer generated.
- "sublocale l < e" replaces "interpretation l < e". The
instantiation clause in "interpretation" and "interpret" (square
brackets) is no longer available. Use locale expressions.
-- When converting proof scripts, be sure to replace qualifiers in
-"interpretation" and "interpret" by strict qualifiers. Qualifiers in
-locale expressions range over a single locale instance only.
+- When converting proof scripts, be sure to mandatory qualifiers in
+'interpretation' and 'interpret' should be retained by default, even
+if this is an INCOMPATIBILITY compared to former behaviour.
+Qualifiers in locale expressions range over a single locale instance
+only.
* Command 'instance': attached definitions no longer accepted.
INCOMPATIBILITY, use proper 'instantiation' target.
@@ -180,9 +184,9 @@
directly solve the current goal.
* Auto solve feature for main theorem statements (cf. option in Proof
-General Isabelle settings menu, enabled by default). Whenever a new
+General Isabelle settings menu, disabled by default). Whenever a new
goal is stated, "find_theorems solves" is called; any theorems that
-could solve the lemma directly are listed underneath the goal.
+could solve the lemma directly are listed as part of the goal state.
* Command 'find_consts' searches for constants based on type and name
patterns, e.g.
@@ -190,7 +194,7 @@
find_consts "_ => bool"
By default, matching is against subtypes, but it may be restricted to
-the whole type. Searching by name is possible. Multiple queries are
+the whole type. Searching by name is possible. Multiple queries are
conjunctive and queries may be negated by prefixing them with a
hyphen:
--- a/doc-src/Classes/Thy/Classes.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/doc-src/Classes/Thy/Classes.thy Thu Mar 26 20:09:58 2009 +0100
@@ -458,7 +458,7 @@
of monoids for lists:
*}
-interpretation %quote list_monoid!: monoid append "[]"
+interpretation %quote list_monoid: monoid append "[]"
proof qed auto
text {*
@@ -473,7 +473,7 @@
"replicate 0 _ = []"
| "replicate (Suc n) xs = xs @ replicate n xs"
-interpretation %quote list_monoid!: monoid append "[]" where
+interpretation %quote list_monoid: monoid append "[]" where
"monoid.pow_nat append [] = replicate"
proof -
interpret monoid append "[]" ..
--- a/doc-src/Classes/Thy/document/Classes.tex Thu Mar 26 11:33:50 2009 -0700
+++ b/doc-src/Classes/Thy/document/Classes.tex Thu Mar 26 20:09:58 2009 +0100
@@ -863,7 +863,7 @@
%
\isatagquote
\isacommand{interpretation}\isamarkupfalse%
-\ list{\isacharunderscore}monoid{\isacharbang}{\isacharcolon}\ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
+\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ \isacommand{qed}\isamarkupfalse%
\ auto%
@@ -894,7 +894,7 @@
\ \ {\isacharbar}\ {\isachardoublequoteopen}replicate\ {\isacharparenleft}Suc\ n{\isacharparenright}\ xs\ {\isacharequal}\ xs\ {\isacharat}\ replicate\ n\ xs{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{interpretation}\isamarkupfalse%
-\ list{\isacharunderscore}monoid{\isacharbang}{\isacharcolon}\ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharminus}\isanewline
@@ -1191,7 +1191,7 @@
\hspace*{0pt}\\
\hspace*{0pt}pow{\char95}nat ::~forall a.~(Monoid a) => Nat -> a -> a;\\
\hspace*{0pt}pow{\char95}nat Zero{\char95}nat x = neutral;\\
-\hspace*{0pt}pow{\char95}nat (Suc n) x = mult x (pow{\char95}nat n x);\\
+\hspace*{0pt}pow{\char95}nat (Suc n) xa = mult xa (pow{\char95}nat n xa);\\
\hspace*{0pt}\\
\hspace*{0pt}pow{\char95}int ::~forall a.~(Group a) => Integer -> a -> a;\\
\hspace*{0pt}pow{\char95}int k x =\\
@@ -1272,8 +1272,8 @@
\hspace*{0pt} ~IntInf.int group;\\
\hspace*{0pt}\\
\hspace*{0pt}fun pow{\char95}nat A{\char95}~Zero{\char95}nat x = neutral (monoidl{\char95}monoid A{\char95})\\
-\hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) x =\\
-\hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) x (pow{\char95}nat A{\char95}~n x);\\
+\hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) xa =\\
+\hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) xa (pow{\char95}nat A{\char95}~n xa);\\
\hspace*{0pt}\\
\hspace*{0pt}fun pow{\char95}int A{\char95}~k x =\\
\hspace*{0pt} ~(if IntInf.<= ((0 :~IntInf.int),~k)\\
--- a/src/FOL/ex/LocaleTest.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/FOL/ex/LocaleTest.thy Thu Mar 26 20:09:58 2009 +0100
@@ -119,7 +119,7 @@
term extra_type.test thm extra_type.test_def
-interpretation var: extra_type "0" "%x y. x = 0" .
+interpretation var?: extra_type "0" "%x y. x = 0" .
thm var.test_def
@@ -381,13 +381,13 @@
subsection {* Sublocale, then interpretation in theory *}
-interpretation int: lgrp "op +" "0" "minus"
+interpretation int?: lgrp "op +" "0" "minus"
proof unfold_locales
qed (rule int_assoc int_zero int_minus)+
thm int.assoc int.semi_axioms
-interpretation int2: semi "op +"
+interpretation int2?: semi "op +"
by unfold_locales (* subsumed, thm int2.assoc not generated *)
thm int.lone int.right.rone
@@ -443,7 +443,7 @@
end
-interpretation x!: logic_o "op &" "Not"
+interpretation x: logic_o "op &" "Not"
where bool_logic_o: "logic_o.lor_o(op &, Not, x, y) <-> x | y"
proof -
show bool_logic_o: "PROP logic_o(op &, Not)" by unfold_locales fast+
--- a/src/HOL/Algebra/AbelCoset.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOL/Algebra/AbelCoset.thy Thu Mar 26 20:09:58 2009 +0100
@@ -540,8 +540,8 @@
(| carrier = carrier H, mult = add H, one = zero H |) h"
shows "abelian_group_hom G H h"
proof -
- interpret G!: abelian_group G by fact
- interpret H!: abelian_group H by fact
+ interpret G: abelian_group G by fact
+ interpret H: abelian_group H by fact
show ?thesis apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
apply fact
apply fact
@@ -692,7 +692,7 @@
assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
shows "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)"
proof -
- interpret G!: ring G by fact
+ interpret G: ring G by fact
from carr
have "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)" by (rule a_rcos_module)
with carr
--- a/src/HOL/Algebra/Group.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOL/Algebra/Group.thy Thu Mar 26 20:09:58 2009 +0100
@@ -488,8 +488,8 @@
assumes "monoid G" and "monoid H"
shows "monoid (G \<times>\<times> H)"
proof -
- interpret G!: monoid G by fact
- interpret H!: monoid H by fact
+ interpret G: monoid G by fact
+ interpret H: monoid H by fact
from assms
show ?thesis by (unfold monoid_def DirProd_def, auto)
qed
@@ -500,8 +500,8 @@
assumes "group G" and "group H"
shows "group (G \<times>\<times> H)"
proof -
- interpret G!: group G by fact
- interpret H!: group H by fact
+ interpret G: group G by fact
+ interpret H: group H by fact
show ?thesis by (rule groupI)
(auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
simp add: DirProd_def)
@@ -525,9 +525,9 @@
and h: "h \<in> carrier H"
shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
proof -
- interpret G!: group G by fact
- interpret H!: group H by fact
- interpret Prod!: group "G \<times>\<times> H"
+ interpret G: group G by fact
+ interpret H: group H by fact
+ interpret Prod: group "G \<times>\<times> H"
by (auto intro: DirProd_group group.intro group.axioms assms)
show ?thesis by (simp add: Prod.inv_equality g h)
qed
--- a/src/HOL/Algebra/Ideal.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOL/Algebra/Ideal.thy Thu Mar 26 20:09:58 2009 +0100
@@ -711,7 +711,7 @@
obtains "carrier R = I"
| "\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I"
proof -
- interpret R!: cring R by fact
+ interpret R: cring R by fact
assume "carrier R = I ==> thesis"
and "\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I \<Longrightarrow> thesis"
then show thesis using primeidealCD [OF R.is_cring notprime] by blast
--- a/src/HOL/Algebra/IntRing.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOL/Algebra/IntRing.thy Thu Mar 26 20:09:58 2009 +0100
@@ -96,7 +96,7 @@
interpretation needs to be done as early as possible --- that is,
with as few assumptions as possible. *}
-interpretation int!: monoid \<Z>
+interpretation int: monoid \<Z>
where "carrier \<Z> = UNIV"
and "mult \<Z> x y = x * y"
and "one \<Z> = 1"
@@ -104,7 +104,7 @@
proof -
-- "Specification"
show "monoid \<Z>" proof qed (auto simp: int_ring_def)
- then interpret int!: monoid \<Z> .
+ then interpret int: monoid \<Z> .
-- "Carrier"
show "carrier \<Z> = UNIV" by (simp add: int_ring_def)
@@ -116,12 +116,12 @@
show "pow \<Z> x n = x^n" by (induct n) (simp, simp add: int_ring_def)+
qed
-interpretation int!: comm_monoid \<Z>
+interpretation int: comm_monoid \<Z>
where "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
proof -
-- "Specification"
show "comm_monoid \<Z>" proof qed (auto simp: int_ring_def)
- then interpret int!: comm_monoid \<Z> .
+ then interpret int: comm_monoid \<Z> .
-- "Operations"
{ fix x y have "mult \<Z> x y = x * y" by (simp add: int_ring_def) }
@@ -139,14 +139,14 @@
qed
qed
-interpretation int!: abelian_monoid \<Z>
+interpretation int: abelian_monoid \<Z>
where "zero \<Z> = 0"
and "add \<Z> x y = x + y"
and "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
proof -
-- "Specification"
show "abelian_monoid \<Z>" proof qed (auto simp: int_ring_def)
- then interpret int!: abelian_monoid \<Z> .
+ then interpret int: abelian_monoid \<Z> .
-- "Operations"
{ fix x y show "add \<Z> x y = x + y" by (simp add: int_ring_def) }
@@ -164,7 +164,7 @@
qed
qed
-interpretation int!: abelian_group \<Z>
+interpretation int: abelian_group \<Z>
where "a_inv \<Z> x = - x"
and "a_minus \<Z> x y = x - y"
proof -
@@ -174,7 +174,7 @@
show "!!x. x \<in> carrier \<Z> ==> EX y : carrier \<Z>. y \<oplus>\<^bsub>\<Z>\<^esub> x = \<zero>\<^bsub>\<Z>\<^esub>"
by (simp add: int_ring_def) arith
qed (auto simp: int_ring_def)
- then interpret int!: abelian_group \<Z> .
+ then interpret int: abelian_group \<Z> .
-- "Operations"
{ fix x y have "add \<Z> x y = x + y" by (simp add: int_ring_def) }
@@ -187,7 +187,7 @@
show "a_minus \<Z> x y = x - y" by (simp add: int.minus_eq add a_inv)
qed
-interpretation int!: "domain" \<Z>
+interpretation int: "domain" \<Z>
proof qed (auto simp: int_ring_def left_distrib right_distrib)
@@ -203,7 +203,7 @@
"(True ==> PROP R) == PROP R"
by simp_all
-interpretation int! (* FIXME [unfolded UNIV] *) :
+interpretation int (* FIXME [unfolded UNIV] *) :
partial_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
where "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
and "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
@@ -219,7 +219,7 @@
by (simp add: lless_def) auto
qed
-interpretation int! (* FIXME [unfolded UNIV] *) :
+interpretation int (* FIXME [unfolded UNIV] *) :
lattice "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
where "join (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = max x y"
and "meet (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = min x y"
@@ -232,7 +232,7 @@
apply (simp add: greatest_def Lower_def)
apply arith
done
- then interpret int!: lattice "?Z" .
+ then interpret int: lattice "?Z" .
show "join ?Z x y = max x y"
apply (rule int.joinI)
apply (simp_all add: least_def Upper_def)
@@ -245,7 +245,7 @@
done
qed
-interpretation int! (* [unfolded UNIV] *) :
+interpretation int (* [unfolded UNIV] *) :
total_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
proof qed clarsimp
--- a/src/HOL/Algebra/RingHom.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOL/Algebra/RingHom.thy Thu Mar 26 20:09:58 2009 +0100
@@ -61,8 +61,8 @@
assumes h: "h \<in> ring_hom R S"
shows "ring_hom_ring R S h"
proof -
- interpret R!: ring R by fact
- interpret S!: ring S by fact
+ interpret R: ring R by fact
+ interpret S: ring S by fact
show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
apply (rule R.is_ring)
apply (rule S.is_ring)
@@ -78,8 +78,8 @@
shows "ring_hom_ring R S h"
proof -
interpret abelian_group_hom R S h by fact
- interpret R!: ring R by fact
- interpret S!: ring S by fact
+ interpret R: ring R by fact
+ interpret S: ring S by fact
show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring)
apply (insert group_hom.homh[OF a_group_hom])
apply (unfold hom_def ring_hom_def, simp)
@@ -94,8 +94,8 @@
shows "ring_hom_cring R S h"
proof -
interpret ring_hom_ring R S h by fact
- interpret R!: cring R by fact
- interpret S!: cring S by fact
+ interpret R: cring R by fact
+ interpret S: cring S by fact
show ?thesis by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro)
(rule R.is_cring, rule S.is_cring, rule homh)
qed
--- a/src/HOL/Algebra/UnivPoly.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOL/Algebra/UnivPoly.thy Thu Mar 26 20:09:58 2009 +0100
@@ -1886,7 +1886,7 @@
"UP INTEG"} globally.
*}
-interpretation INTEG!: UP_pre_univ_prop INTEG INTEG id "UP INTEG"
+interpretation INTEG: UP_pre_univ_prop INTEG INTEG id "UP INTEG"
using INTEG_id_eval by simp_all
lemma INTEG_closed [intro, simp]:
--- a/src/HOL/Complex.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOL/Complex.thy Thu Mar 26 20:09:58 2009 +0100
@@ -348,13 +348,13 @@
subsection {* Completeness of the Complexes *}
-interpretation Re!: bounded_linear "Re"
+interpretation Re: bounded_linear "Re"
apply (unfold_locales, simp, simp)
apply (rule_tac x=1 in exI)
apply (simp add: complex_norm_def)
done
-interpretation Im!: bounded_linear "Im"
+interpretation Im: bounded_linear "Im"
apply (unfold_locales, simp, simp)
apply (rule_tac x=1 in exI)
apply (simp add: complex_norm_def)
@@ -516,7 +516,7 @@
lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<twosuperior>"
by (simp add: norm_mult power2_eq_square)
-interpretation cnj!: bounded_linear "cnj"
+interpretation cnj: bounded_linear "cnj"
apply (unfold_locales)
apply (rule complex_cnj_add)
apply (rule complex_cnj_scaleR)
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Thu Mar 26 20:09:58 2009 +0100
@@ -637,7 +637,7 @@
using eq_diff_eq[where a= x and b=t and c=0] by simp
-interpretation class_ordered_field_dense_linear_order!: constr_dense_linear_order
+interpretation class_ordered_field_dense_linear_order: constr_dense_linear_order
"op <=" "op <"
"\<lambda> x y. 1/2 * ((x::'a::{ordered_field,recpower,number_ring}) + y)"
proof (unfold_locales, dlo, dlo, auto)
--- a/src/HOL/Divides.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOL/Divides.thy Thu Mar 26 20:09:58 2009 +0100
@@ -852,7 +852,7 @@
text {* @{term "op dvd"} is a partial order *}
-interpretation dvd!: order "op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"
+interpretation dvd: order "op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"
proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym)
lemma nat_dvd_diff[simp]: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
--- a/src/HOL/Finite_Set.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOL/Finite_Set.thy Thu Mar 26 20:09:58 2009 +0100
@@ -928,7 +928,7 @@
subsection {* Generalized summation over a set *}
-interpretation comm_monoid_add!: comm_monoid_mult "0::'a::comm_monoid_add" "op +"
+interpretation comm_monoid_add: comm_monoid_mult "0::'a::comm_monoid_add" "op +"
proof qed (auto intro: add_assoc add_commute)
definition setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
--- a/src/HOL/Groebner_Basis.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOL/Groebner_Basis.thy Thu Mar 26 20:09:58 2009 +0100
@@ -163,7 +163,7 @@
end
-interpretation class_semiring!: gb_semiring
+interpretation class_semiring: gb_semiring
"op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"
proof qed (auto simp add: algebra_simps power_Suc)
@@ -242,7 +242,7 @@
end
-interpretation class_ring!: gb_ring "op +" "op *" "op ^"
+interpretation class_ring: gb_ring "op +" "op *" "op ^"
"0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"
proof qed simp_all
@@ -343,7 +343,7 @@
thus "b = 0" by blast
qed
-interpretation class_ringb!: ringb
+interpretation class_ringb: ringb
"op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus"
proof(unfold_locales, simp add: algebra_simps power_Suc, auto)
fix w x y z ::"'a::{idom,recpower,number_ring}"
@@ -359,7 +359,7 @@
declaration {* normalizer_funs @{thm class_ringb.ringb_axioms'} *}
-interpretation natgb!: semiringb
+interpretation natgb: semiringb
"op +" "op *" "op ^" "0::nat" "1"
proof (unfold_locales, simp add: algebra_simps power_Suc)
fix w x y z ::"nat"
@@ -463,7 +463,7 @@
subsection{* Groebner Bases for fields *}
-interpretation class_fieldgb!:
+interpretation class_fieldgb:
fieldgb "op +" "op *" "op ^" "0::'a::{field,recpower,number_ring}" "1" "op -" "uminus" "op /" "inverse" apply (unfold_locales) by (simp_all add: divide_inverse)
lemma divide_Numeral1: "(x::'a::{field,number_ring}) / Numeral1 = x" by simp
--- a/src/HOL/HahnBanach/Subspace.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOL/HahnBanach/Subspace.thy Thu Mar 26 20:09:58 2009 +0100
@@ -59,7 +59,7 @@
assumes "vectorspace V"
shows "0 \<in> U"
proof -
- interpret V!: vectorspace V by fact
+ interpret V: vectorspace V by fact
have "U \<noteq> {}" by (rule non_empty)
then obtain x where x: "x \<in> U" by blast
then have "x \<in> V" .. then have "0 = x - x" by simp
--- a/src/HOL/Lattices.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOL/Lattices.thy Thu Mar 26 20:09:58 2009 +0100
@@ -299,7 +299,7 @@
by auto
qed (auto simp add: min_def max_def not_le less_imp_le)
-interpretation min_max!: distrib_lattice "op \<le> :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max
+interpretation min_max: distrib_lattice "op \<le> :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max
by (rule distrib_lattice_min_max)
lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{lower_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
--- a/src/HOL/Library/FrechetDeriv.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOL/Library/FrechetDeriv.thy Thu Mar 26 20:09:58 2009 +0100
@@ -222,8 +222,8 @@
let ?k = "\<lambda>h. f (x + h) - f x"
let ?Nf = "\<lambda>h. norm (?Rf h) / norm h"
let ?Ng = "\<lambda>h. norm (?Rg (?k h)) / norm (?k h)"
- from f interpret F!: bounded_linear "F" by (rule FDERIV_bounded_linear)
- from g interpret G!: bounded_linear "G" by (rule FDERIV_bounded_linear)
+ from f interpret F: bounded_linear "F" by (rule FDERIV_bounded_linear)
+ from g interpret G: bounded_linear "G" by (rule FDERIV_bounded_linear)
from F.bounded obtain kF where kF: "\<And>x. norm (F x) \<le> norm x * kF" by fast
from G.bounded obtain kG where kG: "\<And>x. norm (G x) \<le> norm x * kG" by fast
--- a/src/HOL/Library/Inner_Product.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOL/Library/Inner_Product.thy Thu Mar 26 20:09:58 2009 +0100
@@ -116,7 +116,7 @@
end
-interpretation inner!:
+interpretation inner:
bounded_bilinear "inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real"
proof
fix x y z :: 'a and r :: real
@@ -135,11 +135,11 @@
qed
qed
-interpretation inner_left!:
+interpretation inner_left:
bounded_linear "\<lambda>x::'a::real_inner. inner x y"
by (rule inner.bounded_linear_left)
-interpretation inner_right!:
+interpretation inner_right:
bounded_linear "\<lambda>y::'a::real_inner. inner x y"
by (rule inner.bounded_linear_right)
--- a/src/HOL/Library/Multiset.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOL/Library/Multiset.thy Thu Mar 26 20:09:58 2009 +0100
@@ -1077,15 +1077,15 @@
apply simp
done
-interpretation mset_order!: order "op \<le>#" "op <#"
+interpretation mset_order: order "op \<le>#" "op <#"
proof qed (auto intro: order.intro mset_le_refl mset_le_antisym
mset_le_trans simp: mset_less_def)
-interpretation mset_order_cancel_semigroup!:
+interpretation mset_order_cancel_semigroup:
pordered_cancel_ab_semigroup_add "op +" "op \<le>#" "op <#"
proof qed (erule mset_le_mono_add [OF mset_le_refl])
-interpretation mset_order_semigroup_cancel!:
+interpretation mset_order_semigroup_cancel:
pordered_ab_semigroup_add_imp_le "op +" "op \<le>#" "op <#"
proof qed simp
@@ -1433,7 +1433,7 @@
definition [code del]:
"image_mset f = fold_mset (op + o single o f) {#}"
-interpretation image_left_comm!: left_commutative "op + o single o f"
+interpretation image_left_comm: left_commutative "op + o single o f"
proof qed (simp add:union_ac)
lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
--- a/src/HOL/Library/Numeral_Type.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOL/Library/Numeral_Type.thy Thu Mar 26 20:09:58 2009 +0100
@@ -313,7 +313,7 @@
end
-interpretation bit0!:
+interpretation bit0:
mod_type "int CARD('a::finite bit0)"
"Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int"
"Abs_bit0 :: int \<Rightarrow> 'a::finite bit0"
@@ -329,7 +329,7 @@
apply (rule power_bit0_def [unfolded Abs_bit0'_def])
done
-interpretation bit1!:
+interpretation bit1:
mod_type "int CARD('a::finite bit1)"
"Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int"
"Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"
@@ -363,13 +363,13 @@
end
-interpretation bit0!:
+interpretation bit0:
mod_ring "int CARD('a::finite bit0)"
"Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int"
"Abs_bit0 :: int \<Rightarrow> 'a::finite bit0"
..
-interpretation bit1!:
+interpretation bit1:
mod_ring "int CARD('a::finite bit1)"
"Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int"
"Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"
--- a/src/HOL/Library/Product_Vector.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOL/Library/Product_Vector.thy Thu Mar 26 20:09:58 2009 +0100
@@ -116,14 +116,14 @@
subsection {* Pair operations are linear and continuous *}
-interpretation fst!: bounded_linear fst
+interpretation fst: bounded_linear fst
apply (unfold_locales)
apply (rule fst_add)
apply (rule fst_scaleR)
apply (rule_tac x="1" in exI, simp add: norm_Pair)
done
-interpretation snd!: bounded_linear snd
+interpretation snd: bounded_linear snd
apply (unfold_locales)
apply (rule snd_add)
apply (rule snd_scaleR)
--- a/src/HOL/Library/SetsAndFunctions.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOL/Library/SetsAndFunctions.thy Thu Mar 26 20:09:58 2009 +0100
@@ -107,26 +107,26 @@
apply simp
done
-interpretation set_semigroup_add!: semigroup_add "op \<oplus> :: ('a::semigroup_add) set => 'a set => 'a set"
+interpretation set_semigroup_add: semigroup_add "op \<oplus> :: ('a::semigroup_add) set => 'a set => 'a set"
apply default
apply (unfold set_plus_def)
apply (force simp add: add_assoc)
done
-interpretation set_semigroup_mult!: semigroup_mult "op \<otimes> :: ('a::semigroup_mult) set => 'a set => 'a set"
+interpretation set_semigroup_mult: semigroup_mult "op \<otimes> :: ('a::semigroup_mult) set => 'a set => 'a set"
apply default
apply (unfold set_times_def)
apply (force simp add: mult_assoc)
done
-interpretation set_comm_monoid_add!: comm_monoid_add "{0}" "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set"
+interpretation set_comm_monoid_add: comm_monoid_add "{0}" "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set"
apply default
apply (unfold set_plus_def)
apply (force simp add: add_ac)
apply force
done
-interpretation set_comm_monoid_mult!: comm_monoid_mult "{1}" "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set"
+interpretation set_comm_monoid_mult: comm_monoid_mult "{1}" "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set"
apply default
apply (unfold set_times_def)
apply (force simp add: mult_ac)
--- a/src/HOL/NSA/StarDef.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOL/NSA/StarDef.thy Thu Mar 26 20:09:58 2009 +0100
@@ -23,7 +23,7 @@
apply (rule nat_infinite)
done
-interpretation FreeUltrafilterNat!: freeultrafilter FreeUltrafilterNat
+interpretation FreeUltrafilterNat: freeultrafilter FreeUltrafilterNat
by (rule freeultrafilter_FreeUltrafilterNat)
text {* This rule takes the place of the old ultra tactic *}
--- a/src/HOL/RealVector.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOL/RealVector.thy Thu Mar 26 20:09:58 2009 +0100
@@ -145,7 +145,7 @@
and scaleR_scaleR: "scaleR a (scaleR b x) = scaleR (a * b) x"
and scaleR_one: "scaleR 1 x = x"
-interpretation real_vector!:
+interpretation real_vector:
vector_space "scaleR :: real \<Rightarrow> 'a \<Rightarrow> 'a::real_vector"
apply unfold_locales
apply (rule scaleR_right_distrib)
@@ -190,10 +190,10 @@
end
-interpretation scaleR_left!: additive "(\<lambda>a. scaleR a x::'a::real_vector)"
+interpretation scaleR_left: additive "(\<lambda>a. scaleR a x::'a::real_vector)"
proof qed (rule scaleR_left_distrib)
-interpretation scaleR_right!: additive "(\<lambda>x. scaleR a x::'a::real_vector)"
+interpretation scaleR_right: additive "(\<lambda>x. scaleR a x::'a::real_vector)"
proof qed (rule scaleR_right_distrib)
lemma nonzero_inverse_scaleR_distrib:
@@ -789,7 +789,7 @@
end
-interpretation mult!:
+interpretation mult:
bounded_bilinear "op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra"
apply (rule bounded_bilinear.intro)
apply (rule left_distrib)
@@ -800,19 +800,19 @@
apply (simp add: norm_mult_ineq)
done
-interpretation mult_left!:
+interpretation mult_left:
bounded_linear "(\<lambda>x::'a::real_normed_algebra. x * y)"
by (rule mult.bounded_linear_left)
-interpretation mult_right!:
+interpretation mult_right:
bounded_linear "(\<lambda>y::'a::real_normed_algebra. x * y)"
by (rule mult.bounded_linear_right)
-interpretation divide!:
+interpretation divide:
bounded_linear "(\<lambda>x::'a::real_normed_field. x / y)"
unfolding divide_inverse by (rule mult.bounded_linear_left)
-interpretation scaleR!: bounded_bilinear "scaleR"
+interpretation scaleR: bounded_bilinear "scaleR"
apply (rule bounded_bilinear.intro)
apply (rule scaleR_left_distrib)
apply (rule scaleR_right_distrib)
@@ -822,13 +822,13 @@
apply (simp add: norm_scaleR)
done
-interpretation scaleR_left!: bounded_linear "\<lambda>r. scaleR r x"
+interpretation scaleR_left: bounded_linear "\<lambda>r. scaleR r x"
by (rule scaleR.bounded_linear_left)
-interpretation scaleR_right!: bounded_linear "\<lambda>x. scaleR r x"
+interpretation scaleR_right: bounded_linear "\<lambda>x. scaleR r x"
by (rule scaleR.bounded_linear_right)
-interpretation of_real!: bounded_linear "\<lambda>r. of_real r"
+interpretation of_real: bounded_linear "\<lambda>r. of_real r"
unfolding of_real_def by (rule scaleR.bounded_linear_left)
end
--- a/src/HOL/Word/TdThs.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOL/Word/TdThs.thy Thu Mar 26 20:09:58 2009 +0100
@@ -89,7 +89,7 @@
end
-interpretation nat_int!: type_definition int nat "Collect (op <= 0)"
+interpretation nat_int: type_definition int nat "Collect (op <= 0)"
by (rule td_nat_int)
declare
--- a/src/HOL/Word/WordArith.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOL/Word/WordArith.thy Thu Mar 26 20:09:58 2009 +0100
@@ -21,7 +21,7 @@
proof
qed (unfold word_sle_def word_sless_def, auto)
-interpretation signed!: linorder "word_sle" "word_sless"
+interpretation signed: linorder "word_sle" "word_sless"
by (rule signed_linorder)
lemmas word_arith_wis =
@@ -862,7 +862,7 @@
lemmas td_ext_unat = refl [THEN td_ext_unat']
lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm, standard]
-interpretation word_unat!:
+interpretation word_unat:
td_ext "unat::'a::len word => nat"
of_nat
"unats (len_of TYPE('a::len))"
--- a/src/HOL/Word/WordBitwise.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOL/Word/WordBitwise.thy Thu Mar 26 20:09:58 2009 +0100
@@ -343,7 +343,7 @@
lemmas td_ext_nth = td_ext_nth' [OF refl refl refl, unfolded word_size]
-interpretation test_bit!:
+interpretation test_bit:
td_ext "op !! :: 'a::len0 word => nat => bool"
set_bits
"{f. \<forall>i. f i \<longrightarrow> i < len_of TYPE('a::len0)}"
--- a/src/HOL/Word/WordDefinition.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOL/Word/WordDefinition.thy Thu Mar 26 20:09:58 2009 +0100
@@ -351,7 +351,7 @@
lemmas int_word_uint = td_ext_uint [THEN td_ext.eq_norm, standard]
-interpretation word_uint!:
+interpretation word_uint:
td_ext "uint::'a::len0 word \<Rightarrow> int"
word_of_int
"uints (len_of TYPE('a::len0))"
@@ -363,7 +363,7 @@
lemmas td_ext_ubin = td_ext_uint
[simplified len_gt_0 no_bintr_alt1 [symmetric]]
-interpretation word_ubin!:
+interpretation word_ubin:
td_ext "uint::'a::len0 word \<Rightarrow> int"
word_of_int
"uints (len_of TYPE('a::len0))"
@@ -418,7 +418,7 @@
and interpretations do not produce thm duplicates. I.e.
we get the name word_sint.Rep_eqD, but not word_sbin.Req_eqD,
because the latter is the same thm as the former *)
-interpretation word_sint!:
+interpretation word_sint:
td_ext "sint ::'a::len word => int"
word_of_int
"sints (len_of TYPE('a::len))"
@@ -426,7 +426,7 @@
2 ^ (len_of TYPE('a::len) - 1)"
by (rule td_ext_sint)
-interpretation word_sbin!:
+interpretation word_sbin:
td_ext "sint ::'a::len word => int"
word_of_int
"sints (len_of TYPE('a::len))"
@@ -630,7 +630,7 @@
apply simp
done
-interpretation word_bl!:
+interpretation word_bl:
type_definition "to_bl :: 'a::len0 word => bool list"
of_bl
"{bl. length bl = len_of TYPE('a::len0)}"
--- a/src/HOL/Word/WordGenLib.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOL/Word/WordGenLib.thy Thu Mar 26 20:09:58 2009 +0100
@@ -106,7 +106,7 @@
apply (rule word_or_not)
done
-interpretation word_bool_alg!:
+interpretation word_bool_alg:
boolean "op AND" "op OR" bitNOT 0 max_word
by (rule word_boolean)
@@ -114,7 +114,7 @@
"x XOR y = x AND NOT y OR NOT x AND (y::'a::len0 word)"
by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
-interpretation word_bool_alg!:
+interpretation word_bool_alg:
boolean_xor "op AND" "op OR" bitNOT 0 max_word "op XOR"
apply (rule boolean_xor.intro)
apply (rule word_boolean)
--- a/src/HOL/ex/LocaleTest2.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOL/ex/LocaleTest2.thy Thu Mar 26 20:09:58 2009 +0100
@@ -468,7 +468,7 @@
subsubsection {* Total order @{text "<="} on @{typ int} *}
-interpretation int!: dpo "op <= :: [int, int] => bool"
+interpretation int: dpo "op <= :: [int, int] => bool"
where "(dpo.less (op <=) (x::int) y) = (x < y)"
txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
proof -
@@ -487,7 +487,7 @@
lemma "(op < :: [int, int] => bool) = op <"
apply (rule int.abs_test) done
-interpretation int!: dlat "op <= :: [int, int] => bool"
+interpretation int: dlat "op <= :: [int, int] => bool"
where meet_eq: "dlat.meet (op <=) (x::int) y = min x y"
and join_eq: "dlat.join (op <=) (x::int) y = max x y"
proof -
@@ -511,7 +511,7 @@
by auto
qed
-interpretation int!: dlo "op <= :: [int, int] => bool"
+interpretation int: dlo "op <= :: [int, int] => bool"
proof qed arith
text {* Interpreted theorems from the locales, involving defined terms. *}
@@ -524,7 +524,7 @@
subsubsection {* Total order @{text "<="} on @{typ nat} *}
-interpretation nat!: dpo "op <= :: [nat, nat] => bool"
+interpretation nat: dpo "op <= :: [nat, nat] => bool"
where "dpo.less (op <=) (x::nat) y = (x < y)"
txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
proof -
@@ -538,7 +538,7 @@
done
qed
-interpretation nat!: dlat "op <= :: [nat, nat] => bool"
+interpretation nat: dlat "op <= :: [nat, nat] => bool"
where "dlat.meet (op <=) (x::nat) y = min x y"
and "dlat.join (op <=) (x::nat) y = max x y"
proof -
@@ -562,7 +562,7 @@
by auto
qed
-interpretation nat!: dlo "op <= :: [nat, nat] => bool"
+interpretation nat: dlo "op <= :: [nat, nat] => bool"
proof qed arith
text {* Interpreted theorems from the locales, involving defined terms. *}
@@ -575,7 +575,7 @@
subsubsection {* Lattice @{text "dvd"} on @{typ nat} *}
-interpretation nat_dvd!: dpo "op dvd :: [nat, nat] => bool"
+interpretation nat_dvd: dpo "op dvd :: [nat, nat] => bool"
where "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)"
txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
proof -
@@ -589,7 +589,7 @@
done
qed
-interpretation nat_dvd!: dlat "op dvd :: [nat, nat] => bool"
+interpretation nat_dvd: dlat "op dvd :: [nat, nat] => bool"
where "dlat.meet (op dvd) (x::nat) y = gcd x y"
and "dlat.join (op dvd) (x::nat) y = lcm x y"
proof -
@@ -834,7 +834,7 @@
subsubsection {* Interpretation of Functions *}
-interpretation Dfun!: Dmonoid "op o" "id :: 'a => 'a"
+interpretation Dfun: Dmonoid "op o" "id :: 'a => 'a"
where "Dmonoid.unit (op o) id f = bij (f::'a => 'a)"
(* and "Dmonoid.inv (op o) id" = "inv :: ('a => 'a) => ('a => 'a)" *)
proof -
@@ -884,7 +884,7 @@
"(f :: unit => unit) = id"
by rule simp
-interpretation Dfun!: Dgrp "op o" "id :: unit => unit"
+interpretation Dfun: Dgrp "op o" "id :: unit => unit"
where "Dmonoid.inv (op o) id f = inv (f :: unit => unit)"
proof -
have "Dmonoid op o (id :: 'a => 'a)" ..
--- a/src/HOLCF/Algebraic.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOLCF/Algebraic.thy Thu Mar 26 20:09:58 2009 +0100
@@ -215,7 +215,7 @@
lemma finite_deflation_Rep_fin_defl: "finite_deflation (Rep_fin_defl d)"
using Rep_fin_defl by simp
-interpretation Rep_fin_defl!: finite_deflation "Rep_fin_defl d"
+interpretation Rep_fin_defl: finite_deflation "Rep_fin_defl d"
by (rule finite_deflation_Rep_fin_defl)
lemma fin_defl_lessI:
@@ -320,7 +320,7 @@
apply (rule Rep_fin_defl.compact)
done
-interpretation fin_defl!: basis_take sq_le fd_take
+interpretation fin_defl: basis_take sq_le fd_take
apply default
apply (rule fd_take_less)
apply (rule fd_take_idem)
@@ -370,7 +370,7 @@
unfolding alg_defl_principal_def
by (simp add: Abs_alg_defl_inverse sq_le.ideal_principal)
-interpretation alg_defl!:
+interpretation alg_defl:
ideal_completion sq_le fd_take alg_defl_principal Rep_alg_defl
apply default
apply (rule ideal_Rep_alg_defl)
@@ -461,7 +461,7 @@
apply (rule finite_deflation_Rep_fin_defl)
done
-interpretation cast!: deflation "cast\<cdot>d"
+interpretation cast: deflation "cast\<cdot>d"
by (rule deflation_cast)
lemma "cast\<cdot>(\<Squnion>i. alg_defl_principal (Abs_fin_defl (approx i)))\<cdot>x = x"
--- a/src/HOLCF/Bifinite.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOLCF/Bifinite.thy Thu Mar 26 20:09:58 2009 +0100
@@ -37,7 +37,7 @@
by (rule finite_fixes_approx)
qed
-interpretation approx!: finite_deflation "approx i"
+interpretation approx: finite_deflation "approx i"
by (rule finite_deflation_approx)
lemma (in deflation) deflation: "deflation d" ..
--- a/src/HOLCF/CompactBasis.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOLCF/CompactBasis.thy Thu Mar 26 20:09:58 2009 +0100
@@ -46,7 +46,7 @@
lemmas approx_Rep_compact_basis = Rep_compact_take [symmetric]
-interpretation compact_basis!:
+interpretation compact_basis:
basis_take sq_le compact_take
proof
fix n :: nat and a :: "'a compact_basis"
@@ -92,7 +92,7 @@
approximants :: "'a \<Rightarrow> 'a compact_basis set" where
"approximants = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})"
-interpretation compact_basis!:
+interpretation compact_basis:
ideal_completion sq_le compact_take Rep_compact_basis approximants
proof
fix w :: 'a
--- a/src/HOLCF/Completion.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOLCF/Completion.thy Thu Mar 26 20:09:58 2009 +0100
@@ -156,7 +156,7 @@
end
-interpretation sq_le!: preorder "sq_le :: 'a::po \<Rightarrow> 'a \<Rightarrow> bool"
+interpretation sq_le: preorder "sq_le :: 'a::po \<Rightarrow> 'a \<Rightarrow> bool"
apply unfold_locales
apply (rule refl_less)
apply (erule (1) trans_less)
--- a/src/HOLCF/ConvexPD.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOLCF/ConvexPD.thy Thu Mar 26 20:09:58 2009 +0100
@@ -20,7 +20,7 @@
lemma convex_le_trans: "\<lbrakk>t \<le>\<natural> u; u \<le>\<natural> v\<rbrakk> \<Longrightarrow> t \<le>\<natural> v"
unfolding convex_le_def by (fast intro: upper_le_trans lower_le_trans)
-interpretation convex_le!: preorder convex_le
+interpretation convex_le: preorder convex_le
by (rule preorder.intro, rule convex_le_refl, rule convex_le_trans)
lemma upper_le_minimal [simp]: "PDUnit compact_bot \<le>\<natural> t"
@@ -178,7 +178,7 @@
unfolding convex_principal_def
by (simp add: Abs_convex_pd_inverse convex_le.ideal_principal)
-interpretation convex_pd!:
+interpretation convex_pd:
ideal_completion convex_le pd_take convex_principal Rep_convex_pd
apply unfold_locales
apply (rule pd_take_convex_le)
--- a/src/HOLCF/LowerPD.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOLCF/LowerPD.thy Thu Mar 26 20:09:58 2009 +0100
@@ -26,7 +26,7 @@
apply (erule (1) trans_less)
done
-interpretation lower_le!: preorder lower_le
+interpretation lower_le: preorder lower_le
by (rule preorder.intro, rule lower_le_refl, rule lower_le_trans)
lemma lower_le_minimal [simp]: "PDUnit compact_bot \<le>\<flat> t"
@@ -133,7 +133,7 @@
unfolding lower_principal_def
by (simp add: Abs_lower_pd_inverse lower_le.ideal_principal)
-interpretation lower_pd!:
+interpretation lower_pd:
ideal_completion lower_le pd_take lower_principal Rep_lower_pd
apply unfold_locales
apply (rule pd_take_lower_le)
--- a/src/HOLCF/Universal.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOLCF/Universal.thy Thu Mar 26 20:09:58 2009 +0100
@@ -230,13 +230,13 @@
apply (simp add: ubasis_take_same)
done
-interpretation udom!: preorder ubasis_le
+interpretation udom: preorder ubasis_le
apply default
apply (rule ubasis_le_refl)
apply (erule (1) ubasis_le_trans)
done
-interpretation udom!: basis_take ubasis_le ubasis_take
+interpretation udom: basis_take ubasis_le ubasis_take
apply default
apply (rule ubasis_take_less)
apply (rule ubasis_take_idem)
@@ -285,7 +285,7 @@
unfolding udom_principal_def
by (simp add: Abs_udom_inverse udom.ideal_principal)
-interpretation udom!:
+interpretation udom:
ideal_completion ubasis_le ubasis_take udom_principal Rep_udom
apply unfold_locales
apply (rule ideal_Rep_udom)
--- a/src/HOLCF/UpperPD.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/HOLCF/UpperPD.thy Thu Mar 26 20:09:58 2009 +0100
@@ -26,7 +26,7 @@
apply (erule (1) trans_less)
done
-interpretation upper_le!: preorder upper_le
+interpretation upper_le: preorder upper_le
by (rule preorder.intro, rule upper_le_refl, rule upper_le_trans)
lemma upper_le_minimal [simp]: "PDUnit compact_bot \<le>\<sharp> t"
@@ -131,7 +131,7 @@
unfolding upper_principal_def
by (simp add: Abs_upper_pd_inverse upper_le.ideal_principal)
-interpretation upper_pd!:
+interpretation upper_pd:
ideal_completion upper_le pd_take upper_principal Rep_upper_pd
apply unfold_locales
apply (rule pd_take_upper_le)
--- a/src/Pure/Isar/expression.ML Thu Mar 26 11:33:50 2009 -0700
+++ b/src/Pure/Isar/expression.ML Thu Mar 26 20:09:58 2009 +0100
@@ -203,7 +203,7 @@
fun parse_concl prep_term ctxt concl =
(map o map) (fn (t, ps) =>
- (prep_term (ProofContext.set_mode ProofContext.mode_schematic ctxt) t, (* FIXME ?? *)
+ (prep_term (ProofContext.set_mode ProofContext.mode_schematic ctxt) t,
map (prep_term (ProofContext.set_mode ProofContext.mode_pattern ctxt)) ps)) concl;
@@ -288,13 +288,13 @@
fun closeup _ _ false elem = elem
| closeup ctxt parms true elem =
let
+ (* FIXME consider closing in syntactic phase -- before type checking *)
fun close_frees t =
let
val rev_frees =
Term.fold_aterms (fn Free (x, T) =>
if AList.defined (op =) parms x then I else insert (op =) (x, T) | _ => I) t [];
- in Term.list_all_free (rev rev_frees, t) end; (* FIXME use fold Logic.all *)
- (* FIXME consider closing in syntactic phase *)
+ in fold (Logic.all o Free) rev_frees t end;
fun no_binds [] = []
| no_binds _ = error "Illegal term bindings in context element";
@@ -325,9 +325,7 @@
in (loc, morph) end;
fun finish_elem ctxt parms do_close elem =
- let
- val elem' = finish_primitive parms (closeup ctxt parms do_close) elem;
- in elem' end
+ finish_primitive parms (closeup ctxt parms do_close) elem;
fun finish ctxt parms do_close insts elems =
let
@@ -363,7 +361,7 @@
val inst''' = insts'' |> List.last |> snd |> snd;
val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst''') ctxt;
val ctxt'' = Locale.activate_declarations thy (loc, morph) ctxt;
- in (i+1, insts', ctxt'') end;
+ in (i + 1, insts', ctxt'') end;
fun prep_elem insts raw_elem (elems, ctxt) =
let
@@ -564,9 +562,7 @@
in text' end;
fun eval_elem ctxt elem text =
- let
- val text' = eval_text ctxt true elem text;
- in text' end;
+ eval_text ctxt true elem text;
fun eval ctxt deps elems =
let
@@ -676,7 +672,7 @@
thy'
|> Sign.mandatory_path (Binding.name_of aname)
|> PureThy.note_thmss Thm.internalK
- [((Binding.name introN, []), [([intro], [Locale.unfold_attrib])])]
+ [((Binding.name introN, []), [([intro], [Locale.unfold_add])])]
||> Sign.restore_naming thy';
in (SOME statement, SOME intro, axioms, thy'') end;
val (b_pred, b_intro, b_axioms, thy'''') =
@@ -690,7 +686,7 @@
thy'''
|> Sign.mandatory_path (Binding.name_of pname)
|> PureThy.note_thmss Thm.internalK
- [((Binding.name introN, []), [([intro], [Locale.intro_attrib])]),
+ [((Binding.name introN, []), [([intro], [Locale.intro_add])]),
((Binding.name axiomsN, []),
[(map (Drule.standard o Element.conclude_witness) axioms, [])])]
||> Sign.restore_naming thy''';
@@ -712,7 +708,7 @@
fun defines_to_notes thy (Defines defs) =
Notes (Thm.definitionK, map (fn (a, (def, _)) =>
(a, [([Assumption.assume (cterm_of thy def)],
- [(Attrib.internal o K) Locale.witness_attrib])])) defs)
+ [(Attrib.internal o K) Locale.witness_add])])) defs)
| defines_to_notes _ e = e;
fun gen_add_locale prep_decl
@@ -745,11 +741,11 @@
val asm = if is_some b_statement then b_statement else a_statement;
val notes =
- if is_some asm
- then [(Thm.internalK, [((Binding.suffix_name ("_" ^ axiomsN) bname, []),
- [([Assumption.assume (cterm_of thy' (the asm))],
- [(Attrib.internal o K) Locale.witness_attrib])])])]
- else [];
+ if is_some asm
+ then [(Thm.internalK, [((Binding.suffix_name ("_" ^ axiomsN) bname, []),
+ [([Assumption.assume (cterm_of thy' (the asm))],
+ [(Attrib.internal o K) Locale.witness_add])])])]
+ else [];
val notes' = body_elems |>
map (defines_to_notes thy') |>
@@ -764,8 +760,7 @@
val loc_ctxt = thy'
|> Locale.register_locale bname (extraTs, params)
- (asm, rev defs) (a_intro, b_intro) axioms ([], [])
- (map (fn n => (n, stamp ())) notes |> rev) (map (fn d => (d, stamp ())) deps' |> rev)
+ (asm, rev defs) (a_intro, b_intro) axioms ([], []) (rev notes) (rev deps')
|> TheoryTarget.init (SOME name)
|> fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes';
@@ -792,11 +787,11 @@
val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
- fun after_qed witss = ProofContext.theory (
- fold2 (fn (name, morph) => fn wits => Locale.add_dependency target
+ fun after_qed witss = ProofContext.theory
+ (fold2 (fn (name, morph) => fn wits => Locale.add_dependency target
(name, morph $> Element.satisfy_morphism wits $> export)) deps witss #>
(fn thy => fold_rev Locale.activate_global_facts
- (Locale.get_registrations thy) thy));
+ (Locale.get_registrations thy) thy));
in Element.witness_proof after_qed propss goal_ctxt end;
in
--- a/src/Pure/Isar/isar_syn.ML Thu Mar 26 11:33:50 2009 -0700
+++ b/src/Pure/Isar/isar_syn.ML Thu Mar 26 20:09:58 2009 +0100
@@ -404,7 +404,7 @@
(* locales *)
val locale_val =
- SpecParse.locale_expression --
+ SpecParse.locale_expression false --
Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
Scan.repeat1 SpecParse.context_element >> pair ([], []);
@@ -418,25 +418,24 @@
val _ =
OuterSyntax.command "sublocale"
"prove sublocale relation between a locale and a locale expression" K.thy_goal
- (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expression
+ (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! (SpecParse.locale_expression false)
>> (fn (loc, expr) =>
- Toplevel.print o (Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr))));
+ Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr)));
val _ =
OuterSyntax.command "interpretation"
"prove interpretation of locale expression in theory" K.thy_goal
- (P.!!! SpecParse.locale_expression --
- Scan.optional (P.$$$ "where" |-- P.and_list1 (SpecParse.opt_thm_name ":" -- P.prop)) []
- >> (fn (expr, equations) => Toplevel.print o
- Toplevel.theory_to_proof (Expression.interpretation_cmd expr equations)));
+ (P.!!! (SpecParse.locale_expression true) --
+ Scan.optional (P.where_ |-- P.and_list1 (SpecParse.opt_thm_name ":" -- P.prop)) []
+ >> (fn (expr, equations) => Toplevel.print o
+ Toplevel.theory_to_proof (Expression.interpretation_cmd expr equations)));
val _ =
OuterSyntax.command "interpret"
"prove interpretation of locale expression in proof context"
(K.tag_proof K.prf_goal)
- (P.!!! SpecParse.locale_expression
- >> (fn expr => Toplevel.print o
- Toplevel.proof' (fn int => Expression.interpret_cmd expr int)));
+ (P.!!! (SpecParse.locale_expression true)
+ >> (fn expr => Toplevel.print o Toplevel.proof' (Expression.interpret_cmd expr)));
(* classes *)
--- a/src/Pure/Isar/locale.ML Thu Mar 26 11:33:50 2009 -0700
+++ b/src/Pure/Isar/locale.ML Thu Mar 26 20:09:58 2009 +0100
@@ -1,8 +1,7 @@
(* Title: Pure/Isar/locale.ML
Author: Clemens Ballarin, TU Muenchen
-Locales -- Isar proof contexts as meta-level predicates, with local
-syntax and implicit structures.
+Locales -- managed Isar proof contexts, based on Pure predicates.
Draws basic ideas from Florian Kammueller's original version of
locales, but uses the richer infrastructure of Isar instead of the raw
@@ -34,9 +33,9 @@
(string * sort) list * (binding * typ option * mixfix) list ->
term option * term list ->
thm option * thm option -> thm list ->
- (declaration * stamp) list * (declaration * stamp) list ->
- ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list ->
- ((string * morphism) * stamp) list -> theory -> theory
+ declaration list * declaration list ->
+ (string * (Attrib.binding * (thm list * Attrib.src list) list) list) list ->
+ (string * morphism) list -> theory -> theory
val intern: theory -> xstring -> string
val extern: theory -> string -> xstring
val defined: theory -> string -> bool
@@ -64,16 +63,17 @@
val init: string -> theory -> Proof.context
(* Reasoning about locales *)
- val witness_attrib: attribute
- val intro_attrib: attribute
- val unfold_attrib: attribute
+ val get_witnesses: Proof.context -> thm list
+ val get_intros: Proof.context -> thm list
+ val get_unfolds: Proof.context -> thm list
+ val witness_add: attribute
+ val intro_add: attribute
+ val unfold_add: attribute
val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
(* Registrations *)
- val add_registration: string * (morphism * morphism) ->
- theory -> theory
- val amend_registration: morphism -> string * morphism ->
- theory -> theory
+ val add_registration: string * (morphism * morphism) -> theory -> theory
+ val amend_registration: morphism -> string * morphism -> theory -> theory
val get_registrations: theory -> (string * morphism) list
(* Diagnostic *)
@@ -81,27 +81,6 @@
val print_locale: theory -> bool -> xstring -> unit
end;
-
-(*** Theorem list extensible via attribute --- to control intro_locales_tac ***)
-
-(* FIXME: consider moving named_thms.ML up in the build hierarchy and using that *)
-functor ThmsFun() =
-struct
-
-structure Data = GenericDataFun
-(
- type T = thm list;
- val empty = [];
- val extend = I;
- fun merge _ = Thm.merge_thms;
-);
-
-val get = Data.get o Context.Proof;
-val add = Thm.declaration_attribute (Data.map o Thm.add_thm);
-
-end;
-
-
structure Locale: LOCALE =
struct
@@ -140,7 +119,7 @@
merge (eq_snd op =) (notes, notes')),
merge (eq_snd op =) (dependencies, dependencies')));
-structure LocalesData = TheoryDataFun
+structure Locales = TheoryDataFun
(
type T = locale NameSpace.table;
val empty = NameSpace.empty_table;
@@ -149,26 +128,29 @@
fun merge _ = NameSpace.join_tables (K merge_locale);
);
-val intern = NameSpace.intern o #1 o LocalesData.get;
-val extern = NameSpace.extern o #1 o LocalesData.get;
-
-fun get_locale thy = Symtab.lookup (#2 (LocalesData.get thy));
+val intern = NameSpace.intern o #1 o Locales.get;
+val extern = NameSpace.extern o #1 o Locales.get;
-fun defined thy = is_some o get_locale thy;
+val get_locale = Symtab.lookup o #2 o Locales.get;
+val defined = Symtab.defined o #2 o Locales.get;
-fun the_locale thy name = case get_locale thy name
- of SOME (Loc loc) => loc
- | NONE => error ("Unknown locale " ^ quote name);
+fun the_locale thy name =
+ (case get_locale thy name of
+ SOME (Loc loc) => loc
+ | NONE => error ("Unknown locale " ^ quote name));
fun register_locale binding parameters spec intros axioms decls notes dependencies thy =
- thy |> LocalesData.map (NameSpace.define (Sign.naming_of thy) (binding,
- mk_locale ((parameters, spec, intros, axioms), ((decls, notes), dependencies))) #> snd);
+ thy |> Locales.map (NameSpace.define (Sign.naming_of thy)
+ (binding,
+ mk_locale ((parameters, spec, intros, axioms),
+ ((pairself (map (fn decl => (decl, stamp ()))) decls, map (fn n => (n, stamp ())) notes),
+ map (fn d => (d, stamp ())) dependencies))) #> snd);
fun change_locale name =
- LocalesData.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
+ Locales.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
fun print_locales thy =
- Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (LocalesData.get thy)))
+ Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (Locales.get thy)))
|> Pretty.writeln;
@@ -181,12 +163,12 @@
fun axioms_of thy = #axioms o the_locale thy;
fun instance_of thy name morph = params_of thy name |>
- map ((fn (b, T, _) => Free (Name.of_binding b, the T)) #> Morphism.term morph);
+ map (fn (b, T, _) => Morphism.term morph (Free (Name.of_binding b, the T)));
fun specification_of thy = #spec o the_locale thy;
fun declarations_of thy name = the_locale thy name |>
- #decls |> apfst (map fst) |> apsnd (map fst);
+ #decls |> pairself (map fst);
fun dependencies_of thy name = the_locale thy name |>
#dependencies |> map fst;
@@ -206,7 +188,7 @@
datatype 'a delayed = Ready of 'a | ToDo of ('a delayed * 'a delayed);
-structure IdentifiersData = GenericDataFun
+structure Identifiers = GenericDataFun
(
type T = identifiers delayed;
val empty = Ready empty;
@@ -220,18 +202,17 @@
| finish _ (Ready ids) = ids;
val _ = Context.>> (Context.map_theory (Theory.at_begin (fn thy =>
- (case IdentifiersData.get (Context.Theory thy) of
- Ready _ => NONE |
- ids => SOME (Context.theory_map (IdentifiersData.put (Ready (finish thy ids))) thy))
- )));
+ (case Identifiers.get (Context.Theory thy) of
+ Ready _ => NONE
+ | ids => SOME (Context.theory_map (Identifiers.put (Ready (finish thy ids))) thy)))));
fun get_global_idents thy =
- let val (Ready ids) = (IdentifiersData.get o Context.Theory) thy in ids end;
-val put_global_idents = Context.theory_map o IdentifiersData.put o Ready;
+ let val (Ready ids) = (Identifiers.get o Context.Theory) thy in ids end;
+val put_global_idents = Context.theory_map o Identifiers.put o Ready;
fun get_local_idents ctxt =
- let val (Ready ids) = (IdentifiersData.get o Context.Proof) ctxt in ids end;
-val put_local_idents = Context.proof_map o IdentifiersData.put o Ready;
+ let val (Ready ids) = (Identifiers.get o Context.Proof) ctxt in ids end;
+val put_local_idents = Context.proof_map o Identifiers.put o Ready;
end;
@@ -385,7 +366,7 @@
(*** Registrations: interpretations in theories ***)
-structure RegistrationsData = TheoryDataFun
+structure Registrations = TheoryDataFun
(
type T = ((string * (morphism * morphism)) * stamp) list;
(* FIXME mixins need to be stamped *)
@@ -398,17 +379,17 @@
);
val get_registrations =
- RegistrationsData.get #> map fst #> map (apsnd op $>);
+ Registrations.get #> map fst #> map (apsnd op $>);
fun add_registration (name, (base_morph, export)) thy =
roundup thy (fn _ => fn (name', morph') =>
- (RegistrationsData.map o cons) ((name', (morph', export)), stamp ()))
+ (Registrations.map o cons) ((name', (morph', export)), stamp ()))
(name, base_morph) (get_global_idents thy, thy) |> snd
(* FIXME |-> put_global_idents ?*);
fun amend_registration morph (name, base_morph) thy =
let
- val regs = (RegistrationsData.get #> map fst) thy;
+ val regs = (Registrations.get #> map fst) thy;
val base = instance_of thy name base_morph;
fun match (name', (morph', _)) =
name = name' andalso eq_list (op aconv) (base, instance_of thy name' morph');
@@ -418,7 +399,7 @@
space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available.")
else ();
in
- RegistrationsData.map (nth_map (length regs - 1 - i)
+ Registrations.map (nth_map (length regs - 1 - i)
(fn ((name, (base, export)), stamp) => ((name, (base $> morph, export)), stamp))) thy
end;
@@ -463,6 +444,7 @@
end;
+
(* Dependencies *)
fun add_dependency loc dep = (change_locale loc o apsnd) (cons (dep, stamp ()));
@@ -470,21 +452,36 @@
(*** Reasoning about locales ***)
-(** Storage for witnesses, intro and unfold rules **)
+(* Storage for witnesses, intro and unfold rules *)
-structure Witnesses = ThmsFun();
-structure Intros = ThmsFun();
-structure Unfolds = ThmsFun();
+structure Thms = GenericDataFun
+(
+ type T = thm list * thm list * thm list;
+ val empty = ([], [], []);
+ val extend = I;
+ fun merge _ ((witnesses1, intros1, unfolds1), (witnesses2, intros2, unfolds2)) =
+ (Thm.merge_thms (witnesses1, witnesses2),
+ Thm.merge_thms (intros1, intros2),
+ Thm.merge_thms (unfolds1, unfolds2));
+);
-val witness_attrib = Witnesses.add;
-val intro_attrib = Intros.add;
-val unfold_attrib = Unfolds.add;
+val get_witnesses = #1 o Thms.get o Context.Proof;
+val get_intros = #2 o Thms.get o Context.Proof;
+val get_unfolds = #3 o Thms.get o Context.Proof;
-(** Tactic **)
+val witness_add =
+ Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (Thm.add_thm th x, y, z)));
+val intro_add =
+ Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, Thm.add_thm th y, z)));
+val unfold_add =
+ Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, y, Thm.add_thm th z)));
-fun intro_locales_tac eager ctxt facts st =
+
+(* Tactic *)
+
+fun intro_locales_tac eager ctxt =
Method.intros_tac
- (Witnesses.get ctxt @ Intros.get ctxt @ (if eager then Unfolds.get ctxt else [])) facts st;
+ (get_witnesses ctxt @ get_intros ctxt @ (if eager then get_unfolds ctxt else []));
val _ = Context.>> (Context.map_theory
(Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o intro_locales_tac false))
--- a/src/Pure/Isar/proof_context.ML Thu Mar 26 11:33:50 2009 -0700
+++ b/src/Pure/Isar/proof_context.ML Thu Mar 26 20:09:58 2009 +0100
@@ -36,6 +36,9 @@
val theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
val extern_fact: Proof.context -> string -> xstring
val pretty_term_abbrev: Proof.context -> term -> Pretty.T
+ val pretty_thm_aux: Proof.context -> bool -> thm -> Pretty.T
+ val pretty_thms_aux: Proof.context -> bool -> thm list -> Pretty.T
+ val pretty_fact_aux: Proof.context -> bool -> string * thm list -> Pretty.T
val pretty_thm: Proof.context -> thm -> Pretty.T
val pretty_thms: Proof.context -> thm list -> Pretty.T
val pretty_fact: Proof.context -> string * thm list -> Pretty.T
@@ -295,21 +298,28 @@
fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt);
-fun pretty_thm ctxt th =
- let val asms = map Thm.term_of (Assumption.all_assms_of ctxt)
- in Display.pretty_thm_aux (Syntax.pp ctxt) false true asms th end;
+fun pretty_thm_aux ctxt show_status th =
+ let
+ val flags = {quote = false, show_hyps = true, show_status = show_status};
+ val asms = map Thm.term_of (Assumption.all_assms_of ctxt);
+ in Display.pretty_thm_aux (Syntax.pp ctxt) flags asms th end;
-fun pretty_thms ctxt [th] = pretty_thm ctxt th
- | pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths));
+fun pretty_thms_aux ctxt flag [th] = pretty_thm_aux ctxt flag th
+ | pretty_thms_aux ctxt flag ths =
+ Pretty.blk (0, Pretty.fbreaks (map (pretty_thm_aux ctxt flag) ths));
fun pretty_fact_name ctxt a = Pretty.block
[Pretty.markup (Markup.fact a) [Pretty.str (extern_fact ctxt a)], Pretty.str ":"];
-fun pretty_fact ctxt ("", ths) = pretty_thms ctxt ths
- | pretty_fact ctxt (a, [th]) = Pretty.block
- [pretty_fact_name ctxt a, Pretty.brk 1, pretty_thm ctxt th]
- | pretty_fact ctxt (a, ths) = Pretty.block
- (Pretty.fbreaks (pretty_fact_name ctxt a :: map (pretty_thm ctxt) ths));
+fun pretty_fact_aux ctxt flag ("", ths) = pretty_thms_aux ctxt flag ths
+ | pretty_fact_aux ctxt flag (a, [th]) = Pretty.block
+ [pretty_fact_name ctxt a, Pretty.brk 1, pretty_thm_aux ctxt flag th]
+ | pretty_fact_aux ctxt flag (a, ths) = Pretty.block
+ (Pretty.fbreaks (pretty_fact_name ctxt a :: map (pretty_thm_aux ctxt flag) ths));
+
+fun pretty_thm ctxt = pretty_thm_aux ctxt true;
+fun pretty_thms ctxt = pretty_thms_aux ctxt true;
+fun pretty_fact ctxt = pretty_fact_aux ctxt true;
val string_of_thm = Pretty.string_of oo pretty_thm;
--- a/src/Pure/Isar/proof_display.ML Thu Mar 26 11:33:50 2009 -0700
+++ b/src/Pure/Isar/proof_display.ML Thu Mar 26 20:09:58 2009 +0100
@@ -32,8 +32,10 @@
else Pretty.str "<context>");
fun pp_thm th =
- let val thy = Thm.theory_of_thm th
- in Display.pretty_thm_aux (Syntax.pp_global thy) true false [] th end;
+ let
+ val thy = Thm.theory_of_thm th;
+ val flags = {quote = true, show_hyps = false, show_status = true};
+ in Display.pretty_thm_aux (Syntax.pp_global thy) flags [] th end;
val pp_typ = Pretty.quote oo Syntax.pretty_typ_global;
val pp_term = Pretty.quote oo Syntax.pretty_term_global;
@@ -66,7 +68,7 @@
fun pretty_rule ctxt s thm =
Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
- Pretty.fbrk, ProofContext.pretty_thm ctxt thm];
+ Pretty.fbrk, ProofContext.pretty_thm_aux ctxt false thm];
val string_of_rule = Pretty.string_of ooo pretty_rule;
@@ -81,7 +83,7 @@
fun pretty_facts ctxt =
flat o (separate [Pretty.fbrk, Pretty.str "and "]) o
- map (single o ProofContext.pretty_fact ctxt);
+ map (single o ProofContext.pretty_fact_aux ctxt false);
in
@@ -92,7 +94,7 @@
else Pretty.writeln
(case facts of
[fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
- ProofContext.pretty_fact ctxt fact])
+ ProofContext.pretty_fact_aux ctxt false fact])
| _ => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]));
--- a/src/Pure/Isar/spec_parse.ML Thu Mar 26 11:33:50 2009 -0700
+++ b/src/Pure/Isar/spec_parse.ML Thu Mar 26 20:09:58 2009 +0100
@@ -22,7 +22,7 @@
val locale_fixes: (binding * string option * mixfix) list parser
val locale_insts: (string option list * (Attrib.binding * string) list) parser
val class_expr: string list parser
- val locale_expression: Expression.expression parser
+ val locale_expression: bool -> Expression.expression parser
val locale_keyword: string parser
val context_element: Element.context parser
val statement: (Attrib.binding * (string * string list) list) list parser
@@ -77,7 +77,7 @@
val locale_insts =
Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) []
- -- Scan.optional (P.$$$ "where" |-- P.and_list1 (opt_thm_name ":" -- P.prop)) [];
+ -- Scan.optional (P.where_ |-- P.and_list1 (opt_thm_name ":" -- P.prop)) [];
local
@@ -95,13 +95,12 @@
fun plus1_unless test scan =
scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
-val rename = P.name -- Scan.option P.mixfix;
+fun prefix mandatory =
+ P.name -- (P.$$$ "!" >> K true || P.$$$ "?" >> K false || Scan.succeed mandatory) --| P.$$$ ":";
-val prefix = P.name -- Scan.optional (P.$$$ "!" >> K true) false --| P.$$$ ":";
-val named = P.name -- (P.$$$ "=" |-- P.term);
-val position = P.maybe P.term;
-val instance = P.$$$ "where" |-- P.and_list1 named >> Expression.Named ||
- Scan.repeat1 position >> Expression.Positional;
+val instance = P.where_ |--
+ P.and_list1 (P.name -- (P.$$$ "=" |-- P.term)) >> Expression.Named ||
+ Scan.repeat1 (P.maybe P.term) >> Expression.Positional;
in
@@ -110,10 +109,10 @@
val class_expr = plus1_unless locale_keyword P.xname;
-val locale_expression =
+fun locale_expression mandatory =
let
val expr2 = P.xname;
- val expr1 = Scan.optional prefix ("", false) -- expr2 --
+ val expr1 = Scan.optional (prefix mandatory) ("", false) -- expr2 --
Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
val expr0 = plus1_unless locale_keyword expr1;
in expr0 -- Scan.optional (P.$$$ "for" |-- P.!!! locale_fixes) [] end;
@@ -128,7 +127,7 @@
val statement = P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp);
val obtain_case =
- P.parbinding -- (Scan.optional (P.simple_fixes --| P.$$$ "where") [] --
+ P.parbinding -- (Scan.optional (P.simple_fixes --| P.where_) [] --
(P.and_list1 (Scan.repeat1 P.prop) >> flat));
val general_statement =
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Mar 26 11:33:50 2009 -0700
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Mar 26 20:09:58 2009 +0100
@@ -655,13 +655,9 @@
text=[XML.Elem("pgml",[],
maps YXML.parse_body strings)] })
- fun string_of_thm th = Pretty.string_of
- (Display.pretty_thm_aux
- (Syntax.pp_global (Thm.theory_of_thm th))
- false (* quote *)
- false (* show hyps *)
- [] (* asms *)
- th)
+ fun string_of_thm th = Pretty.string_of (Display.pretty_thm_aux
+ (Syntax.pp_global (Thm.theory_of_thm th))
+ {quote = false, show_hyps = false, show_status = true} [] th)
fun strings_of_thm (thy, name) = map string_of_thm (PureThy.get_thms thy name)
--- a/src/Pure/display.ML Thu Mar 26 11:33:50 2009 -0700
+++ b/src/Pure/display.ML Thu Mar 26 20:09:58 2009 +0100
@@ -17,7 +17,8 @@
sig
include BASIC_DISPLAY
val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T
- val pretty_thm_aux: Pretty.pp -> bool -> bool -> term list -> thm -> Pretty.T
+ val pretty_thm_aux: Pretty.pp -> {quote: bool, show_hyps: bool, show_status: bool} ->
+ term list -> thm -> Pretty.T
val pretty_thm: thm -> Pretty.T
val string_of_thm: thm -> string
val pretty_thms: thm list -> Pretty.T
@@ -57,19 +58,20 @@
fun pretty_flexpair pp (t, u) = Pretty.block
[Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u];
-fun display_status th =
- let
- val {oracle = oracle0, unfinished, failed} = Thm.status_of th;
- val oracle = oracle0 andalso (not (! quick_and_dirty) orelse ! show_hyps);
- in
- if failed then "!!"
- else if oracle andalso unfinished then "!?"
- else if oracle then "!"
- else if unfinished then "?"
- else ""
- end;
+fun display_status false _ = ""
+ | display_status true th =
+ let
+ val {oracle = oracle0, unfinished, failed} = Thm.status_of th;
+ val oracle = oracle0 andalso (not (! quick_and_dirty) orelse ! show_hyps);
+ in
+ if failed then "!!"
+ else if oracle andalso unfinished then "!?"
+ else if oracle then "!"
+ else if unfinished then "?"
+ else ""
+ end;
-fun pretty_thm_aux pp quote show_hyps' asms raw_th =
+fun pretty_thm_aux pp {quote, show_hyps = show_hyps', show_status} asms raw_th =
let
val th = Thm.strip_shyps raw_th;
val {hyps, tpairs, prop, ...} = Thm.rep_thm th;
@@ -80,7 +82,7 @@
val prt_term = q o Pretty.term pp;
val hyps' = if ! show_hyps then hyps else subtract (op aconv) asms hyps;
- val status = display_status th;
+ val status = display_status show_status th;
val hlen = length xshyps + length hyps' + length tpairs;
val hsymbs =
@@ -97,7 +99,8 @@
in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
fun pretty_thm th =
- pretty_thm_aux (Syntax.pp_global (Thm.theory_of_thm th)) true false [] th;
+ pretty_thm_aux (Syntax.pp_global (Thm.theory_of_thm th))
+ {quote = true, show_hyps = false, show_status = true} [] th;
val string_of_thm = Pretty.string_of o pretty_thm;
--- a/src/ZF/Constructible/L_axioms.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/ZF/Constructible/L_axioms.thy Thu Mar 26 20:09:58 2009 +0100
@@ -99,7 +99,7 @@
apply (rule L_nat)
done
-interpretation L: M_trivial L by (rule M_trivial_L)
+interpretation L?: M_trivial L by (rule M_trivial_L)
(* Replaces the following declarations...
lemmas rall_abs = M_trivial.rall_abs [OF M_trivial_L]
--- a/src/ZF/Constructible/Rec_Separation.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/ZF/Constructible/Rec_Separation.thy Thu Mar 26 20:09:58 2009 +0100
@@ -185,7 +185,7 @@
theorem M_trancl_L: "PROP M_trancl(L)"
by (rule M_trancl.intro [OF M_basic_L M_trancl_axioms_L])
-interpretation L: M_trancl L by (rule M_trancl_L)
+interpretation L?: M_trancl L by (rule M_trancl_L)
subsection{*@{term L} is Closed Under the Operator @{term list}*}
@@ -372,7 +372,7 @@
apply (rule M_datatypes_axioms_L)
done
-interpretation L: M_datatypes L by (rule M_datatypes_L)
+interpretation L?: M_datatypes L by (rule M_datatypes_L)
subsection{*@{term L} is Closed Under the Operator @{term eclose}*}
@@ -435,7 +435,7 @@
apply (rule M_eclose_axioms_L)
done
-interpretation L: M_eclose L by (rule M_eclose_L)
+interpretation L?: M_eclose L by (rule M_eclose_L)
end
--- a/src/ZF/Constructible/Separation.thy Thu Mar 26 11:33:50 2009 -0700
+++ b/src/ZF/Constructible/Separation.thy Thu Mar 26 20:09:58 2009 +0100
@@ -305,7 +305,7 @@
theorem M_basic_L: "PROP M_basic(L)"
by (rule M_basic.intro [OF M_trivial_L M_basic_axioms_L])
-interpretation L: M_basic L by (rule M_basic_L)
+interpretation L?: M_basic L by (rule M_basic_L)
end