equal
deleted
inserted
replaced
9 nominal_datatype rlam = |
9 nominal_datatype rlam = |
10 rVar "name" |
10 rVar "name" |
11 | rApp "rlam" "rlam" |
11 | rApp "rlam" "rlam" |
12 | rLam "name" "rlam" |
12 | rLam "name" "rlam" |
13 |
13 |
14 inductive |
|
15 alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100) |
|
16 where |
|
17 a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)" |
|
18 | a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2" |
|
19 | a3: "\<lbrakk>t \<approx> ([(a,b)]\<bullet>s); a\<sharp>[b].s\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s" |
|
20 |
14 |
21 function |
15 function |
22 rfv :: "rlam \<Rightarrow> name set" |
16 rfv :: "rlam \<Rightarrow> name set" |
23 where |
17 where |
24 rfv_var: "rfv (rVar a) = {a}" |
18 rfv_var: "rfv (rVar a) = {a}" |
25 | rfv_app: "rfv (rApp t1 t2) = (rfv t1) \<union> (rfv t2)" |
19 | rfv_app: "rfv (rApp t1 t2) = (rfv t1) \<union> (rfv t2)" |
26 | rfv_lam: "rfv (rLam a t) = (rfv t) - {a}" |
20 | rfv_lam: "rfv (rLam a t) = (rfv t) - {a}" |
27 sorry |
21 sorry |
28 |
22 |
29 termination rfv sorry |
23 termination rfv sorry |
|
24 |
|
25 inductive |
|
26 alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100) |
|
27 where |
|
28 a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)" |
|
29 | a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2" |
|
30 | a3: "\<lbrakk>t \<approx> ([(a,b)]\<bullet>s); a \<notin> rfv (rLam b t)\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s" |
30 |
31 |
31 quotient lam = rlam / alpha |
32 quotient lam = rlam / alpha |
32 sorry |
33 sorry |
33 |
34 |
34 print_quotients |
35 print_quotients |