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