782 ([Logic.mk_equals (f, g), Logic.mk_equals (x, y)], |
782 ([Logic.mk_equals (f, g), Logic.mk_equals (x, y)], |
783 Logic.mk_equals (f $ x, g $ y)))]; |
783 Logic.mk_equals (f $ x, g $ y)))]; |
784 |
784 |
785 val [reflexive_axm, symmetric_axm, transitive_axm, equal_intr_axm, |
785 val [reflexive_axm, symmetric_axm, transitive_axm, equal_intr_axm, |
786 equal_elim_axm, abstract_rule_axm, combination_axm] = |
786 equal_elim_axm, abstract_rule_axm, combination_axm] = |
787 map (fn (s, t) => PAxm ("ProtoPure." ^ s, varify t, NONE)) equality_axms; |
787 map (fn (s, t) => PAxm ("Pure." ^ s, varify t, NONE)) equality_axms; |
788 |
788 |
789 end; |
789 end; |
790 |
790 |
791 val reflexive = reflexive_axm % NONE; |
791 val reflexive = reflexive_axm % NONE; |
792 |
792 |
793 fun symmetric (prf as PAxm ("ProtoPure.reflexive", _, _) % _) = prf |
793 fun symmetric (prf as PAxm ("Pure.reflexive", _, _) % _) = prf |
794 | symmetric prf = symmetric_axm % NONE % NONE %% prf; |
794 | symmetric prf = symmetric_axm % NONE % NONE %% prf; |
795 |
795 |
796 fun transitive _ _ (PAxm ("ProtoPure.reflexive", _, _) % _) prf2 = prf2 |
796 fun transitive _ _ (PAxm ("Pure.reflexive", _, _) % _) prf2 = prf2 |
797 | transitive _ _ prf1 (PAxm ("ProtoPure.reflexive", _, _) % _) = prf1 |
797 | transitive _ _ prf1 (PAxm ("Pure.reflexive", _, _) % _) = prf1 |
798 | transitive u (Type ("prop", [])) prf1 prf2 = |
798 | transitive u (Type ("prop", [])) prf1 prf2 = |
799 transitive_axm % NONE % SOME (remove_types u) % NONE %% prf1 %% prf2 |
799 transitive_axm % NONE % SOME (remove_types u) % NONE %% prf1 %% prf2 |
800 | transitive u T prf1 prf2 = |
800 | transitive u T prf1 prf2 = |
801 transitive_axm % NONE % NONE % NONE %% prf1 %% prf2; |
801 transitive_axm % NONE % NONE % NONE %% prf1 %% prf2; |
802 |
802 |
803 fun abstract_rule x a prf = |
803 fun abstract_rule x a prf = |
804 abstract_rule_axm % NONE % NONE %% forall_intr_proof x a prf; |
804 abstract_rule_axm % NONE % NONE %% forall_intr_proof x a prf; |
805 |
805 |
806 fun check_comb (PAxm ("ProtoPure.combination", _, _) % f % g % _ % _ %% prf %% _) = |
806 fun check_comb (PAxm ("Pure.combination", _, _) % f % g % _ % _ %% prf %% _) = |
807 is_some f orelse check_comb prf |
807 is_some f orelse check_comb prf |
808 | check_comb (PAxm ("ProtoPure.transitive", _, _) % _ % _ % _ %% prf1 %% prf2) = |
808 | check_comb (PAxm ("Pure.transitive", _, _) % _ % _ % _ %% prf1 %% prf2) = |
809 check_comb prf1 andalso check_comb prf2 |
809 check_comb prf1 andalso check_comb prf2 |
810 | check_comb (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% prf) = check_comb prf |
810 | check_comb (PAxm ("Pure.symmetric", _, _) % _ % _ %% prf) = check_comb prf |
811 | check_comb _ = false; |
811 | check_comb _ = false; |
812 |
812 |
813 fun combination f g t u (Type (_, [T, U])) prf1 prf2 = |
813 fun combination f g t u (Type (_, [T, U])) prf1 prf2 = |
814 let |
814 let |
815 val f = Envir.beta_norm f; |
815 val f = Envir.beta_norm f; |
816 val g = Envir.beta_norm g; |
816 val g = Envir.beta_norm g; |
817 val prf = if check_comb prf1 then |
817 val prf = if check_comb prf1 then |
818 combination_axm % NONE % NONE |
818 combination_axm % NONE % NONE |
819 else (case prf1 of |
819 else (case prf1 of |
820 PAxm ("ProtoPure.reflexive", _, _) % _ => |
820 PAxm ("Pure.reflexive", _, _) % _ => |
821 combination_axm %> remove_types f % NONE |
821 combination_axm %> remove_types f % NONE |
822 | _ => combination_axm %> remove_types f %> remove_types g) |
822 | _ => combination_axm %> remove_types f %> remove_types g) |
823 in |
823 in |
824 (case T of |
824 (case T of |
825 Type ("fun", _) => prf % |
825 Type ("fun", _) => prf % |