--- a/src/HOL/Finite_Set.thy Thu May 24 08:37:37 2007 +0200
+++ b/src/HOL/Finite_Set.thy Thu May 24 08:37:39 2007 +0200
@@ -2602,7 +2602,7 @@
fix A :: "'a set"
show "Linorder.Min (op \<le>) A = Min A"
by (simp add: Min_def Linorder.Min_def [OF Linorder.intro, OF linorder_axioms]
- linorder_class_min)
+ ord_class.min)
qed
lemma Linorder_Max:
@@ -2611,16 +2611,16 @@
fix A :: "'a set"
show "Linorder.Max (op \<le>) A = Max A"
by (simp add: Max_def Linorder.Max_def [OF Linorder.intro, OF linorder_axioms]
- linorder_class_max)
+ ord_class.max)
qed
-interpretation [unfolded linorder_class_min linorder_class_max Linorder_Min Linorder_Max]:
+interpretation [folded ord_class.min ord_class.max, unfolded Linorder_Min Linorder_Max]:
Linorder_ab_semigroup_add ["op \<le> \<Colon> 'a\<Colon>{linorder, pordered_ab_semigroup_add} \<Rightarrow> 'a \<Rightarrow> bool" "op <" "op +"]
by (rule Linorder_ab_semigroup_add.intro,
rule Linorder.intro, rule linorder_axioms, rule pordered_ab_semigroup_add_axioms)
hide const Min Max
-interpretation [unfolded linorder_class_min linorder_class_max Linorder_Min Linorder_Max]:
+interpretation [folded ord_class.min ord_class.max, unfolded Linorder_Min Linorder_Max]:
Linorder ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <"]
by (rule Linorder.intro, rule linorder_axioms)
declare Min_singleton [simp]
--- a/src/HOL/Lattices.thy Thu May 24 08:37:37 2007 +0200
+++ b/src/HOL/Lattices.thy Thu May 24 08:37:39 2007 +0200
@@ -295,7 +295,7 @@
interpretation min_max:
distrib_lattice ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max]
- by (rule distrib_lattice_min_max [unfolded linorder_class_min linorder_class_max])
+ by (rule distrib_lattice_min_max [folded ord_class.min ord_class.max])
lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{lower_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
by (rule ext)+ auto
--- a/src/HOL/Orderings.thy Thu May 24 08:37:37 2007 +0200
+++ b/src/HOL/Orderings.thy Thu May 24 08:37:39 2007 +0200
@@ -81,26 +81,8 @@
notation (input)
greater_eq (infix "\<ge>" 50)
-hide const min max
-
-definition
- min :: "'a\<Colon>ord \<Rightarrow> 'a \<Rightarrow> 'a" where
- "min a b = (if a \<le> b then a else b)"
-
-definition
- max :: "'a\<Colon>ord \<Rightarrow> 'a \<Rightarrow> 'a" where
- "max a b = (if a \<le> b then b else a)"
-
-declare min_def[code unfold, code inline del]
- max_def[code unfold, code inline del]
-
-lemma linorder_class_min:
- "ord.min (op \<le> \<Colon> 'a\<Colon>ord \<Rightarrow> 'a \<Rightarrow> bool) = min"
- by rule+ (simp add: min_def ord_class.min_def)
-
-lemma linorder_class_max:
- "ord.max (op \<le> \<Colon> 'a\<Colon>ord \<Rightarrow> 'a \<Rightarrow> bool) = max"
- by rule+ (simp add: max_def ord_class.max_def)
+lemmas min_def [code func, code unfold, code inline del] = min_def [folded ord_class.min]
+lemmas max_def [code func, code unfold, code inline del] = max_def [folded ord_class.max]
subsection {* Partial orders *}
@@ -351,14 +333,14 @@
lemmas leD = linorder_class.leD
lemmas not_leE = linorder_class.not_leE
-lemmas min_le_iff_disj = linorder_class.min_le_iff_disj [unfolded linorder_class_min]
-lemmas le_max_iff_disj = linorder_class.le_max_iff_disj [unfolded linorder_class_max]
-lemmas min_less_iff_disj = linorder_class.min_less_iff_disj [unfolded linorder_class_min]
-lemmas less_max_iff_disj = linorder_class.less_max_iff_disj [unfolded linorder_class_max]
-lemmas min_less_iff_conj [simp] = linorder_class.min_less_iff_conj [unfolded linorder_class_min]
-lemmas max_less_iff_conj [simp] = linorder_class.max_less_iff_conj [unfolded linorder_class_max]
-lemmas split_min = linorder_class.split_min [unfolded linorder_class_min]
-lemmas split_max = linorder_class.split_max [unfolded linorder_class_max]
+lemmas min_le_iff_disj = linorder_class.min_le_iff_disj [folded ord_class.min]
+lemmas le_max_iff_disj = linorder_class.le_max_iff_disj [folded ord_class.max]
+lemmas min_less_iff_disj = linorder_class.min_less_iff_disj [folded ord_class.min]
+lemmas less_max_iff_disj = linorder_class.less_max_iff_disj [folded ord_class.max]
+lemmas min_less_iff_conj [simp] = linorder_class.min_less_iff_conj [folded ord_class.min]
+lemmas max_less_iff_conj [simp] = linorder_class.max_less_iff_conj [folded ord_class.max]
+lemmas split_min = linorder_class.split_min [folded ord_class.min]
+lemmas split_max = linorder_class.split_max [folded ord_class.max]
subsection {* Reasoning tools setup *}
--- a/src/Pure/Isar/theory_target.ML Thu May 24 08:37:37 2007 +0200
+++ b/src/Pure/Isar/theory_target.ML Thu May 24 08:37:39 2007 +0200
@@ -55,8 +55,8 @@
fun internal_abbrev prmode ((c, mx), t) =
(* FIXME really permissive *)
- LocalTheory.term_syntax (perhaps o try o ProofContext.target_abbrev prmode ((c, mx), t)) #>
- ProofContext.add_abbrev Syntax.internalM (c, t) #> snd;
+ LocalTheory.term_syntax (perhaps o try o ProofContext.target_abbrev prmode ((c, mx), t))
+ #> ProofContext.add_abbrev Syntax.internalM (c, t) #> snd;
fun consts is_loc some_class depends decls lthy =
let
@@ -70,12 +70,19 @@
val thy' = Sign.add_consts_authentic [(c, U, mx1)] thy;
in (((c, mx2), t), thy') end;
- val (abbrs, lthy') = lthy |> LocalTheory.theory_result (fold_map const decls);
+ fun const_class (SOME class) ((c, _), mx) (_, t) =
+ ClassPackage.add_const_in_class class ((c, t), mx)
+ | const_class NONE _ _ = I;
+
+ val (abbrs, lthy') = lthy
+ |> LocalTheory.theory_result (fold_map const decls)
val defs = map (apsnd (pair ("", []))) abbrs;
in
lthy'
|> is_loc ? fold (internal_abbrev Syntax.default_mode) abbrs
- |> LocalDefs.add_defs defs |>> map (apsnd snd)
+ |> LocalTheory.raw_theory (fold2 (const_class some_class) decls abbrs)
+ |> LocalDefs.add_defs defs
+ |>> map (apsnd snd)
end;
@@ -85,7 +92,7 @@
#1 (ProofContext.inferred_fixes ctxt)
|> filter (member (op =) (fold (Variable.add_fixed ctxt) ts []));
-fun abbrev is_loc some_class prmode ((raw_c, mx), raw_t) lthy =
+fun abbrev is_loc some_class prmode ((raw_c, mx), raw_t) lthy =
let
val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
val target = LocalTheory.target_of lthy;
@@ -127,15 +134,16 @@
in
-fun defs loc some_class kind args lthy0 =
+fun defs loc kind args lthy0 =
let
fun def ((c, mx), ((name, atts), rhs)) lthy1 =
let
val (rhs', rhs_conv) = expand_term lthy0 rhs;
val xs = Variable.add_fixed (LocalTheory.target_of lthy0) rhs' [];
+ val T = Term.fastype_of rhs;
val ([(lhs, lhs_def)], lthy2) = lthy1
- |> LocalTheory.consts (member (op =) xs) [((c, Term.fastype_of rhs), mx)];
+ |> LocalTheory.consts (member (op =) xs) [((c, T), mx)];
val lhs' = #2 (Logic.dest_equals (Thm.prop_of lhs_def));
val name' = Thm.def_name_optional c name;
@@ -145,14 +153,7 @@
[(*c == loc.c xs*) lhs_def,
(*lhs' == rhs'*) def,
(*rhs' == rhs*) Thm.symmetric rhs_conv];
- val lthy4 = case some_class
- of SOME class =>
- lthy3
- |> LocalTheory.raw_theory
- (ClassPackage.add_def_in_class lthy3 class
- ((c, mx), ((name, atts), (rhs, eq))))
- | _ => lthy3;
- in ((lhs, ((name', atts), [([eq], [])])), lthy4) end;
+ in ((lhs, ((name', atts), [([eq], [])])), lthy3) end;
val ((lhss, facts), lthy') = lthy0 |> fold_map def args |>> split_list;
val (res, lthy'') = lthy' |> LocalTheory.notes kind facts;
@@ -320,7 +321,7 @@
consts = consts is_loc some_class,
axioms = axioms,
abbrev = abbrev is_loc some_class,
- defs = defs loc some_class,
+ defs = defs loc,
notes = notes loc,
type_syntax = type_syntax loc,
term_syntax = term_syntax loc,
--- a/src/Pure/Tools/class_package.ML Thu May 24 08:37:37 2007 +0200
+++ b/src/Pure/Tools/class_package.ML Thu May 24 08:37:39 2007 +0200
@@ -29,11 +29,9 @@
val instance_sort_cmd: string * string -> theory -> Proof.state
val prove_instance_sort: tactic -> class * sort -> theory -> theory
- (* experimental class target *)
val class_of_locale: theory -> string -> class option
- val add_def_in_class: local_theory -> string
- -> (string * Syntax.mixfix) * ((string * Attrib.src list) * (term * thm)) -> theory -> theory
- val CLASS_TARGET: bool ref
+ val add_const_in_class: string -> (string * term) * Syntax.mixfix
+ -> theory -> theory
val print_classes: theory -> unit
val intro_classes_tac: thm list -> tactic
@@ -88,7 +86,7 @@
gen_instance (single oo (Logic.mk_classrel oo AxClass.cert_classrel))
AxClass.add_classrel I o single;
-end; (* local *)
+end; (*local*)
(* introducing axclasses with implicit parameter handling *)
@@ -222,7 +220,7 @@
val instance_arity = instance_arity' axclass_instance_arity;
val prove_instance_arity = instance_arity' o tactic_proof;
-end; (* local *)
+end; (*local*)
@@ -234,10 +232,8 @@
locale: string,
consts: (string * string) list
(*locale parameter ~> toplevel theory constant*),
+ v: string option,
intro: thm,
- witness: Element.witness list,
- primdefs: thm list,
- (*for experimental class target*)
propnames: string list
(*for ad-hoc instance_in*)
};
@@ -282,7 +278,7 @@
fun these_intros thy =
Graph.fold (fn (_, (data, _)) => insert Thm.eq_thm ((#intro o rep_classdata) data))
((fst o ClassData.get) thy) [];
-val the_witness = #witness oo the_class_data;
+
val the_propnames = #propnames oo the_class_data;
fun print_classes thy =
@@ -320,44 +316,21 @@
(* updaters *)
-fun add_class_data ((class, superclasses), (locale, consts, intro, witness, propnames)) =
+fun add_class_data ((class, superclasses), (locale, consts, v, intro, propnames)) =
ClassData.map (fn (gr, tab) => (
gr
|> Graph.new_node (class, ClassData {
locale = locale,
consts = consts,
+ v = v,
intro = intro,
- witness = witness,
- propnames = propnames,
- primdefs = []})
+ propnames = propnames}
+ )
|> fold (curry Graph.add_edge class) superclasses,
tab
|> Symtab.update (locale, class)
));
-fun add_primdef (class, thm) thy =
- (ClassData.map o apfst o Graph.map_node class)
- (fn ClassData { locale, consts, intro, witness, propnames, primdefs } =>
- ClassData { locale = locale, consts = consts, intro = intro,
- witness = witness, propnames = propnames, primdefs = thm :: primdefs });
-
-
-(* exporting terms and theorems to global toplevel *)
-
-fun globalize thy classes =
- let
- val consts = param_map thy classes;
- val constrain_sort = curry (Sorts.inter_sort (Sign.classes_of thy)) classes;
- val subst_typ = Term.map_type_tfree (fn var as (v, sort) =>
- if v = AxClass.param_tyvarname then TFree (v, constrain_sort sort) else TFree var)
- fun subst_aterm (t as Free (v, ty)) = (case AList.lookup (op =) consts v
- of SOME (c, _) => Const (c, ty)
- | NONE => t)
- | subst_aterm t = t;
- in (subst_typ, map_types subst_typ #> Term.map_aterms subst_aterm) end;
-
-val global_term = snd oo globalize
-
(* tactics and methods *)
@@ -524,12 +497,15 @@
fun extract_params thy name_locale =
let
val params = Locale.parameters_of thy name_locale;
+ val v = case (maps typ_tfrees o map (snd o fst)) params
+ of (v, _) :: _ => SOME v
+ | _ => NONE;
in
- (map (fst o fst) params, params
+ (v, (map (fst o fst) params, params
|> (map o apfst o apsnd o Term.map_type_tfree) mk_tyvar
|> (map o apsnd) (fork_mixfix true NONE #> fst)
|> chop (length supconsts)
- |> snd)
+ |> snd))
end;
fun extract_assumes name_locale params thy cs =
let
@@ -554,7 +530,6 @@
Symtab.empty
|> fold2 (fn v => fn (c, ty) => Symtab.update (v, Const
(c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty))) param_names cs;
- fun make_witness t thm = Element.make_witness t (Goal.protect thm);
fun note_intro name_axclass class_intro =
PureThy.note_thmss_qualified "" ((Logic.const_of_class o NameSpace.base) name_axclass)
[(("intro", []), [([class_intro], [])])]
@@ -564,15 +539,15 @@
|> add_locale (SOME "") bname supexpr ((*elems_constrains @*) elems)
|-> (fn name_locale => ProofContext.theory_result (
`(fn thy => extract_params thy name_locale)
- #-> (fn (param_names, params) =>
+ #-> (fn (v, (param_names, params)) =>
axclass_params (bname, supsort) params (extract_assumes name_locale params) other_consts
#-> (fn (name_axclass, ((_, (ax_terms, ax_axioms)), consts)) =>
`(fn thy => class_intro thy name_locale name_axclass sups)
##>> `(fn thy => extract_axiom_names thy name_locale)
#-> (fn (class_intro, axiom_names) =>
add_class_data ((name_axclass, sups),
- (name_locale, map (fst o fst) params ~~ map fst consts,
- class_intro, map2 make_witness ax_terms ax_axioms, axiom_names))
+ (name_locale, map (fst o fst) params ~~ map fst consts, v,
+ class_intro, axiom_names))
#> note_intro name_axclass class_intro
#> prove_interpretation ((ALLGOALS o ProofContext.fact_tac) ax_axioms)
((false, Logic.const_of_class bname), []) (Locale.Locale name_locale)
@@ -615,69 +590,48 @@
val instance_class_cmd = gen_instance_class Sign.read_class;
val instance_class = gen_instance_class Sign.certify_class;
-end; (* local *)
+end; (*local*)
-(** experimental class target **)
+(** class target **)
-fun print_witness wit =
+fun export_fixes thy class =
let
- val (t, thm) = Element.dest_witness wit;
- val prop = Thm.prop_of thm;
- fun string_of_tfree (v, sort) = v ^ "::" ^ Display.raw_string_of_sort sort;
- fun string_of_tvar (v, sort) = Library.string_of_indexname v ^ "::" ^ Display.raw_string_of_sort sort;
- fun print_term t =
- let
- val term = Display.raw_string_of_term t;
- val tfrees = map string_of_tfree (Term.add_tfrees t []);
- val tvars = map string_of_tvar (Term.add_tvars t []);
- in term :: tfrees @ tvars end;
- in (map warning (print_term t); map warning (print_term prop)) end;
+ val v = (#v o the_class_data thy) class;
+ val constrain_sort = curry (Sorts.inter_sort (Sign.classes_of thy)) [class];
+ val subst_typ = Term.map_type_tfree (fn var as (w, sort) =>
+ if SOME w = v then TFree (w, constrain_sort sort) else TFree var);
+ val consts = param_map thy [class];
+ fun subst_aterm (t as Free (v, ty)) = (case AList.lookup (op =) consts v
+ of SOME (c, _) => Const (c, ty)
+ | NONE => t)
+ | subst_aterm t = t;
+ in map_types subst_typ #> Term.map_aterms subst_aterm end;
-val CLASS_TARGET = ref true;
-
-fun add_def_in_class lthy class ((c, syn), ((name, atts), (rhs, eq))) thy =
+fun add_const_in_class class ((c, rhs), syn) thy =
let
val prfx = (Logic.const_of_class o NameSpace.base) class;
- val rhs' = global_term thy [class] rhs;
- val (syn', _) = fork_mixfix true NONE syn;
- val ty = Term.fastype_of rhs';
- fun mk_name thy c =
+ fun mk_name inject c =
let
val n1 = Sign.full_name thy c;
val n2 = NameSpace.qualifier n1;
val n3 = NameSpace.base n1;
- in NameSpace.implode [n2, prfx, n3] end;
- fun add_const (c, ty, syn) =
- Sign.add_consts_authentic [(c, ty, syn)]
- #> pair (mk_name thy c, ty);
- fun add_def ((name, atts), prop) thy =
- thy
- |> PureThy.add_defs_i false [((name, prop), map (Attrib.attribute thy) atts)]
- |>> the_single;
- (*val _ = warning "------ DEF ------";
- val _ = warning c;
- val _ = warning name;
- val _ = (warning o Sign.string_of_term thy) rhs';
- val eq' = Morphism.thm (LocalTheory.target_morphism lthy) eq;
- val _ = (warning o string_of_thm) eq;
- val _ = (warning o string_of_thm) eq';
- val witness = the_witness thy class;
- val _ = warning "------ WIT ------";
- fun print_wit (t, thm) = "(" ^ Sign.string_of_term thy t ^ ", " ^ Display.string_of_thm thm ^ ")"
- fun print_raw_wit (t, thm) = "(" ^ Display.raw_string_of_term t ^ ", " ^ (Display.raw_string_of_term o Thm.prop_of) thm ^ ")"
- val _ = (warning o cat_lines o map (print_wit o Element.dest_witness)) witness;
- val _ = map print_witness witness;
- val _ = (warning o string_of_thm) eq';
- val eq'' = Element.satisfy_thm witness eq';
- val _ = (warning o string_of_thm) eq'';*)
+ in NameSpace.implode (n2 :: inject @ [n3]) end;
+ val abbr' = mk_name [prfx, prfx] c;
+ val rhs' = export_fixes thy class rhs;
+ val ty' = Term.fastype_of rhs';
+ val def = (c, Logic.mk_equals (Const (mk_name [prfx] c, ty'), rhs'));
+ val (syn', _) = fork_mixfix true NONE syn;
in
thy
- (* |> Sign.add_path prfx
- |> add_const (c, ty, syn')
- |-> (fn c => add_def ((name, atts), Logic.mk_equals (Const c, rhs')))
- |-> (fn global_def_thm => tap (fn _ => (warning o string_of_thm) global_def_thm))
- |> Sign.restore_naming thy *)
+ |> Sign.hide_consts_i true [abbr']
+ |> Sign.add_path prfx
+ |> Sign.add_consts_authentic [(c, ty', syn')]
+ |> Sign.parent_path
+ |> Sign.sticky_prefix prfx
+ |> PureThy.add_defs_i false [(def, [])]
+ |> snd
+ |> Sign.restore_naming thy
end;
end;