30 |
30 |
31 - in case the argument is recursive it returns |
31 - in case the argument is recursive it returns |
32 |
32 |
33 permute_fn p arg |
33 permute_fn p arg |
34 |
34 |
35 - in case the argument is non-recursive it will build |
35 - in case the argument is non-recursive it will return |
36 |
36 |
37 p o arg |
37 p o arg |
38 |
38 |
39 *) |
39 *) |
40 fun perm_arg permute_fns pi (arg_dty, arg) = |
40 fun perm_arg permute_fns p (arg_dty, arg) = |
41 if Datatype_Aux.is_rec_type arg_dty |
41 if Datatype_Aux.is_rec_type arg_dty |
42 then Free (nth permute_fns (Datatype_Aux.body_index arg_dty)) $ pi $ arg |
42 then Free (nth permute_fns (Datatype_Aux.body_index arg_dty)) $ p $ arg |
43 else mk_perm pi arg |
43 else mk_perm p arg |
44 *} |
44 *} |
45 |
45 |
46 ML {* |
46 ML {* |
47 (* equation for permutation function for one constructor; |
47 (* generates the equation for the permutation function for one constructor; |
48 i is the index of the correspodning datatype *) |
48 i is the index of the corresponding datatype *) |
49 fun perm_eq_constr dt_descr sorts permute_fns i (cnstr_name, dts) = |
49 fun perm_eq_constr dt_descr sorts permute_fns i (cnstr_name, dts) = |
50 let |
50 let |
51 val pi = Free ("p", @{typ perm}) |
51 val p = Free ("p", @{typ perm}) |
52 val arg_tys = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts |
52 val arg_tys = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts |
53 val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys) |
53 val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys) |
54 val args = map Free (arg_names ~~ arg_tys) |
54 val args = map Free (arg_names ~~ arg_tys) |
55 val cnstr = Const (cnstr_name, arg_tys ---> (nth_dtyp dt_descr sorts i)) |
55 val cnstr = Const (cnstr_name, arg_tys ---> (nth_dtyp dt_descr sorts i)) |
56 val lhs = Free (nth permute_fns i) $ pi $ list_comb (cnstr, args) |
56 val lhs = Free (nth permute_fns i) $ p $ list_comb (cnstr, args) |
57 val rhs = list_comb (cnstr, map (perm_arg permute_fns pi) (dts ~~ args)) |
57 val rhs = list_comb (cnstr, map (perm_arg permute_fns p) (dts ~~ args)) |
58 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |
58 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |
59 in |
59 in |
60 (Attrib.empty_binding, eq) |
60 (Attrib.empty_binding, eq) |
61 end |
61 end |
62 *} |
62 *} |
114 proves that they are instances of pt |
114 proves that they are instances of pt |
115 |
115 |
116 dt_nos refers to the number of "un-unfolded" datatypes |
116 dt_nos refers to the number of "un-unfolded" datatypes |
117 given by the user |
117 given by the user |
118 *) |
118 *) |
119 fun define_raw_perms (dt_info : Datatype_Aux.info) dt_nos thy = |
119 fun define_raw_perms (dt_info : Datatype_Aux.info) thy = |
120 let |
120 let |
121 val {descr as dt_descr, induct, sorts, ...} = dt_info; |
121 val {descr as dt_descr, induct, sorts, ...} = dt_info; |
|
122 val dt_nos = length descr |
122 val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr; |
123 val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr; |
123 val full_tnames = List.take (all_full_tnames, dt_nos); |
124 val full_tnames = List.take (all_full_tnames, dt_nos); |
124 |
125 |
125 val perm_fn_names = prefix_dt_names dt_descr sorts "permute_" |
126 val perm_fn_names = prefix_dt_names dt_descr sorts "permute_" |
126 |
127 |
160 |> Class_Target.prove_instantiation_exit_result morphism tac |
161 |> Class_Target.prove_instantiation_exit_result morphism tac |
161 (perm_ldef, perm_zero_thms' @ perm_plus_thms', perm_fns) |
162 (perm_ldef, perm_zero_thms' @ perm_plus_thms', perm_fns) |
162 end |
163 end |
163 *} |
164 *} |
164 |
165 |
|
166 |
|
167 |
|
168 |
|
169 |
165 (* permutations for quotient types *) |
170 (* permutations for quotient types *) |
166 |
171 |
167 ML {* |
172 ML {* |
168 fun quotient_lift_consts_export qtys spec ctxt = |
173 fun quotient_lift_consts_export qtys spec ctxt = |
169 let |
174 let |