src/HOL/Decision_Procs/ferrack_tac.ML
author wenzelm
Fri Mar 21 20:33:56 2014 +0100 (2014-03-21)
changeset 56245 84fc7dfa3cd4
parent 55498 cf829d10d1d4
child 58956 a816aa3ff391
permissions -rw-r--r--
more qualified names;
     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 real_of_int_inject}, @{thm real_of_int_less_iff}, 
    14                                 @{thm real_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 [@{thm split_min}, @{thm split_max}, @{thm abs_split}])
    51         THEN' SUBGOAL (fn (g, i) =>
    52   let
    53     val thy = Proof_Context.theory_of ctxt
    54     (* Transform the term*)
    55     val (t,np,nh) = prepare_for_linr q g
    56     (* Some simpsets for dealing with mod div abs and nat*)
    57     val simpset0 = put_simpset HOL_basic_ss ctxt addsimps comp_arith
    58     val ct = cterm_of thy (HOLogic.mk_Trueprop t)
    59     (* Theorem for the nat --> int transformation *)
    60    val pre_thm = Seq.hd (EVERY
    61       [simp_tac simpset0 1,
    62        TRY (simp_tac (put_simpset ferrack_ss ctxt) 1)]
    63       (Thm.trivial ct))
    64     fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
    65     (* The result of the quantifier elimination *)
    66     val (th, tac) = case prop_of pre_thm of
    67         Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
    68     let val pth = linr_oracle (ctxt, Envir.eta_long [] t1)
    69     in 
    70        ((pth RS iffD2) RS pre_thm,
    71         assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))
    72     end
    73       | _ => (pre_thm, assm_tac i)
    74   in rtac ((mp_step nh o spec_step np) th) i THEN tac end);
    75 
    76 end