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 |
|
1234
|
138 |
lemmas permute_ktt[simp] = permute_rkind_permute_rty_permute_rtrm.simps[quot_lifted]
|
1083
|
139 |
|
1240
|
140 |
lemma perm_zero_ok: "0 \<bullet> (x :: kind) = x \<and> 0 \<bullet> (y :: ty) = y \<and> 0 \<bullet> (z :: trm) = z"
|
|
141 |
apply (induct rule: kind_ty_trm_induct)
|
1083
|
142 |
apply (simp_all)
|
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
143 |
done
|
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
144 |
|
1082
|
145 |
lemma perm_add_ok:
|
1240
|
146 |
"((p + q) \<bullet> (x1 :: kind) = (p \<bullet> q \<bullet> x1))"
|
|
147 |
"((p + q) \<bullet> (x2 :: ty) = p \<bullet> q \<bullet> x2)"
|
|
148 |
"((p + q) \<bullet> (x3 :: trm) = p \<bullet> q \<bullet> x3)"
|
|
149 |
apply (induct x1 and x2 and x3 rule: kind_ty_trm_inducts)
|
1083
|
150 |
apply (simp_all)
|
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
|
151 |
done
|
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
152 |
|
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
153 |
instance
|
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
154 |
apply default
|
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
155 |
apply (simp_all add: perm_zero_ok perm_add_ok)
|
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
156 |
done
|
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
157 |
|
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
158 |
end
|
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
159 |
|
1240
|
160 |
lemmas ALPHA_kind_ALPHA_ty_ALPHA_trm_inducts = alpha_rkind_alpha_rty_alpha_rtrm.inducts[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
|
161 |
|
1240
|
162 |
lemmas kind_ty_trm_INJECT = 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
|
163 |
|
1236
|
164 |
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
|
165 |
|
1082
|
166 |
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
|
167 |
|
1244
|
168 |
lemma supports:
|
|
169 |
"{} supports TYP"
|
|
170 |
"(supp (atom i)) supports (TCONST i)"
|
|
171 |
"(supp A \<union> supp M) supports (TAPP A M)"
|
|
172 |
"(supp (atom i)) supports (CONS i)"
|
|
173 |
"(supp (atom x)) supports (VAR x)"
|
|
174 |
"(supp M \<union> supp N) supports (APP M N)"
|
|
175 |
"(supp ty \<union> supp (atom na) \<union> supp ki) supports (KPI ty na ki)"
|
|
176 |
"(supp ty \<union> supp (atom na) \<union> supp ty2) supports (TPI ty na ty2)"
|
|
177 |
"(supp ty \<union> supp (atom na) \<union> supp trm) supports (LAM ty na trm)"
|
|
178 |
apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh)
|
|
179 |
apply(rule_tac [!] allI)+
|
|
180 |
apply(rule_tac [!] impI)
|
|
181 |
apply(tactic {* ALLGOALS (REPEAT o etac conjE) *})
|
|
182 |
apply(simp_all add: fresh_atom)
|
|
183 |
done
|
|
184 |
|
|
185 |
lemma kind_ty_trm_fs:
|
|
186 |
"finite (supp (x\<Colon>kind))"
|
|
187 |
"finite (supp (y\<Colon>ty))"
|
|
188 |
"finite (supp (z\<Colon>trm))"
|
|
189 |
apply(induct x and y and z rule: kind_ty_trm_inducts)
|
|
190 |
apply(tactic {* ALLGOALS (rtac @{thm supports_finite} THEN' resolve_tac @{thms supports}) *})
|
|
191 |
apply(simp_all add: supp_atom)
|
|
192 |
done
|
|
193 |
|
|
194 |
instance kind and ty and trm :: fs
|
|
195 |
apply(default)
|
|
196 |
apply(simp_all only: kind_ty_trm_fs)
|
|
197 |
done
|
|
198 |
|
1234
|
199 |
lemma supp_rkind_rty_rtrm_easy:
|
1002
|
200 |
"supp TYP = {}"
|
|
201 |
"supp (TCONST i) = {atom i}"
|
|
202 |
"supp (TAPP A M) = supp A \<union> supp M"
|
|
203 |
"supp (CONS i) = {atom i}"
|
|
204 |
"supp (VAR x) = {atom x}"
|
|
205 |
"supp (APP M N) = supp M \<union> supp N"
|
1239
|
206 |
apply (simp_all add: supp_def permute_ktt)
|
1240
|
207 |
apply (simp_all only: kind_ty_trm_INJECT)
|
1002
|
208 |
apply (simp_all only: supp_at_base[simplified supp_def])
|
|
209 |
apply (simp_all add: Collect_imp_eq Collect_neg_eq)
|
|
210 |
done
|
|
211 |
|
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
|
212 |
lemma supp_fv:
|
1236
|
213 |
"supp t1 = fv_kind t1"
|
|
214 |
"supp t2 = fv_ty t2"
|
|
215 |
"supp t3 = fv_trm t3"
|
1240
|
216 |
apply(induct t1 and t2 and t3 rule: kind_ty_trm_inducts)
|
1234
|
217 |
apply (simp_all add: supp_rkind_rty_rtrm_easy)
|
1236
|
218 |
apply (simp_all add: fv_kind_ty_trm)
|
1234
|
219 |
apply(subgoal_tac "supp (KPI rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)")
|
1244
|
220 |
apply(simp only: supp_Abs)
|
1002
|
221 |
apply(simp (no_asm) add: supp_def)
|
1240
|
222 |
apply(simp add: kind_ty_trm_INJECT)
|
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
223 |
apply(simp add: Abs_eq_iff)
|
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
224 |
apply(simp add: alpha_gen)
|
1045
|
225 |
apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute insert_eqvt empty_eqvt atom_eqvt)
|
|
226 |
apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric])
|
1234
|
227 |
apply(subgoal_tac "supp (TPI rty1 name rty2) = supp rty1 \<union> supp (Abs {atom name} rty2)")
|
1244
|
228 |
apply(simp add: supp_Abs)
|
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
229 |
apply(simp (no_asm) add: supp_def)
|
1240
|
230 |
apply(simp add: kind_ty_trm_INJECT)
|
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
231 |
apply(simp add: Abs_eq_iff)
|
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
232 |
apply(simp add: alpha_gen)
|
1045
|
233 |
apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] insert_eqvt empty_eqvt atom_eqvt)
|
1002
|
234 |
apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)
|
1234
|
235 |
apply(subgoal_tac "supp (LAM rty name rtrm) = supp rty \<union> supp (Abs {atom name} rtrm)")
|
1244
|
236 |
apply(simp add: supp_Abs)
|
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
237 |
apply(simp (no_asm) add: supp_def)
|
1240
|
238 |
apply(simp add: kind_ty_trm_INJECT)
|
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
239 |
apply(simp add: Abs_eq_iff)
|
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
240 |
apply(simp add: alpha_gen)
|
1045
|
241 |
apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] insert_eqvt empty_eqvt atom_eqvt)
|
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
242 |
apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)
|
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
243 |
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
|
244 |
|
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
245 |
(* Not needed anymore *)
|
1244
|
246 |
lemma supp_kpi: "supp (KPI rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)"
|
1240
|
247 |
apply (simp add: permute_set_eq supp_def Abs_eq_iff kind_ty_trm_INJECT)
|
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
248 |
apply (simp add: alpha_gen supp_fv)
|
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
249 |
apply (simp add: Collect_imp_eq Collect_neg_eq add: atom_eqvt Set.Un_commute)
|
997
b7d259ded92e
Ported LF to the generic lambda and solved the simpler _supp cases.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
250 |
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
|
251 |
|
1234
|
252 |
lemma supp_rkind_rty_rtrm:
|
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
|
253 |
"supp TYP = {}"
|
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
254 |
"supp (KPI A x K) = supp A \<union> (supp K - {atom x})"
|
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
255 |
"supp (TCONST i) = {atom i}"
|
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
256 |
"supp (TAPP A M) = supp A \<union> supp M"
|
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
257 |
"supp (TPI A x B) = supp A \<union> (supp B - {atom x})"
|
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
258 |
"supp (CONS i) = {atom i}"
|
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
259 |
"supp (VAR x) = {atom x}"
|
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
260 |
"supp (APP M N) = supp M \<union> supp N"
|
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
261 |
"supp (LAM A x M) = supp A \<union> (supp M - {atom x})"
|
1234
|
262 |
apply (simp_all only: supp_rkind_rty_rtrm_easy)
|
1236
|
263 |
apply (simp_all only: supp_fv fv_kind_ty_trm)
|
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
264 |
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
|
265 |
|
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
266 |
end
|
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
267 |
|
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
268 |
|
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
269 |
|
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
270 |
|