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