# HG changeset patch # User haftmann # Date 1185283251 -7200 # Node ID f7eedf3d09a3cb2a15397ba1589854d53b88eee2 # Parent e65254ce5019d7973505ab1dfe997c6625786d38 interpretation_in diff -r e65254ce5019 -r f7eedf3d09a3 src/Pure/Tools/class_package.ML --- a/src/Pure/Tools/class_package.ML Tue Jul 24 15:20:50 2007 +0200 +++ b/src/Pure/Tools/class_package.ML Tue Jul 24 15:20:51 2007 +0200 @@ -29,7 +29,6 @@ val instance_sort_cmd: string * string -> theory -> Proof.state val prove_instance_sort: tactic -> class * sort -> theory -> theory - val INTERPRET_DEF: bool ref val class_of_locale: theory -> string -> class option val add_const_in_class: string -> (string * term) * Syntax.mixfix -> theory -> theory @@ -210,7 +209,7 @@ |-> (fn (cs, defs) => do_proof (after_qed cs defs) arities) end; -fun instance_arity_e' do_proof = gen_instance_arity Sign.read_arity read_def_cmd do_proof; +fun instance_arity_cmd' do_proof = gen_instance_arity Sign.read_arity read_def_cmd do_proof; fun instance_arity' do_proof = gen_instance_arity Sign.cert_arity read_def do_proof; fun tactic_proof tac after_qed arities = fold (fn arity => AxClass.prove_arity arity tac) arities @@ -218,7 +217,7 @@ in -val instance_arity_cmd = instance_arity_e' axclass_instance_arity; +val instance_arity_cmd = instance_arity_cmd' axclass_instance_arity; val instance_arity = instance_arity' axclass_instance_arity; val prove_instance_arity = instance_arity' o tactic_proof; @@ -235,9 +234,7 @@ consts: (string * string) list (*locale parameter ~> toplevel theory constant*), v: string option, - intro: thm, - propnames: string list - (*for ad-hoc instance_in*) + intro: thm }; fun rep_classdata (ClassData c) = c; @@ -281,8 +278,6 @@ Graph.fold (fn (_, (data, _)) => insert Thm.eq_thm ((#intro o rep_classdata) data)) ((fst o ClassData.get) thy) []; -val the_propnames = #propnames oo the_class_data; - fun print_classes thy = let val algebra = Sign.classes_of thy; @@ -318,15 +313,14 @@ (* updaters *) -fun add_class_data ((class, superclasses), (locale, consts, v, intro, propnames)) = +fun add_class_data ((class, superclasses), (locale, consts, v, intro)) = ClassData.map (fn (gr, tab) => ( gr |> Graph.new_node (class, ClassData { locale = locale, consts = consts, v = v, - intro = intro, - propnames = propnames} + intro = intro} ) |> fold (curry Graph.add_edge class) superclasses, tab @@ -380,56 +374,38 @@ |> Proof.global_terminal_proof (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE) |> ProofContext.theory_of; -fun instance_sort' do_proof (class, sort) theory = + +(* constructing class introduction and other rules from axclass and locale rules *) + +fun mk_instT class = Symtab.empty + |> Symtab.update (AxClass.param_tyvarname, TFree (AxClass.param_tyvarname, [class])); + +fun mk_inst class param_names cs = + 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 OF_LAST thm1 thm2 = let - val loc_name = (#locale o the_class_data theory) class; - val loc_expr = - (Locale.Merge o map (Locale.Locale o #locale o the_class_data theory)) sort; - val const_names = (map (NameSpace.base o snd) - o maps (#consts o the_class_data theory) - o ancestry theory) [class]; - fun get_thms thy = - ancestry thy sort - |> AList.make (the_propnames thy) - |> map (apsnd (map (NameSpace.append (Logic.const_of_class loc_name)))) - |> map_filter (fn (superclass, thm_names) => - case map_filter (try (PureThy.get_thm thy o Name)) thm_names - of [] => NONE - | thms => SOME (superclass, thms)); - fun after_qed thy = - thy - |> `get_thms - |-> fold (fn (supclass, thms) => I - AxClass.prove_classrel (class, supclass) - (ALLGOALS (K (intro_classes_tac [])) THEN - (ALLGOALS o ProofContext.fact_tac) thms)) - in - theory - |> do_proof after_qed (loc_name, loc_expr) - end; + val n = (length o Logic.strip_imp_prems o prop_of) thm2; + in (thm1 RSN (n, thm2)) end; -val prove_instance_sort = instance_sort' o prove_interpretation_in; - - -(* constructing class introduction rules from axclass and locale rules *) - -fun class_intro thy locale class sups = +fun strip_all_ofclass thy sort = let - fun OF_LAST thm1 thm2 = - let - val n = (length o Logic.strip_imp_prems o prop_of) thm2; - in (thm1 RSN (n, thm2)) end; + val typ = TVar ((AxClass.param_tyvarname, 0), sort); fun prem_inclass t = case Logic.strip_imp_prems t of ofcls :: _ => try Logic.dest_inclass ofcls | [] => NONE; - val typ = TVar ((AxClass.param_tyvarname, 0), Sign.super_classes thy class); fun strip_ofclass class thm = thm OF (fst o AxClass.of_sort thy (typ, [class])) AxClass.cache; - fun strip_all_ofclass thm = - case (prem_inclass o Thm.prop_of) thm - of SOME (_, class) => thm |> strip_ofclass class |> strip_all_ofclass - | NONE => thm; + fun strip thm = case (prem_inclass o Thm.prop_of) thm + of SOME (_, class) => thm |> strip_ofclass class |> strip + | NONE => thm; + in strip end; + +fun class_intro thy locale class sups = + let fun class_elim class = case (map Drule.unconstrainTs o #axioms o AxClass.get_definition thy) class of [thm] => SOME thm @@ -445,24 +421,39 @@ val raw_intro = case pred_intro' of SOME pred_intro => class_intro |> OF_LAST pred_intro | NONE => class_intro; + val sort = Sign.super_classes thy class; + val typ = TVar ((AxClass.param_tyvarname, 0), sort); in raw_intro |> Drule.instantiate' [SOME (Thm.ctyp_of thy typ)] [] - |> strip_all_ofclass + |> strip_all_ofclass thy sort |> Thm.strip_shyps |> Drule.unconstrainTs end; - -(* classes and instances *) +fun interpretation_in_rule thy (class1, class2) = + let + val (params, consts) = split_list (param_map thy [class1]); + (*FIXME also remember this at add_class*) + fun mk_axioms class = + let + val name_locale = (#locale o the_class_data thy) class; + val inst = mk_inst class params consts; + in + Locale.global_asms_of thy name_locale + |> maps snd + |> (map o map_aterms) (fn Free (s, _) => (the o Symtab.lookup inst) s | t => t) + |> (map o map_types o map_atyps) (fn TFree _ => TFree ("'a", [class1]) | T => T) + |> map (ObjectLogic.ensure_propT thy) + end; + val (prems, concls) = pairself mk_axioms (class1, class2); + in + Goal.prove_global thy [] prems (Logic.mk_conjunction_list concls) + (Locale.intro_locales_tac true (ProofContext.init thy)) + end; -fun mk_instT class = Symtab.empty - |> Symtab.update (AxClass.param_tyvarname, TFree (AxClass.param_tyvarname, [class])); -fun mk_inst class param_names cs = - 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; +(* classes *) local @@ -530,10 +521,6 @@ Locale.global_asms_of thy name_locale |> map prep_asm end; - fun extract_axiom_names thy name_locale = - name_locale - |> Locale.global_asms_of thy - |> map (NameSpace.base o fst o fst) (*FIXME - is finally dropped*); fun note_intro name_axclass class_intro = PureThy.note_thmss_qualified "" ((Logic.const_of_class o NameSpace.base) name_axclass) [(("intro", []), [([class_intro], [])])] @@ -547,11 +534,10 @@ 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) => + #-> (fn class_intro => add_class_data ((name_axclass, sups), (name_locale, map (fst o fst) params ~~ map fst consts, v, - class_intro, axiom_names)) + class_intro)) (*FIXME: class_data should already contain data relevant for interpretation; use this later for class target*) (*FIXME: general export_fixes which may be parametrized @@ -573,6 +559,41 @@ local +fun singular_instance_subclass (class1, class2) thy = + let + val interp = interpretation_in_rule thy (class1, class2); + val ax = #axioms (AxClass.get_definition thy class1); + val intro = #intro (AxClass.get_definition thy class2) + |> Drule.instantiate' [SOME (Thm.ctyp_of thy + (TVar ((AxClass.param_tyvarname, 0), [class1])))] []; + val thm = + intro + |> OF_LAST (interp OF ax) + |> strip_all_ofclass thy (Sign.super_classes thy class2); + in + thy |> AxClass.add_classrel thm + end; + +fun instance_subsort (class, sort) thy = + let + val super_sort = (Graph.all_succs o #classes o Sorts.rep_algebra + o Sign.classes_of) thy sort; + val classes = filter_out (fn class' => Sign.subsort thy ([class], [class'])) + (rev super_sort); + in + thy |> fold (curry singular_instance_subclass class) classes + end; + +fun instance_sort' do_proof (class, sort) theory = + let + val loc_name = (#locale o the_class_data theory) class; + val loc_expr = + (Locale.Merge o map (Locale.Locale o #locale o the_class_data theory)) sort; + in + theory + |> do_proof (instance_subsort (class, sort)) (loc_name, loc_expr) + end; + fun gen_instance_sort prep_class prep_sort (raw_class, raw_sort) theory = let val class = prep_class theory raw_class; @@ -595,6 +616,7 @@ val instance_sort_cmd = gen_instance_sort Sign.read_class Sign.read_sort; val instance_sort = gen_instance_sort Sign.certify_class Sign.certify_sort; +val prove_instance_sort = instance_sort' o prove_interpretation_in; val instance_class_cmd = gen_instance_class Sign.read_class; val instance_class = gen_instance_class Sign.certify_class; @@ -603,8 +625,6 @@ (** class target **) -val INTERPRET_DEF = ref false; - fun export_fixes thy class = let val v = (#v o the_class_data thy) class; @@ -651,8 +671,12 @@ |> Sign.parent_path |> Sign.sticky_prefix prfx |> PureThy.add_defs_i false [(def, [])] - |-> (fn [def] => ! INTERPRET_DEF ? interpret def) + |-> (fn [def] => interpret def) |> Sign.restore_naming thy end; + +(** experimental interpretation_in **) + + end;