# HG changeset patch # User wenzelm # Date 1138881248 -3600 # Node ID a8e913c93578e7b66e61ee58b76ed6a371522093 # Parent e3d2aa8ba0e170b5bd6e58ee86b5481e2980f5ba theorem(_in_locale): Element.statement, Obtain.statement; diff -r e3d2aa8ba0e1 -r a8e913c93578 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Thu Feb 02 12:52:25 2006 +0100 +++ b/src/Pure/Isar/locale.ML Thu Feb 02 12:54:08 2006 +0100 @@ -52,7 +52,7 @@ val global_asms_of: theory -> string -> ((string * Attrib.src list) * term list) list - (* Processing of locale statements *) (* FIXME export more abstract version *) + (* Processing of locale statements *) val read_context_statement: xstring option -> Element.context element list -> (string * (string list * string list)) list list -> Proof.context -> string option * (cterm list * Proof.context) * (cterm list * Proof.context) * @@ -92,26 +92,21 @@ ((string * thm list) list * (string * thm list) list) * Proof.context val theorem: string -> Method.text option -> (thm list list -> theory -> theory) -> - string * Attrib.src list -> Element.context element list -> - ((string * Attrib.src list) * (string * (string list * string list)) list) list -> + string * Attrib.src list -> Element.context element list -> Element.statement -> theory -> Proof.state val theorem_i: string -> Method.text option -> (thm list list -> theory -> theory) -> - string * attribute list -> Element.context_i element list -> - ((string * attribute list) * (term * (term list * term list)) list) list -> + string * attribute list -> Element.context_i element list -> Element.statement_i -> theory -> Proof.state val theorem_in_locale: string -> Method.text option -> (thm list list -> thm list list -> theory -> theory) -> - xstring -> string * Attrib.src list -> Element.context element list -> - ((string * Attrib.src list) * (string * (string list * string list)) list) list -> + xstring -> string * Attrib.src list -> Element.context element list -> Element.statement -> theory -> Proof.state val theorem_in_locale_i: string -> Method.text option -> (thm list list -> thm list list -> theory -> theory) -> string -> string * Attrib.src list -> Element.context_i element list -> - ((string * Attrib.src list) * (term * (term list * term list)) list) list -> - theory -> Proof.state + (typ, term, Attrib.src) Element.stmt -> theory -> Proof.state val smart_theorem: string -> xstring option -> - string * Attrib.src list -> Element.context element list -> - ((string * Attrib.src list) * (string * (string list * string list)) list) list -> + string * Attrib.src list -> Element.context element list -> Element.statement -> theory -> Proof.state val interpretation: string * Attrib.src list -> expr -> string option list -> theory -> Proof.state @@ -1108,9 +1103,7 @@ fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) => (x, AList.lookup (op =) parms x, mx)) fixes) - | finish_ext_elem parms _ (Constrains csts, _) = - (* FIXME fails if x is not a parameter *) - Constrains (map (fn (x, _) => (x, (the o AList.lookup (op =) parms) x)) csts) + | finish_ext_elem parms _ (Constrains _, _) = Constrains [] | finish_ext_elem _ close (Assumes asms, propp) = close (Assumes (map #1 asms ~~ propp)) | finish_ext_elem _ close (Defines defs, propp) = @@ -1746,23 +1739,35 @@ fun global_goal prep_att = Proof.global_goal ProofDisplay.present_results prep_att ProofContext.bind_propp_schematic_i; -fun gen_theorem prep_att prep_elem prep_stmt kind before_qed after_qed a raw_elems concl thy = +fun insert_facts [] = I + | insert_facts ths = Seq.hd o Proof.refine (Method.Basic (K (Method.insert ths))); + +fun conclusion (Element.Shows concl) = (([], concl), fn stmt => fn ctxt => ((stmt, []), ctxt)) + | conclusion (Element.Obtains cases) = apfst (apfst (map Elem)) (Obtain.statement cases); + +fun gen_theorem prep_att prep_elem prep_stmt kind before_qed after_qed a raw_elems raw_concl thy = let + val ((concl_elems, concl), mk_stmt) = conclusion raw_concl; val thy_ctxt = ProofContext.init thy; - val elems = map (prep_elem thy) raw_elems; + val elems = map (prep_elem thy) (raw_elems @ concl_elems); val (_, _, (view, ctxt), propp) = prep_stmt NONE elems (map snd concl) thy_ctxt; - val ctxt' = ctxt |> ProofContext.add_view thy_ctxt view; - val stmt = map fst concl ~~ propp; - in global_goal prep_att kind before_qed after_qed (SOME "") a stmt ctxt' end; + val ((stmt, facts), goal_ctxt) = ctxt + |> ProofContext.add_view thy_ctxt view + |> mk_stmt (map fst concl ~~ propp); + in + global_goal prep_att kind before_qed after_qed (SOME "") a stmt goal_ctxt + |> insert_facts 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 concl thy = + kind before_qed after_qed raw_loc (name, atts) raw_elems raw_concl thy = let + val ((concl_elems, concl), mk_stmt) = conclusion 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; + val elems = map (prep_elem thy) (raw_elems @ concl_elems); val names = map (fst o fst) concl; val thy_ctxt = ProofContext.init thy; @@ -1774,11 +1779,12 @@ val loc_ctxt' = loc_ctxt |> ProofContext.add_view thy_ctxt loc_view; - val stmt = map (apsnd (K []) o fst) concl ~~ propp; + val ((stmt, facts), goal_ctxt) = + elems_ctxt' |> mk_stmt (map (apsnd (K []) o fst) concl ~~ propp); fun after_qed' results = let val loc_results = results |> (map o map) - (ProofContext.export_standard elems_ctxt' loc_ctxt') in + (ProofContext.export_standard goal_ctxt loc_ctxt') in curry (locale_results kind loc ((names ~~ loc_attss) ~~ loc_results)) loc_ctxt #-> (fn res => if name = "" andalso null loc_atts then I @@ -1786,7 +1792,10 @@ #> #2 #> after_qed loc_results results end; - in global_goal (K I) kind before_qed after_qed' target (name, []) stmt elems_ctxt' end; + in + global_goal (K I) kind before_qed after_qed' target (name, []) stmt goal_ctxt + |> insert_facts facts + end; in @@ -1802,7 +1811,7 @@ 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 [] concl = +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 @@ -2144,7 +2153,8 @@ val after_qed = K (activate o prep_result propss); in thy - |> theorem_in_locale_no_target kind NONE after_qed target ("", []) [] (prep_propp propss) + |> theorem_in_locale_no_target kind NONE after_qed target ("", []) [] + (Element.Shows (prep_propp propss)) |> refine_protected end;