375 lits_of_nodes thy (add_constraint (constraint_of_node true u, vt), lits) us |
375 lits_of_nodes thy (add_constraint (constraint_of_node true u, vt), lits) us |
376 handle NODE _ => lits_of_nodes thy (vt, term_of_node [] thy u :: lits) us |
376 handle NODE _ => lits_of_nodes thy (vt, term_of_node [] thy u :: lits) us |
377 |
377 |
378 (*Update TVars/TFrees with detected sort constraints.*) |
378 (*Update TVars/TFrees with detected sort constraints.*) |
379 fun repair_sorts vt = |
379 fun repair_sorts vt = |
380 let fun tysubst (Type (a, Ts)) = Type (a, map tysubst Ts) |
380 let |
381 | tysubst (TVar (xi, s)) = TVar (xi, the_default s (Vartab.lookup vt xi)) |
381 fun do_type (Type (a, Ts)) = Type (a, map do_type Ts) |
382 | tysubst (TFree (x, s)) = TFree (x, the_default s (Vartab.lookup vt (x, ~1))) |
382 | do_type (TVar (xi, s)) = TVar (xi, the_default s (Vartab.lookup vt xi)) |
383 fun tmsubst (Const (a, T)) = Const (a, tysubst T) |
383 | do_type (TFree (x, s)) = |
384 | tmsubst (Free (a, T)) = Free (a, tysubst T) |
384 TFree (x, the_default s (Vartab.lookup vt (x, ~1))) |
385 | tmsubst (Var (xi, T)) = Var (xi, tysubst T) |
385 fun do_term (Const (a, T)) = Const (a, do_type T) |
386 | tmsubst (t as Bound _) = t |
386 | do_term (Free (a, T)) = Free (a, do_type T) |
387 | tmsubst (Abs (a, T, t)) = Abs (a, tysubst T, tmsubst t) |
387 | do_term (Var (xi, T)) = Var (xi, do_type T) |
388 | tmsubst (t1 $ t2) = tmsubst t1 $ tmsubst t2 |
388 | do_term (t as Bound _) = t |
389 in not (Vartab.is_empty vt) ? tmsubst end |
389 | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t) |
|
390 | do_term (t1 $ t2) = do_term t1 $ do_term t2 |
|
391 in not (Vartab.is_empty vt) ? do_term end |
390 |
392 |
391 fun unskolemize_term t = |
393 fun unskolemize_term t = |
392 fold forall_of (Term.add_consts t [] |
394 fold forall_of (Term.add_consts t [] |
393 |> filter (is_skolem_const_name o fst) |> map Const) t |
395 |> filter (is_skolem_const_name o fst) |> map Const) t |
394 |
396 |
412 conjecture clauses. *) |
414 conjecture clauses. *) |
413 fun clause_of_nodes ctxt vt us = |
415 fun clause_of_nodes ctxt vt us = |
414 let val (vt, t) = lits_of_nodes (ProofContext.theory_of ctxt) (vt, []) us in |
416 let val (vt, t) = lits_of_nodes (ProofContext.theory_of ctxt) (vt, []) us in |
415 t |> repair_sorts vt |
417 t |> repair_sorts vt |
416 end |
418 end |
417 fun check_clause ctxt = |
419 fun check_formula ctxt = |
418 TypeInfer.constrain HOLogic.boolT |
420 TypeInfer.constrain HOLogic.boolT |
419 #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt) |
421 #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt) |
420 |
422 |
421 (** Global sort constraints on TFrees (from tfree_tcs) are positive unit |
423 (** Global sort constraints on TFrees (from tfree_tcs) are positive unit |
422 clauses. **) |
424 clauses. **) |
448 val frees = map unvarify_term vars |
450 val frees = map unvarify_term vars |
449 val unvarify_args = subst_atomic (vars ~~ frees) |
451 val unvarify_args = subst_atomic (vars ~~ frees) |
450 val t2 = clause_of_nodes ctxt vt us |
452 val t2 = clause_of_nodes ctxt vt us |
451 val (t1, t2) = |
453 val (t1, t2) = |
452 HOLogic.eq_const HOLogic.typeT $ t1 $ t2 |
454 HOLogic.eq_const HOLogic.typeT $ t1 $ t2 |
453 |> unvarify_args |> uncombine_term |> check_clause ctxt |
455 |> unvarify_args |> uncombine_term |> check_formula ctxt |
454 |> HOLogic.dest_eq |
456 |> HOLogic.dest_eq |
455 in |
457 in |
456 (Definition (num, t1, t2), |
458 (Definition (num, t1, t2), |
457 fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt) |
459 fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt) |
458 end |
460 end |
459 | decode_line vt (Inference (num, us, deps)) ctxt = |
461 | decode_line vt (Inference (num, us, deps)) ctxt = |
460 let |
462 let |
461 val t = us |> clause_of_nodes ctxt vt |
463 val t = us |> clause_of_nodes ctxt vt |
462 |> unskolemize_term |> uncombine_term |> check_clause ctxt |
464 |> unskolemize_term |> uncombine_term |> check_formula ctxt |
463 in |
465 in |
464 (Inference (num, t, deps), |
466 (Inference (num, t, deps), |
465 fold Variable.declare_term (OldTerm.term_frees t) ctxt) |
467 fold Variable.declare_term (OldTerm.term_frees t) ctxt) |
466 end |
468 end |
467 fun decode_lines ctxt lines = |
469 fun decode_lines ctxt lines = |
653 should be associated with forthcoming proof steps. The second component is a |
655 should be associated with forthcoming proof steps. The second component is a |
654 pair ("keep_ls", "drop_ls"), where "keep_ls" are the labels to keep and |
656 pair ("keep_ls", "drop_ls"), where "keep_ls" are the labels to keep and |
655 "drop_ls" are those that should be dropped in a case split. *) |
657 "drop_ls" are those that should be dropped in a case split. *) |
656 type backpatches = (label * facts) list * (label list * label list) |
658 type backpatches = (label * facts) list * (label list * label list) |
657 |
659 |
658 fun using_of_step (Have (_, _, _, by)) = |
660 fun used_labels_of_step (Have (_, _, _, by)) = |
659 (case by of |
661 (case by of |
660 Facts (ls, _) => ls |
662 Facts (ls, _) => ls |
661 | CaseSplit (proofs, (ls, _)) => fold (union (op =) o using_of) proofs ls) |
663 | CaseSplit (proofs, (ls, _)) => |
662 | using_of_step _ = [] |
664 fold (union (op =) o used_labels_of) proofs ls) |
663 and using_of proof = fold (union (op =) o using_of_step) proof [] |
665 | used_labels_of_step _ = [] |
|
666 and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof [] |
664 |
667 |
665 fun new_labels_of_step (Fix _) = [] |
668 fun new_labels_of_step (Fix _) = [] |
666 | new_labels_of_step (Let _) = [] |
669 | new_labels_of_step (Let _) = [] |
667 | new_labels_of_step (Assume (l, _)) = [l] |
670 | new_labels_of_step (Assume (l, _)) = [l] |
668 | new_labels_of_step (Have (_, l, _, _)) = [l] |
671 | new_labels_of_step (Have (_, l, _, _)) = [l] |
679 else case hd proof1 of |
682 else case hd proof1 of |
680 Have ([], l, t, by) => |
683 Have ([], l, t, by) => |
681 if forall (fn Have ([], l', t', _) :: _ => (l, t) = (l', t') |
684 if forall (fn Have ([], l', t', _) :: _ => (l, t) = (l', t') |
682 | _ => false) (tl proofs) andalso |
685 | _ => false) (tl proofs) andalso |
683 not (exists (member (op =) (maps new_labels_of proofs)) |
686 not (exists (member (op =) (maps new_labels_of proofs)) |
684 (using_of proof_tail)) then |
687 (used_labels_of proof_tail)) then |
685 SOME (l, t, map rev proofs, proof_tail) |
688 SOME (l, t, map rev proofs, proof_tail) |
686 else |
689 else |
687 NONE |
690 NONE |
688 | _ => NONE |
691 | _ => NONE |
689 in aux [] o map rev end |
692 in aux [] o map rev end |
821 | aux _ (step :: proof) = step :: aux no_label proof |
824 | aux _ (step :: proof) = step :: aux no_label proof |
822 in aux no_label end |
825 in aux no_label end |
823 |
826 |
824 fun kill_useless_labels_in_proof proof = |
827 fun kill_useless_labels_in_proof proof = |
825 let |
828 let |
826 val used_ls = using_of proof |
829 val used_ls = used_labels_of proof |
827 fun do_label l = if member (op =) used_ls l then l else no_label |
830 fun do_label l = if member (op =) used_ls l then l else no_label |
828 fun kill (Assume (l, t)) = Assume (do_label l, t) |
831 fun do_step (Assume (l, t)) = Assume (do_label l, t) |
829 | kill (Have (qs, l, t, by)) = |
832 | do_step (Have (qs, l, t, by)) = |
830 Have (qs, do_label l, t, |
833 Have (qs, do_label l, t, |
831 case by of |
834 case by of |
832 CaseSplit (proofs, facts) => |
835 CaseSplit (proofs, facts) => |
833 CaseSplit (map (map kill) proofs, facts) |
836 CaseSplit (map (map do_step) proofs, facts) |
834 | _ => by) |
837 | _ => by) |
835 | kill step = step |
838 | do_step step = step |
836 in map kill proof end |
839 in map do_step proof end |
837 |
840 |
838 fun prefix_for_depth n = replicate_string (n + 1) |
841 fun prefix_for_depth n = replicate_string (n + 1) |
839 |
842 |
840 val relabel_proof = |
843 val relabel_proof = |
841 let |
844 let |
889 (if member (op =) qs Then then |
892 (if member (op =) qs Then then |
890 if member (op =) qs Show then "thus" else "hence" |
893 if member (op =) qs Show then "thus" else "hence" |
891 else |
894 else |
892 if member (op =) qs Show then "show" else "have") |
895 if member (op =) qs Show then "show" else "have") |
893 val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt) |
896 val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt) |
894 fun do_using [] = "" |
897 fun do_facts ([], []) = "by metis" |
895 | do_using ls = "using " ^ (space_implode " " (map do_raw_label ls)) ^ " " |
898 | do_facts (ls, ss) = |
896 fun do_by_facts [] = "by metis" |
899 "by (metis " ^ space_implode " " (map do_raw_label ls @ ss) ^ ")" |
897 | do_by_facts ss = "by (metis " ^ space_implode " " ss ^ ")" |
|
898 fun do_facts (ls, ss) = do_using ls ^ do_by_facts ss |
|
899 and do_step ind (Fix xs) = |
900 and do_step ind (Fix xs) = |
900 do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n" |
901 do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n" |
901 | do_step ind (Let (t1, t2)) = |
902 | do_step ind (Let (t1, t2)) = |
902 do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n" |
903 do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n" |
903 | do_step ind (Assume (l, t)) = |
904 | do_step ind (Assume (l, t)) = |