118 (Const ("0", Ind_Syntax.iT), |
118 (Const ("0", Ind_Syntax.iT), |
119 #2 recursor_pair, Const ("0", Ind_Syntax.iT))) |
119 #2 recursor_pair, Const ("0", Ind_Syntax.iT))) |
120 | SOME (rhs, cargs', eq) => |
120 | SOME (rhs, cargs', eq) => |
121 (rhs, inst_recursor (recursor_pair, cargs'), eq) |
121 (rhs, inst_recursor (recursor_pair, cargs'), eq) |
122 val allowed_terms = map use_fabs (#2 (strip_comb recursor_rhs)) |
122 val allowed_terms = map use_fabs (#2 (strip_comb recursor_rhs)) |
123 val abs = foldr absterm rhs allowed_terms |
123 val abs = List.foldr absterm rhs allowed_terms |
124 in |
124 in |
125 if !Ind_Syntax.trace then |
125 if !Ind_Syntax.trace then |
126 writeln ("recursor_rhs = " ^ |
126 writeln ("recursor_rhs = " ^ |
127 Syntax.string_of_term_global thy recursor_rhs ^ |
127 Syntax.string_of_term_global thy recursor_rhs ^ |
128 "\nabs = " ^ Syntax.string_of_term_global thy abs) |
128 "\nabs = " ^ Syntax.string_of_term_global thy abs) |
143 Ind_Syntax.iT) |
143 Ind_Syntax.iT) |
144 |
144 |
145 val def_tm = Logic.mk_equals |
145 val def_tm = Logic.mk_equals |
146 (subst_bound (rec_arg, fabs), |
146 (subst_bound (rec_arg, fabs), |
147 list_comb (recursor, |
147 list_comb (recursor, |
148 foldr add_case [] (cnames ~~ recursor_pairs)) |
148 List.foldr add_case [] (cnames ~~ recursor_pairs)) |
149 $ rec_arg) |
149 $ rec_arg) |
150 |
150 |
151 in |
151 in |
152 if !Ind_Syntax.trace then |
152 if !Ind_Syntax.trace then |
153 writeln ("primrec def:\n" ^ |
153 writeln ("primrec def:\n" ^ |
162 |
162 |
163 fun add_primrec_i args thy = |
163 fun add_primrec_i args thy = |
164 let |
164 let |
165 val ((eqn_names, eqn_terms), eqn_atts) = apfst split_list (split_list args); |
165 val ((eqn_names, eqn_terms), eqn_atts) = apfst split_list (split_list args); |
166 val SOME (fname, ftype, ls, rs, con_info, eqns) = |
166 val SOME (fname, ftype, ls, rs, con_info, eqns) = |
167 foldr (process_eqn thy) NONE eqn_terms; |
167 List.foldr (process_eqn thy) NONE eqn_terms; |
168 val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns); |
168 val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns); |
169 |
169 |
170 val ([def_thm], thy1) = thy |
170 val ([def_thm], thy1) = thy |
171 |> Sign.add_path (Sign.base_name fname) |
171 |> Sign.add_path (Sign.base_name fname) |
172 |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name def)]; |
172 |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name def)]; |