1168
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 1
theory Fv
1334
+ − 2
imports "Nominal2_Atoms" "Abs" "Perm" "Rsp"
1168
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 3
begin
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 4
1358
+ − 5
(* Bindings are a list of lists of lists of triples.
1172
+ − 6
1358
+ − 7
The first list represents the datatypes defined.
+ − 8
The second list represents the constructors.
+ − 9
The internal list is a list of all the bndings that
+ − 10
concern the constructor.
1172
+ − 11
1358
+ − 12
Every triple consists of a function, the binding and
+ − 13
the body.
1169
+ − 14
+ − 15
Eg:
+ − 16
nominal_datatype
+ − 17
+ − 18
C1
+ − 19
| C2 x y z bind x in z
1172
+ − 20
| C3 x y z bind f x in z bind g y in z
1169
+ − 21
+ − 22
yields:
1172
+ − 23
[
+ − 24
[],
1358
+ − 25
[(NONE, 0, 2)],
+ − 26
[(SOME (Const f), 0, 2), (Some (Const g), 1, 2)]]
1185
+ − 27
1358
+ − 28
A SOME binding has to have a function which takes an appropriate
+ − 29
argument and returns an atom set. A NONE binding has to be on an
+ − 30
argument that is an atom or an atom set.
1185
+ − 31
1191
+ − 32
How the procedure works:
+ − 33
For each of the defined datatypes,
+ − 34
For each of the constructors,
+ − 35
It creates a union of free variables for each argument.
+ − 36
+ − 37
For an argument the free variables are the variables minus
+ − 38
bound variables.
+ − 39
+ − 40
The variables are:
+ − 41
For an atom, a singleton set with the atom itself.
+ − 42
For an atom set, the atom set itself.
+ − 43
For a recursive argument, the appropriate fv function applied to it.
+ − 44
(* TODO: This one is not implemented *)
+ − 45
For other arguments it should be an appropriate fv function stored
+ − 46
in the database.
+ − 47
The bound variables are a union of results of all bindings that
+ − 48
involve the given argument. For a paricular binding the result is:
+ − 49
For a function applied to an argument this function with the argument.
+ − 50
For an atom, a singleton set with the atom itself.
+ − 51
For an atom set, the atom set itself.
+ − 52
For a recursive argument, the appropriate fv function applied to it.
+ − 53
(* TODO: This one is not implemented *)
+ − 54
For other arguments it should be an appropriate fv function stored
+ − 55
in the database.
1358
+ − 56
+ − 57
For every argument that is a binding, we add a the same binding in its
+ − 58
body.
1169
+ − 59
*)
+ − 60
1362
+ − 61
ML {*
+ − 62
fun is_atom thy typ =
+ − 63
Sign.of_sort thy (typ, @{sort at})
1366
+ − 64
+ − 65
fun is_atom_set thy (Type ("fun", [t, @{typ bool}])) = is_atom thy t
+ − 66
| is_atom_set thy _ = false;
1362
+ − 67
*}
+ − 68
+ − 69
1366
+ − 70
1358
+ − 71
(* Like map2, only if the second list is empty passes empty lists insted of error *)
1302
+ − 72
ML {*
+ − 73
fun map2i _ [] [] = []
+ − 74
| map2i f (x :: xs) (y :: ys) = f x y :: map2i f xs ys
+ − 75
| map2i f (x :: xs) [] = f x [] :: map2i f xs []
+ − 76
| map2i _ _ _ = raise UnequalLengths;
+ − 77
*}
+ − 78
1358
+ − 79
(* Finds bindings with the same function and binding, and gathers all
1375
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 80
bodys for such pairs
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 81
*)
1168
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 82
ML {*
1357
42b7abf779ec
Gather bindings with same binder, and generate only one permutation for them.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 83
fun gather_binds binds =
42b7abf779ec
Gather bindings with same binder, and generate only one permutation for them.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 84
let
42b7abf779ec
Gather bindings with same binder, and generate only one permutation for them.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 85
fun gather_binds_cons binds =
42b7abf779ec
Gather bindings with same binder, and generate only one permutation for them.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 86
let
42b7abf779ec
Gather bindings with same binder, and generate only one permutation for them.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 87
val common = map (fn (f, bi, _) => (f, bi)) binds
42b7abf779ec
Gather bindings with same binder, and generate only one permutation for them.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 88
val nodups = distinct (op =) common
42b7abf779ec
Gather bindings with same binder, and generate only one permutation for them.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 89
fun find_bodys (sf, sbi) =
42b7abf779ec
Gather bindings with same binder, and generate only one permutation for them.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 90
filter (fn (f, bi, _) => f = sf andalso bi = sbi) binds
42b7abf779ec
Gather bindings with same binder, and generate only one permutation for them.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 91
val bodys = map ((map (fn (_, _, bo) => bo)) o find_bodys) nodups
42b7abf779ec
Gather bindings with same binder, and generate only one permutation for them.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 92
in
42b7abf779ec
Gather bindings with same binder, and generate only one permutation for them.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 93
nodups ~~ bodys
42b7abf779ec
Gather bindings with same binder, and generate only one permutation for them.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 94
end
42b7abf779ec
Gather bindings with same binder, and generate only one permutation for them.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 95
in
42b7abf779ec
Gather bindings with same binder, and generate only one permutation for them.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 96
map (map gather_binds_cons) binds
42b7abf779ec
Gather bindings with same binder, and generate only one permutation for them.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 97
end
42b7abf779ec
Gather bindings with same binder, and generate only one permutation for them.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 98
*}
42b7abf779ec
Gather bindings with same binder, and generate only one permutation for them.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 99
42b7abf779ec
Gather bindings with same binder, and generate only one permutation for them.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 100
ML {*
42b7abf779ec
Gather bindings with same binder, and generate only one permutation for them.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 101
fun un_gather_binds_cons binds =
42b7abf779ec
Gather bindings with same binder, and generate only one permutation for them.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 102
flat (map (fn (((f, bi), bos), pi) => map (fn bo => ((f, bi, bo), pi)) bos) binds)
42b7abf779ec
Gather bindings with same binder, and generate only one permutation for them.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 103
*}
42b7abf779ec
Gather bindings with same binder, and generate only one permutation for them.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 104
42b7abf779ec
Gather bindings with same binder, and generate only one permutation for them.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 105
ML {*
1175
+ − 106
open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *);
1178
+ − 107
(* TODO: It is the same as one in 'nominal_atoms' *)
1175
+ − 108
fun mk_atom ty = Const (@{const_name atom}, ty --> @{typ atom});
+ − 109
val noatoms = @{term "{} :: atom set"};
+ − 110
fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x];
+ − 111
fun mk_union sets =
+ − 112
fold (fn a => fn b =>
+ − 113
if a = noatoms then b else
+ − 114
if b = noatoms then a else
1323
+ − 115
if a = b then a else
1325
+ − 116
HOLogic.mk_binop @{const_name sup} (a, b)) (rev sets) noatoms;
+ − 117
val mk_inter = foldr1 (HOLogic.mk_binop @{const_name inf})
1288
+ − 118
fun mk_conjl props =
+ − 119
fold (fn a => fn b =>
+ − 120
if a = @{term True} then b else
+ − 121
if b = @{term True} then a else
+ − 122
HOLogic.mk_conj (a, b)) props @{term True};
1175
+ − 123
fun mk_diff a b =
+ − 124
if b = noatoms then a else
+ − 125
if b = a then noatoms else
+ − 126
HOLogic.mk_binop @{const_name minus} (a, b);
1185
+ − 127
fun mk_atoms t =
+ − 128
let
+ − 129
val ty = fastype_of t;
+ − 130
val atom_ty = HOLogic.dest_setT ty --> @{typ atom};
+ − 131
val img_ty = atom_ty --> ty --> @{typ "atom set"};
+ − 132
in
+ − 133
(Const (@{const_name image}, img_ty) $ Const (@{const_name atom}, atom_ty) $ t)
+ − 134
end;
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 135
(* Similar to one in USyntax *)
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 136
fun mk_pair (fst, snd) =
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 137
let val ty1 = fastype_of fst
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 138
val ty2 = fastype_of snd
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 139
val c = HOLogic.pair_const ty1 ty2
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 140
in c $ fst $ snd
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 141
end;
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 142
1175
+ − 143
*}
+ − 144
1288
+ − 145
ML {* fun add_perm (p1, p2) = Const(@{const_name plus}, @{typ "perm \<Rightarrow> perm \<Rightarrow> perm"}) $ p1 $ p2 *}
+ − 146
1375
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 147
ML {*
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 148
fun non_rec_binds l =
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 149
let
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 150
fun is_non_rec (SOME (f, false), _, _) = SOME f
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 151
| is_non_rec _ = NONE
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 152
in
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 153
distinct (op =) (map_filter is_non_rec (flat (flat l)))
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 154
end
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 155
*}
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 156
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 157
(* We assume no bindings in the type on which bn is defined *)
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 158
ML {*
1379
+ − 159
fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees (bn, ith_dtyp, args_in_bns) =
1375
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 160
let
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 161
val {descr, sorts, ...} = dt_info;
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 162
fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 163
val fvbn_name = "fv_" ^ (Long_Name.base_name (fst (dest_Const bn)));
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 164
val fvbn = Free (fvbn_name, fastype_of (nth fv_frees ith_dtyp));
1379
+ − 165
fun fv_bn_constr (cname, dts) args_in_bn =
1375
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 166
let
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 167
val Ts = map (typ_of_dtyp descr sorts) dts;
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 168
val names = Datatype_Prop.make_tnames Ts;
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 169
val args = map Free (names ~~ Ts);
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 170
val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp));
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 171
fun fv_arg ((dt, x), arg_no) =
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 172
let
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 173
val ty = fastype_of x
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 174
in
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 175
if arg_no mem args_in_bn then
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 176
(if is_rec_type dt then
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 177
(if body_index dt = ith_dtyp then fvbn $ x else error "fv_bn: not good")
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 178
else @{term "{} :: atom set"}) else
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 179
if is_atom thy ty then mk_single_atom x else
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 180
if is_atom_set thy ty then mk_atoms x else
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 181
if is_rec_type dt then nth fv_frees (body_index dt) $ x else
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 182
@{term "{} :: atom set"}
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 183
end;
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 184
val arg_nos = 0 upto (length dts - 1)
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 185
in
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 186
HOLogic.mk_Trueprop (HOLogic.mk_eq
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 187
(fvbn $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ arg_nos))))
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 188
end;
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 189
val (_, (_, _, constrs)) = nth descr ith_dtyp;
1379
+ − 190
val eqs = map2i fv_bn_constr constrs args_in_bns
1375
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 191
in
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 192
((bn, fvbn), (fvbn_name, eqs))
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 193
end
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 194
*}
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 195
1376
+ − 196
ML {* fn x => split_list(flat x) *}
+ − 197
ML {* fn x => apsnd flat (split_list (map split_list x)) *}
1206
+ − 198
(* TODO: Notice datatypes without bindings and replace alpha with equality *)
1175
+ − 199
ML {*
1375
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 200
fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall bns lthy =
1178
+ − 201
let
1366
+ − 202
val thy = ProofContext.theory_of lthy;
1277
+ − 203
val {descr, sorts, ...} = dt_info;
1168
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 204
fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 205
val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 206
"fv_" ^ name_of_typ (nth_dtyp i)) descr);
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 207
val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr;
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 208
val fv_frees = map Free (fv_names ~~ fv_types);
1375
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 209
val nr_bns = non_rec_binds bindsall;
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 210
val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns;
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 211
val (bn_fv_bns, fv_bn_names_eqs) = split_list (map (fv_bn thy dt_info fv_frees) rel_bns);
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 212
val fv_bns = map snd bn_fv_bns;
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 213
val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs;
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 214
val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 215
"alpha_" ^ name_of_typ (nth_dtyp i)) descr);
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 216
val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr;
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 217
val alpha_frees = map Free (alpha_names ~~ alpha_types);
1382
+ − 218
val alpha_bnnames = map (fn (bn, _, _) => "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn)))) bns;
+ − 219
val alpha_bntypes = map (fn (_, i, _) => @{typ perm} --> nth_dtyp i --> nth_dtyp i --> @{typ bool}) bns;
+ − 220
val alpha_bnfrees = map Free (alpha_bnnames ~~ alpha_bntypes);
1288
+ − 221
fun fv_alpha_constr ith_dtyp (cname, dts) bindcs =
1168
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 222
let
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 223
val Ts = map (typ_of_dtyp descr sorts) dts;
1288
+ − 224
val bindslen = length bindcs
1323
+ − 225
val pi_strs_same = replicate bindslen "pi"
+ − 226
val pi_strs = Name.variant_list [] pi_strs_same;
1288
+ − 227
val pis = map (fn ps => Free (ps, @{typ perm})) pi_strs;
1357
42b7abf779ec
Gather bindings with same binder, and generate only one permutation for them.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 228
val bind_pis_gath = bindcs ~~ pis;
42b7abf779ec
Gather bindings with same binder, and generate only one permutation for them.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 229
val bind_pis = un_gather_binds_cons bind_pis_gath;
42b7abf779ec
Gather bindings with same binder, and generate only one permutation for them.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 230
val bindcs = map fst bind_pis;
1288
+ − 231
val names = Name.variant_list pi_strs (Datatype_Prop.make_tnames Ts);
1168
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 232
val args = map Free (names ~~ Ts);
1288
+ − 233
val names2 = Name.variant_list (pi_strs @ names) (Datatype_Prop.make_tnames Ts);
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 234
val args2 = map Free (names2 ~~ Ts);
1288
+ − 235
val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp));
+ − 236
val fv_c = nth fv_frees ith_dtyp;
+ − 237
val alpha = nth alpha_frees ith_dtyp;
+ − 238
val arg_nos = 0 upto (length dts - 1)
+ − 239
fun fv_bind args (NONE, i, _) =
1177
+ − 240
if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else
1366
+ − 241
if ((is_atom thy) o fastype_of) (nth args i) then mk_single_atom (nth args i) else
+ − 242
if ((is_atom_set thy) o fastype_of) (nth args i) then mk_atoms (nth args i) else
+ − 243
(* TODO we do not know what to do with non-atomizable things *)
+ − 244
@{term "{} :: atom set"}
1375
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 245
| fv_bind args (SOME (f, _), i, _) = f $ (nth args i);
1288
+ − 246
fun fv_binds args relevant = mk_union (map (fv_bind args) relevant)
1375
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 247
fun find_nonrec_binder j (SOME (f, false), i, _) = if i = j then SOME f else NONE
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 248
| find_nonrec_binder _ _ = NONE
1288
+ − 249
fun fv_arg ((dt, x), arg_no) =
1375
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 250
case get_first (find_nonrec_binder arg_no) bindcs of
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 251
SOME f =>
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 252
(case get_first (fn (x, y) => if x = f then SOME y else NONE) bn_fv_bns of
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 253
SOME fv_bn => fv_bn $ x
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 254
| NONE => error "bn specified in a non-rec binding but not in bn list")
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 255
| NONE =>
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 256
let
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 257
val arg =
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 258
if is_rec_type dt then nth fv_frees (body_index dt) $ x else
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 259
if ((is_atom thy) o fastype_of) x then mk_single_atom x else
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 260
if ((is_atom_set thy) o fastype_of) x then mk_atoms x else
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 261
(* TODO we do not know what to do with non-atomizable things *)
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 262
@{term "{} :: atom set"}
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 263
(* If i = j then we generate it only once *)
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 264
val relevant = filter (fn (_, i, j) => ((i = arg_no) orelse (j = arg_no))) bindcs;
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 265
val sub = fv_binds args relevant
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 266
in
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 267
mk_diff arg sub
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 268
end;
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 269
val fv_eq = HOLogic.mk_Trueprop (HOLogic.mk_eq
1288
+ − 270
(fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ arg_nos))))
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 271
val alpha_rhs =
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 272
HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2)));
1288
+ − 273
fun alpha_arg ((dt, arg_no), (arg, arg2)) =
+ − 274
let
+ − 275
val relevant = filter (fn ((_, i, j), _) => i = arg_no orelse j = arg_no) bind_pis;
+ − 276
in
+ − 277
if relevant = [] then (
+ − 278
if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2)
+ − 279
else (HOLogic.mk_eq (arg, arg2)))
+ − 280
else
+ − 281
if is_rec_type dt then let
+ − 282
(* THE HARD CASE *)
+ − 283
val (rbinds, rpis) = split_list relevant
+ − 284
val lhs_binds = fv_binds args rbinds
+ − 285
val lhs = mk_pair (lhs_binds, arg);
+ − 286
val rhs_binds = fv_binds args2 rbinds;
+ − 287
val rhs = mk_pair (rhs_binds, arg2);
+ − 288
val alpha = nth alpha_frees (body_index dt);
+ − 289
val fv = nth fv_frees (body_index dt);
1359
+ − 290
val pi = foldr1 add_perm (distinct (op =) rpis);
1288
+ − 291
val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs;
1325
+ − 292
val alpha_gen = Syntax.check_term lthy alpha_gen_pre
1357
42b7abf779ec
Gather bindings with same binder, and generate only one permutation for them.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 293
(* val pi_supps = map ((curry op $) @{term "supp :: perm \<Rightarrow> atom set"}) rpis;
42b7abf779ec
Gather bindings with same binder, and generate only one permutation for them.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 294
val pi_supps_eq = HOLogic.mk_eq (mk_inter pi_supps, @{term "{} :: atom set"}) *)
1288
+ − 295
in
1357
42b7abf779ec
Gather bindings with same binder, and generate only one permutation for them.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 296
(*if length pi_supps > 1 then HOLogic.mk_conj (alpha_gen, pi_supps_eq) else*)
42b7abf779ec
Gather bindings with same binder, and generate only one permutation for them.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 297
alpha_gen
1288
+ − 298
(* TODO Add some test that is makes sense *)
+ − 299
end else @{term "True"}
+ − 300
end
+ − 301
val alphas = map alpha_arg (dts ~~ arg_nos ~~ (args ~~ args2))
+ − 302
val alpha_lhss = mk_conjl alphas
+ − 303
val alpha_lhss_ex =
+ − 304
fold (fn pi_str => fn t => HOLogic.mk_exists (pi_str, @{typ perm}, t)) pi_strs alpha_lhss
+ − 305
val alpha_eq = Logic.mk_implies (HOLogic.mk_Trueprop alpha_lhss_ex, alpha_rhs)
1173
+ − 306
in
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 307
(fv_eq, alpha_eq)
1168
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 308
end;
1302
+ − 309
fun fv_alpha_eq (i, (_, _, constrs)) binds = map2i (fv_alpha_constr i) constrs binds;
1376
+ − 310
val fveqs_alphaeqs = map2i fv_alpha_eq descr (gather_binds bindsall)
+ − 311
val (fv_eqs_perfv, alpha_eqs) = apsnd flat (split_list (map split_list fveqs_alphaeqs))
+ − 312
val rel_bns_nos = map (fn (_, i, _) => i) rel_bns;
+ − 313
fun filter_fun (a, b) = b mem rel_bns_nos;
+ − 314
val all_fvs = (fv_names ~~ fv_eqs_perfv) ~~ (0 upto (length fv_names - 1))
+ − 315
val (fv_names_fst, fv_eqs_fst) = apsnd flat (split_list (map fst (filter_out filter_fun all_fvs)))
+ − 316
val (fv_names_snd, fv_eqs_snd) = apsnd flat (split_list (map fst (filter filter_fun all_fvs)))
+ − 317
val fv_eqs_all = fv_eqs_fst @ (flat fv_bn_eqs);
+ − 318
val fv_names_all = fv_names_fst @ fv_bn_names;
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 319
val add_binds = map (fn x => (Attrib.empty_binding, x))
1375
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 320
(* Function_Fun.add_fun Function_Common.default_config ... true *)
1376
+ − 321
val _ = map tracing (map (Syntax.string_of_term @{context}) fv_eqs_all)
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 322
val (fvs, lthy') = (Primrec.add_primrec
1375
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 323
(map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_all) (add_binds fv_eqs_all) lthy)
1376
+ − 324
val (fvs2, lthy'') =
+ − 325
if fv_eqs_snd = [] then (([], []), lthy') else
+ − 326
(Primrec.add_primrec
+ − 327
(map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_snd) (add_binds fv_eqs_snd) lthy')
+ − 328
val (alphas, lthy''') = (Inductive.add_inductive_i
1325
+ − 329
{quiet_mode = true, verbose = false, alt_name = Binding.empty,
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 330
coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 331
(map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) alpha_names alpha_types) []
1376
+ − 332
(add_binds alpha_eqs) [] lthy'')
1178
+ − 333
in
1377
+ − 334
((fvs, alphas), lthy''')
1178
+ − 335
end
1168
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 336
*}
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 337
1375
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 338
(*
1178
+ − 339
atom_decl name
+ − 340
1375
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 341
datatype lam =
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 342
VAR "name"
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 343
| APP "lam" "lam"
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 344
| LET "bp" "lam"
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 345
and bp =
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 346
BP "name" "lam"
1185
+ − 347
1375
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 348
primrec
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 349
bi::"bp \<Rightarrow> atom set"
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 350
where
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 351
"bi (BP x t) = {atom x}"
1185
+ − 352
1375
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 353
setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.lam") 2 *}
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 354
1185
+ − 355
1375
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 356
local_setup {*
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 357
snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.lam")
1379
+ − 358
[[[], [], [(SOME (@{term bi}, false), 0, 1)]], [[]]] [(@{term bi}, 1, [[0]])] *}
1375
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 359
print_theorems
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 360
*)
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 361
aa787c9b6955
A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 362
(*
1178
+ − 363
datatype rtrm1 =
+ − 364
rVr1 "name"
+ − 365
| rAp1 "rtrm1" "rtrm1"
+ − 366
| rLm1 "name" "rtrm1" --"name is bound in trm1"
+ − 367
| rLt1 "bp" "rtrm1" "rtrm1" --"all variables in bp are bound in the 2nd trm1"
+ − 368
and bp =
+ − 369
BUnit
+ − 370
| BVr "name"
+ − 371
| BPr "bp" "bp"
+ − 372
+ − 373
(* to be given by the user *)
+ − 374
1358
+ − 375
primrec
1178
+ − 376
bv1
+ − 377
where
+ − 378
"bv1 (BUnit) = {}"
+ − 379
| "bv1 (BVr x) = {atom x}"
+ − 380
| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"
+ − 381
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 382
setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Fv.rtrm1", "Fv.bp"] *}
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 383
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 384
local_setup {* define_fv_alpha "Fv.rtrm1"
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 385
[[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]],
1178
+ − 386
[[], [[]], [[], []]]] *}
1168
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 387
print_theorems
1193
a228acf2907e
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 388
*)
1180
+ − 389
1199
+ − 390
1196
+ − 391
ML {*
1199
+ − 392
fun alpha_inj_tac dist_inj intrs elims =
+ − 393
SOLVED' (asm_full_simp_tac (HOL_ss addsimps intrs)) ORELSE'
1216
+ − 394
(rtac @{thm iffI} THEN' RANGE [
1199
+ − 395
(eresolve_tac elims THEN_ALL_NEW
+ − 396
asm_full_simp_tac (HOL_ss addsimps dist_inj)
+ − 397
),
1216
+ − 398
asm_full_simp_tac (HOL_ss addsimps intrs)])
1199
+ − 399
*}
+ − 400
+ − 401
ML {*
+ − 402
fun build_alpha_inj_gl thm =
+ − 403
let
+ − 404
val prop = prop_of thm;
+ − 405
val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop);
+ − 406
val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop);
+ − 407
fun list_conj l = foldr1 HOLogic.mk_conj l;
+ − 408
in
+ − 409
if hyps = [] then concl
+ − 410
else HOLogic.mk_eq (concl, list_conj hyps)
+ − 411
end;
+ − 412
*}
+ − 413
+ − 414
ML {*
+ − 415
fun build_alpha_inj intrs dist_inj elims ctxt =
1196
+ − 416
let
1199
+ − 417
val ((_, thms_imp), ctxt') = Variable.import false intrs ctxt;
+ − 418
val gls = map (HOLogic.mk_Trueprop o build_alpha_inj_gl) thms_imp;
+ − 419
fun tac _ = alpha_inj_tac dist_inj intrs elims 1;
+ − 420
val thms = map (fn gl => Goal.prove ctxt' [] [] gl tac) gls;
1196
+ − 421
in
1199
+ − 422
Variable.export ctxt' ctxt thms
1168
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 423
end
1196
+ − 424
*}
+ − 425
1207
+ − 426
ML {*
1214
+ − 427
fun build_alpha_refl_gl alphas (x, y, z) =
1207
+ − 428
let
+ − 429
fun build_alpha alpha =
+ − 430
let
+ − 431
val ty = domain_type (fastype_of alpha);
1214
+ − 432
val var = Free(x, ty);
+ − 433
val var2 = Free(y, ty);
+ − 434
val var3 = Free(z, ty);
1209
+ − 435
val symp = HOLogic.mk_imp (alpha $ var $ var2, alpha $ var2 $ var);
+ − 436
val transp = HOLogic.mk_imp (alpha $ var $ var2,
1214
+ − 437
HOLogic.mk_all (z, ty,
1209
+ − 438
HOLogic.mk_imp (alpha $ var2 $ var3, alpha $ var $ var3)))
1207
+ − 439
in
1209
+ − 440
((alpha $ var $ var), (symp, transp))
1208
+ − 441
end;
1209
+ − 442
val (refl_eqs, eqs) = split_list (map build_alpha alphas)
+ − 443
val (sym_eqs, trans_eqs) = split_list eqs
+ − 444
fun conj l = @{term Trueprop} $ foldr1 HOLogic.mk_conj l
1207
+ − 445
in
1209
+ − 446
(conj refl_eqs, (conj sym_eqs, conj trans_eqs))
1196
+ − 447
end
1207
+ − 448
*}
+ − 449
1213
+ − 450
ML {*
1333
+ − 451
fun reflp_tac induct inj ctxt =
1213
+ − 452
rtac induct THEN_ALL_NEW
1333
+ − 453
simp_tac ((mk_minimal_ss ctxt) addsimps inj) THEN_ALL_NEW
+ − 454
split_conjs THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}
+ − 455
THEN_ALL_NEW split_conjs THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps
+ − 456
@{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv
+ − 457
add_0_left supp_zero_perm Int_empty_left})
1213
+ − 458
*}
+ − 459
1333
+ − 460
1301
+ − 461
lemma exi_neg: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>pi. Q pi"
+ − 462
apply (erule exE)
+ − 463
apply (rule_tac x="-pi" in exI)
+ − 464
by auto
+ − 465
1213
+ − 466
ML {*
1334
+ − 467
fun symp_tac induct inj eqvt ctxt =
+ − 468
ind_tac induct THEN_ALL_NEW
+ − 469
simp_tac ((mk_minimal_ss ctxt) addsimps inj) THEN_ALL_NEW split_conjs
+ − 470
THEN_ALL_NEW
+ − 471
REPEAT o etac @{thm exi_neg}
+ − 472
THEN_ALL_NEW
+ − 473
split_conjs THEN_ALL_NEW
+ − 474
asm_full_simp_tac (HOL_ss addsimps @{thms supp_minus_perm minus_add[symmetric]}) THEN_ALL_NEW
+ − 475
(rtac @{thm alpha_gen_compose_sym} THEN' RANGE [
+ − 476
(asm_full_simp_tac (HOL_ss addsimps @{thms plus_perm_eq})),
+ − 477
(asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt)))
+ − 478
])
1213
+ − 479
*}
+ − 480
+ − 481
ML {*
1217
+ − 482
fun imp_elim_tac case_rules =
+ − 483
Subgoal.FOCUS (fn {concl, context, ...} =>
+ − 484
case term_of concl of
+ − 485
_ $ (_ $ asm $ _) =>
+ − 486
let
+ − 487
fun filter_fn case_rule = (
+ − 488
case Logic.strip_assums_hyp (prop_of case_rule) of
+ − 489
((_ $ asmc) :: _) =>
+ − 490
let
+ − 491
val thy = ProofContext.theory_of context
+ − 492
in
+ − 493
Pattern.matches thy (asmc, asm)
+ − 494
end
+ − 495
| _ => false)
+ − 496
val matching_rules = filter filter_fn case_rules
+ − 497
in
+ − 498
(rtac impI THEN' rotate_tac (~1) THEN' eresolve_tac matching_rules) 1
+ − 499
end
+ − 500
| _ => no_tac
+ − 501
)
+ − 502
*}
+ − 503
1301
+ − 504
+ − 505
lemma exi_sum: "\<exists>(pi :: perm). P pi \<Longrightarrow> \<exists>(pi :: perm). Q pi \<Longrightarrow> (\<And>(p :: perm) (pi :: perm). P p \<Longrightarrow> Q pi \<Longrightarrow> R (pi + p)) \<Longrightarrow> \<exists>pi. R pi"
+ − 506
apply (erule exE)+
+ − 507
apply (rule_tac x="pia + pi" in exI)
+ − 508
by auto
+ − 509
1217
+ − 510
ML {*
1339
5256f256edd8
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 511
fun is_ex (Const ("Ex", _) $ Abs _) = true
5256f256edd8
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 512
| is_ex _ = false;
5256f256edd8
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 513
*}
5256f256edd8
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 514
5256f256edd8
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 515
ML {*
5256f256edd8
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 516
fun eetac rule = Subgoal.FOCUS_PARAMS
5256f256edd8
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 517
(fn (focus) =>
5256f256edd8
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 518
let
5256f256edd8
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 519
val concl = #concl focus
5256f256edd8
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 520
val prems = Logic.strip_imp_prems (term_of concl)
5256f256edd8
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 521
val exs = filter (fn x => is_ex (HOLogic.dest_Trueprop x)) prems
5256f256edd8
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 522
val cexs = map (SOME o (cterm_of (ProofContext.theory_of (#context focus)))) exs
5256f256edd8
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 523
val thins = map (fn cex => Drule.instantiate' [] [cex] Drule.thin_rl) cexs
5256f256edd8
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 524
in
5256f256edd8
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 525
(etac rule THEN' RANGE[
5256f256edd8
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 526
atac,
5256f256edd8
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 527
eresolve_tac thins
5256f256edd8
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 528
]) 1
5256f256edd8
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 529
end
5256f256edd8
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 530
)
5256f256edd8
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 531
*}
5256f256edd8
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 532
5256f256edd8
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 533
ML {*
1217
+ − 534
fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt =
1339
5256f256edd8
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 535
ind_tac induct THEN_ALL_NEW
1217
+ − 536
(TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW
1339
5256f256edd8
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 537
asm_full_simp_tac ((mk_minimal_ss ctxt) addsimps alpha_inj) THEN_ALL_NEW
5256f256edd8
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 538
split_conjs THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) THEN_ALL_NEW split_conjs
5256f256edd8
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 539
THEN_ALL_NEW (asm_full_simp_tac (HOL_ss addsimps (term_inj @ distinct)))
5256f256edd8
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 540
THEN_ALL_NEW split_conjs THEN_ALL_NEW
5256f256edd8
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 541
TRY o (etac @{thm alpha_gen_compose_trans} THEN' RANGE[atac]) THEN_ALL_NEW
5256f256edd8
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 542
(asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ eqvt @ term_inj @ distinct)))
1213
+ − 543
*}
+ − 544
1215
+ − 545
lemma transp_aux:
+ − 546
"(\<And>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z)) \<Longrightarrow> transp R"
+ − 547
unfolding transp_def
+ − 548
by blast
+ − 549
+ − 550
ML {*
+ − 551
fun equivp_tac reflps symps transps =
+ − 552
simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def})
1221
+ − 553
THEN' rtac conjI THEN' rtac allI THEN'
1215
+ − 554
resolve_tac reflps THEN'
1221
+ − 555
rtac conjI THEN' rtac allI THEN' rtac allI THEN'
1215
+ − 556
resolve_tac symps THEN'
+ − 557
rtac @{thm transp_aux} THEN' resolve_tac transps
+ − 558
*}
+ − 559
1213
+ − 560
ML {*
1214
+ − 561
fun build_equivps alphas term_induct alpha_induct term_inj alpha_inj distinct cases eqvt ctxt =
1213
+ − 562
let
1214
+ − 563
val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt;
+ − 564
val (reflg, (symg, transg)) = build_alpha_refl_gl alphas (x, y, z)
1333
+ − 565
fun reflp_tac' _ = reflp_tac term_induct alpha_inj ctxt 1;
1334
+ − 566
fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt ctxt 1;
1217
+ − 567
fun transp_tac' _ = transp_tac ctxt alpha_induct alpha_inj term_inj distinct cases eqvt 1;
1214
+ − 568
val reflt = Goal.prove ctxt' [] [] reflg reflp_tac';
+ − 569
val symt = Goal.prove ctxt' [] [] symg symp_tac';
+ − 570
val transt = Goal.prove ctxt' [] [] transg transp_tac';
+ − 571
val [refltg, symtg, transtg] = Variable.export ctxt' ctxt [reflt, symt, transt]
1215
+ − 572
val reflts = HOLogic.conj_elims refltg
+ − 573
val symts = HOLogic.conj_elims symtg
+ − 574
val transts = HOLogic.conj_elims transtg
1214
+ − 575
fun equivp alpha =
+ − 576
let
1215
+ − 577
val equivp = Const (@{const_name equivp}, fastype_of alpha --> @{typ bool})
+ − 578
val goal = @{term Trueprop} $ (equivp $ alpha)
+ − 579
fun tac _ = equivp_tac reflts symts transts 1
+ − 580
in
+ − 581
Goal.prove ctxt [] [] goal tac
+ − 582
end
1213
+ − 583
in
1215
+ − 584
map equivp alphas
1213
+ − 585
end
+ − 586
*}
1207
+ − 587
1217
+ − 588
(*
+ − 589
Tests:
+ − 590
prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *}
+ − 591
by (tactic {* reflp_tac @{thm rtrm1_bp.induct} @{thms alpha1_inj} 1 *})
+ − 592
+ − 593
prove alpha1_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *}
+ − 594
by (tactic {* symp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms alpha1_eqvt} 1 *})
+ − 595
+ − 596
prove alpha1_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *}
+ − 597
by (tactic {* transp_tac @{context} @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms rtrm1.inject bp.inject} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} 1 *})
+ − 598
+ − 599
lemma alpha1_equivp:
+ − 600
"equivp alpha_rtrm1"
+ − 601
"equivp alpha_bp"
+ − 602
apply (tactic {*
+ − 603
(simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def})
+ − 604
THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN'
+ − 605
resolve_tac (HOLogic.conj_elims @{thm alpha1_reflp_aux})
+ − 606
THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN'
+ − 607
resolve_tac (HOLogic.conj_elims @{thm alpha1_symp_aux}) THEN' rtac @{thm transp_aux}
+ − 608
THEN' resolve_tac (HOLogic.conj_elims @{thm alpha1_transp_aux})
+ − 609
)
+ − 610
1 *})
+ − 611
done*)
+ − 612
1308
+ − 613
ML {*
+ − 614
fun dtyp_no_of_typ _ (TFree (n, _)) = error "dtyp_no_of_typ: Illegal free"
+ − 615
| dtyp_no_of_typ _ (TVar _) = error "dtyp_no_of_typ: Illegal schematic"
+ − 616
| dtyp_no_of_typ dts (Type (tname, Ts)) =
+ − 617
case try (find_index (curry op = tname o fst)) dts of
+ − 618
NONE => error "dtyp_no_of_typ: Illegal recursion"
+ − 619
| SOME i => i
+ − 620
*}
+ − 621
1207
+ − 622
end