equal
deleted
inserted
replaced
114 proves that they are instances of pt |
114 proves that they are instances of pt |
115 |
115 |
116 user_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) user_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 user_full_tnames = List.take (all_full_tnames, user_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 val perm_fn_types = map (fn (i, _) => perm_ty (nth_dtyp dt_descr sorts i)) dt_descr |
125 val perm_fn_types = map (fn (i, _) => perm_ty (nth_dtyp dt_descr sorts i)) dt_descr |
136 |
135 |
137 val ((perm_funs, perm_eq_thms), lthy') = |
136 val ((perm_funs, perm_eq_thms), lthy') = |
138 Primrec.add_primrec |
137 Primrec.add_primrec |
139 (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; |
140 |
139 |
141 val perm_zero_thms = prove_permute_zero lthy' induct perm_eq_thms perm_funs |
140 val perm_zero_thms = prove_permute_zero lthy' induct_thm perm_eq_thms perm_funs |
142 val perm_plus_thms = prove_permute_plus lthy' induct perm_eq_thms perm_funs |
141 val perm_plus_thms = prove_permute_plus lthy' induct_thm perm_eq_thms perm_funs |
143 val perm_zero_thms' = List.take (perm_zero_thms, user_dt_nos); |
142 val perm_zero_thms' = List.take (perm_zero_thms, user_dt_nos); |
144 val perm_plus_thms' = List.take (perm_plus_thms, user_dt_nos) |
143 val perm_plus_thms' = List.take (perm_plus_thms, user_dt_nos) |
145 val perms_name = space_implode "_" perm_fn_names |
144 val perms_name = space_implode "_" perm_fn_names |
146 val perms_zero_bind = Binding.name (perms_name ^ "_zero") |
145 val perms_zero_bind = Binding.name (perms_name ^ "_zero") |
147 val perms_plus_bind = Binding.name (perms_name ^ "_plus") |
146 val perms_plus_bind = Binding.name (perms_name ^ "_plus") |