src/Provers/trancl.ML
author wenzelm
Sat, 16 Apr 2011 18:11:20 +0200
changeset 42364 8c674b3b8e44
parent 42361 23f352990944
child 43278 1fbdcebb364b
permissions -rw-r--r--
eliminated old List.nth; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
37744
3daaf23b9ab4 tuned titles
haftmann
parents: 36692
diff changeset
     1
(*  Title:      Provers/trancl.ML
30190
479806475f3c use long names for old-style fold combinators;
wenzelm
parents: 26834
diff changeset
     2
    Author:     Oliver Kutter, TU Muenchen
37744
3daaf23b9ab4 tuned titles
haftmann
parents: 36692
diff changeset
     3
3daaf23b9ab4 tuned titles
haftmann
parents: 36692
diff changeset
     4
Transitivity reasoner for transitive closures of relations
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
     5
*)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
     6
15098
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
     7
(*
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
     8
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
     9
The packages provides tactics trancl_tac and rtrancl_tac that prove
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
    10
goals of the form
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
    11
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
    12
   (x,y) : r^+     and     (x,y) : r^* (rtrancl_tac only)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
    13
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
    14
from premises of the form
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
    15
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
    16
   (x,y) : r,     (x,y) : r^+     and     (x,y) : r^* (rtrancl_tac only)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
    17
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
    18
by reflexivity and transitivity.  The relation r is determined by inspecting
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
    19
the conclusion.
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
    20
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
    21
The package is implemented as an ML functor and thus not limited to
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
    22
particular constructs for transitive and reflexive-transitive
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
    23
closures, neither need relations be represented as sets of pairs.  In
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
    24
order to instantiate the package for transitive closure only, supply
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
    25
dummy theorems to the additional rules for reflexive-transitive
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
    26
closures, and don't use rtrancl_tac!
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
    27
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
    28
*)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
    29
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
    30
signature TRANCL_ARITH =
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    31
sig
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    32
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    33
  (* theorems for transitive closure *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    34
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    35
  val r_into_trancl : thm
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    36
      (* (a,b) : r ==> (a,b) : r^+ *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    37
  val trancl_trans : thm
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    38
      (* [| (a,b) : r^+ ; (b,c) : r^+ |] ==> (a,c) : r^+ *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    39
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    40
  (* additional theorems for reflexive-transitive closure *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    41
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    42
  val rtrancl_refl : thm
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    43
      (* (a,a): r^* *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    44
  val r_into_rtrancl : thm
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    45
      (* (a,b) : r ==> (a,b) : r^* *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    46
  val trancl_into_rtrancl : thm
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    47
      (* (a,b) : r^+ ==> (a,b) : r^* *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    48
  val rtrancl_trancl_trancl : thm
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    49
      (* [| (a,b) : r^* ; (b,c) : r^+ |] ==> (a,c) : r^+ *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    50
  val trancl_rtrancl_trancl : thm
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    51
      (* [| (a,b) : r^+ ; (b,c) : r^* |] ==> (a,c) : r^+ *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    52
  val rtrancl_trans : thm
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    53
      (* [| (a,b) : r^* ; (b,c) : r^* |] ==> (a,c) : r^* *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    54
15098
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
    55
  (* decomp: decompose a premise or conclusion
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
    56
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
    57
     Returns one of the following:
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
    58
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15098
diff changeset
    59
     NONE if not an instance of a relation,
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15098
diff changeset
    60
     SOME (x, y, r, s) if instance of a relation, where
15098
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
    61
       x: left hand side argument, y: right hand side argument,
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
    62
       r: the relation,
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
    63
       s: the kind of closure, one of
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
    64
            "r":   the relation itself,
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
    65
            "r^+": transitive closure of the relation,
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
    66
            "r^*": reflexive-transitive closure of the relation
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
    67
  *)
15098
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
    68
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
    69
  val decomp: term ->  (term * term * term * string) option
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    70
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    71
end;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    72
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
    73
signature TRANCL_TAC =
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    74
sig
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
    75
  val trancl_tac: Proof.context -> int -> tactic
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
    76
  val rtrancl_tac: Proof.context -> int -> tactic
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    77
end;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    78
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
    79
functor Trancl_Tac(Cls: TRANCL_ARITH): TRANCL_TAC =
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    80
struct
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    81
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
    82
22257
159bfab776e2 "prove" function now instantiates relation variable in order
berghofe
parents: 15574
diff changeset
    83
datatype proof
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
    84
  = Asm of int
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
    85
  | Thm of proof list * thm;
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    86
22257
159bfab776e2 "prove" function now instantiates relation variable in order
berghofe
parents: 15574
diff changeset
    87
exception Cannot; (* internal exception: raised if no proof can be found *)
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    88
26834
87a5b9ec3863 Terms returned by decomp are now eta-contracted.
berghofe
parents: 22257
diff changeset
    89
fun decomp t = Option.map (fn (x, y, rel, r) =>
87a5b9ec3863 Terms returned by decomp are now eta-contracted.
berghofe
parents: 22257
diff changeset
    90
  (Envir.beta_eta_contract x, Envir.beta_eta_contract y,
87a5b9ec3863 Terms returned by decomp are now eta-contracted.
berghofe
parents: 22257
diff changeset
    91
   Envir.beta_eta_contract rel, r)) (Cls.decomp t);
87a5b9ec3863 Terms returned by decomp are now eta-contracted.
berghofe
parents: 22257
diff changeset
    92
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
    93
fun prove thy r asms =
22257
159bfab776e2 "prove" function now instantiates relation variable in order
berghofe
parents: 15574
diff changeset
    94
  let
159bfab776e2 "prove" function now instantiates relation variable in order
berghofe
parents: 15574
diff changeset
    95
    fun inst thm =
26834
87a5b9ec3863 Terms returned by decomp are now eta-contracted.
berghofe
parents: 22257
diff changeset
    96
      let val SOME (_, _, r', _) = decomp (concl_of thm)
22257
159bfab776e2 "prove" function now instantiates relation variable in order
berghofe
parents: 15574
diff changeset
    97
      in Drule.cterm_instantiate [(cterm_of thy r', cterm_of thy r)] thm end;
42364
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 42361
diff changeset
    98
    fun pr (Asm i) = nth asms i
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 42361
diff changeset
    99
      | pr (Thm (prfs, thm)) = map pr prfs MRS inst thm;
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   100
  in pr end;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   101
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   102
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   103
(* Internal datatype for inequalities *)
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   104
datatype rel
15098
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   105
   = Trans  of term * term * proof  (* R^+ *)
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   106
   | RTrans of term * term * proof; (* R^* *)
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   107
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   108
 (* Misc functions for datatype rel *)
15098
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   109
fun lower (Trans (x, _, _)) = x
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   110
  | lower (RTrans (x,_,_)) = x;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   111
15098
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   112
fun upper (Trans (_, y, _)) = y
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   113
  | upper (RTrans (_,y,_)) = y;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   114
15098
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   115
fun getprf   (Trans   (_, _, p)) = p
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   116
|   getprf   (RTrans (_,_, p)) = p;
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   117
15098
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   118
(* ************************************************************************ *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   119
(*                                                                          *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   120
(*  mkasm_trancl Rel (t,n): term -> (term , int) -> rel list                *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   121
(*                                                                          *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   122
(*  Analyse assumption t with index n with respect to relation Rel:         *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   123
(*  If t is of the form "(x, y) : Rel" (or Rel^+), translate to             *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   124
(*  an object (singleton list) of internal datatype rel.                    *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   125
(*  Otherwise return empty list.                                            *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   126
(*                                                                          *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   127
(* ************************************************************************ *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   128
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   129
fun mkasm_trancl  Rel  (t, n) =
26834
87a5b9ec3863 Terms returned by decomp are now eta-contracted.
berghofe
parents: 22257
diff changeset
   130
  case decomp t of
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   131
    SOME (x, y, rel,r) => if rel aconv Rel then
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   132
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   133
    (case r of
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   134
      "r"   => [Trans (x,y, Thm([Asm n], Cls.r_into_trancl))]
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   135
    | "r+"  => [Trans (x,y, Asm n)]
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   136
    | "r*"  => []
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   137
    | _     => error ("trancl_tac: unknown relation symbol"))
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   138
    else []
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15098
diff changeset
   139
  | NONE => [];
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   140
15098
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   141
(* ************************************************************************ *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   142
(*                                                                          *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   143
(*  mkasm_rtrancl Rel (t,n): term -> (term , int) -> rel list               *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   144
(*                                                                          *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   145
(*  Analyse assumption t with index n with respect to relation Rel:         *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   146
(*  If t is of the form "(x, y) : Rel" (or Rel^+ or Rel^* ), translate to   *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   147
(*  an object (singleton list) of internal datatype rel.                    *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   148
(*  Otherwise return empty list.                                            *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   149
(*                                                                          *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   150
(* ************************************************************************ *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   151
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   152
fun mkasm_rtrancl Rel (t, n) =
26834
87a5b9ec3863 Terms returned by decomp are now eta-contracted.
berghofe
parents: 22257
diff changeset
   153
  case decomp t of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15098
diff changeset
   154
   SOME (x, y, rel, r) => if rel aconv Rel then
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   155
    (case r of
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   156
      "r"   => [ Trans (x,y, Thm([Asm n], Cls.r_into_trancl))]
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   157
    | "r+"  => [ Trans (x,y, Asm n)]
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   158
    | "r*"  => [ RTrans(x,y, Asm n)]
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   159
    | _     => error ("rtrancl_tac: unknown relation symbol" ))
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   160
   else []
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15098
diff changeset
   161
  | NONE => [];
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   162
15098
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   163
(* ************************************************************************ *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   164
(*                                                                          *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   165
(*  mkconcl_trancl t: term -> (term, rel, proof)                            *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   166
(*  mkconcl_rtrancl t: term -> (term, rel, proof)                           *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   167
(*                                                                          *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   168
(*  Analyse conclusion t:                                                   *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   169
(*    - must be of form "(x, y) : r^+ (or r^* for rtrancl)                  *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   170
(*    - returns r                                                           *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   171
(*    - conclusion in internal form                                         *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   172
(*    - proof object                                                        *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   173
(*                                                                          *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   174
(* ************************************************************************ *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   175
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   176
fun mkconcl_trancl  t =
26834
87a5b9ec3863 Terms returned by decomp are now eta-contracted.
berghofe
parents: 22257
diff changeset
   177
  case decomp t of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15098
diff changeset
   178
    SOME (x, y, rel, r) => (case r of
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   179
      "r+"  => (rel, Trans (x,y, Asm ~1), Asm 0)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   180
    | _     => raise Cannot)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15098
diff changeset
   181
  | NONE => raise Cannot;
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   182
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   183
fun mkconcl_rtrancl  t =
26834
87a5b9ec3863 Terms returned by decomp are now eta-contracted.
berghofe
parents: 22257
diff changeset
   184
  case decomp t of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15098
diff changeset
   185
    SOME (x,  y, rel,r ) => (case r of
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   186
      "r+"  => (rel, Trans (x,y, Asm ~1),  Asm 0)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   187
    | "r*"  => (rel, RTrans (x,y, Asm ~1), Asm 0)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   188
    | _     => raise Cannot)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15098
diff changeset
   189
  | NONE => raise Cannot;
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   190
15098
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   191
(* ************************************************************************ *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   192
(*                                                                          *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   193
(*  makeStep (r1, r2): rel * rel -> rel                                     *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   194
(*                                                                          *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   195
(*  Apply transitivity to r1 and r2, obtaining a new element of r^+ or r^*, *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   196
(*  according the following rules:                                          *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   197
(*                                                                          *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   198
(* ( (a, b) : r^+ , (b,c) : r^+ ) --> (a,c) : r^+                           *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   199
(* ( (a, b) : r^* , (b,c) : r^+ ) --> (a,c) : r^+                           *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   200
(* ( (a, b) : r^+ , (b,c) : r^* ) --> (a,c) : r^+                           *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   201
(* ( (a, b) : r^* , (b,c) : r^* ) --> (a,c) : r^*                           *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   202
(*                                                                          *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   203
(* ************************************************************************ *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   204
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   205
fun makeStep (Trans (a,_,p), Trans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.trancl_trans))
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   206
(* refl. + trans. cls. rules *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   207
|   makeStep (RTrans (a,_,p), Trans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.rtrancl_trancl_trancl))
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   208
|   makeStep (Trans (a,_,p), RTrans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.trancl_rtrancl_trancl))
15098
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   209
|   makeStep (RTrans (a,_,p), RTrans(_,c,q))  = RTrans (a,c, Thm ([p,q], Cls.rtrancl_trans));
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   210
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   211
(* ******************************************************************* *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   212
(*                                                                     *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   213
(* transPath (Clslist, Cls): (rel  list * rel) -> rel                  *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   214
(*                                                                     *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   215
(* If a path represented by a list of elements of type rel is found,   *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   216
(* this needs to be contracted to a single element of type rel.        *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   217
(* Prior to each transitivity step it is checked whether the step is   *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   218
(* valid.                                                              *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   219
(*                                                                     *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   220
(* ******************************************************************* *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   221
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   222
fun transPath ([],acc) = acc
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   223
|   transPath (x::xs,acc) = transPath (xs, makeStep(acc,x))
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   224
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   225
(* ********************************************************************* *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   226
(* Graph functions                                                       *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   227
(* ********************************************************************* *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   228
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   229
(* *********************************************************** *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   230
(* Functions for constructing graphs                           *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   231
(* *********************************************************** *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   232
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   233
fun addEdge (v,d,[]) = [(v,d)]
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   234
|   addEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   235
    else (u,dl):: (addEdge(v,d,el));
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   236
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   237
(* ********************************************************************** *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   238
(*                                                                        *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   239
(* mkGraph constructs from a list of objects of type rel  a graph g       *)
15098
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   240
(* and a list of all edges with label r+.                                 *)
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   241
(*                                                                        *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   242
(* ********************************************************************** *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   243
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   244
fun mkGraph [] = ([],[])
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   245
|   mkGraph ys =
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   246
 let
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   247
  fun buildGraph ([],g,zs) = (g,zs)
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   248
  |   buildGraph (x::xs, g, zs) =
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   249
        case x of (Trans (_,_,_)) =>
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   250
               buildGraph (xs, addEdge((upper x), [],(addEdge ((lower x),[((upper x),x)],g))), x::zs)
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   251
        | _ => buildGraph (xs, addEdge((upper x), [],(addEdge ((lower x),[((upper x),x)],g))), zs)
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   252
in buildGraph (ys, [], []) end;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   253
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   254
(* *********************************************************************** *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   255
(*                                                                         *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   256
(* adjacent g u : (''a * 'b list ) list -> ''a -> 'b list                  *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   257
(*                                                                         *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   258
(* List of successors of u in graph g                                      *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   259
(*                                                                         *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   260
(* *********************************************************************** *)
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   261
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   262
fun adjacent eq_comp ((v,adj)::el) u =
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   263
    if eq_comp (u, v) then adj else adjacent eq_comp el u
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   264
|   adjacent _  []  _ = []
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   265
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   266
(* *********************************************************************** *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   267
(*                                                                         *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   268
(* dfs eq_comp g u v:                                                      *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   269
(* ('a * 'a -> bool) -> ('a  *( 'a * rel) list) list ->                    *)
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   270
(* 'a -> 'a -> (bool * ('a * rel) list)                                    *)
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   271
(*                                                                         *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   272
(* Depth first search of v from u.                                         *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   273
(* Returns (true, path(u, v)) if successful, otherwise (false, []).        *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   274
(*                                                                         *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   275
(* *********************************************************************** *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   276
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   277
fun dfs eq_comp g u v =
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   278
 let
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32285
diff changeset
   279
    val pred = Unsynchronized.ref [];
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32285
diff changeset
   280
    val visited = Unsynchronized.ref [];
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   281
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   282
    fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   283
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   284
    fun dfs_visit u' =
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   285
    let val _ = visited := u' :: (!visited)
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   286
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   287
    fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   288
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   289
    in if been_visited v then ()
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   290
    else (app (fn (v',l) => if been_visited v' then () else (
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   291
       update (v',l);
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   292
       dfs_visit v'; ()) )) (adjacent eq_comp g u')
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   293
     end
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   294
  in
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   295
    dfs_visit u;
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   296
    if (been_visited v) then (true, (!pred)) else (false , [])
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   297
  end;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   298
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   299
(* *********************************************************************** *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   300
(*                                                                         *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   301
(* transpose g:                                                            *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   302
(* (''a * ''a list) list -> (''a * ''a list) list                          *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   303
(*                                                                         *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   304
(* Computes transposed graph g' from g                                     *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   305
(* by reversing all edges u -> v to v -> u                                 *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   306
(*                                                                         *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   307
(* *********************************************************************** *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   308
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   309
fun transpose eq_comp g =
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   310
  let
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   311
   (* Compute list of reversed edges for each adjacency list *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   312
   fun flip (u,(v,l)::el) = (v,(u,l)) :: flip (u,el)
32768
wenzelm
parents: 32740
diff changeset
   313
     | flip (_,[]) = []
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   314
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   315
   (* Compute adjacency list for node u from the list of edges
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   316
      and return a likewise reduced list of edges.  The list of edges
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   317
      is searches for edges starting from u, and these edges are removed. *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   318
   fun gather (u,(v,w)::el) =
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   319
    let
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   320
     val (adj,edges) = gather (u,el)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   321
    in
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   322
     if eq_comp (u, v) then (w::adj,edges)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   323
     else (adj,(v,w)::edges)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   324
    end
32768
wenzelm
parents: 32740
diff changeset
   325
   | gather (_,[]) = ([],[])
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   326
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   327
   (* For every node in the input graph, call gather to find all reachable
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   328
      nodes in the list of edges *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   329
   fun assemble ((u,_)::el) edges =
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   330
       let val (adj,edges) = gather (u,edges)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   331
       in (u,adj) :: assemble el edges
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   332
       end
32768
wenzelm
parents: 32740
diff changeset
   333
     | assemble [] _ = []
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   334
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   335
   (* Compute, for each adjacency list, the list with reversed edges,
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   336
      and concatenate these lists. *)
32768
wenzelm
parents: 32740
diff changeset
   337
   val flipped = maps flip g
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   338
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   339
 in assemble g flipped end
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   340
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   341
(* *********************************************************************** *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   342
(*                                                                         *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   343
(* dfs_reachable eq_comp g u:                                              *)
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   344
(* (int * int list) list -> int -> int list                                *)
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   345
(*                                                                         *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   346
(* Computes list of all nodes reachable from u in g.                       *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   347
(*                                                                         *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   348
(* *********************************************************************** *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   349
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   350
fun dfs_reachable eq_comp g u =
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   351
 let
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   352
  (* List of vertices which have been visited. *)
32768
wenzelm
parents: 32740
diff changeset
   353
  val visited  = Unsynchronized.ref [];
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   354
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   355
  fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   356
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   357
  fun dfs_visit g u  =
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   358
      let
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   359
   val _ = visited := u :: !visited
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   360
   val descendents =
30190
479806475f3c use long names for old-style fold combinators;
wenzelm
parents: 26834
diff changeset
   361
       List.foldr (fn ((v,l),ds) => if been_visited v then ds
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   362
            else v :: dfs_visit g v @ ds)
32768
wenzelm
parents: 32740
diff changeset
   363
        [] (adjacent eq_comp g u)
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   364
   in  descendents end
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   365
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   366
 in u :: dfs_visit g u end;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   367
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   368
(* *********************************************************************** *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   369
(*                                                                         *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   370
(* dfs_term_reachable g u:                                                  *)
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   371
(* (term * term list) list -> term -> term list                            *)
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   372
(*                                                                         *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   373
(* Computes list of all nodes reachable from u in g.                       *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   374
(*                                                                         *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   375
(* *********************************************************************** *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   376
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   377
fun dfs_term_reachable g u = dfs_reachable (op aconv) g u;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   378
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   379
(* ************************************************************************ *)
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   380
(*                                                                          *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   381
(* findPath x y g: Term.term -> Term.term ->                                *)
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   382
(*                  (Term.term * (Term.term * rel list) list) ->            *)
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   383
(*                  (bool, rel list)                                        *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   384
(*                                                                          *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   385
(*  Searches a path from vertex x to vertex y in Graph g, returns true and  *)
15098
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   386
(*  the list of edges if path is found, otherwise false and nil.            *)
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   387
(*                                                                          *)
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   388
(* ************************************************************************ *)
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   389
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   390
fun findPath x y g =
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   391
  let
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   392
   val (found, tmp) =  dfs (op aconv) g x y ;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   393
   val pred = map snd tmp;
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   394
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   395
   fun path x y  =
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   396
    let
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   397
         (* find predecessor u of node v and the edge u -> v *)
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   398
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   399
      fun lookup v [] = raise Cannot
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   400
      |   lookup v (e::es) = if (upper e) aconv v then e else lookup v es;
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   401
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   402
      (* traverse path backwards and return list of visited edges *)
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   403
      fun rev_path v =
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   404
        let val l = lookup v pred
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   405
            val u = lower l;
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   406
        in
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   407
          if u aconv x then [l] else (rev_path u) @ [l]
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   408
        end
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   409
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   410
    in rev_path y end;
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   411
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   412
   in
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   413
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   414
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   415
      if found then ( (found, (path x y) )) else (found,[])
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   416
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   417
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   418
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   419
   end;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   420
15098
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   421
(* ************************************************************************ *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   422
(*                                                                          *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   423
(* findRtranclProof g tranclEdges subgoal:                                  *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   424
(* (Term.term * (Term.term * rel list) list) -> rel -> proof list           *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   425
(*                                                                          *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   426
(* Searches in graph g a proof for subgoal.                                 *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   427
(*                                                                          *)
0726e7b15618 Documentation added/improved.
ballarin
parents: 15078
diff changeset
   428
(* ************************************************************************ *)
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   429
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   430
fun findRtranclProof g tranclEdges subgoal =
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   431
   case subgoal of (RTrans (x,y,_)) => if x aconv y then [Thm ([], Cls.rtrancl_refl)] else (
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   432
     let val (found, path) = findPath (lower subgoal) (upper subgoal) g
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   433
     in
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   434
       if found then (
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   435
          let val path' = (transPath (tl path, hd path))
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   436
          in
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   437
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   438
            case path' of (Trans (_,_,p)) => [Thm ([p], Cls.trancl_into_rtrancl )]
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   439
            | _ => [getprf path']
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   440
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   441
          end
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   442
       )
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   443
       else raise Cannot
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   444
     end
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   445
   )
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   446
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   447
| (Trans (x,y,_)) => (
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   448
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   449
  let
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   450
   val Vx = dfs_term_reachable g x;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   451
   val g' = transpose (op aconv) g;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   452
   val Vy = dfs_term_reachable g' y;
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   453
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   454
   fun processTranclEdges [] = raise Cannot
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   455
   |   processTranclEdges (e::es) =
36692
54b64d4ad524 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents: 35281
diff changeset
   456
          if member (op =) Vx (upper e) andalso member (op =) Vx (lower e)
54b64d4ad524 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents: 35281
diff changeset
   457
          andalso member (op =) Vy (upper e) andalso member (op =) Vy (lower e)
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   458
          then (
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   459
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   460
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   461
            if (lower e) aconv x then (
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   462
              if (upper e) aconv y then (
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   463
                  [(getprf e)]
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   464
              )
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   465
              else (
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   466
                  let
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   467
                    val (found,path) = findPath (upper e) y g
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   468
                  in
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   469
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   470
                   if found then (
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   471
                       [getprf (transPath (path, e))]
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   472
                      ) else processTranclEdges es
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   473
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   474
                  end
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   475
              )
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   476
            )
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   477
            else if (upper e) aconv y then (
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   478
               let val (xufound,xupath) = findPath x (lower e) g
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   479
               in
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   480
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   481
                  if xufound then (
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   482
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   483
                    let val xuRTranclEdge = transPath (tl xupath, hd xupath)
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   484
                            val xyTranclEdge = makeStep(xuRTranclEdge,e)
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   485
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   486
                                in [getprf xyTranclEdge] end
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   487
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   488
                 ) else processTranclEdges es
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   489
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   490
               end
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   491
            )
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   492
            else (
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   493
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   494
                let val (xufound,xupath) = findPath x (lower e) g
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   495
                    val (vyfound,vypath) = findPath (upper e) y g
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   496
                 in
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   497
                    if xufound then (
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   498
                         if vyfound then (
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   499
                            let val xuRTranclEdge = transPath (tl xupath, hd xupath)
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   500
                                val vyRTranclEdge = transPath (tl vypath, hd vypath)
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   501
                                val xyTranclEdge = makeStep (makeStep(xuRTranclEdge,e),vyRTranclEdge)
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   502
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   503
                                in [getprf xyTranclEdge] end
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   504
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   505
                         ) else processTranclEdges es
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   506
                    )
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   507
                    else processTranclEdges es
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   508
                 end
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   509
            )
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   510
          )
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   511
          else processTranclEdges es;
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   512
   in processTranclEdges tranclEdges end )
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   513
| _ => raise Cannot
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   514
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   515
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   516
fun solveTrancl (asms, concl) =
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   517
 let val (g,_) = mkGraph asms
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   518
 in
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   519
  let val (_, subgoal, _) = mkconcl_trancl concl
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   520
      val (found, path) = findPath (lower subgoal) (upper subgoal) g
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   521
  in
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   522
    if found then  [getprf (transPath (tl path, hd path))]
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   523
    else raise Cannot
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   524
  end
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   525
 end;
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   526
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   527
fun solveRtrancl (asms, concl) =
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   528
 let val (g,tranclEdges) = mkGraph asms
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   529
     val (_, subgoal, _) = mkconcl_rtrancl concl
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   530
in
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   531
  findRtranclProof g tranclEdges subgoal
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   532
end;
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   533
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   534
32277
ff1e59a15146 trans_tac: use theory from goal state, not the static context, which seems to be outdated under certain circumstances (why?);
wenzelm
parents: 32215
diff changeset
   535
fun trancl_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   536
 let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 37744
diff changeset
   537
  val thy = Proof_Context.theory_of ctxt;
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   538
  val Hs = Logic.strip_assums_hyp A;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   539
  val C = Logic.strip_assums_concl A;
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   540
  val (rel, subgoals, prf) = mkconcl_trancl C;
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   541
33063
4d462963a7db map_range (and map_index) combinator
haftmann
parents: 32768
diff changeset
   542
  val prems = flat (map_index (mkasm_trancl rel o swap) Hs);
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   543
  val prfs = solveTrancl (prems, C);
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   544
 in
35281
206e2f1759cc Fixed bug that caused (r)trancl_tac to crash when the term denoting the relation
berghofe
parents: 33063
diff changeset
   545
  Subgoal.FOCUS (fn {prems, concl, ...} =>
206e2f1759cc Fixed bug that caused (r)trancl_tac to crash when the term denoting the relation
berghofe
parents: 33063
diff changeset
   546
    let
206e2f1759cc Fixed bug that caused (r)trancl_tac to crash when the term denoting the relation
berghofe
parents: 33063
diff changeset
   547
      val SOME (_, _, rel', _) = decomp (term_of concl);
206e2f1759cc Fixed bug that caused (r)trancl_tac to crash when the term denoting the relation
berghofe
parents: 33063
diff changeset
   548
      val thms = map (prove thy rel' prems) prfs
206e2f1759cc Fixed bug that caused (r)trancl_tac to crash when the term denoting the relation
berghofe
parents: 33063
diff changeset
   549
    in rtac (prove thy rel' thms prf) 1 end) ctxt n st
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   550
 end
32277
ff1e59a15146 trans_tac: use theory from goal state, not the static context, which seems to be outdated under certain circumstances (why?);
wenzelm
parents: 32215
diff changeset
   551
 handle Cannot => Seq.empty);
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   552
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   553
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   554
fun rtrancl_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   555
 let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 37744
diff changeset
   556
  val thy = Proof_Context.theory_of ctxt;
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   557
  val Hs = Logic.strip_assums_hyp A;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   558
  val C = Logic.strip_assums_concl A;
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   559
  val (rel, subgoals, prf) = mkconcl_rtrancl C;
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   560
33063
4d462963a7db map_range (and map_index) combinator
haftmann
parents: 32768
diff changeset
   561
  val prems = flat (map_index (mkasm_rtrancl rel o swap) Hs);
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   562
  val prfs = solveRtrancl (prems, C);
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   563
 in
35281
206e2f1759cc Fixed bug that caused (r)trancl_tac to crash when the term denoting the relation
berghofe
parents: 33063
diff changeset
   564
  Subgoal.FOCUS (fn {prems, concl, ...} =>
206e2f1759cc Fixed bug that caused (r)trancl_tac to crash when the term denoting the relation
berghofe
parents: 33063
diff changeset
   565
    let
206e2f1759cc Fixed bug that caused (r)trancl_tac to crash when the term denoting the relation
berghofe
parents: 33063
diff changeset
   566
      val SOME (_, _, rel', _) = decomp (term_of concl);
206e2f1759cc Fixed bug that caused (r)trancl_tac to crash when the term denoting the relation
berghofe
parents: 33063
diff changeset
   567
      val thms = map (prove thy rel' prems) prfs
206e2f1759cc Fixed bug that caused (r)trancl_tac to crash when the term denoting the relation
berghofe
parents: 33063
diff changeset
   568
    in rtac (prove thy rel' thms prf) 1 end) ctxt n st
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   569
 end
32215
87806301a813 replaced old METAHYPS by FOCUS;
wenzelm
parents: 30190
diff changeset
   570
 handle Cannot => Seq.empty | Subscript => Seq.empty);
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   571
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   572
end;