35 - in case the argument is non-recursive it will return |
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 p (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)) $ p $ arg |
42 then (nth permute_fn_frees (Datatype_Aux.body_index arg_dty)) $ p $ arg |
43 else mk_perm p arg |
43 else mk_perm p arg |
44 *} |
44 *} |
45 |
45 |
46 ML {* |
46 ML {* |
47 (* generates the equation for the permutation function for one constructor; |
47 (* generates the equation for the permutation function for one constructor; |
48 i is the index of the corresponding 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 p = 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) $ p $ 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 p) (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 |
121 val {descr as dt_descr, induct, sorts, ...} = dt_info; |
121 val {descr as dt_descr, induct, sorts, ...} = dt_info; |
122 val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr; |
122 val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr; |
123 val user_full_tnames = List.take (all_full_tnames, user_dt_nos); |
123 val user_full_tnames = List.take (all_full_tnames, user_dt_nos); |
124 |
124 |
125 val perm_fn_names = prefix_dt_names dt_descr sorts "permute_" |
125 val perm_fn_names = prefix_dt_names dt_descr sorts "permute_" |
126 |
126 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 |
127 val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types) |
128 |
|
129 val permute_fns = perm_fn_names ~~ perm_types |
|
130 |
128 |
131 fun perm_eq (i, (_, _, constrs)) = |
129 fun perm_eq (i, (_, _, constrs)) = |
132 map (perm_eq_constr dt_descr sorts permute_fns i) constrs; |
130 map (perm_eq_constr dt_descr sorts perm_fn_frees i) constrs; |
133 |
131 |
134 val perm_eqs = maps perm_eq dt_descr; |
132 val perm_eqs = maps perm_eq dt_descr; |
135 |
133 |
136 val lthy = |
134 val lthy = |
137 Theory_Target.instantiation (user_full_tnames, [], @{sort pt}) thy; |
135 Theory_Target.instantiation (user_full_tnames, [], @{sort pt}) thy; |
138 |
136 |
139 val ((perm_fns, perm_ldef), lthy') = |
137 val ((perm_funs, perm_eq_thms), lthy') = |
140 Primrec.add_primrec |
138 Primrec.add_primrec |
141 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy; |
139 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy; |
142 |
140 |
143 val perm_zero_thms = prove_permute_zero lthy' induct perm_ldef perm_fns |
141 val perm_zero_thms = prove_permute_zero lthy' induct perm_eq_thms perm_funs |
144 val perm_plus_thms = prove_permute_plus lthy' induct perm_ldef perm_fns |
142 val perm_plus_thms = prove_permute_plus lthy' induct perm_eq_thms perm_funs |
145 val perm_zero_thms' = List.take (perm_zero_thms, user_dt_nos); |
143 val perm_zero_thms' = List.take (perm_zero_thms, user_dt_nos); |
146 val perm_plus_thms' = List.take (perm_plus_thms, user_dt_nos) |
144 val perm_plus_thms' = List.take (perm_plus_thms, user_dt_nos) |
147 val perms_name = space_implode "_" perm_fn_names |
145 val perms_name = space_implode "_" perm_fn_names |
148 val perms_zero_bind = Binding.name (perms_name ^ "_zero") |
146 val perms_zero_bind = Binding.name (perms_name ^ "_zero") |
149 val perms_plus_bind = Binding.name (perms_name ^ "_plus") |
147 val perms_plus_bind = Binding.name (perms_name ^ "_plus") |
156 in |
154 in |
157 lthy' |
155 lthy' |
158 |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms')) |
156 |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms')) |
159 |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms')) |
157 |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms')) |
160 |> Class_Target.prove_instantiation_exit_result morphism tac |
158 |> Class_Target.prove_instantiation_exit_result morphism tac |
161 (perm_ldef, perm_zero_thms' @ perm_plus_thms', perm_fns) |
159 (perm_eq_thms, perm_zero_thms' @ perm_plus_thms', perm_funs) |
162 end |
160 end |
163 *} |
161 *} |
164 |
162 |
165 |
163 |
166 |
164 |