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