more uniform / rigid checking of Goal.prove_common vs. Proof.conclude_goal -- NB: Goal.prove_common cannot check hyps right now, e.g. due to undeclared Simplifier prems;
authorwenzelm
Sat Nov 23 17:15:44 2013 +0100 (2013-11-23)
changeset 54567cfe53047dc16
parent 54566 5f3e9baa8f13
child 54569 e51a0c4965f7
more uniform / rigid checking of Goal.prove_common vs. Proof.conclude_goal -- NB: Goal.prove_common cannot check hyps right now, e.g. due to undeclared Simplifier prems;
src/Pure/Isar/proof.ML
src/Pure/assumption.ML
src/Pure/goal.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Sat Nov 23 17:07:36 2013 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Sat Nov 23 17:15:44 2013 +0100
     1.3 @@ -480,28 +480,25 @@
     1.4  fun conclude_goal ctxt goal propss =
     1.5    let
     1.6      val thy = Proof_Context.theory_of ctxt;
     1.7 -    val string_of_term = Syntax.string_of_term ctxt;
     1.8 -    val string_of_thm = Display.string_of_thm ctxt;
     1.9  
    1.10      val _ = Thm.no_prems goal orelse error (Proof_Display.string_of_goal ctxt goal);
    1.11  
    1.12 -    val extra_hyps = Assumption.extra_hyps ctxt goal;
    1.13 -    val _ = null extra_hyps orelse
    1.14 -      error ("Additional hypotheses:\n" ^ cat_lines (map string_of_term extra_hyps));
    1.15 +    fun lost_structure () = error ("Lost goal structure:\n" ^ Display.string_of_thm ctxt goal);
    1.16  
    1.17 -    fun lost_structure () = error ("Lost goal structure:\n" ^ string_of_thm goal);
    1.18 +    val th =
    1.19 +      (Goal.conclude (if length (flat propss) > 1 then Thm.norm_proof goal else goal)
    1.20 +        handle THM _ => lost_structure ())
    1.21 +      |> Drule.flexflex_unique
    1.22 +      |> Thm.check_shyps (Variable.sorts_of ctxt)
    1.23 +      |> Assumption.check_hyps ctxt;
    1.24  
    1.25 -    val th = Goal.conclude
    1.26 -      (if length (flat propss) > 1 then Thm.norm_proof goal else goal)
    1.27 -      handle THM _ => lost_structure ();
    1.28      val goal_propss = filter_out null propss;
    1.29      val results =
    1.30        Conjunction.elim_balanced (length goal_propss) th
    1.31        |> map2 Conjunction.elim_balanced (map length goal_propss)
    1.32        handle THM _ => lost_structure ();
    1.33      val _ = Unify.matches_list thy (flat goal_propss) (map Thm.prop_of (flat results)) orelse
    1.34 -      error ("Proved a different theorem:\n" ^ string_of_thm th);
    1.35 -    val _ = Thm.check_shyps (Variable.sorts_of ctxt) th;
    1.36 +      error ("Proved a different theorem:\n" ^ Display.string_of_thm ctxt th);
    1.37  
    1.38      fun recover_result ([] :: pss) thss = [] :: recover_result pss thss
    1.39        | recover_result (_ :: pss) (ths :: thss) = ths :: recover_result pss thss
     2.1 --- a/src/Pure/assumption.ML	Sat Nov 23 17:07:36 2013 +0100
     2.2 +++ b/src/Pure/assumption.ML	Sat Nov 23 17:15:44 2013 +0100
     2.3 @@ -12,7 +12,7 @@
     2.4    val assume: cterm -> thm
     2.5    val all_assms_of: Proof.context -> cterm list
     2.6    val all_prems_of: Proof.context -> thm list
     2.7 -  val extra_hyps: Proof.context -> thm -> term list
     2.8 +  val check_hyps: Proof.context -> thm -> thm
     2.9    val local_assms_of: Proof.context -> Proof.context -> cterm list
    2.10    val local_prems_of: Proof.context -> Proof.context -> thm list
    2.11    val add_assms: export -> cterm list -> Proof.context -> thm list * Proof.context
    2.12 @@ -76,8 +76,12 @@
    2.13  val all_assms_of = maps #2 o all_assumptions_of;
    2.14  val all_prems_of = #prems o rep_data;
    2.15  
    2.16 -fun extra_hyps ctxt th =
    2.17 -  subtract (op aconv) (map Thm.term_of (all_assms_of ctxt)) (Thm.hyps_of th);
    2.18 +fun check_hyps ctxt th =
    2.19 +  let
    2.20 +    val extra_hyps = subtract (op aconv) (map Thm.term_of (all_assms_of ctxt)) (Thm.hyps_of th);
    2.21 +    val _ = null extra_hyps orelse
    2.22 +      error ("Additional hypotheses:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) extra_hyps));
    2.23 +  in th end;
    2.24  
    2.25  
    2.26  (* local assumptions *)
     3.1 --- a/src/Pure/goal.ML	Sat Nov 23 17:07:36 2013 +0100
     3.2 +++ b/src/Pure/goal.ML	Sat Nov 23 17:15:44 2013 +0100
     3.3 @@ -182,7 +182,6 @@
     3.4  fun prove_common immediate pri ctxt xs asms props tac =
     3.5    let
     3.6      val thy = Proof_Context.theory_of ctxt;
     3.7 -    val string_of_term = Syntax.string_of_term ctxt;
     3.8  
     3.9      val schematic = exists is_schematic props;
    3.10      val future = future_enabled 1;
    3.11 @@ -191,7 +190,7 @@
    3.12      val pos = Position.thread_data ();
    3.13      fun err msg = cat_error msg
    3.14        ("The error(s) above occurred for the goal statement:\n" ^
    3.15 -        string_of_term (Logic.list_implies (asms, Logic.mk_conjunction_list props)) ^
    3.16 +        Syntax.string_of_term ctxt (Logic.list_implies (asms, Logic.mk_conjunction_list props)) ^
    3.17          (case Position.here pos of "" => "" | s => "\n" ^ s));
    3.18  
    3.19      fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm (Term.no_dummy_patterns t))
    3.20 @@ -215,10 +214,16 @@
    3.21        (case SINGLE (tac' {prems = prems, context = ctxt'}) (init stmt) of
    3.22          NONE => err "Tactic failed"
    3.23        | SOME st =>
    3.24 -          let val res = finish ctxt' st handle THM (msg, _, _) => err msg in
    3.25 -            if Unify.matches_list thy [Thm.term_of stmt] [Thm.prop_of res]
    3.26 -            then Thm.check_shyps sorts res
    3.27 -            else err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res))
    3.28 +          let
    3.29 +            val res =
    3.30 +              (finish ctxt' st
    3.31 +                |> Drule.flexflex_unique
    3.32 +                |> Thm.check_shyps sorts
    3.33 +                (* |> Assumption.check_hyps ctxt' FIXME *))
    3.34 +              handle THM (msg, _, _) => err msg | ERROR msg => err msg;
    3.35 +          in
    3.36 +            if Unify.matches_list thy [Thm.term_of stmt] [Thm.prop_of res] then res
    3.37 +            else err ("Proved a different theorem: " ^ Syntax.string_of_term ctxt' (Thm.prop_of res))
    3.38            end);
    3.39      val res =
    3.40        if immediate orelse schematic orelse not future orelse skip then result ()