equal
deleted
inserted
replaced
35 quotient lam = rlam / alpha |
35 quotient lam = rlam / alpha |
36 sorry |
36 sorry |
37 |
37 |
38 print_quotients |
38 print_quotients |
39 |
39 |
40 quotient_def (for lam) |
40 quotient_def |
41 Var :: "name \<Rightarrow> lam" |
41 Var :: "name \<Rightarrow> lam" |
42 where |
42 where |
43 "Var \<equiv> rVar" |
43 "Var \<equiv> rVar" |
44 |
44 |
45 quotient_def (for lam) |
45 quotient_def |
46 App :: "lam \<Rightarrow> lam \<Rightarrow> lam" |
46 App :: "lam \<Rightarrow> lam \<Rightarrow> lam" |
47 where |
47 where |
48 "App \<equiv> rApp" |
48 "App \<equiv> rApp" |
49 |
49 |
50 quotient_def (for lam) |
50 quotient_def |
51 Lam :: "name \<Rightarrow> lam \<Rightarrow> lam" |
51 Lam :: "name \<Rightarrow> lam \<Rightarrow> lam" |
52 where |
52 where |
53 "Lam \<equiv> rLam" |
53 "Lam \<equiv> rLam" |
54 |
54 |
55 thm Var_def |
55 thm Var_def |
56 thm App_def |
56 thm App_def |
57 thm Lam_def |
57 thm Lam_def |
58 |
58 |
59 quotient_def (for lam) |
59 quotient_def |
60 fv :: "lam \<Rightarrow> name set" |
60 fv :: "lam \<Rightarrow> name set" |
61 where |
61 where |
62 "fv \<equiv> rfv" |
62 "fv \<equiv> rfv" |
63 |
63 |
64 thm fv_def |
64 thm fv_def |
65 |
65 |
66 (* definition of overloaded permutation function *) |
66 (* definition of overloaded permutation function *) |
67 (* for the lifted type lam *) |
67 (* for the lifted type lam *) |
68 overloading |
68 overloading |
69 perm_lam \<equiv> "perm :: 'x prm \<Rightarrow> lam \<Rightarrow> lam" (unchecked) |
69 perm_lam \<equiv> "perm :: 'x prm \<Rightarrow> lam \<Rightarrow> lam" (unchecked) |
70 begin |
70 begin |
71 |
71 |
72 quotient_def (for lam) |
72 quotient_def |
73 perm_lam :: "'x prm \<Rightarrow> lam \<Rightarrow> lam" |
73 perm_lam :: "'x prm \<Rightarrow> lam \<Rightarrow> lam" |
74 where |
74 where |
75 "perm_lam \<equiv> (perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam)" |
75 "perm_lam \<equiv> (perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam)" |
76 |
76 |
77 end |
77 end |
306 |
306 |
307 thm alpha_induct |
307 thm alpha_induct |
308 thm alpha.induct |
308 thm alpha.induct |
309 |
309 |
310 lemma rvar_inject: "rVar a \<approx> rVar b \<Longrightarrow> (a = b)" |
310 lemma rvar_inject: "rVar a \<approx> rVar b \<Longrightarrow> (a = b)" |
311 apply (rule alpha.cases) |
311 apply (erule alpha.cases) |
312 apply (assumption) |
312 apply (simp add: rlam.inject) |
313 apply (assumption) |
313 apply (simp) |
314 apply (simp_all) |
314 apply (simp) |
315 apply (cases "a = b") |
315 done |
316 apply (simp_all) |
|
317 apply (cases "ba = b") |
|
318 apply (simp_all) |
|
319 |
316 |
320 |
317 |
321 lemma var_inject_test: |
318 lemma var_inject_test: |
322 fixes a b |
319 fixes a b |
323 assumes a: "Var a = Var b" |
320 assumes a: "Var a = Var b" |