|
1 theory LFex |
|
2 imports Nominal QuotMain |
|
3 begin |
|
4 |
|
5 atom_decl name id |
|
6 |
|
7 nominal_datatype kind = |
|
8 Type |
|
9 | KPi "ty" "name" "kind" |
|
10 and ty = |
|
11 TConst "id" |
|
12 | TApp "ty" "trm" |
|
13 | TPi "ty" "name" "ty" |
|
14 and trm = |
|
15 Const "id" |
|
16 | Var "name" |
|
17 | App "trm" "trm" |
|
18 | Lam "ty" "name" "trm" |
|
19 |
|
20 function |
|
21 fv_kind :: "kind \<Rightarrow> name set" |
|
22 and fv_ty :: "ty \<Rightarrow> name set" |
|
23 and fv_trm :: "trm \<Rightarrow> name set" |
|
24 where |
|
25 "fv_kind (Type) = {}" |
|
26 | "fv_kind (KPi A x K) = (fv_ty A) \<union> ((fv_kind K) - {x})" |
|
27 | "fv_ty (TConst i) = {}" |
|
28 | "fv_ty (TApp A M) = (fv_ty A) \<union> (fv_trm M)" |
|
29 | "fv_ty (TPi A x B) = (fv_ty A) \<union> ((fv_ty B) - {x})" |
|
30 | "fv_trm (Const i) = {}" |
|
31 | "fv_trm (Var x) = {x}" |
|
32 | "fv_trm (App M N) = (fv_trm M) \<union> (fv_trm N)" |
|
33 | "fv_trm (Lam A x M) = (fv_ty A) \<union> ((fv_trm M) - {x})" |
|
34 sorry |
|
35 |
|
36 termination fv_kind sorry |
|
37 |
|
38 inductive |
|
39 akind :: "kind \<Rightarrow> kind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100) |
|
40 and aty :: "ty \<Rightarrow> ty \<Rightarrow> bool" ("_ \<approx>ty _" [100, 100] 100) |
|
41 and atrm :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<approx>tr _" [100, 100] 100) |
|
42 where |
|
43 a1: "(Type) \<approx>ki (Type)" |
|
44 | a21: "\<lbrakk>A \<approx>ty A'; K \<approx>ki K'\<rbrakk> \<Longrightarrow> (KPi A x K) \<approx>ki (KPi A' x K')" |
|
45 | a22: "\<lbrakk>A \<approx>ty A'; K \<approx>ki ([(x,x')]\<bullet>K'); x \<notin> (fv_ty A'); x \<notin> ((fv_kind K') - {x'})\<rbrakk> |
|
46 \<Longrightarrow> (KPi A x K) \<approx>ki (KPi A' x' K')" |
|
47 | a3: "i = j \<Longrightarrow> (TConst i) \<approx>ty (TConst j)" |
|
48 | a4: "\<lbrakk>A \<approx>ty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (TApp A M) \<approx>ty (TApp A' M')" |
|
49 | a51: "\<lbrakk>A \<approx>ty A'; B \<approx>ty B'\<rbrakk> \<Longrightarrow> (TPi A x B) \<approx>ty (TPi A' x B')" |
|
50 | a52: "\<lbrakk>A \<approx>ty A'; B \<approx>ty ([(x,x')]\<bullet>B'); x \<notin> (fv_ty B'); x \<notin> ((fv_ty B') - {x'})\<rbrakk> |
|
51 \<Longrightarrow> (TPi A x B) \<approx>ty (TPi A' x' B')" |
|
52 | a6: "i = j \<Longrightarrow> (Const i) \<approx>trm (Const j)" |
|
53 | a7: "x = y \<Longrightarrow> (Var x) \<approx>trm (Var y)" |
|
54 | a8: "\<lbrakk>M \<approx>trm M'; N \<approx>tr N'\<rbrakk> \<Longrightarrow> (App M N) \<approx>tr (App M' N')" |
|
55 | a91: "\<lbrakk>A \<approx>ty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (Lam A x M) \<approx>tr (Lam A' x M')" |
|
56 | a92: "\<lbrakk>A \<approx>ty A'; M \<approx>tr ([(x,x')]\<bullet>M'); x \<notin> (fv_ty B'); x \<notin> ((fv_trm M') - {x'})\<rbrakk> |
|
57 \<Longrightarrow> (Lam A x M) \<approx>tr (Lam A' x' M')" |
|
58 |
|
59 lemma al_refl: |
|
60 fixes K::"kind" |
|
61 and A::"ty" |
|
62 and M::"trm" |
|
63 shows "K \<approx>ki K" |
|
64 and "A \<approx>ty A" |
|
65 and "M \<approx>tr M" |
|
66 apply(induct K and A and M rule: kind_ty_trm.inducts) |
|
67 apply(auto intro: akind_aty_atrm.intros) |
|
68 done |
|
69 |
|
70 lemma alpha_EQUIVs: |
|
71 shows "EQUIV akind" |
|
72 and "EQUIV aty" |
|
73 and "EQUIV atrm" |
|
74 sorry |
|
75 |
|
76 quotient KIND = kind / akind |
|
77 by (rule alpha_EQUIVs) |
|
78 |
|
79 quotient TY = ty / aty |
|
80 and TRM = trm / atrm |
|
81 by (auto intro: alpha_EQUIVs) |
|
82 |
|
83 print_quotients |
|
84 |
|
85 quotient_def |
|
86 TYP :: "KIND" |
|
87 where |
|
88 "TYP \<equiv> Type" |
|
89 |
|
90 quotient_def |
|
91 KPI :: "TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND" |
|
92 where |
|
93 "KPI \<equiv> KPi" |
|
94 |
|
95 quotient_def |
|
96 TCONST :: "id \<Rightarrow> TY" |
|
97 where |
|
98 "TCONST \<equiv> TConst" |
|
99 |
|
100 quotient_def |
|
101 TAPP :: "TY \<Rightarrow> TRM \<Rightarrow> TY" |
|
102 where |
|
103 "TAPP \<equiv> TApp" |
|
104 |
|
105 quotient_def |
|
106 TPI :: "TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY" |
|
107 where |
|
108 "TPI \<equiv> TPi" |
|
109 |
|
110 (* FIXME: does not work with CONST *) |
|
111 quotient_def |
|
112 CONS :: "id \<Rightarrow> TRM" |
|
113 where |
|
114 "CONS \<equiv> Const" |
|
115 |
|
116 quotient_def |
|
117 VAR :: "name \<Rightarrow> TRM" |
|
118 where |
|
119 "VAR \<equiv> Var" |
|
120 |
|
121 quotient_def |
|
122 APP :: "TRM \<Rightarrow> TRM \<Rightarrow> TRM" |
|
123 where |
|
124 "APP \<equiv> App" |
|
125 |
|
126 quotient_def |
|
127 LAM :: "TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM" |
|
128 where |
|
129 "LAM \<equiv> Lam" |
|
130 |
|
131 thm TYP_def |
|
132 thm KPI_def |
|
133 thm TCONST_def |
|
134 thm TAPP_def |
|
135 thm TPI_def |
|
136 thm VAR_def |
|
137 thm CONS_def |
|
138 thm APP_def |
|
139 thm LAM_def |
|
140 |
|
141 (* FIXME: print out a warning if the type contains a liftet type, like kind \<Rightarrow> name set *) |
|
142 quotient_def |
|
143 FV_kind :: "KIND \<Rightarrow> name set" |
|
144 where |
|
145 "FV_kind \<equiv> fv_kind" |
|
146 |
|
147 quotient_def |
|
148 FV_ty :: "TY \<Rightarrow> name set" |
|
149 where |
|
150 "FV_ty \<equiv> fv_ty" |
|
151 |
|
152 quotient_def |
|
153 FV_trm :: "TRM \<Rightarrow> name set" |
|
154 where |
|
155 "FV_trm \<equiv> fv_trm" |
|
156 |
|
157 thm FV_kind_def |
|
158 thm FV_ty_def |
|
159 thm FV_trm_def |
|
160 |
|
161 (* FIXME: does not work yet *) |
|
162 (* |
|
163 overloading |
|
164 perm_kind \<equiv> "perm :: 'x prm \<Rightarrow> KIND \<Rightarrow> KIND" (unchecked) |
|
165 perm_ty \<equiv> "perm :: 'x prm \<Rightarrow> TY \<Rightarrow> TY" (unchecked) |
|
166 perm_trm \<equiv> "perm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM" (unchecked) |
|
167 begin |
|
168 |
|
169 quotient_def |
|
170 perm_kind :: "'x prm \<Rightarrow> KIND \<Rightarrow> KIND" |
|
171 where |
|
172 "perm_kind \<equiv> (perm::'x prm \<Rightarrow> KIND \<Rightarrow> KIND)" |
|
173 end |
|
174 *) |
|
175 |