Merged.
--- a/etc/isar-keywords.el Tue Dec 16 15:08:08 2008 +0100
+++ b/etc/isar-keywords.el Tue Dec 16 15:09:37 2008 +0100
@@ -45,6 +45,9 @@
"chapter"
"class"
"class_deps"
+ "class_interpret"
+ "class_interpretation"
+ "class_locale"
"classes"
"classrel"
"code_abort"
@@ -418,6 +421,7 @@
"axiomatization"
"axioms"
"class"
+ "class_locale"
"classes"
"classrel"
"code_abort"
@@ -501,6 +505,7 @@
(defconst isar-keywords-theory-goal
'("ax_specification"
+ "class_interpretation"
"corollary"
"cpodef"
"function"
@@ -539,7 +544,8 @@
"subsubsect"))
(defconst isar-keywords-proof-goal
- '("have"
+ '("class_interpret"
+ "have"
"hence"
"interpret"
"invoke"))
--- a/src/HOL/Complex.thy Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/Complex.thy Tue Dec 16 15:09:37 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/Divides.thy Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/Divides.thy Tue Dec 16 15:09:37 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 Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/Finite_Set.thy Tue Dec 16 15:09:37 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 Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/FrechetDeriv.thy Tue Dec 16 15:09:37 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 Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/Groebner_Basis.thy Tue Dec 16 15:09:37 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/Lattices.thy Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/Lattices.thy Tue Dec 16 15:09:37 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/Dense_Linear_Order.thy Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/Library/Dense_Linear_Order.thy Tue Dec 16 15:09:37 2008 +0100
@@ -1,5 +1,4 @@
(*
- ID: $Id$
Author: Amine Chaieb, TU Muenchen
*)
@@ -304,7 +303,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
@@ -314,7 +313,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
@@ -363,7 +362,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
@@ -410,12 +409,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)
@@ -638,7 +637,7 @@
using eq_diff_eq[where a= x and b=t and c=0] by simp
-interpretation class_ordered_field_dense_linear_order: constr_dense_linear_order
+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/Library/Multiset.thy Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/Library/Multiset.thy Tue Dec 16 15:09:37 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 Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/Library/SetsAndFunctions.thy Tue Dec 16 15:09:37 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 Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/List.thy Tue Dec 16 15:09:37 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 Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/MicroJava/BV/Kildall.thy Tue Dec 16 15:09:37 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 Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy Tue Dec 16 15:09:37 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 Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/MicroJava/BV/Listn.thy Tue Dec 16 15:09:37 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 Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/MicroJava/BV/SemilatAlg.thy Tue Dec 16 15:09:37 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 Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/NSA/StarDef.thy Tue Dec 16 15:09:37 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/ROOT.ML Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/ROOT.ML Tue Dec 16 15:09:37 2008 +0100
@@ -3,6 +3,7 @@
Classical Higher-order Logic -- batteries included.
*)
+set new_locales;
use_thy "Complex_Main";
val HOL_proofs = ! Proofterm.proofs;
--- a/src/HOL/Real/HahnBanach/Bounds.thy Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/Real/HahnBanach/Bounds.thy Tue Dec 16 15:09:37 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/Real/HahnBanach/FunctionNorm.thy Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Tue Dec 16 15:09:37 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/Real/HahnBanach/HahnBanach.thy Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Tue Dec 16 15:09:37 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/Real/HahnBanach/HahnBanachExtLemmas.thy Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Tue Dec 16 15:09:37 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/Real/HahnBanach/HahnBanachSupLemmas.thy Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Tue Dec 16 15:09:37 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/Real/HahnBanach/Linearform.thy Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/Real/HahnBanach/Linearform.thy Tue Dec 16 15:09:37 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/Real/HahnBanach/NormedSpace.thy Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy Tue Dec 16 15:09:37 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/Real/HahnBanach/Subspace.thy Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/Real/HahnBanach/Subspace.thy Tue Dec 16 15:09:37 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/Real/HahnBanach/VectorSpace.thy Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Tue Dec 16 15:09:37 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/Real/HahnBanach/ZornLemma.thy Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/Real/HahnBanach/ZornLemma.thy Tue Dec 16 15:09:37 2008 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Real/HahnBanach/ZornLemma.thy
- ID: $Id$
Author: Gertrud Bauer, TU Munich
*)
--- a/src/HOL/Real/RealVector.thy Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/Real/RealVector.thy Tue Dec 16 15:09:37 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 Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/Statespace/StateSpaceEx.thy Tue Dec 16 15:09:37 2008 +0100
@@ -37,7 +37,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]"
@@ -204,7 +204,7 @@
assumes "foo f a b c p1 i1 p2 i2 p3 i3 p4 i4"
shows True
proof
- interpret foo [f a b c p1 i1 p2 i2 p3 i3 p4 i4] by fact
+ class_interpret foo [f a b c p1 i1 p2 i2 p3 i3 p4 i4] by fact
term "s<a := i>\<cdot>a = i"
qed
--- a/src/HOL/Statespace/StateSpaceLocale.thy Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/Statespace/StateSpaceLocale.thy Tue Dec 16 15:09:37 2008 +0100
@@ -16,7 +16,7 @@
concrete values.*}
-locale project_inject =
+class_locale project_inject =
fixes project :: "'value \<Rightarrow> 'a"
and "inject":: "'a \<Rightarrow> 'value"
assumes project_inject_cancel [statefun_simp]: "project (inject x) = x"
--- a/src/HOL/Word/TdThs.thy Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/Word/TdThs.thy Tue Dec 16 15:09:37 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 Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/Word/WordArith.thy Tue Dec 16 15:09:37 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 Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/Word/WordBitwise.thy Tue Dec 16 15:09:37 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 Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/Word/WordDefinition.thy Tue Dec 16 15:09:37 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 Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/Word/WordGenLib.thy Tue Dec 16 15:09:37 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 Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/ex/Abstract_NAT.thy Tue Dec 16 15:09:37 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 Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/ex/LocaleTest2.thy Tue Dec 16 15:09:37 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 Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/ex/Tarski.thy Tue Dec 16 15:09:37 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/main.ML Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/main.ML Tue Dec 16 15:09:37 2008 +0100
@@ -4,4 +4,5 @@
Classical Higher-order Logic -- only "Main".
*)
+set new_locales;
use_thy "Main";
--- a/src/HOL/plain.ML Tue Dec 16 15:08:08 2008 +0100
+++ b/src/HOL/plain.ML Tue Dec 16 15:09:37 2008 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/plain.ML
- ID: $Id$
Classical Higher-order Logic -- plain Tool bootstrap.
*)
+set new_locales;
use_thy "Plain";
--- a/src/Pure/Isar/isar_cmd.ML Tue Dec 16 15:08:08 2008 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Tue Dec 16 15:09:37 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 Tue Dec 16 15:08:08 2008 +0100
+++ b/src/Pure/Isar/isar_syn.ML Tue Dec 16 15:09:37 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/subclass.ML Tue Dec 16 15:08:08 2008 +0100
+++ b/src/Pure/Isar/subclass.ML Tue Dec 16 15:09:37 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 Tue Dec 16 15:08:08 2008 +0100
+++ b/src/Pure/Isar/theory_target.ML Tue Dec 16 15:09:37 2008 +0100
@@ -8,7 +8,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
@@ -24,25 +24,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_locales andalso new_locale then NewLocale.extern x else Locale.extern x;
+fun locale_add_type_syntax new_locale x =
+ if !new_locales andalso new_locale then NewLocale.add_type_syntax x else Locale.add_type_syntax x;
+fun locale_add_term_syntax new_locale x =
+ if !new_locales andalso new_locale then NewLocale.add_term_syntax x else Locale.add_term_syntax x;
+fun locale_add_declaration new_locale x =
+ if !new_locales andalso new_locale then NewLocale.add_declaration x else Locale.add_declaration x;
+fun locale_add_thmss new_locale x =
+ if !new_locales andalso new_locale then NewLocale.add_thmss x else Locale.add_thmss x;
+fun locale_init new_locale x =
+ if !new_locales andalso new_locale then NewLocale.init x else Locale.init x;
+fun locale_intern new_locale x =
+ if !new_locales andalso 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
(
@@ -58,7 +65,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, [])]))
@@ -73,7 +80,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]
@@ -83,7 +90,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';
@@ -94,7 +101,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;
@@ -160,7 +167,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
@@ -179,7 +186,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;
@@ -328,13 +335,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, ...}) =
@@ -359,7 +367,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
@@ -367,9 +375,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/ZF/Constructible/L_axioms.thy Tue Dec 16 15:08:08 2008 +0100
+++ b/src/ZF/Constructible/L_axioms.thy Tue Dec 16 15:09:37 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 Tue Dec 16 15:08:08 2008 +0100
+++ b/src/ZF/Constructible/Rec_Separation.thy Tue Dec 16 15:09:37 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 Tue Dec 16 15:08:08 2008 +0100
+++ b/src/ZF/Constructible/Separation.thy Tue Dec 16 15:09:37 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/ROOT.ML Tue Dec 16 15:08:08 2008 +0100
+++ b/src/ZF/ROOT.ML Tue Dec 16 15:09:37 2008 +0100
@@ -8,5 +8,6 @@
Paulson.
*)
+set new_locales;
use_thys ["Main", "Main_ZFC"];
--- a/src/ZF/ex/Group.thy Tue Dec 16 15:08:08 2008 +0100
+++ b/src/ZF/ex/Group.thy Tue Dec 16 15:09:37 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 Tue Dec 16 15:08:08 2008 +0100
+++ b/src/ZF/ex/Ring.thy Tue Dec 16 15:09:37 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]