equal
deleted
inserted
replaced
110 error |
110 error |
111 ("Theorem must be of the form \"?p \<bullet> c \<equiv> c\", with c a constant or fixed parameter:\n" ^ |
111 ("Theorem must be of the form \"?p \<bullet> c \<equiv> c\", with c a constant or fixed parameter:\n" ^ |
112 Syntax.string_of_term (Context.proof_of context) (prop_of thm)) |
112 Syntax.string_of_term (Context.proof_of context) (prop_of thm)) |
113 in |
113 in |
114 case prop_of thm of |
114 case prop_of thm of |
115 Const ("Pure.eq", _) $ (Const (@{const_name "permute"}, _) $ p $ c) $ c' => |
115 Const (@{const_name Pure.eq}, _) $ (Const (@{const_name "permute"}, _) $ p $ c) $ c' => |
116 if is_Var p andalso is_fixed (Context.proof_of context) c andalso c aconv c' then |
116 if is_Var p andalso is_fixed (Context.proof_of context) c andalso c aconv c' then |
117 c |
117 c |
118 else |
118 else |
119 error_msg () |
119 error_msg () |
120 | _ => error_msg () |
120 | _ => error_msg () |
254 |
254 |
255 (* Transforms a theorem of the form (1) or (2) into the form (4). *) |
255 (* Transforms a theorem of the form (1) or (2) into the form (4). *) |
256 fun eqvt_transform ctxt thm = |
256 fun eqvt_transform ctxt thm = |
257 (case prop_of thm of @{const "Trueprop"} $ _ => |
257 (case prop_of thm of @{const "Trueprop"} $ _ => |
258 thm_4_of_1 ctxt thm |
258 thm_4_of_1 ctxt thm |
259 | @{const "Pure.imp"} $ _ $ _ => |
259 | @{const Pure.imp} $ _ $ _ => |
260 thm_4_of_1 ctxt (thm_1_of_2 ctxt thm) |
260 thm_4_of_1 ctxt (thm_1_of_2 ctxt thm) |
261 | _ => |
261 | _ => |
262 error msg) |
262 error msg) |
263 handle THM _ => |
263 handle THM _ => |
264 error msg |
264 error msg |
277 else |
277 else |
278 thm |
278 thm |
279 in |
279 in |
280 (th', thm_4_of_1 ctxt thm) |
280 (th', thm_4_of_1 ctxt thm) |
281 end |
281 end |
282 | @{const "Pure.imp"} $ _ $ _ => |
282 | @{const Pure.imp} $ _ $ _ => |
283 let |
283 let |
284 val th1 = thm_1_of_2 ctxt thm |
284 val th1 = thm_1_of_2 ctxt thm |
285 in |
285 in |
286 (thm_3_of_1 ctxt th1, thm_4_of_1 ctxt th1) |
286 (thm_3_of_1 ctxt th1, thm_4_of_1 ctxt th1) |
287 end |
287 end |