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_definition |
60 "Var :: name \<Rightarrow> lam" |
60 "Var :: name \<Rightarrow> lam" |
61 as |
61 as |
62 "rVar" |
62 "rVar" |
63 |
63 |
64 quotient_def |
64 quotient_definition |
65 "App :: lam \<Rightarrow> lam \<Rightarrow> lam" |
65 "App :: lam \<Rightarrow> lam \<Rightarrow> lam" |
66 as |
66 as |
67 "rApp" |
67 "rApp" |
68 |
68 |
69 quotient_def |
69 quotient_definition |
70 "Lam :: name \<Rightarrow> lam \<Rightarrow> lam" |
70 "Lam :: name \<Rightarrow> lam \<Rightarrow> lam" |
71 as |
71 as |
72 "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_definition |
79 "fv :: lam \<Rightarrow> name set" |
79 "fv :: lam \<Rightarrow> name set" |
80 as |
80 as |
81 "rfv" |
81 "rfv" |
82 |
82 |
83 thm fv_def |
83 thm fv_def |
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_definition |
92 "perm_lam :: 'x prm \<Rightarrow> lam \<Rightarrow> lam" |
92 "perm_lam :: 'x prm \<Rightarrow> lam \<Rightarrow> lam" |
93 as |
93 as |
94 "perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam" |
94 "perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam" |
95 |
95 |
96 end |
96 end |