# HG changeset patch # User haftmann # Date 1232349402 -3600 # Node ID 9846af6c6d6a42ded603060fd45bb4a618595cfa # Parent 5362cc5ee3a87b07b81247dbb03c5ba782b0b803 improved tackling of subclasses diff -r 5362cc5ee3a8 -r 9846af6c6d6a src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Mon Jan 19 08:16:42 2009 +0100 +++ b/src/Pure/Isar/class.ML Mon Jan 19 08:16:42 2009 +0100 @@ -89,7 +89,7 @@ in (base_morph, morph, export_morph, axiom, assm_intro, of_class) end; -fun gen_class_spec prep_class process_decl thy raw_supclasses raw_elems = +fun prep_class_spec prep_class process_decl thy raw_supclasses raw_elems = let (*FIXME 2009 simplify*) val supclasses = map (prep_class thy) raw_supclasses; @@ -125,8 +125,8 @@ val (elems, global_syntax) = fold_map fork_syn syntax_elems []; in (((sups, supparam_names), (supsort, base_sort, supexpr)), (constrain :: elems, global_syntax)) end; -val cert_class_spec = gen_class_spec (K I) Expression.cert_declaration; -val read_class_spec = gen_class_spec Sign.intern_class Expression.cert_read_declaration; +val cert_class_spec = prep_class_spec (K I) Expression.cert_declaration; +val read_class_spec = prep_class_spec Sign.intern_class Expression.cert_read_declaration; fun add_consts bname class base_sort sups supparams global_syntax thy = let @@ -218,51 +218,36 @@ fun gen_subclass prep_class do_proof raw_sup lthy = let val thy = ProofContext.theory_of lthy; - val sup = prep_class thy raw_sup; - val sub = case TheoryTarget.peek lthy - of {is_class = false, ...} => error "Not a class context" + val proto_sup = prep_class thy raw_sup; + val proto_sub = case TheoryTarget.peek lthy + of {is_class = false, ...} => error "Not in a class context" | {target, ...} => target; - - val _ = if Sign.subsort thy ([sup], [sub]) - then error ("Class " ^ Syntax.string_of_sort lthy [sup] - ^ " is subclass of class " ^ Syntax.string_of_sort lthy [sub]) - else (); - val sub_params = map fst (these_params thy [sub]); - val sup_params = map fst (these_params thy [sup]); - val err_params = subtract (op =) sub_params sup_params; - val _ = if null err_params then [] else - error ("Class " ^ Syntax.string_of_sort lthy [sub] ^ " lacks parameter(s) " ^ - commas_quote err_params ^ " of " ^ Syntax.string_of_sort lthy [sup]); + val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup) val expr = ([(sup, (("", false), Expression.Positional []))], []); - val (([props], _, _), goal_ctxt) = + val (([props], deps, export), goal_ctxt) = Expression.cert_goal_expression expr lthy; val some_prop = try the_single props; - - fun tac some_thm = ALLGOALS (ProofContext.fact_tac (the_list some_thm)); - fun prove_sublocale some_thm = - Expression.sublocale sub expr - #> Proof.global_terminal_proof - (Method.Basic (K (Method.SIMPLE_METHOD (tac some_thm)), Position.none), NONE) - #> ProofContext.theory_of; - fun after_qed some_thm = - LocalTheory.theory (register_subclass (sub, sup) some_thm) - #> is_some some_thm ? LocalTheory.theory (prove_sublocale some_thm) - (*FIXME should also go to register_subclass*) - #> ProofContext.theory_of - #> TheoryTarget.init (SOME sub); - in do_proof after_qed some_prop lthy end; + val some_dep_morph = try the_single (map snd deps); + fun after_qed some_wit = + ProofContext.theory (register_subclass (sub, sup) + some_dep_morph some_wit export) + #> ProofContext.theory_of #> TheoryTarget.init (SOME sub); + in do_proof after_qed some_prop goal_ctxt end; fun user_proof after_qed NONE = Proof.theorem_i NONE (K (after_qed NONE)) [[]] + #> Element.refine_witness #> Seq.hd | user_proof after_qed (SOME prop) = - Proof.theorem_i NONE (after_qed o try the_single o the_single) [[(prop, [])]]; + Proof.theorem_i NONE (after_qed o SOME o Element.make_witness prop + o Thm.close_derivation o the_single o the_single) + [[(Element.mark_witness prop, [])]] + #> Element.refine_witness #> Seq.hd; -fun tactic_proof tac after_qed NONE lthy = - after_qed NONE lthy - | tactic_proof tac after_qed (SOME prop) lthy = - after_qed (SOME (Goal.prove (LocalTheory.target_of lthy) [] [] prop - (K tac))) lthy; +fun tactic_proof tac after_qed NONE ctxt = + after_qed NONE ctxt + | tactic_proof tac after_qed (SOME prop) ctxt = + after_qed (SOME (Element.prove_witness ctxt prop tac)) ctxt; in diff -r 5362cc5ee3a8 -r 9846af6c6d6a src/Pure/Isar/class_target.ML --- a/src/Pure/Isar/class_target.ML Mon Jan 19 08:16:42 2009 +0100 +++ b/src/Pure/Isar/class_target.ML Mon Jan 19 08:16:42 2009 +0100 @@ -10,8 +10,8 @@ val register: class -> class list -> ((string * typ) * (string * typ)) list -> sort -> morphism -> thm option -> thm option -> thm -> theory -> theory - val register_subclass: class * class -> thm option - -> theory -> theory + val register_subclass: class * class -> morphism option -> Element.witness option + -> morphism -> theory -> theory val is_class: theory -> class -> bool val base_sort: theory -> class -> sort @@ -270,16 +270,14 @@ |> is_some some_def ? activate_defs class (the_list some_def) end; -fun register_subclass (sub, sup) thms thy = - (*FIXME should also add subclass interpretation*) +fun register_subclass (sub, sup) some_dep_morph some_wit export thy = let - val of_class = (snd o rules thy) sup; - val intro = case thms - of SOME thm => Drule.standard' (of_class OF [Drule.standard' thm]) - | NONE => Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o pair (Name.aT, 0)) - ([], [sub])], []) of_class; - val classrel = (intro OF (the_list o fst o rules thy) sub) - |> Thm.close_derivation; + val intros = (snd o rules thy) sup :: map_filter I + [Option.map (Drule.standard' o Element.conclude_witness) some_wit, + (fst o rules thy) sub]; + val tac = ALLGOALS (EVERY' (map Tactic.rtac intros)); + val classrel = Goal.prove_global thy [] [] (Logic.mk_classrel (sub, sup)) + (K tac); val diff_sort = Sign.complete_sort thy [sup] |> subtract (op =) (Sign.complete_sort thy [sub]); in @@ -287,6 +285,11 @@ |> AxClass.add_classrel classrel |> ClassData.map (Graph.add_edge (sub, sup)) |> activate_defs sub (these_defs thy diff_sort) + |> fold2 (fn dep_morph => fn wit => Locale.add_dependency sub (sup, + dep_morph $> Element.satisfy_morphism [wit] $> export)) + (the_list some_dep_morph) (the_list some_wit) + |> (fn thy => fold_rev Locale.activate_global_facts + (Locale.get_registrations thy) thy) end;