41 |
41 |
42 val psimp_attribs = map (Attrib.internal o K) |
42 val psimp_attribs = map (Attrib.internal o K) |
43 [Simplifier.simp_add, |
43 [Simplifier.simp_add, |
44 Nitpick_Psimps.add] |
44 Nitpick_Psimps.add] |
45 |
45 |
46 fun note_theorem ((binding, atts), ths) = |
|
47 LocalTheory.note "" ((binding, atts), ths) |
|
48 |
|
49 fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" |
46 fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" |
50 |
47 |
51 fun add_simps fnames post sort extra_qualify label mod_binding moreatts simps lthy = |
48 fun add_simps fnames post sort extra_qualify label mod_binding moreatts simps lthy = |
52 let |
49 let |
53 val spec = post simps |
50 val spec = post simps |
54 |> map (apfst (apsnd (fn ats => moreatts @ ats))) |
51 |> map (apfst (apsnd (fn ats => moreatts @ ats))) |
55 |> map (apfst (apfst extra_qualify)) |
52 |> map (apfst (apfst extra_qualify)) |
56 |
53 |
57 val (saved_spec_simps, lthy) = |
54 val (saved_spec_simps, lthy) = |
58 fold_map (LocalTheory.note "") spec lthy |
55 fold_map LocalTheory.note spec lthy |
59 |
56 |
60 val saved_simps = maps snd saved_spec_simps |
57 val saved_simps = maps snd saved_spec_simps |
61 val simps_by_f = sort saved_simps |
58 val simps_by_f = sort saved_simps |
62 |
59 |
63 fun add_for_f fname simps = |
60 fun add_for_f fname simps = |
64 note_theorem ((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps) |
61 LocalTheory.note ((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps) |
65 #> snd |
62 #> snd |
66 in |
63 in |
67 (saved_simps, |
64 (saved_simps, |
68 fold2 add_for_f fnames simps_by_f lthy) |
65 fold2 add_for_f fnames simps_by_f lthy) |
69 end |
66 end |
98 val (((psimps', pinducts'), (_, [termination'])), lthy) = |
95 val (((psimps', pinducts'), (_, [termination'])), lthy) = |
99 lthy |
96 lthy |
100 |> addsmps (conceal_partial o Binding.qualify false "partial") |
97 |> addsmps (conceal_partial o Binding.qualify false "partial") |
101 "psimps" conceal_partial psimp_attribs psimps |
98 "psimps" conceal_partial psimp_attribs psimps |
102 ||> fold_option (snd oo addsmps I "simps" I simp_attribs) trsimps |
99 ||> fold_option (snd oo addsmps I "simps" I simp_attribs) trsimps |
103 ||>> note_theorem ((conceal_partial (qualify "pinduct"), |
100 ||>> LocalTheory.note ((conceal_partial (qualify "pinduct"), |
104 [Attrib.internal (K (Rule_Cases.case_names cnames)), |
101 [Attrib.internal (K (Rule_Cases.case_names cnames)), |
105 Attrib.internal (K (Rule_Cases.consumes 1)), |
102 Attrib.internal (K (Rule_Cases.consumes 1)), |
106 Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts) |
103 Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts) |
107 ||>> note_theorem ((Binding.conceal (qualify "termination"), []), [termination]) |
104 ||>> LocalTheory.note ((Binding.conceal (qualify "termination"), []), [termination]) |
108 ||> (snd o note_theorem ((qualify "cases", |
105 ||> (snd o LocalTheory.note ((qualify "cases", |
109 [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases])) |
106 [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases])) |
110 ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros |
107 ||> fold_option (snd oo curry LocalTheory.note (qualify "domintros", [])) domintros |
111 |
108 |
112 val cdata = FunctionCtxData { add_simps=addsmps, case_names=cnames, psimps=psimps', |
109 val cdata = FunctionCtxData { add_simps=addsmps, case_names=cnames, psimps=psimps', |
113 pinducts=snd pinducts', termination=termination', |
110 pinducts=snd pinducts', termination=termination', |
114 fs=fs, R=R, defname=defname } |
111 fs=fs, R=R, defname=defname } |
115 val _ = |
112 val _ = |