equal
deleted
inserted
replaced
1658 next |
1658 next |
1659 fix x y assume "f (x, y) \<noteq> g (x, y)" "x \<in> Field s" "y \<in> Field t" |
1659 fix x y assume "f (x, y) \<noteq> g (x, y)" "x \<in> Field s" "y \<in> Field t" |
1660 thus "((x, y), (s.max_fun_diff (rev_curr f m) (rev_curr g m), m)) \<in> s *o t" |
1660 thus "((x, y), (s.max_fun_diff (rev_curr f m) (rev_curr g m), m)) \<in> s *o t" |
1661 using rst.max_fun_diff_in[OF diff1] rs.max_fun_diff_in[OF diff2] diff1 diff2 |
1661 using rst.max_fun_diff_in[OF diff1] rs.max_fun_diff_in[OF diff2] diff1 diff2 |
1662 rst.max_fun_diff_max[OF diff1, of y] rs.max_fun_diff_le_eq[OF _ diff2, of x] |
1662 rst.max_fun_diff_max[OF diff1, of y] rs.max_fun_diff_le_eq[OF _ diff2, of x] |
1663 unfolding oprod_def m_def rev_curr_def fun_eq_iff by auto (metis s.in_notinI) |
1663 unfolding oprod_def m_def rev_curr_def fun_eq_iff by (auto intro: s.in_notinI) |
1664 qed |
1664 qed |
1665 qed |
1665 qed |
1666 |
1666 |
1667 lemma oexp_oexp: "(r ^o s) ^o t =o r ^o (s *o t)" (is "?R =o ?L") |
1667 lemma oexp_oexp: "(r ^o s) ^o t =o r ^o (s *o t)" (is "?R =o ?L") |
1668 proof (cases "r = {}") |
1668 proof (cases "r = {}") |