21 | rfv_lam: "rfv (rLam a t) = (rfv t) - {a}" |
21 | rfv_lam: "rfv (rLam a t) = (rfv t) - {a}" |
22 sorry |
22 sorry |
23 |
23 |
24 termination rfv sorry |
24 termination rfv sorry |
25 |
25 |
26 inductive |
26 inductive |
27 alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100) |
27 alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100) |
28 where |
28 where |
29 a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)" |
29 a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)" |
30 | a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2" |
30 | a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2" |
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 |
|
35 lemma alpha_refl: |
|
36 shows "x \<approx> x" |
|
37 sorry |
34 |
38 |
35 quotient lam = rlam / alpha |
39 quotient lam = rlam / alpha |
36 sorry |
40 sorry |
37 |
41 |
38 print_quotients |
42 print_quotients |
114 |
118 |
115 lemma real_alpha: |
119 lemma real_alpha: |
116 assumes "t = [(a,b)]\<bullet>s" "a\<sharp>[b].s" |
120 assumes "t = [(a,b)]\<bullet>s" "a\<sharp>[b].s" |
117 shows "Lam a t = Lam b s" |
121 shows "Lam a t = Lam b s" |
118 sorry |
122 sorry |
119 |
|
120 |
|
121 |
|
122 |
|
123 |
|
124 (* Construction Site code *) |
|
125 |
123 |
126 lemma perm_rsp: "(op = ===> alpha ===> alpha) op \<bullet> op \<bullet>" |
124 lemma perm_rsp: "(op = ===> alpha ===> alpha) op \<bullet> op \<bullet>" |
127 apply(auto) |
125 apply(auto) |
128 (* this is propably true if some type conditions are imposed ;o) *) |
126 (* this is propably true if some type conditions are imposed ;o) *) |
129 sorry |
127 sorry |
161 |
159 |
162 lemma rfv_rsp: "(alpha ===> op =) rfv rfv" |
160 lemma rfv_rsp: "(alpha ===> op =) rfv rfv" |
163 sorry |
161 sorry |
164 |
162 |
165 ML {* val qty = @{typ "lam"} *} |
163 ML {* val qty = @{typ "lam"} *} |
166 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
|
167 ML {* val defs = @{thms Var_def App_def Lam_def perm_lam_def fv_def} *} |
164 ML {* val defs = @{thms Var_def App_def Lam_def perm_lam_def fv_def} *} |
168 ML {* val consts = lookup_quot_consts defs *} |
165 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} @ |
169 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *} |
166 @{thms ho_all_prs ho_ex_prs} *} |
170 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} @ @{thms ho_all_prs ho_ex_prs} *} |
167 |
171 ML {* fun lift_thm_lam lthy t = lift_thm lthy qty "lam" rsp_thms defs t *} |
168 ML {* fun lift_thm_lam lthy t = lift_thm lthy qty "lam" rsp_thms defs t *} |
172 |
169 |
173 ML {* val pi_var = lift_thm_lam @{context} @{thm pi_var_com} *} |
170 ML {* val pi_var = lift_thm_lam @{context} @{thm pi_var_com} *} |
174 ML {* val pi_app = lift_thm_lam @{context} @{thm pi_app_com} *} |
171 ML {* val pi_app = lift_thm_lam @{context} @{thm pi_app_com} *} |
175 ML {* val pi_lam = lift_thm_lam @{context} @{thm pi_lam_com} *} |
172 ML {* val pi_lam = lift_thm_lam @{context} @{thm pi_lam_com} *} |
181 ML {* val a1 = lift_thm_lam @{context} @{thm a1} *} |
178 ML {* val a1 = lift_thm_lam @{context} @{thm a1} *} |
182 ML {* val a2 = lift_thm_lam @{context} @{thm a2} *} |
179 ML {* val a2 = lift_thm_lam @{context} @{thm a2} *} |
183 ML {* val a3 = lift_thm_lam @{context} @{thm a3} *} |
180 ML {* val a3 = lift_thm_lam @{context} @{thm a3} *} |
184 |
181 |
185 ML {* val alpha_cases = lift_thm_lam @{context} @{thm alpha.cases} *} |
182 ML {* val alpha_cases = lift_thm_lam @{context} @{thm alpha.cases} *} |
|
183 ML {* val alpha_induct = lift_thm_lam @{context} @{thm alpha.induct} *} |
186 |
184 |
187 local_setup {* |
185 local_setup {* |
188 Quotient.note (@{binding "pi_var"}, pi_var) #> snd #> |
186 Quotient.note (@{binding "pi_var"}, pi_var) #> snd #> |
189 Quotient.note (@{binding "pi_app"}, pi_app) #> snd #> |
187 Quotient.note (@{binding "pi_app"}, pi_app) #> snd #> |
190 Quotient.note (@{binding "pi_lam"}, pi_lam) #> snd #> |
188 Quotient.note (@{binding "pi_lam"}, pi_lam) #> snd #> |
191 Quotient.note (@{binding "a1"}, a1) #> snd #> |
189 Quotient.note (@{binding "a1"}, a1) #> snd #> |
192 Quotient.note (@{binding "a2"}, a2) #> snd #> |
190 Quotient.note (@{binding "a2"}, a2) #> snd #> |
193 Quotient.note (@{binding "a3"}, a3) #> snd #> |
191 Quotient.note (@{binding "a3"}, a3) #> snd #> |
194 Quotient.note (@{binding "alpha_cases"}, alpha_cases) #> snd |
192 Quotient.note (@{binding "alpha_cases"}, alpha_cases) #> snd #> |
|
193 Quotient.note (@{binding "alpha_induct"}, alpha_induct) #> snd |
195 *} |
194 *} |
196 |
195 |
197 thm alpha.cases |
196 thm alpha.cases |
198 thm alpha_cases |
197 thm alpha_cases |
199 |
198 thm alpha.induct |
200 thm rlam.inject |
199 thm alpha_induct |
201 thm pi_var |
200 |
202 |
201 lemma rvar_inject: "rVar a \<approx> rVar b = (a = b)" |
203 |
202 apply (auto) |
204 lemma var_inject: |
203 apply (erule alpha.cases) |
205 shows "(Var a = Var b) = (a = b)" |
204 apply (simp_all add: rlam.inject alpha_refl) |
206 sorry |
205 done |
|
206 |
|
207 ML {* val var_inject = Toplevel.program (fn () => lift_thm_lam @{context} @{thm rvar_inject}) *} |
|
208 |
|
209 local_setup {* |
|
210 Quotient.note (@{binding "var_inject"}, var_inject) #> snd |
|
211 *} |
207 |
212 |
208 lemma var_supp: |
213 lemma var_supp: |
209 shows "supp (Var a) = ((supp a)::name set)" |
214 shows "supp (Var a) = ((supp a)::name set)" |
210 apply(simp add: supp_def) |
215 apply(simp add: supp_def) |
211 apply(simp add: pi_var) |
216 apply(simp add: pi_var) |
222 |
227 |
223 |
228 |
224 |
229 |
225 |
230 |
226 |
231 |
|
232 |
|
233 |
|
234 |
|
235 |
|
236 |
|
237 |
|
238 (* Construction Site code *) |
|
239 |
|
240 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
|
241 ML {* val consts = lookup_quot_consts defs *} |
|
242 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *} |
227 |
243 |
228 ML {* val t_a = atomize_thm @{thm alpha.induct} *} |
244 ML {* val t_a = atomize_thm @{thm alpha.induct} *} |
229 (* prove {* build_regularize_goal t_a rty rel @{context} *} |
245 (* prove {* build_regularize_goal t_a rty rel @{context} *} |
230 ML_prf {* fun tac ctxt = |
246 ML_prf {* fun tac ctxt = |
231 (FIRST' [ |
247 (FIRST' [ |
298 ML {* val t_r1 = repeat_eqsubst_thm @{context} @{thms fun_map.simps} t_r *} |
314 ML {* val t_r1 = repeat_eqsubst_thm @{context} @{thms fun_map.simps} t_r *} |
299 ML {* val t_r2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_lam.thm10} t_r1 *} |
315 ML {* val t_r2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_lam.thm10} t_r1 *} |
300 ML {* val t_r3 = MetaSimplifier.rewrite_rule @{thms eq_reflection[OF id_apply]} t_r2 *} |
316 ML {* val t_r3 = MetaSimplifier.rewrite_rule @{thms eq_reflection[OF id_apply]} t_r2 *} |
301 ML {* val alpha_induct = ObjectLogic.rulify t_r3 *} |
317 ML {* val alpha_induct = ObjectLogic.rulify t_r3 *} |
302 |
318 |
303 local_setup {* |
319 (*local_setup {* |
304 Quotient.note (@{binding "alpha_induct"}, alpha_induct) #> snd |
320 Quotient.note (@{binding "alpha_induct"}, alpha_induct) #> snd |
305 *} |
321 *}*) |
306 |
322 |
307 thm alpha_induct |
323 thm alpha_induct |
308 thm alpha.induct |
324 thm alpha.induct |
309 |
325 |
310 lemma rvar_inject: "rVar a \<approx> rVar b \<Longrightarrow> (a = b)" |
326 |
311 apply (erule alpha.cases) |
327 |
312 apply (simp add: rlam.inject) |
328 |
313 apply (simp) |
329 |
314 apply (simp) |
330 |
315 done |
331 |
316 |
332 |
317 |
|
318 lemma var_inject_test: |
|
319 fixes a b |
|
320 assumes a: "Var a = Var b" |
|
321 shows "(a = b)" |
|
322 using a apply (cases "a = b") |
|
323 apply (simp_all) |
|
324 apply (rule_tac x="Var a" and xa = "Var b" in alpha_cases) |
|
325 apply (rule a) |
|
326 |
|
327 |
|
328 lemma |
|
329 assumes a: "(x::lam) = y" |
|
330 shows "P x y" |
|
331 apply (induct rule: alpha_induct) |
|
332 apply (rule a) |
|
333 thm alpha.induct |
|
334 thm alpha_induct |
|
335 fun |
333 fun |
336 option_map::"('a \<Rightarrow> 'b) \<Rightarrow> ('a noption) \<Rightarrow> ('b noption)" |
334 option_map::"('a \<Rightarrow> 'b) \<Rightarrow> ('a noption) \<Rightarrow> ('b noption)" |
337 where |
335 where |
338 "option_map f (nSome x) = nSome (f x)" |
336 "option_map f (nSome x) = nSome (f x)" |
339 | "option_map f nNone = nNone" |
337 | "option_map f nNone = nNone" |