equal
deleted
inserted
replaced
336 else [])) @ |
336 else [])) @ |
337 (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers) |
337 (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers) |
338 |> map (snd o make_axiom ctxt) |
338 |> map (snd o make_axiom ctxt) |
339 end |
339 end |
340 |
340 |
341 fun s_not (@{const Not} $ t) = t |
341 fun meta_not t = @{const "==>"} $ t $ @{prop False} |
342 | s_not t = @{const Not} $ t |
|
343 |
342 |
344 fun prepare_formulas ctxt full_types hyp_ts concl_t axcls = |
343 fun prepare_formulas ctxt full_types hyp_ts concl_t axcls = |
345 let |
344 let |
346 val thy = ProofContext.theory_of ctxt |
345 val thy = ProofContext.theory_of ctxt |
347 val goal_t = Logic.list_implies (hyp_ts, concl_t) |
346 val goal_t = Logic.list_implies (hyp_ts, concl_t) |
349 val axtms = map (prop_of o snd) axcls |
348 val axtms = map (prop_of o snd) axcls |
350 val subs = tfree_classes_of_terms [goal_t] |
349 val subs = tfree_classes_of_terms [goal_t] |
351 val supers = tvar_classes_of_terms axtms |
350 val supers = tvar_classes_of_terms axtms |
352 val tycons = type_consts_of_terms thy (goal_t :: axtms) |
351 val tycons = type_consts_of_terms thy (goal_t :: axtms) |
353 (* TFrees in the conjecture; TVars in the axioms *) |
352 (* TFrees in the conjecture; TVars in the axioms *) |
354 val conjectures = |
353 val conjectures = map meta_not hyp_ts @ [concl_t] |> make_conjectures ctxt |
355 map (s_not o HOLogic.dest_Trueprop) hyp_ts @ |
|
356 [HOLogic.dest_Trueprop concl_t] |
|
357 |> make_conjectures ctxt |
|
358 val (clnames, axioms) = ListPair.unzip (map (make_axiom ctxt) axcls) |
354 val (clnames, axioms) = ListPair.unzip (map (make_axiom ctxt) axcls) |
359 val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms |
355 val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms |
360 val (supers', arity_clauses) = make_arity_clauses thy tycons supers |
356 val (supers', arity_clauses) = make_arity_clauses thy tycons supers |
361 val class_rel_clauses = make_class_rel_clauses thy subs supers' |
357 val class_rel_clauses = make_class_rel_clauses thy subs supers' |
362 in |
358 in |