TFL/post.sml
author paulson
Fri, 03 Jan 1997 10:45:31 +0100
changeset 2467 357adb429fda
parent 2112 3902e9af752f
child 3191 14bd6e5985f1
permissions -rw-r--r--
Conversion to Basis Library (using prs instead of output)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     1
structure Tfl
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     2
 :sig
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     3
   structure Prim : TFL_sig
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     4
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     5
   val tgoalw : theory -> thm list -> thm -> thm list
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     6
   val tgoal: theory -> thm -> thm list
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     7
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     8
   val WF_TAC : thm list -> tactic
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     9
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    10
   val simplifier : thm -> thm
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    11
   val std_postprocessor : theory 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    12
                           -> {induction:thm, rules:thm, TCs:term list list} 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    13
                           -> {induction:thm, rules:thm, nested_tcs:thm list}
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    14
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    15
   val rfunction  : theory
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    16
                     -> (thm list -> thm -> thm)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    17
                        -> term -> term  
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    18
                          -> {induction:thm, rules:thm, 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    19
                              tcs:term list, theory:theory}
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    20
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    21
   val Rfunction : theory -> term -> term  
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    22
                   -> {induction:thm, rules:thm, 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    23
                       theory:theory, tcs:term list}
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    24
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    25
   val function : theory -> term -> {theory:theory, eq_ind : thm}
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    26
   val lazyR_def : theory -> term -> {theory:theory, eqns : thm}
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    27
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    28
   val tflcongs : theory -> thm list
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    29
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    30
  end = 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    31
struct
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    32
 structure Prim = Prim
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    33
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    34
 fun tgoalw thy defs thm = 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    35
    let val L = Prim.termination_goals thm
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    36
        open USyntax
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    37
        val g = cterm_of (sign_of thy) (mk_prop(list_mk_conj L))
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    38
    in goalw_cterm defs g
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    39
    end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    40
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    41
 val tgoal = Utils.C tgoalw [];
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    42
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    43
 fun WF_TAC thms = REPEAT(FIRST1(map rtac thms))
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    44
 val WFtac = WF_TAC[wf_measure, wf_inv_image, wf_lex_prod, 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    45
                    wf_pred_nat, wf_pred_list, wf_trancl];
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    46
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    47
 val terminator = simp_tac(HOL_ss addsimps[pred_nat_def,pred_list_def,
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    48
                                           fst_conv,snd_conv,
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    49
                                           mem_Collect_eq,lessI]) 1
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    50
                  THEN TRY(fast_tac set_cs 1);
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    51
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    52
 val simpls = [less_eq RS eq_reflection,
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    53
               lex_prod_def, measure_def, inv_image_def, 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    54
               fst_conv RS eq_reflection, snd_conv RS eq_reflection,
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    55
               mem_Collect_eq RS eq_reflection(*, length_Cons RS eq_reflection*)];
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    56
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    57
 val std_postprocessor = Prim.postprocess{WFtac = WFtac,
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    58
                                    terminator = terminator, 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    59
                                    simplifier = Prim.Rules.simpl_conv simpls};
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    60
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    61
 val simplifier = rewrite_rule (simpls @ #simps(rep_ss HOL_ss) @ 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    62
                                [pred_nat_def,pred_list_def]);
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    63
 fun tflcongs thy = Prim.Context.read() @ (#case_congs(Thry.extract_info thy));
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    64
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    65
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    66
local structure S = Prim.USyntax
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    67
in
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    68
fun func_of_cond_eqn tm =
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    69
  #1(S.strip_comb(#lhs(S.dest_eq(#2(S.strip_forall(#2(S.strip_imp tm)))))))
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    70
end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    71
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    72
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    73
val concl = #2 o Prim.Rules.dest_thm;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    74
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    75
(*---------------------------------------------------------------------------
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    76
 * Defining a function with an associated termination relation. Lots of
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    77
 * postprocessing takes place.
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    78
 *---------------------------------------------------------------------------*)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    79
local 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    80
structure S = Prim.USyntax
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    81
structure R = Prim.Rules
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    82
structure U = Utils
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    83
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    84
val solved = not o U.can S.dest_eq o #2 o S.strip_forall o concl
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    85
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    86
fun id_thm th = 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    87
   let val {lhs,rhs} = S.dest_eq(#2(S.strip_forall(#2 (R.dest_thm th))))
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    88
   in S.aconv lhs rhs
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    89
   end handle _ => false
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    90
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    91
fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    92
val P_imp_P_iff_True = prover "P --> (P= True)" RS mp;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    93
val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    94
fun mk_meta_eq r = case concl_of r of
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    95
     Const("==",_)$_$_ => r
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    96
  |   _$(Const("op =",_)$_$_) => r RS eq_reflection
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    97
  |   _ => r RS P_imp_P_eq_True
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    98
fun rewrite L = rewrite_rule (map mk_meta_eq (Utils.filter(not o id_thm) L))
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    99
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   100
fun join_assums th = 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   101
  let val {sign,...} = rep_thm th
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   102
      val tych = cterm_of sign
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   103
      val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th)))
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   104
      val cntxtl = (#1 o S.strip_imp) lhs  (* cntxtl should = cntxtr *)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   105
      val cntxtr = (#1 o S.strip_imp) rhs  (* but union is solider *)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   106
      val cntxt = U.union S.aconv cntxtl cntxtr
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   107
  in 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   108
  R.GEN_ALL 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   109
  (R.DISCH_ALL 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   110
    (rewrite (map (R.ASSUME o tych) cntxt) (R.SPEC_ALL th)))
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   111
  end
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   112
  val gen_all = S.gen_all
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   113
in
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   114
fun rfunction theory reducer R eqs = 
2467
357adb429fda Conversion to Basis Library (using prs instead of output)
paulson
parents: 2112
diff changeset
   115
 let val _ = prs "Making definition..  "
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   116
     val {rules,theory, full_pats_TCs,
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   117
          TCs,...} = Prim.gen_wfrec_definition theory {R=R,eqs=eqs} 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   118
     val f = func_of_cond_eqn(concl(R.CONJUNCT1 rules handle _ => rules))
2467
357adb429fda Conversion to Basis Library (using prs instead of output)
paulson
parents: 2112
diff changeset
   119
     val _ = prs "Definition made.\n"
357adb429fda Conversion to Basis Library (using prs instead of output)
paulson
parents: 2112
diff changeset
   120
     val _ = prs "Proving induction theorem..  "
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   121
     val ind = Prim.mk_induction theory f R full_pats_TCs
2467
357adb429fda Conversion to Basis Library (using prs instead of output)
paulson
parents: 2112
diff changeset
   122
     val _ = prs "Proved induction theorem.\n"
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   123
     val pp = std_postprocessor theory
2467
357adb429fda Conversion to Basis Library (using prs instead of output)
paulson
parents: 2112
diff changeset
   124
     val _ = prs "Postprocessing..  "
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   125
     val {rules,induction,nested_tcs} = pp{rules=rules,induction=ind,TCs=TCs}
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   126
     val normal_tcs = Prim.termination_goals rules
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   127
 in
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   128
 case nested_tcs
2467
357adb429fda Conversion to Basis Library (using prs instead of output)
paulson
parents: 2112
diff changeset
   129
 of [] => (prs "Postprocessing done.\n";
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   130
           {theory=theory, induction=induction, rules=rules,tcs=normal_tcs})
2467
357adb429fda Conversion to Basis Library (using prs instead of output)
paulson
parents: 2112
diff changeset
   131
  | L  => let val _ = prs "Simplifying nested TCs..  "
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   132
              val (solved,simplified,stubborn) =
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   133
               U.itlist (fn th => fn (So,Si,St) =>
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   134
                     if (id_thm th) then (So, Si, th::St) else
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   135
                     if (solved th) then (th::So, Si, St) 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   136
                     else (So, th::Si, St)) nested_tcs ([],[],[])
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   137
              val simplified' = map join_assums simplified
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   138
              val induction' = reducer (solved@simplified') induction
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   139
              val rules' = reducer (solved@simplified') rules
2467
357adb429fda Conversion to Basis Library (using prs instead of output)
paulson
parents: 2112
diff changeset
   140
              val _ = prs "Postprocessing done.\n"
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   141
          in
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   142
          {induction = induction',
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   143
               rules = rules',
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   144
                 tcs = normal_tcs @
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   145
                      map (gen_all o S.rhs o #2 o S.strip_forall o concl)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   146
                           (simplified@stubborn),
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   147
              theory = theory}
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   148
          end
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   149
 end
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   150
 handle (e as Utils.ERR _) => Utils.Raise e
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   151
     |     e               => print_exn e
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   152
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   153
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   154
fun Rfunction thry = 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   155
     rfunction thry 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   156
       (fn thl => rewrite (map standard thl @ #simps(rep_ss HOL_ss)));
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   157
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   158
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   159
end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   160
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   161
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   162
local structure R = Prim.Rules
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   163
in
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   164
fun function theory eqs = 
2467
357adb429fda Conversion to Basis Library (using prs instead of output)
paulson
parents: 2112
diff changeset
   165
 let val _ = prs "Making definition..  "
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   166
     val {rules,R,theory,full_pats_TCs,...} = Prim.lazyR_def theory eqs
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   167
     val f = func_of_cond_eqn (concl(R.CONJUNCT1 rules handle _ => rules))
2467
357adb429fda Conversion to Basis Library (using prs instead of output)
paulson
parents: 2112
diff changeset
   168
     val _ = prs "Definition made.\n"
357adb429fda Conversion to Basis Library (using prs instead of output)
paulson
parents: 2112
diff changeset
   169
     val _ = prs "Proving induction theorem..  "
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   170
     val induction = Prim.mk_induction theory f R full_pats_TCs
2467
357adb429fda Conversion to Basis Library (using prs instead of output)
paulson
parents: 2112
diff changeset
   171
     val _ = prs "Induction theorem proved.\n"
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   172
 in {theory = theory, 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   173
     eq_ind = standard (induction RS (rules RS conjI))}
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   174
 end
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   175
 handle (e as Utils.ERR _) => Utils.Raise e
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   176
      |     e              => print_exn e
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   177
end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   178
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   179
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   180
fun lazyR_def theory eqs = 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   181
   let val {rules,theory, ...} = Prim.lazyR_def theory eqs
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   182
   in {eqns=rules, theory=theory}
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   183
   end
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   184
   handle (e as Utils.ERR _) => Utils.Raise e
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   185
        |     e              => print_exn e;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   186
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   187
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   188
 val () = Prim.Context.write[Thms.LET_CONG, Thms.COND_CONG];
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   189
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   190
end;