# HG changeset patch # User haftmann # Date 1174913587 -7200 # Node ID f9bf5c08b446c3583b46075d16536bd8c9d467ca # Parent 19e4fd6ffcaa197f3907f9dbdeafd28653ed0766 minimal intro rules diff -r 19e4fd6ffcaa -r f9bf5c08b446 src/Pure/Tools/class_package.ML --- a/src/Pure/Tools/class_package.ML Mon Mar 26 14:53:06 2007 +0200 +++ b/src/Pure/Tools/class_package.ML Mon Mar 26 14:53:07 2007 +0200 @@ -31,7 +31,6 @@ 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 fully_qualified: bool ref; val print_classes: theory -> unit val intro_classes_tac: thm list -> tactic @@ -212,11 +211,12 @@ locale: string, consts: (string * string) list (*locale parameter ~> toplevel theory constant*), + intro: thm, witness: Element.witness list, - propnames: string list, + primdefs: thm list, + (*for experimental class target*) + propnames: string list (*for ad-hoc instance_in*) - primdefs: thm list - (*for experimental class target*) }; fun rep_classdata (ClassData c) = c; @@ -261,6 +261,9 @@ end; in maps (params thy) o ancestry thy end; +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; @@ -299,12 +302,13 @@ (* updaters *) -fun add_class_data ((class, superclasses), (locale, consts, witness, propnames)) = +fun add_class_data ((class, superclasses), (locale, consts, intro, witness, propnames)) = ClassData.map (fn (gr, tab) => ( gr |> Graph.new_node (class, ClassData { locale = locale, consts = consts, + intro = intro, witness = witness, propnames = propnames, primdefs = []}) @@ -315,8 +319,9 @@ fun add_primdef (class, thm) thy = (ClassData.map o apfst o Graph.map_node class) - (fn ClassData { locale, consts, witness, propnames, primdefs } => ClassData { locale = locale, - consts = consts, witness = witness, propnames = propnames, primdefs = thm :: primdefs }); + (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 *) @@ -339,7 +344,7 @@ (* tactics and methods *) (*FIXME adjust these when minimal intro rules are at hand*) -fun intro_classes_tac facts st = +fun intro_classes_tac' facts st = let val thy = Thm.theory_of_thm st; val ctxt = ProofContext.init thy; @@ -352,6 +357,22 @@ (intro_classes_tac THEN REPEAT (intro_locales_tac ORELSE intro_locales_tac)) st end; +fun intro_classes_tac facts st = + let + val thy = Thm.theory_of_thm st; + val classes = Sign.all_classes thy; + val class_trivs = map (Thm.class_triv thy) classes; + val class_intros = these_intros thy; + fun add_axclass_intro class = + case try (AxClass.get_definition thy) class of SOME {intro, ...} => cons intro | _ => I; + val axclass_intros = fold add_axclass_intro classes []; + in + st + |> ((ALLGOALS (Method.insert_tac facts THEN' + REPEAT_ALL_NEW (resolve_tac (class_trivs @ class_intros @ axclass_intros)))) + THEN Tactic.distinct_subgoals_tac) + end; + fun default_intro_classes_tac [] = intro_classes_tac [] | default_intro_classes_tac _ = Tactical.no_tac; (*no error message!*) @@ -360,7 +381,9 @@ default_intro_classes_tac facts; val _ = Context.add_setup (Method.add_methods - [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac), + [("intro_classes2", Method.no_args (Method.METHOD intro_classes_tac'), + "back-chain introduction rules of classes"), + ("intro_classes", Method.no_args (Method.METHOD intro_classes_tac), "back-chain introduction rules of classes"), ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some intro/elim rule")]); @@ -411,9 +434,50 @@ val prove_instance_sort = instance_sort' o prove_interpretation_in; -(* classes and instances *) +(* constructing class introduction rules from axclass and locale rules *) -val fully_qualified = ref false; +fun class_intro thy locale class sups = + 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; + 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 class_elim class = + case (map Drule.unconstrainTs o #axioms o AxClass.get_definition thy) class + of [thm] => SOME thm + | [] => NONE; + val pred_intro = case Locale.intros thy locale + of ([ax_intro], [intro]) => intro |> OF_LAST ax_intro |> SOME + | ([intro], []) => SOME intro + | ([], [intro]) => SOME intro + | _ => NONE; + val pred_intro' = pred_intro + |> Option.map (fn intro => intro OF map_filter class_elim sups); + val class_intro = (#intro o AxClass.get_definition thy) class; + val raw_intro = case pred_intro' + of SOME pred_intro => class_intro |> OF_LAST pred_intro + | NONE => class_intro; + in + raw_intro + |> Drule.instantiate' [SOME (Thm.ctyp_of thy typ)] [] + |> strip_all_ofclass + |> Thm.strip_shyps + |> Drule.unconstrainTs + end; + + +(* classes and instances *) local @@ -431,7 +495,8 @@ val (elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e) | Locale.Expr i => apsnd (cons i)) raw_elems ([], []); val supclasses = map (prep_class thy) raw_supclasses; - val sups = filter (is_some o lookup_class_data thy) supclasses; + val sups = filter (is_some o lookup_class_data thy) supclasses + |> Sign.certify_sort thy; val supsort = Sign.certify_sort thy supclasses; val suplocales = map (Locale.Locale o #locale o the_class_data thy) sups; val supexpr = Locale.Merge (suplocales @ includes); @@ -472,7 +537,7 @@ 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*) + |> map (NameSpace.base o fst o fst) (*FIXME - is finally dropped*); fun mk_instT class = Symtab.empty |> Symtab.update (AxClass.param_tyvarname, TFree (AxClass.param_tyvarname, [class])); fun mk_inst class param_names cs = @@ -480,6 +545,10 @@ |> 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], [])])] + #> snd in thy |> add_locale (SOME (bname ^ "_pred")) bname supexpr ((*elems_constrains @*) elems) @@ -488,13 +557,15 @@ #-> (fn (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 => extract_axiom_names thy name_locale) - #-> (fn axiom_names => + `(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, - map2 make_witness ax_terms ax_axioms, axiom_names)) + class_intro, map2 make_witness ax_terms ax_axioms, axiom_names)) + #> note_intro name_axclass class_intro #> prove_interpretation ((ALLGOALS o ProofContext.fact_tac) ax_axioms) - ((!fully_qualified, Logic.const_of_class bname), []) (Locale.Locale name_locale) + ((false, Logic.const_of_class bname), []) (Locale.Locale name_locale) (mk_instT name_axclass, mk_inst name_axclass param_names (map snd supconsts @ consts)) #> pair name_axclass )))))