TFL/post.sml
author paulson
Thu May 15 12:29:59 1997 +0200 (1997-05-15)
changeset 3191 14bd6e5985f1
parent 2467 357adb429fda
child 3208 8336393de482
permissions -rw-r--r--
TFL now integrated with HOL (more work needed)
paulson@3191
     1
signature TFL = 
paulson@3191
     2
  sig
paulson@2112
     3
   structure Prim : TFL_sig
paulson@2112
     4
paulson@3191
     5
   val tgoalw : theory -> thm list -> thm list -> thm list
paulson@3191
     6
   val tgoal: theory -> thm list -> thm list
paulson@2112
     7
paulson@2112
     8
   val WF_TAC : thm list -> tactic
paulson@2112
     9
paulson@2112
    10
   val simplifier : thm -> thm
paulson@2112
    11
   val std_postprocessor : theory 
paulson@2112
    12
                           -> {induction:thm, rules:thm, TCs:term list list} 
paulson@2112
    13
                           -> {induction:thm, rules:thm, nested_tcs:thm list}
paulson@2112
    14
paulson@3191
    15
   val define_i : theory -> term -> term -> theory * (thm * Prim.pattern list)
paulson@3191
    16
   val define   : theory -> string -> string list -> theory * Prim.pattern list
paulson@2112
    17
paulson@3191
    18
   val simplify_defn : theory * (string * Prim.pattern list)
paulson@3191
    19
                        -> {rules:thm list, induct:thm, tcs:term list}
paulson@2112
    20
paulson@3191
    21
  (*-------------------------------------------------------------------------
paulson@3191
    22
       val function : theory -> term -> {theory:theory, eq_ind : thm}
paulson@3191
    23
       val lazyR_def: theory -> term -> {theory:theory, eqns : thm}
paulson@3191
    24
   *-------------------------------------------------------------------------*)
paulson@2112
    25
paulson@2112
    26
   val tflcongs : theory -> thm list
paulson@2112
    27
paulson@3191
    28
  end;
paulson@3191
    29
paulson@3191
    30
paulson@3191
    31
structure Tfl: TFL =
paulson@2112
    32
struct
paulson@2112
    33
 structure Prim = Prim
paulson@3191
    34
 structure S = Prim.USyntax
paulson@2112
    35
paulson@3191
    36
(*---------------------------------------------------------------------------
paulson@3191
    37
 * Extract termination goals so that they can be put it into a goalstack, or 
paulson@3191
    38
 * have a tactic directly applied to them.
paulson@3191
    39
 *--------------------------------------------------------------------------*)
paulson@3191
    40
fun termination_goals rules = 
paulson@3191
    41
    map (Logic.freeze_vars o S.drop_Trueprop)
paulson@3191
    42
      (foldr (fn (th,A) => union_term (prems_of th, A)) (rules, []));
paulson@3191
    43
paulson@3191
    44
 (*---------------------------------------------------------------------------
paulson@3191
    45
  * Finds the termination conditions in (highly massaged) definition and 
paulson@3191
    46
  * puts them into a goalstack.
paulson@3191
    47
  *--------------------------------------------------------------------------*)
paulson@3191
    48
 fun tgoalw thy defs rules = 
paulson@3191
    49
    let val L = termination_goals rules
paulson@2112
    50
        open USyntax
paulson@2112
    51
        val g = cterm_of (sign_of thy) (mk_prop(list_mk_conj L))
paulson@2112
    52
    in goalw_cterm defs g
paulson@2112
    53
    end;
paulson@2112
    54
paulson@2112
    55
 val tgoal = Utils.C tgoalw [];
paulson@2112
    56
paulson@3191
    57
 (*---------------------------------------------------------------------------
paulson@3191
    58
  * Simple wellfoundedness prover.
paulson@3191
    59
  *--------------------------------------------------------------------------*)
paulson@2112
    60
 fun WF_TAC thms = REPEAT(FIRST1(map rtac thms))
paulson@2112
    61
 val WFtac = WF_TAC[wf_measure, wf_inv_image, wf_lex_prod, 
paulson@2112
    62
                    wf_pred_nat, wf_pred_list, wf_trancl];
paulson@2112
    63
paulson@2112
    64
 val terminator = simp_tac(HOL_ss addsimps[pred_nat_def,pred_list_def,
paulson@2112
    65
                                           fst_conv,snd_conv,
paulson@2112
    66
                                           mem_Collect_eq,lessI]) 1
paulson@2112
    67
                  THEN TRY(fast_tac set_cs 1);
paulson@2112
    68
paulson@3191
    69
val length_Cons = prove_goal List.thy "length(h#t) = Suc(length t)" 
paulson@3191
    70
    (fn _ => [Simp_tac 1]);
paulson@3191
    71
paulson@2112
    72
 val simpls = [less_eq RS eq_reflection,
paulson@2112
    73
               lex_prod_def, measure_def, inv_image_def, 
paulson@2112
    74
               fst_conv RS eq_reflection, snd_conv RS eq_reflection,
paulson@3191
    75
               mem_Collect_eq RS eq_reflection, length_Cons RS eq_reflection];
paulson@2112
    76
paulson@3191
    77
 (*---------------------------------------------------------------------------
paulson@3191
    78
  * Does some standard things with the termination conditions of a definition:
paulson@3191
    79
  * attempts to prove wellfoundedness of the given relation; simplifies the
paulson@3191
    80
  * non-proven termination conditions; and finally attempts to prove the 
paulson@3191
    81
  * simplified termination conditions.
paulson@3191
    82
  *--------------------------------------------------------------------------*)
paulson@2112
    83
 val std_postprocessor = Prim.postprocess{WFtac = WFtac,
paulson@2112
    84
                                    terminator = terminator, 
paulson@2112
    85
                                    simplifier = Prim.Rules.simpl_conv simpls};
paulson@2112
    86
paulson@2112
    87
 val simplifier = rewrite_rule (simpls @ #simps(rep_ss HOL_ss) @ 
paulson@2112
    88
                                [pred_nat_def,pred_list_def]);
paulson@3191
    89
paulson@2112
    90
 fun tflcongs thy = Prim.Context.read() @ (#case_congs(Thry.extract_info thy));
paulson@2112
    91
paulson@2112
    92
paulson@2112
    93
val concl = #2 o Prim.Rules.dest_thm;
paulson@2112
    94
paulson@2112
    95
(*---------------------------------------------------------------------------
paulson@3191
    96
 * Defining a function with an associated termination relation. 
paulson@3191
    97
 *---------------------------------------------------------------------------*)
paulson@3191
    98
fun define_i thy R eqs = 
paulson@3191
    99
  let val dummy = require_thy thy "WF_Rel" "recursive function definitions";
paulson@3191
   100
      
paulson@3191
   101
      val {functional,pats} = Prim.mk_functional thy eqs
paulson@3191
   102
      val (thm,thry) = Prim.wfrec_definition0 thy  R functional
paulson@3191
   103
  in (thry,(thm,pats))
paulson@3191
   104
  end;
paulson@3191
   105
paulson@3191
   106
(*lcp's version: takes strings; doesn't return "thm" 
paulson@3191
   107
	(whose signature is a draft and therefore useless) *)
paulson@3191
   108
fun define thy R eqs = 
paulson@3191
   109
  let fun read thy = readtm (sign_of thy) (TVar(("DUMMY",0),[])) 
paulson@3191
   110
      val (thy',(_,pats)) =
paulson@3191
   111
	     define_i thy (read thy R) 
paulson@3191
   112
	              (fold_bal (app Ind_Syntax.conj) (map (read thy) eqs))
paulson@3191
   113
  in  (thy',pats)  end
paulson@3191
   114
  handle Utils.ERR {mesg,...} => error mesg;
paulson@3191
   115
paulson@3191
   116
(*---------------------------------------------------------------------------
paulson@3191
   117
 * Postprocess a definition made by "define". This is a separate stage of 
paulson@3191
   118
 * processing from the definition stage.
paulson@2112
   119
 *---------------------------------------------------------------------------*)
paulson@2112
   120
local 
paulson@2112
   121
structure R = Prim.Rules
paulson@2112
   122
structure U = Utils
paulson@2112
   123
paulson@3191
   124
(* The rest of these local definitions are for the tricky nested case *)
paulson@2112
   125
val solved = not o U.can S.dest_eq o #2 o S.strip_forall o concl
paulson@2112
   126
paulson@2112
   127
fun id_thm th = 
paulson@2112
   128
   let val {lhs,rhs} = S.dest_eq(#2(S.strip_forall(#2 (R.dest_thm th))))
paulson@2112
   129
   in S.aconv lhs rhs
paulson@2112
   130
   end handle _ => false
paulson@2112
   131
paulson@2112
   132
fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
paulson@2112
   133
val P_imp_P_iff_True = prover "P --> (P= True)" RS mp;
paulson@2112
   134
val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection;
paulson@2112
   135
fun mk_meta_eq r = case concl_of r of
paulson@2112
   136
     Const("==",_)$_$_ => r
paulson@2112
   137
  |   _$(Const("op =",_)$_$_) => r RS eq_reflection
paulson@2112
   138
  |   _ => r RS P_imp_P_eq_True
paulson@2112
   139
fun rewrite L = rewrite_rule (map mk_meta_eq (Utils.filter(not o id_thm) L))
paulson@3191
   140
fun reducer thl = rewrite (map standard thl @ #simps(rep_ss HOL_ss))
paulson@2112
   141
paulson@2112
   142
fun join_assums th = 
paulson@2112
   143
  let val {sign,...} = rep_thm th
paulson@2112
   144
      val tych = cterm_of sign
paulson@2112
   145
      val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th)))
paulson@2112
   146
      val cntxtl = (#1 o S.strip_imp) lhs  (* cntxtl should = cntxtr *)
paulson@2112
   147
      val cntxtr = (#1 o S.strip_imp) rhs  (* but union is solider *)
paulson@2112
   148
      val cntxt = U.union S.aconv cntxtl cntxtr
paulson@2112
   149
  in 
paulson@3191
   150
    R.GEN_ALL 
paulson@3191
   151
      (R.DISCH_ALL 
paulson@3191
   152
         (rewrite (map (R.ASSUME o tych) cntxt) (R.SPEC_ALL th)))
paulson@2112
   153
  end
paulson@2112
   154
  val gen_all = S.gen_all
paulson@2112
   155
in
paulson@3191
   156
(*---------------------------------------------------------------------------
paulson@3191
   157
 * The "reducer" argument is 
paulson@3191
   158
 *  (fn thl => rewrite (map standard thl @ #simps(rep_ss HOL_ss))); 
paulson@3191
   159
 *---------------------------------------------------------------------------*)
paulson@3191
   160
fun proof_stage theory reducer {f, R, rules, full_pats_TCs, TCs} =
paulson@3191
   161
  let val dummy = output(std_out, "Proving induction theorem..  ")
paulson@3191
   162
      val ind = Prim.mk_induction theory f R full_pats_TCs
paulson@3191
   163
      val dummy = output(std_out, "Proved induction theorem.\n")
paulson@3191
   164
      val pp = std_postprocessor theory
paulson@3191
   165
      val dummy = output(std_out, "Postprocessing..  ")
paulson@3191
   166
      val {rules,induction,nested_tcs} = pp{rules=rules,induction=ind,TCs=TCs}
paulson@3191
   167
  in
paulson@3191
   168
  case nested_tcs
paulson@3191
   169
  of [] => (output(std_out, "Postprocessing done.\n");
paulson@3191
   170
            {induction=induction, rules=rules,tcs=[]})
paulson@3191
   171
  | L  => let val dummy = output(std_out, "Simplifying nested TCs..  ")
paulson@2112
   172
              val (solved,simplified,stubborn) =
paulson@2112
   173
               U.itlist (fn th => fn (So,Si,St) =>
paulson@2112
   174
                     if (id_thm th) then (So, Si, th::St) else
paulson@2112
   175
                     if (solved th) then (th::So, Si, St) 
paulson@2112
   176
                     else (So, th::Si, St)) nested_tcs ([],[],[])
paulson@2112
   177
              val simplified' = map join_assums simplified
paulson@2112
   178
              val induction' = reducer (solved@simplified') induction
paulson@2112
   179
              val rules' = reducer (solved@simplified') rules
paulson@3191
   180
              val dummy = output(std_out, "Postprocessing done.\n")
paulson@2112
   181
          in
paulson@2112
   182
          {induction = induction',
paulson@2112
   183
               rules = rules',
paulson@3191
   184
                 tcs = map (gen_all o S.rhs o #2 o S.strip_forall o concl)
paulson@3191
   185
                           (simplified@stubborn)}
paulson@2112
   186
          end
paulson@3191
   187
  end handle (e as Utils.ERR _) => Utils.Raise e
paulson@3191
   188
          |   e                 => print_exn e;
paulson@3191
   189
paulson@3191
   190
paulson@3191
   191
(*lcp: put a theorem into Isabelle form, using meta-level connectives*)
paulson@3191
   192
val meta_outer = 
paulson@3191
   193
    standard o rule_by_tactic (REPEAT_FIRST (resolve_tac [allI, impI, conjI]));
paulson@3191
   194
paulson@3191
   195
paulson@3191
   196
(*Strip off the outer !P*)
paulson@3191
   197
val spec'= read_instantiate [("x","P::?'b=>bool")] spec;
paulson@2112
   198
paulson@2112
   199
paulson@3191
   200
fun simplify_defn (thy,(id,pats)) =
paulson@3191
   201
   let val def = freezeT(get_def thy id  RS  meta_eq_to_obj_eq)
paulson@3191
   202
       val {theory,rules,TCs,full_pats_TCs,patterns} = 
paulson@3191
   203
		Prim.post_definition (thy,(def,pats))
paulson@3191
   204
       val {lhs=f,rhs} = S.dest_eq(concl def)
paulson@3191
   205
       val (_,[R,_]) = S.strip_comb rhs
paulson@3191
   206
       val {induction, rules, tcs} = 
paulson@3191
   207
             proof_stage theory reducer
paulson@3191
   208
	       {f = f, R = R, rules = rules,
paulson@3191
   209
		full_pats_TCs = full_pats_TCs,
paulson@3191
   210
		TCs = TCs}
paulson@3191
   211
       val rules' = map (standard o normalize_thm [RSmp]) (R.CONJUNCTS rules)
paulson@3191
   212
   in  {induct = meta_outer
paulson@3191
   213
	          (normalize_thm [RSspec,RSmp] (induction RS spec')), 
paulson@3191
   214
	rules = rules', 
paulson@3191
   215
	tcs = (termination_goals rules') @ tcs}
paulson@3191
   216
   end
paulson@3191
   217
  handle Utils.ERR {mesg,...} => error mesg
paulson@2112
   218
end;
paulson@2112
   219
paulson@3191
   220
(*---------------------------------------------------------------------------
paulson@3191
   221
 *
paulson@3191
   222
 *     Definitions with synthesized termination relation temporarily
paulson@3191
   223
 *     deleted -- it's not clear how to integrate this facility with
paulson@3191
   224
 *     the Isabelle theory file scheme, which restricts
paulson@3191
   225
 *     inference at theory-construction time.
paulson@3191
   226
 *
paulson@2112
   227
paulson@3191
   228
local fun floutput s = (output(std_out,s); flush_out std_out)
paulson@3191
   229
      structure R = Prim.Rules
paulson@2112
   230
in
paulson@2112
   231
fun function theory eqs = 
paulson@3191
   232
 let val dummy = floutput "Making definition..   "
paulson@2112
   233
     val {rules,R,theory,full_pats_TCs,...} = Prim.lazyR_def theory eqs
paulson@2112
   234
     val f = func_of_cond_eqn (concl(R.CONJUNCT1 rules handle _ => rules))
paulson@3191
   235
     val dummy = floutput "Definition made.\n"
paulson@3191
   236
     val dummy = floutput "Proving induction theorem..  "
paulson@2112
   237
     val induction = Prim.mk_induction theory f R full_pats_TCs
paulson@3191
   238
     val dummy = floutput "Induction theorem proved.\n"
paulson@2112
   239
 in {theory = theory, 
paulson@2112
   240
     eq_ind = standard (induction RS (rules RS conjI))}
paulson@2112
   241
 end
paulson@2112
   242
 handle (e as Utils.ERR _) => Utils.Raise e
paulson@2112
   243
      |     e              => print_exn e
paulson@2112
   244
end;
paulson@2112
   245
paulson@2112
   246
paulson@2112
   247
fun lazyR_def theory eqs = 
paulson@2112
   248
   let val {rules,theory, ...} = Prim.lazyR_def theory eqs
paulson@2112
   249
   in {eqns=rules, theory=theory}
paulson@2112
   250
   end
paulson@2112
   251
   handle (e as Utils.ERR _) => Utils.Raise e
paulson@2112
   252
        |     e              => print_exn e;
paulson@3191
   253
 *
paulson@3191
   254
 *
paulson@3191
   255
 *---------------------------------------------------------------------------*)
paulson@3191
   256
paulson@3191
   257
paulson@2112
   258
paulson@2112
   259
paulson@3191
   260
(*---------------------------------------------------------------------------
paulson@3191
   261
 * Install the basic context notions. Others (for nat and list and prod) 
paulson@3191
   262
 * have already been added in thry.sml
paulson@3191
   263
 *---------------------------------------------------------------------------*)
paulson@3191
   264
val () = Prim.Context.write[Thms.LET_CONG, Thms.COND_CONG];
paulson@2112
   265
paulson@2112
   266
end;