(* Basic_1: was: flt_wf__q_ind *)
(* Basic_1: was: flt_wf_ind *)
-axiom cw_wf_ind: ∀R:lenv→term→Prop.
+axiom cw_wf_ind: ∀R:lenv→predicate term.
(∀L2,T2. (∀L1,T1. #[L1,T1] < #[L2,T2] → R L1 T1) → R L2 T2) →
∀L,T. R L T.
(* SIMPLE (NEUTRAL) TERMS ***************************************************)
-inductive simple: term → Prop ≝
+inductive simple: predicate term ≝
| simple_atom: ∀I. simple (𝕒{I})
| simple_flat: ∀I,V,T. simple (𝕗{I} V. T)
.
(* Basic eliminators ********************************************************)
-axiom tw_wf_ind: ∀R:term→Prop.
+axiom tw_wf_ind: ∀R:predicate term.
(∀T2. (∀T1. #[T1] < #[T2] → R T1) → R T2) →
∀T. R T.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "Basic_2/grammar/term_simple.ma".
+
+(* CANDIDATES OF REDUCIBILITY ***********************************************)
+
+(* abstract conditions for candidates *)
+
+definition CR1: predicate term → predicate term → Prop ≝
+ λRD,RC. ∀T. RC T → RD T.
+
+definition CR2: relation term → predicate term → Prop ≝
+ λRR,RC. ∀T1,T2. RC T1 → 𝕊[T1] → RR T1 T2 → RC T2.
+
+definition CR3: relation term → predicate term → Prop ≝
+ λRR,RC. ∀T1. (∀T2. RR T1 T2 → RC T2) → 𝕊[T1] → RC T1.
+
+(* a candidate *)
+record cr (RR:relation term) (RD:predicate term): Type[0] ≝ {
+ in_cr: predicate term;
+ cr1: CR1 RD in_cr;
+ cr2: CR2 RR in_cr;
+ cr3: CR3 RR in_cr
+}.
+
+interpretation
+ "context-free parallel reduction (term)"
+ 'InSubset T R = (in_cr ? ? R T).
+
+definition in_fun_cr: ∀RR,RD. ∀D,C:(cr RR RD). predicate term ≝
+ λRR,RD,D,C,T. ∀V. V ϵ D → 𝕔{Appl}V.T ϵ C.
(* CONTEXT-FREE NORMAL TERMS ************************************************)
-definition tnf: term → Prop ≝
- NF … tpr (eq …).
+definition tnf: predicate term ≝ NF … tpr (eq …).
interpretation
"context-free normality (term)"
(* CONTEXT-FREE REDUCIBLE AND IRREDUCIBLE TERMS *****************************)
(* reducible terms *)
-inductive trf: term → Prop ≝
+inductive trf: predicate term ≝
| 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)
'Reducible T = (trf T).
(* irreducible terms *)
-definition tif: term → Prop ≝
- λT. ℝ[T] → False.
+definition tif: predicate term ≝ λT. ℝ[T] → False.
interpretation
"context-free irreducibility (term)"
(* CONTEXT-FREE WEAK HEAD NORMAL TERMS **************************************)
-definition twhnf: term → Prop ≝
- NF … tpr thom.
+definition twhnf: predicate term ≝ NF … tpr thom.
interpretation
"context-free weak head normality (term)"
(* Basic eliminators ********************************************************)
-lemma ltpss_ind: ∀d,e,L1. ∀R: lenv → Prop. R L1 →
+lemma ltpss_ind: ∀d,e,L1. ∀R:predicate lenv. R L1 →
(∀L,L2. L1 [d, e] ≫* L → L [d, e] ≫ L2 → R L → R L2) →
∀L2. L1 [d, e] ≫* L2 → R L2.
#d #e #L1 #R #HL1 #IHL1 #L2 #HL12 @(TC_star_ind … HL1 IHL1 … HL12) //
(* Basic eliminators ********************************************************)
-lemma tpss_ind: ∀d,e,L,T1. ∀R: term → Prop. R T1 →
+lemma tpss_ind: ∀d,e,L,T1. ∀R:predicate term. R T1 →
(∀T,T2. L ⊢ T1 [d, e] ≫* T → L ⊢ T [d, e] ≫ T2 → R T → R T2) →
∀T2. L ⊢ T1 [d, e] ≫* T2 → R T2.
#d #e #L #T1 #R #HT1 #IHT1 #T2 #HT12 @(TC_star_ind … HT1 IHT1 … HT12) //
(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* Subsets ******************************************************************)
+
+notation "hvbox( T ϵ break R )"
+ non associative with precedence 45
+ for @{ 'InSubset $T $R }.
+
(* Lists ********************************************************************)
notation "hvbox( hd break :: tl )"
(* PROPERTIES of RELATIONS **************************************************)
+definition predicate: Type[0] → Type[0] ≝ λA. A → Prop.
+
definition Decidable: Prop → Prop ≝
λR. R ∨ (R → False).
lemma TC_reflexive: ∀A,R. reflexive A R → reflexive A (TC … R).
/2/ qed.
-lemma TC_star_ind: ∀A,R. reflexive A R → ∀a1. ∀P:A→Prop.
+lemma TC_star_ind: ∀A,R. reflexive A R → ∀a1. ∀P:predicate A.
P a1 → (∀a,a2. TC … R a1 a → R a a2 → P a → P a2) →
∀a2. TC … R a1 a2 → P a2.
#A #R #H #a1 #P #Ha1 #IHa1 #a2 #Ha12 elim Ha12 -Ha12 a2 /3/
qed.
-definition NF: ∀A. relation A → relation A → A → Prop ≝
+definition NF: ∀A. relation A → relation A → predicate A ≝
λA,R,S,a1. ∀a2. R a1 a2 → S a1 a2.
-inductive SN (A) (R,S:relation A): A → Prop ≝
+inductive SN (A) (R,S:relation A): predicate A ≝
| SN_intro: ∀a1. (∀a2. R a1 a2 → (S a1 a2 → False) → SN A R S a2) → SN A R S a1
.
projects / helm.git / commitdiff