Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 4 kB

Quelle preorder.ML Sprache: SML

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

Reasoner for simple transitivity and quasi orders.
*)

(*

The package provides tactics trans_tac and quasi_tac that use
premises of the form

  t = u, t ~= u, t < u and t <= u

to
- either derive a contradiction, in which case the conclusion can be
  any term,
- or prove the concluson, which must be of the form t ~= u, t < u or
  t <= u.

Details:

1. trans_tac:
   Only premises of form t <= u are used and the conclusion must be of
   the same form.  The conclusion is proved, if possible, by a chain of
   transitivity from the assumptions.

2. quasi_tac:
   <= is assumed to be a quasi order and < its strict relative, defined
   as t < u == t <= u & t ~= u.  Again, the conclusion is proved from
   the assumptions.
   Note that the presence of a strict relation is not necessary for
   quasi_tac.  Configure decomp_quasi to ignore < and ~=.  A list of
   required theorems for both situations is given below.
*)

signature LESS_ARITH =
sig
  (* Transitivity of <=
     Note that transitivities for < hold for partial orders only. *)
  val le_trans: thm  (* [| x <= y; y <= z |] ==> x <= z *)

  (* Additional theorem for quasi orders *)
  val le_refl: thm  (* x <= x *)
  val eqD1: thm (* x = y ==> x <= y *)
  val eqD2: thm (* x = y ==> y <= x *)

  (* Additional theorems for premises of the form x < y *)
  val less_reflE: thm  (* x < x ==> P *)
  val less_imp_le : thm (* x < y ==> x <= y *)

  (* Additional theorems for premises of the form x ~= y *)
  val le_neq_trans : thm (* [| x <= y ; x ~= y |] ==> x < y *)
  val neq_le_trans : thm (* [| x ~= y ; x <= y |] ==> x < y *)

  (* Additional theorem for goals of form x ~= y *)
  val less_imp_neq : thm (* x < y ==> x ~= y *)

  (* Analysis of premises and conclusion *)
  (* decomp_x (`x Rel y') should yield SOME (x, Rel, y)
       where Rel is one of "<", "<=", "=" and "~=",
       other relation symbols cause an error message *)
  (* decomp_trans is used by trans_tac, it may only return Rel = "<=" *)
  val decomp_trans: theory -> term -> (term * string * term) option
  (* decomp_quasi is used by quasi_tac *)
  val decomp_quasi: theory -> term -> (term * string * term) option
end;

signature QUASI_TAC =
sig
  val trans_tac: Proof.context -> int -> tactic
  val quasi_tac: Proof.context -> int -> tactic
end;

functor Quasi_Tac(Less: LESS_ARITH): QUASI_TAC =
struct

(* 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_trans sign (t, n) :  theory -> (Term.term * int)  -> less          *)
(*                                                                          *)
(* Tuple (t, n) (t an assumption, n its index in the assumptions) is        *)
(* translated to an element of type less.                                   *)
(* Only assumptions of form x <= y are used, all others are ignored         *)
(*                                                                          *)
(* ************************************************************************ *)

fun mkasm_trans thy (t, n) =
  case Less.decomp_trans thy t of
    SOME (x, rel, y) =>
    (case rel of
     "<="  =>  [Le (x, y, Asm n)]
    | _     => error ("trans_tac: unknown relation symbol ``" ^ rel ^
                 "''returned by decomp_trans."))
  | NONE => [];

(* ************************************************************************ *)
(*                                                                          *)
(* mkasm_quasi sign (t, n) : theory -> (Term.term * int) -> less            *)
(*                                                                          *)
(* Tuple (t, n) (t an assumption, n its index in the assumptions) is        *)
(* translated to an element of type less.                                   *)
(* Quasi orders only.                                                       *)
(*                                                                          *)
(* ************************************************************************ *)

fun mkasm_quasi thy (t, n) =
  case Less.decomp_quasi thy t of
    SOME (x, rel, y) => (case rel of
      "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], Less.less_reflE))
               else [Less (x, y, Asm n)]
    | "<="  => [Le (x, y, Asm n)]
    | "="   => [Le (x, y, Thm ([Asm n], Less.eqD1)),
                Le (y, x, Thm ([Asm n], Less.eqD2))]
    | "~="  => if (x aconv y) then
                  raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE))
               else [ NotEq (x, y, Asm n),
                      NotEq (y, x,Thm ( [Asm n], @{thm not_sym}))]
    | _     => error ("quasi_tac: unknown relation symbol ``" ^ rel ^
                 "''returned by decomp_quasi."))
  | NONE => [];

(* ************************************************************************ *)
(*                                                                          *)
(* mkconcl_trans sign t : theory -> Term.term -> less                       *)
(*                                                                          *)
(* Translates conclusion t to an element of type less.                      *)
(* Only for Conclusions of form x <= y or x < y.                            *)
(*                                                                          *)
(* ************************************************************************ *)

fun mkconcl_trans thy t =
  case Less.decomp_trans thy t of
    SOME (x, rel, y) => (case rel of
     "<="  => (Le (x, y, Asm ~1), Asm 0)
    | _  => raise Cannot)
  | NONE => raise Cannot;

(* ************************************************************************ *)
(*                                                                          *)
(* mkconcl_quasi sign t : theory -> Term.term -> less                       *)
(*                                                                          *)
(* Translates conclusion t to an element of type less.                      *)
(* Quasi orders only.                                                       *)
(*                                                                          *)
(* ************************************************************************ *)

fun mkconcl_quasi thy t =
  case Less.decomp_quasi thy t of
    SOME (x, rel, y) => (case rel of
      "<"   => ([Less (x, y, Asm ~1)], Asm 0)
    | "<="  => ([Le (x, y, Asm ~1)], Asm 0)
    | "~="  => ([NotEq (x,y, Asm ~1)], Asm 0)
    | _  => raise Cannot)
| NONE => raise Cannot;

(* ******************************************************************* *)
(*                                                                     *)
(* mergeLess (less1,less2):  less * less -> less                       *)
(*                                                                     *)
(* Merge to elements of type less according to the following rules     *)
(*                                                                     *)
(* x <= y && y <= z ==> x <= z                                         *)
(* x <= y && x ~= y ==> x < y                                          *)
(* x ~= y && x <= y ==> x < y                                          *)
(*                                                                     *)
(* ******************************************************************* *)

fun mergeLess (Le (x, _, p) , Le (_ , z, q)) =
      Le (x, z, Thm ([p,q] , Less.le_trans))
|   mergeLess (Le (x, z, p) , NotEq (x', z', q)) =
      if (x aconv x' andalso z aconv z' )
       then Less (x, z, Thm ([p,q] , Less.le_neq_trans))
        else error "quasi_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] , Less.neq_le_trans))
      else error "quasi_tac: internal error neq_le_trans"
|   mergeLess (_, _) =
      error "quasi_tac: internal error: undefined case";

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

infix tr;
fun (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 "trans/quasi_tac: internal error transpath";

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

infix subsumes;
fun (Le (x, y, _)) subsumes (Le (x', y', _)) =
      (x aconv x' andalso y aconv y')
  | (Le _) subsumes (Less _) =
      error "trans/quasi_tac: internal error: Le cannot subsume Less"
  | (NotEq(x,y,_)) subsumes (NotEq(x',y',_)) = x aconv x' andalso y aconv y' orelse x aconv y' andalso y aconv x'
  | _ 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 ([], Less.le_refl))
    else NONE
|   triv_solv _ = NONE;

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

(* *********************************************************** *)
(* 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));

(* ********************************************************************** *)
(*                                                                        *)
(* mkQuasiGraph 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 mkQuasiGraph [] = ([],[])
|   mkQuasiGraph lessList =
let
fun buildGraphs ([],leG, neqE) = (leG,  neqE)
  |   buildGraphs (l::ls, leG,  neqE) = case l of
       (Less (x,y,p)) =>
         let
          val leEdge  = Le (x,y, Thm ([p], Less.less_imp_le))
          val neqEdges = [ NotEq (x,y, Thm ([p], Less.less_imp_neq)),
                           NotEq (y,x, Thm ( [Thm ([p], Less.less_imp_neq)], @{thm not_sym}))]
         in
           buildGraphs (ls, addEdge(y,[],(addEdge (x,[(y,leEdge)],leG))), neqEdges@neqE)
         end
     |  (Le (x,y,p))   => buildGraphs (ls, addEdge(y,[],(addEdge (x,[(y,l)],leG))), neqE)
     | _ =>  buildGraphs (ls, leG,  l::neqE) ;

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

(* ********************************************************************** *)
(*                                                                        *)
(* mkGraph constructs from a list of objects of type less a graph g       *)
(* Used for plain transitivity chain reasoning.                           *)
(*                                                                        *)
(* ********************************************************************** *)

fun mkGraph [] = []
|   mkGraph lessList =
let
  fun buildGraph ([],g) = g
  |   buildGraph (l::ls, g) =  buildGraph (ls, (addEdge ((lower l),[((upper l),l)],g)))

in buildGraph (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 _  []  _ = []

(* *********************************************************************** *)
(*                                                                         *)
(* 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;

(* ************************************************************************ *)
(*                                                                          *)
(* Begin: Quasi Order relevant functions                                    *)
(*                                                                          *)
(*                                                                          *)
(* ************************************************************************ *)

(* ************************************************************************ *)
(*                                                                          *)
(* findPath x y g: Term.term -> Term.term ->                                *)
(*                  (Term.term * (Term.term * less list) list) ->           *)
(*                  (bool, less list)                                       *)
(*                                                                          *)
(*  Searches a path from vertex x to vertex y in Graph g, returns true and  *)
(*  the list of edges forming the path, if a path is found, otherwise false *)
(*  and nil.                                                                *)
(*                                                                          *)
(* ************************************************************************ *)

fun findPath x y g =
  let
    val (found, tmp) =  dfs (op aconv) g x y ;
    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 x aconv y then (found,[(Le (x, y, (Thm ([], Less.le_refl))))])
    else (found, (path x y) ))
   else (found,[])
  end;

(* ************************************************************************ *)
(*                                                                          *)
(* findQuasiProof (leqG, neqE) subgoal:                                     *)
(* (Term.term * (Term.term * less list) list) * less list  -> less -> proof *)
(*                                                                          *)
(* Constructs a proof for subgoal by searching a special path in leqG and   *)
(* neqE. Raises Cannot if construction of the proof fails.                  *)
(*                                                                          *)
(* ************************************************************************ *)

(* As the conlusion can be either of form x <= y, x < y or x ~= y we have        *)
(* three cases to deal with. Finding a transitivity path from x to y with label  *)
(* 1. <=                                                                         *)
(*    This is simply done by searching any path from x to y in the graph leG.    *)
(*    The graph leG contains only edges with label <=.                           *)
(*                                                                               *)
(* 2. <                                                                          *)
(*    A path from x to y with label < can be found by searching a path with      *)
(*    label <= from x to y in the graph leG and merging the path x <= y with     *)
(*    a parallel edge x ~= y resp. y ~= x to x < y.                              *)
(*                                                                               *)
(* 3. ~=                                                                         *)
(*   If the conclusion is of form x ~= y, we can find a proof either directly,   *)
(*   if x ~= y or y ~= x are among the assumptions, or by constructing x ~= y if *)
(*   x < y or y < x follows from the assumptions.                                *)

fun findQuasiProof (leG, neqE) subgoal =
  case subgoal of (Le (x,y, _)) => (
   let
    val (xyLefound,xyLePath) = findPath x y leG
   in
    if xyLefound then (
     let
      val Le_x_y = (transPath (tl xyLePath, hd xyLePath))
     in getprf Le_x_y end )
    else raise Cannot
   end )
  | (Less (x,y,_))  => (
   let
    fun findParallelNeq []  = NONE
    |   findParallelNeq (e::es)  =
     if (x aconv (lower e) andalso y aconv (upper e)) then SOME e
     else if (y aconv (lower e) andalso x aconv (upper e))
     then SOME (NotEq (x,y, (Thm ([getprf e], @{thm not_sym}))))
     else findParallelNeq es;
   in
   (* test if there is a edge x ~= y respectivly  y ~= x and     *)
   (* if it possible to find a path x <= y in leG, thus we can conclude x < y *)
    (case findParallelNeq neqE of (SOME e) =>
      let
       val (xyLeFound,xyLePath) = findPath x y leG
      in
       if xyLeFound then (
        let
         val Le_x_y = (transPath (tl xyLePath, hd xyLePath))
         val Less_x_y = mergeLess (e, Le_x_y)
        in getprf Less_x_y end
       ) else raise Cannot
      end
    | _ => raise Cannot)
   end )
| (NotEq (x,y,_)) =>
  (* First check if a single premiss is sufficient *)
  (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], @{thm not_sym})
    | _  => raise Cannot
  )

(* ************************************************************************ *)
(*                                                                          *)
(* End: Quasi Order relevant functions                                      *)
(*                                                                          *)
(*                                                                          *)
(* ************************************************************************ *)

(* *********************************************************************** *)
(*                                                                         *)
(* solveLeTrans sign (asms,concl) :                                        *)
(* theory -> less list * Term.term -> proof list                           *)
(*                                                                         *)
(* Solves                                                                  *)
(*                                                                         *)
(* *********************************************************************** *)

fun solveLeTrans thy (asms, concl) =
let
  val g = mkGraph asms
in
   let
    val (subgoal, prf) = mkconcl_trans thy concl
    val (found, path) = findPath (lower subgoal) (upper subgoal) g
   in
    if found then [getprf (transPath (tl path, hd path))]
    else raise Cannot
  end
end;

(* *********************************************************************** *)
(*                                                                         *)
(* solveQuasiOrder sign (asms,concl) :                                     *)
(* theory -> less list * Term.term -> proof list                           *)
(*                                                                         *)
(* Find proof if possible for quasi order.                                 *)
(*                                                                         *)
(* *********************************************************************** *)

fun solveQuasiOrder thy (asms, concl) =
let
  val (leG, neqE) = mkQuasiGraph asms
in
   let
   val (subgoals, prf) = mkconcl_quasi thy concl
   fun solve facts less =
       (case triv_solv less of NONE => findQuasiProof (leG, neqE) less
       | SOME prf => prf )
  in   map (solve asms) subgoals end
end;

(* ************************************************************************ *)
(*                                                                          *)
(* Tactics                                                                  *)
(*                                                                          *)
(*  - trans_tac                                                          *)
(*  - quasi_tac, solves quasi orders                                        *)
(* ************************************************************************ *)

(* trans_tac - solves transitivity chains over <= *)

fun trans_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
let
  val thy = Proof_Context.theory_of ctxt;
  val rfrees = map Free (rev (Term.variant_bounds A (Logic.strip_params A)));
  val Hs = 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_trans thy o swap) Hs);
  val prfs = solveLeTrans thy (lesss, C);

  val (subgoal, prf) = mkconcl_trans thy C;
in
  Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
    let val thms = map (prove prems) prfs
    in resolve_tac ctxt' [prove thms prf] 1 end) ctxt n st
end
handle Contr p =>
    Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
      resolve_tac ctxt' [prove prems p] 1) ctxt n st
  | Cannot => Seq.empty);

(* quasi_tac - solves quasi orders *)

fun quasi_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
let
  val thy = Proof_Context.theory_of ctxt
  val rfrees = map Free (rev (Term.variant_bounds A (Logic.strip_params A)));
  val Hs = 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_quasi thy o swap) Hs);
  val prfs = solveQuasiOrder thy (lesss, C);
  val (subgoals, prf) = mkconcl_quasi thy C;
in
  Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
    let val thms = map (prove prems) prfs
    in resolve_tac ctxt' [prove thms prf] 1 end) ctxt n st
end
handle Contr p =>
    (Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
      resolve_tac ctxt' [prove prems p] 1) ctxt n st handle General.Subscript => Seq.empty)
  | Cannot => Seq.empty
  | General.Subscript => Seq.empty);

end;

quality100%

¤ 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.0.6Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.