src/HOL/Complex/ex/linrtac.ML
author chaieb
Tue, 05 Jun 2007 20:44:12 +0200
changeset 23264 324622260d29
child 23318 6d68b07ab5cf
permissions -rw-r--r--
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
     1
structure LinrTac =
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
     2
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
     3
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
     4
val trace = ref false;
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
     5
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
     6
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
     7
val ferrack_ss = let val ths = map thm ["real_of_int_inject", "real_of_int_less_iff", 
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
     8
				"real_of_int_le_iff"]
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
     9
	     in @{simpset} delsimps ths addsimps (map (fn th => th RS sym) ths)
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
    10
	     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
    11
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
    12
val nT = HOLogic.natT;
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
val binarith = map 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
    14
  ["Pls_0_eq", "Min_1_eq",
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
    15
 "pred_Pls","pred_Min","pred_1","pred_0",
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
  "succ_Pls", "succ_Min", "succ_1", "succ_0",
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
  "add_Pls", "add_Min", "add_BIT_0", "add_BIT_10",
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
    18
  "add_BIT_11", "minus_Pls", "minus_Min", "minus_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
    19
  "minus_0", "mult_Pls", "mult_Min", "mult_num1", "mult_num0", 
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
    20
  "add_Pls_right", "add_Min_right"];
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
    21
 val intarithrel = 
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
     (map thm ["int_eq_number_of_eq","int_neg_number_of_BIT", 
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
    23
		"int_le_number_of_eq","int_iszero_number_of_0",
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
    24
		"int_less_number_of_eq_neg"]) @
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
    25
     (map (fn s => thm s RS thm "lift_bool") 
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
    26
	  ["int_iszero_number_of_Pls","int_iszero_number_of_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
    27
	   "int_neg_number_of_Min"])@
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
    28
     (map (fn s => thm s RS thm "nlift_bool") 
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
    29
	  ["int_nonzero_number_of_Min","int_not_neg_number_of_Pls"]);
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
    30
     
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
    31
val intarith = map thm ["int_number_of_add_sym", "int_number_of_minus_sym",
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
    32
			"int_number_of_diff_sym", "int_number_of_mult_sym"];
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
    33
val natarith = map thm ["add_nat_number_of", "diff_nat_number_of",
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
    34
			"mult_nat_number_of", "eq_nat_number_of",
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
    35
			"less_nat_number_of"]
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
    36
val powerarith = 
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
    37
    (map thm ["nat_number_of", "zpower_number_of_even", 
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
    38
	      "zpower_Pls", "zpower_Min"]) @ 
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
    39
    [thm "zpower_number_of_odd"]
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
    40
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
    41
val comp_arith = binarith @ intarith @ intarithrel @ natarith 
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
    42
	    @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
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
    43
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
    44
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
    45
val zdvd_int = thm "zdvd_int";
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
    46
val zdiff_int_split = thm "zdiff_int_split";
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
val all_nat = thm "all_nat";
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
val ex_nat = thm "ex_nat";
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
val number_of1 = thm "number_of1";
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 number_of2 = thm "number_of2";
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 split_zdiv = thm "split_zdiv";
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 split_zmod = thm "split_zmod";
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
val mod_div_equality' = thm "mod_div_equality'";
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
    54
val split_div' = thm "split_div'";
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
val Suc_plus1 = thm "Suc_plus1";
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
val imp_le_cong = thm "imp_le_cong";
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
val conj_le_cong = thm "conj_le_cong";
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 nat_mod_add_eq = mod_add1_eq RS sym;
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 nat_mod_add_left_eq = mod_add_left_eq RS sym;
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 nat_mod_add_right_eq = mod_add_right_eq RS sym;
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
    61
val int_mod_add_eq = @{thm "zmod_zadd1_eq"} RS sym;
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
    62
val int_mod_add_left_eq = @{thm "zmod_zadd_left_eq"} RS sym;
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
    63
val int_mod_add_right_eq = @{thm "zmod_zadd_right_eq"} RS sym;
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
    64
val nat_div_add_eq = @{thm "div_add1_eq"} RS sym;
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
    65
val int_div_add_eq = @{thm "zdiv_zadd1_eq"} RS sym;
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
val ZDIVISION_BY_ZERO_MOD = @{thm "DIVISION_BY_ZERO"} RS conjunct2;
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
val ZDIVISION_BY_ZERO_DIV = @{thm "DIVISION_BY_ZERO"} RS conjunct1;
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
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 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
    70
  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
    71
    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
    72
    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
    73
    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
    74
    fun mk_all ((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
    75
      if 0 mem loose_bnos P then
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
    76
        (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
    77
      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
    78
    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
    79
      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
    80
(*    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
    81
    val np = length ps
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 (fm',np) =  foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,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
    83
      (foldr HOLogic.mk_imp c rhs, np) ps
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
    84
    val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
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
      (term_frees fm' @ term_vars 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
    86
    val fm2 = foldr mk_all2 fm' vs
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
  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
    88
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
    89
(*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
    90
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
    91
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
(* 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
    93
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
    94
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
    95
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
fun linr_tac ctxt q 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
    97
    (ObjectLogic.atomize_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
    98
	THEN (REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}] 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
    99
	THEN (fn st =>
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
  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
   101
    val g = List.nth (prems_of st, i - 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
   102
    val thy = ProofContext.theory_of ctxt
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
   103
    (* 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
   104
    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
   105
    (* Some simpsets for dealing with mod div abs and nat*)
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
   106
    val simpset0 = Simplifier.theory_context thy HOL_basic_ss addsimps comp_arith
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
   107
    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
   108
    (* 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
   109
   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
   110
      [simp_tac simpset0 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
   111
       TRY (simp_tac (Simplifier.theory_context thy ferrack_ss) 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
   112
      (trivial ct))
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
   113
    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
   114
    (* The result of the quantifier elimination *)
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
   115
    val (th, tac) = case (prop_of pre_thm) of
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
   116
        Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
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
   117
    let val pth = linr_oracle thy (Pattern.eta_long [] t1)
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
   118
    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
   119
          (trace_msg ("calling procedure with term:\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
   120
             Sign.string_of_term thy t1);
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
   121
           ((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
   122
            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
   123
    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
   124
      | _ => (pre_thm, assm_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
   125
  in (rtac (((mp_step nh) o (spec_step np)) th) 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
   126
      THEN tac) st
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
   127
  end handle Subscript => no_tac st | ReflectedFerrack.LINR => no_tac st);
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
   128
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
   129
fun linr_meth src =
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
   130
  Method.syntax (Args.mode "no_quantify") src
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
   131
  #> (fn (q, ctxt) => Method.SIMPLE_METHOD' (linr_tac ctxt (not q)));
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
   132
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
   133
val setup =
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
   134
  Method.add_method ("rferrack", linr_meth,
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
   135
     "decision procedure for linear real arithmetic");
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
   136
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
   137
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
   138
end