equal
deleted
inserted
replaced
22 "bn (As x y t) = {atom x}" |
22 "bn (As x y t) = {atom x}" |
23 |
23 |
24 thm alpha_sym_thms |
24 thm alpha_sym_thms |
25 thm alpha_trans_thms |
25 thm alpha_trans_thms |
26 thm size_eqvt |
26 thm size_eqvt |
|
27 thm size_simps |
|
28 thm size_rsp |
27 thm alpha_bn_imps |
29 thm alpha_bn_imps |
28 thm distinct |
30 thm distinct |
29 thm eq_iff |
31 thm eq_iff |
30 thm eq_iff_simps |
32 thm eq_iff_simps |
31 thm fv_defs |
33 thm fv_defs |
40 term App |
42 term App |
41 term Baz |
43 term Baz |
42 term bn |
44 term bn |
43 term fv_trm |
45 term fv_trm |
44 term alpha_bn |
46 term alpha_bn |
45 |
|
46 |
47 |
47 lemma exi_zero: "P 0 \<Longrightarrow> \<exists>(x::perm). P x" by auto |
48 lemma exi_zero: "P 0 \<Longrightarrow> \<exists>(x::perm). P x" by auto |
48 |
49 |
49 ML {* |
50 ML {* |
50 val pre_ss = @{thms fun_rel_def} |
51 val pre_ss = @{thms fun_rel_def} |
75 "(alpha_trm_raw ===> op =) fv_trm_raw fv_trm_raw" |
76 "(alpha_trm_raw ===> op =) fv_trm_raw fv_trm_raw" |
76 "(alpha_assg_raw ===> op =) fv_bn_raw fv_bn_raw" |
77 "(alpha_assg_raw ===> op =) fv_bn_raw fv_bn_raw" |
77 "(alpha_assg_raw ===> op =) bn_raw bn_raw" |
78 "(alpha_assg_raw ===> op =) bn_raw bn_raw" |
78 "(alpha_assg_raw ===> op =) fv_assg_raw fv_assg_raw" |
79 "(alpha_assg_raw ===> op =) fv_assg_raw fv_assg_raw" |
79 "(op = ===> alpha_trm_raw ===> alpha_trm_raw) permute permute" |
80 "(op = ===> alpha_trm_raw ===> alpha_trm_raw) permute permute" |
80 apply(simp_all add: alpha_bn_imps funs_rsp) |
81 "(alpha_trm_raw ===> op =) size size" |
|
82 apply(simp_all add: alpha_bn_imps funs_rsp size_rsp) |
81 sorry |
83 sorry |
82 |
84 |
83 ML {* |
85 ML {* |
84 val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct} |
86 val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct} |
85 *} |
87 *} |