--- a/src/HOL/Finite_Set.thy Sat Jul 25 18:55:30 2009 +0200
+++ b/src/HOL/Finite_Set.thy Sun Jul 26 07:54:28 2009 +0200
@@ -2960,13 +2960,9 @@
"ab_semigroup_idem_mult max"
proof qed (auto simp add: max_def)
-lemma min_lattice:
- "lower_semilattice (op \<le>) (op <) min"
- proof qed (auto simp add: min_def)
-
lemma max_lattice:
"lower_semilattice (op \<ge>) (op >) max"
- proof qed (auto simp add: max_def)
+ by (fact min_max.dual_semilattice)
lemma dual_max:
"ord.max (op \<ge>) = min"
@@ -3126,11 +3122,7 @@
lemma Min_le [simp]:
assumes "finite A" and "x \<in> A"
shows "Min A \<le> x"
-proof -
- interpret lower_semilattice "op \<le>" "op <" min
- by (rule min_lattice)
- from assms show ?thesis by (simp add: Min_def fold1_belowI)
-qed
+ using assms by (simp add: Min_def min_max.fold1_belowI)
lemma Max_ge [simp]:
assumes "finite A" and "x \<in> A"
@@ -3144,11 +3136,7 @@
lemma Min_ge_iff [simp, noatp]:
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
- by (rule min_lattice)
- from assms show ?thesis by (simp add: Min_def below_fold1_iff)
-qed
+ using assms by (simp add: Min_def min_max.below_fold1_iff)
lemma Max_le_iff [simp, noatp]:
assumes "finite A" and "A \<noteq> {}"
@@ -3162,63 +3150,46 @@
lemma Min_gr_iff [simp, noatp]:
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
- by (rule min_lattice)
- from assms show ?thesis by (simp add: Min_def strict_below_fold1_iff)
-qed
+ using assms by (simp add: Min_def strict_below_fold1_iff)
lemma Max_less_iff [simp, noatp]:
assumes "finite A" and "A \<noteq> {}"
shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
proof -
- note Max = Max_def
- interpret linorder "op \<ge>" "op >"
+ interpret dual: linorder "op \<ge>" "op >"
by (rule dual_linorder)
from assms show ?thesis
- by (simp add: Max strict_below_fold1_iff [folded dual_max])
+ by (simp add: Max_def dual.strict_below_fold1_iff [folded dual.dual_max])
qed
lemma Min_le_iff [noatp]:
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
- by (rule min_lattice)
- from assms show ?thesis
- by (simp add: Min_def fold1_below_iff)
-qed
+ using assms by (simp add: Min_def fold1_below_iff)
lemma Max_ge_iff [noatp]:
assumes "finite A" and "A \<noteq> {}"
shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
proof -
- note Max = Max_def
- interpret linorder "op \<ge>" "op >"
+ interpret dual: linorder "op \<ge>" "op >"
by (rule dual_linorder)
from assms show ?thesis
- by (simp add: Max fold1_below_iff [folded dual_max])
+ by (simp add: Max_def dual.fold1_below_iff [folded dual.dual_max])
qed
lemma Min_less_iff [noatp]:
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
- by (rule min_lattice)
- from assms show ?thesis
- by (simp add: Min_def fold1_strict_below_iff)
-qed
+ using assms by (simp add: Min_def fold1_strict_below_iff)
lemma Max_gr_iff [noatp]:
assumes "finite A" and "A \<noteq> {}"
shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
proof -
- note Max = Max_def
- interpret linorder "op \<ge>" "op >"
+ interpret dual: linorder "op \<ge>" "op >"
by (rule dual_linorder)
from assms show ?thesis
- by (simp add: Max fold1_strict_below_iff [folded dual_max])
+ by (simp add: Max_def dual.fold1_strict_below_iff [folded dual.dual_max])
qed
lemma Min_eqI:
@@ -3248,21 +3219,16 @@
lemma Min_antimono:
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
- by (rule distrib_lattice_min_max)
- from assms show ?thesis by (simp add: Min_def fold1_antimono)
-qed
+ using assms by (simp add: Min_def fold1_antimono)
lemma Max_mono:
assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
shows "Max M \<le> Max N"
proof -
- note Max = Max_def
- interpret linorder "op \<ge>" "op >"
+ interpret dual: linorder "op \<ge>" "op >"
by (rule dual_linorder)
from assms show ?thesis
- by (simp add: Max fold1_antimono [folded dual_max])
+ by (simp add: Max_def dual.fold1_antimono [folded dual.dual_max])
qed
lemma finite_linorder_max_induct[consumes 1, case_names empty insert]:
--- a/src/Pure/Isar/class.ML Sat Jul 25 18:55:30 2009 +0200
+++ b/src/Pure/Isar/class.ML Sun Jul 26 07:54:28 2009 +0200
@@ -101,7 +101,7 @@
(* reading and processing class specifications *)
-fun prep_class_elems prep_decl thy supexpr sups proto_base_sort raw_elems =
+fun prep_class_elems prep_decl thy sups proto_base_sort raw_elems =
let
(* user space type system: only permits 'a type variable, improves towards 'a *)
@@ -129,16 +129,19 @@
^ Syntax.string_of_sort_global thy a_sort ^ ".")
| _ => error "Multiple type variables in class specification.";
in (map o map_atyps) (K (TFree (Name.aT, fixate_sort))) Ts end;
- fun add_typ_check level name f = Context.proof_map (Syntax.add_typ_check level name (fn xs => fn ctxt =>
- let val xs' = f xs in if eq_list (op =) (xs, xs') then NONE else SOME (xs', ctxt) end));
+ fun add_typ_check level name f = Context.proof_map
+ (Syntax.add_typ_check level name (fn xs => fn ctxt =>
+ let val xs' = f xs in if eq_list (op =) (xs, xs') then NONE else SOME (xs', ctxt) end));
- (* preprocessing elements, retrieving base sort from type-checked elements *)
+ (* preprocessing elements, retrieving base sort from typechecked elements *)
val init_class_body = fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints
#> redeclare_operations thy sups
#> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc
#> add_typ_check ~10 "singleton_fixate" (singleton_fixate thy (Sign.classes_of thy));
- val ((_, _, inferred_elems), _) = ProofContext.init thy
- |> prep_decl supexpr init_class_body raw_elems;
+ val raw_supexpr = (map (fn sup => (sup, (("", false),
+ Expression.Positional []))) sups, []);
+ val ((raw_supparams, _, inferred_elems), _) = ProofContext.init thy
+ |> prep_decl raw_supexpr init_class_body raw_elems;
fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs
| fold_element_types f (Element.Constrains cnstrs) = fold (f o snd) cnstrs
| fold_element_types f (Element.Assumes assms) = fold (fold (fn (t, ts) =>
@@ -151,9 +154,16 @@
case (fold o fold_element_types) Term.add_tfreesT inferred_elems []
of [] => error "No type variable in class specification"
| [(_, sort)] => sort
- | _ => error "Multiple type variables in class specification"
+ | _ => error "Multiple type variables in class specification";
+ val supparams = map (fn ((c, T), _) =>
+ (c, map_atyps (K (TFree (Name.aT, base_sort))) T)) raw_supparams;
+ val supparam_names = map fst supparams;
+ fun mk_param ((c, _), _) = Free (c, (the o AList.lookup (op =) supparams) c);
+ val supexpr = (map (fn sup => (sup, (("", false),
+ Expression.Positional (map (SOME o mk_param) (Locale.params_of thy sup))))) sups,
+ map (fn (c, T) => (Binding.name c, SOME T, NoSyn)) supparams);
- in (base_sort, inferred_elems) end;
+ in (base_sort, supparam_names, supexpr, inferred_elems) end;
val cert_class_elems = prep_class_elems Expression.cert_declaration;
val read_class_elems = prep_class_elems Expression.cert_read_declaration;
@@ -168,23 +178,21 @@
val _ = case filter_out (is_class thy) sups
of [] => ()
| no_classes => error ("No (proper) classes: " ^ commas (map quote no_classes));
- 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
+ val raw_supparams = (map o apsnd) (snd o snd) (these_params thy sups);
+ val raw_supparam_names = map fst raw_supparams;
+ val _ = if has_duplicates (op =) raw_supparam_names
then error ("Duplicate parameter(s) in superclasses: "
- ^ (commas o map quote o duplicates (op =)) supparam_names)
+ ^ (commas o map quote o duplicates (op =)) raw_supparam_names)
else ();
- val supexpr = (map (fn sup => (sup, (("", false), Expression.Positional [])))
- sups, []);
val given_basesort = fold inter_sort (map (base_sort thy) sups) [];
(* infer types and base sort *)
- val (base_sort, inferred_elems) = prep_class_elems thy supexpr sups
- given_basesort raw_elems;
- val sup_sort = inter_sort base_sort sups
+ val (base_sort, supparam_names, supexpr, inferred_elems) =
+ prep_class_elems thy sups given_basesort raw_elems;
+ val sup_sort = inter_sort base_sort sups;
(* process elements as class specification *)
- val class_ctxt = begin sups base_sort (ProofContext.init thy)
+ val class_ctxt = begin sups base_sort (ProofContext.init thy);
val ((_, _, syntax_elems), _) = class_ctxt
|> Expression.cert_declaration supexpr I inferred_elems;
fun check_vars e vs = if null vs
@@ -204,11 +212,11 @@
| fork_syn x = pair x;
val (elems, global_syntax) = fold_map fork_syn syntax_elems [];
val constrain = Element.Constrains ((map o apsnd o map_atyps)
- (K (TFree (Name.aT, base_sort))) supparams);
+ (K (TFree (Name.aT, base_sort))) raw_supparams);
(*FIXME perhaps better: control type variable by explicit
parameter instantiation of import expression*)
- in (((sups, supparam_names), (sup_sort, base_sort, supexpr)), (constrain :: elems, global_syntax)) end;
+ in (((sups, supparam_names), (sup_sort, base_sort, supexpr)), ((*constrain :: *)elems, global_syntax)) end;
val cert_class_spec = prep_class_spec (K I) cert_class_elems;
val read_class_spec = prep_class_spec Sign.intern_class read_class_elems;
@@ -216,14 +224,14 @@
(* class establishment *)
-fun add_consts class base_sort sups supparams global_syntax thy =
+fun add_consts class base_sort sups supparam_names global_syntax thy =
let
(*FIXME simplify*)
- val supconsts = supparams
+ val supconsts = supparam_names
|> 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 = Locale.params_of thy class;
- val raw_params = (snd o chop (length supparams)) all_params;
+ val raw_params = (snd o chop (length supparam_names)) all_params;
fun add_const ((raw_c, raw_ty), _) thy =
let
val b = Binding.name raw_c;
@@ -246,7 +254,7 @@
|-> (fn params => pair (supconsts @ (map o apfst) fst params, params))
end;
-fun adjungate_axclass bname class base_sort sups supsort supparams global_syntax thy =
+fun adjungate_axclass bname class base_sort sups supsort supparam_names global_syntax thy =
let
(*FIXME simplify*)
fun globalize param_map = map_aterms
@@ -260,7 +268,7 @@
| [thm] => SOME thm;
in
thy
- |> add_consts class base_sort sups supparams global_syntax
+ |> add_consts class base_sort sups supparam_names global_syntax
|-> (fn (param_map, params) => AxClass.define_class (bname, supsort)
(map (fst o snd) params)
[(Thm.empty_binding, Option.map (globalize param_map) raw_pred |> the_list)]
@@ -270,16 +278,16 @@
#> pair (param_map, params, assm_axiom)))
end;
-fun gen_class prep_spec bname raw_supclasses raw_elems thy =
+fun gen_class prep_class_spec bname raw_supclasses raw_elems thy =
let
val class = Sign.full_name thy bname;
- val (((sups, supparams), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
- prep_spec thy raw_supclasses raw_elems;
+ val (((sups, supparam_names), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
+ prep_class_spec thy raw_supclasses raw_elems;
in
thy
|> Expression.add_locale bname Binding.empty supexpr elems
|> snd |> LocalTheory.exit_global
- |> adjungate_axclass bname class base_sort sups supsort supparams global_syntax
+ |> adjungate_axclass bname class base_sort sups supsort supparam_names global_syntax
||> Theory.checkpoint
|-> (fn (param_map, params, assm_axiom) =>
`(fn thy => calculate thy class sups base_sort param_map assm_axiom)