| author | Christian Urban <urbanc@in.tum.de> |
| Sat, 21 Aug 2010 20:07:36 +0800 | |
| changeset 2426 | deb5be0115a7 |
| parent 2335 | 558c823f96aa |
| permissions | -rw-r--r-- |
|
1274
d867021d8ac1
Preparing the generalized lifting procedure
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
1 |
theory Lift |
|
2015
3e7969262809
Move old fv_alpha_export to Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2008
diff
changeset
|
2 |
imports "../Nominal-General/Nominal2_Atoms" |
|
3e7969262809
Move old fv_alpha_export to Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2008
diff
changeset
|
3 |
"../Nominal-General/Nominal2_Eqvt" |
|
3e7969262809
Move old fv_alpha_export to Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2008
diff
changeset
|
4 |
"../Nominal-General/Nominal2_Supp" |
| 2296 | 5 |
"Abs" "Perm" "Rsp" |
|
1274
d867021d8ac1
Preparing the generalized lifting procedure
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
6 |
begin |
|
d867021d8ac1
Preparing the generalized lifting procedure
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
7 |
|
|
1316
0577afdb1732
Porting from Lift to Parser; until defining the Quotient type.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1309
diff
changeset
|
8 |
ML {*
|
|
1681
b8a07a3c1692
Get lifted types information from the quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1656
diff
changeset
|
9 |
fun define_quotient_types binds tys alphas equivps ctxt = |
|
1656
c9d3dda79fe3
Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1553
diff
changeset
|
10 |
let |
|
1681
b8a07a3c1692
Get lifted types information from the quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1656
diff
changeset
|
11 |
fun def_ty ((b, ty), (alpha, equivp)) ctxt = |
|
2325
29532d69111c
changes for partial-equivalence quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2015
diff
changeset
|
12 |
Quotient_Type.add_quotient_type ((([], b, NoSyn), (ty, alpha, false)), equivp) ctxt; |
|
1681
b8a07a3c1692
Get lifted types information from the quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1656
diff
changeset
|
13 |
val alpha_equivps = List.take (equivps, length alphas) |
|
2335
558c823f96aa
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
2330
diff
changeset
|
14 |
val (qinfo, ctxt') = fold_map def_ty ((binds ~~ tys) ~~ (alphas ~~ alpha_equivps)) ctxt; |
|
558c823f96aa
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
2330
diff
changeset
|
15 |
val qtys = map #qtyp qinfo; |
|
1656
c9d3dda79fe3
Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1553
diff
changeset
|
16 |
in |
|
1681
b8a07a3c1692
Get lifted types information from the quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1656
diff
changeset
|
17 |
(qtys, ctxt') |
|
1656
c9d3dda79fe3
Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1553
diff
changeset
|
18 |
end |
|
c9d3dda79fe3
Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1553
diff
changeset
|
19 |
*} |
|
c9d3dda79fe3
Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1553
diff
changeset
|
20 |
|
|
2426
deb5be0115a7
moved lifting code from Lift.thy to nominal_dt_quot.ML
Christian Urban <urbanc@in.tum.de>
parents:
2335
diff
changeset
|
21 |
(* Unrawifying schematic and bound variables *) |
|
deb5be0115a7
moved lifting code from Lift.thy to nominal_dt_quot.ML
Christian Urban <urbanc@in.tum.de>
parents:
2335
diff
changeset
|
22 |
|
|
1656
c9d3dda79fe3
Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1553
diff
changeset
|
23 |
ML {*
|
|
2426
deb5be0115a7
moved lifting code from Lift.thy to nominal_dt_quot.ML
Christian Urban <urbanc@in.tum.de>
parents:
2335
diff
changeset
|
24 |
fun unraw_str s = |
|
deb5be0115a7
moved lifting code from Lift.thy to nominal_dt_quot.ML
Christian Urban <urbanc@in.tum.de>
parents:
2335
diff
changeset
|
25 |
unsuffix "_raw" s |
|
deb5be0115a7
moved lifting code from Lift.thy to nominal_dt_quot.ML
Christian Urban <urbanc@in.tum.de>
parents:
2335
diff
changeset
|
26 |
handle Fail _ => s |
|
deb5be0115a7
moved lifting code from Lift.thy to nominal_dt_quot.ML
Christian Urban <urbanc@in.tum.de>
parents:
2335
diff
changeset
|
27 |
|
|
deb5be0115a7
moved lifting code from Lift.thy to nominal_dt_quot.ML
Christian Urban <urbanc@in.tum.de>
parents:
2335
diff
changeset
|
28 |
fun unraw_vars_thm thm = |
|
1498
2ff84b1f551f
Rename bound variables + minor cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1497
diff
changeset
|
29 |
let |
|
2426
deb5be0115a7
moved lifting code from Lift.thy to nominal_dt_quot.ML
Christian Urban <urbanc@in.tum.de>
parents:
2335
diff
changeset
|
30 |
fun unraw_var ((s, i), T) = ((unraw_str s, i), T) |
|
deb5be0115a7
moved lifting code from Lift.thy to nominal_dt_quot.ML
Christian Urban <urbanc@in.tum.de>
parents:
2335
diff
changeset
|
31 |
|
|
1498
2ff84b1f551f
Rename bound variables + minor cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1497
diff
changeset
|
32 |
val vars = Term.add_vars (prop_of thm) [] |
|
2426
deb5be0115a7
moved lifting code from Lift.thy to nominal_dt_quot.ML
Christian Urban <urbanc@in.tum.de>
parents:
2335
diff
changeset
|
33 |
val nvars = map (Var o unraw_var) vars |
|
1498
2ff84b1f551f
Rename bound variables + minor cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1497
diff
changeset
|
34 |
in |
|
2ff84b1f551f
Rename bound variables + minor cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1497
diff
changeset
|
35 |
Thm.certify_instantiate ([], (vars ~~ nvars)) thm |
|
2ff84b1f551f
Rename bound variables + minor cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1497
diff
changeset
|
36 |
end |
|
2ff84b1f551f
Rename bound variables + minor cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1497
diff
changeset
|
37 |
*} |
|
2ff84b1f551f
Rename bound variables + minor cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1497
diff
changeset
|
38 |
|
|
2ff84b1f551f
Rename bound variables + minor cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1497
diff
changeset
|
39 |
ML {*
|
|
2426
deb5be0115a7
moved lifting code from Lift.thy to nominal_dt_quot.ML
Christian Urban <urbanc@in.tum.de>
parents:
2335
diff
changeset
|
40 |
fun unraw_bounds_thm th = |
|
1494
923413256cbb
Clean 'Lift', start working only on exported things in Parser.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1342
diff
changeset
|
41 |
let |
|
2426
deb5be0115a7
moved lifting code from Lift.thy to nominal_dt_quot.ML
Christian Urban <urbanc@in.tum.de>
parents:
2335
diff
changeset
|
42 |
val trm = Thm.prop_of th |
|
deb5be0115a7
moved lifting code from Lift.thy to nominal_dt_quot.ML
Christian Urban <urbanc@in.tum.de>
parents:
2335
diff
changeset
|
43 |
val trm' = Term.map_abs_vars unraw_str trm |
|
1498
2ff84b1f551f
Rename bound variables + minor cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1497
diff
changeset
|
44 |
in |
|
2426
deb5be0115a7
moved lifting code from Lift.thy to nominal_dt_quot.ML
Christian Urban <urbanc@in.tum.de>
parents:
2335
diff
changeset
|
45 |
Thm.rename_boundvars trm trm' th |
|
1498
2ff84b1f551f
Rename bound variables + minor cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1497
diff
changeset
|
46 |
end |
|
2ff84b1f551f
Rename bound variables + minor cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1497
diff
changeset
|
47 |
*} |
|
2ff84b1f551f
Rename bound variables + minor cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1497
diff
changeset
|
48 |
|
|
2ff84b1f551f
Rename bound variables + minor cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1497
diff
changeset
|
49 |
|
|
2ff84b1f551f
Rename bound variables + minor cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1497
diff
changeset
|
50 |
ML {*
|
|
1683
f78c820f67c3
Automatically lift theorems and constants only using the new quotient types. Requires new Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1681
diff
changeset
|
51 |
fun lift_thm qtys ctxt thm = |
|
2426
deb5be0115a7
moved lifting code from Lift.thy to nominal_dt_quot.ML
Christian Urban <urbanc@in.tum.de>
parents:
2335
diff
changeset
|
52 |
Quotient_Tacs.lifted qtys ctxt thm |
|
deb5be0115a7
moved lifting code from Lift.thy to nominal_dt_quot.ML
Christian Urban <urbanc@in.tum.de>
parents:
2335
diff
changeset
|
53 |
|> unraw_bounds_thm |
|
deb5be0115a7
moved lifting code from Lift.thy to nominal_dt_quot.ML
Christian Urban <urbanc@in.tum.de>
parents:
2335
diff
changeset
|
54 |
|> unraw_vars_thm |
|
1276
3365fce80f0f
To call quotient it is enough to export the alpha frees to proper constants and their respective equivp theorems.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1274
diff
changeset
|
55 |
*} |
|
1274
d867021d8ac1
Preparing the generalized lifting procedure
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
56 |
|
|
2426
deb5be0115a7
moved lifting code from Lift.thy to nominal_dt_quot.ML
Christian Urban <urbanc@in.tum.de>
parents:
2335
diff
changeset
|
57 |
|
|
1280
1f057f8da8aa
Progress with general lifting procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1277
diff
changeset
|
58 |
end |
|
1274
d867021d8ac1
Preparing the generalized lifting procedure
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
59 |