equal
deleted
inserted
replaced
5 Deriving support propoerties for the quotient types. |
5 Deriving support propoerties for the quotient types. |
6 *) |
6 *) |
7 |
7 |
8 signature NOMINAL_DT_SUPP = |
8 signature NOMINAL_DT_SUPP = |
9 sig |
9 sig |
10 val prove_supports: Proof.context -> thm list -> term list -> thm list |
10 |
11 val prove_fsupp: Proof.context -> typ list -> thm -> thm list -> thm list |
|
12 |
|
13 val fs_instance: typ list -> string list -> (string * sort) list -> thm list -> |
|
14 local_theory -> local_theory |
|
15 |
|
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 |
|
18 |
|
19 val prove_bns_finite: typ list -> term list -> thm -> thm list -> Proof.context -> thm list |
|
20 val prove_perm_bn_alpha_thms: typ list -> term list -> term list -> thm -> thm list -> thm list -> |
|
21 thm list -> Proof.context -> thm list |
|
22 end |
11 end |
23 |
12 |
24 structure Nominal_Dt_Supp: NOMINAL_DT_SUPP = |
13 structure Nominal_Dt_Supp: NOMINAL_DT_SUPP = |
25 struct |
14 struct |
26 |
15 |
215 in |
204 in |
216 (arg_ty, fn x => (mk_id (Abs ("", arg_ty, alpha_bn $ Bound 0 $ (qperm_bn $ p $ Bound 0)))) $ x) |
205 (arg_ty, fn x => (mk_id (Abs ("", arg_ty, alpha_bn $ Bound 0 $ (qperm_bn $ p $ Bound 0)))) $ x) |
217 end |
206 end |
218 |
207 |
219 val props = map2 mk_goal qperm_bns alpha_bns |
208 val props = map2 mk_goal qperm_bns alpha_bns |
220 val ss_tac = (K (print_tac "test")) THEN' |
209 val ss = @{thm id_def}::qperm_bn_simps @ qeq_iffs @ qalpha_refls |
221 asm_full_simp_tac (HOL_ss addsimps (@{thm id_def}::qperm_bn_simps @ qeq_iffs @ qalpha_refls)) |
210 val ss_tac = asm_full_simp_tac (HOL_ss addsimps ss) |
222 in |
211 in |
223 induct_prove qtys props qinduct (K ss_tac) ctxt' |
212 induct_prove qtys props qinduct (K ss_tac) ctxt' |
224 |> ProofContext.export ctxt' ctxt |
213 |> ProofContext.export ctxt' ctxt |
225 |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) |
214 |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) |
226 end |
215 end |