equal
deleted
inserted
replaced
13 val fs_instance: typ list -> string list -> (string * sort) list -> thm list -> |
13 val fs_instance: typ list -> string list -> (string * sort) list -> thm list -> |
14 local_theory -> local_theory |
14 local_theory -> local_theory |
15 |
15 |
16 val prove_fv_supp: typ list -> term list -> term list -> term list -> term list -> thm list -> |
16 val prove_fv_supp: typ list -> term list -> term list -> term list -> term list -> thm list -> |
17 thm list -> thm list -> thm list -> thm -> bclause list list -> Proof.context -> thm list |
17 thm list -> thm list -> thm list -> thm -> bclause list list -> Proof.context -> thm list |
|
18 |
|
19 val prove_bns_finite: typ list -> term list -> thm -> thm list -> Proof.context -> thm list |
|
20 |
18 end |
21 end |
19 |
22 |
20 structure Nominal_Dt_Supp: NOMINAL_DT_SUPP = |
23 structure Nominal_Dt_Supp: NOMINAL_DT_SUPP = |
21 struct |
24 struct |
22 |
25 |
143 |
146 |
144 |
147 |
145 val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc} |
148 val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc} |
146 val thms2 = @{thms de_Morgan_conj Collect_disj_eq finite_Un} |
149 val thms2 = @{thms de_Morgan_conj Collect_disj_eq finite_Un} |
147 val thms3 = @{thms alphas prod_alpha_def prod_fv.simps prod_rel_def permute_prod_def |
150 val thms3 = @{thms alphas prod_alpha_def prod_fv.simps prod_rel_def permute_prod_def |
148 prod.recs prod.cases prod.inject not_True_eq_False empty_def[symmetric] Finite_Set.finite.emptyI} |
151 prod.recs prod.cases prod.inject not_True_eq_False empty_def[symmetric] finite.emptyI} |
149 |
152 |
150 fun p_tac msg i = |
153 fun p_tac msg i = |
151 if false then print_tac ("ptest: " ^ msg) else all_tac |
154 if false then print_tac ("ptest: " ^ msg) else all_tac |
152 |
155 |
153 fun q_tac msg i = |
156 fun q_tac msg i = |
187 |> map atomize |
190 |> map atomize |
188 |> map (simplify (HOL_basic_ss addsimps @{thms fun_eq_iff[symmetric]})) |
191 |> map (simplify (HOL_basic_ss addsimps @{thms fun_eq_iff[symmetric]})) |
189 end |
192 end |
190 |
193 |
191 |
194 |
|
195 fun prove_bns_finite qtys qbns qinduct qbn_simps ctxt = |
|
196 let |
|
197 fun mk_goal qbn = |
|
198 let |
|
199 val arg_ty = domain_type (fastype_of qbn) |
|
200 val finite = @{term "finite :: atom set => bool"} |
|
201 in |
|
202 (arg_ty, fn x => finite $ (to_set (qbn $ x))) |
|
203 end |
|
204 |
|
205 val props = map mk_goal qbns |
|
206 val ss_tac = asm_full_simp_tac (HOL_basic_ss addsimps (qbn_simps @ |
|
207 @{thms set.simps set_append finite_insert finite.emptyI finite_Un})) |
|
208 in |
|
209 induct_prove qtys props qinduct (K (ss_tac ORELSE' (K no_tac))) ctxt |
|
210 end |
|
211 |
192 |
212 |
193 end (* structure *) |
213 end (* structure *) |