6498

1 
(* Title: TFL/rules


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 


10 
structure Rules : Rules_sig =


11 
struct


12 


13 
open Utils;


14 


15 
structure USyntax = USyntax;


16 
structure S = USyntax;


17 
structure U = Utils;


18 
structure D = Dcterm;


19 


20 


21 
fun RULES_ERR{func,mesg} = Utils.ERR{module = "Rules",func=func,mesg=mesg};


22 


23 


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


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


26 


27 
fun dest_thm thm =


28 
let val {prop,hyps,...} = rep_thm thm


29 
in (map HOLogic.dest_Trueprop hyps, HOLogic.dest_Trueprop prop)


30 
end;


31 


32 


33 


34 
(* Inference rules *)


35 


36 
(*


37 
* Equality (one step)


38 
**)


39 
fun REFL tm = Thm.reflexive tm RS meta_eq_to_obj_eq;


40 
fun SYM thm = thm RS sym;


41 


42 
fun ALPHA thm ctm1 =


43 
let val ctm2 = cprop_of thm


44 
val ctm2_eq = reflexive ctm2


45 
val ctm1_eq = reflexive ctm1


46 
in equal_elim (transitive ctm2_eq ctm1_eq) thm


47 
end;


48 

7262

49 
fun rbeta th =


50 
case Dcterm.strip_comb (cconcl th)


51 
of (eeq,[l,r]) => transitive th (beta_conversion r)


52 
 _ => raise RULES_ERR{func="rbeta", mesg =""};

6498

53 


54 
(*


55 
* typ instantiation


56 
**)


57 
fun INST_TYPE blist thm =


58 
let val {sign,...} = rep_thm thm


59 
val blist' = map (fn (TVar(idx,_), B) => (idx, ctyp_of sign B)) blist


60 
in Thm.instantiate (blist',[]) thm


61 
end


62 
handle _ => raise RULES_ERR{func = "INST_TYPE", mesg = ""};


63 


64 


65 
(*


66 
* Implication and the assumption list


67 
*


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


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


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


71 
**)


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


73 


74 


75 
(*


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


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


78 
**)


79 
fun MP th1 th2 = th2 RS (th1 RS mp);


80 


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


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


83 


84 
fun DISCH_ALL thm = Utils.itlist DISCH (#hyps (crep_thm thm)) thm;


85 


86 


87 
fun FILTER_DISCH_ALL P thm =


88 
let fun check tm = U.holds P (#t(rep_cterm tm))


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


90 
(chyps thm, thm)


91 
end;


92 


93 
(* freezeT expensive! *)


94 
fun UNDISCH thm =


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


96 
in implies_elim (thm RS mp) (ASSUME tm)


97 
end


98 
handle _ => raise RULES_ERR{func = "UNDISCH", mesg = ""};


99 


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


101 


102 
local val [p1,p2] = goal HOL.thy "(A>B) ==> (B > C) ==> (A>C)"


103 
val dummy = by (rtac impI 1)


104 
val dummy = by (rtac (p2 RS mp) 1)


105 
val dummy = by (rtac (p1 RS mp) 1)


106 
val dummy = by (assume_tac 1)


107 
val imp_trans = result()


108 
in


109 
fun IMP_TRANS th1 th2 = th2 RS (th1 RS imp_trans)


110 
end;


111 


112 
(*


113 
* Conjunction


114 
**)


115 
fun CONJUNCT1 thm = (thm RS conjunct1)


116 
fun CONJUNCT2 thm = (thm RS conjunct2);


117 
fun CONJUNCTS th = (CONJUNCTS (CONJUNCT1 th) @ CONJUNCTS (CONJUNCT2 th))


118 
handle _ => [th];


119 


120 
fun LIST_CONJ [] = raise RULES_ERR{func = "LIST_CONJ", mesg = "empty list"}


121 
 LIST_CONJ [th] = th


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


123 


124 


125 
(*


126 
* Disjunction


127 
**)


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


129 
val [P,Q] = term_vars prop


130 
val disj1 = forall_intr (cterm_of sign Q) disjI1


131 
in


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


133 
end;


134 


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


136 
val [P,Q] = term_vars prop


137 
val disj2 = forall_intr (cterm_of sign P) disjI2


138 
in


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


140 
end;


141 


142 


143 
(*


144 
*


145 
* A1  M1, ..., An  Mn


146 
* 


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


148 
*


149 
**)


150 


151 


152 
fun EVEN_ORS thms =


153 
let fun blue ldisjs [] _ = []


154 
 blue ldisjs (th::rst) rdisjs =


155 
let val tail = tl rdisjs


156 
val rdisj_tl = D.list_mk_disj tail


157 
in itlist DISJ2 ldisjs (DISJ1 th rdisj_tl)


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


159 
end handle _ => [itlist DISJ2 ldisjs th]


160 
in


161 
blue [] thms (map cconcl thms)


162 
end;


163 


164 


165 
(*


166 
*


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


168 
* 


169 
* A U B U C  R


170 
*


171 
**)


172 
local val [p1,p2,p3] = goal HOL.thy "(P  Q) ==> (P > R) ==> (Q > R) ==> R"


173 
val dummy = by (rtac (p1 RS disjE) 1)


174 
val dummy = by (rtac (p2 RS mp) 1)


175 
val dummy = by (assume_tac 1)


176 
val dummy = by (rtac (p3 RS mp) 1)


177 
val dummy = by (assume_tac 1)


178 
val tfl_exE = result()


179 
in


180 
fun DISJ_CASES th1 th2 th3 =


181 
let val c = D.drop_prop(cconcl th1)


182 
val (disj1,disj2) = D.dest_disj c


183 
val th2' = DISCH disj1 th2


184 
val th3' = DISCH disj2 th3


185 
in


186 
th3' RS (th2' RS (th1 RS tfl_exE))


187 
end


188 
end;


189 


190 


191 
(*


192 
*


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


194 
* 


195 
*  M


196 
*


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


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


199 
* theorem).


200 
**)


201 


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


203 
let fun extract a alist =


204 
let fun ex (_,[]) = raise RULES_ERR{func = "organize",


205 
mesg = "not a permutation.1"}


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


207 
in ex ([],alist)


208 
end


209 
fun place [] [] = []


210 
 place (a::rst) alist =


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


212 
in item::place rst next


213 
end


214 
 place _ _ = raise RULES_ERR{func = "organize",


215 
mesg = "not a permutation.2"}


216 
in place


217 
end;


218 
(* freezeT expensive! *)


219 
fun DISJ_CASESL disjth thl =


220 
let val c = cconcl disjth


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


222 
aconv term_of atm)


223 
(#hyps(rep_thm th))


224 
val tml = D.strip_disj c


225 
fun DL th [] = raise RULES_ERR{func="DISJ_CASESL",mesg="no cases"}


226 
 DL th [th1] = PROVE_HYP th th1


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


228 
 DL th (th1::rst) =


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


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


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


232 
end;


233 


234 


235 
(*


236 
* Universals


237 
**)


238 
local (* this is fragile *)


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


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


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


242 
val gspec = forall_intr (cterm_of sign x) spec


243 
in


244 
fun SPEC tm thm =


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


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


247 
in


248 
thm RS (forall_elim tm gspec')


249 
end


250 
end;


251 


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


253 


254 
val ISPEC = SPEC


255 
val ISPECL = rev_itlist ISPEC;


256 


257 
(* Not optimized! Too complicated. *)


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


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


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


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


262 
let val ctm2 = cterm_of s tm2


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


264 
end)


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


266 
ctm_theta s tm_theta)


267 
in


268 
fun GEN v th =


269 
let val gth = forall_intr v th


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


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


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


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


274 
val allI2 = instantiate (certify sign theta) allI


275 
val thm = implies_elim allI2 gth


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


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


278 
in ALPHA thm (cterm_of sign prop')


279 
end


280 
end;


281 


282 
val GENL = itlist GEN;


283 


284 
fun GEN_ALL thm =


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


286 
val tycheck = cterm_of sign


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


288 
in GENL vlist thm


289 
end;


290 


291 


292 
fun MATCH_MP th1 th2 =


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


294 
then MATCH_MP (th1 RS spec) th2


295 
else MP th1 th2;


296 


297 


298 
(*


299 
* Existentials


300 
**)


301 


302 


303 


304 
(*


305 
* Existential elimination


306 
*


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


308 
*  (variable v occurs nowhere)


309 
* A1 u A2  t'


310 
*


311 
**)


312 


313 
local val [p1,p2] = goal HOL.thy "(? x. P x) ==> (!x. P x > Q) ==> Q"


314 
val dummy = by (rtac (p1 RS exE) 1)


315 
val dummy = by (rtac ((p2 RS allE) RS mp) 1)


316 
val dummy = by (assume_tac 2)


317 
val dummy = by (assume_tac 1)


318 
val choose_thm = result()


319 
in


320 
fun CHOOSE(fvar,exth) fact =


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


322 
val redex = capply lam fvar


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


324 
val residue = cterm_of sign (betapply(t,u))


325 
in GEN fvar (DISCH residue fact) RS (exth RS choose_thm)


326 
end


327 
end;


328 


329 


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


331 
val [P,x] = term_vars prop


332 
in


333 
fun EXISTS (template,witness) thm =


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


335 
val P' = cterm_of sign P


336 
val x' = cterm_of sign x


337 
val abstr = #2(dest_comb template)


338 
in


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


340 
end


341 
end;


342 


343 
(*


344 
*


345 
* A  M


346 
*  [v_1,...,v_n]


347 
* A  ?v1...v_n. M


348 
*


349 
**)


350 


351 
fun EXISTL vlist th =


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


353 
vlist th;


354 


355 


356 
(*


357 
*


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


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


360 
* A  ?y_1...y_n. M


361 
*


362 
**)


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


364 


365 
fun IT_EXISTS blist th =


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


367 
val tych = cterm_of sign


368 
val detype = #t o rep_cterm


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


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


371 


372 
in


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


374 
EXISTS(?r2(subst_free[b]


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


376 
thm)


377 
blist' th


378 
end;


379 


380 
(*


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


382 
* fun IT_EXISTS blist th =


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


384 
* val tych = cterm_of sign


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


386 
* in


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


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


389 
* r1) thm) blist th


390 
* end;


391 
**)


392 


393 
(*


394 
* Rewriting


395 
**)


396 


397 
fun SUBS thl =


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


399 


400 
local fun rew_conv mss = Thm.rewrite_cterm (true,false,false) mss (K(K None))


401 
in


402 
fun simpl_conv ss thl ctm =


403 
rew_conv (Thm.mss_of (#simps (Thm.dest_mss (#mss (rep_ss ss))) @ thl)) ctm


404 
RS meta_eq_to_obj_eq


405 
end;


406 


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


408 
in


409 
val RIGHT_ASSOC = rewrite_rule [prover"((ab)c) = (a(bc))" RS eq_reflection]


410 
val ASM = refl RS iffD1


411 
end;


412 


413 


414 


415 


416 
(*


417 
* TERMINATION CONDITION EXTRACTION


418 
**)


419 


420 


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


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


423 


424 


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


426 
fun is_cong thm =


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


428 
in case prop


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


430 
(Const("==",_) $ (Const ("cut",_) $ f $ R $ a $ x) $ _)) => false


431 
 _ => true


432 
end;


433 


434 


435 


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


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


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


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


440 
 dest_equal tm = S.dest_eq tm;


441 


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


443 


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


445 
 dest_all _ = raise RULES_ERR{func = "dest_all", mesg = "not a !!"};


446 


447 
val is_all = Utils.can dest_all;


448 


449 
fun strip_all fm =


450 
if (is_all fm)


451 
then let val {Bvar,Body} = dest_all fm


452 
val (bvs,core) = strip_all Body


453 
in ((Bvar::bvs), core)


454 
end


455 
else ([],fm);


456 


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


458 
 break_all _ = raise RULES_ERR{func = "break_all", mesg = "not a !!"};


459 


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


461 
let val (L,core) = list_break_all body


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


463 
end


464 
 list_break_all tm = ([],tm);


465 


466 
(*


467 
* Rename a term of the form


468 
*


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


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


471 
* to one of


472 
*


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


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


475 
*


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


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


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


479 
**)


480 


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


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


483 
case (list_break_all ant)


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


485 
 (vlist,body) =>


486 
let val eq = Logic.strip_imp_concl body


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


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


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


490 
add_term_names(body, []))


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


492 
end handle _ => get (rst, n+1, L);


493 


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


495 
fun rename thm =


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


497 
val tych = cterm_of sign


498 
val ants = Logic.strip_imp_prems prop


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


500 
in


501 
U.rev_itlist rename_params_rule news thm


502 
end;


503 


504 


505 
(*


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


507 
**)


508 


509 
fun list_beta_conv tm =


510 
let fun rbeta th = transitive th (beta_conversion(#2(D.dest_eq(cconcl th))))


511 
fun iter [] = reflexive tm


512 
 iter (v::rst) = rbeta (combination(iter rst) (reflexive v))


513 
in iter end;


514 


515 


516 
(*


517 
* Trace information for the rewriter


518 
**)


519 
val term_ref = ref[] : term list ref


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


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


522 
val tracing = ref false;


523 


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


525 


526 
fun print_thms s L =


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


528 


529 
fun print_cterms s L =


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


531 


532 


533 
(*


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


535 
**)


536 
fun mk_aabs(vstr,body) = S.mk_abs{Bvar=vstr,Body=body}


537 
handle _ => S.mk_pabs{varstruct = vstr, body = body};


538 


539 
fun list_mk_aabs (vstrl,tm) =


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


541 


542 
fun dest_aabs tm =


543 
let val {Bvar,Body} = S.dest_abs tm


544 
in (Bvar,Body)


545 
end handle _ => let val {varstruct,body} = S.dest_pabs tm


546 
in (varstruct,body)


547 
end;


548 


549 
fun strip_aabs tm =


550 
let val (vstr,body) = dest_aabs tm


551 
val (bvs, core) = strip_aabs body


552 
in (vstr::bvs, core)


553 
end


554 
handle _ => ([],tm);


555 


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


557 
 dest_combn tm n =


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


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


560 
in (f,Rand::rands)


561 
end;


562 


563 


564 


565 


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


567 
fun mk_fst tm =


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


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


570 
fun mk_snd tm =


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


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


573 
in


574 
fun XFILL tych x vstruct =


575 
let fun traverse p xocc L =


576 
if (is_Free p)


577 
then tych xocc::L


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


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


580 
end


581 
in


582 
traverse vstruct x []


583 
end end;


584 


585 
(*


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


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


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


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


590 
* the wrong word to use).


591 
**)


592 


593 
fun VSTRUCT_ELIM tych a vstr th =


594 
let val L = S.free_vars_lr vstr


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


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


597 
val thm2 = forall_intr_list (map tych L) thm1


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


599 
in refl RS


600 
rewrite_rule[symmetric (surjective_pairing RS eq_reflection)] thm3


601 
end;


602 


603 
fun PGEN tych a vstr th =


604 
let val a1 = tych a


605 
val vstr1 = tych vstr


606 
in


607 
forall_intr a1


608 
(if (is_Free vstr)


609 
then cterm_instantiate [(vstr1,a1)] th


610 
else VSTRUCT_ELIM tych a vstr th)


611 
end;


612 


613 


614 
(*


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


616 
*


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


618 
**)


619 
fun dest_pbeta_redex M n =


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


621 
val dummy = dest_aabs f


622 
in (strip_aabs f,args)


623 
end;


624 


625 
fun pbeta_redex M n = U.can (U.C dest_pbeta_redex n) M;


626 


627 
fun dest_impl tm =


628 
let val ants = Logic.strip_imp_prems tm


629 
val eq = Logic.strip_imp_concl tm


630 
in (ants,get_lhs eq)


631 
end;


632 


633 
fun restricted t = is_some (S.find_term


634 
(fn (Const("cut",_)) =>true  _ => false)


635 
t)


636 


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


638 
let val globals = func::G


639 
val pbeta_reduce = simpl_conv empty_ss [split RS eq_reflection];


640 
val tc_list = ref[]: term list ref


641 
val dummy = term_ref := []


642 
val dummy = thm_ref := []


643 
val dummy = mss_ref := []


644 
val cut_lemma' = cut_lemma RS eq_reflection


645 
fun prover mss thm =


646 
let fun cong_prover mss thm =


647 
let val dummy = say "cong_prover:"


648 
val cntxt = prems_of_mss mss


649 
val dummy = print_thms "cntxt:" cntxt


650 
val dummy = say "cong rule:"


651 
val dummy = say (string_of_thm thm)


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


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


654 
(* Unquantified eliminate *)


655 
fun uq_eliminate (thm,imp,sign) =


656 
let val tych = cterm_of sign


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


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


659 
val eq = Logic.strip_imp_concl imp


660 
val lhs = tych(get_lhs eq)


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


662 
val lhs_eq_lhs1 = Thm.rewrite_cterm(false,true,false)mss' prover lhs


663 
handle _ => reflexive lhs


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


665 
val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1


666 
val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq


667 
in


668 
lhs_eeq_lhs2 COMP thm


669 
end


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


671 
let val ((vstrl,_),args) = dest_pbeta_redex lhs_eq(length vlist)


672 
val dummy = assert (forall (op aconv)


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


674 
"assertion failed in CONTEXT_REWRITE_RULE"


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


676 
imp_body


677 
val tych = cterm_of sign


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


679 
val eq1 = Logic.strip_imp_concl imp_body1


680 
val Q = get_lhs eq1


681 
val QeqQ1 = pbeta_reduce (tych Q)


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


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


684 
val Q1eeqQ2 = Thm.rewrite_cterm (false,true,false) mss' prover Q1


685 
handle _ => reflexive Q1


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


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


688 
val Q2eeqQ3 = symmetric(pbeta_reduce Q3 RS eq_reflection)


689 
val thA = transitive(QeqQ1 RS eq_reflection) Q1eeqQ2


690 
val QeeqQ3 = transitive thA Q2eeqQ3 handle _ =>


691 
((Q2eeqQ3 RS meta_eq_to_obj_eq)


692 
RS ((thA RS meta_eq_to_obj_eq) RS trans))


693 
RS eq_reflection


694 
val impth = implies_intr_list ants1 QeeqQ3


695 
val impth1 = impth RS meta_eq_to_obj_eq


696 
(* Need to abstract *)


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


698 
in ant_th COMP thm


699 
end


700 
fun q_eliminate (thm,imp,sign) =


701 
let val (vlist,imp_body) = strip_all imp


702 
val (ants,Q) = dest_impl imp_body


703 
in if (pbeta_redex Q) (length vlist)


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


705 
else


706 
let val tych = cterm_of sign


707 
val ants1 = map tych ants


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


709 
val Q_eeq_Q1 = Thm.rewrite_cterm(false,true,false) mss'


710 
prover (tych Q)


711 
handle _ => reflexive (tych Q)


712 
val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1


713 
val lhs_eq_lhs2 = lhs_eeq_lhs2 RS meta_eq_to_obj_eq


714 
val ant_th = forall_intr_list(map tych vlist)lhs_eq_lhs2


715 
in


716 
ant_th COMP thm


717 
end end


718 


719 
fun eliminate thm =


720 
case (rep_thm thm)


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


722 
eliminate


723 
(if not(is_all imp)


724 
then uq_eliminate (thm,imp,sign)


725 
else q_eliminate (thm,imp,sign))


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


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


728 
in Some(eliminate (rename thm))


729 
end handle _ => None


730 


731 
fun restrict_prover mss thm =


732 
let val dummy = say "restrict_prover:"


733 
val cntxt = rev(prems_of_mss mss)


734 
val dummy = print_thms "cntxt:" cntxt


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


736 
sign,...} = rep_thm thm


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


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


739 
in U.itlist Forall vlist tm


740 
end


741 
(*


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


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


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


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


746 
* of "f" will match.


747 
**)


748 
val func_name = #1(dest_Const func)


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


750 
 is_func _ = false


751 
val rcontext = rev cntxt


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


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


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


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


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


757 
val dummy = print_cterms "TC:"


758 
[cterm_of sign (HOLogic.mk_Trueprop TC)]


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


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


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


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


763 
val th' = if nestedp then raise RULES_ERR{func = "solver",


764 
mesg = "nested function"}


765 
else let val cTC = cterm_of sign


766 
(HOLogic.mk_Trueprop TC)


767 
in case rcontext of


768 
[] => SPEC_ALL(ASSUME cTC)


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


770 
(LIST_CONJ rcontext)


771 
end


772 
val th'' = th' RS thm


773 
in Some (th'')


774 
end handle _ => None


775 
in


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


777 
end


778 
val ctm = cprop_of th

7262

779 
val th1 = Thm.rewrite_cterm(false,true,false)


780 
(add_congs(mss_of [cut_lemma'], congs))

6498

781 
prover ctm


782 
val th2 = equal_elim th1 th


783 
in


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


785 
end;


786 


787 


788 


789 
fun prove (ptm,tac) =


790 
#1 (freeze_thaw (prove_goalw_cterm [] ptm (fn _ => [tac])));


791 


792 


793 
end; (* Rules *)
