src/Pure/goal.ML
changeset 17986 0450847646c3
parent 17983 89103008502f
child 18027 09ab79d4e8e1
     1.1 --- a/src/Pure/goal.ML	Tue Oct 25 18:18:49 2005 +0200
     1.2 +++ b/src/Pure/goal.ML	Tue Oct 25 18:18:57 2005 +0200
     1.3 @@ -17,8 +17,8 @@
     1.4    val init: cterm -> thm
     1.5    val conclude: thm -> thm
     1.6    val finish: thm -> thm
     1.7 -  val prove_raw: theory -> term -> tactic -> thm
     1.8    val norm_hhf_rule: thm -> thm
     1.9 +  val prove_raw: cterm list -> cterm -> (thm list -> tactic) -> thm
    1.10    val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
    1.11    val prove_multi: theory -> string list -> term list -> term list ->
    1.12      (thm list -> tactic) -> thm list
    1.13 @@ -65,15 +65,7 @@
    1.14        ("\n" ^ string_of_int n ^ " unsolved goal(s)!"), 0, [th]));
    1.15  
    1.16  
    1.17 -(* prove_raw -- minimal checks, no normalization *)
    1.18 -
    1.19 -fun prove_raw thy goal tac =
    1.20 -  (case SINGLE tac (init (Thm.cterm_of thy goal)) of
    1.21 -    SOME th => finish th
    1.22 -  | NONE => raise ERROR_MESSAGE "Tactic failed.");
    1.23 -
    1.24 -
    1.25 -(* tactical proving *)
    1.26 +(* prove_raw -- minimal result checks, no normalization *)
    1.27  
    1.28  val norm_hhf_plain =  (* FIXME remove *)
    1.29    (not o Drule.is_norm_hhf o Thm.prop_of) ?
    1.30 @@ -84,6 +76,14 @@
    1.31    #> Thm.adjust_maxidx_thm
    1.32    #> Drule.gen_all;
    1.33  
    1.34 +fun prove_raw casms cprop tac =
    1.35 +  (case SINGLE (tac (map (norm_hhf_rule o Thm.assume) casms)) (init cprop) of
    1.36 +    SOME th => Drule.implies_intr_list casms (finish th)
    1.37 +  | NONE => raise ERROR_MESSAGE "Tactic failed.");
    1.38 +
    1.39 +
    1.40 +(* tactical proving *)
    1.41 +
    1.42  local
    1.43  
    1.44  fun gen_prove finish_thm thy xs asms props tac =
    1.45 @@ -114,7 +114,7 @@
    1.46      val raw_result = finish goal' handle THM (msg, _, _) => err msg;
    1.47  
    1.48      val prop' = Thm.prop_of raw_result;
    1.49 -    val _ = conditional (not (Pattern.matches thy (prop, prop'))) (fn () =>
    1.50 +    val _ = conditional (not (Pattern.matches thy (Envir.beta_norm prop, prop'))) (fn () =>
    1.51        err ("Proved a different theorem: " ^ Sign.string_of_term thy prop'));
    1.52    in
    1.53      Drule.conj_elim_precise (length props) raw_result