1 (* Title: HOL/Tools/Qelim/presburger.ML
2 Author: Amine Chaieb, TU Muenchen
7 val cooper_tac: bool -> thm list -> thm list -> Proof.context -> int -> tactic
10 structure Presburger : PRESBURGER =
14 val comp_ss = HOL_ss addsimps @{thms "Groebner_Basis.comp_arith"};
17 (case Thm.term_of ct of
18 Const ("op -->", _) $ _ $ _ =>
19 let val (A, B) = Thm.dest_binop ct
20 in A :: strip_objimp B end
25 Const ("All", _) $ Abs (xn,xT,p) =>
26 let val (a,(v,t')) = (apsnd (Thm.dest_abs (SOME xn)) o Thm.dest_comb) ct
27 in apfst (cons (a,v)) (strip_objall t')
33 HOL_basic_ss addsimps map (fn th => th RS sym) @{thms "all_simps"}
35 fun thin_prems_tac P = simp_tac all_maxscope_ss THEN'
36 CSUBGOAL (fn (p', i) =>
38 val (qvs, p) = strip_objall (Thm.dest_arg p')
39 val (ps, c) = split_last (strip_objimp p)
41 val q = if P c then c else @{cterm "False"}
42 val ng = fold_rev (fn (a,v) => fn t => Thm.capply a (Thm.cabs v t)) qvs
43 (fold_rev (fn p => fn q => Thm.capply (Thm.capply @{cterm "op -->"} p) q) qs q)
44 val g = Thm.capply (Thm.capply @{cterm "op ==>"} (Thm.capply @{cterm "Trueprop"} ng)) p'
45 val ntac = (case qs of [] => q aconvc @{cterm "False"}
49 else rtac (Goal.prove_internal [] g (K (blast_tac HOL_cs 1))) i
54 fun isnum t = case t of
55 Const(@{const_name Groups.zero},_) => true
56 | Const(@{const_name Groups.one},_) => true
57 | @{term "Suc"}$s => isnum s
58 | @{term "nat"}$s => isnum s
59 | @{term "int"}$s => isnum s
60 | Const(@{const_name Groups.uminus},_)$s => isnum s
61 | Const(@{const_name Groups.plus},_)$l$r => isnum l andalso isnum r
62 | Const(@{const_name Groups.times},_)$l$r => isnum l andalso isnum r
63 | Const(@{const_name Groups.minus},_)$l$r => isnum l andalso isnum r
64 | Const(@{const_name Power.power},_)$l$r => isnum l andalso isnum r
65 | Const(@{const_name Divides.mod},_)$l$r => isnum l andalso isnum r
66 | Const(@{const_name Divides.div},_)$l$r => isnum l andalso isnum r
67 | _ => can HOLogic.dest_number t orelse can HOLogic.dest_nat t
70 if not (typ_of (ctyp_of_term t) mem [HOLogic.intT, HOLogic.natT, HOLogic.boolT]) then false
71 else case term_of t of
72 c$l$r => if c mem [@{term"op *::int => _"}, @{term"op *::nat => _"}]
73 then not (isnum l orelse isnum r)
74 else not (member (op aconv) cts c)
75 | c$_ => not (member (op aconv) cts c)
76 | c => not (member (op aconv) cts c)
79 let fun h acc t = case t of
80 Const _ => insert (op aconv) t acc
81 | a$b => h (h acc a) b
82 | Abs (_,_,t) => h acc t
86 fun is_relevant ctxt ct =
87 subset (op aconv) (term_constants (term_of ct) , snd (CooperData.get ctxt))
88 andalso forall (fn Free (_,T) => T mem [@{typ "int"}, @{typ nat}]) (OldTerm.term_frees (term_of ct))
89 andalso forall (fn Var (_,T) => T mem [@{typ "int"}, @{typ nat}]) (OldTerm.term_vars (term_of ct));
91 fun int_nat_terms ctxt ct =
93 val cts = snd (CooperData.get ctxt)
94 fun h acc t = if ty cts t then insert (op aconvc) t acc else
96 _$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
97 | Abs(_,_,_) => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc))
102 fun generalize_tac f = CSUBGOAL (fn (p, i) => PRIMITIVE (fn st =>
104 fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
105 fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
106 val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
107 val p' = fold_rev gen ts p
108 in implies_intr p' (implies_elim st (fold forall_elim ts (assume p'))) end));
112 addsimps @{thms simp_thms} @ [@{thm "nat_number_of_def"}, @{thm "zdvd_int"}]
113 @ map (fn r => r RS sym)
114 [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "zless_int"}, @{thm "zadd_int"},
116 addsplits [@{thm "zdiff_int_split"}]
118 val ss2 = HOL_basic_ss
119 addsimps [@{thm "nat_0_le"}, @{thm "int_nat_number_of"},
120 @{thm "all_nat"}, @{thm "ex_nat"}, @{thm "number_of1"},
121 @{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_eq_plus1"}]
122 addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
123 val div_mod_ss = HOL_basic_ss addsimps @{thms simp_thms}
124 @ map (symmetric o mk_meta_eq)
125 [@{thm "dvd_eq_mod_eq_0"},
126 @{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"},
127 @{thm "mod_add_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
128 @ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "mod_by_0"},
129 @{thm "div_by_0"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1,
130 @{thm "DIVISION_BY_ZERO"} RS conjunct2, @{thm "zdiv_zero"}, @{thm "zmod_zero"},
131 @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"},
132 @{thm "mod_1"}, @{thm "Suc_eq_plus1"}]
134 addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
135 val splits_ss = comp_ss addsimps [@{thm "mod_div_equality'"}] addsplits
136 [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"},
137 @{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}]
139 fun nat_to_int_tac ctxt =
140 simp_tac (Simplifier.context ctxt ss1) THEN_ALL_NEW
141 simp_tac (Simplifier.context ctxt ss2) THEN_ALL_NEW
142 simp_tac (Simplifier.context ctxt comp_ss);
144 fun div_mod_tac ctxt i = simp_tac (Simplifier.context ctxt div_mod_ss) i;
145 fun splits_tac ctxt i = simp_tac (Simplifier.context ctxt splits_ss) i;
149 fun core_cooper_tac ctxt = CSUBGOAL (fn (p, i) =>
153 then linzqe_oracle (Thm.cterm_of (ProofContext.theory_of ctxt)
154 (Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p)))))
155 else arg_conv (Cooper.cooper_conv ctxt) p
156 val p' = Thm.rhs_of cpth
157 val th = implies_intr p' (equal_elim (symmetric cpth) (assume p'))
159 handle Cooper.COOPER _ => no_tac);
161 fun finish_tac q = SUBGOAL (fn (_, i) =>
162 (if q then I else TRY) (rtac TrueI i));
164 fun cooper_tac elim add_ths del_ths ctxt =
165 let val ss = Simplifier.context ctxt (fst (CooperData.get ctxt)) delsimps del_ths addsimps add_ths
166 val aprems = Arith_Data.get_arith_facts ctxt
168 Method.insert_tac aprems
169 THEN_ALL_NEW Object_Logic.full_atomize_tac
170 THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
171 THEN_ALL_NEW simp_tac ss
172 THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
173 THEN_ALL_NEW Object_Logic.full_atomize_tac
174 THEN_ALL_NEW (thin_prems_tac (is_relevant ctxt))
175 THEN_ALL_NEW Object_Logic.full_atomize_tac
176 THEN_ALL_NEW div_mod_tac ctxt
177 THEN_ALL_NEW splits_tac ctxt
178 THEN_ALL_NEW simp_tac ss
179 THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
180 THEN_ALL_NEW nat_to_int_tac ctxt
181 THEN_ALL_NEW (core_cooper_tac ctxt)
182 THEN_ALL_NEW finish_tac elim