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