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