|
1 (* Title: nominal_basic.ML |
|
2 Author: Christian Urban |
|
3 |
|
4 Basic functions for nominal. |
|
5 *) |
|
6 |
|
7 signature NOMINAL_BASIC = |
|
8 sig |
|
9 val trace: bool Unsynchronized.ref |
|
10 val trace_msg: (unit -> string) -> unit |
|
11 |
|
12 val last2: 'a list -> 'a * 'a |
|
13 val split_last2: 'a list -> 'a list * 'a * 'a |
|
14 val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list |
|
15 val order_default: ('a * 'a -> bool) -> 'b -> 'a list -> ('a * 'b) list -> 'b list |
|
16 val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list |
|
17 val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list |
|
18 val split_filter: ('a -> bool) -> 'a list -> 'a list * 'a list |
|
19 val fold_left: ('a * 'a -> 'a) -> 'a list -> 'a -> 'a |
|
20 |
|
21 val is_true: term -> bool |
|
22 |
|
23 val dest_listT: typ -> typ |
|
24 val dest_fsetT: typ -> typ |
|
25 |
|
26 val mk_id: term -> term |
|
27 val mk_all: (string * typ) -> term -> term |
|
28 val mk_All: (string * typ) -> term -> term |
|
29 val mk_exists: (string * typ) -> term -> term |
|
30 |
|
31 val sum_case_const: typ -> typ -> typ -> term |
|
32 val mk_sum_case: term -> term -> term |
|
33 |
|
34 val mk_equiv: thm -> thm |
|
35 val safe_mk_equiv: thm -> thm |
|
36 |
|
37 val mk_minus: term -> term |
|
38 val mk_plus: term -> term -> term |
|
39 |
|
40 val perm_ty: typ -> typ |
|
41 val perm_const: typ -> term |
|
42 val mk_perm_ty: typ -> term -> term -> term |
|
43 val mk_perm: term -> term -> term |
|
44 val dest_perm: term -> term * term |
|
45 |
|
46 end |
|
47 |
|
48 |
|
49 structure Nominal_Basic: NOMINAL_BASIC = |
|
50 struct |
|
51 |
|
52 val trace = Unsynchronized.ref false |
|
53 fun trace_msg msg = if ! trace then tracing (msg ()) else () |
|
54 |
|
55 |
|
56 (* orders an AList according to keys - every key needs to be there *) |
|
57 fun order eq keys list = |
|
58 map (the o AList.lookup eq list) keys |
|
59 |
|
60 (* orders an AList according to keys - returns default for non-existing keys *) |
|
61 fun order_default eq default keys list = |
|
62 map (the_default default o AList.lookup eq list) keys |
|
63 |
|
64 (* remove duplicates *) |
|
65 fun remove_dups eq [] = [] |
|
66 | remove_dups eq (x :: xs) = |
|
67 if member eq xs x |
|
68 then remove_dups eq xs |
|
69 else x :: remove_dups eq xs |
|
70 |
|
71 fun last2 [] = raise Empty |
|
72 | last2 [_] = raise Empty |
|
73 | last2 [x, y] = (x, y) |
|
74 | last2 (_ :: xs) = last2 xs |
|
75 |
|
76 fun split_last2 xs = |
|
77 let |
|
78 val (xs', x) = split_last xs |
|
79 val (xs'', y) = split_last xs' |
|
80 in |
|
81 (xs'', y, x) |
|
82 end |
|
83 |
|
84 fun map4 _ [] [] [] [] = [] |
|
85 | map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us |
|
86 |
|
87 fun split_filter f [] = ([], []) |
|
88 | split_filter f (x :: xs) = |
|
89 let |
|
90 val (r, l) = split_filter f xs |
|
91 in |
|
92 if f x |
|
93 then (x :: r, l) |
|
94 else (r, x :: l) |
|
95 end |
|
96 |
|
97 (* to be used with left-infix binop-operations *) |
|
98 fun fold_left f [] z = z |
|
99 | fold_left f [x] z = x |
|
100 | fold_left f (x :: y :: xs) z = fold_left f (f (x, y) :: xs) z |
|
101 |
|
102 |
|
103 |
|
104 fun is_true @{term "Trueprop True"} = true |
|
105 | is_true _ = false |
|
106 |
|
107 fun dest_listT (Type (@{type_name list}, [T])) = T |
|
108 | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], []) |
|
109 |
|
110 fun dest_fsetT (Type (@{type_name fset}, [T])) = T |
|
111 | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); |
|
112 |
|
113 |
|
114 fun mk_id trm = HOLogic.id_const (fastype_of trm) $ trm |
|
115 |
|
116 fun mk_all (a, T) t = Term.all T $ Abs (a, T, t) |
|
117 |
|
118 fun mk_All (a, T) t = HOLogic.all_const T $ Abs (a, T, t) |
|
119 |
|
120 fun mk_exists (a, T) t = HOLogic.exists_const T $ Abs (a, T, t) |
|
121 |
|
122 fun sum_case_const ty1 ty2 ty3 = |
|
123 Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3) |
|
124 |
|
125 fun mk_sum_case trm1 trm2 = |
|
126 let |
|
127 val ([ty1], ty3) = strip_type (fastype_of trm1) |
|
128 val ty2 = domain_type (fastype_of trm2) |
|
129 in |
|
130 sum_case_const ty1 ty2 ty3 $ trm1 $ trm2 |
|
131 end |
|
132 |
|
133 |
|
134 fun mk_equiv r = r RS @{thm eq_reflection}; |
|
135 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; |
|
136 |
|
137 |
|
138 fun mk_minus p = @{term "uminus::perm => perm"} $ p |
|
139 |
|
140 fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q |
|
141 |
|
142 fun perm_ty ty = @{typ "perm"} --> ty --> ty |
|
143 fun perm_const ty = Const (@{const_name "permute"}, perm_ty ty) |
|
144 fun mk_perm_ty ty p trm = perm_const ty $ p $ trm |
|
145 fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm |
|
146 |
|
147 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) |
|
148 | dest_perm t = raise TERM ("dest_perm", [t]); |
|
149 |
|
150 end (* structure *) |
|
151 |
|
152 open Nominal_Basic; |