2297
|
1 |
(* Title: nominal_dt_rawfuns.ML
|
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>
parents:
diff
changeset
|
2 |
Author: Cezary Kaliszyk
|
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>
parents:
diff
changeset
|
3 |
Author: Christian Urban
|
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>
parents:
diff
changeset
|
4 |
|
2297
|
5 |
Definitions of the raw fv and fv_bn functions
|
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>
parents:
diff
changeset
|
6 |
*)
|
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>
parents:
diff
changeset
|
7 |
|
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>
parents:
diff
changeset
|
8 |
signature NOMINAL_DT_RAWFUNS =
|
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>
parents:
diff
changeset
|
9 |
sig
|
2295
|
10 |
(* info of binding functions *)
|
|
11 |
type bn_info = (term * int * (int * term option) list 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>
parents:
diff
changeset
|
12 |
|
2295
|
13 |
(* binding modes and binding clauses *)
|
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>
parents:
diff
changeset
|
14 |
datatype bmode = Lst | Res | Set
|
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>
parents:
diff
changeset
|
15 |
datatype bclause = BC of bmode * (term option * int) list * int 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>
parents:
diff
changeset
|
16 |
|
2296
|
17 |
val is_atom: Proof.context -> typ -> bool
|
|
18 |
val is_atom_set: Proof.context -> typ -> bool
|
|
19 |
val is_atom_fset: Proof.context -> typ -> bool
|
|
20 |
val is_atom_list: Proof.context -> typ -> bool
|
|
21 |
val mk_atom_set: term -> term
|
|
22 |
val mk_atom_fset: term -> term
|
|
23 |
|
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>
parents:
diff
changeset
|
24 |
val setify: Proof.context -> term -> term
|
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>
parents:
diff
changeset
|
25 |
val listify: Proof.context -> term -> term
|
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>
parents:
diff
changeset
|
26 |
|
2407
|
27 |
val define_raw_fvs: string list -> typ list -> cns_info list -> bn_info -> bclause list list list ->
|
2410
2bbdb9c427b5
improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
28 |
thm list -> thm list -> Proof.context -> term list * term list * thm list * thm list * local_theory
|
2305
|
29 |
|
|
30 |
val raw_prove_eqvt: term list -> thm list -> thm list -> Proof.context -> thm 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>
parents:
diff
changeset
|
31 |
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>
parents:
diff
changeset
|
32 |
|
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>
parents:
diff
changeset
|
33 |
|
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>
parents:
diff
changeset
|
34 |
structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS =
|
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>
parents:
diff
changeset
|
35 |
struct
|
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>
parents:
diff
changeset
|
36 |
|
2375
|
37 |
(* term - is constant of the bn-function
|
|
38 |
int - is datatype number over which the bn-function is defined
|
|
39 |
int * term option - is number of the corresponding argument with possibly
|
|
40 |
recursive call with bn-function term
|
|
41 |
*)
|
2295
|
42 |
type bn_info = (term * int * (int * term option) list list) list
|
|
43 |
|
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>
parents:
diff
changeset
|
44 |
datatype bmode = Lst | Res | Set
|
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>
parents:
diff
changeset
|
45 |
datatype bclause = BC of bmode * (term option * int) list * int 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>
parents:
diff
changeset
|
46 |
|
2292
|
47 |
(* testing for concrete atom types *)
|
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>
parents:
diff
changeset
|
48 |
fun is_atom ctxt ty =
|
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>
parents:
diff
changeset
|
49 |
Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base})
|
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>
parents:
diff
changeset
|
50 |
|
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>
parents:
diff
changeset
|
51 |
fun is_atom_set ctxt (Type ("fun", [t, @{typ bool}])) = is_atom ctxt 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>
parents:
diff
changeset
|
52 |
| is_atom_set _ _ = false;
|
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>
parents:
diff
changeset
|
53 |
|
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>
parents:
diff
changeset
|
54 |
fun is_atom_fset ctxt (Type (@{type_name "fset"}, [t])) = is_atom ctxt 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>
parents:
diff
changeset
|
55 |
| is_atom_fset _ _ = false;
|
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>
parents:
diff
changeset
|
56 |
|
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>
parents:
diff
changeset
|
57 |
fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt 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>
parents:
diff
changeset
|
58 |
| is_atom_list _ _ = false
|
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>
parents:
diff
changeset
|
59 |
|
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>
parents:
diff
changeset
|
60 |
|
2292
|
61 |
(* functions for producing sets, fsets and lists of general atom type
|
|
62 |
out from concrete atom types *)
|
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>
parents:
diff
changeset
|
63 |
fun mk_atom_set 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>
parents:
diff
changeset
|
64 |
let
|
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>
parents:
diff
changeset
|
65 |
val ty = fastype_of t;
|
2290
|
66 |
val atom_ty = HOLogic.dest_setT ty --> @{typ "atom"};
|
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>
parents:
diff
changeset
|
67 |
val img_ty = atom_ty --> ty --> @{typ "atom set"};
|
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>
parents:
diff
changeset
|
68 |
in
|
2292
|
69 |
Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t
|
|
70 |
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>
parents:
diff
changeset
|
71 |
|
2321
|
72 |
|
|
73 |
fun dest_fsetT (Type (@{type_name fset}, [T])) = T
|
|
74 |
| dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
|
|
75 |
|
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>
parents:
diff
changeset
|
76 |
fun mk_atom_fset 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>
parents:
diff
changeset
|
77 |
let
|
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>
parents:
diff
changeset
|
78 |
val ty = fastype_of t;
|
2290
|
79 |
val atom_ty = dest_fsetT ty --> @{typ "atom"};
|
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>
parents:
diff
changeset
|
80 |
val fmap_ty = atom_ty --> ty --> @{typ "atom fset"};
|
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>
parents:
diff
changeset
|
81 |
val fset_to_set = @{term "fset_to_set :: atom fset => atom set"}
|
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>
parents:
diff
changeset
|
82 |
in
|
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>
parents:
diff
changeset
|
83 |
fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)
|
2292
|
84 |
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>
parents:
diff
changeset
|
85 |
|
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>
parents:
diff
changeset
|
86 |
fun mk_atom_list 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>
parents:
diff
changeset
|
87 |
let
|
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>
parents:
diff
changeset
|
88 |
val ty = fastype_of 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>
parents:
diff
changeset
|
89 |
val atom_ty = dest_listT ty --> @{typ atom};
|
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>
parents:
diff
changeset
|
90 |
val map_ty = atom_ty --> ty --> @{typ "atom 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>
parents:
diff
changeset
|
91 |
in
|
2292
|
92 |
Const (@{const_name map}, map_ty) $ mk_atom_ty atom_ty t
|
|
93 |
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>
parents:
diff
changeset
|
94 |
|
2295
|
95 |
(* functions that coerces singletons, sets and fsets of concrete atoms
|
|
96 |
into sets of general atoms *)
|
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>
parents:
diff
changeset
|
97 |
fun setify ctxt 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>
parents:
diff
changeset
|
98 |
let
|
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>
parents:
diff
changeset
|
99 |
val ty = fastype_of 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>
parents:
diff
changeset
|
100 |
in
|
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>
parents:
diff
changeset
|
101 |
if is_atom ctxt ty
|
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>
parents:
diff
changeset
|
102 |
then HOLogic.mk_set @{typ atom} [mk_atom 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>
parents:
diff
changeset
|
103 |
else if is_atom_set ctxt ty
|
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>
parents:
diff
changeset
|
104 |
then mk_atom_set 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>
parents:
diff
changeset
|
105 |
else if is_atom_fset ctxt ty
|
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>
parents:
diff
changeset
|
106 |
then mk_atom_fset 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>
parents:
diff
changeset
|
107 |
else raise TERM ("setify", [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>
parents:
diff
changeset
|
108 |
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>
parents:
diff
changeset
|
109 |
|
2295
|
110 |
(* functions that coerces singletons and lists of concrete atoms
|
|
111 |
into lists of general atoms *)
|
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>
parents:
diff
changeset
|
112 |
fun listify ctxt 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>
parents:
diff
changeset
|
113 |
let
|
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>
parents:
diff
changeset
|
114 |
val ty = fastype_of 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>
parents:
diff
changeset
|
115 |
in
|
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>
parents:
diff
changeset
|
116 |
if is_atom ctxt ty
|
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>
parents:
diff
changeset
|
117 |
then HOLogic.mk_list @{typ atom} [mk_atom 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>
parents:
diff
changeset
|
118 |
else if is_atom_list ctxt ty
|
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>
parents:
diff
changeset
|
119 |
then mk_atom_set 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>
parents:
diff
changeset
|
120 |
else raise TERM ("listify", [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>
parents:
diff
changeset
|
121 |
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>
parents:
diff
changeset
|
122 |
|
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>
parents:
diff
changeset
|
123 |
(* coerces a list into a set *)
|
2290
|
124 |
fun to_set t =
|
|
125 |
if fastype_of t = @{typ "atom list"}
|
|
126 |
then @{term "set::atom list => atom set"} $ t
|
|
127 |
else t
|
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>
parents:
diff
changeset
|
128 |
|
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>
parents:
diff
changeset
|
129 |
|
2295
|
130 |
(** functions that construct the equations for fv and fv_bn **)
|
2292
|
131 |
|
|
132 |
fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) =
|
|
133 |
let
|
2295
|
134 |
fun mk_fv_body fv_map args i =
|
|
135 |
let
|
|
136 |
val arg = nth args i
|
|
137 |
val ty = fastype_of arg
|
|
138 |
in
|
|
139 |
case AList.lookup (op=) fv_map ty of
|
|
140 |
NONE => mk_supp arg
|
|
141 |
| SOME fv => fv $ arg
|
|
142 |
end
|
|
143 |
|
|
144 |
fun mk_fv_binder lthy fv_bn_map args (bn_option, i) =
|
|
145 |
let
|
|
146 |
val arg = nth args i
|
|
147 |
in
|
|
148 |
case bn_option of
|
|
149 |
NONE => (setify lthy arg, @{term "{}::atom set"})
|
|
150 |
| SOME bn => (to_set (bn $ arg), the (AList.lookup (op=) fv_bn_map bn) $ arg)
|
|
151 |
end
|
|
152 |
|
2292
|
153 |
val t1 = map (mk_fv_body fv_map args) bodies
|
|
154 |
val (t2, t3) = split_list (map (mk_fv_binder lthy fv_bn_map args) binders)
|
|
155 |
in
|
|
156 |
fold_union (mk_diff (fold_union t1, fold_union t2)::t3)
|
|
157 |
end
|
|
158 |
|
2293
|
159 |
(* in case of fv_bn we have to treat the case special, where an
|
|
160 |
"empty" binding clause is given *)
|
2292
|
161 |
fun mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause =
|
2295
|
162 |
let
|
|
163 |
fun mk_fv_bn_body fv_map fv_bn_map bn_args args i =
|
|
164 |
let
|
|
165 |
val arg = nth args i
|
|
166 |
val ty = fastype_of arg
|
|
167 |
in
|
|
168 |
case AList.lookup (op=) bn_args i of
|
|
169 |
NONE => (case (AList.lookup (op=) fv_map ty) of
|
|
170 |
NONE => mk_supp arg
|
2296
|
171 |
| SOME fv => fv $ arg)
|
2295
|
172 |
| SOME (NONE) => @{term "{}::atom set"}
|
|
173 |
| SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg
|
|
174 |
end
|
|
175 |
in
|
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>
parents:
diff
changeset
|
176 |
case bclause of
|
2292
|
177 |
BC (_, [], bodies) => fold_union (map (mk_fv_bn_body fv_map fv_bn_map bn_args args) bodies)
|
2293
|
178 |
| _ => mk_fv_rhs lthy fv_map fv_bn_map args bclause
|
2295
|
179 |
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>
parents:
diff
changeset
|
180 |
|
2296
|
181 |
fun mk_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys, _) bclauses =
|
2292
|
182 |
let
|
|
183 |
val arg_names = Datatype_Prop.make_tnames arg_tys
|
|
184 |
val args = map Free (arg_names ~~ arg_tys)
|
|
185 |
val fv = the (AList.lookup (op=) fv_map ty)
|
|
186 |
val lhs = fv $ list_comb (constr, args)
|
|
187 |
val rhs_trms = map (mk_fv_rhs lthy fv_map fv_bn_map args) bclauses
|
|
188 |
val rhs = fold_union rhs_trms
|
|
189 |
in
|
|
190 |
HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
|
|
191 |
end
|
|
192 |
|
2296
|
193 |
fun mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, _, arg_tys, _)) bclauses =
|
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>
parents:
diff
changeset
|
194 |
let
|
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>
parents:
diff
changeset
|
195 |
val arg_names = Datatype_Prop.make_tnames arg_tys
|
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>
parents:
diff
changeset
|
196 |
val args = map Free (arg_names ~~ arg_tys)
|
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>
parents:
diff
changeset
|
197 |
val fv_bn = the (AList.lookup (op=) fv_bn_map bn_trm)
|
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>
parents:
diff
changeset
|
198 |
val lhs = fv_bn $ list_comb (constr, args)
|
2292
|
199 |
val rhs_trms = map (mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args) bclauses
|
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>
parents:
diff
changeset
|
200 |
val rhs = fold_union rhs_trms
|
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>
parents:
diff
changeset
|
201 |
in
|
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>
parents:
diff
changeset
|
202 |
HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
|
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>
parents:
diff
changeset
|
203 |
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>
parents:
diff
changeset
|
204 |
|
2292
|
205 |
fun mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) =
|
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>
parents:
diff
changeset
|
206 |
let
|
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>
parents:
diff
changeset
|
207 |
val nth_constrs_info = nth constrs_info bn_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>
parents:
diff
changeset
|
208 |
val nth_bclausess = nth bclausesss bn_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>
parents:
diff
changeset
|
209 |
in
|
2292
|
210 |
map2 (mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess
|
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>
parents:
diff
changeset
|
211 |
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>
parents:
diff
changeset
|
212 |
|
2410
2bbdb9c427b5
improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
213 |
fun define_raw_fvs raw_full_ty_names raw_tys cns_info bn_info bclausesss constr_thms size_simps lthy =
|
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>
parents:
diff
changeset
|
214 |
let
|
2407
|
215 |
val fv_names = map (prefix "fv_" o Long_Name.base_name) raw_full_ty_names
|
|
216 |
val fv_tys = map (fn ty => ty --> @{typ "atom set"}) raw_tys
|
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>
parents:
diff
changeset
|
217 |
val fv_frees = map Free (fv_names ~~ fv_tys);
|
2407
|
218 |
val fv_map = raw_tys ~~ fv_frees
|
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>
parents:
diff
changeset
|
219 |
|
2295
|
220 |
val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info)
|
|
221 |
val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns
|
|
222 |
val fv_bn_names = map (prefix "fv_") bn_names
|
2407
|
223 |
val fv_bn_arg_tys = map (nth raw_tys) bn_tys
|
2295
|
224 |
val fv_bn_tys = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys
|
|
225 |
val fv_bn_frees = map Free (fv_bn_names ~~ fv_bn_tys)
|
|
226 |
val fv_bn_map = bns ~~ fv_bn_frees
|
2292
|
227 |
|
2407
|
228 |
val fv_eqs = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) cns_info bclausesss
|
|
229 |
val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map cns_info bclausesss) bn_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>
parents:
diff
changeset
|
230 |
|
2295
|
231 |
val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
|
|
232 |
val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs)
|
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>
parents:
diff
changeset
|
233 |
|
2295
|
234 |
val (_, lthy') = Function.add_function all_fun_names all_fun_eqs
|
2304
|
235 |
Function_Common.default_config (pat_completeness_simp constr_thms) lthy
|
2410
2bbdb9c427b5
improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
236 |
|
2bbdb9c427b5
improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
237 |
val (info, lthy'') = prove_termination size_simps (Local_Theory.restore lthy')
|
2bbdb9c427b5
improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
238 |
|
2305
|
239 |
val {fs, simps, inducts, ...} = 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>
parents:
diff
changeset
|
240 |
|
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>
parents:
diff
changeset
|
241 |
val morphism = ProofContext.export_morphism lthy'' lthy
|
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>
parents:
diff
changeset
|
242 |
val fs_exp = map (Morphism.term morphism) fs
|
2409
|
243 |
val simps_exp = map (Morphism.thm morphism) (the simps)
|
|
244 |
val inducts_exp = map (Morphism.thm morphism) (the inducts)
|
2410
2bbdb9c427b5
improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
245 |
val (fvs_exp, fv_bns_exp) = chop (length fv_frees) fs_exp
|
2305
|
246 |
in
|
2410
2bbdb9c427b5
improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
247 |
(fvs_exp, fv_bns_exp, simps_exp, inducts_exp, lthy'')
|
2305
|
248 |
end
|
|
249 |
|
|
250 |
|
|
251 |
(** equivarance proofs **)
|
|
252 |
|
2311
|
253 |
val eqvt_apply_sym = @{thm eqvt_apply[symmetric]}
|
|
254 |
|
|
255 |
fun subproof_tac const_names simps =
|
2388
|
256 |
SUBPROOF (fn {prems, context, ...} =>
|
2311
|
257 |
HEADGOAL
|
|
258 |
(simp_tac (HOL_basic_ss addsimps simps)
|
|
259 |
THEN' Nominal_Permeq.eqvt_tac context [] const_names
|
2388
|
260 |
THEN' simp_tac (HOL_basic_ss addsimps (prems @ [eqvt_apply_sym]))))
|
2311
|
261 |
|
|
262 |
fun prove_eqvt_tac insts ind_thms const_names simps ctxt =
|
|
263 |
HEADGOAL
|
|
264 |
(Object_Logic.full_atomize_tac
|
|
265 |
THEN' (DETERM o (InductTacs.induct_rules_tac ctxt insts ind_thms))
|
|
266 |
THEN_ALL_NEW subproof_tac const_names simps ctxt)
|
|
267 |
|
2305
|
268 |
fun mk_eqvt_goal pi const arg =
|
|
269 |
let
|
|
270 |
val lhs = mk_perm pi (const $ arg)
|
|
271 |
val rhs = const $ (mk_perm pi arg)
|
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>
parents:
diff
changeset
|
272 |
in
|
2305
|
273 |
HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
|
|
274 |
end
|
|
275 |
|
|
276 |
fun raw_prove_eqvt consts ind_thms simps ctxt =
|
2308
|
277 |
if null consts then []
|
|
278 |
else
|
|
279 |
let
|
|
280 |
val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
|
|
281 |
val p = Free (p, @{typ perm})
|
|
282 |
val arg_tys =
|
|
283 |
consts
|
|
284 |
|> map fastype_of
|
|
285 |
|> map domain_type
|
2311
|
286 |
val (arg_names, ctxt'') =
|
|
287 |
Variable.variant_fixes (Datatype_Prop.make_tnames arg_tys) ctxt'
|
2308
|
288 |
val args = map Free (arg_names ~~ arg_tys)
|
|
289 |
val goals = map2 (mk_eqvt_goal p) consts args
|
|
290 |
val insts = map (single o SOME) arg_names
|
2311
|
291 |
val const_names = map (fst o dest_Const) consts
|
2308
|
292 |
in
|
2311
|
293 |
Goal.prove_multi ctxt'' [] [] goals (fn {context, ...} =>
|
|
294 |
prove_eqvt_tac insts ind_thms const_names simps context)
|
2308
|
295 |
|> ProofContext.export ctxt'' ctxt
|
|
296 |
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>
parents:
diff
changeset
|
297 |
|
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>
parents:
diff
changeset
|
298 |
end (* structure *)
|
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>
parents:
diff
changeset
|
299 |
|