# HG changeset patch # User haftmann # Date 1179988659 -7200 # Node ID ad7244663431d205feccd7b6c2631b5bde33e01c # Parent 12320f6e25234db2a3a681b1e3bdd12cbcc7a25b rudimentary class target implementation diff -r 12320f6e2523 -r ad7244663431 src/HOL/Finite_Set.thy --- 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 \) 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 \) 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 \ \ 'a\{linorder, pordered_ab_semigroup_add} \ 'a \ 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 \ \ 'a\linorder \ 'a \ bool" "op <"] by (rule Linorder.intro, rule linorder_axioms) declare Min_singleton [simp] diff -r 12320f6e2523 -r ad7244663431 src/HOL/Lattices.thy --- 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 \ \ 'a\linorder \ 'a \ 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 \ 'a\{lower_semilattice, linorder} \ 'a \ 'a)" by (rule ext)+ auto diff -r 12320f6e2523 -r ad7244663431 src/HOL/Orderings.thy --- 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 "\" 50) -hide const min max - -definition - min :: "'a\ord \ 'a \ 'a" where - "min a b = (if a \ b then a else b)" - -definition - max :: "'a\ord \ 'a \ 'a" where - "max a b = (if a \ 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 \ \ 'a\ord \ 'a \ bool) = min" - by rule+ (simp add: min_def ord_class.min_def) - -lemma linorder_class_max: - "ord.max (op \ \ 'a\ord \ 'a \ 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 *} diff -r 12320f6e2523 -r ad7244663431 src/Pure/Isar/theory_target.ML --- 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, diff -r 12320f6e2523 -r ad7244663431 src/Pure/Tools/class_package.ML --- 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;