1960
|
1 |
theory NewFv
|
1981
|
2 |
imports "../Nominal-General/Nominal2_Atoms"
|
|
3 |
"Abs" "Perm" "Nominal2_FSet"
|
1960
|
4 |
begin
|
|
5 |
|
|
6 |
ML {*
|
2046
73c50e913db6
tuned and added some comments to the code; added also an exception for early exit of the nominal2_cmd function
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
7 |
(* binding modes *)
|
73c50e913db6
tuned and added some comments to the code; added also an exception for early exit of the nominal2_cmd function
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
8 |
|
1960
|
9 |
datatype bmodes =
|
|
10 |
BEmy of int
|
|
11 |
| BLst of ((term option * int) list) * (int list)
|
|
12 |
| BSet of ((term option * int) list) * (int list)
|
|
13 |
| BRes of ((term option * int) list) * (int list)
|
|
14 |
*}
|
|
15 |
|
|
16 |
ML {*
|
1965
4a3c05fe2bc5
closed Datatype_Aux; replaced nth_dtyp by the function used in Perm.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
17 |
fun mk_singleton_atom x = HOLogic.mk_set @{typ atom} [mk_atom x];
|
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
|
18 |
|
1965
4a3c05fe2bc5
closed Datatype_Aux; replaced nth_dtyp by the function used in Perm.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
19 |
val noatoms = @{term "{} :: atom set"};
|
1963
|
20 |
|
1965
4a3c05fe2bc5
closed Datatype_Aux; replaced nth_dtyp by the function used in Perm.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
21 |
fun mk_union sets =
|
4a3c05fe2bc5
closed Datatype_Aux; replaced nth_dtyp by the function used in Perm.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
22 |
fold (fn a => fn b =>
|
4a3c05fe2bc5
closed Datatype_Aux; replaced nth_dtyp by the function used in Perm.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
23 |
if a = noatoms then b else
|
4a3c05fe2bc5
closed Datatype_Aux; replaced nth_dtyp by the function used in Perm.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
24 |
if b = noatoms then a else
|
4a3c05fe2bc5
closed Datatype_Aux; replaced nth_dtyp by the function used in Perm.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
25 |
if a = b then a else
|
4a3c05fe2bc5
closed Datatype_Aux; replaced nth_dtyp by the function used in Perm.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
26 |
HOLogic.mk_binop @{const_name sup} (a, b)) (rev sets) noatoms;
|
1960
|
27 |
*}
|
|
28 |
|
|
29 |
ML {*
|
1963
|
30 |
fun is_atom thy ty =
|
1970
|
31 |
Sign.of_sort thy (ty, @{sort at_base})
|
1960
|
32 |
|
|
33 |
fun is_atom_set thy (Type ("fun", [t, @{typ bool}])) = is_atom thy t
|
|
34 |
| is_atom_set _ _ = false;
|
|
35 |
|
|
36 |
fun is_atom_fset thy (Type ("FSet.fset", [t])) = is_atom thy t
|
|
37 |
| is_atom_fset _ _ = false;
|
|
38 |
|
|
39 |
fun mk_atom_set t =
|
|
40 |
let
|
|
41 |
val ty = fastype_of t;
|
|
42 |
val atom_ty = HOLogic.dest_setT ty --> @{typ atom};
|
|
43 |
val img_ty = atom_ty --> ty --> @{typ "atom set"};
|
|
44 |
in
|
1963
|
45 |
(Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t)
|
1960
|
46 |
end;
|
|
47 |
|
|
48 |
fun mk_atom_fset t =
|
|
49 |
let
|
|
50 |
val ty = fastype_of t;
|
|
51 |
val atom_ty = dest_fsetT ty --> @{typ atom};
|
|
52 |
val fmap_ty = atom_ty --> ty --> @{typ "atom fset"};
|
|
53 |
val fset_to_set = @{term "fset_to_set :: atom fset \<Rightarrow> atom set"}
|
|
54 |
in
|
1984
|
55 |
fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)
|
1960
|
56 |
end;
|
|
57 |
|
|
58 |
fun mk_diff a b =
|
|
59 |
if b = noatoms then a else
|
|
60 |
if b = a then noatoms else
|
|
61 |
HOLogic.mk_binop @{const_name minus} (a, b);
|
|
62 |
*}
|
|
63 |
|
|
64 |
ML {*
|
1989
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
65 |
fun is_atom_list (Type (@{type_name list}, [T])) = true
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
66 |
| is_atom_list _ = false
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
67 |
*}
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
68 |
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
69 |
ML {*
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
70 |
fun dest_listT (Type (@{type_name list}, [T])) = T
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
71 |
| dest_listT T = raise TYPE ("dest_listT: list type expected", [T], [])
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
72 |
*}
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
73 |
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
74 |
ML {*
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
75 |
fun mk_atom_list t =
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
76 |
let
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
77 |
val ty = fastype_of t;
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
78 |
val atom_ty = dest_listT ty --> @{typ atom};
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
79 |
val map_ty = atom_ty --> ty --> @{typ "atom list"};
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
80 |
in
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
81 |
(Const (@{const_name map}, map_ty) $ mk_atom_ty atom_ty t)
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
82 |
end;
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
83 |
*}
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
84 |
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
85 |
ML {*
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
86 |
fun setify thy t =
|
1960
|
87 |
let
|
1963
|
88 |
val ty = fastype_of t;
|
1960
|
89 |
in
|
1983
4538d63ecc9b
Support in positive position and atoms in negative positions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
90 |
if is_atom thy ty
|
4538d63ecc9b
Support in positive position and atoms in negative positions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
91 |
then mk_singleton_atom t
|
4538d63ecc9b
Support in positive position and atoms in negative positions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
92 |
else if is_atom_set thy ty
|
4538d63ecc9b
Support in positive position and atoms in negative positions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
93 |
then mk_atom_set t
|
4538d63ecc9b
Support in positive position and atoms in negative positions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
94 |
else if is_atom_fset thy ty
|
4538d63ecc9b
Support in positive position and atoms in negative positions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
95 |
then mk_atom_fset t
|
1989
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
96 |
else error ("setify" ^ (PolyML.makestring (t, ty)))
|
1960
|
97 |
end
|
|
98 |
*}
|
|
99 |
|
|
100 |
ML {*
|
1989
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
101 |
fun listify thy t =
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
102 |
let
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
103 |
val ty = fastype_of t;
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
104 |
in
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
105 |
if is_atom thy ty
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
106 |
then HOLogic.mk_list @{typ atom} [mk_atom t]
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
107 |
else if is_atom_list ty
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
108 |
then mk_atom_set t
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
109 |
else error "listify"
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
110 |
end
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
111 |
*}
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
112 |
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
113 |
ML {*
|
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
114 |
fun set x =
|
1983
4538d63ecc9b
Support in positive position and atoms in negative positions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
115 |
if fastype_of x = @{typ "atom list"}
|
4538d63ecc9b
Support in positive position and atoms in negative positions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
116 |
then @{term "set::atom list \<Rightarrow> atom set"} $ x
|
1969
|
117 |
else x
|
1960
|
118 |
*}
|
|
119 |
|
|
120 |
ML {*
|
1986
|
121 |
fun fv_body thy dts args fv_frees supp i =
|
|
122 |
let
|
|
123 |
val x = nth args i;
|
|
124 |
val dt = nth dts i;
|
|
125 |
in
|
|
126 |
if Datatype_Aux.is_rec_type dt
|
|
127 |
then nth fv_frees (Datatype_Aux.body_index dt) $ x
|
1989
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
128 |
else (if supp then mk_supp x else setify thy x)
|
1986
|
129 |
end
|
|
130 |
*}
|
|
131 |
|
|
132 |
ML {*
|
1960
|
133 |
fun fv_bm_lsts thy dts args fv_frees bn_fvbn binds bodys =
|
|
134 |
let
|
1986
|
135 |
val fv_bodys = mk_union (map (fv_body thy dts args fv_frees true) bodys)
|
1960
|
136 |
val bound_vars =
|
|
137 |
case binds of
|
1989
45721f92e471
Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
138 |
[(SOME bn, i)] => set (bn $ nth args i)
|
1986
|
139 |
| _ => mk_union (map (fv_body thy dts args fv_frees false) (map snd binds));
|
1960
|
140 |
val non_rec_vars =
|
|
141 |
case binds of
|
|
142 |
[(SOME bn, i)] =>
|
2071
|
143 |
if member (op =) bodys i
|
1985
|
144 |
then noatoms
|
|
145 |
else ((the (AList.lookup (op=) bn_fvbn bn)) $ nth args i)
|
1960
|
146 |
| _ => noatoms
|
|
147 |
in
|
|
148 |
mk_union [mk_diff fv_bodys bound_vars, non_rec_vars]
|
|
149 |
end
|
|
150 |
*}
|
|
151 |
|
|
152 |
ML {*
|
|
153 |
fun fv_bn_bm thy dts args fv_frees bn_fvbn args_in_bn bm =
|
|
154 |
case bm of
|
|
155 |
BEmy i =>
|
|
156 |
let
|
|
157 |
val x = nth args i;
|
|
158 |
val dt = nth dts i;
|
|
159 |
in
|
|
160 |
case AList.lookup (op=) args_in_bn i of
|
1981
|
161 |
NONE => if Datatype_Aux.is_rec_type dt
|
|
162 |
then nth fv_frees (Datatype_Aux.body_index dt) $ x
|
|
163 |
else mk_supp x
|
1960
|
164 |
| SOME (SOME (f : term)) => (the (AList.lookup (op=) bn_fvbn f)) $ x
|
|
165 |
| SOME NONE => noatoms
|
|
166 |
end
|
|
167 |
| BLst (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
|
|
168 |
| BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
|
|
169 |
| BRes (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
|
|
170 |
*}
|
|
171 |
|
|
172 |
ML {*
|
1981
|
173 |
fun fv_bn thy dt_descr sorts fv_frees bn_fvbn bclausess (fvbn, (_, ith_dtyp, args_in_bns)) =
|
1960
|
174 |
let
|
1981
|
175 |
fun fv_bn_constr (cname, dts) (args_in_bn, bclauses) =
|
1960
|
176 |
let
|
1968
|
177 |
val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts;
|
1960
|
178 |
val names = Datatype_Prop.make_tnames Ts;
|
|
179 |
val args = map Free (names ~~ Ts);
|
1968
|
180 |
val c = Const (cname, Ts ---> (nth_dtyp dt_descr sorts ith_dtyp));
|
1960
|
181 |
val fv_bn_bm = fv_bn_bm thy dts args fv_frees bn_fvbn args_in_bn
|
|
182 |
in
|
|
183 |
HOLogic.mk_Trueprop (HOLogic.mk_eq
|
1981
|
184 |
(fvbn $ list_comb (c, args), mk_union (map fv_bn_bm bclauses)))
|
1960
|
185 |
end;
|
1968
|
186 |
val (_, (_, _, constrs)) = nth dt_descr ith_dtyp;
|
1960
|
187 |
in
|
1981
|
188 |
map2 fv_bn_constr constrs (args_in_bns ~~ bclausess)
|
1960
|
189 |
end
|
|
190 |
*}
|
|
191 |
|
|
192 |
ML {*
|
1981
|
193 |
fun fv_bns thy dt_descr sorts fv_frees bn_funs bclausesss =
|
1960
|
194 |
let
|
|
195 |
fun mk_fvbn_free (bn, ith, _) =
|
|
196 |
let
|
|
197 |
val fvbn_name = "fv_" ^ (Long_Name.base_name (fst (dest_Const bn)));
|
|
198 |
in
|
|
199 |
(fvbn_name, Free (fvbn_name, fastype_of (nth fv_frees ith)))
|
|
200 |
end;
|
1967
|
201 |
val (fvbn_names, fvbn_frees) = split_list (map mk_fvbn_free bn_funs);
|
|
202 |
val bn_fvbn = (map (fn (bn, _, _) => bn) bn_funs) ~~ fvbn_frees
|
1981
|
203 |
val bclausessl = map (fn (_, i, _) => nth bclausesss i) bn_funs;
|
|
204 |
val eqs = map2 (fv_bn thy dt_descr sorts fv_frees bn_fvbn) bclausessl (fvbn_frees ~~ bn_funs);
|
1960
|
205 |
in
|
1967
|
206 |
(bn_fvbn, fvbn_names, eqs)
|
1960
|
207 |
end
|
|
208 |
*}
|
|
209 |
|
|
210 |
ML {*
|
|
211 |
fun fv_bm thy dts args fv_frees bn_fvbn bm =
|
|
212 |
case bm of
|
|
213 |
BEmy i =>
|
|
214 |
let
|
|
215 |
val x = nth args i;
|
|
216 |
val dt = nth dts i;
|
|
217 |
in
|
1981
|
218 |
if Datatype_Aux.is_rec_type dt
|
|
219 |
then nth fv_frees (Datatype_Aux.body_index dt) $ x
|
|
220 |
else mk_supp x
|
1960
|
221 |
end
|
|
222 |
| BLst (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
|
|
223 |
| BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
|
|
224 |
| BRes (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
|
|
225 |
*}
|
|
226 |
|
|
227 |
ML {*
|
1981
|
228 |
fun fv thy dt_descr sorts fv_frees bn_fvbn bclausess (fv_free, ith_dtyp) =
|
1960
|
229 |
let
|
1981
|
230 |
fun fv_constr (cname, dts) bclauses =
|
1960
|
231 |
let
|
1968
|
232 |
val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts;
|
1960
|
233 |
val names = Datatype_Prop.make_tnames Ts;
|
|
234 |
val args = map Free (names ~~ Ts);
|
1968
|
235 |
val c = Const (cname, Ts ---> (nth_dtyp dt_descr sorts ith_dtyp));
|
1960
|
236 |
val fv_bn_bm = fv_bm thy dts args fv_frees bn_fvbn
|
|
237 |
in
|
|
238 |
HOLogic.mk_Trueprop (HOLogic.mk_eq
|
1981
|
239 |
(fv_free $ list_comb (c, args), mk_union (map fv_bn_bm bclauses)))
|
1960
|
240 |
end;
|
1968
|
241 |
val (_, (_, _, constrs)) = nth dt_descr ith_dtyp;
|
1960
|
242 |
in
|
1981
|
243 |
map2 fv_constr constrs bclausess
|
1960
|
244 |
end
|
|
245 |
*}
|
1963
|
246 |
|
1960
|
247 |
ML {*
|
2046
73c50e913db6
tuned and added some comments to the code; added also an exception for early exit of the nominal2_cmd function
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
248 |
fun define_raw_fv dt_descr sorts bn_funs bclausesss lthy =
|
1960
|
249 |
let
|
|
250 |
val thy = ProofContext.theory_of lthy;
|
1965
4a3c05fe2bc5
closed Datatype_Aux; replaced nth_dtyp by the function used in Perm.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
251 |
|
1967
|
252 |
val fv_names = prefix_dt_names dt_descr sorts "fv_"
|
2046
73c50e913db6
tuned and added some comments to the code; added also an exception for early exit of the nominal2_cmd function
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
253 |
val fv_types = map (fn (i, _) => nth_dtyp dt_descr sorts i --> @{typ "atom set"}) dt_descr;
|
1960
|
254 |
val fv_frees = map Free (fv_names ~~ fv_types);
|
1967
|
255 |
|
2046
73c50e913db6
tuned and added some comments to the code; added also an exception for early exit of the nominal2_cmd function
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
256 |
(* free variables for the bn-functions *)
|
1981
|
257 |
val (bn_fvbn, fv_bn_names, fv_bn_eqs) =
|
1984
|
258 |
fv_bns thy dt_descr sorts fv_frees bn_funs bclausesss;
|
1965
4a3c05fe2bc5
closed Datatype_Aux; replaced nth_dtyp by the function used in Perm.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
259 |
|
2046
73c50e913db6
tuned and added some comments to the code; added also an exception for early exit of the nominal2_cmd function
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
260 |
|
1986
|
261 |
val fv_bns = map snd bn_fvbn;
|
1960
|
262 |
val fv_nums = 0 upto (length fv_frees - 1)
|
1965
4a3c05fe2bc5
closed Datatype_Aux; replaced nth_dtyp by the function used in Perm.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
263 |
|
1984
|
264 |
val fv_eqs = map2 (fv thy dt_descr sorts fv_frees bn_fvbn) bclausesss (fv_frees ~~ fv_nums);
|
1981
|
265 |
|
1971
8daf6ff5e11a
simpliied and moved the remaining lemmas about the atom-function to Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
266 |
val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
|
8daf6ff5e11a
simpliied and moved the remaining lemmas about the atom-function to Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
267 |
val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs)
|
1965
4a3c05fe2bc5
closed Datatype_Aux; replaced nth_dtyp by the function used in Perm.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
268 |
|
1981
|
269 |
fun pat_completeness_auto ctxt =
|
|
270 |
Pat_Completeness.pat_completeness_tac ctxt 1
|
|
271 |
THEN auto_tac (clasimpset_of ctxt)
|
|
272 |
|
|
273 |
fun prove_termination lthy =
|
|
274 |
Function.prove_termination NONE
|
|
275 |
(Lexicographic_Order.lexicographic_order_tac true lthy) lthy
|
|
276 |
|
2000
|
277 |
val (_, lthy') = Function.add_function all_fv_names all_fv_eqs
|
1981
|
278 |
Function_Common.default_config pat_completeness_auto lthy
|
|
279 |
|
2000
|
280 |
val (info, lthy'') = prove_termination (Local_Theory.restore lthy')
|
|
281 |
|
|
282 |
val {fs, simps, ...} = info;
|
1986
|
283 |
|
|
284 |
val morphism = ProofContext.export_morphism lthy'' lthy
|
2000
|
285 |
val fs_exp = map (Morphism.term morphism) fs
|
1986
|
286 |
|
2000
|
287 |
val (fv_frees_exp, fv_bns_exp) = chop (length fv_frees) fs_exp
|
|
288 |
val simps_exp = Morphism.fact morphism (the simps)
|
1960
|
289 |
in
|
2000
|
290 |
((fv_frees_exp, fv_bns_exp), simps_exp, lthy'')
|
1960
|
291 |
end
|
|
292 |
*}
|
|
293 |
|
|
294 |
end
|