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 set "baseuri" "cic:/matita/LOGIC/Track/inv".
  16
  17 include "Track/defs.ma".
  18
  19 theorem track_inv_lref: \forall Q,S,i. Track Q (lref i) S \to
  20                         \exists P. Insert S i P Q.
  21  intros; inversion H; clear H; intros; subst; autobatch.
  22 qed.
  23
  24 theorem track_inv_parx: \forall P,S,h. Track P (parx h) S \to
  25                         S = pair (posr h) (posr h).
  26  intros; inversion H; clear H; intros; subst; autobatch.
  27 qed.
  28
  29 theorem track_inv_impw: \forall P,p,S. Track P (impw p) S \to
  30                         \exists B,a,b.
  31                         S = pair (impl a b) B \land
  32                         Track P p (pair lleaf B).
  33  intros; inversion H; clear H; intros; subst; autobatch depth = 5.
  34 qed.
  35
  36 theorem track_inv_impr: \forall P,p,S. Track P (impr p) S \to
  37                         \exists a,b:Formula.
  38                         S = pair lleaf (impl a b) \land
  39                         Track P p (pair a b).
  40  intros; inversion H; clear H; intros; subst; autobatch depth = 4.
  41 qed.
  42
  43 theorem track_inv_impi: \forall P,p,q,r,S. Track P (impi p q r) S \to
  44                         \exists Q,A,B,D,i. \exists a,b:Formula.
  45                         S = pair (impl a b) D \land
  46                         Track P p (pair A a) \land
  47                         Track P q (pair b B) \land
  48                         Track Q r (pair lleaf D) \land
  49                         Insert (pair A B) i P Q.
  50  intros; inversion H; clear H; intros; subst; autobatch depth = 12 width = 5 size = 16.
  51 qed.
  52
  53 theorem track_inv_scut: \forall P,q,r,S. Track P (scut q r) S \to False.
  54  intros; inversion H; clear H; intros; subst.
  55 qed.
  56
  57 theorem track_inv_lleaf_impl:
  58    \forall Q,p,a,b. Track Q p (pair lleaf (impl a b)) \to
  59    (\exists P,i. p = lref i \land Insert (pair lleaf (impl a b)) i P Q) \lor
  60    (\exists r. p = impr r \land Track Q r (pair a b)).
  61  intros; inversion H; clear H; intros; subst;
  62  [ autobatch depth = 5
  63  | subst; autobatch depth = 4
  64  ].
  65 qed.