3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 atom_decl ident |
6 atom_decl ident |
7 |
7 |
8 datatype rtrm2 = |
8 (* datatype rtrm2 = |
9 rVr2 "name" |
9 rVr2 "name" |
10 | rAp2 "rtrm2" "rtrm2" |
10 | rAp2 "rtrm2" "rtrm2" |
11 | rLt2 "ras" "rtrm2" --"bind (bv2 l) in (r)" |
11 | rLt2 "ras" "rtrm2" --"bind (bv2 l) in (r)" |
12 and ras = |
12 and ras = |
13 rAs "name" "rtrm2" |
13 rAs "name" "rtrm2" |
14 |
14 |
15 primrec rbv2 where "rbv2 (rAs x t) = {atom x}" |
15 primrec rbv2 where "rbv2 (rAs x t) = {atom x}" |
16 |
|
17 ML {* |
16 ML {* |
18 val thy1 = @{theory}; |
17 val thy1 = @{theory}; |
19 val info = Datatype.the_info @{theory} "Lift.rtrm2" |
18 val info = Datatype.the_info @{theory} "Lift.rtrm2" |
20 val number = 2; (* Number of defined types, rest are unfoldings *) |
19 val number = 2; (* Number of defined types, rest are unfoldings *) |
21 val binds = [[[[]], [[], []], [[], [(SOME @{term rbv2}, 0)]]], |
20 val binds = [[[[]], [[], []], [[], [(SOME @{term rbv2}, 0)]]], |
22 [[[], []]] (*, [[], [[], []]] *) ]; |
21 [[[], []]] (*, [[], [[], []]] *) ]; |
23 val bvs = [(@{term rbv2}, 1)] (* Which type it operates on *) |
22 val bvs = [(@{term rbv2}, 1)] (* Which type it operates on *) |
24 val bv_simps = @{thms rbv2.simps} |
23 val bv_simps = @{thms rbv2.simps} |
25 |
24 |
26 val ntnames = [@{binding trm2}, @{binding as}] |
25 val ntnames = [@{binding trm2}, @{binding as}] |
27 val ncnames = ["Vr2", "Ap2", "Lt2", "As"] |
26 val ncnames = ["Vr2", "Ap2", "Lt2", "As"] *} *) |
28 |
27 |
|
28 (* datatype rkind = |
|
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; |
|
44 val binds = [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ], |
|
45 [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ], |
|
46 [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]]; |
|
47 val bvs = [] |
|
48 val bv_simps = [] |
29 |
49 |
|
50 val ntnames = [@{binding kind}, @{binding ty}, @{binding trm}] |
|
51 val ncnames = ["TYP", "KPI", "TCONST", "TAPP", "TPI", "CONST", "VAR", "APP", "LAM"]*} *) |
30 |
52 |
|
53 datatype rtrm5 = |
|
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" |
|
60 |
|
61 primrec |
|
62 rbv5 |
|
63 where |
|
64 "rbv5 rLnil = {}" |
|
65 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)" |
|
66 |
|
67 ML {* |
|
68 val thy1 = @{theory}; |
|
69 val info = Datatype.the_info @{theory} "Lift.rtrm5" |
|
70 val number = 2; |
|
71 val binds = [ [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]] ] |
|
72 val bvs = [(@{term rbv5}, 1)] |
|
73 val bv_simps = @{thms rbv5.simps} |
|
74 |
|
75 val ntnames = [@{binding trm5}, @{binding lts}] |
|
76 val ncnames = ["Vr5", "Ap5", "Lt5", "Lnil", "Lcons"] |
31 |
77 |
32 val descr = #descr info; |
78 val descr = #descr info; |
33 val sorts = #sorts info; |
79 val sorts = #sorts info; |
34 val nos = map fst descr |
80 val nos = map fst descr |
35 val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) nos |
81 val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) nos |
86 val bvs_rsp = flat (map snd bvs_rsp') |
132 val bvs_rsp = flat (map snd bvs_rsp') |
87 val (const_rsps, lthy9) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
133 val (const_rsps, lthy9) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
88 (fn _ => constr_rsp_tac alpha_inj (fv_rsp @ bvs_rsp) alpha_equivp 1)) consts lthy8 |
134 (fn _ => constr_rsp_tac alpha_inj (fv_rsp @ bvs_rsp) alpha_equivp 1)) consts lthy8 |
89 val (perms_rsp, lthy10) = prove_const_rsp Binding.empty perms |
135 val (perms_rsp, lthy10) = prove_const_rsp Binding.empty perms |
90 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy9; |
136 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy9; |
91 val lift_induct = snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy1, induct)); |
137 val thy3 = Local_Theory.exit_global lthy10; |
92 val lthy11 = snd (Local_Theory.note ((@{binding lift_induct}, []), [lift_induct]) lthy10) |
138 val lthy11 = Theory_Target.init NONE thy3; |
|
139 val lift_induct = snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy11, induct)); |
|
140 val lthy12 = snd (Local_Theory.note ((@{binding lift_induct}, []), [lift_induct]) lthy11) |
93 *} |
141 *} |
94 |
142 |
95 setup {* fn _ => Local_Theory.exit_global lthy11 *} |
143 setup {* fn _ => Local_Theory.exit_global lthy12 *} |
96 thm lift_induct |
144 thm lift_induct |
97 |
145 |
98 end |
146 end |
99 |
147 |