Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: order.ML Sprache: SML

Original von: Isabelle^©

(*  Title:      Provers/order.ML
    Author:     Oliver Kutter, TU Muenchen

Transitivity reasoner for partial and linear orders.
*)

(* TODO: reduce number of input thms *)

(*

The package provides tactics partial_tac and linear_tac that use all
premises of the form

  t = u, t ~= u, t < u, t <= u, ~(t < u) and ~(t <= u)

to
1. either derive a contradiction,
   in which case the conclusion can be any term,
2. or prove the conclusion, which must be of the same form as the
   premises (excluding ~(t < u) and ~(t <= u) for partial orders)

The package is not limited to the relation <= and friends.  It can be
instantiated to any partial and/or linear order --- for example, the
divisibility relation "dvd".  In order to instantiate the package for
a partial order only, supply dummy theorems to the rules for linear
orders, and don't use linear_tac!

*)

signature ORDER_TAC =
sig
  (* Theorems required by the reasoner *)
  type less_arith
  val empty : thm -> less_arith
  val update : string -> thm -> less_arith -> less_arith

  (* Tactics *)
  val partial_tac:
    (theory -> term -> (term * string * term) option) -> less_arith ->
    Proof.context -> thm list -> int -> tactic
  val linear_tac:
    (theory -> term -> (term * string * term) option) -> less_arith ->
    Proof.context -> thm list -> int -> tactic
end;

structure Order_Tac: ORDER_TAC =
struct

(* Record to handle input theorems in a convenient way. *)

type less_arith =
  {
    (* Theorems for partial orders *)
    less_reflE: thm,  (* x < x ==> P *)
    le_refl: thm,  (* x <= x *)
    less_imp_le: thm, (* x < y ==> x <= y *)
    eqI: thm, (* [| x <= y; y <= x |] ==> x = y *)
    eqD1: thm, (* x = y ==> x <= y *)
    eqD2: thm, (* x = y ==> y <= x *)
    less_trans: thm,  (* [| x < y; y < z |] ==> x < z *)
    less_le_trans: thm,  (* [| x < y; y <= z |] ==> x < z *)
    le_less_trans: thm,  (* [| x <= y; y < z |] ==> x < z *)
    le_trans: thm,  (* [| x <= y; y <= z |] ==> x <= z *)
    le_neq_trans : thm, (* [| x <= y ; x ~= y |] ==> x < y *)
    neq_le_trans : thm, (* [| x ~= y ; x <= y |] ==> x < y *)
    not_sym : thm, (* x ~= y ==> y ~= x *)

    (* Additional theorems for linear orders *)
    not_lessD: thm, (* ~(x < y) ==> y <= x *)
    not_leD: thm, (* ~(x <= y) ==> y < x *)
    not_lessI: thm, (* y <= x  ==> ~(x < y) *)
    not_leI: thm, (* y < x  ==> ~(x <= y) *)

    (* Additional theorems for subgoals of form x ~= y *)
    less_imp_neq : thm, (* x < y ==> x ~= y *)
    eq_neq_eq_imp_neq : thm (* [| x = u ; u ~= v ; v = z|] ==> x ~= z *)
  }

fun empty dummy_thm =
    {less_reflE= dummy_thm, le_refl= dummy_thm, less_imp_le= dummy_thm, eqI= dummy_thm,
      eqD1= dummy_thm, eqD2= dummy_thm,
      less_trans= dummy_thm, less_le_trans= dummy_thm, le_less_trans= dummy_thm,
      le_trans= dummy_thm, le_neq_trans = dummy_thm, neq_le_trans = dummy_thm,
      not_sym = dummy_thm,
      not_lessD= dummy_thm, not_leD= dummy_thm, not_lessI= dummy_thm, not_leI= dummy_thm,
      less_imp_neq = dummy_thm, eq_neq_eq_imp_neq = dummy_thm}

fun change thms f =
  let
    val {less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
      eq_neq_eq_imp_neq} = thms;
    val (less_reflE', le_refl', less_imp_le', eqI', eqD1', eqD2', less_trans',
      less_le_trans', le_less_trans', le_trans', le_neq_trans', neq_le_trans',
      not_sym', not_lessD', not_leD', not_lessI', not_leI', less_imp_neq',
      eq_neq_eq_imp_neq') =
     f (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
      eq_neq_eq_imp_neq)
  in {less_reflE = less_reflE', le_refl= le_refl',
      less_imp_le = less_imp_le', eqI = eqI', eqD1 = eqD1', eqD2 = eqD2',
      less_trans = less_trans', less_le_trans = less_le_trans',
      le_less_trans = le_less_trans', le_trans = le_trans', le_neq_trans = le_neq_trans',
      neq_le_trans = neq_le_trans', not_sym = not_sym',
      not_lessD = not_lessD', not_leD = not_leD', not_lessI = not_lessI',
      not_leI = not_leI',
      less_imp_neq = less_imp_neq', eq_neq_eq_imp_neq = eq_neq_eq_imp_neq'}
  end;

fun update "less_reflE" thm thms =
    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
      eq_neq_eq_imp_neq) =>
    (thm, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
  | update "le_refl" thm thms =
    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
      eq_neq_eq_imp_neq) =>
    (less_reflE, thm, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
  | update "less_imp_le" thm thms =
    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
      eq_neq_eq_imp_neq) =>
    (less_reflE, le_refl, thm, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
  | update "eqI" thm thms =
    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
      eq_neq_eq_imp_neq) =>
    (less_reflE, le_refl, less_imp_le, thm, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
  | update "eqD1" thm thms =
    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
      eq_neq_eq_imp_neq) =>
    (less_reflE, le_refl, less_imp_le, eqI, thm, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
  | update "eqD2" thm thms =
    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
      eq_neq_eq_imp_neq) =>
    (less_reflE, le_refl, less_imp_le, eqI, eqD1, thm, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
  | update "less_trans" thm thms =
    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
      eq_neq_eq_imp_neq) =>
    (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, thm,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
  | update "less_le_trans" thm thms =
    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
      eq_neq_eq_imp_neq) =>
    (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      thm, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
  | update "le_less_trans" thm thms =
    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
      eq_neq_eq_imp_neq) =>
    (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, thm, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
  | update "le_trans" thm thms =
    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
      eq_neq_eq_imp_neq) =>
    (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, thm, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
  | update "le_neq_trans" thm thms =
    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
      eq_neq_eq_imp_neq) =>
    (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, thm, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
  | update "neq_le_trans" thm thms =
    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
      eq_neq_eq_imp_neq) =>
    (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, thm,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
  | update "not_sym" thm thms =
    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
      eq_neq_eq_imp_neq) =>
    (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      thm, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
  | update "not_lessD" thm thms =
    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
      eq_neq_eq_imp_neq) =>
    (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, thm, not_leD, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
  | update "not_leD" thm thms =
    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
      eq_neq_eq_imp_neq) =>
    (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, thm, not_lessI, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
  | update "not_lessI" thm thms =
    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
      eq_neq_eq_imp_neq) =>
    (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, thm, not_leI, less_imp_neq, eq_neq_eq_imp_neq))
  | update "not_leI" thm thms =
    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
      eq_neq_eq_imp_neq) =>
    (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, thm, less_imp_neq, eq_neq_eq_imp_neq))
  | update "less_imp_neq" thm thms =
    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
      eq_neq_eq_imp_neq) =>
    (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, thm, eq_neq_eq_imp_neq))
  | update "eq_neq_eq_imp_neq" thm thms =
    change thms (fn (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq,
      eq_neq_eq_imp_neq) =>
    (less_reflE, le_refl, less_imp_le, eqI, eqD1, eqD2, less_trans,
      less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
      not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, thm));

(* Internal datatype for the proof *)
datatype proof
  = Asm of int
  | Thm of proof list * thm;

exception Cannot;
(* Internal exception, raised if conclusion cannot be derived from
     assumptions. *)
exception Contr of proof;
  (* Internal exception, raised if contradiction ( x < x ) was derived *)

fun prove asms =
  let
    fun pr (Asm i) = nth asms i
      | pr (Thm (prfs, thm)) = map pr prfs MRS thm;
  in pr end;

(* Internal datatype for inequalities *)
datatype less
   = Less  of term * term * proof
   | Le    of term * term * proof
   | NotEq of term * term * proof;

(* Misc functions for datatype less *)
fun lower (Less (x, _, _)) = x
  | lower (Le (x, _, _)) = x
  | lower (NotEq (x,_,_)) = x;

fun upper (Less (_, y, _)) = y
  | upper (Le (_, y, _)) = y
  | upper (NotEq (_,y,_)) = y;

fun getprf   (Less (_, _, p)) = p
|   getprf   (Le   (_, _, p)) = p
|   getprf   (NotEq (_,_, p)) = p;

(* ************************************************************************ *)
(*                                                                          *)
(* mkasm_partial                                                            *)
(*                                                                          *)
(* Tuple (t, n) (t an assumption, n its index in the assumptions) is        *)
(* translated to an element of type less.                                   *)
(* Partial orders only.                                                     *)
(*                                                                          *)
(* ************************************************************************ *)

fun mkasm_partial decomp (less_thms : less_arith) sign (n, t) =
  case decomp sign t of
    SOME (x, rel, y) => (case rel of
      "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], #less_reflE less_thms))
               else [Less (x, y, Asm n)]
    | "~<"  => []
    | "<="  => [Le (x, y, Asm n)]
    | "~<=" => []
    | "="   => [Le (x, y, Thm ([Asm n], #eqD1 less_thms)),
                Le (y, x, Thm ([Asm n], #eqD2 less_thms))]
    | "~="  => if (x aconv y) then
                  raise Contr (Thm ([(Thm ([(Thm ([], #le_refl less_thms)) ,(Asm n)], #le_neq_trans less_thms))], #less_reflE less_thms))
               else [ NotEq (x, y, Asm n),
                      NotEq (y, x,Thm ( [Asm n], #not_sym less_thms))]
    | _     => error ("partial_tac: unknown relation symbol ``" ^ rel ^
                 "''returned by decomp."))
  | NONE => [];

(* ************************************************************************ *)
(*                                                                          *)
(* mkasm_linear                                                             *)
(*                                                                          *)
(* Tuple (t, n) (t an assumption, n its index in the assumptions) is        *)
(* translated to an element of type less.                                   *)
(* Linear orders only.                                                      *)
(*                                                                          *)
(* ************************************************************************ *)

fun mkasm_linear decomp (less_thms : less_arith) sign (n, t) =
  case decomp sign t of
    SOME (x, rel, y) => (case rel of
      "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], #less_reflE less_thms))
               else [Less (x, y, Asm n)]
    | "~<"  => [Le (y, x, Thm ([Asm n], #not_lessD less_thms))]
    | "<="  => [Le (x, y, Asm n)]
    | "~<=" => if (x aconv y) then
                  raise (Contr (Thm ([Thm ([Asm n], #not_leD less_thms)], #less_reflE less_thms)))
               else [Less (y, x, Thm ([Asm n], #not_leD less_thms))]
    | "="   => [Le (x, y, Thm ([Asm n], #eqD1 less_thms)),
                Le (y, x, Thm ([Asm n], #eqD2 less_thms))]
    | "~="  => if (x aconv y) then
                  raise Contr (Thm ([(Thm ([(Thm ([], #le_refl less_thms)) ,(Asm n)], #le_neq_trans less_thms))], #less_reflE less_thms))
               else [ NotEq (x, y, Asm n),
                      NotEq (y, x,Thm ( [Asm n], #not_sym less_thms))]
    | _     => error ("linear_tac: unknown relation symbol ``" ^ rel ^
                 "''returned by decomp."))
  | NONE => [];

(* ************************************************************************ *)
(*                                                                          *)
(* mkconcl_partial                                                          *)
(*                                                                          *)
(* Translates conclusion t to an element of type less.                      *)
(* Partial orders only.                                                     *)
(*                                                                          *)
(* ************************************************************************ *)

fun mkconcl_partial decomp (less_thms : less_arith) sign t =
  case decomp sign t of
    SOME (x, rel, y) => (case rel of
      "<"   => ([Less (x, y, Asm ~1)], Asm 0)
    | "<="  => ([Le (x, y, Asm ~1)], Asm 0)
    | "="   => ([Le (x, y, Asm ~1), Le (y, x, Asm ~1)],
                 Thm ([Asm 0, Asm 1], #eqI less_thms))
    | "~="  => ([NotEq (x,y, Asm ~1)], Asm 0)
    | _  => raise Cannot)
  | NONE => raise Cannot;

(* ************************************************************************ *)
(*                                                                          *)
(* mkconcl_linear                                                           *)
(*                                                                          *)
(* Translates conclusion t to an element of type less.                      *)
(* Linear orders only.                                                      *)
(*                                                                          *)
(* ************************************************************************ *)

fun mkconcl_linear decomp (less_thms : less_arith) sign t =
  case decomp sign t of
    SOME (x, rel, y) => (case rel of
      "<"   => ([Less (x, y, Asm ~1)], Asm 0)
    | "~<"  => ([Le (y, x, Asm ~1)], Thm ([Asm 0], #not_lessI less_thms))
    | "<="  => ([Le (x, y, Asm ~1)], Asm 0)
    | "~<=" => ([Less (y, x, Asm ~1)], Thm ([Asm 0], #not_leI less_thms))
    | "="   => ([Le (x, y, Asm ~1), Le (y, x, Asm ~1)],
                 Thm ([Asm 0, Asm 1], #eqI less_thms))
    | "~="  => ([NotEq (x,y, Asm ~1)], Asm 0)
    | _  => raise Cannot)
  | NONE => raise Cannot;

(*** The common part for partial and linear orders ***)

(* Analysis of premises and conclusion: *)
(* decomp (`x Rel y') should yield (x, Rel, y)
     where Rel is one of "<", "<=", "~<", "~<=", "=" and "~=",
     other relation symbols cause an error message *)

fun gen_order_tac mkasm mkconcl decomp' (less_thms : less_arith) ctxt prems =

let

fun decomp sign t = Option.map (fn (x, rel, y) =>
  (Envir.beta_eta_contract x, rel, Envir.beta_eta_contract y)) (decomp' sign t);

(* ******************************************************************* *)
(*                                                                     *)
(* mergeLess                                                           *)
(*                                                                     *)
(* Merge two elements of type less according to the following rules    *)
(*                                                                     *)
(* x <  y && y <  z ==> x < z                                          *)
(* x <  y && y <= z ==> x < z                                          *)
(* x <= y && y <  z ==> x < z                                          *)
(* x <= y && y <= z ==> x <= z                                         *)
(* x <= y && x ~= y ==> x < y                                          *)
(* x ~= y && x <= y ==> x < y                                          *)
(* x <  y && x ~= y ==> x < y                                          *)
(* x ~= y && x <  y ==> x < y                                          *)
(*                                                                     *)
(* ******************************************************************* *)

fun mergeLess (Less (x, _, p) , Less (_ , z, q)) =
      Less (x, z, Thm ([p,q] , #less_trans less_thms))
|   mergeLess (Less (x, _, p) , Le (_ , z, q)) =
      Less (x, z, Thm ([p,q] , #less_le_trans less_thms))
|   mergeLess (Le (x, _, p) , Less (_ , z, q)) =
      Less (x, z, Thm ([p,q] , #le_less_trans less_thms))
|   mergeLess (Le (x, z, p) , NotEq (x', z', q)) =
      if (x aconv x' andalso z aconv z' )
      then Less (x, z, Thm ([p,q] , #le_neq_trans less_thms))
      else error "linear/partial_tac: internal error le_neq_trans"
|   mergeLess (NotEq (x, z, p) , Le (x' , z', q)) =
      if (x aconv x' andalso z aconv z')
      then Less (x, z, Thm ([p,q] , #neq_le_trans less_thms))
      else error "linear/partial_tac: internal error neq_le_trans"
|   mergeLess (NotEq (x, z, p) , Less (x' , z', q)) =
      if (x aconv x' andalso z aconv z')
      then Less ((x' , z', q))
      else error "linear/partial_tac: internal error neq_less_trans"
|   mergeLess (Less (x, z, p) , NotEq (x', z', q)) =
      if (x aconv x' andalso z aconv z')
      then Less (x, z, p)
      else error "linear/partial_tac: internal error less_neq_trans"
|   mergeLess (Le (x, _, p) , Le (_ , z, q)) =
      Le (x, z, Thm ([p,q] , #le_trans less_thms))
|   mergeLess (_, _) =
      error "linear/partial_tac: internal error: undefined case";

(* ******************************************************************** *)
(* tr checks for valid transitivity step                                *)
(* ******************************************************************** *)

infix tr;
fun (Less (_, y, _)) tr (Le (x', _, _)) = ( y aconv x' )
  | (Le   (_, y, _)) tr (Less (x', _, _)) = ( y aconv x' )
  | (Less (_, y, _)) tr (Less (x', _, _)) = ( y aconv x' )
  | (Le (_, y, _))   tr (Le (x', _, _)) = ( y aconv x' )
  | _ tr _ = false;

(* ******************************************************************* *)
(*                                                                     *)
(* transPath (Lesslist, Less): (less list * less) -> less              *)
(*                                                                     *)
(* If a path represented by a list of elements of type less is found,  *)
(* this needs to be contracted to a single element of type less.       *)
(* Prior to each transitivity step it is checked whether the step is   *)
(* valid.                                                              *)
(*                                                                     *)
(* ******************************************************************* *)

fun transPath ([],lesss) = lesss
|   transPath (x::xs,lesss) =
      if lesss tr x then transPath (xs, mergeLess(lesss,x))
      else error "linear/partial_tac: internal error transpath";

(* ******************************************************************* *)
(*                                                                     *)
(* less1 subsumes less2 : less -> less -> bool                         *)
(*                                                                     *)
(* subsumes checks whether less1 implies less2                         *)
(*                                                                     *)
(* ******************************************************************* *)

infix subsumes;
fun (Less (x, y, _)) subsumes (Le (x', y', _)) =
      (x aconv x' andalso y aconv y')
  | (Less (x, y, _)) subsumes (Less (x', y', _)) =
      (x aconv x' andalso y aconv y')
  | (Le (x, y, _)) subsumes (Le (x', y', _)) =
      (x aconv x' andalso y aconv y')
  | (Less (x, y, _)) subsumes (NotEq (x', y', _)) =
      (x aconv x' andalso y aconv y') orelse (y aconv x' andalso x aconv y')
  | (NotEq (x, y, _)) subsumes (NotEq (x', y', _)) =
      (x aconv x' andalso y aconv y') orelse (y aconv x' andalso x aconv y')
  | (Le _) subsumes (Less _) =
      error "linear/partial_tac: internal error: Le cannot subsume Less"
  | _ subsumes _ = false;

(* ******************************************************************* *)
(*                                                                     *)
(* triv_solv less1 : less ->  proof option                     *)
(*                                                                     *)
(* Solves trivial goal x <= x.                                         *)
(*                                                                     *)
(* ******************************************************************* *)

fun triv_solv (Le (x, x', _)) =
    if x aconv x' then SOME (Thm ([], #le_refl less_thms))
    else NONE
|   triv_solv _ = NONE;

(* ********************************************************************* *)
(* Graph functions                                                       *)
(* ********************************************************************* *)

(* ******************************************************************* *)
(*                                                                     *)
(* General:                                                            *)
(*                                                                     *)
(* Inequalities are represented by various types of graphs.            *)
(*                                                                     *)
(* 1. (Term.term * (Term.term * less) list) list                       *)
(*    - Graph of this type is generated from the assumptions,          *)
(*      it does contain information on which edge stems from which     *)
(*      assumption.                                                    *)
(*    - Used to compute strongly connected components                  *)
(*    - Used to compute component subgraphs                            *)
(*    - Used for component subgraphs to reconstruct paths in components*)
(*                                                                     *)
(* 2. (int * (int * less) list ) list                                  *)
(*    - Graph of this type is generated from the strong components of  *)
(*      graph of type 1.  It consists of the strong components of      *)
(*      graph 1, where nodes are indices of the components.            *)
(*      Only edges between components are part of this graph.          *)
(*    - Used to reconstruct paths between several components.          *)
(*                                                                     *)
(* ******************************************************************* *)

(* *********************************************************** *)
(* Functions for constructing graphs                           *)
(* *********************************************************** *)

fun addEdge (v,d,[]) = [(v,d)]
|   addEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el)
    else (u,dl):: (addEdge(v,d,el));

(* ********************************************************************* *)
(*                                                                       *)
(* mkGraphs constructs from a list of objects of type less a graph g,    *)
(* by taking all edges that are candidate for a <=, and a list neqE, by  *)
(* taking all edges that are candiate for a ~=                           *)
(*                                                                       *)
(* ********************************************************************* *)

fun mkGraphs [] = ([],[],[])
|   mkGraphs lessList =
let

fun buildGraphs ([],leqG,neqG,neqE) = (leqG, neqG, neqE)
|   buildGraphs (l::ls, leqG,neqG, neqE) = case l of
  (Less (x,y,p)) =>
       buildGraphs (ls, addEdge (x,[(y,(Less (x, y, p)))],leqG) ,
                        addEdge (x,[(y,(Less (x, y, p)))],neqG), l::neqE)
| (Le (x,y,p)) =>
      buildGraphs (ls, addEdge (x,[(y,(Le (x, y,p)))],leqG) , neqG, neqE)
| (NotEq  (x,y,p)) =>
      buildGraphs (ls, leqG , addEdge (x,[(y,(NotEq (x, y, p)))],neqG), l::neqE) ;

  in buildGraphs (lessList, [], [], []) end;

(* *********************************************************************** *)
(*                                                                         *)
(* adjacent g u : (''a * 'b list ) list -> ''a -> 'b list                  *)
(*                                                                         *)
(* List of successors of u in graph g                                      *)
(*                                                                         *)
(* *********************************************************************** *)

fun adjacent eq_comp ((v,adj)::el) u =
    if eq_comp (u, v) then adj else adjacent eq_comp el u
|   adjacent _  []  _ = []

(* *********************************************************************** *)
(*                                                                         *)
(* transpose g:                                                            *)
(* (''a * ''a list) list -> (''a * ''a list) list                          *)
(*                                                                         *)
(* Computes transposed graph g' from g                                     *)
(* by reversing all edges u -> v to v -> u                                 *)
(*                                                                         *)
(* *********************************************************************** *)

fun transpose eq_comp g =
  let
   (* Compute list of reversed edges for each adjacency list *)
   fun flip (u,(v,l)::el) = (v,(u,l)) :: flip (u,el)
     | flip (_,[]) = []

   (* Compute adjacency list for node u from the list of edges
      and return a likewise reduced list of edges.  The list of edges
      is searches for edges starting from u, and these edges are removed. *)
   fun gather (u,(v,w)::el) =
    let
     val (adj,edges) = gather (u,el)
    in
     if eq_comp (u, v) then (w::adj,edges)
     else (adj,(v,w)::edges)
    end
   | gather (_,[]) = ([],[])

   (* For every node in the input graph, call gather to find all reachable
      nodes in the list of edges *)
   fun assemble ((u,_)::el) edges =
       let val (adj,edges) = gather (u,edges)
       in (u,adj) :: assemble el edges
       end
     | assemble [] _ = []

   (* Compute, for each adjacency list, the list with reversed edges,
      and concatenate these lists. *)
   val flipped = maps flip g

in assemble g flipped end

(* *********************************************************************** *)
(*                                                                         *)
(* scc_term : (term * term list) list -> term list list                    *)
(*                                                                         *)
(* The following is based on the algorithm for finding strongly connected  *)
(* components described in Introduction to Algorithms, by Cormon, Leiserson*)
(* and Rivest, section 23.5. The input G is an adjacency list description  *)
(* of a directed graph. The output is a list of the strongly connected     *)
(* components (each a list of vertices).                                   *)
(*                                                                         *)
(*                                                                         *)
(* *********************************************************************** *)

fun scc_term G =
     let
  (* Ordered list of the vertices that DFS has finished with;
     most recently finished goes at the head. *)
  val finish : term list Unsynchronized.ref = Unsynchronized.ref []

  (* List of vertices which have been visited. *)
  val visited : term list Unsynchronized.ref = Unsynchronized.ref []

  fun been_visited v = exists (fn w => w aconv v) (!visited)

  (* Given the adjacency list rep of a graph (a list of pairs),
     return just the first element of each pair, yielding the
     vertex list. *)
  val members = map (fn (v,_) => v)

  (* Returns the nodes in the DFS tree rooted at u in g *)
  fun dfs_visit g u : term list =
      let
   val _ = visited := u :: !visited
   val descendents =
       List.foldr (fn ((v,l),ds) => if been_visited v then ds
            else v :: dfs_visit g v @ ds)
        [] (adjacent (op aconv) g u)
      in
   finish := u :: !finish;
   descendents
      end
     in

  (* DFS on the graph; apply dfs_visit to each vertex in
     the graph, checking first to make sure the vertex is
     as yet unvisited. *)
  List.app (fn u => if been_visited u then ()
        else (dfs_visit G u; ()))  (members G);
  visited := [];

  (* We don't reset finish because its value is used by
     foldl below, and it will never be used again (even
     though dfs_visit will continue to modify it). *)

  (* DFS on the transpose. The vertices returned by
     dfs_visit along with u form a connected component. We
     collect all the connected components together in a
     list, which is what is returned. *)
  fold (fn u => fn comps =>
      if been_visited u then comps
      else (u :: dfs_visit (transpose (op aconv) G) u) :: comps) (!finish) []
end;

(* *********************************************************************** *)
(*                                                                         *)
(* dfs_int_reachable g u:                                                  *)
(* (int * int list) list -> int -> int list                                *)
(*                                                                         *)
(* Computes list of all nodes reachable from u in g.                       *)
(*                                                                         *)
(* *********************************************************************** *)

fun dfs_int_reachable g u =
let
  (* List of vertices which have been visited. *)
  val visited : int list Unsynchronized.ref = Unsynchronized.ref []

  fun been_visited v = exists (fn w => w = v) (!visited)

  fun dfs_visit g u : int list =
      let
   val _ = visited := u :: !visited
   val descendents =
       List.foldr (fn ((v,l),ds) => if been_visited v then ds
            else v :: dfs_visit g v @ ds)
        [] (adjacent (op =) g u)
   in  descendents end

in u :: dfs_visit g u end;

fun indexNodes IndexComp =
    maps (fn (index, comp) => (map (fn v => (v,index)) comp)) IndexComp;

fun getIndex v [] = ~1
|   getIndex v ((v',k)::vs) = if v aconv v' then k else getIndex v vs;

(* *********************************************************************** *)
(*                                                                         *)
(* dfs eq_comp g u v:                                                       *)
(* ('a * 'a -> bool) -> ('a  *( 'a * less) list) list ->                   *)
(* 'a -> 'a -> (bool * ('a * less) list)                                   *)
(*                                                                         *)
(* Depth first search of v from u.                                         *)
(* Returns (true, path(u, v)) if successful, otherwise (false, []).        *)
(*                                                                         *)
(* *********************************************************************** *)

fun dfs eq_comp g u v =
let
    val pred = Unsynchronized.ref [];
    val visited = Unsynchronized.ref [];

    fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)

    fun dfs_visit u' =
    let val _ = visited := u' :: (!visited)

    fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;

    in if been_visited v then ()
    else (List.app (fn (v',l) => if been_visited v' then () else (
       update (v',l);
       dfs_visit v'; ()) )) (adjacent eq_comp g u')
     end
  in
    dfs_visit u;
    if (been_visited v) then (true, (!pred)) else (false , [])
  end;

(* *********************************************************************** *)
(*                                                                         *)
(* completeTermPath u v g:                                                 *)
(* Term.term -> Term.term -> (Term.term * (Term.term * less) list) list    *)
(* -> less list                                                            *)
(*                                                                         *)
(* Complete the path from u to v in graph g.  Path search is performed     *)
(* with dfs_term g u v.  This yields for each node v' its predecessor u'   *)
(* and the edge u' -> v'.  Allows traversing graph backwards from v and    *)
(* finding the path u -> v.                                                *)
(*                                                                         *)
(* *********************************************************************** *)

fun completeTermPath u v g  =
  let
   val (found, tmp) =  dfs (op aconv) g u v ;
   val pred = map snd tmp;

   fun path x y  =
      let

      (* find predecessor u of node v and the edge u -> v *)

      fun lookup v [] = raise Cannot
      |   lookup v (e::es) = if (upper e) aconv v then e else lookup v es;

      (* traverse path backwards and return list of visited edges *)
      fun rev_path v =
       let val l = lookup v pred
           val u = lower l;
       in
        if u aconv x then [l]
        else (rev_path u) @ [l]
       end
     in rev_path y end;

  in
  if found then (if u aconv v then [(Le (u, v, (Thm ([], #le_refl less_thms))))]
  else path u v ) else raise Cannot
end;

(* *********************************************************************** *)
(*                                                                         *)
(* findProof (sccGraph, neqE, ntc, sccSubgraphs) subgoal:                  *)
(*                                                                         *)
(* (int * (int * less) list) list * less list *  (Term.term * int) list    *)
(* * ((term * (term * less) list) list) list -> Less -> proof              *)
(*                                                                         *)
(* findProof constructs from graphs (sccGraph, sccSubgraphs) and neqE a    *)
(* proof for subgoal.  Raises exception Cannot if this is not possible.    *)
(*                                                                         *)
(* *********************************************************************** *)

fun findProof (sccGraph, neqE, ntc, sccSubgraphs) subgoal =
let

(* complete path x y from component graph *)
fun completeComponentPath x y predlist =
   let
          val xi = getIndex x ntc
          val yi = getIndex y ntc

          fun lookup k [] =  raise Cannot
          |   lookup k ((h: int,l)::us) = if k = h then l else lookup k us;

          fun rev_completeComponentPath y' =
           let val edge = lookup (getIndex y' ntc) predlist
               val u = lower edge
               val v = upper edge
           in
             if (getIndex u ntc) = xi then
               completeTermPath x u (nth sccSubgraphs xi) @ [edge] @
               completeTermPath v y' (nth sccSubgraphs (getIndex y' ntc))
             else
              rev_completeComponentPath u @ [edge] @
                completeTermPath v y' (nth sccSubgraphs (getIndex y' ntc))
           end
   in
     if x aconv y then
       [(Le (x, y, (Thm ([], #le_refl less_thms))))]
     else if xi = yi then completeTermPath x y (nth sccSubgraphs xi)
     else rev_completeComponentPath y
   end;

(* ******************************************************************* *)
(* findLess e x y xi yi xreachable yreachable                          *)
(*                                                                     *)
(* Find a path from x through e to y, of weight <                      *)
(* ******************************************************************* *)

fun findLess e x y xi yi xreachable yreachable =
  let val u = lower e
      val v = upper e
      val ui = getIndex u ntc
      val vi = getIndex v ntc

  in
      if member (op =) xreachable ui andalso member (op =) xreachable vi andalso
         member (op =) yreachable ui andalso member (op =) yreachable vi then (

  (case e of (Less (_, _, _)) =>
       let
        val (xufound, xupred) =  dfs (op =) sccGraph xi (getIndex u ntc)
            in
             if xufound then (
              let
               val (vyfound, vypred) =  dfs (op =) sccGraph (getIndex v ntc) yi
              in
               if vyfound then (
                let
                 val xypath = (completeComponentPath x u xupred)@[e]@(completeComponentPath v y vypred)
                 val xyLesss = transPath (tl xypath, hd xypath)
                in
                 if xyLesss subsumes subgoal then SOME (getprf xyLesss)
                 else NONE
               end)
               else NONE
              end)
             else NONE
            end
       |  _   =>
         let val (uvfound, uvpred) =  dfs (op =) sccGraph (getIndex u ntc) (getIndex v ntc)
             in
              if uvfound then (
               let
                val (xufound, xupred) = dfs (op =) sccGraph xi (getIndex u ntc)
               in
                if xufound then (
                 let
                  val (vyfound, vypred) =  dfs (op =) sccGraph (getIndex v ntc) yi
                 in
                  if vyfound then (
                   let
                    val uvpath = completeComponentPath u v uvpred
                    val uvLesss = mergeLess ( transPath (tl uvpath, hd uvpath), e)
                    val xypath = (completeComponentPath  x u xupred)@[uvLesss]@(completeComponentPath v y vypred)
                    val xyLesss = transPath (tl xypath, hd xypath)
                   in
                    if xyLesss subsumes subgoal then SOME (getprf xyLesss)
                    else NONE
                   end )
                  else NONE
                 end)
                else NONE
               end )
              else NONE
             end )
    ) else NONE
end;

in
  (* looking for x <= y: any path from x to y is sufficient *)
  case subgoal of (Le (x, y, _)) => (
  if null sccGraph then raise Cannot else (
   let
    val xi = getIndex x ntc
    val yi = getIndex y ntc
    (* searches in sccGraph a path from xi to yi *)
    val (found, pred) = dfs (op =) sccGraph xi yi
   in
    if found then (
       let val xypath = completeComponentPath x y pred
           val xyLesss = transPath (tl xypath, hd xypath)
       in
          (case xyLesss of
            (Less (_, _, q)) => if xyLesss subsumes subgoal then (Thm ([q], #less_imp_le less_thms))
                                else raise Cannot
             | _   => if xyLesss subsumes subgoal then (getprf xyLesss)
                      else raise Cannot)
       end )
     else raise Cannot
   end
    )
   )
(* looking for x < y: particular path required, which is not necessarily
    found by normal dfs *)
|   (Less (x, y, _)) => (
  if null sccGraph then raise Cannot else (
   let
    val xi = getIndex x ntc
    val yi = getIndex y ntc
    val sccGraph_transpose = transpose (op =) sccGraph
    (* all components that can be reached from component xi  *)
    val xreachable = dfs_int_reachable sccGraph xi
    (* all comonents reachable from y in the transposed graph sccGraph' *)
    val yreachable = dfs_int_reachable sccGraph_transpose yi
    (* for all edges u ~= v or u < v check if they are part of path x < y *)
    fun processNeqEdges [] = raise Cannot
    |   processNeqEdges (e::es) =
      case  (findLess e x y xi yi xreachable yreachable) of (SOME prf) => prf
      | _ => processNeqEdges es

    in
       processNeqEdges neqE
    end
  )
)
| (NotEq (x, y, _)) => (
  (* if there aren't any edges that are candidate for a ~= raise Cannot *)
  if null neqE then raise Cannot
  (* if there aren't any edges that are candidate for <= then just search a edge in neqE that implies the subgoal *)
  else if null sccSubgraphs then (
     (case (find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of
       ( SOME (NotEq (x, y, p)), NotEq (x', y', _)) =>
          if  (x aconv x' andalso y aconv y') then p
          else Thm ([p], #not_sym less_thms)
     | ( SOME (Less (x, y, p)), NotEq (x', y', _)) =>
          if x aconv x' andalso y aconv y' then (Thm ([p], #less_imp_neq less_thms))
          else (Thm ([(Thm ([p], #less_imp_neq less_thms))], #not_sym less_thms))
     | _ => raise Cannot)
   ) else (

   let  val xi = getIndex x ntc
        val yi = getIndex y ntc
        val sccGraph_transpose = transpose (op =) sccGraph
        val xreachable = dfs_int_reachable sccGraph xi
        val yreachable = dfs_int_reachable sccGraph_transpose yi

        fun processNeqEdges [] = raise Cannot
        |   processNeqEdges (e::es) = (
            let val u = lower e
                val v = upper e
                val ui = getIndex u ntc
                val vi = getIndex v ntc

            in
                (* if x ~= y follows from edge e *)
                if e subsumes subgoal then (
                     case e of (Less (u, v, q)) => (
                       if u aconv x andalso v aconv y then (Thm ([q], #less_imp_neq less_thms))
                       else (Thm ([(Thm ([q], #less_imp_neq less_thms))], #not_sym less_thms))
                     )
                     |    (NotEq (u,v, q)) => (
                       if u aconv x andalso v aconv y then q
                       else (Thm ([q],  #not_sym less_thms))
                     )
                 )
                (* if SCC_x is linked to SCC_y via edge e *)
                 else if ui = xi andalso vi = yi then (
                   case e of (Less (_, _,_)) => (
                        let
                          val xypath =
                            completeTermPath x u (nth sccSubgraphs ui) @ [e] @
                            completeTermPath v y (nth sccSubgraphs vi)
                          val xyLesss = transPath (tl xypath, hd xypath)
                        in  (Thm ([getprf xyLesss], #less_imp_neq less_thms)) end)
                   | _ => (
                        let
                            val xupath = completeTermPath x u (nth sccSubgraphs ui)
                            val uxpath = completeTermPath u x (nth sccSubgraphs ui)
                            val vypath = completeTermPath v y (nth sccSubgraphs vi)
                            val yvpath = completeTermPath y v (nth sccSubgraphs vi)
                            val xuLesss = transPath (tl xupath, hd xupath)
                            val uxLesss = transPath (tl uxpath, hd uxpath)
                            val vyLesss = transPath (tl vypath, hd vypath)
                            val yvLesss = transPath (tl yvpath, hd yvpath)
                            val x_eq_u =  (Thm ([(getprf xuLesss),(getprf uxLesss)], #eqI less_thms))
                            val v_eq_y =  (Thm ([(getprf vyLesss),(getprf yvLesss)], #eqI less_thms))
                        in
                           (Thm ([x_eq_u , (getprf e), v_eq_y ], #eq_neq_eq_imp_neq less_thms))
                        end
                        )
                  ) else if ui = yi andalso vi = xi then (
                     case e of (Less (_, _,_)) => (
                        let
                          val xypath =
                            completeTermPath y u (nth sccSubgraphs ui) @ [e] @
                            completeTermPath v x (nth sccSubgraphs vi)
                          val xyLesss = transPath (tl xypath, hd xypath)
                        in (Thm ([(Thm ([getprf xyLesss], #less_imp_neq less_thms))] , #not_sym less_thms)) end )
                     | _ => (

                        let val yupath = completeTermPath y u (nth sccSubgraphs ui)
                            val uypath = completeTermPath u y (nth sccSubgraphs ui)
                            val vxpath = completeTermPath v x (nth sccSubgraphs vi)
                            val xvpath = completeTermPath x v (nth sccSubgraphs vi)
                            val yuLesss = transPath (tl yupath, hd yupath)
                            val uyLesss = transPath (tl uypath, hd uypath)
                            val vxLesss = transPath (tl vxpath, hd vxpath)
                            val xvLesss = transPath (tl xvpath, hd xvpath)
                            val y_eq_u =  (Thm ([(getprf yuLesss),(getprf uyLesss)], #eqI less_thms))
                            val v_eq_x =  (Thm ([(getprf vxLesss),(getprf xvLesss)], #eqI less_thms))
                        in
                            (Thm ([(Thm ([y_eq_u , (getprf e), v_eq_x ], #eq_neq_eq_imp_neq less_thms))], #not_sym less_thms))
                        end
                       )
                  ) else (
                       (* there exists a path x < y or y < x such that
                          x ~= y may be concluded *)
                        case  (findLess e x y xi yi xreachable yreachable) of
                              (SOME prf) =>  (Thm ([prf], #less_imp_neq less_thms))
                             | NONE =>  (
                               let
                                val yr = dfs_int_reachable sccGraph yi
                                val xr = dfs_int_reachable sccGraph_transpose xi
                               in
                                case  (findLess e y x yi xi yr xr) of
                                      (SOME prf) => (Thm ([(Thm ([prf], #less_imp_neq less_thms))], #not_sym less_thms))
                                      | _ => processNeqEdges es
                               end)
                 ) end)
     in processNeqEdges neqE end)
  )
end;

(* ******************************************************************* *)
(*                                                                     *)
(* mk_sccGraphs components leqG neqG ntc :                             *)
(* Term.term list list ->                                              *)
(* (Term.term * (Term.term * less) list) list ->                       *)
(* (Term.term * (Term.term * less) list) list ->                       *)
(* (Term.term * int)  list ->                                          *)
(* (int * (int * less) list) list   *                                  *)
(* ((Term.term * (Term.term * less) list) list) list                   *)
(*                                                                     *)
(*                                                                     *)
(* Computes, from graph leqG, list of all its components and the list  *)
(* ntc (nodes, index of component) a graph whose nodes are the         *)
(* indices of the components of g.  Egdes of the new graph are         *)
(* only the edges of g linking two components. Also computes for each  *)
(* component the subgraph of leqG that forms this component.           *)
(*                                                                     *)
(* For each component SCC_i is checked if there exists a edge in neqG  *)
(* that leads to a contradiction.                                      *)
(*                                                                     *)
(* We have a contradiction for edge u ~= v and u < v if:               *)
(* - u and v are in the same component,                                *)
(* that is, a path u <= v and a path v <= u exist, hence u = v.        *)
(* From irreflexivity of < follows u < u or v < v. Ex false quodlibet. *)
(*                                                                     *)
(* ******************************************************************* *)

fun mk_sccGraphs _ [] _ _ = ([],[])
|   mk_sccGraphs components leqG neqG ntc =
    let
    (* Liste (Index der Komponente, Komponente *)
    val IndexComp = map_index I components;

    fun handleContr edge g =
       (case edge of
          (Less  (x, y, _)) => (
            let
             val xxpath = edge :: (completeTermPath y x g )
             val xxLesss = transPath (tl xxpath, hd xxpath)
             val q = getprf xxLesss
            in
             raise (Contr (Thm ([q], #less_reflE less_thms )))
            end
          )
        | (NotEq (x, y, _)) => (
            let
             val xypath = (completeTermPath x y g )
             val yxpath = (completeTermPath y x g )
             val xyLesss = transPath (tl xypath, hd xypath)
             val yxLesss = transPath (tl yxpath, hd yxpath)
             val q = getprf (mergeLess ((mergeLess (edge, xyLesss)),yxLesss ))
            in
             raise (Contr (Thm ([q], #less_reflE less_thms )))
            end
         )
        | _ =>  error "trans_tac/handleContr: invalid Contradiction");

    (* k is index of the actual component *)

    fun processComponent (k, comp) =
     let
        (* all edges with weight <= of the actual component *)
        val leqEdges = maps (adjacent (op aconv) leqG) comp;
        (* all edges with weight ~= of the actual component *)
        val neqEdges = map snd (maps (adjacent (op aconv) neqG) comp);

       (* find an edge leading to a contradiction *)
       fun findContr [] = NONE
       |   findContr (e::es) =
                    let val ui = (getIndex (lower e) ntc)
                        val vi = (getIndex (upper e) ntc)
                    in
                        if ui = vi then  SOME e
                        else findContr es
                    end;

                (* sort edges into component internal edges and
                   edges pointing away from the component *)
                fun sortEdges  [] (intern,extern)  = (intern,extern)
                |   sortEdges  ((v,l)::es) (intern, extern) =
                    let val k' = getIndex v ntc in
                        if k' = k then
                            sortEdges es (l::intern, extern)
                        else sortEdges  es (intern, (k',l)::extern) end;

                (* Insert edge into sorted list of edges, where edge is
                    only added if
                    - it is found for the first time
                    - it is a <= edge and no parallel < edge was found earlier
                    - it is a < edge
                 *)
                 fun insert (h: int,l) [] = [(h,l)]
                 |   insert (h,l) ((k',l')::es) = if h = k' then (
                     case l of (Less (_, _, _)) => (h,l)::es
                     | _  => (case l' of (Less (_, _, _)) => (h,l')::es
                              | _ => (k',l)::es) )
                     else (k',l'):: insert (h,l) es;

                (* Reorganise list of edges such that
                    - duplicate edges are removed
                    - if a < edge and a <= edge exist at the same time,
                      remove <= edge *)
                 fun reOrganizeEdges [] sorted = sorted: (int * less) list
                 |   reOrganizeEdges (e::es) sorted = reOrganizeEdges es (insert e sorted);

                 (* construct the subgraph forming the strongly connected component
                    from the edge list *)
                 fun sccSubGraph [] g  = g
                 |   sccSubGraph (l::ls) g =
                          sccSubGraph ls (addEdge ((lower l),[((upper l),l)],g))

                 val (intern, extern) = sortEdges leqEdges ([], []);
                 val subGraph = sccSubGraph intern [];

     in
         case findContr neqEdges of SOME e => handleContr e subGraph
         | _ => ((k, (reOrganizeEdges (extern) [])), subGraph)
     end;

    val tmp =  map processComponent IndexComp
in
     ( (map fst tmp), (map snd tmp))
end;

(** Find proof if possible. **)

fun gen_solve mkconcl sign (asms, concl) =
let
  val (leqG, neqG, neqE) = mkGraphs asms
  val components = scc_term leqG
  val ntc = indexNodes (map_index I components)
  val (sccGraph, sccSubgraphs) = mk_sccGraphs components leqG neqG ntc
in
   let
   val (subgoals, prf) = mkconcl decomp less_thms sign concl
   fun solve facts less =
      (case triv_solv less of NONE => findProof (sccGraph, neqE, ntc, sccSubgraphs) less
      | SOME prf => prf )
  in
   map (solve asms) subgoals
  end
end;

in
SUBGOAL (fn (A, n) => fn st =>
  let
   val thy = Proof_Context.theory_of ctxt;
   val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
   val Hs =
    map Thm.prop_of prems @
    map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
   val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
   val lesss = flat (map_index (mkasm decomp less_thms thy) Hs)
   val prfs = gen_solve mkconcl thy (lesss, C);
   val (subgoals, prf) = mkconcl decomp less_thms thy C;
  in
   Subgoal.FOCUS (fn {context = ctxt', prems = asms, ...} =>
     let val thms = map (prove (prems @ asms)) prfs
     in resolve_tac ctxt' [prove thms prf] 1 end) ctxt n st
  end
  handle Contr p =>
      (Subgoal.FOCUS (fn {context = ctxt', prems = asms, ...} =>
          resolve_tac ctxt' [prove asms p] 1) ctxt n st
        handle General.Subscript => Seq.empty)
   | Cannot => Seq.empty
   | General.Subscript => Seq.empty)
end;

(* partial_tac - solves partial orders *)
val partial_tac = gen_order_tac mkasm_partial mkconcl_partial;

(* linear_tac - solves linear/total orders *)
val linear_tac = gen_order_tac mkasm_linear mkconcl_linear;

end;

¤ Dauer der Verarbeitung: 0.31 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.