38 |
38 |
39 val note_theorem = LocalTheory.note Thm.theoremK |
39 val note_theorem = LocalTheory.note Thm.theoremK |
40 |
40 |
41 fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" |
41 fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" |
42 |
42 |
43 fun add_simps fnames post sort label moreatts simps lthy = |
43 fun add_simps fnames post sort extra_qualify label moreatts simps lthy = |
44 let |
44 let |
45 val atts = Attrib.internal (K Simplifier.simp_add) :: moreatts |
45 val atts = Attrib.internal (K Simplifier.simp_add) :: moreatts |
46 val spec = post simps |
46 val spec = post simps |
47 |> map (apfst (apsnd (append atts))) |
47 |> map (apfst (apsnd (append atts))) |
|
48 |> map (apfst (apfst extra_qualify)) |
48 |
49 |
49 val (saved_spec_simps, lthy) = |
50 val (saved_spec_simps, lthy) = |
50 fold_map note_theorem spec lthy |
51 fold_map note_theorem spec lthy |
51 |
52 |
52 val saved_simps = flat (map snd saved_spec_simps) |
53 val saved_simps = flat (map snd saved_spec_simps) |
59 fold2 add_for_f fnames simps_by_f lthy) |
60 fold2 add_for_f fnames simps_by_f lthy) |
60 end |
61 end |
61 |
62 |
62 fun fundef_afterqed config fixes post defname cont sort_cont cnames [[proof]] lthy = |
63 fun fundef_afterqed config fixes post defname cont sort_cont cnames [[proof]] lthy = |
63 let |
64 let |
64 val FundefResult {fs, R, psimps, trsimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = |
65 val FundefResult {fs, R, psimps, trsimps, simple_pinducts, termination, domintros, cases, ...} = |
65 cont (Goal.close_result proof) |
66 cont (Goal.close_result proof) |
66 |
67 |
67 val fnames = map (fst o fst) fixes |
68 val fnames = map (fst o fst) fixes |
68 val qualify = NameSpace.qualified defname |
69 val qualify = NameSpace.qualified defname |
69 val addsmps = add_simps fnames post sort_cont |
70 val addsmps = add_simps fnames post sort_cont |
70 |
71 |
71 val (((psimps', pinducts'), (_, [termination'])), lthy) = |
72 val (((psimps', pinducts'), (_, [termination'])), lthy) = |
72 lthy |
73 lthy |
73 |> addsmps "psimps" [] psimps |
74 |> addsmps (NameSpace.qualified "partial") "psimps" [] psimps |
74 ||> fold_option (snd oo addsmps "simps" []) trsimps |
75 ||> fold_option (snd oo addsmps I "simps" []) trsimps |
75 ||>> note_theorem ((qualify "pinduct", |
76 ||>> note_theorem ((qualify "pinduct", |
76 [Attrib.internal (K (RuleCases.case_names cnames)), |
77 [Attrib.internal (K (RuleCases.case_names cnames)), |
77 Attrib.internal (K (RuleCases.consumes 1)), |
78 Attrib.internal (K (RuleCases.consumes 1)), |
78 Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts) |
79 Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts) |
79 ||>> note_theorem ((qualify "termination", []), [termination]) |
80 ||>> note_theorem ((qualify "termination", []), [termination]) |
123 val allatts = if has_guards then [] else [Attrib.internal (K RecfunCodegen.add_default)] |
124 val allatts = if has_guards then [] else [Attrib.internal (K RecfunCodegen.add_default)] |
124 |
125 |
125 val qualify = NameSpace.qualified defname; |
126 val qualify = NameSpace.qualified defname; |
126 in |
127 in |
127 lthy |
128 lthy |
128 |> add_simps "simps" allatts tsimps |> snd |
129 |> add_simps I "simps" allatts tsimps |> snd |
129 |> note_theorem ((qualify "induct", [Attrib.internal (K (RuleCases.case_names case_names))]), tinduct) |> snd |
130 |> note_theorem ((qualify "induct", [Attrib.internal (K (RuleCases.case_names case_names))]), tinduct) |> snd |
130 end |
131 end |
131 |
132 |
132 |
133 |
133 fun setup_termination_proof term_opt lthy = |
134 fun setup_termination_proof term_opt lthy = |