65 |
65 |
66 fun eq_brl ((b1 : bool, th1), (b2, th2)) = b1 = b2 andalso Thm.eq_thm_prop (th1, th2); |
66 fun eq_brl ((b1 : bool, th1), (b2, th2)) = b1 = b2 andalso Thm.eq_thm_prop (th1, th2); |
67 |
67 |
68 (*insert a thm in a discrimination net by its lhs*) |
68 (*insert a thm in a discrimination net by its lhs*) |
69 fun lhs_insert_thm th net = |
69 fun lhs_insert_thm th net = |
70 Net.insert_term eq_brl (lhs_of (concl_of th), (false,th)) net |
70 Net.insert_term eq_brl (lhs_of (Thm.concl_of th), (false,th)) net |
71 handle Net.INSERT => net; |
71 handle Net.INSERT => net; |
72 |
72 |
73 (*match subgoal i against possible theorems in the net. |
73 (*match subgoal i against possible theorems in the net. |
74 Similar to match_from_nat_tac, but the net does not contain numbers; |
74 Similar to match_from_nat_tac, but the net does not contain numbers; |
75 rewrite rules are not ordered.*) |
75 rewrite rules are not ordered.*) |
187 |
187 |
188 |
188 |
189 fun add_norms(congs,ccs,new_asms) thm = |
189 fun add_norms(congs,ccs,new_asms) thm = |
190 let val thm' = mk_trans2 thm; |
190 let val thm' = mk_trans2 thm; |
191 (* thm': [?z -> l; Prems; r -> ?t] ==> ?z -> ?t *) |
191 (* thm': [?z -> l; Prems; r -> ?t] ==> ?z -> ?t *) |
192 val nops = nprems_of thm' |
192 val nops = Thm.nprems_of thm' |
193 val lhs = rhs_of_eq 1 thm' |
193 val lhs = rhs_of_eq 1 thm' |
194 val rhs = lhs_of_eq nops thm' |
194 val rhs = lhs_of_eq nops thm' |
195 val asms = tl(rev(tl(prems_of thm'))) |
195 val asms = tl(rev(tl(Thm.prems_of thm'))) |
196 val hvars = fold_rev (add_hidden_vars ccs) (lhs::rhs::asms) [] |
196 val hvars = fold_rev (add_hidden_vars ccs) (lhs::rhs::asms) [] |
197 val hvars = add_new_asm_vars new_asms (rhs,hvars) |
197 val hvars = add_new_asm_vars new_asms (rhs,hvars) |
198 fun it_asms asm hvars = |
198 fun it_asms asm hvars = |
199 if atomic asm then add_new_asm_vars new_asms (asm,hvars) |
199 if atomic asm then add_new_asm_vars new_asms (asm,hvars) |
200 else Misc_Legacy.add_term_frees(asm,hvars) |
200 else Misc_Legacy.add_term_frees(asm,hvars) |
346 (COND (if_rewritable ifc i) (DETERM(rtac ifth i)) |
346 (COND (if_rewritable ifc i) (DETERM(rtac ifth i)) |
347 (seq_try(ifths,ifcs))) thm |
347 (seq_try(ifths,ifcs))) thm |
348 | seq_try([],_) thm = no_tac thm |
348 | seq_try([],_) thm = no_tac thm |
349 and try_rew thm = (seq_try(case_rews,case_consts) ORELSE one_subt) thm |
349 and try_rew thm = (seq_try(case_rews,case_consts) ORELSE one_subt) thm |
350 and one_subt thm = |
350 and one_subt thm = |
351 let val test = has_fewer_prems (nprems_of thm + 1) |
351 let val test = has_fewer_prems (Thm.nprems_of thm + 1) |
352 fun loop thm = |
352 fun loop thm = |
353 COND test no_tac |
353 COND test no_tac |
354 ((try_rew THEN DEPTH_FIRST test (refl_tac i)) |
354 ((try_rew THEN DEPTH_FIRST test (refl_tac i)) |
355 ORELSE (refl_tac i THEN loop)) thm |
355 ORELSE (refl_tac i THEN loop)) thm |
356 in (cong_tac THEN loop) thm end |
356 in (cong_tac THEN loop) thm end |
422 fun simp_lhs(thm,ss,anet,ats,cs) = |
422 fun simp_lhs(thm,ss,anet,ats,cs) = |
423 if var_lhs(thm,i) then (ss,thm,anet,ats,cs) else |
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) |
424 if lhs_is_NORM(thm,i) then (ss, res1(thm,trans_norms,i), anet,ats,cs) |
425 else case Seq.pull(cong_tac i thm) of |
425 else case Seq.pull(cong_tac i thm) of |
426 SOME(thm',_) => |
426 SOME(thm',_) => |
427 let val ps = prems_of thm |
427 let val ps = Thm.prems_of thm |
428 and ps' = prems_of thm'; |
428 and ps' = Thm.prems_of thm'; |
429 val n = length(ps')-length(ps); |
429 val n = length(ps')-length(ps); |
430 val a = length(Logic.strip_assums_hyp(nth ps (i - 1))) |
430 val a = length(Logic.strip_assums_hyp(nth ps (i - 1))) |
431 val l = map (length o Logic.strip_assums_hyp) (take n (drop (i-1) ps')); |
431 val l = map (length o Logic.strip_assums_hyp) (take n (drop (i-1) ps')); |
432 in (simp_refl(rev(l),a,REW::ss),thm',anet,ats,cs) end |
432 in (simp_refl(rev(l),a,REW::ss),thm',anet,ats,cs) end |
433 | NONE => (REW::ss,thm,anet,ats,cs); |
433 | NONE => (REW::ss,thm,anet,ats,cs); |
434 |
434 |
435 (*NB: the "Adding rewrites:" trace will look strange because assumptions |
435 (*NB: the "Adding rewrites:" trace will look strange because assumptions |
436 are represented by rules, generalized over their parameters*) |
436 are represented by rules, generalized over their parameters*) |
437 fun add_asms(ss,thm,a,anet,ats,cs) = |
437 fun add_asms(ss,thm,a,anet,ats,cs) = |
438 let val As = strip_varify(nth_subgoal i thm, a, []); |
438 let val As = strip_varify(nth_subgoal i thm, a, []); |
439 val thms = map (Thm.trivial o cterm_of(Thm.theory_of_thm thm)) As; |
439 val thms = map (Thm.trivial o Thm.cterm_of(Thm.theory_of_thm thm)) As; |
440 val new_rws = maps mk_rew_rules thms; |
440 val new_rws = maps mk_rew_rules thms; |
441 val rwrls = map mk_trans (maps mk_rew_rules thms); |
441 val rwrls = map mk_trans (maps mk_rew_rules thms); |
442 val anet' = fold_rev lhs_insert_thm rwrls anet; |
442 val anet' = fold_rev lhs_insert_thm rwrls anet; |
443 in if !tracing andalso not(null new_rws) |
443 in if !tracing andalso not(null new_rws) |
444 then writeln (cat_lines |
444 then writeln (cat_lines |
447 (ss,thm,anet',anet::ats,cs) |
447 (ss,thm,anet',anet::ats,cs) |
448 end; |
448 end; |
449 |
449 |
450 fun rew(seq,thm,ss,anet,ats,cs, more) = case Seq.pull seq of |
450 fun rew(seq,thm,ss,anet,ats,cs, more) = case Seq.pull seq of |
451 SOME(thm',seq') => |
451 SOME(thm',seq') => |
452 let val n = (nprems_of thm') - (nprems_of thm) |
452 let val n = (Thm.nprems_of thm') - (Thm.nprems_of thm) |
453 in pr_rew(i,n,thm,thm',more); |
453 in pr_rew(i,n,thm,thm',more); |
454 if n=0 then (SIMP_LHS::ss, thm', anet, ats, cs) |
454 if n=0 then (SIMP_LHS::ss, thm', anet, ats, cs) |
455 else ((replicate n PROVE) @ (POP_CS::SIMP_LHS::ss), |
455 else ((replicate n PROVE) @ (POP_CS::SIMP_LHS::ss), |
456 thm', anet, ats, (ss,thm,anet,ats,seq',more)::cs) |
456 thm', anet, ats, (ss,thm,anet,ats,seq',more)::cs) |
457 end |
457 end |
497 |
497 |
498 fun EXEC_TAC(ss,fl) (SS{auto_tac,cong_net,simp_net,...}) = |
498 fun EXEC_TAC(ss,fl) (SS{auto_tac,cong_net,simp_net,...}) = |
499 let val cong_tac = net_tac cong_net |
499 let val cong_tac = net_tac cong_net |
500 in fn i => |
500 in fn i => |
501 (fn thm => |
501 (fn thm => |
502 if i <= 0 orelse nprems_of thm < i then Seq.empty |
502 if i <= 0 orelse Thm.nprems_of thm < i then Seq.empty |
503 else Seq.single(execute(ss,fl,auto_tac,cong_tac,simp_net,i,thm))) |
503 else Seq.single(execute(ss,fl,auto_tac,cong_tac,simp_net,i,thm))) |
504 THEN TRY(auto_tac i) |
504 THEN TRY(auto_tac i) |
505 end; |
505 end; |
506 |
506 |
507 val SIMP_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,REFL,STOP],false); |
507 val SIMP_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,REFL,STOP],false); |
545 val rhs = list_comb(f,xn_list("X",i-1) @ [Bound 0] @ yik) |
545 val rhs = list_comb(f,xn_list("X",i-1) @ [Bound 0] @ yik) |
546 in Abs("", T, Const(eq,[fT,fT]--->eqT) $ lhs $ rhs) end; |
546 in Abs("", T, Const(eq,[fT,fT]--->eqT) $ lhs $ rhs) end; |
547 |
547 |
548 fun find_subst sg T = |
548 fun find_subst sg T = |
549 let fun find (thm::thms) = |
549 let fun find (thm::thms) = |
550 let val (Const(_,cT), va, vb) = dest_red(hd(prems_of thm)); |
550 let val (Const(_,cT), va, vb) = dest_red(hd(Thm.prems_of thm)); |
551 val [P] = subtract (op =) [va, vb] (Misc_Legacy.add_term_vars (concl_of thm, [])); |
551 val [P] = subtract (op =) [va, vb] (Misc_Legacy.add_term_vars (Thm.concl_of thm, [])); |
552 val eqT::_ = binder_types cT |
552 val eqT::_ = binder_types cT |
553 in if Sign.typ_instance sg (T,eqT) then SOME(thm,va,vb,P) |
553 in if Sign.typ_instance sg (T,eqT) then SOME(thm,va,vb,P) |
554 else find thms |
554 else find thms |
555 end |
555 end |
556 | find [] = NONE |
556 | find [] = NONE |
557 in find subst_thms end; |
557 in find subst_thms end; |
558 |
558 |
559 fun mk_cong sg (f,aTs,rT) (refl,eq) = |
559 fun mk_cong sg (f,aTs,rT) (refl,eq) = |
560 let val k = length aTs; |
560 let val k = length aTs; |
561 fun ri((subst,va as Var(_,Ta),vb as Var(_,Tb),P),i,si,T,yik) = |
561 fun ri((subst,va as Var(_,Ta),vb as Var(_,Tb),P),i,si,T,yik) = |
562 let val ca = cterm_of sg va |
562 let val ca = Thm.cterm_of sg va |
563 and cx = cterm_of sg (eta_Var(("X"^si,0),T)) |
563 and cx = Thm.cterm_of sg (eta_Var(("X"^si,0),T)) |
564 val cb = cterm_of sg vb |
564 val cb = Thm.cterm_of sg vb |
565 and cy = cterm_of sg (eta_Var(("Y"^si,0),T)) |
565 and cy = Thm.cterm_of sg (eta_Var(("Y"^si,0),T)) |
566 val cP = cterm_of sg P |
566 val cP = Thm.cterm_of sg P |
567 and cp = cterm_of sg (Pinst(f,rT,eq,k,i,T,yik,aTs)) |
567 and cp = Thm.cterm_of sg (Pinst(f,rT,eq,k,i,T,yik,aTs)) |
568 in cterm_instantiate [(ca,cx),(cb,cy),(cP,cp)] subst end; |
568 in cterm_instantiate [(ca,cx),(cb,cy),(cP,cp)] subst end; |
569 fun mk(c,T::Ts,i,yik) = |
569 fun mk(c,T::Ts,i,yik) = |
570 let val si = radixstring(26,"a",i) |
570 let val si = radixstring(26,"a",i) |
571 in case find_subst sg T of |
571 in case find_subst sg T of |
572 NONE => mk(c,Ts,i-1,eta_Var(("X"^si,0),T)::yik) |
572 NONE => mk(c,Ts,i-1,eta_Var(("X"^si,0),T)::yik) |
577 in mk(refl,rev aTs,k-1,[]) end; |
577 in mk(refl,rev aTs,k-1,[]) end; |
578 |
578 |
579 fun mk_cong_type sg (f,T) = |
579 fun mk_cong_type sg (f,T) = |
580 let val (aTs,rT) = strip_type T; |
580 let val (aTs,rT) = strip_type T; |
581 fun find_refl(r::rs) = |
581 fun find_refl(r::rs) = |
582 let val (Const(eq,eqT),_,_) = dest_red(concl_of r) |
582 let val (Const(eq,eqT),_,_) = dest_red(Thm.concl_of r) |
583 in if Sign.typ_instance sg (rT, hd(binder_types eqT)) |
583 in if Sign.typ_instance sg (rT, hd(binder_types eqT)) |
584 then SOME(r,(eq,body_type eqT)) else find_refl rs |
584 then SOME(r,(eq,body_type eqT)) else find_refl rs |
585 end |
585 end |
586 | find_refl([]) = NONE; |
586 | find_refl([]) = NONE; |
587 in case find_refl refl_thms of |
587 in case find_refl refl_thms of |