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;