TFL/post.sml
changeset 2112 3902e9af752f
child 2467 357adb429fda
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/TFL/post.sml	Fri Oct 18 12:41:04 1996 +0200
     1.3 @@ -0,0 +1,193 @@
     1.4 +structure Tfl
     1.5 + :sig
     1.6 +   structure Prim : TFL_sig
     1.7 +
     1.8 +   val tgoalw : theory -> thm list -> thm -> thm list
     1.9 +   val tgoal: theory -> thm -> thm list
    1.10 +
    1.11 +   val WF_TAC : thm list -> tactic
    1.12 +
    1.13 +   val simplifier : thm -> thm
    1.14 +   val std_postprocessor : theory 
    1.15 +                           -> {induction:thm, rules:thm, TCs:term list list} 
    1.16 +                           -> {induction:thm, rules:thm, nested_tcs:thm list}
    1.17 +
    1.18 +   val rfunction  : theory
    1.19 +                     -> (thm list -> thm -> thm)
    1.20 +                        -> term -> term  
    1.21 +                          -> {induction:thm, rules:thm, 
    1.22 +                              tcs:term list, theory:theory}
    1.23 +
    1.24 +   val Rfunction : theory -> term -> term  
    1.25 +                   -> {induction:thm, rules:thm, 
    1.26 +                       theory:theory, tcs:term list}
    1.27 +
    1.28 +   val function : theory -> term -> {theory:theory, eq_ind : thm}
    1.29 +   val lazyR_def : theory -> term -> {theory:theory, eqns : thm}
    1.30 +
    1.31 +   val tflcongs : theory -> thm list
    1.32 +
    1.33 +  end = 
    1.34 +struct
    1.35 + structure Prim = Prim
    1.36 +
    1.37 + fun tgoalw thy defs thm = 
    1.38 +    let val L = Prim.termination_goals thm
    1.39 +        open USyntax
    1.40 +        val g = cterm_of (sign_of thy) (mk_prop(list_mk_conj L))
    1.41 +    in goalw_cterm defs g
    1.42 +    end;
    1.43 +
    1.44 + val tgoal = Utils.C tgoalw [];
    1.45 +
    1.46 + fun WF_TAC thms = REPEAT(FIRST1(map rtac thms))
    1.47 + val WFtac = WF_TAC[wf_measure, wf_inv_image, wf_lex_prod, 
    1.48 +                    wf_pred_nat, wf_pred_list, wf_trancl];
    1.49 +
    1.50 + val terminator = simp_tac(HOL_ss addsimps[pred_nat_def,pred_list_def,
    1.51 +                                           fst_conv,snd_conv,
    1.52 +                                           mem_Collect_eq,lessI]) 1
    1.53 +                  THEN TRY(fast_tac set_cs 1);
    1.54 +
    1.55 + val simpls = [less_eq RS eq_reflection,
    1.56 +               lex_prod_def, measure_def, inv_image_def, 
    1.57 +               fst_conv RS eq_reflection, snd_conv RS eq_reflection,
    1.58 +               mem_Collect_eq RS eq_reflection(*, length_Cons RS eq_reflection*)];
    1.59 +
    1.60 + val std_postprocessor = Prim.postprocess{WFtac = WFtac,
    1.61 +                                    terminator = terminator, 
    1.62 +                                    simplifier = Prim.Rules.simpl_conv simpls};
    1.63 +
    1.64 + val simplifier = rewrite_rule (simpls @ #simps(rep_ss HOL_ss) @ 
    1.65 +                                [pred_nat_def,pred_list_def]);
    1.66 + fun tflcongs thy = Prim.Context.read() @ (#case_congs(Thry.extract_info thy));
    1.67 +
    1.68 +
    1.69 +local structure S = Prim.USyntax
    1.70 +in
    1.71 +fun func_of_cond_eqn tm =
    1.72 +  #1(S.strip_comb(#lhs(S.dest_eq(#2(S.strip_forall(#2(S.strip_imp tm)))))))
    1.73 +end;
    1.74 +
    1.75 +
    1.76 +val concl = #2 o Prim.Rules.dest_thm;
    1.77 +
    1.78 +(*---------------------------------------------------------------------------
    1.79 + * Defining a function with an associated termination relation. Lots of
    1.80 + * postprocessing takes place.
    1.81 + *---------------------------------------------------------------------------*)
    1.82 +local 
    1.83 +structure S = Prim.USyntax
    1.84 +structure R = Prim.Rules
    1.85 +structure U = Utils
    1.86 +
    1.87 +val solved = not o U.can S.dest_eq o #2 o S.strip_forall o concl
    1.88 +
    1.89 +fun id_thm th = 
    1.90 +   let val {lhs,rhs} = S.dest_eq(#2(S.strip_forall(#2 (R.dest_thm th))))
    1.91 +   in S.aconv lhs rhs
    1.92 +   end handle _ => false
    1.93 +
    1.94 +fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
    1.95 +val P_imp_P_iff_True = prover "P --> (P= True)" RS mp;
    1.96 +val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection;
    1.97 +fun mk_meta_eq r = case concl_of r of
    1.98 +     Const("==",_)$_$_ => r
    1.99 +  |   _$(Const("op =",_)$_$_) => r RS eq_reflection
   1.100 +  |   _ => r RS P_imp_P_eq_True
   1.101 +fun rewrite L = rewrite_rule (map mk_meta_eq (Utils.filter(not o id_thm) L))
   1.102 +
   1.103 +fun join_assums th = 
   1.104 +  let val {sign,...} = rep_thm th
   1.105 +      val tych = cterm_of sign
   1.106 +      val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th)))
   1.107 +      val cntxtl = (#1 o S.strip_imp) lhs  (* cntxtl should = cntxtr *)
   1.108 +      val cntxtr = (#1 o S.strip_imp) rhs  (* but union is solider *)
   1.109 +      val cntxt = U.union S.aconv cntxtl cntxtr
   1.110 +  in 
   1.111 +  R.GEN_ALL 
   1.112 +  (R.DISCH_ALL 
   1.113 +    (rewrite (map (R.ASSUME o tych) cntxt) (R.SPEC_ALL th)))
   1.114 +  end
   1.115 +  val gen_all = S.gen_all
   1.116 +in
   1.117 +fun rfunction theory reducer R eqs = 
   1.118 + let val _ = output(std_out, "Making definition..  ")
   1.119 +     val _ = flush_out std_out
   1.120 +     val {rules,theory, full_pats_TCs,
   1.121 +          TCs,...} = Prim.gen_wfrec_definition theory {R=R,eqs=eqs} 
   1.122 +     val f = func_of_cond_eqn(concl(R.CONJUNCT1 rules handle _ => rules))
   1.123 +     val _ = output(std_out, "Definition made.\n")
   1.124 +     val _ = output(std_out, "Proving induction theorem..  ")
   1.125 +     val _ = flush_out std_out
   1.126 +     val ind = Prim.mk_induction theory f R full_pats_TCs
   1.127 +     val _ = output(std_out, "Proved induction theorem.\n")
   1.128 +     val pp = std_postprocessor theory
   1.129 +     val _ = output(std_out, "Postprocessing..  ")
   1.130 +     val _ = flush_out std_out
   1.131 +     val {rules,induction,nested_tcs} = pp{rules=rules,induction=ind,TCs=TCs}
   1.132 +     val normal_tcs = Prim.termination_goals rules
   1.133 + in
   1.134 + case nested_tcs
   1.135 + of [] => (output(std_out, "Postprocessing done.\n");
   1.136 +           {theory=theory, induction=induction, rules=rules,tcs=normal_tcs})
   1.137 +  | L  => let val _ = output(std_out, "Simplifying nested TCs..  ")
   1.138 +              val (solved,simplified,stubborn) =
   1.139 +               U.itlist (fn th => fn (So,Si,St) =>
   1.140 +                     if (id_thm th) then (So, Si, th::St) else
   1.141 +                     if (solved th) then (th::So, Si, St) 
   1.142 +                     else (So, th::Si, St)) nested_tcs ([],[],[])
   1.143 +              val simplified' = map join_assums simplified
   1.144 +              val induction' = reducer (solved@simplified') induction
   1.145 +              val rules' = reducer (solved@simplified') rules
   1.146 +              val _ = output(std_out, "Postprocessing done.\n")
   1.147 +          in
   1.148 +          {induction = induction',
   1.149 +               rules = rules',
   1.150 +                 tcs = normal_tcs @
   1.151 +                      map (gen_all o S.rhs o #2 o S.strip_forall o concl)
   1.152 +                           (simplified@stubborn),
   1.153 +              theory = theory}
   1.154 +          end
   1.155 + end
   1.156 + handle (e as Utils.ERR _) => Utils.Raise e
   1.157 +     |     e               => print_exn e
   1.158 +
   1.159 +
   1.160 +fun Rfunction thry = 
   1.161 +     rfunction thry 
   1.162 +       (fn thl => rewrite (map standard thl @ #simps(rep_ss HOL_ss)));
   1.163 +
   1.164 +
   1.165 +end;
   1.166 +
   1.167 +
   1.168 +local structure R = Prim.Rules
   1.169 +in
   1.170 +fun function theory eqs = 
   1.171 + let val _ = output(std_out, "Making definition..  ")
   1.172 +     val {rules,R,theory,full_pats_TCs,...} = Prim.lazyR_def theory eqs
   1.173 +     val f = func_of_cond_eqn (concl(R.CONJUNCT1 rules handle _ => rules))
   1.174 +     val _ = output(std_out, "Definition made.\n")
   1.175 +     val _ = output(std_out, "Proving induction theorem..  ")
   1.176 +     val induction = Prim.mk_induction theory f R full_pats_TCs
   1.177 +      val _ = output(std_out, "Induction theorem proved.\n")
   1.178 + in {theory = theory, 
   1.179 +     eq_ind = standard (induction RS (rules RS conjI))}
   1.180 + end
   1.181 + handle (e as Utils.ERR _) => Utils.Raise e
   1.182 +      |     e              => print_exn e
   1.183 +end;
   1.184 +
   1.185 +
   1.186 +fun lazyR_def theory eqs = 
   1.187 +   let val {rules,theory, ...} = Prim.lazyR_def theory eqs
   1.188 +   in {eqns=rules, theory=theory}
   1.189 +   end
   1.190 +   handle (e as Utils.ERR _) => Utils.Raise e
   1.191 +        |     e              => print_exn e;
   1.192 +
   1.193 +
   1.194 + val () = Prim.Context.write[Thms.LET_CONG, Thms.COND_CONG];
   1.195 +
   1.196 +end;