23 val bv_simps = @{thms rbv2.simps} |
23 val bv_simps = @{thms rbv2.simps} |
24 |
24 |
25 val ntnames = [@{binding trm2}, @{binding as}] |
25 val ntnames = [@{binding trm2}, @{binding as}] |
26 val ncnames = ["Vr2", "Ap2", "Lt2", "As"] *} *) |
26 val ncnames = ["Vr2", "Ap2", "Lt2", "As"] *} *) |
27 |
27 |
28 datatype rkind = |
28 (*datatype rkind = |
29 Type |
29 Type |
30 | KPi "rty" "name" "rkind" |
30 | KPi "rty" "name" "rkind" |
31 and rty = |
31 and rty = |
32 TConst "ident" |
32 TConst "ident" |
33 | TApp "rty" "rtrm" |
33 | TApp "rty" "rtrm" |
46 [ [], [], [], [(NONE, 1, 2)]]]; |
46 [ [], [], [], [(NONE, 1, 2)]]]; |
47 val bvs = [] |
47 val bvs = [] |
48 val bv_simps = [] |
48 val bv_simps = [] |
49 |
49 |
50 val ntnames = [@{binding kind}, @{binding ty}, @{binding trm}] |
50 val ntnames = [@{binding kind}, @{binding ty}, @{binding trm}] |
51 val ncnames = ["TYP", "KPI", "TCONST", "TAPP", "TPI", "CONST", "VAR", "APP", "LAM"] |
51 val ncnames = ["TYP", "KPI", "TCONST", "TAPP", "TPI", "CONST", "VAR", "APP", "LAM"]*}*) |
52 |
52 |
53 (*datatype rtrm5 = |
53 datatype rtrm5 = |
54 rVr5 "name" |
54 rVr5 "name" |
55 | rAp5 "rtrm5" "rtrm5" |
55 | rAp5 "rtrm5" "rtrm5" |
56 | rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)" |
56 | rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)" |
57 and rlts = |
57 and rlts = |
58 rLnil |
58 rLnil |
62 rbv5 |
62 rbv5 |
63 where |
63 where |
64 "rbv5 rLnil = {}" |
64 "rbv5 rLnil = {}" |
65 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)" |
65 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)" |
66 |
66 |
67 ML |
67 ML {* |
68 val thy1 = @{theory}; |
68 val thy1 = @{theory}; |
69 val info = Datatype.the_info @{theory} "Lift.rtrm5" |
69 val info = Datatype.the_info @{theory} "Lift.rtrm5" |
70 val number = 2; |
70 val number = 2; |
71 val binds = [ [[], [], [(SOME @{term rbv5}, 0, 1)]], [[], []] ] |
71 val binds = [ [[], [], [(SOME @{term rbv5}, 0, 1)]], [[], []] ] |
72 val bvs = [(@{term rbv5}, 1)] |
72 val bvs = [(@{term rbv5}, 1)] |
73 val bv_simps = @{thms rbv5.simps} |
73 val bv_simps = @{thms rbv5.simps} |
74 |
74 |
75 val ntnames = [@{binding trm5}, @{binding lts}] |
75 val ntnames = [@{binding trm5}, @{binding lts}] |
76 val ncnames = ["Vr5", "Ap5", "Lt5", "Lnil", "Lcons"]*) |
76 val ncnames = ["Vr5", "Ap5", "Lt5", "Lnil", "Lcons"] |
77 |
77 |
78 |
78 |
79 val descr = #descr info; |
79 val descr = #descr info; |
80 val sorts = #sorts info; |
80 val sorts = #sorts info; |
81 val nos = map fst descr |
81 val nos = map fst descr |