src/Provers/order.ML
author wenzelm
Mon Mar 25 16:45:08 2019 +0100 (3 months ago)
changeset 69980 f2e3adfd916f
parent 67379 c2dfc510a38c
permissions -rw-r--r--
tuned signature;
     1 (*  Title:      Provers/order.ML
     2     Author:     Oliver Kutter, TU Muenchen
     3 
     4 Transitivity reasoner for partial and linear orders.
     5 *)
     6 
     7 (* TODO: reduce number of input thms *)
     8 
     9 (*
    10 
    11 The package provides tactics partial_tac and linear_tac that use all
    12 premises of the form
    13 
    14   t = u, t ~= u, t < u, t <= u, ~(t < u) and ~(t <= u)
    15 
    16 to
    17 1. either derive a contradiction,
    18    in which case the conclusion can be any term,
    19 2. 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 
    22 The package is not limited to the relation <= and friends.  It can be
    23 instantiated to any partial and/or linear order --- for example, the
    24 divisibility relation "dvd".  In order to instantiate the package for
    25 a partial order only, supply dummy theorems to the rules for linear
    26 orders, and don't use linear_tac!
    27 
    28 *)
    29 
    30 signature ORDER_TAC =
    31 sig
    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
    44 end;
    45 
    46 structure Order_Tac: ORDER_TAC =
    47 struct
    48 
    49 (* Record to handle input theorems in a convenient way. *)
    50 
    51 type 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 
    79 fun 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 
    88 fun 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 
   112 fun 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 *)
   266 datatype proof
   267   = Asm of int
   268   | Thm of proof list * thm;
   269 
   270 exception Cannot;
   271  (* Internal exception, raised if conclusion cannot be derived from
   272      assumptions. *)
   273 exception Contr of proof;
   274   (* Internal exception, raised if contradiction ( x < x ) was derived *)
   275 
   276 fun 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 *)
   283 datatype 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 *)
   289 fun lower (Less (x, _, _)) = x
   290   | lower (Le (x, _, _)) = x
   291   | lower (NotEq (x,_,_)) = x;
   292 
   293 fun upper (Less (_, y, _)) = y
   294   | upper (Le (_, y, _)) = y
   295   | upper (NotEq (_,y,_)) = y;
   296 
   297 fun 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 
   312 fun 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 
   340 fun 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 
   369 fun 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 
   389 fun 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 
   410 fun gen_order_tac mkasm mkconcl decomp' (less_thms : less_arith) ctxt prems =
   411 
   412 let
   413 
   414 fun 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 
   434 fun 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 
   466 infix tr;
   467 fun (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 
   485 fun 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 
   498 infix subsumes;
   499 fun (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 
   521 fun 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 
   560 fun 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 
   572 fun mkGraphs [] = ([],[],[])
   573 |   mkGraphs lessList =
   574  let
   575 
   576 fun 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 
   597 fun 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 
   612 fun 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 
   657 fun 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) []
   705 end;
   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 
   717 fun 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 
   736 fun indexNodes IndexComp =
   737     maps (fn (index, comp) => (map (fn v => (v,index)) comp)) IndexComp;
   738 
   739 fun 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 
   755 fun 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 
   792 fun 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
   818 end;
   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 
   833 fun findProof (sccGraph, neqE, ntc, sccSubgraphs) subgoal =
   834 let
   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
   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 (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   )
  1084 end;
  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 
  1114 fun 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
  1209 in
  1210      ( (map fst tmp), (map snd tmp))
  1211 end;
  1212 
  1213 
  1214 (** Find proof if possible. **)
  1215 
  1216 fun 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 
  1233 in
  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)
  1256 end;
  1257 
  1258 (* partial_tac - solves partial orders *)
  1259 val partial_tac = gen_order_tac mkasm_partial mkconcl_partial;
  1260 
  1261 (* linear_tac - solves linear/total orders *)
  1262 val linear_tac = gen_order_tac mkasm_linear mkconcl_linear;
  1263 
  1264 end;