23274

1 
structure LinZTac =


2 
struct


3 


4 
val trace = ref false;


5 
fun trace_msg s = if !trace then tracing s else ();


6 


7 
val cooper_ss = @{simpset};


8 


9 
val nT = HOLogic.natT;


10 
val binarith = map thm


11 
["Pls_0_eq", "Min_1_eq"];

23318

12 
val comp_arith = binarith @ simp_thms

23274

13 


14 
val zdvd_int = thm "zdvd_int";


15 
val zdiff_int_split = thm "zdiff_int_split";


16 
val all_nat = thm "all_nat";


17 
val ex_nat = thm "ex_nat";


18 
val number_of1 = thm "number_of1";


19 
val number_of2 = thm "number_of2";


20 
val split_zdiv = thm "split_zdiv";


21 
val split_zmod = thm "split_zmod";


22 
val mod_div_equality' = thm "mod_div_equality'";


23 
val split_div' = thm "split_div'";


24 
val Suc_plus1 = thm "Suc_plus1";


25 
val imp_le_cong = thm "imp_le_cong";


26 
val conj_le_cong = thm "conj_le_cong";


27 
val nat_mod_add_eq = mod_add1_eq RS sym;


28 
val nat_mod_add_left_eq = mod_add_left_eq RS sym;


29 
val nat_mod_add_right_eq = mod_add_right_eq RS sym;


30 
val int_mod_add_eq = @{thm "zmod_zadd1_eq"} RS sym;


31 
val int_mod_add_left_eq = @{thm "zmod_zadd_left_eq"} RS sym;


32 
val int_mod_add_right_eq = @{thm "zmod_zadd_right_eq"} RS sym;


33 
val nat_div_add_eq = @{thm "div_add1_eq"} RS sym;


34 
val int_div_add_eq = @{thm "zdiv_zadd1_eq"} RS sym;


35 
val ZDIVISION_BY_ZERO_MOD = @{thm "DIVISION_BY_ZERO"} RS conjunct2;


36 
val ZDIVISION_BY_ZERO_DIV = @{thm "DIVISION_BY_ZERO"} RS conjunct1;


37 


38 
(*


39 
val fn_rews = List.concat (map thms ["allpairs.simps","iupt.simps","decr.simps", "decrnum.simps","disjuncts.simps","simpnum.simps", "simpfm.simps","numadd.simps","nummul.simps","numneg_def","numsub","simp_num_pair_def","not.simps","prep.simps","qelim.simps","minusinf.simps","plusinf.simps","rsplit0.simps","rlfm.simps","\\<Upsilon>.simps","\\<upsilon>.simps","linrqe_def", "ferrack_def", "Let_def", "numsub_def", "numneg_def","DJ_def", "imp_def", "evaldjf_def", "djf_def", "split_def", "eq_def", "disj_def", "simp_num_pair_def", "conj_def", "lt_def", "neq_def","gt_def"]);


40 
*)


41 
fun prepare_for_linz 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, n1)


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) = nT)


57 
(term_frees fm' @ 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 (n1) th) RS spec ;


63 


64 
(* object implication to meta*)


65 
fun mp_step n th = if (n=0) then th else (mp_step (n1) th) RS mp;


66 


67 


68 
fun linz_tac ctxt q i = ObjectLogic.atomize_tac i THEN (fn st =>


69 
let


70 
val g = List.nth (prems_of st, i  1)


71 
val thy = ProofContext.theory_of ctxt


72 
(* Transform the term*)


73 
val (t,np,nh) = prepare_for_linz q g


74 
(* Some simpsets for dealing with mod div abs and nat*)


75 
val mod_div_simpset = HOL_basic_ss


76 
addsimps [refl,nat_mod_add_eq, nat_mod_add_left_eq,


77 
nat_mod_add_right_eq, int_mod_add_eq,


78 
int_mod_add_right_eq, int_mod_add_left_eq,


79 
nat_div_add_eq, int_div_add_eq,


80 
mod_self, @{thm "zmod_self"},


81 
DIVISION_BY_ZERO_MOD,DIVISION_BY_ZERO_DIV,


82 
ZDIVISION_BY_ZERO_MOD,ZDIVISION_BY_ZERO_DIV,


83 
@{thm "zdiv_zero"}, @{thm "zmod_zero"}, @{thm "div_0"}, @{thm "mod_0"},


84 
@{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"},


85 
Suc_plus1]


86 
addsimps add_ac


87 
addsimprocs [cancel_div_mod_proc]


88 
val simpset0 = HOL_basic_ss


89 
addsimps [mod_div_equality', Suc_plus1]


90 
addsimps comp_arith


91 
addsplits [split_zdiv, split_zmod, split_div', @{thm "split_min"}, @{thm "split_max"}]


92 
(* Simp rules for changing (n::int) to int n *)


93 
val simpset1 = HOL_basic_ss


94 
addsimps [nat_number_of_def, zdvd_int] @ map (fn r => r RS sym)


95 
[int_int_eq, zle_int, zless_int, zadd_int, zmult_int]


96 
addsplits [zdiff_int_split]


97 
(*simp rules for elimination of int n*)


98 


99 
val simpset2 = HOL_basic_ss


100 
addsimps [nat_0_le, all_nat, ex_nat, number_of1, number_of2, int_0, int_1]


101 
addcongs [conj_le_cong, imp_le_cong]


102 
(* simp rules for elimination of abs *)


103 
val simpset3 = HOL_basic_ss addsplits [abs_split]


104 
val ct = cterm_of thy (HOLogic.mk_Trueprop t)


105 
(* Theorem for the nat > int transformation *)


106 
val pre_thm = Seq.hd (EVERY


107 
[simp_tac mod_div_simpset 1, simp_tac simpset0 1,


108 
TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1),


109 
TRY (simp_tac simpset3 1), TRY (simp_tac cooper_ss 1)]


110 
(trivial ct))


111 
fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)


112 
(* The result of the quantifier elimination *)


113 
val (th, tac) = case (prop_of pre_thm) of


114 
Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>


115 
let val pth = linzqe_oracle thy (Pattern.eta_long [] t1)


116 
in


117 
((pth RS iffD2) RS pre_thm,


118 
assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))


119 
end


120 
 _ => (pre_thm, assm_tac i)


121 
in (rtac (((mp_step nh) o (spec_step np)) th) i


122 
THEN tac) st


123 
end handle Subscript => no_tac st);


124 


125 
fun linz_args meth =


126 
let val parse_flag =


127 
Args.$$$ "no_quantify" >> (K (K false));


128 
in


129 
Method.simple_args


130 
(Scan.optional (Args.$$$ "("  Scan.repeat1 parse_flag  Args.$$$ ")") [] >>


131 
curry (Library.foldl op >) true)


132 
(fn q => fn ctxt => meth ctxt q 1)


133 
end;


134 


135 
fun linz_method ctxt q i = Method.METHOD (fn facts =>


136 
Method.insert_tac facts 1 THEN linz_tac ctxt q i);


137 


138 
val setup =


139 
Method.add_method ("cooper",


140 
linz_args linz_method,


141 
"decision procedure for linear integer arithmetic");


142 


143 
end 