equal
deleted
inserted
replaced
31 | a3: "\<lbrakk>t \<approx> ([(a,b)]\<bullet>s); a \<notin> rfv (rLam b t)\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s" |
31 | a3: "\<lbrakk>t \<approx> ([(a,b)]\<bullet>s); a \<notin> rfv (rLam b t)\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s" |
32 |
32 |
33 print_theorems |
33 print_theorems |
34 |
34 |
35 lemma alpha_refl: |
35 lemma alpha_refl: |
36 shows "x \<approx> x" |
36 fixes t::"rlam" |
37 apply (rule rlam.induct) |
37 shows "t \<approx> t" |
38 apply (simp_all add:a1 a2) |
38 apply(induct t rule: rlam.induct) |
39 apply (rule a3) |
39 apply(simp add: a1) |
40 apply (simp_all) |
40 apply(simp add: a2) |
41 (* apply (simp add: pt_swap_bij'') *) |
41 apply(rule a3) |
|
42 apply(subst pt_swap_bij'') |
|
43 apply(rule pt_name_inst) |
|
44 apply(rule at_name_inst) |
|
45 apply(simp) |
|
46 apply(simp) |
|
47 done |
|
48 |
|
49 lemma alpha_EQUIV: |
|
50 shows "EQUIV alpha" |
42 sorry |
51 sorry |
43 |
52 |
44 quotient lam = rlam / alpha |
53 quotient lam = rlam / alpha |
45 sorry |
54 apply(rule alpha_EQUIV) |
|
55 done |
46 |
56 |
47 print_quotients |
57 print_quotients |
48 |
58 |
49 quotient_def |
59 quotient_def |
50 Var :: "name \<Rightarrow> lam" |
60 Var :: "name \<Rightarrow> lam" |
124 lemma real_alpha: |
134 lemma real_alpha: |
125 assumes "t = [(a,b)]\<bullet>s" "a\<sharp>[b].s" |
135 assumes "t = [(a,b)]\<bullet>s" "a\<sharp>[b].s" |
126 shows "Lam a t = Lam b s" |
136 shows "Lam a t = Lam b s" |
127 sorry |
137 sorry |
128 |
138 |
129 lemma perm_rsp: "(op = ===> alpha ===> alpha) op \<bullet> op \<bullet>" |
139 lemma perm_rsp: |
|
140 "(op = ===> alpha ===> alpha) op \<bullet> op \<bullet>" |
130 apply(auto) |
141 apply(auto) |
131 (* this is propably true if some type conditions are imposed ;o) *) |
142 (* this is propably true if some type conditions are imposed ;o) *) |
132 sorry |
143 sorry |
133 |
144 |
134 lemma fresh_rsp: "(op = ===> alpha ===> op =) fresh fresh" |
145 lemma fresh_rsp: |
|
146 "(op = ===> alpha ===> op =) fresh fresh" |
135 apply(auto) |
147 apply(auto) |
136 (* this is probably only true if some type conditions are imposed *) |
148 (* this is probably only true if some type conditions are imposed *) |
137 sorry |
149 sorry |
138 |
150 |
139 lemma rVar_rsp: "(op = ===> alpha) rVar rVar" |
151 lemma rVar_rsp: "(op = ===> alpha) rVar rVar" |
187 ML {* val fv_lam = lift_thm_lam @{context} @{thm rfv_lam} *} |
199 ML {* val fv_lam = lift_thm_lam @{context} @{thm rfv_lam} *} |
188 |
200 |
189 ML {* val a1 = lift_thm_lam @{context} @{thm a1} *} |
201 ML {* val a1 = lift_thm_lam @{context} @{thm a1} *} |
190 ML {* val a2 = lift_thm_lam @{context} @{thm a2} *} |
202 ML {* val a2 = lift_thm_lam @{context} @{thm a2} *} |
191 ML {* val a3 = lift_thm_lam @{context} @{thm a3} *} |
203 ML {* val a3 = lift_thm_lam @{context} @{thm a3} *} |
|
204 |
|
205 thm a2 |
|
206 ML {* val t_a = atomize_thm @{thm a2} *} |
|
207 ML {* val t_r = regularize t_a @{typ rlam} @{term alpha} @{thm alpha_EQUIV} @{thm alpha_refl} @{context} *} |
192 |
208 |
193 ML {* val alpha_cases = lift_thm_lam @{context} @{thm alpha.cases} *} |
209 ML {* val alpha_cases = lift_thm_lam @{context} @{thm alpha.cases} *} |
194 ML {* val alpha_induct = lift_thm_lam @{context} @{thm alpha.induct} *} |
210 ML {* val alpha_induct = lift_thm_lam @{context} @{thm alpha.induct} *} |
195 |
211 |
196 ML {* val var_inject = lift_thm_lam @{context} @{thm rvar_inject} *} |
212 ML {* val var_inject = lift_thm_lam @{context} @{thm rvar_inject} *} |