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