1(* Title: HOL/Tools/SMT/z3_isar.ML 2 Author: Jasmin Blanchette, TU Muenchen 3 4Z3 proofs as generic ATP proofs for Isar proof reconstruction. 5*) 6 7signature Z3_ISAR = 8sig 9 val atp_proof_of_z3_proof: Proof.context -> term list -> thm list -> term list -> term -> 10 (string * term) list -> int list -> int -> (int * string) list -> Z3_Proof.z3_step list -> 11 (term, string) ATP_Proof.atp_step list 12end; 13 14structure Z3_Isar: Z3_ISAR = 15struct 16 17open ATP_Util 18open ATP_Problem 19open ATP_Proof 20open ATP_Proof_Reconstruct 21open SMTLIB_Isar 22 23val z3_apply_def_rule = Z3_Proof.string_of_rule Z3_Proof.Apply_Def 24val z3_hypothesis_rule = Z3_Proof.string_of_rule Z3_Proof.Hypothesis 25val z3_intro_def_rule = Z3_Proof.string_of_rule Z3_Proof.Intro_Def 26val z3_lemma_rule = Z3_Proof.string_of_rule Z3_Proof.Lemma 27 28fun inline_z3_defs _ [] = [] 29 | inline_z3_defs defs ((name, role, t, rule, deps) :: lines) = 30 if rule = z3_intro_def_rule then 31 let val def = t |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> swap in 32 inline_z3_defs (insert (op =) def defs) 33 (map (replace_dependencies_in_line (name, [])) lines) 34 end 35 else if rule = z3_apply_def_rule then 36 inline_z3_defs defs (map (replace_dependencies_in_line (name, [])) lines) 37 else 38 (name, role, Term.subst_atomic defs t, rule, deps) :: inline_z3_defs defs lines 39 40fun add_z3_hypotheses [] = I 41 | add_z3_hypotheses hyps = 42 HOLogic.dest_Trueprop 43 #> curry s_imp (Library.foldr1 s_conj (map HOLogic.dest_Trueprop hyps)) 44 #> HOLogic.mk_Trueprop 45 46fun inline_z3_hypotheses _ _ [] = [] 47 | inline_z3_hypotheses hyp_names hyps ((name, role, t, rule, deps) :: lines) = 48 if rule = z3_hypothesis_rule then 49 inline_z3_hypotheses (name :: hyp_names) (AList.map_default (op =) (t, []) (cons name) hyps) 50 lines 51 else 52 let val deps' = subtract (op =) hyp_names deps in 53 if rule = z3_lemma_rule then 54 (name, role, t, rule, deps') :: inline_z3_hypotheses hyp_names hyps lines 55 else 56 let 57 val add_hyps = filter_out (null o inter (op =) deps o snd) hyps 58 val t' = add_z3_hypotheses (map fst add_hyps) t 59 val hyps' = fold (AList.update (op =) o apsnd (insert (op =) name)) add_hyps hyps 60 in 61 (name, role, t', rule, deps') :: inline_z3_hypotheses hyp_names hyps' lines 62 end 63 end 64 65fun dest_alls (Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (abs as (_, T, _))) = 66 let val (s', t') = Term.dest_abs abs in 67 dest_alls t' |>> cons (s', T) 68 end 69 | dest_alls t = ([], t) 70 71val reorder_foralls = 72 dest_alls 73 #>> sort_by fst 74 #-> fold_rev (Logic.all o Free); 75 76fun atp_proof_of_z3_proof ctxt ll_defs rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids 77 conjecture_id fact_helper_ids proof = 78 let 79 fun steps_of (Z3_Proof.Z3_Step {id, rule, prems, concl, ...}) = 80 let 81 val sid = string_of_int id 82 83 val concl' = concl 84 |> reorder_foralls (* crucial for skolemization steps *) 85 |> postprocess_step_conclusion ctxt rewrite_rules ll_defs 86 fun standard_step role = 87 ((sid, []), role, concl', Z3_Proof.string_of_rule rule, 88 map (fn id => (string_of_int id, [])) prems) 89 in 90 (case rule of 91 Z3_Proof.Asserted => 92 let val ss = the_list (AList.lookup (op =) fact_helper_ids id) in 93 (case distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids fact_helper_ts 94 hyp_ts concl_t of 95 NONE => [] 96 | SOME (role0, concl00) => 97 let 98 val name0 = (sid ^ "a", ss) 99 val concl0 = unskolemize_names ctxt concl00 100 in 101 (if role0 = Axiom then [] 102 else [(name0, role0, concl0, Z3_Proof.string_of_rule rule, [])]) @ 103 [((sid, []), Plain, concl', Z3_Proof.string_of_rule Z3_Proof.Rewrite, 104 name0 :: normalizing_prems ctxt concl0)] 105 end) 106 end 107 | Z3_Proof.Rewrite => [standard_step Lemma] 108 | Z3_Proof.Rewrite_Star => [standard_step Lemma] 109 | Z3_Proof.Skolemize => [standard_step Lemma] 110 | Z3_Proof.Th_Lemma _ => [standard_step Lemma] 111 | _ => [standard_step Plain]) 112 end 113 in 114 proof 115 |> maps steps_of 116 |> inline_z3_defs [] 117 |> inline_z3_hypotheses [] [] 118 end 119 120end; 121