- notation fix for reducible and normal forms

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / reducibility / trf.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/trf.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/trf.ma
index ccdf59224fd0ea15abc19dbc17b58d250f0b6e5f..3ae5bfd176e142ef0a505e4fa93f4e8d0e1c585d 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/trf.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/trf.ma
@@ -14,34 +14,26 @@
 
 include "Basic_2/grammar/term_simple.ma".
 
-(* CONTEXT-FREE REDUCIBLE AND IRREDUCIBLE TERMS *****************************)
+(* CONTEXT-FREE REDUCIBLE TERMS *********************************************)
 
 (* reducible terms *)
-inductive trf: term → Prop ≝
-| trf_abst_sn: ∀V,T.   trf V → trf (𝕔{Abst} V. T)
-| trf_abst_dx: ∀V,T.   trf T → trf (𝕔{Abst} V. T)
-| trf_appl_sn: ∀V,T.   trf V → trf (𝕔{Appl} V. T)
-| trf_appl_dx: ∀V,T.   trf T → trf (𝕔{Appl} V. T)
-| trf_abbr   : ∀V,T.           trf (𝕔{Abbr} V. T)
-| trf_cast   : ∀V,T.           trf (𝕔{Cast} V. T)
-| trf_beta   : ∀V,W,T. trf (𝕔{Appl} V. 𝕔{Abst} W. T)
+inductive trf: predicate term ≝
+| trf_abst_sn: ∀V,T.   trf V → trf (ⓛV. T)
+| trf_abst_dx: ∀V,T.   trf T → trf (ⓛV. T)
+| trf_appl_sn: ∀V,T.   trf V → trf (ⓐV. T)
+| trf_appl_dx: ∀V,T.   trf T → trf (ⓐV. T)
+| trf_abbr   : ∀V,T.           trf (ⓓV. T)
+| trf_cast   : ∀V,T.           trf (ⓣV. T)
+| trf_beta   : ∀V,W,T. trf (ⓐV. ⓛW. T)
 .
 
 interpretation
    "context-free reducibility (term)"
    'Reducible T = (trf T).
 
-(* irreducible terms *)
-definition tif: term → Prop ≝
-   λT. ℝ[T] → False.
-
-interpretation
-   "context-free irreducibility (term)"
-   'NotReducible T = (tif T).
-
 (* Basic inversion lemmas ***************************************************)
 
-fact trf_inv_atom_aux: ∀I,T. ℝ[T] → T =  𝕒{I} → False.
+fact trf_inv_atom_aux: ∀I,T. 𝐑[T] → T =  ⓪{I} → False.
 #I #T * -T
 [ #V #T #_ #H destruct
 | #V #T #_ #H destruct
@@ -53,13 +45,13 @@ fact trf_inv_atom_aux: ∀I,T. ℝ[T] → T =  𝕒{I} → False.
 ]
 qed.
 
-lemma trf_inv_atom: ∀I. ℝ[𝕒{I}] → False.
-/2/ qed-.
+lemma trf_inv_atom: ∀I. 𝐑[⓪{I}] → False.
+/2 width=4/ qed-.
 
-fact trf_inv_abst_aux: ∀W,U,T. ℝ[T] → T =  𝕔{Abst} W. U → ℝ[W] ∨ ℝ[U].
+fact trf_inv_abst_aux: ∀W,U,T. 𝐑[T] → T =  ⓛW. U → 𝐑[W] ∨ 𝐑[U].
 #W #U #T * -T
-[ #V #T #HV #H destruct -V T /2/
-| #V #T #HT #H destruct -V T /2/
+[ #V #T #HV #H destruct /2 width=1/
+| #V #T #HT #H destruct /2 width=1/
 | #V #T #_ #H destruct
 | #V #T #_ #H destruct
 | #V #T #H destruct
@@ -68,52 +60,22 @@ fact trf_inv_abst_aux: ∀W,U,T. ℝ[T] → T =  𝕔{Abst} W. U → ℝ[W] ∨
 ]
 qed.
 
-lemma trf_inv_abst: ∀V,T. ℝ[𝕔{Abst}V.T] → ℝ[V] ∨ ℝ[T].
-/2/ qed-.
+lemma trf_inv_abst: ∀V,T. 𝐑[ⓛV.T] → 𝐑[V] ∨ 𝐑[T].
+/2 width=3/ qed-.
 
-fact trf_inv_appl_aux: ∀W,U,T. ℝ[T] → T =  𝕔{Appl} W. U →
-                       ∨∨ ℝ[W] | ℝ[U] | (𝕊[U] → False).
+fact trf_inv_appl_aux: ∀W,U,T. 𝐑[T] → T =  ⓐW. U →
+                       ∨∨ 𝐑[W] | 𝐑[U] | (𝐒[U] → False).
 #W #U #T * -T
 [ #V #T #_ #H destruct
 | #V #T #_ #H destruct
-| #V #T #HV #H destruct -V T /2/
-| #V #T #HT #H destruct -V T /2/
+| #V #T #HV #H destruct /2 width=1/
+| #V #T #HT #H destruct /2 width=1/
 | #V #T #H destruct
 | #V #T #H destruct
-| #V #W0 #T #H destruct -V U
+| #V #W0 #T #H destruct
   @or3_intro2 #H elim (simple_inv_bind … H)
 ]
 qed.
 
-lemma trf_inv_appl: ∀W,U. ℝ[𝕔{Appl}W.U] → ∨∨ ℝ[W] | ℝ[U] | (𝕊[U] → False).
-/2/ qed-.
-
-lemma tif_inv_abbr: ∀V,T. 𝕀[𝕔{Abbr}V.T] → False.
-/2/ qed-.
-
-lemma tif_inv_abst: ∀V,T. 𝕀[𝕔{Abst}V.T] → 𝕀[V] ∧ 𝕀[T].
-/4/ qed-.
-
-lemma tif_inv_appl: ∀V,T. 𝕀[𝕔{Appl}V.T] → ∧∧ 𝕀[V] & 𝕀[T] & 𝕊[T].
-#V #T #HVT @and3_intro /3/
-generalize in match HVT -HVT; elim T -T //
-* // * #U #T #_ #_ #H elim (H ?) -H /2/
-qed-.
-
-lemma tif_inv_cast: ∀V,T. 𝕀[𝕔{Cast}V.T] → False.
-/2/ qed-.
-
-(* Basic properties *********************************************************)
-
-lemma tif_atom: ∀I. 𝕀[𝕒{I}].
-/2/ qed.
-
-lemma tif_abst: ∀V,T. 𝕀[V] →  𝕀[T] →  𝕀[𝕔 {Abst}V.T].
-#V #T #HV #HT #H
-elim (trf_inv_abst … H) -H /2/
-qed.
-
-lemma tif_appl: ∀V,T. 𝕀[V] →  𝕀[T] →  𝕊[T] → 𝕀[𝕔{Appl}V.T].
-#V #T #HV #HT #S #H
-elim (trf_inv_appl … H) -H /2/
-qed.
+lemma trf_inv_appl: ∀W,U. 𝐑[ⓐW.U] → ∨∨ 𝐑[W] | 𝐑[U] | (𝐒[U] → False).
+/2 width=3/ qed-.