src/HOL/Decision_Procs/ferrack_tac.ML
author wenzelm
Wed, 10 Aug 2011 20:53:43 +0200
changeset 44121 44adaa6db327
parent 42361 23f352990944
child 45654 cf10bde35973
permissions -rw-r--r--
old term operations are legacy;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30439
57c68b3af2ea Updated paths in Decision_Procs comments and NEWS
hoelzl
parents: 30242
diff changeset
     1
(*  Title:      HOL/Decision_Procs/ferrack_tac.ML
29788
1b80ebe713a4 established session HOL-Reflection
haftmann
parents: 29265
diff changeset
     2
    Author:     Amine Chaieb, TU Muenchen
1b80ebe713a4 established session HOL-Reflection
haftmann
parents: 29265
diff changeset
     3
*)
1b80ebe713a4 established session HOL-Reflection
haftmann
parents: 29265
diff changeset
     4
31302
12677a808d43 proper signature constraint;
wenzelm
parents: 30510
diff changeset
     5
signature FERRACK_TAC =
12677a808d43 proper signature constraint;
wenzelm
parents: 30510
diff changeset
     6
sig
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 31790
diff changeset
     7
  val trace: bool Unsynchronized.ref
31302
12677a808d43 proper signature constraint;
wenzelm
parents: 30510
diff changeset
     8
  val linr_tac: Proof.context -> bool -> int -> tactic
12677a808d43 proper signature constraint;
wenzelm
parents: 30510
diff changeset
     9
  val setup: theory -> theory
12677a808d43 proper signature constraint;
wenzelm
parents: 30510
diff changeset
    10
end
12677a808d43 proper signature constraint;
wenzelm
parents: 30510
diff changeset
    11
29788
1b80ebe713a4 established session HOL-Reflection
haftmann
parents: 29265
diff changeset
    12
structure Ferrack_Tac =
23264
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    13
struct
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    14
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 31790
diff changeset
    15
val trace = Unsynchronized.ref false;
23264
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    16
fun trace_msg s = if !trace then tracing s else ();
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    17
26075
815f3ccc0b45 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents: 23590
diff changeset
    18
val ferrack_ss = let val ths = [@{thm real_of_int_inject}, @{thm real_of_int_less_iff}, 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32740
diff changeset
    19
                                @{thm real_of_int_le_iff}]
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32740
diff changeset
    20
             in @{simpset} delsimps ths addsimps (map (fn th => th RS sym) ths)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32740
diff changeset
    21
             end;
23264
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    22
26075
815f3ccc0b45 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents: 23590
diff changeset
    23
val binarith =
815f3ccc0b45 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents: 23590
diff changeset
    24
  @{thms normalize_bin_simps} @ @{thms pred_bin_simps} @ @{thms succ_bin_simps} @
815f3ccc0b45 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents: 23590
diff changeset
    25
  @{thms add_bin_simps} @ @{thms minus_bin_simps} @  @{thms mult_bin_simps};
23318
6d68b07ab5cf tuned tactic
chaieb
parents: 23264
diff changeset
    26
val comp_arith = binarith @ simp_thms
23264
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    27
26075
815f3ccc0b45 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents: 23590
diff changeset
    28
val zdvd_int = @{thm zdvd_int};
815f3ccc0b45 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents: 23590
diff changeset
    29
val zdiff_int_split = @{thm zdiff_int_split};
815f3ccc0b45 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents: 23590
diff changeset
    30
val all_nat = @{thm all_nat};
815f3ccc0b45 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents: 23590
diff changeset
    31
val ex_nat = @{thm ex_nat};
815f3ccc0b45 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents: 23590
diff changeset
    32
val number_of1 = @{thm number_of1};
815f3ccc0b45 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents: 23590
diff changeset
    33
val number_of2 = @{thm number_of2};
815f3ccc0b45 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents: 23590
diff changeset
    34
val split_zdiv = @{thm split_zdiv};
815f3ccc0b45 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents: 23590
diff changeset
    35
val split_zmod = @{thm split_zmod};
815f3ccc0b45 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents: 23590
diff changeset
    36
val mod_div_equality' = @{thm mod_div_equality'};
815f3ccc0b45 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents: 23590
diff changeset
    37
val split_div' = @{thm split_div'};
31790
05c92381363c corrected and unified thm names
nipkow
parents: 31302
diff changeset
    38
val Suc_eq_plus1 = @{thm Suc_eq_plus1};
26075
815f3ccc0b45 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents: 23590
diff changeset
    39
val imp_le_cong = @{thm imp_le_cong};
815f3ccc0b45 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents: 23590
diff changeset
    40
val conj_le_cong = @{thm conj_le_cong};
30034
60f64f112174 removed redundant thms
nipkow
parents: 29948
diff changeset
    41
val mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
60f64f112174 removed redundant thms
nipkow
parents: 29948
diff changeset
    42
val mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
26075
815f3ccc0b45 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents: 23590
diff changeset
    43
val nat_div_add_eq = @{thm div_add1_eq} RS sym;
815f3ccc0b45 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents: 23590
diff changeset
    44
val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
815f3ccc0b45 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents: 23590
diff changeset
    45
val ZDIVISION_BY_ZERO_MOD = @{thm DIVISION_BY_ZERO} RS conjunct2;
815f3ccc0b45 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents: 23590
diff changeset
    46
val ZDIVISION_BY_ZERO_DIV = @{thm DIVISION_BY_ZERO} RS conjunct1;
23264
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    47
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    48
fun prepare_for_linr sg q fm = 
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    49
  let
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    50
    val ps = Logic.strip_params fm
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    51
    val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    52
    val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    53
    fun mk_all ((s, T), (P,n)) =
42083
e1209fc7ecdc added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
wenzelm
parents: 38558
diff changeset
    54
      if Term.is_dependent P then
23264
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    55
        (HOLogic.all_const T $ Abs (s, T, P), n)
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    56
      else (incr_boundvars ~1 P, n-1)
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    57
    fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    58
      val rhs = hs
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    59
(*    val (rhs,irhs) = List.partition (relevant (rev ps)) hs *)
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    60
    val np = length ps
33004
715566791eb0 always qualify NJ's old List.foldl/foldr in Isabelle/ML;
wenzelm
parents: 32960
diff changeset
    61
    val (fm',np) =  List.foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
715566791eb0 always qualify NJ's old List.foldl/foldr in Isabelle/ML;
wenzelm
parents: 32960
diff changeset
    62
      (List.foldr HOLogic.mk_imp c rhs, np) ps
27436
9581777503e9 code antiquotation roaring ahead
haftmann
parents: 26939
diff changeset
    63
    val (vs, _) = List.partition (fn t => q orelse (type_of t) = HOLogic.natT)
44121
44adaa6db327 old term operations are legacy;
wenzelm
parents: 42361
diff changeset
    64
      (Misc_Legacy.term_frees fm' @ Misc_Legacy.term_vars fm');
33004
715566791eb0 always qualify NJ's old List.foldl/foldr in Isabelle/ML;
wenzelm
parents: 32960
diff changeset
    65
    val fm2 = List.foldr mk_all2 fm' vs
23264
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    66
  in (fm2, np + length vs, length rhs) end;
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    67
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    68
(*Object quantifier to meta --*)
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    69
fun spec_step n th = if (n=0) then th else (spec_step (n-1) th) RS spec ;
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    70
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    71
(* object implication to meta---*)
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    72
fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    73
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    74
35233
6af1caf7be69 local Simplifier.context;
wenzelm
parents: 35232
diff changeset
    75
fun linr_tac ctxt q =
35625
9c818cab0dd0 modernized structure Object_Logic;
wenzelm
parents: 35233
diff changeset
    76
    Object_Logic.atomize_prems_tac
35233
6af1caf7be69 local Simplifier.context;
wenzelm
parents: 35232
diff changeset
    77
        THEN' (REPEAT_DETERM o split_tac [@{thm split_min}, @{thm split_max}, @{thm abs_split}])
6af1caf7be69 local Simplifier.context;
wenzelm
parents: 35232
diff changeset
    78
        THEN' SUBGOAL (fn (g, i) =>
23264
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    79
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42083
diff changeset
    80
    val thy = Proof_Context.theory_of ctxt
23264
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    81
    (* Transform the term*)
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    82
    val (t,np,nh) = prepare_for_linr thy q g
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    83
    (* Some simpsets for dealing with mod div abs and nat*)
35233
6af1caf7be69 local Simplifier.context;
wenzelm
parents: 35232
diff changeset
    84
    val simpset0 = Simplifier.context ctxt HOL_basic_ss addsimps comp_arith
23264
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    85
    val ct = cterm_of thy (HOLogic.mk_Trueprop t)
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    86
    (* Theorem for the nat --> int transformation *)
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    87
   val pre_thm = Seq.hd (EVERY
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    88
      [simp_tac simpset0 1,
35233
6af1caf7be69 local Simplifier.context;
wenzelm
parents: 35232
diff changeset
    89
       TRY (simp_tac (Simplifier.context ctxt ferrack_ss) 1)]
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36853
diff changeset
    90
      (Thm.trivial ct))
23264
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    91
    fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    92
    (* The result of the quantifier elimination *)
35233
6af1caf7be69 local Simplifier.context;
wenzelm
parents: 35232
diff changeset
    93
    val (th, tac) = case prop_of pre_thm of
38558
32ad17fe2b9c tuned quotes
haftmann
parents: 38549
diff changeset
    94
        Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
36853
c8e4102b08aa modernized specifications; tuned reification
haftmann
parents: 36692
diff changeset
    95
    let val pth = linr_oracle (ctxt, Pattern.eta_long [] t1)
23264
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    96
    in 
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    97
          (trace_msg ("calling procedure with term:\n" ^
26939
1035c89b4c02 moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents: 26075
diff changeset
    98
             Syntax.string_of_term ctxt t1);
23264
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
    99
           ((pth RS iffD2) RS pre_thm,
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
   100
            assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
   101
    end
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
   102
      | _ => (pre_thm, assm_tac i)
35233
6af1caf7be69 local Simplifier.context;
wenzelm
parents: 35232
diff changeset
   103
  in rtac ((mp_step nh o spec_step np) th) i THEN tac end);
23264
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
   104
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
   105
val setup =
31302
12677a808d43 proper signature constraint;
wenzelm
parents: 30510
diff changeset
   106
  Method.setup @{binding rferrack}
12677a808d43 proper signature constraint;
wenzelm
parents: 30510
diff changeset
   107
    (Args.mode "no_quantify" >> (fn q => fn ctxt =>
12677a808d43 proper signature constraint;
wenzelm
parents: 30510
diff changeset
   108
      SIMPLE_METHOD' (linr_tac ctxt (not q))))
12677a808d43 proper signature constraint;
wenzelm
parents: 30510
diff changeset
   109
    "decision procedure for linear real arithmetic";
23264
324622260d29 Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff changeset
   110
23469
3f309f885d0b add thm antiquotations
huffman
parents: 23318
diff changeset
   111
end