equal
deleted
inserted
replaced
57 by blast |
57 by blast |
58 show ?case |
58 show ?case |
59 proof (cases "a = b") |
59 proof (cases "a = b") |
60 case True |
60 case True |
61 have "((I + {#b#}) + K, (I + {#b#}) + J) \<in> mult R" |
61 have "((I + {#b#}) + K, (I + {#b#}) + J) \<in> mult R" |
62 apply (rule one_step_implies_mult[OF transR]) |
62 apply (rule one_step_implies_mult) |
63 apply (auto simp add: decomposed) |
63 apply (auto simp add: decomposed) |
64 done |
64 done |
65 then show ?thesis |
65 then show ?thesis |
66 apply (simp only: as bs) |
66 apply (simp only: as bs) |
67 apply (simp only: decomposed True) |
67 apply (simp only: decomposed True) |
69 done |
69 done |
70 next |
70 next |
71 case False |
71 case False |
72 from False lprod_list have False: "(a, b) \<in> R" by blast |
72 from False lprod_list have False: "(a, b) \<in> R" by blast |
73 have "(I + (K + {#a#}), I + (J + {#b#})) \<in> mult R" |
73 have "(I + (K + {#a#}), I + (J + {#b#})) \<in> mult R" |
74 apply (rule one_step_implies_mult[OF transR]) |
74 apply (rule one_step_implies_mult) |
75 apply (auto simp add: False decomposed) |
75 apply (auto simp add: False decomposed) |
76 done |
76 done |
77 then show ?thesis |
77 then show ?thesis |
78 apply (simp only: as bs) |
78 apply (simp only: as bs) |
79 apply (simp only: decomposed) |
79 apply (simp only: decomposed) |