0

1 
(* Title: thm


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1991 University of Cambridge


5 


6 
The abstract types "theory" and "thm"


7 
*)


8 


9 
signature THM =


10 
sig


11 
structure Envir : ENVIR


12 
structure Sequence : SEQUENCE


13 
structure Sign : SIGN


14 
type meta_simpset


15 
type theory


16 
type thm


17 
exception THM of string * int * thm list


18 
exception THEORY of string * theory list


19 
exception SIMPLIFIER of string * thm


20 
val abstract_rule: string > Sign.cterm > thm > thm


21 
val add_congs: meta_simpset * thm list > meta_simpset


22 
val add_prems: meta_simpset * thm list > meta_simpset


23 
val add_simps: meta_simpset * thm list > meta_simpset


24 
val assume: Sign.cterm > thm


25 
val assumption: int > thm > thm Sequence.seq


26 
val axioms_of: theory > (string * thm) list


27 
val beta_conversion: Sign.cterm > thm


28 
val bicompose: bool > bool * thm * int > int > thm > thm Sequence.seq


29 
val biresolution: bool > (bool*thm)list > int > thm > thm Sequence.seq


30 
val combination: thm > thm > thm


31 
val concl_of: thm > term


32 
val dest_state: thm * int > (term*term)list * term list * term * term


33 
val empty_mss: meta_simpset


34 
val eq_assumption: int > thm > thm


35 
val equal_intr: thm > thm > thm


36 
val equal_elim: thm > thm > thm


37 
val extend_theory: theory > string


38 
> (class * class list) list * sort


39 
* (string list * int)list


40 
* (string list * (sort list * class))list


41 
* (string list * string)list * Sign.Syntax.sext option


42 
> (string*string)list > theory


43 
val extensional: thm > thm


44 
val flexflex_rule: thm > thm Sequence.seq


45 
val flexpair_def: thm


46 
val forall_elim: Sign.cterm > thm > thm


47 
val forall_intr: Sign.cterm > thm > thm


48 
val freezeT: thm > thm


49 
val get_axiom: theory > string > thm


50 
val implies_elim: thm > thm > thm


51 
val implies_intr: Sign.cterm > thm > thm


52 
val implies_intr_hyps: thm > thm


53 
val instantiate: (indexname*Sign.ctyp)list * (Sign.cterm*Sign.cterm)list


54 
> thm > thm


55 
val lift_rule: (thm * int) > thm > thm


56 
val merge_theories: theory * theory > theory


57 
val mk_rews_of_mss: meta_simpset > thm > thm list


58 
val mss_of: thm list > meta_simpset


59 
val nprems_of: thm > int


60 
val parents_of: theory > theory list


61 
val prems_of: thm > term list


62 
val prems_of_mss: meta_simpset > thm list


63 
val pure_thy: theory


64 
val reflexive: Sign.cterm > thm


65 
val rename_params_rule: string list * int > thm > thm


66 
val rep_thm: thm > {prop: term, hyps: term list, maxidx: int, sign: Sign.sg}


67 
val rewrite_cterm: meta_simpset > (meta_simpset > thm > thm option)


68 
> Sign.cterm > thm


69 
val set_mk_rews: meta_simpset * (thm > thm list) > meta_simpset


70 
val sign_of: theory > Sign.sg


71 
val syn_of: theory > Sign.Syntax.syntax


72 
val stamps_of_thm: thm > string ref list


73 
val stamps_of_thy: theory > string ref list


74 
val symmetric: thm > thm


75 
val tpairs_of: thm > (term*term)list


76 
val trace_simp: bool ref


77 
val transitive: thm > thm > thm


78 
val trivial: Sign.cterm > thm


79 
val varifyT: thm > thm


80 
end;


81 


82 


83 


84 
functor ThmFun (structure Logic: LOGIC and Unify: UNIFY and Pattern:PATTERN


85 
and Net:NET


86 
sharing type Pattern.type_sig = Unify.Sign.Type.type_sig)


87 
: THM =


88 
struct


89 
structure Sequence = Unify.Sequence;


90 
structure Envir = Unify.Envir;


91 
structure Sign = Unify.Sign;


92 
structure Type = Sign.Type;


93 
structure Syntax = Sign.Syntax;


94 
structure Symtab = Sign.Symtab;


95 


96 


97 
(*Metatheorems*)


98 
datatype thm = Thm of


99 
{sign: Sign.sg, maxidx: int, hyps: term list, prop: term};


100 


101 
fun rep_thm (Thm x) = x;


102 


103 
(*Errors involving theorems*)


104 
exception THM of string * int * thm list;


105 


106 
(*maps objectrule to tpairs *)


107 
fun tpairs_of (Thm{prop,...}) = #1 (Logic.strip_flexpairs prop);


108 


109 
(*maps objectrule to premises *)


110 
fun prems_of (Thm{prop,...}) =


111 
Logic.strip_imp_prems (Logic.skip_flexpairs prop);


112 


113 
(*counts premises in a rule*)


114 
fun nprems_of (Thm{prop,...}) =


115 
Logic.count_prems (Logic.skip_flexpairs prop, 0);


116 


117 
(*maps objectrule to conclusion *)


118 
fun concl_of (Thm{prop,...}) = Logic.strip_imp_concl prop;


119 


120 
(*Stamps associated with a signature*)


121 
val stamps_of_thm = #stamps o Sign.rep_sg o #sign o rep_thm;


122 


123 
(*Theories. There is one pure theory.


124 
A theory can be extended. Two theories can be merged.*)


125 
datatype theory =


126 
Pure of {sign: Sign.sg}


127 
 Extend of {sign: Sign.sg, axioms: thm Symtab.table, thy: theory}


128 
 Merge of {sign: Sign.sg, thy1: theory, thy2: theory};


129 


130 
(*Errors involving theories*)


131 
exception THEORY of string * theory list;


132 


133 
fun sign_of (Pure {sign}) = sign


134 
 sign_of (Extend {sign,...}) = sign


135 
 sign_of (Merge {sign,...}) = sign;


136 


137 
val syn_of = #syn o Sign.rep_sg o sign_of;


138 


139 
(*return the axioms of a theory and its ancestors*)


140 
fun axioms_of (Pure _) = []


141 
 axioms_of (Extend{axioms,thy,...}) = Symtab.alist_of axioms


142 
 axioms_of (Merge{thy1,thy2,...}) = axioms_of thy1 @ axioms_of thy2;


143 


144 
(*return the immediate ancestors  also distinguishes the kinds of theories*)


145 
fun parents_of (Pure _) = []


146 
 parents_of (Extend{thy,...}) = [thy]


147 
 parents_of (Merge{thy1,thy2,...}) = [thy1,thy2];


148 


149 


150 
(*Merge theories of two theorems. Raise exception if incompatible.


151 
Prefers (via Sign.merge) the signature of th1. *)


152 
fun merge_theories(th1,th2) =


153 
let val Thm{sign=sign1,...} = th1 and Thm{sign=sign2,...} = th2


154 
in Sign.merge (sign1,sign2) end


155 
handle TERM _ => raise THM("incompatible signatures", 0, [th1,th2]);


156 


157 
(*Stamps associated with a theory*)


158 
val stamps_of_thy = #stamps o Sign.rep_sg o sign_of;


159 


160 


161 
(**** Primitive rules ****)


162 


163 
(* discharge all assumptions t from ts *)


164 
val disch = gen_rem (op aconv);


165 


166 
(*The assumption rule AA in a theory *)


167 
fun assume ct : thm =


168 
let val {sign, t=prop, T, maxidx} = Sign.rep_cterm ct


169 
in if T<>propT then


170 
raise THM("assume: assumptions must have type prop", 0, [])


171 
else if maxidx <> ~1 then


172 
raise THM("assume: assumptions may not contain scheme variables",


173 
maxidx, [])


174 
else Thm{sign = sign, maxidx = ~1, hyps = [prop], prop = prop}


175 
end;


176 


177 
(* Implication introduction


178 
A  B


179 



180 
A ==> B *)


181 
fun implies_intr cA (thB as Thm{sign,maxidx,hyps,prop}) : thm =


182 
let val {sign=signA, t=A, T, maxidx=maxidxA} = Sign.rep_cterm cA


183 
in if T<>propT then


184 
raise THM("implies_intr: assumptions must have type prop", 0, [thB])


185 
else Thm{sign= Sign.merge (sign,signA), maxidx= max[maxidxA, maxidx],


186 
hyps= disch(hyps,A), prop= implies$A$prop}


187 
handle TERM _ =>


188 
raise THM("implies_intr: incompatible signatures", 0, [thB])


189 
end;


190 


191 
(* Implication elimination


192 
A ==> B A


193 



194 
B *)


195 
fun implies_elim thAB thA : thm =


196 
let val Thm{maxidx=maxA, hyps=hypsA, prop=propA,...} = thA


197 
and Thm{sign, maxidx, hyps, prop,...} = thAB;


198 
fun err(a) = raise THM("implies_elim: "^a, 0, [thAB,thA])


199 
in case prop of


200 
imp$A$B =>


201 
if imp=implies andalso A aconv propA


202 
then Thm{sign= merge_theories(thAB,thA),


203 
maxidx= max[maxA,maxidx],


204 
hyps= hypsA union hyps, (*dups suppressed*)


205 
prop= B}


206 
else err("major premise")


207 
 _ => err("major premise")


208 
end;


209 


210 
(* Forall introduction. The Free or Var x must not be free in the hypotheses.


211 
A


212 



213 
!!x.A *)


214 
fun forall_intr cx (th as Thm{sign,maxidx,hyps,prop}) =


215 
let val x = Sign.term_of cx;


216 
fun result(a,T) = Thm{sign= sign, maxidx= maxidx, hyps= hyps,


217 
prop= all(T) $ Abs(a, T, abstract_over (x,prop))}


218 
in case x of


219 
Free(a,T) =>


220 
if exists (apl(x, Logic.occs)) hyps


221 
then raise THM("forall_intr: variable free in assumptions", 0, [th])


222 
else result(a,T)


223 
 Var((a,_),T) => result(a,T)


224 
 _ => raise THM("forall_intr: not a variable", 0, [th])


225 
end;


226 


227 
(* Forall elimination


228 
!!x.A


229 



230 
A[t/x] *)


231 
fun forall_elim ct (th as Thm{sign,maxidx,hyps,prop}) : thm =


232 
let val {sign=signt, t, T, maxidx=maxt} = Sign.rep_cterm ct


233 
in case prop of


234 
Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A =>


235 
if T<>qary then


236 
raise THM("forall_elim: type mismatch", 0, [th])


237 
else Thm{sign= Sign.merge(sign,signt),


238 
maxidx= max[maxidx, maxt],


239 
hyps= hyps, prop= betapply(A,t)}


240 
 _ => raise THM("forall_elim: not quantified", 0, [th])


241 
end


242 
handle TERM _ =>


243 
raise THM("forall_elim: incompatible signatures", 0, [th]);


244 


245 


246 
(*** Equality ***)


247 


248 
(*Definition of the relation =?= *)


249 
val flexpair_def =


250 
Thm{sign= Sign.pure, hyps= [], maxidx= 0,


251 
prop= Sign.term_of


252 
(Sign.read_cterm Sign.pure


253 
("(?t =?= ?u) == (?t == ?u::?'a::{})", propT))};


254 


255 
(*The reflexivity rule: maps t to the theorem t==t *)


256 
fun reflexive ct =


257 
let val {sign, t, T, maxidx} = Sign.rep_cterm ct


258 
in Thm{sign= sign, hyps= [], maxidx= maxidx, prop= Logic.mk_equals(t,t)}


259 
end;


260 


261 
(*The symmetry rule


262 
t==u


263 



264 
u==t *)


265 
fun symmetric (th as Thm{sign,hyps,prop,maxidx}) =


266 
case prop of


267 
(eq as Const("==",_)) $ t $ u =>


268 
Thm{sign=sign, hyps=hyps, maxidx=maxidx, prop= eq$u$t}


269 
 _ => raise THM("symmetric", 0, [th]);


270 


271 
(*The transitive rule


272 
t1==u u==t2


273 



274 
t1==t2 *)


275 
fun transitive th1 th2 =


276 
let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1


277 
and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2;


278 
fun err(msg) = raise THM("transitive: "^msg, 0, [th1,th2])


279 
in case (prop1,prop2) of


280 
((eq as Const("==",_)) $ t1 $ u, Const("==",_) $ u' $ t2) =>


281 
if not (u aconv u') then err"middle term" else


282 
Thm{sign= merge_theories(th1,th2), hyps= hyps1 union hyps2,


283 
maxidx= max[max1,max2], prop= eq$t1$t2}


284 
 _ => err"premises"


285 
end;


286 


287 
(*Betaconversion: maps (%(x)t)(u) to the theorem (%(x)t)(u) == t[u/x] *)


288 
fun beta_conversion ct =


289 
let val {sign, t, T, maxidx} = Sign.rep_cterm ct


290 
in case t of


291 
Abs(_,_,bodt) $ u =>


292 
Thm{sign= sign, hyps= [],


293 
maxidx= maxidx_of_term t,


294 
prop= Logic.mk_equals(t, subst_bounds([u],bodt))}


295 
 _ => raise THM("beta_conversion: not a redex", 0, [])


296 
end;


297 


298 
(*The extensionality rule (proviso: x not free in f, g, or hypotheses)


299 
f(x) == g(x)


300 



301 
f == g *)


302 
fun extensional (th as Thm{sign,maxidx,hyps,prop}) =


303 
case prop of


304 
(Const("==",_)) $ (f$x) $ (g$y) =>


305 
let fun err(msg) = raise THM("extensional: "^msg, 0, [th])


306 
in (if x<>y then err"different variables" else


307 
case y of


308 
Free _ =>


309 
if exists (apl(y, Logic.occs)) (f::g::hyps)


310 
then err"variable free in hyps or functions" else ()


311 
 Var _ =>


312 
if Logic.occs(y,f) orelse Logic.occs(y,g)


313 
then err"variable free in functions" else ()


314 
 _ => err"not a variable");


315 
Thm{sign=sign, hyps=hyps, maxidx=maxidx,


316 
prop= Logic.mk_equals(f,g)}


317 
end


318 
 _ => raise THM("extensional: premise", 0, [th]);


319 


320 
(*The abstraction rule. The Free or Var x must not be free in the hypotheses.


321 
The bound variable will be named "a" (since x will be something like x320)


322 
t == u


323 



324 
%(x)t == %(x)u *)


325 
fun abstract_rule a cx (th as Thm{sign,maxidx,hyps,prop}) =


326 
let val x = Sign.term_of cx;


327 
val (t,u) = Logic.dest_equals prop


328 
handle TERM _ =>


329 
raise THM("abstract_rule: premise not an equality", 0, [th])


330 
fun result T =


331 
Thm{sign= sign, maxidx= maxidx, hyps= hyps,


332 
prop= Logic.mk_equals(Abs(a, T, abstract_over (x,t)),


333 
Abs(a, T, abstract_over (x,u)))}


334 
in case x of


335 
Free(_,T) =>


336 
if exists (apl(x, Logic.occs)) hyps


337 
then raise THM("abstract_rule: variable free in assumptions", 0, [th])


338 
else result T


339 
 Var(_,T) => result T


340 
 _ => raise THM("abstract_rule: not a variable", 0, [th])


341 
end;


342 


343 
(*The combination rule


344 
f==g t==u


345 



346 
f(t)==g(u) *)


347 
fun combination th1 th2 =


348 
let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1


349 
and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2


350 
in case (prop1,prop2) of


351 
(Const("==",_) $ f $ g, Const("==",_) $ t $ u) =>


352 
Thm{sign= merge_theories(th1,th2), hyps= hyps1 union hyps2,


353 
maxidx= max[max1,max2], prop= Logic.mk_equals(f$t, g$u)}


354 
 _ => raise THM("combination: premises", 0, [th1,th2])


355 
end;


356 


357 


358 
(*The equal propositions rule


359 
A==B A


360 



361 
B *)


362 
fun equal_elim th1 th2 =


363 
let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1


364 
and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2;


365 
fun err(msg) = raise THM("equal_elim: "^msg, 0, [th1,th2])


366 
in case prop1 of


367 
Const("==",_) $ A $ B =>


368 
if not (prop2 aconv A) then err"not equal" else


369 
Thm{sign= merge_theories(th1,th2), hyps= hyps1 union hyps2,


370 
maxidx= max[max1,max2], prop= B}


371 
 _ => err"major premise"


372 
end;


373 


374 


375 
(* Equality introduction


376 
A==>B B==>A


377 



378 
A==B *)


379 
fun equal_intr th1 th2 =


380 
let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1


381 
and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2;


382 
fun err(msg) = raise THM("equal_intr: "^msg, 0, [th1,th2])


383 
in case (prop1,prop2) of


384 
(Const("==>",_) $ A $ B, Const("==>",_) $ B' $ A') =>


385 
if A aconv A' andalso B aconv B'


386 
then Thm{sign= merge_theories(th1,th2), hyps= hyps1 union hyps2,


387 
maxidx= max[max1,max2], prop= Logic.mk_equals(A,B)}


388 
else err"not equal"


389 
 _ => err"premises"


390 
end;


391 


392 
(**** Derived rules ****)


393 


394 
(*Discharge all hypotheses (need not verify cterms)


395 
Repeated hypotheses are discharged only once; fold cannot do this*)


396 
fun implies_intr_hyps (Thm{sign, maxidx, hyps=A::As, prop}) =


397 
implies_intr_hyps


398 
(Thm{sign=sign, maxidx=maxidx,


399 
hyps= disch(As,A), prop= implies$A$prop})


400 
 implies_intr_hyps th = th;


401 


402 
(*Smash" unifies the list of term pairs leaving no flexflex pairs.


403 
Instantiates the theorem and deletes trivial tpairs.


404 
Resulting sequence may contain multiple elements if the tpairs are


405 
not all flexflex. *)


406 
fun flexflex_rule (Thm{sign,maxidx,hyps,prop}) =


407 
let fun newthm env =


408 
let val (tpairs,horn) =


409 
Logic.strip_flexpairs (Envir.norm_term env prop)


410 
(*Remove trivial tpairs, of the form t=t*)


411 
val distpairs = filter (not o op aconv) tpairs


412 
val newprop = Logic.list_flexpairs(distpairs, horn)


413 
in Thm{sign= sign, hyps= hyps,


414 
maxidx= maxidx_of_term newprop, prop= newprop}


415 
end;


416 
val (tpairs,_) = Logic.strip_flexpairs prop


417 
in Sequence.maps newthm


418 
(Unify.smash_unifiers(sign, Envir.empty maxidx, tpairs))


419 
end;


420 


421 


422 
(*Instantiation of Vars


423 
A


424 



425 
A[t1/v1,....,tn/vn] *)


426 


427 
(*Check that all the terms are Vars and are distinct*)


428 
fun instl_ok ts = forall is_Var ts andalso null(findrep ts);


429 


430 
(*For instantiate: process pair of cterms, merge theories*)


431 
fun add_ctpair ((ct,cu), (sign,tpairs)) =


432 
let val {sign=signt, t=t, T= T, ...} = Sign.rep_cterm ct


433 
and {sign=signu, t=u, T= U, ...} = Sign.rep_cterm cu


434 
in if T=U then (Sign.merge(sign, Sign.merge(signt, signu)), (t,u)::tpairs)


435 
else raise TYPE("add_ctpair", [T,U], [t,u])


436 
end;


437 


438 
fun add_ctyp ((v,ctyp), (sign',vTs)) =


439 
let val {T,sign} = Sign.rep_ctyp ctyp


440 
in (Sign.merge(sign,sign'), (v,T)::vTs) end;


441 


442 
fun duplicates t = findrep (map (#1 o dest_Var) (term_vars t));


443 


444 
(*Lefttoright replacements: ctpairs = [...,(vi,ti),...].


445 
Instantiates distinct Vars by terms of same type.


446 
Normalizes the new theorem! *)


447 
fun instantiate (vcTs,ctpairs) (th as Thm{sign,maxidx,hyps,prop}) =


448 
let val (newsign,tpairs) = foldr add_ctpair (ctpairs, (sign,[]));


449 
val (newsign,vTs) = foldr add_ctyp (vcTs, (newsign,[]));


450 
val prop = Type.inst_term_tvars(#tsig(Sign.rep_sg newsign),vTs) prop;


451 
val newprop = Envir.norm_term (Envir.empty 0) (subst_atomic tpairs prop)


452 
val newth = Thm{sign= newsign, hyps= hyps,


453 
maxidx= maxidx_of_term newprop, prop= newprop}


454 
in if not(instl_ok(map #1 tpairs)) orelse not(null(findrep(map #1 vTs)))


455 
then raise THM("instantiate: not distinct Vars", 0, [th])


456 
else case duplicates newprop of


457 
[] => newth


458 
 ix::_ => raise THM("instantiate: conflicting types for " ^


459 
Syntax.string_of_vname ix ^ "\n", 0, [newth])


460 
end


461 
handle TERM _ =>


462 
raise THM("instantiate: incompatible signatures",0,[th])


463 
 TYPE _ => raise THM("instantiate: types", 0, [th]);


464 


465 


466 
(*The trivial implication A==>A, justified by assume and forall rules.


467 
A can contain Vars, not so for assume! *)


468 
fun trivial ct : thm =


469 
let val {sign, t=A, T, maxidx} = Sign.rep_cterm ct


470 
in if T<>propT then


471 
raise THM("trivial: the term must have type prop", 0, [])


472 
else Thm{sign= sign, maxidx= maxidx, hyps= [], prop= implies$A$A}


473 
end;


474 


475 
(* Replace all TFrees not in the hyps by new TVars *)


476 
fun varifyT(Thm{sign,maxidx,hyps,prop}) =


477 
let val tfrees = foldr add_term_tfree_names (hyps,[])


478 
in Thm{sign=sign, maxidx=max[0,maxidx], hyps=hyps,


479 
prop= Type.varify(prop,tfrees)}


480 
end;


481 


482 
(* Replace all TVars by new TFrees *)


483 
fun freezeT(Thm{sign,maxidx,hyps,prop}) =


484 
let val prop' = Type.freeze (K true) prop


485 
in Thm{sign=sign, maxidx=maxidx_of_term prop', hyps=hyps, prop=prop'} end;


486 


487 


488 
(*** Inference rules for tactics ***)


489 


490 
(*Destruct proof state into constraints, other goals, goal(i), rest *)


491 
fun dest_state (state as Thm{prop,...}, i) =


492 
let val (tpairs,horn) = Logic.strip_flexpairs prop


493 
in case Logic.strip_prems(i, [], horn) of


494 
(B::rBs, C) => (tpairs, rev rBs, B, C)


495 
 _ => raise THM("dest_state", i, [state])


496 
end


497 
handle TERM _ => raise THM("dest_state", i, [state]);


498 


499 
(*Increment variables and parameters of rule as required for


500 
resolution with goal i of state. *)


501 
fun lift_rule (state, i) orule =


502 
let val Thm{prop=sprop,maxidx=smax,...} = state;


503 
val (Bi::_, _) = Logic.strip_prems(i, [], Logic.skip_flexpairs sprop)


504 
handle TERM _ => raise THM("lift_rule", i, [orule,state]);


505 
val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1);


506 
val (Thm{sign,maxidx,hyps,prop}) = orule


507 
val (tpairs,As,B) = Logic.strip_horn prop


508 
in Thm{hyps=hyps, sign= merge_theories(state,orule),


509 
maxidx= maxidx+smax+1,


510 
prop= Logic.rule_of(map (pairself lift_abs) tpairs,


511 
map lift_all As, lift_all B)}


512 
end;


513 


514 
(*Solve subgoal Bi of proof state B1...Bn/C by assumption. *)


515 
fun assumption i state =


516 
let val Thm{sign,maxidx,hyps,prop} = state;


517 
val (tpairs, Bs, Bi, C) = dest_state(state,i)


518 
fun newth (env as Envir.Envir{maxidx,asol,iTs}, tpairs) =


519 
Thm{sign=sign, hyps=hyps, maxidx=maxidx, prop=


520 
case (Envir.alist_of_olist asol, iTs) of


521 
(*avoid wasted normalizations*)


522 
([],[]) => Logic.rule_of(tpairs, Bs, C)


523 
 _ => (*normalize the new rule fully*)


524 
Envir.norm_term env (Logic.rule_of(tpairs, Bs, C))};


525 
fun addprfs [] = Sequence.null


526 
 addprfs ((t,u)::apairs) = Sequence.seqof (fn()=> Sequence.pull


527 
(Sequence.mapp newth


528 
(Unify.unifiers(sign,Envir.empty maxidx, (t,u)::tpairs))


529 
(addprfs apairs)))


530 
in addprfs (Logic.assum_pairs Bi) end;


531 


532 
(*Solve subgoal Bi of proof state B1...Bn/C by assumption.


533 
Checks if Bi's conclusion is alphaconvertible to one of its assumptions*)


534 
fun eq_assumption i state =


535 
let val Thm{sign,maxidx,hyps,prop} = state;


536 
val (tpairs, Bs, Bi, C) = dest_state(state,i)


537 
in if exists (op aconv) (Logic.assum_pairs Bi)


538 
then Thm{sign=sign, hyps=hyps, maxidx=maxidx,


539 
prop=Logic.rule_of(tpairs, Bs, C)}


540 
else raise THM("eq_assumption", 0, [state])


541 
end;


542 


543 


544 
(** User renaming of parameters in a subgoal **)


545 


546 
(*Calls error rather than raising an exception because it is intended


547 
for toplevel use  exception handling would not make sense here.


548 
The names in cs, if distinct, are used for the innermost parameters;


549 
preceding parameters may be renamed to make all params distinct.*)


550 
fun rename_params_rule (cs, i) state =


551 
let val Thm{sign,maxidx,hyps,prop} = state


552 
val (tpairs, Bs, Bi, C) = dest_state(state,i)


553 
val iparams = map #1 (Logic.strip_params Bi)


554 
val short = length iparams  length cs


555 
val newnames =


556 
if short<0 then error"More names than abstractions!"


557 
else variantlist(take (short,iparams), cs) @ cs


558 
val freenames = map (#1 o dest_Free) (term_frees prop)


559 
val newBi = Logic.list_rename_params (newnames, Bi)


560 
in


561 
case findrep cs of


562 
c::_ => error ("Bound variables not distinct: " ^ c)


563 
 [] => (case cs inter freenames of


564 
a::_ => error ("Bound/Free variable clash: " ^ a)


565 
 [] => Thm{sign=sign, hyps=hyps, maxidx=maxidx, prop=


566 
Logic.rule_of(tpairs, Bs@[newBi], C)})


567 
end;


568 


569 
(*** Preservation of bound variable names ***)


570 


571 
(*Scan a pair of terms; while they are similar,


572 
accumulate corresponding bound vars in "al"*)


573 
fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) = match_bvs(s,t,(x,y)::al)


574 
 match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al))


575 
 match_bvs(_,_,al) = al;


576 


577 
(* strip abstractions created by parameters *)


578 
fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al);


579 


580 


581 
(* strip_apply f A(,B) strips off all assumptions/parameters from A


582 
introduced by lifting over B, and applies f to remaining part of A*)


583 
fun strip_apply f =


584 
let fun strip(Const("==>",_)$ A1 $ B1,


585 
Const("==>",_)$ _ $ B2) = implies $ A1 $ strip(B1,B2)


586 
 strip((c as Const("all",_)) $ Abs(a,T,t1),


587 
Const("all",_) $ Abs(_,_,t2)) = c$Abs(a,T,strip(t1,t2))


588 
 strip(A,_) = f A


589 
in strip end;


590 


591 
(*Use the alist to rename all bound variables and some unknowns in a term


592 
dpairs = current disagreement pairs; tpairs = permanent ones (flexflex);


593 
Preserves unknowns in tpairs and on lhs of dpairs. *)


594 
fun rename_bvs([],_,_,_) = I


595 
 rename_bvs(al,dpairs,tpairs,B) =


596 
let val vars = foldr add_term_vars


597 
(map fst dpairs @ map fst tpairs @ map snd tpairs, [])


598 
(*unknowns appearing elsewhere be preserved!*)


599 
val vids = map (#1 o #1 o dest_Var) vars;


600 
fun rename(t as Var((x,i),T)) =


601 
(case assoc(al,x) of


602 
Some(y) => if x mem vids orelse y mem vids then t


603 
else Var((y,i),T)


604 
 None=> t)


605 
 rename(Abs(x,T,t)) =


606 
Abs(case assoc(al,x) of Some(y) => y  None => x,


607 
T, rename t)


608 
 rename(f$t) = rename f $ rename t


609 
 rename(t) = t;


610 
fun strip_ren Ai = strip_apply rename (Ai,B)


611 
in strip_ren end;


612 


613 
(*Function to rename bounds/unknowns in the argument, lifted over B*)


614 
fun rename_bvars(dpairs, tpairs, B) =


615 
rename_bvs(foldr match_bvars (dpairs,[]), dpairs, tpairs, B);


616 


617 


618 
(*** RESOLUTION ***)


619 


620 
(*strip off pairs of assumptions/parameters in parallel  they are


621 
identical because of lifting*)


622 
fun strip_assums2 (Const("==>", _) $ _ $ B1,


623 
Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2)


624 
 strip_assums2 (Const("all",_)$Abs(a,T,t1),


625 
Const("all",_)$Abs(_,_,t2)) =


626 
let val (B1,B2) = strip_assums2 (t1,t2)


627 
in (Abs(a,T,B1), Abs(a,T,B2)) end


628 
 strip_assums2 BB = BB;


629 


630 


631 
(*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C)


632 
Unifies B with Bi, replacing subgoal i (1 <= i <= n)


633 
If match then forbid instantiations in proof state


634 
If lifted then shorten the dpair using strip_assums2.


635 
If eres_flg then simultaneously proves A1 by assumption.


636 
nsubgoal is the number of new subgoals (written m above).


637 
Curried so that resolution calls dest_state only once.


638 
*)


639 
local open Sequence; exception Bicompose


640 
in


641 
fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted)


642 
(eres_flg, orule, nsubgoal) =


643 
let val Thm{maxidx=smax, hyps=shyps, ...} = state


644 
and Thm{maxidx=rmax, hyps=rhyps, prop=rprop,...} = orule;


645 
val sign = merge_theories(state,orule);


646 
(** Add new theorem with prop = '[ Bs; As ] ==> C' to thq **)


647 
fun addth As ((env as Envir.Envir{maxidx,asol,iTs}, tpairs), thq) =


648 
let val minenv = case Envir.alist_of_olist asol of


649 
[] => ~1  ((_,i),_) :: _ => i;


650 
val minx = min (minenv :: map (fn ((_,i),_) => i) iTs);


651 
val normt = Envir.norm_term env;


652 
(*Perform minimal copying here by examining env*)


653 
val normp = if minx = ~1 then (tpairs, Bs@As, C)


654 
else


655 
let val ntps = map (pairself normt) tpairs


656 
in if minx>smax then (*no assignments in state*)


657 
(ntps, Bs @ map normt As, C)


658 
else if match then raise Bicompose


659 
else (*normalize the new rule fully*)


660 
(ntps, map normt (Bs @ As), normt C)


661 
end


662 
val th = Thm{sign=sign, hyps=rhyps union shyps, maxidx=maxidx,


663 
prop= Logic.rule_of normp}


664 
in cons(th, thq) end handle Bicompose => thq


665 
val (rtpairs,rhorn) = Logic.strip_flexpairs(rprop);


666 
val (rAs,B) = Logic.strip_prems(nsubgoal, [], rhorn)


667 
handle TERM _ => raise THM("bicompose: rule", 0, [orule,state]);


668 
(*Modify assumptions, deleting nth if n>0 for eresolution*)


669 
fun newAs(As0, n, dpairs, tpairs) =


670 
let val As1 = if !Logic.auto_rename orelse not lifted then As0


671 
else map (rename_bvars(dpairs,tpairs,B)) As0


672 
in (map (Logic.flatten_params n) As1)


673 
handle TERM _ =>


674 
raise THM("bicompose: 1st premise", 0, [orule])


675 
end;


676 
val env = Envir.empty(max[rmax,smax]);


677 
val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi);


678 
val dpairs = BBi :: (rtpairs@stpairs);


679 
(*elimresolution: try each assumption in turn. Initially n=1*)


680 
fun tryasms (_, _, []) = null


681 
 tryasms (As, n, (t,u)::apairs) =


682 
(case pull(Unify.unifiers(sign, env, (t,u)::dpairs)) of


683 
None => tryasms (As, n+1, apairs)


684 
 cell as Some((_,tpairs),_) =>


685 
its_right (addth (newAs(As, n, [BBi,(u,t)], tpairs)))


686 
(seqof (fn()=> cell),


687 
seqof (fn()=> pull (tryasms (As, n+1, apairs)))));


688 
fun eres [] = raise THM("bicompose: no premises", 0, [orule,state])


689 
 eres (A1::As) = tryasms (As, 1, Logic.assum_pairs A1);


690 
(*ordinary resolution*)


691 
fun res(None) = null


692 
 res(cell as Some((_,tpairs),_)) =


693 
its_right (addth(newAs(rev rAs, 0, [BBi], tpairs)))


694 
(seqof (fn()=> cell), null)


695 
in if eres_flg then eres(rev rAs)


696 
else res(pull(Unify.unifiers(sign, env, dpairs)))


697 
end;


698 
end; (*open Sequence*)


699 


700 


701 
fun bicompose match arg i state =


702 
bicompose_aux match (state, dest_state(state,i), false) arg;


703 


704 
(*Quick test whether rule is resolvable with the subgoal with hyps Hs


705 
and conclusion B. If eres_flg then checks 1st premise of rule also*)


706 
fun could_bires (Hs, B, eres_flg, rule) =


707 
let fun could_reshyp (A1::_) = exists (apl(A1,could_unify)) Hs


708 
 could_reshyp [] = false; (*no premise  illegal*)


709 
in could_unify(concl_of rule, B) andalso


710 
(not eres_flg orelse could_reshyp (prems_of rule))


711 
end;


712 


713 
(*Biresolution of a state with a list of (flag,rule) pairs.


714 
Puts the rule above: rule/state. Renames vars in the rules. *)


715 
fun biresolution match brules i state =


716 
let val lift = lift_rule(state, i);


717 
val (stpairs, Bs, Bi, C) = dest_state(state,i)


718 
val B = Logic.strip_assums_concl Bi;


719 
val Hs = Logic.strip_assums_hyp Bi;


720 
val comp = bicompose_aux match (state, (stpairs, Bs, Bi, C), true);


721 
fun res [] = Sequence.null


722 
 res ((eres_flg, rule)::brules) =


723 
if could_bires (Hs, B, eres_flg, rule)


724 
then Sequence.seqof (*delay processing remainder til needed*)


725 
(fn()=> Some(comp (eres_flg, lift rule, nprems_of rule),


726 
res brules))


727 
else res brules


728 
in Sequence.flats (res brules) end;


729 


730 


731 
(**** THEORIES ****)


732 


733 
val pure_thy = Pure{sign = Sign.pure};


734 


735 
(*Look up the named axiom in the theory*)


736 
fun get_axiom thy axname =


737 
let fun get (Pure _) = raise Match


738 
 get (Extend{axioms,thy,...}) =


739 
(case Symtab.lookup(axioms,axname) of


740 
Some th => th


741 
 None => get thy)


742 
 get (Merge{thy1,thy2,...}) =


743 
get thy1 handle Match => get thy2


744 
in get thy


745 
handle Match => raise THEORY("get_axiom: No axiom "^axname, [thy])


746 
end;


747 


748 
(*Converts Frees to Vars: axioms can be written without question marks*)


749 
fun prepare_axiom sign sP =


750 
Logic.varify (Sign.term_of (Sign.read_cterm sign (sP,propT)));


751 


752 
(*Read an axiom for a new theory*)


753 
fun read_ax sign (a, sP) : string*thm =


754 
let val prop = prepare_axiom sign sP


755 
in (a, Thm{sign=sign, hyps=[], maxidx= maxidx_of_term prop, prop= prop})


756 
end


757 
handle ERROR =>


758 
error("extend_theory: The error above occurred in axiom " ^ a);


759 


760 
fun mk_axioms sign axpairs =


761 
Symtab.st_of_alist(map (read_ax sign) axpairs, Symtab.null)


762 
handle Symtab.DUPLICATE(a) => error("Two axioms named " ^ a);


763 


764 
(*Extension of a theory with given classes, types, constants and syntax.


765 
Reads the axioms from strings: axpairs have the form (axname, axiom). *)


766 
fun extend_theory thy thyname ext axpairs =


767 
let val sign = Sign.extend (sign_of thy) thyname ext;


768 
val axioms= mk_axioms sign axpairs


769 
in Extend{sign=sign, axioms= axioms, thy = thy} end;


770 


771 
(*The union of two theories*)


772 
fun merge_theories (thy1,thy2) =


773 
Merge{sign = Sign.merge(sign_of thy1, sign_of thy2),


774 
thy1 = thy1, thy2 = thy2};


775 


776 


777 
(*** Meta simp sets ***)


778 


779 
type rrule = {thm:thm, lhs:term};


780 
datatype meta_simpset =


781 
Mss of {net:rrule Net.net, congs:(string * rrule)list, primes:string,


782 
prems: thm list, mk_rews: thm > thm list};


783 


784 
(*A "mss" contains data needed during conversion:


785 
net: discrimination net of rewrite rules


786 
congs: association list of congruence rules


787 
primes: offset for generating unique new names


788 
for rewriting under lambda abstractions


789 
mk_rews: used when local assumptions are added


790 
*)


791 


792 
val empty_mss = Mss{net= Net.empty, congs= [], primes="", prems= [],


793 
mk_rews = K[]};


794 


795 
exception SIMPLIFIER of string * thm;


796 


797 
fun prtm a sg t = (writeln a; writeln(Sign.string_of_term sg t));


798 


799 
(*simple test for looping rewrite*)


800 
fun loops sign prems (lhs,rhs) =


801 
null(prems) andalso


802 
Pattern.eta_matches (#tsig(Sign.rep_sg sign)) (lhs,rhs);


803 


804 
fun mk_rrule (thm as Thm{hyps,sign,prop,maxidx,...}) =


805 
let val prems = Logic.strip_imp_prems prop


806 
val concl = Pattern.eta_contract (Logic.strip_imp_concl prop)


807 
val (lhs,rhs) = Logic.dest_equals concl handle TERM _ =>


808 
raise SIMPLIFIER("Rewrite rule not a metaequality",thm)


809 
in if loops sign prems (lhs,rhs)


810 
then (prtm "Warning: ignoring looping rewrite rule" sign prop; None)


811 
else Some{thm=thm,lhs=lhs}


812 
end;


813 


814 
fun add_simp(mss as Mss{net,congs,primes,prems,mk_rews},


815 
thm as Thm{sign,prop,...}) =


816 
let fun eq({thm=Thm{prop=p1,...},...}:rrule,


817 
{thm=Thm{prop=p2,...},...}:rrule) = p1 aconv p2


818 
in case mk_rrule thm of


819 
None => mss


820 
 Some(rrule as {lhs,...}) =>


821 
Mss{net= (Net.insert_term((lhs,rrule),net,eq)


822 
handle Net.INSERT =>


823 
(prtm "Warning: ignoring duplicate rewrite rule" sign prop;


824 
net)),


825 
congs=congs, primes=primes, prems=prems,mk_rews=mk_rews}


826 
end;


827 


828 
val add_simps = foldl add_simp;


829 


830 
fun mss_of thms = add_simps(empty_mss,thms);


831 


832 
fun add_cong(Mss{net,congs,primes,prems,mk_rews},thm) =


833 
let val (lhs,_) = Logic.dest_equals(concl_of thm) handle TERM _ =>


834 
raise SIMPLIFIER("Congruence not a metaequality",thm)


835 
val lhs = Pattern.eta_contract lhs


836 
val (a,_) = dest_Const (head_of lhs) handle TERM _ =>


837 
raise SIMPLIFIER("Congruence must start with a constant",thm)


838 
in Mss{net=net, congs=(a,{lhs=lhs,thm=thm})::congs, primes=primes,


839 
prems=prems, mk_rews=mk_rews}


840 
end;


841 


842 
val (op add_congs) = foldl add_cong;


843 


844 
fun add_prems(Mss{net,congs,primes,prems,mk_rews},thms) =


845 
Mss{net=net, congs=congs, primes=primes, prems=thms@prems, mk_rews=mk_rews};


846 


847 
fun prems_of_mss(Mss{prems,...}) = prems;


848 


849 
fun set_mk_rews(Mss{net,congs,primes,prems,...},mk_rews) =


850 
Mss{net=net, congs=congs, primes=primes, prems=prems, mk_rews=mk_rews};


851 
fun mk_rews_of_mss(Mss{mk_rews,...}) = mk_rews;


852 


853 


854 
(*** Metalevel rewriting


855 
uses conversions, omitting proofs for efficiency. See


856 
L C Paulson, A higherorder implementation of rewriting,


857 
Science of Computer Programming 3 (1983), pages 119149. ***)


858 


859 
type prover = meta_simpset > thm > thm option;


860 
type termrec = (Sign.sg * term list) * term;


861 
type conv = meta_simpset > termrec > termrec;


862 


863 
val trace_simp = ref false;


864 


865 
fun trace_term a sg t = if !trace_simp then prtm a sg t else ();


866 


867 
fun trace_thm a (Thm{sign,prop,...}) = trace_term a sign prop;


868 


869 
fun check_conv(thm as Thm{sign,hyps,prop,...}, prop0) =


870 
let fun err() = (trace_term "Proved wrong thm" sign prop;


871 
error "Check your prover")


872 
val (lhs0,_) = Logic.dest_equals(Logic.strip_imp_concl prop0)


873 
in case prop of


874 
Const("==",_) $ lhs $ rhs =>


875 
if (lhs = lhs0) orelse


876 
(lhs aconv (Envir.norm_term (Envir.empty 0) lhs0))


877 
then (trace_thm "SUCCEEDED" thm; ((sign,hyps),rhs))


878 
else err()


879 
 _ => err()


880 
end;


881 


882 
(*Conversion to apply the meta simpset to a term*)


883 
fun rewritec prover (mss as Mss{net,...}) (sghyt as (sgt,hypst),t) =


884 
let val t = Pattern.eta_contract t


885 
fun rew {thm as Thm{sign,hyps,maxidx,prop,...}, lhs} =


886 
let val sign' = Sign.merge(sgt,sign)


887 
val tsig = #tsig(Sign.rep_sg sign')


888 
val insts = Pattern.match tsig (lhs,t)


889 
val prop' = subst_vars insts prop;


890 
val hyps' = hyps union hypst;


891 
val thm' = Thm{sign=sign', hyps=hyps', prop=prop', maxidx=maxidx}


892 
in if nprems_of thm' = 0


893 
then let val (_,rhs) = Logic.dest_equals prop'


894 
in trace_thm "Rewriting:" thm'; Some((sign',hyps'),rhs) end


895 
else (trace_thm "Trying to rewrite:" thm';


896 
case prover mss thm' of


897 
None => (trace_thm "FAILED" thm'; None)


898 
 Some(thm2) => Some(check_conv(thm2,prop')))


899 
end


900 


901 
fun rewl [] = None


902 
 rewl (rrule::rrules) =


903 
let val opt = rew rrule handle Pattern.MATCH => None


904 
in case opt of None => rewl rrules  some => some end;


905 


906 
in case t of


907 
Abs(_,_,body) $ u => Some(sghyt,subst_bounds([u], body))


908 
 _ => rewl (Net.match_term net t)


909 
end;


910 


911 
(*Conversion to apply a congruence rule to a term*)


912 
fun congc prover {thm=cong,lhs=lhs} (sghyt as (sgt,hypst),t) =


913 
let val Thm{sign,hyps,maxidx,prop,...} = cong


914 
val sign' = Sign.merge(sgt,sign)


915 
val tsig = #tsig(Sign.rep_sg sign')


916 
val insts = Pattern.match tsig (lhs,t) handle Pattern.MATCH =>


917 
error("Congruence rule did not match")


918 
val prop' = subst_vars insts prop;


919 
val thm' = Thm{sign=sign', hyps=hyps union hypst,


920 
prop=prop', maxidx=maxidx}


921 
val unit = trace_thm "Applying congruence rule" thm';


922 


923 
in case prover thm' of


924 
None => error("Failed congruence proof!")


925 
 Some(thm2) => check_conv(thm2,prop')


926 
end;


927 


928 


929 
fun bottomc prover =


930 
let fun botc mss trec = let val trec1 = subc mss trec


931 
in case rewritec prover mss trec1 of


932 
None => trec1


933 
 Some(trec2) => botc mss trec2


934 
end


935 


936 
and subc (mss as Mss{net,congs,primes,prems,mk_rews})


937 
(trec as (sghy,t)) =


938 
(case t of


939 
Abs(a,T,t) =>


940 
let val v = Free(".subc." ^ primes,T)


941 
val mss' = Mss{net=net, congs=congs, primes=primes^"'",


942 
prems=prems,mk_rews=mk_rews}


943 
val (sghy',t') = botc mss' (sghy,subst_bounds([v],t))


944 
in (sghy', Abs(a, T, abstract_over(v,t'))) end


945 
 t$u => (case t of


946 
Const("==>",_)$s => impc(sghy,s,u,mss)


947 
 Abs(_,_,body) => subc mss (sghy,subst_bounds([u], body))


948 
 _ =>


949 
let fun appc() = let val (sghy1,t1) = botc mss (sghy,t)


950 
val (sghy2,u1) = botc mss (sghy1,u)


951 
in (sghy2,t1$u1) end


952 
val (h,ts) = strip_comb t


953 
in case h of


954 
Const(a,_) =>


955 
(case assoc(congs,a) of


956 
None => appc()


957 
 Some(cong) => congc (prover mss) cong trec)


958 
 _ => appc()


959 
end)


960 
 _ => trec)


961 


962 
and impc(sghy,s,u,mss as Mss{mk_rews,...}) =


963 
let val (sghy1 as (sg1,hyps1),s') = botc mss (sghy,s)


964 
val (rthms,mss) =


965 
if maxidx_of_term s' <> ~1 then ([],mss)


966 
else let val thm = Thm{sign=sg1,hyps=[s'],prop=s',maxidx= ~1}


967 
in (mk_rews thm, add_prems(mss,[thm])) end


968 
val unit = seq (trace_thm "Adding rewrite rule:") rthms


969 
val mss' = add_simps(mss,rthms)


970 
val ((sg2,hyps2),u') = botc mss' (sghy1,u)


971 
in ((sg2,hyps2\s'), Logic.mk_implies(s',u')) end


972 


973 
in botc end;


974 


975 


976 
(*** Metarewriting: rewrites t to u and returns the theorem t==u ***)


977 
(* Parameters:


978 
mss: contains equality theorems of the form [p1,...] ==> t==u


979 
prover: how to solve premises in conditional rewrites and congruences


980 
*)


981 


982 
(*** FIXME: check that #primes(mss) does not "occur" in ct alread ***)


983 
fun rewrite_cterm mss prover ct =


984 
let val {sign, t, T, maxidx} = Sign.rep_cterm ct;


985 
val ((sign',hyps),u) = bottomc prover mss ((sign,[]),t);


986 
val prop = Logic.mk_equals(t,u)


987 
in Thm{sign= sign', hyps= hyps, maxidx= maxidx_of_term prop, prop= prop}


988 
end


989 


990 
end;
