985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
1 |
theory LFex
|
1348
|
2 |
imports "Parser"
|
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 |
|
1454
7c8cd6eae8e2
FV_bn generated for recursive functions as well, and used in main fv for bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
8 |
ML {* val _ = cheat_fv_rsp := false *}
|
7c8cd6eae8e2
FV_bn generated for recursive functions as well, and used in main fv for bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
9 |
ML {* val _ = cheat_const_rsp := false *}
|
7c8cd6eae8e2
FV_bn generated for recursive functions as well, and used in main fv for bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
10 |
ML {* val _ = cheat_equivp := false *}
|
7c8cd6eae8e2
FV_bn generated for recursive functions as well, and used in main fv for bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
11 |
ML {* val _ = cheat_fv_eqvt := false *}
|
7c8cd6eae8e2
FV_bn generated for recursive functions as well, and used in main fv for bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
12 |
ML {* val _ = cheat_alpha_eqvt := false *}
|
1444
|
13 |
|
1348
|
14 |
nominal_datatype kind =
|
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
15 |
Type
|
1348
|
16 |
| KPi "ty" n::"name" k::"kind" bind n in k
|
|
17 |
and ty =
|
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
18 |
TConst "ident"
|
1348
|
19 |
| TApp "ty" "trm"
|
|
20 |
| TPi "ty" n::"name" t::"ty" bind n in t
|
|
21 |
and trm =
|
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
22 |
Const "ident"
|
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
23 |
| Var "name"
|
1348
|
24 |
| App "trm" "trm"
|
|
25 |
| Lam "ty" n::"name" t::"trm" bind n in t
|
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
|
26 |
|
1344
|
27 |
lemma ex_out:
|
|
28 |
"(\<exists>x. Z x \<and> Q) = (Q \<and> (\<exists>x. Z x))"
|
|
29 |
"(\<exists>x. Q \<and> Z x) = (Q \<and> (\<exists>x. Z x))"
|
|
30 |
"(\<exists>x. P x \<and> Q \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))"
|
|
31 |
"(\<exists>x. Q \<and> P x \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))"
|
|
32 |
apply (blast)+
|
|
33 |
done
|
|
34 |
|
1348
|
35 |
lemma Collect_neg_conj: "{x. \<not>(P x \<and> Q x)} = {x. \<not>(P x)} \<union> {x. \<not>(Q x)}"
|
|
36 |
by (simp add: Collect_imp_eq Collect_neg_eq[symmetric])
|
|
37 |
|
1245
|
38 |
lemma supp_eqs:
|
1348
|
39 |
"supp Type = {}"
|
1498
|
40 |
"supp kind = fv_kind kind \<Longrightarrow> supp (KPi ty name kind) = supp ty \<union> supp (Abs {atom name} kind)"
|
1348
|
41 |
"supp (TConst i) = {atom i}"
|
|
42 |
"supp (TApp A M) = supp A \<union> supp M"
|
1498
|
43 |
"supp ty2 = fv_ty ty2 \<Longrightarrow> supp (TPi ty1 name ty2) = supp ty1 \<union> supp (Abs {atom name} ty2)"
|
1348
|
44 |
"supp (Const i) = {atom i}"
|
|
45 |
"supp (Var x) = {atom x}"
|
|
46 |
"supp (App M N) = supp M \<union> supp N"
|
1498
|
47 |
"supp trm = fv_trm trm \<Longrightarrow> supp (Lam ty name trm) = supp ty \<union> supp (Abs {atom name} trm)"
|
1348
|
48 |
apply(simp_all (no_asm) add: supp_def permute_set_eq atom_eqvt kind_ty_trm_perm)
|
1496
fd483d8f486b
Prove pseudo-inject (eq-iff) on the exported level and rename appropriately.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
49 |
apply(simp_all only: kind_ty_trm_eq_iff Abs_eq_iff alpha_gen)
|
1348
|
50 |
apply(simp_all only: ex_out)
|
|
51 |
apply(simp_all only: eqvts[symmetric])
|
|
52 |
apply(simp_all only: Collect_neg_conj)
|
|
53 |
apply(simp_all only: supp_at_base[simplified supp_def] Un_commute Un_assoc)
|
|
54 |
apply(simp_all add: Collect_imp_eq Collect_neg_eq[symmetric] Un_commute Un_assoc)
|
|
55 |
apply(simp_all add: Un_left_commute)
|
1245
|
56 |
done
|
1002
|
57 |
|
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
|
58 |
lemma supp_fv:
|
1348
|
59 |
"supp t1 = fv_kind t1 \<and> supp t2 = fv_ty t2 \<and> supp t3 = fv_trm t3"
|
|
60 |
apply(induct rule: kind_ty_trm_induct)
|
|
61 |
apply(simp_all (no_asm) only: supp_eqs kind_ty_trm_fv)
|
1245
|
62 |
apply(simp_all)
|
1348
|
63 |
apply(simp_all add: supp_eqs)
|
1245
|
64 |
apply(simp_all add: supp_Abs)
|
|
65 |
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
|
66 |
|
1498
|
67 |
lemma supp_kind_ty_trm:
|
1348
|
68 |
"supp Type = {}"
|
|
69 |
"supp (KPi A x K) = supp A \<union> (supp K - {atom x})"
|
|
70 |
"supp (TConst i) = {atom i}"
|
|
71 |
"supp (TApp A M) = supp A \<union> supp M"
|
|
72 |
"supp (TPi A x B) = supp A \<union> (supp B - {atom x})"
|
|
73 |
"supp (Const i) = {atom i}"
|
|
74 |
"supp (Var x) = {atom x}"
|
|
75 |
"supp (App M N) = supp M \<union> supp N"
|
|
76 |
"supp (Lam A x M) = supp A \<union> (supp M - {atom x})"
|
|
77 |
apply (simp_all add: supp_fv kind_ty_trm_fv)
|
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
|
78 |
|
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
79 |
end
|
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
80 |
|
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
81 |
|
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
82 |
|
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
83 |
|