1 theory Fv |
1 theory Fv |
2 imports "Nominal2_Atoms" "Abs" "Perm" "Rsp" |
2 imports "Nominal2_Atoms" "Abs" "Perm" "Rsp" |
3 begin |
3 begin |
4 |
4 |
|
5 (* TODO: update the comment *) |
5 (* Bindings are given as a list which has a length being equal |
6 (* Bindings are given as a list which has a length being equal |
6 to the length of the number of constructors. |
7 to the length of the number of constructors. |
7 |
8 |
8 Each element is a list whose length is equal to the number |
9 Each element is a list whose length is equal to the number |
9 of arguents. |
10 of arguents. |
57 ML {* |
58 ML {* |
58 fun map2i _ [] [] = [] |
59 fun map2i _ [] [] = [] |
59 | map2i f (x :: xs) (y :: ys) = f x y :: map2i f xs ys |
60 | map2i f (x :: xs) (y :: ys) = f x y :: map2i f xs ys |
60 | map2i f (x :: xs) [] = f x [] :: map2i f xs [] |
61 | map2i f (x :: xs) [] = f x [] :: map2i f xs [] |
61 | map2i _ _ _ = raise UnequalLengths; |
62 | map2i _ _ _ = raise UnequalLengths; |
|
63 *} |
|
64 |
|
65 ML {* |
|
66 fun gather_binds binds = |
|
67 let |
|
68 fun gather_binds_cons binds = |
|
69 let |
|
70 val common = map (fn (f, bi, _) => (f, bi)) binds |
|
71 val nodups = distinct (op =) common |
|
72 fun find_bodys (sf, sbi) = |
|
73 filter (fn (f, bi, _) => f = sf andalso bi = sbi) binds |
|
74 val bodys = map ((map (fn (_, _, bo) => bo)) o find_bodys) nodups |
|
75 in |
|
76 nodups ~~ bodys |
|
77 end |
|
78 in |
|
79 map (map gather_binds_cons) binds |
|
80 end |
|
81 *} |
|
82 |
|
83 ML {* |
|
84 fun un_gather_binds_cons binds = |
|
85 flat (map (fn (((f, bi), bos), pi) => map (fn bo => ((f, bi, bo), pi)) bos) binds) |
62 *} |
86 *} |
63 |
87 |
64 ML {* |
88 ML {* |
65 open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *); |
89 open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *); |
66 (* TODO: It is the same as one in 'nominal_atoms' *) |
90 (* TODO: It is the same as one in 'nominal_atoms' *) |
108 |
132 |
109 (* TODO: Notice datatypes without bindings and replace alpha with equality *) |
133 (* TODO: Notice datatypes without bindings and replace alpha with equality *) |
110 ML {* |
134 ML {* |
111 fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall lthy = |
135 fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall lthy = |
112 let |
136 let |
113 val thy = ProofContext.theory_of lthy; |
|
114 val {descr, sorts, ...} = dt_info; |
137 val {descr, sorts, ...} = dt_info; |
115 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
138 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
116 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
139 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
117 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
140 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
118 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
141 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
126 val Ts = map (typ_of_dtyp descr sorts) dts; |
149 val Ts = map (typ_of_dtyp descr sorts) dts; |
127 val bindslen = length bindcs |
150 val bindslen = length bindcs |
128 val pi_strs_same = replicate bindslen "pi" |
151 val pi_strs_same = replicate bindslen "pi" |
129 val pi_strs = Name.variant_list [] pi_strs_same; |
152 val pi_strs = Name.variant_list [] pi_strs_same; |
130 val pis = map (fn ps => Free (ps, @{typ perm})) pi_strs; |
153 val pis = map (fn ps => Free (ps, @{typ perm})) pi_strs; |
131 val bind_pis = bindcs ~~ pis; |
154 val bind_pis_gath = bindcs ~~ pis; |
|
155 val bind_pis = un_gather_binds_cons bind_pis_gath; |
|
156 val bindcs = map fst bind_pis; |
132 val names = Name.variant_list pi_strs (Datatype_Prop.make_tnames Ts); |
157 val names = Name.variant_list pi_strs (Datatype_Prop.make_tnames Ts); |
133 val args = map Free (names ~~ Ts); |
158 val args = map Free (names ~~ Ts); |
134 val names2 = Name.variant_list (pi_strs @ names) (Datatype_Prop.make_tnames Ts); |
159 val names2 = Name.variant_list (pi_strs @ names) (Datatype_Prop.make_tnames Ts); |
135 val args2 = map Free (names2 ~~ Ts); |
160 val args2 = map Free (names2 ~~ Ts); |
136 val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp)); |
161 val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp)); |
179 val alpha = nth alpha_frees (body_index dt); |
204 val alpha = nth alpha_frees (body_index dt); |
180 val fv = nth fv_frees (body_index dt); |
205 val fv = nth fv_frees (body_index dt); |
181 val pi = foldr1 add_perm rpis; |
206 val pi = foldr1 add_perm rpis; |
182 val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; |
207 val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; |
183 val alpha_gen = Syntax.check_term lthy alpha_gen_pre |
208 val alpha_gen = Syntax.check_term lthy alpha_gen_pre |
184 val pi_supps = map ((curry op $) @{term "supp :: perm \<Rightarrow> atom set"}) rpis; |
209 (* val pi_supps = map ((curry op $) @{term "supp :: perm \<Rightarrow> atom set"}) rpis; |
185 val pi_supps_eq = HOLogic.mk_eq (mk_inter pi_supps, @{term "{} :: atom set"}) |
210 val pi_supps_eq = HOLogic.mk_eq (mk_inter pi_supps, @{term "{} :: atom set"}) *) |
186 in |
211 in |
187 (*if length pi_supps > 1 then |
212 (*if length pi_supps > 1 then HOLogic.mk_conj (alpha_gen, pi_supps_eq) else*) |
188 HOLogic.mk_conj (alpha_gen, pi_supps_eq) else*) alpha_gen |
213 alpha_gen |
189 (* TODO Add some test that is makes sense *) |
214 (* TODO Add some test that is makes sense *) |
190 end else @{term "True"} |
215 end else @{term "True"} |
191 end |
216 end |
192 val alphas = map alpha_arg (dts ~~ arg_nos ~~ (args ~~ args2)) |
217 val alphas = map alpha_arg (dts ~~ arg_nos ~~ (args ~~ args2)) |
193 val alpha_lhss = mk_conjl alphas |
218 val alpha_lhss = mk_conjl alphas |
196 val alpha_eq = Logic.mk_implies (HOLogic.mk_Trueprop alpha_lhss_ex, alpha_rhs) |
221 val alpha_eq = Logic.mk_implies (HOLogic.mk_Trueprop alpha_lhss_ex, alpha_rhs) |
197 in |
222 in |
198 (fv_eq, alpha_eq) |
223 (fv_eq, alpha_eq) |
199 end; |
224 end; |
200 fun fv_alpha_eq (i, (_, _, constrs)) binds = map2i (fv_alpha_constr i) constrs binds; |
225 fun fv_alpha_eq (i, (_, _, constrs)) binds = map2i (fv_alpha_constr i) constrs binds; |
201 val (fv_eqs, alpha_eqs) = split_list (flat (map2i fv_alpha_eq descr bindsall)) |
226 val (fv_eqs, alpha_eqs) = split_list (flat (map2i fv_alpha_eq descr (gather_binds bindsall))) |
202 val add_binds = map (fn x => (Attrib.empty_binding, x)) |
227 val add_binds = map (fn x => (Attrib.empty_binding, x)) |
203 val (fvs, lthy') = (Primrec.add_primrec |
228 val (fvs, lthy') = (Primrec.add_primrec |
204 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) (add_binds fv_eqs) lthy) |
229 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) (add_binds fv_eqs) lthy) |
205 val (alphas, lthy'') = (Inductive.add_inductive_i |
230 val (alphas, lthy'') = (Inductive.add_inductive_i |
206 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
231 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |