|
201
|
1 |
theory LamEx
|
|
|
2 |
imports Nominal QuotMain
|
|
|
3 |
begin
|
|
|
4 |
|
|
|
5 |
atom_decl name
|
|
|
6 |
|
|
|
7 |
nominal_datatype rlam =
|
|
|
8 |
rVar "name"
|
|
|
9 |
| rApp "rlam" "rlam"
|
|
|
10 |
| rLam "name" "rlam"
|
|
|
11 |
|
|
|
12 |
inductive
|
|
|
13 |
alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100)
|
|
|
14 |
where
|
|
|
15 |
a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)"
|
|
|
16 |
| a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2"
|
|
|
17 |
| a3: "\<lbrakk>t \<approx> ([(a,b)]\<bullet>s); a\<sharp>s\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s"
|
|
|
18 |
|
|
|
19 |
quotient lam = rlam / alpha
|
|
203
|
20 |
apply -
|
|
201
|
21 |
sorry
|
|
|
22 |
|
|
203
|
23 |
print_quotients
|
|
|
24 |
|
|
201
|
25 |
local_setup {*
|
|
|
26 |
make_const_def @{binding Var} @{term "rVar"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #>
|
|
|
27 |
make_const_def @{binding App} @{term "rApp"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #>
|
|
|
28 |
make_const_def @{binding Lam} @{term "rLam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd
|
|
|
29 |
*}
|
|
|
30 |
|
|
|
31 |
lemma real_alpha:
|
|
|
32 |
assumes "t = ([(a,b)]\<bullet>s)" "a\<sharp>s"
|
|
|
33 |
shows "Lam a t = Lam b s"
|
|
|
34 |
sorry |