Goal.prove;
authorwenzelm
Fri Oct 21 18:14:34 2005 +0200 (2005-10-21)
changeset 17956369e2af8ee45
parent 17955 3b34516662c6
child 17957 d31acb64aa9a
Goal.prove;
src/HOL/Algebra/abstract/Ring.thy
src/HOL/Fun.thy
src/HOL/Hoare/hoare.ML
src/HOL/Hoare/hoareAbort.ML
src/HOL/Hyperreal/transfer.ML
src/HOL/IMPP/Hoare.ML
src/HOL/Integ/int_arith1.ML
src/HOL/List.thy
src/HOL/Product_Type.thy
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/typedef_package.ML
src/HOLCF/adm_tac.ML
src/Provers/Arith/abel_cancel.ML
src/Provers/Arith/assoc_fold.ML
src/Provers/quantifier1.ML
src/Pure/Isar/skip_proof.ML
src/Pure/axclass.ML
src/ZF/Datatype.ML
src/ZF/arith_data.ML
     1.1 --- a/src/HOL/Algebra/abstract/Ring.thy	Fri Oct 21 18:14:32 2005 +0200
     1.2 +++ b/src/HOL/Algebra/abstract/Ring.thy	Fri Oct 21 18:14:34 2005 +0200
     1.3 @@ -164,7 +164,7 @@
     1.4  	 "t * u::'a::ring",
     1.5  	 "- t::'a::ring"];
     1.6      fun proc sg ss t = 
     1.7 -      let val rew = Tactic.prove sg [] []
     1.8 +      let val rew = Goal.prove sg [] []
     1.9              (HOLogic.mk_Trueprop
    1.10                (HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t))))
    1.11                  (fn _ => simp_tac (Simplifier.inherit_context ss ring_ss) 1)
     2.1 --- a/src/HOL/Fun.thy	Fri Oct 21 18:14:32 2005 +0200
     2.2 +++ b/src/HOL/Fun.thy	Fri Oct 21 18:14:34 2005 +0200
     2.3 @@ -497,7 +497,7 @@
     2.4        (fn sg => fn ss => fn t =>
     2.5          case find_double t of (T, NONE) => NONE
     2.6          | (T, SOME rhs) =>
     2.7 -            SOME (Tactic.prove sg [] [] (Term.equals T $ t $ rhs) (K (fun_upd_prover ss))))
     2.8 +            SOME (Goal.prove sg [] [] (Term.equals T $ t $ rhs) (K (fun_upd_prover ss))))
     2.9  end;
    2.10  Addsimprocs[fun_upd2_simproc];
    2.11  
     3.1 --- a/src/HOL/Hoare/hoare.ML	Fri Oct 21 18:14:32 2005 +0200
     3.2 +++ b/src/HOL/Hoare/hoare.ML	Fri Oct 21 18:14:34 2005 +0200
     3.3 @@ -82,7 +82,7 @@
     3.4                             Free ("P",varsT --> boolT) $ Bound 0));
     3.5                     val impl = implies $ (Mset_incl big_Collect) $ 
     3.6                                            (Mset_incl small_Collect);
     3.7 -   in Tactic.prove (Thm.sign_of_thm thm) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
     3.8 +   in Goal.prove (Thm.sign_of_thm thm) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
     3.9  
    3.10  end;
    3.11  
     4.1 --- a/src/HOL/Hoare/hoareAbort.ML	Fri Oct 21 18:14:32 2005 +0200
     4.2 +++ b/src/HOL/Hoare/hoareAbort.ML	Fri Oct 21 18:14:34 2005 +0200
     4.3 @@ -83,7 +83,7 @@
     4.4                             Free ("P",varsT --> boolT) $ Bound 0));
     4.5                     val impl = implies $ (Mset_incl big_Collect) $ 
     4.6                                            (Mset_incl small_Collect);
     4.7 -   in Tactic.prove (Thm.sign_of_thm thm) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
     4.8 +   in Goal.prove (Thm.sign_of_thm thm) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
     4.9  
    4.10  end;
    4.11  
     5.1 --- a/src/HOL/Hyperreal/transfer.ML	Fri Oct 21 18:14:32 2005 +0200
     5.2 +++ b/src/HOL/Hyperreal/transfer.ML	Fri Oct 21 18:14:34 2005 +0200
     5.3 @@ -72,7 +72,7 @@
     5.4        , REPEAT_ALL_NEW (resolve_tac intros) 1
     5.5        , match_tac [reflexive_thm] 1 ]
     5.6    in
     5.7 -    prove_goalw_cterm (ths @ refolds @ unfolds) ct (fn _ => tacs)
     5.8 +    OldGoals.prove_goalw_cterm (ths @ refolds @ unfolds) ct (fn _ => tacs)
     5.9    end
    5.10  
    5.11  fun transfer_tac ths =
     6.1 --- a/src/HOL/IMPP/Hoare.ML	Fri Oct 21 18:14:32 2005 +0200
     6.2 +++ b/src/HOL/IMPP/Hoare.ML	Fri Oct 21 18:14:34 2005 +0200
     6.3 @@ -268,7 +268,7 @@
     6.4  by  (resolve_tac (premises()(*hoare_derivs.asm*)) 1);
     6.5  by  (Fast_tac 1);
     6.6  by (resolve_tac (tl(premises())(*MGT_BodyN*)) 1);
     6.7 -byev[dtac spec 1, etac impE 1, etac impE 2, dtac spec 3,etac mp 3];
     6.8 +by (EVERY [dtac spec 1, etac impE 1, etac impE 2, dtac spec 3,etac mp 3]);
     6.9  by   (eresolve_tac (tl(tl(tl(premises())))) 3);
    6.10  by   (Fast_tac 1);
    6.11  by (dtac finite_subset 1);
     7.1 --- a/src/HOL/Integ/int_arith1.ML	Fri Oct 21 18:14:32 2005 +0200
     7.2 +++ b/src/HOL/Integ/int_arith1.ML	Fri Oct 21 18:14:34 2005 +0200
     7.3 @@ -96,7 +96,7 @@
     7.4      if t aconv u then NONE
     7.5      else
     7.6        let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
     7.7 -      in SOME (Tactic.prove sg xs [] eq (K (EVERY tacs))) end
     7.8 +      in SOME (Goal.prove sg xs [] eq (K (EVERY tacs))) end
     7.9  
    7.10    fun prove_conv_nohyps tacs sg = prove_conv tacs sg [];
    7.11    fun prove_conv_nohyps_novars tacs sg = prove_conv tacs sg [] [];
     8.1 --- a/src/HOL/List.thy	Fri Oct 21 18:14:32 2005 +0200
     8.2 +++ b/src/HOL/List.thy	Fri Oct 21 18:14:34 2005 +0200
     8.3 @@ -453,7 +453,7 @@
     8.4          val app = Const("List.op @",appT)
     8.5          val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
     8.6          val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2));
     8.7 -        val thm = Tactic.prove sg [] [] eq
     8.8 +        val thm = Goal.prove sg [] [] eq
     8.9            (K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1));
    8.10        in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;
    8.11  
     9.1 --- a/src/HOL/Product_Type.thy	Fri Oct 21 18:14:32 2005 +0200
     9.2 +++ b/src/HOL/Product_Type.thy	Fri Oct 21 18:14:34 2005 +0200
     9.3 @@ -413,7 +413,7 @@
     9.4    fun split_pat tp i (Abs  (_,_,t)) = if tp 0 i t then SOME (i,t) else NONE
     9.5    |   split_pat tp i (Const ("split", _) $ Abs (_, _, t)) = split_pat tp (i+1) t
     9.6    |   split_pat tp i _ = NONE;
     9.7 -  fun metaeq thy ss lhs rhs = mk_meta_eq (Tactic.prove thy [] []
     9.8 +  fun metaeq thy ss lhs rhs = mk_meta_eq (Goal.prove thy [] []
     9.9          (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs)))
    9.10          (K (simp_tac (Simplifier.inherit_context ss HOL_basic_ss addsimps [cond_split_eta]) 1)));
    9.11  
    10.1 --- a/src/HOL/Tools/datatype_package.ML	Fri Oct 21 18:14:32 2005 +0200
    10.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Oct 21 18:14:34 2005 +0200
    10.3 @@ -347,10 +347,10 @@
    10.4                               in (case (#distinct (datatype_info_err sg tname1)) of
    10.5                                   QuickAndDirty => SOME (Thm.invoke_oracle
    10.6                                     Datatype_thy distinctN (sg, ConstrDistinct eq_t))
    10.7 -                               | FewConstrs thms => SOME (Tactic.prove sg [] [] eq_t (K
    10.8 +                               | FewConstrs thms => SOME (Goal.prove sg [] [] eq_t (K
    10.9                                     (EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
   10.10                                      atac 2, resolve_tac thms 1, etac FalseE 1])))
   10.11 -                               | ManyConstrs (thm, simpset) => SOME (Tactic.prove sg [] [] eq_t (K
   10.12 +                               | ManyConstrs (thm, simpset) => SOME (Goal.prove sg [] [] eq_t (K
   10.13                                     (EVERY [rtac eq_reflection 1, rtac iffI 1, dtac thm 1,
   10.14                                      full_simp_tac (Simplifier.inherit_context ss simpset) 1,
   10.15                                      REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
    11.1 --- a/src/HOL/Tools/typedef_package.ML	Fri Oct 21 18:14:32 2005 +0200
    11.2 +++ b/src/HOL/Tools/typedef_package.ML	Fri Oct 21 18:14:34 2005 +0200
    11.3 @@ -226,8 +226,8 @@
    11.4      val (cset, goal, _, typedef_result) =
    11.5        prepare_typedef prep_term def name typ set opt_morphs thy;
    11.6      val _ = message ("Proving non-emptiness of set " ^ quote (string_of_cterm cset) ^ " ...");
    11.7 -    val non_empty = Tactic.prove thy [] [] goal (K tac) handle ERROR =>
    11.8 -      error ("Failed to prove non-emptiness of " ^ quote (string_of_cterm cset));
    11.9 +    val non_empty = Goal.prove thy [] [] goal (K tac) handle ERROR_MESSAGE msg =>
   11.10 +      error (msg ^ "\nFailed to prove non-emptiness of " ^ quote (string_of_cterm cset));
   11.11      val ((thy', _), result) = (thy, non_empty) |> typedef_result;
   11.12    in (thy', result) end;
   11.13  
    12.1 --- a/src/HOLCF/adm_tac.ML	Fri Oct 21 18:14:32 2005 +0200
    12.2 +++ b/src/HOLCF/adm_tac.ML	Fri Oct 21 18:14:34 2005 +0200
    12.3 @@ -102,7 +102,7 @@
    12.4           | mk_all ((a,T)::Ts) t = (all T) $ (Abs (a, T, mk_all Ts t));
    12.5         val t = HOLogic.mk_Trueprop((Const (cont_name, contT)) $ (Abs(s, T, t)));
    12.6         val t' = mk_all params (Logic.list_implies (prems, t));
    12.7 -       val thm = Tactic.prove sign [] [] t' (K (tac 1));
    12.8 +       val thm = Goal.prove sign [] [] t' (K (tac 1));
    12.9    in (ts, thm)::l end
   12.10    handle ERROR_MESSAGE _ => l;
   12.11  
    13.1 --- a/src/Provers/Arith/abel_cancel.ML	Fri Oct 21 18:14:32 2005 +0200
    13.2 +++ b/src/Provers/Arith/abel_cancel.ML	Fri Oct 21 18:14:34 2005 +0200
    13.3 @@ -90,7 +90,7 @@
    13.4  
    13.5  fun sum_proc sg ss t =
    13.6     let val t' = cancel sg t
    13.7 -       val thm = Tactic.prove sg [] [] (Logic.mk_equals (t, t'))
    13.8 +       val thm = Goal.prove sg [] [] (Logic.mk_equals (t, t'))
    13.9                     (fn _ => simp_tac (Simplifier.inherit_context ss cancel_ss) 1)
   13.10     in SOME thm end
   13.11     handle Cancel => NONE;
   13.12 @@ -110,7 +110,7 @@
   13.13  
   13.14   fun rel_proc sg ss t =
   13.15     let val t' = cancel sg t
   13.16 -       val thm = Tactic.prove sg [] [] (Logic.mk_equals (t, t'))
   13.17 +       val thm = Goal.prove sg [] [] (Logic.mk_equals (t, t'))
   13.18                     (fn _ => rtac eq_reflection 1 THEN
   13.19                              resolve_tac eqI_rules 1 THEN
   13.20                              simp_tac (Simplifier.inherit_context ss cancel_ss) 1)
    14.1 --- a/src/Provers/Arith/assoc_fold.ML	Fri Oct 21 18:14:32 2005 +0200
    14.2 +++ b/src/Provers/Arith/assoc_fold.ML	Fri Oct 21 18:14:34 2005 +0200
    14.3 @@ -54,7 +54,7 @@
    14.4                 else ()
    14.5         val rhs = plus $ mk_sum plus lits $ mk_sum plus others
    14.6         val _ = if !trace then tracing ("RHS = " ^ show rhs) else ()
    14.7 -       val th = Tactic.prove thy [] [] (Logic.mk_equals (lhs, rhs))
    14.8 +       val th = Goal.prove thy [] [] (Logic.mk_equals (lhs, rhs))
    14.9                     (fn _ => rtac Data.eq_reflection 1 THEN
   14.10                              simp_tac (Simplifier.inherit_context ss assoc_ss) 1)
   14.11     in SOME th end
    15.1 --- a/src/Provers/quantifier1.ML	Fri Oct 21 18:14:32 2005 +0200
    15.2 +++ b/src/Provers/quantifier1.ML	Fri Oct 21 18:14:34 2005 +0200
    15.3 @@ -104,7 +104,7 @@
    15.4    in exqu end;
    15.5  
    15.6  fun prove_conv tac thy tu =
    15.7 -  Tactic.prove thy [] [] (Logic.mk_equals tu) (K (rtac iff_reflection 1 THEN tac));
    15.8 +  Goal.prove thy [] [] (Logic.mk_equals tu) (K (rtac iff_reflection 1 THEN tac));
    15.9  
   15.10  fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i) 
   15.11  
    16.1 --- a/src/Pure/Isar/skip_proof.ML	Fri Oct 21 18:14:32 2005 +0200
    16.2 +++ b/src/Pure/Isar/skip_proof.ML	Fri Oct 21 18:14:34 2005 +0200
    16.3 @@ -35,7 +35,7 @@
    16.4    ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
    16.5  
    16.6  fun prove thy xs asms prop tac =
    16.7 -  Tactic.prove thy xs asms prop
    16.8 +  Goal.prove thy xs asms prop
    16.9      (if ! quick_and_dirty then (K (cheat_tac thy)) else tac);
   16.10  
   16.11  end;
    17.1 --- a/src/Pure/axclass.ML	Fri Oct 21 18:14:32 2005 +0200
    17.2 +++ b/src/Pure/axclass.ML	Fri Oct 21 18:14:34 2005 +0200
    17.3 @@ -272,8 +272,8 @@
    17.4      val (c1, c2) = prep_classrel thy raw_cc;
    17.5      val txt = quote (Sign.string_of_classrel thy [c1, c2]);
    17.6      val _ = message ("Proving class inclusion " ^ txt ^ " ...");
    17.7 -    val th = Tactic.prove thy [] [] (mk_classrel (c1, c2)) (K tac) handle ERROR =>
    17.8 -      error ("The error(s) above occurred while trying to prove " ^ txt);
    17.9 +    val th = Goal.prove thy [] [] (mk_classrel (c1, c2)) (K tac) handle ERROR_MESSAGE msg =>
   17.10 +      error (msg ^ "\nThe error(s) above occurred while trying to prove " ^ txt);
   17.11    in add_classrel_thms [th] thy end;
   17.12  
   17.13  fun ext_inst_arity prep_arity raw_arity tac thy =
   17.14 @@ -282,9 +282,9 @@
   17.15      val txt = quote (Sign.string_of_arity thy arity);
   17.16      val _ = message ("Proving type arity " ^ txt ^ " ...");
   17.17      val props = (mk_arities arity);
   17.18 -    val ths = Tactic.prove_multi thy [] [] props
   17.19 -        (fn _ => Tactic.smart_conjunction_tac (length props) THEN tac)
   17.20 -      handle ERROR => error ("The error(s) above occurred while trying to prove " ^ txt);
   17.21 +    val ths = Goal.prove_multi thy [] [] props
   17.22 +      (fn _ => Tactic.smart_conjunction_tac (length props) THEN tac) handle ERROR_MESSAGE msg =>
   17.23 +        error (msg ^ "\nThe error(s) above occurred while trying to prove " ^ txt);
   17.24    in add_arity_thms ths thy end;
   17.25  
   17.26  in
    18.1 --- a/src/ZF/Datatype.ML	Fri Oct 21 18:14:32 2005 +0200
    18.2 +++ b/src/ZF/Datatype.ML	Fri Oct 21 18:14:34 2005 +0200
    18.3 @@ -87,7 +87,7 @@
    18.4                   writeln ("NEW = " ^ string_of_cterm (Thm.cterm_of sg new))
    18.5                 else ();
    18.6         val goal = Logic.mk_equals (old, new)
    18.7 -       val thm = Tactic.prove sg [] [] goal (fn _ => rtac iff_reflection 1 THEN
    18.8 +       val thm = Goal.prove sg [] [] goal (fn _ => rtac iff_reflection 1 THEN
    18.9             simp_tac (Simplifier.inherit_context ss datatype_ss addsimps #free_iffs lcon_info) 1)
   18.10           handle ERROR_MESSAGE msg =>
   18.11           (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Sign.string_of_term sg goal);
    19.1 --- a/src/ZF/arith_data.ML	Fri Oct 21 18:14:32 2005 +0200
    19.2 +++ b/src/ZF/arith_data.ML	Fri Oct 21 18:14:34 2005 +0200
    19.3 @@ -74,7 +74,7 @@
    19.4    let val hyps' = List.filter (not o is_eq_thm) hyps
    19.5        val goal = Logic.list_implies (map (#prop o Thm.rep_thm) hyps',
    19.6          FOLogic.mk_Trueprop (mk_eq_iff (t, u)));
    19.7 -  in SOME (hyps' MRS Tactic.prove sg xs [] goal (K (EVERY tacs)))
    19.8 +  in SOME (hyps' MRS Goal.prove sg xs [] goal (K (EVERY tacs)))
    19.9        handle ERROR_MESSAGE msg =>
   19.10          (warning (msg ^ "\nCancellation failed: no typing information? (" ^ name ^ ")"); NONE)
   19.11    end;