equal
deleted
inserted
replaced
1 theory LamEx |
1 theory LamEx |
2 imports Nominal QuotMain |
2 imports Nominal QuotMain |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
|
6 |
|
7 thm abs_fresh(1) |
6 |
8 |
7 nominal_datatype rlam = |
9 nominal_datatype rlam = |
8 rVar "name" |
10 rVar "name" |
9 | rApp "rlam" "rlam" |
11 | rApp "rlam" "rlam" |
10 | rLam "name" "rlam" |
12 | rLam "name" "rlam" |
14 where |
16 where |
15 a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)" |
17 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" |
18 | 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>[b].s\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s" |
19 | a3: "\<lbrakk>t \<approx> ([(a,b)]\<bullet>s); a\<sharp>[b].s\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s" |
18 |
20 |
|
21 function |
|
22 rfv :: "rlam \<Rightarrow> name set" |
|
23 where |
|
24 rfv_var: "rfv (rVar a) = {a}" |
|
25 | rfv_app: "rfv (rApp t1 t2) = (rfv t1) \<union> (rfv t2)" |
|
26 | rfv_lam: "rfv (rLam a t) = (rfv t) - {a}" |
|
27 sorry |
|
28 |
|
29 termination rfv sorry |
|
30 |
19 quotient lam = rlam / alpha |
31 quotient lam = rlam / alpha |
20 sorry |
32 sorry |
21 |
33 |
22 print_quotients |
34 print_quotients |
23 |
35 |
37 "Lam \<equiv> rLam" |
49 "Lam \<equiv> rLam" |
38 |
50 |
39 thm Var_def |
51 thm Var_def |
40 thm App_def |
52 thm App_def |
41 thm Lam_def |
53 thm Lam_def |
|
54 |
|
55 quotient_def (for lam) |
|
56 fv :: "lam \<Rightarrow> name set" |
|
57 where |
|
58 "fv \<equiv> rfv" |
|
59 |
|
60 thm fv_def |
42 |
61 |
43 (* definition of overloaded permutation function *) |
62 (* definition of overloaded permutation function *) |
44 (* for the lifted type lam *) |
63 (* for the lifted type lam *) |
45 overloading |
64 overloading |
46 perm_lam \<equiv> "perm :: 'x prm \<Rightarrow> lam \<Rightarrow> lam" (unchecked) |
65 perm_lam \<equiv> "perm :: 'x prm \<Rightarrow> lam \<Rightarrow> lam" (unchecked) |
75 lemma pi_lam_com: |
94 lemma pi_lam_com: |
76 fixes pi::"'x prm" |
95 fixes pi::"'x prm" |
77 shows "(pi\<bullet>rLam a t) \<approx> rLam (pi\<bullet>a) (pi\<bullet>t)" |
96 shows "(pi\<bullet>rLam a t) \<approx> rLam (pi\<bullet>a) (pi\<bullet>t)" |
78 sorry |
97 sorry |
79 |
98 |
|
99 lemma fv_var: |
|
100 shows "fv (Var a) = {a}" |
|
101 sorry |
|
102 |
|
103 lemma fv_app: |
|
104 shows "fv (App t1 t2) = (fv t1) \<union> (fv t2)" |
|
105 sorry |
|
106 |
|
107 lemma fv_lam: |
|
108 shows "fv (Lam a t) = (fv t) - {a}" |
|
109 sorry |
|
110 |
80 lemma real_alpha: |
111 lemma real_alpha: |
81 assumes "t = ([(a,b)]\<bullet>s)" "a\<sharp>s" |
112 assumes "t = ([(a,b)]\<bullet>s)" "a\<sharp>[b].s" |
82 shows "Lam a t = Lam b s" |
113 shows "Lam a t = Lam b s" |
83 sorry |
114 sorry |
84 |
115 |
85 |
116 |
86 |
117 |