src/Provers/quasi.ML
author wenzelm
Sun, 11 Jan 2009 21:49:59 +0100
changeset 29450 ac7f67be7f1f
parent 29276 94b1ffec9201
child 32215 87806301a813
permissions -rw-r--r--
tuned categories;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
29276
94b1ffec9201 qualified Term.rename_wrt_term;
wenzelm
parents: 22578
diff changeset
     1
(*  Author:     Oliver Kutter, TU Muenchen
94b1ffec9201 qualified Term.rename_wrt_term;
wenzelm
parents: 22578
diff changeset
     2
94b1ffec9201 qualified Term.rename_wrt_term;
wenzelm
parents: 22578
diff changeset
     3
Reasoner for simple transitivity and quasi orders.
94b1ffec9201 qualified Term.rename_wrt_term;
wenzelm
parents: 22578
diff changeset
     4
*)
15103
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
     5
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
     6
(* 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
     7
 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
     8
The package provides tactics trans_tac and quasi_tac that use
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
     9
premises of the form 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    10
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    11
  t = u, t ~= u, t < u and t <= u
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    12
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    13
to
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    14
- either derive a contradiction, in which case the conclusion can be
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    15
  any term,
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    16
- or prove the concluson, which must be of the form t ~= u, t < u or
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    17
  t <= u.
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    18
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    19
Details:
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    20
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    21
1. trans_tac:
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    22
   Only premises of form t <= u are used and the conclusion must be of
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    23
   the same form.  The conclusion is proved, if possible, by a chain of
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    24
   transitivity from the assumptions.
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    25
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    26
2. quasi_tac:
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    27
   <= is assumed to be a quasi order and < its strict relative, defined
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    28
   as t < u == t <= u & t ~= u.  Again, the conclusion is proved from
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    29
   the assumptions.
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    30
   Note that the presence of a strict relation is not necessary for
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    31
   quasi_tac.  Configure decomp_quasi to ignore < and ~=.  A list of
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    32
   required theorems for both situations is given below. 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    33
*)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    34
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    35
signature LESS_ARITH =
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    36
sig
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    37
  (* Transitivity of <=
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    38
     Note that transitivities for < hold for partial orders only. *) 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    39
  val le_trans: thm  (* [| x <= y; y <= z |] ==> x <= z *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    40
 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    41
  (* Additional theorem for quasi orders *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    42
  val le_refl: thm  (* x <= x *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    43
  val eqD1: thm (* x = y ==> x <= y *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    44
  val eqD2: thm (* x = y ==> y <= x *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    45
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    46
  (* Additional theorems for premises of the form x < y *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    47
  val less_reflE: thm  (* x < x ==> P *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    48
  val less_imp_le : thm (* x < y ==> x <= y *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    49
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    50
  (* Additional theorems for premises of the form x ~= y *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    51
  val le_neq_trans : thm (* [| x <= y ; x ~= y |] ==> x < y *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    52
  val neq_le_trans : thm (* [| x ~= y ; x <= y |] ==> x < y *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    53
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    54
  (* Additional theorem for goals of form x ~= y *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    55
  val less_imp_neq : thm (* x < y ==> x ~= y *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    56
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    57
  (* Analysis of premises and conclusion *)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15103
diff changeset
    58
  (* decomp_x (`x Rel y') should yield SOME (x, Rel, y)
15103
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    59
       where Rel is one of "<", "<=", "=" and "~=",
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    60
       other relation symbols cause an error message *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    61
  (* decomp_trans is used by trans_tac, it may only return Rel = "<=" *)
19250
932a50e2332f got rid of type Sign.sg;
wenzelm
parents: 15570
diff changeset
    62
  val decomp_trans: theory -> term -> (term * string * term) option
15103
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    63
  (* decomp_quasi is used by quasi_tac *)
19250
932a50e2332f got rid of type Sign.sg;
wenzelm
parents: 15570
diff changeset
    64
  val decomp_quasi: theory -> term -> (term * string * term) option
15103
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    65
end;
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    66
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    67
signature QUASI_TAC = 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    68
sig
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    69
  val trans_tac: int -> tactic
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    70
  val quasi_tac: int -> tactic
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    71
end;
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    72
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    73
functor Quasi_Tac_Fun (Less: LESS_ARITH): QUASI_TAC =
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    74
struct
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    75
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    76
(* Extract subgoal with signature *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    77
fun SUBGOAL goalfun i st =
22578
b0eb5652f210 removed obsolete sign_of/sign_of_thm;
wenzelm
parents: 19250
diff changeset
    78
  goalfun (List.nth(prems_of st, i-1),  i, Thm.theory_of_thm st) st
15103
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    79
                             handle Subscript => Seq.empty;
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    80
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    81
(* Internal datatype for the proof *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    82
datatype proof
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    83
  = Asm of int 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    84
  | Thm of proof list * thm; 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    85
  
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    86
exception Cannot;
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    87
 (* Internal exception, raised if conclusion cannot be derived from
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    88
     assumptions. *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    89
exception Contr of proof;
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    90
  (* Internal exception, raised if contradiction ( x < x ) was derived *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    91
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    92
fun prove asms = 
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
    93
  let fun pr (Asm i) = List.nth (asms, i)
15103
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    94
  |       pr (Thm (prfs, thm)) = (map pr prfs) MRS thm
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    95
  in pr end;
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    96
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    97
(* Internal datatype for inequalities *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    98
datatype less 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
    99
   = Less  of term * term * proof 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   100
   | Le    of term * term * proof
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   101
   | NotEq of term * term * proof; 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   102
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   103
 (* Misc functions for datatype less *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   104
fun lower (Less (x, _, _)) = x
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   105
  | lower (Le (x, _, _)) = x
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   106
  | lower (NotEq (x,_,_)) = x;
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   107
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   108
fun upper (Less (_, y, _)) = y
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   109
  | upper (Le (_, y, _)) = y
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   110
  | upper (NotEq (_,y,_)) = y;
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   111
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   112
fun getprf   (Less (_, _, p)) = p
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   113
|   getprf   (Le   (_, _, p)) = p
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   114
|   getprf   (NotEq (_,_, p)) = p;
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   115
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   116
(* ************************************************************************ *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   117
(*                                                                          *)
19250
932a50e2332f got rid of type Sign.sg;
wenzelm
parents: 15570
diff changeset
   118
(* mkasm_trans sign (t, n) :  theory -> (Term.term * int)  -> less          *)
15103
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   119
(*                                                                          *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   120
(* Tuple (t, n) (t an assumption, n its index in the assumptions) is        *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   121
(* translated to an element of type less.                                   *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   122
(* Only assumptions of form x <= y are used, all others are ignored         *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   123
(*                                                                          *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   124
(* ************************************************************************ *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   125
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   126
fun mkasm_trans sign (t, n) =
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   127
  case Less.decomp_trans sign t of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15103
diff changeset
   128
    SOME (x, rel, y) => 
15103
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   129
    (case rel of
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   130
     "<="  =>  [Le (x, y, Asm n)]
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   131
    | _     => error ("trans_tac: unknown relation symbol ``" ^ rel ^
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   132
                 "''returned by decomp_trans."))
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15103
diff changeset
   133
  | NONE => [];
15103
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   134
  
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   135
(* ************************************************************************ *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   136
(*                                                                          *)
19250
932a50e2332f got rid of type Sign.sg;
wenzelm
parents: 15570
diff changeset
   137
(* mkasm_quasi sign (t, n) : theory -> (Term.term * int) -> less            *)
15103
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   138
(*                                                                          *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   139
(* Tuple (t, n) (t an assumption, n its index in the assumptions) is        *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   140
(* translated to an element of type less.                                   *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   141
(* Quasi orders only.                                                       *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   142
(*                                                                          *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   143
(* ************************************************************************ *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   144
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   145
fun mkasm_quasi sign (t, n) =
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   146
  case Less.decomp_quasi sign t of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15103
diff changeset
   147
    SOME (x, rel, y) => (case rel of
15103
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   148
      "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], Less.less_reflE)) 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   149
               else [Less (x, y, Asm n)]
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   150
    | "<="  => [Le (x, y, Asm n)]
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   151
    | "="   => [Le (x, y, Thm ([Asm n], Less.eqD1)),
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   152
                Le (y, x, Thm ([Asm n], Less.eqD2))]
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   153
    | "~="  => if (x aconv y) then 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   154
                  raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE))
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   155
               else [ NotEq (x, y, Asm n),
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   156
                      NotEq (y, x,Thm ( [Asm n], thm "not_sym"))] 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   157
    | _     => error ("quasi_tac: unknown relation symbol ``" ^ rel ^
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   158
                 "''returned by decomp_quasi."))
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15103
diff changeset
   159
  | NONE => [];
15103
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   160
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   161
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   162
(* ************************************************************************ *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   163
(*                                                                          *)
19250
932a50e2332f got rid of type Sign.sg;
wenzelm
parents: 15570
diff changeset
   164
(* mkconcl_trans sign t : theory -> Term.term -> less                       *)
15103
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   165
(*                                                                          *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   166
(* Translates conclusion t to an element of type less.                      *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   167
(* Only for Conclusions of form x <= y or x < y.                            *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   168
(*                                                                          *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   169
(* ************************************************************************ *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   170
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   171
  
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   172
fun mkconcl_trans sign t =
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   173
  case Less.decomp_trans sign t of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15103
diff changeset
   174
    SOME (x, rel, y) => (case rel of
15103
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   175
     "<="  => (Le (x, y, Asm ~1), Asm 0) 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   176
    | _  => raise Cannot)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15103
diff changeset
   177
  | NONE => raise Cannot;
15103
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   178
  
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   179
  
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   180
(* ************************************************************************ *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   181
(*                                                                          *)
19250
932a50e2332f got rid of type Sign.sg;
wenzelm
parents: 15570
diff changeset
   182
(* mkconcl_quasi sign t : theory -> Term.term -> less                       *)
15103
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   183
(*                                                                          *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   184
(* Translates conclusion t to an element of type less.                      *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   185
(* Quasi orders only.                                                       *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   186
(*                                                                          *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   187
(* ************************************************************************ *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   188
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   189
fun mkconcl_quasi sign t =
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   190
  case Less.decomp_quasi sign t of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15103
diff changeset
   191
    SOME (x, rel, y) => (case rel of
15103
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   192
      "<"   => ([Less (x, y, Asm ~1)], Asm 0)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   193
    | "<="  => ([Le (x, y, Asm ~1)], Asm 0)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   194
    | "~="  => ([NotEq (x,y, Asm ~1)], Asm 0)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   195
    | _  => raise Cannot)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15103
diff changeset
   196
| NONE => raise Cannot;
15103
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   197
  
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   198
  
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   199
(* ******************************************************************* *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   200
(*                                                                     *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   201
(* mergeLess (less1,less2):  less * less -> less                       *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   202
(*                                                                     *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   203
(* Merge to elements of type less according to the following rules     *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   204
(*                                                                     *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   205
(* x <= y && y <= z ==> x <= z                                         *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   206
(* x <= y && x ~= y ==> x < y                                          *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   207
(* x ~= y && x <= y ==> x < y                                          *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   208
(*                                                                     *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   209
(* ******************************************************************* *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   210
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   211
fun mergeLess (Le (x, _, p) , Le (_ , z, q)) =
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   212
      Le (x, z, Thm ([p,q] , Less.le_trans))
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   213
|   mergeLess (Le (x, z, p) , NotEq (x', z', q)) =
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   214
      if (x aconv x' andalso z aconv z' ) 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   215
       then Less (x, z, Thm ([p,q] , Less.le_neq_trans))
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   216
        else error "quasi_tac: internal error le_neq_trans"
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   217
|   mergeLess (NotEq (x, z, p) , Le (x' , z', q)) =
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   218
      if (x aconv x' andalso z aconv z') 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   219
      then Less (x, z, Thm ([p,q] , Less.neq_le_trans))
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   220
      else error "quasi_tac: internal error neq_le_trans"
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   221
|   mergeLess (_, _) =
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   222
      error "quasi_tac: internal error: undefined case";
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   223
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   224
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   225
(* ******************************************************************** *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   226
(* tr checks for valid transitivity step                                *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   227
(* ******************************************************************** *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   228
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   229
infix tr;
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   230
fun (Le (_, y, _))   tr (Le (x', _, _))   = ( y aconv x' )
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   231
  | _ tr _ = false;
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   232
  
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   233
(* ******************************************************************* *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   234
(*                                                                     *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   235
(* transPath (Lesslist, Less): (less list * less) -> less              *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   236
(*                                                                     *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   237
(* If a path represented by a list of elements of type less is found,  *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   238
(* this needs to be contracted to a single element of type less.       *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   239
(* Prior to each transitivity step it is checked whether the step is   *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   240
(* valid.                                                              *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   241
(*                                                                     *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   242
(* ******************************************************************* *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   243
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   244
fun transPath ([],lesss) = lesss
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   245
|   transPath (x::xs,lesss) =
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   246
      if lesss tr x then transPath (xs, mergeLess(lesss,x))
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   247
      else error "trans/quasi_tac: internal error transpath";
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   248
  
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   249
(* ******************************************************************* *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   250
(*                                                                     *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   251
(* less1 subsumes less2 : less -> less -> bool                         *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   252
(*                                                                     *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   253
(* subsumes checks whether less1 implies less2                         *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   254
(*                                                                     *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   255
(* ******************************************************************* *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   256
  
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   257
infix subsumes;
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   258
fun (Le (x, y, _)) subsumes (Le (x', y', _)) =
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   259
      (x aconv x' andalso y aconv y')
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   260
  | (Le _) subsumes (Less _) =
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   261
      error "trans/quasi_tac: internal error: Le cannot subsume Less"
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   262
  | (NotEq(x,y,_)) subsumes (NotEq(x',y',_)) = x aconv x' andalso y aconv y' orelse x aconv y' andalso y aconv x'
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   263
  | _ subsumes _ = false;
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   264
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   265
(* ******************************************************************* *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   266
(*                                                                     *)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15103
diff changeset
   267
(* triv_solv less1 : less ->  proof option                     *)
15103
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   268
(*                                                                     *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   269
(* Solves trivial goal x <= x.                                         *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   270
(*                                                                     *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   271
(* ******************************************************************* *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   272
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   273
fun triv_solv (Le (x, x', _)) =
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15103
diff changeset
   274
    if x aconv x' then  SOME (Thm ([], Less.le_refl)) 
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15103
diff changeset
   275
    else NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15103
diff changeset
   276
|   triv_solv _ = NONE;
15103
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   277
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   278
(* ********************************************************************* *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   279
(* Graph functions                                                       *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   280
(* ********************************************************************* *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   281
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   282
(* *********************************************************** *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   283
(* Functions for constructing graphs                           *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   284
(* *********************************************************** *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   285
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   286
fun addEdge (v,d,[]) = [(v,d)]
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   287
|   addEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   288
    else (u,dl):: (addEdge(v,d,el));
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   289
    
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   290
(* ********************************************************************** *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   291
(*                                                                        *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   292
(* mkQuasiGraph constructs from a list of objects of type less a graph g, *) 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   293
(* by taking all edges that are candidate for a <=, and a list neqE, by   *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   294
(* taking all edges that are candiate for a ~=                            *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   295
(*                                                                        *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   296
(* ********************************************************************** *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   297
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   298
fun mkQuasiGraph [] = ([],[])
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   299
|   mkQuasiGraph lessList = 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   300
 let
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   301
 fun buildGraphs ([],leG, neqE) = (leG,  neqE)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   302
  |   buildGraphs (l::ls, leG,  neqE) = case l of 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   303
       (Less (x,y,p)) =>
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   304
         let 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   305
	  val leEdge  = Le (x,y, Thm ([p], Less.less_imp_le)) 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   306
	  val neqEdges = [ NotEq (x,y, Thm ([p], Less.less_imp_neq)),
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   307
	                   NotEq (y,x, Thm ( [Thm ([p], Less.less_imp_neq)], thm "not_sym"))]
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   308
	 in
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   309
           buildGraphs (ls, addEdge(y,[],(addEdge (x,[(y,leEdge)],leG))), neqEdges@neqE) 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   310
	 end
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   311
     |  (Le (x,y,p))   => buildGraphs (ls, addEdge(y,[],(addEdge (x,[(y,l)],leG))), neqE) 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   312
     | _ =>  buildGraphs (ls, leG,  l::neqE) ;
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   313
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   314
in buildGraphs (lessList, [],  []) end;
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   315
  
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   316
(* ********************************************************************** *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   317
(*                                                                        *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   318
(* mkGraph constructs from a list of objects of type less a graph g       *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   319
(* Used for plain transitivity chain reasoning.                           *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   320
(*                                                                        *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   321
(* ********************************************************************** *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   322
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   323
fun mkGraph [] = []
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   324
|   mkGraph lessList = 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   325
 let
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   326
  fun buildGraph ([],g) = g
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   327
  |   buildGraph (l::ls, g) =  buildGraph (ls, (addEdge ((lower l),[((upper l),l)],g))) 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   328
     
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   329
in buildGraph (lessList, []) end;
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   330
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   331
(* *********************************************************************** *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   332
(*                                                                         *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   333
(* adjacent g u : (''a * 'b list ) list -> ''a -> 'b list                  *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   334
(*                                                                         *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   335
(* List of successors of u in graph g                                      *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   336
(*                                                                         *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   337
(* *********************************************************************** *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   338
 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   339
fun adjacent eq_comp ((v,adj)::el) u = 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   340
    if eq_comp (u, v) then adj else adjacent eq_comp el u
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   341
|   adjacent _  []  _ = []  
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   342
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   343
(* *********************************************************************** *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   344
(*                                                                         *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   345
(* dfs eq_comp g u v:                                                      *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   346
(* ('a * 'a -> bool) -> ('a  *( 'a * less) list) list ->                   *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   347
(* 'a -> 'a -> (bool * ('a * less) list)                                   *) 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   348
(*                                                                         *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   349
(* Depth first search of v from u.                                         *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   350
(* Returns (true, path(u, v)) if successful, otherwise (false, []).        *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   351
(*                                                                         *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   352
(* *********************************************************************** *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   353
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   354
fun dfs eq_comp g u v = 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   355
 let 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   356
    val pred = ref nil;
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   357
    val visited = ref nil;
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   358
    
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   359
    fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   360
    
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   361
    fun dfs_visit u' = 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   362
    let val _ = visited := u' :: (!visited)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   363
    
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   364
    fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   365
    
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   366
    in if been_visited v then () 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   367
    else (app (fn (v',l) => if been_visited v' then () else (
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   368
       update (v',l); 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   369
       dfs_visit v'; ()) )) (adjacent eq_comp g u')
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   370
     end
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   371
  in 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   372
    dfs_visit u; 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   373
    if (been_visited v) then (true, (!pred)) else (false , [])   
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   374
  end;
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   375
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   376
(* ************************************************************************ *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   377
(*                                                                          *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   378
(* Begin: Quasi Order relevant functions                                    *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   379
(*                                                                          *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   380
(*                                                                          *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   381
(* ************************************************************************ *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   382
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   383
(* ************************************************************************ *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   384
(*                                                                          *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   385
(* findPath x y g: Term.term -> Term.term ->                                *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   386
(*                  (Term.term * (Term.term * less list) list) ->           *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   387
(*                  (bool, less list)                                       *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   388
(*                                                                          *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   389
(*  Searches a path from vertex x to vertex y in Graph g, returns true and  *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   390
(*  the list of edges forming the path, if a path is found, otherwise false *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   391
(*  and nil.                                                                *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   392
(*                                                                          *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   393
(* ************************************************************************ *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   394
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   395
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   396
 fun findPath x y g = 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   397
  let 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   398
    val (found, tmp) =  dfs (op aconv) g x y ;
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   399
    val pred = map snd tmp;
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   400
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   401
    fun path x y  =
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   402
      let
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   403
       (* find predecessor u of node v and the edge u -> v *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   404
       fun lookup v [] = raise Cannot
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   405
       |   lookup v (e::es) = if (upper e) aconv v then e else lookup v es;
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   406
		
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   407
       (* traverse path backwards and return list of visited edges *)   
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   408
       fun rev_path v = 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   409
 	let val l = lookup v pred
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   410
            val u = lower l;
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   411
 	in
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   412
           if u aconv x then [l] else (rev_path u) @ [l] 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   413
	end
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   414
      in rev_path y end;
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   415
		
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   416
  in 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   417
   if found then (
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   418
    if x aconv y then (found,[(Le (x, y, (Thm ([], Less.le_refl))))])
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   419
    else (found, (path x y) )) 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   420
   else (found,[])
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   421
  end; 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   422
	
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   423
      
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   424
(* ************************************************************************ *) 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   425
(*                                                                          *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   426
(* findQuasiProof (leqG, neqE) subgoal:                                     *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   427
(* (Term.term * (Term.term * less list) list) * less list  -> less -> proof *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   428
(*                                                                          *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   429
(* Constructs a proof for subgoal by searching a special path in leqG and   *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   430
(* neqE. Raises Cannot if construction of the proof fails.                  *)   
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   431
(*                                                                          *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   432
(* ************************************************************************ *) 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   433
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   434
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   435
(* As the conlusion can be either of form x <= y, x < y or x ~= y we have        *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   436
(* three cases to deal with. Finding a transitivity path from x to y with label  *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   437
(* 1. <=                                                                         *) 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   438
(*    This is simply done by searching any path from x to y in the graph leG.    *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   439
(*    The graph leG contains only edges with label <=.                           *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   440
(*                                                                               *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   441
(* 2. <                                                                          *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   442
(*    A path from x to y with label < can be found by searching a path with      *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   443
(*    label <= from x to y in the graph leG and merging the path x <= y with     *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   444
(*    a parallel edge x ~= y resp. y ~= x to x < y.                              *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   445
(*                                                                               *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   446
(* 3. ~=                                                                         *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   447
(*   If the conclusion is of form x ~= y, we can find a proof either directly,   *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   448
(*   if x ~= y or y ~= x are among the assumptions, or by constructing x ~= y if *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   449
(*   x < y or y < x follows from the assumptions.                                *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   450
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   451
fun findQuasiProof (leG, neqE) subgoal =
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   452
  case subgoal of (Le (x,y, _)) => (
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   453
   let 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   454
    val (xyLefound,xyLePath) = findPath x y leG 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   455
   in
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   456
    if xyLefound then (
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   457
     let 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   458
      val Le_x_y = (transPath (tl xyLePath, hd xyLePath))
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   459
     in getprf Le_x_y end )
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   460
    else raise Cannot
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   461
   end )
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   462
  | (Less (x,y,_))  => (
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   463
   let 
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15103
diff changeset
   464
    fun findParallelNeq []  = NONE
15103
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   465
    |   findParallelNeq (e::es)  =
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15103
diff changeset
   466
     if      (x aconv (lower e) andalso y aconv (upper e)) then SOME e
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15103
diff changeset
   467
     else if (y aconv (lower e) andalso x aconv (upper e)) then SOME (NotEq (x,y, (Thm ([getprf e], thm "not_sym"))))
15103
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   468
     else findParallelNeq es ;  
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   469
   in
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   470
   (* test if there is a edge x ~= y respectivly  y ~= x and     *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   471
   (* if it possible to find a path x <= y in leG, thus we can conclude x < y *)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15103
diff changeset
   472
    (case findParallelNeq neqE of (SOME e) => 
15103
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   473
      let 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   474
       val (xyLeFound,xyLePath) = findPath x y leG 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   475
      in
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   476
       if xyLeFound then (
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   477
        let 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   478
         val Le_x_y = (transPath (tl xyLePath, hd xyLePath))
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   479
         val Less_x_y = mergeLess (e, Le_x_y)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   480
        in getprf Less_x_y end
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   481
       ) else raise Cannot
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   482
      end 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   483
    | _ => raise Cannot)    
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   484
   end )
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   485
 | (NotEq (x,y,_)) => 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   486
  (* First check if a single premiss is sufficient *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   487
  (case (Library.find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15103
diff changeset
   488
    (SOME (NotEq (x, y, p)), NotEq (x', y', _)) =>
15103
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   489
      if  (x aconv x' andalso y aconv y') then p 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   490
      else Thm ([p], thm "not_sym")
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   491
    | _  => raise Cannot 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   492
  )
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   493
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   494
      
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   495
(* ************************************************************************ *) 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   496
(*                                                                          *) 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   497
(* End: Quasi Order relevant functions                                      *) 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   498
(*                                                                          *) 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   499
(*                                                                          *) 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   500
(* ************************************************************************ *) 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   501
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   502
(* *********************************************************************** *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   503
(*                                                                         *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   504
(* solveLeTrans sign (asms,concl) :                                        *)
19250
932a50e2332f got rid of type Sign.sg;
wenzelm
parents: 15570
diff changeset
   505
(* theory -> less list * Term.term -> proof list                           *)
15103
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   506
(*                                                                         *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   507
(* Solves                                                                  *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   508
(*                                                                         *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   509
(* *********************************************************************** *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   510
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   511
fun solveLeTrans sign (asms, concl) =
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   512
 let 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   513
  val g = mkGraph asms
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   514
 in
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   515
   let 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   516
    val (subgoal, prf) = mkconcl_trans sign concl
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   517
    val (found, path) = findPath (lower subgoal) (upper subgoal) g 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   518
   in
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   519
    if found then [getprf (transPath (tl path, hd path))] 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   520
    else raise Cannot
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   521
  end
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   522
 end;
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   523
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   524
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   525
(* *********************************************************************** *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   526
(*                                                                         *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   527
(* solveQuasiOrder sign (asms,concl) :                                     *)
19250
932a50e2332f got rid of type Sign.sg;
wenzelm
parents: 15570
diff changeset
   528
(* theory -> less list * Term.term -> proof list                           *)
15103
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   529
(*                                                                         *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   530
(* Find proof if possible for quasi order.                                 *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   531
(*                                                                         *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   532
(* *********************************************************************** *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   533
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   534
fun solveQuasiOrder sign (asms, concl) =
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   535
 let 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   536
  val (leG, neqE) = mkQuasiGraph asms
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   537
 in
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   538
   let 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   539
   val (subgoals, prf) = mkconcl_quasi sign concl
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   540
   fun solve facts less =
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15103
diff changeset
   541
       (case triv_solv less of NONE => findQuasiProof (leG, neqE) less
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15103
diff changeset
   542
       | SOME prf => prf )
15103
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   543
  in   map (solve asms) subgoals end
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   544
 end;
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   545
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   546
(* ************************************************************************ *) 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   547
(*                                                                          *) 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   548
(* Tactics                                                                  *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   549
(*                                                                          *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   550
(*  - trans_tac                                                          *)                     
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   551
(*  - quasi_tac, solves quasi orders                                        *)                     
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   552
(* ************************************************************************ *) 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   553
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   554
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   555
(* trans_tac - solves transitivity chains over <= *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   556
val trans_tac  =  SUBGOAL (fn (A, n, sign) =>
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   557
 let
29276
94b1ffec9201 qualified Term.rename_wrt_term;
wenzelm
parents: 22578
diff changeset
   558
  val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A))
15103
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   559
  val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   560
  val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   561
  val lesss = List.concat (ListPair.map (mkasm_trans  sign) (Hs, 0 upto (length Hs - 1)))
15103
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   562
  val prfs = solveLeTrans  sign (lesss, C);
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   563
  
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   564
  val (subgoal, prf) = mkconcl_trans  sign C;
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   565
 in
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   566
  
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   567
  METAHYPS (fn asms =>
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   568
    let val thms = map (prove asms) prfs
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   569
    in rtac (prove thms prf) 1 end) n
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   570
  
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   571
 end
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   572
 handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   573
      | Cannot  => no_tac
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   574
);
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   575
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   576
(* quasi_tac - solves quasi orders *)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   577
val quasi_tac = SUBGOAL (fn (A, n, sign) =>
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   578
 let
29276
94b1ffec9201 qualified Term.rename_wrt_term;
wenzelm
parents: 22578
diff changeset
   579
  val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A))
15103
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   580
  val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   581
  val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   582
  val lesss = List.concat (ListPair.map (mkasm_quasi sign) (Hs, 0 upto (length Hs - 1)))
15103
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   583
  val prfs = solveQuasiOrder sign (lesss, C);
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   584
  val (subgoals, prf) = mkconcl_quasi sign C;
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   585
 in
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   586
 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   587
  METAHYPS (fn asms =>
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   588
    let val thms = map (prove asms) prfs
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   589
    in rtac (prove thms prf) 1 end) n
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   590
 
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   591
 end
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   592
 handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   593
      | Cannot  => no_tac
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   594
);
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   595
   
79846e8792eb New transitivity reasoners for transitivity only and quasi orders.
ballarin
parents:
diff changeset
   596
end;