--- a/src/Provers/order.ML Wed Mar 31 11:24:46 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1264 +0,0 @@
-(* 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;