src/Provers/order.ML
author haftmann
Wed May 05 18:25:34 2010 +0200 (2010-05-05)
changeset 36692 54b64d4ad524
parent 33245 65232054ffd0
child 37744 3daaf23b9ab4
permissions -rw-r--r--
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
     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 (n, t) =
   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 (n, t) =
   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 (_,[]) = []
   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 (_,[]) = ([],[])
   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 [] _ = []
   635 
   636    (* Compute, for each adjacency list, the list with reversed edges,
   637       and concatenate these lists. *)
   638    val flipped = maps 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         [] (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 := [];
   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   fold (fn u => fn comps =>
   701       if been_visited u then comps
   702       else (u :: dfs_visit (transpose (op aconv) G) u) :: comps) (!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         [] (adjacent (op =) g u)
   729    in  descendents end
   730 
   731  in u :: dfs_visit g u end;
   732 
   733 
   734 fun indexNodes IndexComp =
   735     maps (fn (index, comp) => (map (fn v => (v,index)) comp)) IndexComp;
   736 
   737 fun getIndex v [] = ~1
   738 |   getIndex v ((v',k)::vs) = if v aconv v' then k else getIndex v vs;
   739 
   740 
   741 
   742 (* *********************************************************************** *)
   743 (*                                                                         *)
   744 (* dfs eq_comp g u v:                                                       *)
   745 (* ('a * 'a -> bool) -> ('a  *( 'a * less) list) list ->                   *)
   746 (* 'a -> 'a -> (bool * ('a * less) list)                                   *)
   747 (*                                                                         *)
   748 (* Depth first search of v from u.                                         *)
   749 (* Returns (true, path(u, v)) if successful, otherwise (false, []).        *)
   750 (*                                                                         *)
   751 (* *********************************************************************** *)
   752 
   753 fun dfs eq_comp g u v =
   754  let
   755     val pred = Unsynchronized.ref [];
   756     val visited = Unsynchronized.ref [];
   757 
   758     fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
   759 
   760     fun dfs_visit u' =
   761     let val _ = visited := u' :: (!visited)
   762 
   763     fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
   764 
   765     in if been_visited v then ()
   766     else (app (fn (v',l) => if been_visited v' then () else (
   767        update (v',l);
   768        dfs_visit v'; ()) )) (adjacent eq_comp g u')
   769      end
   770   in
   771     dfs_visit u;
   772     if (been_visited v) then (true, (!pred)) else (false , [])
   773   end;
   774 
   775 
   776 (* *********************************************************************** *)
   777 (*                                                                         *)
   778 (* completeTermPath u v g:                                                 *)
   779 (* Term.term -> Term.term -> (Term.term * (Term.term * less) list) list    *)
   780 (* -> less list                                                            *)
   781 (*                                                                         *)
   782 (* Complete the path from u to v in graph g.  Path search is performed     *)
   783 (* with dfs_term g u v.  This yields for each node v' its predecessor u'   *)
   784 (* and the edge u' -> v'.  Allows traversing graph backwards from v and    *)
   785 (* finding the path u -> v.                                                *)
   786 (*                                                                         *)
   787 (* *********************************************************************** *)
   788 
   789 
   790 fun completeTermPath u v g  =
   791   let
   792    val (found, tmp) =  dfs (op aconv) g u v ;
   793    val pred = map snd tmp;
   794 
   795    fun path x y  =
   796       let
   797 
   798       (* find predecessor u of node v and the edge u -> v *)
   799 
   800       fun lookup v [] = raise Cannot
   801       |   lookup v (e::es) = if (upper e) aconv v then e else lookup v es;
   802 
   803       (* traverse path backwards and return list of visited edges *)
   804       fun rev_path v =
   805        let val l = lookup v pred
   806            val u = lower l;
   807        in
   808         if u aconv x then [l]
   809         else (rev_path u) @ [l]
   810        end
   811      in rev_path y end;
   812 
   813   in
   814   if found then (if u aconv v then [(Le (u, v, (Thm ([], #le_refl less_thms))))]
   815   else path u v ) else raise Cannot
   816 end;
   817 
   818 
   819 (* *********************************************************************** *)
   820 (*                                                                         *)
   821 (* findProof (sccGraph, neqE, ntc, sccSubgraphs) subgoal:                  *)
   822 (*                                                                         *)
   823 (* (int * (int * less) list) list * less list *  (Term.term * int) list    *)
   824 (* * ((term * (term * less) list) list) list -> Less -> proof              *)
   825 (*                                                                         *)
   826 (* findProof constructs from graphs (sccGraph, sccSubgraphs) and neqE a    *)
   827 (* proof for subgoal.  Raises exception Cannot if this is not possible.    *)
   828 (*                                                                         *)
   829 (* *********************************************************************** *)
   830 
   831 fun findProof (sccGraph, neqE, ntc, sccSubgraphs) subgoal =
   832 let
   833 
   834  (* complete path x y from component graph *)
   835  fun completeComponentPath x y predlist =
   836    let
   837           val xi = getIndex x ntc
   838           val yi = getIndex y ntc
   839 
   840           fun lookup k [] =  raise Cannot
   841           |   lookup k ((h: int,l)::us) = if k = h then l else lookup k us;
   842 
   843           fun rev_completeComponentPath y' =
   844            let val edge = lookup (getIndex y' ntc) predlist
   845                val u = lower edge
   846                val v = upper edge
   847            in
   848              if (getIndex u ntc) = xi then
   849                (completeTermPath x u (List.nth(sccSubgraphs, xi)) )@[edge]
   850                @(completeTermPath v y' (List.nth(sccSubgraphs, getIndex y' ntc)) )
   851              else (rev_completeComponentPath u)@[edge]
   852                   @(completeTermPath v y' (List.nth(sccSubgraphs, getIndex y' ntc)) )
   853            end
   854    in
   855       if x aconv y then
   856         [(Le (x, y, (Thm ([], #le_refl less_thms))))]
   857       else ( if xi = yi then completeTermPath x y (List.nth(sccSubgraphs, xi))
   858              else rev_completeComponentPath y )
   859    end;
   860 
   861 (* ******************************************************************* *)
   862 (* findLess e x y xi yi xreachable yreachable                          *)
   863 (*                                                                     *)
   864 (* Find a path from x through e to y, of weight <                      *)
   865 (* ******************************************************************* *)
   866 
   867  fun findLess e x y xi yi xreachable yreachable =
   868   let val u = lower e
   869       val v = upper e
   870       val ui = getIndex u ntc
   871       val vi = getIndex v ntc
   872 
   873   in
   874       if member (op =) xreachable ui andalso member (op =) xreachable vi andalso
   875          member (op =) yreachable ui andalso member (op =) yreachable vi then (
   876 
   877   (case e of (Less (_, _, _)) =>
   878        let
   879         val (xufound, xupred) =  dfs (op =) sccGraph xi (getIndex u ntc)
   880             in
   881              if xufound then (
   882               let
   883                val (vyfound, vypred) =  dfs (op =) sccGraph (getIndex v ntc) yi
   884               in
   885                if vyfound then (
   886                 let
   887                  val xypath = (completeComponentPath x u xupred)@[e]@(completeComponentPath v y vypred)
   888                  val xyLesss = transPath (tl xypath, hd xypath)
   889                 in
   890                  if xyLesss subsumes subgoal then SOME (getprf xyLesss)
   891                  else NONE
   892                end)
   893                else NONE
   894               end)
   895              else NONE
   896             end
   897        |  _   =>
   898          let val (uvfound, uvpred) =  dfs (op =) sccGraph (getIndex u ntc) (getIndex v ntc)
   899              in
   900               if uvfound then (
   901                let
   902                 val (xufound, xupred) = dfs (op =) sccGraph xi (getIndex u ntc)
   903                in
   904                 if xufound then (
   905                  let
   906                   val (vyfound, vypred) =  dfs (op =) sccGraph (getIndex v ntc) yi
   907                  in
   908                   if vyfound then (
   909                    let
   910                     val uvpath = completeComponentPath u v uvpred
   911                     val uvLesss = mergeLess ( transPath (tl uvpath, hd uvpath), e)
   912                     val xypath = (completeComponentPath  x u xupred)@[uvLesss]@(completeComponentPath v y vypred)
   913                     val xyLesss = transPath (tl xypath, hd xypath)
   914                    in
   915                     if xyLesss subsumes subgoal then SOME (getprf xyLesss)
   916                     else NONE
   917                    end )
   918                   else NONE
   919                  end)
   920                 else NONE
   921                end )
   922               else NONE
   923              end )
   924     ) else NONE
   925 end;
   926 
   927 
   928 in
   929   (* looking for x <= y: any path from x to y is sufficient *)
   930   case subgoal of (Le (x, y, _)) => (
   931   if null sccGraph then raise Cannot else (
   932    let
   933     val xi = getIndex x ntc
   934     val yi = getIndex y ntc
   935     (* searches in sccGraph a path from xi to yi *)
   936     val (found, pred) = dfs (op =) sccGraph xi yi
   937    in
   938     if found then (
   939        let val xypath = completeComponentPath x y pred
   940            val xyLesss = transPath (tl xypath, hd xypath)
   941        in
   942           (case xyLesss of
   943             (Less (_, _, q)) => if xyLesss subsumes subgoal then (Thm ([q], #less_imp_le less_thms))
   944                                 else raise Cannot
   945              | _   => if xyLesss subsumes subgoal then (getprf xyLesss)
   946                       else raise Cannot)
   947        end )
   948      else raise Cannot
   949    end
   950     )
   951    )
   952  (* looking for x < y: particular path required, which is not necessarily
   953     found by normal dfs *)
   954  |   (Less (x, y, _)) => (
   955   if null sccGraph then raise Cannot else (
   956    let
   957     val xi = getIndex x ntc
   958     val yi = getIndex y ntc
   959     val sccGraph_transpose = transpose (op =) sccGraph
   960     (* all components that can be reached from component xi  *)
   961     val xreachable = dfs_int_reachable sccGraph xi
   962     (* all comonents reachable from y in the transposed graph sccGraph' *)
   963     val yreachable = dfs_int_reachable sccGraph_transpose yi
   964     (* for all edges u ~= v or u < v check if they are part of path x < y *)
   965     fun processNeqEdges [] = raise Cannot
   966     |   processNeqEdges (e::es) =
   967       case  (findLess e x y xi yi xreachable yreachable) of (SOME prf) => prf
   968       | _ => processNeqEdges es
   969 
   970     in
   971        processNeqEdges neqE
   972     end
   973   )
   974  )
   975 | (NotEq (x, y, _)) => (
   976   (* if there aren't any edges that are candidate for a ~= raise Cannot *)
   977   if null neqE then raise Cannot
   978   (* if there aren't any edges that are candidate for <= then just search a edge in neqE that implies the subgoal *)
   979   else if null sccSubgraphs then (
   980      (case (Library.find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of
   981        ( SOME (NotEq (x, y, p)), NotEq (x', y', _)) =>
   982           if  (x aconv x' andalso y aconv y') then p
   983           else Thm ([p], #not_sym less_thms)
   984      | ( SOME (Less (x, y, p)), NotEq (x', y', _)) =>
   985           if x aconv x' andalso y aconv y' then (Thm ([p], #less_imp_neq less_thms))
   986           else (Thm ([(Thm ([p], #less_imp_neq less_thms))], #not_sym less_thms))
   987      | _ => raise Cannot)
   988    ) else (
   989 
   990    let  val xi = getIndex x ntc
   991         val yi = getIndex y ntc
   992         val sccGraph_transpose = transpose (op =) sccGraph
   993         val xreachable = dfs_int_reachable sccGraph xi
   994         val yreachable = dfs_int_reachable sccGraph_transpose yi
   995 
   996         fun processNeqEdges [] = raise Cannot
   997         |   processNeqEdges (e::es) = (
   998             let val u = lower e
   999                 val v = upper e
  1000                 val ui = getIndex u ntc
  1001                 val vi = getIndex v ntc
  1002 
  1003             in
  1004                 (* if x ~= y follows from edge e *)
  1005                 if e subsumes subgoal then (
  1006                      case e of (Less (u, v, q)) => (
  1007                        if u aconv x andalso v aconv y then (Thm ([q], #less_imp_neq less_thms))
  1008                        else (Thm ([(Thm ([q], #less_imp_neq less_thms))], #not_sym less_thms))
  1009                      )
  1010                      |    (NotEq (u,v, q)) => (
  1011                        if u aconv x andalso v aconv y then q
  1012                        else (Thm ([q],  #not_sym less_thms))
  1013                      )
  1014                  )
  1015                 (* if SCC_x is linked to SCC_y via edge e *)
  1016                  else if ui = xi andalso vi = yi then (
  1017                    case e of (Less (_, _,_)) => (
  1018                         let val xypath = (completeTermPath x u (List.nth(sccSubgraphs, ui)) ) @ [e] @ (completeTermPath v y (List.nth(sccSubgraphs, vi)) )
  1019                             val xyLesss = transPath (tl xypath, hd xypath)
  1020                         in  (Thm ([getprf xyLesss], #less_imp_neq less_thms)) end)
  1021                    | _ => (
  1022                         let
  1023                             val xupath = completeTermPath x u  (List.nth(sccSubgraphs, ui))
  1024                             val uxpath = completeTermPath u x  (List.nth(sccSubgraphs, ui))
  1025                             val vypath = completeTermPath v y  (List.nth(sccSubgraphs, vi))
  1026                             val yvpath = completeTermPath y v  (List.nth(sccSubgraphs, vi))
  1027                             val xuLesss = transPath (tl xupath, hd xupath)
  1028                             val uxLesss = transPath (tl uxpath, hd uxpath)
  1029                             val vyLesss = transPath (tl vypath, hd vypath)
  1030                             val yvLesss = transPath (tl yvpath, hd yvpath)
  1031                             val x_eq_u =  (Thm ([(getprf xuLesss),(getprf uxLesss)], #eqI less_thms))
  1032                             val v_eq_y =  (Thm ([(getprf vyLesss),(getprf yvLesss)], #eqI less_thms))
  1033                         in
  1034                            (Thm ([x_eq_u , (getprf e), v_eq_y ], #eq_neq_eq_imp_neq less_thms))
  1035                         end
  1036                         )
  1037                   ) else if ui = yi andalso vi = xi then (
  1038                      case e of (Less (_, _,_)) => (
  1039                         let val xypath = (completeTermPath y u (List.nth(sccSubgraphs, ui)) ) @ [e] @ (completeTermPath v x (List.nth(sccSubgraphs, vi)) )
  1040                             val xyLesss = transPath (tl xypath, hd xypath)
  1041                         in (Thm ([(Thm ([getprf xyLesss], #less_imp_neq less_thms))] , #not_sym less_thms)) end )
  1042                      | _ => (
  1043 
  1044                         let val yupath = completeTermPath y u (List.nth(sccSubgraphs, ui))
  1045                             val uypath = completeTermPath u y (List.nth(sccSubgraphs, ui))
  1046                             val vxpath = completeTermPath v x (List.nth(sccSubgraphs, vi))
  1047                             val xvpath = completeTermPath x v (List.nth(sccSubgraphs, vi))
  1048                             val yuLesss = transPath (tl yupath, hd yupath)
  1049                             val uyLesss = transPath (tl uypath, hd uypath)
  1050                             val vxLesss = transPath (tl vxpath, hd vxpath)
  1051                             val xvLesss = transPath (tl xvpath, hd xvpath)
  1052                             val y_eq_u =  (Thm ([(getprf yuLesss),(getprf uyLesss)], #eqI less_thms))
  1053                             val v_eq_x =  (Thm ([(getprf vxLesss),(getprf xvLesss)], #eqI less_thms))
  1054                         in
  1055                             (Thm ([(Thm ([y_eq_u , (getprf e), v_eq_x ], #eq_neq_eq_imp_neq less_thms))], #not_sym less_thms))
  1056                         end
  1057                        )
  1058                   ) else (
  1059                        (* there exists a path x < y or y < x such that
  1060                           x ~= y may be concluded *)
  1061                         case  (findLess e x y xi yi xreachable yreachable) of
  1062                               (SOME prf) =>  (Thm ([prf], #less_imp_neq less_thms))
  1063                              | NONE =>  (
  1064                                let
  1065                                 val yr = dfs_int_reachable sccGraph yi
  1066                                 val xr = dfs_int_reachable sccGraph_transpose xi
  1067                                in
  1068                                 case  (findLess e y x yi xi yr xr) of
  1069                                       (SOME prf) => (Thm ([(Thm ([prf], #less_imp_neq less_thms))], #not_sym less_thms))
  1070                                       | _ => processNeqEdges es
  1071                                end)
  1072                  ) end)
  1073      in processNeqEdges neqE end)
  1074   )
  1075 end;
  1076 
  1077 
  1078 (* ******************************************************************* *)
  1079 (*                                                                     *)
  1080 (* mk_sccGraphs components leqG neqG ntc :                             *)
  1081 (* Term.term list list ->                                              *)
  1082 (* (Term.term * (Term.term * less) list) list ->                       *)
  1083 (* (Term.term * (Term.term * less) list) list ->                       *)
  1084 (* (Term.term * int)  list ->                                          *)
  1085 (* (int * (int * less) list) list   *                                  *)
  1086 (* ((Term.term * (Term.term * less) list) list) list                   *)
  1087 (*                                                                     *)
  1088 (*                                                                     *)
  1089 (* Computes, from graph leqG, list of all its components and the list  *)
  1090 (* ntc (nodes, index of component) a graph whose nodes are the         *)
  1091 (* indices of the components of g.  Egdes of the new graph are         *)
  1092 (* only the edges of g linking two components. Also computes for each  *)
  1093 (* component the subgraph of leqG that forms this component.           *)
  1094 (*                                                                     *)
  1095 (* For each component SCC_i is checked if there exists a edge in neqG  *)
  1096 (* that leads to a contradiction.                                      *)
  1097 (*                                                                     *)
  1098 (* We have a contradiction for edge u ~= v and u < v if:               *)
  1099 (* - u and v are in the same component,                                *)
  1100 (* that is, a path u <= v and a path v <= u exist, hence u = v.        *)
  1101 (* From irreflexivity of < follows u < u or v < v. Ex false quodlibet. *)
  1102 (*                                                                     *)
  1103 (* ******************************************************************* *)
  1104 
  1105 fun mk_sccGraphs _ [] _ _ = ([],[])
  1106 |   mk_sccGraphs components leqG neqG ntc =
  1107     let
  1108     (* Liste (Index der Komponente, Komponente *)
  1109     val IndexComp = map_index I components;
  1110 
  1111 
  1112     fun handleContr edge g =
  1113        (case edge of
  1114           (Less  (x, y, _)) => (
  1115             let
  1116              val xxpath = edge :: (completeTermPath y x g )
  1117              val xxLesss = transPath (tl xxpath, hd xxpath)
  1118              val q = getprf xxLesss
  1119             in
  1120              raise (Contr (Thm ([q], #less_reflE less_thms )))
  1121             end
  1122           )
  1123         | (NotEq (x, y, _)) => (
  1124             let
  1125              val xypath = (completeTermPath x y g )
  1126              val yxpath = (completeTermPath y x g )
  1127              val xyLesss = transPath (tl xypath, hd xypath)
  1128              val yxLesss = transPath (tl yxpath, hd yxpath)
  1129              val q = getprf (mergeLess ((mergeLess (edge, xyLesss)),yxLesss ))
  1130             in
  1131              raise (Contr (Thm ([q], #less_reflE less_thms )))
  1132             end
  1133          )
  1134         | _ =>  error "trans_tac/handleContr: invalid Contradiction");
  1135 
  1136 
  1137     (* k is index of the actual component *)
  1138 
  1139     fun processComponent (k, comp) =
  1140      let
  1141         (* all edges with weight <= of the actual component *)
  1142         val leqEdges = maps (adjacent (op aconv) leqG) comp;
  1143         (* all edges with weight ~= of the actual component *)
  1144         val neqEdges = map snd (maps (adjacent (op aconv) neqG) comp);
  1145 
  1146        (* find an edge leading to a contradiction *)
  1147        fun findContr [] = NONE
  1148        |   findContr (e::es) =
  1149                     let val ui = (getIndex (lower e) ntc)
  1150                         val vi = (getIndex (upper e) ntc)
  1151                     in
  1152                         if ui = vi then  SOME e
  1153                         else findContr es
  1154                     end;
  1155 
  1156                 (* sort edges into component internal edges and
  1157                    edges pointing away from the component *)
  1158                 fun sortEdges  [] (intern,extern)  = (intern,extern)
  1159                 |   sortEdges  ((v,l)::es) (intern, extern) =
  1160                     let val k' = getIndex v ntc in
  1161                         if k' = k then
  1162                             sortEdges es (l::intern, extern)
  1163                         else sortEdges  es (intern, (k',l)::extern) end;
  1164 
  1165                 (* Insert edge into sorted list of edges, where edge is
  1166                     only added if
  1167                     - it is found for the first time
  1168                     - it is a <= edge and no parallel < edge was found earlier
  1169                     - it is a < edge
  1170                  *)
  1171                  fun insert (h: int,l) [] = [(h,l)]
  1172                  |   insert (h,l) ((k',l')::es) = if h = k' then (
  1173                      case l of (Less (_, _, _)) => (h,l)::es
  1174                      | _  => (case l' of (Less (_, _, _)) => (h,l')::es
  1175                               | _ => (k',l)::es) )
  1176                      else (k',l'):: insert (h,l) es;
  1177 
  1178                 (* Reorganise list of edges such that
  1179                     - duplicate edges are removed
  1180                     - if a < edge and a <= edge exist at the same time,
  1181                       remove <= edge *)
  1182                  fun reOrganizeEdges [] sorted = sorted: (int * less) list
  1183                  |   reOrganizeEdges (e::es) sorted = reOrganizeEdges es (insert e sorted);
  1184 
  1185                  (* construct the subgraph forming the strongly connected component
  1186                     from the edge list *)
  1187                  fun sccSubGraph [] g  = g
  1188                  |   sccSubGraph (l::ls) g =
  1189                           sccSubGraph ls (addEdge ((lower l),[((upper l),l)],g))
  1190 
  1191                  val (intern, extern) = sortEdges leqEdges ([], []);
  1192                  val subGraph = sccSubGraph intern [];
  1193 
  1194      in
  1195          case findContr neqEdges of SOME e => handleContr e subGraph
  1196          | _ => ((k, (reOrganizeEdges (extern) [])), subGraph)
  1197      end;
  1198 
  1199     val tmp =  map processComponent IndexComp
  1200 in
  1201      ( (map fst tmp), (map snd tmp))
  1202 end;
  1203 
  1204 
  1205 (** Find proof if possible. **)
  1206 
  1207 fun gen_solve mkconcl sign (asms, concl) =
  1208  let
  1209   val (leqG, neqG, neqE) = mkGraphs asms
  1210   val components = scc_term leqG
  1211   val ntc = indexNodes (map_index I components)
  1212   val (sccGraph, sccSubgraphs) = mk_sccGraphs components leqG neqG ntc
  1213  in
  1214    let
  1215    val (subgoals, prf) = mkconcl decomp less_thms sign concl
  1216    fun solve facts less =
  1217       (case triv_solv less of NONE => findProof (sccGraph, neqE, ntc, sccSubgraphs) less
  1218       | SOME prf => prf )
  1219   in
  1220    map (solve asms) subgoals
  1221   end
  1222  end;
  1223 
  1224 in
  1225  SUBGOAL (fn (A, n) => fn st =>
  1226   let
  1227    val thy = ProofContext.theory_of ctxt;
  1228    val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
  1229    val Hs = map prop_of prems @ map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
  1230    val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
  1231    val lesss = flat (map_index (mkasm decomp less_thms thy) Hs)
  1232    val prfs = gen_solve mkconcl thy (lesss, C);
  1233    val (subgoals, prf) = mkconcl decomp less_thms thy C;
  1234   in
  1235    Subgoal.FOCUS (fn {prems = asms, ...} =>
  1236      let val thms = map (prove (prems @ asms)) prfs
  1237      in rtac (prove thms prf) 1 end) ctxt n st
  1238   end
  1239   handle Contr p =>
  1240       (Subgoal.FOCUS (fn {prems = asms, ...} => rtac (prove asms p) 1) ctxt n st
  1241         handle Subscript => Seq.empty)
  1242    | Cannot => Seq.empty
  1243    | Subscript => Seq.empty)
  1244 end;
  1245 
  1246 (* partial_tac - solves partial orders *)
  1247 val partial_tac = gen_order_tac mkasm_partial mkconcl_partial;
  1248 
  1249 (* linear_tac - solves linear/total orders *)
  1250 val linear_tac = gen_order_tac mkasm_linear mkconcl_linear;
  1251 
  1252 end;