1 theory LFex |
1 theory LFex |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" |
2 imports "Parser" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 atom_decl ident |
6 atom_decl ident |
7 |
7 |
8 datatype rkind = |
8 ML {* restricted_nominal := false *} |
|
9 |
|
10 nominal_datatype kind = |
9 Type |
11 Type |
10 | KPi "rty" "name" "rkind" |
12 | KPi "ty" n::"name" k::"kind" bind n in k |
11 and rty = |
13 and ty = |
12 TConst "ident" |
14 TConst "ident" |
13 | TApp "rty" "rtrm" |
15 | TApp "ty" "trm" |
14 | TPi "rty" "name" "rty" |
16 | TPi "ty" n::"name" t::"ty" bind n in t |
15 and rtrm = |
17 and trm = |
16 Const "ident" |
18 Const "ident" |
17 | Var "name" |
19 | Var "name" |
18 | App "rtrm" "rtrm" |
20 | App "trm" "trm" |
19 | Lam "rty" "name" "rtrm" |
21 | Lam "ty" n::"name" t::"trm" bind n in t |
20 |
|
21 |
|
22 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "LFex.rkind") 3 *} |
|
23 print_theorems |
|
24 |
|
25 local_setup {* |
|
26 snd o define_fv_alpha (Datatype.the_info @{theory} "LFex.rkind") |
|
27 [[ [], [(NONE, 1, 2)]], |
|
28 [ [], [], [(NONE, 1, 2)] ], |
|
29 [ [], [], [], [(NONE, 1, 2)]]] *} |
|
30 notation |
|
31 alpha_rkind ("_ \<approx>ki _" [100, 100] 100) |
|
32 and alpha_rty ("_ \<approx>ty _" [100, 100] 100) |
|
33 and alpha_rtrm ("_ \<approx>tr _" [100, 100] 100) |
|
34 thm fv_rkind_fv_rty_fv_rtrm.simps alpha_rkind_alpha_rty_alpha_rtrm.intros |
|
35 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)) *} |
|
36 thm alpha_rkind_alpha_rty_alpha_rtrm_inj |
|
37 |
|
38 lemma rfv_eqvt[eqvt]: |
|
39 "((pi\<bullet>fv_rkind t1) = fv_rkind (pi\<bullet>t1))" |
|
40 "((pi\<bullet>fv_rty t2) = fv_rty (pi\<bullet>t2))" |
|
41 "((pi\<bullet>fv_rtrm t3) = fv_rtrm (pi\<bullet>t3))" |
|
42 apply(induct t1 and t2 and t3 rule: rkind_rty_rtrm.inducts) |
|
43 apply(simp_all add: union_eqvt Diff_eqvt) |
|
44 apply(simp_all add: permute_set_eq atom_eqvt) |
|
45 done |
|
46 |
|
47 lemma alpha_eqvt: |
|
48 "(t1 \<approx>ki s1 \<longrightarrow> (p \<bullet> t1) \<approx>ki (p \<bullet> s1)) \<and> |
|
49 (t2 \<approx>ty s2 \<longrightarrow> (p \<bullet> t2) \<approx>ty (p \<bullet> s2)) \<and> |
|
50 (t3 \<approx>tr s3 \<longrightarrow> (p \<bullet> t3) \<approx>tr (p \<bullet> s3))" |
|
51 apply(rule alpha_rkind_alpha_rty_alpha_rtrm.induct) |
|
52 apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm_inj) |
|
53 apply (erule alpha_gen_compose_eqvt) |
|
54 apply (simp_all add: rfv_eqvt eqvts atom_eqvt) |
|
55 apply (erule alpha_gen_compose_eqvt) |
|
56 apply (simp_all add: rfv_eqvt eqvts atom_eqvt) |
|
57 apply (erule alpha_gen_compose_eqvt) |
|
58 apply (simp_all add: rfv_eqvt eqvts atom_eqvt) |
|
59 done |
|
60 |
|
61 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_equivps}, []), |
|
62 (build_equivps [@{term alpha_rkind}, @{term alpha_rty}, @{term alpha_rtrm}] |
|
63 @{thm rkind_rty_rtrm.induct} @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} |
|
64 @{thms rkind.inject rty.inject rtrm.inject} @{thms alpha_rkind_alpha_rty_alpha_rtrm_inj} |
|
65 @{thms rkind.distinct rty.distinct rtrm.distinct} |
|
66 @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases} |
|
67 @{thms alpha_eqvt} ctxt)) ctxt)) *} |
|
68 thm alpha_equivps |
|
69 |
|
70 local_setup {* define_quotient_type |
|
71 [(([], @{binding kind}, NoSyn), (@{typ rkind}, @{term alpha_rkind})), |
|
72 (([], @{binding ty}, NoSyn), (@{typ rty}, @{term alpha_rty} )), |
|
73 (([], @{binding trm}, NoSyn), (@{typ rtrm}, @{term alpha_rtrm} ))] |
|
74 (ALLGOALS (resolve_tac @{thms alpha_equivps})) |
|
75 *} |
|
76 |
|
77 local_setup {* |
|
78 (fn ctxt => ctxt |
|
79 |> snd o (Quotient_Def.quotient_lift_const ("TYP", @{term Type})) |
|
80 |> snd o (Quotient_Def.quotient_lift_const ("KPI", @{term KPi})) |
|
81 |> snd o (Quotient_Def.quotient_lift_const ("TCONST", @{term TConst})) |
|
82 |> snd o (Quotient_Def.quotient_lift_const ("TAPP", @{term TApp})) |
|
83 |> snd o (Quotient_Def.quotient_lift_const ("TPI", @{term TPi})) |
|
84 |> snd o (Quotient_Def.quotient_lift_const ("CONS", @{term Const})) |
|
85 |> snd o (Quotient_Def.quotient_lift_const ("VAR", @{term Var})) |
|
86 |> snd o (Quotient_Def.quotient_lift_const ("APP", @{term App})) |
|
87 |> snd o (Quotient_Def.quotient_lift_const ("LAM", @{term Lam})) |
|
88 |> snd o (Quotient_Def.quotient_lift_const ("fv_kind", @{term fv_rkind})) |
|
89 |> snd o (Quotient_Def.quotient_lift_const ("fv_ty", @{term fv_rty})) |
|
90 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm", @{term fv_rtrm}))) *} |
|
91 print_theorems |
|
92 |
|
93 local_setup {* snd o prove_const_rsp @{binding rfv_rsp} [@{term fv_rkind}, @{term fv_rty}, @{term fv_rtrm}] |
|
94 (fn _ => fvbv_rsp_tac @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} @{thms fv_rkind_fv_rty_fv_rtrm.simps} 1) *} |
|
95 local_setup {* snd o prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind"}, @{term "permute :: perm \<Rightarrow> rty \<Rightarrow> rty"}, @{term "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm"}] |
|
96 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *} |
|
97 ML {* fun const_rsp_tac _ = constr_rsp_tac @{thms alpha_rkind_alpha_rty_alpha_rtrm_inj} |
|
98 @{thms rfv_rsp} @{thms alpha_equivps} 1 *} |
|
99 local_setup {* snd o prove_const_rsp Binding.empty [@{term TConst}] const_rsp_tac *} |
|
100 local_setup {* snd o prove_const_rsp Binding.empty [@{term TApp}] const_rsp_tac *} |
|
101 local_setup {* snd o prove_const_rsp Binding.empty [@{term Var}] const_rsp_tac *} |
|
102 local_setup {* snd o prove_const_rsp Binding.empty [@{term App}] const_rsp_tac *} |
|
103 local_setup {* snd o prove_const_rsp Binding.empty [@{term Const}] const_rsp_tac *} |
|
104 local_setup {* snd o prove_const_rsp Binding.empty [@{term KPi}] const_rsp_tac *} |
|
105 local_setup {* snd o prove_const_rsp Binding.empty [@{term TPi}] const_rsp_tac *} |
|
106 local_setup {* snd o prove_const_rsp Binding.empty [@{term Lam}] const_rsp_tac *} |
|
107 |
|
108 lemmas kind_ty_trm_induct = rkind_rty_rtrm.induct[quot_lifted] |
|
109 |
|
110 thm rkind_rty_rtrm.inducts |
|
111 lemmas kind_ty_trm_inducts = rkind_rty_rtrm.inducts[quot_lifted] |
|
112 |
|
113 setup {* define_lifted_perms ["LFex.kind", "LFex.ty", "LFex.trm"] |
|
114 [("permute_kind", @{term "permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind"}), |
|
115 ("permute_ty", @{term "permute :: perm \<Rightarrow> rty \<Rightarrow> rty"}), |
|
116 ("permute_trm", @{term "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm"})] |
|
117 @{thms permute_rkind_permute_rty_permute_rtrm_zero permute_rkind_permute_rty_permute_rtrm_append} *} |
|
118 |
|
119 (* |
|
120 Lifts, but slow and not needed?. |
|
121 lemmas alpha_kind_alpha_ty_alpha_trm_induct = alpha_rkind_alpha_rty_alpha_rtrm.induct[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
|
122 *) |
|
123 |
|
124 lemmas permute_ktt[simp] = permute_rkind_permute_rty_permute_rtrm.simps[quot_lifted] |
|
125 |
|
126 lemmas kind_ty_trm_inj = alpha_rkind_alpha_rty_alpha_rtrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
|
127 |
|
128 lemmas fv_kind_ty_trm = fv_rkind_fv_rty_fv_rtrm.simps[quot_lifted] |
|
129 |
|
130 lemmas fv_eqvt = rfv_eqvt[quot_lifted] |
|
131 |
22 |
132 lemma supports: |
23 lemma supports: |
133 "{} supports TYP" |
24 "{} supports Type" |
134 "(supp (atom i)) supports (TCONST i)" |
25 "(supp (atom i)) supports (TConst i)" |
135 "(supp A \<union> supp M) supports (TAPP A M)" |
26 "(supp A \<union> supp M) supports (TApp A M)" |
136 "(supp (atom i)) supports (CONS i)" |
27 "(supp (atom i)) supports (Const i)" |
137 "(supp (atom x)) supports (VAR x)" |
28 "(supp (atom x)) supports (Var x)" |
138 "(supp M \<union> supp N) supports (APP M N)" |
29 "(supp M \<union> supp N) supports (App M N)" |
139 "(supp ty \<union> supp (atom na) \<union> supp ki) supports (KPI ty na ki)" |
30 "(supp ty \<union> supp (atom na) \<union> supp ki) supports (KPi ty na ki)" |
140 "(supp ty \<union> supp (atom na) \<union> supp ty2) supports (TPI ty na ty2)" |
31 "(supp ty \<union> supp (atom na) \<union> supp ty2) supports (TPi ty na ty2)" |
141 "(supp ty \<union> supp (atom na) \<union> supp trm) supports (LAM ty na trm)" |
32 "(supp ty \<union> supp (atom na) \<union> supp trm) supports (Lam ty na trm)" |
142 apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh) |
33 apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh kind_ty_trm_perm) |
143 apply(rule_tac [!] allI)+ |
34 apply(rule_tac [!] allI)+ |
144 apply(rule_tac [!] impI) |
35 apply(rule_tac [!] impI) |
145 apply(tactic {* ALLGOALS (REPEAT o etac conjE) *}) |
36 apply(tactic {* ALLGOALS (REPEAT o etac conjE) *}) |
146 apply(simp_all add: fresh_atom) |
37 apply(simp_all add: fresh_atom) |
147 done |
38 done |
148 |
39 |
149 lemma kind_ty_trm_fs: |
40 lemma kind_ty_trm_fs: |
150 "finite (supp (x\<Colon>kind))" |
41 "finite (supp (x\<Colon>kind)) \<and> finite (supp (y\<Colon>ty)) \<and> finite (supp (z\<Colon>trm))" |
151 "finite (supp (y\<Colon>ty))" |
42 apply(induct rule: kind_ty_trm_induct) |
152 "finite (supp (z\<Colon>trm))" |
|
153 apply(induct x and y and z rule: kind_ty_trm_inducts) |
|
154 apply(tactic {* ALLGOALS (rtac @{thm supports_finite} THEN' resolve_tac @{thms supports}) *}) |
43 apply(tactic {* ALLGOALS (rtac @{thm supports_finite} THEN' resolve_tac @{thms supports}) *}) |
155 apply(simp_all add: supp_atom) |
44 apply(simp_all add: supp_atom) |
156 done |
45 done |
157 |
46 |
158 instance kind and ty and trm :: fs |
47 instance kind and ty and trm :: fs |
159 apply(default) |
48 apply(default) |
160 apply(simp_all only: kind_ty_trm_fs) |
49 apply(simp_all only: kind_ty_trm_fs) |
161 done |
50 done |
162 |
51 |
|
52 lemma ex_out: |
|
53 "(\<exists>x. Z x \<and> Q) = (Q \<and> (\<exists>x. Z x))" |
|
54 "(\<exists>x. Q \<and> Z x) = (Q \<and> (\<exists>x. Z x))" |
|
55 "(\<exists>x. P x \<and> Q \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))" |
|
56 "(\<exists>x. Q \<and> P x \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))" |
|
57 apply (blast)+ |
|
58 done |
|
59 |
|
60 lemma Collect_neg_conj: "{x. \<not>(P x \<and> Q x)} = {x. \<not>(P x)} \<union> {x. \<not>(Q x)}" |
|
61 by (simp add: Collect_imp_eq Collect_neg_eq[symmetric]) |
|
62 |
163 lemma supp_eqs: |
63 lemma supp_eqs: |
164 "supp TYP = {}" |
64 "supp Type = {}" |
165 "supp rkind = fv_kind rkind \<Longrightarrow> supp (KPI rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)" |
65 "supp rkind = fv_kind rkind \<Longrightarrow> supp (KPi rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)" |
166 "supp (TCONST i) = {atom i}" |
66 "supp (TConst i) = {atom i}" |
167 "supp (TAPP A M) = supp A \<union> supp M" |
67 "supp (TApp A M) = supp A \<union> supp M" |
168 "supp rty2 = fv_ty rty2 \<Longrightarrow> supp (TPI rty1 name rty2) = supp rty1 \<union> supp (Abs {atom name} rty2)" |
68 "supp rty2 = fv_ty rty2 \<Longrightarrow> supp (TPi rty1 name rty2) = supp rty1 \<union> supp (Abs {atom name} rty2)" |
169 "supp (CONS i) = {atom i}" |
69 "supp (Const i) = {atom i}" |
170 "supp (VAR x) = {atom x}" |
70 "supp (Var x) = {atom x}" |
171 "supp (APP M N) = supp M \<union> supp N" |
71 "supp (App M N) = supp M \<union> supp N" |
172 "supp rtrm = fv_trm rtrm \<Longrightarrow> supp (LAM rty name rtrm) = supp rty \<union> supp (Abs {atom name} rtrm)" |
72 "supp rtrm = fv_trm rtrm \<Longrightarrow> supp (Lam rty name rtrm) = supp rty \<union> supp (Abs {atom name} rtrm)" |
173 apply(simp_all (no_asm) add: supp_def) |
73 apply(simp_all (no_asm) add: supp_def permute_set_eq atom_eqvt kind_ty_trm_perm) |
174 apply(simp_all only: kind_ty_trm_inj Abs_eq_iff alpha_gen) |
74 apply(simp_all only: kind_ty_trm_inject Abs_eq_iff alpha_gen) |
175 apply(simp_all only: insert_eqvt empty_eqvt atom_eqvt supp_eqvt[symmetric] fv_eqvt[symmetric]) |
75 apply(simp_all only: ex_out) |
176 apply(simp_all add: Collect_imp_eq Collect_neg_eq[symmetric] Set.Un_commute) |
76 apply(simp_all only: eqvts[symmetric]) |
177 apply(simp_all add: supp_at_base[simplified supp_def]) |
77 apply(simp_all only: Collect_neg_conj) |
|
78 apply(simp_all only: supp_at_base[simplified supp_def] Un_commute Un_assoc) |
|
79 apply(simp_all add: Collect_imp_eq Collect_neg_eq[symmetric] Un_commute Un_assoc) |
|
80 apply(simp_all add: Un_left_commute) |
178 done |
81 done |
179 |
82 |
180 lemma supp_fv: |
83 lemma supp_fv: |
181 "supp t1 = fv_kind t1" |
84 "supp t1 = fv_kind t1 \<and> supp t2 = fv_ty t2 \<and> supp t3 = fv_trm t3" |
182 "supp t2 = fv_ty t2" |
85 apply(induct rule: kind_ty_trm_induct) |
183 "supp t3 = fv_trm t3" |
86 apply(simp_all (no_asm) only: supp_eqs kind_ty_trm_fv) |
184 apply(induct t1 and t2 and t3 rule: kind_ty_trm_inducts) |
|
185 apply(simp_all (no_asm) only: supp_eqs fv_kind_ty_trm) |
|
186 apply(simp_all) |
87 apply(simp_all) |
187 apply(subst supp_eqs) |
88 apply(simp_all add: supp_eqs) |
188 apply(simp_all add: supp_Abs) |
|
189 apply(subst supp_eqs) |
|
190 apply(simp_all add: supp_Abs) |
|
191 apply(subst supp_eqs) |
|
192 apply(simp_all add: supp_Abs) |
89 apply(simp_all add: supp_Abs) |
193 done |
90 done |
194 |
91 |
195 lemma supp_rkind_rty_rtrm: |
92 lemma supp_rkind_rty_rtrm: |
196 "supp TYP = {}" |
93 "supp Type = {}" |
197 "supp (KPI A x K) = supp A \<union> (supp K - {atom x})" |
94 "supp (KPi A x K) = supp A \<union> (supp K - {atom x})" |
198 "supp (TCONST i) = {atom i}" |
95 "supp (TConst i) = {atom i}" |
199 "supp (TAPP A M) = supp A \<union> supp M" |
96 "supp (TApp A M) = supp A \<union> supp M" |
200 "supp (TPI A x B) = supp A \<union> (supp B - {atom x})" |
97 "supp (TPi A x B) = supp A \<union> (supp B - {atom x})" |
201 "supp (CONS i) = {atom i}" |
98 "supp (Const i) = {atom i}" |
202 "supp (VAR x) = {atom x}" |
99 "supp (Var x) = {atom x}" |
203 "supp (APP M N) = supp M \<union> supp N" |
100 "supp (App M N) = supp M \<union> supp N" |
204 "supp (LAM A x M) = supp A \<union> (supp M - {atom x})" |
101 "supp (Lam A x M) = supp A \<union> (supp M - {atom x})" |
205 by (simp_all only: supp_fv fv_kind_ty_trm) |
102 apply (simp_all add: supp_fv kind_ty_trm_fv) |
206 |
103 |
207 end |
104 end |
208 |
105 |
209 |
106 |
210 |
107 |