135 THEN |
135 THEN |
136 EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1) |
136 EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1) |
137 end) |
137 end) |
138 (* @end *) |
138 (* @end *) |
139 |
139 |
|
140 fun introductions_tac defs rules preds i ctxt = |
|
141 EVERY1 [ObjectLogic.rulify_tac, |
|
142 K (rewrite_goals_tac defs), |
|
143 REPEAT o (resolve_tac [@{thm allI},@{thm impI}]), |
|
144 subproof1 rules preds i ctxt] |
|
145 |
|
146 |
140 (* @chunk intro_rules *) |
147 (* @chunk intro_rules *) |
141 fun INTROS rules parnames preds defs lthy1 = |
148 fun introductions rules parnames preds defs lthy1 = |
142 let |
149 let |
143 val (_, lthy2) = Variable.add_fixes parnames lthy1 |
150 val (_, lthy2) = Variable.add_fixes parnames lthy1 |
144 |
151 |
145 fun prove_intro (i, goal) = |
152 fun prove_intro (i, goal) = |
146 Goal.prove lthy2 [] [] goal |
153 Goal.prove lthy2 [] [] goal |
147 (fn {context = ctxt, ...} => |
154 (fn {context, ...} => introductions_tac defs rules preds i context) |
148 EVERY1 |
155 |> singleton (ProofContext.export lthy2 lthy1) |
149 [ObjectLogic.rulify_tac, |
|
150 K (rewrite_goals_tac defs), |
|
151 REPEAT o (resolve_tac [@{thm allI},@{thm impI}]), |
|
152 subproof1 rules preds i ctxt]) |
|
153 |> singleton (ProofContext.export lthy2 lthy1) |
|
154 in |
156 in |
155 map_index prove_intro rules |
157 map_index prove_intro rules |
156 end |
158 end |
157 |
|
158 (* @end *) |
159 (* @end *) |
159 |
160 |
160 (* @chunk add_inductive_i *) |
161 (* @chunk add_inductive_i *) |
161 fun add_inductive_i preds params specs lthy = |
162 fun add_inductive_i preds params specs lthy = |
162 let |
163 let |
163 val params' = map (fn (p, T) => Free (Binding.name_of p, T)) params; |
164 val params' = map (fn (p, T) => Free (Binding.name_of p, T)) params; |
164 val preds' = map (fn ((R, T), _) => list_comb (Free (Binding.name_of R, T), params')) preds; |
165 val preds' = map (fn ((R, T), _) => list_comb (Free (Binding.name_of R, T), params')) preds; |
165 val Tss = map (binder_types o fastype_of) preds'; |
166 val Tss = map (binder_types o fastype_of) preds'; |
166 val (ass,rules) = split_list specs; |
167 val (ass, rules) = split_list specs; (* FIXME: ass not used? *) |
167 |
168 |
168 val prednames = map (fst o fst) preds |
169 val prednames = map (fst o fst) preds |
169 val syns = map snd preds |
170 val syns = map snd preds |
170 val parnames = map (Binding.name_of o fst) params |
171 val parnames = map (Binding.name_of o fst) params |
171 |
172 |
172 val (defs, lthy1) = definitions rules params' preds' prednames syns Tss lthy; |
173 val (defs, lthy1) = definitions rules params' preds' prednames syns Tss lthy; |
173 |
174 |
174 val inducts = inductions rules defs parnames preds' Tss lthy1 |
175 val inducts = inductions rules defs parnames preds' Tss lthy1 |
175 |
176 |
176 val intros = INTROS rules parnames preds' defs lthy1 |
177 val intros = introductions rules parnames preds' defs lthy1 |
177 |
178 |
178 val mut_name = space_implode "_" (map (Binding.name_of o fst o fst) preds); |
179 val mut_name = space_implode "_" (map (Binding.name_of o fst o fst) preds); |
179 val case_names = map (Binding.name_of o fst o fst) specs |
180 val case_names = map (Binding.name_of o fst o fst) specs |
180 in |
181 in |
181 lthy1 |
182 lthy1 |