author  chaieb 
Tue, 05 Jun 2007 20:44:12 +0200  
changeset 23264  324622260d29 
child 23318  6d68b07ab5cf 
permissions  rwrr 
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, n1) 
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 (n1) 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 (n1) 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 