equal
deleted
inserted
replaced
55 done |
55 done |
56 |
56 |
57 print_quotients |
57 print_quotients |
58 |
58 |
59 quotient_def |
59 quotient_def |
60 Var :: "Var :: name \<Rightarrow> lam" |
60 "Var :: name \<Rightarrow> lam" |
61 where |
61 as |
62 "rVar" |
62 "rVar" |
63 |
63 |
64 quotient_def |
64 quotient_def |
65 App :: "App :: lam \<Rightarrow> lam \<Rightarrow> lam" |
65 "App :: lam \<Rightarrow> lam \<Rightarrow> lam" |
66 where |
66 as |
67 "rApp" |
67 "rApp" |
68 |
68 |
69 quotient_def |
69 quotient_def |
70 Lam :: "Lam :: name \<Rightarrow> lam \<Rightarrow> lam" |
70 "Lam :: name \<Rightarrow> lam \<Rightarrow> lam" |
71 where |
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_def |
79 fv :: "fv :: lam \<Rightarrow> name set" |
79 "fv :: lam \<Rightarrow> name set" |
80 where |
80 as |
81 "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 *) |
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 :: "perm_lam :: 'x prm \<Rightarrow> lam \<Rightarrow> lam" |
92 "perm_lam :: 'x prm \<Rightarrow> lam \<Rightarrow> lam" |
93 where |
93 as |
94 "perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam" |
94 "perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam" |
95 |
95 |
96 end |
96 end |
97 |
|
98 (*quotient_def (for lam) |
|
99 abs_fun_lam :: "'x prm \<Rightarrow> lam \<Rightarrow> lam" |
|
100 where |
|
101 "perm_lam \<equiv> (perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam)"*) |
|
102 |
|
103 |
97 |
104 thm perm_lam_def |
98 thm perm_lam_def |
105 |
99 |
106 (* lemmas that need to lift *) |
100 (* lemmas that need to lift *) |
107 lemma pi_var_com: |
101 lemma pi_var_com: |