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