# HG changeset patch # User haftmann # Date 1232114346 -3600 # Node ID 25472dc71a4b897cdb63d578ac8f64929bceec30 # Parent b0e01a48867c5a2724fdcf4a70a976ea6024b0f6# Parent 7071b017cb3519456575f68a1c2a3192535a9711 merged diff -r b0e01a48867c -r 25472dc71a4b src/HOL/Dense_Linear_Order.thy --- a/src/HOL/Dense_Linear_Order.thy Fri Jan 16 12:11:06 2009 +0100 +++ b/src/HOL/Dense_Linear_Order.thy Fri Jan 16 14:59:06 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 \") and @@ -311,7 +311,7 @@ end -class_locale linorder_no_ub = linorder_stupid_syntax + +locale linorder_no_ub = linorder_stupid_syntax + assumes gt_ex: "\y. less x y" begin lemma ge_ex: "\y. x \ y" using gt_ex by auto @@ -360,7 +360,7 @@ text {* Linear order without upper bounds *} -class_locale linorder_no_lb = linorder_stupid_syntax + +locale linorder_no_lb = linorder_stupid_syntax + assumes lt_ex: "\y. less y x" begin lemma le_ex: "\y. y \ x" using lt_ex by auto @@ -407,12 +407,12 @@ end -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 \ less x (between x y) \ 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 <" - "\ 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 <" + "\ 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 diff -r b0e01a48867c -r 25472dc71a4b src/HOL/Divides.thy --- a/src/HOL/Divides.thy Fri Jan 16 12:11:06 2009 +0100 +++ b/src/HOL/Divides.thy Fri Jan 16 14:59:06 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" "\n m \ nat. n dvd m \ \ m dvd n"] +interpretation dvd!: order "op dvd" "\n m \ nat. n dvd m \ \ m dvd n" proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym) lemma dvd_diff: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)" diff -r b0e01a48867c -r 25472dc71a4b src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Fri Jan 16 12:11:06 2009 +0100 +++ b/src/HOL/Finite_Set.thy Fri Jan 16 14:59:06 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 \ {}" shows "x \ fold1 inf A \ (\a\A. x \ 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 \ a \ F" by simp @@ -2288,7 +2288,7 @@ and "A \ {}" shows "sup x (\\<^bsub>fin\<^esub>A) = \\<^bsub>fin\<^esub>{sup x a|a. a \ A}" proof - - 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 \ B}" @@ -2333,7 +2333,7 @@ assumes "finite A" and "A \ {}" shows "inf x (\\<^bsub>fin\<^esub>A) = \\<^bsub>fin\<^esub>{inf x a|a. a \ A}" proof - - 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 \ A \ b \ B} \ {}" 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 (\\<^bsub>fin\<^esub>(insert x A)) (\\<^bsub>fin\<^esub>B) = inf (sup x (\\<^bsub>fin\<^esub>A)) (\\<^bsub>fin\<^esub>B)" using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def]) @@ -2386,7 +2386,7 @@ assumes "finite A" and "A \ {}" shows "\\<^bsub>fin\<^esub>A = Inf A" proof - - 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 \ {}" shows "\\<^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 \ {}" shows "x < fold1 min A \ (\a\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 \ {}" shows "fold1 min A \ x \ (\a\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) @@ -2468,7 +2468,7 @@ assumes "finite A" and "A \ {}" shows "fold1 min A < x \ (\a\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 \ B" have B: "B = A \ (B-A)" using `A \ B` by blast @@ -2515,7 +2515,7 @@ assumes "finite A" and "A \ {}" shows "Min (insert x A) = min x (Min A)" proof - - 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 \ {}" 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 \ {}" shows "Min A \ 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 \ {}" shows "Max A \ 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 \ {}" and "finite B" and "B \ {}" shows "Min (A \ 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 \ {}" and "finite B" and "B \ {}" shows "Max (A \ 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 \ {}" 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 \ {}" 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 \ A" shows "Min A \ x" proof - - class_interpret lower_semilattice ["op \" "op <" min] + interpret lower_semilattice "op \" "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 \ A" shows "x \ Max A" proof - - invoke lower_semilattice ["op \" "op >" max] + interpret lower_semilattice "op \" "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 \ {}" shows "x \ Min A \ (\a\A. x \ a)" proof - - class_interpret lower_semilattice ["op \" "op <" min] + interpret lower_semilattice "op \" "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 \ {}" shows "Max A \ x \ (\a\A. a \ x)" proof - - invoke lower_semilattice ["op \" "op >" max] + interpret lower_semilattice "op \" "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 \ {}" shows "x < Min A \ (\a\A. x < a)" proof - - class_interpret lower_semilattice ["op \" "op <" min] + interpret lower_semilattice "op \" "op <" min by (rule min_lattice) from assms show ?thesis by (simp add: Min_def strict_below_fold1_iff) qed @@ -2639,7 +2639,7 @@ shows "Max A < x \ (\a\A. a < x)" proof - note Max = Max_def - class_interpret linorder ["op \" "op >"] + interpret linorder "op \" "op >" by (rule dual_linorder) from assms show ?thesis by (simp add: Max strict_below_fold1_iff [folded dual_max]) @@ -2649,7 +2649,7 @@ assumes "finite A" and "A \ {}" shows "Min A \ x \ (\a\A. a \ x)" proof - - class_interpret lower_semilattice ["op \" "op <" min] + interpret lower_semilattice "op \" "op <" min by (rule min_lattice) from assms show ?thesis by (simp add: Min_def fold1_below_iff) @@ -2660,7 +2660,7 @@ shows "x \ Max A \ (\a\A. x \ a)" proof - note Max = Max_def - class_interpret linorder ["op \" "op >"] + interpret linorder "op \" "op >" by (rule dual_linorder) from assms show ?thesis by (simp add: Max fold1_below_iff [folded dual_max]) @@ -2670,7 +2670,7 @@ assumes "finite A" and "A \ {}" shows "Min A < x \ (\a\A. a < x)" proof - - class_interpret lower_semilattice ["op \" "op <" min] + interpret lower_semilattice "op \" "op <" min by (rule min_lattice) from assms show ?thesis by (simp add: Min_def fold1_strict_below_iff) @@ -2681,7 +2681,7 @@ shows "x < Max A \ (\a\A. x < a)" proof - note Max = Max_def - class_interpret linorder ["op \" "op >"] + interpret linorder "op \" "op >" by (rule dual_linorder) from assms show ?thesis by (simp add: Max fold1_strict_below_iff [folded dual_max]) @@ -2691,7 +2691,7 @@ assumes "M \ N" and "M \ {}" and "finite N" shows "Min N \ Min M" proof - - class_interpret distrib_lattice ["op \" "op <" min max] + interpret distrib_lattice "op \" "op <" min max by (rule distrib_lattice_min_max) from assms show ?thesis by (simp add: Min_def fold1_antimono) qed @@ -2701,7 +2701,7 @@ shows "Max M \ Max N" proof - note Max = Max_def - class_interpret linorder ["op \" "op >"] + interpret linorder "op \" "op >" by (rule dual_linorder) from assms show ?thesis by (simp add: Max fold1_antimono [folded dual_max]) diff -r b0e01a48867c -r 25472dc71a4b src/HOL/Lattices.thy --- a/src/HOL/Lattices.thy Fri Jan 16 12:11:06 2009 +0100 +++ b/src/HOL/Lattices.thy Fri Jan 16 14:59:06 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 \ \ 'a\linorder \ 'a \ bool" "op <" min max] +interpretation min_max!: distrib_lattice "op \ :: 'a::linorder \ 'a \ bool" "op <" min max by (rule distrib_lattice_min_max) lemma inf_min: "inf = (min \ 'a\{lower_semilattice, linorder} \ 'a \ 'a)" diff -r b0e01a48867c -r 25472dc71a4b src/HOL/Library/Countable.thy --- a/src/HOL/Library/Countable.thy Fri Jan 16 12:11:06 2009 +0100 +++ b/src/HOL/Library/Countable.thy Fri Jan 16 14:59:06 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Library/Countable.thy - ID: $Id$ Author: Alexander Krauss, TU Muenchen *) diff -r b0e01a48867c -r 25472dc71a4b src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Fri Jan 16 12:11:06 2009 +0100 +++ b/src/HOL/Library/Multiset.thy Fri Jan 16 14:59:06 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 \#" "op <#"] +interpretation mset_order!: order "op \#" "op <#" proof qed (auto intro: order.intro mset_le_refl mset_le_antisym mset_le_trans simp: mset_less_def) -class_interpretation mset_order_cancel_semigroup: - pordered_cancel_ab_semigroup_add ["op +" "op \#" "op <#"] +interpretation mset_order_cancel_semigroup!: + pordered_cancel_ab_semigroup_add "op +" "op \#" "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 \#" "op <#"] +interpretation mset_order_semigroup_cancel!: + pordered_ab_semigroup_add_imp_le "op +" "op \#" "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 \# B \ B - {#c#} \# B" by (auto simp: mset_le_def mset_less_def multi_drop_mem_not_eq) diff -r b0e01a48867c -r 25472dc71a4b src/HOL/Library/SetsAndFunctions.thy --- a/src/HOL/Library/SetsAndFunctions.thy Fri Jan 16 12:11:06 2009 +0100 +++ b/src/HOL/Library/SetsAndFunctions.thy Fri Jan 16 14:59:06 2009 +0100 @@ -107,26 +107,26 @@ apply simp done -class_interpretation set_semigroup_add: semigroup_add ["op \ :: ('a::semigroup_add) set => 'a set => 'a set"] +interpretation set_semigroup_add!: semigroup_add "op \ :: ('a::semigroup_add) set => 'a set => 'a set" apply default apply (unfold set_plus_def) apply (force simp add: add_assoc) done -class_interpretation set_semigroup_mult: semigroup_mult ["op \ :: ('a::semigroup_mult) set => 'a set => 'a set"] +interpretation set_semigroup_mult!: semigroup_mult "op \ :: ('a::semigroup_mult) set => 'a set => 'a set" apply default apply (unfold set_times_def) apply (force simp add: mult_assoc) done -class_interpretation set_comm_monoid_add: comm_monoid_add ["{0}" "op \ :: ('a::comm_monoid_add) set => 'a set => 'a set"] +interpretation set_comm_monoid_add!: comm_monoid_add "{0}" "op \ :: ('a::comm_monoid_add) set => 'a set => 'a set" apply default apply (unfold set_plus_def) apply (force simp add: add_ac) apply force done -class_interpretation set_comm_monoid_mult: comm_monoid_mult ["{1}" "op \ :: ('a::comm_monoid_mult) set => 'a set => 'a set"] +interpretation set_comm_monoid_mult!: comm_monoid_mult "{1}" "op \ :: ('a::comm_monoid_mult) set => 'a set => 'a set" apply default apply (unfold set_times_def) apply (force simp add: mult_ac) diff -r b0e01a48867c -r 25472dc71a4b src/HOL/List.thy --- a/src/HOL/List.thy Fri Jan 16 12:11:06 2009 +0100 +++ b/src/HOL/List.thy Fri Jan 16 14:59:06 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 = [] \ ys = [])" diff -r b0e01a48867c -r 25472dc71a4b src/HOL/MetisExamples/BT.thy --- a/src/HOL/MetisExamples/BT.thy Fri Jan 16 12:11:06 2009 +0100 +++ b/src/HOL/MetisExamples/BT.thy Fri Jan 16 14:59:06 2009 +0100 @@ -84,7 +84,7 @@ lemma depth_reflect: "depth (reflect t) = depth t" apply (induct t) apply (metis depth.simps(1) reflect.simps(1)) - apply (metis depth.simps(2) min_max.less_eq_less_sup.sup_commute reflect.simps(2)) + apply (metis depth.simps(2) min_max.sup_commute reflect.simps(2)) done text {* diff -r b0e01a48867c -r 25472dc71a4b src/HOL/MetisExamples/BigO.thy --- a/src/HOL/MetisExamples/BigO.thy Fri Jan 16 12:11:06 2009 +0100 +++ b/src/HOL/MetisExamples/BigO.thy Fri Jan 16 14:59:06 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/MetisExamples/BigO.thy - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Testing the metis method @@ -13,9 +12,7 @@ subsection {* Definitions *} -constdefs - - bigo :: "('a => 'b::ordered_idom) => ('a => 'b) set" ("(1O'(_'))") +definition bigo :: "('a => 'b::ordered_idom) => ('a => 'b) set" ("(1O'(_'))") where "O(f::('a => 'b)) == {h. EX c. ALL x. abs (h x) <= c * abs (f x)}" ML_command{*AtpWrapper.problem_name := "BigO__bigo_pos_const"*} @@ -362,7 +359,7 @@ apply (rule add_mono) ML_command{*AtpWrapper.problem_name := "BigO__bigo_plus_eq_simpler"*} (*Found by SPASS; SLOW*) -apply (metis le_maxI2 linorder_linear linorder_not_le min_max.less_eq_less_sup.sup_absorb1 mult_le_cancel_right order_trans) +apply (metis le_maxI2 linorder_linear linorder_not_le min_max.sup_absorb1 mult_le_cancel_right order_trans) apply (metis le_maxI2 linorder_not_le mult_le_cancel_right order_trans) done @@ -1164,7 +1161,7 @@ (*sledgehammer*); apply (case_tac "0 <= k x - g x") prefer 2 (*re-order subgoals because I don't know what to put after a structured proof*) - apply (metis abs_ge_zero abs_minus_commute linorder_linear min_max.less_eq_less_sup.sup_absorb1 min_max.less_eq_less_sup.sup_commute) + apply (metis abs_ge_zero abs_minus_commute linorder_linear min_max.sup_absorb1 min_max.sup_commute) proof (neg_clausify) fix x assume 0: "\A. k A \ f A" @@ -1174,16 +1171,16 @@ have 3: "\ k x - g x < (0\'b)" by (metis 2 linorder_not_less) have 4: "\X1 X2. min X1 (k X2) \ f X2" - by (metis min_max.less_eq_less_inf.inf_le2 min_max.less_eq_less_inf.le_inf_iff min_max.less_eq_less_inf.le_iff_inf 0) + by (metis min_max.inf_le2 min_max.le_inf_iff min_max.le_iff_inf 0) have 5: "\g x - f x\ = f x - g x" - by (metis abs_minus_commute combine_common_factor mult_zero_right minus_add_cancel minus_zero abs_if diff_less_eq min_max.less_eq_less_inf.inf_commute 4 linorder_not_le min_max.less_eq_less_inf.le_iff_inf 3 diff_less_0_iff_less linorder_not_less) + by (metis abs_minus_commute combine_common_factor mult_zero_right minus_add_cancel minus_zero abs_if diff_less_eq min_max.inf_commute 4 linorder_not_le min_max.le_iff_inf 3 diff_less_0_iff_less linorder_not_less) have 6: "max (0\'b) (k x - g x) = k x - g x" - by (metis min_max.less_eq_less_sup.le_iff_sup 2) + by (metis min_max.le_iff_sup 2) assume 7: "\ max (k x - g x) (0\'b) \ \f x - g x\" have 8: "\ k x - g x \ f x - g x" - by (metis 5 abs_minus_commute 7 min_max.less_eq_less_sup.sup_commute 6) + by (metis 5 abs_minus_commute 7 min_max.sup_commute 6) show "False" - by (metis min_max.less_eq_less_sup.sup_commute min_max.less_eq_less_inf.inf_commute min_max.less_eq_less_inf_sup.sup_inf_absorb min_max.less_eq_less_inf.le_iff_inf 0 max_diff_distrib_left 1 linorder_not_le 8) + by (metis min_max.sup_commute min_max.inf_commute min_max.sup_inf_absorb min_max.le_iff_inf 0 max_diff_distrib_left 1 linorder_not_le 8) qed ML_command{*AtpWrapper.problem_name := "BigO__bigo_lesso3"*} @@ -1206,7 +1203,7 @@ ML_command{*AtpWrapper.problem_name := "BigO__bigo_lesso3_simpler"*} apply (metis diff_less_0_iff_less linorder_not_le not_leE uminus_add_conv_diff xt1(12) xt1(6)) apply (metis add_minus_cancel diff_le_eq le_diff_eq uminus_add_conv_diff) -apply (metis abs_ge_zero linorder_linear min_max.less_eq_less_sup.sup_absorb1 min_max.less_eq_less_sup.sup_commute) +apply (metis abs_ge_zero linorder_linear min_max.sup_absorb1 min_max.sup_commute) done lemma bigo_lesso4: "f 'b::ordered_field) ==> diff -r b0e01a48867c -r 25472dc71a4b src/HOL/Statespace/StateSpaceEx.thy --- a/src/HOL/Statespace/StateSpaceEx.thy Fri Jan 16 12:11:06 2009 +0100 +++ b/src/HOL/Statespace/StateSpaceEx.thy Fri Jan 16 14:59:06 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]" diff -r b0e01a48867c -r 25472dc71a4b src/HOL/Word/WordArith.thy --- a/src/HOL/Word/WordArith.thy Fri Jan 16 12:11:06 2009 +0100 +++ b/src/HOL/Word/WordArith.thy Fri Jan 16 14:59:06 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 = diff -r b0e01a48867c -r 25472dc71a4b src/HOLCF/CompactBasis.thy --- a/src/HOLCF/CompactBasis.thy Fri Jan 16 12:11:06 2009 +0100 +++ b/src/HOLCF/CompactBasis.thy Fri Jan 16 14:59:06 2009 +0100 @@ -244,7 +244,7 @@ assumes "ab_semigroup_idem_mult f" shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)" proof - - class_interpret ab_semigroup_idem_mult [f] by fact + interpret ab_semigroup_idem_mult f by fact show ?thesis unfolding fold_pd_def Rep_PDPlus by (simp add: image_Un fold1_Un2) qed diff -r b0e01a48867c -r 25472dc71a4b src/HOLCF/ConvexPD.thy --- a/src/HOLCF/ConvexPD.thy Fri Jan 16 12:11:06 2009 +0100 +++ b/src/HOLCF/ConvexPD.thy Fri Jan 16 14:59:06 2009 +0100 @@ -296,9 +296,8 @@ apply (simp add: PDPlus_absorb) done -class_interpretation aci_convex_plus: ab_semigroup_idem_mult ["op +\"] - by unfold_locales - (rule convex_plus_assoc convex_plus_commute convex_plus_absorb)+ +interpretation aci_convex_plus!: ab_semigroup_idem_mult "op +\" + proof qed (rule convex_plus_assoc convex_plus_commute convex_plus_absorb)+ lemma convex_plus_left_commute: "xs +\ (ys +\ zs) = ys +\ (xs +\ zs)" by (rule aci_convex_plus.mult_left_commute) diff -r b0e01a48867c -r 25472dc71a4b src/HOLCF/HOLCF.thy --- a/src/HOLCF/HOLCF.thy Fri Jan 16 12:11:06 2009 +0100 +++ b/src/HOLCF/HOLCF.thy Fri Jan 16 14:59:06 2009 +0100 @@ -16,7 +16,6 @@ "Tools/domain/domain_theorems.ML" "Tools/domain/domain_extender.ML" "Tools/adm_tac.ML" - begin defaultsort pcpo diff -r b0e01a48867c -r 25472dc71a4b src/HOLCF/LowerPD.thy --- a/src/HOLCF/LowerPD.thy Fri Jan 16 12:11:06 2009 +0100 +++ b/src/HOLCF/LowerPD.thy Fri Jan 16 14:59:06 2009 +0100 @@ -250,9 +250,8 @@ apply (simp add: PDPlus_absorb) done -class_interpretation aci_lower_plus: ab_semigroup_idem_mult ["op +\"] - by unfold_locales - (rule lower_plus_assoc lower_plus_commute lower_plus_absorb)+ +interpretation aci_lower_plus!: ab_semigroup_idem_mult "op +\" + proof qed (rule lower_plus_assoc lower_plus_commute lower_plus_absorb)+ lemma lower_plus_left_commute: "xs +\ (ys +\ zs) = ys +\ (xs +\ zs)" by (rule aci_lower_plus.mult_left_commute) diff -r b0e01a48867c -r 25472dc71a4b src/HOLCF/UpperPD.thy --- a/src/HOLCF/UpperPD.thy Fri Jan 16 12:11:06 2009 +0100 +++ b/src/HOLCF/UpperPD.thy Fri Jan 16 14:59:06 2009 +0100 @@ -248,9 +248,8 @@ apply (simp add: PDPlus_absorb) done -class_interpretation aci_upper_plus: ab_semigroup_idem_mult ["op +\"] - by unfold_locales - (rule upper_plus_assoc upper_plus_commute upper_plus_absorb)+ +interpretation aci_upper_plus!: ab_semigroup_idem_mult "op +\" + proof qed (rule upper_plus_assoc upper_plus_commute upper_plus_absorb)+ lemma upper_plus_left_commute: "xs +\ (ys +\ zs) = ys +\ (xs +\ zs)" by (rule aci_upper_plus.mult_left_commute) diff -r b0e01a48867c -r 25472dc71a4b src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Fri Jan 16 12:11:06 2009 +0100 +++ b/src/Pure/Isar/class.ML Fri Jan 16 14:59:06 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 = diff -r b0e01a48867c -r 25472dc71a4b src/Pure/Isar/class_target.ML --- a/src/Pure/Isar/class_target.ML Fri Jan 16 12:11:06 2009 +0100 +++ b/src/Pure/Isar/class_target.ML Fri Jan 16 14:59:06 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') diff -r b0e01a48867c -r 25472dc71a4b src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Fri Jan 16 12:11:06 2009 +0100 +++ b/src/Pure/Isar/expression.ML Fri Jan 16 14:59:06 2009 +0100 @@ -150,14 +150,14 @@ local -fun prep_inst parse_term parms (Positional insts) ctxt = +fun prep_inst parse_term ctxt parms (Positional insts) = (insts ~~ parms) |> map (fn - (NONE, p) => Syntax.parse_term ctxt p | + (NONE, p) => Free (p, the (Variable.default_type ctxt p)) | (SOME t, _) => parse_term ctxt t) - | prep_inst parse_term parms (Named insts) ctxt = + | prep_inst parse_term ctxt parms (Named insts) = parms |> map (fn p => case AList.lookup (op =) insts p of SOME t => parse_term ctxt t | - NONE => Syntax.parse_term ctxt p); + NONE => Free (p, the (Variable.default_type ctxt p))); in @@ -325,7 +325,7 @@ let val thy = ProofContext.theory_of ctxt; val (parm_names, parm_types) = Locale.params_of thy loc |> - map (fn (b, SOME T, _) => (Binding.base_name b, T)) |> split_list; + map_split (fn (b, SOME T, _) => (Binding.base_name b, T)); val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt; in (loc, morph) end; @@ -357,8 +357,9 @@ fun prep_inst (loc, (prfx, inst)) (i, insts, ctxt) = let val (parm_names, parm_types) = Locale.params_of thy loc |> - map (fn (b, SOME T, _) => (Binding.base_name b, T)) |> split_list; - val inst' = parse_inst parm_names inst ctxt; + map_split (fn (b, SOME T, _) => (Binding.base_name b, T)) + (*FIXME return value of Locale.params_of has strange type*) + val inst' = parse_inst ctxt parm_names inst; val parm_types' = map (TypeInfer.paramify_vars o Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT) parm_types; val inst'' = map2 TypeInfer.constrain parm_types' inst';