matita/contribs/LOGIC/Track/inv.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15
  16
  17 include "Track/defs.ma".
  18
  19 (* Main inversion lemmas ****************************************************)
  20
  21 theorem track_inv_lref: \forall Q,S,i. Track Q (lref i) S \to
  22                         \exists p1,p2,P. Insert p1 p2 S i P Q.
  23  intros; inversion H; clear H; intros; destruct; autobatch depth = 4.
  24 qed.
  25
  26 theorem track_inv_prin: \forall P,S,h. Track P (prin h) S \to
  27                         S = pair (posr h) (posr h).
  28  intros; inversion H; clear H; intros; destruct; autobatch.
  29 qed.
  30
  31 theorem track_inv_impw: \forall P,p,S. Track P (impw p) S \to
  32                         \exists B,a,b.
  33                         S = pair (impl a b) B \land
  34                         Track P p (pair lleaf B).
  35  intros; inversion H; clear H; intros; destruct; autobatch depth = 5.
  36 qed.
  37
  38 theorem track_inv_impr: \forall Q,p,S. Track Q (impr p) S \to
  39                         \exists a,b:Formula.
  40                         S = pair lleaf (impl a b) \land
  41                         Track Q p (pair a b).
  42  intros; inversion H; clear H; intros; destruct; autobatch depth = 4.
  43 qed.
  44
  45 theorem track_inv_impi: \forall P,p,q,r,S. Track P (impi p q r) S \to
  46                         \exists A,B,D. \exists a,b:Formula.
  47                         S = pair (impl a b) D \land
  48                         Track P p (pair A a) \land
  49                         Track P q (pair b B) \land
  50                         Track (abst P p q (pair A B)) r (pair lleaf D).
  51  intros; inversion H; clear H; intros; destruct; autobatch depth = 9 width = 4 size = 12.
  52 qed.
  53
  54 theorem track_inv_scut: \forall P,q,r,S. Track P (scut q r) S \to
  55                         \exists A,B. \exists c:Formula.
  56                         S = pair A B \land
  57                         Track P q (pair A c) \land
  58                         Track P r (pair c B).
  59  intros; inversion H; clear H; intros; destruct; autobatch depth = 6 size = 8.
  60 qed.