142 |
132 |
143 fun mk_supp_abs_tac ctxt [] = [] |
133 fun mk_supp_abs_tac ctxt [] = [] |
144 | mk_supp_abs_tac ctxt (BC (_, [], _)::xs) = mk_supp_abs_tac ctxt xs |
134 | mk_supp_abs_tac ctxt (BC (_, [], _)::xs) = mk_supp_abs_tac ctxt xs |
145 | mk_supp_abs_tac ctxt (bc::xs) = (DETERM o mk_supp_abs ctxt bc)::mk_supp_abs_tac ctxt xs |
135 | mk_supp_abs_tac ctxt (bc::xs) = (DETERM o mk_supp_abs ctxt bc)::mk_supp_abs_tac ctxt xs |
146 |
136 |
147 fun mk_bn_supp_abs_tac thm = |
137 fun mk_bn_supp_abs_tac trm = |
148 (prop_of thm) |
138 trm |
149 |> HOLogic.dest_Trueprop |
|
150 |> snd o HOLogic.dest_eq |
|
151 |> fastype_of |
139 |> fastype_of |
|
140 |> body_type |
152 |> (fn ty => case ty of |
141 |> (fn ty => case ty of |
153 @{typ "atom set"} => simp_tac (add_ss supp_abs_set) |
142 @{typ "atom set"} => simp_tac (add_ss supp_abs_set) |
154 | @{typ "atom list"} => simp_tac (add_ss supp_abs_lst) |
143 | @{typ "atom list"} => simp_tac (add_ss supp_abs_lst) |
155 | _ => raise TERM ("mk_bn_supp_abs_tac", [prop_of thm])) |
144 | _ => raise TERM ("mk_bn_supp_abs_tac", [trm])) |
156 |
145 |
157 |
146 |
158 val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc} |
147 val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc} |
159 val thms2 = @{thms de_Morgan_conj Collect_disj_eq finite_Un} |
148 val thms2 = @{thms de_Morgan_conj Collect_disj_eq finite_Un} |
160 val thms3 = @{thms alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def |
149 val thms3 = @{thms alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def |
161 prod.recs prod.cases prod.inject not_True_eq_False empty_def[symmetric] Finite_Set.finite.emptyI} |
150 prod.recs prod.cases prod.inject not_True_eq_False empty_def[symmetric] Finite_Set.finite.emptyI} |
162 |
151 |
163 fun ind_tac ctxt qinducts = |
|
164 let |
|
165 fun CASES_TAC_TO_TAC cases_tac st = Seq.map snd (cases_tac st) |
|
166 in |
|
167 DETERM o (CASES_TAC_TO_TAC o (Induct.induct_tac ctxt false [] [] [] (SOME qinducts) [])) |
|
168 end |
|
169 |
|
170 fun p_tac msg i = |
152 fun p_tac msg i = |
171 if false then print_tac ("ptest: " ^ msg) else all_tac |
153 if false then print_tac ("ptest: " ^ msg) else all_tac |
172 |
154 |
173 fun q_tac msg i = |
155 fun q_tac msg i = |
174 if true then print_tac ("qtest: " ^ msg) else all_tac |
156 if true then print_tac ("qtest: " ^ msg) else all_tac |
175 |
157 |
176 fun prove_fv_supp qtys fvs fv_bns alpha_bns bn_simps fv_simps eq_iffs perm_simps |
158 fun prove_fv_supp qtys qtrms fvs fv_bns alpha_bns bn_simps fv_simps eq_iffs perm_simps |
177 fv_bn_eqvts qinducts bclausess ctxt = |
159 fv_bn_eqvts qinduct bclausess ctxt = |
178 let |
160 let |
179 val (arg_names, ctxt') = |
161 val goals1 = map mk_fvs_goals fvs |
180 Variable.variant_fixes (replicate (length qtys) "x") ctxt |
162 val goals2 = map2 mk_fv_bns_goals fv_bns alpha_bns |
181 val args = map2 (curry Free) arg_names qtys |
163 |
182 val ty_arg_map = qtys ~~ args |
164 |
183 val ind_args = map SOME arg_names |
165 |
184 |
166 fun tac ctxt = |
185 val goals1 = map (mk_fvs_goals ty_arg_map) fvs |
167 SUBGOAL (fn (goal, i) => |
186 val goals2 = map2 (mk_fv_bns_goals ty_arg_map) fv_bns alpha_bns |
168 let |
187 |
169 val (fv_fun, arg) = |
188 fun fv_tac ctxt bclauses = |
170 goal |> Envir.eta_contract |
|
171 |> Logic.strip_assums_concl |
|
172 |> HOLogic.dest_Trueprop |
|
173 |> fst o HOLogic.dest_eq |
|
174 |> dest_comb |
|
175 val supp_abs_tac = |
|
176 case (AList.lookup (op=) (qtrms ~~ bclausess) (head_of arg)) of |
|
177 SOME bclauses => EVERY' (mk_supp_abs_tac ctxt bclauses) |
|
178 | NONE => mk_bn_supp_abs_tac fv_fun |
|
179 in |
|
180 EVERY' [ TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)), |
|
181 TRY o supp_abs_tac, |
|
182 TRY o simp_tac (add_ss @{thms supp_def supp_rel_def}), |
|
183 TRY o Nominal_Permeq.eqvt_tac ctxt (perm_simps @ fv_bn_eqvts) [], |
|
184 TRY o simp_tac (add_ss (@{thms Abs_eq_iff} @ eq_iffs)), |
|
185 TRY o asm_full_simp_tac (add_ss thms3), |
|
186 TRY o simp_tac (add_ss thms2), |
|
187 TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts)))] i |
|
188 end) |
|
189 in |
|
190 induct_prove qtys (goals1 @ goals2) qinduct tac ctxt |
|
191 end |
|
192 |
|
193 (* |
|
194 fun fv_tac bclauses ctxt = |
189 SOLVED' (EVERY' [ |
195 SOLVED' (EVERY' [ |
190 (fn i => print_tac ("FV Goal: " ^ string_of_int i ^ " with " ^ (@{make_string} bclauses))), |
196 (fn i => print_tac ("FV Goal: " ^ string_of_int i ^ " with " ^ (@{make_string} bclauses))), |
191 TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)), |
197 TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)), |
192 p_tac "A", |
198 p_tac "A", |
193 TRY o EVERY' (mk_supp_abs_tac ctxt bclauses), |
199 TRY o EVERY' (mk_supp_abs_tac ctxt bclauses), |
205 TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts))), |
211 TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts))), |
206 p_tac "H", |
212 p_tac "H", |
207 (fn i => print_tac ("finished with FV Goal: " ^ string_of_int i)) |
213 (fn i => print_tac ("finished with FV Goal: " ^ string_of_int i)) |
208 ]) |
214 ]) |
209 |
215 |
210 fun bn_tac ctxt bn_simp = |
216 fun fv_tacs ctxt = map (fv_tac ctxt) bclausess |
|
217 (*fun bn_tacs ctxt = map (bn_tac ctxt) bn_simps*) |
|
218 *) |
|
219 |
|
220 (* |
|
221 fun bn_tac ctxt bn_simp = |
211 SOLVED' (EVERY' [ |
222 SOLVED' (EVERY' [ |
212 (fn i => print_tac ("BN Goal: " ^ string_of_int i)), |
223 (fn i => print_tac ("BN Goal: " ^ string_of_int i)), |
213 TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)), |
224 TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)), |
214 q_tac "A", |
225 q_tac "A", |
215 TRY o mk_bn_supp_abs_tac bn_simp, |
226 TRY o mk_bn_supp_abs_tac bn_simp, |