# HG changeset patch # User wenzelm # Date 1160686658 -7200 # Node ID 8f3896f0e5af7dc3ee43f3e4fb4e2f741303210f # Parent 081674431d683fc0e1d971dbcef34fce031c91f4 interpretation_in_locale: standalone goal setup; moved theorem statements to bottom; diff -r 081674431d68 -r 8f3896f0e5af src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Thu Oct 12 22:57:35 2006 +0200 +++ b/src/Pure/Isar/locale.ML Thu Oct 12 22:57:38 2006 +0200 @@ -88,6 +88,15 @@ Proof.context -> (string * thm list) list * Proof.context val add_term_syntax: string -> (Proof.context -> Proof.context) -> Proof.context -> Proof.context + val interpretation: (Proof.context -> Proof.context) -> + string * Attrib.src list -> expr -> string option list -> + theory -> Proof.state + val interpretation_in_locale: (Proof.context -> Proof.context) -> + xstring * expr -> theory -> Proof.state + val interpret: (Proof.state -> Proof.state Seq.seq) -> + string * Attrib.src list -> expr -> string option list -> + bool -> Proof.state -> Proof.state + val theorem: string -> Method.text option -> (thm list list -> Proof.context -> Proof.context) -> string * Attrib.src list -> Element.context element list -> Element.statement -> @@ -107,14 +116,6 @@ val smart_theorem: string -> xstring option -> string * Attrib.src list -> Element.context element list -> Element.statement -> theory -> Proof.state - val interpretation: (Proof.context -> Proof.context) -> - string * Attrib.src list -> expr -> string option list -> - theory -> Proof.state - val interpretation_in_locale: (Proof.context -> Proof.context) -> - xstring * expr -> theory -> Proof.state - val interpret: (Proof.state -> Proof.state Seq.seq) -> - string * Attrib.src list -> expr -> string option list -> - bool -> Proof.state -> Proof.state end; structure Locale: LOCALE = @@ -1819,98 +1820,6 @@ -(** locale goals **) - -local - -fun intern_attrib thy = map_elem (Element.map_ctxt - {name = I, var = I, typ = I, term = I, fact = I, attrib = Attrib.intern_src thy}); - -val global_goal = Proof.global_goal ProofDisplay.present_results - Attrib.attribute_i ProofContext.bind_propp_schematic_i; - -fun mk_shows prep_att stmt ctxt = - ((Attrib.map_specs prep_att stmt, []), fold (fold (Variable.fix_frees o fst) o snd) stmt ctxt); - -fun conclusion prep_att (Element.Shows concl) = (([], concl), mk_shows prep_att) - | conclusion _ (Element.Obtains cases) = apfst (apfst (map Elem)) (Obtain.statement cases); - -fun gen_theorem prep_src prep_elem prep_stmt - kind before_qed after_qed (name, raw_atts) raw_elems raw_concl thy = - let - val atts = map (prep_src thy) raw_atts; - val ((concl_elems, concl), mk_stmt) = conclusion (prep_src thy) raw_concl; - - val thy_ctxt = ProofContext.init thy; - val elems = map (prep_elem thy) (raw_elems @ concl_elems); - val (_, _, elems_ctxt, propp) = prep_stmt NONE elems (map snd concl) thy_ctxt; - val ((stmt, facts), goal_ctxt) = mk_stmt (map fst concl ~~ propp) elems_ctxt; - - fun after_qed' results goal_ctxt' = - thy_ctxt - |> ProofContext.transfer (ProofContext.theory_of goal_ctxt') - |> after_qed results; - in - global_goal kind before_qed after_qed' (SOME "") (name, atts) stmt goal_ctxt - |> Proof.refine_insert facts - end; - -fun gen_theorem_in_locale prep_locale prep_src prep_elem prep_stmt no_target - kind before_qed after_qed raw_loc (name, atts) raw_elems raw_concl thy = - let - val ((concl_elems, concl), mk_stmt) = conclusion (prep_src thy) raw_concl; - val loc = prep_locale thy raw_loc; - val loc_atts = map (prep_src thy) atts; - val loc_attss = map (map (prep_src thy) o snd o fst) concl; - val target = if no_target then NONE else SOME (extern thy loc); - val elems = map (prep_elem thy) (raw_elems @ concl_elems); - val names = map (fst o fst) concl; - - val thy_ctxt = init_term_syntax loc (ProofContext.init thy); - val (_, loc_ctxt, elems_ctxt, propp) = - prep_stmt (SOME raw_loc) elems (map snd concl) thy_ctxt; - val ((stmt, facts), goal_ctxt) = mk_stmt (map (apsnd (K []) o fst) concl ~~ propp) elems_ctxt; - - fun after_qed' results goal_ctxt' = - let - val loc_ctxt' = loc_ctxt |> ProofContext.transfer (ProofContext.theory_of goal_ctxt'); - val loc_results = results |> burrow (ProofContext.export_standard goal_ctxt' loc_ctxt'); - in - loc_ctxt' - |> locale_results kind loc ((names ~~ loc_attss) ~~ loc_results) - |-> (fn res => - if name = "" andalso null loc_atts then I - else #2 o locale_results kind loc [((name, loc_atts), maps #2 res)]) - |> after_qed loc_results results - end; - in - global_goal kind before_qed after_qed' target (name, []) stmt goal_ctxt - |> Proof.refine_insert facts - end; - -in - -val theorem = gen_theorem Attrib.intern_src intern_attrib read_context_statement; -val theorem_i = gen_theorem (K I) (K I) cert_context_statement; - -val theorem_in_locale = gen_theorem_in_locale intern Attrib.intern_src intern_attrib - read_context_statement false; - -val theorem_in_locale_i = gen_theorem_in_locale (K I) (K I) (K I) - cert_context_statement false; - -val theorem_in_locale_no_target = gen_theorem_in_locale (K I) (K I) (K I) - cert_context_statement true; - -fun smart_theorem kind NONE a [] (Element.Shows concl) = - Proof.theorem kind NONE (K I) (SOME "") a concl o ProofContext.init - | smart_theorem kind NONE a elems concl = - theorem kind NONE (K I) a elems concl - | smart_theorem kind (SOME loc) a elems concl = - theorem_in_locale kind NONE (K (K I)) loc a elems concl; - -end; - (** Normalisation of locale statements --- discharges goals implied by interpretations **) @@ -2246,7 +2155,7 @@ in (propss, activate) end; -fun prep_propp propss = propss |> map (fn ((name, _), props) => +fun prep_propp propss = propss |> map (fn (_, props) => (("", []), map (rpair [] o Element.mark_witness) props)); fun prep_result propps thmss = @@ -2256,6 +2165,9 @@ kind ^ Proof.goal_names (Option.map (extern thy) target) "" (propss |> map (fn ((name, _), _) => extern thy name)); +val global_goal = Proof.global_goal ProofDisplay.present_results + Attrib.attribute_i ProofContext.bind_propp_schematic_i; + in fun interpretation after_qed (prfx, atts) expr insts thy = @@ -2276,13 +2188,18 @@ val target = intern thy raw_target; val (propss, activate) = prep_registration_in_locale target expr thy; val kind = goal_name thy "interpretation" (SOME target) propss; - fun after_qed' _ results = + val raw_stmt = prep_propp propss; + + val (_, _, goal_ctxt, propp) = thy + |> ProofContext.init |> init_term_syntax target + |> cert_context_statement (SOME target) [] (map snd raw_stmt) + + fun after_qed' results = ProofContext.theory (activate (prep_result propss results)) #> after_qed; in - thy - |> theorem_in_locale_no_target kind NONE after_qed' target ("", []) [] - (Element.Shows (prep_propp propss)) + goal_ctxt + |> global_goal kind NONE after_qed' NONE ("", []) (map fst raw_stmt ~~ propp) |> Element.refine_witness |> Seq.hd end; @@ -2305,4 +2222,94 @@ end; + + +(** locale goals **) + +local + +val global_goal = Proof.global_goal ProofDisplay.present_results + Attrib.attribute_i ProofContext.bind_propp_schematic_i; + +fun intern_attrib thy = map_elem (Element.map_ctxt + {name = I, var = I, typ = I, term = I, fact = I, attrib = Attrib.intern_src thy}); + +fun mk_shows prep_att stmt ctxt = + ((Attrib.map_specs prep_att stmt, []), fold (fold (Variable.fix_frees o fst) o snd) stmt ctxt); + +fun conclusion prep_att (Element.Shows concl) = (([], concl), mk_shows prep_att) + | conclusion _ (Element.Obtains cases) = apfst (apfst (map Elem)) (Obtain.statement cases); + +fun gen_theorem prep_src prep_elem prep_stmt + kind before_qed after_qed (name, raw_atts) raw_elems raw_concl thy = + let + val atts = map (prep_src thy) raw_atts; + val ((concl_elems, concl), mk_stmt) = conclusion (prep_src thy) raw_concl; + + val thy_ctxt = ProofContext.init thy; + val elems = map (prep_elem thy) (raw_elems @ concl_elems); + val (_, _, elems_ctxt, propp) = prep_stmt NONE elems (map snd concl) thy_ctxt; + val ((stmt, facts), goal_ctxt) = mk_stmt (map fst concl ~~ propp) elems_ctxt; + + fun after_qed' results goal_ctxt' = + thy_ctxt + |> ProofContext.transfer (ProofContext.theory_of goal_ctxt') + |> after_qed results; + in + global_goal kind before_qed after_qed' (SOME "") (name, atts) stmt goal_ctxt + |> Proof.refine_insert facts + end; + +fun gen_theorem_in_locale prep_locale prep_src prep_elem prep_stmt + kind before_qed after_qed raw_loc (name, atts) raw_elems raw_concl thy = + let + val ((concl_elems, concl), mk_stmt) = conclusion (prep_src thy) raw_concl; + val loc = prep_locale thy raw_loc; + val loc_atts = map (prep_src thy) atts; + val loc_attss = map (map (prep_src thy) o snd o fst) concl; + val elems = map (prep_elem thy) (raw_elems @ concl_elems); + val names = map (fst o fst) concl; + + val thy_ctxt = init_term_syntax loc (ProofContext.init thy); + val (_, loc_ctxt, elems_ctxt, propp) = + prep_stmt (SOME raw_loc) elems (map snd concl) thy_ctxt; + val ((stmt, facts), goal_ctxt) = mk_stmt (map (apsnd (K []) o fst) concl ~~ propp) elems_ctxt; + + fun after_qed' results goal_ctxt' = + let + val loc_ctxt' = loc_ctxt |> ProofContext.transfer (ProofContext.theory_of goal_ctxt'); + val loc_results = results |> burrow (ProofContext.export_standard goal_ctxt' loc_ctxt'); + in + loc_ctxt' + |> locale_results kind loc ((names ~~ loc_attss) ~~ loc_results) + |-> (fn res => + if name = "" andalso null loc_atts then I + else #2 o locale_results kind loc [((name, loc_atts), maps #2 res)]) + |> after_qed loc_results results + end; + in + global_goal kind before_qed after_qed' (SOME (extern thy loc)) (name, []) stmt goal_ctxt + |> Proof.refine_insert facts + end; + +in + +val theorem = gen_theorem Attrib.intern_src intern_attrib read_context_statement; +val theorem_i = gen_theorem (K I) (K I) cert_context_statement; + +val theorem_in_locale = + gen_theorem_in_locale intern Attrib.intern_src intern_attrib read_context_statement; + +val theorem_in_locale_i = + gen_theorem_in_locale (K I) (K I) (K I) cert_context_statement; + +fun smart_theorem kind NONE a [] (Element.Shows concl) = + Proof.theorem kind NONE (K I) (SOME "") a concl o ProofContext.init + | smart_theorem kind NONE a elems concl = + theorem kind NONE (K I) a elems concl + | smart_theorem kind (SOME loc) a elems concl = + theorem_in_locale kind NONE (K (K I)) loc a elems concl; + end; + +end;