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_fn_frees 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 (nth permute_fn_frees (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_fn_frees 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 = (nth permute_fn_frees 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_fn_frees 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 *} |
85 *} |
85 *} |
86 |
86 |
87 ML {* |
87 ML {* |
88 fun prove_permute_plus lthy induct perm_defs perm_fns = |
88 fun prove_permute_plus lthy induct perm_defs perm_fns = |
89 let |
89 let |
90 val pi1 = Free ("p", @{typ perm}) |
90 val p = Free ("p", @{typ perm}) |
91 val pi2 = Free ("q", @{typ perm}) |
91 val q = Free ("q", @{typ perm}) |
92 val perm_types = map (body_type o fastype_of) perm_fns |
92 val perm_types = map (body_type o fastype_of) perm_fns |
93 val perm_indnames = Datatype_Prop.make_tnames perm_types |
93 val perm_indnames = Datatype_Prop.make_tnames perm_types |
94 |
94 |
95 fun single_goal ((perm, T), x) = HOLogic.mk_eq |
95 fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq |
96 (perm $ (mk_plus pi1 pi2) $ Free (x, T), perm $ pi1 $ (perm $ pi2 $ Free (x, T))) |
96 (perm_fn $ (mk_plus p q) $ Free (x, T), perm_fn $ p $ (perm_fn $ q $ Free (x, T))) |
97 |
97 |
98 val goals = |
98 val goals = |
99 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
99 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
100 (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) |
100 (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) |
101 |
101 |
111 |
111 |
112 ML {* |
112 ML {* |
113 (* defines the permutation functions for raw datatypes and |
113 (* defines the permutation functions for raw datatypes and |
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 user_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_descr sorts induct_thm user_dt_nos thy = |
120 let |
120 let |
121 val {descr as dt_descr, induct, sorts, ...} = dt_info; |
|
122 val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr; |
121 val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr; |
123 val full_tnames = List.take (all_full_tnames, dt_nos); |
122 val user_full_tnames = List.take (all_full_tnames, user_dt_nos); |
124 |
123 |
125 val perm_fn_names = prefix_dt_names dt_descr sorts "permute_" |
124 val perm_fn_names = prefix_dt_names dt_descr sorts "permute_" |
126 |
125 val perm_fn_types = map (fn (i, _) => perm_ty (nth_dtyp dt_descr sorts i)) dt_descr |
127 val perm_types = map (fn (i, _) => perm_ty (nth_dtyp dt_descr sorts i)) dt_descr |
126 val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types) |
128 |
|
129 val permute_fns = perm_fn_names ~~ perm_types |
|
130 |
127 |
131 fun perm_eq (i, (_, _, constrs)) = |
128 fun perm_eq (i, (_, _, constrs)) = |
132 map (perm_eq_constr dt_descr sorts permute_fns i) constrs; |
129 map (perm_eq_constr dt_descr sorts perm_fn_frees i) constrs; |
133 |
130 |
134 val perm_eqs = maps perm_eq dt_descr; |
131 val perm_eqs = maps perm_eq dt_descr; |
135 |
132 |
136 val lthy = |
133 val lthy = |
137 Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy; |
134 Theory_Target.instantiation (user_full_tnames, [], @{sort pt}) thy; |
138 |
135 |
139 val ((perm_fns, perm_ldef), lthy') = |
136 val ((perm_funs, perm_eq_thms), lthy') = |
140 Primrec.add_primrec |
137 Primrec.add_primrec |
141 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy; |
138 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy; |
142 |
139 |
143 val perm_zero_thms = prove_permute_zero lthy' induct perm_ldef perm_fns |
140 val perm_zero_thms = prove_permute_zero lthy' induct_thm perm_eq_thms perm_funs |
144 val perm_plus_thms = prove_permute_plus lthy' induct perm_ldef perm_fns |
141 val perm_plus_thms = prove_permute_plus lthy' induct_thm perm_eq_thms perm_funs |
145 val perm_zero_thms' = List.take (perm_zero_thms, dt_nos); |
142 val perm_zero_thms' = List.take (perm_zero_thms, user_dt_nos); |
146 val perm_plus_thms' = List.take (perm_plus_thms, dt_nos) |
143 val perm_plus_thms' = List.take (perm_plus_thms, user_dt_nos) |
147 val perms_name = space_implode "_" perm_fn_names |
144 val perms_name = space_implode "_" perm_fn_names |
148 val perms_zero_bind = Binding.name (perms_name ^ "_zero") |
145 val perms_zero_bind = Binding.name (perms_name ^ "_zero") |
149 val perms_plus_bind = Binding.name (perms_name ^ "_plus") |
146 val perms_plus_bind = Binding.name (perms_name ^ "_plus") |
150 |
147 |
151 fun tac _ (_, simps, _) = |
148 fun tac _ (_, simps, _) = |
156 in |
153 in |
157 lthy' |
154 lthy' |
158 |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms')) |
155 |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms')) |
159 |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms')) |
156 |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms')) |
160 |> Class_Target.prove_instantiation_exit_result morphism tac |
157 |> Class_Target.prove_instantiation_exit_result morphism tac |
161 (perm_ldef, perm_zero_thms' @ perm_plus_thms', perm_fns) |
158 (perm_eq_thms, perm_zero_thms' @ perm_plus_thms', perm_funs) |
162 end |
159 end |
163 *} |
160 *} |
|
161 |
|
162 |
|
163 |
|
164 |
164 |
165 |
165 (* permutations for quotient types *) |
166 (* permutations for quotient types *) |
166 |
167 |
167 ML {* |
168 ML {* |
168 fun quotient_lift_consts_export qtys spec ctxt = |
169 fun quotient_lift_consts_export qtys spec ctxt = |