10769

1 
(* Title: TFL/post.ML


2 
ID: $Id$


3 
Author: Konrad Slind, Cambridge University Computer Laboratory


4 
Copyright 1997 University of Cambridge


5 


6 
Second part of main module (postprocessing of TFL definitions).


7 
*)


8 


9 
signature TFL =


10 
sig


11 
val trace: bool ref


12 
val quiet_mode: bool ref


13 
val message: string > unit


14 
val tgoalw: theory > thm list > thm list > thm list


15 
val tgoal: theory > thm list > thm list


16 
val std_postprocessor: claset > simpset > thm list > theory >


17 
{induction: thm, rules: thm, TCs: term list list} >


18 
{induction: thm, rules: thm, nested_tcs: thm list}


19 
val define_i: theory > claset > simpset > thm list > thm list > xstring >


20 
term > term list > theory * {rules: (thm * int) list, induct: thm, tcs: term list}


21 
val define: theory > claset > simpset > thm list > thm list > xstring >


22 
string > string list > theory * {rules: (thm * int) list, induct: thm, tcs: term list}


23 
val defer_i: theory > thm list > xstring > term list > theory * thm


24 
val defer: theory > thm list > xstring > string list > theory * thm


25 
end;


26 


27 
structure Tfl: TFL =


28 
struct


29 


30 
structure S = USyntax


31 


32 


33 
(* messages *)


34 


35 
val trace = Prim.trace


36 


37 
val quiet_mode = ref false;


38 
fun message s = if ! quiet_mode then () else writeln s;


39 


40 


41 
(* misc *)


42 


43 
fun read_term thy = Sign.simple_read_term (Theory.sign_of thy) HOLogic.termT;


44 


45 


46 
(*


47 
* Extract termination goals so that they can be put it into a goalstack, or


48 
* have a tactic directly applied to them.


49 
**)


50 
fun termination_goals rules =


51 
map (#1 o Type.freeze_thaw o HOLogic.dest_Trueprop)


52 
(foldr (fn (th,A) => union_term (prems_of th, A)) (rules, []));


53 


54 
(*


55 
* Finds the termination conditions in (highly massaged) definition and


56 
* puts them into a goalstack.


57 
**)


58 
fun tgoalw thy defs rules =


59 
case termination_goals rules of


60 
[] => error "tgoalw: no termination conditions to prove"


61 
 L => goalw_cterm defs


62 
(Thm.cterm_of (Theory.sign_of thy)


63 
(HOLogic.mk_Trueprop(USyntax.list_mk_conj L)));


64 


65 
fun tgoal thy = tgoalw thy [];


66 


67 
(*


68 
* Three postprocessors are applied to the definition. It


69 
* attempts to prove wellfoundedness of the given relation, simplifies the


70 
* nonproved termination conditions, and finally attempts to prove the


71 
* simplified termination conditions.


72 
**)


73 
fun std_postprocessor cs ss wfs =


74 
Prim.postprocess


75 
{wf_tac = REPEAT (ares_tac wfs 1),


76 
terminator = asm_simp_tac ss 1


77 
THEN TRY (fast_tac (cs addSDs [not0_implies_Suc] addss ss) 1),


78 
simplifier = Rules.simpl_conv ss []};


79 


80 


81 


82 
val concl = #2 o Rules.dest_thm;


83 


84 
(*


85 
* Postprocess a definition made by "define". This is a separate stage of


86 
* processing from the definition stage.


87 
**)


88 
local


89 
structure R = Rules


90 
structure U = Utils


91 


92 
(* The rest of these local definitions are for the tricky nested case *)


93 
val solved = not o can S.dest_eq o #2 o S.strip_forall o concl


94 


95 
fun id_thm th =


96 
let val {lhs,rhs} = S.dest_eq (#2 (S.strip_forall (#2 (R.dest_thm th))));


97 
in lhs aconv rhs end


98 
handle U.ERR _ => false;


99 


100 


101 
fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);


102 
val P_imp_P_iff_True = prover "P > (P= True)" RS mp;


103 
val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection;


104 
fun mk_meta_eq r = case concl_of r of


105 
Const("==",_)$_$_ => r


106 
 _ $(Const("op =",_)$_$_) => r RS eq_reflection


107 
 _ => r RS P_imp_P_eq_True


108 


109 
(*Is this the best way to invoke the simplifier??*)


110 
fun rewrite L = rewrite_rule (map mk_meta_eq (filter(not o id_thm) L))


111 


112 
fun join_assums th =


113 
let val {sign,...} = rep_thm th


114 
val tych = cterm_of sign


115 
val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th)))


116 
val cntxtl = (#1 o S.strip_imp) lhs (* cntxtl should = cntxtr *)


117 
val cntxtr = (#1 o S.strip_imp) rhs (* but union is solider *)


118 
val cntxt = gen_union (op aconv) (cntxtl, cntxtr)


119 
in


120 
R.GEN_ALL


121 
(R.DISCH_ALL


122 
(rewrite (map (R.ASSUME o tych) cntxt) (R.SPEC_ALL th)))


123 
end


124 
val gen_all = S.gen_all


125 
in


126 
fun proof_stage cs ss wfs theory {f, R, rules, full_pats_TCs, TCs} =


127 
let


128 
val _ = message "Proving induction theorem ..."


129 
val ind = Prim.mk_induction theory {fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs}


130 
val _ = message "Postprocessing ...";


131 
val {rules, induction, nested_tcs} =


132 
std_postprocessor cs ss wfs theory {rules=rules, induction=ind, TCs=TCs}


133 
in


134 
case nested_tcs


135 
of [] => {induction=induction, rules=rules,tcs=[]}


136 
 L => let val dummy = message "Simplifying nested TCs ..."


137 
val (solved,simplified,stubborn) =


138 
U.itlist (fn th => fn (So,Si,St) =>


139 
if (id_thm th) then (So, Si, th::St) else


140 
if (solved th) then (th::So, Si, St)


141 
else (So, th::Si, St)) nested_tcs ([],[],[])


142 
val simplified' = map join_assums simplified


143 
val rewr = full_simplify (ss addsimps (solved @ simplified'));


144 
val induction' = rewr induction


145 
and rules' = rewr rules


146 
in


147 
{induction = induction',


148 
rules = rules',


149 
tcs = map (gen_all o S.rhs o #2 o S.strip_forall o concl)


150 
(simplified@stubborn)}


151 
end


152 
end;


153 


154 


155 
(*lcp: curry the predicate of the induction rule*)


156 
fun curry_rule rl = split_rule_var


157 
(head_of (HOLogic.dest_Trueprop (concl_of rl)),


158 
rl);


159 


160 
(*lcp: put a theorem into Isabelle form, using metalevel connectives*)


161 
val meta_outer =


162 
curry_rule o standard o


163 
rule_by_tactic (REPEAT


164 
(FIRSTGOAL (resolve_tac [allI, impI, conjI]


165 
ORELSE' etac conjE)));


166 


167 
(*Strip off the outer !P*)


168 
val spec'= read_instantiate [("x","P::?'b=>bool")] spec;


169 


170 
fun simplify_defn thy cs ss congs wfs id pats def0 =


171 
let val def = freezeT def0 RS meta_eq_to_obj_eq


172 
val {theory,rules,rows,TCs,full_pats_TCs} = Prim.post_definition congs (thy, (def,pats))


173 
val {lhs=f,rhs} = S.dest_eq (concl def)


174 
val (_,[R,_]) = S.strip_comb rhs


175 
val {induction, rules, tcs} =


176 
proof_stage cs ss wfs theory


177 
{f = f, R = R, rules = rules,


178 
full_pats_TCs = full_pats_TCs,


179 
TCs = TCs}


180 
val rules' = map (standard o Rulify.rulify_no_asm) (R.CONJUNCTS rules)


181 
in {induct = meta_outer (Rulify.rulify_no_asm (induction RS spec')),


182 
rules = ListPair.zip(rules', rows),


183 
tcs = (termination_goals rules') @ tcs}


184 
end


185 
handle U.ERR {mesg,func,module} =>


186 
error (mesg ^


187 
"\n (In TFL function " ^ module ^ "." ^ func ^ ")");


188 


189 
(*


190 
* Defining a function with an associated termination relation.


191 
**)


192 
fun define_i thy cs ss congs wfs fid R eqs =


193 
let val {functional,pats} = Prim.mk_functional thy eqs


194 
val (thy, def) = Prim.wfrec_definition0 thy (Sign.base_name fid) R functional


195 
in (thy, simplify_defn thy cs ss congs wfs fid pats def) end;


196 


197 
fun define thy cs ss congs wfs fid R seqs =


198 
define_i thy cs ss congs wfs fid (read_term thy R) (map (read_term thy) seqs)


199 
handle U.ERR {mesg,...} => error mesg;


200 


201 


202 
(*


203 
*


204 
* Definitions with synthesized termination relation


205 
*


206 
**)


207 


208 
fun func_of_cond_eqn tm =


209 
#1 (S.strip_comb (#lhs (S.dest_eq (#2 (S.strip_forall (#2 (S.strip_imp tm)))))));


210 


211 
fun defer_i thy congs fid eqs =


212 
let val {rules,R,theory,full_pats_TCs,SV,...} =


213 
Prim.lazyR_def thy (Sign.base_name fid) congs eqs


214 
val f = func_of_cond_eqn (concl (R.CONJUNCT1 rules handle U.ERR _ => rules));


215 
val dummy = message "Proving induction theorem ...";


216 
val induction = Prim.mk_induction theory


217 
{fconst=f, R=R, SV=SV, pat_TCs_list=full_pats_TCs}


218 
in (theory,


219 
(*return the conjoined induction rule and recursion equations,


220 
with assumptions remaining to discharge*)


221 
standard (induction RS (rules RS conjI)))


222 
end


223 


224 
fun defer thy congs fid seqs =


225 
defer_i thy congs fid (map (read_term thy) seqs)


226 
handle U.ERR {mesg,...} => error mesg;


227 
end;


228 


229 
end;
