TFL/post.ML
author wenzelm
Tue Jun 13 23:41:39 2006 +0200 (2006-06-13)
changeset 19876 11d447d5d68c
parent 19736 d8d0f8f51d69
child 19925 3f9341831812
permissions -rw-r--r--
tuned;
     1 (*  Title:      TFL/post.ML
     2     ID:         $Id$
     3     Author:     Konrad Slind, Cambridge University Computer Laboratory
     4     Copyright   1997  University of Cambridge
     5 
     6 Second part of main module (postprocessing of TFL definitions).
     7 *)
     8 
     9 signature TFL =
    10 sig
    11   val trace: bool ref
    12   val quiet_mode: bool ref
    13   val message: string -> unit
    14   val tgoalw: theory -> thm list -> thm list -> thm list
    15   val tgoal: theory -> thm list -> thm list
    16   val define_i: bool -> theory -> claset -> simpset -> thm list -> thm list -> xstring ->
    17     term -> term list -> theory * {rules: (thm * int) list, induct: thm, tcs: term list}
    18   val define: bool -> theory -> claset -> simpset -> thm list -> thm list -> xstring ->
    19     string -> string list -> theory * {rules: (thm * int) list, induct: thm, tcs: term list}
    20   val defer_i: theory -> thm list -> xstring -> term list -> theory * thm
    21   val defer: theory -> thm list -> xstring -> string list -> theory * thm
    22 end;
    23 
    24 structure Tfl: TFL =
    25 struct
    26 
    27 structure S = USyntax
    28 
    29 
    30 (* messages *)
    31 
    32 val trace = Prim.trace
    33 
    34 val quiet_mode = ref false;
    35 fun message s = if ! quiet_mode then () else writeln s;
    36 
    37 
    38 (* misc *)
    39 
    40 (*---------------------------------------------------------------------------
    41  * Extract termination goals so that they can be put it into a goalstack, or
    42  * have a tactic directly applied to them.
    43  *--------------------------------------------------------------------------*)
    44 fun termination_goals rules =
    45     map (Type.freeze o HOLogic.dest_Trueprop)
    46       (foldr (fn (th,A) => gen_union (op aconv) (prems_of th, A)) [] rules);
    47 
    48 (*---------------------------------------------------------------------------
    49  * Finds the termination conditions in (highly massaged) definition and
    50  * puts them into a goalstack.
    51  *--------------------------------------------------------------------------*)
    52 fun tgoalw thy defs rules =
    53   case termination_goals rules of
    54       [] => error "tgoalw: no termination conditions to prove"
    55     | L  => OldGoals.goalw_cterm defs
    56               (Thm.cterm_of (Theory.sign_of thy)
    57                         (HOLogic.mk_Trueprop(USyntax.list_mk_conj L)));
    58 
    59 fun tgoal thy = tgoalw thy [];
    60 
    61 (*---------------------------------------------------------------------------
    62  * Three postprocessors are applied to the definition.  It
    63  * attempts to prove wellfoundedness of the given relation, simplifies the
    64  * non-proved termination conditions, and finally attempts to prove the
    65  * simplified termination conditions.
    66  *--------------------------------------------------------------------------*)
    67 fun std_postprocessor strict cs ss wfs =
    68   Prim.postprocess strict
    69    {wf_tac     = REPEAT (ares_tac wfs 1),
    70     terminator = asm_simp_tac ss 1
    71                  THEN TRY (silent_arith_tac 1 ORELSE
    72                            fast_tac (cs addSDs [not0_implies_Suc] addss ss) 1),
    73     simplifier = Rules.simpl_conv ss []};
    74 
    75 
    76 
    77 val concl = #2 o Rules.dest_thm;
    78 
    79 (*---------------------------------------------------------------------------
    80  * Postprocess a definition made by "define". This is a separate stage of
    81  * processing from the definition stage.
    82  *---------------------------------------------------------------------------*)
    83 local
    84 structure R = Rules
    85 structure U = Utils
    86 
    87 (* The rest of these local definitions are for the tricky nested case *)
    88 val solved = not o can S.dest_eq o #2 o S.strip_forall o concl
    89 
    90 fun id_thm th =
    91    let val {lhs,rhs} = S.dest_eq (#2 (S.strip_forall (#2 (R.dest_thm th))));
    92    in lhs aconv rhs end
    93    handle U.ERR _ => false;
    94    
    95 
    96 fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
    97 val P_imp_P_iff_True = prover "P --> (P= True)" RS mp;
    98 val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection;
    99 fun mk_meta_eq r = case concl_of r of
   100      Const("==",_)$_$_ => r
   101   |   _ $(Const("op =",_)$_$_) => r RS eq_reflection
   102   |   _ => r RS P_imp_P_eq_True
   103 
   104 (*Is this the best way to invoke the simplifier??*)
   105 fun rewrite L = rewrite_rule (map mk_meta_eq (List.filter(not o id_thm) L))
   106 
   107 fun join_assums th =
   108   let val {sign,...} = rep_thm th
   109       val tych = cterm_of sign
   110       val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th)))
   111       val cntxtl = (#1 o S.strip_imp) lhs  (* cntxtl should = cntxtr *)
   112       val cntxtr = (#1 o S.strip_imp) rhs  (* but union is solider *)
   113       val cntxt = gen_union (op aconv) (cntxtl, cntxtr)
   114   in
   115     R.GEN_ALL
   116       (R.DISCH_ALL
   117          (rewrite (map (R.ASSUME o tych) cntxt) (R.SPEC_ALL th)))
   118   end
   119   val gen_all = S.gen_all
   120 in
   121 fun proof_stage strict cs ss wfs theory {f, R, rules, full_pats_TCs, TCs} =
   122   let
   123     val _ = message "Proving induction theorem ..."
   124     val ind = Prim.mk_induction theory {fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs}
   125     val _ = message "Postprocessing ...";
   126     val {rules, induction, nested_tcs} =
   127       std_postprocessor strict cs ss wfs theory {rules=rules, induction=ind, TCs=TCs}
   128   in
   129   case nested_tcs
   130   of [] => {induction=induction, rules=rules,tcs=[]}
   131   | L  => let val dummy = message "Simplifying nested TCs ..."
   132               val (solved,simplified,stubborn) =
   133                fold_rev (fn th => fn (So,Si,St) =>
   134                      if (id_thm th) then (So, Si, th::St) else
   135                      if (solved th) then (th::So, Si, St)
   136                      else (So, th::Si, St)) nested_tcs ([],[],[])
   137               val simplified' = map join_assums simplified
   138               val dummy = (Prim.trace_thms "solved =" solved;
   139                            Prim.trace_thms "simplified' =" simplified')
   140               val rewr = full_simplify (ss addsimps (solved @ simplified'));
   141               val dummy = Prim.trace_thms "Simplifying the induction rule..."
   142                                           [induction]
   143               val induction' = rewr induction
   144               val dummy = Prim.trace_thms "Simplifying the recursion rules..."
   145                                           [rules]
   146               val rules'     = rewr rules
   147               val _ = message "... Postprocessing finished";
   148           in
   149           {induction = induction',
   150                rules = rules',
   151                  tcs = map (gen_all o S.rhs o #2 o S.strip_forall o concl)
   152                            (simplified@stubborn)}
   153           end
   154   end;
   155 
   156 
   157 (*lcp: curry the predicate of the induction rule*)
   158 fun curry_rule rl =
   159   SplitRule.split_rule_var (Term.head_of (HOLogic.dest_Trueprop (concl_of rl))) rl;
   160 
   161 (*lcp: put a theorem into Isabelle form, using meta-level connectives*)
   162 val meta_outer =
   163   curry_rule o standard o
   164   rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE)));
   165 
   166 (*Strip off the outer !P*)
   167 val spec'= read_instantiate [("x","P::?'b=>bool")] spec;
   168 
   169 fun tracing true _ = ()
   170   | tracing false msg = writeln msg;
   171 
   172 fun simplify_defn strict thy cs ss congs wfs id pats def0 =
   173    let val def = Thm.freezeT def0 RS meta_eq_to_obj_eq
   174        val {theory,rules,rows,TCs,full_pats_TCs} =
   175            Prim.post_definition congs (thy, (def,pats))
   176        val {lhs=f,rhs} = S.dest_eq (concl def)
   177        val (_,[R,_]) = S.strip_comb rhs
   178        val dummy = Prim.trace_thms "congs =" congs
   179        (*the next step has caused simplifier looping in some cases*)
   180        val {induction, rules, tcs} =
   181              proof_stage strict cs ss wfs theory
   182                {f = f, R = R, rules = rules,
   183                 full_pats_TCs = full_pats_TCs,
   184                 TCs = TCs}
   185        val rules' = map (standard o ObjectLogic.rulify_no_asm)
   186                         (R.CONJUNCTS rules)
   187          in  {induct = meta_outer (ObjectLogic.rulify_no_asm (induction RS spec')),
   188         rules = ListPair.zip(rules', rows),
   189         tcs = (termination_goals rules') @ tcs}
   190    end
   191   handle U.ERR {mesg,func,module} =>
   192                error (mesg ^
   193                       "\n    (In TFL function " ^ module ^ "." ^ func ^ ")");
   194 
   195 
   196 (* Derive the initial equations from the case-split rules to meet the
   197 users specification of the recursive function. 
   198  Note: We don't do this if the wf conditions fail to be solved, as each
   199 case may have a different wf condition. We could group the conditions
   200 together and say that they must be true to solve the general case,
   201 but that would hide from the user which sub-case they were related
   202 to. Probably this is not important, and it would work fine, but, for now, I
   203 prefer leaving more fine-grain control to the user. 
   204 -- Lucas Dixon, Aug 2004 *)
   205 local
   206   fun get_related_thms i = 
   207       List.mapPartial ((fn (r,x) => if x = i then SOME r else NONE));
   208 
   209   fun solve_eq (th, [], i) = 
   210         error "derive_init_eqs: missing rules"
   211     | solve_eq (th, [a], i) = [(a, i)]
   212     | solve_eq (th, splitths as (_ :: _), i) = 
   213       (writeln "Proving unsplit equation...";
   214       [((standard o ObjectLogic.rulify_no_asm)
   215           (CaseSplit.splitto splitths th), i)])
   216       (* if there's an error, pretend nothing happened with this definition 
   217          We should probably print something out so that the user knows...? *)
   218       handle ERROR s => 
   219              (warning ("recdef (solve_eq): " ^ s); map (fn x => (x,i)) splitths);
   220 in
   221 fun derive_init_eqs sgn rules eqs = 
   222     let 
   223       val eqths = map (Thm.trivial o (Thm.cterm_of sgn) o HOLogic.mk_Trueprop) 
   224                       eqs
   225       fun countlist l = 
   226           (rev o snd o (Library.foldl (fn ((i,L), e) => (i + 1,(e,i) :: L)))) ((0,[]), l)
   227     in
   228       List.concat (map (fn (e,i) => solve_eq (e, (get_related_thms i rules), i))
   229                 (countlist eqths))
   230     end;
   231 end;
   232 
   233 
   234 (*---------------------------------------------------------------------------
   235  * Defining a function with an associated termination relation.
   236  *---------------------------------------------------------------------------*)
   237 fun define_i strict thy cs ss congs wfs fid R eqs =
   238   let val {functional,pats} = Prim.mk_functional thy eqs
   239       val (thy, def) = Prim.wfrec_definition0 thy (Sign.base_name fid) R functional
   240       val {induct, rules, tcs} = 
   241           simplify_defn strict thy cs ss congs wfs fid pats def
   242       val rules' = 
   243           if strict then derive_init_eqs (Theory.sign_of thy) rules eqs
   244           else rules
   245   in (thy, {rules = rules', induct = induct, tcs = tcs}) end;
   246 
   247 fun define strict thy cs ss congs wfs fid R seqs =
   248   define_i strict thy cs ss congs wfs fid (Sign.read_term thy R) (map (Sign.read_term thy) seqs)
   249     handle U.ERR {mesg,...} => error mesg;
   250 
   251 
   252 (*---------------------------------------------------------------------------
   253  *
   254  *     Definitions with synthesized termination relation
   255  *
   256  *---------------------------------------------------------------------------*)
   257 
   258 fun func_of_cond_eqn tm =
   259   #1 (S.strip_comb (#lhs (S.dest_eq (#2 (S.strip_forall (#2 (S.strip_imp tm)))))));
   260 
   261 fun defer_i thy congs fid eqs =
   262  let val {rules,R,theory,full_pats_TCs,SV,...} =
   263              Prim.lazyR_def thy (Sign.base_name fid) congs eqs
   264      val f = func_of_cond_eqn (concl (R.CONJUNCT1 rules handle U.ERR _ => rules));
   265      val dummy = message "Proving induction theorem ...";
   266      val induction = Prim.mk_induction theory
   267                         {fconst=f, R=R, SV=SV, pat_TCs_list=full_pats_TCs}
   268  in (theory,
   269      (*return the conjoined induction rule and recursion equations,
   270        with assumptions remaining to discharge*)
   271      standard (induction RS (rules RS conjI)))
   272  end
   273 
   274 fun defer thy congs fid seqs =
   275   defer_i thy congs fid (map (Sign.read_term thy) seqs)
   276     handle U.ERR {mesg,...} => error mesg;
   277 end;
   278 
   279 end;