740 Thm.transfer' ctxt #> |
740 Thm.transfer' ctxt #> |
741 (case optcT of NONE => I | SOME cT => inst [cT] [] #> norm) |
741 (case optcT of NONE => I | SOME cT => inst [cT] [] #> norm) |
742 in (map tr ths1, map tr ths2, map tr ths3, map tr ths4, tr th5, tr th) end |
742 in (map tr ths1, map tr ths2, map tr ths3, map tr ths4, tr th5, tr th) end |
743 | NONE => error "get_ring_simps: lookup failed"); |
743 | NONE => error "get_ring_simps: lookup failed"); |
744 |
744 |
745 fun ring_struct (Const (@{const_name Ring.ring.add}, _) $ R $ _ $ _) = SOME R |
745 fun ring_struct (Const (\<^const_name>\<open>Ring.ring.add\<close>, _) $ R $ _ $ _) = SOME R |
746 | ring_struct (Const (@{const_name Ring.a_minus}, _) $ R $ _ $ _) = SOME R |
746 | ring_struct (Const (\<^const_name>\<open>Ring.a_minus\<close>, _) $ R $ _ $ _) = SOME R |
747 | ring_struct (Const (@{const_name Group.monoid.mult}, _) $ R $ _ $ _) = SOME R |
747 | ring_struct (Const (\<^const_name>\<open>Group.monoid.mult\<close>, _) $ R $ _ $ _) = SOME R |
748 | ring_struct (Const (@{const_name Ring.a_inv}, _) $ R $ _) = SOME R |
748 | ring_struct (Const (\<^const_name>\<open>Ring.a_inv\<close>, _) $ R $ _) = SOME R |
749 | ring_struct (Const (@{const_name Group.pow}, _) $ R $ _ $ _) = SOME R |
749 | ring_struct (Const (\<^const_name>\<open>Group.pow\<close>, _) $ R $ _ $ _) = SOME R |
750 | ring_struct (Const (@{const_name Ring.ring.zero}, _) $ R) = SOME R |
750 | ring_struct (Const (\<^const_name>\<open>Ring.ring.zero\<close>, _) $ R) = SOME R |
751 | ring_struct (Const (@{const_name Group.monoid.one}, _) $ R) = SOME R |
751 | ring_struct (Const (\<^const_name>\<open>Group.monoid.one\<close>, _) $ R) = SOME R |
752 | ring_struct (Const (@{const_name Algebra_Aux.of_integer}, _) $ R $ _) = SOME R |
752 | ring_struct (Const (\<^const_name>\<open>Algebra_Aux.of_integer\<close>, _) $ R $ _) = SOME R |
753 | ring_struct _ = NONE; |
753 | ring_struct _ = NONE; |
754 |
754 |
755 fun reif_polex vs (Const (@{const_name Ring.ring.add}, _) $ _ $ a $ b) = |
755 fun reif_polex vs (Const (\<^const_name>\<open>Ring.ring.add\<close>, _) $ _ $ a $ b) = |
756 @{const Add} $ reif_polex vs a $ reif_polex vs b |
756 \<^const>\<open>Add\<close> $ reif_polex vs a $ reif_polex vs b |
757 | reif_polex vs (Const (@{const_name Ring.a_minus}, _) $ _ $ a $ b) = |
757 | reif_polex vs (Const (\<^const_name>\<open>Ring.a_minus\<close>, _) $ _ $ a $ b) = |
758 @{const Sub} $ reif_polex vs a $ reif_polex vs b |
758 \<^const>\<open>Sub\<close> $ reif_polex vs a $ reif_polex vs b |
759 | reif_polex vs (Const (@{const_name Group.monoid.mult}, _) $ _ $ a $ b) = |
759 | reif_polex vs (Const (\<^const_name>\<open>Group.monoid.mult\<close>, _) $ _ $ a $ b) = |
760 @{const Mul} $ reif_polex vs a $ reif_polex vs b |
760 \<^const>\<open>Mul\<close> $ reif_polex vs a $ reif_polex vs b |
761 | reif_polex vs (Const (@{const_name Ring.a_inv}, _) $ _ $ a) = |
761 | reif_polex vs (Const (\<^const_name>\<open>Ring.a_inv\<close>, _) $ _ $ a) = |
762 @{const Neg} $ reif_polex vs a |
762 \<^const>\<open>Neg\<close> $ reif_polex vs a |
763 | reif_polex vs (Const (@{const_name Group.pow}, _) $ _ $ a $ n) = |
763 | reif_polex vs (Const (\<^const_name>\<open>Group.pow\<close>, _) $ _ $ a $ n) = |
764 @{const Pow} $ reif_polex vs a $ n |
764 \<^const>\<open>Pow\<close> $ reif_polex vs a $ n |
765 | reif_polex vs (Free x) = |
765 | reif_polex vs (Free x) = |
766 @{const Var} $ HOLogic.mk_number HOLogic.natT (find_index (equal x) vs) |
766 \<^const>\<open>Var\<close> $ HOLogic.mk_number HOLogic.natT (find_index (equal x) vs) |
767 | reif_polex vs (Const (@{const_name Ring.ring.zero}, _) $ _) = |
767 | reif_polex vs (Const (\<^const_name>\<open>Ring.ring.zero\<close>, _) $ _) = |
768 @{term "Const 0"} |
768 \<^term>\<open>Const 0\<close> |
769 | reif_polex vs (Const (@{const_name Group.monoid.one}, _) $ _) = |
769 | reif_polex vs (Const (\<^const_name>\<open>Group.monoid.one\<close>, _) $ _) = |
770 @{term "Const 1"} |
770 \<^term>\<open>Const 1\<close> |
771 | reif_polex vs (Const (@{const_name Algebra_Aux.of_integer}, _) $ _ $ n) = |
771 | reif_polex vs (Const (\<^const_name>\<open>Algebra_Aux.of_integer\<close>, _) $ _ $ n) = |
772 @{const Const} $ n |
772 \<^const>\<open>Const\<close> $ n |
773 | reif_polex _ _ = error "reif_polex: bad expression"; |
773 | reif_polex _ _ = error "reif_polex: bad expression"; |
774 |
774 |
775 fun reif_polex' vs (Const (@{const_name Groups.plus}, _) $ a $ b) = |
775 fun reif_polex' vs (Const (\<^const_name>\<open>Groups.plus\<close>, _) $ a $ b) = |
776 @{const Add} $ reif_polex' vs a $ reif_polex' vs b |
776 \<^const>\<open>Add\<close> $ reif_polex' vs a $ reif_polex' vs b |
777 | reif_polex' vs (Const (@{const_name Groups.minus}, _) $ a $ b) = |
777 | reif_polex' vs (Const (\<^const_name>\<open>Groups.minus\<close>, _) $ a $ b) = |
778 @{const Sub} $ reif_polex' vs a $ reif_polex' vs b |
778 \<^const>\<open>Sub\<close> $ reif_polex' vs a $ reif_polex' vs b |
779 | reif_polex' vs (Const (@{const_name Groups.times}, _) $ a $ b) = |
779 | reif_polex' vs (Const (\<^const_name>\<open>Groups.times\<close>, _) $ a $ b) = |
780 @{const Mul} $ reif_polex' vs a $ reif_polex' vs b |
780 \<^const>\<open>Mul\<close> $ reif_polex' vs a $ reif_polex' vs b |
781 | reif_polex' vs (Const (@{const_name Groups.uminus}, _) $ a) = |
781 | reif_polex' vs (Const (\<^const_name>\<open>Groups.uminus\<close>, _) $ a) = |
782 @{const Neg} $ reif_polex' vs a |
782 \<^const>\<open>Neg\<close> $ reif_polex' vs a |
783 | reif_polex' vs (Const (@{const_name Power.power}, _) $ a $ n) = |
783 | reif_polex' vs (Const (\<^const_name>\<open>Power.power\<close>, _) $ a $ n) = |
784 @{const Pow} $ reif_polex' vs a $ n |
784 \<^const>\<open>Pow\<close> $ reif_polex' vs a $ n |
785 | reif_polex' vs (Free x) = |
785 | reif_polex' vs (Free x) = |
786 @{const Var} $ HOLogic.mk_number HOLogic.natT (find_index (equal x) vs) |
786 \<^const>\<open>Var\<close> $ HOLogic.mk_number HOLogic.natT (find_index (equal x) vs) |
787 | reif_polex' vs (Const (@{const_name numeral}, _) $ b) = |
787 | reif_polex' vs (Const (\<^const_name>\<open>numeral\<close>, _) $ b) = |
788 @{const Const} $ (@{const numeral (int)} $ b) |
788 \<^const>\<open>Const\<close> $ (@{const numeral (int)} $ b) |
789 | reif_polex' vs (Const (@{const_name zero_class.zero}, _)) = @{term "Const 0"} |
789 | reif_polex' vs (Const (\<^const_name>\<open>zero_class.zero\<close>, _)) = \<^term>\<open>Const 0\<close> |
790 | reif_polex' vs (Const (@{const_name one_class.one}, _)) = @{term "Const 1"} |
790 | reif_polex' vs (Const (\<^const_name>\<open>one_class.one\<close>, _)) = \<^term>\<open>Const 1\<close> |
791 | reif_polex' vs t = error "reif_polex: bad expression"; |
791 | reif_polex' vs t = error "reif_polex: bad expression"; |
792 |
792 |
793 fun head_conv (_, _, _, _, head_simp, _) ys = |
793 fun head_conv (_, _, _, _, head_simp, _) ys = |
794 (case strip_app ys of |
794 (case strip_app ys of |
795 (@{const_name Cons}, [y, xs]) => inst [] [y, xs] head_simp); |
795 (\<^const_name>\<open>Cons\<close>, [y, xs]) => inst [] [y, xs] head_simp); |
796 |
796 |
797 fun Ipol_conv (rls as |
797 fun Ipol_conv (rls as |
798 ([Ipol_simps_1, Ipol_simps_2, Ipol_simps_3, |
798 ([Ipol_simps_1, Ipol_simps_2, Ipol_simps_3, |
799 Ipol_simps_4, Ipol_simps_5, Ipol_simps_6, |
799 Ipol_simps_4, Ipol_simps_5, Ipol_simps_6, |
800 Ipol_simps_7], _, _, _, _, _)) = |
800 Ipol_simps_7], _, _, _, _, _)) = |
801 let |
801 let |
802 val a = type_of_eqn Ipol_simps_1; |
802 val a = type_of_eqn Ipol_simps_1; |
803 val drop_conv_a = drop_conv a; |
803 val drop_conv_a = drop_conv a; |
804 |
804 |
805 fun conv l p = (case strip_app p of |
805 fun conv l p = (case strip_app p of |
806 (@{const_name Pc}, [c]) => (case strip_numeral c of |
806 (\<^const_name>\<open>Pc\<close>, [c]) => (case strip_numeral c of |
807 (@{const_name zero_class.zero}, _) => inst [] [l] Ipol_simps_4 |
807 (\<^const_name>\<open>zero_class.zero\<close>, _) => inst [] [l] Ipol_simps_4 |
808 | (@{const_name one_class.one}, _) => inst [] [l] Ipol_simps_5 |
808 | (\<^const_name>\<open>one_class.one\<close>, _) => inst [] [l] Ipol_simps_5 |
809 | (@{const_name numeral}, [m]) => inst [] [l, m] Ipol_simps_6 |
809 | (\<^const_name>\<open>numeral\<close>, [m]) => inst [] [l, m] Ipol_simps_6 |
810 | (@{const_name uminus}, [m]) => inst [] [l, m] Ipol_simps_7 |
810 | (\<^const_name>\<open>uminus\<close>, [m]) => inst [] [l, m] Ipol_simps_7 |
811 | _ => inst [] [l, c] Ipol_simps_1) |
811 | _ => inst [] [l, c] Ipol_simps_1) |
812 | (@{const_name Pinj}, [i, P]) => |
812 | (\<^const_name>\<open>Pinj\<close>, [i, P]) => |
813 transitive' |
813 transitive' |
814 (inst [] [l, i, P] Ipol_simps_2) |
814 (inst [] [l, i, P] Ipol_simps_2) |
815 (cong2' conv (args2 drop_conv_a) Thm.reflexive) |
815 (cong2' conv (args2 drop_conv_a) Thm.reflexive) |
816 | (@{const_name PX}, [P, x, Q]) => |
816 | (\<^const_name>\<open>PX\<close>, [P, x, Q]) => |
817 transitive' |
817 transitive' |
818 (inst [] [l, P, x, Q] Ipol_simps_3) |
818 (inst [] [l, P, x, Q] Ipol_simps_3) |
819 (cong2 |
819 (cong2 |
820 (cong2 |
820 (cong2 |
821 (args2 conv) (cong2 (args1 (head_conv rls)) Thm.reflexive)) |
821 (args2 conv) (cong2 (args1 (head_conv rls)) Thm.reflexive)) |
831 let |
831 let |
832 val a = type_of_eqn Ipolex_Var; |
832 val a = type_of_eqn Ipolex_Var; |
833 val drop_conv_a = drop_conv a; |
833 val drop_conv_a = drop_conv a; |
834 |
834 |
835 fun conv l r = (case strip_app r of |
835 fun conv l r = (case strip_app r of |
836 (@{const_name Var}, [n]) => |
836 (\<^const_name>\<open>Var\<close>, [n]) => |
837 transitive' |
837 transitive' |
838 (inst [] [l, n] Ipolex_Var) |
838 (inst [] [l, n] Ipolex_Var) |
839 (cong1' (head_conv rls) (args2 drop_conv_a)) |
839 (cong1' (head_conv rls) (args2 drop_conv_a)) |
840 | (@{const_name Const}, [i]) => (case strip_app i of |
840 | (\<^const_name>\<open>Const\<close>, [i]) => (case strip_app i of |
841 (@{const_name zero_class.zero}, _) => inst [] [l] Ipolex_Const_0 |
841 (\<^const_name>\<open>zero_class.zero\<close>, _) => inst [] [l] Ipolex_Const_0 |
842 | (@{const_name one_class.one}, _) => inst [] [l] Ipolex_Const_1 |
842 | (\<^const_name>\<open>one_class.one\<close>, _) => inst [] [l] Ipolex_Const_1 |
843 | (@{const_name numeral}, [m]) => inst [] [l, m] Ipolex_Const_numeral |
843 | (\<^const_name>\<open>numeral\<close>, [m]) => inst [] [l, m] Ipolex_Const_numeral |
844 | _ => inst [] [l, i] Ipolex_Const) |
844 | _ => inst [] [l, i] Ipolex_Const) |
845 | (@{const_name Add}, [P, Q]) => |
845 | (\<^const_name>\<open>Add\<close>, [P, Q]) => |
846 transitive' |
846 transitive' |
847 (inst [] [l, P, Q] Ipolex_Add) |
847 (inst [] [l, P, Q] Ipolex_Add) |
848 (cong2 (args2 conv) (args2 conv)) |
848 (cong2 (args2 conv) (args2 conv)) |
849 | (@{const_name Sub}, [P, Q]) => |
849 | (\<^const_name>\<open>Sub\<close>, [P, Q]) => |
850 transitive' |
850 transitive' |
851 (inst [] [l, P, Q] Ipolex_Sub) |
851 (inst [] [l, P, Q] Ipolex_Sub) |
852 (cong2 (args2 conv) (args2 conv)) |
852 (cong2 (args2 conv) (args2 conv)) |
853 | (@{const_name Mul}, [P, Q]) => |
853 | (\<^const_name>\<open>Mul\<close>, [P, Q]) => |
854 transitive' |
854 transitive' |
855 (inst [] [l, P, Q] Ipolex_Mul) |
855 (inst [] [l, P, Q] Ipolex_Mul) |
856 (cong2 (args2 conv) (args2 conv)) |
856 (cong2 (args2 conv) (args2 conv)) |
857 | (@{const_name Pow}, [P, n]) => |
857 | (\<^const_name>\<open>Pow\<close>, [P, n]) => |
858 transitive' |
858 transitive' |
859 (inst [] [l, P, n] Ipolex_Pow) |
859 (inst [] [l, P, n] Ipolex_Pow) |
860 (cong2 (args2 conv) Thm.reflexive) |
860 (cong2 (args2 conv) Thm.reflexive) |
861 | (@{const_name Neg}, [P]) => |
861 | (\<^const_name>\<open>Neg\<close>, [P]) => |
862 transitive' |
862 transitive' |
863 (inst [] [l, P] Ipolex_Neg) |
863 (inst [] [l, P] Ipolex_Neg) |
864 (cong1 (args2 conv))) |
864 (cong1 (args2 conv))) |
865 in conv end; |
865 in conv end; |
866 |
866 |
867 fun Ipolex_polex_list_conv (rls as |
867 fun Ipolex_polex_list_conv (rls as |
868 (_, _, |
868 (_, _, |
869 [Ipolex_polex_list_Nil, Ipolex_polex_list_Cons], _, _, _)) l pps = |
869 [Ipolex_polex_list_Nil, Ipolex_polex_list_Cons], _, _, _)) l pps = |
870 (case strip_app pps of |
870 (case strip_app pps of |
871 (@{const_name Nil}, []) => inst [] [l] Ipolex_polex_list_Nil |
871 (\<^const_name>\<open>Nil\<close>, []) => inst [] [l] Ipolex_polex_list_Nil |
872 | (@{const_name Cons}, [p, pps']) => (case strip_app p of |
872 | (\<^const_name>\<open>Cons\<close>, [p, pps']) => (case strip_app p of |
873 (@{const_name Pair}, [P, Q]) => |
873 (\<^const_name>\<open>Pair\<close>, [P, Q]) => |
874 transitive' |
874 transitive' |
875 (inst [] [l, P, Q, pps'] Ipolex_polex_list_Cons) |
875 (inst [] [l, P, Q, pps'] Ipolex_polex_list_Cons) |
876 (cong2 |
876 (cong2 |
877 (cong2 (args2 (Ipolex_conv rls)) (args2 (Ipolex_conv rls))) |
877 (cong2 (args2 (Ipolex_conv rls)) (args2 (Ipolex_conv rls))) |
878 (args2 (Ipolex_polex_list_conv rls))))); |
878 (args2 (Ipolex_polex_list_conv rls))))); |