--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR DELAYED UPDATING ********************************************)
+
+notation "hvbox( ππ )"
+ non associative with precedence 75
+ for @{ 'ClassDPhi }.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR DELAYED UPDATING ********************************************)
+
+notation "hvbox( β΅ term 75 t )"
+ non associative with precedence 75
+ for @{ 'UpTriangle $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 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR DELAYED UPDATING ********************************************)
-
-notation "hvbox( t Ο΅ break ππ )"
- non associative with precedence 45
- for @{ 'InPredicateDPhi $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 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR DELAYED UPDATING ********************************************)
-
-notation "hvbox( p Ο΅β΅ break term 46 t )"
- non associative with precedence 45
- for @{ 'UpArrowEpsilon $p $t }.
include "ground/xoa/ex_4_2.ma".
include "ground/xoa/ex_4_3.ma".
include "ground/xoa/ex_5_3.ma".
+include "delayed_updating/syntax/preterm_equivalence.ma".
include "delayed_updating/syntax/preterm_constructors.ma".
-include "delayed_updating/notation/relations/in_predicate_d_phi_1.ma".
+include "delayed_updating/notation/functions/class_d_phi_0.ma".
(* BY-DEPTH DELAYED (BDD) TERM **********************************************)
-inductive bdd: predicate preterm β
+inductive bdd: π«β¨pretermβ© β
| bdd_oref: βn. bdd #n
| bdd_iref: βt,n. bdd t β bdd πn.t
| bdd_abst: βt. bdd t β bdd π.t
| bdd_appl: βu,t. bdd u β bdd t β bdd @u.t
+| bdd_conv: βt1,t2. t1 β t2 β bdd t1 β bdd t2
.
interpretation
- "well-formed by-depth delayed (preterm)"
- 'InPredicateDPhi t = (bdd t).
+ "by-depth delayed (preterm)"
+ 'ClassDPhi = (bdd).
(* Basic inversions *********************************************************)
lemma bdd_inv_in_comp_gen:
- βt,p. t Ο΅ ππ β p ϡ⬦ t β
- β¨β¨ ββn. #n = t & π±β¨nβ©;π = p
- | ββu,q,n. u Ο΅ ππ & q ϡ⬦ u & πn.u = t & π±β¨nβ©;q = p
- | ββu,q. u Ο΅ ππ & q ϡ⬦ u & π.u = t & π;q = p
- | ββv,u,q. v Ο΅ ππ & u Ο΅ ππ & q ϡ⬦ u & @v.u = t & π;q = p
- | ββv,u,q. v Ο΅ ππ & u Ο΅ ππ & q ϡ⬦ v & @v.u = t & π¦;q = p
+ βt,p. t Ο΅ ππ β p Ο΅ t β
+ β¨β¨ ββn. #n β t & π±β¨nβ©;π = p
+ | ββu,q,n. u Ο΅ ππ & q Ο΅ u & πn.u β t & π±β¨nβ©;q = p
+ | ββu,q. u Ο΅ ππ & q Ο΅ u & π.u β t & π;q = p
+ | ββv,u,q. v Ο΅ ππ & u Ο΅ ππ & q Ο΅ u & @v.u β t & π;q = p
+ | ββv,u,q. v Ο΅ ππ & u Ο΅ ππ & q Ο΅ v & @v.u β t & π¦;q = p
.
-#t #p *
+#t #p #H elim H -H
[ #n * /3 width=3 by or5_intro0, ex2_intro/
-| #u #n #Hu * #q #Hq #Hp /3 width=7 by ex4_3_intro, or5_intro1/
-| #u #Hu * #q #Hq #Hp /3 width=6 by or5_intro2, ex4_2_intro/
-| #v #u #Hv #Hu * * #q #Hq #Hp /3 width=8 by ex5_3_intro, or5_intro3, or5_intro4/
+| #u #n #Hu #_ * #q #Hq #Hp /3 width=7 by ex4_3_intro, or5_intro1/
+| #u #Hu #_ * #q #Hq #Hp /3 width=6 by or5_intro2, ex4_2_intro/
+| #v #u #Hv #Hu #_ #_ * * #q #Hq #Hp /3 width=8 by ex5_3_intro, or5_intro3, or5_intro4/
+| #t1 #t2 #Ht12 #_ #IH #Ht2
+ elim IH -IH [6: /2 width=3 by subset_in_eq_repl_fwd/ ] *
+ [ /4 width=3 by subset_eq_trans, or5_intro0, ex2_intro/
+ | /4 width=7 by subset_eq_trans, ex4_3_intro, or5_intro1/
+ | /4 width=6 by subset_eq_trans, or5_intro2, ex4_2_intro/
+ | /4 width=8 by subset_eq_trans, ex5_3_intro, or5_intro3/
+ | /4 width=8 by subset_eq_trans, ex5_3_intro, or5_intro4/
+ ]
]
qed-.
lemma bdd_inv_in_comp_d:
- βt,q,n. t Ο΅ ππ β π±β¨nβ©;q ϡ⬦ t β
- β¨β¨ β§β§ #n = t & π = q
- | ββu. u Ο΅ ππ & q ϡ⬦ u & πn.u = t
+ βt,q,n. t Ο΅ ππ β π±β¨nβ©;q Ο΅ t β
+ β¨β¨ β§β§ #n β t & π = q
+ | ββu. u Ο΅ ππ & q Ο΅ u & πn.u β t
.
#t #q #n #Ht #Hq
elim (bdd_inv_in_comp_gen β¦ Ht Hq) -Ht -Hq *
qed-.
lemma bdd_inv_in_root_d:
- βt,q,n. t Ο΅ ππ β π±β¨nβ©;q Ο΅β΅ t β
- β¨β¨ β§β§ #n = t & π = q
- | ββu. u Ο΅ ππ & q Ο΅β΅ u & πn.u = t
+ βt,q,n. t Ο΅ ππ β π±β¨nβ©;q Ο΅ β΅t β
+ β¨β¨ β§β§ #n β t & π = q
+ | ββu. u Ο΅ ππ & q Ο΅ β΅u & πn.u β t
.
#t #q #n #Ht * #r #Hq
elim (bdd_inv_in_comp_d β¦ Ht Hq) -Ht -Hq *
qed-.
lemma bdd_inv_in_comp_L:
- βt,q. t Ο΅ ππ β π;q ϡ⬦ t β
- ββu. u Ο΅ ππ & q ϡ⬦ u & π.u = t
+ βt,q. t Ο΅ ππ β π;q Ο΅ t β
+ ββu. u Ο΅ ππ & q Ο΅ u & π.u β t
.
#t #q #Ht #Hq
elim (bdd_inv_in_comp_gen β¦ Ht Hq) -Ht -Hq *
qed-.
lemma bdd_inv_in_root_L:
- βt,q. t Ο΅ ππ β π;q Ο΅β΅ t β
- ββu. u Ο΅ ππ & q Ο΅β΅ u & π.u = t.
+ βt,q. t Ο΅ ππ β π;q Ο΅ β΅t β
+ ββu. u Ο΅ ππ & q Ο΅ β΅u & π.u β t.
#t #q #Ht * #r #Hq
elim (bdd_inv_in_comp_L β¦ Ht Hq) -Ht -Hq
#u #Hu #Hq #H0 destruct
qed-.
lemma bdd_inv_in_comp_A:
- βt,q. t Ο΅ ππ β π;q ϡ⬦ t β
- ββv,u. v Ο΅ ππ & u Ο΅ ππ & q ϡ⬦ u & @v.u = t
+ βt,q. t Ο΅ ππ β π;q Ο΅ t β
+ ββv,u. v Ο΅ ππ & u Ο΅ ππ & q Ο΅ u & @v.u β t
.
#t #q #Ht #Hq
elim (bdd_inv_in_comp_gen β¦ Ht Hq) -Ht -Hq *
qed-.
lemma bdd_inv_in_root_A:
- βt,q. t Ο΅ ππ β π;q Ο΅β΅ t β
- ββv,u. v Ο΅ ππ & u Ο΅ ππ & q Ο΅β΅ u & @v.u = t
+ βt,q. t Ο΅ ππ β π;q Ο΅ β΅t β
+ ββv,u. v Ο΅ ππ & u Ο΅ ππ & q Ο΅ β΅u & @v.u β t
.
#t #q #Ht * #r #Hq
elim (bdd_inv_in_comp_A β¦ Ht Hq) -Ht -Hq
qed-.
lemma bdd_inv_in_comp_S:
- βt,q. t Ο΅ ππ β π¦;q ϡ⬦ t β
- ββv,u. v Ο΅ ππ & u Ο΅ ππ & q ϡ⬦ v & @v.u = t
+ βt,q. t Ο΅ ππ β π¦;q Ο΅ t β
+ ββv,u. v Ο΅ ππ & u Ο΅ ππ & q Ο΅ v & @v.u β t
.
#t #q #Ht #Hq
elim (bdd_inv_in_comp_gen β¦ Ht Hq) -Ht -Hq *
qed-.
lemma bdd_inv_in_root_S:
- βt,q. t Ο΅ ππ β π¦;q Ο΅β΅ t β
- ββv,u. v Ο΅ ππ & u Ο΅ ππ & q Ο΅β΅ v & @v.u = t
+ βt,q. t Ο΅ ππ β π¦;q Ο΅ β΅t β
+ ββv,u. v Ο΅ ππ & u Ο΅ ππ & q Ο΅ β΅v & @v.u β t
.
#t #q #Ht * #r #Hq
elim (bdd_inv_in_comp_S β¦ Ht Hq) -Ht -Hq
(* Advanced inversions ******************************************************)
lemma bbd_mono_in_root_d:
- βl,n,p,t. t Ο΅ ππ β p,π±β¨nβ© Ο΅β΅ t β p,l Ο΅β΅ t β π±β¨nβ© = l.
+ βl,n,p,t. t Ο΅ ππ β p,π±β¨nβ© Ο΅ β΅t β p,l Ο΅ β΅t β π±β¨nβ© = l.
#l #n #p elim p -p
[ #t #Ht <list_cons_comm <list_cons_comm #Hn #Hl
elim (bdd_inv_in_root_d β¦ Ht Hn) -Ht -Hn *
- [ #H0 #_ destruct
+ [ #H0 #_
+ lapply (preterm_root_eq_repl β¦ H0) -H0 #H0
+ lapply (subset_in_eq_repl_fwd ?? β¦ Hl β¦ H0) -H0 -Hl #Hl
elim (preterm_in_root_inv_lcons_oref β¦ Hl) -Hl //
- | #u #_ #_ #H0 destruct
+ | #u #_ #_ #H0
+ lapply (preterm_root_eq_repl β¦ H0) -H0 #H0
+ lapply (subset_in_eq_repl_fwd ?? β¦ Hl β¦ H0) -H0 -Hl #Hl
elim (preterm_in_root_inv_lcons_iref β¦ Hl) -Hl //
]
| * [ #m ] #p #IH #t #Ht
[ elim (bdd_inv_in_root_d β¦ Ht Hn) -Ht -Hn *
[ #_ #H0
elim (eq_inv_list_empty_rcons ??? H0)
- | #u #Hu #Hp #H0 destruct
+ | #u #Hu #Hp #H0
+ lapply (preterm_root_eq_repl β¦ H0) -H0 #H0
+ lapply (subset_in_eq_repl_fwd ?? β¦ Hl β¦ H0) -H0 -Hl #Hl
elim (preterm_in_root_inv_lcons_iref β¦ Hl) -Hl #_ #Hl
/2 width=4 by/
]
| elim (bdd_inv_in_root_L β¦ Ht Hn) -Ht -Hn
- #u #Hu #Hp #H0 destruct
+ #u #Hu #Hp #H0
+ lapply (preterm_root_eq_repl β¦ H0) -H0 #H0
+ lapply (subset_in_eq_repl_fwd ?? β¦ Hl β¦ H0) -H0 -Hl #Hl
elim (preterm_in_root_inv_lcons_abst β¦ Hl) -Hl #_ #Hl
/2 width=4 by/
| elim (bdd_inv_in_root_A β¦ Ht Hn) -Ht -Hn
- #v #u #_ #Hu #Hp #H0 destruct
+ #v #u #_ #Hu #Hp #H0
+ lapply (preterm_root_eq_repl β¦ H0) -H0 #H0
+ lapply (subset_in_eq_repl_fwd ?? β¦ Hl β¦ H0) -H0 -Hl #Hl
elim (preterm_in_root_inv_lcons_appl β¦ Hl) -Hl * #H0 #Hl destruct
/2 width=4 by/
| elim (bdd_inv_in_root_S β¦ Ht Hn) -Ht -Hn
- #v #u #Hv #_ #Hp #H0 destruct
+ #v #u #Hv #_ #Hp #H0
+ lapply (preterm_root_eq_repl β¦ H0) -H0 #H0
+ lapply (subset_in_eq_repl_fwd ?? β¦ Hl β¦ H0) -H0 -Hl #Hl
elim (preterm_in_root_inv_lcons_appl β¦ Hl) -Hl * #H0 #Hl destruct
/2 width=4 by/
]
(* *)
(**************************************************************************)
+include "ground/lib/subset.ma".
include "delayed_updating/syntax/path.ma".
-include "delayed_updating/notation/relations/up_down_arrow_epsilon_2.ma".
-include "delayed_updating/notation/relations/up_arrow_epsilon_2.ma".
+include "delayed_updating/notation/functions/uptriangle_1.ma".
(* PRETERM ******************************************************************)
-definition preterm: Type[0] β predicate path.
+(* Note: preterms are subsets of complete paths *)
+definition preterm: Type[0] β π«β¨pathβ©.
-definition preterm_in_comp: relation2 path preterm β
- Ξ»p,t. t p.
+definition preterm_root: preterm β preterm β
+ Ξ»t,p. βq. p;;q Ο΅ t.
interpretation
- "belongs to complete (preterm)"
- 'UpDownArrowEpsilon p t = (preterm_in_comp p t).
-
-definition preterm_in_root: relation2 path preterm β
- Ξ»p,t. βq. p;;q ϡ⬦ t.
-
-interpretation
- "belongs to root (preterm)"
- 'UpArrowEpsilon p t = (preterm_in_root p t).
+ "root (preterm)"
+ 'UpTriangle t = (preterm_root t).
(* Basic constructions ******************************************************)
lemma preterm_in_comp_root (p) (t):
- p ϡ⬦ t β p Ο΅β΅ t.
+ p Ο΅ t β p Ο΅ β΅t.
/2 width=2 by ex_intro/
qed.
Ξ»p. l;π = p.
definition preterm_node_1 (l): preterm β preterm β
- Ξ»t,p. ββq. q ϡ⬦ t & l;q = p.
+ Ξ»t,p. ββq. q Ο΅ t & l;q = p.
definition preterm_node_2 (l1) (l2): preterm β preterm β preterm β
Ξ»t1,t2,p.
- β¨β¨ ββq. q ϡ⬦ t1 & l1;q = p
- | ββq. q ϡ⬦ t2 & l2;q = p.
+ β¨β¨ ββq. q Ο΅ t1 & l1;q = p
+ | ββq. q Ο΅ t2 & l2;q = p.
interpretation
"outer variable reference by depth (preterm)"
(* Basic Inversions *********************************************************)
lemma preterm_in_root_inv_lcons_oref:
- βp,l,n. l;p Ο΅β΅ #n β
+ βp,l,n. l;p Ο΅ β΅#n β
β§β§ π±β¨nβ© = l & π = p.
#p #l #n * #q
<list_append_lcons_sn #H0 destruct -H0
qed-.
lemma preterm_in_root_inv_lcons_iref:
- βt,p,l,n. l;p Ο΅β΅ πn.t β
- β§β§ π±β¨nβ© = l & p Ο΅β΅ t.
+ βt,p,l,n. l;p Ο΅ β΅πn.t β
+ β§β§ π±β¨nβ© = l & p Ο΅ β΅t.
#t #p #l #n * #q
<list_append_lcons_sn * #r #Hr #H0 destruct
/3 width=2 by ex_intro, conj/
qed-.
lemma preterm_in_root_inv_lcons_abst:
- βt,p,l. l;p Ο΅β΅ π.t β
- β§β§ π = l & p Ο΅β΅ t.
+ βt,p,l. l;p Ο΅ β΅π.t β
+ β§β§ π = l & p Ο΅ β΅t.
#t #p #l * #q
<list_append_lcons_sn * #r #Hr #H0 destruct
/3 width=2 by ex_intro, conj/
qed-.
lemma preterm_in_root_inv_lcons_appl:
- βu,t,p,l. l;p Ο΅β΅ @u.t β
- β¨β¨ β§β§ π¦ = l & p Ο΅β΅ u
- | β§β§ π = l & p Ο΅β΅ t.
+ βu,t,p,l. l;p Ο΅ β΅@u.t β
+ β¨β¨ β§β§ π¦ = l & p Ο΅ β΅u
+ | β§β§ π = l & p Ο΅ β΅t.
#u #t #p #l * #q
<list_append_lcons_sn * * #r #Hr #H0 destruct
/4 width=2 by ex_intro, or_introl, or_intror, conj/
(* *)
(**************************************************************************)
+include "delayed_updating/syntax/path_dephi.ma".
include "delayed_updating/syntax/preterm_constructors.ma".
(* DEPHI FOR PRETERM ********************************************************)
-definition preterm_dephi (f) (t) β
- Ξ»p. ββq. q ϡ⬦ t & p = path_dephi f q.
+definition preterm_dephi (f) (t): preterm β
+ Ξ»p. ββq. q Ο΅ t & p = path_dephi f q.
--- /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 "ground/lib/subset_equivalence.ma".
+include "delayed_updating/syntax/preterm.ma".
+
+(* EQUIVALENCE FOR PRETERM **************************************************)
+
+(* Constructions with preterm_root ******************************************)
+
+lemma preterm_root_incl_repl:
+ βt1,t2. t1 β t2 β β΅t1 β β΅t2.
+#t1 #t2 #Ht #p * #q #Hq
+/3 width=2 by ex_intro/
+qed.
+
+lemma preterm_root_eq_repl:
+ βt1,t2. t1 β t2 β β΅t1 β β΅t2.
+#t1 #t2 * #H1 #H2
+/3 width=3 by conj, preterm_root_incl_repl/
+qed.
(* *)
(**************************************************************************)
-include "ground/notation/relations/white_harrow_2.ma".
+include "ground/notation/relations/arroweq_2.ma".
include "ground/lib/subset_inclusion.ma".
(* EQUIVALENCE FOR SUBSETS **************************************************)
interpretation
"equivalence (subset)"
- 'WhiteHArrow u1 u2 = (subset_eq ? u1 u2).
+ 'ArrowEq u1 u2 = (subset_eq ? u1 u2).
+
+(* Basic destructions *******************************************************)
+
+lemma subset_in_eq_repl_back (A) (a:A):
+ βu1. a Ο΅ u1 β βu2. u1 β u2 β a Ο΅ u2.
+#A #a #u1 #Hu1 #u2 *
+/2 width=1 by/
+qed-.
+
+lemma subset_in_eq_repl_fwd (A) (a:A):
+ βu1. a Ο΅ u1 β βu2. u2 β u1 β a Ο΅ u2.
+#A #a #u1 #Hu1 #u2 *
+/2 width=1 by/
+qed-.
(* Basic constructions ******************************************************)
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* GROUND NOTATION **********************************************************)
+
+notation "hvbox( a1 β break term 46 a2 )"
+ non associative with precedence 45
+ for @{ 'ArrowEq $a1 $a2 }.
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-(* GROUND NOTATION **********************************************************)
-
-notation "hvbox( a1 β break term 46 a2 )"
- non associative with precedence 45
- for @{ 'WhiteHArrow $a1 $a2 }.