src/Provers/Arith/nat_transitive.ML
author wenzelm
Mon, 16 Nov 1998 13:54:35 +0100
changeset 5897 b3548f939dd2
parent 4293 66da34945f8b
permissions -rw-r--r--
removed genelim.ML;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4293
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
     1
(*  Title:      Provers/nat_transitive.ML
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
     3
    Author:     Tobias Nipkow
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
     4
    Copyright   1996  TU Munich
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
     5
*)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
     6
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
     7
(***
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
     8
A very simple package for inequalities over nat.
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
     9
It uses all premises of the form
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    10
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    11
t = u, t < u, t <= u, ~(t < u), ~(t <= u)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    12
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    13
where t and u must be of type nat, to
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    14
1. either derive a contradiction,
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    15
   in which case the conclusion can be any term,
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    16
2. or prove the conclusion, which must be of the same form as the premises.
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    17
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    18
The package
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    19
- does not deal with the relation ~=
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    20
- treats `pred', +, *, ... as atomic terms. Hence it can prove
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    21
  [| x < y+z; y+z < u |] ==> Suc x < u
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    22
  but not
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    23
  [| x < y+z; z < u |] ==> Suc x < y+u
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    24
- takes only (in)equalities which are atomic premises into account. It does
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    25
  not deal with logical operators like -->, & etc. Hence it cannot prove 
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    26
  [| x < y+z & y+z < u |] ==> Suc x < u
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    27
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    28
In order not to fall foul of the above limitations, the following hints are
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    29
useful:
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    30
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    31
1. You may need to run `by(safe_tac HOL_cs)' in order to bring out the atomic
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    32
   premises.
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    33
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    34
2. To get rid of ~= in the premises, it is advisable to use a rule like
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    35
   nat_neqE = "[| (m::nat) ~= n; m < n ==> P; n < m ==> P |] ==> P" : thm
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    36
   (the name nat_eqE is chosen in HOL), for example as follows:
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    37
   by(safe_tac (HOL_cs addSEs [nat_neqE])
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    38
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    39
3. To get rid of `pred', you may be able to do the following:
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    40
   expand `pred(m)' into `case m of 0 => 0 | Suc n => n' and use split_tac
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    41
   to turn the case-expressions into logical case distinctions. In HOL:
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    42
   simp_tac (... addsimps [pred_def] setloop (split_tac [expand_nat_case]))
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    43
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    44
The basic tactic is `trans_tac'. In order to use `trans_tac' as a solver in
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    45
the simplifier, `cut_trans_tac' is also provided, which cuts the given thms
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    46
in as facts.
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    47
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    48
Notes:
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    49
- It should easily be possible to adapt this package to other numeric types
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    50
  like int.
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    51
- There is ample scope for optimizations, which so far have not proved
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    52
  necessary.
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    53
- The code can be simplified by adding the negated conclusion to the
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    54
  premises to derive a contradiction. However, this would restrict the
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    55
  package to classical logics.
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    56
***)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    57
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    58
(* The package works for arbitrary logics.
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    59
   You just need to instantiate the following parameter structure.
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    60
*)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    61
signature LESS_ARITH =
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    62
sig
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    63
  val lessI:            thm (* n < Suc n *)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    64
  val zero_less_Suc:    thm (* 0 < Suc n *)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    65
  val less_reflE:       thm (* n < n ==> P *)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    66
  val less_zeroE:       thm (* n < 0 ==> P *)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    67
  val less_incr:        thm (* m < n ==> Suc m < Suc n *)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    68
  val less_decr:        thm (* Suc m < Suc n ==> m < n *)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    69
  val less_incr_rhs:    thm (* m < n ==> m < Suc n *)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    70
  val less_decr_lhs:    thm (* Suc m < n ==> m < n *)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    71
  val less_trans_Suc:   thm (* [| i < j; j < k |] ==> Suc i < k *)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    72
  val leD:              thm (* m <= n ==> m < Suc n *)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    73
  val not_lessD:        thm (* ~(m < n) ==> n < Suc m *)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    74
  val not_leD:          thm (* ~(m <= n) ==> n < m *)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    75
  val eqD1:             thm (* m = n ==> m < Suc n *)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    76
  val eqD2:             thm (* m = n ==> m < Suc n *)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    77
  val not_lessI:        thm (* n < Suc m ==> ~(m < n) *)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    78
  val leI:              thm (* m < Suc n ==> m <= n *)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    79
  val not_leI:          thm (* n < m ==> ~(m <= n) *)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    80
  val eqI:              thm (* [| m < Suc n; n < Suc m |] ==> n = m *)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    81
  val is_zero: term -> bool
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    82
  val decomp:  term -> (term * int * string * term * int)option
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    83
(* decomp(`Suc^i(x) Rel Suc^j(y)') should yield (x,i,Rel,y,j)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    84
   where Rel is one of "<", "~<", "<=", "~<=" and "=" *)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    85
end;
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    86
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    87
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    88
signature TRANS_TAC =
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    89
sig
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    90
  val trans_tac: int -> tactic
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    91
  val cut_trans_tac: thm list -> int -> tactic
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    92
end;
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    93
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    94
functor Trans_Tac_Fun(Less:LESS_ARITH):TRANS_TAC =
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    95
struct
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    96
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    97
datatype proof = Asm of int
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    98
               | Thm of proof list * thm
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
    99
               | Incr1 of proof * int (* Increment 1 side *)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   100
               | Incr2 of proof * int (* Increment 2 sides *);
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   101
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   102
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   103
(*** Turn proof objects into thms ***)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   104
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   105
fun incr2(th,i) = if i=0 then th else
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   106
                  if i>0 then incr2(th RS Less.less_incr,i-1)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   107
                  else incr2(th RS Less.less_decr,i+1);
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   108
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   109
fun incr1(th,i) = if i=0 then th else
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   110
                  if i>0 then incr1(th RS Less.less_incr_rhs,i-1)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   111
                  else incr1(th RS Less.less_decr_lhs,i+1);
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   112
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   113
fun prove asms =
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   114
  let fun pr(Asm i) = nth_elem(i,asms)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   115
        | pr(Thm(prfs,thm)) = (map pr prfs) MRS thm
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   116
        | pr(Incr1(p,i)) = incr1(pr p,i)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   117
        | pr(Incr2(p,i)) = incr2(pr p,i)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   118
  in pr end;
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   119
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   120
(*** Internal representation of inequalities
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   121
(x,i,y,j) means x+i < y+j.
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   122
Leads to simpler case distinctions than the normalized x < y+k
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   123
***)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   124
type less = term * int * term * int * proof;
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   125
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   126
(*** raised when contradiction is found ***)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   127
exception Contr of proof;
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   128
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   129
(*** raised when goal can't be proved ***)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   130
exception Cant;
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   131
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   132
infix subsumes;
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   133
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   134
fun (x,i,y,j:int,_) subsumes (x',i',y',j',_) =
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   135
  x=x' andalso y=y' andalso j-i<=j'-i';
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   136
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   137
fun trivial(x,i:int,y,j,_)  =  (x=y orelse Less.is_zero(x)) andalso i<j;
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   138
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   139
(*** transitive closure ***)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   140
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   141
(* Very naive: computes all consequences of a set of less-statements. *)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   142
(* In the worst case very expensive not just in time but also space *)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   143
(* Could easily be optimized but there are ususally only a few < asms *)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   144
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   145
fun add new =
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   146
  let fun adds([],news) = new::news
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   147
        | adds(old::olds,news) = if new subsumes old then adds(olds,news)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   148
                                 else adds(olds,old::news)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   149
  in adds end;
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   150
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   151
fun ctest(less as (x,i,y,j,p)) =
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   152
  if x=y andalso i>=j
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   153
  then raise Contr(Thm([Incr1(Incr2(p,~j),j-i)],Less.less_reflE)) else
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   154
  if Less.is_zero(y) andalso i>=j
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   155
  then raise Contr(Thm([Incr2(p,~j)],Less.less_zeroE))
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   156
  else less;
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   157
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   158
fun mktrans((x,i,_,j,p):less,(_,k,z,l,q)) =
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   159
  ctest(if j >= k
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   160
        then (x,i+1,z,l+(j-k),Thm([p,Incr2(q,j-k)],Less.less_trans_Suc))
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   161
        else (x,i+(k-j)+1,z,l,Thm([Incr2(p,k-j),q],Less.less_trans_Suc)));
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   162
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   163
fun trans (new as (x,i,y,j,p)) olds =
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   164
  let fun tr(news, old as (x1,i1,y1,j1,p1):less) =
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   165
           if y1=x then mktrans(old,new)::news else
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   166
           if x1=y then mktrans(new,old)::news else news
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   167
  in foldl tr ([],olds) end;
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   168
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   169
fun close1(olds: less list)(new:less):less list =
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   170
      if trivial new orelse exists (fn old => old subsumes new) olds then olds
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   171
      else let val news = trans new olds
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   172
           in  close (add new (olds,[])) news end
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   173
and close (olds: less list) ([]:less list) = olds
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   174
  | close olds ((new:less)::news) = close (close1 olds (ctest new)) news;
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   175
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   176
(*** end of transitive closure ***)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   177
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   178
(* recognize and solve trivial goal *)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   179
fun triv_sol(x,i,y,j,_) =
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   180
  if x=y andalso i<j
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   181
  then Some(Incr1(Incr2(Thm([],Less.lessI),i),j-i-1)) else
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   182
  if Less.is_zero(x) andalso i<j
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   183
  then Some(Incr1(Incr2(Thm([],Less.zero_less_Suc),i),j-i-1))
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   184
  else None;
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   185
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   186
(* solve less starting from facts *)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   187
fun solve facts (less as (x,i,y,j,_)) =
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   188
  case triv_sol less of
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   189
    None => (case find_first (fn fact => fact subsumes less) facts of
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   190
               None => raise Cant
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   191
             | Some(a,m,b,n,p) => Incr1(Incr2(p,j-n),n+i-m-j))
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   192
  | Some prf => prf;
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   193
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   194
(* turn term into a less-tuple *)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   195
fun mkasm(t,n) =
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   196
  case Less.decomp(t) of
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   197
    Some(x,i,rel,y,j) => (case rel of
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   198
      "<"   => [(x,i,y,j,Asm n)]
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   199
    | "~<"  => [(y,j,x,i+1,Thm([Asm n],Less.not_lessD))]
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   200
    | "<="  => [(x,i,y,j+1,Thm([Asm n],Less.leD))]
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   201
    | "~<=" => [(y,j,x,i,Thm([Asm n],Less.not_leD))]
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   202
    | "="   => [(x,i,y,j+1,Thm([Asm n],Less.eqD1)),
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   203
                (y,j,x,i+1,Thm([Asm n],Less.eqD2))]
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   204
    | "~="  => []
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   205
    | _     => error("trans_tac/decomp: unknown relation " ^ rel))
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   206
  | None => [];
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   207
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   208
(* mkconcl t returns a pair (goals,proof) where goals is a list of *)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   209
(* less-subgoals to solve, and proof the validation which proves the concl t *)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   210
(* from the subgoals. Asm ~1 is dummy *)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   211
fun mkconcl t =
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   212
  case Less.decomp(t) of
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   213
    Some(x,i,rel,y,j) => (case rel of
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   214
      "<"   => ([(x,i,y,j,Asm ~1)],Asm 0)
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   215
    | "~<"  => ([(y,j,x,i+1,Asm ~1)],Thm([Asm 0],Less.not_lessI))
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   216
    | "<="  => ([(x,i,y,j+1,Asm ~1)],Thm([Asm 0],Less.leI))
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   217
    | "~<=" => ([(y,j,x,i,Asm ~1)],Thm([Asm 0],Less.not_leI))
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   218
    | "="   => ([(x,i,y,j+1,Asm ~1),(y,j,x,i+1,Asm ~1)],
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   219
                Thm([Asm 0,Asm 1],Less.eqI))
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   220
    | "~="  => raise Cant
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   221
    | _     => error("trans_tac/decomp: unknown relation " ^ rel))
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   222
  | None => raise Cant;
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   223
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   224
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   225
val trans_tac = SUBGOAL (fn (A,n) =>
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   226
  let val Hs = Logic.strip_assums_hyp A
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   227
      val C = Logic.strip_assums_concl A
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   228
      val lesss = flat(ListPair.map mkasm (Hs, 0 upto (length Hs - 1)))
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   229
      val clesss = close [] lesss
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   230
      val (subgoals,prf) = mkconcl C
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   231
      val prfs = map (solve clesss) subgoals
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   232
  in METAHYPS (fn asms => let val thms = map (prove asms) prfs
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   233
                          in rtac (prove thms prf) 1 end) n
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   234
  end
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   235
  handle Contr(p) => METAHYPS (fn asms => rtac (prove asms p) 1) n
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   236
       | Cant => no_tac);
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   237
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   238
fun cut_trans_tac thms = cut_facts_tac thms THEN' trans_tac;
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   239
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   240
end;
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   241
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   242
(*** Tests
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   243
fun test s = prove_goal Nat.thy ("!!m::nat." ^ s) (fn _ => [trans_tac 1]);
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   244
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   245
test "[| i<j; j<=k; ~(l < Suc k); ~(m <= l) |] ==> Suc(Suc i) < m";
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   246
test "[| i<j; j<=k; ~(l < Suc k); ~(m <= l) |] ==> Suc(Suc(Suc i)) <= m";
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   247
test "[| i<j; j<=k; ~(l < Suc k); ~(m <= l) |] ==> ~ m <= Suc(Suc i)";
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   248
test "[| i<j; j<=k; ~(l < Suc k); ~(m <= l) |] ==> ~ m < Suc(Suc(Suc i))";
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   249
test "[| i<j; j<=k; ~(l < Suc k); ~(m <= l); m <= Suc(Suc(Suc i)) |] \
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   250
\     ==> m = Suc(Suc(Suc i))";
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   251
test "[| i<j; j<=k; ~(l < Suc k); ~(m <= l); m=n; n <= Suc(Suc(Suc i)) |] \
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   252
\     ==> m = Suc(Suc(Suc i))";
66da34945f8b moved to Arith/;
wenzelm
parents:
diff changeset
   253
***)