--- a/NEWS Thu Mar 26 13:02:12 2009 +0100
+++ b/NEWS Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/doc-src/Classes/Thy/Classes.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/doc-src/Classes/Thy/document/Classes.tex Fri Mar 27 09:58:48 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/Iff_Oracle.thy Thu Mar 26 13:02:12 2009 +0100
+++ b/src/FOL/ex/Iff_Oracle.thy Fri Mar 27 09:58:48 2009 +0100
@@ -34,7 +34,7 @@
ML {* iff_oracle (@{theory}, 2) *}
ML {* iff_oracle (@{theory}, 10) *}
-ML {* Thm.proof_of (iff_oracle (@{theory}, 10)) *}
+ML {* Thm.proof_body_of (iff_oracle (@{theory}, 10)) *}
text {* These oracle calls had better fail. *}
--- a/src/FOL/ex/LocaleTest.thy Thu Mar 26 13:02:12 2009 +0100
+++ b/src/FOL/ex/LocaleTest.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/HOL/Algebra/AbelCoset.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/HOL/Algebra/Group.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/HOL/Algebra/Ideal.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/HOL/Algebra/IntRing.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/HOL/Algebra/RingHom.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy Fri Mar 27 09:58:48 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/Algebra/ringsimp.ML Thu Mar 26 13:02:12 2009 +0100
+++ b/src/HOL/Algebra/ringsimp.ML Fri Mar 27 09:58:48 2009 +0100
@@ -62,11 +62,13 @@
Thm.declaration_attribute
(fn _ => Data.map (AList.delete struct_eq s));
-val attribute =
- Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon ||
- Scan.succeed true) -- Scan.lift Args.name --
- Scan.repeat Args.term
- >> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts));
+val attrib_setup =
+ Attrib.setup @{binding algebra}
+ (Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon || Scan.succeed true)
+ -- Scan.lift Args.name -- Scan.repeat Args.term
+ >> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts)))
+ "theorems controlling algebra method";
+
(** Setup **)
@@ -74,6 +76,6 @@
val setup =
Method.setup @{binding algebra} (Scan.succeed (SIMPLE_METHOD' o algebra_tac))
"normalisation of algebraic structure" #>
- Attrib.setup @{binding algebra} attribute "theorems controlling algebra method";
+ attrib_setup;
end;
--- a/src/HOL/Complex.thy Thu Mar 26 13:02:12 2009 +0100
+++ b/src/HOL/Complex.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/HOL/Divides.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/HOL/Finite_Set.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/HOL/Groebner_Basis.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/HOL/HahnBanach/Subspace.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/HOL/Lattices.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/HOL/Library/FrechetDeriv.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/HOL/Library/Inner_Product.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/HOL/Library/Multiset.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/HOL/Library/Numeral_Type.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/HOL/Library/Product_Vector.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/HOL/Library/SetsAndFunctions.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/HOL/NSA/StarDef.thy Fri Mar 27 09:58:48 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/Orderings.thy Thu Mar 26 13:02:12 2009 +0100
+++ b/src/HOL/Orderings.thy Fri Mar 27 09:58:48 2009 +0100
@@ -372,13 +372,14 @@
Thm.declaration_attribute
(fn _ => Data.map (AList.delete struct_eq s));
-val attribute =
- Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) ||
- Args.del >> K NONE) --| Args.colon (* FIXME ||
- Scan.succeed true *) ) -- Scan.lift Args.name --
- Scan.repeat Args.term
- >> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag
- | ((NONE, n), ts) => del_struct (n, ts));
+val attrib_setup =
+ Attrib.setup @{binding order}
+ (Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) || Args.del >> K NONE) --|
+ Args.colon (* FIXME || Scan.succeed true *) ) -- Scan.lift Args.name --
+ Scan.repeat Args.term
+ >> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag
+ | ((NONE, n), ts) => del_struct (n, ts)))
+ "theorems controlling transitivity reasoner";
(** Diagnostic command **)
@@ -397,8 +398,9 @@
(** Setup **)
val setup =
- Method.setup @{binding order} (Scan.succeed (SIMPLE_METHOD' o order_tac [])) "transitivity reasoner" #>
- Attrib.setup @{binding order} attribute "theorems controlling transitivity reasoner";
+ Method.setup @{binding order} (Scan.succeed (SIMPLE_METHOD' o order_tac []))
+ "transitivity reasoner" #>
+ attrib_setup;
end;
--- a/src/HOL/Power.thy Thu Mar 26 13:02:12 2009 +0100
+++ b/src/HOL/Power.thy Fri Mar 27 09:58:48 2009 +0100
@@ -186,6 +186,10 @@
apply (auto simp add: abs_mult)
done
+lemma abs_power_minus [simp]:
+ fixes a:: "'a::{ordered_idom,recpower}" shows "abs((-a) ^ n) = abs(a ^ n)"
+ by (simp add: abs_minus_cancel power_abs)
+
lemma zero_less_power_abs_iff [simp,noatp]:
"(0 < (abs a)^n) = (a \<noteq> (0::'a::{ordered_idom,recpower}) | n=0)"
proof (induct "n")
--- a/src/HOL/RealVector.thy Thu Mar 26 13:02:12 2009 +0100
+++ b/src/HOL/RealVector.thy Fri Mar 27 09:58:48 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/SEQ.thy Thu Mar 26 13:02:12 2009 +0100
+++ b/src/HOL/SEQ.thy Fri Mar 27 09:58:48 2009 +0100
@@ -40,10 +40,23 @@
definition
monoseq :: "(nat=>real)=>bool" where
- --{*Definition for monotonicity*}
+ --{*Definition of monotonicity.
+ The use of disjunction here complicates proofs considerably.
+ One alternative is to add a Boolean argument to indicate the direction.
+ Another is to develop the notions of increasing and decreasing first.*}
[code del]: "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
definition
+ incseq :: "(nat=>real)=>bool" where
+ --{*Increasing sequence*}
+ [code del]: "incseq X = (\<forall>m. \<forall>n\<ge>m. X m \<le> X n)"
+
+definition
+ decseq :: "(nat=>real)=>bool" where
+ --{*Increasing sequence*}
+ [code del]: "decseq X = (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
+
+definition
subseq :: "(nat => nat) => bool" where
--{*Definition of subsequence*}
[code del]: "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
@@ -886,6 +899,14 @@
thus ?case by arith
qed
+lemma LIMSEQ_subseq_LIMSEQ:
+ "\<lbrakk> X ----> L; subseq f \<rbrakk> \<Longrightarrow> (X o f) ----> L"
+apply (auto simp add: LIMSEQ_def)
+apply (drule_tac x=r in spec, clarify)
+apply (rule_tac x=no in exI, clarify)
+apply (blast intro: seq_suble le_trans dest!: spec)
+done
+
subsection {* Bounded Monotonic Sequences *}
@@ -1021,6 +1042,47 @@
apply (auto intro!: Bseq_mono_convergent)
done
+subsubsection{*Increasing and Decreasing Series*}
+
+lemma incseq_imp_monoseq: "incseq X \<Longrightarrow> monoseq X"
+ by (simp add: incseq_def monoseq_def)
+
+lemma incseq_le: assumes inc: "incseq X" and lim: "X ----> L" shows "X n \<le> L"
+ using monoseq_le [OF incseq_imp_monoseq [OF inc] lim]
+proof
+ assume "(\<forall>n. X n \<le> L) \<and> (\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n)"
+ thus ?thesis by simp
+next
+ assume "(\<forall>n. L \<le> X n) \<and> (\<forall>m n. m \<le> n \<longrightarrow> X n \<le> X m)"
+ hence const: "(!!m n. m \<le> n \<Longrightarrow> X n = X m)" using inc
+ by (auto simp add: incseq_def intro: order_antisym)
+ have X: "!!n. X n = X 0"
+ by (blast intro: const [of 0])
+ have "X = (\<lambda>n. X 0)"
+ by (blast intro: ext X)
+ hence "L = X 0" using LIMSEQ_const [of "X 0"]
+ by (auto intro: LIMSEQ_unique lim)
+ thus ?thesis
+ by (blast intro: eq_refl X)
+qed
+
+lemma decseq_imp_monoseq: "decseq X \<Longrightarrow> monoseq X"
+ by (simp add: decseq_def monoseq_def)
+
+lemma decseq_eq_incseq: "decseq X = incseq (\<lambda>n. - X n)"
+ by (simp add: decseq_def incseq_def)
+
+
+lemma decseq_le: assumes dec: "decseq X" and lim: "X ----> L" shows "L \<le> X n"
+proof -
+ have inc: "incseq (\<lambda>n. - X n)" using dec
+ by (simp add: decseq_eq_incseq)
+ have "- X n \<le> - L"
+ by (blast intro: incseq_le [OF inc] LIMSEQ_minus lim)
+ thus ?thesis
+ by simp
+qed
+
subsubsection{*A Few More Equivalence Theorems for Boundedness*}
text{*alternative formulation for boundedness*}
@@ -1065,6 +1127,14 @@
"\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e"
by (simp add: Cauchy_def)
+lemma Cauchy_subseq_Cauchy:
+ "\<lbrakk> Cauchy X; subseq f \<rbrakk> \<Longrightarrow> Cauchy (X o f)"
+apply (auto simp add: Cauchy_def)
+apply (drule_tac x=e in spec, clarify)
+apply (rule_tac x=M in exI, clarify)
+apply (blast intro: seq_suble le_trans dest!: spec)
+done
+
subsubsection {* Cauchy Sequences are Bounded *}
text{*A Cauchy sequence is bounded -- this is the standard
@@ -1238,6 +1308,11 @@
shows "Cauchy X = convergent X"
by (fast intro: Cauchy_convergent convergent_Cauchy)
+lemma convergent_subseq_convergent:
+ fixes X :: "nat \<Rightarrow> 'a::banach"
+ shows "\<lbrakk> convergent X; subseq f \<rbrakk> \<Longrightarrow> convergent (X o f)"
+ by (simp add: Cauchy_subseq_Cauchy Cauchy_convergent_iff [symmetric])
+
subsection {* Power Sequences *}
--- a/src/HOL/SizeChange/sct.ML Thu Mar 26 13:02:12 2009 +0100
+++ b/src/HOL/SizeChange/sct.ML Fri Mar 27 09:58:48 2009 +0100
@@ -105,7 +105,7 @@
fun dest_case rebind t =
let
- val (_ $ _ $ rhs :: _ $ _ $ match :: guards) = HOLogic.dest_conj t
+ val ((_ $ _ $ rhs) :: (_ $ _ $ match) :: guards) = HOLogic.dest_conj t
val guard = case guards of [] => HOLogic.true_const | gs => foldr1 HOLogic.mk_conj gs
in
foldr1 HOLogic.mk_prod [rebind guard, rebind rhs, rebind match]
--- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML Thu Mar 26 13:02:12 2009 +0100
+++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML Fri Mar 27 09:58:48 2009 +0100
@@ -191,16 +191,17 @@
in
-val attribute =
- Scan.lift (Args.$$$ delN >> K del) ||
- ((keyword2 semiringN opsN |-- terms) --
- (keyword2 semiringN rulesN |-- thms)) --
- (optional (keyword2 ringN opsN |-- terms) --
- optional (keyword2 ringN rulesN |-- thms)) --
- optional (keyword2 idomN rulesN |-- thms) --
- optional (keyword2 idealN rulesN |-- thms)
- >> (fn (((sr, r), id), idl) =>
- add {semiring = sr, ring = r, idom = id, ideal = idl});
+val normalizer_setup =
+ Attrib.setup @{binding normalizer}
+ (Scan.lift (Args.$$$ delN >> K del) ||
+ ((keyword2 semiringN opsN |-- terms) --
+ (keyword2 semiringN rulesN |-- thms)) --
+ (optional (keyword2 ringN opsN |-- terms) --
+ optional (keyword2 ringN rulesN |-- thms)) --
+ optional (keyword2 idomN rulesN |-- thms) --
+ optional (keyword2 idealN rulesN |-- thms)
+ >> (fn (((sr, r), id), idl) => add {semiring = sr, ring = r, idom = id, ideal = idl}))
+ "semiring normalizer data";
end;
@@ -208,7 +209,7 @@
(* theory setup *)
val setup =
- Attrib.setup @{binding normalizer} attribute "semiring normalizer data" #>
+ normalizer_setup #>
Attrib.setup @{binding algebra} (Attrib.add_del add_ss del_ss) "pre-simplification for algebra";
end;
--- a/src/HOL/Tools/Qelim/cooper_data.ML Thu Mar 26 13:02:12 2009 +0100
+++ b/src/HOL/Tools/Qelim/cooper_data.ML Fri Mar 27 09:58:48 2009 +0100
@@ -67,6 +67,7 @@
(* concrete syntax *)
local
+
fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
val constsN = "consts";
@@ -77,14 +78,17 @@
fun optional scan = Scan.optional scan [];
in
-val attribute =
- (Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
- optional (keyword constsN |-- terms) >> add
+
+val presburger_setup =
+ Attrib.setup @{binding presburger}
+ ((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
+ optional (keyword constsN |-- terms) >> add) "Cooper data";
+
end;
(* theory setup *)
-val setup = Attrib.setup @{binding presburger} attribute "Cooper data";
+val setup = presburger_setup;
end;
--- a/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML Thu Mar 26 13:02:12 2009 +0100
+++ b/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML Fri Mar 27 09:58:48 2009 +0100
@@ -122,26 +122,28 @@
val terms = thms >> map Drule.dest_term;
in
-val attribute =
- (keyword minfN |-- thms)
+val ferrak_setup =
+ Attrib.setup @{binding ferrack}
+ ((keyword minfN |-- thms)
-- (keyword pinfN |-- thms)
-- (keyword nmiN |-- thms)
-- (keyword npiN |-- thms)
-- (keyword lin_denseN |-- thms)
-- (keyword qeN |-- thms)
- -- (keyword atomsN |-- terms) >>
- (fn ((((((minf,pinf),nmi),npi),lin_dense),qe), atoms)=>
- if length qe = 1 then
- add ({minf = minf, pinf = pinf, nmi = nmi, npi = npi, ld = lin_dense,
- qe = hd qe, atoms = atoms},
- {isolate_conv = undefined, whatis = undefined, simpset = HOL_ss})
- else error "only one theorem for qe!")
+ -- (keyword atomsN |-- terms) >>
+ (fn ((((((minf,pinf),nmi),npi),lin_dense),qe), atoms)=>
+ if length qe = 1 then
+ add ({minf = minf, pinf = pinf, nmi = nmi, npi = npi, ld = lin_dense,
+ qe = hd qe, atoms = atoms},
+ {isolate_conv = undefined, whatis = undefined, simpset = HOL_ss})
+ else error "only one theorem for qe!"))
+ "Ferrante Rackoff data";
end;
(* theory setup *)
-val setup = Attrib.setup @{binding ferrack} attribute "Ferrante Rackoff data";
+val setup = ferrak_setup;
end;
--- a/src/HOL/Tools/Qelim/langford_data.ML Thu Mar 26 13:02:12 2009 +0100
+++ b/src/HOL/Tools/Qelim/langford_data.ML Fri Mar 27 09:58:48 2009 +0100
@@ -85,25 +85,28 @@
val terms = thms >> map Drule.dest_term;
in
-val attribute =
- (keyword qeN |-- thms)
+val langford_setup =
+ Attrib.setup @{binding langford}
+ ((keyword qeN |-- thms)
-- (keyword gatherN |-- thms)
- -- (keyword atomsN |-- terms) >>
- (fn ((qes,gs), atoms) =>
- if length qes = 3 andalso length gs > 1 then
- let
- val [q1,q2,q3] = qes
- val gst::gss = gs
- val entry = {qe_bnds = q1, qe_nolb = q2,
- qe_noub = q3, gs = gss, gst = gst, atoms = atoms}
- in add entry end
- else error "Need 3 theorems for qe and at least one for gs")
+ -- (keyword atomsN |-- terms) >>
+ (fn ((qes,gs), atoms) =>
+ if length qes = 3 andalso length gs > 1 then
+ let
+ val [q1,q2,q3] = qes
+ val gst::gss = gs
+ val entry = {qe_bnds = q1, qe_nolb = q2,
+ qe_noub = q3, gs = gss, gst = gst, atoms = atoms}
+ in add entry end
+ else error "Need 3 theorems for qe and at least one for gs"))
+ "Langford data";
+
end;
(* theory setup *)
val setup =
- Attrib.setup @{binding langford} attribute "Langford data" #>
+ langford_setup #>
Attrib.setup @{binding langfordsimp} (Attrib.add_del add_simp del_simp) "Langford simpset";
end;
--- a/src/HOL/Tools/arith_data.ML Thu Mar 26 13:02:12 2009 +0100
+++ b/src/HOL/Tools/arith_data.ML Fri Mar 27 09:58:48 2009 +0100
@@ -57,12 +57,13 @@
val arith_tac = gen_arith_tac false;
val verbose_arith_tac = gen_arith_tac true;
-val arith_method = Args.bang_facts >> (fn prems => fn ctxt =>
- METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ get_arith_facts ctxt @ facts)
- THEN' verbose_arith_tac ctxt)));
-
-val setup = Arith_Facts.setup
- #> Method.setup @{binding arith} arith_method "various arithmetic decision procedures";
+val setup =
+ Arith_Facts.setup #>
+ Method.setup @{binding arith}
+ (Args.bang_facts >> (fn prems => fn ctxt =>
+ METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ get_arith_facts ctxt @ facts)
+ THEN' verbose_arith_tac ctxt))))
+ "various arithmetic decision procedures";
(* various auxiliary and legacy *)
--- a/src/HOL/Tools/function_package/lexicographic_order.ML Thu Mar 26 13:02:12 2009 +0100
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML Fri Mar 27 09:58:48 2009 +0100
@@ -176,7 +176,7 @@
val gc = map (fn i => chr (i + 96)) (1 upto length table)
val mc = 1 upto length measure_funs
- val tstr = "Result matrix:" :: " " ^ concat (map (enclose " " " " o string_of_int) mc)
+ val tstr = "Result matrix:" :: (" " ^ concat (map (enclose " " " " o string_of_int) mc))
:: map2 (fn r => fn i => i ^ ": " ^ concat (map pr_cell r)) table gc
val gstr = "Calls:" :: map2 (prefix " " oo pr_goal) tl gc
val mstr = "Measures:" :: map2 (prefix " " oo pr_fun) measure_funs mc
--- a/src/HOL/Tools/inductive_package.ML Thu Mar 26 13:02:12 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML Fri Mar 27 09:58:48 2009 +0100
@@ -460,17 +460,18 @@
val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
-val ind_cases =
- Scan.lift (Scan.repeat1 Args.name_source --
- Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.name) []) >>
- (fn (raw_props, fixes) => fn ctxt =>
- let
- val (_, ctxt') = Variable.add_fixes fixes ctxt;
- val props = Syntax.read_props ctxt' raw_props;
- val ctxt'' = fold Variable.declare_term props ctxt';
- val rules = ProofContext.export ctxt'' ctxt (map (mk_cases ctxt'') props)
- in Method.erule 0 rules end);
-
+val ind_cases_setup =
+ Method.setup @{binding ind_cases}
+ (Scan.lift (Scan.repeat1 Args.name_source --
+ Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.name) []) >>
+ (fn (raw_props, fixes) => fn ctxt =>
+ let
+ val (_, ctxt') = Variable.add_fixes fixes ctxt;
+ val props = Syntax.read_props ctxt' raw_props;
+ val ctxt'' = fold Variable.declare_term props ctxt';
+ val rules = ProofContext.export ctxt'' ctxt (map (mk_cases ctxt'') props)
+ in Method.erule 0 rules end))
+ "dynamic case analysis on predicates";
(* prove induction rule *)
@@ -934,7 +935,7 @@
(* setup theory *)
val setup =
- Method.setup @{binding ind_cases} ind_cases "dynamic case analysis on predicates" #>
+ ind_cases_setup #>
Attrib.setup @{binding mono} (Attrib.add_del mono_add mono_del)
"declaration of monotonicity rule";
--- a/src/HOL/Tools/inductive_realizer.ML Thu Mar 26 13:02:12 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Fri Mar 27 09:58:48 2009 +0100
@@ -505,13 +505,11 @@
| SOME (SOME sets') => sets \\ sets')
end I);
-val ind_realizer =
- (Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
- Scan.option (Scan.lift (Args.colon) |--
- Scan.repeat1 Args.const))) >> rlz_attrib;
-
val setup =
- Attrib.setup @{binding ind_realizer} ind_realizer "add realizers for inductive set";
+ Attrib.setup @{binding ind_realizer}
+ ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
+ Scan.option (Scan.lift (Args.colon) |-- Scan.repeat1 Args.const))) >> rlz_attrib)
+ "add realizers for inductive set";
end;
--- a/src/HOL/Tools/int_arith.ML Thu Mar 26 13:02:12 2009 +0100
+++ b/src/HOL/Tools/int_arith.ML Fri Mar 27 09:58:48 2009 +0100
@@ -377,6 +377,8 @@
struct
val assoc_ss = HOL_ss addsimps @{thms mult_ac}
val eq_reflection = eq_reflection
+ fun is_numeral (Const(@{const_name Int.number_of}, _) $ _) = true
+ | is_numeral _ = false;
end;
structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
--- a/src/HOL/Tools/lin_arith.ML Thu Mar 26 13:02:12 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML Fri Mar 27 09:58:48 2009 +0100
@@ -882,10 +882,6 @@
val linear_arith_tac = gen_linear_arith_tac true;
-val linarith_method = Args.bang_facts >> (fn prems => fn ctxt =>
- METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ Arith_Data.get_arith_facts ctxt @ facts)
- THEN' linear_arith_tac ctxt)));
-
end;
@@ -899,7 +895,11 @@
Context.mapping
(setup_options #>
Arith_Data.add_tactic "linear arithmetic" gen_linear_arith_tac #>
- Method.setup @{binding linarith} linarith_method "linear arithmetic" #>
+ Method.setup @{binding linarith}
+ (Args.bang_facts >> (fn prems => fn ctxt =>
+ METHOD (fn facts =>
+ HEADGOAL (Method.insert_tac (prems @ Arith_Data.get_arith_facts ctxt @ facts)
+ THEN' linear_arith_tac ctxt)))) "linear arithmetic" #>
Attrib.setup @{binding arith_split} (Scan.succeed arith_split_add)
"declaration of split rules for arithmetic procedure") I;
--- a/src/HOL/Tools/record_package.ML Thu Mar 26 13:02:12 2009 +0100
+++ b/src/HOL/Tools/record_package.ML Fri Mar 27 09:58:48 2009 +0100
@@ -1782,7 +1782,8 @@
val alphas_fields = List.foldr OldTerm.add_typ_tfree_names [] types;
val alphas_ext = alphas inter alphas_fields;
val len = length fields;
- val variants = Name.variant_list (moreN::rN::rN ^ "'"::wN::parent_variants) (map fst bfields);
+ val variants =
+ Name.variant_list (moreN :: rN :: (rN ^ "'") :: wN :: parent_variants) (map fst bfields);
val vars = ListPair.map Free (variants, types);
val named_vars = names ~~ vars;
val idxs = 0 upto (len - 1);
--- a/src/HOL/Tools/res_axioms.ML Thu Mar 26 13:02:12 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML Fri Mar 27 09:58:48 2009 +0100
@@ -521,18 +521,19 @@
REPEAT_DETERM_N (length ts) o (etac thin_rl)]
end);
-val setup_methods =
+val neg_clausify_setup =
Method.setup @{binding neg_clausify} (Scan.succeed (K (SIMPLE_METHOD' neg_clausify_tac)))
"conversion of goal to conjecture clauses";
(** Attribute for converting a theorem into clauses **)
-val clausify = Scan.lift OuterParse.nat >>
- (fn i => Thm.rule_attribute (fn context => fn th =>
- Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i)));
-
-val setup_attrs = Attrib.setup @{binding clausify} clausify "conversion of theorem to clauses";
+val clausify_setup =
+ Attrib.setup @{binding clausify}
+ (Scan.lift OuterParse.nat >>
+ (fn i => Thm.rule_attribute (fn context => fn th =>
+ Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i))))
+ "conversion of theorem to clauses";
@@ -540,8 +541,8 @@
val setup =
meson_method_setup #>
- setup_methods #>
- setup_attrs #>
+ neg_clausify_setup #>
+ clausify_setup #>
perhaps saturate_skolem_cache #>
Theory.at_end clause_cache_endtheory;
--- a/src/HOL/Tools/split_rule.ML Thu Mar 26 13:02:12 2009 +0100
+++ b/src/HOL/Tools/split_rule.ML Fri Mar 27 09:58:48 2009 +0100
@@ -141,18 +141,18 @@
|> RuleCases.save rl
end;
+
(* attribute syntax *)
(* FIXME dynamically scoped due to Args.name_source/pair_tac *)
-val split_format = Scan.lift
- (Args.parens (Args.$$$ "complete") >> K (Thm.rule_attribute (K complete_split_rule)) ||
- OuterParse.and_list1 (Scan.repeat Args.name_source)
- >> (fn xss => Thm.rule_attribute (fn context =>
- split_rule_goal (Context.proof_of context) xss)));
-
val setup =
- Attrib.setup @{binding split_format} split_format
+ Attrib.setup @{binding split_format}
+ (Scan.lift
+ (Args.parens (Args.$$$ "complete") >> K (Thm.rule_attribute (K complete_split_rule)) ||
+ OuterParse.and_list1 (Scan.repeat Args.name_source)
+ >> (fn xss => Thm.rule_attribute (fn context =>
+ split_rule_goal (Context.proof_of context) xss))))
"split pair-typed subterms in premises, or function arguments" #>
Attrib.setup @{binding split_rule} (Scan.succeed (Thm.rule_attribute (K split_rule)))
"curries ALL function variables occurring in a rule's conclusion";
--- a/src/HOL/Word/TdThs.thy Thu Mar 26 13:02:12 2009 +0100
+++ b/src/HOL/Word/TdThs.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/HOL/Word/WordArith.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/HOL/Word/WordBitwise.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/HOL/Word/WordDefinition.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/HOL/Word/WordGenLib.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/HOL/ex/LocaleTest2.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/HOLCF/Algebraic.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/HOLCF/Bifinite.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/HOLCF/CompactBasis.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/HOLCF/Completion.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/HOLCF/ConvexPD.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/HOLCF/LowerPD.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/HOLCF/Universal.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/HOLCF/UpperPD.thy Fri Mar 27 09:58:48 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/Provers/Arith/assoc_fold.ML Thu Mar 26 13:02:12 2009 +0100
+++ b/src/Provers/Arith/assoc_fold.ML Fri Mar 27 09:58:48 2009 +0100
@@ -12,6 +12,7 @@
sig
val assoc_ss: simpset
val eq_reflection: thm
+ val is_numeral: term -> bool
end;
signature ASSOC_FOLD =
@@ -29,10 +30,9 @@
(*Separate the literals from the other terms being combined*)
fun sift_terms plus (t, (lits,others)) =
+ if Data.is_numeral t then (t::lits, others) (*new literal*) else
(case t of
- Const (@{const_name Int.number_of}, _) $ _ => (* FIXME logic dependent *)
- (t::lits, others) (*new literal*)
- | (f as Const _) $ x $ y =>
+ (f as Const _) $ x $ y =>
if f = plus
then sift_terms plus (x, sift_terms plus (y, (lits,others)))
else (lits, t::others) (*arbitrary summand*)
--- a/src/Provers/blast.ML Thu Mar 26 13:02:12 2009 +0100
+++ b/src/Provers/blast.ML Fri Mar 27 09:58:48 2009 +0100
@@ -1302,14 +1302,13 @@
(** method setup **)
-val blast_method =
- Args.bang_facts -- Scan.lift (Scan.option OuterParse.nat) --|
- Method.sections Data.cla_modifiers >>
- (fn (prems, NONE) => Data.cla_meth' blast_tac prems
- | (prems, SOME lim) => Data.cla_meth' (fn cs => depth_tac cs lim) prems);
-
val setup =
setup_depth_limit #>
- Method.setup @{binding blast} blast_method "tableau prover";
+ Method.setup @{binding blast}
+ (Args.bang_facts -- Scan.lift (Scan.option OuterParse.nat) --|
+ Method.sections Data.cla_modifiers >>
+ (fn (prems, NONE) => Data.cla_meth' blast_tac prems
+ | (prems, SOME lim) => Data.cla_meth' (fn cs => depth_tac cs lim) prems))
+ "classical tableau prover";
end;
--- a/src/Provers/splitter.ML Thu Mar 26 13:02:12 2009 +0100
+++ b/src/Provers/splitter.ML Fri Mar 27 09:58:48 2009 +0100
@@ -467,14 +467,13 @@
Args.$$$ splitN -- Args.add -- Args.colon >> K (I, split_add),
Args.$$$ splitN -- Args.del -- Args.colon >> K (I, split_del)];
-fun split_meth parser = (Attrib.thms >>
- (fn ths => K (SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths)))) parser;
-
(* theory setup *)
val setup =
Attrib.setup @{binding split} (Attrib.add_del split_add split_del) "declare case split rule" #>
- Method.setup @{binding split} split_meth "apply case split rule";
+ Method.setup @{binding split}
+ (Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths))))
+ "apply case split rule";
end;
--- a/src/Pure/Isar/code.ML Thu Mar 26 13:02:12 2009 +0100
+++ b/src/Pure/Isar/code.ML Fri Mar 27 09:58:48 2009 +0100
@@ -98,14 +98,12 @@
then error ("Code attribute " ^ name ^ " already declared") else add_parser attr attrs)
end;
-val _ =
- let
- val code_attr = Scan.peek (fn context =>
- List.foldr op || Scan.fail (map snd (CodeAttr.get (Context.theory_of context))));
- in
- Context.>> (Context.map_theory
- (Attrib.setup (Binding.name "code") code_attr "declare theorems for code generation"))
- end;
+val _ = Context.>> (Context.map_theory
+ (Attrib.setup (Binding.name "code")
+ (Scan.peek (fn context =>
+ List.foldr op || Scan.fail (map snd (CodeAttr.get (Context.theory_of context)))))
+ "declare theorems for code generation"));
+
(** logical and syntactical specification of executable code **)
--- a/src/Pure/Isar/expression.ML Thu Mar 26 13:02:12 2009 +0100
+++ b/src/Pure/Isar/expression.ML Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/Pure/Isar/locale.ML Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/Pure/Isar/proof_display.ML Fri Mar 27 09:58:48 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/rule_insts.ML Thu Mar 26 13:02:12 2009 +0100
+++ b/src/Pure/Isar/rule_insts.ML Fri Mar 27 09:58:48 2009 +0100
@@ -220,8 +220,11 @@
in
-fun where_att x = (Scan.lift (P.and_list inst) >> (fn args =>
- Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args))) x;
+val _ = Context.>> (Context.map_theory
+ (Attrib.setup (Binding.name "where")
+ (Scan.lift (P.and_list inst) >> (fn args =>
+ Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)))
+ "named instantiation of theorem"));
end;
@@ -243,19 +246,15 @@
in
-fun of_att x = (Scan.lift insts >> (fn args =>
- Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args))) x;
+val _ = Context.>> (Context.map_theory
+ (Attrib.setup (Binding.name "of")
+ (Scan.lift insts >> (fn args =>
+ Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args)))
+ "positional instantiation of theorem"));
end;
-(* setup *)
-
-val _ = Context.>> (Context.map_theory
- (Attrib.setup (Binding.name "where") where_att "named instantiation of theorem" #>
- Attrib.setup (Binding.name "of") of_att "positional instantiation of theorem"));
-
-
(** tactics **)
--- a/src/Pure/Isar/spec_parse.ML Thu Mar 26 13:02:12 2009 +0100
+++ b/src/Pure/Isar/spec_parse.ML Fri Mar 27 09:58:48 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,12 +109,12 @@
val class_expr = plus1_unless locale_keyword P.xname;
-val locale_expression =
+fun locale_expression mandatory =
let
- fun expr2 x = P.xname x;
- fun expr1 x = (Scan.optional prefix ("", false) -- expr2 --
- Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)))) x;
- fun expr0 x = (plus1_unless locale_keyword expr1) x;
+ val expr2 = P.xname;
+ 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;
val context_element = P.group "context element" loc_element;
@@ -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/ML/ml_antiquote.ML Thu Mar 26 13:02:12 2009 +0100
+++ b/src/Pure/ML/ml_antiquote.ML Fri Mar 27 09:58:48 2009 +0100
@@ -59,7 +59,7 @@
structure P = OuterParse;
-val _ = inline "binding"
+val _ = value "binding"
(Scan.lift (P.position Args.name) >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name)));
val _ = value "theory"
--- a/src/Pure/Proof/extraction.ML Thu Mar 26 13:02:12 2009 +0100
+++ b/src/Pure/Proof/extraction.ML Fri Mar 27 09:58:48 2009 +0100
@@ -568,7 +568,7 @@
(proof_combt
(PThm (serial (),
((corr_name name vs', corr_prop, SOME (map TVar (OldTerm.term_tvars corr_prop))),
- Future.value (make_proof_body corr_prf))), vfs_of corr_prop))
+ Future.value (approximate_proof_body corr_prf))), vfs_of corr_prop))
(map (get_var_type corr_prop) (vfs_of prop))
in
((name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'',
@@ -679,7 +679,7 @@
(proof_combt
(PThm (serial (),
((corr_name s vs', corr_prop, SOME (map TVar (OldTerm.term_tvars corr_prop))),
- Future.value (make_proof_body corr_prf'))), vfs_of corr_prop))
+ Future.value (approximate_proof_body corr_prf'))), vfs_of corr_prop))
(map (get_var_type corr_prop) (vfs_of prop));
in
((s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'',
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Mar 26 13:02:12 2009 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Fri Mar 27 09:58:48 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/Tools/xml_syntax.ML Thu Mar 26 13:02:12 2009 +0100
+++ b/src/Pure/Tools/xml_syntax.ML Fri Mar 27 09:58:48 2009 +0100
@@ -158,7 +158,7 @@
| proof_of_xml (XML.Elem ("PThm", [("name", s)], term :: opttypes)) =
(* FIXME? *)
PThm (serial (), ((s, term_of_xml term, opttypes_of_xml opttypes),
- Future.value (Proofterm.make_proof_body MinProof)))
+ Future.value (Proofterm.approximate_proof_body MinProof)))
| proof_of_xml (XML.Elem ("PAxm", [("name", s)], term :: opttypes)) =
PAxm (s, term_of_xml term, opttypes_of_xml opttypes)
| proof_of_xml (XML.Elem ("Oracle", [("name", s)], term :: opttypes)) =
--- a/src/Pure/display.ML Thu Mar 26 13:02:12 2009 +0100
+++ b/src/Pure/display.ML Fri Mar 27 09:58:48 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/Pure/proofterm.ML Thu Mar 26 13:02:12 2009 +0100
+++ b/src/Pure/proofterm.ML Fri Mar 27 09:58:48 2009 +0100
@@ -46,11 +46,10 @@
val oracle_ord: oracle * oracle -> order
val thm_ord: pthm * pthm -> order
- val make_proof_body: proof -> proof_body
val merge_oracles: oracle OrdList.T -> oracle OrdList.T -> oracle OrdList.T
- val make_oracles: proof -> oracle OrdList.T
val merge_thms: pthm OrdList.T -> pthm OrdList.T -> pthm OrdList.T
- val make_thms: proof -> pthm OrdList.T
+ val all_oracles_of: proof_body -> oracle OrdList.T
+ val approximate_proof_body: proof -> proof_body
(** primitive operations **)
val proof_combt: proof * term list -> proof
@@ -107,11 +106,11 @@
val equal_intr: term -> term -> proof -> proof -> proof
val equal_elim: term -> term -> proof -> proof -> proof
val axm_proof: string -> term -> proof
- val oracle_proof: string -> term -> proof
+ val oracle_proof: string -> term -> oracle * proof
val promise_proof: theory -> serial -> term -> proof
- val fulfill_proof: theory -> (serial * proof) list -> proof_body -> proof_body
+ val fulfill_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
val thm_proof: theory -> string -> term list -> term ->
- (serial * proof future) list -> proof_body -> pthm * proof
+ (serial * proof_body future) list -> proof_body -> pthm * proof
val get_name: term list -> term -> proof -> string
(** rewriting on proof terms **)
@@ -214,26 +213,32 @@
val oracle_ord = prod_ord fast_string_ord TermOrd.fast_term_ord;
fun thm_ord ((i, _): pthm, (j, _)) = int_ord (j, i);
-fun make_body prf =
+val merge_oracles = OrdList.union oracle_ord;
+val merge_thms = OrdList.union thm_ord;
+
+val all_oracles_of =
+ let
+ fun collect (PBody {oracles, thms, ...}) = thms |> fold (fn (i, (_, _, body)) => fn (x, seen) =>
+ if Inttab.defined seen i then (x, seen)
+ else
+ let
+ val body' = Future.join body;
+ val (x', seen') = collect body' (x, Inttab.update (i, ()) seen);
+ in (merge_oracles oracles x', seen') end);
+ in fn body => #1 (collect body ([], Inttab.empty)) end;
+
+fun approximate_proof_body prf =
let
val (oracles, thms) = fold_proof_atoms false
(fn Oracle (s, prop, _) => apfst (cons (s, prop))
| PThm (i, ((name, prop, _), body)) => apsnd (cons (i, (name, prop, body)))
| _ => I) [prf] ([], []);
- in (OrdList.make oracle_ord oracles, OrdList.make thm_ord thms) end;
-
-fun make_proof_body prf =
- let val (oracles, thms) = make_body prf
- in PBody {oracles = oracles, thms = thms, proof = prf} end;
-
-val make_oracles = #1 o make_body;
-val make_thms = #2 o make_body;
-
-val merge_oracles = OrdList.union oracle_ord;
-val merge_thms = OrdList.union thm_ord;
-
-fun merge_body (oracles1, thms1) (oracles2, thms2) =
- (merge_oracles oracles1 oracles2, merge_thms thms1 thms2);
+ in
+ PBody
+ {oracles = OrdList.make oracle_ord oracles,
+ thms = OrdList.make thm_ord thms,
+ proof = prf}
+ end;
(***** proof objects with different levels of detail *****)
@@ -930,8 +935,8 @@
val dummy = Const (Term.dummy_patternN, dummyT);
fun oracle_proof name prop =
- if !proofs = 0 then Oracle (name, dummy, NONE)
- else gen_axm_proof Oracle name prop;
+ if ! proofs = 0 then ((name, dummy), Oracle (name, dummy, NONE))
+ else ((name, prop), gen_axm_proof Oracle name prop);
fun shrink_proof thy =
let
@@ -1235,16 +1240,17 @@
in Promise (i, prop, map TVar (Term.add_tvars prop [])) end;
fun fulfill_proof _ [] body0 = body0
- | fulfill_proof thy promises body0 =
+ | fulfill_proof thy ps body0 =
let
val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
- val (oracles, thms) = fold (merge_body o make_body o #2) promises (oracles0, thms0);
+ val oracles = fold (fn (_, PBody {oracles, ...}) => merge_oracles oracles) ps oracles0;
+ val thms = fold (fn (_, PBody {thms, ...}) => merge_thms thms) ps thms0;
+ val proofs = fold (fn (i, PBody {proof, ...}) => Inttab.update (i, proof)) ps Inttab.empty;
- val tab = Inttab.make promises;
fun fill (Promise (i, prop, Ts)) =
- (case Inttab.lookup tab i of
+ (case Inttab.lookup proofs i of
NONE => NONE
- | SOME p => SOME (instantiate (Term.add_tvars prop [] ~~ Ts, []) p))
+ | SOME prf => SOME (instantiate (Term.add_tvars prop [] ~~ Ts, []) prf))
| fill _ = NONE;
val (rules, procs) = get_data thy;
val proof = rewrite_prf fst (rules, K fill :: procs) proof0;
--- a/src/Pure/thm.ML Thu Mar 26 13:02:12 2009 +0100
+++ b/src/Pure/thm.ML Fri Mar 27 09:58:48 2009 +0100
@@ -1662,7 +1662,7 @@
fun proof_body_of (Thm (Deriv {open_promises, promises, body, ...}, {thy_ref, ...})) =
let
val _ = Exn.release_all (map (Future.join_result o #2) (rev open_promises));
- val ps = map (apsnd (raw_proof_of o Future.join)) promises;
+ val ps = map (apsnd (raw_proof_body_of o Future.join)) promises;
in Pt.fulfill_proof (Theory.deref thy_ref) ps body end;
val proof_of = Proofterm.proof_of o proof_body_of;
@@ -1680,7 +1680,7 @@
val {thy_ref, hyps, prop, tpairs, ...} = args;
val _ = null tpairs orelse raise THM ("put_name: unsolved flex-flex constraints", 0, [thm]);
- val ps = map (apsnd (Future.map proof_of)) promises;
+ val ps = map (apsnd (Future.map proof_body_of)) promises;
val thy = Theory.deref thy_ref;
val (pthm, proof) = Pt.thm_proof thy name hyps prop ps body;
@@ -1701,8 +1701,8 @@
if T <> propT then
raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
else
- let val prf = Pt.oracle_proof name prop in
- Thm (make_deriv ~1 [] [] (Pt.make_oracles prf) [] prf,
+ let val (ora, prf) = Pt.oracle_proof name prop in
+ Thm (make_deriv ~1 [] [] [ora] [] prf,
{thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
tags = [],
maxidx = maxidx,
--- a/src/Tools/induct.ML Thu Mar 26 13:02:12 2009 +0100
+++ b/src/Tools/induct.ML Fri Mar 27 09:58:48 2009 +0100
@@ -259,16 +259,15 @@
spec setN Args.const >> add_pred ||
Scan.lift Args.del >> K del;
-val cases_att = attrib cases_type cases_pred cases_del;
-val induct_att = attrib induct_type induct_pred induct_del;
-val coinduct_att = attrib coinduct_type coinduct_pred coinduct_del;
-
in
val attrib_setup =
- Attrib.setup @{binding cases} cases_att "declaration of cases rule" #>
- Attrib.setup @{binding induct} induct_att "declaration of induction rule" #>
- Attrib.setup @{binding coinduct} coinduct_att "declaration of coinduction rule";
+ Attrib.setup @{binding cases} (attrib cases_type cases_pred cases_del)
+ "declaration of cases rule" #>
+ Attrib.setup @{binding induct} (attrib induct_type induct_pred induct_del)
+ "declaration of induction rule" #>
+ Attrib.setup @{binding coinduct} (attrib coinduct_type coinduct_pred coinduct_del)
+ "declaration of coinduction rule";
end;
@@ -735,23 +734,29 @@
in
-val cases_meth =
- P.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule >>
- (fn (insts, opt_rule) => fn ctxt =>
- METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL (cases_tac ctxt insts opt_rule facts))));
+val cases_setup =
+ Method.setup @{binding cases}
+ (P.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule >>
+ (fn (insts, opt_rule) => fn ctxt =>
+ METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL (cases_tac ctxt insts opt_rule facts)))))
+ "case analysis on types or predicates/sets";
-val induct_meth =
- P.and_list' (Scan.repeat (unless_more_args def_inst)) --
- (arbitrary -- taking -- Scan.option induct_rule) >>
- (fn (insts, ((arbitrary, taking), opt_rule)) => fn ctxt =>
- RAW_METHOD_CASES (fn facts =>
- Seq.DETERM (HEADGOAL (induct_tac ctxt insts arbitrary taking opt_rule facts))));
+val induct_setup =
+ Method.setup @{binding induct}
+ (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
+ (arbitrary -- taking -- Scan.option induct_rule) >>
+ (fn (insts, ((arbitrary, taking), opt_rule)) => fn ctxt =>
+ RAW_METHOD_CASES (fn facts =>
+ Seq.DETERM (HEADGOAL (induct_tac ctxt insts arbitrary taking opt_rule facts)))))
+ "induction on types or predicates/sets";
-val coinduct_meth =
- Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
- (fn ((insts, taking), opt_rule) => fn ctxt =>
- RAW_METHOD_CASES (fn facts =>
- Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts))));
+val coinduct_setup =
+ Method.setup @{binding coinduct}
+ (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
+ (fn ((insts, taking), opt_rule) => fn ctxt =>
+ RAW_METHOD_CASES (fn facts =>
+ Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts)))))
+ "coinduction on types or predicates/sets";
end;
@@ -759,10 +764,6 @@
(** theory setup **)
-val setup =
- attrib_setup #>
- Method.setup @{binding cases} cases_meth "case analysis on types or predicates/sets" #>
- Method.setup @{binding induct} induct_meth "induction on types or predicates/sets" #>
- Method.setup @{binding coinduct} coinduct_meth "coinduction on types or predicates/sets";
+val setup = attrib_setup #> cases_setup #> induct_setup #> coinduct_setup;
end;
--- a/src/ZF/Constructible/L_axioms.thy Thu Mar 26 13:02:12 2009 +0100
+++ b/src/ZF/Constructible/L_axioms.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/ZF/Constructible/Rec_Separation.thy Fri Mar 27 09:58:48 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 13:02:12 2009 +0100
+++ b/src/ZF/Constructible/Separation.thy Fri Mar 27 09:58:48 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
--- a/src/ZF/Tools/ind_cases.ML Thu Mar 26 13:02:12 2009 +0100
+++ b/src/ZF/Tools/ind_cases.ML Fri Mar 27 09:58:48 2009 +0100
@@ -57,14 +57,14 @@
(* ind_cases method *)
-val mk_cases_meth = Scan.lift (Scan.repeat1 Args.name_source) >>
- (fn props => fn ctxt =>
- props
- |> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt) (Syntax.read_prop ctxt))
- |> Method.erule 0);
-
val setup =
- Method.setup @{binding "ind_cases"} mk_cases_meth "dynamic case analysis on sets";
+ Method.setup @{binding "ind_cases"}
+ (Scan.lift (Scan.repeat1 Args.name_source) >>
+ (fn props => fn ctxt =>
+ props
+ |> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt) (Syntax.read_prop ctxt))
+ |> Method.erule 0))
+ "dynamic case analysis on sets";
(* outer syntax *)
--- a/src/ZF/Tools/typechk.ML Thu Mar 26 13:02:12 2009 +0100
+++ b/src/ZF/Tools/typechk.ML Fri Mar 27 09:58:48 2009 +0100
@@ -109,11 +109,13 @@
(* concrete syntax *)
-val typecheck_meth =
- Method.sections
- [Args.add -- Args.colon >> K (I, TC_add),
- Args.del -- Args.colon >> K (I, TC_del)]
- >> (K (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt))));
+val typecheck_setup =
+ Method.setup @{binding typecheck}
+ (Method.sections
+ [Args.add -- Args.colon >> K (I, TC_add),
+ Args.del -- Args.colon >> K (I, TC_del)]
+ >> (K (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt)))))
+ "ZF type-checking";
val _ =
OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag
@@ -125,7 +127,7 @@
val setup =
Attrib.setup @{binding TC} (Attrib.add_del TC_add TC_del) "declaration of type-checking rule" #>
- Method.setup @{binding typecheck} typecheck_meth "ZF type-checking" #>
+ typecheck_setup #>
Simplifier.map_simpset (fn ss => ss setSolver type_solver);
end;