|
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
|
|
|
11 |
|
|
|
12 |
end
|
|
|
13 |
|
|
|
14 |
structure Nominal_Dt_Supp: NOMINAL_DT_SUPP =
|
|
|
15 |
struct
|
|
|
16 |
|
|
|
17 |
|
|
|
18 |
(* supports lemmas *)
|
|
|
19 |
|
|
|
20 |
fun mk_supports_goal ctxt qtrm =
|
|
|
21 |
let
|
|
|
22 |
val vs = fresh_args ctxt qtrm
|
|
|
23 |
val rhs = list_comb (qtrm, vs)
|
|
|
24 |
val lhs = mk_supp (foldl1 HOLogic.mk_prod vs)
|
|
|
25 |
in
|
|
|
26 |
mk_supports lhs rhs
|
|
|
27 |
|> HOLogic.mk_Trueprop
|
|
|
28 |
end
|
|
|
29 |
|
|
|
30 |
fun supports_tac ctxt perm_simps =
|
|
|
31 |
let
|
|
|
32 |
val ss1 = HOL_basic_ss addsimps @{thms supports_def fresh_def[symmetric]}
|
|
|
33 |
val ss2 = HOL_ss addsimps @{thms swap_fresh_fresh fresh_Pair}
|
|
|
34 |
in
|
|
|
35 |
EVERY' [ simp_tac ss1,
|
|
|
36 |
Nominal_Permeq.eqvt_strict_tac ctxt perm_simps [],
|
|
|
37 |
simp_tac ss2 ]
|
|
|
38 |
end
|
|
|
39 |
|
|
|
40 |
fun prove_supports_single ctxt perm_simps qtrm =
|
|
|
41 |
let
|
|
|
42 |
val goal = mk_supports_goal ctxt qtrm
|
|
|
43 |
val ctxt' = Variable.auto_fixes goal ctxt
|
|
|
44 |
in
|
|
|
45 |
Goal.prove ctxt' [] [] goal
|
|
|
46 |
(K (HEADGOAL (supports_tac ctxt perm_simps)))
|
|
|
47 |
|> singleton (ProofContext.export ctxt' ctxt)
|
|
|
48 |
end
|
|
|
49 |
|
|
|
50 |
fun prove_supports ctxt perm_simps qtrms =
|
|
|
51 |
map (prove_supports_single ctxt perm_simps) qtrms
|
|
|
52 |
|
|
|
53 |
|
|
|
54 |
|
|
|
55 |
|
|
|
56 |
end (* structure *)
|
|
|
57 |
|