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