author  wenzelm 
Fri, 01 Jan 2016 10:49:00 +0100  
changeset 62020  5d208fd2507d 
parent 61268  abe08fb15a12 
child 69593  3dda49e08b9d 
permissions  rwrr 
29265
5b4247055bd7
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents:
26939
diff
changeset

1 
(* Title: FOLP/simp.ML 
0  2 
Author: Tobias Nipkow 
3 
Copyright 1993 University of Cambridge 

4 

5 
FOLP version of... 

6 

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

8 

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

10 
term must change. 

11 
*) 

12 

13 
signature SIMP_DATA = 

14 
sig 

15 
val case_splits : (thm * string) list 

16 
val dest_red : term > term * term * term 

17 
val mk_rew_rules : thm > thm list 

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

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

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

21 
val refl_thms : thm list 

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

23 
val trans_thms : thm list 

24 
end; 

25 

26 

60644  27 
infix 4 addcongs delrews delcongs setauto; 
0  28 

29 
signature SIMP = 

30 
sig 

31 
type simpset 

32 
val empty_ss : simpset 

33 
val addcongs : simpset * thm list > simpset 

60644  34 
val addrew : Proof.context > thm > simpset > simpset 
0  35 
val delcongs : simpset * thm list > simpset 
36 
val delrews : simpset * thm list > simpset 

37 
val dest_ss : simpset > thm list * thm list 

60645
2affe7e97a34
eliminated spurious warning/tracing messages  avoid Display.string_of_thm_without_context;
wenzelm
parents:
60644
diff
changeset

38 
val print_ss : Proof.context > simpset > unit 
60774  39 
val setauto : simpset * (Proof.context > int > tactic) > simpset 
60646  40 
val ASM_SIMP_CASE_TAC : Proof.context > simpset > int > tactic 
41 
val ASM_SIMP_TAC : Proof.context > simpset > int > tactic 

60754  42 
val CASE_TAC : Proof.context > simpset > int > tactic 
60646  43 
val SIMP_CASE2_TAC : Proof.context > simpset > int > tactic 
44 
val SIMP_THM : Proof.context > simpset > thm > thm 

45 
val SIMP_TAC : Proof.context > simpset > int > tactic 

46 
val SIMP_CASE_TAC : Proof.context > simpset > int > tactic 

60789  47 
val mk_congs : Proof.context > string list > thm list 
48 
val mk_typed_congs : Proof.context > (string * string) list > thm list 

0  49 
(* temporarily disabled: 
50 
val extract_free_congs : unit > thm list 

51 
*) 

32740  52 
val tracing : bool Unsynchronized.ref 
0  53 
end; 
54 

32449  55 
functor SimpFun (Simp_data: SIMP_DATA) : SIMP = 
0  56 
struct 
57 

19805  58 
local open Simp_data in 
0  59 

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

61 
val lhs_of = #2 o dest_red; 

62 
val rhs_of = #3 o dest_red; 

63 

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

65 

22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
21287
diff
changeset

66 
fun eq_brl ((b1 : bool, th1), (b2, th2)) = b1 = b2 andalso Thm.eq_thm_prop (th1, th2); 
0  67 

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

33339  69 
fun lhs_insert_thm th net = 
59582  70 
Net.insert_term eq_brl (lhs_of (Thm.concl_of th), (false,th)) net 
0  71 
handle Net.INSERT => net; 
72 

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

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

75 
rewrite rules are not ordered.*) 

60756  76 
fun net_tac ctxt net = 
77 
SUBGOAL(fn (prem, i) => 

78 
resolve_tac ctxt (Net.unify_term net (Logic.strip_assums_concl prem)) i); 

0  79 

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

60756  81 
fun lhs_net_tac ctxt net = 
32449  82 
SUBGOAL(fn (prem,i) => 
60756  83 
biresolve_tac ctxt (Net.unify_term net 
19805  84 
(lhs_of (Logic.strip_assums_concl prem))) i); 
0  85 

59582  86 
fun nth_subgoal i thm = nth (Thm.prems_of thm) (i  1); 
0  87 

19805  88 
fun goal_concl i thm = Logic.strip_assums_concl (nth_subgoal i thm); 
0  89 

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

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

92 

93 
fun var_lhs(thm,i) = 

94 
let fun var(Var _) = true 

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

96 
 var(f$_) = var f 

97 
 var _ = false; 

98 
in var(lhs_of_eq i thm) end; 

99 

100 
fun contains_op opns = 

36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36603
diff
changeset

101 
let fun contains(Const(s,_)) = member (op =) opns s  
0  102 
contains(s$t) = contains s orelse contains t  
103 
contains(Abs(_,_,t)) = contains t  

104 
contains _ = false; 

105 
in contains end; 

106 

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

108 

109 
val (normI_thms,normE_thms) = split_list norm_thms; 

110 

111 
(*Get the norm constants from norm_thms*) 

112 
val norms = 

32449  113 
let fun norm thm = 
59582  114 
case lhs_of (Thm.concl_of thm) of 
1459  115 
Const(n,_)$_ => n 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
30190
diff
changeset

116 
 _ => error "No constant in lhs of a norm_thm" 
0  117 
in map norm normE_thms end; 
118 

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

36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36603
diff
changeset

120 
Const(s,_)$_ => member (op =) norms s  _ => false; 
0  121 

60756  122 
fun refl_tac ctxt = resolve_tac ctxt refl_thms; 
0  123 

124 
fun find_res thms thm = 

32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
30190
diff
changeset

125 
let fun find [] = error "Check Simp_Data" 
6969  126 
 find(th::thms) = thm RS th handle THM _ => find thms 
0  127 
in find thms end; 
128 

129 
val mk_trans = find_res trans_thms; 

130 

131 
fun mk_trans2 thm = 

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

6969  133 
 mk(t::ts) = (thm RSN (2,t)) handle THM _ => mk ts 
0  134 
in mk trans_thms end; 
135 

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

4271
3a82492e70c5
changed Pure/Sequence interface  isatool fixseq;
wenzelm
parents:
3537
diff
changeset

137 
fun one_result(tac,thm) = case Seq.pull(tac thm) of 
15531  138 
SOME(thm',_) => thm' 
139 
 NONE => raise THM("Simplifier: could not continue", 0, [thm]); 

0  140 

60756  141 
fun res1 ctxt (thm,thms,i) = one_result (resolve_tac ctxt thms i,thm); 
0  142 

143 

144 
(**** Adding "NORM" tags ****) 

145 

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

32449  147 
fun cong_const cong = 
59582  148 
case head_of (lhs_of (Thm.concl_of cong)) of 
1459  149 
Const(c,_) => c 
150 
 _ => "" (*a placeholder distinct from const names*); 

0  151 

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

19805  153 
val atomic = null o Logic.strip_assums_hyp; 
0  154 

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

156 
fun add_hidden_vars ccs = 

21078  157 
let fun add_hvars tm hvars = case tm of 
44121  158 
Abs(_,_,body) => Misc_Legacy.add_term_vars(body,hvars) 
32449  159 
 _$_ => let val (f,args) = strip_comb tm 
1459  160 
in case f of 
32449  161 
Const(c,T) => 
21078  162 
if member (op =) ccs c 
163 
then fold_rev add_hvars args hvars 

44121  164 
else Misc_Legacy.add_term_vars (tm, hvars) 
165 
 _ => Misc_Legacy.add_term_vars (tm, hvars) 

1459  166 
end 
167 
 _ => hvars; 

0  168 
in add_hvars end; 
169 

170 
fun add_new_asm_vars new_asms = 

21078  171 
let fun itf (tm, at) vars = 
44121  172 
if at then vars else Misc_Legacy.add_term_vars(tm,vars) 
1459  173 
fun add_list(tm,al,vars) = let val (_,tml) = strip_comb tm 
174 
in if length(tml)=length(al) 

21078  175 
then fold_rev itf (tml ~~ al) vars 
1459  176 
else vars 
177 
end 

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

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

180 
 r$s => (case head_of tm of 

17325  181 
Const(c,T) => (case AList.lookup (op =) new_asms c of 
15531  182 
NONE => add_vars(r,add_vars(s,vars)) 
183 
 SOME(al) => add_list(tm,al,vars)) 

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

0  186 
in add_vars end; 
187 

188 

60756  189 
fun add_norms ctxt (congs,ccs,new_asms) thm = 
0  190 
let val thm' = mk_trans2 thm; 
191 
(* thm': [?z > l; Prems; r > ?t] ==> ?z > ?t *) 

59582  192 
val nops = Thm.nprems_of thm' 
0  193 
val lhs = rhs_of_eq 1 thm' 
194 
val rhs = lhs_of_eq nops thm' 

59582  195 
val asms = tl(rev(tl(Thm.prems_of thm'))) 
21078  196 
val hvars = fold_rev (add_hidden_vars ccs) (lhs::rhs::asms) [] 
0  197 
val hvars = add_new_asm_vars new_asms (rhs,hvars) 
21078  198 
fun it_asms asm hvars = 
1459  199 
if atomic asm then add_new_asm_vars new_asms (asm,hvars) 
44121  200 
else Misc_Legacy.add_term_frees(asm,hvars) 
21078  201 
val hvars = fold_rev it_asms asms hvars 
0  202 
val hvs = map (#1 o dest_Var) hvars 
3537  203 
fun norm_step_tac st = st > 
32449  204 
(case head_of(rhs_of_eq 1 st) of 
60756  205 
Var(ixn,_) => if member (op =) hvs ixn then refl_tac ctxt 1 
206 
else resolve_tac ctxt normI_thms 1 ORELSE refl_tac ctxt 1 

207 
 Const _ => resolve_tac ctxt normI_thms 1 ORELSE 

208 
resolve_tac ctxt congs 1 ORELSE refl_tac ctxt 1 

209 
 Free _ => resolve_tac ctxt congs 1 ORELSE refl_tac ctxt 1 

210 
 _ => refl_tac ctxt 1) 

3537  211 
val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops) norm_step_tac 
15531  212 
val SOME(thm'',_) = Seq.pull(add_norm_tac thm') 
0  213 
in thm'' end; 
214 

60756  215 
fun add_norm_tags ctxt congs = 
0  216 
let val ccs = map cong_const congs 
33317  217 
val new_asms = filter (exists not o #2) 
59582  218 
(ccs ~~ (map (map atomic o Thm.prems_of) congs)); 
60756  219 
in add_norms ctxt (congs,ccs,new_asms) end; 
0  220 

60756  221 
fun normed_rews ctxt congs = 
60644  222 
let 
60756  223 
val add_norms = add_norm_tags ctxt congs 
224 
fun normed thm = 

59170  225 
let 
60644  226 
val ctxt' = Variable.declare_thm thm ctxt; 
59170  227 
in Variable.tradeT (K (map (add_norms o mk_trans) o maps mk_rew_rules)) ctxt [thm] end 
60644  228 
in normed end; 
0  229 

60756  230 
fun NORM ctxt norm_lhs_tac = EVERY' [resolve_tac ctxt [red2], norm_lhs_tac, refl_tac ctxt]; 
0  231 

232 
val trans_norms = map mk_trans normE_thms; 

233 

234 

235 
(* SIMPSET *) 

236 

237 
datatype simpset = 

60774  238 
SS of {auto_tac: Proof.context > int > tactic, 
1459  239 
congs: thm list, 
240 
cong_net: thm Net.net, 

60644  241 
mk_simps: Proof.context > thm > thm list, 
1459  242 
simps: (thm * thm list) list, 
243 
simp_net: thm Net.net} 

0  244 

60774  245 
val empty_ss = SS{auto_tac= K (K no_tac), congs=[], cong_net=Net.empty, 
60756  246 
mk_simps = fn ctxt => normed_rews ctxt [], simps=[], simp_net=Net.empty}; 
0  247 

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

249 

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

60645
2affe7e97a34
eliminated spurious warning/tracing messages  avoid Display.string_of_thm_without_context;
wenzelm
parents:
60644
diff
changeset

251 
fun insert_thm th net = 
59582  252 
Net.insert_term Thm.eq_thm_prop (Thm.concl_of th, th) net 
60645
2affe7e97a34
eliminated spurious warning/tracing messages  avoid Display.string_of_thm_without_context;
wenzelm
parents:
60644
diff
changeset

253 
handle Net.INSERT => net; 
0  254 

60645
2affe7e97a34
eliminated spurious warning/tracing messages  avoid Display.string_of_thm_without_context;
wenzelm
parents:
60644
diff
changeset

255 
val insert_thms = fold_rev insert_thm; 
0  256 

60644  257 
fun addrew ctxt thm (SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}) = 
258 
let val thms = mk_simps ctxt thm 

0  259 
in SS{auto_tac=auto_tac,congs=congs, cong_net=cong_net, mk_simps=mk_simps, 
21078  260 
simps = (thm,thms)::simps, simp_net = insert_thms thms simp_net} 
0  261 
end; 
262 

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

264 
let val congs' = thms @ congs; 

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

21078  266 
cong_net= insert_thms (map mk_trans thms) cong_net, 
60756  267 
mk_simps = fn ctxt => normed_rews ctxt congs', simps=simps, simp_net=simp_net} 
0  268 
end; 
269 

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

271 

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

60645
2affe7e97a34
eliminated spurious warning/tracing messages  avoid Display.string_of_thm_without_context;
wenzelm
parents:
60644
diff
changeset

273 
fun delete_thm th net = 
59582  274 
Net.delete_term Thm.eq_thm_prop (Thm.concl_of th, th) net 
60645
2affe7e97a34
eliminated spurious warning/tracing messages  avoid Display.string_of_thm_without_context;
wenzelm
parents:
60644
diff
changeset

275 
handle Net.DELETE => net; 
0  276 

60645
2affe7e97a34
eliminated spurious warning/tracing messages  avoid Display.string_of_thm_without_context;
wenzelm
parents:
60644
diff
changeset

277 
val delete_thms = fold_rev delete_thm; 
0  278 

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

22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
21287
diff
changeset

280 
let val congs' = fold (remove Thm.eq_thm_prop) thms congs 
0  281 
in SS{auto_tac=auto_tac, congs= congs', 
21078  282 
cong_net= delete_thms (map mk_trans thms) cong_net, 
60756  283 
mk_simps= fn ctxt => normed_rews ctxt congs', simps=simps, simp_net=simp_net} 
0  284 
end; 
285 

33245  286 
fun delrew thm (SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}) = 
0  287 
let fun find((p as (th,ths))::ps',ps) = 
22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
21287
diff
changeset

288 
if Thm.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps) 
60645
2affe7e97a34
eliminated spurious warning/tracing messages  avoid Display.string_of_thm_without_context;
wenzelm
parents:
60644
diff
changeset

289 
 find([],simps') = ([], simps') 
0  290 
val (thms,simps') = find(simps,[]) 
291 
in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps, 

21078  292 
simps = simps', simp_net = delete_thms thms simp_net } 
0  293 
end; 
294 

33245  295 
fun ss delrews thms = fold delrew thms ss; 
0  296 

297 

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

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

300 
simps=simps, simp_net=simp_net}; 

301 

302 

303 
(** Inspection of a simpset **) 

304 

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

306 

60645
2affe7e97a34
eliminated spurious warning/tracing messages  avoid Display.string_of_thm_without_context;
wenzelm
parents:
60644
diff
changeset

307 
fun print_ss ctxt (SS{congs,simps,...}) = 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
30190
diff
changeset

308 
writeln (cat_lines 
61268  309 
(["Congruences:"] @ map (Thm.string_of_thm ctxt) congs @ 
310 
["Rewrite Rules:"] @ map (Thm.string_of_thm ctxt o #1) simps)); 

0  311 

312 

313 
(* Rewriting with conditionals *) 

314 

315 
val (case_thms,case_consts) = split_list case_splits; 

316 
val case_rews = map mk_trans case_thms; 

317 

318 
fun if_rewritable ifc i thm = 

319 
let val tm = goal_concl i thm 

1459  320 
fun nobound(Abs(_,_,tm),j,k) = nobound(tm,j,k+1) 
321 
 nobound(s$t,j,k) = nobound(s,j,k) andalso nobound(t,j,k) 

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

323 
 nobound(_) = true; 

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

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

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

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

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

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

330 
 find_if(_) = false; 

0  331 
in find_if(tm,0) end; 
332 

60754  333 
fun IF1_TAC ctxt cong_tac i = 
32449  334 
let fun seq_try (ifth::ifths,ifc::ifcs) thm = 
60754  335 
(COND (if_rewritable ifc i) (DETERM(resolve_tac ctxt [ifth] i)) 
1512  336 
(seq_try(ifths,ifcs))) thm 
337 
 seq_try([],_) thm = no_tac thm 

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

1459  339 
and one_subt thm = 
59582  340 
let val test = has_fewer_prems (Thm.nprems_of thm + 1) 
32449  341 
fun loop thm = 
342 
COND test no_tac 

60756  343 
((try_rew THEN DEPTH_FIRST test (refl_tac ctxt i)) 
344 
ORELSE (refl_tac ctxt i THEN loop)) thm 

1512  345 
in (cong_tac THEN loop) thm end 
346 
in COND (may_match(case_consts,i)) try_rew no_tac end; 

0  347 

60754  348 
fun CASE_TAC ctxt (SS{cong_net,...}) i = 
60756  349 
let val cong_tac = net_tac ctxt cong_net i 
350 
in NORM ctxt (IF1_TAC ctxt cong_tac) i end; 

351 

0  352 

353 
(* Rewriting Automaton *) 

354 

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

1459  356 
 PROVE  POP_CS  POP_ARTR  IF; 
22578  357 

0  358 
fun simp_refl([],_,ss) = ss 
359 
 simp_refl(a'::ns,a,ss) = if a'=a then simp_refl(ns,a,SIMP_LHS::REFL::ss) 

1459  360 
else simp_refl(ns,a,ASMS(a)::SIMP_LHS::REFL::POP_ARTR::ss); 
0  361 

362 
(** Tracing **) 

363 

32740  364 
val tracing = Unsynchronized.ref false; 
0  365 

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

367 
fun variants_abs ([],P) = P 

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

42284  369 
variants_abs (aTs, #2 (Syntax_Trans.variant_abs(a,T,P))); 
0  370 

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

372 
fun prepare_goal i st = 

373 
let val subgi = nth_subgoal i st 

19805  374 
val params = rev (Logic.strip_params subgi) 
375 
in variants_abs (params, Logic.strip_assums_concl subgi) end; 

0  376 

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

60646  378 
fun pr_goal_lhs ctxt i st = 
379 
writeln (Syntax.string_of_term ctxt (lhs_of (prepare_goal i st))); 

0  380 

381 
(*print conclusion of subgoal i*) 

60646  382 
fun pr_goal_concl ctxt i st = 
383 
writeln (Syntax.string_of_term ctxt (prepare_goal i st)) 

0  384 

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

60646  386 
fun pr_goals ctxt (i,j) st = 
0  387 
if i>j then () 
60646  388 
else (pr_goal_concl ctxt i st; pr_goals ctxt (i+1,j) st); 
0  389 

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

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

60646  392 
fun pr_rew ctxt (i,n,thm,thm',not_asms) = 
0  393 
if !tracing 
394 
then (if not_asms then () else writeln"Assumption used in"; 

60646  395 
pr_goal_lhs ctxt i thm; writeln">"; pr_goal_lhs ctxt (i+n) thm'; 
396 
if n>0 then (writeln"Conditions:"; pr_goals ctxt (i, i+n1) thm') 

0  397 
else (); 
398 
writeln"" ) 

399 
else (); 

400 

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

56245  402 
fun strip_varify(Const(@{const_name Pure.imp}, _) $ H $ B, n, vs) = 
1459  403 
if n=0 then subst_bounds(vs,H)::strip_varify(B,0,vs) 
404 
else strip_varify(B,n1,vs) 

56245  405 
 strip_varify(Const(@{const_name Pure.all},_)$Abs(_,T,t), n, vs) = 
1459  406 
strip_varify(t,n,Var(("?",length vs),T)::vs) 
0  407 
 strip_varify _ = []; 
408 

60646  409 
fun execute ctxt (ss,if_fl,auto_tac,cong_tac,net,i,thm) = 
410 
let 

0  411 

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

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

60756  414 
if lhs_is_NORM(thm,i) then (ss, res1 ctxt (thm,trans_norms,i), anet,ats,cs) 
4271
3a82492e70c5
changed Pure/Sequence interface  isatool fixseq;
wenzelm
parents:
3537
diff
changeset

415 
else case Seq.pull(cong_tac i thm) of 
15531  416 
SOME(thm',_) => 
59582  417 
let val ps = Thm.prems_of thm 
418 
and ps' = Thm.prems_of thm'; 

1459  419 
val n = length(ps')length(ps); 
42364  420 
val a = length(Logic.strip_assums_hyp(nth ps (i  1))) 
33955  421 
val l = map (length o Logic.strip_assums_hyp) (take n (drop (i1) ps')); 
1459  422 
in (simp_refl(rev(l),a,REW::ss),thm',anet,ats,cs) end 
15531  423 
 NONE => (REW::ss,thm,anet,ats,cs); 
0  424 

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

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

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

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

60646  429 
val thms = map (Thm.trivial o Thm.cterm_of ctxt) As; 
32952  430 
val new_rws = maps mk_rew_rules thms; 
431 
val rwrls = map mk_trans (maps mk_rew_rules thms); 

33339  432 
val anet' = fold_rev lhs_insert_thm rwrls anet; 
60645
2affe7e97a34
eliminated spurious warning/tracing messages  avoid Display.string_of_thm_without_context;
wenzelm
parents:
60644
diff
changeset

433 
in (ss,thm,anet',anet::ats,cs) end; 
0  434 

4271
3a82492e70c5
changed Pure/Sequence interface  isatool fixseq;
wenzelm
parents:
3537
diff
changeset

435 
fun rew(seq,thm,ss,anet,ats,cs, more) = case Seq.pull seq of 
15531  436 
SOME(thm',seq') => 
59582  437 
let val n = (Thm.nprems_of thm')  (Thm.nprems_of thm) 
60646  438 
in pr_rew ctxt (i,n,thm,thm',more); 
1459  439 
if n=0 then (SIMP_LHS::ss, thm', anet, ats, cs) 
440 
else ((replicate n PROVE) @ (POP_CS::SIMP_LHS::ss), 

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

442 
end 

15531  443 
 NONE => if more 
60756  444 
then rew((lhs_net_tac ctxt anet i THEN assume_tac ctxt i) thm, 
1459  445 
thm,ss,anet,ats,cs,false) 
446 
else (ss,thm,anet,ats,cs); 

0  447 

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

60774  449 
case Seq.pull(auto_tac ctxt i thm) of 
15531  450 
SOME(thm',_) => (ss,thm',anet,ats,cs) 
451 
 NONE => let val (ss0,thm0,anet0,ats0,seq,more)::cs0 = cs 

1459  452 
in if !tracing 
453 
then (writeln"*** Failed to prove precondition. Normal form:"; 

60646  454 
pr_goal_concl ctxt i thm; writeln"") 
1459  455 
else (); 
456 
rew(seq,thm0,ss0,anet0,ats0,cs0,more) 

457 
end; 

0  458 

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

60754  460 
case Seq.pull (IF1_TAC ctxt (cong_tac i) i thm) of 
15531  461 
SOME(thm',_) => (SIMP_LHS::IF::ss,thm',anet,ats,cs) 
462 
 NONE => (ss,thm,anet,ats,cs); 

0  463 

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

60756  465 
MK_EQ => (ss, res1 ctxt (thm,[red2],i), anet, ats, cs) 
1459  466 
 ASMS(a) => add_asms(ss,thm,a,anet,ats,cs) 
467 
 SIMP_LHS => simp_lhs(thm,ss,anet,ats,cs) 

60756  468 
 REW => rew(net_tac ctxt net i thm,thm,ss,anet,ats,cs,true) 
469 
 REFL => (ss, res1 ctxt (thm,refl_thms,i), anet, ats, cs) 

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

1459  471 
 PROVE => (if if_fl then MK_EQ::SIMP_LHS::IF::TRUE::ss 
472 
else MK_EQ::SIMP_LHS::TRUE::ss, thm, anet, ats, cs) 

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

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

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

0  476 

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

1459  478 
if s=STOP then thm else exec(step(state)); 
0  479 

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

481 

482 

60646  483 
fun EXEC_TAC ctxt (ss,fl) (SS{auto_tac,cong_net,simp_net,...}) = 
60756  484 
let val cong_tac = net_tac ctxt cong_net 
32449  485 
in fn i => 
1512  486 
(fn thm => 
59582  487 
if i <= 0 orelse Thm.nprems_of thm < i then Seq.empty 
60646  488 
else Seq.single(execute ctxt (ss,fl,auto_tac,cong_tac,simp_net,i,thm))) 
60774  489 
THEN TRY(auto_tac ctxt i) 
0  490 
end; 
491 

60646  492 
fun SIMP_TAC ctxt = EXEC_TAC ctxt ([MK_EQ,SIMP_LHS,REFL,STOP],false); 
493 
fun SIMP_CASE_TAC ctxt = EXEC_TAC ctxt ([MK_EQ,SIMP_LHS,IF,REFL,STOP],false); 

0  494 

60646  495 
fun ASM_SIMP_TAC ctxt = EXEC_TAC ctxt ([ASMS(0),MK_EQ,SIMP_LHS,REFL,STOP],false); 
496 
fun ASM_SIMP_CASE_TAC ctxt = EXEC_TAC ctxt ([ASMS(0),MK_EQ,SIMP_LHS,IF,REFL,STOP],false); 

0  497 

60646  498 
fun SIMP_CASE2_TAC ctxt = EXEC_TAC ctxt ([MK_EQ,SIMP_LHS,IF,REFL,STOP],true); 
0  499 

60646  500 
fun REWRITE ctxt (ss,fl) (SS{auto_tac,cong_net,simp_net,...}) = 
60756  501 
let val cong_tac = net_tac ctxt cong_net 
0  502 
in fn thm => let val state = thm RSN (2,red1) 
60646  503 
in execute ctxt (ss,fl,auto_tac,cong_tac,simp_net,1,state) end 
0  504 
end; 
505 

60646  506 
fun SIMP_THM ctxt = REWRITE ctxt ([ASMS(0),SIMP_LHS,IF,REFL,STOP],false); 
0  507 

508 

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

510 
rules *) 

511 

35021
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33955
diff
changeset

512 
val subst_thms = map Drule.export_without_context subst_thms; 
0  513 

514 

515 
fun exp_app(0,t) = t 

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

517 

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

1459  519 
Abs("x"^string_of_int i,T1,exp_abs(T2,t,i+1)) 
0  520 
 exp_abs(T,t,i) = exp_app(i,t); 
521 

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

523 

524 

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

526 
let fun xn_list(x,n) = 

33063  527 
let val ixs = map_range (fn i => (x^(radixstring(26,"a",i)),0)) (n  1); 
33955  528 
in ListPair.map eta_Var (ixs, take (n+1) Ts) end 
0  529 
val lhs = list_comb(f,xn_list("X",k1)) 
530 
val rhs = list_comb(f,xn_list("X",i1) @ [Bound 0] @ yik) 

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

532 

60789  533 
fun find_subst ctxt T = 
0  534 
let fun find (thm::thms) = 
59582  535 
let val (Const(_,cT), va, vb) = dest_red(hd(Thm.prems_of thm)); 
536 
val [P] = subtract (op =) [va, vb] (Misc_Legacy.add_term_vars (Thm.concl_of thm, [])); 

1459  537 
val eqT::_ = binder_types cT 
60789  538 
in if Sign.typ_instance (Proof_Context.theory_of ctxt) (T,eqT) then SOME(thm,va,vb,P) 
1459  539 
else find thms 
540 
end 

15531  541 
 find [] = NONE 
0  542 
in find subst_thms end; 
543 

60789  544 
fun mk_cong ctxt (f,aTs,rT) (refl,eq) = 
16931  545 
let val k = length aTs; 
60790  546 
fun ri((subst,va as Var(a,Ta),vb as Var(b,Tb), Var (P, _)),i,si,T,yik) = 
547 
let val cx = Thm.cterm_of ctxt (eta_Var(("X"^si,0),T)) 

60789  548 
val cb = Thm.cterm_of ctxt vb 
60790  549 
val cy = Thm.cterm_of ctxt (eta_Var(("Y"^si,0),T)) 
550 
val cp = Thm.cterm_of ctxt (Pinst(f,rT,eq,k,i,T,yik,aTs)) 

551 
in infer_instantiate ctxt [(a,cx),(b,cy),(P,cp)] subst end; 

0  552 
fun mk(c,T::Ts,i,yik) = 
1459  553 
let val si = radixstring(26,"a",i) 
60789  554 
in case find_subst ctxt T of 
15531  555 
NONE => mk(c,Ts,i1,eta_Var(("X"^si,0),T)::yik) 
556 
 SOME s => let val c' = c RSN (2,ri(s,i,si,T,yik)) 

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

0  559 
 mk(c,[],_,_) = c; 
560 
in mk(refl,rev aTs,k1,[]) end; 

561 

60789  562 
fun mk_cong_type ctxt (f,T) = 
0  563 
let val (aTs,rT) = strip_type T; 
564 
fun find_refl(r::rs) = 

59582  565 
let val (Const(eq,eqT),_,_) = dest_red(Thm.concl_of r) 
60789  566 
in if Sign.typ_instance (Proof_Context.theory_of ctxt) (rT, hd(binder_types eqT)) 
15531  567 
then SOME(r,(eq,body_type eqT)) else find_refl rs 
1459  568 
end 
15531  569 
 find_refl([]) = NONE; 
0  570 
in case find_refl refl_thms of 
60789  571 
NONE => []  SOME(refl) => [mk_cong ctxt (f,aTs,rT) refl] 
0  572 
end; 
573 

60789  574 
fun mk_congs' ctxt f = 
575 
let val T = case Sign.const_type (Proof_Context.theory_of ctxt) f of 

15531  576 
NONE => error(f^" not declared")  SOME(T) => T; 
16876  577 
val T' = Logic.incr_tvar 9 T; 
60789  578 
in mk_cong_type ctxt (Const(f,T'),T') end; 
0  579 

60789  580 
val mk_congs = maps o mk_congs'; 
0  581 

60789  582 
fun mk_typed_congs ctxt = 
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22596
diff
changeset

583 
let 
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22596
diff
changeset

584 
fun readfT(f,s) = 
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22596
diff
changeset

585 
let 
60789  586 
val T = Logic.incr_tvar 9 (Syntax.read_typ ctxt s); 
587 
val t = case Sign.const_type (Proof_Context.theory_of ctxt) f of 

22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22596
diff
changeset

588 
SOME(_) => Const(f,T)  NONE => Free(f,T) 
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22596
diff
changeset

589 
in (t,T) end 
60789  590 
in maps (mk_cong_type ctxt o readfT) end; 
0  591 

22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22596
diff
changeset

592 
end; 
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22596
diff
changeset

593 
end; 