| author | Christian Urban <urbanc@in.tum.de> |
| Sun, 29 Aug 2010 00:36:47 +0800 | |
| changeset 2449 | 6b51117b8955 |
| parent 2448 | b9d9c4540265 |
| child 2450 | 217ef3e4282e |
| permissions | -rw-r--r-- |
| 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) |
|
|
2449
6b51117b8955
fiexed problem with constructors that have no arguments
Christian Urban <urbanc@in.tum.de>
parents:
2448
diff
changeset
|
24 |
val lhs = fold (curry HOLogic.mk_prod) vs @{term "()"}
|
|
6b51117b8955
fiexed problem with constructors that have no arguments
Christian Urban <urbanc@in.tum.de>
parents:
2448
diff
changeset
|
25 |
|> mk_supp |
| 2448 | 26 |
in |
27 |
mk_supports lhs rhs |
|
28 |
|> HOLogic.mk_Trueprop |
|
29 |
end |
|
30 |
||
31 |
fun supports_tac ctxt perm_simps = |
|
32 |
let |
|
33 |
val ss1 = HOL_basic_ss addsimps @{thms supports_def fresh_def[symmetric]}
|
|
34 |
val ss2 = HOL_ss addsimps @{thms swap_fresh_fresh fresh_Pair}
|
|
35 |
in |
|
36 |
EVERY' [ simp_tac ss1, |
|
37 |
Nominal_Permeq.eqvt_strict_tac ctxt perm_simps [], |
|
38 |
simp_tac ss2 ] |
|
39 |
end |
|
40 |
||
41 |
fun prove_supports_single ctxt perm_simps qtrm = |
|
42 |
let |
|
43 |
val goal = mk_supports_goal ctxt qtrm |
|
44 |
val ctxt' = Variable.auto_fixes goal ctxt |
|
45 |
in |
|
46 |
Goal.prove ctxt' [] [] goal |
|
47 |
(K (HEADGOAL (supports_tac ctxt perm_simps))) |
|
48 |
|> singleton (ProofContext.export ctxt' ctxt) |
|
49 |
end |
|
50 |
||
51 |
fun prove_supports ctxt perm_simps qtrms = |
|
52 |
map (prove_supports_single ctxt perm_simps) qtrms |
|
53 |
||
54 |
||
55 |
||
56 |
||
57 |
end (* structure *) |
|
58 |