1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
(* Title: nominal_library.ML
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
Author: Christian Urban
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
|
1979
|
4 |
Basic functions for nominal.
|
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
*)
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
6 |
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
7 |
signature NOMINAL_LIBRARY =
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
8 |
sig
|
2593
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
9 |
val last2: 'a list -> 'a * 'a
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
10 |
val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list
|
2608
|
11 |
val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list
|
2480
ac7dff1194e8
introduced a general procedure for structural inductions; simplified reflexivity proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
12 |
|
2593
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
13 |
val is_true: term -> bool
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
14 |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
15 |
val dest_listT: typ -> typ
|
2607
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
16 |
val dest_fsetT: typ -> typ
|
2313
|
17 |
|
2593
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
18 |
val mk_id: term -> term
|
2288
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
19 |
|
2399
|
20 |
val size_const: typ -> term
|
|
21 |
|
2410
2bbdb9c427b5
improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
22 |
val sum_case_const: typ -> typ -> typ -> term
|
2bbdb9c427b5
improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
23 |
val mk_sum_case: term -> term -> term
|
2bbdb9c427b5
improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
24 |
|
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
25 |
val mk_minus: term -> term
|
1896
996d4411e95e
tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
26 |
val mk_plus: term -> term -> term
|
996d4411e95e
tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
27 |
|
1899
|
28 |
val perm_ty: typ -> typ
|
1871
|
29 |
val mk_perm_ty: typ -> term -> term -> term
|
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
30 |
val mk_perm: term -> term -> term
|
1834
|
31 |
val dest_perm: term -> term * term
|
|
32 |
|
1962
84a13d1e2511
moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
33 |
val mk_sort_of: term -> term
|
1979
|
34 |
val atom_ty: typ -> typ
|
2569
94750b31a97d
fixed bug in fv function where a shallow binder binds lists of names
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
35 |
val atom_const: typ -> term
|
1962
84a13d1e2511
moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
36 |
val mk_atom_ty: typ -> term -> term
|
84a13d1e2511
moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
37 |
val mk_atom: term -> term
|
84a13d1e2511
moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
38 |
|
2607
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
39 |
val mk_atom_set_ty: typ -> term -> term
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
40 |
val mk_atom_set: term -> term
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
41 |
val mk_atom_fset_ty: typ -> term -> term
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
42 |
val mk_atom_fset: term -> term
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
43 |
val mk_atom_list_ty: typ -> term -> term
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
44 |
val mk_atom_list: term -> term
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
45 |
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
46 |
val is_atom: Proof.context -> typ -> bool
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
47 |
val is_atom_set: Proof.context -> typ -> bool
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
48 |
val is_atom_fset: Proof.context -> typ -> bool
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
49 |
val is_atom_list: Proof.context -> typ -> bool
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
50 |
|
2608
|
51 |
val to_atom_set: term -> term
|
|
52 |
val to_set_ty: typ -> term -> term
|
|
53 |
val to_set: term -> term
|
|
54 |
|
2607
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
55 |
val setify_ty: Proof.context -> typ -> term -> term
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
56 |
val setify: Proof.context -> term -> term
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
57 |
val listify_ty: Proof.context -> typ -> term -> term
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
58 |
val listify: Proof.context -> term -> term
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
59 |
|
2608
|
60 |
val fresh_star_ty: typ -> typ
|
|
61 |
val fresh_star_const: typ -> term
|
|
62 |
val mk_fresh_star_ty: typ -> term -> term -> term
|
2607
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
63 |
val mk_fresh_star: term -> term -> term
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
64 |
|
1979
|
65 |
val supp_ty: typ -> typ
|
2296
|
66 |
val supp_const: typ -> term
|
1979
|
67 |
val mk_supp_ty: typ -> term -> term
|
|
68 |
val mk_supp: term -> term
|
|
69 |
|
2475
486d4647bb37
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
70 |
val supp_rel_ty: typ -> typ
|
486d4647bb37
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
71 |
val supp_rel_const: typ -> term
|
486d4647bb37
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
72 |
val mk_supp_rel_ty: typ -> term -> term -> term
|
486d4647bb37
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
73 |
val mk_supp_rel: term -> term -> term
|
486d4647bb37
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
74 |
|
2448
|
75 |
val supports_const: typ -> term
|
|
76 |
val mk_supports_ty: typ -> term -> term -> term
|
|
77 |
val mk_supports: term -> term -> term
|
|
78 |
|
2450
|
79 |
val finite_const: typ -> term
|
|
80 |
val mk_finite_ty: typ -> term -> term
|
|
81 |
val mk_finite: term -> term
|
|
82 |
|
1834
|
83 |
val mk_equiv: thm -> thm
|
|
84 |
val safe_mk_equiv: thm -> thm
|
2288
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
85 |
|
2289
|
86 |
val mk_diff: term * term -> term
|
2296
|
87 |
val mk_append: term * term -> term
|
2289
|
88 |
val mk_union: term * term -> term
|
|
89 |
val fold_union: term list -> term
|
2464
f4eba60cbd69
made the fv-definition aggree more with alpha (needed in the support proofs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
90 |
val fold_append: term list -> term
|
2389
|
91 |
val mk_conj: term * term -> term
|
|
92 |
val fold_conj: term list -> term
|
2289
|
93 |
|
2448
|
94 |
(* fresh arguments for a term *)
|
|
95 |
val fresh_args: Proof.context -> term -> term list
|
|
96 |
|
2288
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
97 |
(* datatype operations *)
|
2407
|
98 |
type cns_info = (term * typ * typ list * bool list) list
|
|
99 |
|
2296
|
100 |
val all_dtyps: Datatype_Aux.descr -> (string * sort) list -> typ list
|
2288
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
101 |
val nth_dtyp: Datatype_Aux.descr -> (string * sort) list -> int -> typ
|
2407
|
102 |
val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> cns_info list
|
|
103 |
val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int -> cns_info
|
2288
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
104 |
val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list
|
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
105 |
|
2304
|
106 |
(* tactics for function package *)
|
|
107 |
val pat_completeness_simp: thm list -> Proof.context -> tactic
|
2410
2bbdb9c427b5
improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
108 |
val prove_termination: thm list -> Proof.context -> Function.info * local_theory
|
2304
|
109 |
|
2311
|
110 |
(* transformations of premises in inductions *)
|
|
111 |
val transform_prem1: Proof.context -> string list -> thm -> thm
|
|
112 |
val transform_prem2: Proof.context -> string list -> thm -> thm
|
2397
|
113 |
|
|
114 |
(* transformation into the object logic *)
|
|
115 |
val atomize: thm -> thm
|
2398
|
116 |
|
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
117 |
end
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
118 |
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
119 |
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
120 |
structure Nominal_Library: NOMINAL_LIBRARY =
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
121 |
struct
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
122 |
|
2593
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
123 |
(* orders an AList according to keys *)
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
124 |
fun order eq keys list =
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
125 |
map (the o AList.lookup eq list) keys
|
2480
ac7dff1194e8
introduced a general procedure for structural inductions; simplified reflexivity proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
126 |
|
2608
|
127 |
fun remove_dups eq [] = []
|
|
128 |
| remove_dups eq (x::xs) =
|
|
129 |
if (member eq xs x)
|
|
130 |
then remove_dups eq xs
|
|
131 |
else x::(remove_dups eq xs)
|
|
132 |
|
|
133 |
|
2313
|
134 |
fun last2 [] = raise Empty
|
|
135 |
| last2 [_] = raise Empty
|
2375
|
136 |
| last2 [x, y] = (x, y)
|
2313
|
137 |
| last2 (_ :: xs) = last2 xs
|
|
138 |
|
2593
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
139 |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
140 |
fun is_true @{term "Trueprop True"} = true
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
141 |
| is_true _ = false
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
142 |
|
2288
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
143 |
fun dest_listT (Type (@{type_name list}, [T])) = T
|
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
144 |
| dest_listT T = raise TYPE ("dest_listT: list type expected", [T], [])
|
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
145 |
|
2607
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
146 |
fun dest_fsetT (Type (@{type_name fset}, [T])) = T
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
147 |
| dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
148 |
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
149 |
|
2593
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
150 |
fun mk_id trm =
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
151 |
let
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
152 |
val ty = fastype_of trm
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
153 |
in
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
154 |
Const (@{const_name id}, ty --> ty) $ trm
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
155 |
end
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
156 |
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
157 |
|
2399
|
158 |
fun size_const ty = Const (@{const_name size}, ty --> @{typ nat})
|
1979
|
159 |
|
2410
2bbdb9c427b5
improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
160 |
fun sum_case_const ty1 ty2 ty3 =
|
2bbdb9c427b5
improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
161 |
Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3)
|
2bbdb9c427b5
improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
162 |
fun mk_sum_case trm1 trm2 =
|
2477
|
163 |
let
|
|
164 |
val ([ty1], ty3) = strip_type (fastype_of trm1)
|
|
165 |
val ty2 = domain_type (fastype_of trm2)
|
|
166 |
in
|
|
167 |
sum_case_const ty1 ty2 ty3 $ trm1 $ trm2
|
|
168 |
end
|
2410
2bbdb9c427b5
improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
169 |
|
2bbdb9c427b5
improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
170 |
|
2bbdb9c427b5
improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
171 |
|
2399
|
172 |
fun mk_minus p = @{term "uminus::perm => perm"} $ p
|
1896
996d4411e95e
tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
173 |
|
2399
|
174 |
fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q
|
|
175 |
|
|
176 |
fun perm_ty ty = @{typ "perm"} --> ty --> ty
|
|
177 |
fun mk_perm_ty ty p trm = Const (@{const_name "permute"}, perm_ty ty) $ p $ trm
|
|
178 |
fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm
|
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
179 |
|
1834
|
180 |
fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
|
1979
|
181 |
| dest_perm t = raise TERM ("dest_perm", [t]);
|
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
182 |
|
1962
84a13d1e2511
moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
183 |
fun mk_sort_of t = @{term "sort_of"} $ t;
|
84a13d1e2511
moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
184 |
|
1979
|
185 |
fun atom_ty ty = ty --> @{typ "atom"};
|
2569
94750b31a97d
fixed bug in fv function where a shallow binder binds lists of names
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
186 |
fun atom_const ty = Const (@{const_name "atom"}, atom_ty ty)
|
94750b31a97d
fixed bug in fv function where a shallow binder binds lists of names
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
187 |
fun mk_atom_ty ty t = atom_const ty $ t;
|
1962
84a13d1e2511
moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
188 |
fun mk_atom t = mk_atom_ty (fastype_of t) t;
|
84a13d1e2511
moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
189 |
|
2607
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
190 |
fun mk_atom_set_ty ty t =
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
191 |
let
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
192 |
val atom_ty = HOLogic.dest_setT ty --> @{typ "atom"};
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
193 |
val img_ty = atom_ty --> ty --> @{typ "atom set"};
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
194 |
in
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
195 |
Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
196 |
end
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
197 |
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
198 |
fun mk_atom_fset_ty ty t =
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
199 |
let
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
200 |
val atom_ty = dest_fsetT ty
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
201 |
val fmap_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom fset"};
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
202 |
val fset = @{term "fset :: atom fset => atom set"}
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
203 |
in
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
204 |
fset $ (Const (@{const_name map_fset}, fmap_ty) $ (atom_const atom_ty) $ t)
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
205 |
end
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
206 |
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
207 |
fun mk_atom_list_ty ty t =
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
208 |
let
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
209 |
val atom_ty = dest_listT ty
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
210 |
val map_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom list"}
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
211 |
in
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
212 |
Const (@{const_name map}, map_ty) $ (atom_const atom_ty) $ t
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
213 |
end
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
214 |
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
215 |
fun mk_atom_set t = mk_atom_set_ty (fastype_of t) t
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
216 |
fun mk_atom_fset t = mk_atom_fset_ty (fastype_of t) t
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
217 |
fun mk_atom_list t = mk_atom_list_ty (fastype_of t) t
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
218 |
|
2608
|
219 |
(* coerces a list into a set *)
|
|
220 |
fun to_atom_set t = @{term "set :: atom list => atom set"} $ t
|
|
221 |
|
|
222 |
fun to_set_ty ty t =
|
|
223 |
if ty = @{typ "atom list"}
|
|
224 |
then to_atom_set t else t
|
|
225 |
|
|
226 |
fun to_set t = to_set_ty (fastype_of t) t
|
2607
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
227 |
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
228 |
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
229 |
(* testing for concrete atom types *)
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
230 |
fun is_atom ctxt ty =
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
231 |
Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base})
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
232 |
|
2608
|
233 |
fun is_atom_set ctxt (Type ("fun", [ty, @{typ bool}])) = is_atom ctxt ty
|
2607
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
234 |
| is_atom_set _ _ = false;
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
235 |
|
2608
|
236 |
fun is_atom_fset ctxt (Type (@{type_name "fset"}, [ty])) = is_atom ctxt ty
|
2607
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
237 |
| is_atom_fset _ _ = false;
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
238 |
|
2608
|
239 |
fun is_atom_list ctxt (Type (@{type_name "list"}, [ty])) = is_atom ctxt ty
|
2607
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
240 |
| is_atom_list _ _ = false
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
241 |
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
242 |
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
243 |
(* functions that coerces singletons, sets and fsets of concrete atoms
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
244 |
into sets of general atoms *)
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
245 |
fun setify_ty ctxt ty t =
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
246 |
if is_atom ctxt ty
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
247 |
then HOLogic.mk_set @{typ atom} [mk_atom_ty ty t]
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
248 |
else if is_atom_set ctxt ty
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
249 |
then mk_atom_set_ty ty t
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
250 |
else if is_atom_fset ctxt ty
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
251 |
then mk_atom_fset_ty ty t
|
2608
|
252 |
else if is_atom_list ctxt ty
|
|
253 |
then to_atom_set (mk_atom_list_ty ty t)
|
2607
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
254 |
else raise TERM ("setify", [t])
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
255 |
|
2608
|
256 |
|
2607
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
257 |
(* functions that coerces singletons and lists of concrete atoms
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
258 |
into lists of general atoms *)
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
259 |
fun listify_ty ctxt ty t =
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
260 |
if is_atom ctxt ty
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
261 |
then HOLogic.mk_list @{typ atom} [mk_atom_ty ty t]
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
262 |
else if is_atom_list ctxt ty
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
263 |
then mk_atom_list_ty ty t
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
264 |
else raise TERM ("listify", [t])
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
265 |
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
266 |
fun setify ctxt t = setify_ty ctxt (fastype_of t) t
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
267 |
fun listify ctxt t = listify_ty ctxt (fastype_of t) t
|
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
268 |
|
2608
|
269 |
fun fresh_star_ty ty = [@{typ "atom set"}, ty] ---> @{typ bool}
|
|
270 |
fun fresh_star_const ty = Const (@{const_name fresh_star}, fresh_star_ty ty)
|
|
271 |
fun mk_fresh_star_ty ty t1 t2 = fresh_star_const ty $ t1 $ t2
|
|
272 |
fun mk_fresh_star t1 t2 = mk_fresh_star_ty (fastype_of t2) t1 t2
|
2607
7430e07a5d61
moved setify and listify functions into the library; introduced versions that have a type argument
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
273 |
|
1979
|
274 |
fun supp_ty ty = ty --> @{typ "atom set"};
|
2450
|
275 |
fun supp_const ty = Const (@{const_name supp}, supp_ty ty)
|
2475
486d4647bb37
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
276 |
fun mk_supp_ty ty t = supp_const ty $ t
|
486d4647bb37
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
277 |
fun mk_supp t = mk_supp_ty (fastype_of t) t
|
486d4647bb37
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
278 |
|
486d4647bb37
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
279 |
fun supp_rel_ty ty = ([ty, ty] ---> @{typ bool}) --> ty --> @{typ "atom set"};
|
486d4647bb37
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
280 |
fun supp_rel_const ty = Const (@{const_name supp_rel}, supp_rel_ty ty)
|
486d4647bb37
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
281 |
fun mk_supp_rel_ty ty r t = supp_rel_const ty $ r $ t
|
486d4647bb37
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
282 |
fun mk_supp_rel r t = mk_supp_rel_ty (fastype_of t) r t
|
1979
|
283 |
|
2450
|
284 |
fun supports_const ty = Const (@{const_name supports}, [@{typ "atom set"}, ty] ---> @{typ bool});
|
2448
|
285 |
fun mk_supports_ty ty t1 t2 = supports_const ty $ t1 $ t2;
|
|
286 |
fun mk_supports t1 t2 = mk_supports_ty (fastype_of t2) t1 t2;
|
1979
|
287 |
|
2450
|
288 |
fun finite_const ty = Const (@{const_name finite}, ty --> @{typ bool})
|
|
289 |
fun mk_finite_ty ty t = finite_const ty $ t
|
|
290 |
fun mk_finite t = mk_finite_ty (fastype_of t) t
|
|
291 |
|
|
292 |
|
1834
|
293 |
fun mk_equiv r = r RS @{thm eq_reflection};
|
|
294 |
fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;
|
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
295 |
|
1962
84a13d1e2511
moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
296 |
|
2296
|
297 |
(* functions that construct differences, appends and unions
|
|
298 |
but avoid producing empty atom sets or empty atom lists *)
|
2289
|
299 |
|
|
300 |
fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"}
|
|
301 |
| mk_diff (t1, @{term "{}::atom set"}) = t1
|
2464
f4eba60cbd69
made the fv-definition aggree more with alpha (needed in the support proofs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
302 |
| mk_diff (@{term "set ([]::atom list)"}, _) = @{term "set ([]::atom list)"}
|
f4eba60cbd69
made the fv-definition aggree more with alpha (needed in the support proofs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
303 |
| mk_diff (t1, @{term "set ([]::atom list)"}) = t1
|
2289
|
304 |
| mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2)
|
|
305 |
|
2389
|
306 |
fun mk_append (t1, @{term "[]::atom list"}) = t1
|
2296
|
307 |
| mk_append (@{term "[]::atom list"}, t2) = t2
|
|
308 |
| mk_append (t1, t2) = HOLogic.mk_binop @{const_name "append"} (t1, t2)
|
|
309 |
|
2389
|
310 |
fun mk_union (t1, @{term "{}::atom set"}) = t1
|
2289
|
311 |
| mk_union (@{term "{}::atom set"}, t2) = t2
|
2464
f4eba60cbd69
made the fv-definition aggree more with alpha (needed in the support proofs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
312 |
| mk_union (t1, @{term "set ([]::atom list)"}) = t1
|
f4eba60cbd69
made the fv-definition aggree more with alpha (needed in the support proofs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
313 |
| mk_union (@{term "set ([]::atom list)"}, t2) = t2
|
2296
|
314 |
| mk_union (t1, t2) = HOLogic.mk_binop @{const_name "sup"} (t1, t2)
|
2289
|
315 |
|
2384
|
316 |
fun fold_union trms = fold_rev (curry mk_union) trms @{term "{}::atom set"}
|
2464
f4eba60cbd69
made the fv-definition aggree more with alpha (needed in the support proofs)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
317 |
fun fold_append trms = fold_rev (curry mk_append) trms @{term "[]::atom list"}
|
2289
|
318 |
|
2389
|
319 |
fun mk_conj (t1, @{term "True"}) = t1
|
|
320 |
| mk_conj (@{term "True"}, t2) = t2
|
|
321 |
| mk_conj (t1, t2) = HOLogic.mk_conj (t1, t2)
|
2289
|
322 |
|
2389
|
323 |
fun fold_conj trms = fold_rev (curry mk_conj) trms @{term "True"}
|
2296
|
324 |
|
2448
|
325 |
|
|
326 |
(* produces fresh arguments for a term *)
|
|
327 |
|
|
328 |
fun fresh_args ctxt f =
|
|
329 |
f |> fastype_of
|
|
330 |
|> binder_types
|
|
331 |
|> map (pair "z")
|
|
332 |
|> Variable.variant_frees ctxt [f]
|
|
333 |
|> map Free
|
|
334 |
|
|
335 |
|
|
336 |
|
2288
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
337 |
(** datatypes **)
|
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
338 |
|
2407
|
339 |
(* constructor infos *)
|
|
340 |
type cns_info = (term * typ * typ list * bool list) list
|
2288
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
341 |
|
2602
|
342 |
(* - term for constructor constant
|
|
343 |
- type of the constructor
|
|
344 |
- types of the arguments
|
|
345 |
- flags indicating whether the argument is recursive
|
|
346 |
*)
|
|
347 |
|
2288
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
348 |
(* returns the type of the nth datatype *)
|
2296
|
349 |
fun all_dtyps descr sorts =
|
|
350 |
map (fn n => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n)) (0 upto (length descr - 1))
|
|
351 |
|
2288
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
352 |
fun nth_dtyp descr sorts n =
|
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
353 |
Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n);
|
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
354 |
|
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
355 |
(* returns info about constructors in a datatype *)
|
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
356 |
fun all_dtyp_constrs_info descr =
|
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
357 |
map (fn (_, (ty, vs, constrs)) => map (pair (ty, vs)) constrs) descr
|
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
358 |
|
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
359 |
(* returns the constants of the constructors plus the
|
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
360 |
corresponding type and types of arguments *)
|
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
361 |
fun all_dtyp_constrs_types descr sorts =
|
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
362 |
let
|
2477
|
363 |
fun aux ((ty_name, vs), (cname, args)) =
|
|
364 |
let
|
|
365 |
val vs_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) vs
|
|
366 |
val ty = Type (ty_name, vs_tys)
|
|
367 |
val arg_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) args
|
|
368 |
val is_rec = map Datatype_Aux.is_rec_type args
|
|
369 |
in
|
|
370 |
(Const (cname, arg_tys ---> ty), ty, arg_tys, is_rec)
|
|
371 |
end
|
2288
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
372 |
in
|
2477
|
373 |
map (map aux) (all_dtyp_constrs_info descr)
|
2288
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
374 |
end
|
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
375 |
|
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
376 |
fun nth_dtyp_constrs_types descr sorts n =
|
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
377 |
nth (all_dtyp_constrs_types descr sorts) n
|
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
378 |
|
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
379 |
|
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
380 |
(* generates for every datatype a name str ^ dt_name
|
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
381 |
plus and index for multiple occurences of a string *)
|
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
382 |
fun prefix_dt_names descr sorts str =
|
2477
|
383 |
let
|
|
384 |
fun get_nth_name (i, _) =
|
|
385 |
Datatype_Aux.name_of_typ (nth_dtyp descr sorts i)
|
|
386 |
in
|
|
387 |
Datatype_Prop.indexify_names
|
|
388 |
(map (prefix str o get_nth_name) descr)
|
|
389 |
end
|
2288
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
390 |
|
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
391 |
|
2311
|
392 |
|
|
393 |
(** function package tactics **)
|
|
394 |
|
2304
|
395 |
fun pat_completeness_simp simps lthy =
|
2477
|
396 |
let
|
|
397 |
val simp_set = HOL_basic_ss addsimps (@{thms sum.inject sum.distinct} @ simps)
|
|
398 |
in
|
|
399 |
Pat_Completeness.pat_completeness_tac lthy 1
|
|
400 |
THEN ALLGOALS (asm_full_simp_tac simp_set)
|
|
401 |
end
|
2304
|
402 |
|
2557
781fbc8c0591
fixed locally the problem with the function package; all tests work again
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
403 |
|
2559
add799cf0817
adapted to changes by Florian on the quotient package and removed local fix for function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
404 |
fun prove_termination_tac size_simps ctxt =
|
2477
|
405 |
let
|
2560
|
406 |
val natT = @{typ nat}
|
|
407 |
fun prod_size_const fT sT =
|
|
408 |
let
|
|
409 |
val fT_fun = fT --> natT
|
|
410 |
val sT_fun = sT --> natT
|
|
411 |
val prodT = Type (@{type_name prod}, [fT, sT])
|
|
412 |
in
|
|
413 |
Const (@{const_name prod_size}, [fT_fun, sT_fun, prodT] ---> natT)
|
|
414 |
end
|
|
415 |
|
|
416 |
fun mk_size_measure T =
|
|
417 |
case T of
|
|
418 |
(Type (@{type_name Sum_Type.sum}, [fT, sT])) =>
|
|
419 |
SumTree.mk_sumcase fT sT natT (mk_size_measure fT) (mk_size_measure sT)
|
|
420 |
| (Type (@{type_name Product_Type.prod}, [fT, sT])) =>
|
|
421 |
prod_size_const fT sT $ (mk_size_measure fT) $ (mk_size_measure sT)
|
|
422 |
| _ => size_const T
|
2304
|
423 |
|
2559
add799cf0817
adapted to changes by Florian on the quotient package and removed local fix for function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
424 |
fun mk_measure_trm T =
|
add799cf0817
adapted to changes by Florian on the quotient package and removed local fix for function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
425 |
HOLogic.dest_setT T
|
add799cf0817
adapted to changes by Florian on the quotient package and removed local fix for function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
426 |
|> fst o HOLogic.dest_prodT
|
2477
|
427 |
|> mk_size_measure
|
2560
|
428 |
|> curry (op $) (Const (@{const_name "measure"}, dummyT))
|
2477
|
429 |
|> Syntax.check_term ctxt
|
2560
|
430 |
|
2477
|
431 |
val ss = HOL_ss addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral
|
2560
|
432 |
zero_less_Suc prod.size(1) mult_Suc_right} @ size_simps
|
|
433 |
val ss' = ss addsimprocs Nat_Numeral_Simprocs.cancel_numerals
|
2477
|
434 |
in
|
2559
add799cf0817
adapted to changes by Florian on the quotient package and removed local fix for function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
435 |
Function_Relation.relation_tac ctxt mk_measure_trm
|
2560
|
436 |
THEN_ALL_NEW simp_tac ss'
|
2477
|
437 |
end
|
2410
2bbdb9c427b5
improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
438 |
|
2bbdb9c427b5
improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
439 |
fun prove_termination size_simps ctxt =
|
2bbdb9c427b5
improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
440 |
Function.prove_termination NONE
|
2bbdb9c427b5
improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
441 |
(HEADGOAL (prove_termination_tac size_simps ctxt)) ctxt
|
2311
|
442 |
|
|
443 |
(** transformations of premises (in inductive proofs) **)
|
|
444 |
|
|
445 |
(*
|
|
446 |
given the theorem F[t]; proves the theorem F[f t]
|
|
447 |
|
|
448 |
- F needs to be monotone
|
|
449 |
- f returns either SOME for a term it fires on
|
|
450 |
and NONE elsewhere
|
|
451 |
*)
|
|
452 |
fun map_term f t =
|
|
453 |
(case f t of
|
|
454 |
NONE => map_term' f t
|
|
455 |
| x => x)
|
|
456 |
and map_term' f (t $ u) =
|
|
457 |
(case (map_term f t, map_term f u) of
|
|
458 |
(NONE, NONE) => NONE
|
|
459 |
| (SOME t'', NONE) => SOME (t'' $ u)
|
|
460 |
| (NONE, SOME u'') => SOME (t $ u'')
|
|
461 |
| (SOME t'', SOME u'') => SOME (t'' $ u''))
|
|
462 |
| map_term' f (Abs (s, T, t)) =
|
|
463 |
(case map_term f t of
|
|
464 |
NONE => NONE
|
|
465 |
| SOME t'' => SOME (Abs (s, T, t'')))
|
|
466 |
| map_term' _ _ = NONE;
|
|
467 |
|
|
468 |
fun map_thm_tac ctxt tac thm =
|
2477
|
469 |
let
|
|
470 |
val monos = Inductive.get_monos ctxt
|
|
471 |
val simps = HOL_basic_ss addsimps @{thms split_def}
|
|
472 |
in
|
|
473 |
EVERY [cut_facts_tac [thm] 1, etac rev_mp 1,
|
|
474 |
REPEAT_DETERM (FIRSTGOAL (simp_tac simps THEN' resolve_tac monos)),
|
|
475 |
REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))]
|
|
476 |
end
|
2311
|
477 |
|
|
478 |
fun map_thm ctxt f tac thm =
|
2477
|
479 |
let
|
|
480 |
val opt_goal_trm = map_term f (prop_of thm)
|
|
481 |
in
|
|
482 |
case opt_goal_trm of
|
|
483 |
NONE => thm
|
|
484 |
| SOME goal =>
|
|
485 |
Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm)
|
|
486 |
end
|
2311
|
487 |
|
|
488 |
(*
|
|
489 |
inductive premises can be of the form
|
|
490 |
R ... /\ P ...; split_conj_i picks out
|
|
491 |
the part R or P part
|
|
492 |
*)
|
2480
ac7dff1194e8
introduced a general procedure for structural inductions; simplified reflexivity proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
493 |
fun split_conj1 names (Const (@{const_name "conj"}, _) $ f1 $ _) =
|
2311
|
494 |
(case head_of f1 of
|
|
495 |
Const (name, _) => if member (op =) names name then SOME f1 else NONE
|
|
496 |
| _ => NONE)
|
|
497 |
| split_conj1 _ _ = NONE;
|
|
498 |
|
2446
|
499 |
fun split_conj2 names (Const (@{const_name "conj"}, _) $ f1 $ f2) =
|
2311
|
500 |
(case head_of f1 of
|
|
501 |
Const (name, _) => if member (op =) names name then SOME f2 else NONE
|
|
502 |
| _ => NONE)
|
|
503 |
| split_conj2 _ _ = NONE;
|
|
504 |
|
|
505 |
fun transform_prem1 ctxt names thm =
|
|
506 |
map_thm ctxt (split_conj1 names) (etac conjunct1 1) thm
|
|
507 |
|
|
508 |
fun transform_prem2 ctxt names thm =
|
|
509 |
map_thm ctxt (split_conj2 names) (etac conjunct2 1) thm
|
|
510 |
|
|
511 |
|
2397
|
512 |
(* transformes a theorem into one of the object logic *)
|
|
513 |
val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars
|
|
514 |
|
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
515 |
end (* structure *)
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
516 |
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
517 |
open Nominal_Library; |