New transitivity reasoners for transitivity only and quasi orders.
authorballarin
Tue Aug 03 14:47:51 2004 +0200 (2004-08-03)
changeset 1510379846e8792eb
parent 15102 04b0e943fcc9
child 15104 f14e0d9587be
New transitivity reasoners for transitivity only and quasi orders.
NEWS
src/HOL/HOL.thy
src/HOL/IsaMakefile
src/HOL/ROOT.ML
src/Provers/order.ML
src/Provers/quasi.ML
     1.1 --- a/NEWS	Tue Aug 03 13:48:00 2004 +0200
     1.2 +++ b/NEWS	Tue Aug 03 14:47:51 2004 +0200
     1.3 @@ -6,6 +6,9 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* Provers/quasi.ML:  new transitivity reasoners for transitivity only
     1.8 +  and quasi orders.
     1.9 +
    1.10  * Provers/trancl.ML:  new transitivity reasoner for transitive and
    1.11    reflexive-transitive closure of relations.
    1.12  
     2.1 --- a/src/HOL/HOL.thy	Tue Aug 03 13:48:00 2004 +0200
     2.2 +++ b/src/HOL/HOL.thy	Tue Aug 03 14:47:51 2004 +0200
     2.3 @@ -986,7 +986,49 @@
     2.4  
     2.5  ML_setup {*
     2.6  
     2.7 -structure Trans_Tac = Trans_Tac_Fun (
     2.8 +(* The setting up of Quasi_Tac serves as a demo.  Since there is no
     2.9 +   class for quasi orders, the tactics Quasi_Tac.trans_tac and
    2.10 +   Quasi_Tac.quasi_tac are not of much use. *)
    2.11 +
    2.12 +structure Quasi_Tac = Quasi_Tac_Fun (
    2.13 +  struct
    2.14 +    val le_trans = thm "order_trans";
    2.15 +    val le_refl = thm "order_refl";
    2.16 +    val eqD1 = thm "order_eq_refl";
    2.17 +    val eqD2 = thm "sym" RS thm "order_eq_refl";
    2.18 +    val less_reflE = thm "order_less_irrefl" RS thm "notE";
    2.19 +    val less_imp_le = thm "order_less_imp_le";
    2.20 +    val le_neq_trans = thm "order_le_neq_trans";
    2.21 +    val neq_le_trans = thm "order_neq_le_trans";
    2.22 +    val less_imp_neq = thm "less_imp_neq";
    2.23 +
    2.24 +    fun decomp_gen sort sign (Trueprop $ t) =
    2.25 +      let fun of_sort t = Sign.of_sort sign (type_of t, sort)
    2.26 +      fun dec (Const ("Not", _) $ t) = (
    2.27 +              case dec t of
    2.28 +                None => None
    2.29 +              | Some (t1, rel, t2) => Some (t1, "~" ^ rel, t2))
    2.30 +            | dec (Const ("op =",  _) $ t1 $ t2) = 
    2.31 +                if of_sort t1
    2.32 +                then Some (t1, "=", t2)
    2.33 +                else None
    2.34 +            | dec (Const ("op <=",  _) $ t1 $ t2) = 
    2.35 +                if of_sort t1
    2.36 +                then Some (t1, "<=", t2)
    2.37 +                else None
    2.38 +            | dec (Const ("op <",  _) $ t1 $ t2) = 
    2.39 +                if of_sort t1
    2.40 +                then Some (t1, "<", t2)
    2.41 +                else None
    2.42 +            | dec _ = None
    2.43 +      in dec t end;
    2.44 +
    2.45 +    val decomp_trans = decomp_gen ["HOL.order"];
    2.46 +    val decomp_quasi = decomp_gen ["HOL.order"];
    2.47 +
    2.48 +  end);  (* struct *)
    2.49 +
    2.50 +structure Order_Tac = Order_Tac_Fun (
    2.51    struct
    2.52      val less_reflE = thm "order_less_irrefl" RS thm "notE";
    2.53      val le_refl = thm "order_refl";
    2.54 @@ -1034,26 +1076,29 @@
    2.55    end);  (* struct *)
    2.56  
    2.57  simpset_ref() := simpset ()
    2.58 -    addSolver (mk_solver "Trans_linear" (fn _ => Trans_Tac.linear_tac))
    2.59 -    addSolver (mk_solver "Trans_partial" (fn _ => Trans_Tac.partial_tac));
    2.60 +    addSolver (mk_solver "Trans_linear" (fn _ => Order_Tac.linear_tac))
    2.61 +    addSolver (mk_solver "Trans_partial" (fn _ => Order_Tac.partial_tac));
    2.62    (* Adding the transitivity reasoners also as safe solvers showed a slight
    2.63       speed up, but the reasoning strength appears to be not higher (at least
    2.64       no breaking of additional proofs in the entire HOL distribution, as
    2.65       of 5 March 2004, was observed). *)
    2.66  *}
    2.67  
    2.68 -(* Optional methods
    2.69 +(* Optional setup of methods *)
    2.70  
    2.71 +(*
    2.72  method_setup trans_partial =
    2.73 -  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (trans_tac_partial)) *}
    2.74 -  {* simple transitivity reasoner *}	    
    2.75 +  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (Order_Tac.partial_tac)) *}
    2.76 +  {* transitivity reasoner for partial orders *}	    
    2.77  method_setup trans_linear =
    2.78 -  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (trans_tac_linear)) *}
    2.79 -  {* simple transitivity reasoner *}
    2.80 +  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (Order_Tac.linear_tac)) *}
    2.81 +  {* transitivity reasoner for linear orders *}
    2.82  *)
    2.83  
    2.84  (*
    2.85  declare order.order_refl [simp del] order_less_irrefl [simp del]
    2.86 +
    2.87 +can currently not be removed, abel_cancel relies on it.
    2.88  *)
    2.89  
    2.90  subsubsection "Bounded quantifiers"
     3.1 --- a/src/HOL/IsaMakefile	Tue Aug 03 13:48:00 2004 +0200
     3.2 +++ b/src/HOL/IsaMakefile	Tue Aug 03 14:47:51 2004 +0200
     3.3 @@ -77,6 +77,7 @@
     3.4    $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
     3.5    $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/induct_method.ML \
     3.6    $(SRC)/Provers/make_elim.ML $(SRC)/Provers/order.ML \
     3.7 +  $(SRC)/Provers/quasi.ML \
     3.8    $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML \
     3.9    $(SRC)/Provers/trancl.ML \
    3.10    $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML $(SRC)/TFL/rules.ML \
     4.1 --- a/src/HOL/ROOT.ML	Tue Aug 03 13:48:00 2004 +0200
     4.2 +++ b/src/HOL/ROOT.ML	Tue Aug 03 14:47:51 2004 +0200
     4.3 @@ -34,6 +34,7 @@
     4.4  use "~~/src/Provers/Arith/cancel_numeral_factor.ML";
     4.5  use "~~/src/Provers/Arith/extract_common_term.ML";
     4.6  use "~~/src/Provers/Arith/cancel_div_mod.ML";
     4.7 +use "~~/src/Provers/quasi.ML";
     4.8  use "~~/src/Provers/order.ML";
     4.9  
    4.10  with_path "Integ" use_thy "Main";
     5.1 --- a/src/Provers/order.ML	Tue Aug 03 13:48:00 2004 +0200
     5.2 +++ b/src/Provers/order.ML	Tue Aug 03 14:47:51 2004 +0200
     5.3 @@ -9,7 +9,7 @@
     5.4  
     5.5  (*
     5.6  
     5.7 -The packages provides tactics partial_tac and linear_tac that use all
     5.8 +The package provides tactics partial_tac and linear_tac that use all
     5.9  premises of the form
    5.10  
    5.11    t = u, t ~= u, t < u, t <= u, ~(t < u) and ~(t <= u)
    5.12 @@ -56,21 +56,22 @@
    5.13    val eq_neq_eq_imp_neq : thm (* [| x = u ; u ~= v ; v = z|] ==> x ~= z *)
    5.14  
    5.15    (* Analysis of premises and conclusion *)
    5.16 -  (* decomp_part is for partial_tac, decomp_lin is for linear_tac;
    5.17 -     decomp_x (`x Rel y') should yield (x, Rel, y)
    5.18 +  (* decomp_x (`x Rel y') should yield (x, Rel, y)
    5.19         where Rel is one of "<", "<=", "~<", "~<=", "=" and "~=",
    5.20         other relation symbols cause an error message *)
    5.21 +  (* decomp_part is used by partial_tac *)
    5.22    val decomp_part: Sign.sg -> term -> (term * string * term) option
    5.23 +  (* decomp_lin is used by linear_tac *)
    5.24    val decomp_lin: Sign.sg -> term -> (term * string * term) option
    5.25  end;
    5.26  
    5.27 -signature TRANS_TAC  =
    5.28 +signature ORDER_TAC  =
    5.29  sig
    5.30    val partial_tac: int -> tactic
    5.31    val linear_tac:  int -> tactic
    5.32  end;
    5.33  
    5.34 -functor Trans_Tac_Fun (Less: LESS_ARITH): TRANS_TAC =
    5.35 +functor Order_Tac_Fun (Less: LESS_ARITH): ORDER_TAC =
    5.36  struct
    5.37  
    5.38  (* Extract subgoal with signature *)
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Provers/quasi.ML	Tue Aug 03 14:47:51 2004 +0200
     6.3 @@ -0,0 +1,598 @@
     6.4 +(* 
     6.5 +   Title:	Reasoner for simple transitivity and quasi orders. 
     6.6 +   Id:		$Id$
     6.7 +   Author:	Oliver Kutter
     6.8 +   Copyright:	TU Muenchen
     6.9 + *)
    6.10 +
    6.11 +(* 
    6.12 + 
    6.13 +The package provides tactics trans_tac and quasi_tac that use
    6.14 +premises of the form 
    6.15 +
    6.16 +  t = u, t ~= u, t < u and t <= u
    6.17 +
    6.18 +to
    6.19 +- either derive a contradiction, in which case the conclusion can be
    6.20 +  any term,
    6.21 +- or prove the concluson, which must be of the form t ~= u, t < u or
    6.22 +  t <= u.
    6.23 +
    6.24 +Details:
    6.25 +
    6.26 +1. trans_tac:
    6.27 +   Only premises of form t <= u are used and the conclusion must be of
    6.28 +   the same form.  The conclusion is proved, if possible, by a chain of
    6.29 +   transitivity from the assumptions.
    6.30 +
    6.31 +2. quasi_tac:
    6.32 +   <= is assumed to be a quasi order and < its strict relative, defined
    6.33 +   as t < u == t <= u & t ~= u.  Again, the conclusion is proved from
    6.34 +   the assumptions.
    6.35 +   Note that the presence of a strict relation is not necessary for
    6.36 +   quasi_tac.  Configure decomp_quasi to ignore < and ~=.  A list of
    6.37 +   required theorems for both situations is given below. 
    6.38 +*)
    6.39 +
    6.40 +signature LESS_ARITH =
    6.41 +sig
    6.42 +  (* Transitivity of <=
    6.43 +     Note that transitivities for < hold for partial orders only. *) 
    6.44 +  val le_trans: thm  (* [| x <= y; y <= z |] ==> x <= z *)
    6.45 + 
    6.46 +  (* Additional theorem for quasi orders *)
    6.47 +  val le_refl: thm  (* x <= x *)
    6.48 +  val eqD1: thm (* x = y ==> x <= y *)
    6.49 +  val eqD2: thm (* x = y ==> y <= x *)
    6.50 +
    6.51 +  (* Additional theorems for premises of the form x < y *)
    6.52 +  val less_reflE: thm  (* x < x ==> P *)
    6.53 +  val less_imp_le : thm (* x < y ==> x <= y *)
    6.54 +
    6.55 +  (* Additional theorems for premises of the form x ~= y *)
    6.56 +  val le_neq_trans : thm (* [| x <= y ; x ~= y |] ==> x < y *)
    6.57 +  val neq_le_trans : thm (* [| x ~= y ; x <= y |] ==> x < y *)
    6.58 +
    6.59 +  (* Additional theorem for goals of form x ~= y *)
    6.60 +  val less_imp_neq : thm (* x < y ==> x ~= y *)
    6.61 +
    6.62 +  (* Analysis of premises and conclusion *)
    6.63 +  (* decomp_x (`x Rel y') should yield Some (x, Rel, y)
    6.64 +       where Rel is one of "<", "<=", "=" and "~=",
    6.65 +       other relation symbols cause an error message *)
    6.66 +  (* decomp_trans is used by trans_tac, it may only return Rel = "<=" *)
    6.67 +  val decomp_trans: Sign.sg -> term -> (term * string * term) option
    6.68 +  (* decomp_quasi is used by quasi_tac *)
    6.69 +  val decomp_quasi: Sign.sg -> term -> (term * string * term) option
    6.70 +end;
    6.71 +
    6.72 +signature QUASI_TAC = 
    6.73 +sig
    6.74 +  val trans_tac: int -> tactic
    6.75 +  val quasi_tac: int -> tactic
    6.76 +end;
    6.77 +
    6.78 +functor Quasi_Tac_Fun (Less: LESS_ARITH): QUASI_TAC =
    6.79 +struct
    6.80 +
    6.81 +(* Extract subgoal with signature *)
    6.82 +fun SUBGOAL goalfun i st =
    6.83 +  goalfun (List.nth(prems_of st, i-1),  i, sign_of_thm st) st
    6.84 +                             handle Subscript => Seq.empty;
    6.85 +
    6.86 +(* Internal datatype for the proof *)
    6.87 +datatype proof
    6.88 +  = Asm of int 
    6.89 +  | Thm of proof list * thm; 
    6.90 +  
    6.91 +exception Cannot;
    6.92 + (* Internal exception, raised if conclusion cannot be derived from
    6.93 +     assumptions. *)
    6.94 +exception Contr of proof;
    6.95 +  (* Internal exception, raised if contradiction ( x < x ) was derived *)
    6.96 +
    6.97 +fun prove asms = 
    6.98 +  let fun pr (Asm i) = nth_elem (i, asms)
    6.99 +  |       pr (Thm (prfs, thm)) = (map pr prfs) MRS thm
   6.100 +  in pr end;
   6.101 +
   6.102 +(* Internal datatype for inequalities *)
   6.103 +datatype less 
   6.104 +   = Less  of term * term * proof 
   6.105 +   | Le    of term * term * proof
   6.106 +   | NotEq of term * term * proof; 
   6.107 +
   6.108 + (* Misc functions for datatype less *)
   6.109 +fun lower (Less (x, _, _)) = x
   6.110 +  | lower (Le (x, _, _)) = x
   6.111 +  | lower (NotEq (x,_,_)) = x;
   6.112 +
   6.113 +fun upper (Less (_, y, _)) = y
   6.114 +  | upper (Le (_, y, _)) = y
   6.115 +  | upper (NotEq (_,y,_)) = y;
   6.116 +
   6.117 +fun getprf   (Less (_, _, p)) = p
   6.118 +|   getprf   (Le   (_, _, p)) = p
   6.119 +|   getprf   (NotEq (_,_, p)) = p;
   6.120 +
   6.121 +(* ************************************************************************ *)
   6.122 +(*                                                                          *)
   6.123 +(* mkasm_trans sign (t, n) :  Sign.sg -> (Term.term * int)  -> less         *)
   6.124 +(*                                                                          *)
   6.125 +(* Tuple (t, n) (t an assumption, n its index in the assumptions) is        *)
   6.126 +(* translated to an element of type less.                                   *)
   6.127 +(* Only assumptions of form x <= y are used, all others are ignored         *)
   6.128 +(*                                                                          *)
   6.129 +(* ************************************************************************ *)
   6.130 +
   6.131 +fun mkasm_trans sign (t, n) =
   6.132 +  case Less.decomp_trans sign t of
   6.133 +    Some (x, rel, y) => 
   6.134 +    (case rel of
   6.135 +     "<="  =>  [Le (x, y, Asm n)]
   6.136 +    | _     => error ("trans_tac: unknown relation symbol ``" ^ rel ^
   6.137 +                 "''returned by decomp_trans."))
   6.138 +  | None => [];
   6.139 +  
   6.140 +(* ************************************************************************ *)
   6.141 +(*                                                                          *)
   6.142 +(* mkasm_quasi sign (t, n) : Sign.sg -> (Term.term * int) -> less           *)
   6.143 +(*                                                                          *)
   6.144 +(* Tuple (t, n) (t an assumption, n its index in the assumptions) is        *)
   6.145 +(* translated to an element of type less.                                   *)
   6.146 +(* Quasi orders only.                                                       *)
   6.147 +(*                                                                          *)
   6.148 +(* ************************************************************************ *)
   6.149 +
   6.150 +fun mkasm_quasi sign (t, n) =
   6.151 +  case Less.decomp_quasi sign t of
   6.152 +    Some (x, rel, y) => (case rel of
   6.153 +      "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], Less.less_reflE)) 
   6.154 +               else [Less (x, y, Asm n)]
   6.155 +    | "<="  => [Le (x, y, Asm n)]
   6.156 +    | "="   => [Le (x, y, Thm ([Asm n], Less.eqD1)),
   6.157 +                Le (y, x, Thm ([Asm n], Less.eqD2))]
   6.158 +    | "~="  => if (x aconv y) then 
   6.159 +                  raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE))
   6.160 +               else [ NotEq (x, y, Asm n),
   6.161 +                      NotEq (y, x,Thm ( [Asm n], thm "not_sym"))] 
   6.162 +    | _     => error ("quasi_tac: unknown relation symbol ``" ^ rel ^
   6.163 +                 "''returned by decomp_quasi."))
   6.164 +  | None => [];
   6.165 +
   6.166 +
   6.167 +(* ************************************************************************ *)
   6.168 +(*                                                                          *)
   6.169 +(* mkconcl_trans sign t : Sign.sg -> Term.term -> less                      *)
   6.170 +(*                                                                          *)
   6.171 +(* Translates conclusion t to an element of type less.                      *)
   6.172 +(* Only for Conclusions of form x <= y or x < y.                            *)
   6.173 +(*                                                                          *)
   6.174 +(* ************************************************************************ *)
   6.175 +
   6.176 +  
   6.177 +fun mkconcl_trans sign t =
   6.178 +  case Less.decomp_trans sign t of
   6.179 +    Some (x, rel, y) => (case rel of
   6.180 +     "<="  => (Le (x, y, Asm ~1), Asm 0) 
   6.181 +    | _  => raise Cannot)
   6.182 +  | None => raise Cannot;
   6.183 +  
   6.184 +  
   6.185 +(* ************************************************************************ *)
   6.186 +(*                                                                          *)
   6.187 +(* mkconcl_quasi sign t : Sign.sg -> Term.term -> less                      *)
   6.188 +(*                                                                          *)
   6.189 +(* Translates conclusion t to an element of type less.                      *)
   6.190 +(* Quasi orders only.                                                       *)
   6.191 +(*                                                                          *)
   6.192 +(* ************************************************************************ *)
   6.193 +
   6.194 +fun mkconcl_quasi sign t =
   6.195 +  case Less.decomp_quasi sign t of
   6.196 +    Some (x, rel, y) => (case rel of
   6.197 +      "<"   => ([Less (x, y, Asm ~1)], Asm 0)
   6.198 +    | "<="  => ([Le (x, y, Asm ~1)], Asm 0)
   6.199 +    | "~="  => ([NotEq (x,y, Asm ~1)], Asm 0)
   6.200 +    | _  => raise Cannot)
   6.201 +| None => raise Cannot;
   6.202 +  
   6.203 +  
   6.204 +(* ******************************************************************* *)
   6.205 +(*                                                                     *)
   6.206 +(* mergeLess (less1,less2):  less * less -> less                       *)
   6.207 +(*                                                                     *)
   6.208 +(* Merge to elements of type less according to the following rules     *)
   6.209 +(*                                                                     *)
   6.210 +(* x <= y && y <= z ==> x <= z                                         *)
   6.211 +(* x <= y && x ~= y ==> x < y                                          *)
   6.212 +(* x ~= y && x <= y ==> x < y                                          *)
   6.213 +(*                                                                     *)
   6.214 +(* ******************************************************************* *)
   6.215 +
   6.216 +fun mergeLess (Le (x, _, p) , Le (_ , z, q)) =
   6.217 +      Le (x, z, Thm ([p,q] , Less.le_trans))
   6.218 +|   mergeLess (Le (x, z, p) , NotEq (x', z', q)) =
   6.219 +      if (x aconv x' andalso z aconv z' ) 
   6.220 +       then Less (x, z, Thm ([p,q] , Less.le_neq_trans))
   6.221 +        else error "quasi_tac: internal error le_neq_trans"
   6.222 +|   mergeLess (NotEq (x, z, p) , Le (x' , z', q)) =
   6.223 +      if (x aconv x' andalso z aconv z') 
   6.224 +      then Less (x, z, Thm ([p,q] , Less.neq_le_trans))
   6.225 +      else error "quasi_tac: internal error neq_le_trans"
   6.226 +|   mergeLess (_, _) =
   6.227 +      error "quasi_tac: internal error: undefined case";
   6.228 +
   6.229 +
   6.230 +(* ******************************************************************** *)
   6.231 +(* tr checks for valid transitivity step                                *)
   6.232 +(* ******************************************************************** *)
   6.233 +
   6.234 +infix tr;
   6.235 +fun (Le (_, y, _))   tr (Le (x', _, _))   = ( y aconv x' )
   6.236 +  | _ tr _ = false;
   6.237 +  
   6.238 +(* ******************************************************************* *)
   6.239 +(*                                                                     *)
   6.240 +(* transPath (Lesslist, Less): (less list * less) -> less              *)
   6.241 +(*                                                                     *)
   6.242 +(* If a path represented by a list of elements of type less is found,  *)
   6.243 +(* this needs to be contracted to a single element of type less.       *)
   6.244 +(* Prior to each transitivity step it is checked whether the step is   *)
   6.245 +(* valid.                                                              *)
   6.246 +(*                                                                     *)
   6.247 +(* ******************************************************************* *)
   6.248 +
   6.249 +fun transPath ([],lesss) = lesss
   6.250 +|   transPath (x::xs,lesss) =
   6.251 +      if lesss tr x then transPath (xs, mergeLess(lesss,x))
   6.252 +      else error "trans/quasi_tac: internal error transpath";
   6.253 +  
   6.254 +(* ******************************************************************* *)
   6.255 +(*                                                                     *)
   6.256 +(* less1 subsumes less2 : less -> less -> bool                         *)
   6.257 +(*                                                                     *)
   6.258 +(* subsumes checks whether less1 implies less2                         *)
   6.259 +(*                                                                     *)
   6.260 +(* ******************************************************************* *)
   6.261 +  
   6.262 +infix subsumes;
   6.263 +fun (Le (x, y, _)) subsumes (Le (x', y', _)) =
   6.264 +      (x aconv x' andalso y aconv y')
   6.265 +  | (Le _) subsumes (Less _) =
   6.266 +      error "trans/quasi_tac: internal error: Le cannot subsume Less"
   6.267 +  | (NotEq(x,y,_)) subsumes (NotEq(x',y',_)) = x aconv x' andalso y aconv y' orelse x aconv y' andalso y aconv x'
   6.268 +  | _ subsumes _ = false;
   6.269 +
   6.270 +(* ******************************************************************* *)
   6.271 +(*                                                                     *)
   6.272 +(* triv_solv less1 : less ->  proof Library.option                     *)
   6.273 +(*                                                                     *)
   6.274 +(* Solves trivial goal x <= x.                                         *)
   6.275 +(*                                                                     *)
   6.276 +(* ******************************************************************* *)
   6.277 +
   6.278 +fun triv_solv (Le (x, x', _)) =
   6.279 +    if x aconv x' then  Some (Thm ([], Less.le_refl)) 
   6.280 +    else None
   6.281 +|   triv_solv _ = None;
   6.282 +
   6.283 +(* ********************************************************************* *)
   6.284 +(* Graph functions                                                       *)
   6.285 +(* ********************************************************************* *)
   6.286 +
   6.287 +(* *********************************************************** *)
   6.288 +(* Functions for constructing graphs                           *)
   6.289 +(* *********************************************************** *)
   6.290 +
   6.291 +fun addEdge (v,d,[]) = [(v,d)]
   6.292 +|   addEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el)
   6.293 +    else (u,dl):: (addEdge(v,d,el));
   6.294 +    
   6.295 +(* ********************************************************************** *)
   6.296 +(*                                                                        *)
   6.297 +(* mkQuasiGraph constructs from a list of objects of type less a graph g, *) 
   6.298 +(* by taking all edges that are candidate for a <=, and a list neqE, by   *)
   6.299 +(* taking all edges that are candiate for a ~=                            *)
   6.300 +(*                                                                        *)
   6.301 +(* ********************************************************************** *)
   6.302 +
   6.303 +fun mkQuasiGraph [] = ([],[])
   6.304 +|   mkQuasiGraph lessList = 
   6.305 + let
   6.306 + fun buildGraphs ([],leG, neqE) = (leG,  neqE)
   6.307 +  |   buildGraphs (l::ls, leG,  neqE) = case l of 
   6.308 +       (Less (x,y,p)) =>
   6.309 +         let 
   6.310 +	  val leEdge  = Le (x,y, Thm ([p], Less.less_imp_le)) 
   6.311 +	  val neqEdges = [ NotEq (x,y, Thm ([p], Less.less_imp_neq)),
   6.312 +	                   NotEq (y,x, Thm ( [Thm ([p], Less.less_imp_neq)], thm "not_sym"))]
   6.313 +	 in
   6.314 +           buildGraphs (ls, addEdge(y,[],(addEdge (x,[(y,leEdge)],leG))), neqEdges@neqE) 
   6.315 +	 end
   6.316 +     |  (Le (x,y,p))   => buildGraphs (ls, addEdge(y,[],(addEdge (x,[(y,l)],leG))), neqE) 
   6.317 +     | _ =>  buildGraphs (ls, leG,  l::neqE) ;
   6.318 +
   6.319 +in buildGraphs (lessList, [],  []) end;
   6.320 +  
   6.321 +(* ********************************************************************** *)
   6.322 +(*                                                                        *)
   6.323 +(* mkGraph constructs from a list of objects of type less a graph g       *)
   6.324 +(* Used for plain transitivity chain reasoning.                           *)
   6.325 +(*                                                                        *)
   6.326 +(* ********************************************************************** *)
   6.327 +
   6.328 +fun mkGraph [] = []
   6.329 +|   mkGraph lessList = 
   6.330 + let
   6.331 +  fun buildGraph ([],g) = g
   6.332 +  |   buildGraph (l::ls, g) =  buildGraph (ls, (addEdge ((lower l),[((upper l),l)],g))) 
   6.333 +     
   6.334 +in buildGraph (lessList, []) end;
   6.335 +
   6.336 +(* *********************************************************************** *)
   6.337 +(*                                                                         *)
   6.338 +(* adjacent g u : (''a * 'b list ) list -> ''a -> 'b list                  *)
   6.339 +(*                                                                         *)
   6.340 +(* List of successors of u in graph g                                      *)
   6.341 +(*                                                                         *)
   6.342 +(* *********************************************************************** *)
   6.343 + 
   6.344 +fun adjacent eq_comp ((v,adj)::el) u = 
   6.345 +    if eq_comp (u, v) then adj else adjacent eq_comp el u
   6.346 +|   adjacent _  []  _ = []  
   6.347 +
   6.348 +(* *********************************************************************** *)
   6.349 +(*                                                                         *)
   6.350 +(* dfs eq_comp g u v:                                                      *)
   6.351 +(* ('a * 'a -> bool) -> ('a  *( 'a * less) list) list ->                   *)
   6.352 +(* 'a -> 'a -> (bool * ('a * less) list)                                   *) 
   6.353 +(*                                                                         *)
   6.354 +(* Depth first search of v from u.                                         *)
   6.355 +(* Returns (true, path(u, v)) if successful, otherwise (false, []).        *)
   6.356 +(*                                                                         *)
   6.357 +(* *********************************************************************** *)
   6.358 +
   6.359 +fun dfs eq_comp g u v = 
   6.360 + let 
   6.361 +    val pred = ref nil;
   6.362 +    val visited = ref nil;
   6.363 +    
   6.364 +    fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
   6.365 +    
   6.366 +    fun dfs_visit u' = 
   6.367 +    let val _ = visited := u' :: (!visited)
   6.368 +    
   6.369 +    fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
   6.370 +    
   6.371 +    in if been_visited v then () 
   6.372 +    else (app (fn (v',l) => if been_visited v' then () else (
   6.373 +       update (v',l); 
   6.374 +       dfs_visit v'; ()) )) (adjacent eq_comp g u')
   6.375 +     end
   6.376 +  in 
   6.377 +    dfs_visit u; 
   6.378 +    if (been_visited v) then (true, (!pred)) else (false , [])   
   6.379 +  end;
   6.380 +
   6.381 +(* ************************************************************************ *)
   6.382 +(*                                                                          *)
   6.383 +(* Begin: Quasi Order relevant functions                                    *)
   6.384 +(*                                                                          *)
   6.385 +(*                                                                          *)
   6.386 +(* ************************************************************************ *)
   6.387 +
   6.388 +(* ************************************************************************ *)
   6.389 +(*                                                                          *)
   6.390 +(* findPath x y g: Term.term -> Term.term ->                                *)
   6.391 +(*                  (Term.term * (Term.term * less list) list) ->           *)
   6.392 +(*                  (bool, less list)                                       *)
   6.393 +(*                                                                          *)
   6.394 +(*  Searches a path from vertex x to vertex y in Graph g, returns true and  *)
   6.395 +(*  the list of edges forming the path, if a path is found, otherwise false *)
   6.396 +(*  and nil.                                                                *)
   6.397 +(*                                                                          *)
   6.398 +(* ************************************************************************ *)
   6.399 +
   6.400 +
   6.401 + fun findPath x y g = 
   6.402 +  let 
   6.403 +    val (found, tmp) =  dfs (op aconv) g x y ;
   6.404 +    val pred = map snd tmp;
   6.405 +
   6.406 +    fun path x y  =
   6.407 +      let
   6.408 +       (* find predecessor u of node v and the edge u -> v *)
   6.409 +       fun lookup v [] = raise Cannot
   6.410 +       |   lookup v (e::es) = if (upper e) aconv v then e else lookup v es;
   6.411 +		
   6.412 +       (* traverse path backwards and return list of visited edges *)   
   6.413 +       fun rev_path v = 
   6.414 + 	let val l = lookup v pred
   6.415 +            val u = lower l;
   6.416 + 	in
   6.417 +           if u aconv x then [l] else (rev_path u) @ [l] 
   6.418 +	end
   6.419 +      in rev_path y end;
   6.420 +		
   6.421 +  in 
   6.422 +   if found then (
   6.423 +    if x aconv y then (found,[(Le (x, y, (Thm ([], Less.le_refl))))])
   6.424 +    else (found, (path x y) )) 
   6.425 +   else (found,[])
   6.426 +  end; 
   6.427 +	
   6.428 +      
   6.429 +(* ************************************************************************ *) 
   6.430 +(*                                                                          *)
   6.431 +(* findQuasiProof (leqG, neqE) subgoal:                                     *)
   6.432 +(* (Term.term * (Term.term * less list) list) * less list  -> less -> proof *)
   6.433 +(*                                                                          *)
   6.434 +(* Constructs a proof for subgoal by searching a special path in leqG and   *)
   6.435 +(* neqE. Raises Cannot if construction of the proof fails.                  *)   
   6.436 +(*                                                                          *)
   6.437 +(* ************************************************************************ *) 
   6.438 +
   6.439 +
   6.440 +(* As the conlusion can be either of form x <= y, x < y or x ~= y we have        *)
   6.441 +(* three cases to deal with. Finding a transitivity path from x to y with label  *)
   6.442 +(* 1. <=                                                                         *) 
   6.443 +(*    This is simply done by searching any path from x to y in the graph leG.    *)
   6.444 +(*    The graph leG contains only edges with label <=.                           *)
   6.445 +(*                                                                               *)
   6.446 +(* 2. <                                                                          *)
   6.447 +(*    A path from x to y with label < can be found by searching a path with      *)
   6.448 +(*    label <= from x to y in the graph leG and merging the path x <= y with     *)
   6.449 +(*    a parallel edge x ~= y resp. y ~= x to x < y.                              *)
   6.450 +(*                                                                               *)
   6.451 +(* 3. ~=                                                                         *)
   6.452 +(*   If the conclusion is of form x ~= y, we can find a proof either directly,   *)
   6.453 +(*   if x ~= y or y ~= x are among the assumptions, or by constructing x ~= y if *)
   6.454 +(*   x < y or y < x follows from the assumptions.                                *)
   6.455 +
   6.456 +fun findQuasiProof (leG, neqE) subgoal =
   6.457 +  case subgoal of (Le (x,y, _)) => (
   6.458 +   let 
   6.459 +    val (xyLefound,xyLePath) = findPath x y leG 
   6.460 +   in
   6.461 +    if xyLefound then (
   6.462 +     let 
   6.463 +      val Le_x_y = (transPath (tl xyLePath, hd xyLePath))
   6.464 +     in getprf Le_x_y end )
   6.465 +    else raise Cannot
   6.466 +   end )
   6.467 +  | (Less (x,y,_))  => (
   6.468 +   let 
   6.469 +    fun findParallelNeq []  = None
   6.470 +    |   findParallelNeq (e::es)  =
   6.471 +     if      (x aconv (lower e) andalso y aconv (upper e)) then Some e
   6.472 +     else if (y aconv (lower e) andalso x aconv (upper e)) then Some (NotEq (x,y, (Thm ([getprf e], thm "not_sym"))))
   6.473 +     else findParallelNeq es ;  
   6.474 +   in
   6.475 +   (* test if there is a edge x ~= y respectivly  y ~= x and     *)
   6.476 +   (* if it possible to find a path x <= y in leG, thus we can conclude x < y *)
   6.477 +    (case findParallelNeq neqE of (Some e) => 
   6.478 +      let 
   6.479 +       val (xyLeFound,xyLePath) = findPath x y leG 
   6.480 +      in
   6.481 +       if xyLeFound then (
   6.482 +        let 
   6.483 +         val Le_x_y = (transPath (tl xyLePath, hd xyLePath))
   6.484 +         val Less_x_y = mergeLess (e, Le_x_y)
   6.485 +        in getprf Less_x_y end
   6.486 +       ) else raise Cannot
   6.487 +      end 
   6.488 +    | _ => raise Cannot)    
   6.489 +   end )
   6.490 + | (NotEq (x,y,_)) => 
   6.491 +  (* First check if a single premiss is sufficient *)
   6.492 +  (case (Library.find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of
   6.493 +    (Some (NotEq (x, y, p)), NotEq (x', y', _)) =>
   6.494 +      if  (x aconv x' andalso y aconv y') then p 
   6.495 +      else Thm ([p], thm "not_sym")
   6.496 +    | _  => raise Cannot 
   6.497 +  )
   6.498 +
   6.499 +      
   6.500 +(* ************************************************************************ *) 
   6.501 +(*                                                                          *) 
   6.502 +(* End: Quasi Order relevant functions                                      *) 
   6.503 +(*                                                                          *) 
   6.504 +(*                                                                          *) 
   6.505 +(* ************************************************************************ *) 
   6.506 +
   6.507 +(* *********************************************************************** *)
   6.508 +(*                                                                         *)
   6.509 +(* solveLeTrans sign (asms,concl) :                                        *)
   6.510 +(* Sign.sg -> less list * Term.term -> proof list                          *)
   6.511 +(*                                                                         *)
   6.512 +(* Solves                                                                  *)
   6.513 +(*                                                                         *)
   6.514 +(* *********************************************************************** *)
   6.515 +
   6.516 +fun solveLeTrans sign (asms, concl) =
   6.517 + let 
   6.518 +  val g = mkGraph asms
   6.519 + in
   6.520 +   let 
   6.521 +    val (subgoal, prf) = mkconcl_trans sign concl
   6.522 +    val (found, path) = findPath (lower subgoal) (upper subgoal) g 
   6.523 +   in
   6.524 +    if found then [getprf (transPath (tl path, hd path))] 
   6.525 +    else raise Cannot
   6.526 +  end
   6.527 + end;
   6.528 +
   6.529 +
   6.530 +(* *********************************************************************** *)
   6.531 +(*                                                                         *)
   6.532 +(* solveQuasiOrder sign (asms,concl) :                                     *)
   6.533 +(* Sign.sg -> less list * Term.term -> proof list                          *)
   6.534 +(*                                                                         *)
   6.535 +(* Find proof if possible for quasi order.                                 *)
   6.536 +(*                                                                         *)
   6.537 +(* *********************************************************************** *)
   6.538 +
   6.539 +fun solveQuasiOrder sign (asms, concl) =
   6.540 + let 
   6.541 +  val (leG, neqE) = mkQuasiGraph asms
   6.542 + in
   6.543 +   let 
   6.544 +   val (subgoals, prf) = mkconcl_quasi sign concl
   6.545 +   fun solve facts less =
   6.546 +       (case triv_solv less of None => findQuasiProof (leG, neqE) less
   6.547 +       | Some prf => prf )
   6.548 +  in   map (solve asms) subgoals end
   6.549 + end;
   6.550 +
   6.551 +(* ************************************************************************ *) 
   6.552 +(*                                                                          *) 
   6.553 +(* Tactics                                                                  *)
   6.554 +(*                                                                          *)
   6.555 +(*  - trans_tac                                                          *)                     
   6.556 +(*  - quasi_tac, solves quasi orders                                        *)                     
   6.557 +(* ************************************************************************ *) 
   6.558 +
   6.559 +
   6.560 +(* trans_tac - solves transitivity chains over <= *)
   6.561 +val trans_tac  =  SUBGOAL (fn (A, n, sign) =>
   6.562 + let
   6.563 +  val rfrees = map Free (rename_wrt_term A (Logic.strip_params A))
   6.564 +  val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
   6.565 +  val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
   6.566 +  val lesss = flat (ListPair.map (mkasm_trans  sign) (Hs, 0 upto (length Hs - 1)))
   6.567 +  val prfs = solveLeTrans  sign (lesss, C);
   6.568 +  
   6.569 +  val (subgoal, prf) = mkconcl_trans  sign C;
   6.570 + in
   6.571 +  
   6.572 +  METAHYPS (fn asms =>
   6.573 +    let val thms = map (prove asms) prfs
   6.574 +    in rtac (prove thms prf) 1 end) n
   6.575 +  
   6.576 + end
   6.577 + handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n
   6.578 +      | Cannot  => no_tac
   6.579 +);
   6.580 +
   6.581 +(* quasi_tac - solves quasi orders *)
   6.582 +val quasi_tac = SUBGOAL (fn (A, n, sign) =>
   6.583 + let
   6.584 +  val rfrees = map Free (rename_wrt_term A (Logic.strip_params A))
   6.585 +  val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
   6.586 +  val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
   6.587 +  val lesss = flat (ListPair.map (mkasm_quasi sign) (Hs, 0 upto (length Hs - 1)))
   6.588 +  val prfs = solveQuasiOrder sign (lesss, C);
   6.589 +  val (subgoals, prf) = mkconcl_quasi sign C;
   6.590 + in
   6.591 + 
   6.592 +  METAHYPS (fn asms =>
   6.593 +    let val thms = map (prove asms) prfs
   6.594 +    in rtac (prove thms prf) 1 end) n
   6.595 + 
   6.596 + end
   6.597 + handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n
   6.598 +      | Cannot  => no_tac
   6.599 +);
   6.600 +   
   6.601 +end;