32 @{term "uminus::perm => perm"} $ p |
32 @{term "uminus::perm => perm"} $ p |
33 |
33 |
34 fun mk_plus p q = |
34 fun mk_plus p q = |
35 @{term "plus::perm => perm => perm"} $ p $ q |
35 @{term "plus::perm => perm => perm"} $ p $ q |
36 |
36 |
37 fun perm_ty ty = @{typ perm} --> ty --> ty |
37 fun perm_ty ty = @{typ "perm"} --> ty --> ty |
38 |
|
39 fun mk_perm_ty ty p trm = |
38 fun mk_perm_ty ty p trm = |
40 Const (@{const_name "permute"}, perm_ty ty) $ p $ trm |
39 Const (@{const_name "permute"}, perm_ty ty) $ p $ trm |
41 |
|
42 fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm |
40 fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm |
43 |
41 |
44 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) |
42 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) |
45 | dest_perm t = raise TERM ("dest_perm", [t]) |
43 | dest_perm t = raise TERM ("dest_perm", [t]) |
46 |
44 |
47 |
45 |
48 fun mk_sort_of t = @{term "sort_of"} $ t; |
46 fun mk_sort_of t = @{term "sort_of"} $ t; |
49 |
47 |
50 fun mk_atom_ty T t = Const (@{const_name atom}, T --> @{typ atom}) $ t; |
48 fun atom_ty ty = ty --> @{typ "atom"} |
|
49 fun mk_atom_ty ty t = Const (@{const_name "atom"}, atom_ty ty) $ t; |
51 fun mk_atom t = mk_atom_ty (fastype_of t) t; |
50 fun mk_atom t = mk_atom_ty (fastype_of t) t; |
52 |
51 |
53 fun mk_equiv r = r RS @{thm eq_reflection}; |
52 fun mk_equiv r = r RS @{thm eq_reflection}; |
54 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; |
53 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; |
55 |
54 |