Porting to new locales.
--- a/etc/isar-keywords-ZF.el Fri Dec 12 17:00:42 2008 +0100
+++ b/etc/isar-keywords-ZF.el Fri Dec 12 20:03:30 2008 +0100
@@ -40,6 +40,9 @@
"chapter"
"class"
"class_deps"
+ "class_interpret"
+ "class_interpretation"
+ "class_locale"
"classes"
"classrel"
"codatatype"
@@ -349,6 +352,7 @@
"axiomatization"
"axioms"
"class"
+ "class_locale"
"classes"
"classrel"
"codatatype"
@@ -411,7 +415,8 @@
'("inductive_cases"))
(defconst isar-keywords-theory-goal
- '("corollary"
+ '("class_interpretation"
+ "corollary"
"instance"
"interpretation"
"lemma"
@@ -438,7 +443,8 @@
"subsubsect"))
(defconst isar-keywords-proof-goal
- '("have"
+ '("class_interpret"
+ "have"
"hence"
"interpret"
"invoke"))
--- a/src/HOL/Library/Dense_Linear_Order.thy Fri Dec 12 17:00:42 2008 +0100
+++ b/src/HOL/Library/Dense_Linear_Order.thy Fri Dec 12 20:03:30 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/Real/RealVector.thy Fri Dec 12 17:00:42 2008 +0100
+++ b/src/HOL/Real/RealVector.thy Fri Dec 12 20:03:30 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)
@@ -152,7 +152,7 @@
and scaleR_one [simp]: "scaleR 1 x = x"
interpretation real_vector:
- vector_space ["scaleR :: real \<Rightarrow> 'a \<Rightarrow> 'a::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:
@@ -797,7 +797,7 @@
end
interpretation mult:
- bounded_bilinear ["op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra"]
+ bounded_bilinear "op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra"
apply (rule bounded_bilinear.intro)
apply (rule left_distrib)
apply (rule right_distrib)
@@ -808,18 +808,18 @@
done
interpretation mult_left:
- bounded_linear ["(\<lambda>x::'a::real_normed_algebra. x * y)"]
+ 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)"]
+ 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)"]
+ 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