2112

1 
structure Tfl


2 
:sig


3 
structure Prim : TFL_sig


4 


5 
val tgoalw : theory > thm list > thm > thm list


6 
val tgoal: theory > thm > thm list


7 


8 
val WF_TAC : thm list > tactic


9 


10 
val simplifier : thm > thm


11 
val std_postprocessor : theory


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


13 
> {induction:thm, rules:thm, nested_tcs:thm list}


14 


15 
val rfunction : theory


16 
> (thm list > thm > thm)


17 
> term > term


18 
> {induction:thm, rules:thm,


19 
tcs:term list, theory:theory}


20 


21 
val Rfunction : theory > term > term


22 
> {induction:thm, rules:thm,


23 
theory:theory, tcs:term list}


24 


25 
val function : theory > term > {theory:theory, eq_ind : thm}


26 
val lazyR_def : theory > term > {theory:theory, eqns : thm}


27 


28 
val tflcongs : theory > thm list


29 


30 
end =


31 
struct


32 
structure Prim = Prim


33 


34 
fun tgoalw thy defs thm =


35 
let val L = Prim.termination_goals thm


36 
open USyntax


37 
val g = cterm_of (sign_of thy) (mk_prop(list_mk_conj L))


38 
in goalw_cterm defs g


39 
end;


40 


41 
val tgoal = Utils.C tgoalw [];


42 


43 
fun WF_TAC thms = REPEAT(FIRST1(map rtac thms))


44 
val WFtac = WF_TAC[wf_measure, wf_inv_image, wf_lex_prod,


45 
wf_pred_nat, wf_pred_list, wf_trancl];


46 


47 
val terminator = simp_tac(HOL_ss addsimps[pred_nat_def,pred_list_def,


48 
fst_conv,snd_conv,


49 
mem_Collect_eq,lessI]) 1


50 
THEN TRY(fast_tac set_cs 1);


51 


52 
val simpls = [less_eq RS eq_reflection,


53 
lex_prod_def, measure_def, inv_image_def,


54 
fst_conv RS eq_reflection, snd_conv RS eq_reflection,


55 
mem_Collect_eq RS eq_reflection(*, length_Cons RS eq_reflection*)];


56 


57 
val std_postprocessor = Prim.postprocess{WFtac = WFtac,


58 
terminator = terminator,


59 
simplifier = Prim.Rules.simpl_conv simpls};


60 


61 
val simplifier = rewrite_rule (simpls @ #simps(rep_ss HOL_ss) @


62 
[pred_nat_def,pred_list_def]);


63 
fun tflcongs thy = Prim.Context.read() @ (#case_congs(Thry.extract_info thy));


64 


65 


66 
local structure S = Prim.USyntax


67 
in


68 
fun func_of_cond_eqn tm =


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


70 
end;


71 


72 


73 
val concl = #2 o Prim.Rules.dest_thm;


74 


75 
(*


76 
* Defining a function with an associated termination relation. Lots of


77 
* postprocessing takes place.


78 
**)


79 
local


80 
structure S = Prim.USyntax


81 
structure R = Prim.Rules


82 
structure U = Utils


83 


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


85 


86 
fun id_thm th =


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


88 
in S.aconv lhs rhs


89 
end handle _ => false


90 


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


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


93 
val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection;


94 
fun mk_meta_eq r = case concl_of r of


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


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


97 
 _ => r RS P_imp_P_eq_True


98 
fun rewrite L = rewrite_rule (map mk_meta_eq (Utils.filter(not o id_thm) L))


99 


100 
fun join_assums th =


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


102 
val tych = cterm_of sign


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


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


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


106 
val cntxt = U.union S.aconv cntxtl cntxtr


107 
in


108 
R.GEN_ALL


109 
(R.DISCH_ALL


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


111 
end


112 
val gen_all = S.gen_all


113 
in


114 
fun rfunction theory reducer R eqs =


115 
let val _ = output(std_out, "Making definition.. ")


116 
val _ = flush_out std_out


117 
val {rules,theory, full_pats_TCs,


118 
TCs,...} = Prim.gen_wfrec_definition theory {R=R,eqs=eqs}


119 
val f = func_of_cond_eqn(concl(R.CONJUNCT1 rules handle _ => rules))


120 
val _ = output(std_out, "Definition made.\n")


121 
val _ = output(std_out, "Proving induction theorem.. ")


122 
val _ = flush_out std_out


123 
val ind = Prim.mk_induction theory f R full_pats_TCs


124 
val _ = output(std_out, "Proved induction theorem.\n")


125 
val pp = std_postprocessor theory


126 
val _ = output(std_out, "Postprocessing.. ")


127 
val _ = flush_out std_out


128 
val {rules,induction,nested_tcs} = pp{rules=rules,induction=ind,TCs=TCs}


129 
val normal_tcs = Prim.termination_goals rules


130 
in


131 
case nested_tcs


132 
of [] => (output(std_out, "Postprocessing done.\n");


133 
{theory=theory, induction=induction, rules=rules,tcs=normal_tcs})


134 
 L => let val _ = output(std_out, "Simplifying nested TCs.. ")


135 
val (solved,simplified,stubborn) =


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


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


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


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


140 
val simplified' = map join_assums simplified


141 
val induction' = reducer (solved@simplified') induction


142 
val rules' = reducer (solved@simplified') rules


143 
val _ = output(std_out, "Postprocessing done.\n")


144 
in


145 
{induction = induction',


146 
rules = rules',


147 
tcs = normal_tcs @


148 
map (gen_all o S.rhs o #2 o S.strip_forall o concl)


149 
(simplified@stubborn),


150 
theory = theory}


151 
end


152 
end


153 
handle (e as Utils.ERR _) => Utils.Raise e


154 
 e => print_exn e


155 


156 


157 
fun Rfunction thry =


158 
rfunction thry


159 
(fn thl => rewrite (map standard thl @ #simps(rep_ss HOL_ss)));


160 


161 


162 
end;


163 


164 


165 
local structure R = Prim.Rules


166 
in


167 
fun function theory eqs =


168 
let val _ = output(std_out, "Making definition.. ")


169 
val {rules,R,theory,full_pats_TCs,...} = Prim.lazyR_def theory eqs


170 
val f = func_of_cond_eqn (concl(R.CONJUNCT1 rules handle _ => rules))


171 
val _ = output(std_out, "Definition made.\n")


172 
val _ = output(std_out, "Proving induction theorem.. ")


173 
val induction = Prim.mk_induction theory f R full_pats_TCs


174 
val _ = output(std_out, "Induction theorem proved.\n")


175 
in {theory = theory,


176 
eq_ind = standard (induction RS (rules RS conjI))}


177 
end


178 
handle (e as Utils.ERR _) => Utils.Raise e


179 
 e => print_exn e


180 
end;


181 


182 


183 
fun lazyR_def theory eqs =


184 
let val {rules,theory, ...} = Prim.lazyR_def theory eqs


185 
in {eqns=rules, theory=theory}


186 
end


187 
handle (e as Utils.ERR _) => Utils.Raise e


188 
 e => print_exn e;


189 


190 


191 
val () = Prim.Context.write[Thms.LET_CONG, Thms.COND_CONG];


192 


193 
end;
