helm/software/matita/contribs/ng_assembly/freescale/theory.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                           Progetto FreeScale                           *)
  17 (*                                                                        *)
  18 (* Sviluppato da:                                                         *)
  19 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  20 (*                                                                        *)
  21 (* Questo materiale fa parte della tesi:                                  *)
  22 (*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
  23 (*                                                                        *)
  24 (*                    data ultima modifica 15/11/2007                     *)
  25 (* ********************************************************************** *)
  26
  27 include "freescale/pts.ma".
  28
  29 (* ********************************** *)
  30 (* SOTTOINSIEME MINIMALE DELLA TEORIA *)
  31 (* ********************************** *)
  32
  33 ninductive True: Prop ≝
  34  I : True.
  35
  36 ndefinition True_ind : ΠP:Prop.P → True → P ≝
  37 λP:Prop.λp:P.λH:True.
  38  match H with [ I ⇒ p ].
  39
  40 ndefinition True_rec : ΠP:Set.P → True → P ≝
  41 λP:Set.λp:P.λH:True.
  42  match H with [ I ⇒ p ].
  43
  44 ndefinition True_rect : ΠP:Type.P → True → P ≝
  45 λP:Type.λp:P.λH:True.
  46  match H with [ I ⇒ p ].
  47
  48 ninductive False: Prop ≝.
  49
  50 ndefinition False_ind : ΠP:Prop.False → P ≝
  51 λP:Prop.λH:False.
  52  match H in False return λH1:False.P with [].
  53
  54 ndefinition False_rec : ΠP:Set.False → P ≝
  55 λP:Set.λH:False.
  56  match H in False return λH1:False.P with [].
  57
  58 ndefinition False_rect : ΠP:Type.False → P ≝
  59 λP:Type.λH:False.
  60  match H in False return λH1:False.P with [].
  61
  62 ndefinition Not: Prop → Prop ≝
  63 λA.(A → False).
  64
  65 interpretation "logical not" 'not x = (Not x).
  66
  67 ntheorem absurd : ∀A,C:Prop.A → ¬A → C.
  68  #A; #C; #H;
  69  nnormalize;
  70  #H1;
  71  nelim (H1 H).
  72 nqed.
  73
  74 ntheorem not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
  75  #A; #B; #H;
  76  nnormalize;
  77  #H1; #H2;
  78  nelim (H1 (H H2)).
  79 nqed.
  80
  81 ninductive And (A,B:Prop) : Prop ≝
  82  conj : A → B → (And A B).
  83
  84 ndefinition And_ind : ΠA,B:Prop.ΠP:Prop.(A → B → P) → And A B → P ≝
  85 λA,B:Prop.λP:Prop.λf:A → B → P.λH:And A B.
  86  match H with [conj H1 H2 ⇒ f H1 H2 ].
  87
  88 ndefinition And_rec : ΠA,B:Prop.ΠP:Set.(A → B → P) → And A B → P ≝
  89 λA,B:Prop.λP:Set.λf:A → B → P.λH:And A B.
  90  match H with [conj H1 H2 ⇒ f H1 H2 ].
  91
  92 ndefinition And_rect : ΠA,B:Prop.ΠP:Type.(A → B → P) → And A B → P ≝
  93 λA,B:Prop.λP:Type.λf:A → B → P.λH:And A B.
  94  match H with [conj H1 H2 ⇒ f H1 H2 ].
  95
  96 interpretation "logical and" 'and x y = (And x y).
  97
  98 ntheorem proj1: ∀A,B:Prop.A ∧ B → A.
  99  #A; #B; #H;
 100  napply (And_ind A B ?? H);
 101  #H1; #H2;
 102  napply H1.
 103 nqed.
 104
 105 ntheorem proj2: ∀A,B:Prop.A ∧ B → B.
 106  #A; #B; #H;
 107  napply (And_ind A B ?? H);
 108  #H1; #H2;
 109  napply H2.
 110 nqed.
 111
 112 ninductive Or (A,B:Prop) : Prop ≝
 113   or_introl : A → (Or A B)
 114 | or_intror : B → (Or A B).
 115
 116 ndefinition Or_ind : ΠA,B:Prop.ΠP:Prop.(A → P) → (B → P) → Or A B → P ≝
 117 λA,B:Prop.λP:Prop.λf1:A → P.λf2:B → P.λH:Or A B.
 118  match H with [ or_introl H1 ⇒ f1 H1 | or_intror H1 ⇒ f2 H1 ].
 119
 120 interpretation "logical or" 'or x y = (Or x y).
 121
 122 ndefinition decidable : Prop → Prop ≝ λA:Prop.A ∨ ¬A.
 123
 124 ninductive ex (A:Type) (Q:A → Prop) : Prop ≝
 125  ex_intro: ∀x:A.Q x → ex A Q.
 126
 127 ndefinition ex_ind : ΠA:Type.ΠQ:A → Prop.ΠP:Prop.(Πa:A.Q a → P) → ex A Q → P ≝
 128 λA:Type.λQ:A → Prop.λP:Prop.λf:(Πa:A.Q a → P).λH:ex A Q.
 129  match H with [ ex_intro H1 H2 ⇒ f H1 H2 ].
 130
 131 interpretation "exists" 'exists x = (ex ? x).
 132
 133 ninductive ex2 (A:Type) (Q,R:A → Prop) : Prop ≝
 134  ex_intro2: ∀x:A.Q x → R x → ex2 A Q R.
 135
 136 ndefinition ex2_ind : ΠA:Type.ΠQ,R:A → Prop.ΠP:Prop.(Πa:A.Q a → R a → P) → ex2 A Q R → P ≝
 137 λA:Type.λQ,R:A → Prop.λP:Prop.λf:(Πa:A.Q a → R a → P).λH:ex2 A Q R.
 138  match H with [ ex_intro2 H1 H2 H3 ⇒ f H1 H2 H3 ].
 139
 140 ndefinition iff ≝
 141 λA,B.(A -> B) ∧ (B -> A).
 142
 143 ndefinition relation : Type → Type ≝
 144 λA:Type.A → A → Prop.
 145
 146 ndefinition reflexive : ∀A:Type.∀R:relation A.Prop ≝
 147 λA.λR.∀x:A.R x x.
 148
 149 ndefinition symmetric : ∀A:Type.∀R:relation A.Prop ≝
 150 λA.λR.∀x,y:A.R x y → R y x.
 151
 152 ndefinition transitive : ∀A:Type.∀R:relation A.Prop ≝
 153 λA.λR.∀x,y,z:A.R x y → R y z → R x z.
 154
 155 ndefinition irreflexive : ∀A:Type.∀R:relation A.Prop ≝
 156 λA.λR.∀x:A.¬ (R x x).
 157
 158 ndefinition cotransitive : ∀A:Type.∀R:relation A.Prop ≝
 159 λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y.
 160
 161 ndefinition tight_apart : ∀A:Type.∀eq,ap:relation A.Prop ≝
 162 λA.λeq,ap.∀x,y:A. (¬ (ap x y) → eq x y) ∧ (eq x y → ¬ (ap x y)).
 163
 164 ndefinition antisymmetric : ∀A:Type.∀R:relation A.Prop ≝
 165 λA.λR.∀x,y:A.R x y → ¬ (R y x).
 166
 167 ninductive eq (A:Type) (x:A) : A → Prop ≝
 168  refl_eq : eq A x x.
 169
 170 ndefinition eq_ind : ΠA:Type.Πx:A.ΠP:A → Prop.P x → Πa:A.eq A x a → P a ≝
 171 λA:Type.λx:A.λP:A → Prop.λp:P x.λa:A.λH:eq A x a.
 172  match H with [refl_eq ⇒ p ].
 173
 174 ndefinition eq_rec : ΠA:Type.Πx:A.ΠP:A → Set.P x → Πa:A.eq A x a → P a ≝
 175 λA:Type.λx:A.λP:A → Set.λp:P x.λa:A.λH:eq A x a.
 176  match H with [refl_eq ⇒ p ].
 177
 178 ndefinition eq_rect : ΠA:Type.Πx:A.ΠP:A → Type.P x → Πa:A.eq A x a → P a ≝
 179 λA:Type.λx:A.λP:A → Type.λp:P x.λa:A.λH:eq A x a.
 180  match H with [refl_eq ⇒ p ].
 181
 182 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
 183
 184 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
 185
 186 ntheorem symmetric_eq: ∀A:Type. symmetric A (eq A).
 187  #A;
 188  nnormalize;
 189  #x; #y; #H;
 190  nrewrite < H;
 191  napply (refl_eq ??).
 192 nqed.
 193
 194 ntheorem eq_elim_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
 195  #A; #x; #P; #H; #y; #H1;
 196  napply (eq_ind ? x ? H y ?);
 197  nrewrite < H1;
 198  napply (refl_eq ??).
 199 nqed.