541 let |
541 let |
542 fun mk v v' q n P = |
542 fun mk v v' q n P = |
543 if v=v' andalso not (v mem (map fst (Term.add_frees n []))) |
543 if v=v' andalso not (v mem (map fst (Term.add_frees n []))) |
544 then Syntax.const q $ Syntax.mark_bound v' $ n $ P else raise Match; |
544 then Syntax.const q $ Syntax.mark_bound v' $ n $ P else raise Match; |
545 fun all_tr' [Const ("_bound",_) $ Free (v,_), |
545 fun all_tr' [Const ("_bound",_) $ Free (v,_), |
546 Const("op -->",_) $ (Const ("Orderings.less",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = |
546 Const("op -->",_) $ (Const ("less",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = |
547 mk v v' "_lessAll" n P |
547 mk v v' "_lessAll" n P |
548 |
548 |
549 | all_tr' [Const ("_bound",_) $ Free (v,_), |
549 | all_tr' [Const ("_bound",_) $ Free (v,_), |
550 Const("op -->",_) $ (Const ("Orderings.less_eq",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = |
550 Const("op -->",_) $ (Const ("less_eq",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = |
551 mk v v' "_leAll" n P |
551 mk v v' "_leAll" n P |
552 |
552 |
553 | all_tr' [Const ("_bound",_) $ Free (v,_), |
553 | all_tr' [Const ("_bound",_) $ Free (v,_), |
554 Const("op -->",_) $ (Const ("Orderings.less",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] = |
554 Const("op -->",_) $ (Const ("less",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] = |
555 mk v v' "_gtAll" n P |
555 mk v v' "_gtAll" n P |
556 |
556 |
557 | all_tr' [Const ("_bound",_) $ Free (v,_), |
557 | all_tr' [Const ("_bound",_) $ Free (v,_), |
558 Const("op -->",_) $ (Const ("Orderings.less_eq",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] = |
558 Const("op -->",_) $ (Const ("less_eq",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] = |
559 mk v v' "_geAll" n P; |
559 mk v v' "_geAll" n P; |
560 |
560 |
561 fun ex_tr' [Const ("_bound",_) $ Free (v,_), |
561 fun ex_tr' [Const ("_bound",_) $ Free (v,_), |
562 Const("op &",_) $ (Const ("Orderings.less",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = |
562 Const("op &",_) $ (Const ("less",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = |
563 mk v v' "_lessEx" n P |
563 mk v v' "_lessEx" n P |
564 |
564 |
565 | ex_tr' [Const ("_bound",_) $ Free (v,_), |
565 | ex_tr' [Const ("_bound",_) $ Free (v,_), |
566 Const("op &",_) $ (Const ("Orderings.less_eq",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = |
566 Const("op &",_) $ (Const ("less_eq",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = |
567 mk v v' "_leEx" n P |
567 mk v v' "_leEx" n P |
568 |
568 |
569 | ex_tr' [Const ("_bound",_) $ Free (v,_), |
569 | ex_tr' [Const ("_bound",_) $ Free (v,_), |
570 Const("op &",_) $ (Const ("Orderings.less",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] = |
570 Const("op &",_) $ (Const ("less",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] = |
571 mk v v' "_gtEx" n P |
571 mk v v' "_gtEx" n P |
572 |
572 |
573 | ex_tr' [Const ("_bound",_) $ Free (v,_), |
573 | ex_tr' [Const ("_bound",_) $ Free (v,_), |
574 Const("op &",_) $ (Const ("Orderings.less_eq",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] = |
574 Const("op &",_) $ (Const ("less_eq",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] = |
575 mk v v' "_geEx" n P |
575 mk v v' "_geEx" n P |
576 in |
576 in |
577 [("ALL ", all_tr'), ("EX ", ex_tr')] |
577 [("ALL ", all_tr'), ("EX ", ex_tr')] |
578 end |
578 end |
579 *} |
579 *} |