20 val atom_ty: typ -> typ |
20 val atom_ty: typ -> typ |
21 val mk_atom_ty: typ -> term -> term |
21 val mk_atom_ty: typ -> term -> term |
22 val mk_atom: term -> term |
22 val mk_atom: term -> term |
23 |
23 |
24 val supp_ty: typ -> typ |
24 val supp_ty: typ -> typ |
|
25 val supp_const: typ -> term |
25 val mk_supp_ty: typ -> term -> term |
26 val mk_supp_ty: typ -> term -> term |
26 val mk_supp: term -> term |
27 val mk_supp: term -> term |
27 |
28 |
28 val mk_equiv: thm -> thm |
29 val mk_equiv: thm -> thm |
29 val safe_mk_equiv: thm -> thm |
30 val safe_mk_equiv: thm -> thm |
30 |
31 |
31 val mk_diff: term * term -> term |
32 val mk_diff: term * term -> term |
|
33 val mk_append: term * term -> term |
32 val mk_union: term * term -> term |
34 val mk_union: term * term -> term |
33 val fold_union: term list -> term |
35 val fold_union: term list -> term |
34 |
36 |
35 (* datatype operations *) |
37 (* datatype operations *) |
|
38 val all_dtyps: Datatype_Aux.descr -> (string * sort) list -> typ list |
36 val nth_dtyp: Datatype_Aux.descr -> (string * sort) list -> int -> typ |
39 val nth_dtyp: Datatype_Aux.descr -> (string * sort) list -> int -> typ |
37 val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> |
40 val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> |
38 (term * typ * typ list) list list |
41 (term * typ * typ list * bool list) list list |
39 val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int -> |
42 val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int -> |
40 (term * typ * typ list) list |
43 (term * typ * typ list * bool list) list |
41 val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list |
44 val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list |
42 |
45 |
43 end |
46 end |
44 |
47 |
45 |
48 |
59 fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm; |
62 fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm; |
60 |
63 |
61 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) |
64 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) |
62 | dest_perm t = raise TERM ("dest_perm", [t]); |
65 | dest_perm t = raise TERM ("dest_perm", [t]); |
63 |
66 |
64 |
|
65 fun mk_sort_of t = @{term "sort_of"} $ t; |
67 fun mk_sort_of t = @{term "sort_of"} $ t; |
66 |
68 |
67 fun atom_ty ty = ty --> @{typ "atom"}; |
69 fun atom_ty ty = ty --> @{typ "atom"}; |
68 fun mk_atom_ty ty t = Const (@{const_name "atom"}, atom_ty ty) $ t; |
70 fun mk_atom_ty ty t = Const (@{const_name "atom"}, atom_ty ty) $ t; |
69 fun mk_atom t = mk_atom_ty (fastype_of t) t; |
71 fun mk_atom t = mk_atom_ty (fastype_of t) t; |
70 |
72 |
71 |
73 |
72 fun supp_ty ty = ty --> @{typ "atom set"}; |
74 fun supp_ty ty = ty --> @{typ "atom set"}; |
73 fun mk_supp_ty ty t = Const (@{const_name "supp"}, supp_ty ty) $ t; |
75 fun supp_const ty = Const (@{const_name "supp"}, supp_ty ty) |
|
76 fun mk_supp_ty ty t = supp_const ty $ t; |
74 fun mk_supp t = mk_supp_ty (fastype_of t) t; |
77 fun mk_supp t = mk_supp_ty (fastype_of t) t; |
75 |
78 |
76 |
79 |
77 fun mk_equiv r = r RS @{thm eq_reflection}; |
80 fun mk_equiv r = r RS @{thm eq_reflection}; |
78 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; |
81 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; |
79 |
82 |
80 |
83 |
81 (* functions that construct differences and unions |
84 (* functions that construct differences, appends and unions |
82 but avoid producing empty atom sets *) |
85 but avoid producing empty atom sets or empty atom lists *) |
83 |
86 |
84 fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"} |
87 fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"} |
85 | mk_diff (t1, @{term "{}::atom set"}) = t1 |
88 | mk_diff (t1, @{term "{}::atom set"}) = t1 |
86 | mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2) |
89 | mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2) |
87 |
90 |
|
91 fun mk_append (@{term "[]::atom list"}, @{term "[]::atom list"}) = @{term "[]::atom list"} |
|
92 | mk_append (t1, @{term "[]::atom list"}) = t1 |
|
93 | mk_append (@{term "[]::atom list"}, t2) = t2 |
|
94 | mk_append (t1, t2) = HOLogic.mk_binop @{const_name "append"} (t1, t2) |
|
95 |
88 fun mk_union (@{term "{}::atom set"}, @{term "{}::atom set"}) = @{term "{}::atom set"} |
96 fun mk_union (@{term "{}::atom set"}, @{term "{}::atom set"}) = @{term "{}::atom set"} |
89 | mk_union (t1 , @{term "{}::atom set"}) = t1 |
97 | mk_union (t1 , @{term "{}::atom set"}) = t1 |
90 | mk_union (@{term "{}::atom set"}, t2) = t2 |
98 | mk_union (@{term "{}::atom set"}, t2) = t2 |
91 | mk_union (t1, t2) = HOLogic.mk_binop @{const_name sup} (t1, t2) |
99 | mk_union (t1, t2) = HOLogic.mk_binop @{const_name "sup"} (t1, t2) |
92 |
100 |
93 fun fold_union trms = fold (curry mk_union) trms @{term "{}::atom set"} |
101 fun fold_union trms = fold (curry mk_union) trms @{term "{}::atom set"} |
|
102 |
|
103 |
94 |
104 |
95 |
105 |
96 (** datatypes **) |
106 (** datatypes **) |
97 |
107 |
98 |
108 |
99 (* returns the type of the nth datatype *) |
109 (* returns the type of the nth datatype *) |
|
110 fun all_dtyps descr sorts = |
|
111 map (fn n => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n)) (0 upto (length descr - 1)) |
|
112 |
100 fun nth_dtyp descr sorts n = |
113 fun nth_dtyp descr sorts n = |
101 Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n); |
114 Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n); |
102 |
115 |
103 (* returns info about constructors in a datatype *) |
116 (* returns info about constructors in a datatype *) |
104 fun all_dtyp_constrs_info descr = |
117 fun all_dtyp_constrs_info descr = |
111 fun aux ((ty_name, vs), (cname, args)) = |
124 fun aux ((ty_name, vs), (cname, args)) = |
112 let |
125 let |
113 val vs_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) vs |
126 val vs_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) vs |
114 val ty = Type (ty_name, vs_tys) |
127 val ty = Type (ty_name, vs_tys) |
115 val arg_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) args |
128 val arg_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) args |
|
129 val is_rec = map Datatype_Aux.is_rec_type args |
116 in |
130 in |
117 (Const (cname, arg_tys ---> ty), ty, arg_tys) |
131 (Const (cname, arg_tys ---> ty), ty, arg_tys, is_rec) |
118 end |
132 end |
119 in |
133 in |
120 map (map aux) (all_dtyp_constrs_info descr) |
134 map (map aux) (all_dtyp_constrs_info descr) |
121 end |
135 end |
122 |
136 |