src/HOL/Decision_Procs/ferrack_tac.ML
author nipkow
Tue Mar 03 17:05:18 2009 +0100 (2009-03-03)
changeset 30224 79136ce06bdb
parent 30034 60f64f112174
child 30242 aea5d7fa7ef5
permissions -rw-r--r--
removed and renamed redundant lemmas
     1 (*  Title:      HOL/Reflection/ferrack_tac.ML
     2     Author:     Amine Chaieb, TU Muenchen
     3 *)
     4 
     5 structure Ferrack_Tac =
     6 struct
     7 
     8 val trace = ref false;
     9 fun trace_msg s = if !trace then tracing s else ();
    10 
    11 val ferrack_ss = let val ths = [@{thm real_of_int_inject}, @{thm real_of_int_less_iff}, 
    12 				@{thm real_of_int_le_iff}]
    13 	     in @{simpset} delsimps ths addsimps (map (fn th => th RS sym) ths)
    14 	     end;
    15 
    16 val binarith =
    17   @{thms normalize_bin_simps} @ @{thms pred_bin_simps} @ @{thms succ_bin_simps} @
    18   @{thms add_bin_simps} @ @{thms minus_bin_simps} @  @{thms mult_bin_simps};
    19 val comp_arith = binarith @ simp_thms
    20 
    21 val zdvd_int = @{thm zdvd_int};
    22 val zdiff_int_split = @{thm zdiff_int_split};
    23 val all_nat = @{thm all_nat};
    24 val ex_nat = @{thm ex_nat};
    25 val number_of1 = @{thm number_of1};
    26 val number_of2 = @{thm number_of2};
    27 val split_zdiv = @{thm split_zdiv};
    28 val split_zmod = @{thm split_zmod};
    29 val mod_div_equality' = @{thm mod_div_equality'};
    30 val split_div' = @{thm split_div'};
    31 val Suc_plus1 = @{thm Suc_plus1};
    32 val imp_le_cong = @{thm imp_le_cong};
    33 val conj_le_cong = @{thm conj_le_cong};
    34 val mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
    35 val mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
    36 val nat_div_add_eq = @{thm div_add1_eq} RS sym;
    37 val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
    38 val ZDIVISION_BY_ZERO_MOD = @{thm DIVISION_BY_ZERO} RS conjunct2;
    39 val ZDIVISION_BY_ZERO_DIV = @{thm DIVISION_BY_ZERO} RS conjunct1;
    40 
    41 fun prepare_for_linr sg q fm = 
    42   let
    43     val ps = Logic.strip_params fm
    44     val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
    45     val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
    46     fun mk_all ((s, T), (P,n)) =
    47       if 0 mem loose_bnos P then
    48         (HOLogic.all_const T $ Abs (s, T, P), n)
    49       else (incr_boundvars ~1 P, n-1)
    50     fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
    51       val rhs = hs
    52 (*    val (rhs,irhs) = List.partition (relevant (rev ps)) hs *)
    53     val np = length ps
    54     val (fm',np) =  foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
    55       (foldr HOLogic.mk_imp c rhs, np) ps
    56     val (vs, _) = List.partition (fn t => q orelse (type_of t) = HOLogic.natT)
    57       (OldTerm.term_frees fm' @ OldTerm.term_vars fm');
    58     val fm2 = foldr mk_all2 fm' vs
    59   in (fm2, np + length vs, length rhs) end;
    60 
    61 (*Object quantifier to meta --*)
    62 fun spec_step n th = if (n=0) then th else (spec_step (n-1) th) RS spec ;
    63 
    64 (* object implication to meta---*)
    65 fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
    66 
    67 
    68 fun linr_tac ctxt q i = 
    69     (ObjectLogic.atomize_prems_tac i) 
    70 	THEN (REPEAT_DETERM (split_tac [@{thm split_min}, @{thm split_max}, @{thm abs_split}] i))
    71 	THEN (fn st =>
    72   let
    73     val g = List.nth (prems_of st, i - 1)
    74     val thy = ProofContext.theory_of ctxt
    75     (* Transform the term*)
    76     val (t,np,nh) = prepare_for_linr thy q g
    77     (* Some simpsets for dealing with mod div abs and nat*)
    78     val simpset0 = Simplifier.theory_context thy HOL_basic_ss addsimps comp_arith
    79     val ct = cterm_of thy (HOLogic.mk_Trueprop t)
    80     (* Theorem for the nat --> int transformation *)
    81    val pre_thm = Seq.hd (EVERY
    82       [simp_tac simpset0 1,
    83        TRY (simp_tac (Simplifier.theory_context thy ferrack_ss) 1)]
    84       (trivial ct))
    85     fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
    86     (* The result of the quantifier elimination *)
    87     val (th, tac) = case (prop_of pre_thm) of
    88         Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
    89     let val pth = linr_oracle (cterm_of thy (Pattern.eta_long [] t1))
    90     in 
    91           (trace_msg ("calling procedure with term:\n" ^
    92              Syntax.string_of_term ctxt t1);
    93            ((pth RS iffD2) RS pre_thm,
    94             assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
    95     end
    96       | _ => (pre_thm, assm_tac i)
    97   in (rtac (((mp_step nh) o (spec_step np)) th) i 
    98       THEN tac) st
    99   end handle Subscript => no_tac st);
   100 
   101 fun linr_meth src =
   102   Method.syntax (Args.mode "no_quantify") src
   103   #> (fn (q, ctxt) => Method.SIMPLE_METHOD' (linr_tac ctxt (not q)));
   104 
   105 val setup =
   106   Method.add_method ("rferrack", linr_meth,
   107      "decision procedure for linear real arithmetic");
   108 
   109 end