equal
deleted
inserted
replaced
425 (* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *) |
425 (* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *) |
426 fun is_cong thm = |
426 fun is_cong thm = |
427 let val {prop, ...} = rep_thm thm |
427 let val {prop, ...} = rep_thm thm |
428 in case prop |
428 in case prop |
429 of (Const("==>",_)$(Const("Trueprop",_)$ _) $ |
429 of (Const("==>",_)$(Const("Trueprop",_)$ _) $ |
430 (Const("==",_) $ (Const ("cut",_) $ f $ R $ a $ x) $ _)) => false |
430 (Const("==",_) $ (Const ("WF.cut",_) $ f $ R $ a $ x) $ _)) => false |
431 | _ => true |
431 | _ => true |
432 end; |
432 end; |
433 |
433 |
434 |
434 |
435 |
435 |
629 val eq = Logic.strip_imp_concl tm |
629 val eq = Logic.strip_imp_concl tm |
630 in (ants,get_lhs eq) |
630 in (ants,get_lhs eq) |
631 end; |
631 end; |
632 |
632 |
633 fun restricted t = is_some (S.find_term |
633 fun restricted t = is_some (S.find_term |
634 (fn (Const("cut",_)) =>true | _ => false) |
634 (fn (Const("WF.cut",_)) =>true | _ => false) |
635 t) |
635 t) |
636 |
636 |
637 fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th = |
637 fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th = |
638 let val globals = func::G |
638 let val globals = func::G |
639 val pbeta_reduce = simpl_conv empty_ss [split RS eq_reflection]; |
639 val pbeta_reduce = simpl_conv empty_ss [split RS eq_reflection]; |