equal
deleted
inserted
replaced
54 apply(rule alpha_equivp) |
54 apply(rule alpha_equivp) |
55 done |
55 done |
56 |
56 |
57 print_quotients |
57 print_quotients |
58 |
58 |
59 quotient_def |
59 quotient_def |
60 Var :: "name \<Rightarrow> lam" |
60 Var :: "Var :: name \<Rightarrow> lam" |
61 where |
61 where |
62 "Var \<equiv> rVar" |
62 "rVar" |
63 |
63 |
64 quotient_def |
64 quotient_def |
65 App :: "lam \<Rightarrow> lam \<Rightarrow> lam" |
65 App :: "App :: lam \<Rightarrow> lam \<Rightarrow> lam" |
66 where |
66 where |
67 "App \<equiv> rApp" |
67 "rApp" |
68 |
68 |
69 quotient_def |
69 quotient_def |
70 Lam :: "name \<Rightarrow> lam \<Rightarrow> lam" |
70 Lam :: "Lam :: name \<Rightarrow> lam \<Rightarrow> lam" |
71 where |
71 where |
72 "Lam \<equiv> rLam" |
72 "rLam" |
73 |
73 |
74 thm Var_def |
74 thm Var_def |
75 thm App_def |
75 thm App_def |
76 thm Lam_def |
76 thm Lam_def |
77 |
77 |
78 quotient_def |
78 quotient_def |
79 fv :: "lam \<Rightarrow> name set" |
79 fv :: "fv :: lam \<Rightarrow> name set" |
80 where |
80 where |
81 "fv \<equiv> rfv" |
81 "rfv" |
82 |
82 |
83 thm fv_def |
83 thm fv_def |
84 |
84 |
85 (* definition of overloaded permutation function *) |
85 (* definition of overloaded permutation function *) |
86 (* for the lifted type lam *) |
86 (* for the lifted type lam *) |
87 overloading |
87 overloading |
88 perm_lam \<equiv> "perm :: 'x prm \<Rightarrow> lam \<Rightarrow> lam" (unchecked) |
88 perm_lam \<equiv> "perm :: 'x prm \<Rightarrow> lam \<Rightarrow> lam" (unchecked) |
89 begin |
89 begin |
90 |
90 |
91 quotient_def |
91 quotient_def |
92 perm_lam :: "'x prm \<Rightarrow> lam \<Rightarrow> lam" |
92 perm_lam :: "perm_lam :: 'x prm \<Rightarrow> lam \<Rightarrow> lam" |
93 where |
93 where |
94 "perm_lam \<equiv> (perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam)" |
94 "perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam" |
95 |
95 |
96 end |
96 end |
97 |
97 |
98 (*quotient_def (for lam) |
98 (*quotient_def (for lam) |
99 abs_fun_lam :: "'x prm \<Rightarrow> lam \<Rightarrow> lam" |
99 abs_fun_lam :: "'x prm \<Rightarrow> lam \<Rightarrow> lam" |