equal
deleted
inserted
replaced
183 (is "PROP ?eq ==> PROP ?cong ==> _ ==> _") |
183 (is "PROP ?eq ==> PROP ?cong ==> _ ==> _") |
184 proof - |
184 proof - |
185 assume cong: "PROP ?cong" |
185 assume cong: "PROP ?cong" |
186 assume "PROP ?eq" and "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" |
186 assume "PROP ?eq" and "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" |
187 hence "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:) |
187 hence "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:) |
188 also have "\<dots> = g a b" |
188 also have "... = g a b" |
189 proof (rule cong) |
189 proof (rule cong) |
190 show "\<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> = \<lfloor>a\<rfloor>" .. |
190 show "\<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> = \<lfloor>a\<rfloor>" .. |
191 moreover |
191 moreover |
192 show "\<lfloor>pick \<lfloor>b\<rfloor>\<rfloor> = \<lfloor>b\<rfloor>" .. |
192 show "\<lfloor>pick \<lfloor>b\<rfloor>\<rfloor> = \<lfloor>b\<rfloor>" .. |
193 moreover |
193 moreover |