57 and assoc_lst = |
57 and assoc_lst = |
58 ANil |
58 ANil |
59 | ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t |
59 | ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t |
60 and pat = |
60 and pat = |
61 K "char" "tvtk_lst" "tvck_lst" "vt_lst" |
61 K "char" "tvtk_lst" "tvck_lst" "vt_lst" |
|
62 and vt_lst = |
|
63 VTNil |
|
64 | VTCons "var" "ty" "vt_lst" |
62 and tvtk_lst = |
65 and tvtk_lst = |
63 TVTKNil |
66 TVTKNil |
64 | TVTKCons "tvar" "tkind" "tvtk_lst" |
67 | TVTKCons "tvar" "tkind" "tvtk_lst" |
65 and tvck_lst = |
68 and tvck_lst = |
66 TVCKNil |
69 TVCKNil |
67 | TVCKCons "tvar" "ckind" "tvck_lst" |
70 | TVCKCons "tvar" "ckind" "tvck_lst" |
68 and vt_lst = |
|
69 VTNil |
|
70 | VTCons "var" "ty" "vt_lst" |
|
71 binder |
71 binder |
72 bv :: "pat \<Rightarrow> atom set" |
72 bv :: "pat \<Rightarrow> atom set" |
73 (*and bv_vt :: "vt_lst \<Rightarrow> atom set" |
73 and bv_vt :: "vt_lst \<Rightarrow> atom set" |
74 and bv_tvtk :: "tvtk_lst \<Rightarrow> atom set" |
74 and bv_tvtk :: "tvtk_lst \<Rightarrow> atom set" |
75 and bv_tvck :: "tvck_lst \<Rightarrow> atom set"*) |
75 and bv_tvck :: "tvck_lst \<Rightarrow> atom set" |
76 where |
76 where |
77 "bv (K s tvts tvcs vs) = {}" (*(bv_tvtk tvts) \<union> (bv_tvck tvcs) \<union> (bv_vt vs) *) |
77 "bv (K s tvts tvcs vs) = (bv_tvtk tvts) \<union> (bv_tvck tvcs) \<union> (bv_vt vs)" |
78 (*| "bv_vt VTNil = {}" |
78 | "bv_vt VTNil = {}" |
79 | "bv_vt (VTCons v k t) = {atom v} \<union> bv_vt t" |
79 | "bv_vt (VTCons v k t) = {atom v} \<union> bv_vt t" |
80 | "bv_tvtk TVTKNil = {}" |
80 | "bv_tvtk TVTKNil = {}" |
81 | "bv_tvtk (TVTKCons v k t) = {atom v} \<union> bv_tvtk t" |
81 | "bv_tvtk (TVTKCons v k t) = {atom v} \<union> bv_tvtk t" |
82 | "bv_tvck TVCKNil = {}" |
82 | "bv_tvck TVCKNil = {}" |
83 | "bv_tvck (TVCKCons v k t) = {atom v} \<union> bv_tvck t"*) |
83 | "bv_tvck (TVCKCons v k t) = {atom v} \<union> bv_tvck t" |
84 |
84 |
85 thm tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_tvtk_lst_tvck_lst_vt_lst.fv |
85 ML {* Sign.of_sort @{theory} (@{typ tkind}, @{sort fs}) *} |
|
86 |
|
87 lemma helper: "((\<exists>p. P p) \<and> Q) = (\<exists>p. (P p \<and> Q))" |
|
88 by auto |
|
89 |
|
90 lemma supp: |
|
91 "fv_tkind tkind = supp tkind \<and> |
|
92 fv_ckind ckind = supp ckind \<and> |
|
93 fv_ty ty = supp ty \<and> |
|
94 fv_ty_lst ty_lst = supp ty_lst \<and> |
|
95 fv_co co = supp co \<and> |
|
96 fv_co_lst co_lst = supp co_lst \<and> |
|
97 fv_trm trm = supp trm \<and> |
|
98 fv_assoc_lst assoc_lst = supp assoc_lst \<and> |
|
99 fv_pat pat = supp pat \<and> |
|
100 fv_vt_lst vt_lst = supp vt_lst \<and> |
|
101 fv_tvtk_lst tvtk_lst = supp tvtk_lst \<and> |
|
102 fv_tvck_lst tvck_lst = supp tvck_lst" |
|
103 apply(rule tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.induct) |
|
104 ML_prf {* |
|
105 fun supp_eq_tac fv perm eqiff ctxt = |
|
106 asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW |
|
107 asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_Abs[symmetric]}) THEN_ALL_NEW |
|
108 simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW |
|
109 simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW |
|
110 simp_tac (HOL_basic_ss addsimps (@{thm permute_ABS} :: perm)) THEN_ALL_NEW |
|
111 simp_tac (HOL_basic_ss addsimps (@{thm Abs_eq_iff} :: eqiff)) THEN_ALL_NEW |
|
112 simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW |
|
113 simp_tac (HOL_basic_ss addsimps @{thms alpha_gen}) THEN_ALL_NEW |
|
114 asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW |
|
115 asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW |
|
116 simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW |
|
117 simp_tac (HOL_basic_ss addsimps @{thms infinite_Un[symmetric] Collect_disj_eq[symmetric]}) THEN_ALL_NEW |
|
118 simp_tac (HOL_basic_ss addsimps @{thms de_Morgan_conj[symmetric]}) THEN_ALL_NEW |
|
119 simp_tac (HOL_ss addsimps @{thms Collect_const finite.emptyI}) |
|
120 *} |
|
121 apply (tactic {* ALLGOALS (TRY o SOLVED' (supp_eq_tac |
|
122 @{thms tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.fv} |
|
123 @{thms tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.perm} |
|
124 @{thms tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.eq_iff} |
|
125 @{context})) *}) |
|
126 apply (simp only: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.fv) |
|
127 apply (simp only: Un_assoc[symmetric]) |
|
128 apply (simp only: Un_Diff[symmetric]) |
|
129 apply (simp only: supp_Pair[symmetric]) |
|
130 apply (simp only: supp_Abs[symmetric]) |
|
131 apply (simp (no_asm) only: supp_def) |
|
132 apply (simp only: permute_ABS) |
|
133 apply (simp only: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.perm) |
|
134 apply (simp only: Abs_eq_iff) |
|
135 apply (simp only: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.eq_iff) |
|
136 apply (simp only: alpha_gen2) |
|
137 apply (simp only: alpha_gen) |
|
138 apply (simp only: eqvts[symmetric]) |
|
139 apply (simp only: supp_Pair) |
|
140 apply (simp only: eqvts) |
|
141 apply (simp only: Pair_eq) |
|
142 apply (simp only: infinite_Un[symmetric] Collect_disj_eq[symmetric]) |
|
143 apply (simp only: de_Morgan_conj[symmetric]) |
|
144 apply (simp only: helper) |
|
145 by (simp) |
|
146 |
|
147 thm tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.fv[simplified supp] |
86 |
148 |
87 |
149 |
88 end |
150 end |
89 |
151 |
90 |
152 |