equal
deleted
inserted
replaced
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 val prove_supports: Proof.context -> thm list -> term list -> thm list |
11 |
11 val prove_fsupp: Proof.context -> typ list -> thm -> thm list -> thm list |
12 end |
12 end |
13 |
13 |
14 structure Nominal_Dt_Supp: NOMINAL_DT_SUPP = |
14 structure Nominal_Dt_Supp: NOMINAL_DT_SUPP = |
15 struct |
15 struct |
16 |
16 |
17 |
17 |
18 (* supports lemmas *) |
18 (* supports lemmas for constructors *) |
19 |
19 |
20 fun mk_supports_goal ctxt qtrm = |
20 fun mk_supports_goal ctxt qtrm = |
21 let |
21 let |
22 val vs = fresh_args ctxt qtrm |
22 val vs = fresh_args ctxt qtrm |
23 val rhs = list_comb (qtrm, vs) |
23 val rhs = list_comb (qtrm, vs) |
50 |
50 |
51 fun prove_supports ctxt perm_simps qtrms = |
51 fun prove_supports ctxt perm_simps qtrms = |
52 map (prove_supports_single ctxt perm_simps) qtrms |
52 map (prove_supports_single ctxt perm_simps) qtrms |
53 |
53 |
54 |
54 |
|
55 (* finite supp lemmas for qtypes *) |
55 |
56 |
|
57 fun prove_fsupp ctxt qtys qinduct qsupports_thms = |
|
58 let |
|
59 val (vs, ctxt') = Variable.variant_fixes (replicate (length qtys) "x") ctxt |
|
60 val goals = vs ~~ qtys |
|
61 |> map Free |
|
62 |> map (mk_finite o mk_supp) |
|
63 |> foldr1 (HOLogic.mk_conj) |
|
64 |> HOLogic.mk_Trueprop |
|
65 |
|
66 val tac = |
|
67 EVERY' [ rtac @{thm supports_finite}, |
|
68 resolve_tac qsupports_thms, |
|
69 asm_simp_tac (HOL_ss addsimps @{thms finite_supp supp_Pair finite_Un}) ] |
|
70 in |
|
71 Goal.prove ctxt' [] [] goals |
|
72 (K (HEADGOAL (rtac qinduct THEN_ALL_NEW tac))) |
|
73 |> singleton (ProofContext.export ctxt' ctxt) |
|
74 |> Datatype_Aux.split_conj_thm |
|
75 |> map zero_var_indexes |
|
76 end |
56 |
77 |
57 end (* structure *) |
78 end (* structure *) |
58 |
79 |