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