1274
|
1 |
theory Lift
|
1280
|
2 |
imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"
|
1274
|
3 |
begin
|
|
4 |
|
|
5 |
atom_decl name
|
|
6 |
atom_decl ident
|
|
7 |
|
1282
|
8 |
(* datatype rtrm2 =
|
1274
|
9 |
rVr2 "name"
|
1280
|
10 |
| rAp2 "rtrm2" "rtrm2"
|
1274
|
11 |
| rLt2 "ras" "rtrm2" --"bind (bv2 l) in (r)"
|
|
12 |
and ras =
|
|
13 |
rAs "name" "rtrm2"
|
|
14 |
|
|
15 |
primrec rbv2 where "rbv2 (rAs x t) = {atom x}"
|
1280
|
16 |
ML {*
|
|
17 |
val thy1 = @{theory};
|
|
18 |
val info = Datatype.the_info @{theory} "Lift.rtrm2"
|
|
19 |
val number = 2; (* Number of defined types, rest are unfoldings *)
|
|
20 |
val binds = [[[[]], [[], []], [[], [(SOME @{term rbv2}, 0)]]],
|
|
21 |
[[[], []]] (*, [[], [[], []]] *) ];
|
|
22 |
val bvs = [(@{term rbv2}, 1)] (* Which type it operates on *)
|
|
23 |
val bv_simps = @{thms rbv2.simps}
|
1274
|
24 |
|
1280
|
25 |
val ntnames = [@{binding trm2}, @{binding as}]
|
1282
|
26 |
val ncnames = ["Vr2", "Ap2", "Lt2", "As"] *} *)
|
|
27 |
|
1303
c28403308b34
More fixes for new alpha, the whole lift script should now work again.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
28 |
datatype rkind =
|
1282
|
29 |
Type
|
|
30 |
| KPi "rty" "name" "rkind"
|
|
31 |
and rty =
|
|
32 |
TConst "ident"
|
|
33 |
| TApp "rty" "rtrm"
|
|
34 |
| TPi "rty" "name" "rty"
|
|
35 |
and rtrm =
|
|
36 |
Const "ident"
|
|
37 |
| Var "name"
|
|
38 |
| App "rtrm" "rtrm"
|
|
39 |
| Lam "rty" "name" "rtrm"
|
|
40 |
ML {*
|
|
41 |
val thy1 = @{theory};
|
|
42 |
val info = Datatype.the_info @{theory} "Lift.rkind"
|
|
43 |
val number = 3;
|
1303
c28403308b34
More fixes for new alpha, the whole lift script should now work again.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
44 |
val binds = [[ [], [(NONE, 1, 2)]],
|
c28403308b34
More fixes for new alpha, the whole lift script should now work again.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
45 |
[ [], [], [(NONE, 1, 2)] ],
|
c28403308b34
More fixes for new alpha, the whole lift script should now work again.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
46 |
[ [], [], [], [(NONE, 1, 2)]]];
|
1282
|
47 |
val bvs = []
|
|
48 |
val bv_simps = []
|
1280
|
49 |
|
1282
|
50 |
val ntnames = [@{binding kind}, @{binding ty}, @{binding trm}]
|
1303
c28403308b34
More fixes for new alpha, the whole lift script should now work again.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
51 |
val ncnames = ["TYP", "KPI", "TCONST", "TAPP", "TPI", "CONST", "VAR", "APP", "LAM"]
|
1280
|
52 |
|
1303
c28403308b34
More fixes for new alpha, the whole lift script should now work again.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
53 |
(*datatype rtrm5 =
|
1282
|
54 |
rVr5 "name"
|
|
55 |
| rAp5 "rtrm5" "rtrm5"
|
|
56 |
| rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)"
|
|
57 |
and rlts =
|
|
58 |
rLnil
|
|
59 |
| rLcons "name" "rtrm5" "rlts"
|
1274
|
60 |
|
1282
|
61 |
primrec
|
|
62 |
rbv5
|
|
63 |
where
|
|
64 |
"rbv5 rLnil = {}"
|
|
65 |
| "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
|
|
66 |
|
1303
c28403308b34
More fixes for new alpha, the whole lift script should now work again.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
67 |
ML
|
1282
|
68 |
val thy1 = @{theory};
|
|
69 |
val info = Datatype.the_info @{theory} "Lift.rtrm5"
|
|
70 |
val number = 2;
|
1303
c28403308b34
More fixes for new alpha, the whole lift script should now work again.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
71 |
val binds = [ [[], [], [(SOME @{term rbv5}, 0, 1)]], [[], []] ]
|
1282
|
72 |
val bvs = [(@{term rbv5}, 1)]
|
|
73 |
val bv_simps = @{thms rbv5.simps}
|
|
74 |
|
|
75 |
val ntnames = [@{binding trm5}, @{binding lts}]
|
1303
c28403308b34
More fixes for new alpha, the whole lift script should now work again.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
76 |
val ncnames = ["Vr5", "Ap5", "Lt5", "Lnil", "Lcons"]*)
|
c28403308b34
More fixes for new alpha, the whole lift script should now work again.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
77 |
|
1274
|
78 |
|
|
79 |
val descr = #descr info;
|
1280
|
80 |
val sorts = #sorts info;
|
|
81 |
val nos = map fst descr
|
|
82 |
val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) nos
|
|
83 |
val typs = List.take (all_typs, number)
|
1274
|
84 |
val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
|
1280
|
85 |
val full_tnames = List.take (all_full_tnames, number);
|
1274
|
86 |
val induct = #induct info;
|
|
87 |
val inducts = #inducts info;
|
1280
|
88 |
val infos = map (Datatype.the_info thy1) all_full_tnames;
|
1274
|
89 |
val inject = flat (map #inject infos);
|
|
90 |
val distinct = flat (map #distinct infos);
|
1280
|
91 |
val ((raw_perm_def, raw_perm_simps, perms), thy2) = define_raw_perms info number thy1;
|
1274
|
92 |
val lthy1 = Theory_Target.init NONE thy2
|
1280
|
93 |
val (((fv_ts_loc, fv_def_loc), alpha), lthy2) = define_fv_alpha info binds lthy1;
|
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>
diff
changeset
|
94 |
val alpha_ts_loc = #preds alpha
|
1274
|
95 |
val alpha_intros = #intrs alpha
|
|
96 |
val alpha_cases = #elims alpha
|
1280
|
97 |
val alpha_induct_loc = #induct alpha
|
|
98 |
val [alpha_induct] = ProofContext.export lthy2 lthy1 [alpha_induct_loc]
|
|
99 |
(* TODO replace when inducts is provided by the 2 lines below: *)
|
|
100 |
val alpha_inducts = Project_Rule.projects lthy2 (1 upto number) alpha_induct
|
|
101 |
(*val alpha_inducts_loc = #inducts alpha
|
|
102 |
val alpha_inducts = ProofContext.export lthy2 lthy1 alpha_inducts_loc*)
|
|
103 |
val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases lthy2
|
|
104 |
val alpha_inj = ProofContext.export lthy2 lthy1 alpha_inj_loc
|
1274
|
105 |
val fv_def = ProofContext.export lthy2 lthy1 fv_def_loc
|
|
106 |
val morphism = ProofContext.export_morphism lthy2 lthy1
|
|
107 |
val fv_ts = map (Morphism.term morphism) fv_ts_loc
|
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>
diff
changeset
|
108 |
val alpha_ts = map (Morphism.term morphism) alpha_ts_loc
|
1280
|
109 |
fun build_bv_eqvt (t, n) =
|
|
110 |
build_eqvts Binding.empty [t] [nth perms n]
|
|
111 |
(bv_simps @ raw_perm_def) (nth inducts n)
|
|
112 |
val (bv_eqvts, lthy3) = fold_map build_bv_eqvt bvs lthy2;
|
|
113 |
val (fv_eqvts, lthy4) = build_eqvts Binding.empty fv_ts_loc perms (fv_def_loc @ raw_perm_def) induct lthy3;
|
|
114 |
val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy4;
|
1303
c28403308b34
More fixes for new alpha, the whole lift script should now work again.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
115 |
val alpha_eqvt = ProofContext.export lthy4 lthy1 alpha_eqvt_loc;
|
1280
|
116 |
val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc inject alpha_inj_loc distinct alpha_cases alpha_eqvt_loc lthy4;
|
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>
diff
changeset
|
117 |
val alpha_equivp = ProofContext.export lthy4 lthy1 alpha_equivp_loc
|
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>
diff
changeset
|
118 |
val lthy5 = define_quotient_type
|
1280
|
119 |
(map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((ntnames ~~ typs) ~~ alpha_ts))
|
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>
diff
changeset
|
120 |
(ALLGOALS (resolve_tac alpha_equivp)) lthy4;
|
1280
|
121 |
val consts =
|
|
122 |
flat (map (fn (i, (_, _, l)) =>
|
|
123 |
map (fn (cname, dts) =>
|
|
124 |
Const (cname, map (typ_of_dtyp descr sorts) dts --->
|
|
125 |
typ_of_dtyp descr sorts (DtRec i))) l) descr);
|
|
126 |
val (csdefl, lthy6) = fold_map Quotient_Def.quotient_lift_const (ncnames ~~ consts) lthy5;
|
|
127 |
val (cs, def) = split_list csdefl;
|
1303
c28403308b34
More fixes for new alpha, the whole lift script should now work again.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
128 |
val (bvs_rsp', lthy7) = fold_map (
|
1280
|
129 |
fn (bv_t, i) => prove_const_rsp Binding.empty [bv_t]
|
1303
c28403308b34
More fixes for new alpha, the whole lift script should now work again.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
130 |
(fn _ => fvbv_rsp_tac (nth alpha_inducts i) bv_simps 1)) bvs lthy6;
|
c28403308b34
More fixes for new alpha, the whole lift script should now work again.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
131 |
val ((_, fv_rsp), lthy8) = prove_const_rsp Binding.empty fv_ts
|
c28403308b34
More fixes for new alpha, the whole lift script should now work again.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
132 |
(fn _ => fvbv_rsp_tac alpha_induct fv_def 1) lthy7;
|
c28403308b34
More fixes for new alpha, the whole lift script should now work again.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
133 |
val bvs_rsp = flat (map snd bvs_rsp');
|
1280
|
134 |
val (const_rsps, lthy9) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
|
|
135 |
(fn _ => constr_rsp_tac alpha_inj (fv_rsp @ bvs_rsp) alpha_equivp 1)) consts lthy8
|
|
136 |
val (perms_rsp, lthy10) = prove_const_rsp Binding.empty perms
|
|
137 |
(fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy9;
|
1282
|
138 |
val thy3 = Local_Theory.exit_global lthy10;
|
1291
|
139 |
(* TODO: fix this hack... *)
|
1303
c28403308b34
More fixes for new alpha, the whole lift script should now work again.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
140 |
(*val tinfo = #abs_type (Typedef.the_info thy3 "Lift.trm5");*)
|
1291
|
141 |
(*val thy4 = define_lifted_perms ["Term1.trm1"] [("permute_trm1", @{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"})]
|
|
142 |
@{thms permute_rtrm1_permute_bp_zero permute_rtrm1_permute_bp_append}*)
|
1282
|
143 |
val lthy11 = Theory_Target.init NONE thy3;
|
|
144 |
val lift_induct = snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy11, induct));
|
1291
|
145 |
val lthy12 = snd (Local_Theory.note ((@{binding lift_induct}, []), [lift_induct]) lthy11);
|
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>
diff
changeset
|
146 |
*}
|
1274
|
147 |
|
1282
|
148 |
setup {* fn _ => Local_Theory.exit_global lthy12 *}
|
1280
|
149 |
thm lift_induct
|
1274
|
150 |
|
1280
|
151 |
end
|
1274
|
152 |
|