53 val spec = post simps |
53 val spec = post simps |
54 |> map (apfst (apsnd (fn ats => moreatts @ ats))) |
54 |> map (apfst (apsnd (fn ats => moreatts @ ats))) |
55 |> map (apfst (apfst extra_qualify)) |
55 |> map (apfst (apfst extra_qualify)) |
56 |
56 |
57 val (saved_spec_simps, lthy) = |
57 val (saved_spec_simps, lthy) = |
58 fold_map note_theorem spec lthy |
58 fold_map (LocalTheory.note Thm.theoremK) spec lthy |
59 |
59 |
60 val saved_simps = flat (map snd saved_spec_simps) |
60 val saved_simps = flat (map snd saved_spec_simps) |
61 val simps_by_f = sort saved_simps |
61 val simps_by_f = sort saved_simps |
62 |
62 |
63 fun add_for_f fname simps = |
63 fun add_for_f fname simps = |
76 val qualify = Long_Name.qualify defname |
76 val qualify = Long_Name.qualify defname |
77 val addsmps = add_simps fnames post sort_cont |
77 val addsmps = add_simps fnames post sort_cont |
78 |
78 |
79 val (((psimps', pinducts'), (_, [termination'])), lthy) = |
79 val (((psimps', pinducts'), (_, [termination'])), lthy) = |
80 lthy |
80 lthy |
81 |> addsmps (Long_Name.qualify "partial") "psimps" |
81 |> addsmps (Binding.qualify false "partial") "psimps" |
82 psimp_attribs psimps |
82 psimp_attribs psimps |
83 ||> fold_option (snd oo addsmps I "simps" simp_attribs) trsimps |
83 ||> fold_option (snd oo addsmps I "simps" simp_attribs) trsimps |
84 ||>> note_theorem ((qualify "pinduct", |
84 ||>> note_theorem ((qualify "pinduct", |
85 [Attrib.internal (K (RuleCases.case_names cnames)), |
85 [Attrib.internal (K (RuleCases.case_names cnames)), |
86 Attrib.internal (K (RuleCases.consumes 1)), |
86 Attrib.internal (K (RuleCases.consumes 1)), |
104 fun gen_add_fundef is_external prep default_constraint fixspec eqns config lthy = |
104 fun gen_add_fundef is_external prep default_constraint fixspec eqns config lthy = |
105 let |
105 let |
106 val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx)) |
106 val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx)) |
107 val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy |
107 val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy |
108 val fixes = map (apfst (apfst Binding.name_of)) fixes0; |
108 val fixes = map (apfst (apfst Binding.name_of)) fixes0; |
109 val spec = map (fn ((b, atts), prop) => ((Binding.name_of b, atts), [prop])) spec0; |
109 val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0; |
110 val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config ctxt' fixes spec |
110 val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config ctxt' fixes spec |
111 |
111 |
112 val defname = mk_defname fixes |
112 val defname = mk_defname fixes |
113 |
113 |
114 val ((goalstate, cont), lthy) = |
114 val ((goalstate, cont), lthy) = |