src/HOL/Decision_Procs/ferrack_tac.ML
changeset 31302 12677a808d43
parent 30510 4120fc59dd85
child 31790 05c92381363c
equal deleted inserted replaced
31301:952d2d0c4446 31302:12677a808d43
     1 (*  Title:      HOL/Decision_Procs/ferrack_tac.ML
     1 (*  Title:      HOL/Decision_Procs/ferrack_tac.ML
     2     Author:     Amine Chaieb, TU Muenchen
     2     Author:     Amine Chaieb, TU Muenchen
     3 *)
     3 *)
       
     4 
       
     5 signature FERRACK_TAC =
       
     6 sig
       
     7   val trace: bool ref
       
     8   val linr_tac: Proof.context -> bool -> int -> tactic
       
     9   val setup: theory -> theory
       
    10 end
     4 
    11 
     5 structure Ferrack_Tac =
    12 structure Ferrack_Tac =
     6 struct
    13 struct
     7 
    14 
     8 val trace = ref false;
    15 val trace = ref false;
    96       | _ => (pre_thm, assm_tac i)
   103       | _ => (pre_thm, assm_tac i)
    97   in (rtac (((mp_step nh) o (spec_step np)) th) i 
   104   in (rtac (((mp_step nh) o (spec_step np)) th) i 
    98       THEN tac) st
   105       THEN tac) st
    99   end handle Subscript => no_tac st);
   106   end handle Subscript => no_tac st);
   100 
   107 
   101 fun linr_meth src =
       
   102   Method.syntax (Args.mode "no_quantify") src
       
   103   #> (fn (q, ctxt) => SIMPLE_METHOD' (linr_tac ctxt (not q)));
       
   104 
       
   105 val setup =
   108 val setup =
   106   Method.add_method ("rferrack", linr_meth,
   109   Method.setup @{binding rferrack}
   107      "decision procedure for linear real arithmetic");
   110     (Args.mode "no_quantify" >> (fn q => fn ctxt =>
       
   111       SIMPLE_METHOD' (linr_tac ctxt (not q))))
       
   112     "decision procedure for linear real arithmetic";
   108 
   113 
   109 end
   114 end