--- a/src/HOL/Dense_Linear_Order.thy Fri Jan 16 08:29:11 2009 +0100
+++ b/src/HOL/Dense_Linear_Order.thy Fri Jan 16 14:58:11 2009 +0100
@@ -301,7 +301,7 @@
text {* Linear order without upper bounds *}
-class_locale linorder_stupid_syntax = linorder
+locale linorder_stupid_syntax = linorder
begin
notation
less_eq ("op \<sqsubseteq>") and
@@ -311,7 +311,7 @@
end
-class_locale linorder_no_ub = linorder_stupid_syntax +
+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 *}
-class_locale linorder_no_lb = linorder_stupid_syntax +
+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
-class_locale constr_dense_linear_order = linorder_no_lb + linorder_no_ub +
+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"
-class_interpretation constr_dense_linear_order < dense_linear_order
+sublocale 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,9 +635,9 @@
using eq_diff_eq[where a= x and b=t and c=0] by simp
-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)"]
+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)
fix x y::'a assume lt: "x < y"
from less_half_sum[OF lt] show "x < (x + y) /2" by simp
--- a/src/HOL/Divides.thy Fri Jan 16 08:29:11 2009 +0100
+++ b/src/HOL/Divides.thy Fri Jan 16 14:58:11 2009 +0100
@@ -20,7 +20,7 @@
subsection {* Abstract division in commutative semirings. *}
-class semiring_div = comm_semiring_1_cancel + div +
+class semiring_div = comm_semiring_1_cancel + div +
assumes mod_div_equality: "a div b * b + a mod b = a"
and div_by_0 [simp]: "a div 0 = 0"
and div_0 [simp]: "0 div a = 0"
@@ -800,7 +800,7 @@
text {* @{term "op dvd"} is a partial order *}
-class_interpretation dvd: order ["op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"]
+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 Fri Jan 16 08:29:11 2009 +0100
+++ b/src/HOL/Finite_Set.thy Fri Jan 16 14:58:11 2009 +0100
@@ -873,7 +873,7 @@
subsection {* Generalized summation over a set *}
-class_interpretation comm_monoid_add: comm_monoid_mult ["0::'a::comm_monoid_add" "op +"]
+interpretation comm_monoid_add!: comm_monoid_mult "0::'a::comm_monoid_add" "op +"
proof qed (auto intro: add_assoc add_commute)
definition setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
@@ -1760,7 +1760,7 @@
proof (induct rule: finite_induct)
case empty then show ?case by simp
next
- class_interpret ab_semigroup_mult ["op Un"]
+ interpret ab_semigroup_mult "op Un"
proof qed auto
case insert
then show ?case by simp
@@ -2198,7 +2198,7 @@
assumes "finite A" "A \<noteq> {}"
shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
proof -
- class_interpret ab_semigroup_idem_mult [inf]
+ 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
- class_interpret ab_semigroup_idem_mult [inf]
+ 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 -
- class_interpret ab_semigroup_idem_mult [inf]
+ 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
- class_interpret ab_semigroup_idem_mult [inf]
+ 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 -
- class_interpret ab_semigroup_idem_mult [sup]
+ 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
- class_interpret ab_semigroup_idem_mult [sup]
+ 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 -
- class_interpret ab_semigroup_idem_mult [inf]
+ 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 -
- class_interpret ab_semigroup_idem_mult [sup]
+ 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 -
- class_interpret ab_semigroup_idem_mult [min]
+ 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 -
- class_interpret ab_semigroup_idem_mult [min]
+ 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 -
- class_interpret ab_semigroup_idem_mult [min]
+ 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
- class_interpret ab_semigroup_idem_mult [min]
+ 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 -
- class_interpret ab_semigroup_idem_mult [min]
+ 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 -
- class_interpret ab_semigroup_idem_mult [max]
+ 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 -
- class_interpret ab_semigroup_idem_mult [min]
+ 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 -
- class_interpret ab_semigroup_idem_mult [max]
+ 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 -
- class_interpret ab_semigroup_idem_mult [min]
+ 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 -
- class_interpret ab_semigroup_idem_mult [max]
+ 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 -
- class_interpret ab_semigroup_idem_mult [min]
+ 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 -
- class_interpret ab_semigroup_idem_mult [max]
+ 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 -
- class_interpret lower_semilattice ["op \<le>" "op <" min]
+ interpret lower_semilattice "op \<le>" "op <" min
by (rule min_lattice)
from assms show ?thesis by (simp add: Min_def fold1_belowI)
qed
@@ -2602,7 +2602,7 @@
assumes "finite A" and "x \<in> A"
shows "x \<le> Max A"
proof -
- invoke lower_semilattice ["op \<ge>" "op >" max]
+ interpret lower_semilattice "op \<ge>" "op >" max
by (rule max_lattice)
from assms show ?thesis by (simp add: Max_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 -
- class_interpret lower_semilattice ["op \<le>" "op <" min]
+ interpret lower_semilattice "op \<le>" "op <" min
by (rule min_lattice)
from assms show ?thesis by (simp add: Min_def below_fold1_iff)
qed
@@ -2620,7 +2620,7 @@
assumes "finite A" and "A \<noteq> {}"
shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
proof -
- invoke lower_semilattice ["op \<ge>" "op >" max]
+ interpret lower_semilattice "op \<ge>" "op >" max
by (rule max_lattice)
from assms show ?thesis by (simp add: Max_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 -
- class_interpret lower_semilattice ["op \<le>" "op <" min]
+ 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
- class_interpret linorder ["op \<ge>" "op >"]
+ 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 -
- class_interpret lower_semilattice ["op \<le>" "op <" min]
+ 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
- class_interpret linorder ["op \<ge>" "op >"]
+ 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 -
- class_interpret lower_semilattice ["op \<le>" "op <" min]
+ 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
- class_interpret linorder ["op \<ge>" "op >"]
+ 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 -
- class_interpret distrib_lattice ["op \<le>" "op <" min max]
+ 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
- class_interpret linorder ["op \<ge>" "op >"]
+ 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/Lattices.thy Fri Jan 16 08:29:11 2009 +0100
+++ b/src/HOL/Lattices.thy Fri Jan 16 14:58:11 2009 +0100
@@ -300,8 +300,7 @@
by auto
qed (auto simp add: min_def max_def not_le less_imp_le)
-class_interpretation min_max:
- distrib_lattice ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max]
+interpretation min_max!: distrib_lattice "op \<le> :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max
by (rule distrib_lattice_min_max)
lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{lower_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
--- a/src/HOL/Library/Multiset.thy Fri Jan 16 08:29:11 2009 +0100
+++ b/src/HOL/Library/Multiset.thy Fri Jan 16 14:58:11 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Library/Multiset.thy
- ID: $Id$
Author: Tobias Nipkow, Markus Wenzel, Lawrence C Paulson, Norbert Voelker
*)
@@ -1080,16 +1079,16 @@
apply simp
done
-class_interpretation mset_order: order ["op \<le>#" "op <#"]
+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)
-class_interpretation mset_order_cancel_semigroup:
- pordered_cancel_ab_semigroup_add ["op +" "op \<le>#" "op <#"]
+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])
-class_interpretation mset_order_semigroup_cancel:
- pordered_ab_semigroup_add_imp_le ["op +" "op \<le>#" "op <#"]
+interpretation mset_order_semigroup_cancel!:
+ pordered_ab_semigroup_add_imp_le "op +" "op \<le>#" "op <#"
proof qed simp
@@ -1156,7 +1155,7 @@
then show ?case using T by simp
qed
-lemmas mset_less_trans = mset_order.less_eq_less.less_trans
+lemmas mset_less_trans = mset_order.less_trans
lemma mset_less_diff_self: "c \<in># B \<Longrightarrow> B - {#c#} \<subset># B"
by (auto simp: mset_le_def mset_less_def multi_drop_mem_not_eq)
--- a/src/HOL/Library/SetsAndFunctions.thy Fri Jan 16 08:29:11 2009 +0100
+++ b/src/HOL/Library/SetsAndFunctions.thy Fri Jan 16 14:58:11 2009 +0100
@@ -107,26 +107,26 @@
apply simp
done
-class_interpretation set_semigroup_add: semigroup_add ["op \<oplus> :: ('a::semigroup_add) set => 'a set => 'a set"]
+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
-class_interpretation set_semigroup_mult: semigroup_mult ["op \<otimes> :: ('a::semigroup_mult) set => 'a set => 'a set"]
+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
-class_interpretation set_comm_monoid_add: comm_monoid_add ["{0}" "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set"]
+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
-class_interpretation set_comm_monoid_mult: comm_monoid_mult ["{1}" "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set"]
+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 Fri Jan 16 08:29:11 2009 +0100
+++ b/src/HOL/List.thy Fri Jan 16 14:58:11 2009 +0100
@@ -547,9 +547,9 @@
lemma append_Nil2 [simp]: "xs @ [] = xs"
by (induct xs) auto
-class_interpretation semigroup_append: semigroup_add ["op @"]
+interpretation semigroup_append!: semigroup_add "op @"
proof qed simp
-class_interpretation monoid_append: monoid_add ["[]" "op @"]
+interpretation monoid_append!: monoid_add "[]" "op @"
proof qed simp+
lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])"
--- a/src/HOL/Statespace/StateSpaceEx.thy Fri Jan 16 08:29:11 2009 +0100
+++ b/src/HOL/Statespace/StateSpaceEx.thy Fri Jan 16 14:58:11 2009 +0100
@@ -41,7 +41,7 @@
projection~/ injection functions that convert from abstract values to
@{typ "nat"} and @{text "bool"}. The logical content of the locale is: *}
-class_locale vars' =
+locale vars' =
fixes n::'name and b::'name
assumes "distinct [n, b]"
--- a/src/HOL/Word/WordArith.thy Fri Jan 16 08:29:11 2009 +0100
+++ b/src/HOL/Word/WordArith.thy Fri Jan 16 14:58:11 2009 +0100
@@ -22,7 +22,7 @@
proof
qed (unfold word_sle_def word_sless_def, auto)
-class_interpretation signed: linorder ["word_sle" "word_sless"]
+interpretation signed!: linorder "word_sle" "word_sless"
by (rule signed_linorder)
lemmas word_arith_wis =
--- a/src/Pure/Isar/class.ML Fri Jan 16 08:29:11 2009 +0100
+++ b/src/Pure/Isar/class.ML Fri Jan 16 14:58:11 2009 +0100
@@ -27,9 +27,9 @@
(** rule calculation **)
fun calculate_axiom thy sups base_sort assm_axiom param_map class =
- case Old_Locale.intros thy class
- of (_, []) => assm_axiom
- | (_, [intro]) =>
+ case Locale.intros_of thy class
+ of (_, NONE) => assm_axiom
+ | (_, SOME intro) =>
let
fun instantiate thy sort = Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o pair (Name.aT, 0))
(base_sort, sort)], map (fn (v, (c, ty)) => pairself (Thm.cterm_of thy)
@@ -45,23 +45,22 @@
|> SOME
end;
-fun raw_morphism thy class param_map some_axiom =
+fun raw_morphism thy class sups param_map some_axiom =
let
val ctxt = ProofContext.init thy;
- val some_wit = case some_axiom
- of SOME axiom => SOME (Element.prove_witness ctxt
- (Logic.unvarify (Thm.prop_of axiom))
- (ALLGOALS (ProofContext.fact_tac [axiom])))
- | NONE => NONE;
- val instT = Symtab.empty |> Symtab.update ("'a", TFree ("'a", [class]));
- val inst = Symtab.make ((map o apsnd) Const param_map);
- in case some_wit
- of SOME wit => Element.inst_morphism thy (instT, inst)
- $> Morphism.binding_morphism (Binding.add_prefix false (class_prefix class))
- $> Element.satisfy_morphism [wit]
- | NONE => Element.inst_morphism thy (instT, inst)
- $> Morphism.binding_morphism (Binding.add_prefix false (class_prefix class))
- end;
+ val (([props], [(_, morph1)], export_morph), _) = ctxt
+ |> Expression.cert_goal_expression ([(class, (("", false),
+ Expression.Named ((map o apsnd) Const param_map)))], []);
+ val morph2 = morph1
+ $> Morphism.binding_morphism (Binding.add_prefix false (class_prefix class));
+ val morph3 = case props
+ of [prop] => morph2
+ $> Element.satisfy_morphism [(Element.prove_witness ctxt prop
+ (ALLGOALS (ProofContext.fact_tac (the_list some_axiom))))]
+ | [] => morph2;
+ (*FIXME generic amend operation for classes*)
+ val morph4 = morph3 $> eq_morph thy (these_defs thy sups);
+ in (morph4, export_morph) end;
fun calculate_rules thy morph sups base_sort param_map axiom class =
let
@@ -70,19 +69,18 @@
(Var ((v, 0), map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty),
Const (c, map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty))) param_map);
val defs = these_defs thy sups;
- val assm_intro = Old_Locale.intros thy class
+ val assm_intro = Locale.intros_of thy class
|> fst
- |> map (instantiate thy base_sort)
- |> map (MetaSimplifier.rewrite_rule defs)
- |> map Thm.close_derivation
- |> try the_single;
+ |> Option.map (instantiate thy base_sort)
+ |> Option.map (MetaSimplifier.rewrite_rule defs)
+ |> Option.map Thm.close_derivation;
val fixate = Thm.instantiate
(map (pairself (Thm.ctyp_of thy)) [(TVar ((Name.aT, 0), []), TFree (Name.aT, base_sort)),
(TVar ((Name.aT, 0), base_sort), TFree (Name.aT, base_sort))], [])
val of_class_sups = if null sups
then map (fixate o Thm.class_triv thy) base_sort
else map (fixate o snd o rules thy) sups;
- val locale_dests = map Drule.standard' (Old_Locale.dests thy class);
+ val locale_dests = map Drule.standard' (Locale.axioms_of thy class);
val num_trivs = case length locale_dests
of 0 => if is_none axiom then 0 else 1
| n => n;
@@ -110,55 +108,54 @@
local
-fun gen_class_spec prep_class process_expr thy raw_supclasses raw_elems =
+fun gen_class_spec prep_class process_decl thy raw_supclasses raw_elems =
let
val supclasses = map (prep_class thy) raw_supclasses;
val supsort = Sign.minimize_sort thy supclasses;
val sups = filter (is_class thy) supsort;
- val supparam_names = map fst (these_params thy sups);
+ val base_sort = if null sups then supsort else
+ foldr1 (Sorts.inter_sort (Sign.classes_of thy))
+ (map (base_sort thy) sups);
+ val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
+ val supparam_names = map fst supparams;
val _ = if has_duplicates (op =) supparam_names
then error ("Duplicate parameter(s) in superclasses: "
^ (commas o map quote o duplicates (op =)) supparam_names)
else ();
- val base_sort = if null sups then supsort else
- foldr1 (Sorts.inter_sort (Sign.classes_of thy))
- (map (base_sort thy) sups);
- val suplocales = map Old_Locale.Locale sups;
- val supexpr = Old_Locale.Merge suplocales;
- val supparams = (map fst o Old_Locale.parameters_of_expr thy) supexpr;
- val mergeexpr = Old_Locale.Merge suplocales;
+
+ val supexpr = (map (fn sup => (sup, (("", false), Expression.Positional [])))
+ sups, []);
val constrain = Element.Constrains ((map o apsnd o map_atyps)
(K (TFree (Name.aT, base_sort))) supparams);
+ (*FIXME perhaps better: control type variable by explicit
+ parameter instantiation of import expression*)
+ val begin_ctxt = begin sups base_sort
+ #> fold (Variable.declare_constraints o Free) ((map o apsnd o map_atyps)
+ (K (TFree (Name.aT, base_sort))) supparams) (*FIXME
+ should constraints be issued in begin?*)
+ val ((_, _, syntax_elems), _) = ProofContext.init thy
+ |> begin_ctxt
+ |> process_decl supexpr raw_elems;
fun fork_syn (Element.Fixes xs) =
fold_map (fn (c, ty, syn) => cons (Binding.base_name c, syn) #> pair (c, ty, NoSyn)) xs
#>> Element.Fixes
| fork_syn x = pair x;
- fun fork_syntax elems =
- let
- val (elems', global_syntax) = fold_map fork_syn elems [];
- in (constrain :: elems', global_syntax) end;
- val (elems, global_syntax) =
- ProofContext.init thy
- |> Old_Locale.cert_expr supexpr [constrain]
- |> snd
- |> begin sups base_sort
- |> process_expr Old_Locale.empty raw_elems
- |> fst
- |> fork_syntax
- in (((sups, supparams), (supsort, base_sort, mergeexpr)), (elems, global_syntax)) end;
+ val (elems, global_syntax) = fold_map fork_syn syntax_elems [];
+ in (((sups, supparam_names), (supsort, base_sort, supexpr)), (constrain :: elems, global_syntax)) end;
-val read_class_spec = gen_class_spec Sign.intern_class Old_Locale.read_expr;
-val check_class_spec = gen_class_spec (K I) Old_Locale.cert_expr;
+val cert_class_spec = gen_class_spec (K I) Expression.cert_declaration;
+val read_class_spec = gen_class_spec Sign.intern_class Expression.cert_read_declaration;
fun add_consts bname class base_sort sups supparams global_syntax thy =
let
- val supconsts = map fst supparams
+ val supconsts = supparams
|> AList.make (snd o the o AList.lookup (op =) (these_params thy sups))
|> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]);
- val all_params = map fst (Old_Locale.parameters_of thy class);
+ val all_params = Locale.params_of thy class;
val raw_params = (snd o chop (length supparams)) all_params;
- fun add_const (v, raw_ty) thy =
+ fun add_const (b, SOME raw_ty, _) thy =
let
+ val v = Binding.base_name b;
val c = Sign.full_bname thy v;
val ty = map_atyps (K (TFree (Name.aT, base_sort))) raw_ty;
val ty0 = Type.strip_sorts ty;
@@ -183,9 +180,9 @@
fun globalize param_map = map_aterms
(fn Free (v, ty) => Const ((fst o the o AList.lookup (op =) param_map) v, ty)
| t => t);
- val raw_pred = Old_Locale.intros thy class
+ val raw_pred = Locale.intros_of thy class
|> fst
- |> map (Logic.unvarify o Logic.strip_imp_concl o Thm.prop_of);
+ |> Option.map (Logic.unvarify o Logic.strip_imp_concl o Thm.prop_of);
fun get_axiom thy = case (#axioms o AxClass.get_info thy) class
of [] => NONE
| [thm] => SOME thm;
@@ -194,7 +191,8 @@
|> add_consts bname class base_sort sups supparams global_syntax
|-> (fn (param_map, params) => AxClass.define_class (bname, supsort)
(map (fst o snd) params)
- [((Binding.name (bname ^ "_" ^ AxClass.axiomsN), []), map (globalize param_map) raw_pred)]
+ [(((*Binding.name (bname ^ "_" ^ AxClass.axiomsN*) Binding.empty, []),
+ Option.map (globalize param_map) raw_pred |> the_list)]
#> snd
#> `get_axiom
#-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params
@@ -204,35 +202,42 @@
fun gen_class prep_spec bname raw_supclasses raw_elems thy =
let
val class = Sign.full_bname thy bname;
- val (((sups, supparams), (supsort, base_sort, mergeexpr)), (elems, global_syntax)) =
+ val (((sups, supparams), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
prep_spec thy raw_supclasses raw_elems;
- val supconsts = map (apsnd fst o snd) (these_params thy sups);
+ (*val export_morph = (*FIXME how canonical is this?*)
+ Morphism.morphism { binding = I, var = I,
+ typ = Logic.varifyT,
+ term = (*map_types Logic.varifyT*) I,
+ fact = map Thm.varifyT
+ } $> Morphism.morphism { binding = I, var = I,
+ typ = Logic.type_map TermSubst.zero_var_indexes,
+ term = TermSubst.zero_var_indexes,
+ fact = Drule.zero_var_indexes_list o map Thm.strip_shyps
+ };*)
in
thy
- |> Old_Locale.add_locale "" bname mergeexpr elems
- |> snd
- |> ProofContext.theory_of
+ |> Expression.add_locale bname "" supexpr elems
+ |> snd |> LocalTheory.exit_global
|> adjungate_axclass bname class base_sort sups supsort supparams global_syntax
|-> (fn (inst, param_map, params, assm_axiom) =>
- `(fn thy => calculate_axiom thy sups base_sort assm_axiom param_map class)
+ `(fn thy => calculate_axiom thy sups base_sort assm_axiom param_map class)
#-> (fn axiom =>
- prove_class_interpretation class inst
- (supconsts @ map (pair class o fst o snd) params) (the_list axiom) []
- #> `(fn thy => raw_morphism thy class param_map axiom)
- #-> (fn morph =>
- `(fn thy => calculate_rules thy morph sups base_sort param_map axiom class)
+ `(fn thy => raw_morphism thy class sups param_map axiom)
+ #-> (fn (morph, export_morph) => Locale.add_registration (class, (morph, export_morph))
+ #> Locale.activate_global_facts (class, morph $> export_morph)
+ #> `(fn thy => calculate_rules thy morph sups base_sort param_map axiom class)
#-> (fn (assm_intro, of_class) =>
register class sups params base_sort inst
morph axiom assm_intro of_class
- #> fold (note_assm_intro class) (the_list assm_intro)))))
+ (*#> fold (note_assm_intro class) (the_list assm_intro*)))))
|> TheoryTarget.init (SOME class)
|> pair class
end;
in
+val class = gen_class cert_class_spec;
val class_cmd = gen_class read_class_spec;
-val class = gen_class check_class_spec;
end; (*local*)
@@ -241,6 +246,12 @@
local
+fun prove_sublocale tac (sub, expr) =
+ Expression.sublocale sub expr
+ #> Proof.global_terminal_proof
+ (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
+ #> ProofContext.theory_of;
+
fun gen_subclass prep_class do_proof raw_sup lthy =
let
val thy = ProofContext.theory_of lthy;
@@ -258,16 +269,18 @@
val _ = if null err_params then [] else
error ("Class " ^ Syntax.string_of_sort lthy [sub] ^ " lacks parameter(s) " ^
commas_quote err_params ^ " of " ^ Syntax.string_of_sort lthy [sup]);
- val sublocale_prop =
- Old_Locale.global_asms_of thy sup
- |> maps snd
- |> try the_single
- |> Option.map (ObjectLogic.ensure_propT thy);
+
+ val expr = ([(sup, (("", false), Expression.Positional []))], []);
+ val (([props], _, _), goal_ctxt) =
+ Expression.cert_goal_expression expr lthy;
+ val some_prop = try the_single props; (*FIXME*)
fun after_qed some_thm =
- LocalTheory.theory (prove_subclass_relation (sub, sup) some_thm)
+ LocalTheory.theory (register_subclass (sub, sup) some_thm)
+ #> is_some some_thm ? LocalTheory.theory
+ (prove_sublocale (ALLGOALS (ProofContext.fact_tac (the_list some_thm))) (sub, expr))
#> (TheoryTarget.init (SOME sub) o ProofContext.theory_of);
in
- do_proof after_qed sublocale_prop lthy
+ do_proof after_qed some_prop lthy
end;
fun user_proof after_qed NONE =
--- a/src/Pure/Isar/class_target.ML Fri Jan 16 08:29:11 2009 +0100
+++ b/src/Pure/Isar/class_target.ML Fri Jan 16 14:58:11 2009 +0100
@@ -10,6 +10,8 @@
val register: class -> class list -> ((string * typ) * (string * typ)) list
-> sort -> term list -> morphism
-> thm option -> thm option -> thm -> theory -> theory
+ val register_subclass: class * class -> thm option
+ -> theory -> theory
val begin: class list -> sort -> Proof.context -> Proof.context
val init: class -> theory -> Proof.context
@@ -21,14 +23,12 @@
val intro_classes_tac: thm list -> tactic
val default_intro_tac: Proof.context -> thm list -> tactic
- val prove_class_interpretation: class -> term list -> (class * string) list
- -> thm list -> thm list -> theory -> theory
- val prove_subclass_relation: class * class -> thm option -> theory -> theory
val class_prefix: string -> string
val is_class: theory -> class -> bool
val these_params: theory -> sort -> (string * (class * (string * typ))) list
val these_defs: theory -> sort -> thm list
+ val eq_morph: theory -> thm list -> morphism
val base_sort: theory -> class -> sort
val rules: theory -> class -> thm option * thm
val print_classes: theory -> unit
@@ -64,36 +64,6 @@
structure Class_Target : CLASS_TARGET =
struct
-(*temporary adaption code to mediate between old and new locale code*)
-
-structure Locale_Layer =
-struct
-
-val init = Old_Locale.init;
-val parameters_of = Old_Locale.parameters_of;
-val intros = Old_Locale.intros;
-val dests = Old_Locale.dests;
-val get_interpret_morph = Old_Locale.get_interpret_morph;
-val Locale = Old_Locale.Locale;
-val extern = Old_Locale.extern;
-val intro_locales_tac = Old_Locale.intro_locales_tac;
-
-fun prove_interpretation tac prfx_atts expr inst =
- Old_Locale.interpretation I prfx_atts expr inst
- ##> Proof.global_terminal_proof
- (Method.Basic (fn ctxt => Method.SIMPLE_METHOD (tac ctxt), Position.none), NONE)
- ##> ProofContext.theory_of;
-
-fun prove_interpretation_in tac after_qed (name, expr) =
- Old_Locale.interpretation_in_locale
- (ProofContext.theory after_qed) (name, expr)
- #> Proof.global_terminal_proof
- (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
- #> ProofContext.theory_of;
-
-end;
-
-
(** primitive axclass and instance commands **)
fun axclass_cmd (class, raw_superclasses) raw_specs thy =
@@ -201,6 +171,8 @@
val ancestry = Graph.all_succs o ClassData.get;
+val heritage = Graph.all_preds o ClassData.get;
+
fun the_inst thy = #inst o the_class_data thy;
fun these_params thy =
@@ -235,14 +207,14 @@
fun class_binding_morph class =
Binding.map_prefix (K (Binding.add_prefix false (class_prefix class)));
+fun eq_morph thy thms = (*FIXME how general is this?*)
+ Morphism.term_morphism (MetaSimplifier.rewrite_term thy thms [])
+ $> Morphism.thm_morphism (MetaSimplifier.rewrite_rule thms);
+
fun morphism thy class =
let
val { base_morph, defs, ... } = the_class_data thy class;
- in
- base_morph
- $> Morphism.term_morphism (MetaSimplifier.rewrite_term thy defs [])
- $> Morphism.thm_morphism (MetaSimplifier.rewrite_rule defs)
- end;
+ in base_morph $> eq_morph thy defs end;
fun print_classes thy =
let
@@ -265,7 +237,7 @@
(SOME o Pretty.block) [Pretty.str "supersort: ",
(Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class],
if is_class thy class then (SOME o Pretty.str)
- ("locale: " ^ Locale_Layer.extern thy class) else NONE,
+ ("locale: " ^ Locale.extern thy class) else NONE,
((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks)
(Pretty.str "parameters:" :: ps)) o map mk_param
o these o Option.map #params o try (AxClass.get_info thy)) class,
@@ -312,39 +284,26 @@
(** tactics and methods **)
-fun prove_class_interpretation class inst consts hyp_facts def_facts thy =
- let
- val constraints = map (fn (class, c) => map_atyps (K (TFree (Name.aT,
- [class]))) (Sign.the_const_type thy c)) consts;
- val no_constraints = map (map_atyps (K (TFree (Name.aT, [])))) constraints;
- fun add_constraint c T = Sign.add_const_constraint (c, SOME T);
- fun tac ctxt = ALLGOALS (ProofContext.fact_tac (hyp_facts @ def_facts)
- ORELSE' (fn n => SELECT_GOAL (Locale_Layer.intro_locales_tac false ctxt []) n));
- val prfx = class_prefix class;
- in
- thy
- |> fold2 add_constraint (map snd consts) no_constraints
- |> Locale_Layer.prove_interpretation tac (class_binding_morph class) (Locale_Layer.Locale class)
- (map SOME inst, map (pair (Attrib.empty_binding) o Thm.prop_of) def_facts)
- |> snd
- |> fold2 add_constraint (map snd consts) constraints
- end;
-
-fun prove_subclass_relation (sub, sup) some_thm thy =
+fun register_subclass (sub, sup) thms thy =
let
val of_class = (snd o rules thy) sup;
- val intro = case some_thm
+ val intro = case thms
of SOME thm => Drule.standard' (of_class OF [Drule.standard' thm])
| NONE => Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o pair (Name.aT, 0))
([], [sub])], []) of_class;
val classrel = (intro OF (the_list o fst o rules thy) sub)
|> Thm.close_derivation;
+ (*FIXME generic amend operation for classes*)
+ val amendments = map (fn class => (class, morphism thy class))
+ (heritage thy [sub]);
+ val diff_sort = Sign.complete_sort thy [sup]
+ |> subtract (op =) (Sign.complete_sort thy [sub]);
+ val defs_morph = eq_morph thy (these_defs thy diff_sort);
in
thy
|> AxClass.add_classrel classrel
- |> Locale_Layer.prove_interpretation_in (ALLGOALS (ProofContext.fact_tac (the_list some_thm)))
- I (sub, Locale_Layer.Locale sup)
|> ClassData.map (Graph.add_edge (sub, sup))
+ |> fold (Locale.amend_registration defs_morph) amendments
end;
fun intro_classes_tac facts st =
@@ -428,7 +387,7 @@
fun init class thy =
thy
- |> Locale_Layer.init class
+ |> Locale.init class
|> begin [class] (base_sort thy class);
@@ -441,12 +400,18 @@
val morph = morphism thy' class;
val inst = the_inst thy' class;
val params = map (apsnd fst o snd) (these_params thy' [class]);
+ val amendments = map (fn class => (class, morphism thy' class))
+ (heritage thy' [class]);
val c' = Sign.full_bname thy' c;
val dict' = Morphism.term morph dict;
val ty' = Term.fastype_of dict';
val ty'' = Type.strip_sorts ty';
val def_eq = Logic.mk_equals (Const (c', ty'), dict');
+ (*FIXME a mess*)
+ fun amend def def' (class, morph) thy =
+ Locale.amend_registration (eq_morph thy [Thm.varifyT def])
+ (class, morph) thy;
fun get_axiom thy = ((Thm.varifyT o Thm.axiom thy) c', thy);
in
thy'
@@ -454,9 +419,9 @@
|> Thm.add_def false false (c, def_eq)
|>> Thm.symmetric
||>> get_axiom
- |-> (fn (def, def') => prove_class_interpretation class inst params [] [def]
- #> register_operation class (c', (dict', SOME (Thm.symmetric def')))
- #> PureThy.store_thm (c ^ "_raw", def')
+ |-> (fn (def, def') => register_operation class (c', (dict', SOME (Thm.symmetric def')))
+ #> fold (amend def def') amendments
+ #> PureThy.store_thm (c ^ "_raw", def') (*FIXME name*)
#> snd)
|> Sign.restore_naming thy
|> Sign.add_const_constraint (c', SOME ty')