Merged.
--- 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"))
--- 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 \
--- 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: <no prefix>, 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: <no prefix>, 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: <no prefix>, i1 *)
-print_interps IB (* output: i1 *)
-print_interps IC (* output: <no prefix, i1 *)
-print_interps ID (* output: i2, i3 *)
-
-
-interpretation i10: ID + ID a' b' d' [X "Y::i" _ u "v::i" _] by intro_locales
-
-corollary (in ID) th_x: True ..
-
-(* possible accesses: for each registration *)
-
-thm i2.th_x thm i3.th_x
-
-ML {* check_thm "i2.th_x"; check_thm "i3.th_x" *}
-
-lemma (in ID) th_y: "d == (a = b)" by (rule d_def)
-
-thm i2.th_y thm i3.th_y
-
-ML {* check_thm "i2.th_y"; check_thm "i3.th_y" *}
-
-lemmas (in ID) th_z = th_y
-
-thm i2.th_z
-
-ML {* check_thm "i2.th_z" *}
-
-
-subsection {* Interpretation in Proof Contexts *}
-
-locale IF = fixes f assumes asm_F: "f & f --> 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: <no prefix>, i1 *)
- interpret i6: IC [alpha beta] by unfold_locales auto
- print_interps IA (* output: <no prefix>, i1 *)
- print_interps IC (* output: <no prefix>, 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
--- 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"
--- 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
--- 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";
--- 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 \<equiv> kernel \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>
\<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> 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 \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
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 \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
lemma (in abelian_subgroup) is_abelian_subgroup:
@@ -230,7 +232,7 @@
and a_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<oplus>\<^bsub>G\<^esub> y = y \<oplus>\<^bsub>G\<^esub> x"
shows "abelian_subgroup H G"
proof -
- interpret normal ["H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"]
+ interpret normal "H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
by (rule a_normal)
show "abelian_subgroup H G"
@@ -243,9 +245,9 @@
and a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
shows "abelian_subgroup H G"
proof -
- interpret comm_group ["\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"]
+ interpret comm_group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
by (rule a_comm_group)
- interpret subgroup ["H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"]
+ interpret subgroup "H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
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 \<in> carrier G" "x' \<in> carrier G"
shows "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)"
proof -
- interpret G: ring [G] by fact
+ interpret G!: ring G by fact
from carr
have "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)" by (rule a_rcos_module)
with carr
--- a/src/HOL/Algebra/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
*)
--- 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 \<in> 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' \<in> H #> a"
shows "a' \<in> carrier G"
proof -
- interpret group [G] by fact
+ interpret group G by fact
from subset and acarr
have "H #> a \<subseteq> carrier G" by (rule r_coset_subset_G)
from this and a'
@@ -142,7 +141,7 @@
assumes hH: "h \<in> 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' \<in> H #> x"
shows "(x' \<otimes> inv x) \<in> H"
proof -
- interpret group [G] by fact
+ interpret group G by fact
from xcarr x'cos
have x'carr: "x' \<in> carrier G"
by (rule elemrcos_carrier[OF is_group])
@@ -213,7 +212,7 @@
and xixH: "(x' \<otimes> inv x) \<in> H"
shows "x' \<in> H #> x"
proof -
- interpret group [G] by fact
+ interpret group G by fact
from xixH
have "\<exists>h\<in>H. x' \<otimes> (inv x) = h" by fast
from this
@@ -244,7 +243,7 @@
assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
shows "(x' \<in> H #> x) = (x' \<otimes> inv x \<in> H)"
proof -
- interpret group [G] by fact
+ interpret group G by fact
show ?thesis proof assume "x' \<in> H #> x"
from this and carr
show "x' \<otimes> inv x \<in> H"
@@ -263,7 +262,7 @@
assumes XH: "X \<in> rcosets H"
shows "X \<subseteq> carrier G"
proof -
- interpret group [G] by fact
+ interpret group G by fact
from XH have "\<exists>x\<in> carrier G. X = H #> x"
unfolding RCOSETS_def
by fast
@@ -348,7 +347,7 @@
and xixH: "(inv x \<otimes> x') \<in> H"
shows "x' \<in> x <# H"
proof -
- interpret group [G] by fact
+ interpret group G by fact
from xixH
have "\<exists>h\<in>H. (inv x) \<otimes> 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 \<in> 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 \<otimes> a = h \<otimes> b" "a \<in> carrier G" "b \<in> carrier G" "h \<in> H" "ha \<in> H" "hb \<in> H"
shows "hb \<otimes> a \<in> (\<Union>h\<in>H. {h \<otimes> 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 \<otimes> ((inv ha) \<otimes> h)"])
apply (simp add: )
apply (simp add: m_assoc transpose_inv)
@@ -670,7 +669,7 @@
assumes p: "a \<in> rcosets H" "b \<in> rcosets H" "a\<noteq>b"
shows "a \<inter> 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 "\<Union>(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 \<in> rcosets H"
proof -
- interpret group [G] by fact
+ interpret group G by fact
from _ subgroup_axioms have "H #> \<one> = H"
by (rule coset_join2) auto
then show ?thesis
--- 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 \<subseteq> monoid_cancel
+sublocale group \<subseteq> monoid_cancel
proof qed simp+
@@ -45,7 +44,7 @@
"\<And>a b c. \<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> 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 \<otimes> c = b \<otimes> c")
@@ -59,7 +58,7 @@
"comm_monoid_cancel G"
by intro_locales
-interpretation comm_group \<subseteq> comm_monoid_cancel
+sublocale comm_group \<subseteq> 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 \<sqsubset>\<^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 \<sqsubset>\<^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' \<in> carrier G \<and> 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 \<in> carrier G" "b \<in> carrier G"
shows "somegcd G a b \<in> 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 \<in> carrier G" "b \<in> 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 \<in> carrier G \<and> (somegcd G a b) gcdof a b"
apply (subst gcdof_greatestLower, simp, simp)
@@ -2983,7 +2982,7 @@
assumes carr: "a \<in> carrier G" "b \<in> carrier G"
shows "\<exists>x\<in>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 \<in> carrier G" "b \<in> 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 \<in> carrier G" "b \<in> 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 \<in> carrier G" "y \<in> carrier G" "z \<in> 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 \<in> carrier G" "x' \<in> carrier G" "y \<in> carrier G"
shows "somegcd G x y \<sim> 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 \<sim> y'"
shows "somegcd G x y \<sim> 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 \<subseteq> carrier G" "A \<noteq> {}"
shows "\<exists>x\<in> 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 \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G"
shows "somegcd G (somegcd G a b) c \<sim> 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 \<subseteq> primeness_condition_monoid
+sublocale gcd_condition_monoid \<subseteq> primeness_condition_monoid
by (rule primeness_condition)
@@ -3832,7 +3831,7 @@
with fca fcb show ?thesis by simp
qed
-interpretation factorial_monoid \<subseteq> divisor_chain_condition_monoid
+sublocale factorial_monoid \<subseteq> 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 \<subseteq> primeness_condition_monoid
+sublocale factorial_monoid \<subseteq> 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 \<subseteq> gcd_condition_monoid
+sublocale factorial_monoid \<subseteq> 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 \<and> 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 \<and> gcd_condition_monoid G"
by rule unfold_locales
qed
--- 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 \<in> A" and fin_A: "finite A" and f_Pi: "f \<in> A \<rightarrow> carrier G"
shows "(\<Otimes>j\<in>A. if i = j then f j else \<one>) = f i"
- using i_in_A G.finprod_insert [of "A - {i}" i "(\<lambda>j. if i = j then f j else \<one>)"]
- fin_A f_Pi G.finprod_one [of "A - {i}"]
- G.finprod_cong [of "A - {i}" "A - {i}" "(\<lambda>j. if i = j then f j else \<one>)" "(\<lambda>i. \<one>)"]
+ using i_in_A finprod_insert [of "A - {i}" i "(\<lambda>j. if i = j then f j else \<one>)"]
+ fin_A f_Pi finprod_one [of "A - {i}"]
+ finprod_cong [of "A - {i}" "A - {i}" "(\<lambda>j. if i = j then f j else \<one>)" "(\<lambda>i. \<one>)"]
unfolding Pi_def simp_implies_def by (force simp add: insert_absorb)
end
--- 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\<lparr>carrier := H\<rparr>)"
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 \<times>\<times> H)"
proof -
- interpret G: monoid [G] by fact
- interpret H: monoid [H] by fact
+ interpret G!: monoid G by fact
+ interpret H!: monoid H by fact
from assms
show ?thesis by (unfold monoid_def DirProd_def, auto)
qed
@@ -501,8 +500,8 @@
assumes "group G" and "group H"
shows "group (G \<times>\<times> H)"
proof -
- interpret G: group [G] by fact
- interpret H: group [H] by fact
+ interpret G!: group G by fact
+ interpret H!: group H by fact
show ?thesis by (rule groupI)
(auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
simp add: DirProd_def)
@@ -526,9 +525,9 @@
and h: "h \<in> carrier H"
shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
proof -
- interpret G: group [G] by fact
- interpret H: group [H] by fact
- interpret Prod: group ["G \<times>\<times> H"]
+ interpret G!: group G by fact
+ interpret H!: group H by fact
+ interpret Prod!: group "G \<times>\<times> H"
by (auto intro: DirProd_group group.intro group.axioms assms)
show ?thesis by (simp add: Prod.inv_equality g h)
qed
@@ -542,15 +541,6 @@
{h. h \<in> carrier G -> carrier H &
(\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y)}"
-lemma hom_mult:
- "[| h \<in> hom G H; x \<in> carrier G; y \<in> carrier G |]
- ==> h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
- by (simp add: hom_def)
-
-lemma hom_closed:
- "[| h \<in> hom G H; x \<in> carrier G |] ==> h x \<in> carrier H"
- by (auto simp add: hom_def funcset_mem)
-
lemma (in group) hom_compose:
"[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> 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 \<in> 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 \<in> carrier G; y \<in> carrier G |] ==> h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
+proof -
+ assume "x \<in> carrier G" "y \<in> carrier G"
+ with homh [unfolded hom_def] show ?thesis by simp
+qed
+
+lemma (in group_hom) hom_closed [simp]:
+ "x \<in> carrier G ==> h x \<in> carrier H"
+proof -
+ assume "x \<in> carrier G"
+ with homh [unfolded hom_def] show ?thesis by (auto simp add: funcset_mem)
+qed
lemma (in group_hom) one_closed [simp]:
"h \<one> \<in> carrier H"
--- 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: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
and I_r_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
-interpretation ideal \<subseteq> abelian_subgroup I R
+sublocale ideal \<subseteq> 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: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> 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: "\<exists>i \<in> 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: "\<And>J. \<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> J = I \<or> 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: "\<And>a b. \<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I \<or> b \<in> 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: "\<And>a b. \<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I \<or> b \<in> 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 \<inter> 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 "\<exists>I0. I0 \<in> S" by blast
from this obtain I0 where I0S: "I0 \<in> 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 \<in> I0" .
from this and a_subset show "x \<in> carrier R" by fast
@@ -258,13 +257,13 @@
fix J
assume JS: "J \<in> 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 \<oplus> y \<in> J" by (rule a_closed)
next
fix J
assume JS: "J \<in> S"
- interpret ideal ["J" "R"] by (rule Sideals[OF JS])
+ interpret ideal J R by (rule Sideals[OF JS])
show "\<zero> \<in> J" by simp
next
fix x
@@ -273,7 +272,7 @@
fix J
assume JS: "J \<in> S"
- interpret ideal ["J" "R"] by (rule Sideals[OF JS])
+ interpret ideal J R by (rule Sideals[OF JS])
from xI[OF JS]
show "\<ominus> x \<in> J" by (rule a_inv_closed)
@@ -285,7 +284,7 @@
fix J
assume JS: "J \<in> 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 \<otimes> x \<in> J" by (rule I_l_closed)
@@ -297,7 +296,7 @@
fix J
assume JS: "J \<in> 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 \<otimes> y \<in> J" by (rule I_r_closed)
@@ -443,7 +442,7 @@
lemma (in ring) genideal_one:
"Idl {\<one>} = carrier R"
proof -
- interpret ideal ["Idl {\<one>}" "R"] by (rule genideal_ideal, fast intro: one_closed)
+ interpret ideal "Idl {\<one>}" "R" by (rule genideal_ideal, fast intro: one_closed)
show "Idl {\<one>} = carrier R"
apply (rule, rule a_subset)
apply (simp add: one_imp_carrier genideal_self')
@@ -533,7 +532,7 @@
assumes aJ: "a \<in> J"
shows "PIdl a \<subseteq> 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 \<union> 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 "\<exists>x\<in>I. I = carrier R #> x"
proof -
- interpret cring [R] by fact
+ interpret cring R by fact
from generate
obtain i
where icarr: "i \<in> carrier R"
@@ -693,7 +692,7 @@
assumes notprime: "\<not> primeideal I R"
shows "carrier R = I \<or> (\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I)"
proof (rule ccontr, clarsimp)
- interpret cring [R] by fact
+ interpret cring R by fact
assume InR: "carrier R \<noteq> I"
and "\<forall>a. a \<in> carrier R \<longrightarrow> (\<forall>b. a \<otimes> b \<in> I \<longrightarrow> b \<in> carrier R \<longrightarrow> a \<in> I \<or> b \<in> I)"
hence I_prime: "\<And> a b. \<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I \<or> b \<in> I" by simp
@@ -713,7 +712,7 @@
obtains "carrier R = I"
| "\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I"
proof -
- interpret R: cring [R] by fact
+ interpret R!: cring R by fact
assume "carrier R = I ==> thesis"
and "\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I \<Longrightarrow> thesis"
then show thesis using primeidealCD [OF R.is_cring notprime] by blast
@@ -726,13 +725,13 @@
apply (rule domain.intro, rule is_cring)
apply (rule domain_axioms.intro)
proof (rule ccontr, simp)
- interpret primeideal ["{\<zero>}" "R"] by (rule pi)
+ interpret primeideal "{\<zero>}" "R" by (rule pi)
assume "\<one> = \<zero>"
hence "carrier R = {\<zero>}" by (rule one_zeroD)
from this[symmetric] and I_notcarr
show "False" by simp
next
- interpret primeideal ["{\<zero>}" "R"] by (rule pi)
+ interpret primeideal "{\<zero>}" "R" by (rule pi)
fix a b
assume ab: "a \<otimes> b = \<zero>"
and carr: "a \<in> carrier R" "b \<in> carrier R"
@@ -771,7 +770,7 @@
assumes acarr: "a \<in> carrier R"
shows "ideal {x\<in>carrier R. a \<otimes> x \<in> 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 \<equiv> "{x\<in>carrier R. a \<otimes> x \<in> 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 \<subseteq> J"
@@ -855,7 +854,7 @@
have "\<one> \<notin> J" unfolding J_def by fast
hence Jncarr: "J \<noteq> carrier R" by fast
- interpret ideal ["J" "R"] by (rule idealJ)
+ interpret ideal J R by (rule idealJ)
have "J = I \<or> J = carrier R"
apply (intro I_maximal)
@@ -932,7 +931,7 @@
fix I
assume a: "I \<in> {I. ideal I R}"
with this
- interpret ideal ["I" "R"] by simp
+ interpret ideal I R by simp
show "I \<in> {{\<zero>}, carrier R}"
proof (cases "\<exists>a. a \<in> I - {\<zero>}")
@@ -1019,7 +1018,7 @@
fix J
assume Jn0: "J \<noteq> {\<zero>}"
and idealJ: "ideal J R"
- interpret ideal ["J" "R"] by (rule idealJ)
+ interpret ideal J R by (rule idealJ)
have "{\<zero>} \<subseteq> J" by (rule ccontr, simp)
from zeromax and idealJ and this and a_subset
have "J = {\<zero>} \<or> J = carrier R" by (rule maximalideal.I_maximal)
--- 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 ["\<Z>"]
+interpretation int!: monoid \<Z>
where "carrier \<Z> = UNIV"
and "mult \<Z> x y = x * y"
and "one \<Z> = 1"
@@ -105,7 +104,7 @@
proof -
-- "Specification"
show "monoid \<Z>" proof qed (auto simp: int_ring_def)
- then interpret int: monoid ["\<Z>"] .
+ then interpret int!: monoid \<Z> .
-- "Carrier"
show "carrier \<Z> = UNIV" by (simp add: int_ring_def)
@@ -117,12 +116,12 @@
show "pow \<Z> x n = x^n" by (induct n) (simp, simp add: int_ring_def)+
qed
-interpretation int: comm_monoid ["\<Z>"]
+interpretation int!: comm_monoid \<Z>
where "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
proof -
-- "Specification"
show "comm_monoid \<Z>" proof qed (auto simp: int_ring_def)
- then interpret int: comm_monoid ["\<Z>"] .
+ then interpret int!: comm_monoid \<Z> .
-- "Operations"
{ fix x y have "mult \<Z> x y = x * y" by (simp add: int_ring_def) }
@@ -140,14 +139,14 @@
qed
qed
-interpretation int: abelian_monoid ["\<Z>"]
+interpretation int!: abelian_monoid \<Z>
where "zero \<Z> = 0"
and "add \<Z> x y = x + y"
and "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
proof -
-- "Specification"
show "abelian_monoid \<Z>" proof qed (auto simp: int_ring_def)
- then interpret int: abelian_monoid ["\<Z>"] .
+ then interpret int!: abelian_monoid \<Z> .
-- "Operations"
{ fix x y show "add \<Z> x y = x + y" by (simp add: int_ring_def) }
@@ -165,7 +164,7 @@
qed
qed
-interpretation int: abelian_group ["\<Z>"]
+interpretation int!: abelian_group \<Z>
where "a_inv \<Z> x = - x"
and "a_minus \<Z> x y = x - y"
proof -
@@ -175,7 +174,7 @@
show "!!x. x \<in> carrier \<Z> ==> EX y : carrier \<Z>. y \<oplus>\<^bsub>\<Z>\<^esub> x = \<zero>\<^bsub>\<Z>\<^esub>"
by (simp add: int_ring_def) arith
qed (auto simp: int_ring_def)
- then interpret int: abelian_group ["\<Z>"] .
+ then interpret int!: abelian_group \<Z> .
-- "Operations"
{ fix x y have "add \<Z> x y = x + y" by (simp add: int_ring_def) }
@@ -188,7 +187,7 @@
show "a_minus \<Z> x y = x - y" by (simp add: int.minus_eq add a_inv)
qed
-interpretation int: "domain" ["\<Z>"]
+interpretation int!: "domain" \<Z>
proof qed (auto simp: int_ring_def left_distrib right_distrib)
@@ -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 \<le> |)"]
+interpretation int! (* FIXME [unfolded UNIV] *) :
+ partial_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
where "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
and "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
and "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) 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 \<le> |)"]
+interpretation int! (* FIXME [unfolded UNIV] *) :
+ lattice "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
where "join (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = max x y"
and "meet (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = min x y"
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 \<le> |)"]
+interpretation int! (* [unfolded UNIV] *) :
+ total_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
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 "\<bar>p * x\<bar> = 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>\<Z>\<^esub> {m}" \<Z>] by (rule int.genideal_ideal, fast)
+ interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z> by (rule int.genideal_ideal, fast)
from zmods
have "b \<in> 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>\<Z>\<^esub> {m}" \<Z>] by (rule int.genideal_ideal, fast)
+ interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z> by (rule int.genideal_ideal, fast)
show ?thesis
unfolding ZMod_def
apply (rule a_repr_independence'[symmetric])
--- 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 "\<sqsubseteq>\<index>" 50)
-locale weak_partial_order = equivalence L +
+locale weak_partial_order = equivalence L for L (structure) +
assumes le_refl [intro, simp]:
"x \<in> carrier L ==> x \<sqsubseteq> 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 \<in> carrier L" "y \<in> carrier L"
@@ -1126,14 +1125,14 @@
assumes sup_of_two_exists:
"[| x \<in> carrier L; y \<in> 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 \<in> carrier L; y \<in> 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 \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> 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 \<subseteq> 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 *}
--- 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 "\<odot>\<index>" 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 \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> x \<in> carrier M"
and smult_l_distr:
@@ -29,7 +28,7 @@
and smult_one [simp]:
"x \<in> carrier M ==> \<one> \<odot>\<^bsub>M\<^esub> x = x"
-locale algebra = module R M + cring M +
+locale algebra = module + cring M +
assumes smult_assoc2:
"[| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
(a \<odot>\<^bsub>M\<^esub> x) \<otimes>\<^bsub>M\<^esub> y = a \<odot>\<^bsub>M\<^esub> (x \<otimes>\<^bsub>M\<^esub> y)"
--- 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
--- 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 \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
shows "abelian_group G"
proof -
- interpret comm_group ["\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"]
+ interpret comm_group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
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 \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
and r_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
@@ -585,8 +584,8 @@
assumes RS: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier S" "d \<in> carrier S"
shows "a \<oplus> \<ominus> (a \<oplus> \<ominus> b) = b & c \<otimes>\<^bsub>S\<^esub> d = d \<otimes>\<^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 \<in> carrier R" "b \<in> carrier R"
shows "a \<ominus> (a \<ominus> 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 \<in> ring_hom R S ==> h \<one> = \<one>\<^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 \<in> ring_hom R S"
notes hom_closed [simp, intro] = ring_hom_closed [OF homh]
--- 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 \<in> 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 \<subseteq> ring_hom_ring
+sublocale ring_hom_cring \<subseteq> ring: ring_hom_ring
proof qed (rule homh)
-interpretation ring_hom_ring \<subseteq> abelian_group_hom R S
+sublocale ring_hom_ring \<subseteq> 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 \<one> = \<one>\<^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 \<in> ring_hom R S"
shows "ring_hom_ring R S h"
proof -
- interpret R: ring [R] by fact
- interpret S: ring [S] by fact
+ interpret R!: ring R by fact
+ interpret S!: ring S by fact
show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
apply (rule R.is_ring)
apply (rule S.is_ring)
@@ -76,9 +77,9 @@
and compatible_one: "h \<one> = \<one>\<^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 \<in> 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 "\<exists>i \<in> a_kernel R S h. x = i \<oplus> a" by (simp add: a_r_coset_defs)
@@ -152,7 +153,7 @@
and hx: "h x = h a"
shows "x \<in> 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 \<in> a_kernel R S h +> a"
@@ -193,7 +194,7 @@
from xcarr and this
show "x \<in> {x \<in> 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 \<in> carrier R"
--- 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 \<in> carrier R" and S: "s \<in> carrier S"
shows "eval R S h s (monom P r n) = h r \<otimes>\<^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 \<in> carrier P" and S: "s \<in> 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 (\<Oplus>\<^bsub>P \<^esub>i \<in> {..deg R p}. monom P (coeff P p i) 0 \<otimes>\<^bsub>P\<^esub> monom P \<one> 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 \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub>P\<^esub> monom P a 0) = \<zero>"
(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 \<in> 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 \<one>\<^bsub>R\<^esub> 1 \<in> carrier P"
and mon0_closed: "monom P a 0 \<in> carrier P"
and min_mon0_closed: "\<ominus>\<^bsub>P\<^esub> monom P a 0 \<in> carrier P"
using a R.a_inv_closed by auto
have "eval R R id a ?g = eval R R id a (monom P \<one> 1) \<ominus> 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 "\<dots> = a \<ominus> 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 \<in> 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 \<oplus>\<^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]:
--- 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)\<twosuperior>"
by (simp add: norm_mult power2_eq_square)
-interpretation cnj: bounded_linear ["cnj"]
+interpretation cnj!: bounded_linear "cnj"
apply (unfold_locales)
apply (rule complex_cnj_add)
apply (rule complex_cnj_scaleR)
--- a/src/HOL/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 \<sqsubseteq>") and
@@ -311,7 +311,7 @@
end
-locale linorder_no_ub = linorder_stupid_syntax +
+class_locale linorder_no_ub = linorder_stupid_syntax +
assumes gt_ex: "\<exists>y. less x y"
begin
lemma ge_ex: "\<exists>y. x \<sqsubseteq> 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: "\<exists>y. less y x"
begin
lemma le_ex: "\<exists>y. y \<sqsubseteq> 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 \<Longrightarrow> less x (between x y) \<and> 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 <"
"\<lambda> x y. 1/2 * ((x::'a::{ordered_field,recpower,number_ring}) + y)"]
proof (unfold_locales, dlo, dlo, auto)
--- 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" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"]
+class_interpretation dvd: order ["op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"]
proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym)
lemma dvd_diff: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
--- 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 \<notin> 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: "\<And>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 \<notin> A"
shows "fold_graph times z (insert b A) (z * y)"
proof -
- interpret fun_left_comm ["op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"] by (rule fun_left_comm)
+ interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> '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 \<notin> A" shows "fold1 times (insert a A) = fold times a A"
proof -
- interpret fun_left_comm ["op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"] by (rule fun_left_comm)
+ interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> '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 \<noteq> {}" and A: "finite A" "x \<notin> A"
shows "fold1 times (insert x A) = x * fold1 times A"
proof -
- interpret fun_left_comm ["op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"] by (rule fun_left_comm)
+ interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> '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 \<noteq> {}" and A: "finite A"
shows "fold1 times (insert x A) = x * fold1 times A"
proof -
- interpret fun_left_comm_idem ["op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"]
+ interpret fun_left_comm_idem "op *::'a \<Rightarrow> 'a \<Rightarrow> '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 \<noteq> {}"
shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> 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 \<or> a \<in> F" by simp
@@ -2288,7 +2288,7 @@
and "A \<noteq> {}"
shows "sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> 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 \<in> B}"
@@ -2333,7 +2333,7 @@
assumes "finite A" and "A \<noteq> {}"
shows "inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> 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 \<in> A \<and> b \<in> B} \<noteq> {}" 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 (\<Squnion>\<^bsub>fin\<^esub>(insert x A)) (\<Squnion>\<^bsub>fin\<^esub>B) = inf (sup x (\<Squnion>\<^bsub>fin\<^esub>A)) (\<Squnion>\<^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 \<noteq> {}"
shows "\<Sqinter>\<^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 \<noteq> {}"
shows "\<Squnion>\<^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 \<noteq> {}"
shows "x < fold1 min A \<longleftrightarrow> (\<forall>a\<in>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 \<noteq> {}"
shows "fold1 min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> 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 \<noteq> {}"
shows "fold1 min A < x \<longleftrightarrow> (\<exists>a\<in>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 \<noteq> B"
have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
@@ -2515,7 +2515,7 @@
assumes "finite A" and "A \<noteq> {}"
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 \<noteq> {}"
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 \<noteq> {}"
shows "Min A \<in> 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 \<noteq> {}"
shows "Max A \<in> 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 \<noteq> {}" and "finite B" and "B \<noteq> {}"
shows "Min (A \<union> 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 \<noteq> {}" and "finite B" and "B \<noteq> {}"
shows "Max (A \<union> 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 \<noteq> {}"
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 \<noteq> {}"
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 \<in> A"
shows "Min A \<le> x"
proof -
- interpret lower_semilattice ["op \<le>" "op <" min]
+ class_interpret lower_semilattice ["op \<le>" "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 \<noteq> {}"
shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
proof -
- interpret lower_semilattice ["op \<le>" "op <" min]
+ class_interpret lower_semilattice ["op \<le>" "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 \<noteq> {}"
shows "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
proof -
- interpret lower_semilattice ["op \<le>" "op <" min]
+ class_interpret lower_semilattice ["op \<le>" "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 \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
proof -
note Max = Max_def
- interpret linorder ["op \<ge>" "op >"]
+ class_interpret linorder ["op \<ge>" "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 \<noteq> {}"
shows "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
proof -
- interpret lower_semilattice ["op \<le>" "op <" min]
+ class_interpret lower_semilattice ["op \<le>" "op <" min]
by (rule min_lattice)
from assms show ?thesis
by (simp add: Min_def fold1_below_iff)
@@ -2660,7 +2660,7 @@
shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
proof -
note Max = Max_def
- interpret linorder ["op \<ge>" "op >"]
+ class_interpret linorder ["op \<ge>" "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 \<noteq> {}"
shows "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
proof -
- interpret lower_semilattice ["op \<le>" "op <" min]
+ class_interpret lower_semilattice ["op \<le>" "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 \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
proof -
note Max = Max_def
- interpret linorder ["op \<ge>" "op >"]
+ class_interpret linorder ["op \<ge>" "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 \<subseteq> N" and "M \<noteq> {}" and "finite N"
shows "Min N \<le> Min M"
proof -
- interpret distrib_lattice ["op \<le>" "op <" min max]
+ class_interpret distrib_lattice ["op \<le>" "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 \<le> Max N"
proof -
note Max = Max_def
- interpret linorder ["op \<ge>" "op >"]
+ class_interpret linorder ["op \<ge>" "op >"]
by (rule dual_linorder)
from assms show ?thesis
by (simp add: Max fold1_antimono [folded dual_max])
--- 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 (\<lambda>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 (\<lambda>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 "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h) -- 0 --> 0"
by (rule FDERIV_D [OF f])
hence "(\<lambda>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 (\<lambda>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 = "\<lambda>h. f (x + h) - f x"
let ?Nf = "\<lambda>h. norm (?Rf h) / norm h"
let ?Ng = "\<lambda>h. norm (?Rg (?k h)) / norm (?k h)"
- from f interpret F: bounded_linear ["F"] by (rule FDERIV_bounded_linear)
- from g interpret G: bounded_linear ["G"] by (rule FDERIV_bounded_linear)
+ from f interpret F!: bounded_linear "F" by (rule FDERIV_bounded_linear)
+ from g interpret G!: bounded_linear "G" by (rule FDERIV_bounded_linear)
from F.bounded obtain kF where kF: "\<And>x. norm (F x) \<le> norm x * kF" by fast
from G.bounded obtain kG where kG: "\<And>x. norm (G x) \<le> norm x * kG" by fast
@@ -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 :> (\<lambda>h. h * D) = (\<lambda>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])
--- 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 \<noteq> 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 \<noteq> 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"
--- 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 "\<Squnion>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"
--- 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: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
declare continuous.intro [intro?] continuous_axioms.intro [intro?]
@@ -91,7 +90,7 @@
assumes "continuous V norm f"
shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>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 \<in> B V f"
shows "b \<le> \<parallel>f\<parallel>\<hyphen>V"
proof -
- interpret continuous [V norm f] by fact
+ interpret continuous V norm f by fact
have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
using `continuous V norm f` by (rule fn_norm_works)
from this and b show ?thesis ..
@@ -170,7 +169,7 @@
assumes b: "\<And>b. b \<in> B V f \<Longrightarrow> b \<le> y"
shows "\<parallel>f\<parallel>\<hyphen>V \<le> y"
proof -
- interpret continuous [V norm f] by fact
+ interpret continuous V norm f by fact
have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>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 \<le> \<parallel>f\<parallel>\<hyphen>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 "\<ge> 0"} if all elements in @{text B} are @{text "\<ge>
0"}, provided the supremum exists and @{text B} is not empty. *}
@@ -204,8 +203,8 @@
assumes x: "x \<in> V"
shows "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
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: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c"
shows "\<parallel>f\<parallel>\<hyphen>V \<le> 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 \<in> B V f"
--- 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 \<equiv> "norm_pres_extensions E p F f"
then have M: "M = \<dots>" by (simp only:)
from E have F: "vectorspace F" ..
@@ -322,10 +321,10 @@
\<and> (\<forall>x \<in> F. g x = f x)
\<and> (\<forall>x \<in> E. \<bar>g x\<bar> \<le> 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 "\<exists>g. linearform E g \<and> (\<forall>x \<in> F. g x = f x) \<and> (\<forall>x \<in> E. g x \<le> p x)"
using E FE sn lf
proof (rule HahnBanach)
@@ -363,12 +362,12 @@
\<and> (\<forall>x \<in> F. g x = f x)
\<and> \<parallel>g\<parallel>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>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"
--- 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: "\<And>u v. u \<in> F \<Longrightarrow> v \<in> F \<Longrightarrow> a u \<le> b v"
shows "\<exists>xi::real. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> 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 \<in> 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': "\<forall>y \<in> H. - p (y + x0) - h y \<le> xi \<and> xi \<le> p (y + x0) - h y"
shows "\<forall>x \<in> H'. h' x \<le> 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 \<in> H'"
--- 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 "(\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x) = (\<forall>x \<in> H. h x \<le> 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
--- 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\<Colon>{minus, plus, zero, uminus} set"
+locale linearform =
+ fixes V :: "'a\<Colon>{minus, plus, zero, uminus} set" and f
assumes add [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y"
and mult [iff]: "x \<in> V \<Longrightarrow> f (a \<cdot> x) = a * f x"
@@ -25,7 +24,7 @@
assumes "vectorspace V"
shows "x \<in> V \<Longrightarrow> f (- x) = - f x"
proof -
- interpret vectorspace [V] by fact
+ interpret vectorspace V by fact
assume x: "x \<in> V"
then have "f (- x) = f ((- 1) \<cdot> x)" by (simp add: negate_eq1)
also from x have "\<dots> = (- 1) * (f x)" by (rule mult)
@@ -37,7 +36,7 @@
assumes "vectorspace V"
shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x - y) = f x - f y"
proof -
- interpret vectorspace [V] by fact
+ interpret vectorspace V by fact
assume x: "x \<in> V" and y: "y \<in> V"
then have "x - y = x + - y" by (rule diff_eq1)
also have "f \<dots> = 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 "\<dots> = f 0 - f 0" using `vectorspace V` by (rule diff) simp_all
also have "\<dots> = 0" by simp
--- 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 \<Rightarrow> real" ("\<parallel>_\<parallel>")
-locale seminorm = var V + norm_syntax +
+locale seminorm = var_V + norm_syntax +
constrains V :: "'a\<Colon>{minus, plus, zero, uminus} set"
assumes ge_zero [iff?]: "x \<in> V \<Longrightarrow> 0 \<le> \<parallel>x\<parallel>"
and abs_homogenous [iff?]: "x \<in> V \<Longrightarrow> \<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>"
@@ -32,7 +31,7 @@
assumes "vectorspace V"
shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x - y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
proof -
- interpret vectorspace [V] by fact
+ interpret vectorspace V by fact
assume x: "x \<in> V" and y: "y \<in> V"
then have "x - y = x + - 1 \<cdot> y"
by (simp add: diff_eq2 negate_eq2a)
@@ -48,7 +47,7 @@
assumes "vectorspace V"
shows "x \<in> V \<Longrightarrow> \<parallel>- x\<parallel> = \<parallel>x\<parallel>"
proof -
- interpret vectorspace [V] by fact
+ interpret vectorspace V by fact
assume x: "x \<in> V"
then have "- x = - 1 \<cdot> x" by (simp only: negate_eq1)
also from x have "\<parallel>\<dots>\<parallel> = \<bar>- 1\<bar> * \<parallel>x\<parallel>"
@@ -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
--- 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\<Colon>{minus, plus, zero, uminus} set"
+locale subspace =
+ fixes U :: "'a\<Colon>{minus, plus, zero, uminus} set" and V
assumes non_empty [iff, intro]: "U \<noteq> {}"
and subset [iff]: "U \<subseteq> V"
and add_closed [iff]: "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x + y \<in> U"
@@ -46,7 +45,7 @@
assumes x: "x \<in> U" and y: "y \<in> U"
shows "x - y \<in> 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 \<in> U"
proof -
- interpret vectorspace [V] by fact
- have "U \<noteq> {}" by (rule U_V.non_empty)
+ interpret V!: vectorspace V by fact
+ have "U \<noteq> {}" by (rule non_empty)
then obtain x where x: "x \<in> U" by blast
then have "x \<in> V" .. then have "0 = x - x" by simp
- also from `vectorspace V` x x have "\<dots> \<in> U" by (rule U_V.diff_closed)
+ also from `vectorspace V` x x have "\<dots> \<in> U" by (rule diff_closed)
finally show ?thesis .
qed
@@ -73,7 +72,7 @@
assumes x: "x \<in> U"
shows "- x \<in> 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 \<noteq> {}" ..
@@ -255,8 +254,8 @@
assumes "vectorspace U" "vectorspace V"
shows "U \<unlhd> 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 \<noteq> {}" ..
@@ -279,9 +278,9 @@
assumes "subspace U E" "vectorspace E" "subspace V E"
shows "U + V \<unlhd> 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 \<in> U + V"
@@ -346,9 +345,9 @@
and sum: "u1 + v1 = u2 + v2"
shows "u1 = u2 \<and> 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 \<cdot> x' = y2 + a2 \<cdot> x'"
shows "y1 = y2 \<and> 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 \<and> a1 \<cdot> x' = a2 \<cdot> x'"
@@ -451,8 +450,8 @@
and x': "x' \<notin> H" "x' \<in> E" "x' \<noteq> 0"
shows "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> 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 \<cdot> x' \<and> t \<in> H" by simp
@@ -483,8 +482,8 @@
and x': "x' \<notin> H" "x' \<in> E" "x' \<noteq> 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 \<in> H + lin x'" by auto
have "\<exists>!p. (\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) p" (is "\<exists>!p. ?P p")
proof (rule ex_ex1I)
--- 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 \<noteq> {}"
and add_closed [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y \<in> V"
and mult_closed [iff]: "x \<in> V \<Longrightarrow> a \<cdot> x \<in> V"
--- 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
*)
--- 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 \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max]
by (rule distrib_lattice_min_max)
--- 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 \<le>#" "op <#"]
+class_interpretation mset_order: order ["op \<le>#" "op <#"]
proof qed (auto intro: order.intro mset_le_refl mset_le_antisym
mset_le_trans simp: mset_less_def)
-interpretation mset_order_cancel_semigroup:
+class_interpretation mset_order_cancel_semigroup:
pordered_cancel_ab_semigroup_add ["op +" "op \<le>#" "op <#"]
proof qed (erule mset_le_mono_add [OF mset_le_refl])
-interpretation mset_order_semigroup_cancel:
+class_interpretation mset_order_semigroup_cancel:
pordered_ab_semigroup_add_imp_le ["op +" "op \<le>#" "op <#"]
proof qed simp
@@ -1404,7 +1404,7 @@
assumes "left_commutative g"
shows "(\<And>x y. h (g x y) = f x (h y)) \<Longrightarrow> 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 {#} = {#}"
--- 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 \<oplus> :: ('a::semigroup_add) set => 'a set => 'a set"]
+class_interpretation set_semigroup_add: semigroup_add ["op \<oplus> :: ('a::semigroup_add) set => 'a set => 'a set"]
apply default
apply (unfold set_plus_def)
apply (force simp add: add_assoc)
done
-interpretation set_semigroup_mult: semigroup_mult ["op \<otimes> :: ('a::semigroup_mult) set => 'a set => 'a set"]
+class_interpretation set_semigroup_mult: semigroup_mult ["op \<otimes> :: ('a::semigroup_mult) set => 'a set => 'a set"]
apply default
apply (unfold set_times_def)
apply (force simp add: mult_assoc)
done
-interpretation set_comm_monoid_add: comm_monoid_add ["{0}" "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set"]
+class_interpretation set_comm_monoid_add: comm_monoid_add ["{0}" "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set"]
apply default
apply (unfold set_plus_def)
apply (force simp add: add_ac)
apply force
done
-interpretation set_comm_monoid_mult: comm_monoid_mult ["{1}" "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set"]
+class_interpretation set_comm_monoid_mult: comm_monoid_mult ["{1}" "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set"]
apply default
apply (unfold set_times_def)
apply (force simp add: mult_ac)
--- a/src/HOL/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 = [] \<and> ys = [])"
--- 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 \<or>
merges f qs ss = ss \<and> {q. \<exists>t. (q,t)\<in>set qs \<and> t +_f ss!q \<noteq> 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 @@
(\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow> 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 @@
\<Longrightarrow> 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])
--- 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 \<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'
then map snd [(p',t') \<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc
- else \<top>)" unfolding merge_def by (rule lbv.merge_def [OF lbvc.axioms(1), OF lbvc_axioms])
+ else \<top>)" unfolding mrg_def by (rule lbv.merge_def [OF lbvc.axioms(1), OF lbvc_axioms])
moreover {
fix pc' s' assume s': "(pc', s') \<in> set ?step" and suc_pc: "pc' \<noteq> pc+1"
with less have "s' <=_r \<phi>!pc'" by auto
--- 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)
--- 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
"\<And>y. \<lbrakk> set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> x ++_f y \<in> 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 "\<And>y. y \<in> A \<Longrightarrow> [] ++_f y \<in> A" by simp
fix y x xs
@@ -164,7 +164,7 @@
shows "\<lbrakk>\<forall>(p,s) \<in> set S. s \<in> A; y \<in> A; (a,b) \<in> set S\<rbrakk>
\<Longrightarrow> b <=_r map snd [(p', t')\<leftarrow>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
--- 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 *}
--- 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 ["\<lambda>a. scale a x"]
+ interpret s: additive "\<lambda>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 ["\<lambda>x. scale a x"]
+ interpret s: additive "\<lambda>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 \<Rightarrow> 'a \<Rightarrow> 'a::real_vector"]
+interpretation real_vector!:
+ vector_space "scaleR :: real \<Rightarrow> 'a \<Rightarrow> '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 ["(\<lambda>a. scaleR a x::'a::real_vector)"]
+interpretation scaleR_left!: additive "(\<lambda>a. scaleR a x::'a::real_vector)"
proof qed (rule scaleR_left_distrib)
-interpretation scaleR_right: additive ["(\<lambda>x. scaleR a x::'a::real_vector)"]
+interpretation scaleR_right!: additive "(\<lambda>x. scaleR a x::'a::real_vector)"
proof qed (rule scaleR_right_distrib)
lemma nonzero_inverse_scaleR_distrib:
@@ -796,8 +796,8 @@
end
-interpretation mult:
- bounded_bilinear ["op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra"]
+interpretation mult!:
+ bounded_bilinear "op * :: 'a \<Rightarrow> 'a \<Rightarrow> '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 ["(\<lambda>x::'a::real_normed_algebra. x * y)"]
+interpretation mult_left!:
+ bounded_linear "(\<lambda>x::'a::real_normed_algebra. x * y)"
by (rule mult.bounded_linear_left)
-interpretation mult_right:
- bounded_linear ["(\<lambda>y::'a::real_normed_algebra. x * y)"]
+interpretation mult_right!:
+ bounded_linear "(\<lambda>y::'a::real_normed_algebra. x * y)"
by (rule mult.bounded_linear_right)
-interpretation divide:
- bounded_linear ["(\<lambda>x::'a::real_normed_field. x / y)"]
+interpretation divide!:
+ bounded_linear "(\<lambda>x::'a::real_normed_field. x / y)"
unfolding divide_inverse by (rule mult.bounded_linear_left)
-interpretation scaleR: bounded_bilinear ["scaleR"]
+interpretation scaleR!: bounded_bilinear "scaleR"
apply (rule bounded_bilinear.intro)
apply (rule scaleR_left_distrib)
apply (rule scaleR_right_distrib)
@@ -829,13 +829,13 @@
apply (simp add: norm_scaleR)
done
-interpretation scaleR_left: bounded_linear ["\<lambda>r. scaleR r x"]
+interpretation scaleR_left!: bounded_linear "\<lambda>r. scaleR r x"
by (rule scaleR.bounded_linear_left)
-interpretation scaleR_right: bounded_linear ["\<lambda>x. scaleR r x"]
+interpretation scaleR_right!: bounded_linear "\<lambda>x. scaleR r x"
by (rule scaleR.bounded_linear_right)
-interpretation of_real: bounded_linear ["\<lambda>r. of_real r"]
+interpretation of_real!: bounded_linear "\<lambda>r. of_real r"
unfolding of_real_def by (rule scaleR.bounded_linear_left)
end
--- a/src/HOL/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<a:=i>\<cdot>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>\<cdot>a = i"
qed
-
+*)
(*
lemma
includes foo
--- 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)
--- 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
--- 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
--- 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. \<forall>i. f i \<longrightarrow> i < len_of TYPE('a::len0)}"
- "(\<lambda>h i. h i \<and> i < len_of TYPE('a::len0))"]
+interpretation test_bit!:
+ td_ext "op !! :: 'a::len0 word => nat => bool"
+ set_bits
+ "{f. \<forall>i. f i \<longrightarrow> i < len_of TYPE('a::len0)}"
+ "(\<lambda>h i. h i \<and> i < len_of TYPE('a::len0))"
by (rule td_ext_nth)
declare test_bit.Rep' [simp del]
--- 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 \<Rightarrow> int"
- word_of_int
- "uints (len_of TYPE('a::len0))"
- "\<lambda>w. w mod 2 ^ len_of TYPE('a::len0)"]
+interpretation word_uint!:
+ td_ext "uint::'a::len0 word \<Rightarrow> int"
+ word_of_int
+ "uints (len_of TYPE('a::len0))"
+ "\<lambda>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 \<Rightarrow> 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 \<Rightarrow> 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)"
--- 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
--- 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
--- 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 \<sqsubseteq> 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 \<sqinter> (y \<squnion> z) = x \<sqinter> y \<squnion> x \<sqinter> 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)" ..
--- 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
--- 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.
*)
--- 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: "\<And>x. f\<cdot>x \<sqsubseteq> 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 "\<And>x. (d oo f)\<cdot>x \<sqsubseteq> x"
by (simp, rule trans_less [OF d.less f])
@@ -173,9 +173,9 @@
assumes f: "\<And>x. f\<cdot>x \<sqsubseteq> x"
shows "eventual (\<lambda>n. iterate n\<cdot>(d oo f))\<cdot>x = x \<longleftrightarrow> d\<cdot>x = x \<and> f\<cdot>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 (\<lambda>n. iterate n\<cdot>?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\<cdot>d"]
+interpretation cast!: deflation "cast\<cdot>d"
by (rule deflation_cast)
lemma "cast\<cdot>(\<Squnion>i. alg_defl_principal (Abs_fin_defl (approx i)))\<cdot>x = x"
@@ -485,7 +485,7 @@
constrains e :: "'a::profinite \<rightarrow> 'b::profinite"
shows "\<exists>d. cast\<cdot>d = e oo p"
proof
- interpret ep_pair [e p] by fact
+ interpret ep_pair e p by fact
let ?a = "\<lambda>i. e oo approx i oo p"
have a: "\<And>i. finite_deflation (?a i)"
apply (rule finite_deflation_e_d_p)
@@ -516,7 +516,7 @@
"\<And>i. finite_deflation (a i)"
"(\<Squnion>i. a i) = ID"
proof
- interpret ep_pair [e p] by fact
+ interpret ep_pair e p by fact
let ?a = "\<lambda>i. p oo cast\<cdot>(approx i\<cdot>d) oo e"
show "\<And>i. finite_deflation (?a i)"
apply (rule finite_deflation_p_d_e)
--- 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" ..
--- 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 \<sqsubseteq> a"
@@ -92,8 +92,8 @@
approximants :: "'a \<Rightarrow> 'a compact_basis set" where
"approximants = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> 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
--- 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 \<Rightarrow> 'a \<Rightarrow> bool"]
+interpretation sq_le!: preorder "sq_le :: 'a::po \<Rightarrow> 'a \<Rightarrow> bool"
apply unfold_locales
apply (rule refl_less)
apply (erule (1) trans_less)
--- a/src/HOLCF/ConvexPD.thy 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: "\<lbrakk>t \<le>\<natural> u; u \<le>\<natural> v\<rbrakk> \<Longrightarrow> t \<le>\<natural> v"
unfolding convex_le_def by (fast intro: upper_le_trans lower_le_trans)
-interpretation convex_le: preorder [convex_le]
+interpretation convex_le!: preorder convex_le
by (rule preorder.intro, rule convex_le_refl, rule convex_le_trans)
lemma upper_le_minimal [simp]: "PDUnit compact_bot \<le>\<natural> t"
@@ -178,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 +\<natural>"]
+class_interpretation aci_convex_plus: ab_semigroup_idem_mult ["op +\<natural>"]
by unfold_locales
(rule convex_plus_assoc convex_plus_commute convex_plus_absorb)+
--- 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 \<sqsubseteq> g \<Longrightarrow> f\<cdot>(g\<cdot>x) = f\<cdot>x"
proof (rule antisym_less)
- interpret g: deflation [g] by fact
+ interpret g: deflation g by fact
from g.less show "f\<cdot>(g\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
next
- interpret f: deflation [f] by fact
+ interpret f: deflation f by fact
assume "f \<sqsubseteq> g" hence "f\<cdot>x \<sqsubseteq> g\<cdot>x" by (rule monofun_cfun_fun)
hence "f\<cdot>(f\<cdot>x) \<sqsubseteq> f\<cdot>(g\<cdot>x)" by (rule monofun_cfun_arg)
also have "f\<cdot>(f\<cdot>x) = f\<cdot>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)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>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)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>x"
by (simp add: idem)
@@ -250,7 +250,7 @@
assumes d: "\<And>x. d\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>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\<cdot>(e\<cdot>x) \<sqsubseteq> e\<cdot>x"
@@ -287,7 +287,7 @@
assumes d: "\<And>x. d\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>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 \<sqsubseteq> 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\<cdot>(p\<cdot>(e2\<cdot>x)) \<sqsubseteq> e2\<cdot>x"
by (rule e1.e_p_less)
@@ -333,8 +333,8 @@
assumes "ep_pair e p1" and "ep_pair e p2"
shows "p1 \<sqsubseteq> 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\<cdot>(p1\<cdot>x) \<sqsubseteq> 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)\<cdot>((e2 oo e1)\<cdot>x) = x"
by simp
--- 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 \<le>\<flat> 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 +\<flat>"]
+class_interpretation aci_lower_plus: ab_semigroup_idem_mult ["op +\<flat>"]
by unfold_locales
(rule lower_plus_assoc lower_plus_commute lower_plus_absorb)+
--- 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)
--- 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 \<le>\<sharp> 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 +\<sharp>"]
+class_interpretation aci_upper_plus: ab_semigroup_idem_mult ["op +\<sharp>"]
by unfold_locales
(rule upper_plus_assoc upper_plus_commute upper_plus_absorb)+
--- 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));
--- 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";
--- 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)
--- 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;
--- 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
--- 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.$$$ "\\<subseteq>" || 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"
--- 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;
--- 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;
--- 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 ()));
--- 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]
--- 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;
--- 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
--- 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;
--- 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]
--- 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
--- 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
--- 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\<index> _" [81] 80) where
"inv\<^bsub>G\<^esub> x == (THE y. y \<in> carrier(G) & y \<cdot>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub> & x \<cdot>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub>)"
-locale monoid = struct G +
+locale monoid = fixes G (structure)
assumes m_closed [intro, simp]:
"\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> x \<cdot> y \<in> 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 \<subseteq> carrier(G)"
and m_closed [intro, simp]: "\<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<cdot> y \<in> H"
and one_closed [simp]: "\<one> \<in> 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 \<Otimes> 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 "(\<lambda><x,y> \<in> carrier(G \<Otimes> H). <y,x>) \<in> (G \<Otimes> H) \<cong> (H \<Otimes> 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 "(\<lambda><<x,y>,z> \<in> carrier((G \<Otimes> H) \<Otimes> I). <x,<y,z>>)
\<in> ((G \<Otimes> H) \<Otimes> I) \<cong> (G \<Otimes> (H \<Otimes> 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 \<in> 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 \<subseteq> carrier(G) \<times> carrier(G)"
by (auto simp add: r_congruent_def)
@@ -907,7 +907,7 @@
assumes a: "a \<in> 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 \<in> H; ha \<in> H; hb \<in> H\<rbrakk>
\<Longrightarrow> hb \<cdot> a \<in> (\<Union>h\<in>H. {h \<cdot> 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 \<cdot> ((inv ha) \<cdot> h)"], simp)
apply (simp add: m_assoc transpose_inv)
@@ -931,7 +931,7 @@
assumes "subgroup(H, G)"
shows "\<lbrakk>a \<in> rcosets H; b \<in> rcosets H; a\<noteq>b\<rbrakk> \<Longrightarrow> a \<inter> 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 \<in> carrier(G) \<Longrightarrow> x \<in> 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="\<one>" in bexI) apply (auto)
@@ -960,7 +960,7 @@
assumes "subgroup(H, G)"
shows "\<Union>(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 \<in> rcosets H"
proof -
- interpret group [G] by fact
+ interpret group G by fact
have "H #> \<one> = H"
using _ subgroup_axioms by (rule coset_join2) simp_all
then show ?thesis
--- 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 "\<ominus>\<index>" 65) where
"\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<ominus>\<^bsub>R\<^esub> y = x \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> y)"
-locale abelian_monoid = struct G +
+locale abelian_monoid = fixes G (structure)
assumes a_comm_monoid:
"comm_monoid (<carrier(G), add_field(G), zero(G), 0>)"
@@ -57,7 +57,7 @@
assumes a_comm_group:
"comm_group (<carrier(G), add_field(G), zero(G), 0>)"
-locale ring = abelian_group R + monoid R +
+locale ring = abelian_group R + monoid R for R (structure) +
assumes l_distr: "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R); z \<in> carrier(R)\<rbrakk>
\<Longrightarrow> (x \<oplus> y) \<cdot> z = x \<cdot> z \<oplus> y \<cdot> z"
and r_distr: "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R); z \<in> carrier(R)\<rbrakk>
@@ -262,7 +262,8 @@
lemma ring_hom_one: "h \<in> ring_hom(R,S) \<Longrightarrow> h ` \<one>\<^bsub>R\<^esub> = \<one>\<^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 \<in> ring_hom(R,S)"
notes hom_closed [simp, intro] = ring_hom_closed [OF homh]
and hom_mult [simp] = ring_hom_mult [OF homh]