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