TFL/post.ML

lucas - fixed bug with name capture variables bound outside redex could (previously)conflict with scheme variables that occur in the conditions of an equation, and which were renamed to avoid conflict with another instantiation. This has now been fixed.

(*  Title:      TFL/post.ML
    ID:         $Id$
    Author:     Konrad Slind, Cambridge University Computer Laboratory
    Copyright   1997  University of Cambridge

Second part of main module (postprocessing of TFL definitions).
*)

signature TFL =
sig
  val trace: bool ref
  val quiet_mode: bool ref
  val message: string -> unit
  val tgoalw: theory -> thm list -> thm list -> thm list
  val tgoal: theory -> thm list -> thm list
  val define_i: bool -> theory -> claset -> simpset -> thm list -> thm list -> xstring ->
    term -> term list -> theory * {rules: (thm * int) list, induct: thm, tcs: term list}
  val define: bool -> theory -> claset -> simpset -> thm list -> thm list -> xstring ->
    string -> string list -> theory * {rules: (thm * int) list, induct: thm, tcs: term list}
  val defer_i: theory -> thm list -> xstring -> term list -> theory * thm
  val defer: theory -> thm list -> xstring -> string list -> theory * thm
end;

structure Tfl: TFL =
struct

structure S = USyntax


(* messages *)

val trace = Prim.trace

val quiet_mode = ref false;
fun message s = if ! quiet_mode then () else writeln s;


(* misc *)

val read_term = Thm.term_of oo (HOLogic.read_cterm o Theory.sign_of);


(*---------------------------------------------------------------------------
 * Extract termination goals so that they can be put it into a goalstack, or
 * have a tactic directly applied to them.
 *--------------------------------------------------------------------------*)
fun termination_goals rules =
    map (#1 o Type.freeze_thaw o HOLogic.dest_Trueprop)
      (foldr (fn (th,A) => union_term (prems_of th, A)) (rules, []));

(*---------------------------------------------------------------------------
 * Finds the termination conditions in (highly massaged) definition and
 * puts them into a goalstack.
 *--------------------------------------------------------------------------*)
fun tgoalw thy defs rules =
  case termination_goals rules of
      [] => error "tgoalw: no termination conditions to prove"
    | L  => goalw_cterm defs
              (Thm.cterm_of (Theory.sign_of thy)
                        (HOLogic.mk_Trueprop(USyntax.list_mk_conj L)));

fun tgoal thy = tgoalw thy [];

(*---------------------------------------------------------------------------
 * Three postprocessors are applied to the definition.  It
 * attempts to prove wellfoundedness of the given relation, simplifies the
 * non-proved termination conditions, and finally attempts to prove the
 * simplified termination conditions.
 *--------------------------------------------------------------------------*)
fun std_postprocessor strict cs ss wfs =
  Prim.postprocess strict
   {wf_tac     = REPEAT (ares_tac wfs 1),
    terminator = asm_simp_tac ss 1
                 THEN TRY (silent_arith_tac 1 ORELSE
                           fast_tac (cs addSDs [not0_implies_Suc] addss ss) 1),
    simplifier = Rules.simpl_conv ss []};



val concl = #2 o Rules.dest_thm;

(*---------------------------------------------------------------------------
 * Postprocess a definition made by "define". This is a separate stage of
 * processing from the definition stage.
 *---------------------------------------------------------------------------*)
local
structure R = Rules
structure U = Utils

(* The rest of these local definitions are for the tricky nested case *)
val solved = not o can S.dest_eq o #2 o S.strip_forall o concl

fun id_thm th =
   let val {lhs,rhs} = S.dest_eq (#2 (S.strip_forall (#2 (R.dest_thm th))));
   in lhs aconv rhs end
   handle U.ERR _ => false;
   

fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
val P_imp_P_iff_True = prover "P --> (P= True)" RS mp;
val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection;
fun mk_meta_eq r = case concl_of r of
     Const("==",_)$_$_ => r
  |   _ $(Const("op =",_)$_$_) => r RS eq_reflection
  |   _ => r RS P_imp_P_eq_True

(*Is this the best way to invoke the simplifier??*)
fun rewrite L = rewrite_rule (map mk_meta_eq (filter(not o id_thm) L))

fun join_assums th =
  let val {sign,...} = rep_thm th
      val tych = cterm_of sign
      val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th)))
      val cntxtl = (#1 o S.strip_imp) lhs  (* cntxtl should = cntxtr *)
      val cntxtr = (#1 o S.strip_imp) rhs  (* but union is solider *)
      val cntxt = gen_union (op aconv) (cntxtl, cntxtr)
  in
    R.GEN_ALL
      (R.DISCH_ALL
         (rewrite (map (R.ASSUME o tych) cntxt) (R.SPEC_ALL th)))
  end
  val gen_all = S.gen_all
in
fun proof_stage strict cs ss wfs theory {f, R, rules, full_pats_TCs, TCs} =
  let
    val _ = message "Proving induction theorem ..."
    val ind = Prim.mk_induction theory {fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs}
    val _ = message "Postprocessing ...";
    val {rules, induction, nested_tcs} =
      std_postprocessor strict cs ss wfs theory {rules=rules, induction=ind, TCs=TCs}
  in
  case nested_tcs
  of [] => {induction=induction, rules=rules,tcs=[]}
  | L  => let val dummy = message "Simplifying nested TCs ..."
              val (solved,simplified,stubborn) =
               U.itlist (fn th => fn (So,Si,St) =>
                     if (id_thm th) then (So, Si, th::St) else
                     if (solved th) then (th::So, Si, St)
                     else (So, th::Si, St)) nested_tcs ([],[],[])
              val simplified' = map join_assums simplified
              val dummy = (Prim.trace_thms "solved =" solved;
                           Prim.trace_thms "simplified' =" simplified')
              val rewr = full_simplify (ss addsimps (solved @ simplified'));
              val dummy = Prim.trace_thms "Simplifying the induction rule..."
                                          [induction]
              val induction' = rewr induction
              val dummy = Prim.trace_thms "Simplifying the recursion rules..."
                                          [rules]
              val rules'     = rewr rules
              val _ = message "... Postprocessing finished";
          in
          {induction = induction',
               rules = rules',
                 tcs = map (gen_all o S.rhs o #2 o S.strip_forall o concl)
                           (simplified@stubborn)}
          end
  end;


(*lcp: curry the predicate of the induction rule*)
fun curry_rule rl =
  SplitRule.split_rule_var (Term.head_of (HOLogic.dest_Trueprop (concl_of rl)), rl);

(*lcp: put a theorem into Isabelle form, using meta-level connectives*)
val meta_outer =
  curry_rule o standard o
  rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE)));

(*Strip off the outer !P*)
val spec'= read_instantiate [("x","P::?'b=>bool")] spec;

fun tracing true _ = ()
  | tracing false msg = writeln msg;

fun simplify_defn strict thy cs ss congs wfs id pats def0 =
   let val def = freezeT def0 RS meta_eq_to_obj_eq
       val {theory,rules,rows,TCs,full_pats_TCs} =
           Prim.post_definition congs (thy, (def,pats))
       val {lhs=f,rhs} = S.dest_eq (concl def)
       val (_,[R,_]) = S.strip_comb rhs
       val dummy = Prim.trace_thms "congs =" congs
       (*the next step has caused simplifier looping in some cases*)
       val {induction, rules, tcs} =
             proof_stage strict cs ss wfs theory
               {f = f, R = R, rules = rules,
                full_pats_TCs = full_pats_TCs,
                TCs = TCs}
       val rules' = map (standard o ObjectLogic.rulify_no_asm)
                        (R.CONJUNCTS rules)
         in  {induct = meta_outer (ObjectLogic.rulify_no_asm (induction RS spec')),
        rules = ListPair.zip(rules', rows),
        tcs = (termination_goals rules') @ tcs}
   end
  handle U.ERR {mesg,func,module} =>
               error (mesg ^
                      "\n    (In TFL function " ^ module ^ "." ^ func ^ ")");


(* Derive the initial equations from the case-split rules to meet the
users specification of the recursive function. 
 Note: We don't do this if the wf conditions fail to be solved, as each
case may have a different wf condition. We could group the conditions
together and say that they must be true to solve the general case,
but that would hide from the user which sub-case they were related
to. Probably this is not important, and it would work fine, but, for now, I
prefer leaving more fine-grain control to the user. 
-- Lucas Dixon, Aug 2004 *)
local
  fun get_related_thms i = 
      mapfilter ((fn (r,x) => if x = i then SOME r else NONE));

  fun solve_eq (th, [], i) = 
      raise ERROR_MESSAGE "derive_init_eqs: missing rules"
    | solve_eq (th, [a], i) = [(a, i)]
    | solve_eq (th, splitths as (_ :: _), i) = 
      (writeln "Proving unsplit equation...";
      [((standard o ObjectLogic.rulify_no_asm)
          (CaseSplit.splitto splitths th), i)])
      (* if there's an error, pretend nothing happened with this definition 
         We should probably print something out so that the user knows...? *)
      handle ERROR_MESSAGE s => 
             (writeln ("WARNING:post.ML:solve_eq: " ^ s); map (fn x => (x,i)) splitths); 
in
fun derive_init_eqs sgn rules eqs = 
    let 
      val eqths = map (Thm.trivial o (Thm.cterm_of sgn) o HOLogic.mk_Trueprop) 
                      eqs
      fun countlist l = 
          (rev o snd o (foldl (fn ((i,L), e) => (i + 1,(e,i) :: L)))) ((0,[]), l)
    in
      flat (map (fn (e,i) => solve_eq (e, (get_related_thms i rules), i))
                (countlist eqths))
    end;
end;


(*---------------------------------------------------------------------------
 * Defining a function with an associated termination relation.
 *---------------------------------------------------------------------------*)
fun define_i strict thy cs ss congs wfs fid R eqs =
  let val {functional,pats} = Prim.mk_functional thy eqs
      val (thy, def) = Prim.wfrec_definition0 thy (Sign.base_name fid) R functional
      val {induct, rules, tcs} = 
          simplify_defn strict thy cs ss congs wfs fid pats def
      val rules' = 
          if strict then derive_init_eqs (Theory.sign_of thy) rules eqs
          else rules
  in (thy, {rules = rules', induct = induct, tcs = tcs}) end;

fun define strict thy cs ss congs wfs fid R seqs =
  define_i strict thy cs ss congs wfs fid (read_term thy R) (map (read_term thy) seqs)
    handle U.ERR {mesg,...} => error mesg;


(*---------------------------------------------------------------------------
 *
 *     Definitions with synthesized termination relation
 *
 *---------------------------------------------------------------------------*)

fun func_of_cond_eqn tm =
  #1 (S.strip_comb (#lhs (S.dest_eq (#2 (S.strip_forall (#2 (S.strip_imp tm)))))));

fun defer_i thy congs fid eqs =
 let val {rules,R,theory,full_pats_TCs,SV,...} =
             Prim.lazyR_def thy (Sign.base_name fid) congs eqs
     val f = func_of_cond_eqn (concl (R.CONJUNCT1 rules handle U.ERR _ => rules));
     val dummy = message "Proving induction theorem ...";
     val induction = Prim.mk_induction theory
                        {fconst=f, R=R, SV=SV, pat_TCs_list=full_pats_TCs}
 in (theory,
     (*return the conjoined induction rule and recursion equations,
       with assumptions remaining to discharge*)
     standard (induction RS (rules RS conjI)))
 end

fun defer thy congs fid seqs =
  defer_i thy congs fid (map (read_term thy) seqs)
    handle U.ERR {mesg,...} => error mesg;
end;

end;