| author | Christian Urban <urbanc@in.tum.de> |
| Sun, 29 Aug 2010 01:17:36 +0800 | |
| changeset 2450 | 217ef3e4282e |
| parent 2449 | 6b51117b8955 |
| child 2451 | d2e929f51fa9 |
| 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 |
|
|
2450
217ef3e4282e
added proofs for fsupp properties
Christian Urban <urbanc@in.tum.de>
parents:
2449
diff
changeset
|
11 |
val prove_fsupp: Proof.context -> typ list -> thm -> thm list -> thm list |
| 2448 | 12 |
end |
13 |
||
14 |
structure Nominal_Dt_Supp: NOMINAL_DT_SUPP = |
|
15 |
struct |
|
16 |
||
17 |
||
|
2450
217ef3e4282e
added proofs for fsupp properties
Christian Urban <urbanc@in.tum.de>
parents:
2449
diff
changeset
|
18 |
(* supports lemmas for constructors *) |
| 2448 | 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 |
||
|
2450
217ef3e4282e
added proofs for fsupp properties
Christian Urban <urbanc@in.tum.de>
parents:
2449
diff
changeset
|
55 |
(* finite supp lemmas for qtypes *) |
| 2448 | 56 |
|
|
2450
217ef3e4282e
added proofs for fsupp properties
Christian Urban <urbanc@in.tum.de>
parents:
2449
diff
changeset
|
57 |
fun prove_fsupp ctxt qtys qinduct qsupports_thms = |
|
217ef3e4282e
added proofs for fsupp properties
Christian Urban <urbanc@in.tum.de>
parents:
2449
diff
changeset
|
58 |
let |
|
217ef3e4282e
added proofs for fsupp properties
Christian Urban <urbanc@in.tum.de>
parents:
2449
diff
changeset
|
59 |
val (vs, ctxt') = Variable.variant_fixes (replicate (length qtys) "x") ctxt |
|
217ef3e4282e
added proofs for fsupp properties
Christian Urban <urbanc@in.tum.de>
parents:
2449
diff
changeset
|
60 |
val goals = vs ~~ qtys |
|
217ef3e4282e
added proofs for fsupp properties
Christian Urban <urbanc@in.tum.de>
parents:
2449
diff
changeset
|
61 |
|> map Free |
|
217ef3e4282e
added proofs for fsupp properties
Christian Urban <urbanc@in.tum.de>
parents:
2449
diff
changeset
|
62 |
|> map (mk_finite o mk_supp) |
|
217ef3e4282e
added proofs for fsupp properties
Christian Urban <urbanc@in.tum.de>
parents:
2449
diff
changeset
|
63 |
|> foldr1 (HOLogic.mk_conj) |
|
217ef3e4282e
added proofs for fsupp properties
Christian Urban <urbanc@in.tum.de>
parents:
2449
diff
changeset
|
64 |
|> HOLogic.mk_Trueprop |
|
217ef3e4282e
added proofs for fsupp properties
Christian Urban <urbanc@in.tum.de>
parents:
2449
diff
changeset
|
65 |
|
|
217ef3e4282e
added proofs for fsupp properties
Christian Urban <urbanc@in.tum.de>
parents:
2449
diff
changeset
|
66 |
val tac = |
|
217ef3e4282e
added proofs for fsupp properties
Christian Urban <urbanc@in.tum.de>
parents:
2449
diff
changeset
|
67 |
EVERY' [ rtac @{thm supports_finite},
|
|
217ef3e4282e
added proofs for fsupp properties
Christian Urban <urbanc@in.tum.de>
parents:
2449
diff
changeset
|
68 |
resolve_tac qsupports_thms, |
|
217ef3e4282e
added proofs for fsupp properties
Christian Urban <urbanc@in.tum.de>
parents:
2449
diff
changeset
|
69 |
asm_simp_tac (HOL_ss addsimps @{thms finite_supp supp_Pair finite_Un}) ]
|
|
217ef3e4282e
added proofs for fsupp properties
Christian Urban <urbanc@in.tum.de>
parents:
2449
diff
changeset
|
70 |
in |
|
217ef3e4282e
added proofs for fsupp properties
Christian Urban <urbanc@in.tum.de>
parents:
2449
diff
changeset
|
71 |
Goal.prove ctxt' [] [] goals |
|
217ef3e4282e
added proofs for fsupp properties
Christian Urban <urbanc@in.tum.de>
parents:
2449
diff
changeset
|
72 |
(K (HEADGOAL (rtac qinduct THEN_ALL_NEW tac))) |
|
217ef3e4282e
added proofs for fsupp properties
Christian Urban <urbanc@in.tum.de>
parents:
2449
diff
changeset
|
73 |
|> singleton (ProofContext.export ctxt' ctxt) |
|
217ef3e4282e
added proofs for fsupp properties
Christian Urban <urbanc@in.tum.de>
parents:
2449
diff
changeset
|
74 |
|> Datatype_Aux.split_conj_thm |
|
217ef3e4282e
added proofs for fsupp properties
Christian Urban <urbanc@in.tum.de>
parents:
2449
diff
changeset
|
75 |
|> map zero_var_indexes |
|
217ef3e4282e
added proofs for fsupp properties
Christian Urban <urbanc@in.tum.de>
parents:
2449
diff
changeset
|
76 |
end |
| 2448 | 77 |
|
78 |
end (* structure *) |
|
79 |