24 fun freetvar s = if (mk_tvar s) mem typevars then freetvar ("t"^s) else mk_tvar s; |
24 fun freetvar s = if (mk_tvar s) mem typevars then freetvar ("t"^s) else mk_tvar s; |
25 fun when_type (_ ,_,args) = foldr (op ~>) (map third args,freetvar "t"); |
25 fun when_type (_ ,_,args) = foldr (op ~>) (map third args,freetvar "t"); |
26 in |
26 in |
27 val dtype = Type(dname,typevars); |
27 val dtype = Type(dname,typevars); |
28 val dtype2 = foldr' (mk_typ "++") (map prod cons'); |
28 val dtype2 = foldr' (mk_typ "++") (map prod cons'); |
29 val const_rep = (dname^"_rep" , dtype ~> dtype2, NoSyn'); |
29 val dnam = Sign.base_name dname; |
30 val const_abs = (dname^"_abs" , dtype2 ~> dtype , NoSyn'); |
30 val const_rep = (dnam^"_rep" , dtype ~> dtype2, NoSyn'); |
31 val const_when = (dname^"_when", foldr (op ~>) ((map when_type cons'), |
31 val const_abs = (dnam^"_abs" , dtype2 ~> dtype , NoSyn'); |
32 dtype ~> freetvar "t"), NoSyn'); |
32 val const_when = (dnam^"_when", foldr (op ~>) ((map when_type cons'), |
33 val const_copy = (dname^"_copy", dtypeprod ~> dtype ~> dtype , NoSyn'); |
33 dtype ~> freetvar "t"), NoSyn'); |
|
34 val const_copy = (dnam^"_copy", dtypeprod ~> dtype ~> dtype , NoSyn'); |
34 end; |
35 end; |
35 |
36 |
36 (* ----- constants concerning the constructors, discriminators and selectors ------ *) |
37 (* ----- constants concerning the constructors, discriminators and selectors ------ *) |
37 |
38 |
38 fun is_infix (ThyOps.CInfixl _ ) = true |
39 fun is_infix (ThyOps.CInfixl _ ) = true |
58 val consts_sel = flat(map sel cons'); |
59 val consts_sel = flat(map sel cons'); |
59 end; |
60 end; |
60 |
61 |
61 (* ----- constants concerning induction ------------------------------------------- *) |
62 (* ----- constants concerning induction ------------------------------------------- *) |
62 |
63 |
63 val const_take = (dname^"_take" , Type("nat",[]) --> dtype ~> dtype, NoSyn'); |
64 val const_take = (dnam^"_take" , Type("nat",[]) --> dtype ~> dtype, NoSyn'); |
64 val const_finite = (dname^"_finite", dtype-->HOLogic.boolT , NoSyn'); |
65 val const_finite = (dnam^"_finite", dtype-->HOLogic.boolT , NoSyn'); |
65 |
66 |
66 (* ----- case translation --------------------------------------------------------- *) |
67 (* ----- case translation --------------------------------------------------------- *) |
67 |
68 |
68 local open Syntax in |
69 local open Syntax in |
69 val case_trans = let |
70 val case_trans = let |
84 (mk_appl (Constant "@case") [Variable "x", foldr' |
85 (mk_appl (Constant "@case") [Variable "x", foldr' |
85 (fn (c,cs) => mk_appl (Constant "@case2") [c,cs]) |
86 (fn (c,cs) => mk_appl (Constant "@case2") [c,cs]) |
86 (mapn case1 1 cons')], |
87 (mapn case1 1 cons')], |
87 mk_appl (Constant "@fapp") [foldl |
88 mk_appl (Constant "@fapp") [foldl |
88 (fn (w,a ) => mk_appl (Constant "@fapp" ) [w,a ]) |
89 (fn (w,a ) => mk_appl (Constant "@fapp" ) [w,a ]) |
89 (Constant (dname^"_when"),mapn arg1 1 cons'), |
90 (Constant (dnam^"_when"),mapn arg1 1 cons'), |
90 Variable "x"]) |
91 Variable "x"]) |
91 end; |
92 end; |
92 end; |
93 end; |
93 |
94 |
94 in ([const_rep, const_abs, const_when, const_copy] @ |
95 in ([const_rep, const_abs, const_when, const_copy] @ |
99 |
100 |
100 (* ----- putting all the syntax stuff together ------------------------------------ *) |
101 (* ----- putting all the syntax stuff together ------------------------------------ *) |
101 |
102 |
102 in (* local *) |
103 in (* local *) |
103 |
104 |
104 fun add_syntax (comp_dname,eqs': ((string * typ list) * |
105 fun add_syntax (comp_dnam,eqs': ((string * typ list) * |
105 (string * ThyOps.cmixfix * (bool*string*typ) list) list) list) thy'' = |
106 (string * ThyOps.cmixfix * (bool*string*typ) list) list) list) thy'' = |
106 let |
107 let |
107 fun thy_type (dname,tvars) = (dname, length tvars, NoSyn); |
108 val dtypes = map (Type o fst) eqs'; |
108 fun thy_arity (dname,tvars) = (dname, map (snd o rep_TFree) tvars, ["pcpo"]); |
|
109 val thy_types = map (thy_type o fst) eqs'; |
|
110 val thy_arities = map (thy_arity o fst) eqs'; |
|
111 val dtypes = map (Type o fst) eqs'; |
|
112 val funprod = foldr' (mk_typ "*") (map (fn tp => tp ~> tp )dtypes); |
109 val funprod = foldr' (mk_typ "*") (map (fn tp => tp ~> tp )dtypes); |
113 val relprod = foldr' (mk_typ "*") (map (fn tp => tp--> tp --> HOLogic.boolT)dtypes); |
110 val relprod = foldr' (mk_typ "*") (map (fn tp => tp--> tp --> HOLogic.boolT)dtypes); |
114 val const_copy = (comp_dname^"_copy" ,funprod ~> funprod , NoSyn'); |
111 val const_copy = (comp_dnam^"_copy" ,funprod ~> funprod , NoSyn'); |
115 val const_bisim = (comp_dname^"_bisim" ,relprod --> HOLogic.boolT, NoSyn'); |
112 val const_bisim = (comp_dnam^"_bisim" ,relprod --> HOLogic.boolT, NoSyn'); |
116 val ctt = map (calc_syntax funprod) eqs'; |
113 val ctt = map (calc_syntax funprod) eqs'; |
117 val add_cur_ops_i = ThyOps.add_ops_i {curried=true, strict=false, total=false}; |
114 val add_cur_ops_i = ThyOps.add_ops_i {curried=true, strict=false, total=false}; |
118 in thy'' |> Theory.add_types thy_types |
115 in thy'' |> add_cur_ops_i (flat(map fst ctt)) |
119 |> Theory.add_arities_i thy_arities |
|
120 |> add_cur_ops_i (flat(map fst ctt)) |
|
121 |> add_cur_ops_i ((if length eqs'>1 then [const_copy] else[])@[const_bisim]) |
116 |> add_cur_ops_i ((if length eqs'>1 then [const_copy] else[])@[const_bisim]) |
122 |> Theory.add_trrules_i (flat(map snd ctt)) |
117 |> Theory.add_trrules_i (flat(map snd ctt)) |
123 end; (* let *) |
118 end; (* let *) |
124 |
119 |
125 end; (* local *) |
120 end; (* local *) |