10781

1 
(* Title: TFL/rules.ML

10769

2 
ID: $Id$


3 
Author: Konrad Slind, Cambridge University Computer Laboratory


4 
Copyright 1997 University of Cambridge


5 


6 
Emulation of HOL inference rules for TFL


7 
*)


8 


9 
signature RULES =


10 
sig


11 
val dest_thm : thm > term list * term


12 


13 
(* Inference rules *)


14 
val REFL :cterm > thm


15 
val ASSUME :cterm > thm


16 
val MP :thm > thm > thm


17 
val MATCH_MP :thm > thm > thm


18 
val CONJUNCT1 :thm > thm


19 
val CONJUNCT2 :thm > thm


20 
val CONJUNCTS :thm > thm list


21 
val DISCH :cterm > thm > thm


22 
val UNDISCH :thm > thm


23 
val SPEC :cterm > thm > thm


24 
val ISPEC :cterm > thm > thm


25 
val ISPECL :cterm list > thm > thm


26 
val GEN :cterm > thm > thm


27 
val GENL :cterm list > thm > thm


28 
val LIST_CONJ :thm list > thm


29 


30 
val SYM : thm > thm


31 
val DISCH_ALL : thm > thm


32 
val FILTER_DISCH_ALL : (term > bool) > thm > thm


33 
val SPEC_ALL : thm > thm


34 
val GEN_ALL : thm > thm


35 
val IMP_TRANS : thm > thm > thm


36 
val PROVE_HYP : thm > thm > thm


37 


38 
val CHOOSE : cterm * thm > thm > thm


39 
val EXISTS : cterm * cterm > thm > thm


40 
val EXISTL : cterm list > thm > thm


41 
val IT_EXISTS : (cterm*cterm) list > thm > thm


42 


43 
val EVEN_ORS : thm list > thm list


44 
val DISJ_CASESL : thm > thm list > thm


45 


46 
val list_beta_conv : cterm > cterm list > thm


47 
val SUBS : thm list > thm > thm


48 
val simpl_conv : simpset > thm list > cterm > thm


49 


50 
val rbeta : thm > thm


51 
(* For debugging my isabelle solver in the conditional rewriter *)


52 
val term_ref : term list ref


53 
val thm_ref : thm list ref


54 
val mss_ref : meta_simpset list ref


55 
val tracing : bool ref


56 
val CONTEXT_REWRITE_RULE : term * term list * thm * thm list


57 
> thm > thm * term list


58 
val RIGHT_ASSOC : thm > thm


59 


60 
val prove : cterm * tactic > thm


61 
end;


62 


63 
structure Rules: RULES =


64 
struct


65 


66 
structure S = USyntax;


67 
structure U = Utils;


68 
structure D = Dcterm;


69 


70 


71 
fun RULES_ERR func mesg = U.ERR {module = "Rules", func = func, mesg = mesg};


72 


73 


74 
fun cconcl thm = D.drop_prop (#prop (Thm.crep_thm thm));


75 
fun chyps thm = map D.drop_prop (#hyps (Thm.crep_thm thm));


76 


77 
fun dest_thm thm =


78 
let val {prop,hyps,...} = Thm.rep_thm thm


79 
in (map HOLogic.dest_Trueprop hyps, HOLogic.dest_Trueprop prop) end


80 
handle TERM _ => raise RULES_ERR "dest_thm" "missing Trueprop";


81 


82 


83 
(* Inference rules *)


84 


85 
(*


86 
* Equality (one step)


87 
**)


88 


89 
fun REFL tm = Thm.reflexive tm RS meta_eq_to_obj_eq


90 
handle THM (msg, _, _) => raise RULES_ERR "REFL" msg;


91 


92 
fun SYM thm = thm RS sym


93 
handle THM (msg, _, _) => raise RULES_ERR "SYM" msg;


94 


95 
fun ALPHA thm ctm1 =


96 
let


97 
val ctm2 = Thm.cprop_of thm;


98 
val ctm2_eq = Thm.reflexive ctm2;


99 
val ctm1_eq = Thm.reflexive ctm1;


100 
in Thm.equal_elim (Thm.transitive ctm2_eq ctm1_eq) thm end


101 
handle THM (msg, _, _) => raise RULES_ERR "ALPHA" msg;


102 


103 
fun rbeta th =


104 
(case D.strip_comb (cconcl th) of


105 
(_, [l, r]) => Thm.transitive th (Thm.beta_conversion false r)


106 
 _ => raise RULES_ERR "rbeta" "");


107 


108 


109 
(*


110 
* Implication and the assumption list


111 
*


112 
* Assumptions get stuck on the metalanguage assumption list. Implications


113 
* are in the object language, so discharging an assumption "A" from theorem


114 
* "B" results in something that looks like "A > B".


115 
**)


116 


117 
fun ASSUME ctm = Thm.assume (D.mk_prop ctm);


118 


119 


120 
(*


121 
* Implication in TFL is >. Metalanguage implication (==>) is only used


122 
* in the implementation of some of the inference rules below.


123 
**)


124 
fun MP th1 th2 = th2 RS (th1 RS mp)


125 
handle THM (msg, _, _) => raise RULES_ERR "MP" msg;


126 


127 
(*forces the first argument to be a proposition if necessary*)


128 
fun DISCH tm thm = Thm.implies_intr (D.mk_prop tm) thm COMP impI


129 
handle THM (msg, _, _) => raise RULES_ERR "DISCH" msg;


130 


131 
fun DISCH_ALL thm = U.itlist DISCH (#hyps (Thm.crep_thm thm)) thm;


132 


133 


134 
fun FILTER_DISCH_ALL P thm =


135 
let fun check tm = P (#t (Thm.rep_cterm tm))


136 
in foldr (fn (tm,th) => if check tm then DISCH tm th else th)


137 
(chyps thm, thm)


138 
end;


139 


140 
(* freezeT expensive! *)


141 
fun UNDISCH thm =


142 
let val tm = D.mk_prop (#1 (D.dest_imp (cconcl (Thm.freezeT thm))))


143 
in Thm.implies_elim (thm RS mp) (ASSUME tm) end


144 
handle U.ERR _ => raise RULES_ERR "UNDISCH" ""


145 
 THM _ => raise RULES_ERR "UNDISCH" "";


146 


147 
fun PROVE_HYP ath bth = MP (DISCH (cconcl ath) bth) ath;


148 


149 
fun IMP_TRANS th1 th2 = th2 RS (th1 RS Thms.imp_trans)


150 
handle THM (msg, _, _) => raise RULES_ERR "IMP_TRANS" msg;


151 


152 


153 
(*


154 
* Conjunction


155 
**)


156 


157 
fun CONJUNCT1 thm = thm RS conjunct1


158 
handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT1" msg;


159 


160 
fun CONJUNCT2 thm = thm RS conjunct2


161 
handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT2" msg;


162 


163 
fun CONJUNCTS th = CONJUNCTS (CONJUNCT1 th) @ CONJUNCTS (CONJUNCT2 th) handle U.ERR _ => [th];


164 


165 
fun LIST_CONJ [] = raise RULES_ERR "LIST_CONJ" "empty list"


166 
 LIST_CONJ [th] = th


167 
 LIST_CONJ (th :: rst) = MP (MP (conjI COMP (impI RS impI)) th) (LIST_CONJ rst)


168 
handle THM (msg, _, _) => raise RULES_ERR "LIST_CONJ" msg;


169 


170 


171 
(*


172 
* Disjunction


173 
**)


174 
local val {prop,sign,...} = rep_thm disjI1


175 
val [P,Q] = term_vars prop


176 
val disj1 = Thm.forall_intr (Thm.cterm_of sign Q) disjI1


177 
in


178 
fun DISJ1 thm tm = thm RS (forall_elim (D.drop_prop tm) disj1)


179 
handle THM (msg, _, _) => raise RULES_ERR "DISJ1" msg;


180 
end;


181 


182 
local val {prop,sign,...} = rep_thm disjI2


183 
val [P,Q] = term_vars prop


184 
val disj2 = Thm.forall_intr (Thm.cterm_of sign P) disjI2


185 
in


186 
fun DISJ2 tm thm = thm RS (forall_elim (D.drop_prop tm) disj2)


187 
handle THM (msg, _, _) => raise RULES_ERR "DISJ2" msg;


188 
end;


189 


190 


191 
(*


192 
*


193 
* A1  M1, ..., An  Mn


194 
* 


195 
* [A1  M1 \/ ... \/ Mn, ..., An  M1 \/ ... \/ Mn]


196 
*


197 
**)


198 


199 


200 
fun EVEN_ORS thms =


201 
let fun blue ldisjs [] _ = []


202 
 blue ldisjs (th::rst) rdisjs =


203 
let val tail = tl rdisjs


204 
val rdisj_tl = D.list_mk_disj tail


205 
in U.itlist DISJ2 ldisjs (DISJ1 th rdisj_tl)


206 
:: blue (ldisjs @ [cconcl th]) rst tail


207 
end handle U.ERR _ => [U.itlist DISJ2 ldisjs th]


208 
in blue [] thms (map cconcl thms) end;


209 


210 


211 
(*


212 
*


213 
* A  P \/ Q B,P  R C,Q  R


214 
* 


215 
* A U B U C  R


216 
*


217 
**)


218 


219 
fun DISJ_CASES th1 th2 th3 =


220 
let


221 
val c = D.drop_prop (cconcl th1);


222 
val (disj1, disj2) = D.dest_disj c;


223 
val th2' = DISCH disj1 th2;


224 
val th3' = DISCH disj2 th3;


225 
in


226 
th3' RS (th2' RS (th1 RS Thms.tfl_disjE))


227 
handle THM (msg, _, _) => raise RULES_ERR "DISJ_CASES" msg


228 
end;


229 


230 


231 
(*


232 
*


233 
*  A1 \/ ... \/ An [A1  M, ..., An  M]


234 
* 


235 
*  M


236 
*


237 
* Note. The list of theorems may be all jumbled up, so we have to


238 
* first organize it to align with the first argument (the disjunctive


239 
* theorem).


240 
**)


241 


242 
fun organize eq = (* a bit slow  analogous to insertion sort *)


243 
let fun extract a alist =


244 
let fun ex (_,[]) = raise RULES_ERR "organize" "not a permutation.1"


245 
 ex(left,h::t) = if (eq h a) then (h,rev left@t) else ex(h::left,t)


246 
in ex ([],alist)


247 
end


248 
fun place [] [] = []


249 
 place (a::rst) alist =


250 
let val (item,next) = extract a alist


251 
in item::place rst next


252 
end


253 
 place _ _ = raise RULES_ERR "organize" "not a permutation.2"


254 
in place


255 
end;


256 
(* freezeT expensive! *)


257 
fun DISJ_CASESL disjth thl =


258 
let val c = cconcl disjth


259 
fun eq th atm = exists (fn t => HOLogic.dest_Trueprop t


260 
aconv term_of atm)


261 
(#hyps(rep_thm th))


262 
val tml = D.strip_disj c


263 
fun DL th [] = raise RULES_ERR "DISJ_CASESL" "no cases"


264 
 DL th [th1] = PROVE_HYP th th1


265 
 DL th [th1,th2] = DISJ_CASES th th1 th2


266 
 DL th (th1::rst) =


267 
let val tm = #2(D.dest_disj(D.drop_prop(cconcl th)))


268 
in DISJ_CASES th th1 (DL (ASSUME tm) rst) end


269 
in DL (freezeT disjth) (organize eq tml thl)


270 
end;


271 


272 


273 
(*


274 
* Universals


275 
**)


276 
local (* this is fragile *)


277 
val {prop,sign,...} = rep_thm spec


278 
val x = hd (tl (term_vars prop))


279 
val (TVar (indx,_)) = type_of x


280 
val gspec = forall_intr (cterm_of sign x) spec


281 
in


282 
fun SPEC tm thm =


283 
let val {sign,T,...} = rep_cterm tm


284 
val gspec' = instantiate([(indx,ctyp_of sign T)],[]) gspec


285 
in


286 
thm RS (forall_elim tm gspec')


287 
end


288 
end;


289 


290 
fun SPEC_ALL thm = U.rev_itlist SPEC (#1(D.strip_forall(cconcl thm))) thm;


291 


292 
val ISPEC = SPEC


293 
val ISPECL = U.rev_itlist ISPEC;


294 


295 
(* Not optimized! Too complicated. *)


296 
local val {prop,sign,...} = rep_thm allI


297 
val [P] = add_term_vars (prop, [])


298 
fun cty_theta s = map (fn (i,ty) => (i, ctyp_of s ty))


299 
fun ctm_theta s = map (fn (i,tm2) =>


300 
let val ctm2 = cterm_of s tm2


301 
in (cterm_of s (Var(i,#T(rep_cterm ctm2))), ctm2)


302 
end)


303 
fun certify s (ty_theta,tm_theta) = (cty_theta s ty_theta,


304 
ctm_theta s tm_theta)


305 
in


306 
fun GEN v th =


307 
let val gth = forall_intr v th


308 
val {prop=Const("all",_)$Abs(x,ty,rst),sign,...} = rep_thm gth


309 
val P' = Abs(x,ty, HOLogic.dest_Trueprop rst) (* get rid of trueprop *)


310 
val tsig = #tsig(Sign.rep_sg sign)


311 
val theta = Pattern.match tsig (P,P')


312 
val allI2 = instantiate (certify sign theta) allI


313 
val thm = Thm.implies_elim allI2 gth


314 
val {prop = tp $ (A $ Abs(_,_,M)),sign,...} = rep_thm thm


315 
val prop' = tp $ (A $ Abs(x,ty,M))


316 
in ALPHA thm (cterm_of sign prop')


317 
end


318 
end;


319 


320 
val GENL = U.itlist GEN;


321 


322 
fun GEN_ALL thm =


323 
let val {prop,sign,...} = rep_thm thm


324 
val tycheck = cterm_of sign


325 
val vlist = map tycheck (add_term_vars (prop, []))


326 
in GENL vlist thm


327 
end;


328 


329 


330 
fun MATCH_MP th1 th2 =


331 
if (D.is_forall (D.drop_prop(cconcl th1)))


332 
then MATCH_MP (th1 RS spec) th2


333 
else MP th1 th2;


334 


335 


336 
(*


337 
* Existentials


338 
**)


339 


340 


341 


342 
(*


343 
* Existential elimination


344 
*


345 
* A1  ?x.t[x] , A2, "t[v]"  t'


346 
*  (variable v occurs nowhere)


347 
* A1 u A2  t'


348 
*


349 
**)


350 


351 
fun CHOOSE (fvar, exth) fact =


352 
let


353 
val lam = #2 (D.dest_comb (D.drop_prop (cconcl exth)))


354 
val redex = D.capply lam fvar


355 
val {sign, t = t$u,...} = Thm.rep_cterm redex


356 
val residue = Thm.cterm_of sign (betapply (t, u))


357 
in


358 
GEN fvar (DISCH residue fact) RS (exth RS Thms.choose_thm)


359 
handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg


360 
end;


361 


362 
local val {prop,sign,...} = rep_thm exI


363 
val [P,x] = term_vars prop


364 
in


365 
fun EXISTS (template,witness) thm =


366 
let val {prop,sign,...} = rep_thm thm


367 
val P' = cterm_of sign P


368 
val x' = cterm_of sign x


369 
val abstr = #2 (D.dest_comb template)


370 
in


371 
thm RS (cterm_instantiate[(P',abstr), (x',witness)] exI)


372 
handle THM (msg, _, _) => raise RULES_ERR "EXISTS" msg


373 
end


374 
end;


375 


376 
(*


377 
*


378 
* A  M


379 
*  [v_1,...,v_n]


380 
* A  ?v1...v_n. M


381 
*


382 
**)


383 


384 
fun EXISTL vlist th =


385 
U.itlist (fn v => fn thm => EXISTS(D.mk_exists(v,cconcl thm), v) thm)


386 
vlist th;


387 


388 


389 
(*


390 
*


391 
* A  M[x_1,...,x_n]


392 
*  [(x > y)_1,...,(x > y)_n]


393 
* A  ?y_1...y_n. M


394 
*


395 
**)


396 
(* Could be improved, but needs "subst_free" for certified terms *)


397 


398 
fun IT_EXISTS blist th =


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


400 
val tych = cterm_of sign


401 
val detype = #t o rep_cterm


402 
val blist' = map (fn (x,y) => (detype x, detype y)) blist


403 
fun ?v M = cterm_of sign (S.mk_exists{Bvar=v,Body = M})


404 


405 
in


406 
U.itlist (fn (b as (r1,r2)) => fn thm =>


407 
EXISTS(?r2(subst_free[b]


408 
(HOLogic.dest_Trueprop(#prop(rep_thm thm)))), tych r1)


409 
thm)


410 
blist' th


411 
end;


412 


413 
(*


414 
* Faster version, that fails for some as yet unknown reason


415 
* fun IT_EXISTS blist th =


416 
* let val {sign,...} = rep_thm th


417 
* val tych = cterm_of sign


418 
* fun detype (x,y) = ((#t o rep_cterm) x, (#t o rep_cterm) y)


419 
* in


420 
* fold (fn (b as (r1,r2), thm) =>


421 
* EXISTS(D.mk_exists(r2, tych(subst_free[detype b](#t(rep_cterm(cconcl thm))))),


422 
* r1) thm) blist th


423 
* end;


424 
**)


425 


426 
(*


427 
* Rewriting


428 
**)


429 


430 
fun SUBS thl =


431 
rewrite_rule (map (fn th => th RS eq_reflection handle THM _ => th) thl);


432 


433 
local fun rew_conv mss = MetaSimplifier.rewrite_cterm (true,false,false) (K(K None)) mss


434 
in


435 
fun simpl_conv ss thl ctm =


436 
rew_conv (MetaSimplifier.mss_of (#simps (MetaSimplifier.dest_mss (#mss (rep_ss ss))) @ thl)) ctm


437 
RS meta_eq_to_obj_eq


438 
end;


439 


440 
val RIGHT_ASSOC = rewrite_rule [Thms.disj_assoc];


441 


442 


443 


444 
(*


445 
* TERMINATION CONDITION EXTRACTION


446 
**)


447 


448 


449 
(* Object language quantifier, i.e., "!" *)


450 
fun Forall v M = S.mk_forall{Bvar=v, Body=M};


451 


452 


453 
(* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *)


454 
fun is_cong thm =


455 
let val {prop, ...} = rep_thm thm


456 
in case prop


457 
of (Const("==>",_)$(Const("Trueprop",_)$ _) $


458 
(Const("==",_) $ (Const ("Wellfounded_Recursion.cut",_) $ f $ R $ a $ x) $ _)) => false


459 
 _ => true


460 
end;


461 


462 


463 


464 
fun dest_equal(Const ("==",_) $


465 
(Const ("Trueprop",_) $ lhs)


466 
$ (Const ("Trueprop",_) $ rhs)) = {lhs=lhs, rhs=rhs}


467 
 dest_equal(Const ("==",_) $ lhs $ rhs) = {lhs=lhs, rhs=rhs}


468 
 dest_equal tm = S.dest_eq tm;


469 


470 
fun get_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm));


471 


472 
fun dest_all used (Const("all",_) $ (a as Abs _)) = S.dest_abs used a


473 
 dest_all _ _ = raise RULES_ERR "dest_all" "not a !!";


474 


475 
val is_all = can (dest_all []);


476 


477 
fun strip_all used fm =


478 
if (is_all fm)


479 
then let val ({Bvar, Body}, used') = dest_all used fm


480 
val (bvs, core, used'') = strip_all used' Body


481 
in ((Bvar::bvs), core, used'')


482 
end


483 
else ([], fm, used);


484 


485 
fun break_all(Const("all",_) $ Abs (_,_,body)) = body


486 
 break_all _ = raise RULES_ERR "break_all" "not a !!";


487 


488 
fun list_break_all(Const("all",_) $ Abs (s,ty,body)) =


489 
let val (L,core) = list_break_all body


490 
in ((s,ty)::L, core)


491 
end


492 
 list_break_all tm = ([],tm);


493 


494 
(*


495 
* Rename a term of the form


496 
*


497 
* !!x1 ...xn. x1=M1 ==> ... ==> xn=Mn


498 
* ==> ((%v1...vn. Q) x1 ... xn = g x1 ... xn.


499 
* to one of


500 
*


501 
* !!v1 ... vn. v1=M1 ==> ... ==> vn=Mn


502 
* ==> ((%v1...vn. Q) v1 ... vn = g v1 ... vn.


503 
*


504 
* This prevents name problems in extraction, and helps the result to read


505 
* better. There is a problem with varstructs, since they can introduce more


506 
* than n variables, and some extra reasoning needs to be done.


507 
**)


508 


509 
fun get ([],_,L) = rev L


510 
 get (ant::rst,n,L) =


511 
case (list_break_all ant)


512 
of ([],_) => get (rst, n+1,L)


513 
 (vlist,body) =>


514 
let val eq = Logic.strip_imp_concl body


515 
val (f,args) = S.strip_comb (get_lhs eq)


516 
val (vstrl,_) = S.strip_abs f


517 
val names = variantlist (map (#1 o dest_Free) vstrl,


518 
add_term_names(body, []))


519 
in get (rst, n+1, (names,n)::L) end


520 
handle TERM _ => get (rst, n+1, L)


521 
 U.ERR _ => get (rst, n+1, L);


522 


523 
(* Note: rename_params_rule counts from 1, not 0 *)


524 
fun rename thm =


525 
let val {prop,sign,...} = rep_thm thm


526 
val tych = cterm_of sign


527 
val ants = Logic.strip_imp_prems prop


528 
val news = get (ants,1,[])


529 
in


530 
U.rev_itlist rename_params_rule news thm


531 
end;


532 


533 


534 
(*


535 
* Betaconversion to the rhs of an equation (taken from hol90/drule.sml)


536 
**)


537 


538 
fun list_beta_conv tm =


539 
let fun rbeta th = Thm.transitive th (beta_conversion false (#2(D.dest_eq(cconcl th))))


540 
fun iter [] = Thm.reflexive tm


541 
 iter (v::rst) = rbeta (combination(iter rst) (Thm.reflexive v))


542 
in iter end;


543 


544 


545 
(*


546 
* Trace information for the rewriter


547 
**)


548 
val term_ref = ref[] : term list ref


549 
val mss_ref = ref [] : meta_simpset list ref;


550 
val thm_ref = ref [] : thm list ref;


551 
val tracing = ref false;


552 


553 
fun say s = if !tracing then writeln s else ();


554 


555 
fun print_thms s L =


556 
say (cat_lines (s :: map string_of_thm L));


557 


558 
fun print_cterms s L =


559 
say (cat_lines (s :: map string_of_cterm L));


560 


561 


562 
(*


563 
* General abstraction handlers, should probably go in USyntax.


564 
**)


565 
fun mk_aabs (vstr, body) =


566 
S.mk_abs {Bvar = vstr, Body = body}


567 
handle U.ERR _ => S.mk_pabs {varstruct = vstr, body = body};


568 


569 
fun list_mk_aabs (vstrl,tm) =


570 
U.itlist (fn vstr => fn tm => mk_aabs(vstr,tm)) vstrl tm;


571 


572 
fun dest_aabs used tm =


573 
let val ({Bvar,Body}, used') = S.dest_abs used tm


574 
in (Bvar, Body, used') end


575 
handle U.ERR _ =>


576 
let val {varstruct, body, used} = S.dest_pabs used tm


577 
in (varstruct, body, used) end;


578 


579 
fun strip_aabs used tm =


580 
let val (vstr, body, used') = dest_aabs used tm


581 
val (bvs, core, used'') = strip_aabs used' body


582 
in (vstr::bvs, core, used'') end


583 
handle U.ERR _ => ([], tm, used);


584 


585 
fun dest_combn tm 0 = (tm,[])


586 
 dest_combn tm n =


587 
let val {Rator,Rand} = S.dest_comb tm


588 
val (f,rands) = dest_combn Rator (n1)


589 
in (f,Rand::rands)


590 
end;


591 


592 


593 


594 


595 
local fun dest_pair M = let val {fst,snd} = S.dest_pair M in (fst,snd) end


596 
fun mk_fst tm =


597 
let val ty as Type("*", [fty,sty]) = type_of tm


598 
in Const ("fst", ty > fty) $ tm end


599 
fun mk_snd tm =


600 
let val ty as Type("*", [fty,sty]) = type_of tm


601 
in Const ("snd", ty > sty) $ tm end


602 
in


603 
fun XFILL tych x vstruct =


604 
let fun traverse p xocc L =


605 
if (is_Free p)


606 
then tych xocc::L


607 
else let val (p1,p2) = dest_pair p


608 
in traverse p1 (mk_fst xocc) (traverse p2 (mk_snd xocc) L)


609 
end


610 
in


611 
traverse vstruct x []


612 
end end;


613 


614 
(*


615 
* Replace a free tuple (vstr) by a universally quantified variable (a).


616 
* Note that the notion of "freeness" for a tuple is different than for a


617 
* variable: if variables in the tuple also occur in any other place than


618 
* an occurrences of the tuple, they aren't "free" (which is thus probably


619 
* the wrong word to use).


620 
**)


621 


622 
fun VSTRUCT_ELIM tych a vstr th =


623 
let val L = S.free_vars_lr vstr


624 
val bind1 = tych (HOLogic.mk_Trueprop (HOLogic.mk_eq(a,vstr)))


625 
val thm1 = implies_intr bind1 (SUBS [SYM(assume bind1)] th)


626 
val thm2 = forall_intr_list (map tych L) thm1


627 
val thm3 = forall_elim_list (XFILL tych a vstr) thm2


628 
in refl RS


629 
rewrite_rule [Thm.symmetric (surjective_pairing RS eq_reflection)] thm3


630 
end;


631 


632 
fun PGEN tych a vstr th =


633 
let val a1 = tych a


634 
val vstr1 = tych vstr


635 
in


636 
forall_intr a1


637 
(if (is_Free vstr)


638 
then cterm_instantiate [(vstr1,a1)] th


639 
else VSTRUCT_ELIM tych a vstr th)


640 
end;


641 


642 


643 
(*


644 
* Takes apart a paired betaredex, looking like "(\(x,y).N) vstr", into


645 
*


646 
* (([x,y],N),vstr)


647 
**)


648 
fun dest_pbeta_redex used M n =


649 
let val (f,args) = dest_combn M n


650 
val dummy = dest_aabs used f


651 
in (strip_aabs used f,args)


652 
end;


653 


654 
fun pbeta_redex M n = can (U.C (dest_pbeta_redex []) n) M;


655 


656 
fun dest_impl tm =


657 
let val ants = Logic.strip_imp_prems tm


658 
val eq = Logic.strip_imp_concl tm


659 
in (ants,get_lhs eq)


660 
end;


661 


662 
fun restricted t = is_some (S.find_term


663 
(fn (Const("Wellfounded_Recursion.cut",_)) =>true  _ => false)


664 
t)


665 


666 
fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =


667 
let val globals = func::G

10918

668 
val pbeta_reduce = simpl_conv empty_ss [split_conv RS eq_reflection];

10769

669 
val tc_list = ref[]: term list ref


670 
val dummy = term_ref := []


671 
val dummy = thm_ref := []


672 
val dummy = mss_ref := []


673 
val cut_lemma' = cut_lemma RS eq_reflection


674 
fun prover used mss thm =


675 
let fun cong_prover mss thm =


676 
let val dummy = say "cong_prover:"


677 
val cntxt = prems_of_mss mss


678 
val dummy = print_thms "cntxt:" cntxt


679 
val dummy = say "cong rule:"


680 
val dummy = say (string_of_thm thm)


681 
val dummy = thm_ref := (thm :: !thm_ref)


682 
val dummy = mss_ref := (mss :: !mss_ref)


683 
(* Unquantified eliminate *)


684 
fun uq_eliminate (thm,imp,sign) =


685 
let val tych = cterm_of sign


686 
val dummy = print_cterms "To eliminate:" [tych imp]


687 
val ants = map tych (Logic.strip_imp_prems imp)


688 
val eq = Logic.strip_imp_concl imp


689 
val lhs = tych(get_lhs eq)


690 
val mss' = add_prems(mss, map ASSUME ants)


691 
val lhs_eq_lhs1 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used) mss' lhs


692 
handle U.ERR _ => Thm.reflexive lhs


693 
val dummy = print_thms "proven:" [lhs_eq_lhs1]


694 
val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1


695 
val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq


696 
in


697 
lhs_eeq_lhs2 COMP thm


698 
end


699 
fun pq_eliminate (thm,sign,vlist,imp_body,lhs_eq) =


700 
let val ((vstrl, _, used'), args) = dest_pbeta_redex used lhs_eq (length vlist)


701 
val dummy = assert (forall (op aconv)


702 
(ListPair.zip (vlist, args)))


703 
"assertion failed in CONTEXT_REWRITE_RULE"


704 
val imp_body1 = subst_free (ListPair.zip (args, vstrl))


705 
imp_body


706 
val tych = cterm_of sign


707 
val ants1 = map tych (Logic.strip_imp_prems imp_body1)


708 
val eq1 = Logic.strip_imp_concl imp_body1


709 
val Q = get_lhs eq1


710 
val QeqQ1 = pbeta_reduce (tych Q)


711 
val Q1 = #2(D.dest_eq(cconcl QeqQ1))


712 
val mss' = add_prems(mss, map ASSUME ants1)


713 
val Q1eeqQ2 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used') mss' Q1


714 
handle U.ERR _ => Thm.reflexive Q1


715 
val Q2 = #2 (Logic.dest_equals (#prop(rep_thm Q1eeqQ2)))


716 
val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl))


717 
val Q2eeqQ3 = Thm.symmetric(pbeta_reduce Q3 RS eq_reflection)


718 
val thA = Thm.transitive(QeqQ1 RS eq_reflection) Q1eeqQ2


719 
val QeeqQ3 = Thm.transitive thA Q2eeqQ3 handle THM _ =>


720 
((Q2eeqQ3 RS meta_eq_to_obj_eq)


721 
RS ((thA RS meta_eq_to_obj_eq) RS trans))


722 
RS eq_reflection


723 
val impth = implies_intr_list ants1 QeeqQ3


724 
val impth1 = impth RS meta_eq_to_obj_eq


725 
(* Need to abstract *)


726 
val ant_th = U.itlist2 (PGEN tych) args vstrl impth1


727 
in ant_th COMP thm


728 
end


729 
fun q_eliminate (thm,imp,sign) =


730 
let val (vlist, imp_body, used') = strip_all used imp


731 
val (ants,Q) = dest_impl imp_body


732 
in if (pbeta_redex Q) (length vlist)


733 
then pq_eliminate (thm,sign,vlist,imp_body,Q)


734 
else


735 
let val tych = cterm_of sign


736 
val ants1 = map tych ants


737 
val mss' = add_prems(mss, map ASSUME ants1)


738 
val Q_eeq_Q1 = MetaSimplifier.rewrite_cterm


739 
(false,true,false) (prover used') mss' (tych Q)


740 
handle U.ERR _ => Thm.reflexive (tych Q)


741 
val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1


742 
val lhs_eq_lhs2 = lhs_eeq_lhs2 RS meta_eq_to_obj_eq


743 
val ant_th = forall_intr_list(map tych vlist)lhs_eq_lhs2


744 
in


745 
ant_th COMP thm


746 
end end


747 


748 
fun eliminate thm =


749 
case (rep_thm thm)


750 
of {prop = (Const("==>",_) $ imp $ _), sign, ...} =>


751 
eliminate


752 
(if not(is_all imp)


753 
then uq_eliminate (thm,imp,sign)


754 
else q_eliminate (thm,imp,sign))


755 
(* Assume that the leading constant is ==, *)


756 
 _ => thm (* if it is not a ==> *)


757 
in Some(eliminate (rename thm)) end


758 
handle U.ERR _ => None (* FIXME handle THM as well?? *)


759 


760 
fun restrict_prover mss thm =


761 
let val dummy = say "restrict_prover:"


762 
val cntxt = rev(prems_of_mss mss)


763 
val dummy = print_thms "cntxt:" cntxt


764 
val {prop = Const("==>",_) $ (Const("Trueprop",_) $ A) $ _,


765 
sign,...} = rep_thm thm


766 
fun genl tm = let val vlist = gen_rems (op aconv)


767 
(add_term_frees(tm,[]), globals)


768 
in U.itlist Forall vlist tm


769 
end


770 
(*


771 
* This actually isn't quite right, since it will think that


772 
* notfully applied occs. of "f" in the context mean that the


773 
* current call is nested. The real solution is to pass in a


774 
* term "f v1..vn" which is a pattern that any full application


775 
* of "f" will match.


776 
**)


777 
val func_name = #1(dest_Const func)


778 
fun is_func (Const (name,_)) = (name = func_name)


779 
 is_func _ = false


780 
val rcontext = rev cntxt


781 
val cncl = HOLogic.dest_Trueprop o #prop o rep_thm


782 
val antl = case rcontext of [] => []


783 
 _ => [S.list_mk_conj(map cncl rcontext)]


784 
val TC = genl(S.list_mk_imp(antl, A))


785 
val dummy = print_cterms "func:" [cterm_of sign func]


786 
val dummy = print_cterms "TC:"


787 
[cterm_of sign (HOLogic.mk_Trueprop TC)]


788 
val dummy = tc_list := (TC :: !tc_list)


789 
val nestedp = is_some (S.find_term is_func TC)


790 
val dummy = if nestedp then say "nested" else say "not_nested"


791 
val dummy = term_ref := ([func,TC]@(!term_ref))


792 
val th' = if nestedp then raise RULES_ERR "solver" "nested function"


793 
else let val cTC = cterm_of sign


794 
(HOLogic.mk_Trueprop TC)


795 
in case rcontext of


796 
[] => SPEC_ALL(ASSUME cTC)


797 
 _ => MP (SPEC_ALL (ASSUME cTC))


798 
(LIST_CONJ rcontext)


799 
end


800 
val th'' = th' RS thm


801 
in Some (th'')


802 
end handle U.ERR _ => None (* FIXME handle THM as well?? *)


803 
in


804 
(if (is_cong thm) then cong_prover else restrict_prover) mss thm


805 
end


806 
val ctm = cprop_of th


807 
val names = add_term_names (term_of ctm, [])


808 
val th1 = MetaSimplifier.rewrite_cterm(false,true,false)


809 
(prover names) (add_congs(mss_of [cut_lemma'], congs)) ctm


810 
val th2 = equal_elim th1 th


811 
in


812 
(th2, filter (not o restricted) (!tc_list))


813 
end;


814 


815 


816 
fun prove (ptm, tac) =


817 
let val result =


818 
Library.transform_error (fn () =>


819 
Goals.prove_goalw_cterm [] ptm (fn _ => [tac])) ()


820 
handle ERROR_MESSAGE msg => (warning msg; raise RULES_ERR "prove" msg)


821 
in #1 (freeze_thaw result) end;


822 


823 


824 
end;
