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) thy = |
119 fun define_raw_perms (dt_info : Datatype_Aux.info) user_dt_nos 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 dt_descr |
|
123 val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr; |
122 val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr; |
124 val full_tnames = List.take (all_full_tnames, dt_nos); |
123 val user_full_tnames = List.take (all_full_tnames, user_dt_nos); |
125 |
124 |
126 val perm_fn_names = prefix_dt_names dt_descr sorts "permute_" |
125 val perm_fn_names = prefix_dt_names dt_descr sorts "permute_" |
127 |
126 |
128 val perm_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 |
129 |
128 |
133 map (perm_eq_constr dt_descr sorts permute_fns i) constrs; |
132 map (perm_eq_constr dt_descr sorts permute_fns i) constrs; |
134 |
133 |
135 val perm_eqs = maps perm_eq dt_descr; |
134 val perm_eqs = maps perm_eq dt_descr; |
136 |
135 |
137 val lthy = |
136 val lthy = |
138 Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy; |
137 Theory_Target.instantiation (user_full_tnames, [], @{sort pt}) thy; |
139 |
138 |
140 val ((perm_fns, perm_ldef), lthy') = |
139 val ((perm_fns, perm_ldef), lthy') = |
141 Primrec.add_primrec |
140 Primrec.add_primrec |
142 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy; |
141 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy; |
143 |
142 |
144 val perm_zero_thms = prove_permute_zero lthy' induct perm_ldef perm_fns |
143 val perm_zero_thms = prove_permute_zero lthy' induct perm_ldef perm_fns |
145 val perm_plus_thms = prove_permute_plus lthy' induct perm_ldef perm_fns |
144 val perm_plus_thms = prove_permute_plus lthy' induct perm_ldef perm_fns |
146 val perm_zero_thms' = List.take (perm_zero_thms, dt_nos); |
145 val perm_zero_thms' = List.take (perm_zero_thms, user_dt_nos); |
147 val perm_plus_thms' = List.take (perm_plus_thms, dt_nos) |
146 val perm_plus_thms' = List.take (perm_plus_thms, user_dt_nos) |
148 val perms_name = space_implode "_" perm_fn_names |
147 val perms_name = space_implode "_" perm_fn_names |
149 val perms_zero_bind = Binding.name (perms_name ^ "_zero") |
148 val perms_zero_bind = Binding.name (perms_name ^ "_zero") |
150 val perms_plus_bind = Binding.name (perms_name ^ "_plus") |
149 val perms_plus_bind = Binding.name (perms_name ^ "_plus") |
151 |
150 |
152 fun tac _ (_, simps, _) = |
151 fun tac _ (_, simps, _) = |