equal
deleted
inserted
replaced
962 end |
962 end |
963 handle _ => no_tac) |
963 handle _ => no_tac) |
964 | _ => no_tac) |
964 | _ => no_tac) |
965 *} |
965 *} |
966 |
966 |
967 lemma fun_rel_id: |
|
968 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
|
969 shows "(R1 ===> R2) f g" |
|
970 using a by simp |
|
971 |
|
972 |
|
973 ML {* |
967 ML {* |
974 fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) => |
968 fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) => |
975 (case (bare_concl goal) of |
969 (case (bare_concl goal) of |
976 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
970 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
977 ((Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)) |
971 ((Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)) |