985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
1 |
theory LFex
|
1241
|
2 |
imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp"
|
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
3 |
begin
|
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
4 |
|
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
5 |
atom_decl name
|
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
6 |
atom_decl ident
|
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
7 |
|
1234
|
8 |
datatype rkind =
|
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
9 |
Type
|
1234
|
10 |
| KPi "rty" "name" "rkind"
|
|
11 |
and rty =
|
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
12 |
TConst "ident"
|
1234
|
13 |
| TApp "rty" "rtrm"
|
|
14 |
| TPi "rty" "name" "rty"
|
|
15 |
and rtrm =
|
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
16 |
Const "ident"
|
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
17 |
| Var "name"
|
1234
|
18 |
| App "rtrm" "rtrm"
|
|
19 |
| Lam "rty" "name" "rtrm"
|
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
20 |
|
1234
|
21 |
|
1239
|
22 |
setup {* snd o define_raw_perms ["rkind", "rty", "rtrm"] ["LFex.rkind", "LFex.rty", "LFex.rtrm"] *}
|
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
23 |
|
1219
|
24 |
local_setup {*
|
1234
|
25 |
snd o define_fv_alpha "LFex.rkind"
|
1219
|
26 |
[[ [], [[], [(NONE, 1)], [(NONE, 1)]] ],
|
|
27 |
[ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ],
|
|
28 |
[ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]] *}
|
|
29 |
notation
|
1234
|
30 |
alpha_rkind ("_ \<approx>ki _" [100, 100] 100)
|
1237
|
31 |
and alpha_rty ("_ \<approx>ty _" [100, 100] 100)
|
1234
|
32 |
and alpha_rtrm ("_ \<approx>tr _" [100, 100] 100)
|
|
33 |
thm fv_rkind_fv_rty_fv_rtrm.simps alpha_rkind_alpha_rty_alpha_rtrm.intros
|
1238
|
34 |
local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_rkind_alpha_rty_alpha_rtrm_inj}, []), (build_alpha_inj @{thms alpha_rkind_alpha_rty_alpha_rtrm.intros} @{thms rkind.distinct rty.distinct rtrm.distinct rkind.inject rty.inject rtrm.inject} @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases} ctxt)) ctxt)) *}
|
|
35 |
thm alpha_rkind_alpha_rty_alpha_rtrm_inj
|
1219
|
36 |
|
992
|
37 |
lemma rfv_eqvt[eqvt]:
|
1236
|
38 |
"((pi\<bullet>fv_rkind t1) = fv_rkind (pi\<bullet>t1))"
|
|
39 |
"((pi\<bullet>fv_rty t2) = fv_rty (pi\<bullet>t2))"
|
|
40 |
"((pi\<bullet>fv_rtrm t3) = fv_rtrm (pi\<bullet>t3))"
|
1234
|
41 |
apply(induct t1 and t2 and t3 rule: rkind_rty_rtrm.inducts)
|
1239
|
42 |
apply(simp_all add: union_eqvt Diff_eqvt)
|
993
|
43 |
apply(simp_all add: permute_set_eq atom_eqvt)
|
992
|
44 |
done
|
|
45 |
|
|
46 |
lemma alpha_eqvt:
|
|
47 |
"t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)"
|
1237
|
48 |
"t2 \<approx>ty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>ty (pi \<bullet> s2)"
|
992
|
49 |
"t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> s3)"
|
1237
|
50 |
apply(induct rule: alpha_rkind_alpha_rty_alpha_rtrm.inducts)
|
|
51 |
apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
|
|
52 |
apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm_inj)
|
1027
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
53 |
apply (rule alpha_gen_atom_eqvt)
|
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
54 |
apply (simp add: rfv_eqvt)
|
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
55 |
apply assumption
|
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
56 |
apply (rule alpha_gen_atom_eqvt)
|
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
57 |
apply (simp add: rfv_eqvt)
|
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
58 |
apply assumption
|
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
59 |
apply (rule alpha_gen_atom_eqvt)
|
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
60 |
apply (simp add: rfv_eqvt)
|
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
61 |
apply assumption
|
992
|
62 |
done
|
|
63 |
|
1239
|
64 |
local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_equivps}, []),
|
|
65 |
(build_equivps [@{term alpha_rkind}, @{term alpha_rty}, @{term alpha_rtrm}]
|
|
66 |
@{thm rkind_rty_rtrm.induct} @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct}
|
|
67 |
@{thms rkind.inject rty.inject rtrm.inject} @{thms alpha_rkind_alpha_rty_alpha_rtrm_inj}
|
|
68 |
@{thms rkind.distinct rty.distinct rtrm.distinct}
|
|
69 |
@{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases}
|
|
70 |
@{thms alpha_eqvt} ctxt)) ctxt)) *}
|
|
71 |
thm alpha_equivps
|
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
72 |
|
1241
|
73 |
local_setup {* define_quotient_type
|
|
74 |
[(([], @{binding kind}, NoSyn), (@{typ rkind}, @{term alpha_rkind})),
|
|
75 |
(([], @{binding ty}, NoSyn), (@{typ rty}, @{term alpha_rty} )),
|
|
76 |
(([], @{binding trm}, NoSyn), (@{typ rtrm}, @{term alpha_rtrm} ))]
|
|
77 |
(ALLGOALS (resolve_tac @{thms alpha_equivps}))
|
|
78 |
*}
|
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
79 |
|
1241
|
80 |
local_setup {*
|
|
81 |
(fn ctxt => ctxt
|
|
82 |
|> snd o (Quotient_Def.quotient_lift_const ("TYP", @{term Type}))
|
|
83 |
|> snd o (Quotient_Def.quotient_lift_const ("KPI", @{term KPi}))
|
|
84 |
|> snd o (Quotient_Def.quotient_lift_const ("TCONST", @{term TConst}))
|
|
85 |
|> snd o (Quotient_Def.quotient_lift_const ("TAPP", @{term TApp}))
|
|
86 |
|> snd o (Quotient_Def.quotient_lift_const ("TPI", @{term TPi}))
|
|
87 |
|> snd o (Quotient_Def.quotient_lift_const ("CONS", @{term Const}))
|
|
88 |
|> snd o (Quotient_Def.quotient_lift_const ("VAR", @{term Var}))
|
|
89 |
|> snd o (Quotient_Def.quotient_lift_const ("APP", @{term App}))
|
|
90 |
|> snd o (Quotient_Def.quotient_lift_const ("LAM", @{term Lam}))
|
|
91 |
|> snd o (Quotient_Def.quotient_lift_const ("fv_kind", @{term fv_rkind}))
|
|
92 |
|> snd o (Quotient_Def.quotient_lift_const ("fv_ty", @{term fv_rty}))
|
|
93 |
|> snd o (Quotient_Def.quotient_lift_const ("fv_trm", @{term fv_rtrm}))) *}
|
|
94 |
print_theorems
|
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
95 |
|
1242
|
96 |
local_setup {* prove_const_rsp @{binding rfv_rsp} [@{term fv_rkind}, @{term fv_rty}, @{term fv_rtrm}]
|
|
97 |
(fn _ => fvbv_rsp_tac @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} @{thms fv_rkind_fv_rty_fv_rtrm.simps} 1) *}
|
1243
|
98 |
local_setup {* prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind"}]
|
|
99 |
(fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *}
|
|
100 |
local_setup {* prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rty \<Rightarrow> rty"}]
|
|
101 |
(fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *}
|
|
102 |
local_setup {* prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm"}]
|
|
103 |
(fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *}
|
|
104 |
ML {* fun const_rsp_tac _ = constr_rsp_tac @{thms alpha_rkind_alpha_rty_alpha_rtrm_inj}
|
|
105 |
@{thms rfv_rsp} @{thms alpha_equivps} 1 *}
|
|
106 |
local_setup {* prove_const_rsp Binding.empty [@{term TConst}] const_rsp_tac *}
|
|
107 |
local_setup {* prove_const_rsp Binding.empty [@{term TApp}] const_rsp_tac *}
|
|
108 |
local_setup {* prove_const_rsp Binding.empty [@{term Var}] const_rsp_tac *}
|
|
109 |
local_setup {* prove_const_rsp Binding.empty [@{term App}] const_rsp_tac *}
|
|
110 |
local_setup {* prove_const_rsp Binding.empty [@{term Const}] const_rsp_tac *}
|
|
111 |
local_setup {* prove_const_rsp Binding.empty [@{term KPi}] const_rsp_tac *}
|
|
112 |
local_setup {* prove_const_rsp Binding.empty [@{term TPi}] const_rsp_tac *}
|
|
113 |
local_setup {* prove_const_rsp Binding.empty [@{term Lam}] const_rsp_tac *}
|
992
|
114 |
|
1240
|
115 |
lemmas kind_ty_trm_induct = rkind_rty_rtrm.induct[quot_lifted]
|
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
116 |
|
1234
|
117 |
thm rkind_rty_rtrm.inducts
|
1240
|
118 |
lemmas kind_ty_trm_inducts = rkind_rty_rtrm.inducts[quot_lifted]
|
994
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
119 |
|
1240
|
120 |
instantiation kind and ty and trm :: pt
|
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
121 |
begin
|
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
122 |
|
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
123 |
quotient_definition
|
1240
|
124 |
"permute_kind :: perm \<Rightarrow> kind \<Rightarrow> kind"
|
1139
|
125 |
is
|
1234
|
126 |
"permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind"
|
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
127 |
|
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
128 |
quotient_definition
|
1240
|
129 |
"permute_ty :: perm \<Rightarrow> ty \<Rightarrow> ty"
|
1139
|
130 |
is
|
1234
|
131 |
"permute :: perm \<Rightarrow> rty \<Rightarrow> rty"
|
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
132 |
|
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
133 |
quotient_definition
|
1240
|
134 |
"permute_trm :: perm \<Rightarrow> trm \<Rightarrow> trm"
|
1139
|
135 |
is
|
1234
|
136 |
"permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm"
|
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
137 |
|
1250
|
138 |
instance by default (simp_all add:
|
|
139 |
permute_rkind_permute_rty_permute_rtrm_zero[quot_lifted]
|
|
140 |
permute_rkind_permute_rty_permute_rtrm_append[quot_lifted])
|
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
141 |
|
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
142 |
end
|
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
143 |
|
1246
|
144 |
(*
|
|
145 |
Lifts, but slow and not needed?.
|
|
146 |
lemmas alpha_kind_alpha_ty_alpha_trm_induct = alpha_rkind_alpha_rty_alpha_rtrm.induct[unfolded alpha_gen, quot_lifted, folded alpha_gen]
|
|
147 |
*)
|
994
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
148 |
|
1250
|
149 |
lemmas permute_ktt[simp] = permute_rkind_permute_rty_permute_rtrm.simps[quot_lifted]
|
|
150 |
|
1246
|
151 |
lemmas kind_ty_trm_inj = alpha_rkind_alpha_rty_alpha_rtrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
|
994
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
152 |
|
1236
|
153 |
lemmas fv_kind_ty_trm = fv_rkind_fv_rty_fv_rtrm.simps[quot_lifted]
|
994
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
154 |
|
1082
|
155 |
lemmas fv_eqvt = rfv_eqvt[quot_lifted]
|
994
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
156 |
|
1244
|
157 |
lemma supports:
|
|
158 |
"{} supports TYP"
|
|
159 |
"(supp (atom i)) supports (TCONST i)"
|
|
160 |
"(supp A \<union> supp M) supports (TAPP A M)"
|
|
161 |
"(supp (atom i)) supports (CONS i)"
|
|
162 |
"(supp (atom x)) supports (VAR x)"
|
|
163 |
"(supp M \<union> supp N) supports (APP M N)"
|
|
164 |
"(supp ty \<union> supp (atom na) \<union> supp ki) supports (KPI ty na ki)"
|
|
165 |
"(supp ty \<union> supp (atom na) \<union> supp ty2) supports (TPI ty na ty2)"
|
|
166 |
"(supp ty \<union> supp (atom na) \<union> supp trm) supports (LAM ty na trm)"
|
|
167 |
apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh)
|
|
168 |
apply(rule_tac [!] allI)+
|
|
169 |
apply(rule_tac [!] impI)
|
|
170 |
apply(tactic {* ALLGOALS (REPEAT o etac conjE) *})
|
|
171 |
apply(simp_all add: fresh_atom)
|
|
172 |
done
|
|
173 |
|
|
174 |
lemma kind_ty_trm_fs:
|
|
175 |
"finite (supp (x\<Colon>kind))"
|
|
176 |
"finite (supp (y\<Colon>ty))"
|
|
177 |
"finite (supp (z\<Colon>trm))"
|
|
178 |
apply(induct x and y and z rule: kind_ty_trm_inducts)
|
|
179 |
apply(tactic {* ALLGOALS (rtac @{thm supports_finite} THEN' resolve_tac @{thms supports}) *})
|
|
180 |
apply(simp_all add: supp_atom)
|
|
181 |
done
|
|
182 |
|
|
183 |
instance kind and ty and trm :: fs
|
|
184 |
apply(default)
|
|
185 |
apply(simp_all only: kind_ty_trm_fs)
|
|
186 |
done
|
|
187 |
|
1245
|
188 |
lemma supp_eqs:
|
|
189 |
"supp TYP = {}"
|
|
190 |
"supp rkind = fv_kind rkind \<Longrightarrow> supp (KPI rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)"
|
|
191 |
"supp (TCONST i) = {atom i}"
|
|
192 |
"supp (TAPP A M) = supp A \<union> supp M"
|
|
193 |
"supp rty2 = fv_ty rty2 \<Longrightarrow> supp (TPI rty1 name rty2) = supp rty1 \<union> supp (Abs {atom name} rty2)"
|
|
194 |
"supp (CONS i) = {atom i}"
|
|
195 |
"supp (VAR x) = {atom x}"
|
|
196 |
"supp (APP M N) = supp M \<union> supp N"
|
|
197 |
"supp rtrm = fv_trm rtrm \<Longrightarrow> supp (LAM rty name rtrm) = supp rty \<union> supp (Abs {atom name} rtrm)"
|
|
198 |
apply(simp_all (no_asm) add: supp_def)
|
1246
|
199 |
apply(simp_all only: kind_ty_trm_inj Abs_eq_iff alpha_gen)
|
1245
|
200 |
apply(simp_all only: insert_eqvt empty_eqvt atom_eqvt supp_eqvt[symmetric] fv_eqvt[symmetric])
|
|
201 |
apply(simp_all add: Collect_imp_eq Collect_neg_eq[symmetric] Set.Un_commute)
|
|
202 |
apply(simp_all add: supp_at_base[simplified supp_def])
|
|
203 |
done
|
1002
|
204 |
|
994
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
205 |
lemma supp_fv:
|
1245
|
206 |
"supp t1 = fv_kind t1"
|
|
207 |
"supp t2 = fv_ty t2"
|
|
208 |
"supp t3 = fv_trm t3"
|
|
209 |
apply(induct t1 and t2 and t3 rule: kind_ty_trm_inducts)
|
|
210 |
apply(simp_all (no_asm) only: supp_eqs fv_kind_ty_trm)
|
|
211 |
apply(simp_all)
|
|
212 |
apply(subst supp_eqs)
|
|
213 |
apply(simp_all add: supp_Abs)
|
|
214 |
apply(subst supp_eqs)
|
|
215 |
apply(simp_all add: supp_Abs)
|
|
216 |
apply(subst supp_eqs)
|
|
217 |
apply(simp_all add: supp_Abs)
|
|
218 |
done
|
994
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
219 |
|
1234
|
220 |
lemma supp_rkind_rty_rtrm:
|
1245
|
221 |
"supp TYP = {}"
|
|
222 |
"supp (KPI A x K) = supp A \<union> (supp K - {atom x})"
|
|
223 |
"supp (TCONST i) = {atom i}"
|
|
224 |
"supp (TAPP A M) = supp A \<union> supp M"
|
|
225 |
"supp (TPI A x B) = supp A \<union> (supp B - {atom x})"
|
|
226 |
"supp (CONS i) = {atom i}"
|
|
227 |
"supp (VAR x) = {atom x}"
|
|
228 |
"supp (APP M N) = supp M \<union> supp N"
|
|
229 |
"supp (LAM A x M) = supp A \<union> (supp M - {atom x})"
|
|
230 |
by (simp_all only: supp_fv fv_kind_ty_trm)
|
994
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
231 |
|
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
232 |
end
|
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
233 |
|
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
234 |
|
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
235 |
|
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
236 |
|