1(* Title: Provers/order.ML 2 Author: Oliver Kutter, TU Muenchen 3 4Transitivity reasoner for partial and linear orders. 5*) 6 7(* TODO: reduce number of input thms *) 8 9(* 10 11The package provides tactics partial_tac and linear_tac that use all 12premises of the form 13 14 t = u, t ~= u, t < u, t <= u, ~(t < u) and ~(t <= u) 15 16to 171. either derive a contradiction, 18 in which case the conclusion can be any term, 192. or prove the conclusion, which must be of the same form as the 20 premises (excluding ~(t < u) and ~(t <= u) for partial orders) 21 22The package is not limited to the relation <= and friends. It can be 23instantiated to any partial and/or linear order --- for example, the 24divisibility relation "dvd". In order to instantiate the package for 25a partial order only, supply dummy theorems to the rules for linear 26orders, and don't use linear_tac! 27 28*) 29 30signature ORDER_TAC = 31sig 32 (* Theorems required by the reasoner *) 33 type less_arith 34 val empty : thm -> less_arith 35 val update : string -> thm -> less_arith -> less_arith 36 37 (* Tactics *) 38 val partial_tac: 39 (theory -> term -> (term * string * term) option) -> less_arith -> 40 Proof.context -> thm list -> int -> tactic 41 val linear_tac: 42 (theory -> term -> (term * string * term) option) -> less_arith -> 43 Proof.context -> thm list -> int -> tactic 44end; 45 46structure Order_Tac: ORDER_TAC = 47struct 48 49(* Record to handle input theorems in a convenient way. *) 50 51type less_arith = 52 { 53 (* Theorems for partial orders *) 54 less_reflE: thm, (* x < x ==> P *) 55 le_refl: thm, (* x <= x *) 56 less_imp_le: thm, (* x < y ==> x <= y *) 57 eqI: thm, (* [| x <= y; y <= x |] ==> x = y *) 58 eqD1: thm, (* x = y ==> x <= y *) 59 eqD2: thm, (* x = y ==> y <= x *) 60 less_trans: thm, (* [| x < y; y < z |] ==> x < z *) 61 less_le_trans: thm, (* [| x < y; y <= z |] ==> x < z *) 62 le_less_trans: thm, (* [| x <= y; y < z |] ==> x < z *) 63 le_trans: thm, (* [| x <= y; y <= z |] ==> x <= z *) 64 le_neq_trans : thm, (* [| x <= y ; x ~= y |] ==> x < y *) 65 neq_le_trans : thm, (* [| x ~= y ; x <= y |] ==> x < y *) 66 not_sym : thm, (* x ~= y ==> y ~= x *) 67 68 (* Additional theorems for linear orders *) 69 not_lessD: thm, (* ~(x < y) ==> y <= x *) 70 not_leD: thm, (* ~(x <= y) ==> y < x *) 71 not_lessI: thm, (* y <= x ==> ~(x < y) *) 72 not_leI: thm, (* y < x ==> ~(x <= y) *) 73 74 (* Additional theorems for subgoals of form x ~= y *) 75 less_imp_neq : thm, (* x < y ==> x ~= y *) 76 eq_neq_eq_imp_neq : thm (* [| x = u ; u ~= v ; v = z|] ==> x ~= z *) 77 } 78 79fun empty dummy_thm = 80 {less_reflE= dummy_thm, le_refl= dummy_thm, less_imp_le= dummy_thm, eqI= dummy_thm, 81 eqD1= dummy_thm, eqD2= dummy_thm, 82 less_trans= dummy_thm, less_le_trans= dummy_thm, le_less_trans= dummy_thm, 83 le_trans= dummy_thm, le_neq_trans = dummy_thm, neq_le_trans = dummy_thm, 84 not_sym = dummy_thm, 85 not_lessD= dummy_thm, not_leD= dummy_thm, not_lessI= dummy_thm, not_leI= dummy_thm, 86 less_imp_neq = dummy_thm, eq_neq_eq_imp_neq = dummy_thm} 87 88fun change thms f = 89 let 90 val {less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 91 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 92 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 93 eq_neq_eq_imp_neq} = thms; 94 val (less_reflE', le_refl', less_imp_le', eqI', eqD1', eqD2', less_trans', 95 less_le_trans', le_less_trans', le_trans', le_neq_trans', neq_le_trans', 96 not_sym', not_lessD', not_leD', not_lessI', not_leI', less_imp_neq', 97 eq_neq_eq_imp_neq') = 98 f (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 99 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 100 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 101 eq_neq_eq_imp_neq) 102 in {less_reflE = less_reflE', le_refl= le_refl', 103 less_imp_le = less_imp_le', eqI = eqI', eqD1 = eqD1', eqD2 = eqD2', 104 less_trans = less_trans', less_le_trans = less_le_trans', 105 le_less_trans = le_less_trans', le_trans = le_trans', le_neq_trans = le_neq_trans', 106 neq_le_trans = neq_le_trans', not_sym = not_sym', 107 not_lessD = not_lessD', not_leD = not_leD', not_lessI = not_lessI', 108 not_leI = not_leI', 109 less_imp_neq = less_imp_neq', eq_neq_eq_imp_neq = eq_neq_eq_imp_neq'} 110 end; 111 112fun update "less_reflE" thm thms = 113 change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 114 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 115 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 116 eq_neq_eq_imp_neq) => 117 (thm, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 118 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 119 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) 120 | update "le_refl" thm thms = 121 change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 122 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 123 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 124 eq_neq_eq_imp_neq) => 125 (less_reflE, thm, less_imp_le, eqI, eqD1, eqD2, less_trans, 126 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 127 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) 128 | update "less_imp_le" thm thms = 129 change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 130 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 131 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 132 eq_neq_eq_imp_neq) => 133 (less_reflE, le_refl, thm, eqI, eqD1, eqD2, less_trans, 134 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 135 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) 136 | update "eqI" thm thms = 137 change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 138 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 139 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 140 eq_neq_eq_imp_neq) => 141 (less_reflE, le_refl, less_imp_le, thm, eqD1, eqD2, less_trans, 142 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 143 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) 144 | update "eqD1" thm thms = 145 change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 146 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 147 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 148 eq_neq_eq_imp_neq) => 149 (less_reflE, le_refl, less_imp_le, eqI, thm, eqD2, less_trans, 150 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 151 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) 152 | update "eqD2" thm thms = 153 change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 154 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 155 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 156 eq_neq_eq_imp_neq) => 157 (less_reflE, le_refl, less_imp_le, eqI, eqD1, thm, less_trans, 158 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 159 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) 160 | update "less_trans" thm thms = 161 change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 162 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 163 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 164 eq_neq_eq_imp_neq) => 165 (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, thm, 166 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 167 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) 168 | update "less_le_trans" thm thms = 169 change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 170 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 171 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 172 eq_neq_eq_imp_neq) => 173 (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 174 thm, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 175 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) 176 | update "le_less_trans" thm thms = 177 change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 178 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 179 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 180 eq_neq_eq_imp_neq) => 181 (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 182 less_le_trans, thm, le_trans, le_neq_trans, neq_le_trans, 183 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) 184 | update "le_trans" thm thms = 185 change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 186 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 187 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 188 eq_neq_eq_imp_neq) => 189 (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 190 less_le_trans, le_less_trans, thm, le_neq_trans, neq_le_trans, 191 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) 192 | update "le_neq_trans" thm thms = 193 change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 194 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 195 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 196 eq_neq_eq_imp_neq) => 197 (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 198 less_le_trans, le_less_trans, le_trans, thm, neq_le_trans, 199 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) 200 | update "neq_le_trans" thm thms = 201 change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 202 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 203 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 204 eq_neq_eq_imp_neq) => 205 (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 206 less_le_trans, le_less_trans, le_trans, le_neq_trans, thm, 207 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) 208 | update "not_sym" thm thms = 209 change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 210 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 211 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 212 eq_neq_eq_imp_neq) => 213 (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 214 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 215 thm, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) 216 | update "not_lessD" thm thms = 217 change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 218 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 219 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 220 eq_neq_eq_imp_neq) => 221 (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 222 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 223 not_sym, thm, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) 224 | update "not_leD" thm thms = 225 change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 226 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 227 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 228 eq_neq_eq_imp_neq) => 229 (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 230 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 231 not_sym, not_lessD, thm, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) 232 | update "not_lessI" thm thms = 233 change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 234 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 235 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 236 eq_neq_eq_imp_neq) => 237 (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 238 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 239 not_sym, not_lessD, not_leD, thm, not_leI, less_imp_neq, eq_neq_eq_imp_neq)) 240 | update "not_leI" thm thms = 241 change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 242 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 243 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 244 eq_neq_eq_imp_neq) => 245 (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 246 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 247 not_sym, not_lessD, not_leD, not_lessI, thm, less_imp_neq, eq_neq_eq_imp_neq)) 248 | update "less_imp_neq" thm thms = 249 change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 250 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 251 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 252 eq_neq_eq_imp_neq) => 253 (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 254 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 255 not_sym, not_lessD, not_leD, not_lessI, not_leI, thm, eq_neq_eq_imp_neq)) 256 | update "eq_neq_eq_imp_neq" thm thms = 257 change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 258 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 259 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, 260 eq_neq_eq_imp_neq) => 261 (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans, 262 less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans, 263 not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, thm)); 264 265(* Internal datatype for the proof *) 266datatype proof 267 = Asm of int 268 | Thm of proof list * thm; 269 270exception Cannot; 271 (* Internal exception, raised if conclusion cannot be derived from 272 assumptions. *) 273exception Contr of proof; 274 (* Internal exception, raised if contradiction ( x < x ) was derived *) 275 276fun prove asms = 277 let 278 fun pr (Asm i) = nth asms i 279 | pr (Thm (prfs, thm)) = map pr prfs MRS thm; 280 in pr end; 281 282(* Internal datatype for inequalities *) 283datatype less 284 = Less of term * term * proof 285 | Le of term * term * proof 286 | NotEq of term * term * proof; 287 288(* Misc functions for datatype less *) 289fun lower (Less (x, _, _)) = x 290 | lower (Le (x, _, _)) = x 291 | lower (NotEq (x,_,_)) = x; 292 293fun upper (Less (_, y, _)) = y 294 | upper (Le (_, y, _)) = y 295 | upper (NotEq (_,y,_)) = y; 296 297fun getprf (Less (_, _, p)) = p 298| getprf (Le (_, _, p)) = p 299| getprf (NotEq (_,_, p)) = p; 300 301 302(* ************************************************************************ *) 303(* *) 304(* mkasm_partial *) 305(* *) 306(* Tuple (t, n) (t an assumption, n its index in the assumptions) is *) 307(* translated to an element of type less. *) 308(* Partial orders only. *) 309(* *) 310(* ************************************************************************ *) 311 312fun mkasm_partial decomp (less_thms : less_arith) sign (n, t) = 313 case decomp sign t of 314 SOME (x, rel, y) => (case rel of 315 "<" => if (x aconv y) then raise Contr (Thm ([Asm n], #less_reflE less_thms)) 316 else [Less (x, y, Asm n)] 317 | "~<" => [] 318 | "<=" => [Le (x, y, Asm n)] 319 | "~<=" => [] 320 | "=" => [Le (x, y, Thm ([Asm n], #eqD1 less_thms)), 321 Le (y, x, Thm ([Asm n], #eqD2 less_thms))] 322 | "~=" => if (x aconv y) then 323 raise Contr (Thm ([(Thm ([(Thm ([], #le_refl less_thms)) ,(Asm n)], #le_neq_trans less_thms))], #less_reflE less_thms)) 324 else [ NotEq (x, y, Asm n), 325 NotEq (y, x,Thm ( [Asm n], #not_sym less_thms))] 326 | _ => error ("partial_tac: unknown relation symbol ``" ^ rel ^ 327 "''returned by decomp.")) 328 | NONE => []; 329 330(* ************************************************************************ *) 331(* *) 332(* mkasm_linear *) 333(* *) 334(* Tuple (t, n) (t an assumption, n its index in the assumptions) is *) 335(* translated to an element of type less. *) 336(* Linear orders only. *) 337(* *) 338(* ************************************************************************ *) 339 340fun mkasm_linear decomp (less_thms : less_arith) sign (n, t) = 341 case decomp sign t of 342 SOME (x, rel, y) => (case rel of 343 "<" => if (x aconv y) then raise Contr (Thm ([Asm n], #less_reflE less_thms)) 344 else [Less (x, y, Asm n)] 345 | "~<" => [Le (y, x, Thm ([Asm n], #not_lessD less_thms))] 346 | "<=" => [Le (x, y, Asm n)] 347 | "~<=" => if (x aconv y) then 348 raise (Contr (Thm ([Thm ([Asm n], #not_leD less_thms)], #less_reflE less_thms))) 349 else [Less (y, x, Thm ([Asm n], #not_leD less_thms))] 350 | "=" => [Le (x, y, Thm ([Asm n], #eqD1 less_thms)), 351 Le (y, x, Thm ([Asm n], #eqD2 less_thms))] 352 | "~=" => if (x aconv y) then 353 raise Contr (Thm ([(Thm ([(Thm ([], #le_refl less_thms)) ,(Asm n)], #le_neq_trans less_thms))], #less_reflE less_thms)) 354 else [ NotEq (x, y, Asm n), 355 NotEq (y, x,Thm ( [Asm n], #not_sym less_thms))] 356 | _ => error ("linear_tac: unknown relation symbol ``" ^ rel ^ 357 "''returned by decomp.")) 358 | NONE => []; 359 360(* ************************************************************************ *) 361(* *) 362(* mkconcl_partial *) 363(* *) 364(* Translates conclusion t to an element of type less. *) 365(* Partial orders only. *) 366(* *) 367(* ************************************************************************ *) 368 369fun mkconcl_partial decomp (less_thms : less_arith) sign t = 370 case decomp sign t of 371 SOME (x, rel, y) => (case rel of 372 "<" => ([Less (x, y, Asm ~1)], Asm 0) 373 | "<=" => ([Le (x, y, Asm ~1)], Asm 0) 374 | "=" => ([Le (x, y, Asm ~1), Le (y, x, Asm ~1)], 375 Thm ([Asm 0, Asm 1], #eqI less_thms)) 376 | "~=" => ([NotEq (x,y, Asm ~1)], Asm 0) 377 | _ => raise Cannot) 378 | NONE => raise Cannot; 379 380(* ************************************************************************ *) 381(* *) 382(* mkconcl_linear *) 383(* *) 384(* Translates conclusion t to an element of type less. *) 385(* Linear orders only. *) 386(* *) 387(* ************************************************************************ *) 388 389fun mkconcl_linear decomp (less_thms : less_arith) sign t = 390 case decomp sign t of 391 SOME (x, rel, y) => (case rel of 392 "<" => ([Less (x, y, Asm ~1)], Asm 0) 393 | "~<" => ([Le (y, x, Asm ~1)], Thm ([Asm 0], #not_lessI less_thms)) 394 | "<=" => ([Le (x, y, Asm ~1)], Asm 0) 395 | "~<=" => ([Less (y, x, Asm ~1)], Thm ([Asm 0], #not_leI less_thms)) 396 | "=" => ([Le (x, y, Asm ~1), Le (y, x, Asm ~1)], 397 Thm ([Asm 0, Asm 1], #eqI less_thms)) 398 | "~=" => ([NotEq (x,y, Asm ~1)], Asm 0) 399 | _ => raise Cannot) 400 | NONE => raise Cannot; 401 402 403(*** The common part for partial and linear orders ***) 404 405(* Analysis of premises and conclusion: *) 406(* decomp (`x Rel y') should yield (x, Rel, y) 407 where Rel is one of "<", "<=", "~<", "~<=", "=" and "~=", 408 other relation symbols cause an error message *) 409 410fun gen_order_tac mkasm mkconcl decomp' (less_thms : less_arith) ctxt prems = 411 412let 413 414fun decomp sign t = Option.map (fn (x, rel, y) => 415 (Envir.beta_eta_contract x, rel, Envir.beta_eta_contract y)) (decomp' sign t); 416 417(* ******************************************************************* *) 418(* *) 419(* mergeLess *) 420(* *) 421(* Merge two elements of type less according to the following rules *) 422(* *) 423(* x < y && y < z ==> x < z *) 424(* x < y && y <= z ==> x < z *) 425(* x <= y && y < z ==> x < z *) 426(* x <= y && y <= z ==> x <= z *) 427(* x <= y && x ~= y ==> x < y *) 428(* x ~= y && x <= y ==> x < y *) 429(* x < y && x ~= y ==> x < y *) 430(* x ~= y && x < y ==> x < y *) 431(* *) 432(* ******************************************************************* *) 433 434fun mergeLess (Less (x, _, p) , Less (_ , z, q)) = 435 Less (x, z, Thm ([p,q] , #less_trans less_thms)) 436| mergeLess (Less (x, _, p) , Le (_ , z, q)) = 437 Less (x, z, Thm ([p,q] , #less_le_trans less_thms)) 438| mergeLess (Le (x, _, p) , Less (_ , z, q)) = 439 Less (x, z, Thm ([p,q] , #le_less_trans less_thms)) 440| mergeLess (Le (x, z, p) , NotEq (x', z', q)) = 441 if (x aconv x' andalso z aconv z' ) 442 then Less (x, z, Thm ([p,q] , #le_neq_trans less_thms)) 443 else error "linear/partial_tac: internal error le_neq_trans" 444| mergeLess (NotEq (x, z, p) , Le (x' , z', q)) = 445 if (x aconv x' andalso z aconv z') 446 then Less (x, z, Thm ([p,q] , #neq_le_trans less_thms)) 447 else error "linear/partial_tac: internal error neq_le_trans" 448| mergeLess (NotEq (x, z, p) , Less (x' , z', q)) = 449 if (x aconv x' andalso z aconv z') 450 then Less ((x' , z', q)) 451 else error "linear/partial_tac: internal error neq_less_trans" 452| mergeLess (Less (x, z, p) , NotEq (x', z', q)) = 453 if (x aconv x' andalso z aconv z') 454 then Less (x, z, p) 455 else error "linear/partial_tac: internal error less_neq_trans" 456| mergeLess (Le (x, _, p) , Le (_ , z, q)) = 457 Le (x, z, Thm ([p,q] , #le_trans less_thms)) 458| mergeLess (_, _) = 459 error "linear/partial_tac: internal error: undefined case"; 460 461 462(* ******************************************************************** *) 463(* tr checks for valid transitivity step *) 464(* ******************************************************************** *) 465 466infix tr; 467fun (Less (_, y, _)) tr (Le (x', _, _)) = ( y aconv x' ) 468 | (Le (_, y, _)) tr (Less (x', _, _)) = ( y aconv x' ) 469 | (Less (_, y, _)) tr (Less (x', _, _)) = ( y aconv x' ) 470 | (Le (_, y, _)) tr (Le (x', _, _)) = ( y aconv x' ) 471 | _ tr _ = false; 472 473 474(* ******************************************************************* *) 475(* *) 476(* transPath (Lesslist, Less): (less list * less) -> less *) 477(* *) 478(* If a path represented by a list of elements of type less is found, *) 479(* this needs to be contracted to a single element of type less. *) 480(* Prior to each transitivity step it is checked whether the step is *) 481(* valid. *) 482(* *) 483(* ******************************************************************* *) 484 485fun transPath ([],lesss) = lesss 486| transPath (x::xs,lesss) = 487 if lesss tr x then transPath (xs, mergeLess(lesss,x)) 488 else error "linear/partial_tac: internal error transpath"; 489 490(* ******************************************************************* *) 491(* *) 492(* less1 subsumes less2 : less -> less -> bool *) 493(* *) 494(* subsumes checks whether less1 implies less2 *) 495(* *) 496(* ******************************************************************* *) 497 498infix subsumes; 499fun (Less (x, y, _)) subsumes (Le (x', y', _)) = 500 (x aconv x' andalso y aconv y') 501 | (Less (x, y, _)) subsumes (Less (x', y', _)) = 502 (x aconv x' andalso y aconv y') 503 | (Le (x, y, _)) subsumes (Le (x', y', _)) = 504 (x aconv x' andalso y aconv y') 505 | (Less (x, y, _)) subsumes (NotEq (x', y', _)) = 506 (x aconv x' andalso y aconv y') orelse (y aconv x' andalso x aconv y') 507 | (NotEq (x, y, _)) subsumes (NotEq (x', y', _)) = 508 (x aconv x' andalso y aconv y') orelse (y aconv x' andalso x aconv y') 509 | (Le _) subsumes (Less _) = 510 error "linear/partial_tac: internal error: Le cannot subsume Less" 511 | _ subsumes _ = false; 512 513(* ******************************************************************* *) 514(* *) 515(* triv_solv less1 : less -> proof option *) 516(* *) 517(* Solves trivial goal x <= x. *) 518(* *) 519(* ******************************************************************* *) 520 521fun triv_solv (Le (x, x', _)) = 522 if x aconv x' then SOME (Thm ([], #le_refl less_thms)) 523 else NONE 524| triv_solv _ = NONE; 525 526(* ********************************************************************* *) 527(* Graph functions *) 528(* ********************************************************************* *) 529 530 531 532(* ******************************************************************* *) 533(* *) 534(* General: *) 535(* *) 536(* Inequalities are represented by various types of graphs. *) 537(* *) 538(* 1. (Term.term * (Term.term * less) list) list *) 539(* - Graph of this type is generated from the assumptions, *) 540(* it does contain information on which edge stems from which *) 541(* assumption. *) 542(* - Used to compute strongly connected components *) 543(* - Used to compute component subgraphs *) 544(* - Used for component subgraphs to reconstruct paths in components*) 545(* *) 546(* 2. (int * (int * less) list ) list *) 547(* - Graph of this type is generated from the strong components of *) 548(* graph of type 1. It consists of the strong components of *) 549(* graph 1, where nodes are indices of the components. *) 550(* Only edges between components are part of this graph. *) 551(* - Used to reconstruct paths between several components. *) 552(* *) 553(* ******************************************************************* *) 554 555 556(* *********************************************************** *) 557(* Functions for constructing graphs *) 558(* *********************************************************** *) 559 560fun addEdge (v,d,[]) = [(v,d)] 561| addEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el) 562 else (u,dl):: (addEdge(v,d,el)); 563 564(* ********************************************************************* *) 565(* *) 566(* mkGraphs constructs from a list of objects of type less a graph g, *) 567(* by taking all edges that are candidate for a <=, and a list neqE, by *) 568(* taking all edges that are candiate for a ~= *) 569(* *) 570(* ********************************************************************* *) 571 572fun mkGraphs [] = ([],[],[]) 573| mkGraphs lessList = 574 let 575 576fun buildGraphs ([],leqG,neqG,neqE) = (leqG, neqG, neqE) 577| buildGraphs (l::ls, leqG,neqG, neqE) = case l of 578 (Less (x,y,p)) => 579 buildGraphs (ls, addEdge (x,[(y,(Less (x, y, p)))],leqG) , 580 addEdge (x,[(y,(Less (x, y, p)))],neqG), l::neqE) 581| (Le (x,y,p)) => 582 buildGraphs (ls, addEdge (x,[(y,(Le (x, y,p)))],leqG) , neqG, neqE) 583| (NotEq (x,y,p)) => 584 buildGraphs (ls, leqG , addEdge (x,[(y,(NotEq (x, y, p)))],neqG), l::neqE) ; 585 586 in buildGraphs (lessList, [], [], []) end; 587 588 589(* *********************************************************************** *) 590(* *) 591(* adjacent g u : (''a * 'b list ) list -> ''a -> 'b list *) 592(* *) 593(* List of successors of u in graph g *) 594(* *) 595(* *********************************************************************** *) 596 597fun adjacent eq_comp ((v,adj)::el) u = 598 if eq_comp (u, v) then adj else adjacent eq_comp el u 599| adjacent _ [] _ = [] 600 601 602(* *********************************************************************** *) 603(* *) 604(* transpose g: *) 605(* (''a * ''a list) list -> (''a * ''a list) list *) 606(* *) 607(* Computes transposed graph g' from g *) 608(* by reversing all edges u -> v to v -> u *) 609(* *) 610(* *********************************************************************** *) 611 612fun transpose eq_comp g = 613 let 614 (* Compute list of reversed edges for each adjacency list *) 615 fun flip (u,(v,l)::el) = (v,(u,l)) :: flip (u,el) 616 | flip (_,[]) = [] 617 618 (* Compute adjacency list for node u from the list of edges 619 and return a likewise reduced list of edges. The list of edges 620 is searches for edges starting from u, and these edges are removed. *) 621 fun gather (u,(v,w)::el) = 622 let 623 val (adj,edges) = gather (u,el) 624 in 625 if eq_comp (u, v) then (w::adj,edges) 626 else (adj,(v,w)::edges) 627 end 628 | gather (_,[]) = ([],[]) 629 630 (* For every node in the input graph, call gather to find all reachable 631 nodes in the list of edges *) 632 fun assemble ((u,_)::el) edges = 633 let val (adj,edges) = gather (u,edges) 634 in (u,adj) :: assemble el edges 635 end 636 | assemble [] _ = [] 637 638 (* Compute, for each adjacency list, the list with reversed edges, 639 and concatenate these lists. *) 640 val flipped = maps flip g 641 642 in assemble g flipped end 643 644(* *********************************************************************** *) 645(* *) 646(* scc_term : (term * term list) list -> term list list *) 647(* *) 648(* The following is based on the algorithm for finding strongly connected *) 649(* components described in Introduction to Algorithms, by Cormon, Leiserson*) 650(* and Rivest, section 23.5. The input G is an adjacency list description *) 651(* of a directed graph. The output is a list of the strongly connected *) 652(* components (each a list of vertices). *) 653(* *) 654(* *) 655(* *********************************************************************** *) 656 657fun scc_term G = 658 let 659 (* Ordered list of the vertices that DFS has finished with; 660 most recently finished goes at the head. *) 661 val finish : term list Unsynchronized.ref = Unsynchronized.ref [] 662 663 (* List of vertices which have been visited. *) 664 val visited : term list Unsynchronized.ref = Unsynchronized.ref [] 665 666 fun been_visited v = exists (fn w => w aconv v) (!visited) 667 668 (* Given the adjacency list rep of a graph (a list of pairs), 669 return just the first element of each pair, yielding the 670 vertex list. *) 671 val members = map (fn (v,_) => v) 672 673 (* Returns the nodes in the DFS tree rooted at u in g *) 674 fun dfs_visit g u : term list = 675 let 676 val _ = visited := u :: !visited 677 val descendents = 678 List.foldr (fn ((v,l),ds) => if been_visited v then ds 679 else v :: dfs_visit g v @ ds) 680 [] (adjacent (op aconv) g u) 681 in 682 finish := u :: !finish; 683 descendents 684 end 685 in 686 687 (* DFS on the graph; apply dfs_visit to each vertex in 688 the graph, checking first to make sure the vertex is 689 as yet unvisited. *) 690 List.app (fn u => if been_visited u then () 691 else (dfs_visit G u; ())) (members G); 692 visited := []; 693 694 (* We don't reset finish because its value is used by 695 foldl below, and it will never be used again (even 696 though dfs_visit will continue to modify it). *) 697 698 (* DFS on the transpose. The vertices returned by 699 dfs_visit along with u form a connected component. We 700 collect all the connected components together in a 701 list, which is what is returned. *) 702 fold (fn u => fn comps => 703 if been_visited u then comps 704 else (u :: dfs_visit (transpose (op aconv) G) u) :: comps) (!finish) [] 705end; 706 707 708(* *********************************************************************** *) 709(* *) 710(* dfs_int_reachable g u: *) 711(* (int * int list) list -> int -> int list *) 712(* *) 713(* Computes list of all nodes reachable from u in g. *) 714(* *) 715(* *********************************************************************** *) 716 717fun dfs_int_reachable g u = 718 let 719 (* List of vertices which have been visited. *) 720 val visited : int list Unsynchronized.ref = Unsynchronized.ref [] 721 722 fun been_visited v = exists (fn w => w = v) (!visited) 723 724 fun dfs_visit g u : int list = 725 let 726 val _ = visited := u :: !visited 727 val descendents = 728 List.foldr (fn ((v,l),ds) => if been_visited v then ds 729 else v :: dfs_visit g v @ ds) 730 [] (adjacent (op =) g u) 731 in descendents end 732 733 in u :: dfs_visit g u end; 734 735 736fun indexNodes IndexComp = 737 maps (fn (index, comp) => (map (fn v => (v,index)) comp)) IndexComp; 738 739fun getIndex v [] = ~1 740| getIndex v ((v',k)::vs) = if v aconv v' then k else getIndex v vs; 741 742 743 744(* *********************************************************************** *) 745(* *) 746(* dfs eq_comp g u v: *) 747(* ('a * 'a -> bool) -> ('a *( 'a * less) list) list -> *) 748(* 'a -> 'a -> (bool * ('a * less) list) *) 749(* *) 750(* Depth first search of v from u. *) 751(* Returns (true, path(u, v)) if successful, otherwise (false, []). *) 752(* *) 753(* *********************************************************************** *) 754 755fun dfs eq_comp g u v = 756 let 757 val pred = Unsynchronized.ref []; 758 val visited = Unsynchronized.ref []; 759 760 fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited) 761 762 fun dfs_visit u' = 763 let val _ = visited := u' :: (!visited) 764 765 fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end; 766 767 in if been_visited v then () 768 else (List.app (fn (v',l) => if been_visited v' then () else ( 769 update (v',l); 770 dfs_visit v'; ()) )) (adjacent eq_comp g u') 771 end 772 in 773 dfs_visit u; 774 if (been_visited v) then (true, (!pred)) else (false , []) 775 end; 776 777 778(* *********************************************************************** *) 779(* *) 780(* completeTermPath u v g: *) 781(* Term.term -> Term.term -> (Term.term * (Term.term * less) list) list *) 782(* -> less list *) 783(* *) 784(* Complete the path from u to v in graph g. Path search is performed *) 785(* with dfs_term g u v. This yields for each node v' its predecessor u' *) 786(* and the edge u' -> v'. Allows traversing graph backwards from v and *) 787(* finding the path u -> v. *) 788(* *) 789(* *********************************************************************** *) 790 791 792fun completeTermPath u v g = 793 let 794 val (found, tmp) = dfs (op aconv) g u v ; 795 val pred = map snd tmp; 796 797 fun path x y = 798 let 799 800 (* find predecessor u of node v and the edge u -> v *) 801 802 fun lookup v [] = raise Cannot 803 | lookup v (e::es) = if (upper e) aconv v then e else lookup v es; 804 805 (* traverse path backwards and return list of visited edges *) 806 fun rev_path v = 807 let val l = lookup v pred 808 val u = lower l; 809 in 810 if u aconv x then [l] 811 else (rev_path u) @ [l] 812 end 813 in rev_path y end; 814 815 in 816 if found then (if u aconv v then [(Le (u, v, (Thm ([], #le_refl less_thms))))] 817 else path u v ) else raise Cannot 818end; 819 820 821(* *********************************************************************** *) 822(* *) 823(* findProof (sccGraph, neqE, ntc, sccSubgraphs) subgoal: *) 824(* *) 825(* (int * (int * less) list) list * less list * (Term.term * int) list *) 826(* * ((term * (term * less) list) list) list -> Less -> proof *) 827(* *) 828(* findProof constructs from graphs (sccGraph, sccSubgraphs) and neqE a *) 829(* proof for subgoal. Raises exception Cannot if this is not possible. *) 830(* *) 831(* *********************************************************************** *) 832 833fun findProof (sccGraph, neqE, ntc, sccSubgraphs) subgoal = 834let 835 836 (* complete path x y from component graph *) 837 fun completeComponentPath x y predlist = 838 let 839 val xi = getIndex x ntc 840 val yi = getIndex y ntc 841 842 fun lookup k [] = raise Cannot 843 | lookup k ((h: int,l)::us) = if k = h then l else lookup k us; 844 845 fun rev_completeComponentPath y' = 846 let val edge = lookup (getIndex y' ntc) predlist 847 val u = lower edge 848 val v = upper edge 849 in 850 if (getIndex u ntc) = xi then 851 completeTermPath x u (nth sccSubgraphs xi) @ [edge] @ 852 completeTermPath v y' (nth sccSubgraphs (getIndex y' ntc)) 853 else 854 rev_completeComponentPath u @ [edge] @ 855 completeTermPath v y' (nth sccSubgraphs (getIndex y' ntc)) 856 end 857 in 858 if x aconv y then 859 [(Le (x, y, (Thm ([], #le_refl less_thms))))] 860 else if xi = yi then completeTermPath x y (nth sccSubgraphs xi) 861 else rev_completeComponentPath y 862 end; 863 864(* ******************************************************************* *) 865(* findLess e x y xi yi xreachable yreachable *) 866(* *) 867(* Find a path from x through e to y, of weight < *) 868(* ******************************************************************* *) 869 870 fun findLess e x y xi yi xreachable yreachable = 871 let val u = lower e 872 val v = upper e 873 val ui = getIndex u ntc 874 val vi = getIndex v ntc 875 876 in 877 if member (op =) xreachable ui andalso member (op =) xreachable vi andalso 878 member (op =) yreachable ui andalso member (op =) yreachable vi then ( 879 880 (case e of (Less (_, _, _)) => 881 let 882 val (xufound, xupred) = dfs (op =) sccGraph xi (getIndex u ntc) 883 in 884 if xufound then ( 885 let 886 val (vyfound, vypred) = dfs (op =) sccGraph (getIndex v ntc) yi 887 in 888 if vyfound then ( 889 let 890 val xypath = (completeComponentPath x u xupred)@[e]@(completeComponentPath v y vypred) 891 val xyLesss = transPath (tl xypath, hd xypath) 892 in 893 if xyLesss subsumes subgoal then SOME (getprf xyLesss) 894 else NONE 895 end) 896 else NONE 897 end) 898 else NONE 899 end 900 | _ => 901 let val (uvfound, uvpred) = dfs (op =) sccGraph (getIndex u ntc) (getIndex v ntc) 902 in 903 if uvfound then ( 904 let 905 val (xufound, xupred) = dfs (op =) sccGraph xi (getIndex u ntc) 906 in 907 if xufound then ( 908 let 909 val (vyfound, vypred) = dfs (op =) sccGraph (getIndex v ntc) yi 910 in 911 if vyfound then ( 912 let 913 val uvpath = completeComponentPath u v uvpred 914 val uvLesss = mergeLess ( transPath (tl uvpath, hd uvpath), e) 915 val xypath = (completeComponentPath x u xupred)@[uvLesss]@(completeComponentPath v y vypred) 916 val xyLesss = transPath (tl xypath, hd xypath) 917 in 918 if xyLesss subsumes subgoal then SOME (getprf xyLesss) 919 else NONE 920 end ) 921 else NONE 922 end) 923 else NONE 924 end ) 925 else NONE 926 end ) 927 ) else NONE 928end; 929 930 931in 932 (* looking for x <= y: any path from x to y is sufficient *) 933 case subgoal of (Le (x, y, _)) => ( 934 if null sccGraph then raise Cannot else ( 935 let 936 val xi = getIndex x ntc 937 val yi = getIndex y ntc 938 (* searches in sccGraph a path from xi to yi *) 939 val (found, pred) = dfs (op =) sccGraph xi yi 940 in 941 if found then ( 942 let val xypath = completeComponentPath x y pred 943 val xyLesss = transPath (tl xypath, hd xypath) 944 in 945 (case xyLesss of 946 (Less (_, _, q)) => if xyLesss subsumes subgoal then (Thm ([q], #less_imp_le less_thms)) 947 else raise Cannot 948 | _ => if xyLesss subsumes subgoal then (getprf xyLesss) 949 else raise Cannot) 950 end ) 951 else raise Cannot 952 end 953 ) 954 ) 955 (* looking for x < y: particular path required, which is not necessarily 956 found by normal dfs *) 957 | (Less (x, y, _)) => ( 958 if null sccGraph then raise Cannot else ( 959 let 960 val xi = getIndex x ntc 961 val yi = getIndex y ntc 962 val sccGraph_transpose = transpose (op =) sccGraph 963 (* all components that can be reached from component xi *) 964 val xreachable = dfs_int_reachable sccGraph xi 965 (* all comonents reachable from y in the transposed graph sccGraph' *) 966 val yreachable = dfs_int_reachable sccGraph_transpose yi 967 (* for all edges u ~= v or u < v check if they are part of path x < y *) 968 fun processNeqEdges [] = raise Cannot 969 | processNeqEdges (e::es) = 970 case (findLess e x y xi yi xreachable yreachable) of (SOME prf) => prf 971 | _ => processNeqEdges es 972 973 in 974 processNeqEdges neqE 975 end 976 ) 977 ) 978| (NotEq (x, y, _)) => ( 979 (* if there aren't any edges that are candidate for a ~= raise Cannot *) 980 if null neqE then raise Cannot 981 (* if there aren't any edges that are candidate for <= then just search a edge in neqE that implies the subgoal *) 982 else if null sccSubgraphs then ( 983 (case (find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of 984 ( SOME (NotEq (x, y, p)), NotEq (x', y', _)) => 985 if (x aconv x' andalso y aconv y') then p 986 else Thm ([p], #not_sym less_thms) 987 | ( SOME (Less (x, y, p)), NotEq (x', y', _)) => 988 if x aconv x' andalso y aconv y' then (Thm ([p], #less_imp_neq less_thms)) 989 else (Thm ([(Thm ([p], #less_imp_neq less_thms))], #not_sym less_thms)) 990 | _ => raise Cannot) 991 ) else ( 992 993 let val xi = getIndex x ntc 994 val yi = getIndex y ntc 995 val sccGraph_transpose = transpose (op =) sccGraph 996 val xreachable = dfs_int_reachable sccGraph xi 997 val yreachable = dfs_int_reachable sccGraph_transpose yi 998 999 fun processNeqEdges [] = raise Cannot 1000 | processNeqEdges (e::es) = ( 1001 let val u = lower e 1002 val v = upper e 1003 val ui = getIndex u ntc 1004 val vi = getIndex v ntc 1005 1006 in 1007 (* if x ~= y follows from edge e *) 1008 if e subsumes subgoal then ( 1009 case e of (Less (u, v, q)) => ( 1010 if u aconv x andalso v aconv y then (Thm ([q], #less_imp_neq less_thms)) 1011 else (Thm ([(Thm ([q], #less_imp_neq less_thms))], #not_sym less_thms)) 1012 ) 1013 | (NotEq (u,v, q)) => ( 1014 if u aconv x andalso v aconv y then q 1015 else (Thm ([q], #not_sym less_thms)) 1016 ) 1017 ) 1018 (* if SCC_x is linked to SCC_y via edge e *) 1019 else if ui = xi andalso vi = yi then ( 1020 case e of (Less (_, _,_)) => ( 1021 let 1022 val xypath = 1023 completeTermPath x u (nth sccSubgraphs ui) @ [e] @ 1024 completeTermPath v y (nth sccSubgraphs vi) 1025 val xyLesss = transPath (tl xypath, hd xypath) 1026 in (Thm ([getprf xyLesss], #less_imp_neq less_thms)) end) 1027 | _ => ( 1028 let 1029 val xupath = completeTermPath x u (nth sccSubgraphs ui) 1030 val uxpath = completeTermPath u x (nth sccSubgraphs ui) 1031 val vypath = completeTermPath v y (nth sccSubgraphs vi) 1032 val yvpath = completeTermPath y v (nth sccSubgraphs vi) 1033 val xuLesss = transPath (tl xupath, hd xupath) 1034 val uxLesss = transPath (tl uxpath, hd uxpath) 1035 val vyLesss = transPath (tl vypath, hd vypath) 1036 val yvLesss = transPath (tl yvpath, hd yvpath) 1037 val x_eq_u = (Thm ([(getprf xuLesss),(getprf uxLesss)], #eqI less_thms)) 1038 val v_eq_y = (Thm ([(getprf vyLesss),(getprf yvLesss)], #eqI less_thms)) 1039 in 1040 (Thm ([x_eq_u , (getprf e), v_eq_y ], #eq_neq_eq_imp_neq less_thms)) 1041 end 1042 ) 1043 ) else if ui = yi andalso vi = xi then ( 1044 case e of (Less (_, _,_)) => ( 1045 let 1046 val xypath = 1047 completeTermPath y u (nth sccSubgraphs ui) @ [e] @ 1048 completeTermPath v x (nth sccSubgraphs vi) 1049 val xyLesss = transPath (tl xypath, hd xypath) 1050 in (Thm ([(Thm ([getprf xyLesss], #less_imp_neq less_thms))] , #not_sym less_thms)) end ) 1051 | _ => ( 1052 1053 let val yupath = completeTermPath y u (nth sccSubgraphs ui) 1054 val uypath = completeTermPath u y (nth sccSubgraphs ui) 1055 val vxpath = completeTermPath v x (nth sccSubgraphs vi) 1056 val xvpath = completeTermPath x v (nth sccSubgraphs vi) 1057 val yuLesss = transPath (tl yupath, hd yupath) 1058 val uyLesss = transPath (tl uypath, hd uypath) 1059 val vxLesss = transPath (tl vxpath, hd vxpath) 1060 val xvLesss = transPath (tl xvpath, hd xvpath) 1061 val y_eq_u = (Thm ([(getprf yuLesss),(getprf uyLesss)], #eqI less_thms)) 1062 val v_eq_x = (Thm ([(getprf vxLesss),(getprf xvLesss)], #eqI less_thms)) 1063 in 1064 (Thm ([(Thm ([y_eq_u , (getprf e), v_eq_x ], #eq_neq_eq_imp_neq less_thms))], #not_sym less_thms)) 1065 end 1066 ) 1067 ) else ( 1068 (* there exists a path x < y or y < x such that 1069 x ~= y may be concluded *) 1070 case (findLess e x y xi yi xreachable yreachable) of 1071 (SOME prf) => (Thm ([prf], #less_imp_neq less_thms)) 1072 | NONE => ( 1073 let 1074 val yr = dfs_int_reachable sccGraph yi 1075 val xr = dfs_int_reachable sccGraph_transpose xi 1076 in 1077 case (findLess e y x yi xi yr xr) of 1078 (SOME prf) => (Thm ([(Thm ([prf], #less_imp_neq less_thms))], #not_sym less_thms)) 1079 | _ => processNeqEdges es 1080 end) 1081 ) end) 1082 in processNeqEdges neqE end) 1083 ) 1084end; 1085 1086 1087(* ******************************************************************* *) 1088(* *) 1089(* mk_sccGraphs components leqG neqG ntc : *) 1090(* Term.term list list -> *) 1091(* (Term.term * (Term.term * less) list) list -> *) 1092(* (Term.term * (Term.term * less) list) list -> *) 1093(* (Term.term * int) list -> *) 1094(* (int * (int * less) list) list * *) 1095(* ((Term.term * (Term.term * less) list) list) list *) 1096(* *) 1097(* *) 1098(* Computes, from graph leqG, list of all its components and the list *) 1099(* ntc (nodes, index of component) a graph whose nodes are the *) 1100(* indices of the components of g. Egdes of the new graph are *) 1101(* only the edges of g linking two components. Also computes for each *) 1102(* component the subgraph of leqG that forms this component. *) 1103(* *) 1104(* For each component SCC_i is checked if there exists a edge in neqG *) 1105(* that leads to a contradiction. *) 1106(* *) 1107(* We have a contradiction for edge u ~= v and u < v if: *) 1108(* - u and v are in the same component, *) 1109(* that is, a path u <= v and a path v <= u exist, hence u = v. *) 1110(* From irreflexivity of < follows u < u or v < v. Ex false quodlibet. *) 1111(* *) 1112(* ******************************************************************* *) 1113 1114fun mk_sccGraphs _ [] _ _ = ([],[]) 1115| mk_sccGraphs components leqG neqG ntc = 1116 let 1117 (* Liste (Index der Komponente, Komponente *) 1118 val IndexComp = map_index I components; 1119 1120 1121 fun handleContr edge g = 1122 (case edge of 1123 (Less (x, y, _)) => ( 1124 let 1125 val xxpath = edge :: (completeTermPath y x g ) 1126 val xxLesss = transPath (tl xxpath, hd xxpath) 1127 val q = getprf xxLesss 1128 in 1129 raise (Contr (Thm ([q], #less_reflE less_thms ))) 1130 end 1131 ) 1132 | (NotEq (x, y, _)) => ( 1133 let 1134 val xypath = (completeTermPath x y g ) 1135 val yxpath = (completeTermPath y x g ) 1136 val xyLesss = transPath (tl xypath, hd xypath) 1137 val yxLesss = transPath (tl yxpath, hd yxpath) 1138 val q = getprf (mergeLess ((mergeLess (edge, xyLesss)),yxLesss )) 1139 in 1140 raise (Contr (Thm ([q], #less_reflE less_thms ))) 1141 end 1142 ) 1143 | _ => error "trans_tac/handleContr: invalid Contradiction"); 1144 1145 1146 (* k is index of the actual component *) 1147 1148 fun processComponent (k, comp) = 1149 let 1150 (* all edges with weight <= of the actual component *) 1151 val leqEdges = maps (adjacent (op aconv) leqG) comp; 1152 (* all edges with weight ~= of the actual component *) 1153 val neqEdges = map snd (maps (adjacent (op aconv) neqG) comp); 1154 1155 (* find an edge leading to a contradiction *) 1156 fun findContr [] = NONE 1157 | findContr (e::es) = 1158 let val ui = (getIndex (lower e) ntc) 1159 val vi = (getIndex (upper e) ntc) 1160 in 1161 if ui = vi then SOME e 1162 else findContr es 1163 end; 1164 1165 (* sort edges into component internal edges and 1166 edges pointing away from the component *) 1167 fun sortEdges [] (intern,extern) = (intern,extern) 1168 | sortEdges ((v,l)::es) (intern, extern) = 1169 let val k' = getIndex v ntc in 1170 if k' = k then 1171 sortEdges es (l::intern, extern) 1172 else sortEdges es (intern, (k',l)::extern) end; 1173 1174 (* Insert edge into sorted list of edges, where edge is 1175 only added if 1176 - it is found for the first time 1177 - it is a <= edge and no parallel < edge was found earlier 1178 - it is a < edge 1179 *) 1180 fun insert (h: int,l) [] = [(h,l)] 1181 | insert (h,l) ((k',l')::es) = if h = k' then ( 1182 case l of (Less (_, _, _)) => (h,l)::es 1183 | _ => (case l' of (Less (_, _, _)) => (h,l')::es 1184 | _ => (k',l)::es) ) 1185 else (k',l'):: insert (h,l) es; 1186 1187 (* Reorganise list of edges such that 1188 - duplicate edges are removed 1189 - if a < edge and a <= edge exist at the same time, 1190 remove <= edge *) 1191 fun reOrganizeEdges [] sorted = sorted: (int * less) list 1192 | reOrganizeEdges (e::es) sorted = reOrganizeEdges es (insert e sorted); 1193 1194 (* construct the subgraph forming the strongly connected component 1195 from the edge list *) 1196 fun sccSubGraph [] g = g 1197 | sccSubGraph (l::ls) g = 1198 sccSubGraph ls (addEdge ((lower l),[((upper l),l)],g)) 1199 1200 val (intern, extern) = sortEdges leqEdges ([], []); 1201 val subGraph = sccSubGraph intern []; 1202 1203 in 1204 case findContr neqEdges of SOME e => handleContr e subGraph 1205 | _ => ((k, (reOrganizeEdges (extern) [])), subGraph) 1206 end; 1207 1208 val tmp = map processComponent IndexComp 1209in 1210 ( (map fst tmp), (map snd tmp)) 1211end; 1212 1213 1214(** Find proof if possible. **) 1215 1216fun gen_solve mkconcl sign (asms, concl) = 1217 let 1218 val (leqG, neqG, neqE) = mkGraphs asms 1219 val components = scc_term leqG 1220 val ntc = indexNodes (map_index I components) 1221 val (sccGraph, sccSubgraphs) = mk_sccGraphs components leqG neqG ntc 1222 in 1223 let 1224 val (subgoals, prf) = mkconcl decomp less_thms sign concl 1225 fun solve facts less = 1226 (case triv_solv less of NONE => findProof (sccGraph, neqE, ntc, sccSubgraphs) less 1227 | SOME prf => prf ) 1228 in 1229 map (solve asms) subgoals 1230 end 1231 end; 1232 1233in 1234 SUBGOAL (fn (A, n) => fn st => 1235 let 1236 val thy = Proof_Context.theory_of ctxt; 1237 val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A)); 1238 val Hs = 1239 map Thm.prop_of prems @ 1240 map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A) 1241 val C = subst_bounds (rfrees, Logic.strip_assums_concl A) 1242 val lesss = flat (map_index (mkasm decomp less_thms thy) Hs) 1243 val prfs = gen_solve mkconcl thy (lesss, C); 1244 val (subgoals, prf) = mkconcl decomp less_thms thy C; 1245 in 1246 Subgoal.FOCUS (fn {context = ctxt', prems = asms, ...} => 1247 let val thms = map (prove (prems @ asms)) prfs 1248 in resolve_tac ctxt' [prove thms prf] 1 end) ctxt n st 1249 end 1250 handle Contr p => 1251 (Subgoal.FOCUS (fn {context = ctxt', prems = asms, ...} => 1252 resolve_tac ctxt' [prove asms p] 1) ctxt n st 1253 handle General.Subscript => Seq.empty) 1254 | Cannot => Seq.empty 1255 | General.Subscript => Seq.empty) 1256end; 1257 1258(* partial_tac - solves partial orders *) 1259val partial_tac = gen_order_tac mkasm_partial mkconcl_partial; 1260 1261(* linear_tac - solves linear/total orders *) 1262val linear_tac = gen_order_tac mkasm_linear mkconcl_linear; 1263 1264end; 1265