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