equal
deleted
inserted
replaced
1 theory Lift |
1 theory Lift |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" |
3 begin |
3 begin |
4 |
4 |
|
5 |
5 ML {* |
6 ML {* |
6 fun define_quotient_type args tac ctxt = |
7 fun define_quotient_types binds tys alphas equivps ctxt = |
7 let |
8 let |
8 val mthd = Method.SIMPLE_METHOD tac |
9 fun def_ty ((b, ty), (alpha, equivp)) ctxt = |
9 val mthdt = Method.Basic (fn _ => mthd) |
10 Quotient_Type.add_quotient_type ((([], b, NoSyn), (ty, alpha)), equivp) ctxt; |
10 val bymt = Proof.global_terminal_proof (mthdt, NONE) |
11 val alpha_equivps = List.take (equivps, length alphas) |
|
12 val (thms, ctxt') = fold_map def_ty ((binds ~~ tys) ~~ (alphas ~~ alpha_equivps)) ctxt; |
|
13 val quot_thms = map fst thms; |
|
14 val quots = map (HOLogic.dest_Trueprop o prop_of) quot_thms; |
|
15 val reps = map (hd o rev o snd o strip_comb) quots; |
|
16 val qtys = map (domain_type o fastype_of) reps; |
11 in |
17 in |
12 bymt (Quotient_Type.quotient_type args ctxt) |
18 (qtys, ctxt') |
13 end |
19 end |
14 *} |
20 *} |
15 |
21 |
16 (* Renames schematic variables in a theorem *) |
22 (* Renames schematic variables in a theorem *) |
17 ML {* |
23 ML {* |