2114

1 
(* Title: Provers/nat_transitive.ML


2 
ID: $Id$


3 
Author: Tobias Nipkow


4 
Copyright 1996 TU Munich


5 
*)


6 


7 
(***


8 
A very simple package for inequalities over nat.


9 
It uses all premises of the form


10 


11 
t = u, t < u, t <= u, ~(t < u), ~(t <= u)


12 


13 
where t and u must be of type nat, to

2273

14 
1. either derive a contradiction,

2114

15 
in which case the conclusion can be any term,


16 
2. or prove the conclusion, which must be of the same form as the premises.


17 


18 
The package


19 
 does not deal with the relation ~=


20 
 treats `pred', +, *, ... as atomic terms. Hence it can prove


21 
[ x < y+z; y+z < u ] ==> Suc x < u


22 
but not


23 
[ x < y+z; z < u ] ==> Suc x < y+u


24 
 takes only (in)equalities which are atomic premises into account. It does


25 
not deal with logical operators like >, & etc. Hence it cannot prove


26 
[ x < y+z & y+z < u ] ==> Suc x < u


27 


28 
In order not to fall foul of the above limitations, the following hints are


29 
useful:


30 


31 
1. You may need to run `by(safe_tac HOL_cs)' in order to bring out the atomic


32 
premises.


33 


34 
2. To get rid of ~= in the premises, it is advisable to use a rule like


35 
nat_neqE = "[ (m::nat) ~= n; m < n ==> P; n < m ==> P ] ==> P" : thm


36 
(the name nat_eqE is chosen in HOL), for example as follows:


37 
by(safe_tac (HOL_cs addSEs [nat_neqE])


38 


39 
3. To get rid of `pred', you may be able to do the following:


40 
expand `pred(m)' into `case m of 0 => 0  Suc n => n' and use split_tac


41 
to turn the caseexpressions into logical case distinctions. In HOL:


42 
simp_tac (... addsimps [pred_def] setloop (split_tac [expand_nat_case]))


43 


44 
The basic tactic is `trans_tac'. In order to use `trans_tac' as a solver in


45 
the simplifier, `cut_trans_tac' is also provided, which cuts the given thms


46 
in as facts.


47 


48 
Notes:


49 
 It should easily be possible to adapt this package to other numeric types


50 
like int.


51 
 There is ample scope for optimizations, which so far have not proved


52 
necessary.


53 
 The code can be simplified by adding the negated conclusion to the


54 
premises to derive a contradiction. However, this would restrict the


55 
package to classical logics.


56 
***)


57 


58 
(* The package works for arbitrary logics.


59 
You just need to instantiate the following parameter structure.


60 
*)


61 
signature LESS_ARITH =


62 
sig


63 
val lessI: thm (* n < Suc n *)


64 
val zero_less_Suc: thm (* 0 < Suc n *)


65 
val less_reflE: thm (* n < n ==> P *)


66 
val less_zeroE: thm (* n < 0 ==> P *)


67 
val less_incr: thm (* m < n ==> Suc m < Suc n *)


68 
val less_decr: thm (* Suc m < Suc n ==> m < n *)


69 
val less_incr_rhs: thm (* m < n ==> m < Suc n *)


70 
val less_decr_lhs: thm (* Suc m < n ==> m < n *)


71 
val less_trans_Suc: thm (* [ i < j; j < k ] ==> Suc i < k *)


72 
val leD: thm (* m <= n ==> m < Suc n *)


73 
val not_lessD: thm (* ~(m < n) ==> n < Suc m *)


74 
val not_leD: thm (* ~(m <= n) ==> n < m *)


75 
val eqD1: thm (* m = n ==> m < Suc n *)


76 
val eqD2: thm (* m = n ==> m < Suc n *)


77 
val not_lessI: thm (* n < Suc m ==> ~(m < n) *)


78 
val leI: thm (* m < Suc n ==> m <= n *)


79 
val not_leI: thm (* n < m ==> ~(m <= n) *)


80 
val eqI: thm (* [ m < Suc n; n < Suc m ] ==> n = m *)


81 
val is_zero: term > bool


82 
val decomp: term > (term * int * string * term * int)option


83 
(* decomp(`Suc^i(x) Rel Suc^j(y)') should yield (x,i,Rel,y,j)


84 
where Rel is one of "<", "~<", "<=", "~<=" and "=" *)


85 
end;


86 


87 


88 
signature TRANS_TAC =


89 
sig


90 
val trans_tac: int > tactic


91 
val cut_trans_tac: thm list > int > tactic


92 
end;


93 


94 
functor Trans_Tac_Fun(Less:LESS_ARITH):TRANS_TAC =


95 
struct


96 


97 
datatype proof = Asm of int


98 
 Thm of proof list * thm


99 
 Incr1 of proof * int (* Increment 1 side *)


100 
 Incr2 of proof * int (* Increment 2 sides *);


101 


102 


103 
(*** Turn proof objects into thms ***)


104 


105 
fun incr2(th,i) = if i=0 then th else


106 
if i>0 then incr2(th RS Less.less_incr,i1)


107 
else incr2(th RS Less.less_decr,i+1);


108 


109 
fun incr1(th,i) = if i=0 then th else


110 
if i>0 then incr1(th RS Less.less_incr_rhs,i1)


111 
else incr1(th RS Less.less_decr_lhs,i+1);


112 


113 
fun prove asms =


114 
let fun pr(Asm i) = nth_elem(i,asms)


115 
 pr(Thm(prfs,thm)) = (map pr prfs) MRS thm


116 
 pr(Incr1(p,i)) = incr1(pr p,i)


117 
 pr(Incr2(p,i)) = incr2(pr p,i)


118 
in pr end;


119 


120 
(*** Internal representation of inequalities


121 
(x,i,y,j) means x+i < y+j.


122 
Leads to simpler case distinctions than the normalized x < y+k


123 
***)


124 
type less = term * int * term * int * proof;


125 


126 
(*** raised when contradiction is found ***)


127 
exception Contr of proof;


128 


129 
(*** raised when goal can't be proved ***)


130 
exception Cant;


131 


132 
infix subsumes;


133 


134 
fun (x,i,y,j:int,_) subsumes (x',i',y',j',_) =


135 
x=x' andalso y=y' andalso ji<=j'i';


136 


137 
fun trivial(x,i:int,y,j,_) = (x=y orelse Less.is_zero(x)) andalso i<j;


138 


139 
(*** transitive closure ***)


140 


141 
(* Very naive: computes all consequences of a set of lessstatements. *)


142 
(* In the worst case very expensive not just in time but also space *)


143 
(* Could easily be optimized but there are ususally only a few < asms *)


144 


145 
fun add new =


146 
let fun adds([],news) = new::news


147 
 adds(old::olds,news) = if new subsumes old then adds(olds,news)


148 
else adds(olds,old::news)


149 
in adds end;


150 


151 
fun ctest(less as (x,i,y,j,p)) =


152 
if x=y andalso i>=j


153 
then raise Contr(Thm([Incr1(Incr2(p,~j),ji)],Less.less_reflE)) else


154 
if Less.is_zero(y) andalso i>=j


155 
then raise Contr(Thm([Incr2(p,~j)],Less.less_zeroE))


156 
else less;


157 


158 
fun mktrans((x,i,_,j,p):less,(_,k,z,l,q)) =


159 
ctest(if j >= k


160 
then (x,i+1,z,l+(jk),Thm([p,Incr2(q,jk)],Less.less_trans_Suc))


161 
else (x,i+(kj)+1,z,l,Thm([Incr2(p,kj),q],Less.less_trans_Suc)));


162 


163 
fun trans (new as (x,i,y,j,p)) olds =


164 
let fun tr(news, old as (x1,i1,y1,j1,p1):less) =


165 
if y1=x then mktrans(old,new)::news else


166 
if x1=y then mktrans(new,old)::news else news


167 
in foldl tr ([],olds) end;


168 


169 
fun close1(olds: less list)(new:less):less list =


170 
if trivial new orelse exists (fn old => old subsumes new) olds then olds


171 
else let val news = trans new olds


172 
in close (add new (olds,[])) news end


173 
and close (olds: less list) ([]:less list) = olds


174 
 close olds ((new:less)::news) = close (close1 olds (ctest new)) news;


175 


176 
(*** end of transitive closure ***)


177 


178 
(* recognize and solve trivial goal *)


179 
fun triv_sol(x,i,y,j,_) =


180 
if x=y andalso i<j

2920

181 
then Some(Incr1(Incr2(Thm([],Less.lessI),i),ji1)) else

2114

182 
if Less.is_zero(x) andalso i<j


183 
then Some(Incr1(Incr2(Thm([],Less.zero_less_Suc),i),ji1))


184 
else None;


185 


186 
(* solve less starting from facts *)


187 
fun solve facts (less as (x,i,y,j,_)) =


188 
case triv_sol less of


189 
None => (case find_first (fn fact => fact subsumes less) facts of


190 
None => raise Cant


191 
 Some(a,m,b,n,p) => Incr1(Incr2(p,jn),n+imj))


192 
 Some prf => prf;


193 


194 
(* turn term into a lesstuple *)


195 
fun mkasm(t,n) =


196 
case Less.decomp(t) of


197 
Some(x,i,rel,y,j) => (case rel of


198 
"<" => [(x,i,y,j,Asm n)]


199 
 "~<" => [(y,j,x,i+1,Thm([Asm n],Less.not_lessD))]


200 
 "<=" => [(x,i,y,j+1,Thm([Asm n],Less.leD))]


201 
 "~<=" => [(y,j,x,i,Thm([Asm n],Less.not_leD))]


202 
 "=" => [(x,i,y,j+1,Thm([Asm n],Less.eqD1)),


203 
(y,j,x,i+1,Thm([Asm n],Less.eqD2))]


204 
 "~=" => []


205 
 _ => error("trans_tac/decomp: unknown relation " ^ rel))


206 
 None => [];


207 


208 
(* mkconcl t returns a pair (goals,proof) where goals is a list of *)


209 
(* lesssubgoals to solve, and proof the validation which proves the concl t *)


210 
(* from the subgoals. Asm ~1 is dummy *)


211 
fun mkconcl t =


212 
case Less.decomp(t) of


213 
Some(x,i,rel,y,j) => (case rel of


214 
"<" => ([(x,i,y,j,Asm ~1)],Asm 0)


215 
 "~<" => ([(y,j,x,i+1,Asm ~1)],Thm([Asm 0],Less.not_lessI))


216 
 "<=" => ([(x,i,y,j+1,Asm ~1)],Thm([Asm 0],Less.leI))


217 
 "~<=" => ([(y,j,x,i,Asm ~1)],Thm([Asm 0],Less.not_leI))


218 
 "=" => ([(x,i,y,j+1,Asm ~1),(y,j,x,i+1,Asm ~1)],


219 
Thm([Asm 0,Asm 1],Less.eqI))


220 
 "~=" => raise Cant


221 
 _ => error("trans_tac/decomp: unknown relation " ^ rel))


222 
 None => raise Cant;


223 


224 


225 
val trans_tac = SUBGOAL (fn (A,n) =>


226 
let val Hs = Logic.strip_assums_hyp A


227 
val C = Logic.strip_assums_concl A

2273

228 
val lesss = flat(ListPair.map mkasm (Hs, 0 upto (length Hs  1)))

2114

229 
val clesss = close [] lesss


230 
val (subgoals,prf) = mkconcl C


231 
val prfs = map (solve clesss) subgoals


232 
in METAHYPS (fn asms => let val thms = map (prove asms) prfs


233 
in rtac (prove thms prf) 1 end) n


234 
end


235 
handle Contr(p) => METAHYPS (fn asms => rtac (prove asms p) 1) n


236 
 Cant => no_tac);


237 


238 
fun cut_trans_tac thms = cut_facts_tac thms THEN' trans_tac;


239 


240 
end;


241 


242 
(*** Tests


243 
fun test s = prove_goal Nat.thy ("!!m::nat." ^ s) (fn _ => [trans_tac 1]);


244 


245 
test "[ i<j; j<=k; ~(l < Suc k); ~(m <= l) ] ==> Suc(Suc i) < m";


246 
test "[ i<j; j<=k; ~(l < Suc k); ~(m <= l) ] ==> Suc(Suc(Suc i)) <= m";


247 
test "[ i<j; j<=k; ~(l < Suc k); ~(m <= l) ] ==> ~ m <= Suc(Suc i)";


248 
test "[ i<j; j<=k; ~(l < Suc k); ~(m <= l) ] ==> ~ m < Suc(Suc(Suc i))";


249 
test "[ i<j; j<=k; ~(l < Suc k); ~(m <= l); m <= Suc(Suc(Suc i)) ] \


250 
\ ==> m = Suc(Suc(Suc i))";


251 
test "[ i<j; j<=k; ~(l < Suc k); ~(m <= l); m=n; n <= Suc(Suc(Suc i)) ] \


252 
\ ==> m = Suc(Suc(Suc i))";


253 
***)
