| author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
| Thu, 18 Mar 2010 07:26:36 +0100 | |
| changeset 1494 | 923413256cbb |
| parent 1342 | 2b98012307f7 |
| child 1497 | 1c9931e5039a |
| permissions | -rw-r--r-- |
|
1274
d867021d8ac1
Preparing the generalized lifting procedure
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
1 |
theory Lift |
|
1494
923413256cbb
Clean 'Lift', start working only on exported things in Parser.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1342
diff
changeset
|
2 |
imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" |
|
1274
d867021d8ac1
Preparing the generalized lifting procedure
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
3 |
begin |
|
d867021d8ac1
Preparing the generalized lifting procedure
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
4 |
|
|
1316
0577afdb1732
Porting from Lift to Parser; until defining the Quotient type.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1309
diff
changeset
|
5 |
ML {*
|
|
1494
923413256cbb
Clean 'Lift', start working only on exported things in Parser.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1342
diff
changeset
|
6 |
fun lift_thm ctxt thm = |
|
923413256cbb
Clean 'Lift', start working only on exported things in Parser.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1342
diff
changeset
|
7 |
let |
|
923413256cbb
Clean 'Lift', start working only on exported things in Parser.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1342
diff
changeset
|
8 |
fun un_raw name = unprefix "_raw" name handle Fail _ => name |
|
923413256cbb
Clean 'Lift', start working only on exported things in Parser.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1342
diff
changeset
|
9 |
fun add_under names = hd names :: (map (prefix "_") (tl names)) |
|
923413256cbb
Clean 'Lift', start working only on exported things in Parser.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1342
diff
changeset
|
10 |
fun un_raws name = implode (map un_raw (add_under (space_explode "_" name))) |
|
923413256cbb
Clean 'Lift', start working only on exported things in Parser.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1342
diff
changeset
|
11 |
val un_raw_names = rename_vars un_raws |
|
923413256cbb
Clean 'Lift', start working only on exported things in Parser.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1342
diff
changeset
|
12 |
in |
|
923413256cbb
Clean 'Lift', start working only on exported things in Parser.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1342
diff
changeset
|
13 |
un_raw_names (snd (Quotient_Tacs.lifted_attrib (Context.Proof ctxt, thm))) |
|
923413256cbb
Clean 'Lift', start working only on exported things in Parser.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1342
diff
changeset
|
14 |
end |
|
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
|
15 |
*} |
|
1274
d867021d8ac1
Preparing the generalized lifting procedure
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
16 |
|
|
1494
923413256cbb
Clean 'Lift', start working only on exported things in Parser.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1342
diff
changeset
|
17 |
ML {*
|
|
923413256cbb
Clean 'Lift', start working only on exported things in Parser.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1342
diff
changeset
|
18 |
fun quotient_lift_consts_export spec ctxt = |
|
923413256cbb
Clean 'Lift', start working only on exported things in Parser.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1342
diff
changeset
|
19 |
let |
|
923413256cbb
Clean 'Lift', start working only on exported things in Parser.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1342
diff
changeset
|
20 |
val (result, ctxt') = fold_map Quotient_Def.quotient_lift_const spec ctxt; |
|
923413256cbb
Clean 'Lift', start working only on exported things in Parser.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1342
diff
changeset
|
21 |
val (ts_loc, defs_loc) = split_list result; |
|
923413256cbb
Clean 'Lift', start working only on exported things in Parser.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1342
diff
changeset
|
22 |
val morphism = ProofContext.export_morphism ctxt' ctxt; |
|
923413256cbb
Clean 'Lift', start working only on exported things in Parser.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1342
diff
changeset
|
23 |
val ts = map (Morphism.term morphism) ts_loc |
|
923413256cbb
Clean 'Lift', start working only on exported things in Parser.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1342
diff
changeset
|
24 |
val defs = Morphism.fact morphism defs_loc |
|
923413256cbb
Clean 'Lift', start working only on exported things in Parser.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1342
diff
changeset
|
25 |
in |
|
923413256cbb
Clean 'Lift', start working only on exported things in Parser.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1342
diff
changeset
|
26 |
(ts, defs, ctxt') |
|
923413256cbb
Clean 'Lift', start working only on exported things in Parser.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1342
diff
changeset
|
27 |
end |
|
923413256cbb
Clean 'Lift', start working only on exported things in Parser.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1342
diff
changeset
|
28 |
*} |
| 1342 | 29 |
|
|
1280
1f057f8da8aa
Progress with general lifting procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1277
diff
changeset
|
30 |
end |
|
1274
d867021d8ac1
Preparing the generalized lifting procedure
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
31 |