theorem(_i): note assms of statement;
authorwenzelm
Tue Nov 21 20:48:11 2006 +0100 (2006-11-21)
changeset 21450f16c9e6401d1
parent 21449 0413b46ee5ef
child 21451 28f1181c1a48
theorem(_i): note assms of statement;
src/Pure/Isar/specification.ML
     1.1 --- a/src/Pure/Isar/specification.ML	Tue Nov 21 20:48:06 2006 +0100
     1.2 +++ b/src/Pure/Isar/specification.ML	Tue Nov 21 20:48:11 2006 +0100
     1.3 @@ -201,14 +201,18 @@
     1.4  
     1.5  local
     1.6  
     1.7 +fun subtract_prems ctxt1 ctxt2 =
     1.8 +  Library.drop (length (Assumption.prems_of ctxt1), Assumption.prems_of ctxt2);
     1.9 +
    1.10  fun prep_statement prep_att prep_stmt elems concl ctxt =
    1.11    (case concl of
    1.12      Element.Shows shows =>
    1.13        let
    1.14 -        val (_, _, elems_ctxt, propp) = prep_stmt elems (map snd shows) ctxt;
    1.15 +        val (_, loc_ctxt, elems_ctxt, propp) = prep_stmt elems (map snd shows) ctxt;
    1.16 +        val prems = subtract_prems loc_ctxt elems_ctxt;
    1.17 +        val stmt = Attrib.map_specs prep_att (map fst shows ~~ propp);
    1.18          val goal_ctxt = fold (fold (Variable.auto_fixes o fst)) propp elems_ctxt;
    1.19 -        val stmt = Attrib.map_specs prep_att (map fst shows ~~ propp);
    1.20 -      in ((stmt, []), goal_ctxt) end
    1.21 +      in ((prems, stmt, []), goal_ctxt) end
    1.22    | Element.Obtains obtains =>
    1.23        let
    1.24          val case_names = obtains |> map_index
    1.25 @@ -218,7 +222,7 @@
    1.26              (vars |> map_filter (fn (x, SOME T) => SOME (x, T) | _ => NONE))));
    1.27  
    1.28          val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
    1.29 -        val (_, _, elems_ctxt, propp) = prep_stmt (elems @ constraints) raw_propp ctxt;
    1.30 +        val (_, loc_ctxt, elems_ctxt, propp) = prep_stmt (elems @ constraints) raw_propp ctxt;
    1.31  
    1.32          val thesis = ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) AutoBind.thesisN;
    1.33  
    1.34 @@ -240,6 +244,7 @@
    1.35  
    1.36          val atts = map Attrib.internal
    1.37            [RuleCases.consumes (~ (length obtains)), RuleCases.case_names case_names];
    1.38 +        val prems = subtract_prems loc_ctxt elems_ctxt;
    1.39          val stmt = [(("", atts), [(thesis, [])])];
    1.40  
    1.41          val (facts, goal_ctxt) = elems_ctxt
    1.42 @@ -247,7 +252,7 @@
    1.43            |> fold_map assume_case (obtains ~~ propp)
    1.44            |-> (fn ths => ProofContext.note_thmss_i Thm.assumptionK
    1.45                  [((Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
    1.46 -      in ((stmt, facts), goal_ctxt) end);
    1.47 +      in ((prems, stmt, facts), goal_ctxt) end);
    1.48  
    1.49  fun gen_theorem prep_att prep_stmt
    1.50      kind before_qed after_qed (name, raw_atts) raw_elems raw_concl lthy0 =
    1.51 @@ -266,7 +271,8 @@
    1.52  
    1.53      val elems = raw_elems |> (map o Locale.map_elem)
    1.54        (Element.map_ctxt {name = I, var = I, typ = I, term = I, fact = I, attrib = attrib});
    1.55 -    val ((stmt, facts), goal_ctxt) = prep_statement attrib (prep_stmt loc) elems raw_concl ctxt;
    1.56 +    val ((prems, stmt, facts), goal_ctxt) =
    1.57 +      prep_statement attrib (prep_stmt loc) elems raw_concl ctxt;
    1.58  
    1.59      fun after_qed' results goal_ctxt' =
    1.60        let val results' = burrow (ProofContext.export_standard goal_ctxt' lthy) results in
    1.61 @@ -280,6 +286,8 @@
    1.62        end;
    1.63    in
    1.64      goal_ctxt
    1.65 +    |> ProofContext.note_thmss_i Thm.assumptionK [((AutoBind.assmsN, []), [(prems, [])])]
    1.66 +    |> snd
    1.67      |> Proof.theorem_i before_qed after_qed' (map snd stmt)
    1.68      |> Proof.refine_insert facts
    1.69    end;