src/Provers/linorder.ML
changeset 14398 c5c47703f763
parent 14397 b3b15305a1c9
child 14399 dc677b35e54f
     1.1 --- a/src/Provers/linorder.ML	Thu Feb 19 10:41:32 2004 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,214 +0,0 @@
     1.4 -(*
     1.5 -  Title:	Transitivity reasoner for linear orders
     1.6 -  Id:		$Id$
     1.7 -  Author:	Clemens Ballarin, started 8 November 2002
     1.8 -  Copyright:	TU Muenchen
     1.9 -*)
    1.10 -
    1.11 -(***
    1.12 -This is a very simple package for transitivity reasoning over linear orders.
    1.13 -Simple means exponential time (and space) in the number of premises.
    1.14 -Should be replaced by a graph-theoretic algorithm.
    1.15 -
    1.16 -The package provides a tactic trans_tac that uses all premises of the form
    1.17 -
    1.18 -  t = u, t < u, t <= u, ~(t < u) and ~(t <= u)
    1.19 -
    1.20 -to
    1.21 -1. either derive a contradiction,
    1.22 -   in which case the conclusion can be any term,
    1.23 -2. or prove the conclusion, which must be of the same form as the premises.
    1.24 -
    1.25 -To get rid of ~= in the premises, it is advisable to use an elimination
    1.26 -rule of the form
    1.27 -
    1.28 -  [| t ~= u; t < u ==> P; u < t ==> P |] ==> P.
    1.29 -
    1.30 -The package is implemented as an ML functor and thus not limited to the
    1.31 -relation <= and friends.  It can be instantiated to any total order ---
    1.32 -for example, the divisibility relation "dvd".
    1.33 -***)
    1.34 -
    1.35 -(*** Credits ***
    1.36 -
    1.37 -This package is closely based on a (no longer used) transitivity reasoner for
    1.38 -the natural numbers, which was written by Tobias Nipkow.
    1.39 -
    1.40 -****************)
    1.41 -
    1.42 -signature LESS_ARITH =
    1.43 -sig
    1.44 -  val less_reflE: thm  (* x < x ==> P *)
    1.45 -  val le_refl: thm  (* x <= x *)
    1.46 -  val less_imp_le: thm (* x < y ==> x <= y *)
    1.47 -  val not_lessI: thm (* y <= x  ==> ~(x < y) *)
    1.48 -  val not_leI: thm (* y < x  ==> ~(x <= y) *)
    1.49 -  val not_lessD: thm (* ~(x < y) ==> y <= x *)
    1.50 -  val not_leD: thm (* ~(x <= y) ==> y < x *)
    1.51 -  val eqI: thm (* [| x <= y; y <= x |] ==> x = y *)
    1.52 -  val eqD1: thm (* x = y ==> x <= y *)
    1.53 -  val eqD2: thm (* x = y ==> y <= x *)
    1.54 -  val less_trans: thm  (* [| x <= y; y <= z |] ==> x <= z *)
    1.55 -  val less_le_trans: thm  (* [| x <= y; y < z |] ==> x < z *)
    1.56 -  val le_less_trans: thm  (* [| x < y; y <= z |] ==> x < z *)
    1.57 -  val le_trans: thm  (* [| x < y; y < z |] ==> x < z *)
    1.58 -  val decomp: term -> (term * string * term) option
    1.59 -    (* decomp (`x Rel y') should yield (x, Rel, y)
    1.60 -       where Rel is one of "<", "<=", "~<", "~<=", "=" and "~="
    1.61 -       other relation symbols are ignored *)
    1.62 -end;
    1.63 -
    1.64 -signature TRANS_TAC =
    1.65 -sig
    1.66 -  val trans_tac: int -> tactic
    1.67 -end;
    1.68 -
    1.69 -functor Trans_Tac_Fun (Less: LESS_ARITH): TRANS_TAC =
    1.70 -struct
    1.71 -
    1.72 -(*** Proof objects ***)
    1.73 -
    1.74 -datatype proof
    1.75 -  = Asm of int
    1.76 -  | Thm of proof list * thm;
    1.77 -
    1.78 -(* Turn proof objects into theorems *)
    1.79 -
    1.80 -fun prove asms =
    1.81 -  let fun pr (Asm i) = nth_elem (i, asms)
    1.82 -        | pr (Thm (prfs, thm)) = (map pr prfs) MRS thm
    1.83 -  in pr end;
    1.84 -
    1.85 -(*** Exceptions ***)
    1.86 -
    1.87 -exception Contr of proof;  (* Raised when contradiction is found *)
    1.88 -
    1.89 -exception Cannot;  (* Raised when goal cannot be proved *)
    1.90 -
    1.91 -(*** Internal representation of inequalities ***)
    1.92 -
    1.93 -datatype less
    1.94 -  = Less of term * term * proof
    1.95 -  | Le of term * term * proof;
    1.96 -
    1.97 -fun lower (Less (x, _, _)) = x
    1.98 -  | lower (Le (x, _, _)) = x;
    1.99 -
   1.100 -fun upper (Less (_, y, _)) = y
   1.101 -  | upper (Le (_, y, _)) = y;
   1.102 -
   1.103 -infix subsumes;
   1.104 -
   1.105 -fun (Less (x, y, _)) subsumes (Le (x', y', _)) = (x = x' andalso y = y')
   1.106 -  | (Less (x, y, _)) subsumes (Less (x', y', _)) = (x = x' andalso y = y')
   1.107 -  | (Le (x, y, _)) subsumes (Le (x', y', _)) = (x = x' andalso y = y')
   1.108 -  | _ subsumes _ = false;
   1.109 -
   1.110 -fun trivial (Le (x, x', _)) = (x = x')
   1.111 -  | trivial _ = false;
   1.112 -
   1.113 -(*** Transitive closure ***)
   1.114 -
   1.115 -fun add new =
   1.116 -  let fun adds([], news) = new::news
   1.117 -        | adds(old::olds, news) = if new subsumes old then adds(olds, news)
   1.118 -                                  else adds(olds, old::news)
   1.119 -  in adds end;
   1.120 -
   1.121 -fun ctest (less as Less (x, x', p)) = 
   1.122 -    if x = x' then raise Contr (Thm ([p], Less.less_reflE))
   1.123 -    else less
   1.124 -  | ctest less = less;
   1.125 -
   1.126 -fun mktrans (Less (x, _, p), Less (_, z, q)) =
   1.127 -    Less (x, z, Thm([p, q], Less.less_trans))
   1.128 -  | mktrans (Less (x, _, p), Le (_, z, q)) =
   1.129 -    Less (x, z, Thm([p, q], Less.less_le_trans))
   1.130 -  | mktrans (Le (x, _, p), Less (_, z, q)) =
   1.131 -    Less (x, z, Thm([p, q], Less.le_less_trans))
   1.132 -  | mktrans (Le (x, _, p), Le (_, z, q)) =
   1.133 -    Le (x, z, Thm([p, q], Less.le_trans));
   1.134 -
   1.135 -fun trans new olds =
   1.136 -  let fun tr (news, old) =
   1.137 -            if upper old = lower new then mktrans (old, new)::news
   1.138 -            else if upper new = lower old then mktrans (new, old)::news
   1.139 -            else news
   1.140 -  in foldl tr ([], olds) end;
   1.141 -
   1.142 -fun close1 olds new =
   1.143 -    if trivial new orelse exists (fn old => old subsumes new) olds then olds
   1.144 -    else let val news = trans new olds
   1.145 -         in close (add new (olds, [])) news end
   1.146 -and close olds [] = olds
   1.147 -  | close olds (new::news) = close (close1 olds (ctest new)) news;
   1.148 -
   1.149 -(*** Solving and proving goals ***)
   1.150 -
   1.151 -(* Recognise and solve trivial goal *)
   1.152 -
   1.153 -fun triv_sol (Le (x, x',  _)) = 
   1.154 -    if x = x' then Some (Thm ([], Less.le_refl)) 
   1.155 -    else None
   1.156 -  | triv_sol _ = None;
   1.157 -
   1.158 -(* Solve less starting from facts *)
   1.159 -
   1.160 -fun solve facts less =
   1.161 -  case triv_sol less of
   1.162 -    None => (case (Library.find_first (fn fact => fact subsumes less) facts, less) of
   1.163 -	(None, _) => raise Cannot
   1.164 -      | (Some (Less (_, _, p)), Less _) => p
   1.165 -      | (Some (Le (_, _, p)), Less _) =>
   1.166 -	   error "trans_tac/solve: internal error: le cannot subsume less"
   1.167 -      | (Some (Less (_, _, p)), Le _) => Thm ([p], Less.less_imp_le)
   1.168 -      | (Some (Le (_, _, p)), Le _) => p)
   1.169 -  | Some prf => prf;
   1.170 -
   1.171 -(* Turn term t into Less or Le; n is position of t in list of assumptions *)
   1.172 -
   1.173 -fun mkasm (t, n) =
   1.174 -  case Less.decomp t of
   1.175 -    Some (x, rel, y) => (case rel of
   1.176 -      "<"   => [Less (x, y, Asm n)]
   1.177 -    | "~<"  => [Le (y, x, Thm ([Asm n], Less.not_lessD))]
   1.178 -    | "<="  => [Le (x, y, Asm n)]
   1.179 -    | "~<=" => [Less (y, x, Thm ([Asm n], Less.not_leD))]
   1.180 -    | "="   => [Le (x, y, Thm ([Asm n], Less.eqD1)),
   1.181 -                Le (x, y, Thm ([Asm n], Less.eqD1))]
   1.182 -    | "~="  => []
   1.183 -    | _     => error ("trans_tac/mkasm: unknown relation " ^ rel))
   1.184 -  | None => [];
   1.185 -
   1.186 -(* Turn goal t into a pair (goals, proof) where goals is a list of
   1.187 -   Le/Less-subgoals to solve, and proof the validation that proves the concl t
   1.188 -   Asm ~1 is dummy (denotes a goal)
   1.189 -*)
   1.190 -
   1.191 -fun mkconcl t =
   1.192 -  case Less.decomp t of
   1.193 -    Some (x, rel, y) => (case rel of
   1.194 -      "<"   => ([Less (x, y, Asm ~1)], Asm 0)
   1.195 -    | "~<"  => ([Le (y, x, Asm ~1)], Thm ([Asm 0], Less.not_lessI))
   1.196 -    | "<="  => ([Le (x, y, Asm ~1)], Asm 0)
   1.197 -    | "~<=" => ([Less (y, x, Asm ~1)], Thm ([Asm 0], Less.not_leI))
   1.198 -    | "="   => ([Le (x, y, Asm ~1), Le (y, x, Asm ~1)],
   1.199 -                 Thm ([Asm 0, Asm 1], Less.eqI))
   1.200 -    | _  => raise Cannot)
   1.201 -  | None => raise Cannot;
   1.202 -
   1.203 -val trans_tac = SUBGOAL (fn (A, n) =>
   1.204 -  let val Hs = Logic.strip_assums_hyp A
   1.205 -    val C = Logic.strip_assums_concl A
   1.206 -    val lesss = flat (ListPair.map mkasm (Hs, 0 upto (length Hs - 1)))
   1.207 -    val clesss = close [] lesss
   1.208 -    val (subgoals, prf) = mkconcl C
   1.209 -    val prfs = map (solve clesss) subgoals
   1.210 -  in METAHYPS (fn asms =>
   1.211 -    let val thms = map (prove asms) prfs
   1.212 -    in rtac (prove thms prf) 1 end) n
   1.213 -  end
   1.214 -  handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n
   1.215 -       | Cannot => no_tac);
   1.216 -
   1.217 -end;