equal
deleted
inserted
replaced
921 using assms by (auto simp: Abs1_eq_iff fresh_permute_left) |
921 using assms by (auto simp: Abs1_eq_iff fresh_permute_left) |
922 |
922 |
923 |
923 |
924 ML {* |
924 ML {* |
925 fun alpha_single_simproc thm _ ctxt ctrm = |
925 fun alpha_single_simproc thm _ ctxt ctrm = |
926 let |
926 let |
927 val thy = Proof_Context.theory_of ctxt |
927 val thy = Proof_Context.theory_of ctxt |
928 val _ $ (_ $ x) $ (_ $ y) = term_of ctrm |
928 val _ $ (_ $ x) $ (_ $ y) = Thm.term_of ctrm |
929 val cvrs = union (op =) (Term.add_frees x []) (Term.add_frees y []) |
929 val cvrs = union (op =) (Term.add_frees x []) (Term.add_frees y []) |
930 |> filter (fn (_, ty) => Sign.of_sort thy (ty, @{sort fs})) |
930 |> filter (fn (_, ty) => Sign.of_sort thy (ty, @{sort fs})) |
931 |> map Free |
931 |> map Free |
932 |> HOLogic.mk_tuple |
932 |> HOLogic.mk_tuple |
933 |> Thm.cterm_of thy |
933 |> Thm.cterm_of ctxt |
934 val cvrs_ty = ctyp_of_term cvrs |
934 val cvrs_ty = Thm.ctyp_of_cterm cvrs |
935 val thm' = thm |
935 val thm' = thm |
936 |> Drule.instantiate' [NONE, NONE, SOME cvrs_ty] [NONE, NONE, NONE, NONE, SOME cvrs] |
936 |> Drule.instantiate' [NONE, NONE, SOME cvrs_ty] [NONE, NONE, NONE, NONE, SOME cvrs] |
937 in |
937 in |
938 SOME thm' |
938 SOME thm' |
939 end |
939 end |
1048 "prod_alpha = rel_prod" |
1048 "prod_alpha = rel_prod" |
1049 |
1049 |
1050 lemma [quot_respect]: |
1050 lemma [quot_respect]: |
1051 shows "((R1 ===> op =) ===> (R2 ===> op =) ===> rel_prod R1 R2 ===> op =) prod_fv prod_fv" |
1051 shows "((R1 ===> op =) ===> (R2 ===> op =) ===> rel_prod R1 R2 ===> op =) prod_fv prod_fv" |
1052 unfolding rel_fun_def |
1052 unfolding rel_fun_def |
1053 unfolding rel_prod_def |
|
1054 by auto |
1053 by auto |
1055 |
1054 |
1056 lemma [quot_preserve]: |
1055 lemma [quot_preserve]: |
1057 assumes q1: "Quotient3 R1 abs1 rep1" |
1056 assumes q1: "Quotient3 R1 abs1 rep1" |
1058 and q2: "Quotient3 R2 abs2 rep2" |
1057 and q2: "Quotient3 R2 abs2 rep2" |
1065 by auto |
1064 by auto |
1066 |
1065 |
1067 lemma [eqvt]: |
1066 lemma [eqvt]: |
1068 shows "p \<bullet> prod_alpha A B x y = prod_alpha (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)" |
1067 shows "p \<bullet> prod_alpha A B x y = prod_alpha (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)" |
1069 unfolding prod_alpha_def |
1068 unfolding prod_alpha_def |
1070 unfolding rel_prod_def |
1069 unfolding rel_prod_conv |
1071 by (perm_simp) (rule refl) |
1070 by (perm_simp) (rule refl) |
1072 |
1071 |
1073 lemma [eqvt]: |
1072 lemma [eqvt]: |
1074 shows "p \<bullet> prod_fv A B (x, y) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)" |
1073 shows "p \<bullet> prod_fv A B (x, y) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)" |
1075 unfolding prod_fv.simps |
1074 unfolding prod_fv.simps |