105 val pelims = Function_Elims.mk_partial_elim_rules lthy result |
105 val pelims = Function_Elims.mk_partial_elim_rules lthy result |
106 |
106 |
107 val fnames = map (fst o fst) fixes |
107 val fnames = map (fst o fst) fixes |
108 fun qualify n = Binding.name n |
108 fun qualify n = Binding.name n |
109 |> Binding.qualify true defname |
109 |> Binding.qualify true defname |
110 val conceal_partial = if partials then I else Binding.conceal |
110 val concealed_partial = if partials then I else Binding.concealed |
111 |
111 |
112 val addsmps = add_simps fnames post sort_cont |
112 val addsmps = add_simps fnames post sort_cont |
113 |
113 |
114 val (((((psimps', [pinducts']), [termination']), cases'), pelims'), lthy) = |
114 val (((((psimps', [pinducts']), [termination']), cases'), pelims'), lthy) = |
115 lthy |
115 lthy |
116 |> addsmps (conceal_partial o Binding.qualify false "partial") |
116 |> addsmps (concealed_partial o Binding.qualify false "partial") |
117 "psimps" conceal_partial psimp_attribs psimps |
117 "psimps" concealed_partial psimp_attribs psimps |
118 ||>> Local_Theory.notes [((conceal_partial (qualify "pinduct"), []), |
118 ||>> Local_Theory.notes [((concealed_partial (qualify "pinduct"), []), |
119 simple_pinducts |> map (fn th => ([th], |
119 simple_pinducts |> map (fn th => ([th], |
120 [Attrib.internal (K (Rule_Cases.case_names cnames)), |
120 [Attrib.internal (K (Rule_Cases.case_names cnames)), |
121 Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th))), |
121 Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th))), |
122 Attrib.internal (K (Induct.induct_pred ""))])))] |
122 Attrib.internal (K (Induct.induct_pred ""))])))] |
123 ||>> (apfst snd o Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination])) |
123 ||>> (apfst snd o Local_Theory.note ((Binding.concealed (qualify "termination"), []), [termination])) |
124 ||>> fold_map (note_qualified "cases" [Rule_Cases.case_names cnames]) (fnames ~~ map single cases) (* TODO: case names *) |
124 ||>> fold_map (note_qualified "cases" [Rule_Cases.case_names cnames]) (fnames ~~ map single cases) (* TODO: case names *) |
125 ||>> fold_map (note_qualified "pelims" [Rule_Cases.consumes 1, Rule_Cases.constraints 1]) (fnames ~~ pelims) |
125 ||>> fold_map (note_qualified "pelims" [Rule_Cases.consumes 1, Rule_Cases.constraints 1]) (fnames ~~ pelims) |
126 ||> (case domintros of NONE => I | SOME thms => |
126 ||> (case domintros of NONE => I | SOME thms => |
127 Local_Theory.note ((qualify "domintros", []), thms) #> snd) |
127 Local_Theory.note ((qualify "domintros", []), thms) #> snd) |
128 |
128 |