0

1 
(* Title: Provers/simp


2 
Author: Tobias Nipkow


3 
Copyright 1993 University of Cambridge


4 


5 
Generic simplifier, suitable for most logics. The only known exception is


6 
Constructive Type Theory. The reflexivity axiom must be unconditional,


7 
namely a=a not a:A ==> a=a:A. Used typedsimp.ML otherwise.


8 
*)


9 


10 
signature SIMP_DATA =


11 
sig


12 
val dest_red : term > term * term * term


13 
val mk_rew_rules : thm > thm list


14 
val norm_thms : (thm*thm) list (* [(?x>>norm(?x), norm(?x)>>?x), ...] *)


15 
val red1 : thm (* ?P>>?Q ==> ?P ==> ?Q *)


16 
val red2 : thm (* ?P>>?Q ==> ?Q ==> ?P *)


17 
val refl_thms : thm list


18 
val subst_thms : thm list (* [ ?a>>?b ==> ?P(?a) ==> ?P(?b), ...] *)


19 
val trans_thms : thm list


20 
end;


21 


22 


23 
infix 4 addrews addcongs addsplits delrews delcongs setauto;


24 


25 
signature SIMP =


26 
sig


27 
type simpset


28 
val empty_ss : simpset


29 
val addcongs : simpset * thm list > simpset


30 
val addrews : simpset * thm list > simpset


31 
val addsplits : simpset * thm list > simpset


32 
val delcongs : simpset * thm list > simpset


33 
val delrews : simpset * thm list > simpset


34 
val dest_ss : simpset > thm list * thm list


35 
val print_ss : simpset > unit


36 
val setauto : simpset * (thm list > int > tactic) > simpset


37 
val ASM_SIMP_TAC : simpset > int > tactic


38 
val SPLIT_TAC : simpset > int > tactic


39 
val SIMP_SPLIT2_TAC : simpset > int > tactic


40 
val SIMP_THM : simpset > thm > thm


41 
val SIMP_TAC : simpset > int > tactic


42 
val mk_congs : theory > string list > thm list


43 
val mk_typed_congs : theory > (string * string) list > thm list


44 
(* temporarily disabled:


45 
val extract_free_congs : unit > thm list


46 
*)


47 
val tracing : bool ref


48 
end;


49 


50 
functor SimpFun (Simp_data: SIMP_DATA) : SIMP =


51 
struct


52 


53 
local open Simp_data Logic in


54 


55 
(*For taking apart reductions into left, right hand sides*)


56 
val lhs_of = #2 o dest_red;


57 
val rhs_of = #3 o dest_red;


58 


59 
(*** Indexing and filtering of theorems ***)


60 


61 
fun eq_brl ((b1,th1),(b2,th2)) = b1=b2 andalso eq_thm(th1,th2);


62 


63 
(*insert a thm in a discrimination net by its lhs*)


64 
fun lhs_insert_thm (th,net) =


65 
Net.insert_term((lhs_of (concl_of th), (false,th)), net, eq_brl)


66 
handle Net.INSERT => net;


67 


68 
(*match subgoal i against possible theorems in the net.


69 
Similar to match_from_nat_tac, but the net does not contain numbers;


70 
rewrite rules are not ordered.*)


71 
fun net_tac net =


72 
SUBGOAL(fn (prem,i) =>


73 
match_tac (Net.match_term net (strip_assums_concl prem)) i);


74 


75 
(*match subgoal i against possible theorems indexed by lhs in the net*)


76 
fun lhs_net_tac net =


77 
SUBGOAL(fn (prem,i) =>


78 
bimatch_tac (Net.match_term net


79 
(lhs_of (strip_assums_concl prem))) i);


80 


81 
fun nth_subgoal i thm = nth_elem(i1,prems_of thm);


82 


83 
fun goal_concl i thm = strip_assums_concl(nth_subgoal i thm);


84 


85 
fun lhs_of_eq i thm = lhs_of(goal_concl i thm)


86 
and rhs_of_eq i thm = rhs_of(goal_concl i thm);


87 


88 
fun var_lhs(thm,i) =


89 
let fun var(Var _) = true


90 
 var(Abs(_,_,t)) = var t


91 
 var(f$_) = var f


92 
 var _ = false;


93 
in var(lhs_of_eq i thm) end;


94 


95 
fun contains_op opns =


96 
let fun contains(Const(s,_)) = s mem opns 


97 
contains(s$t) = contains s orelse contains t 


98 
contains(Abs(_,_,t)) = contains t 


99 
contains _ = false;


100 
in contains end;


101 


102 
fun may_match(match_ops,i) = contains_op match_ops o lhs_of_eq i;


103 


104 
val (normI_thms,normE_thms) = split_list norm_thms;


105 


106 
(*Get the norm constants from norm_thms*)


107 
val norms =


108 
let fun norm thm =


109 
case lhs_of(concl_of thm) of


110 
Const(n,_)$_ => n


111 
 _ => (prths normE_thms; error"No constant in lhs of a norm_thm")


112 
in map norm normE_thms end;


113 


114 
fun lhs_is_NORM(thm,i) = case lhs_of_eq i thm of


115 
Const(s,_)$_ => s mem norms  _ => false;


116 


117 
val refl_tac = resolve_tac refl_thms;


118 


119 
fun find_res thms thm =


120 
let fun find [] = (prths thms; error"Check Simp_Data")


121 
 find(th::thms) = thm RS th handle _ => find thms


122 
in find thms end;


123 


124 
val mk_trans = find_res trans_thms;


125 


126 
fun mk_trans2 thm =


127 
let fun mk[] = error"Check transitivity"


128 
 mk(t::ts) = (thm RSN (2,t)) handle _ => mk ts


129 
in mk trans_thms end;


130 


131 
(*Applies tactic and returns the first resulting state, FAILS if none!*)


132 
fun one_result(tac,thm) = case Sequence.pull(tapply(tac,thm)) of


133 
Some(thm',_) => thm'


134 
 None => raise THM("Simplifier: could not continue", 0, [thm]);


135 


136 
fun res1(thm,thms,i) = one_result(resolve_tac thms i,thm);


137 


138 


139 
(**** Adding "NORM" tags ****)


140 


141 
(*get name of the constant from conclusion of a congruence rule*)


142 
fun cong_const cong =


143 
case head_of (lhs_of (concl_of cong)) of


144 
Const(c,_) => c


145 
 _ => "" (*a placeholder distinct from const names*);


146 


147 
(*true if the term is an atomic proposition (no ==> signs) *)


148 
val atomic = null o strip_assums_hyp;


149 


150 
(*ccs contains the names of the constants possessing congruence rules*)


151 
fun add_hidden_vars ccs =


152 
let fun add_hvars(tm,hvars) = case tm of


153 
Abs(_,_,body) => add_term_vars(body,hvars)


154 
 _$_ => let val (f,args) = strip_comb tm


155 
in case f of


156 
Const(c,T) =>


157 
if c mem ccs


158 
then foldr add_hvars (args,hvars)


159 
else add_term_vars(tm,hvars)


160 
 _ => add_term_vars(tm,hvars)


161 
end


162 
 _ => hvars;


163 
in add_hvars end;


164 


165 
fun add_new_asm_vars new_asms =


166 
let fun itf((tm,at),vars) =


167 
if at then vars else add_term_vars(tm,vars)


168 
fun add_list(tm,al,vars) = let val (_,tml) = strip_comb tm


169 
in if length(tml)=length(al)


170 
then foldr itf (tml~~al,vars)


171 
else vars


172 
end


173 
fun add_vars (tm,vars) = case tm of


174 
Abs (_,_,body) => add_vars(body,vars)


175 
 r$s => (case head_of tm of


176 
Const(c,T) => (case assoc(new_asms,c) of


177 
None => add_vars(r,add_vars(s,vars))


178 
 Some(al) => add_list(tm,al,vars))


179 
 _ => add_vars(r,add_vars(s,vars)))


180 
 _ => vars


181 
in add_vars end;


182 


183 


184 
fun add_norms(congs,ccs,new_asms) thm =


185 
let val thm' = mk_trans2 thm;


186 
(* thm': [?z > l; Prems; r > ?t] ==> ?z > ?t *)


187 
val nops = nprems_of thm'


188 
val lhs = rhs_of_eq 1 thm'


189 
val rhs = lhs_of_eq nops thm'


190 
val asms = tl(rev(tl(prems_of thm')))


191 
val hvars = foldr (add_hidden_vars ccs) (lhs::rhs::asms,[])


192 
val hvars = add_new_asm_vars new_asms (rhs,hvars)


193 
fun it_asms (asm,hvars) =


194 
if atomic asm then add_new_asm_vars new_asms (asm,hvars)


195 
else add_term_frees(asm,hvars)


196 
val hvars = foldr it_asms (asms,hvars)


197 
val hvs = map (#1 o dest_Var) hvars


198 
val refl1_tac = refl_tac 1


199 
val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops)


200 
(STATE(fn thm =>


201 
case head_of(rhs_of_eq 1 thm) of


202 
Var(ixn,_) => if ixn mem hvs then refl1_tac


203 
else resolve_tac normI_thms 1 ORELSE refl1_tac


204 
 Const _ => resolve_tac normI_thms 1 ORELSE


205 
resolve_tac congs 1 ORELSE refl1_tac


206 
 Free _ => resolve_tac congs 1 ORELSE refl1_tac


207 
 _ => refl1_tac))


208 
val Some(thm'',_) = Sequence.pull(tapply(add_norm_tac,thm'))


209 
in thm'' end;


210 


211 
fun add_norm_tags congs =


212 
let val ccs = map cong_const congs


213 
val new_asms = filter (exists not o #2)


214 
(ccs ~~ (map (map atomic o prems_of) congs));


215 
in add_norms(congs,ccs,new_asms) end;


216 


217 
fun normed_rews congs =


218 
let val add_norms = add_norm_tags congs;


219 
in fn thm => map (varifyT o add_norms o mk_trans) (mk_rew_rules(freezeT thm))


220 
end;


221 


222 
fun NORM norm_lhs_tac = EVERY'[resolve_tac [red2], norm_lhs_tac, refl_tac];


223 


224 
val trans_norms = map mk_trans normE_thms;


225 


226 


227 
(* SIMPSET *)


228 


229 
datatype simpset =


230 
SS of {auto_tac: thm list > int > tactic,


231 
congs: thm list,


232 
cong_net: thm Net.net,


233 
mk_simps: thm > thm list,


234 
simps: (thm * thm list) list,


235 
simp_net: thm Net.net,


236 
splits: thm list,


237 
split_consts: string list}


238 


239 
val empty_ss = SS{auto_tac= K (K no_tac), congs=[], cong_net=Net.empty,


240 
mk_simps=normed_rews[], simps=[], simp_net=Net.empty,


241 
splits=[], split_consts=[]};


242 


243 
(** Insertion of congruences, rewrites and case splits **)


244 


245 
(*insert a thm in a thm net*)


246 
fun insert_thm_warn (th,net) =


247 
Net.insert_term((concl_of th, th), net, eq_thm)


248 
handle Net.INSERT =>


249 
(writeln"\nDuplicate rewrite or congruence rule:"; print_thm th;


250 
net);


251 


252 
val insert_thms = foldr insert_thm_warn;


253 


254 
fun addrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net,


255 
splits,split_consts}, thm) =


256 
let val thms = mk_simps thm


257 
in SS{auto_tac=auto_tac,congs=congs, cong_net=cong_net, mk_simps=mk_simps,


258 
simps = (thm,thms)::simps, simp_net = insert_thms(thms,simp_net),


259 
splits=splits,split_consts=split_consts}


260 
end;


261 


262 
val op addrews = foldl addrew;


263 


264 
fun op addcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net,


265 
splits,split_consts}, thms) =


266 
let val congs' = thms @ congs;


267 
in SS{auto_tac=auto_tac, congs= congs',


268 
cong_net= insert_thms (map mk_trans thms,cong_net),


269 
mk_simps= normed_rews congs', simps=simps, simp_net=simp_net,


270 
splits=splits,split_consts=split_consts}


271 
end;


272 


273 
fun split_err() = error("split rule not of the form ?P(c(...)) = ...");


274 


275 
fun split_const(_ $ t) =


276 
(case head_of t of Const(a,_) => a  _ => split_err())


277 
 split_const _ = split_err();


278 


279 
fun addsplit(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net,


280 
splits,split_consts}, thm) =


281 
let val a = split_const(lhs_of(concl_of thm))


282 
in SS{auto_tac=auto_tac,congs=congs,cong_net=cong_net,


283 
mk_simps=mk_simps,simps=simps,simp_net=simp_net,


284 
splits=splits@[mk_trans thm],split_consts=split_consts@[a]} end;


285 


286 
val op addsplits = foldl addsplit;


287 


288 
(** Deletion of congruences and rewrites **)


289 


290 
(*delete a thm from a thm net*)


291 
fun delete_thm_warn (th,net) =


292 
Net.delete_term((concl_of th, th), net, eq_thm)


293 
handle Net.DELETE =>


294 
(writeln"\nNo such rewrite or congruence rule:"; print_thm th;


295 
net);


296 


297 
val delete_thms = foldr delete_thm_warn;


298 


299 
fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net,


300 
splits,split_consts}, thms) =


301 
let val congs' = foldl (gen_rem eq_thm) (congs,thms)


302 
in SS{auto_tac=auto_tac, congs= congs',


303 
cong_net= delete_thms(map mk_trans thms,cong_net),


304 
mk_simps= normed_rews congs', simps=simps, simp_net=simp_net,


305 
splits=splits,split_consts=split_consts}


306 
end;


307 


308 
fun delrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net,


309 
splits,split_consts}, thm) =


310 
let fun find((p as (th,ths))::ps',ps) =


311 
if eq_thm(thm,th) then (ths,ps@ps') else find(ps',p::ps)


312 
 find([],simps') = (writeln"\nNo such rewrite or congruence rule:";


313 
print_thm thm;


314 
([],simps'))


315 
val (thms,simps') = find(simps,[])


316 
in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps,


317 
simps = simps', simp_net = delete_thms(thms,simp_net),


318 
splits=splits,split_consts=split_consts}


319 
end;


320 


321 
val op delrews = foldl delrew;


322 


323 


324 
fun op setauto(SS{congs,cong_net,mk_simps,simps,simp_net,


325 
splits,split_consts,...}, auto_tac) =


326 
SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps,


327 
simps=simps, simp_net=simp_net,splits=splits,split_consts=split_consts};


328 


329 


330 
(** Inspection of a simpset **)


331 


332 
fun dest_ss(SS{congs,simps,...}) = (congs, map #1 simps);


333 


334 
fun print_ss(SS{congs,simps,splits,...}) =


335 
(writeln"Congruences:"; prths congs;


336 
writeln"Case Splits"; prths splits;


337 
writeln"Rewrite Rules:"; prths (map #1 simps); ());


338 


339 


340 
(* Rewriting with case splits *)


341 


342 
fun splittable a i thm =


343 
let val tm = goal_concl i thm


344 
fun nobound(Abs(_,_,tm),j,k) = nobound(tm,j,k+1)


345 
 nobound(s$t,j,k) = nobound(s,j,k) andalso nobound(t,j,k)


346 
 nobound(Bound n,j,k) = n < k orelse k+j <= n


347 
 nobound(_) = true;


348 
fun check_args(al,j) = forall (fn t => nobound(t,j,0)) al


349 
fun find_if(Abs(_,_,tm),j) = find_if(tm,j+1)


350 
 find_if(tm as s$t,j) = let val (f,al) = strip_comb tm in


351 
case f of Const(c,_) => if c=a then check_args(al,j)


352 
else find_if(s,j) orelse find_if(t,j)


353 
 _ => find_if(s,j) orelse find_if(t,j) end


354 
 find_if(_) = false;


355 
in find_if(tm,0) end;


356 


357 
fun split_tac (cong_tac,splits,split_consts) i =


358 
let fun seq_try (split::splits,a::bs) thm = tapply(


359 
COND (splittable a i) (DETERM(resolve_tac[split]i))


360 
(Tactic(seq_try(splits,bs))), thm)


361 
 seq_try([],_) thm = tapply(no_tac,thm)


362 
and try_rew thm = tapply(Tactic(seq_try(splits,split_consts))


363 
ORELSE Tactic one_subt, thm)


364 
and one_subt thm =


365 
let val test = has_fewer_prems (nprems_of thm + 1)


366 
fun loop thm = tapply(COND test no_tac


367 
((Tactic try_rew THEN DEPTH_FIRST test (refl_tac i))


368 
ORELSE (refl_tac i THEN Tactic loop)), thm)


369 
in tapply(cong_tac THEN Tactic loop, thm) end


370 
in if null splits then no_tac


371 
else COND (may_match(split_consts,i)) (Tactic try_rew) no_tac


372 
end;


373 


374 
fun SPLIT_TAC (SS{cong_net,splits,split_consts,...}) i =


375 
let val cong_tac = net_tac cong_net i


376 
in NORM (split_tac (cong_tac,splits,split_consts)) i end;


377 


378 
(* Rewriting Automaton *)


379 


380 
datatype cntrl = STOP  MK_EQ  ASMS of int  SIMP_LHS  REW  REFL  TRUE


381 
 PROVE  POP_CS  POP_ARTR  SPLIT;


382 
(*


383 
fun pr_cntrl c = case c of STOP => prs("STOP")  MK_EQ => prs("MK_EQ") 


384 
ASMS i => print_int i  POP_ARTR => prs("POP_ARTR") 


385 
SIMP_LHS => prs("SIMP_LHS")  REW => prs("REW")  REFL => prs("REFL") 


386 
TRUE => prs("TRUE")  PROVE => prs("PROVE")  POP_CS => prs("POP_CS")  SPLIT


387 
=> prs("SPLIT");


388 
*)


389 
fun simp_refl([],_,ss) = ss


390 
 simp_refl(a'::ns,a,ss) = if a'=a then simp_refl(ns,a,SIMP_LHS::REFL::ss)


391 
else simp_refl(ns,a,ASMS(a)::SIMP_LHS::REFL::POP_ARTR::ss);


392 


393 
(** Tracing **)


394 


395 
val tracing = ref false;


396 


397 
(*Replace parameters by Free variables in P*)


398 
fun variants_abs ([],P) = P


399 
 variants_abs ((a,T)::aTs, P) =


400 
variants_abs (aTs, #2 (variant_abs(a,T,P)));


401 


402 
(*Select subgoal i from proof state; substitute parameters, for printing*)


403 
fun prepare_goal i st =


404 
let val subgi = nth_subgoal i st


405 
val params = rev(strip_params subgi)


406 
in variants_abs (params, strip_assums_concl subgi) end;


407 


408 
(*print lhs of conclusion of subgoal i*)


409 
fun pr_goal_lhs i st =


410 
writeln (Sign.string_of_term (#sign(rep_thm st))


411 
(lhs_of (prepare_goal i st)));


412 


413 
(*print conclusion of subgoal i*)


414 
fun pr_goal_concl i st =


415 
writeln (Sign.string_of_term (#sign(rep_thm st)) (prepare_goal i st))


416 


417 
(*print subgoals i to j (inclusive)*)


418 
fun pr_goals (i,j) st =


419 
if i>j then ()


420 
else (pr_goal_concl i st; pr_goals (i+1,j) st);


421 


422 
(*Print rewrite for tracing; i=subgoal#, n=number of new subgoals,


423 
thm=old state, thm'=new state *)


424 
fun pr_rew (i,n,thm,thm',not_asms) =


425 
if !tracing


426 
then (if not_asms then () else writeln"Assumption used in";


427 
pr_goal_lhs i thm; writeln">"; pr_goal_lhs (i+n) thm';


428 
if n>0 then (writeln"Conditions:"; pr_goals (i, i+n1) thm')


429 
else ();


430 
writeln"" )


431 
else ();


432 


433 
(* Skip the first n hyps of a goal, and return the rest in generalized form *)


434 
fun strip_varify(Const("==>", _) $ H $ B, n, vs) =


435 
if n=0 then subst_bounds(vs,H)::strip_varify(B,0,vs)


436 
else strip_varify(B,n1,vs)


437 
 strip_varify(Const("all",_)$Abs(_,T,t), n, vs) =


438 
strip_varify(t,n,Var(("?",length vs),T)::vs)


439 
 strip_varify _ = [];


440 


441 
fun execute(ss,if_fl,auto_tac,cong_tac,splits,split_consts,net,i) thm = let


442 


443 
fun simp_lhs(thm,ss,anet,ats,cs) =


444 
if var_lhs(thm,i) then (ss,thm,anet,ats,cs) else


445 
if lhs_is_NORM(thm,i) then (ss, res1(thm,trans_norms,i), anet,ats,cs)


446 
else case Sequence.pull(tapply(cong_tac i,thm)) of


447 
Some(thm',_) =>


448 
let val ps = prems_of thm and ps' = prems_of thm';


449 
val n = length(ps')length(ps);


450 
val a = length(strip_assums_hyp(nth_elem(i1,ps)))


451 
val l = map (fn p => length(strip_assums_hyp(p)))


452 
(take(n,drop(i1,ps')));


453 
in (simp_refl(rev(l),a,REW::ss),thm',anet,ats,cs) end


454 
 None => (REW::ss,thm,anet,ats,cs);


455 


456 
(*NB: the "Adding rewrites:" trace will look strange because assumptions


457 
are represented by rules, generalized over their parameters*)


458 
fun add_asms(ss,thm,a,anet,ats,cs) =


459 
let val As = strip_varify(nth_subgoal i thm, a, []);

231

460 
val thms = map (trivial o cterm_of(#sign(rep_thm(thm))))As;

0

461 
val new_rws = flat(map mk_rew_rules thms);


462 
val rwrls = map mk_trans (flat(map mk_rew_rules thms));


463 
val anet' = foldr lhs_insert_thm (rwrls,anet)


464 
in if !tracing andalso not(null new_rws)


465 
then (writeln"Adding rewrites:"; prths new_rws; ())


466 
else ();


467 
(ss,thm,anet',anet::ats,cs)


468 
end;


469 


470 
fun rew(seq,thm,ss,anet,ats,cs, more) = case Sequence.pull seq of


471 
Some(thm',seq') =>


472 
let val n = (nprems_of thm')  (nprems_of thm)


473 
in pr_rew(i,n,thm,thm',more);


474 
if n=0 then (SIMP_LHS::ss, thm', anet, ats, cs)


475 
else ((replicate n PROVE) @ (POP_CS::SIMP_LHS::ss),


476 
thm', anet, ats, (ss,thm,anet,ats,seq',more)::cs)


477 
end


478 
 None => if more


479 
then rew(tapply(lhs_net_tac anet i THEN assume_tac i,thm),


480 
thm,ss,anet,ats,cs,false)


481 
else (ss,thm,anet,ats,cs);


482 


483 
fun try_true(thm,ss,anet,ats,cs) =


484 
case Sequence.pull(tapply(auto_tac i,thm)) of


485 
Some(thm',_) => (ss,thm',anet,ats,cs)


486 
 None => let val (ss0,thm0,anet0,ats0,seq,more)::cs0 = cs


487 
in if !tracing


488 
then (writeln"*** Failed to prove precondition. Normal form:";


489 
pr_goal_concl i thm; writeln"")


490 
else ();


491 
rew(seq,thm0,ss0,anet0,ats0,cs0,more)


492 
end;


493 


494 
fun split(thm,ss,anet,ats,cs) =


495 
case Sequence.pull(tapply(split_tac


496 
(cong_tac i,splits,split_consts) i,thm)) of


497 
Some(thm',_) => (SIMP_LHS::SPLIT::ss,thm',anet,ats,cs)


498 
 None => (ss,thm,anet,ats,cs);


499 


500 
fun step(s::ss, thm, anet, ats, cs) = case s of


501 
MK_EQ => (ss, res1(thm,[red2],i), anet, ats, cs)


502 
 ASMS(a) => add_asms(ss,thm,a,anet,ats,cs)


503 
 SIMP_LHS => simp_lhs(thm,ss,anet,ats,cs)


504 
 REW => rew(tapply(net_tac net i,thm),thm,ss,anet,ats,cs,true)


505 
 REFL => (ss, res1(thm,refl_thms,i), anet, ats, cs)


506 
 TRUE => try_true(res1(thm,refl_thms,i),ss,anet,ats,cs)


507 
 PROVE => (if if_fl then MK_EQ::SIMP_LHS::SPLIT::TRUE::ss


508 
else MK_EQ::SIMP_LHS::TRUE::ss, thm, anet, ats, cs)


509 
 POP_ARTR => (ss,thm,hd ats,tl ats,cs)


510 
 POP_CS => (ss,thm,anet,ats,tl cs)


511 
 SPLIT => split(thm,ss,anet,ats,cs);


512 


513 
fun exec(state as (s::ss, thm, _, _, _)) =


514 
if s=STOP then thm else exec(step(state));


515 


516 
in exec(ss, thm, Net.empty, [], []) end;


517 


518 


519 
(*ss = list of commands (not simpset!);


520 
fl = even use case splits to solve conditional rewrite rules;


521 
addhyps = add hyps to simpset*)


522 
fun EXEC_TAC (ss,fl,addhyps) simpset = METAHYPS


523 
(fn hyps =>


524 
case (if addhyps then simpset addrews hyps else simpset) of


525 
(SS{auto_tac,cong_net,simp_net,splits,split_consts,...}) =>


526 
PRIMITIVE(execute(ss,fl,auto_tac hyps,


527 
net_tac cong_net,splits,split_consts,


528 
simp_net, 1))


529 
THEN TRY(auto_tac hyps 1));


530 


531 
val SIMP_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,SPLIT,REFL,STOP],false,false);


532 


533 
val ASM_SIMP_TAC =


534 
EXEC_TAC([ASMS(0),MK_EQ,SIMP_LHS,SPLIT,REFL,STOP],false,true);


535 


536 
val SIMP_SPLIT2_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,SPLIT,REFL,STOP],true,false);


537 


538 
fun REWRITE (ss,fl) (SS{auto_tac,cong_net,simp_net,splits,split_consts,...}) =


539 
let val cong_tac = net_tac cong_net


540 
in fn thm =>


541 
let val state = thm RSN (2,red1)


542 
in execute(ss,fl,auto_tac[],cong_tac,splits,split_consts,simp_net,1)state


543 
end


544 
end;


545 


546 
val SIMP_THM = REWRITE ([ASMS(0),SIMP_LHS,SPLIT,REFL,STOP],false);


547 


548 


549 
(* Compute Congruence rules for individual constants using the substition


550 
rules *)


551 


552 
val subst_thms = map standard subst_thms;


553 


554 


555 
fun exp_app(0,t) = t


556 
 exp_app(i,t) = exp_app(i1,t $ Bound (i1));


557 


558 
fun exp_abs(Type("fun",[T1,T2]),t,i) =


559 
Abs("x"^string_of_int i,T1,exp_abs(T2,t,i+1))


560 
 exp_abs(T,t,i) = exp_app(i,t);


561 


562 
fun eta_Var(ixn,T) = exp_abs(T,Var(ixn,T),0);


563 


564 


565 
fun Pinst(f,fT,(eq,eqT),k,i,T,yik,Ts) =


566 
let fun xn_list(x,n) =


567 
let val ixs = map (fn i => (x^(radixstring(26,"a",i)),0)) (0 upto n);


568 
in map eta_Var (ixs ~~ (take(n+1,Ts))) end


569 
val lhs = list_comb(f,xn_list("X",k1))


570 
val rhs = list_comb(f,xn_list("X",i1) @ [Bound 0] @ yik)


571 
in Abs("", T, Const(eq,[fT,fT]>eqT) $ lhs $ rhs) end;


572 


573 
fun find_subst tsig T =


574 
let fun find (thm::thms) =


575 
let val (Const(_,cT), va, vb) = dest_red(hd(prems_of thm));


576 
val [P] = term_vars(concl_of thm) \\ [va,vb]


577 
val eqT::_ = binder_types cT


578 
in if Type.typ_instance(tsig,T,eqT) then Some(thm,va,vb,P)


579 
else find thms


580 
end


581 
 find [] = None


582 
in find subst_thms end;


583 


584 
fun mk_cong sg (f,aTs,rT) (refl,eq) =


585 
let val tsig = #tsig(Sign.rep_sg sg);


586 
val k = length aTs;


587 
fun ri((subst,va as Var(_,Ta),vb as Var(_,Tb),P),i,si,T,yik) =

231

588 
let val ca = cterm_of sg va


589 
and cx = cterm_of sg (eta_Var(("X"^si,0),T))


590 
val cb = cterm_of sg vb


591 
and cy = cterm_of sg (eta_Var(("Y"^si,0),T))


592 
val cP = cterm_of sg P


593 
and cp = cterm_of sg (Pinst(f,rT,eq,k,i,T,yik,aTs))

0

594 
in cterm_instantiate [(ca,cx),(cb,cy),(cP,cp)] subst end;


595 
fun mk(c,T::Ts,i,yik) =


596 
let val si = radixstring(26,"a",i)


597 
in case find_subst tsig T of


598 
None => mk(c,Ts,i1,eta_Var(("X"^si,0),T)::yik)


599 
 Some s => let val c' = c RSN (2,ri(s,i,si,T,yik))


600 
in mk(c',Ts,i1,eta_Var(("Y"^si,0),T)::yik) end


601 
end


602 
 mk(c,[],_,_) = c;


603 
in mk(refl,rev aTs,k1,[]) end;


604 


605 
fun mk_cong_type sg (f,T) =


606 
let val (aTs,rT) = strip_type T;


607 
val tsig = #tsig(Sign.rep_sg sg);


608 
fun find_refl(r::rs) =


609 
let val (Const(eq,eqT),_,_) = dest_red(concl_of r)


610 
in if Type.typ_instance(tsig, rT, hd(binder_types eqT))


611 
then Some(r,(eq,body_type eqT)) else find_refl rs


612 
end


613 
 find_refl([]) = None;


614 
in case find_refl refl_thms of


615 
None => []  Some(refl) => [mk_cong sg (f,aTs,rT) refl]


616 
end;


617 


618 
fun mk_cong_thy thy f =


619 
let val sg = sign_of thy;

611

620 
val T = case Sign.const_type sg f of

0

621 
None => error(f^" not declared")  Some(T) => T;


622 
val T' = incr_tvar 9 T;


623 
in mk_cong_type sg (Const(f,T'),T') end;


624 


625 
fun mk_congs thy = filter_out is_fact o flat o map (mk_cong_thy thy);


626 


627 
fun mk_typed_congs thy =


628 
let val sg = sign_of thy;


629 
val S0 = Type.defaultS(#tsig(Sign.rep_sg sg))


630 
fun readfT(f,s) =


631 
let val T = incr_tvar 9 (Sign.read_typ(sg,K(Some(S0))) s);

611

632 
val t = case Sign.const_type sg f of

0

633 
Some(_) => Const(f,T)  None => Free(f,T)


634 
in (t,T) end


635 
in flat o map (mk_cong_type sg o readfT) end;


636 


637 
(* This code is fishy, esp the "let val T' = ..."


638 
fun extract_free_congs() =


639 
let val {prop,sign,...} = rep_thm(topthm());


640 
val frees = add_term_frees(prop,[]);


641 
fun filter(Free(a,T as Type("fun",_))) =


642 
let val T' = incr_tvar 9 (Type.varifyT T)


643 
in [(Free(a,T),T)] end


644 
 filter _ = []


645 
in flat(map (mk_cong_type sign) (flat (map filter frees))) end;


646 
*)


647 


648 
end (* local *)


649 
end (* SIMP *);
