src/HOL/ZF/LProd.thy
 changeset 62651 66568c9b8216 parent 60515 484559628038 child 66453 cc19f7ca2ed6
equal inserted replaced
62650:7e6bb43e7217 62651:66568c9b8216
`    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)`