122 (* @end *) |
122 (* @end *) |
123 |
123 |
124 (* @chunk add_inductive_i *) |
124 (* @chunk add_inductive_i *) |
125 fun add_inductive_i preds params specs lthy = |
125 fun add_inductive_i preds params specs lthy = |
126 let |
126 let |
127 val params' = map (fn (p, T) => Free (Binding.base_name p, T)) params; |
127 val params' = map (fn (p, T) => Free (Binding.name_of p, T)) params; |
128 val preds' = map (fn ((R, T), _) => list_comb (Free (Binding.base_name R, T), params')) preds; |
128 val preds' = map (fn ((R, T), _) => list_comb (Free (Binding.name_of R, T), params')) preds; |
129 val Tss = map (binder_types o fastype_of) preds'; |
129 val Tss = map (binder_types o fastype_of) preds'; |
130 val (ass,rules) = split_list specs; |
130 val (ass,rules) = split_list specs; |
131 |
131 |
132 val (defs, lthy1) = definitions params' rules preds preds' Tss lthy |
132 val (defs, lthy1) = definitions params' rules preds preds' Tss lthy |
133 val (_, lthy2) = Variable.add_fixes (map (Binding.base_name o fst) params) lthy1; |
133 val (_, lthy2) = Variable.add_fixes (map (Binding.name_of o fst) params) lthy1; |
134 |
134 |
135 val inducts = INDUCTION rules preds' Tss defs lthy1 lthy2 |
135 val inducts = INDUCTION rules preds' Tss defs lthy1 lthy2 |
136 |
136 |
137 val intros = INTROS rules preds' defs lthy1 lthy2 |
137 val intros = INTROS rules preds' defs lthy1 lthy2 |
138 |
138 |
139 val mut_name = space_implode "_" (map (Binding.base_name o fst o fst) preds); |
139 val mut_name = space_implode "_" (map (Binding.name_of o fst o fst) preds); |
140 val case_names = map (Binding.base_name o fst o fst) specs |
140 val case_names = map (Binding.name_of o fst o fst) specs |
141 in |
141 in |
142 lthy1 |
142 lthy1 |
143 |> LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) => |
143 |> LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) => |
144 ((Binding.qualify mut_name a, atts), [([th], [])])) (specs ~~ intros)) |
144 ((Binding.qualify false mut_name a, atts), [([th], [])])) (specs ~~ intros)) |
145 |-> (fn intross => LocalTheory.note Thm.theoremK |
145 |-> (fn intross => LocalTheory.note Thm.theoremK |
146 ((Binding.qualify mut_name (Binding.name "intros"), []), maps snd intross)) |
146 ((Binding.qualify false mut_name (Binding.name "intros"), []), maps snd intross)) |
147 |>> snd |
147 |>> snd |
148 ||>> (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) => |
148 ||>> (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) => |
149 ((Binding.qualify (Binding.base_name R) (Binding.name "induct"), |
149 ((Binding.qualify false (Binding.name_of R) (Binding.name "induct"), |
150 [Attrib.internal (K (RuleCases.case_names case_names)), |
150 [Attrib.internal (K (RuleCases.case_names case_names)), |
151 Attrib.internal (K (RuleCases.consumes 1)), |
151 Attrib.internal (K (RuleCases.consumes 1)), |
152 Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])])) |
152 Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])])) |
153 (preds ~~ inducts)) #>> maps snd) |
153 (preds ~~ inducts)) #>> maps snd) |
154 |> snd |
154 |> snd |