2448
|
1 |
(* Title: nominal_dt_alpha.ML
|
|
2 |
Author: Christian Urban
|
|
3 |
Author: Cezary Kaliszyk
|
|
4 |
|
|
5 |
Deriving support propoerties for the quotient types.
|
|
6 |
*)
|
|
7 |
|
|
8 |
signature NOMINAL_DT_SUPP =
|
|
9 |
sig
|
|
10 |
val prove_supports: Proof.context -> thm list -> term list -> thm list
|
2450
|
11 |
val prove_fsupp: Proof.context -> typ list -> thm -> thm list -> thm list
|
2451
|
12 |
|
|
13 |
val fs_instance: typ list -> string list -> (string * sort) list -> thm list ->
|
|
14 |
local_theory -> local_theory
|
2448
|
15 |
end
|
|
16 |
|
|
17 |
structure Nominal_Dt_Supp: NOMINAL_DT_SUPP =
|
|
18 |
struct
|
|
19 |
|
|
20 |
|
2450
|
21 |
(* supports lemmas for constructors *)
|
2448
|
22 |
|
|
23 |
fun mk_supports_goal ctxt qtrm =
|
|
24 |
let
|
|
25 |
val vs = fresh_args ctxt qtrm
|
|
26 |
val rhs = list_comb (qtrm, vs)
|
2449
|
27 |
val lhs = fold (curry HOLogic.mk_prod) vs @{term "()"}
|
|
28 |
|> mk_supp
|
2448
|
29 |
in
|
|
30 |
mk_supports lhs rhs
|
|
31 |
|> HOLogic.mk_Trueprop
|
|
32 |
end
|
|
33 |
|
|
34 |
fun supports_tac ctxt perm_simps =
|
|
35 |
let
|
|
36 |
val ss1 = HOL_basic_ss addsimps @{thms supports_def fresh_def[symmetric]}
|
|
37 |
val ss2 = HOL_ss addsimps @{thms swap_fresh_fresh fresh_Pair}
|
|
38 |
in
|
|
39 |
EVERY' [ simp_tac ss1,
|
|
40 |
Nominal_Permeq.eqvt_strict_tac ctxt perm_simps [],
|
|
41 |
simp_tac ss2 ]
|
|
42 |
end
|
|
43 |
|
|
44 |
fun prove_supports_single ctxt perm_simps qtrm =
|
|
45 |
let
|
|
46 |
val goal = mk_supports_goal ctxt qtrm
|
|
47 |
val ctxt' = Variable.auto_fixes goal ctxt
|
|
48 |
in
|
|
49 |
Goal.prove ctxt' [] [] goal
|
|
50 |
(K (HEADGOAL (supports_tac ctxt perm_simps)))
|
|
51 |
|> singleton (ProofContext.export ctxt' ctxt)
|
|
52 |
end
|
|
53 |
|
|
54 |
fun prove_supports ctxt perm_simps qtrms =
|
|
55 |
map (prove_supports_single ctxt perm_simps) qtrms
|
|
56 |
|
|
57 |
|
2450
|
58 |
(* finite supp lemmas for qtypes *)
|
2448
|
59 |
|
2450
|
60 |
fun prove_fsupp ctxt qtys qinduct qsupports_thms =
|
|
61 |
let
|
|
62 |
val (vs, ctxt') = Variable.variant_fixes (replicate (length qtys) "x") ctxt
|
|
63 |
val goals = vs ~~ qtys
|
|
64 |
|> map Free
|
|
65 |
|> map (mk_finite o mk_supp)
|
|
66 |
|> foldr1 (HOLogic.mk_conj)
|
|
67 |
|> HOLogic.mk_Trueprop
|
|
68 |
|
|
69 |
val tac =
|
|
70 |
EVERY' [ rtac @{thm supports_finite},
|
|
71 |
resolve_tac qsupports_thms,
|
|
72 |
asm_simp_tac (HOL_ss addsimps @{thms finite_supp supp_Pair finite_Un}) ]
|
|
73 |
in
|
|
74 |
Goal.prove ctxt' [] [] goals
|
|
75 |
(K (HEADGOAL (rtac qinduct THEN_ALL_NEW tac)))
|
|
76 |
|> singleton (ProofContext.export ctxt' ctxt)
|
|
77 |
|> Datatype_Aux.split_conj_thm
|
|
78 |
|> map zero_var_indexes
|
|
79 |
end
|
2448
|
80 |
|
2451
|
81 |
|
|
82 |
(* finite supp instances *)
|
|
83 |
|
|
84 |
fun fs_instance qtys qfull_ty_names tvs qfsupp_thms lthy =
|
|
85 |
let
|
|
86 |
val lthy1 =
|
|
87 |
lthy
|
|
88 |
|> Local_Theory.exit_global
|
|
89 |
|> Class.instantiation (qfull_ty_names, tvs, @{sort fs})
|
|
90 |
|
|
91 |
fun tac _ =
|
|
92 |
Class.intro_classes_tac [] THEN
|
|
93 |
(ALLGOALS (resolve_tac qfsupp_thms))
|
|
94 |
in
|
|
95 |
lthy1
|
|
96 |
|> Class.prove_instantiation_exit tac
|
|
97 |
|> Named_Target.theory_init
|
|
98 |
end
|
|
99 |
|
|
100 |
|
2448
|
101 |
end (* structure *)
|
|
102 |
|