prove: ``strict'' argument;
authorwenzelm
Fri Sep 28 19:23:35 2001 +0200 (2001-09-28)
changeset 116326fc8de600f58
parent 11631 b325c05709d3
child 11633 c8945e0dc00b
prove: ``strict'' argument;
TFL/post.ML
TFL/rules.ML
TFL/tfl.ML
     1.1 --- a/TFL/post.ML	Fri Sep 28 19:23:07 2001 +0200
     1.2 +++ b/TFL/post.ML	Fri Sep 28 19:23:35 2001 +0200
     1.3 @@ -13,12 +13,9 @@
     1.4    val message: string -> unit
     1.5    val tgoalw: theory -> thm list -> thm list -> thm list
     1.6    val tgoal: theory -> thm list -> thm list
     1.7 -  val std_postprocessor: claset -> simpset -> thm list -> theory ->
     1.8 -    {induction: thm, rules: thm, TCs: term list list} ->
     1.9 -    {induction: thm, rules: thm, nested_tcs: thm list}
    1.10 -  val define_i: theory -> claset -> simpset -> thm list -> thm list -> xstring ->
    1.11 +  val define_i: bool -> theory -> claset -> simpset -> thm list -> thm list -> xstring ->
    1.12      term -> term list -> theory * {rules: (thm * int) list, induct: thm, tcs: term list}
    1.13 -  val define: theory -> claset -> simpset -> thm list -> thm list -> xstring ->
    1.14 +  val define: bool -> theory -> claset -> simpset -> thm list -> thm list -> xstring ->
    1.15      string -> string list -> theory * {rules: (thm * int) list, induct: thm, tcs: term list}
    1.16    val defer_i: theory -> thm list -> xstring -> term list -> theory * thm
    1.17    val defer: theory -> thm list -> xstring -> string list -> theory * thm
    1.18 @@ -70,8 +67,8 @@
    1.19   * non-proved termination conditions, and finally attempts to prove the
    1.20   * simplified termination conditions.
    1.21   *--------------------------------------------------------------------------*)
    1.22 -fun std_postprocessor cs ss wfs =
    1.23 -  Prim.postprocess
    1.24 +fun std_postprocessor strict cs ss wfs =
    1.25 +  Prim.postprocess strict
    1.26     {wf_tac     = REPEAT (ares_tac wfs 1),
    1.27      terminator = asm_simp_tac ss 1
    1.28                   THEN TRY (fast_tac (cs addSDs [not0_implies_Suc] addss ss) 1),
    1.29 @@ -123,13 +120,13 @@
    1.30    end
    1.31    val gen_all = S.gen_all
    1.32  in
    1.33 -fun proof_stage cs ss wfs theory {f, R, rules, full_pats_TCs, TCs} =
    1.34 +fun proof_stage strict cs ss wfs theory {f, R, rules, full_pats_TCs, TCs} =
    1.35    let
    1.36      val _ = message "Proving induction theorem ..."
    1.37      val ind = Prim.mk_induction theory {fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs}
    1.38      val _ = message "Postprocessing ...";
    1.39      val {rules, induction, nested_tcs} =
    1.40 -      std_postprocessor cs ss wfs theory {rules=rules, induction=ind, TCs=TCs}
    1.41 +      std_postprocessor strict cs ss wfs theory {rules=rules, induction=ind, TCs=TCs}
    1.42    in
    1.43    case nested_tcs
    1.44    of [] => {induction=induction, rules=rules,tcs=[]}
    1.45 @@ -164,13 +161,13 @@
    1.46  (*Strip off the outer !P*)
    1.47  val spec'= read_instantiate [("x","P::?'b=>bool")] spec;
    1.48  
    1.49 -fun simplify_defn thy cs ss congs wfs id pats def0 =
    1.50 +fun simplify_defn strict thy cs ss congs wfs id pats def0 =
    1.51     let val def = freezeT def0 RS meta_eq_to_obj_eq
    1.52         val {theory,rules,rows,TCs,full_pats_TCs} = Prim.post_definition congs (thy, (def,pats))
    1.53         val {lhs=f,rhs} = S.dest_eq (concl def)
    1.54         val (_,[R,_]) = S.strip_comb rhs
    1.55         val {induction, rules, tcs} =
    1.56 -             proof_stage cs ss wfs theory
    1.57 +             proof_stage strict cs ss wfs theory
    1.58                 {f = f, R = R, rules = rules,
    1.59                  full_pats_TCs = full_pats_TCs,
    1.60                  TCs = TCs}
    1.61 @@ -186,13 +183,13 @@
    1.62  (*---------------------------------------------------------------------------
    1.63   * Defining a function with an associated termination relation.
    1.64   *---------------------------------------------------------------------------*)
    1.65 -fun define_i thy cs ss congs wfs fid R eqs =
    1.66 +fun define_i strict thy cs ss congs wfs fid R eqs =
    1.67    let val {functional,pats} = Prim.mk_functional thy eqs
    1.68        val (thy, def) = Prim.wfrec_definition0 thy (Sign.base_name fid) R functional
    1.69 -  in (thy, simplify_defn thy cs ss congs wfs fid pats def) end;
    1.70 +  in (thy, simplify_defn strict thy cs ss congs wfs fid pats def) end;
    1.71  
    1.72 -fun define thy cs ss congs wfs fid R seqs =
    1.73 -  define_i thy cs ss congs wfs fid (read_term thy R) (map (read_term thy) seqs)
    1.74 +fun define strict thy cs ss congs wfs fid R seqs =
    1.75 +  define_i strict thy cs ss congs wfs fid (read_term thy R) (map (read_term thy) seqs)
    1.76      handle U.ERR {mesg,...} => error mesg;
    1.77  
    1.78  
     2.1 --- a/TFL/rules.ML	Fri Sep 28 19:23:07 2001 +0200
     2.2 +++ b/TFL/rules.ML	Fri Sep 28 19:23:35 2001 +0200
     2.3 @@ -57,7 +57,7 @@
     2.4                               -> thm -> thm * term list
     2.5    val RIGHT_ASSOC : thm -> thm
     2.6  
     2.7 -  val prove : cterm * tactic -> thm
     2.8 +  val prove : bool -> cterm * tactic -> thm
     2.9  end;
    2.10  
    2.11  structure Rules: RULES =
    2.12 @@ -813,11 +813,13 @@
    2.13   end;
    2.14  
    2.15  
    2.16 -fun prove (ptm, tac) =
    2.17 +fun prove strict (ptm, tac) =
    2.18    let val result =
    2.19 -    Library.transform_error (fn () =>
    2.20 -      Goals.prove_goalw_cterm [] ptm (fn _ => [tac])) ()
    2.21 -    handle ERROR_MESSAGE msg => (warning msg; raise RULES_ERR "prove" msg)
    2.22 +    if strict then Goals.prove_goalw_cterm [] ptm (fn _ => [tac])
    2.23 +    else
    2.24 +      Library.transform_error (fn () =>
    2.25 +        Goals.prove_goalw_cterm [] ptm (fn _ => [tac])) ()
    2.26 +      handle ERROR_MESSAGE msg => (warning msg; raise RULES_ERR "prove" msg);
    2.27    in #1 (freeze_thaw result) end;
    2.28  
    2.29  
     3.1 --- a/TFL/tfl.ML	Fri Sep 28 19:23:07 2001 +0200
     3.2 +++ b/TFL/tfl.ML	Fri Sep 28 19:23:35 2001 +0200
     3.3 @@ -33,9 +33,9 @@
     3.4      patterns : pattern list}
     3.5    val mk_induction: theory ->
     3.6      {fconst: term, R: term, SV: term list, pat_TCs_list: (term * term list) list} -> thm
     3.7 -  val postprocess: {wf_tac: tactic, terminator: tactic, simplifier: cterm -> thm} -> theory ->
     3.8 -    {rules: thm, induction: thm, TCs: term list list} ->
     3.9 -    {rules: thm, induction: thm, nested_tcs: thm list}
    3.10 +  val postprocess: bool -> {wf_tac: tactic, terminator: tactic, simplifier: cterm -> thm}
    3.11 +    -> theory -> {rules: thm, induction: thm, TCs: term list list}
    3.12 +    -> {rules: thm, induction: thm, nested_tcs: thm list}
    3.13  end;
    3.14  
    3.15  structure Prim: PRIM =
    3.16 @@ -909,14 +909,15 @@
    3.17     (R.MP rule tcthm, R.PROVE_HYP tcthm induction)
    3.18  
    3.19  
    3.20 -fun postprocess{wf_tac, terminator, simplifier} theory {rules,induction,TCs} =
    3.21 +fun postprocess strict {wf_tac, terminator, simplifier} theory {rules,induction,TCs} =
    3.22  let val tych = Thry.typecheck theory
    3.23 +    val prove = R.prove strict;
    3.24  
    3.25     (*---------------------------------------------------------------------
    3.26      * Attempt to eliminate WF condition. It's the only assumption of rules
    3.27      *---------------------------------------------------------------------*)
    3.28     val (rules1,induction1)  =
    3.29 -       let val thm = R.prove(tych(HOLogic.mk_Trueprop
    3.30 +       let val thm = prove(tych(HOLogic.mk_Trueprop
    3.31                                    (hd(#1(R.dest_thm rules)))),
    3.32                               wf_tac)
    3.33         in (R.PROVE_HYP thm rules,  R.PROVE_HYP thm induction)
    3.34 @@ -948,7 +949,7 @@
    3.35         elim_tc (R.MATCH_MP Thms.eqT tc_eq) (r,ind)
    3.36         handle U.ERR _ =>
    3.37          (elim_tc (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq)
    3.38 -                  (R.prove(tych(HOLogic.mk_Trueprop(S.rhs(concl tc_eq))),
    3.39 +                  (prove(tych(HOLogic.mk_Trueprop(S.rhs(concl tc_eq))),
    3.40                             terminator)))
    3.41                   (r,ind)
    3.42           handle U.ERR _ =>
    3.43 @@ -976,7 +977,7 @@
    3.44         (R.MATCH_MP Thms.eqT tc_eq
    3.45          handle U.ERR _ =>
    3.46            (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq)
    3.47 -                      (R.prove(tych(HOLogic.mk_Trueprop (S.rhs(concl tc_eq))),
    3.48 +                      (prove(tych(HOLogic.mk_Trueprop (S.rhs(concl tc_eq))),
    3.49                                 terminator))
    3.50              handle U.ERR _ => tc_eq))
    3.51        end