0

1 
(* Title: FOLP/simp


2 
ID: $Id$


3 
Author: Tobias Nipkow


4 
Copyright 1993 University of Cambridge


5 


6 
FOLP version of...


7 


8 
Generic simplifier, suitable for most logics. (from Provers)


9 


10 
This version allows instantiation of Vars in the subgoal, since the proof


11 
term must change.


12 
*)


13 


14 
signature SIMP_DATA =


15 
sig


16 
val case_splits : (thm * string) list


17 
val dest_red : term > term * term * term


18 
val mk_rew_rules : thm > thm list


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


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


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


22 
val refl_thms : thm list


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


24 
val trans_thms : thm list


25 
end;


26 


27 


28 
infix 4 addrews addcongs delrews delcongs setauto;


29 


30 
signature SIMP =


31 
sig


32 
type simpset


33 
val empty_ss : simpset


34 
val addcongs : simpset * thm list > simpset


35 
val addrews : simpset * thm list > simpset


36 
val delcongs : simpset * thm list > simpset


37 
val delrews : simpset * thm list > simpset


38 
val dest_ss : simpset > thm list * thm list


39 
val print_ss : simpset > unit


40 
val setauto : simpset * (int > tactic) > simpset


41 
val ASM_SIMP_CASE_TAC : simpset > int > tactic


42 
val ASM_SIMP_TAC : simpset > int > tactic


43 
val CASE_TAC : simpset > int > tactic


44 
val SIMP_CASE2_TAC : simpset > int > tactic


45 
val SIMP_THM : simpset > thm > thm


46 
val SIMP_TAC : simpset > int > tactic


47 
val SIMP_CASE_TAC : simpset > int > tactic


48 
val mk_congs : theory > string list > thm list


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


50 
(* temporarily disabled:


51 
val extract_free_congs : unit > thm list


52 
*)


53 
val tracing : bool ref


54 
end;


55 


56 
functor SimpFun (Simp_data: SIMP_DATA) : SIMP =


57 
struct


58 


59 
local open Simp_data Logic in


60 


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


62 
val lhs_of = #2 o dest_red;


63 
val rhs_of = #3 o dest_red;


64 


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


66 


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


68 


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


70 
fun lhs_insert_thm (th,net) =


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


72 
handle Net.INSERT => net;


73 


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


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


76 
rewrite rules are not ordered.*)


77 
fun net_tac net =


78 
SUBGOAL(fn (prem,i) =>

1459

79 
resolve_tac (Net.unify_term net (strip_assums_concl prem)) i);

0

80 


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


82 
fun lhs_net_tac net =


83 
SUBGOAL(fn (prem,i) =>

1459

84 
biresolve_tac (Net.unify_term net


85 
(lhs_of (strip_assums_concl prem))) i);

0

86 


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


88 


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


90 


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


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


93 


94 
fun var_lhs(thm,i) =


95 
let fun var(Var _) = true


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


97 
 var(f$_) = var f


98 
 var _ = false;


99 
in var(lhs_of_eq i thm) end;


100 


101 
fun contains_op opns =


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


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


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


105 
contains _ = false;


106 
in contains end;


107 


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


109 


110 
val (normI_thms,normE_thms) = split_list norm_thms;


111 


112 
(*Get the norm constants from norm_thms*)


113 
val norms =


114 
let fun norm thm =


115 
case lhs_of(concl_of thm) of

1459

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


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

0

118 
in map norm normE_thms end;


119 


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

1459

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

0

122 


123 
val refl_tac = resolve_tac refl_thms;


124 


125 
fun find_res thms thm =


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


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


128 
in find thms end;


129 


130 
val mk_trans = find_res trans_thms;


131 


132 
fun mk_trans2 thm =


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


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


135 
in mk trans_thms end;


136 


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

1512

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

1459

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

0

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


141 


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


143 


144 


145 
(**** Adding "NORM" tags ****)


146 


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


148 
fun cong_const cong =


149 
case head_of (lhs_of (concl_of cong)) of

1459

150 
Const(c,_) => c


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

0

152 


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


154 
val atomic = null o strip_assums_hyp;


155 


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


157 
fun add_hidden_vars ccs =


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

1459

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


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


161 
in case f of


162 
Const(c,T) =>


163 
if c mem ccs


164 
then foldr add_hvars (args,hvars)


165 
else add_term_vars(tm,hvars)


166 
 _ => add_term_vars(tm,hvars)


167 
end


168 
 _ => hvars;

0

169 
in add_hvars end;


170 


171 
fun add_new_asm_vars new_asms =


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

1459

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


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


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


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


177 
else vars


178 
end


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


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


181 
 r$s => (case head_of tm of


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


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


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


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


186 
 _ => vars

0

187 
in add_vars end;


188 


189 


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


191 
let val thm' = mk_trans2 thm;


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


193 
val nops = nprems_of thm'


194 
val lhs = rhs_of_eq 1 thm'


195 
val rhs = lhs_of_eq nops thm'


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


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


198 
val hvars = add_new_asm_vars new_asms (rhs,hvars)


199 
fun it_asms (asm,hvars) =

1459

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


201 
else add_term_frees(asm,hvars)

0

202 
val hvars = foldr it_asms (asms,hvars)


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


204 
val refl1_tac = refl_tac 1


205 
val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops)

1459

206 
(STATE(fn thm =>


207 
case head_of(rhs_of_eq 1 thm) of


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


209 
else resolve_tac normI_thms 1 ORELSE refl1_tac


210 
 Const _ => resolve_tac normI_thms 1 ORELSE


211 
resolve_tac congs 1 ORELSE refl1_tac


212 
 Free _ => resolve_tac congs 1 ORELSE refl1_tac


213 
 _ => refl1_tac))

1512

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

0

215 
in thm'' end;


216 


217 
fun add_norm_tags congs =


218 
let val ccs = map cong_const congs

1459

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


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

0

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


222 


223 
fun normed_rews congs =


224 
let val add_norms = add_norm_tags congs;


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


226 
end;


227 

1459

228 
fun NORM norm_lhs_tac = EVERY'[rtac red2 , norm_lhs_tac, refl_tac];

0

229 


230 
val trans_norms = map mk_trans normE_thms;


231 


232 


233 
(* SIMPSET *)


234 


235 
datatype simpset =

1459

236 
SS of {auto_tac: int > tactic,


237 
congs: thm list,


238 
cong_net: thm Net.net,


239 
mk_simps: thm > thm list,


240 
simps: (thm * thm list) list,


241 
simp_net: thm Net.net}

0

242 


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

1459

244 
mk_simps=normed_rews[], simps=[], simp_net=Net.empty};

0

245 


246 
(** Insertion of congruences and rewrites **)


247 


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


249 
fun insert_thm_warn (th,net) =


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


251 
handle Net.INSERT =>


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


253 
net);


254 


255 
val insert_thms = foldr insert_thm_warn;


256 


257 
fun addrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) =


258 
let val thms = mk_simps thm


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


260 
simps = (thm,thms)::simps, simp_net = insert_thms(thms,simp_net)}


261 
end;


262 


263 
val op addrews = foldl addrew;


264 


265 
fun op addcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, 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 
end;


271 


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


273 


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


275 
fun delete_thm_warn (th,net) =


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


277 
handle Net.DELETE =>


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


279 
net);


280 


281 
val delete_thms = foldr delete_thm_warn;


282 


283 
fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) =


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


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


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


287 
mk_simps= normed_rews congs', simps=simps, simp_net=simp_net}


288 
end;


289 


290 
fun delrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) =


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

1459

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

0

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

1459

294 
print_thm thm;


295 
([],simps'))

0

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


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


298 
simps = simps', simp_net = delete_thms(thms,simp_net)}


299 
end;


300 


301 
val op delrews = foldl delrew;


302 


303 


304 
fun op setauto(SS{congs,cong_net,mk_simps,simps,simp_net,...}, auto_tac) =


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


306 
simps=simps, simp_net=simp_net};


307 


308 


309 
(** Inspection of a simpset **)


310 


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


312 


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

1459

314 
(writeln"Congruences:"; prths congs;


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

0

316 


317 


318 
(* Rewriting with conditionals *)


319 


320 
val (case_thms,case_consts) = split_list case_splits;


321 
val case_rews = map mk_trans case_thms;


322 


323 
fun if_rewritable ifc i thm =


324 
let val tm = goal_concl i thm

1459

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


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


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


328 
 nobound(_) = true;


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


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


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


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


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


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


335 
 find_if(_) = false;

0

336 
in find_if(tm,0) end;


337 


338 
fun IF1_TAC cong_tac i =

1512

339 
let fun seq_try (ifth::ifths,ifc::ifcs) thm =


340 
(COND (if_rewritable ifc i) (DETERM(rtac ifth i))


341 
(seq_try(ifths,ifcs))) thm


342 
 seq_try([],_) thm = no_tac thm


343 
and try_rew thm = (seq_try(case_rews,case_consts) ORELSE one_subt) thm

1459

344 
and one_subt thm =


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

1512

346 
fun loop thm =


347 
COND test no_tac


348 
((try_rew THEN DEPTH_FIRST test (refl_tac i))


349 
ORELSE (refl_tac i THEN loop)) thm


350 
in (cong_tac THEN loop) thm end


351 
in COND (may_match(case_consts,i)) try_rew no_tac end;

0

352 


353 
fun CASE_TAC (SS{cong_net,...}) i =


354 
let val cong_tac = net_tac cong_net i


355 
in NORM (IF1_TAC cong_tac) i end;


356 


357 
(* Rewriting Automaton *)


358 


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

1459

360 
 PROVE  POP_CS  POP_ARTR  IF;

0

361 
(*


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


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


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


365 
TRUE => prs("TRUE")  PROVE => prs("PROVE")  POP_CS => prs("POP_CS")  IF


366 
=> prs("IF");


367 
*)


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


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

1459

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

0

371 


372 
(** Tracing **)


373 


374 
val tracing = ref false;


375 


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


377 
fun variants_abs ([],P) = P


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


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


380 


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


382 
fun prepare_goal i st =


383 
let val subgi = nth_subgoal i st

1459

384 
val params = rev(strip_params subgi)

0

385 
in variants_abs (params, strip_assums_concl subgi) end;


386 


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


388 
fun pr_goal_lhs i st =


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

1459

390 
(lhs_of (prepare_goal i st)));

0

391 


392 
(*print conclusion of subgoal i*)


393 
fun pr_goal_concl i st =


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


395 


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


397 
fun pr_goals (i,j) st =


398 
if i>j then ()


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


400 


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


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


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


404 
if !tracing


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


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

1459

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

0

408 
else ();


409 
writeln"" )


410 
else ();


411 


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


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

1459

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


415 
else strip_varify(B,n1,vs)

0

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

1459

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

0

418 
 strip_varify _ = [];


419 


420 
fun execute(ss,if_fl,auto_tac,cong_tac,net,i,thm) = let


421 


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


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


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

1512

425 
else case Sequence.pull(cong_tac i thm) of

1459

426 
Some(thm',_) =>


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


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


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


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


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


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


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

0

434 


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


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


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


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

1459

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


440 
val new_rws = flat(map mk_rew_rules thms);


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


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

0

443 
in if !tracing andalso not(null new_rws)

1459

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


445 
else ();


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

0

447 
end;


448 


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


450 
Some(thm',seq') =>

1459

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


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


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


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


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


456 
end

0

457 
 None => if more

1512

458 
then rew((lhs_net_tac anet i THEN assume_tac i) thm,

1459

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


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

0

461 


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

1512

463 
case Sequence.pull(auto_tac i thm) of

0

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


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

1459

466 
in if !tracing


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


468 
pr_goal_concl i thm; writeln"")


469 
else ();


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


471 
end;

0

472 


473 
fun if_exp(thm,ss,anet,ats,cs) =

1512

474 
case Sequence.pull (IF1_TAC (cong_tac i) i thm) of

1459

475 
Some(thm',_) => (SIMP_LHS::IF::ss,thm',anet,ats,cs)


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

0

477 


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

1459

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


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


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

1512

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

1459

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


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


485 
 PROVE => (if if_fl then MK_EQ::SIMP_LHS::IF::TRUE::ss


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


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


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


489 
 IF => if_exp(thm,ss,anet,ats,cs);

0

490 


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

1459

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

0

493 


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


495 


496 


497 
fun EXEC_TAC(ss,fl) (SS{auto_tac,cong_net,simp_net,...}) =


498 
let val cong_tac = net_tac cong_net

1512

499 
in fn i =>


500 
(fn thm =>


501 
if i <= 0 orelse nprems_of thm < i then Sequence.null


502 
else Sequence.single(execute(ss,fl,auto_tac,cong_tac,simp_net,i,thm)))


503 
THEN TRY(auto_tac i)

0

504 
end;


505 


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


507 
val SIMP_CASE_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,IF,REFL,STOP],false);


508 


509 
val ASM_SIMP_TAC = EXEC_TAC([ASMS(0),MK_EQ,SIMP_LHS,REFL,STOP],false);


510 
val ASM_SIMP_CASE_TAC = EXEC_TAC([ASMS(0),MK_EQ,SIMP_LHS,IF,REFL,STOP],false);


511 


512 
val SIMP_CASE2_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,IF,REFL,STOP],true);


513 


514 
fun REWRITE (ss,fl) (SS{auto_tac,cong_net,simp_net,...}) =


515 
let val cong_tac = net_tac cong_net


516 
in fn thm => let val state = thm RSN (2,red1)

1459

517 
in execute(ss,fl,auto_tac,cong_tac,simp_net,1,state) end

0

518 
end;


519 


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


521 


522 


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


524 
rules *)


525 


526 
val subst_thms = map standard subst_thms;


527 


528 


529 
fun exp_app(0,t) = t


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


531 


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

1459

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

0

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


535 


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


537 


538 


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


540 
let fun xn_list(x,n) =

1459

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


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

0

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


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


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


546 


547 
fun find_subst tsig T =


548 
let fun find (thm::thms) =

1459

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


550 
val [P] = add_term_vars(concl_of thm,[]) \\ [va,vb]


551 
val eqT::_ = binder_types cT

0

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

1459

553 
else find thms


554 
end

0

555 
 find [] = None


556 
in find subst_thms end;


557 


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


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


560 
val k = length aTs;


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

1459

562 
let val ca = cterm_of sg va


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


564 
val cb = cterm_of sg vb


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


566 
val cP = cterm_of sg P


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


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

0

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

1459

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


571 
in case find_subst tsig T of


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


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


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


575 
end

0

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


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


578 


579 
fun mk_cong_type sg (f,T) =


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


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


582 
fun find_refl(r::rs) =

1459

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


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


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


586 
end

0

587 
 find_refl([]) = None;


588 
in case find_refl refl_thms of


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


590 
end;


591 


592 
fun mk_cong_thy thy f =


593 
let val sg = sign_of thy;

611

594 
val T = case Sign.const_type sg f of

1459

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

0

596 
val T' = incr_tvar 9 T;


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


598 


599 
fun mk_congs thy = flat o map (mk_cong_thy thy);


600 


601 
fun mk_typed_congs thy =


602 
let val sg = sign_of thy;


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


604 
fun readfT(f,s) =

1459

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


606 
val t = case Sign.const_type sg f of


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


608 
in (t,T) end

0

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


610 


611 
end (* local *)


612 
end (* SIMP *);
