src/HOL/Library/Old_SMT/old_z3_proof_tools.ML
author wenzelm
Wed Jun 17 11:03:05 2015 +0200 (2015-06-17)
changeset 60500 903bb1495239
parent 59634 4b94cc030ba0
child 60642 48dd1cefb4ae
permissions -rw-r--r--
isabelle update_cartouches;
     1 (*  Title:      HOL/Library/Old_SMT/old_z3_proof_tools.ML
     2     Author:     Sascha Boehme, TU Muenchen
     3 
     4 Helper functions required for Z3 proof reconstruction.
     5 *)
     6 
     7 signature OLD_Z3_PROOF_TOOLS =
     8 sig
     9   (*modifying terms*)
    10   val as_meta_eq: cterm -> cterm
    11 
    12   (*theorem nets*)
    13   val thm_net_of: ('a -> thm) -> 'a list -> 'a Net.net
    14   val net_instances: (int * thm) Net.net -> cterm -> (int * thm) list
    15   val net_instance: thm Net.net -> cterm -> thm option
    16 
    17   (*proof combinators*)
    18   val under_assumption: (thm -> thm) -> cterm -> thm
    19   val with_conv: conv -> (cterm -> thm) -> cterm -> thm
    20   val discharge: thm -> thm -> thm
    21   val varify: string list -> thm -> thm
    22   val unfold_eqs: Proof.context -> thm list -> conv
    23   val match_instantiate: (cterm -> cterm) -> cterm -> thm -> thm
    24   val by_tac: Proof.context -> (int -> tactic) -> cterm -> thm
    25   val make_hyp_def: thm -> Proof.context -> thm * Proof.context
    26   val by_abstraction: int -> bool * bool -> Proof.context -> thm list ->
    27     (Proof.context -> cterm -> thm) -> cterm -> thm
    28 
    29   (*a faster COMP*)
    30   type compose_data
    31   val precompose: (cterm -> cterm list) -> thm -> compose_data
    32   val precompose2: (cterm -> cterm * cterm) -> thm -> compose_data
    33   val compose: compose_data -> thm -> thm
    34 
    35   (*unfolding of 'distinct'*)
    36   val unfold_distinct_conv: conv
    37 
    38   (*simpset*)
    39   val add_simproc: Simplifier.simproc -> Context.generic -> Context.generic
    40   val make_simpset: Proof.context -> thm list -> simpset
    41 end
    42 
    43 structure Old_Z3_Proof_Tools: OLD_Z3_PROOF_TOOLS =
    44 struct
    45 
    46 
    47 
    48 (* modifying terms *)
    49 
    50 fun as_meta_eq ct =
    51   uncurry Old_SMT_Utils.mk_cequals (Thm.dest_binop (Old_SMT_Utils.dest_cprop ct))
    52 
    53 
    54 
    55 (* theorem nets *)
    56 
    57 fun thm_net_of f xthms =
    58   let fun insert xthm = Net.insert_term (K false) (Thm.prop_of (f xthm), xthm)
    59   in fold insert xthms Net.empty end
    60 
    61 fun maybe_instantiate ct thm =
    62   try Thm.first_order_match (Thm.cprop_of thm, ct)
    63   |> Option.map (fn inst => Thm.instantiate inst thm)
    64 
    65 local
    66   fun instances_from_net match f net ct =
    67     let
    68       val lookup = if match then Net.match_term else Net.unify_term
    69       val xthms = lookup net (Thm.term_of ct)
    70       fun select ct = map_filter (f (maybe_instantiate ct)) xthms 
    71       fun select' ct =
    72         let val thm = Thm.trivial ct
    73         in map_filter (f (try (fn rule => rule COMP thm))) xthms end
    74     in (case select ct of [] => select' ct | xthms' => xthms') end
    75 in
    76 
    77 fun net_instances net =
    78   instances_from_net false (fn f => fn (i, thm) => Option.map (pair i) (f thm))
    79     net
    80 
    81 fun net_instance net = try hd o instances_from_net true I net
    82 
    83 end
    84 
    85 
    86 
    87 (* proof combinators *)
    88 
    89 fun under_assumption f ct =
    90   let val ct' = Old_SMT_Utils.mk_cprop ct
    91   in Thm.implies_intr ct' (f (Thm.assume ct')) end
    92 
    93 fun with_conv conv prove ct =
    94   let val eq = Thm.symmetric (conv ct)
    95   in Thm.equal_elim eq (prove (Thm.lhs_of eq)) end
    96 
    97 fun discharge p pq = Thm.implies_elim pq p
    98 
    99 fun varify vars = Drule.generalize ([], vars)
   100 
   101 fun unfold_eqs _ [] = Conv.all_conv
   102   | unfold_eqs ctxt eqs =
   103       Conv.top_sweep_conv (K (Conv.rewrs_conv eqs)) ctxt
   104 
   105 fun match_instantiate f ct thm =
   106   Thm.instantiate (Thm.match (f (Thm.cprop_of thm), ct)) thm
   107 
   108 fun by_tac ctxt tac ct = Goal.norm_result ctxt (Goal.prove_internal ctxt [] ct (K (tac 1)))
   109 
   110 (*
   111    |- c x == t x ==> P (c x)
   112   ---------------------------
   113       c == t |- P (c x)
   114 *) 
   115 fun make_hyp_def thm ctxt =
   116   let
   117     val (lhs, rhs) = Thm.dest_binop (Thm.cprem_of thm 1)
   118     val (cf, cvs) = Drule.strip_comb lhs
   119     val eq = Old_SMT_Utils.mk_cequals cf (fold_rev Thm.lambda cvs rhs)
   120     fun apply cv th =
   121       Thm.combination th (Thm.reflexive cv)
   122       |> Conv.fconv_rule (Conv.arg_conv (Thm.beta_conversion false))
   123   in
   124     yield_singleton Assumption.add_assumes eq ctxt
   125     |>> Thm.implies_elim thm o fold apply cvs
   126   end
   127 
   128 
   129 
   130 (* abstraction *)
   131 
   132 local
   133 
   134 fun abs_context ctxt = (ctxt, Termtab.empty, 1, false)
   135 
   136 fun context_of (ctxt, _, _, _) = ctxt
   137 
   138 fun replace (_, (cv, ct)) = Thm.forall_elim ct o Thm.forall_intr cv
   139 
   140 fun abs_instantiate (_, tab, _, beta_norm) =
   141   fold replace (Termtab.dest tab) #>
   142   beta_norm ? Conv.fconv_rule (Thm.beta_conversion true)
   143 
   144 fun lambda_abstract cvs t =
   145   let
   146     val frees = map Free (Term.add_frees t [])
   147     val cvs' = filter (fn cv => member (op aconv) frees (Thm.term_of cv)) cvs
   148     val vs = map (Term.dest_Free o Thm.term_of) cvs'
   149   in (fold_rev absfree vs t, cvs') end
   150 
   151 fun fresh_abstraction (_, cvs) ct (cx as (ctxt, tab, idx, beta_norm)) =
   152   let val (t, cvs') = lambda_abstract cvs (Thm.term_of ct)
   153   in
   154     (case Termtab.lookup tab t of
   155       SOME (cv, _) => (Drule.list_comb (cv, cvs'), cx)
   156     | NONE =>
   157         let
   158           val (n, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt
   159           val cv = Thm.cterm_of ctxt'
   160             (Free (n, map Thm.typ_of_cterm cvs' ---> Thm.typ_of_cterm ct))
   161           val cu = Drule.list_comb (cv, cvs')
   162           val e = (t, (cv, fold_rev Thm.lambda cvs' ct))
   163           val beta_norm' = beta_norm orelse not (null cvs')
   164         in (cu, (ctxt', Termtab.update e tab, idx + 1, beta_norm')) end)
   165   end
   166 
   167 fun abs_comb f g dcvs ct =
   168   let val (cf, cu) = Thm.dest_comb ct
   169   in f dcvs cf ##>> g dcvs cu #>> uncurry Thm.apply end
   170 
   171 fun abs_arg f = abs_comb (K pair) f
   172 
   173 fun abs_args f dcvs ct =
   174   (case Thm.term_of ct of
   175     _ $ _ => abs_comb (abs_args f) f dcvs ct
   176   | _ => pair ct)
   177 
   178 fun abs_list f g dcvs ct =
   179   (case Thm.term_of ct of
   180     Const (@{const_name Nil}, _) => pair ct
   181   | Const (@{const_name Cons}, _) $ _ $ _ =>
   182       abs_comb (abs_arg f) (abs_list f g) dcvs ct
   183   | _ => g dcvs ct)
   184 
   185 fun abs_abs f (depth, cvs) ct =
   186   let val (cv, cu) = Thm.dest_abs NONE ct
   187   in f (depth, cv :: cvs) cu #>> Thm.lambda cv end
   188 
   189 val is_atomic =
   190   (fn Free _ => true | Var _ => true | Bound _ => true | _ => false)
   191 
   192 fun abstract depth (ext_logic, with_theories) =
   193   let
   194     fun abstr1 cvs ct = abs_arg abstr cvs ct
   195     and abstr2 cvs ct = abs_comb abstr1 abstr cvs ct
   196     and abstr3 cvs ct = abs_comb abstr2 abstr cvs ct
   197     and abstr_abs cvs ct = abs_arg (abs_abs abstr) cvs ct
   198 
   199     and abstr (dcvs as (d, cvs)) ct =
   200       (case Thm.term_of ct of
   201         @{const Trueprop} $ _ => abstr1 dcvs ct
   202       | @{const Pure.imp} $ _ $ _ => abstr2 dcvs ct
   203       | @{const True} => pair ct
   204       | @{const False} => pair ct
   205       | @{const Not} $ _ => abstr1 dcvs ct
   206       | @{const HOL.conj} $ _ $ _ => abstr2 dcvs ct
   207       | @{const HOL.disj} $ _ $ _ => abstr2 dcvs ct
   208       | @{const HOL.implies} $ _ $ _ => abstr2 dcvs ct
   209       | Const (@{const_name HOL.eq}, _) $ _ $ _ => abstr2 dcvs ct
   210       | Const (@{const_name distinct}, _) $ _ =>
   211           if ext_logic then abs_arg (abs_list abstr fresh_abstraction) dcvs ct
   212           else fresh_abstraction dcvs ct
   213       | Const (@{const_name If}, _) $ _ $ _ $ _ =>
   214           if ext_logic then abstr3 dcvs ct else fresh_abstraction dcvs ct
   215       | Const (@{const_name All}, _) $ _ =>
   216           if ext_logic then abstr_abs dcvs ct else fresh_abstraction dcvs ct
   217       | Const (@{const_name Ex}, _) $ _ =>
   218           if ext_logic then abstr_abs dcvs ct else fresh_abstraction dcvs ct
   219       | t => (fn cx =>
   220           if is_atomic t orelse can HOLogic.dest_number t then (ct, cx)
   221           else if with_theories andalso
   222             Old_Z3_Interface.is_builtin_theory_term (context_of cx) t
   223           then abs_args abstr dcvs ct cx
   224           else if d = 0 then fresh_abstraction dcvs ct cx
   225           else
   226             (case Term.strip_comb t of
   227               (Const _, _) => abs_args abstr (d-1, cvs) ct cx
   228             | (Free _, _) => abs_args abstr (d-1, cvs) ct cx
   229             | _ => fresh_abstraction dcvs ct cx)))
   230   in abstr (depth, []) end
   231 
   232 val cimp = Thm.cterm_of @{context} @{const Pure.imp}
   233 
   234 fun deepen depth f x =
   235   if depth = 0 then f depth x
   236   else (case try (f depth) x of SOME y => y | NONE => deepen (depth - 1) f x)
   237 
   238 fun with_prems depth thms f ct =
   239   fold_rev (Thm.mk_binop cimp o Thm.cprop_of) thms ct
   240   |> deepen depth f
   241   |> fold (fn prem => fn th => Thm.implies_elim th prem) thms
   242 
   243 in
   244 
   245 fun by_abstraction depth mode ctxt thms prove =
   246   with_prems depth thms (fn d => fn ct =>
   247     let val (cu, cx) = abstract d mode ct (abs_context ctxt)
   248     in abs_instantiate cx (prove (context_of cx) cu) end)
   249 
   250 end
   251 
   252 
   253 
   254 (* a faster COMP *)
   255 
   256 type compose_data = cterm list * (cterm -> cterm list) * thm
   257 
   258 fun list2 (x, y) = [x, y]
   259 
   260 fun precompose f rule = (f (Thm.cprem_of rule 1), f, rule)
   261 fun precompose2 f rule = precompose (list2 o f) rule
   262 
   263 fun compose (cvs, f, rule) thm =
   264   discharge thm (Thm.instantiate ([], cvs ~~ f (Thm.cprop_of thm)) rule)
   265 
   266 
   267 
   268 (* unfolding of 'distinct' *)
   269 
   270 local
   271   val set1 = @{lemma "x ~: set [] == ~False" by simp}
   272   val set2 = @{lemma "x ~: set [x] == False" by simp}
   273   val set3 = @{lemma "x ~: set [y] == x ~= y" by simp}
   274   val set4 = @{lemma "x ~: set (x # ys) == False" by simp}
   275   val set5 = @{lemma "x ~: set (y # ys) == x ~= y & x ~: set ys" by simp}
   276 
   277   fun set_conv ct =
   278     (Conv.rewrs_conv [set1, set2, set3, set4] else_conv
   279     (Conv.rewr_conv set5 then_conv Conv.arg_conv set_conv)) ct
   280 
   281   val dist1 = @{lemma "distinct [] == ~False" by (simp add: distinct_def)}
   282   val dist2 = @{lemma "distinct [x] == ~False" by (simp add: distinct_def)}
   283   val dist3 = @{lemma "distinct (x # xs) == x ~: set xs & distinct xs"
   284     by (simp add: distinct_def)}
   285 
   286   fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
   287 in
   288 fun unfold_distinct_conv ct =
   289   (Conv.rewrs_conv [dist1, dist2] else_conv
   290   (Conv.rewr_conv dist3 then_conv binop_conv set_conv unfold_distinct_conv)) ct
   291 end
   292 
   293 
   294 
   295 (* simpset *)
   296 
   297 local
   298   val antisym_le1 = mk_meta_eq @{thm order_class.antisym_conv}
   299   val antisym_le2 = mk_meta_eq @{thm linorder_class.antisym_conv2}
   300   val antisym_less1 = mk_meta_eq @{thm linorder_class.antisym_conv1}
   301   val antisym_less2 = mk_meta_eq @{thm linorder_class.antisym_conv3}
   302 
   303   fun eq_prop t thm = HOLogic.mk_Trueprop t aconv Thm.prop_of thm
   304   fun dest_binop ((c as Const _) $ t $ u) = (c, t, u)
   305     | dest_binop t = raise TERM ("dest_binop", [t])
   306 
   307   fun prove_antisym_le ctxt t =
   308     let
   309       val (le, r, s) = dest_binop t
   310       val less = Const (@{const_name less}, Term.fastype_of le)
   311       val prems = Simplifier.prems_of ctxt
   312     in
   313       (case find_first (eq_prop (le $ s $ r)) prems of
   314         NONE =>
   315           find_first (eq_prop (HOLogic.mk_not (less $ r $ s))) prems
   316           |> Option.map (fn thm => thm RS antisym_less1)
   317       | SOME thm => SOME (thm RS antisym_le1))
   318     end
   319     handle THM _ => NONE
   320 
   321   fun prove_antisym_less ctxt t =
   322     let
   323       val (less, r, s) = dest_binop (HOLogic.dest_not t)
   324       val le = Const (@{const_name less_eq}, Term.fastype_of less)
   325       val prems = Simplifier.prems_of ctxt
   326     in
   327       (case find_first (eq_prop (le $ r $ s)) prems of
   328         NONE =>
   329           find_first (eq_prop (HOLogic.mk_not (less $ s $ r))) prems
   330           |> Option.map (fn thm => thm RS antisym_less2)
   331       | SOME thm => SOME (thm RS antisym_le2))
   332   end
   333   handle THM _ => NONE
   334 
   335   val basic_simpset =
   336     simpset_of (put_simpset HOL_ss @{context}
   337       addsimps @{thms field_simps}
   338       addsimps [@{thm times_divide_eq_right}, @{thm times_divide_eq_left}]
   339       addsimps @{thms arith_special} addsimps @{thms arith_simps}
   340       addsimps @{thms rel_simps}
   341       addsimps @{thms array_rules}
   342       addsimps @{thms term_true_def} addsimps @{thms term_false_def}
   343       addsimps @{thms z3div_def} addsimps @{thms z3mod_def}
   344       addsimprocs [@{simproc binary_int_div}, @{simproc binary_int_mod}]
   345       addsimprocs [
   346         Simplifier.simproc_global @{theory} "fast_int_arith" [
   347           "(m::int) < n", "(m::int) <= n", "(m::int) = n"] Lin_Arith.simproc,
   348         Simplifier.simproc_global @{theory} "antisym_le" ["(x::'a::order) <= y"]
   349           prove_antisym_le,
   350         Simplifier.simproc_global @{theory} "antisym_less" ["~ (x::'a::linorder) < y"]
   351           prove_antisym_less])
   352 
   353   structure Simpset = Generic_Data
   354   (
   355     type T = simpset
   356     val empty = basic_simpset
   357     val extend = I
   358     val merge = Simplifier.merge_ss
   359   )
   360 in
   361 
   362 fun add_simproc simproc context =
   363   Simpset.map (simpset_map (Context.proof_of context)
   364     (fn ctxt => ctxt addsimprocs [simproc])) context
   365 
   366 fun make_simpset ctxt rules =
   367   simpset_of (put_simpset (Simpset.get (Context.Proof ctxt)) ctxt addsimps rules)
   368 
   369 end
   370 
   371 end