equal
deleted
inserted
replaced
15 a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)" |
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" |
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" |
17 | a3: "\<lbrakk>t \<approx> ([(a,b)]\<bullet>s); a\<sharp>s\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s" |
18 |
18 |
19 quotient lam = rlam / alpha |
19 quotient lam = rlam / alpha |
|
20 apply - |
20 sorry |
21 sorry |
|
22 |
|
23 print_quotients |
21 |
24 |
22 local_setup {* |
25 local_setup {* |
23 make_const_def @{binding Var} @{term "rVar"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #> |
26 make_const_def @{binding Var} @{term "rVar"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #> |
24 make_const_def @{binding App} @{term "rApp"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #> |
27 make_const_def @{binding App} @{term "rApp"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #> |
25 make_const_def @{binding Lam} @{term "rLam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd |
28 make_const_def @{binding Lam} @{term "rLam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd |