# HG changeset patch
# User haftmann
# Date 1248587668 -7200
# Node ID d64a1820431d6e995032639e803505e4da9f6ea1
# Parent  bda40fb76a65ef21b35f20fe7779ee1db2f005d2# Parent  b2e93cda0be8de816a3074ecc8ca307a36d96023
merged

diff -r bda40fb76a65 -r d64a1820431d src/HOL/Finite_Set.thy
--- 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]:
diff -r bda40fb76a65 -r d64a1820431d src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Sat Jul 25 18:55:30 2009 +0200
+++ b/src/HOL/Lattices.thy	Sun Jul 26 07:54:28 2009 +0200
@@ -413,20 +413,14 @@
 subsection {* @{const min}/@{const max} on linear orders as
   special case of @{const inf}/@{const sup} *}
 
-lemma (in linorder) distrib_lattice_min_max:
-  "distrib_lattice (op \<le>) (op <) min max"
+sublocale linorder < min_max!: distrib_lattice less_eq less "Orderings.ord.min less_eq" "Orderings.ord.max less_eq"
 proof
-  have aux: "\<And>x y \<Colon> 'a. x < y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
-    by (auto simp add: less_le antisym)
   fix x y z
-  show "max x (min y z) = min (max x y) (max x z)"
-  unfolding min_def max_def
-  by auto
+  show "Orderings.ord.max less_eq x (Orderings.ord.min less_eq y z) =
+    Orderings.ord.min less_eq (Orderings.ord.max less_eq x y) (Orderings.ord.max less_eq x z)"
+  unfolding min_def max_def by auto
 qed (auto simp add: min_def max_def not_le less_imp_le)
 
-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)"
   by (rule ext)+ (auto intro: antisym)
 
diff -r bda40fb76a65 -r d64a1820431d src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Sat Jul 25 18:55:30 2009 +0200
+++ b/src/HOL/Wellfounded.thy	Sun Jul 26 07:54:28 2009 +0200
@@ -187,8 +187,12 @@
 lemma wf_empty [iff]: "wf({})"
   by (simp add: wf_def)
 
-lemmas wfP_empty [iff] =
-  wf_empty [to_pred bot_empty_eq2, simplified bot_fun_eq bot_bool_eq]
+lemma wfP_empty [iff]:
+  "wfP (\<lambda>x y. False)"
+proof -
+  have "wfP bot" by (fact wf_empty [to_pred bot_empty_eq2])
+  then show ?thesis by (simp add: bot_fun_eq bot_bool_eq)
+qed
 
 lemma wf_Int1: "wf r ==> wf (r Int r')"
   apply (erule wf_subset)
diff -r bda40fb76a65 -r d64a1820431d src/Pure/Isar/class.ML
--- 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)