51 "(x, y, z)" == "(x, (y, z))" |
51 "(x, y, z)" == "(x, (y, z))" |
52 "(x, y)" == "Pair x y" |
52 "(x, y)" == "Pair x y" |
53 |
53 |
54 "%(x,y,zs).b" == "split(%x (y,zs).b)" |
54 "%(x,y,zs).b" == "split(%x (y,zs).b)" |
55 "%(x,y).b" == "split(%x y.b)" |
55 "%(x,y).b" == "split(%x y.b)" |
56 (*<<<<<<< Prod.thy*) |
|
57 (* The <= direction fails if split has more than one argument because |
|
58 ast-matching fails. Otherwise it would work fine *) |
|
59 |
|
60 (*=======*) |
|
61 |
56 |
62 "SIGMA x:A. B" => "Sigma A (%x.B)" |
57 "SIGMA x:A. B" => "Sigma A (%x.B)" |
63 "A Times B" => "Sigma A (_K B)" |
58 "A Times B" => "Sigma A (_K B)" |
64 |
59 |
65 (*>>>>>>> 1.13*) |
|
66 defs |
60 defs |
67 Pair_def "Pair a b == Abs_Prod(Pair_Rep a b)" |
61 Pair_def "Pair a b == Abs_Prod(Pair_Rep a b)" |
68 fst_def "fst(p) == @a. ? b. p = (a, b)" |
62 fst_def "fst(p) == @a. ? b. p = (a, b)" |
69 snd_def "snd(p) == @b. ? a. p = (a, b)" |
63 snd_def "snd(p) == @b. ? a. p = (a, b)" |
70 split_def "split == (%c p. c (fst p) (snd p))" |
64 split_def "split == (%c p. c (fst p) (snd p))" |
84 |
78 |
85 (* start 8bit 1 *) |
79 (* start 8bit 1 *) |
86 (* end 8bit 1 *) |
80 (* end 8bit 1 *) |
87 |
81 |
88 end |
82 end |
89 (*<<<<<<< Prod.thy*) |
|
90 (* |
|
91 ML |
|
92 |
|
93 local open Syntax |
|
94 |
|
95 fun pttrn(_ $ s $ t) = const"@pttrn" $ s $ t; |
|
96 fun pttrns s t = const"@pttrns" $ s $ t; |
|
97 |
|
98 fun split2(Abs(x,T,t)) = |
|
99 let val (pats,u) = split1 t |
|
100 in (pttrns (Free(x,T)) pats, subst_bounds([free x],u)) end |
|
101 | split2(Const("split",_) $ r) = |
|
102 let val (pats,s) = split2(r) |
|
103 val (pats2,t) = split1(s) |
|
104 in (pttrns (pttrn pats) pats2, t) end |
|
105 and split1(Abs(x,T,t)) = (Free(x,T), subst_bounds([free x],t)) |
|
106 | split1(Const("split",_)$t) = split2(t); |
|
107 |
|
108 fun split_tr'(t::args) = |
|
109 let val (pats,ft) = split2(t) |
|
110 in list_comb(const"_lambda" $ pttrn pats $ ft, args) end; |
|
111 |
|
112 in |
|
113 |
|
114 val print_translation = [("split", split_tr')]; |
|
115 |
|
116 end; |
|
117 *) |
|
118 (*=======*) |
|
119 |
83 |
120 ML |
84 ML |
121 |
85 |
122 val print_translation = [("Sigma", dependent_tr' ("@Sigma", "@Times"))]; |
86 val print_translation = [("Sigma", dependent_tr' ("@Sigma", "@Times"))]; |
123 |
|
124 (*>>>>>>> 1.13*) |
|