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