159 (* axiomatization -- within global theory *) |
159 (* axiomatization -- within global theory *) |
160 |
160 |
161 fun gen_axioms do_print prep raw_vars raw_specs thy = |
161 fun gen_axioms do_print prep raw_vars raw_specs thy = |
162 let |
162 let |
163 val ((vars, specs), _) = prep raw_vars raw_specs (ProofContext.init thy); |
163 val ((vars, specs), _) = prep raw_vars raw_specs (ProofContext.init thy); |
164 val xs = map (fn ((b, T), _) => (Binding.name_of b, T)) vars; |
164 val xs = map (fn ((b, T), _) => (Name.of_binding b, T)) vars; |
165 |
165 |
166 (*consts*) |
166 (*consts*) |
167 val (consts, consts_thy) = thy |> fold_map (Theory.specify_const []) vars; |
167 val (consts, consts_thy) = thy |> fold_map (Theory.specify_const []) vars; |
168 val subst = Term.subst_atomic (map Free xs ~~ consts); |
168 val subst = Term.subst_atomic (map Free xs ~~ consts); |
169 |
169 |
170 (*axioms*) |
170 (*axioms*) |
171 val (axioms, axioms_thy) = (specs, consts_thy) |-> fold_map (fn ((b, atts), props) => |
171 val (axioms, axioms_thy) = (specs, consts_thy) |-> fold_map (fn ((b, atts), props) => |
172 fold_map Thm.add_axiom |
172 fold_map Thm.add_axiom |
173 (map (apfst (fn a => Binding.map_name (K a) b)) |
173 (map (apfst (fn a => Binding.map_name (K a) b)) |
174 (PureThy.name_multi (Binding.name_of b) (map subst props))) |
174 (PureThy.name_multi (Name.of_binding b) (map subst props))) |
175 #>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])]))); |
175 #>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])]))); |
176 |
176 |
177 (*facts*) |
177 (*facts*) |
178 val (facts, thy') = axioms_thy |> PureThy.note_thmss Thm.axiomK |
178 val (facts, thy') = axioms_thy |> PureThy.note_thmss Thm.axiomK |
179 (Attrib.map_facts (Attrib.attribute_i axioms_thy) axioms); |
179 (Attrib.map_facts (Attrib.attribute_i axioms_thy) axioms); |
196 val var as (b, _) = |
196 val var as (b, _) = |
197 (case vars of |
197 (case vars of |
198 [] => (Binding.name x, NoSyn) |
198 [] => (Binding.name x, NoSyn) |
199 | [((b, _), mx)] => |
199 | [((b, _), mx)] => |
200 let |
200 let |
201 val y = Binding.name_of b; |
201 val y = Name.of_binding b; |
202 val _ = x = y orelse |
202 val _ = x = y orelse |
203 error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^ |
203 error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^ |
204 Position.str_of (Binding.pos_of b)); |
204 Position.str_of (Binding.pos_of b)); |
205 in (b, mx) end); |
205 in (b, mx) end); |
206 val name = Thm.def_binding_optional b raw_name; |
206 val name = Thm.def_binding_optional b raw_name; |
290 val goal_ctxt = fold (fold (Variable.auto_fixes o fst)) propp elems_ctxt; |
290 val goal_ctxt = fold (fold (Variable.auto_fixes o fst)) propp elems_ctxt; |
291 in ((prems, stmt, []), goal_ctxt) end |
291 in ((prems, stmt, []), goal_ctxt) end |
292 | Element.Obtains obtains => |
292 | Element.Obtains obtains => |
293 let |
293 let |
294 val case_names = obtains |> map_index (fn (i, (b, _)) => |
294 val case_names = obtains |> map_index (fn (i, (b, _)) => |
295 if Binding.is_empty b then string_of_int (i + 1) else Binding.name_of b); |
295 if Binding.is_empty b then string_of_int (i + 1) else Name.of_binding b); |
296 val constraints = obtains |> map (fn (_, (vars, _)) => |
296 val constraints = obtains |> map (fn (_, (vars, _)) => |
297 Element.Constrains |
297 Element.Constrains |
298 (vars |> map_filter (fn (x, SOME T) => SOME (Binding.name_of x, T) | _ => NONE))); |
298 (vars |> map_filter (fn (x, SOME T) => SOME (Name.of_binding x, T) | _ => NONE))); |
299 |
299 |
300 val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props); |
300 val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props); |
301 val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt; |
301 val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt; |
302 |
302 |
303 val thesis = ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) AutoBind.thesisN; |
303 val thesis = ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) AutoBind.thesisN; |
304 |
304 |
305 fun assume_case ((name, (vars, _)), asms) ctxt' = |
305 fun assume_case ((name, (vars, _)), asms) ctxt' = |
306 let |
306 let |
307 val bs = map fst vars; |
307 val bs = map fst vars; |
308 val xs = map Binding.name_of bs; |
308 val xs = map Name.of_binding bs; |
309 val props = map fst asms; |
309 val props = map fst asms; |
310 val (Ts, _) = ctxt' |
310 val (Ts, _) = ctxt' |
311 |> fold Variable.declare_term props |
311 |> fold Variable.declare_term props |
312 |> fold_map ProofContext.inferred_param xs; |
312 |> fold_map ProofContext.inferred_param xs; |
313 val asm = Term.list_all_free (xs ~~ Ts, Logic.list_implies (props, thesis)); |
313 val asm = Term.list_all_free (xs ~~ Ts, Logic.list_implies (props, thesis)); |