src/HOL/SMT/Tools/z3_proof_rules.ML

 fun net_instance net ct = first_of (Net.match_term net (Thm.term_of ct)) ct
 end
 
 fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
 fun certify_var ctxt idx T = certify ctxt (Var (("x", idx), T))
+fun certify_free ctxt idx T = certify ctxt (Free ("x" ^ string_of_int idx, T))
 
 fun varify ctxt =
   let
     fun varify1 cv thm =
       let

 in
 fun unfold_distinct_conv ct =
   (More_Conv.rewrs_conv [dist1, dist2] else_conv
   (Conv.rewr_conv dist3 then_conv binop_conv set_conv unfold_distinct_conv)) ct
 end
+
+(** proving abstractions **)
+
+fun fold_map_op f ct =
+  let val (cf, cu) = Thm.dest_comb ct
+  in f cu #>> Thm.capply cf end
+
+fun fold_map_binop f1 f2 ct =
+  let val ((cf, cu1), cu2) = apfst Thm.dest_comb (Thm.dest_comb ct)
+  in f1 cu1 ##>> f2 cu2 #>> uncurry (Thm.mk_binop cf) end
+
+fun abstraction_context ctxt = (ctxt, certify_var, 1, false, Ctermtab.empty)
+fun abstraction_context' ctxt = (ctxt, certify_free, 1, true, Ctermtab.empty)
+
+fun fresh_abstraction ct (cx as (ctxt, mk_var, idx, gen, tab)) =
+  (case Ctermtab.lookup tab ct of
+    SOME cv => (cv, cx)
+  | NONE =>
+      let val cv = mk_var ctxt idx (#T (Thm.rep_cterm ct))
+      in (cv, (ctxt, mk_var, idx + 1, gen, Ctermtab.update (ct, cv) tab)) end)
+
+fun prove_abstraction tac ct (ctxt, _, _, gen, tab) =
+  let
+    val insts = map swap (Ctermtab.dest tab)
+    val thm = Goal.prove_internal [] ct (fn _ => tac 1)
+  in
+    if gen
+    then fold SMT_Normalize.instantiate_free insts thm
+    else Thm.instantiate ([], insts) thm
+  end
 
 
 (* core proof rules *)
 
 datatype assms = Some of thm list | Many of thm Net.net

     as_meta_eq ct
     |> by_tac' (nnf_quant_tac (varify ctxt vars (meta_eq_of p)) qs)
 
   val nnf_rules = thm_net_of [@{thm not_not}]
 
+  fun abstract ct =
+    (case Thm.term_of ct of
+      @{term False} => pair
+    | @{term Not} $ _ => fold_map_op abstract
+    | @{term "op &"} $ _ $ _ => fold_map_binop abstract abstract
+    | @{term "op |"} $ _ $ _ => fold_map_binop abstract abstract
+    | @{term "op -->"} $ _ $ _ => fold_map_binop abstract abstract
+    | @{term "op = :: bool => _"} $ _ $ _ => fold_map_binop abstract abstract
+    | _ => fresh_abstraction) ct
+
+  fun abstracted ctxt ct =
+    abstraction_context' ctxt
+    |> abstract (Thm.dest_arg ct)
+    |>> T.mk_prop
+    |-> prove_abstraction (Classical.best_tac HOL_cs)
+
   fun prove_nnf ctxt =
     try_apply ctxt "nnf" [
       ("conj/disj", prove_conj_disj_eq o Thm.dest_arg),
       ("rule", the o net_instance nnf_rules),
+      ("abstract", abstracted ctxt),
       ("tactic", by_tac' (Classical.best_tac HOL_cs))]
 in
 fun nnf ctxt ps ct =
   (case Thm.term_of ct of
     _ $ (l as Const _ $ Abs _) $ (r as Const _ $ Abs _) =>

   in
   val all_distrib_conv = More_Conv.top_sweep_conv (K distrib_conv)
   end
 
   local
-    fun make_ctxt ctxt = (ctxt, Ctermtab.empty, 1)
-    fun fresh ct (cx as (ctxt, tab, idx)) =
-      (case Ctermtab.lookup tab ct of
-        SOME cv => (cv, cx)
-      | NONE =>
-          let val cv = certify_var ctxt idx (#T (Thm.rep_cterm ct))
-          in (cv, (ctxt, Ctermtab.update (ct, cv) tab, idx + 1)) end)
-
-    fun fold_map_op f ct =
-      let val (cf, cu) = Thm.dest_comb ct
-      in f cu #>> Thm.capply cf end
-
-    fun fold_map_binop f1 f2 ct =
-      let val ((cf, cu1), cu2) = apfst Thm.dest_comb (Thm.dest_comb ct)
-      in f1 cu1 ##>> f2 cu2 #>> uncurry (Thm.mk_binop cf) end
+    fun fresh ct = fresh_abstraction ct
 
     fun mult f1 f2 ct t u =
       if is_number t 
       then if is_number u then pair ct else fold_map_binop f1 f2 ct
       else fresh ct

         @{term "op |"} $ _ $ _ => fold_map_binop disj disj ct
       | @{term False} => pair ct
       | _ => conj ct)
   in
   fun prove_arith ctxt thms ct =
-    let
-      val (goal, (_, tab, _)) =
-        make_ctxt ctxt
-        |> fold_map (fold_map_op ineq o Thm.cprop_of) thms
-        ||>> fold_map_op disj ct
-        |>> uncurry (fold_rev (Thm.mk_binop @{cterm "op ==>"}))
-    in
-      Goal.prove_internal [] goal (fn _ => Arith_Data.arith_tac ctxt 1)
-      |> Thm.instantiate ([], map swap (Ctermtab.dest tab))
-      |> fold (fn th1 => fn th2 => Thm.implies_elim th2 th1) thms
-    end
+    abstraction_context ctxt
+    |> fold_map (fold_map_op ineq o Thm.cprop_of) thms
+    ||>> fold_map_op disj ct
+    |>> uncurry (fold_rev (Thm.mk_binop @{cterm "op ==>"}))
+    |-> prove_abstraction (Arith_Data.arith_tac ctxt)
+    |> fold (fn th1 => fn th2 => Thm.implies_elim th2 th1) thms
   end
 in
 fun arith_lemma ctxt thms ct =
   let val thms' = map (Conv.fconv_rule (all_distrib_conv ctxt)) thms
   in with_conv (all_distrib_conv ctxt) (prove_arith ctxt thms') ct end