47 fun note_theorem ((binding, atts), ths) = |
47 fun note_theorem ((binding, atts), ths) = |
48 LocalTheory.note Thm.generatedK ((binding, atts), ths) |
48 LocalTheory.note Thm.generatedK ((binding, atts), ths) |
49 |
49 |
50 fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" |
50 fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" |
51 |
51 |
52 fun add_simps fnames post sort extra_qualify label moreatts simps lthy = |
52 fun add_simps fnames post sort extra_qualify label mod_binding moreatts simps lthy = |
53 let |
53 let |
54 val spec = post simps |
54 val spec = post simps |
55 |> map (apfst (apsnd (fn ats => moreatts @ ats))) |
55 |> map (apfst (apsnd (fn ats => moreatts @ ats))) |
56 |> map (apfst (apfst extra_qualify)) |
56 |> map (apfst (apfst extra_qualify)) |
57 |
57 |
60 |
60 |
61 val saved_simps = maps snd saved_spec_simps |
61 val saved_simps = maps snd saved_spec_simps |
62 val simps_by_f = sort saved_simps |
62 val simps_by_f = sort saved_simps |
63 |
63 |
64 fun add_for_f fname simps = |
64 fun add_for_f fname simps = |
65 note_theorem ((Binding.qualified_name (Long_Name.qualify fname label), []), simps) |
65 note_theorem ((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps) |
66 #> snd |
66 #> snd |
67 in |
67 in |
68 (saved_simps, |
68 (saved_simps, |
69 fold2 add_for_f fnames simps_by_f lthy) |
69 fold2 add_for_f fnames simps_by_f lthy) |
70 end |
70 end |
90 cont (Thm.close_derivation proof) |
90 cont (Thm.close_derivation proof) |
91 |
91 |
92 val fnames = map (fst o fst) fixes |
92 val fnames = map (fst o fst) fixes |
93 fun qualify n = Binding.name n |
93 fun qualify n = Binding.name n |
94 |> Binding.qualify true defname |
94 |> Binding.qualify true defname |
|
95 val conceal_partial = if partials then I else Binding.conceal |
95 |
96 |
96 val addsmps = add_simps fnames post sort_cont |
97 val addsmps = add_simps fnames post sort_cont |
97 |
98 |
98 val (((psimps', pinducts'), (_, [termination'])), lthy) = |
99 val (((psimps', pinducts'), (_, [termination'])), lthy) = |
99 lthy |
100 lthy |
100 |> addsmps (Binding.qualify false "partial") "psimps" |
101 |> addsmps (conceal_partial o Binding.qualify false "partial") |
101 psimp_attribs psimps |
102 "psimps" conceal_partial psimp_attribs psimps |
102 ||> fold_option (snd oo addsmps I "simps" simp_attribs) trsimps |
103 ||> fold_option (snd oo addsmps I "simps" I simp_attribs) trsimps |
103 ||>> note_theorem ((qualify "pinduct", |
104 ||>> note_theorem ((conceal_partial (qualify "pinduct"), |
104 [Attrib.internal (K (Rule_Cases.case_names cnames)), |
105 [Attrib.internal (K (Rule_Cases.case_names cnames)), |
105 Attrib.internal (K (Rule_Cases.consumes 1)), |
106 Attrib.internal (K (Rule_Cases.consumes 1)), |
106 Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts) |
107 Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts) |
107 ||>> note_theorem ((Binding.conceal (qualify "termination"), []), [termination]) |
108 ||>> note_theorem ((Binding.conceal (qualify "termination"), []), [termination]) |
108 ||> (snd o note_theorem ((qualify "cases", |
109 ||> (snd o note_theorem ((qualify "cases", |
152 val tinduct = map remove_domain_condition pinducts |
153 val tinduct = map remove_domain_condition pinducts |
153 fun qualify n = Binding.name n |
154 fun qualify n = Binding.name n |
154 |> Binding.qualify true defname |
155 |> Binding.qualify true defname |
155 in |
156 in |
156 lthy |
157 lthy |
157 |> add_simps I "simps" simp_attribs tsimps |> snd |
158 |> add_simps I "simps" I simp_attribs tsimps |> snd |
158 |> note_theorem |
159 |> note_theorem |
159 ((qualify "induct", |
160 ((qualify "induct", |
160 [Attrib.internal (K (Rule_Cases.case_names case_names))]), |
161 [Attrib.internal (K (Rule_Cases.case_names case_names))]), |
161 tinduct) |> snd |
162 tinduct) |> snd |
162 end |
163 end |