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