src/HOL/Decision_Procs/ferrack_tac.ML
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 61609 77b453bd616f
child 69597 ff784d5a5bfb
permissions -rw-r--r--
executable domain membership checks
     1 (*  Title:      HOL/Decision_Procs/ferrack_tac.ML
     2     Author:     Amine Chaieb, TU Muenchen
     3 *)
     4 
     5 signature FERRACK_TAC =
     6 sig
     7   val linr_tac: Proof.context -> bool -> int -> tactic
     8 end
     9 
    10 structure Ferrack_Tac: FERRACK_TAC =
    11 struct
    12 
    13 val ferrack_ss = let val ths = [@{thm of_int_eq_iff}, @{thm of_int_less_iff}, 
    14                                 @{thm of_int_le_iff}]
    15              in @{context} delsimps ths addsimps (map (fn th => th RS sym) ths)
    16              end |> simpset_of;
    17 
    18 val binarith = @{thms arith_simps}
    19 val comp_arith = binarith @ @{thms simp_thms}
    20 
    21 fun prepare_for_linr q fm = 
    22   let
    23     val ps = Logic.strip_params fm
    24     val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
    25     val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
    26     fun mk_all ((s, T), (P,n)) =
    27       if Term.is_dependent P then
    28         (HOLogic.all_const T $ Abs (s, T, P), n)
    29       else (incr_boundvars ~1 P, n-1)
    30     fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
    31       val rhs = hs
    32 (*    val (rhs,irhs) = List.partition (relevant (rev ps)) hs *)
    33     val np = length ps
    34     val (fm',np) =  List.foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
    35       (List.foldr HOLogic.mk_imp c rhs, np) ps
    36     val (vs, _) = List.partition (fn t => q orelse (type_of t) = HOLogic.natT)
    37       (Misc_Legacy.term_frees fm' @ Misc_Legacy.term_vars fm');
    38     val fm2 = List.foldr mk_all2 fm' vs
    39   in (fm2, np + length vs, length rhs) end;
    40 
    41 (*Object quantifier to meta --*)
    42 fun spec_step n th = if (n=0) then th else (spec_step (n-1) th) RS spec ;
    43 
    44 (* object implication to meta---*)
    45 fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
    46 
    47 
    48 fun linr_tac ctxt q =
    49     Object_Logic.atomize_prems_tac ctxt
    50         THEN' (REPEAT_DETERM o split_tac ctxt [@{thm split_min}, @{thm split_max}, @{thm abs_split}])
    51         THEN' SUBGOAL (fn (g, i) =>
    52   let
    53     (* Transform the term*)
    54     val (t,np,nh) = prepare_for_linr q g
    55     (* Some simpsets for dealing with mod div abs and nat*)
    56     val simpset0 = put_simpset HOL_basic_ss ctxt addsimps comp_arith
    57     val ct = Thm.cterm_of ctxt (HOLogic.mk_Trueprop t)
    58     (* Theorem for the nat --> int transformation *)
    59    val pre_thm = Seq.hd (EVERY
    60       [simp_tac simpset0 1,
    61        TRY (simp_tac (put_simpset ferrack_ss ctxt) 1)]
    62       (Thm.trivial ct))
    63     fun assm_tac i = REPEAT_DETERM_N nh (assume_tac ctxt i)
    64     (* The result of the quantifier elimination *)
    65     val (th, tac) = case Thm.prop_of pre_thm of
    66         Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
    67     let val pth = linr_oracle (ctxt, Envir.eta_long [] t1)
    68     in 
    69        ((pth RS iffD2) RS pre_thm,
    70         assm_tac (i + 1) THEN (if q then I else TRY) (resolve_tac ctxt [TrueI] i))
    71     end
    72       | _ => (pre_thm, assm_tac i)
    73   in resolve_tac ctxt [(mp_step nh o spec_step np) th] i THEN tac end);
    74 
    75 end