# HG changeset patch # User ballarin # Date 1230631801 -3600 # Node ID ea97aa6aeba2b790c69d6a3b1ba1e6913a3519ca # Parent 8f84a608883d24a8ede1a0052e696c40cedd2a81# Parent 7dc7a75033ea53c879f5c3e26709d974f4e92ba8 Merged. diff -r 7dc7a75033ea -r ea97aa6aeba2 etc/isar-keywords-ZF.el diff -r 7dc7a75033ea -r ea97aa6aeba2 etc/isar-keywords.el --- a/etc/isar-keywords.el Mon Dec 29 22:43:41 2008 +0100 +++ b/etc/isar-keywords.el Tue Dec 30 11:10:01 2008 +0100 @@ -46,6 +46,9 @@ "chapter" "class" "class_deps" + "class_interpret" + "class_interpretation" + "class_locale" "classes" "classrel" "code_abort" @@ -420,6 +423,7 @@ "axiomatization" "axioms" "class" + "class_locale" "classes" "classrel" "code_abort" @@ -503,6 +507,7 @@ (defconst isar-keywords-theory-goal '("ax_specification" + "class_interpretation" "corollary" "cpodef" "function" @@ -541,7 +546,8 @@ "subsubsect")) (defconst isar-keywords-proof-goal - '("have" + '("class_interpret" + "have" "hence" "interpret" "invoke")) diff -r 7dc7a75033ea -r ea97aa6aeba2 src/FOL/IsaMakefile --- a/src/FOL/IsaMakefile Mon Dec 29 22:43:41 2008 +0100 +++ b/src/FOL/IsaMakefile Tue Dec 30 11:10:01 2008 +0100 @@ -46,7 +46,7 @@ FOL-ex: FOL $(LOG)/FOL-ex.gz $(LOG)/FOL-ex.gz: $(OUT)/FOL ex/First_Order_Logic.thy ex/If.thy \ - ex/IffOracle.thy ex/LocaleTest.thy ex/Nat.thy ex/Natural_Numbers.thy \ + ex/IffOracle.thy ex/Nat.thy ex/Natural_Numbers.thy \ ex/NewLocaleSetup.thy ex/NewLocaleTest.thy \ ex/Miniscope.thy ex/Prolog.thy ex/ROOT.ML ex/Classical.thy \ ex/document/root.tex ex/Foundation.thy ex/Intuitionistic.thy \ diff -r 7dc7a75033ea -r ea97aa6aeba2 src/FOL/ex/LocaleTest.thy --- a/src/FOL/ex/LocaleTest.thy Mon Dec 29 22:43:41 2008 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,765 +0,0 @@ -(* Title: FOL/ex/LocaleTest.thy - ID: $Id$ - Author: Clemens Ballarin - Copyright (c) 2005 by Clemens Ballarin - -Collection of regression tests for locales. -*) - -header {* Test of Locale Interpretation *} - -theory LocaleTest -imports FOL -begin - -ML {* set Toplevel.debug *} -ML {* set show_hyps *} -ML {* set show_sorts *} - -ML {* - fun check_thm name = let - val thy = the_context (); - val thm = PureThy.get_thm thy name; - val {prop, hyps, ...} = rep_thm thm; - val prems = Logic.strip_imp_prems prop; - val _ = if null hyps then () - else error ("Theorem " ^ quote name ^ " has meta hyps.\n" ^ - "Consistency check of locales package failed."); - val _ = if null prems then () - else error ("Theorem " ^ quote name ^ " has premises.\n" ^ - "Consistency check of locales package failed."); - in () end; -*} - -section {* Context Elements and Locale Expressions *} - -text {* Naming convention for global objects: prefixes L and l *} - -subsection {* Renaming with Syntax *} - -locale LS = var mult + - assumes "mult(x, y) = mult(y, x)" - -print_locale LS - -locale LS' = LS mult (infixl "**" 60) - -print_locale LS' - -locale LT = var mult (infixl "**" 60) + - assumes "x ** y = y ** x" - -locale LU = LT mult (infixl "**" 60) + LT add (infixl "++" 55) + var h + - assumes hom: "h(x ** y) = h(x) ++ h(y)" - - -(* FIXME: graceful handling of type errors? -locale LY = LT mult (infixl "**" 60) + LT add (binder "++" 55) + var h + - assumes "mult(x) == add" -*) - - -locale LV = LU _ add - -locale LW = LU _ mult (infixl "**" 60) - - -subsection {* Constrains *} - -locale LZ = fixes a (structure) -locale LZ' = LZ + - constrains a :: "'a => 'b" - assumes "a (x :: 'a) = a (y)" -print_locale LZ' - - -section {* Interpretation *} - -text {* Naming convention for global objects: prefixes I and i *} - -text {* interpretation input syntax *} - -locale IL -locale IM = fixes a and b and c - -interpretation test: IL + IM a b c [x y z] . - -print_interps IL (* output: test *) -print_interps IM (* output: test *) - -interpretation test: IL print_interps IM . - -interpretation IL . - -text {* Processing of locale expression *} - -locale IA = fixes a assumes asm_A: "a = a" - -locale IB = fixes b assumes asm_B [simp]: "b = b" - -locale IC = IA + IB + assumes asm_C: "b = b" - -locale IC' = IA + IB + assumes asm_C: "c = c" - (* independent type var in c *) - -locale ID = IA + IB + fixes d defines def_D: "d == (a = b)" - -theorem (in ID) True .. - -typedecl i -arities i :: "term" - - -interpretation i1: IC ["X::i" "Y::i"] by unfold_locales auto - -print_interps IA (* output: i1 *) - -(* possible accesses *) -thm i1.a.asm_A thm LocaleTest.IA_locale.i1.a.asm_A thm IA_locale.i1.a.asm_A -thm i1.asm_A thm LocaleTest.i1.asm_A - -ML {* check_thm "i1.a.asm_A" *} - -(* without prefix *) - -interpretation IC ["W::i" "Z::i"] by intro_locales (* subsumed by i1: IC *) -interpretation IC ["W::'a" "Z::i"] by unfold_locales auto - (* subsumes i1: IA and i1: IC *) - -print_interps IA (* output: , i1 *) - -(* possible accesses *) -thm asm_C thm a_b.asm_C thm LocaleTest.IC_locale.a_b.asm_C thm IC_locale.a_b.asm_C - -ML {* check_thm "asm_C" *} - -interpretation i2: ID [X "Y::i" "Y = X"] - by (simp add: eq_commute) unfold_locales - -print_interps IA (* output: , i1 *) -print_interps ID (* output: i2 *) - - -interpretation i3: ID [X "Y::i"] by simp unfold_locales - -(* duplicate: thm not added *) - -(* thm i3.a.asm_A *) - - -print_interps IA (* output: , i1 *) -print_interps IB (* output: i1 *) -print_interps IC (* output: f" - -consts default :: "'a" - -theorem True -proof - - fix alpha::i and beta - have alpha_A: "IA(alpha)" by unfold_locales - interpret i5: IA [alpha] by intro_locales (* subsumed *) - print_interps IA (* output: , i1 *) - interpret i6: IC [alpha beta] by unfold_locales auto - print_interps IA (* output: , i1 *) - print_interps IC (* output: , i1, i6 *) - interpret i11: IF ["default = default"] by (fast intro: IF.intro) - thm i11.asm_F [where 'a = i] (* default has schematic type *) -qed rule - -theorem (in IA) True -proof - - print_interps! IA - fix beta and gamma - interpret i9: ID [a beta _] - apply - apply assumption - apply unfold_locales - apply (rule refl) done -qed rule - - -(* Definition involving free variable *) - -ML {* reset show_sorts *} - -locale IE = fixes e defines e_def: "e(x) == x & x" - notes e_def2 = e_def - -lemma (in IE) True thm e_def by fast - -interpretation i7: IE ["%x. x"] by simp - -thm i7.e_def2 (* has no premise *) - -ML {* check_thm "i7.e_def2" *} - -locale IE' = fixes e defines e_def: "e == (%x. x & x)" - notes e_def2 = e_def - -interpretation i7': IE' ["(%x. x)"] by simp - -thm i7'.e_def2 - -ML {* check_thm "i7'.e_def2" *} - -(* Definition involving free variable in assm *) - -locale IG = fixes g assumes asm_G: "g --> x" - notes asm_G2 = asm_G - -interpretation i8: IG ["False"] by unfold_locales fast - -thm i8.asm_G2 - -ML {* check_thm "i8.asm_G2" *} - -text {* Locale without assumptions *} - -locale IL1 = notes rev_conjI [intro] = conjI [THEN iffD1 [OF conj_commute]] - -lemma "[| P; Q |] ==> P & Q" -proof - - interpret my: IL1 . txt {* No chained fact required. *} - assume Q and P txt {* order reversed *} - then show "P & Q" .. txt {* Applies @{thm my.rev_conjI}. *} -qed - -locale IL11 = notes rev_conjI = conjI [THEN iffD1 [OF conj_commute]] - - -subsection {* Simple locale with assumptions *} - -consts ibin :: "[i, i] => i" (infixl "#" 60) - -axioms i_assoc: "(x # y) # z = x # (y # z)" - i_comm: "x # y = y # x" - -locale IL2 = - fixes OP (infixl "+" 60) - assumes assoc: "(x + y) + z = x + (y + z)" - and comm: "x + y = y + x" - -lemma (in IL2) lcomm: "x + (y + z) = y + (x + z)" -proof - - have "x + (y + z) = (x + y) + z" by (simp add: assoc) - also have "... = (y + x) + z" by (simp add: comm) - also have "... = y + (x + z)" by (simp add: assoc) - finally show ?thesis . -qed - -lemmas (in IL2) AC = comm assoc lcomm - -lemma "(x::i) # y # z # w = y # x # w # z" -proof - - interpret my: IL2 ["op #"] by (rule IL2.intro [of "op #", OF i_assoc i_comm]) - show ?thesis by (simp only: my.OP.AC) (* or my.AC *) -qed - -subsection {* Nested locale with assumptions *} - -locale IL3 = - fixes OP (infixl "+" 60) - assumes assoc: "(x + y) + z = x + (y + z)" - -locale IL4 = IL3 + - assumes comm: "x + y = y + x" - -lemma (in IL4) lcomm: "x + (y + z) = y + (x + z)" -proof - - have "x + (y + z) = (x + y) + z" by (simp add: assoc) - also have "... = (y + x) + z" by (simp add: comm) - also have "... = y + (x + z)" by (simp add: assoc) - finally show ?thesis . -qed - -lemmas (in IL4) AC = comm assoc lcomm - -lemma "(x::i) # y # z # w = y # x # w # z" -proof - - interpret my: IL4 ["op #"] - by (auto intro: IL4.intro IL3.intro IL4_axioms.intro i_assoc i_comm) - show ?thesis by (simp only: my.OP.AC) (* or simply AC *) -qed - -text {* Locale with definition *} - -text {* This example is admittedly not very creative :-) *} - -locale IL5 = IL4 + var A + - defines A_def: "A == True" - -lemma (in IL5) lem: A - by (unfold A_def) rule - -lemma "IL5(op #) ==> True" -proof - - assume "IL5(op #)" - then interpret IL5 ["op #"] by (auto intro: IL5.axioms) - show ?thesis by (rule lem) (* lem instantiated to True *) -qed - -text {* Interpretation in a context with target *} - -lemma (in IL4) - fixes A (infixl "$" 60) - assumes A: "IL4(A)" - shows "(x::i) $ y $ z $ w = y $ x $ w $ z" -proof - - from A interpret A: IL4 ["A"] by (auto intro: IL4.axioms) - show ?thesis by (simp only: A.OP.AC) -qed - - -section {* Interpretation in Locales *} - -text {* Naming convention for global objects: prefixes R and r *} - -(* locale with many parameters --- - interpretations generate alternating group A5 *) - -locale RA5 = var A + var B + var C + var D + var E + - assumes eq: "A <-> B <-> C <-> D <-> E" - -interpretation RA5 < RA5 _ _ D E C -print_facts -print_interps RA5 - using A_B_C_D_E.eq apply (blast intro: RA5.intro) done - -interpretation RA5 < RA5 C _ E _ A -print_facts -print_interps RA5 - using A_B_C_D_E.eq apply (blast intro: RA5.intro) done - -interpretation RA5 < RA5 B C A _ _ -print_facts -print_interps RA5 - using A_B_C_D_E.eq apply (blast intro: RA5.intro) done - -interpretation RA5 < RA5 _ C D B _ . - (* Any even permutation of parameters is subsumed by the above. *) - -(* circle of three locales, forward direction *) - -locale RA1 = var A + var B + assumes p: "A <-> B" -locale RA2 = var A + var B + assumes q: "A & B | ~ A & ~ B" -locale RA3 = var A + var B + assumes r: "(A --> B) & (B --> A)" - -interpretation RA1 < RA2 - print_facts - using p apply unfold_locales apply fast done -interpretation RA2 < RA3 - print_facts - using q apply unfold_locales apply fast done -interpretation RA3 < RA1 - print_facts - using r apply unfold_locales apply fast done - -(* circle of three locales, backward direction *) - -locale RB1 = var A + var B + assumes p: "A <-> B" -locale RB2 = var A + var B + assumes q: "A & B | ~ A & ~ B" -locale RB3 = var A + var B + assumes r: "(A --> B) & (B --> A)" - -interpretation RB1 < RB2 - print_facts - using p apply unfold_locales apply fast done -interpretation RB3 < RB1 - print_facts - using r apply unfold_locales apply fast done -interpretation RB2 < RB3 - print_facts - using q apply unfold_locales apply fast done - -lemma (in RB1) True - print_facts - .. - - -(* Group example *) - -locale Rsemi = var prod (infixl "**" 65) + - assumes assoc: "(x ** y) ** z = x ** (y ** z)" - -locale Rlgrp = Rsemi + var one + var inv + - assumes lone: "one ** x = x" - and linv: "inv(x) ** x = one" - -lemma (in Rlgrp) lcancel: - "x ** y = x ** z <-> y = z" -proof - assume "x ** y = x ** z" - then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc) - then show "y = z" by (simp add: lone linv) -qed simp - -locale Rrgrp = Rsemi + var one + var inv + - assumes rone: "x ** one = x" - and rinv: "x ** inv(x) = one" - -lemma (in Rrgrp) rcancel: - "y ** x = z ** x <-> y = z" -proof - assume "y ** x = z ** x" - then have "y ** (x ** inv(x)) = z ** (x ** inv(x))" - by (simp add: assoc [symmetric]) - then show "y = z" by (simp add: rone rinv) -qed simp - -interpretation Rlgrp < Rrgrp - proof unfold_locales - { - fix x - have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone) - then show "x ** one = x" by (simp add: assoc lcancel) - } - note rone = this - { - fix x - have "inv(x) ** x ** inv(x) = inv(x) ** one" - by (simp add: linv lone rone) - then show "x ** inv(x) = one" by (simp add: assoc lcancel) - } - qed - -(* effect on printed locale *) - -print_locale! Rlgrp - -(* use of derived theorem *) - -lemma (in Rlgrp) - "y ** x = z ** x <-> y = z" - apply (rule rcancel) - print_interps Rrgrp thm lcancel rcancel - done - -(* circular interpretation *) - -interpretation Rrgrp < Rlgrp - proof unfold_locales - { - fix x - have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone) - then show "one ** x = x" by (simp add: assoc [symmetric] rcancel) - } - note lone = this - { - fix x - have "inv(x) ** (x ** inv(x)) = one ** inv(x)" - by (simp add: rinv lone rone) - then show "inv(x) ** x = one" by (simp add: assoc [symmetric] rcancel) - } - qed - -(* effect on printed locale *) - -print_locale! Rrgrp -print_locale! Rlgrp - -subsection {* Interaction of Interpretation in Theories and Locales: - in Locale, then in Theory *} - -consts - rone :: i - rinv :: "i => i" - -axioms - r_one : "rone # x = x" - r_inv : "rinv(x) # x = rone" - -interpretation Rbool: Rlgrp ["op #" "rone" "rinv"] -proof - fix x y z - { - show "(x # y) # z = x # (y # z)" by (rule i_assoc) - next - show "rone # x = x" by (rule r_one) - next - show "rinv(x) # x = rone" by (rule r_inv) - } -qed - -(* derived elements *) - -print_interps Rrgrp -print_interps Rlgrp - -lemma "y # x = z # x <-> y = z" by (rule Rbool.rcancel) - -(* adding lemma to derived element *) - -lemma (in Rrgrp) new_cancel: - "b ** a = c ** a <-> b = c" - by (rule rcancel) - -thm Rbool.new_cancel (* additional prems discharged!! *) - -ML {* check_thm "Rbool.new_cancel" *} - -lemma "b # a = c # a <-> b = c" by (rule Rbool.new_cancel) - - -subsection {* Interaction of Interpretation in Theories and Locales: - in Theory, then in Locale *} - -(* Another copy of the group example *) - -locale Rqsemi = var prod (infixl "**" 65) + - assumes assoc: "(x ** y) ** z = x ** (y ** z)" - -locale Rqlgrp = Rqsemi + var one + var inv + - assumes lone: "one ** x = x" - and linv: "inv(x) ** x = one" - -lemma (in Rqlgrp) lcancel: - "x ** y = x ** z <-> y = z" -proof - assume "x ** y = x ** z" - then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc) - then show "y = z" by (simp add: lone linv) -qed simp - -locale Rqrgrp = Rqsemi + var one + var inv + - assumes rone: "x ** one = x" - and rinv: "x ** inv(x) = one" - -lemma (in Rqrgrp) rcancel: - "y ** x = z ** x <-> y = z" -proof - assume "y ** x = z ** x" - then have "y ** (x ** inv(x)) = z ** (x ** inv(x))" - by (simp add: assoc [symmetric]) - then show "y = z" by (simp add: rone rinv) -qed simp - -interpretation Rqrgrp < Rrgrp - apply unfold_locales - apply (rule assoc) - apply (rule rone) - apply (rule rinv) - done - -interpretation R2: Rqlgrp ["op #" "rone" "rinv"] - apply unfold_locales (* FIXME: unfold_locales is too eager and shouldn't - solve this. *) - apply (rule i_assoc) - apply (rule r_one) - apply (rule r_inv) - done - -print_interps Rqsemi -print_interps Rqlgrp -print_interps Rlgrp (* no interpretations yet *) - - -interpretation Rqlgrp < Rqrgrp - proof unfold_locales - { - fix x - have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone) - then show "x ** one = x" by (simp add: assoc lcancel) - } - note rone = this - { - fix x - have "inv(x) ** x ** inv(x) = inv(x) ** one" - by (simp add: linv lone rone) - then show "x ** inv(x) = one" by (simp add: assoc lcancel) - } - qed - -print_interps! Rqrgrp -print_interps! Rsemi (* witness must not have meta hyps *) -print_interps! Rrgrp (* witness must not have meta hyps *) -print_interps! Rlgrp (* witness must not have meta hyps *) -thm R2.rcancel -thm R2.lcancel - -ML {* check_thm "R2.rcancel"; check_thm "R2.lcancel" *} - - -subsection {* Generation of Witness Theorems for Transitive Interpretations *} - -locale Rtriv = var x + - assumes x: "x = x" - -locale Rtriv2 = var x + var y + - assumes x: "x = x" and y: "y = y" - -interpretation Rtriv2 < Rtriv x - apply unfold_locales - apply (rule x) - done - -interpretation Rtriv2 < Rtriv y - apply unfold_locales - apply (rule y) - done - -print_locale Rtriv2 - -locale Rtriv3 = var x + var y + var z + - assumes x: "x = x" and y: "y = y" and z: "z = z" - -interpretation Rtriv3 < Rtriv2 x y - apply unfold_locales - apply (rule x) - apply (rule y) - done - -print_locale Rtriv3 - -interpretation Rtriv3 < Rtriv2 x z - apply unfold_locales - apply (rule x_y_z.x) - apply (rule z) - done - -ML {* set show_types *} - -print_locale Rtriv3 - - -subsection {* Normalisation Replaces Assumed Element by Derived Element *} - -typedecl ('a, 'b) pair -arities pair :: ("term", "term") "term" - -consts - pair :: "['a, 'b] => ('a, 'b) pair" - fst :: "('a, 'b) pair => 'a" - snd :: "('a, 'b) pair => 'b" - -axioms - fst [simp]: "fst(pair(x, y)) = x" - snd [simp]: "snd(pair(x, y)) = y" - -locale Rpair = var prod (infixl "**" 65) + var prodP (infixl "***" 65) + - defines P_def: "x *** y == pair(fst(x) ** fst(y), snd(x) ** snd(y))" - -locale Rpair_semi = Rpair + Rsemi - -interpretation Rpair_semi < Rsemi prodP (infixl "***" 65) -proof unfold_locales - fix x y z - show "(x *** y) *** z = x *** (y *** z)" - apply (simp only: P_def) apply (simp add: assoc) (* FIXME: unfold P_def fails *) - done -qed - -locale Rsemi_rev = Rsemi + var rprod (infixl "++" 65) + - defines r_def: "x ++ y == y ** x" - -lemma (in Rsemi_rev) r_assoc: - "(x ++ y) ++ z = x ++ (y ++ z)" - by (simp add: r_def assoc) - - -subsection {* Import of Locales with Predicates as Interpretation *} - -locale Ra = - assumes Ra: "True" - -locale Rb = Ra + - assumes Rb: "True" - -locale Rc = Rb + - assumes Rc: "True" - -print_locale! Rc - - -section {* Interpretation of Defined Concepts *} - -text {* Naming convention for global objects: prefixes D and d *} - - -subsection {* Simple examples *} - -locale Da = fixes a :: o - assumes true: a - -text {* In the following examples, @{term "~ a"} is the defined concept. *} - -lemma (in Da) not_false: "~ a <-> False" - apply simp apply (rule true) done - -interpretation D1: Da ["True"] - where "~ True == False" - apply - - apply unfold_locales [1] apply rule - by simp - -thm D1.not_false -lemma "False <-> False" apply (rule D1.not_false) done - -interpretation D2: Da ["x | ~ x"] - where "~ (x | ~ x) <-> ~ x & x" - apply - - apply unfold_locales [1] apply fast - by simp - -thm D2.not_false -lemma "~ x & x <-> False" apply (rule D2.not_false) done - -print_interps! Da - -(* Subscriptions of interpretations *) - -lemma (in Da) not_false2: "~a <-> False" - apply simp apply (rule true) done - -thm D1.not_false2 D2.not_false2 -lemma "False <-> False" apply (rule D1.not_false2) done -lemma "~x & x <-> False" apply (rule D2.not_false2) done - -(* Unfolding in attributes *) - -locale Db = Da + - fixes b :: o - assumes a_iff_b: "~a <-> b" - -lemmas (in Db) not_false_b = not_false [unfolded a_iff_b] - -interpretation D2: Db ["x | ~ x" "~ (x <-> x)"] - apply unfold_locales apply fast done - -thm D2.not_false_b -lemma "~(x <-> x) <-> False" apply (rule D2.not_false_b) done - -(* Subscription and attributes *) - -lemmas (in Db) not_false_b2 = not_false [unfolded a_iff_b] - -thm D2.not_false_b2 -lemma "~(x <-> x) <-> False" apply (rule D2.not_false_b2) done - -end diff -r 7dc7a75033ea -r ea97aa6aeba2 src/FOL/ex/NewLocaleSetup.thy --- a/src/FOL/ex/NewLocaleSetup.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/FOL/ex/NewLocaleSetup.thy Tue Dec 30 11:10:01 2008 +0100 @@ -44,9 +44,10 @@ val _ = OuterSyntax.command "interpretation" "prove interpretation of locale expression in theory" K.thy_goal - (P.!!! SpecParse.locale_expression - >> (fn expr => Toplevel.print o - Toplevel.theory_to_proof (Expression.interpretation_cmd expr))); + (P.!!! SpecParse.locale_expression -- + Scan.optional (P.$$$ "where" |-- P.and_list1 (SpecParse.opt_thm_name ":" -- P.prop)) [] + >> (fn (expr, mixin) => Toplevel.print o + Toplevel.theory_to_proof (Expression.interpretation_cmd expr mixin))); val _ = OuterSyntax.command "interpret" diff -r 7dc7a75033ea -r ea97aa6aeba2 src/FOL/ex/NewLocaleTest.thy --- a/src/FOL/ex/NewLocaleTest.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/FOL/ex/NewLocaleTest.thy Tue Dec 30 11:10:01 2008 +0100 @@ -8,9 +8,7 @@ imports NewLocaleSetup begin -ML_val {* set new_locales *} ML_val {* set Toplevel.debug *} -ML_val {* set show_hyps *} typedecl int arities int :: "term" @@ -24,7 +22,7 @@ int_minus: "(-x) + x = 0" int_minus2: "-(-x) = x" -text {* Inference of parameter types *} +section {* Inference of parameter types *} locale param1 = fixes p print_locale! param1 @@ -44,7 +42,7 @@ print_locale! param4 -text {* Incremental type constraints *} +subsection {* Incremental type constraints *} locale constraint1 = fixes prod (infixl "**" 65) @@ -58,7 +56,7 @@ print_locale! constraint2 -text {* Inheritance *} +section {* Inheritance *} locale semi = fixes prod (infixl "**" 65) @@ -94,7 +92,7 @@ print_locale! pert_hom' thm pert_hom'_def -text {* Syntax declarations *} +section {* Syntax declarations *} locale logic = fixes land (infixl "&&" 55) @@ -112,14 +110,30 @@ locale use_decl = logic + semi "op ||" print_locale! use_decl thm use_decl_def +locale extra_type = + fixes a :: 'a + and P :: "'a => 'b => o" +begin -text {* Foundational versions of theorems *} +definition test :: "'a => o" where + "test(x) <-> (ALL b. P(x, b))" + +end + +term extra_type.test thm extra_type.test_def + +interpretation var: extra_type "0" "%x y. x = 0" . + +thm var.test_def + + +section {* Foundational versions of theorems *} thm logic.assoc thm logic.lor_def -text {* Defines *} +section {* Defines *} locale logic_def = fixes land (infixl "&&" 55) @@ -149,7 +163,7 @@ end -text {* Notes *} +section {* Notes *} (* A somewhat arcane homomorphism example *) @@ -165,11 +179,21 @@ assumes semi_homh: "semi_hom(prod, sum, h)" notes semi_hom_mult = semi_hom_mult [OF semi_homh] +thm semi_hom_loc.semi_hom_mult +(* unspecified, attribute not applied in backgroud theory !!! *) + lemma (in semi_hom_loc) "h(prod(x, y)) = sum(h(x), h(y))" by (rule semi_hom_mult) +(* Referring to facts from within a context specification *) -text {* Theorem statements *} +lemma + assumes x: "P <-> P" + notes y = x + shows True .. + + +section {* Theorem statements *} lemma (in lgrp) lcancel: "x ** y = x ** z <-> y = z" @@ -200,7 +224,7 @@ print_locale! rgrp -text {* Patterns *} +subsection {* Patterns *} lemma (in rgrp) assumes "y ** x = z ** x" (is ?a) @@ -218,7 +242,7 @@ qed -text {* Interpretation between locales: sublocales *} +section {* Interpretation between locales: sublocales *} sublocale lgrp < right: rgrp print_facts @@ -305,8 +329,7 @@ done print_locale! order_with_def -(* Note that decls come after theorems that make use of them. - Appears to be harmless at least in this example. *) +(* Note that decls come after theorems that make use of them. *) (* locale with many parameters --- @@ -359,7 +382,7 @@ print_locale! trivial (* No instance for y created (subsumed). *) -text {* Sublocale, then interpretation in theory *} +subsection {* Sublocale, then interpretation in theory *} interpretation int: lgrp "op +" "0" "minus" proof unfold_locales @@ -374,7 +397,7 @@ (* the latter comes through the sublocale relation *) -text {* Interpretation in theory, then sublocale *} +subsection {* Interpretation in theory, then sublocale *} interpretation (* fol: *) logic "op +" "minus" (* FIXME declaration of qualified names *) @@ -386,10 +409,12 @@ assumes assoc: "(x && y) && z = x && (y && z)" and notnot: "-- (-- x) = x" begin -(* FIXME + +(* FIXME interpretation below fails definition lor (infixl "||" 50) where "x || y = --(-- x && -- y)" *) + end sublocale logic < two: logic2 @@ -398,7 +423,48 @@ thm two.assoc -text {* Interpretation in proofs *} +subsection {* Declarations and sublocale *} + +locale logic_a = logic +locale logic_b = logic + +sublocale logic_a < logic_b + by unfold_locales + + +subsection {* Equations *} + +locale logic_o = + fixes land (infixl "&&" 55) + and lnot ("-- _" [60] 60) + assumes assoc_o: "(x && y) && z <-> x && (y && z)" + and notnot_o: "-- (-- x) <-> x" +begin + +definition lor_o (infixl "||" 50) where + "x || y <-> --(-- x && -- y)" + +end + +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+ + show "logic_o.lor_o(op &, Not, x, y) <-> x | y" + by (unfold logic_o.lor_o_def [OF bool_logic_o]) fast +qed + +thm x.lor_o_def bool_logic_o + +lemma lor_triv: "z <-> z" .. + +lemma (in logic_o) lor_triv: "x || y <-> x || y" by fast + +thm lor_triv [where z = True] (* Check strict prefix. *) + x.lor_triv + + +subsection {* Interpretation in proofs *} lemma True proof diff -r 7dc7a75033ea -r ea97aa6aeba2 src/FOL/ex/ROOT.ML --- a/src/FOL/ex/ROOT.ML Mon Dec 29 22:43:41 2008 +0100 +++ b/src/FOL/ex/ROOT.ML Tue Dec 30 11:10:01 2008 +0100 @@ -29,6 +29,5 @@ ]; (*regression test for locales -- sets several global flags!*) -no_document use_thy "LocaleTest"; no_document use_thy "NewLocaleTest"; diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/Algebra/AbelCoset.thy --- a/src/HOL/Algebra/AbelCoset.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/Algebra/AbelCoset.thy Tue Dec 30 11:10:01 2008 +0100 @@ -1,6 +1,5 @@ (* Title: HOL/Algebra/AbelCoset.thy - Id: $Id$ Author: Stephan Hohe, TU Muenchen *) @@ -52,7 +51,9 @@ "a_kernel G H h \ kernel \carrier = carrier G, mult = add G, one = zero G\ \carrier = carrier H, mult = add H, one = zero H\ h" -locale abelian_group_hom = abelian_group G + abelian_group H + var h + +locale abelian_group_hom = G: abelian_group G + H: abelian_group H + for G (structure) and H (structure) + + fixes h assumes a_group_hom: "group_hom (| carrier = carrier G, mult = add G, one = zero G |) (| carrier = carrier H, mult = add H, one = zero H |) h" @@ -180,7 +181,8 @@ subsubsection {* Subgroups *} -locale additive_subgroup = var H + struct G + +locale additive_subgroup = + fixes H and G (structure) assumes a_subgroup: "subgroup H \carrier = carrier G, mult = add G, one = zero G\" lemma (in additive_subgroup) is_additive_subgroup: @@ -218,7 +220,7 @@ text {* Every subgroup of an @{text "abelian_group"} is normal *} -locale abelian_subgroup = additive_subgroup H G + abelian_group G + +locale abelian_subgroup = additive_subgroup + abelian_group G + assumes a_normal: "normal H \carrier = carrier G, mult = add G, one = zero G\" lemma (in abelian_subgroup) is_abelian_subgroup: @@ -230,7 +232,7 @@ and a_comm: "!!x y. [| x \ carrier G; y \ carrier G |] ==> x \\<^bsub>G\<^esub> y = y \\<^bsub>G\<^esub> x" shows "abelian_subgroup H G" proof - - interpret normal ["H" "\carrier = carrier G, mult = add G, one = zero G\"] + interpret normal "H" "\carrier = carrier G, mult = add G, one = zero G\" by (rule a_normal) show "abelian_subgroup H G" @@ -243,9 +245,9 @@ and a_subgroup: "subgroup H \carrier = carrier G, mult = add G, one = zero G\" shows "abelian_subgroup H G" proof - - interpret comm_group ["\carrier = carrier G, mult = add G, one = zero G\"] + interpret comm_group "\carrier = carrier G, mult = add G, one = zero G\" by (rule a_comm_group) - interpret subgroup ["H" "\carrier = carrier G, mult = add G, one = zero G\"] + interpret subgroup "H" "\carrier = carrier G, mult = add G, one = zero G\" by (rule a_subgroup) show "abelian_subgroup H G" @@ -538,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 @@ -690,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 7dc7a75033ea -r ea97aa6aeba2 src/HOL/Algebra/Congruence.thy --- a/src/HOL/Algebra/Congruence.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/Algebra/Congruence.thy Tue Dec 30 11:10:01 2008 +0100 @@ -1,6 +1,5 @@ (* Title: Algebra/Congruence.thy - Id: $Id$ Author: Clemens Ballarin, started 3 January 2008 Copyright: Clemens Ballarin *) diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/Algebra/Coset.thy --- a/src/HOL/Algebra/Coset.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/Algebra/Coset.thy Tue Dec 30 11:10:01 2008 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Algebra/Coset.thy - ID: $Id$ Author: Florian Kammueller, with new proofs by L C Paulson, and Stephan Hohe *) @@ -114,7 +113,7 @@ and repr: "H #> x = H #> y" shows "y \ H #> x" proof - - interpret subgroup [H G] by fact + interpret subgroup H G by fact show ?thesis apply (subst repr) apply (intro rcos_self) apply (rule ycarr) @@ -129,7 +128,7 @@ and a': "a' \ H #> a" shows "a' \ carrier G" proof - - interpret group [G] by fact + interpret group G by fact from subset and acarr have "H #> a \ carrier G" by (rule r_coset_subset_G) from this and a' @@ -142,7 +141,7 @@ assumes hH: "h \ H" shows "H #> h = H" proof - - interpret group [G] by fact + interpret group G by fact show ?thesis apply (unfold r_coset_def) apply rule apply rule @@ -173,7 +172,7 @@ and x'cos: "x' \ H #> x" shows "(x' \ inv x) \ H" proof - - interpret group [G] by fact + interpret group G by fact from xcarr x'cos have x'carr: "x' \ carrier G" by (rule elemrcos_carrier[OF is_group]) @@ -213,7 +212,7 @@ and xixH: "(x' \ inv x) \ H" shows "x' \ H #> x" proof - - interpret group [G] by fact + interpret group G by fact from xixH have "\h\H. x' \ (inv x) = h" by fast from this @@ -244,7 +243,7 @@ assumes carr: "x \ carrier G" "x' \ carrier G" shows "(x' \ H #> x) = (x' \ inv x \ H)" proof - - interpret group [G] by fact + interpret group G by fact show ?thesis proof assume "x' \ H #> x" from this and carr show "x' \ inv x \ H" @@ -263,7 +262,7 @@ assumes XH: "X \ rcosets H" shows "X \ carrier G" proof - - interpret group [G] by fact + interpret group G by fact from XH have "\x\ carrier G. X = H #> x" unfolding RCOSETS_def by fast @@ -348,7 +347,7 @@ and xixH: "(inv x \ x') \ H" shows "x' \ x <# H" proof - - interpret group [G] by fact + interpret group G by fact from xixH have "\h\H. (inv x) \ x' = h" by fast from this @@ -600,7 +599,7 @@ assumes "group G" shows "equiv (carrier G) (rcong H)" proof - - interpret group [G] by fact + interpret group G by fact show ?thesis proof (intro equiv.intro) show "refl (carrier G) (rcong H)" @@ -647,7 +646,7 @@ assumes a: "a \ carrier G" shows "a <# H = rcong H `` {a}" proof - - interpret group [G] by fact + interpret group G by fact show ?thesis by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a ) qed @@ -658,7 +657,7 @@ assumes p: "ha \ a = h \ b" "a \ carrier G" "b \ carrier G" "h \ H" "ha \ H" "hb \ H" shows "hb \ a \ (\h\H. {h \ b})" proof - - interpret subgroup [H G] by fact + interpret subgroup H G by fact from p show ?thesis apply (rule_tac UN_I [of "hb \ ((inv ha) \ h)"]) apply (simp add: ) apply (simp add: m_assoc transpose_inv) @@ -670,7 +669,7 @@ assumes p: "a \ rcosets H" "b \ rcosets H" "a\b" shows "a \ b = {}" proof - - interpret subgroup [H G] by fact + interpret subgroup H G by fact from p show ?thesis apply (simp add: RCOSETS_def r_coset_def) apply (blast intro: rcos_equation prems sym) done @@ -760,7 +759,7 @@ assumes "subgroup H G" shows "\(rcosets H) = carrier G" proof - - interpret subgroup [H G] by fact + interpret subgroup H G by fact show ?thesis apply (rule equalityI) apply (force simp add: RCOSETS_def r_coset_def) @@ -847,7 +846,7 @@ assumes "group G" shows "H \ rcosets H" proof - - interpret group [G] by fact + interpret group G by fact from _ subgroup_axioms have "H #> \ = H" by (rule coset_join2) auto then show ?thesis diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/Algebra/Divisibility.thy --- a/src/HOL/Algebra/Divisibility.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/Algebra/Divisibility.thy Tue Dec 30 11:10:01 2008 +0100 @@ -1,6 +1,5 @@ (* Title: Divisibility in monoids and rings - Id: $Id$ Author: Clemens Ballarin, started 18 July 2008 Based on work by Stephan Hohe. @@ -32,7 +31,7 @@ "monoid_cancel G" .. -interpretation group \ monoid_cancel +sublocale group \ monoid_cancel proof qed simp+ @@ -45,7 +44,7 @@ "\a b c. \a \ c = b \ c; a \ carrier G; b \ carrier G; c \ carrier G\ \ a = b" shows "comm_monoid_cancel G" proof - - interpret comm_monoid [G] by fact + interpret comm_monoid G by fact show "comm_monoid_cancel G" apply unfold_locales apply (subgoal_tac "a \ c = b \ c") @@ -59,7 +58,7 @@ "comm_monoid_cancel G" by intro_locales -interpretation comm_group \ comm_monoid_cancel +sublocale comm_group \ comm_monoid_cancel .. @@ -755,7 +754,7 @@ using pf unfolding properfactor_lless proof - - interpret weak_partial_order ["division_rel G"] .. + interpret weak_partial_order "division_rel G" .. from x'x have "x' .=\<^bsub>division_rel G\<^esub> x" by simp also assume "x \\<^bsub>division_rel G\<^esub> y" @@ -771,7 +770,7 @@ using pf unfolding properfactor_lless proof - - interpret weak_partial_order ["division_rel G"] .. + interpret weak_partial_order "division_rel G" .. assume "x \\<^bsub>division_rel G\<^esub> y" also from yy' have "y .=\<^bsub>division_rel G\<^esub> y'" by simp @@ -2916,7 +2915,7 @@ lemma (in gcd_condition_monoid) division_weak_lower_semilattice [simp]: shows "weak_lower_semilattice (division_rel G)" proof - - interpret weak_partial_order ["division_rel G"] .. + interpret weak_partial_order "division_rel G" .. show ?thesis apply (unfold_locales, simp_all) proof - @@ -2941,7 +2940,7 @@ shows "a' gcdof b c" proof - note carr = a'carr carr' - interpret weak_lower_semilattice ["division_rel G"] by simp + interpret weak_lower_semilattice "division_rel G" by simp have "a' \ carrier G \ a' gcdof b c" apply (simp add: gcdof_greatestLower carr') apply (subst greatest_Lower_cong_l[of _ a]) @@ -2958,7 +2957,7 @@ assumes carr: "a \ carrier G" "b \ carrier G" shows "somegcd G a b \ carrier G" proof - - interpret weak_lower_semilattice ["division_rel G"] by simp + interpret weak_lower_semilattice "division_rel G" by simp show ?thesis apply (simp add: somegcd_meet[OF carr]) apply (rule meet_closed[simplified], fact+) @@ -2969,7 +2968,7 @@ assumes carr: "a \ carrier G" "b \ carrier G" shows "(somegcd G a b) gcdof a b" proof - - interpret weak_lower_semilattice ["division_rel G"] by simp + interpret weak_lower_semilattice "division_rel G" by simp from carr have "somegcd G a b \ carrier G \ (somegcd G a b) gcdof a b" apply (subst gcdof_greatestLower, simp, simp) @@ -2983,7 +2982,7 @@ assumes carr: "a \ carrier G" "b \ carrier G" shows "\x\carrier G. x = somegcd G a b" proof - - interpret weak_lower_semilattice ["division_rel G"] by simp + interpret weak_lower_semilattice "division_rel G" by simp show ?thesis apply (simp add: somegcd_meet[OF carr]) apply (rule meet_closed[simplified], fact+) @@ -2994,7 +2993,7 @@ assumes carr: "a \ carrier G" "b \ carrier G" shows "(somegcd G a b) divides a" proof - - interpret weak_lower_semilattice ["division_rel G"] by simp + interpret weak_lower_semilattice "division_rel G" by simp show ?thesis apply (simp add: somegcd_meet[OF carr]) apply (rule meet_left[simplified], fact+) @@ -3005,7 +3004,7 @@ assumes carr: "a \ carrier G" "b \ carrier G" shows "(somegcd G a b) divides b" proof - - interpret weak_lower_semilattice ["division_rel G"] by simp + interpret weak_lower_semilattice "division_rel G" by simp show ?thesis apply (simp add: somegcd_meet[OF carr]) apply (rule meet_right[simplified], fact+) @@ -3017,7 +3016,7 @@ and L: "x \ carrier G" "y \ carrier G" "z \ carrier G" shows "z divides (somegcd G x y)" proof - - interpret weak_lower_semilattice ["division_rel G"] by simp + interpret weak_lower_semilattice "division_rel G" by simp show ?thesis apply (simp add: somegcd_meet L) apply (rule meet_le[simplified], fact+) @@ -3029,7 +3028,7 @@ and carr: "x \ carrier G" "x' \ carrier G" "y \ carrier G" shows "somegcd G x y \ somegcd G x' y" proof - - interpret weak_lower_semilattice ["division_rel G"] by simp + interpret weak_lower_semilattice "division_rel G" by simp show ?thesis apply (simp add: somegcd_meet carr) apply (rule meet_cong_l[simplified], fact+) @@ -3041,7 +3040,7 @@ and yy': "y \ y'" shows "somegcd G x y \ somegcd G x y'" proof - - interpret weak_lower_semilattice ["division_rel G"] by simp + interpret weak_lower_semilattice "division_rel G" by simp show ?thesis apply (simp add: somegcd_meet carr) apply (rule meet_cong_r[simplified], fact+) @@ -3092,7 +3091,7 @@ assumes "finite A" "A \ carrier G" "A \ {}" shows "\x\ carrier G. x = SomeGcd G A" proof - - interpret weak_lower_semilattice ["division_rel G"] by simp + interpret weak_lower_semilattice "division_rel G" by simp show ?thesis apply (simp add: SomeGcd_def) apply (rule finite_inf_closed[simplified], fact+) @@ -3103,7 +3102,7 @@ assumes carr: "a \ carrier G" "b \ carrier G" "c \ carrier G" shows "somegcd G (somegcd G a b) c \ somegcd G a (somegcd G b c)" proof - - interpret weak_lower_semilattice ["division_rel G"] by simp + interpret weak_lower_semilattice "division_rel G" by simp show ?thesis apply (subst (2 3) somegcd_meet, (simp add: carr)+) apply (simp add: somegcd_meet carr) @@ -3313,7 +3312,7 @@ qed qed -interpretation gcd_condition_monoid \ primeness_condition_monoid +sublocale gcd_condition_monoid \ primeness_condition_monoid by (rule primeness_condition) @@ -3832,7 +3831,7 @@ with fca fcb show ?thesis by simp qed -interpretation factorial_monoid \ divisor_chain_condition_monoid +sublocale factorial_monoid \ divisor_chain_condition_monoid apply unfold_locales apply (rule wfUNIVI) apply (rule measure_induct[of "factorcount G"]) @@ -3854,7 +3853,7 @@ done qed -interpretation factorial_monoid \ primeness_condition_monoid +sublocale factorial_monoid \ primeness_condition_monoid proof qed (rule irreducible_is_prime) @@ -3866,13 +3865,13 @@ shows "gcd_condition_monoid G" proof qed (rule gcdof_exists) -interpretation factorial_monoid \ gcd_condition_monoid +sublocale factorial_monoid \ gcd_condition_monoid proof qed (rule gcdof_exists) lemma (in factorial_monoid) division_weak_lattice [simp]: shows "weak_lattice (division_rel G)" proof - - interpret weak_lower_semilattice ["division_rel G"] by simp + interpret weak_lower_semilattice "division_rel G" by simp show "weak_lattice (division_rel G)" apply (unfold_locales, simp_all) @@ -3902,14 +3901,14 @@ proof clarify assume dcc: "divisor_chain_condition_monoid G" and pc: "primeness_condition_monoid G" - interpret divisor_chain_condition_monoid ["G"] by (rule dcc) - interpret primeness_condition_monoid ["G"] by (rule pc) + interpret divisor_chain_condition_monoid "G" by (rule dcc) + interpret primeness_condition_monoid "G" by (rule pc) show "factorial_monoid G" by (fast intro: factorial_monoidI wfactors_exist wfactors_unique) next assume fm: "factorial_monoid G" - interpret factorial_monoid ["G"] by (rule fm) + interpret factorial_monoid "G" by (rule fm) show "divisor_chain_condition_monoid G \ primeness_condition_monoid G" by rule unfold_locales qed @@ -3920,13 +3919,13 @@ proof clarify assume dcc: "divisor_chain_condition_monoid G" and gc: "gcd_condition_monoid G" - interpret divisor_chain_condition_monoid ["G"] by (rule dcc) - interpret gcd_condition_monoid ["G"] by (rule gc) + interpret divisor_chain_condition_monoid "G" by (rule dcc) + interpret gcd_condition_monoid "G" by (rule gc) show "factorial_monoid G" by (simp add: factorial_condition_one[symmetric], rule, unfold_locales) next assume fm: "factorial_monoid G" - interpret factorial_monoid ["G"] by (rule fm) + interpret factorial_monoid "G" by (rule fm) show "divisor_chain_condition_monoid G \ gcd_condition_monoid G" by rule unfold_locales qed diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/Algebra/FiniteProduct.thy --- a/src/HOL/Algebra/FiniteProduct.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/Algebra/FiniteProduct.thy Tue Dec 30 11:10:01 2008 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Algebra/FiniteProduct.thy - ID: $Id$ Author: Clemens Ballarin, started 19 November 2002 This file is largely based on HOL/Finite_Set.thy. @@ -519,9 +518,9 @@ lemma finprod_singleton: assumes i_in_A: "i \ A" and fin_A: "finite A" and f_Pi: "f \ A \ carrier G" shows "(\j\A. if i = j then f j else \) = f i" - using i_in_A G.finprod_insert [of "A - {i}" i "(\j. if i = j then f j else \)"] - fin_A f_Pi G.finprod_one [of "A - {i}"] - G.finprod_cong [of "A - {i}" "A - {i}" "(\j. if i = j then f j else \)" "(\i. \)"] + using i_in_A finprod_insert [of "A - {i}" i "(\j. if i = j then f j else \)"] + fin_A f_Pi finprod_one [of "A - {i}"] + finprod_cong [of "A - {i}" "A - {i}" "(\j. if i = j then f j else \)" "(\i. \)"] unfolding Pi_def simp_implies_def by (force simp add: insert_absorb) end diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/Algebra/Group.thy --- a/src/HOL/Algebra/Group.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/Algebra/Group.thy Tue Dec 30 11:10:01 2008 +0100 @@ -1,6 +1,5 @@ (* Title: HOL/Algebra/Group.thy - Id: $Id$ Author: Clemens Ballarin, started 4 February 2003 Based on work by Florian Kammueller, L C Paulson and Markus Wenzel. @@ -425,7 +424,7 @@ assumes "group G" shows "group (G\carrier := H\)" proof - - interpret group [G] by fact + interpret group G by fact show ?thesis apply (rule monoid.group_l_invI) apply (unfold_locales) [1] @@ -489,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 @@ -501,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) @@ -526,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 @@ -542,15 +541,6 @@ {h. h \ carrier G -> carrier H & (\x \ carrier G. \y \ carrier G. h (x \\<^bsub>G\<^esub> y) = h x \\<^bsub>H\<^esub> h y)}" -lemma hom_mult: - "[| h \ hom G H; x \ carrier G; y \ carrier G |] - ==> h (x \\<^bsub>G\<^esub> y) = h x \\<^bsub>H\<^esub> h y" - by (simp add: hom_def) - -lemma hom_closed: - "[| h \ hom G H; x \ carrier G |] ==> h x \ carrier H" - by (auto simp add: hom_def funcset_mem) - lemma (in group) hom_compose: "[|h \ hom G H; i \ hom H I|] ==> compose (carrier G) i h \ hom G I" apply (auto simp add: hom_def funcset_compose) @@ -587,10 +577,23 @@ text{*Basis for homomorphism proofs: we assume two groups @{term G} and @{term H}, with a homomorphism @{term h} between them*} -locale group_hom = group G + group H + var h + +locale group_hom = G: group G + H: group H for G (structure) and H (structure) + + fixes h assumes homh: "h \ hom G H" - notes hom_mult [simp] = hom_mult [OF homh] - and hom_closed [simp] = hom_closed [OF homh] + +lemma (in group_hom) hom_mult [simp]: + "[| x \ carrier G; y \ carrier G |] ==> h (x \\<^bsub>G\<^esub> y) = h x \\<^bsub>H\<^esub> h y" +proof - + assume "x \ carrier G" "y \ carrier G" + with homh [unfolded hom_def] show ?thesis by simp +qed + +lemma (in group_hom) hom_closed [simp]: + "x \ carrier G ==> h x \ carrier H" +proof - + assume "x \ carrier G" + with homh [unfolded hom_def] show ?thesis by (auto simp add: funcset_mem) +qed lemma (in group_hom) one_closed [simp]: "h \ \ carrier H" diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/Algebra/Ideal.thy --- a/src/HOL/Algebra/Ideal.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/Algebra/Ideal.thy Tue Dec 30 11:10:01 2008 +0100 @@ -1,6 +1,5 @@ (* Title: HOL/Algebra/CIdeal.thy - Id: $Id$ Author: Stephan Hohe, TU Muenchen *) @@ -14,11 +13,11 @@ subsubsection {* General definition *} -locale ideal = additive_subgroup I R + ring R + +locale ideal = additive_subgroup I R + ring R for I and R (structure) + assumes I_l_closed: "\a \ I; x \ carrier R\ \ x \ a \ I" and I_r_closed: "\a \ I; x \ carrier R\ \ a \ x \ I" -interpretation ideal \ abelian_subgroup I R +sublocale ideal \ abelian_subgroup I R apply (intro abelian_subgroupI3 abelian_group.intro) apply (rule ideal.axioms, rule ideal_axioms) apply (rule abelian_group.axioms, rule ring.axioms, rule ideal.axioms, rule ideal_axioms) @@ -37,7 +36,7 @@ and I_r_closed: "\a x. \a \ I; x \ carrier R\ \ a \ x \ I" shows "ideal I R" proof - - interpret ring [R] by fact + interpret ring R by fact show ?thesis apply (intro ideal.intro ideal_axioms.intro additive_subgroupI) apply (rule a_subgroup) apply (rule is_ring) @@ -68,7 +67,7 @@ assumes generate: "\i \ carrier R. I = Idl {i}" shows "principalideal I R" proof - - interpret ideal [I R] by fact + interpret ideal I R by fact show ?thesis by (intro principalideal.intro principalideal_axioms.intro) (rule is_ideal, rule generate) qed @@ -89,7 +88,7 @@ and I_maximal: "\J. \ideal J R; I \ J; J \ carrier R\ \ J = I \ J = carrier R" shows "maximalideal I R" proof - - interpret ideal [I R] by fact + interpret ideal I R by fact show ?thesis by (intro maximalideal.intro maximalideal_axioms.intro) (rule is_ideal, rule I_notcarr, rule I_maximal) qed @@ -112,8 +111,8 @@ and I_prime: "\a b. \a \ carrier R; b \ carrier R; a \ b \ I\ \ a \ I \ b \ I" shows "primeideal I R" proof - - interpret ideal [I R] by fact - interpret cring [R] by fact + interpret ideal I R by fact + interpret cring R by fact show ?thesis by (intro primeideal.intro primeideal_axioms.intro) (rule is_ideal, rule is_cring, rule I_notcarr, rule I_prime) qed @@ -128,8 +127,8 @@ and I_prime: "\a b. \a \ carrier R; b \ carrier R; a \ b \ I\ \ a \ I \ b \ I" shows "primeideal I R" proof - - interpret additive_subgroup [I R] by fact - interpret cring [R] by fact + interpret additive_subgroup I R by fact + interpret cring R by fact show ?thesis apply (intro_locales) apply (intro ideal_axioms.intro) apply (erule (1) I_l_closed) @@ -207,8 +206,8 @@ assumes "ideal J R" shows "ideal (I \ J) R" proof - - interpret ideal [I R] by fact - interpret ideal [J R] by fact + interpret ideal I R by fact + interpret ideal J R by fact show ?thesis apply (intro idealI subgroup.intro) apply (rule is_ring) @@ -245,7 +244,7 @@ from notempty have "\I0. I0 \ S" by blast from this obtain I0 where I0S: "I0 \ S" by auto - interpret ideal ["I0" "R"] by (rule Sideals[OF I0S]) + interpret ideal I0 R by (rule Sideals[OF I0S]) from xI[OF I0S] have "x \ I0" . from this and a_subset show "x \ carrier R" by fast @@ -258,13 +257,13 @@ fix J assume JS: "J \ S" - interpret ideal ["J" "R"] by (rule Sideals[OF JS]) + interpret ideal J R by (rule Sideals[OF JS]) from xI[OF JS] and yI[OF JS] show "x \ y \ J" by (rule a_closed) next fix J assume JS: "J \ S" - interpret ideal ["J" "R"] by (rule Sideals[OF JS]) + interpret ideal J R by (rule Sideals[OF JS]) show "\ \ J" by simp next fix x @@ -273,7 +272,7 @@ fix J assume JS: "J \ S" - interpret ideal ["J" "R"] by (rule Sideals[OF JS]) + interpret ideal J R by (rule Sideals[OF JS]) from xI[OF JS] show "\ x \ J" by (rule a_inv_closed) @@ -285,7 +284,7 @@ fix J assume JS: "J \ S" - interpret ideal ["J" "R"] by (rule Sideals[OF JS]) + interpret ideal J R by (rule Sideals[OF JS]) from xI[OF JS] and ycarr show "y \ x \ J" by (rule I_l_closed) @@ -297,7 +296,7 @@ fix J assume JS: "J \ S" - interpret ideal ["J" "R"] by (rule Sideals[OF JS]) + interpret ideal J R by (rule Sideals[OF JS]) from xI[OF JS] and ycarr show "x \ y \ J" by (rule I_r_closed) @@ -443,7 +442,7 @@ lemma (in ring) genideal_one: "Idl {\} = carrier R" proof - - interpret ideal ["Idl {\}" "R"] by (rule genideal_ideal, fast intro: one_closed) + interpret ideal "Idl {\}" "R" by (rule genideal_ideal, fast intro: one_closed) show "Idl {\} = carrier R" apply (rule, rule a_subset) apply (simp add: one_imp_carrier genideal_self') @@ -533,7 +532,7 @@ assumes aJ: "a \ J" shows "PIdl a \ J" proof - - interpret ideal [J R] by fact + interpret ideal J R by fact show ?thesis unfolding cgenideal_def apply rule apply clarify @@ -580,7 +579,7 @@ shows "Idl (I \ J) = I <+> J" apply rule apply (rule ring.genideal_minimal) - apply (rule R.is_ring) + apply (rule is_ring) apply (rule add_ideals[OF idealI idealJ]) apply (rule) apply (simp add: set_add_defs) apply (elim disjE) defer 1 defer 1 @@ -660,7 +659,7 @@ assumes "cring R" shows "\x\I. I = carrier R #> x" proof - - interpret cring [R] by fact + interpret cring R by fact from generate obtain i where icarr: "i \ carrier R" @@ -693,7 +692,7 @@ assumes notprime: "\ primeideal I R" shows "carrier R = I \ (\a b. a \ carrier R \ b \ carrier R \ a \ b \ I \ a \ I \ b \ I)" proof (rule ccontr, clarsimp) - interpret cring [R] by fact + interpret cring R by fact assume InR: "carrier R \ I" and "\a. a \ carrier R \ (\b. a \ b \ I \ b \ carrier R \ a \ I \ b \ I)" hence I_prime: "\ a b. \a \ carrier R; b \ carrier R; a \ b \ I\ \ a \ I \ b \ I" by simp @@ -713,7 +712,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 @@ -726,13 +725,13 @@ apply (rule domain.intro, rule is_cring) apply (rule domain_axioms.intro) proof (rule ccontr, simp) - interpret primeideal ["{\}" "R"] by (rule pi) + interpret primeideal "{\}" "R" by (rule pi) assume "\ = \" hence "carrier R = {\}" by (rule one_zeroD) from this[symmetric] and I_notcarr show "False" by simp next - interpret primeideal ["{\}" "R"] by (rule pi) + interpret primeideal "{\}" "R" by (rule pi) fix a b assume ab: "a \ b = \" and carr: "a \ carrier R" "b \ carrier R" @@ -771,7 +770,7 @@ assumes acarr: "a \ carrier R" shows "ideal {x\carrier R. a \ x \ I} R" proof - - interpret cring [R] by fact + interpret cring R by fact show ?thesis apply (rule idealI) apply (rule cring.axioms[OF is_cring]) apply (rule subgroup.intro) @@ -812,7 +811,7 @@ assumes "maximalideal I R" shows "primeideal I R" proof - - interpret maximalideal [I R] by fact + interpret maximalideal I R by fact show ?thesis apply (rule ccontr) apply (rule primeidealCE) apply (rule is_cring) @@ -830,7 +829,7 @@ by fast def J \ "{x\carrier R. a \ x \ I}" - from R.is_cring and acarr + from is_cring and acarr have idealJ: "ideal J R" unfolding J_def by (rule helper_max_prime) have IsubJ: "I \ J" @@ -855,7 +854,7 @@ have "\ \ J" unfolding J_def by fast hence Jncarr: "J \ carrier R" by fast - interpret ideal ["J" "R"] by (rule idealJ) + interpret ideal J R by (rule idealJ) have "J = I \ J = carrier R" apply (intro I_maximal) @@ -932,7 +931,7 @@ fix I assume a: "I \ {I. ideal I R}" with this - interpret ideal ["I" "R"] by simp + interpret ideal I R by simp show "I \ {{\}, carrier R}" proof (cases "\a. a \ I - {\}") @@ -1019,7 +1018,7 @@ fix J assume Jn0: "J \ {\}" and idealJ: "ideal J R" - interpret ideal ["J" "R"] by (rule idealJ) + interpret ideal J R by (rule idealJ) have "{\} \ J" by (rule ccontr, simp) from zeromax and idealJ and this and a_subset have "J = {\} \ J = carrier R" by (rule maximalideal.I_maximal) diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/Algebra/IntRing.thy --- a/src/HOL/Algebra/IntRing.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/Algebra/IntRing.thy Tue Dec 30 11:10:01 2008 +0100 @@ -1,6 +1,5 @@ (* Title: HOL/Algebra/IntRing.thy - Id: $Id$ Author: Stephan Hohe, TU Muenchen *) @@ -97,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" @@ -105,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) @@ -117,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) } @@ -140,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) } @@ -165,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 - @@ -175,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) } @@ -188,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) @@ -204,8 +203,8 @@ "(True ==> PROP R) == PROP R" by simp_all -interpretation int (* FIXME [unfolded UNIV] *) : - partial_order ["(| carrier = UNIV::int set, eq = op =, le = op \ |)"] +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)" and "lless (| carrier = UNIV::int set, eq = op =, le = op \ |) x y = (x < y)" @@ -220,8 +219,8 @@ by (simp add: lless_def) auto qed -interpretation int (* FIXME [unfolded UNIV] *) : - lattice ["(| carrier = UNIV::int set, eq = op =, le = op \ |)"] +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" proof - @@ -233,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) @@ -246,8 +245,8 @@ done qed -interpretation int (* [unfolded UNIV] *) : - total_order ["(| carrier = UNIV::int set, eq = op =, le = op \ |)"] +interpretation int! (* [unfolded UNIV] *) : + total_order "(| carrier = UNIV::int set, eq = op =, le = op \ |)" proof qed clarsimp @@ -329,7 +328,7 @@ next assume "UNIV = {uu. EX x. uu = x * p}" from this obtain x - where "1 = x * p" by fast + where "1 = x * p" by best from this [symmetric] have "p * x = 1" by (subst zmult_commute) hence "\p * x\ = 1" by simp @@ -404,7 +403,7 @@ assumes zmods: "ZMod m a = ZMod m b" shows "a mod m = b mod m" proof - - interpret ideal ["Idl\<^bsub>\\<^esub> {m}" \] by (rule int.genideal_ideal, fast) + interpret ideal "Idl\<^bsub>\\<^esub> {m}" \ by (rule int.genideal_ideal, fast) from zmods have "b \ ZMod m a" unfolding ZMod_def @@ -428,7 +427,7 @@ lemma ZMod_mod: shows "ZMod m a = ZMod m (a mod m)" proof - - interpret ideal ["Idl\<^bsub>\\<^esub> {m}" \] by (rule int.genideal_ideal, fast) + interpret ideal "Idl\<^bsub>\\<^esub> {m}" \ by (rule int.genideal_ideal, fast) show ?thesis unfolding ZMod_def apply (rule a_repr_independence'[symmetric]) diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/Algebra/Lattice.thy --- a/src/HOL/Algebra/Lattice.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/Algebra/Lattice.thy Tue Dec 30 11:10:01 2008 +0100 @@ -1,6 +1,5 @@ (* Title: HOL/Algebra/Lattice.thy - Id: $Id$ Author: Clemens Ballarin, started 7 November 2003 Copyright: Clemens Ballarin @@ -16,7 +15,7 @@ record 'a gorder = "'a eq_object" + le :: "['a, 'a] => bool" (infixl "\\" 50) -locale weak_partial_order = equivalence L + +locale weak_partial_order = equivalence L for L (structure) + assumes le_refl [intro, simp]: "x \ carrier L ==> x \ x" and weak_le_anti_sym [intro]: @@ -920,7 +919,7 @@ text {* Total orders are lattices. *} -interpretation weak_total_order < weak_lattice +sublocale weak_total_order < weak: weak_lattice proof fix x y assume L: "x \ carrier L" "y \ carrier L" @@ -1126,14 +1125,14 @@ assumes sup_of_two_exists: "[| x \ carrier L; y \ carrier L |] ==> EX s. least L s (Upper L {x, y})" -interpretation upper_semilattice < weak_upper_semilattice +sublocale upper_semilattice < weak: weak_upper_semilattice proof qed (rule sup_of_two_exists) locale lower_semilattice = partial_order + assumes inf_of_two_exists: "[| x \ carrier L; y \ carrier L |] ==> EX s. greatest L s (Lower L {x, y})" -interpretation lower_semilattice < weak_lower_semilattice +sublocale lower_semilattice < weak: weak_lower_semilattice proof qed (rule inf_of_two_exists) locale lattice = upper_semilattice + lower_semilattice @@ -1184,7 +1183,7 @@ locale total_order = partial_order + assumes total_order_total: "[| x \ carrier L; y \ carrier L |] ==> x \ y | y \ x" -interpretation total_order < weak_total_order +sublocale total_order < weak: weak_total_order proof qed (rule total_order_total) text {* Introduction rule: the usual definition of total order *} @@ -1196,7 +1195,7 @@ text {* Total orders are lattices. *} -interpretation total_order < lattice +sublocale total_order < weak: lattice proof qed (auto intro: sup_of_two_exists inf_of_two_exists) @@ -1208,7 +1207,7 @@ and inf_exists: "[| A \ carrier L |] ==> EX i. greatest L i (Lower L A)" -interpretation complete_lattice < weak_complete_lattice +sublocale complete_lattice < weak: weak_complete_lattice proof qed (auto intro: sup_exists inf_exists) text {* Introduction rule: the usual definition of complete lattice *} diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/Algebra/Module.thy --- a/src/HOL/Algebra/Module.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/Algebra/Module.thy Tue Dec 30 11:10:01 2008 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Algebra/Module.thy - ID: $Id$ Author: Clemens Ballarin, started 15 April 2003 Copyright: Clemens Ballarin *) @@ -14,7 +13,7 @@ record ('a, 'b) module = "'b ring" + smult :: "['a, 'b] => 'b" (infixl "\\" 70) -locale module = cring R + abelian_group M + +locale module = R: cring + M: abelian_group M for M (structure) + assumes smult_closed [simp, intro]: "[| a \ carrier R; x \ carrier M |] ==> a \\<^bsub>M\<^esub> x \ carrier M" and smult_l_distr: @@ -29,7 +28,7 @@ and smult_one [simp]: "x \ carrier M ==> \ \\<^bsub>M\<^esub> x = x" -locale algebra = module R M + cring M + +locale algebra = module + cring M + assumes smult_assoc2: "[| a \ carrier R; x \ carrier M; y \ carrier M |] ==> (a \\<^bsub>M\<^esub> x) \\<^bsub>M\<^esub> y = a \\<^bsub>M\<^esub> (x \\<^bsub>M\<^esub> y)" diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/Algebra/QuotRing.thy --- a/src/HOL/Algebra/QuotRing.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/Algebra/QuotRing.thy Tue Dec 30 11:10:01 2008 +0100 @@ -1,6 +1,5 @@ (* Title: HOL/Algebra/QuotRing.thy - Id: $Id$ Author: Stephan Hohe *) @@ -158,7 +157,7 @@ assumes "cring R" shows "cring (R Quot I)" proof - - interpret cring [R] by fact + interpret cring R by fact show ?thesis apply (intro cring.intro comm_monoid.intro comm_monoid_axioms.intro) apply (rule quotient_is_ring) apply (rule ring.axioms[OF quotient_is_ring]) @@ -173,12 +172,12 @@ assumes "cring R" shows "ring_hom_cring R (R Quot I) (op +> I)" proof - - interpret cring [R] by fact + interpret cring R by fact show ?thesis apply (rule ring_hom_cringI) apply (rule rcos_ring_hom_ring) - apply (rule R.is_cring) + apply (rule is_cring) apply (rule quotient_is_cring) -apply (rule R.is_cring) +apply (rule is_cring) done qed @@ -244,7 +243,7 @@ assumes "cring R" shows "field (R Quot I)" proof - - interpret cring [R] by fact + interpret cring R by fact show ?thesis apply (intro cring.cring_fieldI2) apply (rule quotient_is_cring, rule is_cring) defer 1 diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/Algebra/Ring.thy --- a/src/HOL/Algebra/Ring.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/Algebra/Ring.thy Tue Dec 30 11:10:01 2008 +0100 @@ -1,6 +1,5 @@ (* Title: The algebraic hierarchy of rings - Id: $Id$ Author: Clemens Ballarin, started 9 December 1996 Copyright: Clemens Ballarin *) @@ -187,7 +186,7 @@ assumes cg: "comm_group \carrier = carrier G, mult = add G, one = zero G\" shows "abelian_group G" proof - - interpret comm_group ["\carrier = carrier G, mult = add G, one = zero G\"] + interpret comm_group "\carrier = carrier G, mult = add G, one = zero G\" by (rule cg) show "abelian_group G" .. qed @@ -360,7 +359,7 @@ subsection {* Rings: Basic Definitions *} -locale ring = abelian_group R + monoid R + +locale ring = abelian_group R + monoid R for R (structure) + assumes l_distr: "[| x \ carrier R; y \ carrier R; z \ carrier R |] ==> (x \ y) \ z = x \ z \ y \ z" and r_distr: "[| x \ carrier R; y \ carrier R; z \ carrier R |] @@ -585,8 +584,8 @@ assumes RS: "a \ carrier R" "b \ carrier R" "c \ carrier S" "d \ carrier S" shows "a \ \ (a \ \ b) = b & c \\<^bsub>S\<^esub> d = d \\<^bsub>S\<^esub> c" proof - - interpret ring [R] by fact - interpret cring [S] by fact + interpret ring R by fact + interpret cring S by fact ML_val {* Algebra.print_structures @{context} *} from RS show ?thesis by algebra qed @@ -597,7 +596,7 @@ assumes R: "a \ carrier R" "b \ carrier R" shows "a \ (a \ b) = b" proof - - interpret ring [R] by fact + interpret ring R by fact from R show ?thesis by algebra qed @@ -771,7 +770,8 @@ shows "h \ ring_hom R S ==> h \ = \\<^bsub>S\<^esub>" by (simp add: ring_hom_def) -locale ring_hom_cring = cring R + cring S + +locale ring_hom_cring = R: cring R + S: cring S + for R (structure) and S (structure) + fixes h assumes homh [simp, intro]: "h \ ring_hom R S" notes hom_closed [simp, intro] = ring_hom_closed [OF homh] diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/Algebra/RingHom.thy --- a/src/HOL/Algebra/RingHom.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/Algebra/RingHom.thy Tue Dec 30 11:10:01 2008 +0100 @@ -1,6 +1,5 @@ (* Title: HOL/Algebra/RingHom.thy - Id: $Id$ Author: Stephan Hohe, TU Muenchen *) @@ -11,15 +10,17 @@ section {* Homomorphisms of Non-Commutative Rings *} text {* Lifting existing lemmas in a @{text ring_hom_ring} locale *} -locale ring_hom_ring = ring R + ring S + var h + +locale ring_hom_ring = R: ring R + S: ring S + for R (structure) and S (structure) + + fixes h assumes homh: "h \ ring_hom R S" notes hom_mult [simp] = ring_hom_mult [OF homh] and hom_one [simp] = ring_hom_one [OF homh] -interpretation ring_hom_cring \ ring_hom_ring +sublocale ring_hom_cring \ ring: ring_hom_ring proof qed (rule homh) -interpretation ring_hom_ring \ abelian_group_hom R S +sublocale ring_hom_ring \ abelian_group: abelian_group_hom R S apply (rule abelian_group_homI) apply (rule R.is_abelian_group) apply (rule S.is_abelian_group) @@ -44,8 +45,8 @@ and compatible_one: "h \ = \\<^bsub>S\<^esub>" shows "ring_hom_ring R S h" proof - - interpret ring [R] by fact - interpret ring [S] by fact + interpret ring R by fact + interpret ring S by fact show ?thesis apply unfold_locales apply (unfold ring_hom_def, safe) apply (simp add: hom_closed Pi_def) @@ -60,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) @@ -76,9 +77,9 @@ and compatible_one: "h \ = \\<^bsub>S\<^esub>" 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 abelian_group_hom R S h 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) @@ -92,9 +93,9 @@ assumes "ring_hom_ring R S h" "cring R" "cring S" 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 ring_hom_ring R S h 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 @@ -124,7 +125,7 @@ and xrcos: "x \ a_kernel R S h +> a" shows "h x = h a" proof - - interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal) + interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal) from xrcos have "\i \ a_kernel R S h. x = i \ a" by (simp add: a_r_coset_defs) @@ -152,7 +153,7 @@ and hx: "h x = h a" shows "x \ a_kernel R S h +> a" proof - - interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal) + interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal) note carr = acarr xcarr note hcarr = acarr[THEN hom_closed] xcarr[THEN hom_closed] @@ -180,7 +181,7 @@ apply rule defer 1 apply clarsimp defer 1 proof - interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal) + interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal) fix x assume xrcos: "x \ a_kernel R S h +> a" @@ -193,7 +194,7 @@ from xcarr and this show "x \ {x \ carrier R. h x = h a}" by fast next - interpret ideal ["a_kernel R S h" "R"] by (rule kernel_is_ideal) + interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal) fix x assume xcarr: "x \ carrier R" diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/Algebra/UnivPoly.thy --- a/src/HOL/Algebra/UnivPoly.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/Algebra/UnivPoly.thy Tue Dec 30 11:10:01 2008 +0100 @@ -1,6 +1,5 @@ (* Title: HOL/Algebra/UnivPoly.thy - Id: $Id$ Author: Clemens Ballarin, started 9 December 1996 Copyright: Clemens Ballarin @@ -176,17 +175,17 @@ fixes R (structure) and P (structure) defines P_def: "P == UP R" -locale UP_ring = UP + ring R +locale UP_ring = UP + R: ring R -locale UP_cring = UP + cring R +locale UP_cring = UP + R: cring R -interpretation UP_cring < UP_ring - by (rule P_def) intro_locales +sublocale UP_cring < UP_ring + by intro_locales [1] (rule P_def) -locale UP_domain = UP + "domain" R +locale UP_domain = UP + R: "domain" R -interpretation UP_domain < UP_cring - by (rule P_def) intro_locales +sublocale UP_domain < UP_cring + by intro_locales [1] (rule P_def) context UP begin @@ -458,8 +457,8 @@ end -interpretation UP_ring < ring P using UP_ring . -interpretation UP_cring < cring P using UP_cring . +sublocale UP_ring < P: ring P using UP_ring . +sublocale UP_cring < P: cring P using UP_cring . subsection {* Polynomials Form an Algebra *} @@ -508,7 +507,7 @@ "algebra R P" by (auto intro!: algebraI R.cring UP_cring UP_smult_l_distr UP_smult_r_distr UP_smult_assoc1 UP_smult_assoc2) -interpretation UP_cring < algebra R P using UP_algebra . +sublocale UP_cring < algebra R P using UP_algebra . subsection {* Further Lemmas Involving Monomials *} @@ -1085,7 +1084,7 @@ Interpretation of theorems from @{term domain}. *} -interpretation UP_domain < "domain" P +sublocale UP_domain < "domain" P by intro_locales (rule domain.axioms UP_domain)+ @@ -1204,7 +1203,9 @@ text {* The universal property of the polynomial ring *} -locale UP_pre_univ_prop = ring_hom_cring R S h + UP_cring R P +locale UP_pre_univ_prop = ring_hom_cring + UP_cring + +(* FIXME print_locale ring_hom_cring fails *) locale UP_univ_prop = UP_pre_univ_prop + fixes s and Eval @@ -1350,7 +1351,7 @@ text {* Interpretation of ring homomorphism lemmas. *} -interpretation UP_univ_prop < ring_hom_cring P S Eval +sublocale UP_univ_prop < ring_hom_cring P S Eval apply (unfold Eval_def) apply intro_locales apply (rule ring_hom_cring.axioms) @@ -1391,7 +1392,7 @@ assumes R: "r \ carrier R" and S: "s \ carrier S" shows "eval R S h s (monom P r n) = h r \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n" proof - - interpret UP_univ_prop [R S h P s _] + interpret UP_univ_prop R S h P s "eval R S h s" using UP_pre_univ_prop_axioms P_def R S by (auto intro: UP_univ_prop.intro UP_univ_prop_axioms.intro) from R @@ -1428,8 +1429,8 @@ and P: "p \ carrier P" and S: "s \ carrier S" shows "Phi p = Psi p" proof - - interpret ring_hom_cring [P S Phi] by fact - interpret ring_hom_cring [P S Psi] by fact + interpret ring_hom_cring P S Phi by fact + interpret ring_hom_cring P S Psi by fact have "Phi p = Phi (\\<^bsub>P \<^esub>i \ {..deg R p}. monom P (coeff P p i) 0 \\<^bsub>P\<^esub> monom P \ 1 (^)\<^bsub>P\<^esub> i)" by (simp add: up_repr P monom_mult [THEN sym] monom_pow del: monom_mult) @@ -1772,17 +1773,17 @@ shows "eval R R id a (monom P \\<^bsub>R\<^esub> 1 \\<^bsub>P\<^esub> monom P a 0) = \" (is "eval R R id a ?g = _") proof - - interpret UP_pre_univ_prop [R R id P] proof qed simp + interpret UP_pre_univ_prop R R id proof qed simp have eval_ring_hom: "eval R R id a \ ring_hom P R" using eval_ring_hom [OF a] by simp - interpret ring_hom_cring [P R "eval R R id a"] proof qed (simp add: eval_ring_hom) + interpret ring_hom_cring P R "eval R R id a" proof qed (simp add: eval_ring_hom) have mon1_closed: "monom P \\<^bsub>R\<^esub> 1 \ carrier P" and mon0_closed: "monom P a 0 \ carrier P" and min_mon0_closed: "\\<^bsub>P\<^esub> monom P a 0 \ carrier P" using a R.a_inv_closed by auto have "eval R R id a ?g = eval R R id a (monom P \ 1) \ eval R R id a (monom P a 0)" unfolding P.minus_eq [OF mon1_closed mon0_closed] - unfolding R_S_h.hom_add [OF mon1_closed min_mon0_closed] - unfolding R_S_h.hom_a_inv [OF mon0_closed] + unfolding hom_add [OF mon1_closed min_mon0_closed] + unfolding hom_a_inv [OF mon0_closed] using R.minus_eq [symmetric] mon1_closed mon0_closed by auto also have "\ = a \ a" using eval_monom [OF R.one_closed a, of 1] using eval_monom [OF a a, of 0] using a by simp @@ -1819,7 +1820,7 @@ and deg_r_0: "deg R r = 0" shows "r = monom P (eval R R id a f) 0" proof - - interpret UP_pre_univ_prop [R R id P] proof qed simp + interpret UP_pre_univ_prop R R id P proof qed simp have eval_ring_hom: "eval R R id a \ ring_hom P R" using eval_ring_hom [OF a] by simp have "eval R R id a f = eval R R id a ?gq \\<^bsub>R\<^esub> eval R R id a r" @@ -1885,7 +1886,7 @@ "UP INTEG"} globally. *} -interpretation INTEG: UP_pre_univ_prop [INTEG INTEG id] +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 7dc7a75033ea -r ea97aa6aeba2 src/HOL/Complex.thy --- a/src/HOL/Complex.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/Complex.thy Tue Dec 30 11:10:01 2008 +0100 @@ -345,13 +345,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) @@ -513,7 +513,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 7dc7a75033ea -r ea97aa6aeba2 src/HOL/Dense_Linear_Order.thy --- a/src/HOL/Dense_Linear_Order.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/Dense_Linear_Order.thy Tue Dec 30 11:10:01 2008 +0100 @@ -301,7 +301,7 @@ text {* Linear order without upper bounds *} -locale linorder_stupid_syntax = linorder +class_locale linorder_stupid_syntax = linorder begin notation less_eq ("op \") and @@ -311,7 +311,7 @@ end -locale linorder_no_ub = linorder_stupid_syntax + +class_locale linorder_no_ub = linorder_stupid_syntax + assumes gt_ex: "\y. less x y" begin lemma ge_ex: "\y. x \ y" using gt_ex by auto @@ -360,7 +360,7 @@ text {* Linear order without upper bounds *} -locale linorder_no_lb = linorder_stupid_syntax + +class_locale linorder_no_lb = linorder_stupid_syntax + assumes lt_ex: "\y. less y x" begin lemma le_ex: "\y. y \ x" using lt_ex by auto @@ -407,12 +407,12 @@ end -locale constr_dense_linear_order = linorder_no_lb + linorder_no_ub + +class_locale constr_dense_linear_order = linorder_no_lb + linorder_no_ub + fixes between assumes between_less: "less x y \ less x (between x y) \ less (between x y) y" and between_same: "between x x = x" -interpretation constr_dense_linear_order < dense_linear_order +class_interpretation constr_dense_linear_order < dense_linear_order apply unfold_locales using gt_ex lt_ex between_less by (auto, rule_tac x="between x y" in exI, simp) @@ -635,7 +635,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 +class_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 7dc7a75033ea -r ea97aa6aeba2 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/Divides.thy Tue Dec 30 11:10:01 2008 +0100 @@ -639,7 +639,7 @@ text {* @{term "op dvd"} is a partial order *} -interpretation dvd: order ["op dvd" "\n m \ nat. n dvd m \ \ m dvd n"] +class_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 dvd_diff: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)" diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/Finite_Set.thy Tue Dec 30 11:10:01 2008 +0100 @@ -750,7 +750,7 @@ assumes "finite A" and "a \ A" shows "fold_image times g z (insert a A) = g a * (fold_image times g z A)" proof - - interpret I: fun_left_comm ["%x y. (g x) * y"] + interpret I: fun_left_comm "%x y. (g x) * y" by unfold_locales (simp add: mult_ac) show ?thesis using assms by(simp add:fold_image_def I.fold_insert) qed @@ -798,7 +798,7 @@ and hyp: "\x y. h (g x y) = times x (h y)" shows "h (fold g j w A) = fold times j (h w) A" proof - - interpret ab_semigroup_mult [g] by fact + class_interpret ab_semigroup_mult [g] by fact show ?thesis using fin hyp by (induct set: finite) simp_all qed *) @@ -873,7 +873,7 @@ subsection {* Generalized summation over a set *} -interpretation comm_monoid_add: comm_monoid_mult ["0::'a::comm_monoid_add" "op +"] +class_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" @@ -1760,7 +1760,7 @@ proof (induct rule: finite_induct) case empty then show ?case by simp next - interpret ab_semigroup_mult ["op Un"] + class_interpret ab_semigroup_mult ["op Un"] proof qed auto case insert then show ?case by simp @@ -1943,7 +1943,7 @@ assumes fold: "fold_graph times (b::'a) A y" and "b \ A" shows "fold_graph times z (insert b A) (z * y)" proof - - interpret fun_left_comm ["op *::'a \ 'a \ 'a"] by (rule fun_left_comm) + interpret fun_left_comm "op *::'a \ 'a \ 'a" by (rule fun_left_comm) from assms show ?thesis proof (induct rule: fold_graph.induct) case emptyI thus ?case by (force simp add: fold_insert_aux mult_commute) @@ -1983,7 +1983,7 @@ lemma fold1_eq_fold: assumes "finite A" "a \ A" shows "fold1 times (insert a A) = fold times a A" proof - - interpret fun_left_comm ["op *::'a \ 'a \ 'a"] by (rule fun_left_comm) + interpret fun_left_comm "op *::'a \ 'a \ 'a" by (rule fun_left_comm) from assms show ?thesis apply (simp add: fold1_def fold_def) apply (rule the_equality) @@ -2010,7 +2010,7 @@ assumes nonempty: "A \ {}" and A: "finite A" "x \ A" shows "fold1 times (insert x A) = x * fold1 times A" proof - - interpret fun_left_comm ["op *::'a \ 'a \ 'a"] by (rule fun_left_comm) + interpret fun_left_comm "op *::'a \ 'a \ 'a" by (rule fun_left_comm) from nonempty obtain a A' where "A = insert a A' & a ~: A'" by (auto simp add: nonempty_iff) with A show ?thesis @@ -2033,7 +2033,7 @@ assumes nonempty: "A \ {}" and A: "finite A" shows "fold1 times (insert x A) = x * fold1 times A" proof - - interpret fun_left_comm_idem ["op *::'a \ 'a \ 'a"] + interpret fun_left_comm_idem "op *::'a \ 'a \ 'a" by (rule fun_left_comm_idem) from nonempty obtain a A' where A': "A = insert a A' & a ~: A'" by (auto simp add: nonempty_iff) @@ -2198,7 +2198,7 @@ assumes "finite A" "A \ {}" shows "x \ fold1 inf A \ (\a\A. x \ a)" proof - - interpret ab_semigroup_idem_mult [inf] + class_interpret ab_semigroup_idem_mult [inf] by (rule ab_semigroup_idem_mult_inf) show ?thesis using assms by (induct rule: finite_ne_induct) simp_all qed @@ -2213,7 +2213,7 @@ proof (induct rule: finite_ne_induct) case singleton thus ?case by simp next - interpret ab_semigroup_idem_mult [inf] + class_interpret ab_semigroup_idem_mult [inf] by (rule ab_semigroup_idem_mult_inf) case (insert x F) from insert(5) have "a = x \ a \ F" by simp @@ -2288,7 +2288,7 @@ and "A \ {}" shows "sup x (\\<^bsub>fin\<^esub>A) = \\<^bsub>fin\<^esub>{sup x a|a. a \ A}" proof - - interpret ab_semigroup_idem_mult [inf] + class_interpret ab_semigroup_idem_mult [inf] by (rule ab_semigroup_idem_mult_inf) from assms show ?thesis by (simp add: Inf_fin_def image_def @@ -2303,7 +2303,7 @@ case singleton thus ?case by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def]) next - interpret ab_semigroup_idem_mult [inf] + class_interpret ab_semigroup_idem_mult [inf] by (rule ab_semigroup_idem_mult_inf) case (insert x A) have finB: "finite {sup x b |b. b \ B}" @@ -2333,7 +2333,7 @@ assumes "finite A" and "A \ {}" shows "inf x (\\<^bsub>fin\<^esub>A) = \\<^bsub>fin\<^esub>{inf x a|a. a \ A}" proof - - interpret ab_semigroup_idem_mult [sup] + class_interpret ab_semigroup_idem_mult [sup] by (rule ab_semigroup_idem_mult_sup) from assms show ?thesis by (simp add: Sup_fin_def image_def hom_fold1_commute [where h="inf x", OF inf_sup_distrib1]) @@ -2357,7 +2357,7 @@ thus ?thesis by(simp add: insert(1) B(1)) qed have ne: "{inf a b |a b. a \ A \ b \ B} \ {}" using insert B by blast - interpret ab_semigroup_idem_mult [sup] + class_interpret ab_semigroup_idem_mult [sup] by (rule ab_semigroup_idem_mult_sup) have "inf (\\<^bsub>fin\<^esub>(insert x A)) (\\<^bsub>fin\<^esub>B) = inf (sup x (\\<^bsub>fin\<^esub>A)) (\\<^bsub>fin\<^esub>B)" using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def]) @@ -2386,7 +2386,7 @@ assumes "finite A" and "A \ {}" shows "\\<^bsub>fin\<^esub>A = Inf A" proof - - interpret ab_semigroup_idem_mult [inf] + class_interpret ab_semigroup_idem_mult [inf] by (rule ab_semigroup_idem_mult_inf) from assms show ?thesis unfolding Inf_fin_def by (induct A set: finite) @@ -2397,7 +2397,7 @@ assumes "finite A" and "A \ {}" shows "\\<^bsub>fin\<^esub>A = Sup A" proof - - interpret ab_semigroup_idem_mult [sup] + class_interpret ab_semigroup_idem_mult [sup] by (rule ab_semigroup_idem_mult_sup) from assms show ?thesis unfolding Sup_fin_def by (induct A set: finite) @@ -2446,7 +2446,7 @@ assumes "finite A" and "A \ {}" shows "x < fold1 min A \ (\a\A. x < a)" proof - - interpret ab_semigroup_idem_mult [min] + class_interpret ab_semigroup_idem_mult [min] by (rule ab_semigroup_idem_mult_min) from assms show ?thesis by (induct rule: finite_ne_induct) @@ -2457,7 +2457,7 @@ assumes "finite A" and "A \ {}" shows "fold1 min A \ x \ (\a\A. a \ x)" proof - - interpret ab_semigroup_idem_mult [min] + class_interpret ab_semigroup_idem_mult [min] by (rule ab_semigroup_idem_mult_min) from assms show ?thesis by (induct rule: finite_ne_induct) @@ -2468,7 +2468,7 @@ assumes "finite A" and "A \ {}" shows "fold1 min A < x \ (\a\A. a < x)" proof - - interpret ab_semigroup_idem_mult [min] + class_interpret ab_semigroup_idem_mult [min] by (rule ab_semigroup_idem_mult_min) from assms show ?thesis by (induct rule: finite_ne_induct) @@ -2481,7 +2481,7 @@ proof cases assume "A = B" thus ?thesis by simp next - interpret ab_semigroup_idem_mult [min] + class_interpret ab_semigroup_idem_mult [min] by (rule ab_semigroup_idem_mult_min) assume "A \ B" have B: "B = A \ (B-A)" using `A \ B` by blast @@ -2515,7 +2515,7 @@ assumes "finite A" and "A \ {}" shows "Min (insert x A) = min x (Min A)" proof - - interpret ab_semigroup_idem_mult [min] + class_interpret ab_semigroup_idem_mult [min] by (rule ab_semigroup_idem_mult_min) from assms show ?thesis by (rule fold1_insert_idem_def [OF Min_def]) qed @@ -2524,7 +2524,7 @@ assumes "finite A" and "A \ {}" shows "Max (insert x A) = max x (Max A)" proof - - interpret ab_semigroup_idem_mult [max] + class_interpret ab_semigroup_idem_mult [max] by (rule ab_semigroup_idem_mult_max) from assms show ?thesis by (rule fold1_insert_idem_def [OF Max_def]) qed @@ -2533,7 +2533,7 @@ assumes "finite A" and "A \ {}" shows "Min A \ A" proof - - interpret ab_semigroup_idem_mult [min] + class_interpret ab_semigroup_idem_mult [min] by (rule ab_semigroup_idem_mult_min) from assms fold1_in show ?thesis by (fastsimp simp: Min_def min_def) qed @@ -2542,7 +2542,7 @@ assumes "finite A" and "A \ {}" shows "Max A \ A" proof - - interpret ab_semigroup_idem_mult [max] + class_interpret ab_semigroup_idem_mult [max] by (rule ab_semigroup_idem_mult_max) from assms fold1_in [of A] show ?thesis by (fastsimp simp: Max_def max_def) qed @@ -2551,7 +2551,7 @@ assumes "finite A" and "A \ {}" and "finite B" and "B \ {}" shows "Min (A \ B) = min (Min A) (Min B)" proof - - interpret ab_semigroup_idem_mult [min] + class_interpret ab_semigroup_idem_mult [min] by (rule ab_semigroup_idem_mult_min) from assms show ?thesis by (simp add: Min_def fold1_Un2) @@ -2561,7 +2561,7 @@ assumes "finite A" and "A \ {}" and "finite B" and "B \ {}" shows "Max (A \ B) = max (Max A) (Max B)" proof - - interpret ab_semigroup_idem_mult [max] + class_interpret ab_semigroup_idem_mult [max] by (rule ab_semigroup_idem_mult_max) from assms show ?thesis by (simp add: Max_def fold1_Un2) @@ -2572,7 +2572,7 @@ and "finite N" and "N \ {}" shows "h (Min N) = Min (h ` N)" proof - - interpret ab_semigroup_idem_mult [min] + class_interpret ab_semigroup_idem_mult [min] by (rule ab_semigroup_idem_mult_min) from assms show ?thesis by (simp add: Min_def hom_fold1_commute) @@ -2583,7 +2583,7 @@ and "finite N" and "N \ {}" shows "h (Max N) = Max (h ` N)" proof - - interpret ab_semigroup_idem_mult [max] + class_interpret ab_semigroup_idem_mult [max] by (rule ab_semigroup_idem_mult_max) from assms show ?thesis by (simp add: Max_def hom_fold1_commute [of h]) @@ -2593,7 +2593,7 @@ assumes "finite A" and "x \ A" shows "Min A \ x" proof - - interpret lower_semilattice ["op \" "op <" min] + class_interpret lower_semilattice ["op \" "op <" min] by (rule min_lattice) from assms show ?thesis by (simp add: Min_def fold1_belowI) qed @@ -2611,7 +2611,7 @@ assumes "finite A" and "A \ {}" shows "x \ Min A \ (\a\A. x \ a)" proof - - interpret lower_semilattice ["op \" "op <" min] + class_interpret lower_semilattice ["op \" "op <" min] by (rule min_lattice) from assms show ?thesis by (simp add: Min_def below_fold1_iff) qed @@ -2629,7 +2629,7 @@ assumes "finite A" and "A \ {}" shows "x < Min A \ (\a\A. x < a)" proof - - interpret lower_semilattice ["op \" "op <" min] + class_interpret lower_semilattice ["op \" "op <" min] by (rule min_lattice) from assms show ?thesis by (simp add: Min_def strict_below_fold1_iff) qed @@ -2639,7 +2639,7 @@ shows "Max A < x \ (\a\A. a < x)" proof - note Max = Max_def - interpret linorder ["op \" "op >"] + class_interpret linorder ["op \" "op >"] by (rule dual_linorder) from assms show ?thesis by (simp add: Max strict_below_fold1_iff [folded dual_max]) @@ -2649,7 +2649,7 @@ assumes "finite A" and "A \ {}" shows "Min A \ x \ (\a\A. a \ x)" proof - - interpret lower_semilattice ["op \" "op <" min] + class_interpret lower_semilattice ["op \" "op <" min] by (rule min_lattice) from assms show ?thesis by (simp add: Min_def fold1_below_iff) @@ -2660,7 +2660,7 @@ shows "x \ Max A \ (\a\A. x \ a)" proof - note Max = Max_def - interpret linorder ["op \" "op >"] + class_interpret linorder ["op \" "op >"] by (rule dual_linorder) from assms show ?thesis by (simp add: Max fold1_below_iff [folded dual_max]) @@ -2670,7 +2670,7 @@ assumes "finite A" and "A \ {}" shows "Min A < x \ (\a\A. a < x)" proof - - interpret lower_semilattice ["op \" "op <" min] + class_interpret lower_semilattice ["op \" "op <" min] by (rule min_lattice) from assms show ?thesis by (simp add: Min_def fold1_strict_below_iff) @@ -2681,7 +2681,7 @@ shows "x < Max A \ (\a\A. x < a)" proof - note Max = Max_def - interpret linorder ["op \" "op >"] + class_interpret linorder ["op \" "op >"] by (rule dual_linorder) from assms show ?thesis by (simp add: Max fold1_strict_below_iff [folded dual_max]) @@ -2691,7 +2691,7 @@ assumes "M \ N" and "M \ {}" and "finite N" shows "Min N \ Min M" proof - - interpret distrib_lattice ["op \" "op <" min max] + class_interpret distrib_lattice ["op \" "op <" min max] by (rule distrib_lattice_min_max) from assms show ?thesis by (simp add: Min_def fold1_antimono) qed @@ -2701,7 +2701,7 @@ shows "Max M \ Max N" proof - note Max = Max_def - interpret linorder ["op \" "op >"] + class_interpret linorder ["op \" "op >"] by (rule dual_linorder) from assms show ?thesis by (simp add: Max fold1_antimono [folded dual_max]) diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/FrechetDeriv.thy --- a/src/HOL/FrechetDeriv.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/FrechetDeriv.thy Tue Dec 30 11:10:01 2008 +0100 @@ -65,8 +65,8 @@ assumes "bounded_linear g" shows "bounded_linear (\x. f x + g x)" proof - - interpret f: bounded_linear [f] by fact - interpret g: bounded_linear [g] by fact + interpret f: bounded_linear f by fact + interpret g: bounded_linear g by fact show ?thesis apply (unfold_locales) apply (simp only: f.add g.add add_ac) apply (simp only: f.scaleR g.scaleR scaleR_right_distrib) @@ -124,7 +124,7 @@ assumes "bounded_linear f" shows "bounded_linear (\x. - f x)" proof - - interpret f: bounded_linear [f] by fact + interpret f: bounded_linear f by fact show ?thesis apply (unfold_locales) apply (simp add: f.add) apply (simp add: f.scaleR) @@ -151,7 +151,7 @@ assumes f: "FDERIV f x :> F" shows "isCont f x" proof - - from f interpret F: bounded_linear ["F"] by (rule FDERIV_bounded_linear) + from f interpret F: bounded_linear "F" by (rule FDERIV_bounded_linear) have "(\h. norm (f (x + h) - f x - F h) / norm h) -- 0 --> 0" by (rule FDERIV_D [OF f]) hence "(\h. norm (f (x + h) - f x - F h) / norm h * norm h) -- 0 --> 0" @@ -180,8 +180,8 @@ assumes "bounded_linear g" shows "bounded_linear (\x. f (g x))" proof - - interpret f: bounded_linear [f] by fact - interpret g: bounded_linear [g] by fact + interpret f: bounded_linear f by fact + interpret g: bounded_linear g by fact show ?thesis proof (unfold_locales) fix x y show "f (g (x + y)) = f (g x) + f (g y)" by (simp only: f.add g.add) @@ -223,8 +223,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 @@ -375,9 +375,9 @@ by (simp only: FDERIV_lemma) qed -lemmas FDERIV_mult = bounded_bilinear_locale.mult.prod.FDERIV +lemmas FDERIV_mult = mult.FDERIV -lemmas FDERIV_scaleR = bounded_bilinear_locale.scaleR.prod.FDERIV +lemmas FDERIV_scaleR = scaleR.FDERIV subsection {* Powers *} @@ -409,10 +409,10 @@ by (simp add: right_diff_distrib left_diff_distrib mult_assoc) lemmas bounded_linear_mult_const = - bounded_bilinear_locale.mult.prod.bounded_linear_left [THEN bounded_linear_compose] + mult.bounded_linear_left [THEN bounded_linear_compose] lemmas bounded_linear_const_mult = - bounded_bilinear_locale.mult.prod.bounded_linear_right [THEN bounded_linear_compose] + mult.bounded_linear_right [THEN bounded_linear_compose] lemma FDERIV_inverse: fixes x :: "'a::real_normed_div_algebra" @@ -492,7 +492,7 @@ fixes x :: "'a::real_normed_field" shows "FDERIV f x :> (\h. h * D) = (\h. (f (x + h) - f x) / h) -- 0 --> D" apply (unfold fderiv_def) - apply (simp add: bounded_bilinear_locale.mult.prod.bounded_linear_left) + apply (simp add: mult.bounded_linear_left) apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric]) apply (subst diff_divide_distrib) apply (subst times_divide_eq_left [symmetric]) diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/Groebner_Basis.thy --- a/src/HOL/Groebner_Basis.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/Groebner_Basis.thy Tue Dec 30 11:10:01 2008 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Groebner_Basis.thy - ID: $Id$ Author: Amine Chaieb, TU Muenchen *) @@ -164,8 +163,8 @@ end -interpretation class_semiring: gb_semiring - ["op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"] +interpretation class_semiring!: gb_semiring + "op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1" proof qed (auto simp add: ring_simps power_Suc) lemmas nat_arith = @@ -243,8 +242,8 @@ end -interpretation class_ring: gb_ring ["op +" "op *" "op ^" - "0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"] +interpretation class_ring!: gb_ring "op +" "op *" "op ^" + "0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus" proof qed simp_all @@ -344,8 +343,8 @@ thus "b = 0" by blast qed -interpretation class_ringb: ringb - ["op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus"] +interpretation class_ringb!: ringb + "op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus" proof(unfold_locales, simp add: ring_simps power_Suc, auto) fix w x y z ::"'a::{idom,recpower,number_ring}" assume p: "w * y + x * z = w * z + x * y" and ynz: "y \ z" @@ -360,8 +359,8 @@ declaration {* normalizer_funs @{thm class_ringb.ringb_axioms'} *} -interpretation natgb: semiringb - ["op +" "op *" "op ^" "0::nat" "1"] +interpretation natgb!: semiringb + "op +" "op *" "op ^" "0::nat" "1" proof (unfold_locales, simp add: ring_simps power_Suc) fix w x y z ::"nat" { assume p: "w * y + x * z = w * z + x * y" and ynz: "y \ z" @@ -465,8 +464,8 @@ subsection{* Groebner Bases for fields *} -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) +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 lemma divide_Numeral0: "(x::'a::{field,number_ring, division_by_zero}) / Numeral0 = 0" diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/HahnBanach/Bounds.thy --- a/src/HOL/HahnBanach/Bounds.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/HahnBanach/Bounds.thy Tue Dec 30 11:10:01 2008 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Real/HahnBanach/Bounds.thy - ID: $Id$ Author: Gertrud Bauer, TU Munich *) @@ -27,7 +26,7 @@ assumes "lub A x" shows "\A = (x::'a::order)" proof - - interpret lub [A x] by fact + interpret lub A x by fact show ?thesis proof (unfold the_lub_def) from `lub A x` show "The (lub A) = x" diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/HahnBanach/FunctionNorm.thy --- a/src/HOL/HahnBanach/FunctionNorm.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/HahnBanach/FunctionNorm.thy Tue Dec 30 11:10:01 2008 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Real/HahnBanach/FunctionNorm.thy - ID: $Id$ Author: Gertrud Bauer, TU Munich *) @@ -22,7 +21,7 @@ linear forms: *} -locale continuous = var V + norm_syntax + linearform + +locale continuous = var_V + norm_syntax + linearform + assumes bounded: "\c. \x \ V. \f x\ \ c * \x\" declare continuous.intro [intro?] continuous_axioms.intro [intro?] @@ -91,7 +90,7 @@ assumes "continuous V norm f" shows "lub (B V f) (\f\\V)" proof - - interpret continuous [V norm f] by fact + interpret continuous V norm f by fact txt {* The existence of the supremum is shown using the completeness of the reals. Completeness means, that every non-empty bounded set of reals has a supremum. *} @@ -159,7 +158,7 @@ assumes b: "b \ B V f" shows "b \ \f\\V" proof - - interpret continuous [V norm f] by fact + interpret continuous V norm f by fact have "lub (B V f) (\f\\V)" using `continuous V norm f` by (rule fn_norm_works) from this and b show ?thesis .. @@ -170,7 +169,7 @@ assumes b: "\b. b \ B V f \ b \ y" shows "\f\\V \ y" proof - - interpret continuous [V norm f] by fact + interpret continuous V norm f by fact have "lub (B V f) (\f\\V)" using `continuous V norm f` by (rule fn_norm_works) from this and b show ?thesis .. @@ -182,7 +181,7 @@ assumes "continuous V norm f" shows "0 \ \f\\V" proof - - interpret continuous [V norm f] by fact + interpret continuous V norm f by fact txt {* The function norm is defined as the supremum of @{text B}. So it is @{text "\ 0"} if all elements in @{text B} are @{text "\ 0"}, provided the supremum exists and @{text B} is not empty. *} @@ -204,8 +203,8 @@ assumes x: "x \ V" shows "\f x\ \ \f\\V * \x\" proof - - interpret continuous [V norm f] by fact - interpret linearform [V f] . + interpret continuous V norm f by fact + interpret linearform V f . show ?thesis proof cases assume "x = 0" @@ -246,7 +245,7 @@ assumes ineq: "\x \ V. \f x\ \ c * \x\" and ge: "0 \ c" shows "\f\\V \ c" proof - - interpret continuous [V norm f] by fact + interpret continuous V norm f by fact show ?thesis proof (rule fn_norm_leastB [folded B_def fn_norm_def]) fix b assume b: "b \ B V f" diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/HahnBanach/HahnBanach.thy --- a/src/HOL/HahnBanach/HahnBanach.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/HahnBanach/HahnBanach.thy Tue Dec 30 11:10:01 2008 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Real/HahnBanach/HahnBanach.thy - ID: $Id$ Author: Gertrud Bauer, TU Munich *) @@ -63,10 +62,10 @@ -- {* and @{text f} a linear form on @{text F} such that @{text f} is bounded by @{text p}, *} -- {* then @{text f} can be extended to a linear form @{text h} on @{text E} in a norm-preserving way. \skp *} proof - - interpret vectorspace [E] by fact - interpret subspace [F E] by fact - interpret seminorm [E p] by fact - interpret linearform [F f] by fact + interpret vectorspace E by fact + interpret subspace F E by fact + interpret seminorm E p by fact + interpret linearform F f by fact def M \ "norm_pres_extensions E p F f" then have M: "M = \" by (simp only:) from E have F: "vectorspace F" .. @@ -322,10 +321,10 @@ \ (\x \ F. g x = f x) \ (\x \ E. \g x\ \ p x)" proof - - interpret vectorspace [E] by fact - interpret subspace [F E] by fact - interpret linearform [F f] by fact - interpret seminorm [E p] by fact + interpret vectorspace E by fact + interpret subspace F E by fact + interpret linearform F f by fact + interpret seminorm E p by fact have "\g. linearform E g \ (\x \ F. g x = f x) \ (\x \ E. g x \ p x)" using E FE sn lf proof (rule HahnBanach) @@ -363,12 +362,12 @@ \ (\x \ F. g x = f x) \ \g\\E = \f\\F" proof - - interpret normed_vectorspace [E norm] by fact - interpret normed_vectorspace_with_fn_norm [E norm B fn_norm] + interpret normed_vectorspace E norm by fact + interpret normed_vectorspace_with_fn_norm E norm B fn_norm by (auto simp: B_def fn_norm_def) intro_locales - interpret subspace [F E] by fact - interpret linearform [F f] by fact - interpret continuous [F norm f] by fact + interpret subspace F E by fact + interpret linearform F f by fact + interpret continuous F norm f by fact have E: "vectorspace E" by intro_locales have F: "vectorspace F" by rule intro_locales have F_norm: "normed_vectorspace F norm" diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/HahnBanach/HahnBanachExtLemmas.thy --- a/src/HOL/HahnBanach/HahnBanachExtLemmas.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/HahnBanach/HahnBanachExtLemmas.thy Tue Dec 30 11:10:01 2008 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Real/HahnBanach/HahnBanachExtLemmas.thy - ID: $Id$ Author: Gertrud Bauer, TU Munich *) @@ -46,7 +45,7 @@ assumes r: "\u v. u \ F \ v \ F \ a u \ b v" shows "\xi::real. \y \ F. a y \ xi \ xi \ b y" proof - - interpret vectorspace [F] by fact + interpret vectorspace F by fact txt {* From the completeness of the reals follows: The set @{text "S = {a u. u \ F}"} has a supremum, if it is non-empty and has an upper bound. *} @@ -98,8 +97,8 @@ assumes E: "vectorspace E" shows "linearform H' h'" proof - - interpret linearform [H h] by fact - interpret vectorspace [E] by fact + interpret linearform H h by fact + interpret vectorspace E by fact show ?thesis proof note E = `vectorspace E` @@ -203,10 +202,10 @@ and a': "\y \ H. - p (y + x0) - h y \ xi \ xi \ p (y + x0) - h y" shows "\x \ H'. h' x \ p x" proof - - interpret vectorspace [E] by fact - interpret subspace [H E] by fact - interpret seminorm [E p] by fact - interpret linearform [H h] by fact + interpret vectorspace E by fact + interpret subspace H E by fact + interpret seminorm E p by fact + interpret linearform H h by fact show ?thesis proof fix x assume x': "x \ H'" diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/HahnBanach/HahnBanachSupLemmas.thy --- a/src/HOL/HahnBanach/HahnBanachSupLemmas.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/HahnBanach/HahnBanachSupLemmas.thy Tue Dec 30 11:10:01 2008 +0100 @@ -405,10 +405,10 @@ and "linearform H h" shows "(\x \ H. \h x\ \ p x) = (\x \ H. h x \ p x)" (is "?L = ?R") proof - interpret subspace [H E] by fact - interpret vectorspace [E] by fact - interpret seminorm [E p] by fact - interpret linearform [H h] by fact + interpret subspace H E by fact + interpret vectorspace E by fact + interpret seminorm E p by fact + interpret linearform H h by fact have H: "vectorspace H" using `vectorspace E` .. { assume l: ?L diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/HahnBanach/Linearform.thy --- a/src/HOL/HahnBanach/Linearform.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/HahnBanach/Linearform.thy Tue Dec 30 11:10:01 2008 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Real/HahnBanach/Linearform.thy - ID: $Id$ Author: Gertrud Bauer, TU Munich *) @@ -14,8 +13,8 @@ that is additive and multiplicative. *} -locale linearform = var V + var f + - constrains V :: "'a\{minus, plus, zero, uminus} set" +locale linearform = + fixes V :: "'a\{minus, plus, zero, uminus} set" and f assumes add [iff]: "x \ V \ y \ V \ f (x + y) = f x + f y" and mult [iff]: "x \ V \ f (a \ x) = a * f x" @@ -25,7 +24,7 @@ assumes "vectorspace V" shows "x \ V \ f (- x) = - f x" proof - - interpret vectorspace [V] by fact + interpret vectorspace V by fact assume x: "x \ V" then have "f (- x) = f ((- 1) \ x)" by (simp add: negate_eq1) also from x have "\ = (- 1) * (f x)" by (rule mult) @@ -37,7 +36,7 @@ assumes "vectorspace V" shows "x \ V \ y \ V \ f (x - y) = f x - f y" proof - - interpret vectorspace [V] by fact + interpret vectorspace V by fact assume x: "x \ V" and y: "y \ V" then have "x - y = x + - y" by (rule diff_eq1) also have "f \ = f x + f (- y)" by (rule add) (simp_all add: x y) @@ -51,7 +50,7 @@ assumes "vectorspace V" shows "f 0 = 0" proof - - interpret vectorspace [V] by fact + interpret vectorspace V by fact have "f 0 = f (0 - 0)" by simp also have "\ = f 0 - f 0" using `vectorspace V` by (rule diff) simp_all also have "\ = 0" by simp diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/HahnBanach/NormedSpace.thy --- a/src/HOL/HahnBanach/NormedSpace.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/HahnBanach/NormedSpace.thy Tue Dec 30 11:10:01 2008 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Real/HahnBanach/NormedSpace.thy - ID: $Id$ Author: Gertrud Bauer, TU Munich *) @@ -20,7 +19,7 @@ locale norm_syntax = fixes norm :: "'a \ real" ("\_\") -locale seminorm = var V + norm_syntax + +locale seminorm = var_V + norm_syntax + constrains V :: "'a\{minus, plus, zero, uminus} set" assumes ge_zero [iff?]: "x \ V \ 0 \ \x\" and abs_homogenous [iff?]: "x \ V \ \a \ x\ = \a\ * \x\" @@ -32,7 +31,7 @@ assumes "vectorspace V" shows "x \ V \ y \ V \ \x - y\ \ \x\ + \y\" proof - - interpret vectorspace [V] by fact + interpret vectorspace V by fact assume x: "x \ V" and y: "y \ V" then have "x - y = x + - 1 \ y" by (simp add: diff_eq2 negate_eq2a) @@ -48,7 +47,7 @@ assumes "vectorspace V" shows "x \ V \ \- x\ = \x\" proof - - interpret vectorspace [V] by fact + interpret vectorspace V by fact assume x: "x \ V" then have "- x = - 1 \ x" by (simp only: negate_eq1) also from x have "\\\ = \- 1\ * \x\" @@ -103,8 +102,8 @@ assumes "subspace F E" "normed_vectorspace E norm" shows "normed_vectorspace F norm" proof - - interpret subspace [F E] by fact - interpret normed_vectorspace [E norm] by fact + interpret subspace F E by fact + interpret normed_vectorspace E norm by fact show ?thesis proof show "vectorspace F" by (rule vectorspace) unfold_locales diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/HahnBanach/Subspace.thy --- a/src/HOL/HahnBanach/Subspace.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/HahnBanach/Subspace.thy Tue Dec 30 11:10:01 2008 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Real/HahnBanach/Subspace.thy - ID: $Id$ Author: Gertrud Bauer, TU Munich *) @@ -17,8 +16,8 @@ and scalar multiplication. *} -locale subspace = var U + var V + - constrains U :: "'a\{minus, plus, zero, uminus} set" +locale subspace = + fixes U :: "'a\{minus, plus, zero, uminus} set" and V assumes non_empty [iff, intro]: "U \ {}" and subset [iff]: "U \ V" and add_closed [iff]: "x \ U \ y \ U \ x + y \ U" @@ -46,7 +45,7 @@ assumes x: "x \ U" and y: "y \ U" shows "x - y \ U" proof - - interpret vectorspace [V] by fact + interpret vectorspace V by fact from x y show ?thesis by (simp add: diff_eq1 negate_eq1) qed @@ -60,11 +59,11 @@ assumes "vectorspace V" shows "0 \ U" proof - - interpret vectorspace [V] by fact - have "U \ {}" by (rule U_V.non_empty) + 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 - also from `vectorspace V` x x have "\ \ U" by (rule U_V.diff_closed) + also from `vectorspace V` x x have "\ \ U" by (rule diff_closed) finally show ?thesis . qed @@ -73,7 +72,7 @@ assumes x: "x \ U" shows "- x \ U" proof - - interpret vectorspace [V] by fact + interpret vectorspace V by fact from x show ?thesis by (simp add: negate_eq1) qed @@ -83,7 +82,7 @@ assumes "vectorspace V" shows "vectorspace U" proof - - interpret vectorspace [V] by fact + interpret vectorspace V by fact show ?thesis proof show "U \ {}" .. @@ -255,8 +254,8 @@ assumes "vectorspace U" "vectorspace V" shows "U \ U + V" proof - - interpret vectorspace [U] by fact - interpret vectorspace [V] by fact + interpret vectorspace U by fact + interpret vectorspace V by fact show ?thesis proof show "U \ {}" .. @@ -279,9 +278,9 @@ assumes "subspace U E" "vectorspace E" "subspace V E" shows "U + V \ E" proof - - interpret subspace [U E] by fact - interpret vectorspace [E] by fact - interpret subspace [V E] by fact + interpret subspace U E by fact + interpret vectorspace E by fact + interpret subspace V E by fact show ?thesis proof have "0 \ U + V" @@ -346,9 +345,9 @@ and sum: "u1 + v1 = u2 + v2" shows "u1 = u2 \ v1 = v2" proof - - interpret vectorspace [E] by fact - interpret subspace [U E] by fact - interpret subspace [V E] by fact + interpret vectorspace E by fact + interpret subspace U E by fact + interpret subspace V E by fact show ?thesis proof have U: "vectorspace U" (* FIXME: use interpret *) @@ -395,8 +394,8 @@ and eq: "y1 + a1 \ x' = y2 + a2 \ x'" shows "y1 = y2 \ a1 = a2" proof - - interpret vectorspace [E] by fact - interpret subspace [H E] by fact + interpret vectorspace E by fact + interpret subspace H E by fact show ?thesis proof have c: "y1 = y2 \ a1 \ x' = a2 \ x'" @@ -451,8 +450,8 @@ and x': "x' \ H" "x' \ E" "x' \ 0" shows "(SOME (y, a). t = y + a \ x' \ y \ H) = (t, 0)" proof - - interpret vectorspace [E] by fact - interpret subspace [H E] by fact + interpret vectorspace E by fact + interpret subspace H E by fact show ?thesis proof (rule, simp_all only: split_paired_all split_conv) from t x' show "t = t + 0 \ x' \ t \ H" by simp @@ -483,8 +482,8 @@ and x': "x' \ H" "x' \ E" "x' \ 0" shows "h' x = h y + a * xi" proof - - interpret vectorspace [E] by fact - interpret subspace [H E] by fact + interpret vectorspace E by fact + interpret subspace H E by fact from x y x' have "x \ H + lin x'" by auto have "\!p. (\(y, a). x = y + a \ x' \ y \ H) p" (is "\!p. ?P p") proof (rule ex_ex1I) diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/HahnBanach/VectorSpace.thy --- a/src/HOL/HahnBanach/VectorSpace.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/HahnBanach/VectorSpace.thy Tue Dec 30 11:10:01 2008 +0100 @@ -39,7 +39,9 @@ the neutral element of scalar multiplication. *} -locale vectorspace = var V + +locale var_V = fixes V + +locale vectorspace = var_V + assumes non_empty [iff, intro?]: "V \ {}" and add_closed [iff]: "x \ V \ y \ V \ x + y \ V" and mult_closed [iff]: "x \ V \ a \ x \ V" diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/HahnBanach/ZornLemma.thy --- a/src/HOL/HahnBanach/ZornLemma.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/HahnBanach/ZornLemma.thy Tue Dec 30 11:10:01 2008 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Real/HahnBanach/ZornLemma.thy - ID: $Id$ Author: Gertrud Bauer, TU Munich *) diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/Lattices.thy --- a/src/HOL/Lattices.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/Lattices.thy Tue Dec 30 11:10:01 2008 +0100 @@ -300,7 +300,7 @@ by auto qed (auto simp add: min_def max_def not_le less_imp_le) -interpretation min_max: +class_interpretation min_max: distrib_lattice ["op \ \ 'a\linorder \ 'a \ bool" "op <" min max] by (rule distrib_lattice_min_max) diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/Library/Multiset.thy Tue Dec 30 11:10:01 2008 +0100 @@ -1080,15 +1080,15 @@ apply simp done -interpretation mset_order: order ["op \#" "op <#"] +class_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: +class_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: +class_interpretation mset_order_semigroup_cancel: pordered_ab_semigroup_add_imp_le ["op +" "op \#" "op <#"] proof qed simp @@ -1404,7 +1404,7 @@ assumes "left_commutative g" shows "(\x y. h (g x y) = f x (h y)) \ h (fold_mset g w A) = fold_mset f (h w) A" (is "PROP ?P") proof - - interpret left_commutative [g] by fact + interpret left_commutative g by fact show "PROP ?P" by (induct A) auto qed @@ -1436,7 +1436,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 7dc7a75033ea -r ea97aa6aeba2 src/HOL/Library/SetsAndFunctions.thy --- a/src/HOL/Library/SetsAndFunctions.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/Library/SetsAndFunctions.thy Tue Dec 30 11:10:01 2008 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Library/SetsAndFunctions.thy - ID: $Id$ Author: Jeremy Avigad and Kevin Donnelly *) @@ -108,26 +107,26 @@ apply simp done -interpretation set_semigroup_add: semigroup_add ["op \ :: ('a::semigroup_add) set => 'a set => 'a set"] +class_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"] +class_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"] +class_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"] +class_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 7dc7a75033ea -r ea97aa6aeba2 src/HOL/List.thy --- a/src/HOL/List.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/List.thy Tue Dec 30 11:10:01 2008 +0100 @@ -548,9 +548,9 @@ lemma append_Nil2 [simp]: "xs @ [] = xs" by (induct xs) auto -interpretation semigroup_append: semigroup_add ["op @"] +class_interpretation semigroup_append: semigroup_add ["op @"] proof qed simp -interpretation monoid_append: monoid_add ["[]" "op @"] +class_interpretation monoid_append: monoid_add ["[]" "op @"] proof qed simp+ lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \ ys = [])" diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/MicroJava/BV/Kildall.thy --- a/src/HOL/MicroJava/BV/Kildall.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/MicroJava/BV/Kildall.thy Tue Dec 30 11:10:01 2008 +0100 @@ -321,7 +321,7 @@ ss <[r] merges f qs ss \ merges f qs ss = ss \ {q. \t. (q,t)\set qs \ t +_f ss!q \ ss!q} Un (w-{p}) < w" (is "PROP ?P") proof - - interpret Semilat [A r f] using assms by (rule Semilat.intro) + interpret Semilat A r f using assms by (rule Semilat.intro) show "PROP ?P" apply(insert semilat) apply (unfold lesssub_def) apply (simp (no_asm_simp) add: merges_incr) @@ -351,7 +351,7 @@ (\ts\list n A. ss0 <=[r] ts \ stables r step ts \ ss' <=[r] ts)" (is "PROP ?P") proof - - interpret Semilat [A r f] using assms by (rule Semilat.intro) + interpret Semilat A r f using assms by (rule Semilat.intro) show "PROP ?P" apply(insert semilat) apply (unfold iter_def stables_def) apply (rule_tac P = "%(ss,w). @@ -457,7 +457,7 @@ kildall r f step ss0 <=[r] ts)" (is "PROP ?P") proof - - interpret Semilat [A r f] using assms by (rule Semilat.intro) + interpret Semilat A r f using assms by (rule Semilat.intro) show "PROP ?P" apply (unfold kildall_def) apply(case_tac "iter f step ss0 (unstables r step ss0)") @@ -474,7 +474,7 @@ \ is_bcv r T step n A (kildall r f step)" (is "PROP ?P") proof - - interpret Semilat [A r f] using assms by (rule Semilat.intro) + interpret Semilat A r f using assms by (rule Semilat.intro) show "PROP ?P" apply(unfold is_bcv_def wt_step_def) apply(insert semilat kildall_properties[of A]) diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/MicroJava/BV/LBVComplete.thy --- a/src/HOL/MicroJava/BV/LBVComplete.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/MicroJava/BV/LBVComplete.thy Tue Dec 30 11:10:01 2008 +0100 @@ -197,7 +197,7 @@ have "merge c pc ?step (c!Suc pc) = (if \(pc',s')\set ?step. pc'\pc+1 \ s' <=_r c!pc' then map snd [(p',t') \ ?step.p'=pc+1] ++_f c!Suc pc - else \)" unfolding merge_def by (rule lbv.merge_def [OF lbvc.axioms(1), OF lbvc_axioms]) + else \)" unfolding mrg_def by (rule lbv.merge_def [OF lbvc.axioms(1), OF lbvc_axioms]) moreover { fix pc' s' assume s': "(pc', s') \ set ?step" and suc_pc: "pc' \ pc+1" with less have "s' <=_r \!pc'" by auto diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/MicroJava/BV/Listn.thy --- a/src/HOL/MicroJava/BV/Listn.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/MicroJava/BV/Listn.thy Tue Dec 30 11:10:01 2008 +0100 @@ -380,7 +380,7 @@ lemma Listn_sl_aux: assumes "semilat (A, r, f)" shows "semilat (Listn.sl n (A,r,f))" proof - - interpret Semilat [A r f] using assms by (rule Semilat.intro) + interpret Semilat A r f using assms by (rule Semilat.intro) show ?thesis apply (unfold Listn.sl_def) apply (simp (no_asm) only: semilat_Def split_conv) diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/MicroJava/BV/SemilatAlg.thy --- a/src/HOL/MicroJava/BV/SemilatAlg.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/MicroJava/BV/SemilatAlg.thy Tue Dec 30 11:10:01 2008 +0100 @@ -67,7 +67,7 @@ lemma plusplus_closed: assumes "semilat (A, r, f)" shows "\y. \ set x \ A; y \ A\ \ x ++_f y \ A" (is "PROP ?P") proof - - interpret Semilat [A r f] using assms by (rule Semilat.intro) + interpret Semilat A r f using assms by (rule Semilat.intro) show "PROP ?P" proof (induct x) show "\y. y \ A \ [] ++_f y \ A" by simp fix y x xs @@ -164,7 +164,7 @@ shows "\\(p,s) \ set S. s \ A; y \ A; (a,b) \ set S\ \ b <=_r map snd [(p', t')\S. p' = a] ++_f y" proof - - interpret Semilat [A r f] using assms by (rule Semilat.intro) + interpret Semilat A r f using assms by (rule Semilat.intro) let "b <=_r ?map ++_f y" = ?thesis diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/NSA/StarDef.thy --- a/src/HOL/NSA/StarDef.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/NSA/StarDef.thy Tue Dec 30 11:10:01 2008 +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 7dc7a75033ea -r ea97aa6aeba2 src/HOL/ROOT.ML diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/RealVector.thy --- a/src/HOL/RealVector.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/RealVector.thy Tue Dec 30 11:10:01 2008 +0100 @@ -60,7 +60,7 @@ and scale_minus_left [simp]: "scale (- a) x = - (scale a x)" and scale_left_diff_distrib: "scale (a - b) x = scale a x - scale b x" proof - - interpret s: additive ["\a. scale a x"] + interpret s: additive "\a. scale a x" proof qed (rule scale_left_distrib) show "scale 0 x = 0" by (rule s.zero) show "scale (- a) x = - (scale a x)" by (rule s.minus) @@ -71,7 +71,7 @@ and scale_minus_right [simp]: "scale a (- x) = - (scale a x)" and scale_right_diff_distrib: "scale a (x - y) = scale a x - scale a y" proof - - interpret s: additive ["\x. scale a x"] + interpret s: additive "\x. scale a x" proof qed (rule scale_right_distrib) show "scale a 0 = 0" by (rule s.zero) show "scale a (- x) = - (scale a x)" by (rule s.minus) @@ -151,8 +151,8 @@ and scaleR_scaleR [simp]: "scaleR a (scaleR b x) = scaleR (a * b) x" and scaleR_one [simp]: "scaleR 1 x = x" -interpretation real_vector: - vector_space ["scaleR :: real \ 'a \ 'a::real_vector"] +interpretation real_vector!: + vector_space "scaleR :: real \ 'a \ 'a::real_vector" apply unfold_locales apply (rule scaleR_right_distrib) apply (rule scaleR_left_distrib) @@ -195,10 +195,10 @@ apply (rule mult_left_commute) done -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: @@ -796,8 +796,8 @@ end -interpretation mult: - bounded_bilinear ["op * :: 'a \ 'a \ 'a::real_normed_algebra"] +interpretation mult!: + bounded_bilinear "op * :: 'a \ 'a \ 'a::real_normed_algebra" apply (rule bounded_bilinear.intro) apply (rule left_distrib) apply (rule right_distrib) @@ -807,19 +807,19 @@ apply (simp add: norm_mult_ineq) done -interpretation mult_left: - bounded_linear ["(\x::'a::real_normed_algebra. x * y)"] +interpretation mult_left!: + bounded_linear "(\x::'a::real_normed_algebra. x * y)" by (rule mult.bounded_linear_left) -interpretation mult_right: - bounded_linear ["(\y::'a::real_normed_algebra. x * y)"] +interpretation mult_right!: + bounded_linear "(\y::'a::real_normed_algebra. x * y)" by (rule mult.bounded_linear_right) -interpretation divide: - bounded_linear ["(\x::'a::real_normed_field. x / y)"] +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) @@ -829,13 +829,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 7dc7a75033ea -r ea97aa6aeba2 src/HOL/Statespace/StateSpaceEx.thy --- a/src/HOL/Statespace/StateSpaceEx.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/Statespace/StateSpaceEx.thy Tue Dec 30 11:10:01 2008 +0100 @@ -30,6 +30,10 @@ n::nat b::bool +print_locale vars_namespace +print_locale vars_valuetypes +print_locale vars + text {* \noindent This resembles a \isacommand{record} definition, but introduces sophisticated locale infrastructure instead of HOL type schemes. The resulting context @@ -37,7 +41,7 @@ projection~/ injection functions that convert from abstract values to @{typ "nat"} and @{text "bool"}. The logical content of the locale is: *} -locale vars' = +class_locale vars' = fixes n::'name and b::'name assumes "distinct [n, b]" @@ -196,10 +200,19 @@ by simp +text {* Hmm, I hoped this would work now...*} + +(* +locale fooX = foo + + assumes "s\b = k" +*) + +(* ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ *) text {* There are known problems with syntax-declarations. They currently only work, when the context is already built. Hopefully this will be implemented correctly in future Isabelle versions. *} +(* lemma assumes "foo f a b c p1 i1 p2 i2 p3 i3 p4 i4" shows True @@ -207,7 +220,7 @@ interpret foo [f a b c p1 i1 p2 i2 p3 i3 p4 i4] by fact term "s\a = i" qed - +*) (* lemma includes foo diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/Statespace/StateSpaceLocale.thy diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/Statespace/state_space.ML Tue Dec 30 11:10:01 2008 +0100 @@ -17,7 +17,7 @@ val namespace_definition : bstring -> typ -> - Locale.expr -> + Expression.expression -> string list -> string list -> theory -> theory val define_statespace : @@ -61,7 +61,7 @@ val update_tr' : Proof.context -> term list -> term end; -structure StateSpace: STATE_SPACE = +structure StateSpace : STATE_SPACE = struct (* Theorems *) @@ -148,11 +148,25 @@ fun prove_interpretation_in ctxt_tac (name, expr) thy = thy - |> Locale.interpretation_in_locale I (name, expr) + |> Expression.sublocale_cmd name expr |> Proof.global_terminal_proof (Method.Basic (fn ctxt => Method.SIMPLE_METHOD (ctxt_tac ctxt),Position.none), NONE) |> ProofContext.theory_of +fun add_locale name expr elems thy = + thy + |> Expression.add_locale name name expr elems + |> (fn ((target, notes), ctxt) => TheoryTarget.begin target ctxt |> + fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes) + |> LocalTheory.exit; + +fun add_locale_cmd name expr elems thy = + thy + |> Expression.add_locale_cmd name name expr elems + |> (fn ((target, notes), ctxt) => TheoryTarget.begin target ctxt |> + fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes) + |> LocalTheory.exit; + type statespace_info = {args: (string * sort) list, (* type arguments *) parents: (typ list * string * string option list) list, @@ -252,7 +266,7 @@ in EVERY [rtac rule i] st end - fun tac ctxt = EVERY [Locale.intro_locales_tac true ctxt [], + fun tac ctxt = EVERY [NewLocale.intro_locales_tac true ctxt [], ALLGOALS (SUBGOAL (solve_tac ctxt))] in thy @@ -264,16 +278,11 @@ fun namespace_definition name nameT parent_expr parent_comps new_comps thy = let val all_comps = parent_comps @ new_comps; - val vars = Locale.Merge - (map (fn n => Locale.Rename (Locale.Locale (Locale.intern thy "var") - ,[SOME (n,NONE)])) all_comps); - + val vars = (map (fn n => (Binding.name n, NONE, NoSyn)) all_comps); val full_name = Sign.full_bname thy name; val dist_thm_name = distinct_compsN; - val dist_thm_full_name = - let val prefix = fold1' (fn name => fn prfx => prfx ^ "_" ^ name) all_comps ""; - in if prefix = "" then dist_thm_name else prefix ^ "." ^ dist_thm_name end; + val dist_thm_full_name = dist_thm_name; fun comps_of_thm thm = prop_of thm |> (fn (_$(_$t)) => DistinctTreeProver.dest_tree t) |> map (fst o dest_Free); @@ -309,12 +318,10 @@ DistinctTreeProver.mk_tree (fn n => Free (n,nameT)) nameT (sort fast_string_ord all_comps)), ([]))])]; - in thy - |> Locale.add_locale "" name vars [assumes] - ||> ProofContext.theory_of - ||> interprete_parent name dist_thm_full_name parent_expr - |> #2 + |> add_locale name ([],vars) [assumes] + |> ProofContext.theory_of + |> interprete_parent name dist_thm_full_name parent_expr end; fun encode_dot x = if x= #"." then #"_" else x; @@ -378,11 +385,10 @@ val components' = map (fn (n,T) => (n,(T,full_name))) components; val all_comps' = map (fn (n,T) => (n,(T,full_name))) all_comps; - fun parent_expr (_,n,rs) = Locale.Rename - (Locale.Locale (suffix namespaceN n), - map (Option.map (fn s => (s,NONE))) rs); - val parents_expr = Locale.Merge (fold (fn p => fn es => parent_expr p::es) parents []); + fun parent_expr (_,n,rs) = (suffix namespaceN n,((n,false),Expression.Positional rs)); + (* FIXME: a more specific renaming-prefix (including parameter names) may be nicer *) + val parents_expr = map parent_expr parents; fun distinct_types Ts = let val tab = fold (fn T => fn tab => Typtab.update (T,()) tab) Ts Typtab.empty; in map fst (Typtab.dest tab) end; @@ -396,30 +402,32 @@ val stateT = nameT --> valueT; fun projectT T = valueT --> T; fun injectT T = T --> valueT; - - val locs = map (fn T => Locale.Rename (Locale.Locale project_injectL, - [SOME (project_name T,NONE), - SOME (inject_name T ,NONE)])) Ts; + val locinsts = map (fn T => (project_injectL, + (("",false),Expression.Positional + [SOME (Free (project_name T,projectT T)), + SOME (Free ((inject_name T,injectT T)))]))) Ts; + val locs = flat (map (fn T => [(Binding.name (project_name T),NONE,NoSyn), + (Binding.name (inject_name T),NONE,NoSyn)]) Ts); val constrains = List.concat (map (fn T => [(project_name T,projectT T),(inject_name T,injectT T)]) Ts); - fun interprete_parent_valuetypes (Ts, pname, _) = + fun interprete_parent_valuetypes (Ts, pname, _) thy = let val {args,types,...} = the (Symtab.lookup (StateSpaceData.get (Context.Theory thy)) pname); val inst = map fst args ~~ Ts; val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst); val pars = List.concat (map ((fn T => [project_name T,inject_name T]) o subst) types); - val expr = Locale.Rename (Locale.Locale (suffix valuetypesN name), - map (fn n => SOME (n,NONE)) pars); - in prove_interpretation_in (K all_tac) - (suffix valuetypesN name, expr) end; + + val expr = ([(suffix valuetypesN name, + (("",false),Expression.Positional (map SOME pars)))],[]); + in prove_interpretation_in (K all_tac) (suffix valuetypesN name, expr) thy end; fun interprete_parent (_, pname, rs) = let - val expr = Locale.Rename (Locale.Locale pname, map (Option.map (fn n => (n,NONE))) rs) + val expr = ([(pname, (("",false), Expression.Positional rs))],[]) in prove_interpretation_in - (fn ctxt => Locale.intro_locales_tac false ctxt []) + (fn ctxt => NewLocale.intro_locales_tac false ctxt []) (full_name, expr) end; fun declare_declinfo updates lthy phi ctxt = @@ -454,17 +462,16 @@ in thy |> namespace_definition - (suffix namespaceN name) nameT parents_expr + (suffix namespaceN name) nameT (parents_expr,[]) (map fst parent_comps) (map fst components) |> Context.theory_map (add_statespace full_name args parents components []) - |> Locale.add_locale "" (suffix valuetypesN name) (Locale.Merge locs) - [Element.Constrains constrains] - |> ProofContext.theory_of o #2 + |> add_locale (suffix valuetypesN name) (locinsts,locs) [] + |> ProofContext.theory_of |> fold interprete_parent_valuetypes parents - |> Locale.add_locale_cmd name - (Locale.Merge [Locale.Locale (suffix namespaceN full_name) - ,Locale.Locale (suffix valuetypesN full_name)]) fixestate - |> ProofContext.theory_of o #2 + |> add_locale_cmd name + ([(suffix namespaceN full_name ,(("",false),Expression.Named [])), + (suffix valuetypesN full_name,(("",false),Expression.Named []))],[]) fixestate + |> ProofContext.theory_of |> fold interprete_parent parents |> add_declaration (SOME full_name) (declare_declinfo components') end; @@ -572,7 +579,6 @@ | xs => ["Components already defined in parents: " ^ commas xs]); val errs = err_dup_args @ err_dup_components @ err_extra_frees @ err_dup_types @ err_comp_in_parent; - in if null errs then thy |> statespace_definition state_space args' name parents' parent_comps comps' else error (cat_lines errs) diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/Word/TdThs.thy --- a/src/HOL/Word/TdThs.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/Word/TdThs.thy Tue Dec 30 11:10:01 2008 +0100 @@ -90,7 +90,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 7dc7a75033ea -r ea97aa6aeba2 src/HOL/Word/WordArith.thy --- a/src/HOL/Word/WordArith.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/Word/WordArith.thy Tue Dec 30 11:10:01 2008 +0100 @@ -22,7 +22,7 @@ proof qed (unfold word_sle_def word_sless_def, auto) -interpretation signed: linorder ["word_sle" "word_sless"] +class_interpretation signed: linorder ["word_sle" "word_sless"] by (rule signed_linorder) lemmas word_arith_wis = @@ -858,11 +858,11 @@ 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: - td_ext ["unat::'a::len word => nat" - of_nat - "unats (len_of TYPE('a::len))" - "%i. i mod 2 ^ len_of TYPE('a::len)"] +interpretation word_unat!: + td_ext "unat::'a::len word => nat" + of_nat + "unats (len_of TYPE('a::len))" + "%i. i mod 2 ^ len_of TYPE('a::len)" by (rule td_ext_unat) lemmas td_unat = word_unat.td_thm diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/Word/WordBitwise.thy --- a/src/HOL/Word/WordBitwise.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/Word/WordBitwise.thy Tue Dec 30 11:10:01 2008 +0100 @@ -344,11 +344,11 @@ lemmas td_ext_nth = td_ext_nth' [OF refl refl refl, unfolded word_size] -interpretation test_bit: - td_ext ["op !! :: 'a::len0 word => nat => bool" - set_bits - "{f. \i. f i \ i < len_of TYPE('a::len0)}" - "(\h i. h i \ i < len_of TYPE('a::len0))"] +interpretation test_bit!: + td_ext "op !! :: 'a::len0 word => nat => bool" + set_bits + "{f. \i. f i \ i < len_of TYPE('a::len0)}" + "(\h i. h i \ i < len_of TYPE('a::len0))" by (rule td_ext_nth) declare test_bit.Rep' [simp del] diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/Word/WordDefinition.thy --- a/src/HOL/Word/WordDefinition.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/Word/WordDefinition.thy Tue Dec 30 11:10:01 2008 +0100 @@ -356,11 +356,11 @@ lemmas int_word_uint = td_ext_uint [THEN td_ext.eq_norm, standard] -interpretation word_uint: - td_ext ["uint::'a::len0 word \ int" - word_of_int - "uints (len_of TYPE('a::len0))" - "\w. w mod 2 ^ len_of TYPE('a::len0)"] +interpretation word_uint!: + td_ext "uint::'a::len0 word \ int" + word_of_int + "uints (len_of TYPE('a::len0))" + "\w. w mod 2 ^ len_of TYPE('a::len0)" by (rule td_ext_uint) lemmas td_uint = word_uint.td_thm @@ -368,11 +368,11 @@ lemmas td_ext_ubin = td_ext_uint [simplified len_gt_0 no_bintr_alt1 [symmetric]] -interpretation word_ubin: - td_ext ["uint::'a::len0 word \ int" - word_of_int - "uints (len_of TYPE('a::len0))" - "bintrunc (len_of TYPE('a::len0))"] +interpretation word_ubin!: + td_ext "uint::'a::len0 word \ int" + word_of_int + "uints (len_of TYPE('a::len0))" + "bintrunc (len_of TYPE('a::len0))" by (rule td_ext_ubin) lemma sint_sbintrunc': @@ -423,19 +423,19 @@ 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: - td_ext ["sint ::'a::len word => int" +interpretation word_sint!: + td_ext "sint ::'a::len word => int" word_of_int "sints (len_of TYPE('a::len))" "%w. (w + 2^(len_of TYPE('a::len) - 1)) mod 2^len_of TYPE('a::len) - - 2 ^ (len_of TYPE('a::len) - 1)"] + 2 ^ (len_of TYPE('a::len) - 1)" by (rule td_ext_sint) -interpretation word_sbin: - td_ext ["sint ::'a::len word => int" +interpretation word_sbin!: + td_ext "sint ::'a::len word => int" word_of_int "sints (len_of TYPE('a::len))" - "sbintrunc (len_of TYPE('a::len) - 1)"] + "sbintrunc (len_of TYPE('a::len) - 1)" by (rule td_ext_sbin) lemmas int_word_sint = td_ext_sint [THEN td_ext.eq_norm, standard] @@ -635,10 +635,10 @@ apply simp done -interpretation word_bl: - type_definition ["to_bl :: 'a::len0 word => bool list" - of_bl - "{bl. length bl = len_of TYPE('a::len0)}"] +interpretation word_bl!: + type_definition "to_bl :: 'a::len0 word => bool list" + of_bl + "{bl. length bl = len_of TYPE('a::len0)}" by (rule td_bl) lemma word_size_bl: "size w == size (to_bl w)" diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/Word/WordGenLib.thy --- a/src/HOL/Word/WordGenLib.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/Word/WordGenLib.thy Tue Dec 30 11:10:01 2008 +0100 @@ -107,16 +107,16 @@ apply (rule word_or_not) done -interpretation word_bool_alg: - boolean ["op AND" "op OR" bitNOT 0 max_word] +interpretation word_bool_alg!: + boolean "op AND" "op OR" bitNOT 0 max_word by (rule word_boolean) lemma word_xor_and_or: "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: - boolean_xor ["op AND" "op OR" bitNOT 0 max_word "op XOR"] +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) apply (rule boolean_xor_axioms.intro) @@ -363,7 +363,7 @@ apply (erule contrapos_pn, simp) apply (drule arg_cong[where f=of_nat]) apply simp - apply (subst (asm) word_unat.Rep_Abs_A.Rep_inverse[of n]) + apply (subst (asm) word_unat.Rep_inverse[of n]) apply simp apply simp done diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/ex/Abstract_NAT.thy --- a/src/HOL/ex/Abstract_NAT.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/ex/Abstract_NAT.thy Tue Dec 30 11:10:01 2008 +0100 @@ -1,5 +1,4 @@ (* - ID: $Id$ Author: Makarius *) @@ -131,7 +130,7 @@ text {* \medskip Just see that our abstract specification makes sense \dots *} -interpretation NAT [0 Suc] +interpretation NAT 0 Suc proof (rule NAT.intro) fix m n show "(Suc m = Suc n) = (m = n)" by simp diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/ex/LocaleTest2.thy --- a/src/HOL/ex/LocaleTest2.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/ex/LocaleTest2.thy Tue Dec 30 11:10:01 2008 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/ex/LocaleTest2.thy - ID: $Id$ Author: Clemens Ballarin Copyright (c) 2007 by Clemens Ballarin @@ -433,8 +432,7 @@ end -interpretation dlo < dlat -(* TODO: definition syntax is unavailable *) +sublocale dlo < dlat proof fix x y from total have "is_inf x y (if x \ y then x else y)" by (auto simp: is_inf_def) @@ -445,7 +443,7 @@ then show "EX sup. is_sup x y sup" by blast qed -interpretation dlo < ddlat +sublocale dlo < ddlat proof fix x y z show "x \ (y \ z) = x \ y \ x \ z" (is "?l = ?r") @@ -470,13 +468,13 @@ 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 - show "dpo (op <= :: [int, int] => bool)" proof qed auto - then interpret int: dpo ["op <= :: [int, int] => bool"] . + then interpret int: dpo "op <= :: [int, int] => bool" . txt {* Gives interpreted version of @{text less_def} (without condition). *} show "(dpo.less (op <=) (x::int) y) = (x < y)" by (unfold int.less_def) auto @@ -489,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 - @@ -498,7 +496,7 @@ apply (unfold int.is_inf_def int.is_sup_def) apply arith+ done - then interpret int: dlat ["op <= :: [int, int] => bool"] . + then interpret int: dlat "op <= :: [int, int] => bool" . txt {* Interpretation to ease use of definitions, which are conditional in general but unconditional after interpretation. *} show "dlat.meet (op <=) (x::int) y = min x y" @@ -513,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. *} @@ -526,13 +524,13 @@ 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 - show "dpo (op <= :: [nat, nat] => bool)" proof qed auto - then interpret nat: dpo ["op <= :: [nat, nat] => bool"] . + then interpret nat: dpo "op <= :: [nat, nat] => bool" . txt {* Gives interpreted version of @{text less_def} (without condition). *} show "dpo.less (op <=) (x::nat) y = (x < y)" apply (unfold nat.less_def) @@ -540,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 - @@ -549,7 +547,7 @@ apply (unfold nat.is_inf_def nat.is_sup_def) apply arith+ done - then interpret nat: dlat ["op <= :: [nat, nat] => bool"] . + then interpret nat: dlat "op <= :: [nat, nat] => bool" . txt {* Interpretation to ease use of definitions, which are conditional in general but unconditional after interpretation. *} show "dlat.meet (op <=) (x::nat) y = min x y" @@ -564,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. *} @@ -577,13 +575,13 @@ 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 - show "dpo (op dvd :: [nat, nat] => bool)" proof qed (auto simp: dvd_def) - then interpret nat_dvd: dpo ["op dvd :: [nat, nat] => bool"] . + then interpret nat_dvd: dpo "op dvd :: [nat, nat] => bool" . txt {* Gives interpreted version of @{text less_def} (without condition). *} show "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)" apply (unfold nat_dvd.less_def) @@ -591,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 - @@ -603,7 +601,7 @@ apply (rule_tac x = "lcm x y" in exI) apply (auto intro: lcm_dvd1 lcm_dvd2 lcm_least) done - then interpret nat_dvd: dlat ["op dvd :: [nat, nat] => bool"] . + then interpret nat_dvd: dlat "op dvd :: [nat, nat] => bool" . txt {* Interpretation to ease use of definitions, which are conditional in general but unconditional after interpretation. *} show "dlat.meet (op dvd) (x::nat) y = gcd x y" @@ -819,7 +817,8 @@ end -locale Dhom = Dgrp prod (infixl "**" 65) one + Dgrp sum (infixl "+++" 60) zero + +locale Dhom = prod: Dgrp prod one + sum: Dgrp sum zero + for prod (infixl "**" 65) and one and sum (infixl "+++" 60) and zero + fixes hom assumes hom_mult [simp]: "hom (x ** y) = hom x +++ hom y" @@ -838,14 +837,14 @@ 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 - show "Dmonoid op o (id :: 'a => 'a)" proof qed (simp_all add: o_assoc) note Dmonoid = this (* - from this interpret Dmonoid ["op o" "id :: 'a => 'a"] . + from this interpret Dmonoid "op o" "id :: 'a => 'a" . *) show "Dmonoid.unit (op o) (id :: 'a => 'a) f = bij f" apply (unfold Dmonoid.unit_def [OF Dmonoid]) @@ -888,7 +887,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 7dc7a75033ea -r ea97aa6aeba2 src/HOL/ex/Tarski.thy --- a/src/HOL/ex/Tarski.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/ex/Tarski.thy Tue Dec 30 11:10:01 2008 +0100 @@ -120,7 +120,7 @@ locale CL = S + assumes cl_co: "cl : CompleteLattice" -interpretation CL < PO +sublocale CL < PO apply (simp_all add: A_def r_def) apply unfold_locales using cl_co unfolding CompleteLattice_def by auto @@ -131,7 +131,7 @@ assumes f_cl: "(cl,f) : CLF_set" (*was the equivalent "f : CLF_set``{cl}"*) defines P_def: "P == fix f A" -interpretation CLF < CL +sublocale CLF < CL apply (simp_all add: A_def r_def) apply unfold_locales using f_cl unfolding CLF_set_def by auto diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/main.ML diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOL/plain.ML --- a/src/HOL/plain.ML Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOL/plain.ML Tue Dec 30 11:10:01 2008 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/plain.ML - ID: $Id$ Classical Higher-order Logic -- plain Tool bootstrap. *) diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOLCF/Algebraic.thy --- a/src/HOLCF/Algebraic.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOLCF/Algebraic.thy Tue Dec 30 11:10:01 2008 +0100 @@ -160,7 +160,7 @@ assumes f: "\x. f\x \ x" shows "pre_deflation (d oo f)" proof - interpret d: finite_deflation [d] by fact + interpret d: finite_deflation d by fact fix x show "\x. (d oo f)\x \ x" by (simp, rule trans_less [OF d.less f]) @@ -173,9 +173,9 @@ assumes f: "\x. f\x \ x" shows "eventual (\n. iterate n\(d oo f))\x = x \ d\x = x \ f\x = x" proof - - interpret d: finite_deflation [d] by fact + interpret d: finite_deflation d by fact let ?e = "d oo f" - interpret e: pre_deflation ["d oo f"] + interpret e: pre_deflation "d oo f" using `finite_deflation d` f by (rule pre_deflation_d_f) let ?g = "eventual (\n. iterate n\?e)" @@ -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,8 +370,8 @@ unfolding alg_defl_principal_def by (simp add: Abs_alg_defl_inverse sq_le.ideal_principal) -interpretation alg_defl: - ideal_completion [sq_le fd_take alg_defl_principal Rep_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) apply (erule Rep_alg_defl_lub) @@ -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" @@ -485,7 +485,7 @@ constrains e :: "'a::profinite \ 'b::profinite" shows "\d. cast\d = e oo p" proof - interpret ep_pair [e p] by fact + interpret ep_pair e p by fact let ?a = "\i. e oo approx i oo p" have a: "\i. finite_deflation (?a i)" apply (rule finite_deflation_e_d_p) @@ -516,7 +516,7 @@ "\i. finite_deflation (a i)" "(\i. a i) = ID" proof - interpret ep_pair [e p] by fact + interpret ep_pair e p by fact let ?a = "\i. p oo cast\(approx i\d) oo e" show "\i. finite_deflation (?a i)" apply (rule finite_deflation_p_d_e) diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOLCF/Bifinite.thy --- a/src/HOLCF/Bifinite.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOLCF/Bifinite.thy Tue Dec 30 11:10:01 2008 +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 7dc7a75033ea -r ea97aa6aeba2 src/HOLCF/CompactBasis.thy --- a/src/HOLCF/CompactBasis.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOLCF/CompactBasis.thy Tue Dec 30 11:10:01 2008 +0100 @@ -46,8 +46,8 @@ lemmas approx_Rep_compact_basis = Rep_compact_take [symmetric] -interpretation compact_basis: - basis_take [sq_le compact_take] +interpretation compact_basis!: + basis_take sq_le compact_take proof fix n :: nat and a :: "'a compact_basis" show "compact_take n a \ a" @@ -92,8 +92,8 @@ approximants :: "'a \ 'a compact_basis set" where "approximants = (\x. {a. Rep_compact_basis a \ x})" -interpretation compact_basis: - ideal_completion [sq_le compact_take Rep_compact_basis approximants] +interpretation compact_basis!: + ideal_completion sq_le compact_take Rep_compact_basis approximants proof fix w :: 'a show "preorder.ideal sq_le (approximants w)" @@ -244,7 +244,7 @@ assumes "ab_semigroup_idem_mult f" shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)" proof - - interpret ab_semigroup_idem_mult [f] by fact + class_interpret ab_semigroup_idem_mult [f] by fact show ?thesis unfolding fold_pd_def Rep_PDPlus by (simp add: image_Un fold1_Un2) qed diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOLCF/Completion.thy --- a/src/HOLCF/Completion.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOLCF/Completion.thy Tue Dec 30 11:10:01 2008 +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 7dc7a75033ea -r ea97aa6aeba2 src/HOLCF/ConvexPD.thy --- a/src/HOLCF/ConvexPD.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOLCF/ConvexPD.thy Tue Dec 30 11:10:01 2008 +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,8 +178,8 @@ unfolding convex_principal_def by (simp add: Abs_convex_pd_inverse convex_le.ideal_principal) -interpretation convex_pd: - ideal_completion [convex_le pd_take convex_principal Rep_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) apply (rule pd_take_idem) @@ -296,7 +296,7 @@ apply (simp add: PDPlus_absorb) done -interpretation aci_convex_plus: ab_semigroup_idem_mult ["op +\"] +class_interpretation aci_convex_plus: ab_semigroup_idem_mult ["op +\"] by unfold_locales (rule convex_plus_assoc convex_plus_commute convex_plus_absorb)+ diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOLCF/Deflation.thy --- a/src/HOLCF/Deflation.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOLCF/Deflation.thy Tue Dec 30 11:10:01 2008 +0100 @@ -81,10 +81,10 @@ assumes "deflation g" shows "f \ g \ f\(g\x) = f\x" proof (rule antisym_less) - interpret g: deflation [g] by fact + interpret g: deflation g by fact from g.less show "f\(g\x) \ f\x" by (rule monofun_cfun_arg) next - interpret f: deflation [f] by fact + interpret f: deflation f by fact assume "f \ g" hence "f\x \ g\x" by (rule monofun_cfun_fun) hence "f\(f\x) \ f\(g\x)" by (rule monofun_cfun_arg) also have "f\(f\x) = f\x" by (rule f.idem) @@ -219,7 +219,7 @@ assumes "deflation d" shows "deflation (e oo d oo p)" proof - interpret deflation [d] by fact + interpret deflation d by fact fix x :: 'b show "(e oo d oo p)\((e oo d oo p)\x) = (e oo d oo p)\x" by (simp add: idem) @@ -231,7 +231,7 @@ assumes "finite_deflation d" shows "finite_deflation (e oo d oo p)" proof - interpret finite_deflation [d] by fact + interpret finite_deflation d by fact fix x :: 'b show "(e oo d oo p)\((e oo d oo p)\x) = (e oo d oo p)\x" by (simp add: idem) @@ -250,7 +250,7 @@ assumes d: "\x. d\x \ e\(p\x)" shows "deflation (p oo d oo e)" proof - - interpret d: deflation [d] by fact + interpret d: deflation d by fact { fix x have "d\(e\x) \ e\x" @@ -287,7 +287,7 @@ assumes d: "\x. d\x \ e\(p\x)" shows "finite_deflation (p oo d oo e)" proof - - interpret d: finite_deflation [d] by fact + interpret d: finite_deflation d by fact show ?thesis proof (intro_locales) have "deflation d" .. @@ -316,8 +316,8 @@ assumes "ep_pair e1 p" and "ep_pair e2 p" shows "e1 \ e2" proof (rule less_cfun_ext) - interpret e1: ep_pair [e1 p] by fact - interpret e2: ep_pair [e2 p] by fact + interpret e1: ep_pair e1 p by fact + interpret e2: ep_pair e2 p by fact fix x have "e1\(p\(e2\x)) \ e2\x" by (rule e1.e_p_less) @@ -333,8 +333,8 @@ assumes "ep_pair e p1" and "ep_pair e p2" shows "p1 \ p2" proof (rule less_cfun_ext) - interpret p1: ep_pair [e p1] by fact - interpret p2: ep_pair [e p2] by fact + interpret p1: ep_pair e p1 by fact + interpret p2: ep_pair e p2 by fact fix x have "e\(p1\x) \ x" by (rule p1.e_p_less) @@ -357,8 +357,8 @@ assumes "ep_pair e1 p1" and "ep_pair e2 p2" shows "ep_pair (e2 oo e1) (p1 oo p2)" proof - interpret ep1: ep_pair [e1 p1] by fact - interpret ep2: ep_pair [e2 p2] by fact + interpret ep1: ep_pair e1 p1 by fact + interpret ep2: ep_pair e2 p2 by fact fix x y show "(p1 oo p2)\((e2 oo e1)\x) = x" by simp diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOLCF/LowerPD.thy --- a/src/HOLCF/LowerPD.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOLCF/LowerPD.thy Tue Dec 30 11:10:01 2008 +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,8 +133,8 @@ unfolding lower_principal_def by (simp add: Abs_lower_pd_inverse lower_le.ideal_principal) -interpretation lower_pd: - ideal_completion [lower_le pd_take lower_principal Rep_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) apply (rule pd_take_idem) @@ -250,7 +250,7 @@ apply (simp add: PDPlus_absorb) done -interpretation aci_lower_plus: ab_semigroup_idem_mult ["op +\"] +class_interpretation aci_lower_plus: ab_semigroup_idem_mult ["op +\"] by unfold_locales (rule lower_plus_assoc lower_plus_commute lower_plus_absorb)+ diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOLCF/Universal.thy --- a/src/HOLCF/Universal.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOLCF/Universal.thy Tue Dec 30 11:10:01 2008 +0100 @@ -226,13 +226,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) @@ -281,8 +281,8 @@ unfolding udom_principal_def by (simp add: Abs_udom_inverse udom.ideal_principal) -interpretation udom: - ideal_completion [ubasis_le ubasis_take udom_principal Rep_udom] +interpretation udom!: + ideal_completion ubasis_le ubasis_take udom_principal Rep_udom apply unfold_locales apply (rule ideal_Rep_udom) apply (erule Rep_udom_lub) diff -r 7dc7a75033ea -r ea97aa6aeba2 src/HOLCF/UpperPD.thy --- a/src/HOLCF/UpperPD.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/HOLCF/UpperPD.thy Tue Dec 30 11:10:01 2008 +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,8 +131,8 @@ unfolding upper_principal_def by (simp add: Abs_upper_pd_inverse upper_le.ideal_principal) -interpretation upper_pd: - ideal_completion [upper_le pd_take upper_principal Rep_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) apply (rule pd_take_idem) @@ -248,7 +248,7 @@ apply (simp add: PDPlus_absorb) done -interpretation aci_upper_plus: ab_semigroup_idem_mult ["op +\"] +class_interpretation aci_upper_plus: ab_semigroup_idem_mult ["op +\"] by unfold_locales (rule upper_plus_assoc upper_plus_commute upper_plus_absorb)+ diff -r 7dc7a75033ea -r ea97aa6aeba2 src/Pure/General/binding.ML --- a/src/Pure/General/binding.ML Mon Dec 29 22:43:41 2008 +0100 +++ b/src/Pure/General/binding.ML Tue Dec 30 11:10:01 2008 +0100 @@ -59,8 +59,8 @@ val qualify = map_base o qualify_base; (*FIXME should all operations on bare names move here from name_space.ML ?*) -fun add_prefix sticky prfx b = if prfx = "" then error "empty name prefix" - else (map_binding o apfst) (cons (prfx, sticky)) b; +fun add_prefix sticky "" b = b + | add_prefix sticky prfx b = (map_binding o apfst) (cons (prfx, sticky)) b; fun map_prefix f (Binding ((prefix, name), pos)) = f prefix (name_pos (name, pos)); diff -r 7dc7a75033ea -r ea97aa6aeba2 src/Pure/IsaMakefile diff -r 7dc7a75033ea -r ea97aa6aeba2 src/Pure/Isar/ROOT.ML --- a/src/Pure/Isar/ROOT.ML Mon Dec 29 22:43:41 2008 +0100 +++ b/src/Pure/Isar/ROOT.ML Tue Dec 30 11:10:01 2008 +0100 @@ -51,7 +51,6 @@ use "obtain.ML"; (*local theories and targets*) -val new_locales = ref false; use "local_theory.ML"; use "overloading.ML"; use "locale.ML"; diff -r 7dc7a75033ea -r ea97aa6aeba2 src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Mon Dec 29 22:43:41 2008 +0100 +++ b/src/Pure/Isar/element.ML Tue Dec 30 11:10:01 2008 +0100 @@ -23,6 +23,10 @@ val facts_map: (('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt) -> (Attrib.binding * ('fact * Attrib.src list) list) list -> (Attrib.binding * ('c * Attrib.src list) list) list + val map_ctxt': {binding: Binding.T -> Binding.T, + var: Binding.T * mixfix -> Binding.T * mixfix, + typ: 'typ -> 'a, term: 'term -> 'b, pat: 'term -> 'b, fact: 'fact -> 'c, + attrib: Attrib.src -> Attrib.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt val map_ctxt: {binding: Binding.T -> Binding.T, var: Binding.T * mixfix -> Binding.T * mixfix, typ: 'typ -> 'a, term: 'term -> 'b, fact: 'fact -> 'c, @@ -74,10 +78,9 @@ val generalize_facts: Proof.context -> Proof.context -> (Attrib.binding * (thm list * Attrib.src list) list) list -> (Attrib.binding * (thm list * Attrib.src list) list) list - val activate: (typ, term, Facts.ref) ctxt list -> Proof.context -> - (context_i list * (Binding.T * Thm.thm list) list) * Proof.context - val activate_i: context_i list -> Proof.context -> - (context_i list * (Binding.T * Thm.thm list) list) * Proof.context + val transfer_morphism: theory -> morphism + val activate: (typ, term, Facts.ref) ctxt list -> Proof.context -> context_i list * Proof.context + val activate_i: context_i list -> Proof.context -> context_i list * Proof.context end; structure Element: ELEMENT = @@ -109,18 +112,22 @@ fun facts_map f facts = Notes ("", facts) |> f |> (fn Notes (_, facts') => facts'); -fun map_ctxt {binding, var, typ, term, fact, attrib} = +fun map_ctxt' {binding, var, typ, term, pat, fact, attrib} = fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) => let val (x', mx') = var (x, mx) in (x', Option.map typ T, mx') end)) | Constrains xs => Constrains (xs |> map (fn (x, T) => let val x' = Binding.base_name (#1 (var (Binding.name x, NoSyn))) in (x', typ T) end)) | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) => - ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map term ps))))) + ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map pat ps))))) | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) => - ((binding a, map attrib atts), (term t, map term ps)))) + ((binding a, map attrib atts), (term t, map pat ps)))) | Notes (kind, facts) => Notes (kind, facts |> map (fn ((a, atts), bs) => ((binding a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts))))); +fun map_ctxt {binding, var, typ, term, fact, attrib} = + map_ctxt' {binding = binding, var = var, typ = typ, term = term, pat = term, + fact = fact, attrib = attrib} + fun map_ctxt_attrib attrib = map_ctxt {binding = I, var = I, typ = I, term = I, fact = I, attrib = attrib}; @@ -531,14 +538,23 @@ in facts_map (morph_ctxt morphism) facts end; +(* transfer to theory using closure *) + +fun transfer_morphism thy = + let val thy_ref = Theory.check_thy thy in + Morphism.morphism {binding = I, var = I, typ = I, term = I, + fact = map (fn th => transfer (Theory.deref thy_ref) th)} + end; + + (** activate in context, return elements and facts **) local fun activate_elem (Fixes fixes) ctxt = - ([], ctxt |> ProofContext.add_fixes_i fixes |> snd) + ctxt |> ProofContext.add_fixes_i fixes |> snd | activate_elem (Constrains _) ctxt = - ([], ctxt) + ctxt | activate_elem (Assumes asms) ctxt = let val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms; @@ -546,7 +562,7 @@ val (_, ctxt') = ctxt |> fold Variable.auto_fixes ts |> ProofContext.add_assms_i Assumption.presume_export asms'; - in ([], ctxt') end + in ctxt' end | activate_elem (Defines defs) ctxt = let val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs; @@ -556,19 +572,20 @@ val (_, ctxt') = ctxt |> fold (Variable.auto_fixes o #1) asms |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms); - in ([], ctxt') end + in ctxt' end | activate_elem (Notes (kind, facts)) ctxt = let val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts; val (res, ctxt') = ctxt |> ProofContext.note_thmss_i kind facts'; - in ((map (#1 o #1) facts' ~~ map #2 res), ctxt') end; + in ctxt' end; fun gen_activate prep_facts raw_elems ctxt = let - val elems = map (map_ctxt_attrib Args.assignable o prep_facts ctxt) raw_elems; - val (res, ctxt') = fold_map activate_elem elems (ProofContext.qualified_names ctxt); - val elems' = elems |> map (map_ctxt_attrib Args.closure); - in ((elems', flat res), ProofContext.restore_naming ctxt ctxt') end; + fun activate elem ctxt = + let val elem' = (map_ctxt_attrib Args.assignable o prep_facts ctxt) elem + in (elem', activate_elem elem' ctxt) end + val (elems, ctxt') = fold_map activate raw_elems (ProofContext.qualified_names ctxt); + in (elems |> map (map_ctxt_attrib Args.closure), ProofContext.restore_naming ctxt ctxt') end; fun check_name name = if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name) diff -r 7dc7a75033ea -r ea97aa6aeba2 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Mon Dec 29 22:43:41 2008 +0100 +++ b/src/Pure/Isar/expression.ML Tue Dec 30 11:10:01 2008 +0100 @@ -7,7 +7,7 @@ signature EXPRESSION = sig datatype 'term map = Positional of 'term option list | Named of (string * 'term) list; - type 'term expr = (string * (string * 'term map)) list; + type 'term expr = (string * ((string * bool) * 'term map)) list; type expression = string expr * (Binding.T * string option * mixfix) list; type expression_i = term expr * (Binding.T * typ option * mixfix) list; @@ -28,8 +28,8 @@ (* Interpretation *) val sublocale_cmd: string -> expression -> theory -> Proof.state; val sublocale: string -> expression_i -> theory -> Proof.state; - val interpretation_cmd: expression -> theory -> Proof.state; - val interpretation: expression_i -> theory -> Proof.state; + val interpretation_cmd: expression -> (Attrib.binding * string) list -> theory -> Proof.state; + val interpretation: expression_i -> (Attrib.binding * term) list -> theory -> Proof.state; val interpret_cmd: expression -> bool -> Proof.state -> Proof.state; val interpret: expression_i -> bool -> Proof.state -> Proof.state; end; @@ -47,7 +47,7 @@ Positional of 'term option list | Named of (string * 'term) list; -type 'term expr = (string * (string * 'term map)) list; +type 'term expr = (string * ((string * bool) * 'term map)) list; type expression = string expr * (Binding.T * string option * mixfix) list; type expression_i = term expr * (Binding.T * typ option * mixfix) list; @@ -154,7 +154,7 @@ (* Instantiation morphism *) -fun inst_morph (parm_names, parm_types) (prfx, insts') ctxt = +fun inst_morph (parm_names, parm_types) ((prfx, strict), insts') ctxt = let (* parameters *) val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst; @@ -175,7 +175,7 @@ val inst = Symtab.make insts''; in (Element.inst_morphism (ProofContext.theory_of ctxt) (instT, inst) $> - Morphism.binding_morphism (Binding.qualify prfx), ctxt') + Morphism.binding_morphism (Binding.add_prefix strict prfx), ctxt') end; @@ -184,12 +184,15 @@ (** Parsing **) fun parse_elem prep_typ prep_term ctxt elem = - Element.map_ctxt {binding = I, var = I, typ = prep_typ ctxt, - term = prep_term ctxt, fact = I, attrib = I} elem; + Element.map_ctxt' {binding = I, var = I, typ = prep_typ ctxt, + term = prep_term (ProofContext.set_mode ProofContext.mode_schematic ctxt), (* FIXME ?? *) + pat = prep_term (ProofContext.set_mode ProofContext.mode_pattern ctxt), + fact = I, attrib = I} elem; fun parse_concl prep_term ctxt concl = (map o map) (fn (t, ps) => - (prep_term ctxt, map (prep_term ctxt) ps)) concl; + (prep_term (ProofContext.set_mode ProofContext.mode_schematic ctxt) t, (* FIXME ?? *) + map (prep_term (ProofContext.set_mode ProofContext.mode_pattern ctxt)) ps)) concl; (** Simultaneous type inference: instantiations + elements + conclusion **) @@ -268,38 +271,7 @@ | declare_elem _ (Defines _) ctxt = ctxt | declare_elem _ (Notes _) ctxt = ctxt; -(** Finish locale elements, extract specification text **) - -val norm_term = Envir.beta_norm oo Term.subst_atomic; - -fun bind_def ctxt eq (xs, env, eqs) = - let - val _ = LocalDefs.cert_def ctxt eq; - val ((y, T), b) = LocalDefs.abs_def eq; - val b' = norm_term env b; - fun err msg = error (msg ^ ": " ^ quote y); - in - exists (fn (x, _) => x = y) xs andalso - err "Attempt to define previously specified variable"; - exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso - err "Attempt to redefine variable"; - (Term.add_frees b' xs, (Free (y, T), b') :: env, eq :: eqs) - end; - -fun eval_text _ _ (Fixes _) text = text - | eval_text _ _ (Constrains _) text = text - | eval_text _ is_ext (Assumes asms) - (((exts, exts'), (ints, ints')), (xs, env, defs)) = - let - val ts = maps (map #1 o #2) asms; - val ts' = map (norm_term env) ts; - val spec' = - if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints')) - else ((exts, exts'), (ints @ ts, ints' @ ts')); - in (spec', (fold Term.add_frees ts' xs, env, defs)) end - | eval_text ctxt _ (Defines defs) (spec, binds) = - (spec, fold (bind_def ctxt o #1 o #2) defs binds) - | eval_text _ _ (Notes _) text = text; +(** Finish locale elements **) fun closeup _ _ false elem = elem | closeup ctxt parms true elem = @@ -334,36 +306,24 @@ | finish_primitive _ close (Defines defs) = close (Defines defs) | finish_primitive _ _ (Notes facts) = Notes facts; -fun finish_inst ctxt parms do_close (loc, (prfx, inst)) text = +fun finish_inst ctxt parms do_close (loc, (prfx, inst)) = let val thy = ProofContext.theory_of ctxt; val (parm_names, parm_types) = NewLocale.params_of thy loc |> map (fn (b, SOME T, _) => (Binding.base_name b, T)) |> split_list; - val (asm, defs) = NewLocale.specification_of thy loc; val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt; - val asm' = Option.map (Morphism.term morph) asm; - val defs' = map (Morphism.term morph) defs; - val text' = text |> - (if is_some asm - then eval_text ctxt false (Assumes [(Attrib.empty_binding, [(the asm', [])])]) - else I) |> - (if not (null defs) - then eval_text ctxt false (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs')) - else I) -(* FIXME clone from new_locale.ML *) - in ((loc, morph), text') end; + in (loc, morph) end; -fun finish_elem ctxt parms do_close elem text = +fun finish_elem ctxt parms do_close elem = let val elem' = finish_primitive parms (closeup ctxt parms do_close) elem; - val text' = eval_text ctxt true elem' text; - in (elem', text') end + in elem' end -fun finish ctxt parms do_close insts elems text = +fun finish ctxt parms do_close insts elems = let - val (deps, text') = fold_map (finish_inst ctxt parms do_close) insts text; - val (elems', text'') = fold_map (finish_elem ctxt parms do_close) elems text'; - in (deps, elems', text'') end; + val deps = map (finish_inst ctxt parms do_close) insts; + val elems' = map (finish_elem ctxt parms do_close) elems; + in (deps, elems') end; (** Process full context statement: instantiations + elements + conclusion **) @@ -398,19 +358,17 @@ let val ctxt' = declare_elem prep_vars raw_elem ctxt; val elems' = elems @ [parse_elem parse_typ parse_prop ctxt' raw_elem]; - (* FIXME term bindings *) val (_, _, _, ctxt'') = check_autofix insts elems' [] ctxt'; in (insts, elems', ctxt') end; fun prep_concl raw_concl (insts, elems, ctxt) = let - val concl = (map o map) (fn (t, ps) => - (parse_prop ctxt t, map (parse_prop ctxt) ps)) raw_concl; + val concl = parse_concl parse_prop ctxt raw_concl; in check_autofix insts elems concl ctxt end; val fors = prep_vars fixed context |> fst; val ctxt = context |> ProofContext.add_fixes_i fors |> snd; - val (_, insts', ctxt') = fold prep_inst raw_insts (0, [], NewLocale.clear_local_idents ctxt); + val (_, insts', ctxt') = fold prep_inst raw_insts (0, [], ctxt); val (_, elems'', ctxt'') = fold prep_elem raw_elems (insts', [], ctxt'); val (insts, elems, concl, ctxt) = prep_concl raw_concl (insts', elems'', ctxt''); @@ -421,28 +379,9 @@ val parms = xs ~~ Ts; (* params from expression and elements *) val Fixes fors' = finish_primitive parms I (Fixes fors); - val (deps, elems', text) = finish ctxt' parms do_close insts elems ((([], []), ([], [])), ([], [], [])); - (* text has the following structure: - (((exts, exts'), (ints, ints')), (xs, env, defs)) - where - exts: external assumptions (terms in assumes elements) - exts': dito, normalised wrt. env - ints: internal assumptions (terms in assumptions from insts) - ints': dito, normalised wrt. env - xs: the free variables in exts' and ints' and rhss of definitions, - this includes parameters except defined parameters - env: list of term pairs encoding substitutions, where the first term - is a free variable; substitutions represent defines elements and - the rhs is normalised wrt. the previous env - defs: the equations from the defines elements - elems is an updated version of raw_elems: - - type info added to Fixes and modified in Constrains - - axiom and definition statement replaced by corresponding one - from proppss in Assumes and Defines - - Facts unchanged - *) + val (deps, elems') = finish ctxt' parms do_close insts elems; - in ((fors', deps, elems', concl), (parms, text)) end + in ((fors', deps, elems', concl), (parms, ctxt')) end in @@ -479,14 +418,13 @@ fun prep_declaration prep activate raw_import raw_elems context = let - val ((fixed, deps, elems, _), (parms, (spec, (_, _, defs)))) = - prep false true context raw_import raw_elems []; + val ((fixed, deps, elems, _), (parms, ctxt')) = prep false true context raw_import raw_elems []; (* Declare parameters and imported facts *) val context' = context |> ProofContext.add_fixes_i fixed |> snd |> - NewLocale.clear_local_idents |> fold NewLocale.activate_local_facts deps; - val ((elems', _), _) = activate elems (ProofContext.set_stmt true context'); - in ((fixed, deps, elems'), (parms, spec, defs)) end; + fold NewLocale.activate_local_facts deps; + val (elems', _) = activate elems (ProofContext.set_stmt true context'); + in ((fixed, deps, elems'), (parms, ctxt')) end; in @@ -521,7 +459,7 @@ val export = Variable.export_morphism goal_ctxt context; val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export; - val exp_term = Drule.term_rule thy (singleton exp_fact); + val exp_term = TermSubst.zero_var_indexes o Morphism.term export; val exp_typ = Logic.type_map exp_term; val export' = Morphism.morphism {binding = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact}; @@ -537,6 +475,81 @@ (*** Locale declarations ***) +(* extract specification text *) + +val norm_term = Envir.beta_norm oo Term.subst_atomic; + +fun bind_def ctxt eq (xs, env, eqs) = + let + val _ = LocalDefs.cert_def ctxt eq; + val ((y, T), b) = LocalDefs.abs_def eq; + val b' = norm_term env b; + fun err msg = error (msg ^ ": " ^ quote y); + in + case filter (fn (Free (y', _), _) => y = y' | _ => false) env of + [] => (Term.add_frees b' xs, (Free (y, T), b') :: env, eq :: eqs) | + dups => if forall (fn (_, b'') => b' aconv b'') dups + then (xs, env, eqs) + else err "Attempt to redefine variable" + end; + +(* text has the following structure: + (((exts, exts'), (ints, ints')), (xs, env, defs)) + where + exts: external assumptions (terms in assumes elements) + exts': dito, normalised wrt. env + ints: internal assumptions (terms in assumptions from insts) + ints': dito, normalised wrt. env + xs: the free variables in exts' and ints' and rhss of definitions, + this includes parameters except defined parameters + env: list of term pairs encoding substitutions, where the first term + is a free variable; substitutions represent defines elements and + the rhs is normalised wrt. the previous env + defs: the equations from the defines elements + *) + +fun eval_text _ _ (Fixes _) text = text + | eval_text _ _ (Constrains _) text = text + | eval_text _ is_ext (Assumes asms) + (((exts, exts'), (ints, ints')), (xs, env, defs)) = + let + val ts = maps (map #1 o #2) asms; + val ts' = map (norm_term env) ts; + val spec' = + if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints')) + else ((exts, exts'), (ints @ ts, ints' @ ts')); + in (spec', (fold Term.add_frees ts' xs, env, defs)) end + | eval_text ctxt _ (Defines defs) (spec, binds) = + (spec, fold (bind_def ctxt o #1 o #2) defs binds) + | eval_text _ _ (Notes _) text = text; + +fun eval_inst ctxt (loc, morph) text = + let + val thy = ProofContext.theory_of ctxt; + val (asm, defs) = NewLocale.specification_of thy loc; + val asm' = Option.map (Morphism.term morph) asm; + val defs' = map (Morphism.term morph) defs; + val text' = text |> + (if is_some asm + then eval_text ctxt false (Assumes [(Attrib.empty_binding, [(the asm', [])])]) + else I) |> + (if not (null defs) + then eval_text ctxt false (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs')) + else I) +(* FIXME clone from new_locale.ML *) + in text' end; + +fun eval_elem ctxt elem text = + let + val text' = eval_text ctxt true elem text; + in text' end; + +fun eval ctxt deps elems = + let + val text' = fold (eval_inst ctxt) deps ((([], []), ([], [])), ([], [], [])); + val ((spec, (_, _, defs))) = fold (eval_elem ctxt) elems text'; + in (spec, defs) end; + (* axiomsN: name of theorem set with destruct rules for locale predicates, also name suffix of delta predicates and assumptions. *) @@ -622,7 +635,7 @@ (* CB: main predicate definition function *) -fun define_preds pname (parms, ((exts, exts'), (ints, ints')), defs) thy = +fun define_preds pname parms (((exts, exts'), (ints, ints')), defs) thy = let val defs' = map (cterm_of thy #> Assumption.assume #> Drule.gen_all #> Drule.abs_def) defs; @@ -675,7 +688,8 @@ fun defines_to_notes thy (Defines defs) = Notes (Thm.definitionK, map (fn (a, (def, _)) => - (a, [([Assumption.assume (cterm_of thy def)], [])])) defs) + (a, [([Assumption.assume (cterm_of thy def)], + [(Attrib.internal o K) NewLocale.witness_attrib])])) defs) | defines_to_notes _ e = e; fun gen_add_locale prep_decl @@ -685,10 +699,12 @@ val _ = NewLocale.test_locale thy name andalso error ("Duplicate definition of locale " ^ quote name); - val ((fixed, deps, body_elems), text as (parms, ((_, exts'), _), defs)) = + val ((fixed, deps, body_elems), (parms, ctxt')) = prep_decl raw_imprt raw_body (ProofContext.init thy); + val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems; + val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') = - define_preds predicate_name text thy; + define_preds predicate_name parms text thy; val extraTs = fold Term.add_tfrees exts' [] \\ fold Term.add_tfreesT (map snd parms) []; val _ = if null extraTs then () @@ -786,33 +802,63 @@ local -fun gen_interpretation prep_expr - expression thy = +datatype goal = Reg of string * Morphism.morphism | Eqns of Attrib.binding list; + +fun gen_interpretation prep_expr parse_prop prep_attr + expression equations thy = let val ctxt = ProofContext.init thy; - val ((propss, regs, export), goal_ctxt) = prep_expr expression ctxt; + val ((propss, regs, export), expr_ctxt) = prep_expr expression ctxt; - fun store_reg ((name, morph), thms) = - let - val morph' = morph $> Element.satisfy_morphism thms $> export; - in - NewLocale.add_global_registration (name, morph') #> - NewLocale.activate_global_facts (name, morph') - end; + val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt; + val eq_attns = map ((apsnd o map) (prep_attr thy) o fst) equations; + val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt; + val export' = Variable.export_morphism goal_ctxt expr_ctxt; + + fun store (Reg (name, morph), thms) (regs, thy) = + let + val thms' = map (Element.morph_witness export') thms; + val morph' = morph $> Element.satisfy_morphism thms'; + val add = NewLocale.add_global_registration (name, (morph', export)); + in ((name, morph') :: regs, add thy) end + | store (Eqns [], []) (regs, thy) = + let val add = fold_rev (fn (name, morph) => + NewLocale.activate_global_facts (name, morph $> export)) regs; + in (regs, add thy) end + | store (Eqns attns, thms) (regs, thy) = + let + val thms' = thms |> map (Element.conclude_witness #> + Morphism.thm (export' $> export) #> + LocalDefs.meta_rewrite_rule (ProofContext.init thy) #> + Drule.abs_def); + val eq_morph = + Morphism.term_morphism (MetaSimplifier.rewrite_term thy thms' []) $> + Morphism.thm_morphism (MetaSimplifier.rewrite_rule thms'); + val attns' = map ((apsnd o map) (Attrib.attribute_i thy)) attns; + val add = + fold_rev (fn (name, morph) => + NewLocale.amend_global_registration eq_morph (name, morph) #> + NewLocale.activate_global_facts (name, morph $> eq_morph $> export)) regs #> + PureThy.note_thmss Thm.lemmaK (attns' ~~ map (fn th => [([th], [])]) thms') #> + snd + in (regs, add thy) end; fun after_qed results = - ProofContext.theory (fold store_reg (regs ~~ prep_result propss results)); + ProofContext.theory (fn thy => + fold store (map Reg regs @ [Eqns eq_attns] ~~ + prep_result (propss @ [eqns]) results) ([], thy) |> snd); in goal_ctxt |> - Proof.theorem_i NONE after_qed (prep_propp propss) |> + Proof.theorem_i NONE after_qed (prep_propp (propss @ [eqns])) |> Element.refine_witness |> Seq.hd end; in -fun interpretation_cmd x = gen_interpretation read_goal_expression x; -fun interpretation x = gen_interpretation cert_goal_expression x; +fun interpretation_cmd x = gen_interpretation read_goal_expression + Syntax.parse_prop Attrib.intern_src x; +fun interpretation x = gen_interpretation cert_goal_expression (K I) (K I) x; end; diff -r 7dc7a75033ea -r ea97aa6aeba2 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Mon Dec 29 22:43:41 2008 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Tue Dec 30 11:10:01 2008 +0100 @@ -53,8 +53,7 @@ val print_configs: Toplevel.transition -> Toplevel.transition val print_theorems: Toplevel.transition -> Toplevel.transition val print_locales: Toplevel.transition -> Toplevel.transition - val print_locale: bool * (Locale.expr * Element.context list) - -> Toplevel.transition -> Toplevel.transition + val print_locale: bool * xstring -> Toplevel.transition -> Toplevel.transition val print_registrations: bool -> string -> Toplevel.transition -> Toplevel.transition val print_attributes: Toplevel.transition -> Toplevel.transition val print_simpset: Toplevel.transition -> Toplevel.transition @@ -355,11 +354,11 @@ val print_theorems = Toplevel.unknown_context o print_theorems_theory o print_theorems_proof; val print_locales = Toplevel.unknown_theory o - Toplevel.keep (Locale.print_locales o Toplevel.theory_of); + Toplevel.keep (NewLocale.print_locales o Toplevel.theory_of); -fun print_locale (show_facts, (imports, body)) = Toplevel.unknown_theory o +fun print_locale (show_facts, name) = Toplevel.unknown_theory o Toplevel.keep (fn state => - Locale.print_locale (Toplevel.theory_of state) show_facts imports body); + NewLocale.print_locale (Toplevel.theory_of state) show_facts name); fun print_registrations show_wits name = Toplevel.unknown_context o Toplevel.keep (Toplevel.node_case diff -r 7dc7a75033ea -r ea97aa6aeba2 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Mon Dec 29 22:43:41 2008 +0100 +++ b/src/Pure/Isar/isar_syn.ML Tue Dec 30 11:10:01 2008 +0100 @@ -385,18 +385,18 @@ (* locales *) val locale_val = - SpecParse.locale_expr -- + SpecParse.locale_expression -- Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] || - Scan.repeat1 SpecParse.context_element >> pair Locale.empty; + Scan.repeat1 SpecParse.context_element >> pair ([], []); val _ = OuterSyntax.command "locale" "define named proof context" K.thy_decl - (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, []) -- P.opt_begin + (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (([], []), []) -- P.opt_begin >> (fn ((name, (expr, elems)), begin) => (begin ? Toplevel.print) o Toplevel.begin_local_theory begin - (Locale.add_locale_cmd name expr elems #-> TheoryTarget.begin))); - -val opt_prefix = Scan.optional (P.binding --| P.$$$ ":") Binding.empty; + (Expression.add_locale_cmd name name expr elems #> + (fn ((target, notes), ctxt) => TheoryTarget.begin target ctxt |> + fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes)))); val _ = OuterSyntax.command "sublocale" @@ -407,6 +407,40 @@ 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))); + +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))); + +local + +val opt_prefix = Scan.optional (P.binding --| P.$$$ ":") Binding.empty; + +in + +val locale_val = + SpecParse.locale_expr -- + Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] || + Scan.repeat1 SpecParse.context_element >> pair Locale.empty; + +val _ = + OuterSyntax.command "class_locale" "define named proof context based on classes" K.thy_decl + (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, []) -- P.opt_begin + >> (fn ((name, (expr, elems)), begin) => + (begin ? Toplevel.print) o Toplevel.begin_local_theory begin + (Locale.add_locale_cmd name expr elems #-> TheoryTarget.begin))); + +val _ = + OuterSyntax.command "class_interpretation" "prove and register interpretation of locale expression in theory or locale" K.thy_goal (P.xname --| (P.$$$ "\\" || P.$$$ "<") -- P.!!! SpecParse.locale_expr >> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale I)) || @@ -416,7 +450,7 @@ (Locale.interpretation_cmd (Binding.base_name name) expr insts))); val _ = - OuterSyntax.command "interpret" + OuterSyntax.command "class_interpret" "prove and register interpretation of locale expression in proof context" (K.tag_proof K.prf_goal) (opt_prefix -- SpecParse.locale_expr -- SpecParse.locale_insts @@ -424,6 +458,8 @@ Toplevel.proof' (fn int => Locale.interpret_cmd (Binding.base_name name) expr insts int))); +end; + (* classes *) @@ -817,7 +853,7 @@ val _ = OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag - (opt_bang -- locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale)); + (opt_bang -- P.xname >> (Toplevel.no_timing oo IsarCmd.print_locale)); val _ = OuterSyntax.improper_command "print_interps" diff -r 7dc7a75033ea -r ea97aa6aeba2 src/Pure/Isar/new_locale.ML --- a/src/Pure/Isar/new_locale.ML Mon Dec 29 22:43:41 2008 +0100 +++ b/src/Pure/Isar/new_locale.ML Tue Dec 30 11:10:01 2008 +0100 @@ -47,9 +47,11 @@ val unfold_attrib: attribute val intro_locales_tac: bool -> Proof.context -> thm list -> tactic - (* Identifiers and registrations *) - val clear_local_idents: Proof.context -> Proof.context - val add_global_registration: (string * Morphism.morphism) -> theory -> theory + (* Registrations *) + val add_global_registration: (string * (Morphism.morphism * Morphism.morphism)) -> + theory -> theory + val amend_global_registration: Morphism.morphism -> (string * Morphism.morphism) -> + theory -> theory val get_global_registrations: theory -> (string * Morphism.morphism) list (* Diagnostic *) @@ -223,12 +225,10 @@ 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; -val clear_global_idents = put_global_idents empty; 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; -val clear_local_idents = put_local_idents empty; end; @@ -287,18 +287,18 @@ fold_rev (fn (decl, _) => Context.proof_map (decl morph)) term_decls end; -fun activate_notes activ_elem thy (name, morph) input = +fun activate_notes activ_elem transfer thy (name, morph) input = let val Loc {notes, ...} = the_locale thy name; fun activate ((kind, facts), _) input = let - val facts' = facts |> Element.facts_map (Element.morph_ctxt morph) + val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph)) in activ_elem (Notes (kind, facts')) input end; in fold_rev activate notes input end; -fun activate_all name thy activ_elem (marked, input) = +fun activate_all name thy activ_elem transfer (marked, input) = let val Loc {parameters = (_, params), spec = (asm, defs), ...} = the_locale thy name; @@ -310,7 +310,7 @@ (if not (null defs) then activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs)) else I) |> - pair marked |> roundup thy (activate_notes activ_elem) (name, Morphism.identity) + pair marked |> roundup thy (activate_notes activ_elem transfer) (name, Morphism.identity) end; @@ -354,15 +354,19 @@ roundup thy activate_decls dep (get_local_idents ctxt, ctxt) |> uncurry put_local_idents; fun activate_global_facts dep thy = - roundup thy (activate_notes init_global_elem) dep (get_global_idents thy, thy) |> + roundup thy (activate_notes init_global_elem Element.transfer_morphism) + dep (get_global_idents thy, thy) |> uncurry put_global_idents; fun activate_local_facts dep ctxt = - roundup (ProofContext.theory_of ctxt) (activate_notes init_local_elem) dep + roundup (ProofContext.theory_of ctxt) + (activate_notes init_local_elem (Element.transfer_morphism o ProofContext.theory_of)) dep (get_local_idents ctxt, ctxt) |> uncurry put_local_idents; -fun init name thy = activate_all name thy init_local_elem (empty, ProofContext.init thy) |> +fun init name thy = + activate_all name thy init_local_elem (Element.transfer_morphism o ProofContext.theory_of) + (empty, ProofContext.init thy) |> uncurry put_local_idents; fun print_locale thy show_facts name = @@ -371,25 +375,74 @@ val ctxt = init name' thy in Pretty.big_list "locale elements:" - (activate_all name' thy (cons_elem show_facts) (empty, []) |> snd |> rev |> + (activate_all name' thy (cons_elem show_facts) (K (Element.transfer_morphism thy)) + (empty, []) |> snd |> rev |> map (Element.pretty_ctxt ctxt) |> map Pretty.chunks) |> Pretty.writeln end end; +(*** Registrations: interpretations in theories ***) + +(* FIXME only global variant needed *) +structure RegistrationsData = GenericDataFun +( + type T = ((string * (Morphism.morphism * Morphism.morphism)) * stamp) list; +(* FIXME mixins need to be stamped *) + (* registrations, in reverse order of declaration *) + val empty = []; + val extend = I; + fun merge _ = Library.merge (eq_snd (op =)); + (* FIXME consolidate with dependencies, consider one data slot only *) +); + +val get_global_registrations = + Context.Theory #> RegistrationsData.get #> map fst #> map (apsnd op $>); + +fun add_global reg = + (Context.theory_map o RegistrationsData.map) (cons (reg, stamp ())); + +fun add_global_registration (name, (base_morph, export)) thy = + roundup thy (fn _ => fn (name', morph') => fn thy => add_global (name', (morph', export)) thy) + (name, base_morph) (get_global_idents thy, thy) |> + snd (* FIXME ?? uncurry put_global_idents *); + +fun amend_global_registration morph (name, base_morph) thy = + let + val regs = (Context.Theory #> RegistrationsData.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'); + val i = find_index match (rev regs); + val _ = if i = ~1 then error ("No interpretation of locale " ^ + quote (extern thy name) ^ " and parameter instantiation " ^ + space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available.") + else (); + in + (Context.theory_map o RegistrationsData.map) (nth_map (length regs - 1 - i) + (fn ((name, (base, export)), stamp) => ((name, (base $> morph, export)), stamp))) thy + end; + + (*** Storing results ***) (* Theorems *) fun add_thmss loc kind args ctxt = let - val (([Notes args'], _), ctxt') = Element.activate_i [Notes (kind, args)] ctxt; - val ctxt'' = ctxt' |> ProofContext.theory - (change_locale loc + val ([Notes args'], ctxt') = Element.activate_i [Notes (kind, args)] ctxt; + val ctxt'' = ctxt' |> ProofContext.theory ( + change_locale loc (fn (parameters, spec, decls, notes, dependencies) => - (parameters, spec, decls, (args', stamp ()) :: notes, dependencies))) - (* FIXME registrations *) + (parameters, spec, decls, (args', stamp ()) :: notes, dependencies)) #> + (* Registrations *) + (fn thy => fold_rev (fn (name, morph) => + let + val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |> + Attrib.map_facts (Attrib.attribute_i thy) + in Locale.global_note_qualified kind args'' #> snd end) + (get_global_registrations thy |> filter (fn (name, _) => name = loc)) thy)) in ctxt'' end; @@ -451,23 +504,5 @@ Locale.intro_locales_tac true ctxt)), "back-chain all introduction rules of locales")])); - -(*** Registrations: interpretations in theories ***) - -(* FIXME only global variant needed *) -structure RegistrationsData = GenericDataFun -( - type T = ((string * Morphism.morphism) * stamp) list; - (* registrations, in reverse order of declaration *) - val empty = []; - val extend = I; - fun merge _ = Library.merge (eq_snd (op =)); - (* FIXME consolidate with dependencies, consider one data slot only *) -); - -val get_global_registrations = map fst o RegistrationsData.get o Context.Theory; -fun add_global_registration reg = - (Context.theory_map o RegistrationsData.map) (cons (reg, stamp ())); - end; diff -r 7dc7a75033ea -r ea97aa6aeba2 src/Pure/Isar/spec_parse.ML --- a/src/Pure/Isar/spec_parse.ML Mon Dec 29 22:43:41 2008 +0100 +++ b/src/Pure/Isar/spec_parse.ML Tue Dec 30 11:10:01 2008 +0100 @@ -104,7 +104,7 @@ val rename = P.name -- Scan.option P.mixfix; -val prefix = P.name --| 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 || @@ -127,7 +127,7 @@ val locale_expression = let fun expr2 x = P.xname x; - fun expr1 x = (Scan.optional prefix "" -- expr2 -- + 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; in expr0 -- Scan.optional (P.$$$ "for" |-- P.!!! locale_fixes) [] end; diff -r 7dc7a75033ea -r ea97aa6aeba2 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Mon Dec 29 22:43:41 2008 +0100 +++ b/src/Pure/Isar/specification.ML Tue Dec 30 11:10:01 2008 +0100 @@ -59,18 +59,6 @@ structure Specification: SPECIFICATION = struct -(* new locales *) - -fun cert_stmt body concl ctxt = - let val (_, _, ctxt', concl') = Locale.cert_context_statement NONE body concl ctxt - in (concl', ctxt') end; -fun read_stmt body concl ctxt = - let val (_, _, ctxt', concl') = Locale.read_context_statement NONE body concl ctxt - in (concl', ctxt') end; - -fun cert_context_statement x = if !new_locales then Expression.cert_statement x else cert_stmt x; -fun read_context_statement x = if !new_locales then Expression.read_statement x else read_stmt x; - (* diagnostics *) fun print_consts _ _ [] = () @@ -370,8 +358,8 @@ in -val theorem = gen_theorem (K I) cert_context_statement; -val theorem_cmd = gen_theorem Attrib.intern_src read_context_statement; +val theorem = gen_theorem (K I) Expression.cert_statement; +val theorem_cmd = gen_theorem Attrib.intern_src Expression.read_statement; fun add_theorem_hook f = TheoremHook.map (cons (f, stamp ())); diff -r 7dc7a75033ea -r ea97aa6aeba2 src/Pure/Isar/subclass.ML --- a/src/Pure/Isar/subclass.ML Mon Dec 29 22:43:41 2008 +0100 +++ b/src/Pure/Isar/subclass.ML Tue Dec 30 11:10:01 2008 +0100 @@ -1,5 +1,4 @@ (* Title: Pure/Isar/subclass.ML - ID: $Id$ Author: Florian Haftmann, TU Muenchen User interface for proving subclass relationship between type classes. @@ -22,7 +21,7 @@ val thy = ProofContext.theory_of lthy; val sup = prep_class thy raw_sup; val sub = case TheoryTarget.peek lthy - of {is_class = false, ...} => error "No class context" + of {is_class = false, ...} => error "Not a class context" | {target, ...} => target; val _ = if Sign.subsort thy ([sup], [sub]) then error ("Class " ^ Syntax.string_of_sort lthy [sup] diff -r 7dc7a75033ea -r ea97aa6aeba2 src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Mon Dec 29 22:43:41 2008 +0100 +++ b/src/Pure/Isar/theory_target.ML Tue Dec 30 11:10:01 2008 +0100 @@ -6,7 +6,7 @@ signature THEORY_TARGET = sig - val peek: local_theory -> {target: string, is_locale: bool, + val peek: local_theory -> {target: string, new_locale: bool, is_locale: bool, is_class: bool, instantiation: string list * (string * sort) list * sort, overloading: (string * (string * typ) * bool) list} val init: string option -> theory -> local_theory @@ -22,25 +22,32 @@ (* new locales *) -fun locale_extern x = if !new_locales then NewLocale.extern x else Locale.extern x; -fun locale_add_type_syntax x = if !new_locales then NewLocale.add_type_syntax x else Locale.add_type_syntax x; -fun locale_add_term_syntax x = if !new_locales then NewLocale.add_term_syntax x else Locale.add_term_syntax x; -fun locale_add_declaration x = if !new_locales then NewLocale.add_declaration x else Locale.add_declaration x; -fun locale_add_thmss x = if !new_locales then NewLocale.add_thmss x else Locale.add_thmss x; -fun locale_init x = if !new_locales then NewLocale.init x else Locale.init x; -fun locale_intern x = if !new_locales then NewLocale.intern x else Locale.intern x; +fun locale_extern new_locale x = + if new_locale then NewLocale.extern x else Locale.extern x; +fun locale_add_type_syntax new_locale x = + if new_locale then NewLocale.add_type_syntax x else Locale.add_type_syntax x; +fun locale_add_term_syntax new_locale x = + if new_locale then NewLocale.add_term_syntax x else Locale.add_term_syntax x; +fun locale_add_declaration new_locale x = + if new_locale then NewLocale.add_declaration x else Locale.add_declaration x; +fun locale_add_thmss new_locale x = + if new_locale then NewLocale.add_thmss x else Locale.add_thmss x; +fun locale_init new_locale x = + if new_locale then NewLocale.init x else Locale.init x; +fun locale_intern new_locale x = + if new_locale then NewLocale.intern x else Locale.intern x; (* context data *) -datatype target = Target of {target: string, is_locale: bool, +datatype target = Target of {target: string, new_locale: bool, is_locale: bool, is_class: bool, instantiation: string list * (string * sort) list * sort, overloading: (string * (string * typ) * bool) list}; -fun make_target target is_locale is_class instantiation overloading = - Target {target = target, is_locale = is_locale, +fun make_target target new_locale is_locale is_class instantiation overloading = + Target {target = target, new_locale = new_locale, is_locale = is_locale, is_class = is_class, instantiation = instantiation, overloading = overloading}; -val global_target = make_target "" false false ([], [], []) []; +val global_target = make_target "" false false false ([], [], []) []; structure Data = ProofDataFun ( @@ -56,7 +63,7 @@ fun pretty_thy ctxt target is_locale is_class = let val thy = ProofContext.theory_of ctxt; - val target_name = (if is_class then "class " else "locale ") ^ locale_extern thy target; + val target_name = (if is_class then "class " else "locale ") ^ locale_extern is_class thy target; val fixes = map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt)); val assumes = map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])])) @@ -71,7 +78,7 @@ (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)] end; -fun pretty (Target {target, is_locale, is_class, instantiation, overloading}) ctxt = +fun pretty (Target {target, is_locale, is_class, instantiation, overloading, ...}) ctxt = Pretty.block [Pretty.str "theory", Pretty.brk 1, Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] :: (if not (null overloading) then [Overloading.pretty ctxt] @@ -81,7 +88,7 @@ (* target declarations *) -fun target_decl add (Target {target, is_class, ...}) d lthy = +fun target_decl add (Target {target, new_locale, ...}) d lthy = let val d' = Morphism.transform (LocalTheory.target_morphism lthy) d; val d0 = Morphism.form d'; @@ -92,7 +99,7 @@ |> LocalTheory.target (Context.proof_map d0) else lthy - |> LocalTheory.target (add target d') + |> LocalTheory.target (add new_locale target d') end; val type_syntax = target_decl locale_add_type_syntax; @@ -158,7 +165,7 @@ |> ProofContext.note_thmss_i kind facts ||> ProofContext.restore_naming ctxt; -fun notes (Target {target, is_locale, is_class, ...}) kind facts lthy = +fun notes (Target {target, is_locale, new_locale, ...}) kind facts lthy = let val thy = ProofContext.theory_of lthy; val facts' = facts @@ -177,7 +184,7 @@ #> PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd #> Sign.restore_naming thy) |> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd) - |> is_locale ? LocalTheory.target (locale_add_thmss target kind target_facts) + |> is_locale ? LocalTheory.target (locale_add_thmss new_locale target kind target_facts) |> note_local kind local_facts end; @@ -326,13 +333,14 @@ fun init_target _ NONE = global_target | init_target thy (SOME target) = - make_target target true (Class.is_class thy target) ([], [], []) []; + make_target target (NewLocale.test_locale thy (NewLocale.intern thy target)) + true (Class.is_class thy target) ([], [], []) []; -fun init_ctxt (Target {target, is_locale, is_class, instantiation, overloading}) = +fun init_ctxt (Target {target, new_locale, is_locale, is_class, instantiation, overloading}) = if not (null (#1 instantiation)) then Class.init_instantiation instantiation else if not (null overloading) then Overloading.init overloading else if not is_locale then ProofContext.init - else if not is_class then locale_init target + else if not is_class then locale_init new_locale target else Class.init target; fun init_lthy (ta as Target {target, instantiation, overloading, ...}) = @@ -357,7 +365,7 @@ val ctxt = ProofContext.init thy; val ops = raw_ops |> map (fn (name, const, checked) => (name, Term.dest_Const (prep_const ctxt const), checked)); - in thy |> init_lthy_ctxt (make_target "" false false ([], [], []) ops) end; + in thy |> init_lthy_ctxt (make_target "" false false false ([], [], []) ops) end; in @@ -365,9 +373,10 @@ fun begin target ctxt = init_lthy (init_target (ProofContext.theory_of ctxt) (SOME target)) ctxt; fun context "-" thy = init NONE thy - | context target thy = init (SOME (locale_intern thy target)) thy; + | context target thy = init (SOME (locale_intern + (NewLocale.test_locale thy (NewLocale.intern thy target)) thy target)) thy; -fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []); +fun instantiation arities = init_lthy_ctxt (make_target "" false false false arities []); val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const); val overloading_cmd = gen_overloading Syntax.read_term; diff -r 7dc7a75033ea -r ea97aa6aeba2 src/Pure/consts.ML --- a/src/Pure/consts.ML Mon Dec 29 22:43:41 2008 +0100 +++ b/src/Pure/consts.ML Tue Dec 30 11:10:01 2008 +0100 @@ -275,8 +275,8 @@ val T = Term.fastype_of rhs; val lhs = Const (NameSpace.full_name naming b, T); - fun err msg = error (msg ^ " on rhs of abbreviation:\n" ^ - Pretty.string_of_term pp (Logic.mk_equals (lhs, rhs))); + fun err msg = (warning (* FIXME should be error *) (msg ^ " on rhs of abbreviation:\n" ^ + Pretty.string_of_term pp (Logic.mk_equals (lhs, rhs))); true); val _ = Term.exists_subterm Term.is_Var rhs andalso err "Illegal schematic variables"; val _ = null (Term.hidden_polymorphism rhs) orelse err "Extra type variables"; in diff -r 7dc7a75033ea -r ea97aa6aeba2 src/Pure/library.ML --- a/src/Pure/library.ML Mon Dec 29 22:43:41 2008 +0100 +++ b/src/Pure/library.ML Tue Dec 30 11:10:01 2008 +0100 @@ -1,5 +1,4 @@ (* Title: Pure/library.ML - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Author: Markus Wenzel, TU Muenchen @@ -491,7 +490,7 @@ | split_last [x] = ([], x) | split_last (x :: xs) = apfst (cons x) (split_last xs); -(*find the position of an element in a list*) +(*find position of first element satisfying a predicate*) fun find_index pred = let fun find (_: int) [] = ~1 | find n (x :: xs) = if pred x then n else find (n + 1) xs; diff -r 7dc7a75033ea -r ea97aa6aeba2 src/ZF/Constructible/L_axioms.thy --- a/src/ZF/Constructible/L_axioms.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/ZF/Constructible/L_axioms.thy Tue Dec 30 11:10:01 2008 +0100 @@ -1,5 +1,4 @@ (* Title: ZF/Constructible/L_axioms.thy - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory *) @@ -100,7 +99,7 @@ apply (rule L_nat) done -interpretation 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 7dc7a75033ea -r ea97aa6aeba2 src/ZF/Constructible/Rec_Separation.thy --- a/src/ZF/Constructible/Rec_Separation.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/ZF/Constructible/Rec_Separation.thy Tue Dec 30 11:10:01 2008 +0100 @@ -1,5 +1,4 @@ (* Title: ZF/Constructible/Rec_Separation.thy - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory *) @@ -186,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 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}*} @@ -373,7 +372,7 @@ apply (rule M_datatypes_axioms_L) done -interpretation 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}*} @@ -436,7 +435,7 @@ apply (rule M_eclose_axioms_L) done -interpretation M_eclose [L] by (rule M_eclose_L) +interpretation L: M_eclose L by (rule M_eclose_L) end diff -r 7dc7a75033ea -r ea97aa6aeba2 src/ZF/Constructible/Separation.thy --- a/src/ZF/Constructible/Separation.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/ZF/Constructible/Separation.thy Tue Dec 30 11:10:01 2008 +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 M_basic [L] by (rule M_basic_L) +interpretation L: M_basic L by (rule M_basic_L) end diff -r 7dc7a75033ea -r ea97aa6aeba2 src/ZF/ROOT.ML diff -r 7dc7a75033ea -r ea97aa6aeba2 src/ZF/ex/Group.thy --- a/src/ZF/ex/Group.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/ZF/ex/Group.thy Tue Dec 30 11:10:01 2008 +0100 @@ -1,5 +1,4 @@ (* Title: ZF/ex/Group.thy - Id: $Id$ *) @@ -40,7 +39,7 @@ m_inv :: "i => i => i" ("inv\ _" [81] 80) where "inv\<^bsub>G\<^esub> x == (THE y. y \ carrier(G) & y \\<^bsub>G\<^esub> x = \\<^bsub>G\<^esub> & x \\<^bsub>G\<^esub> y = \\<^bsub>G\<^esub>)" -locale monoid = struct G + +locale monoid = fixes G (structure) assumes m_closed [intro, simp]: "\x \ carrier(G); y \ carrier(G)\ \ x \ y \ carrier(G)" and m_assoc: @@ -242,7 +241,7 @@ subsection {* Substructures *} -locale subgroup = var H + struct G + +locale subgroup = fixes H and G (structure) assumes subset: "H \ carrier(G)" and m_closed [intro, simp]: "\x \ H; y \ H\ \ x \ y \ H" and one_closed [simp]: "\ \ H" @@ -262,7 +261,7 @@ assumes "group(G)" shows "group_axioms (update_carrier(G,H))" proof - - interpret group [G] by fact + interpret group G by fact show ?thesis by (force intro: group_axioms.intro l_inv r_inv) qed @@ -270,7 +269,7 @@ assumes "group(G)" shows "group (update_carrier(G,H))" proof - - interpret group [G] by fact + interpret group G by fact show ?thesis by (rule groupI) (auto intro: m_assoc l_inv mem_carrier) qed @@ -316,8 +315,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 (force intro!: groupI G.m_assoc H.m_assoc G.l_inv H.l_inv simp add: DirProdGroup_def) qed @@ -397,8 +396,8 @@ assumes "group(G)" and "group(H)" shows "(\ \ carrier(G \ H). ) \ (G \ H) \ (H \ G)" proof - - interpret group [G] by fact - interpret group [H] by fact + interpret group G by fact + interpret group H by fact show ?thesis by (auto simp add: iso_def hom_def inj_def surj_def bij_def) qed @@ -407,16 +406,17 @@ shows "(\<,z> \ carrier((G \ H) \ I). >) \ ((G \ H) \ I) \ (G \ (H \ I))" proof - - interpret group [G] by fact - interpret group [H] by fact - interpret group [I] by fact + interpret group G by fact + interpret group H by fact + interpret group I by fact show ?thesis by (auto intro: lam_type simp add: iso_def hom_def inj_def surj_def bij_def) qed text{*Basis for homomorphism proofs: we assume two groups @{term G} and @term{H}, with a homomorphism @{term h} between them*} -locale group_hom = group G + group H + var h + +locale group_hom = G: group G + H: group H + for G (structure) and H (structure) and h + assumes homh: "h \ hom(G,H)" notes hom_mult [simp] = hom_mult [OF homh] and hom_closed [simp] = hom_closed [OF homh] @@ -870,7 +870,7 @@ assumes "group(G)" shows "equiv (carrier(G), rcong H)" proof - - interpret group [G] by fact + interpret group G by fact show ?thesis proof (simp add: equiv_def, intro conjI) show "rcong H \ carrier(G) \ carrier(G)" by (auto simp add: r_congruent_def) @@ -907,7 +907,7 @@ assumes a: "a \ carrier(G)" shows "a <# H = (rcong H) `` {a}" proof - - interpret group [G] by fact + interpret group G by fact show ?thesis by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a Collect_image_eq) @@ -920,7 +920,7 @@ h \ H; ha \ H; hb \ H\ \ hb \ a \ (\h\H. {h \ b})" (is "PROP ?P") proof - - interpret subgroup [H G] by fact + interpret subgroup H G by fact show "PROP ?P" apply (rule UN_I [of "hb \ ((inv ha) \ h)"], simp) apply (simp add: m_assoc transpose_inv) @@ -931,7 +931,7 @@ assumes "subgroup(H, G)" shows "\a \ rcosets H; b \ rcosets H; a\b\ \ a \ b = 0" (is "PROP ?P") proof - - interpret subgroup [H G] by fact + interpret subgroup H G by fact show "PROP ?P" apply (simp add: RCOSETS_def r_coset_def) apply (blast intro: rcos_equation prems sym) @@ -949,7 +949,7 @@ assumes "subgroup(H, G)" shows "x \ carrier(G) \ x \ H #> x" (is "PROP ?P") proof - - interpret subgroup [H G] by fact + interpret subgroup H G by fact show "PROP ?P" apply (simp add: r_coset_def) apply (rule_tac x="\" in bexI) apply (auto) @@ -960,7 +960,7 @@ assumes "subgroup(H, G)" shows "\(rcosets H) = carrier(G)" proof - - interpret subgroup [H G] by fact + interpret subgroup H G by fact show ?thesis apply (rule equalityI) apply (force simp add: RCOSETS_def r_coset_def) @@ -1044,7 +1044,7 @@ assumes "group(G)" shows "H \ rcosets H" proof - - interpret group [G] by fact + interpret group G by fact have "H #> \ = H" using _ subgroup_axioms by (rule coset_join2) simp_all then show ?thesis diff -r 7dc7a75033ea -r ea97aa6aeba2 src/ZF/ex/Ring.thy --- a/src/ZF/ex/Ring.thy Mon Dec 29 22:43:41 2008 +0100 +++ b/src/ZF/ex/Ring.thy Tue Dec 30 11:10:01 2008 +0100 @@ -45,7 +45,7 @@ minus :: "[i,i,i] => i" (infixl "\\" 65) where "\x \ carrier(R); y \ carrier(R)\ \ x \\<^bsub>R\<^esub> y = x \\<^bsub>R\<^esub> (\\<^bsub>R\<^esub> y)" -locale abelian_monoid = struct G + +locale abelian_monoid = fixes G (structure) assumes a_comm_monoid: "comm_monoid ()" @@ -57,7 +57,7 @@ assumes a_comm_group: "comm_group ()" -locale ring = abelian_group R + monoid R + +locale ring = abelian_group R + monoid R for R (structure) + assumes l_distr: "\x \ carrier(R); y \ carrier(R); z \ carrier(R)\ \ (x \ y) \ z = x \ z \ y \ z" and r_distr: "\x \ carrier(R); y \ carrier(R); z \ carrier(R)\ @@ -262,7 +262,8 @@ lemma ring_hom_one: "h \ ring_hom(R,S) \ h ` \\<^bsub>R\<^esub> = \\<^bsub>S\<^esub>" by (simp add: ring_hom_def) -locale ring_hom_cring = cring R + cring S + var h + +locale ring_hom_cring = R: cring R + S: cring S + for R (structure) and S (structure) and h + assumes homh [simp, intro]: "h \ ring_hom(R,S)" notes hom_closed [simp, intro] = ring_hom_closed [OF homh] and hom_mult [simp] = ring_hom_mult [OF homh]