38 term bn |
40 term bn |
39 term fv_trm |
41 term fv_trm |
40 term alpha_bn |
42 term alpha_bn |
41 |
43 |
42 |
44 |
43 lemma a2: |
45 lemma exi_zero: "P 0 \<Longrightarrow> \<exists>(x::perm). P x" by auto |
44 shows "alpha_trm_raw x1 y1 \<Longrightarrow> fv_trm_raw x1 = fv_trm_raw y1" |
46 |
45 and "alpha_assg_raw x2 y2 \<Longrightarrow> fv_assg_raw x2 = fv_assg_raw y2 \<and> bn_raw x2 = bn_raw y2" |
47 ML {* |
46 and "alpha_bn_raw x3 y3 \<Longrightarrow> fv_bn_raw x3 = fv_bn_raw y3" |
48 val pre_ss = @{thms fun_rel_def} |
47 apply(induct rule: alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts) |
49 val post_ss = @{thms alphas prod_alpha_def prod_rel.simps |
48 apply(simp_all only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps bn_raw.simps |
50 prod_fv.simps fresh_star_zero permute_zero funs_rsp prod.cases alpha_bn_imps} |
49 alphas prod_fv.simps prod_alpha_def ex_simps Un_assoc set.simps append.simps Un_insert_left Un_empty_right Un_empty_left simp_thms) |
51 |
50 done |
52 val tac = |
|
53 asm_full_simp_tac (HOL_ss addsimps pre_ss) |
|
54 THEN' REPEAT o (resolve_tac @{thms allI impI}) |
|
55 THEN' resolve_tac @{thms alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros} |
|
56 THEN_ALL_NEW (TRY o (rtac @{thm exi_zero}) THEN' asm_full_simp_tac (HOL_ss addsimps post_ss)) |
|
57 *} |
51 |
58 |
52 lemma [quot_respect]: |
59 lemma [quot_respect]: |
53 "(op= ===> alpha_trm_raw) Var_raw Var_raw" |
60 "(op= ===> alpha_trm_raw) Var_raw Var_raw" |
54 "(alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) App_raw App_raw" |
61 "(alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) App_raw App_raw" |
55 "(op= ===> alpha_trm_raw ===> alpha_trm_raw) Lam_raw Lam_raw" |
62 "(op= ===> alpha_trm_raw ===> alpha_trm_raw) Lam_raw Lam_raw" |
56 "(alpha_assg_raw ===> alpha_trm_raw ===> alpha_trm_raw) Let_raw Let_raw" |
63 "(alpha_assg_raw ===> alpha_trm_raw ===> alpha_trm_raw) Let_raw Let_raw" |
57 "(op= ===> op= ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) |
64 "(op= ===> op= ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) |
58 Foo_raw Foo_raw" |
65 Foo_raw Foo_raw" |
59 "(op= ===> op= ===> alpha_trm_raw ===> alpha_trm_raw) Bar_raw Bar_raw" |
66 "(op= ===> op= ===> alpha_trm_raw ===> alpha_trm_raw) Bar_raw Bar_raw" |
60 "(op= ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) Baz_raw Baz_raw" |
67 "(op= ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) Baz_raw Baz_raw" |
61 "(op = ===> op = ===> alpha_trm_raw ===> alpha_assg_raw) As_raw As_raw" |
68 "(op = ===> op = ===> alpha_trm_raw ===> alpha_assg_raw) As_raw As_raw" |
62 apply(simp only: fun_rel_def) |
69 apply(tactic {* ALLGOALS tac *}) |
63 apply(simp only: eq_iff) |
|
64 apply(simp only: simp_thms) |
|
65 apply(simp only: fun_rel_def) |
|
66 apply(simp only: eq_iff) |
|
67 apply(tactic {* asm_full_simp_tac HOL_ss 1*}) |
|
68 apply(simp only: fun_rel_def) |
|
69 apply(simp only: eq_iff alphas fresh_star_def fresh_zero_perm a2) |
|
70 apply(rule allI | rule impI)+ |
|
71 apply(rule_tac x="0" in exI) |
|
72 apply(simp only: eq_iff alphas fresh_star_def fresh_zero_perm a2 permute_zero a2) |
|
73 apply(simp add: a2) |
|
74 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 alpha_bn_imps) |
|
75 apply(simp only: fun_rel_def) |
|
76 apply(rule allI | rule impI)+ |
|
77 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
|
78 apply(rule_tac x="0" in exI) |
|
79 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def) |
|
80 apply(simp only: fun_rel_def) |
|
81 apply(rule allI | rule impI)+ |
|
82 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
|
83 apply(rule_tac x="0" in exI) |
|
84 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def) |
|
85 apply(simp only: fun_rel_def) |
|
86 apply(rule allI | rule impI)+ |
|
87 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
|
88 apply(rule_tac x="0" in exI) |
|
89 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def) |
|
90 apply(rule_tac x="0" in exI) |
|
91 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def) |
|
92 apply(simp only: fun_rel_def) |
|
93 apply(rule allI | rule impI)+ |
|
94 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
|
95 apply(rule_tac x="0" in exI) |
|
96 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def) |
|
97 apply(assumption) |
|
98 done |
70 done |
99 |
71 |
100 lemma [quot_respect]: |
72 lemma [quot_respect]: |
101 "(alpha_trm_raw ===> op =) fv_trm_raw fv_trm_raw" |
73 "(alpha_trm_raw ===> op =) fv_trm_raw fv_trm_raw" |
102 "(alpha_assg_raw ===> op =) fv_bn_raw fv_bn_raw" |
74 "(alpha_assg_raw ===> op =) fv_bn_raw fv_bn_raw" |
103 "(alpha_assg_raw ===> op =) bn_raw bn_raw" |
75 "(alpha_assg_raw ===> op =) bn_raw bn_raw" |
104 "(alpha_assg_raw ===> op =) fv_assg_raw fv_assg_raw" |
76 "(alpha_assg_raw ===> op =) fv_assg_raw fv_assg_raw" |
105 "(op = ===> alpha_trm_raw ===> alpha_trm_raw) permute permute" |
77 "(op = ===> alpha_trm_raw ===> alpha_trm_raw) permute permute" |
106 apply(simp_all add: a2 a1) |
78 apply(simp_all add: alpha_bn_imps funs_rsp) |
107 sorry |
79 sorry |
108 |
80 |
109 ML {* |
81 ML {* |
110 val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct} |
82 val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct} |
111 *} |
83 *} |