--- /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( @ break term 76 u. break term 75 t )"
+ non associative with precedence 75
+ for @{ 'At $u $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( hd , break tl )"
+ right associative with precedence 50
+ for @{ 'Comma $hd $tl }.
--- /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( # break term 90 n )"
+ non associative with precedence 75
+ for @{ 'Hash $n }.
--- /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( š . break term 75 t )"
+ non associative with precedence 75
+ for @{ 'Lamda $t }.
(* *)
(**************************************************************************)
-(* GROUND NOTATION **********************************************************)
+(* NOTATION FOR DELAYED UPDATING ********************************************)
notation "hvbox( š±āØ break term 46 a ā© )"
non associative with precedence 75
--- /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( š break term 76 n. break term 75 t )"
+ non associative with precedence 75
+ for @{ 'Phi $n $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( hd ; break tl )"
+ right associative with precedence 47
+ for @{ 'Semicolon $hd $tl }.
--- /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 }.
--- /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 @{ 'UpDownArrowEpsilon $p $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 "ground/xoa/or_5.ma".
+include "ground/xoa/ex_3_1.ma".
+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/term_constructors.ma".
+include "delayed_updating/notation/relations/in_predicate_d_phi_1.ma".
+
+(* BY-DEPTH DELAYED (BDD) TERM **********************************************)
+
+inductive bdd: predicate term ā
+| 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
+.
+
+interpretation
+ "well-formed by-depth delayed (term)"
+ 'InPredicateDPhi t = (bdd t).
+
+(* Basic destructions *******************************************************)
+
+lemma bdd_inv_in_com_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 *
+[ #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/
+]
+qed-.
+
+lemma bdd_inv_in_com_d:
+ ā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_com_gen ā¦ Ht Hq) -Ht -Hq *
+[ #n0 #H1 #H2 destruct /3 width=1 by or_introl, conj/
+| #u0 #q0 #n0 #Hu0 #Hq0 #H1 #H2 destruct /3 width=4 by ex3_intro, or_intror/
+| #u0 #q0 #_ #_ #_ #H0 destruct
+| #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
+| #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
+]
+qed-.
+
+lemma bdd_inv_in_ini_d:
+ ā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_com_d ā¦ Ht Hq) -Ht -Hq *
+[ #H1 #H2
+ elim (eq_inv_list_empty_append ā¦ H2) -H2 #H2 #_ destruct
+ /3 width=1 by or_introl, conj/
+| #u #Hu #Hq #H1 destruct
+ /4 width=4 by ex3_intro, ex_intro, or_intror/
+]
+qed-.
+
+lemma pippo:
+ ā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_ini_d ā¦ Ht Hn) -Ht -Hn *
+ [ #H1 #_ destruct
+ elim (term_in_ini_inv_lcons_oref ā¦ Hl) -Hl //
+ | #u #_ #_ #H1 destruct
+ elim (term_in_ini_inv_lcons_iref ā¦ Hl) -Hl //
+ ]
+| * [ #m ] #p #IH #t #Ht
+ <list_cons_shift <list_cons_shift #Hn #Hl
+ [ elim (bdd_inv_in_ini_d ā¦ Ht Hn) -Ht -Hn *
+ [ #_ #H
+ elim (eq_inv_list_empty_rcons ??? H)
+ | #u #Hu #Hp #H destruct
+ elim (term_in_ini_inv_lcons_iref ā¦ Hl) -Hl #_ #Hl
+ @(IH ā¦ Hu) //
+ ]
+ |
+ ]
+]
| label_edge_s: label
.
-coercion label_node_d.
-
interpretation
"variable reference by depth (label)"
'NodeLabelD p = (label_node_d p).
(* *)
(**************************************************************************)
-include "ground/lib/list.ma".
-include "delayed_updating/notation/functions/element_e_0.ma".
+include "ground/lib/list_rcons.ma".
+include "ground/notation/functions/element_e_0.ma".
+include "ground/notation/functions/double_semicolon_2.ma".
include "delayed_updating/syntax/label.ma".
+include "delayed_updating/notation/functions/semicolon_2.ma".
+include "delayed_updating/notation/functions/comma_2.ma".
+
(* PATH *********************************************************************)
interpretation
"empty (paths)"
- 'ElementE = (list_nil label).
+ 'ElementE = (list_empty label).
+
+interpretation
+ "left cons (paths)"
+ 'Semicolon l p = (list_lcons label l p).
+
+interpretation
+ "append (paths)"
+ 'DoubleSemicolon l1 l2 = (list_append label l1 l2).
+
+interpretation
+ "right cons (paths)"
+ 'Comma p l = (list_append label p (list_lcons label l (list_empty label))).
--- /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 "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".
+
+(* TERM *********************************************************************)
+
+definition term: Type[0] ā predicate path.
+
+definition term_in_com: relation2 path term ā
+ Ī»p,t. t p.
+
+interpretation
+ "belongs to complete (term)"
+ 'UpDownArrowEpsilon p t = (term_in_com p t).
+
+definition term_in_ini: relation2 path term ā
+ Ī»p,t. āq. p;;q Ļµā¬¦ t.
+
+interpretation
+ "belongs to initial (term)"
+ 'UpArrowEpsilon p t = (term_in_ini p t).
+
+(* Basic constructions ******************************************************)
+
+lemma term_in_com_ini (p) (t):
+ p Ļµā¬¦ t ā p Ļµāµ t.
+/2 width=2 by ex_intro/
+qed.
--- /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 "delayed_updating/syntax/term.ma".
+include "delayed_updating/notation/functions/hash_1.ma".
+include "delayed_updating/notation/functions/phi_2.ma".
+include "delayed_updating/notation/functions/lamda_1.ma".
+include "delayed_updating/notation/functions/at_2.ma".
+
+(* CONSTRUCTORS FOR TERM ****************************************************)
+
+definition term_node_0 (l): term ā
+ Ī»p. l;š = p.
+
+definition term_node_1 (l): term ā term ā
+ Ī»t,p. āāq. q Ļµā¬¦ t & l;q = p.
+
+definition term_node_2 (l1) (l2): term ā term ā term ā
+ Ī»t1,t2,p.
+ āØāØ āāq. q Ļµā¬¦ t1 & l1;q = p
+ | āāq. q Ļµā¬¦ t2 & l2;q = p.
+
+interpretation
+ "outer variable reference by depth (term)"
+ 'Hash n = (term_node_0 (label_node_d n)).
+
+interpretation
+ "inner variable reference by depth (term)"
+ 'Phi n t = (term_node_1 (label_node_d n) t).
+
+interpretation
+ "name-free functional abstraction (term)"
+ 'Lamda t = (term_node_1 label_edge_l t).
+
+interpretation
+ "application (term)"
+ 'At u t = (term_node_2 label_edge_s label_edge_a u t).
+
+(* Basic Inversions *********************************************************)
+
+lemma term_in_ini_inv_lcons_oref:
+ āp,l,n. l;p Ļµāµ #n ā
+ ā§ā§ š±āØnā© = l & š = p.
+#p #l #n * #q
+<list_append_lcons_sn #H destruct -H
+elim (eq_inv_list_empty_append ā¦ e0) -e0 #H1 #_
+/2 width=1 by conj/
+qed-.
+
+lemma term_in_ini_inv_lcons_iref:
+ āt,p,l,n. l;p Ļµāµ šn.t ā
+ ā§ā§ š±āØnā© = l & p Ļµāµ t.
+#t #p #l #n * #q
+<list_append_lcons_sn * #r #Hr #H1 destruct
+/3 width=2 by ex_intro, conj/
+qed-.
]
]
qed.
+
+(* Basic inversions *********************************************************)
+
+lemma eq_inv_list_empty_append (A):
+ āl1,l2. ā = l1āØ{A}l2 ā
+ ā§ā§ ā = l1 & ā = l2.
+#A *
+[ #l2 /2 width=1 by conj/
+| #a1 #l1 #l2 <list_append_lcons_sn #H destruct
+]
+qed-.
lemma list_append_rcons_dx (A):
āl1,l2,a. l1 āØ l2 āØ a = l1 āØ{A} (l2 āØ a).
// qed.
+
+(* Basic inversions *********************************************************)
+
+lemma eq_inv_list_empty_rcons (A):
+ āl,a. ā = lāØ{A}a ā ā„.
+#A #l #a #H
+elim (eq_inv_list_empty_append ā¦ H) -H #_ #H destruct
+qed-.
["="; "ā"; "ā”"; "ā"; "ā"; "ā"; "ā"; "ā"; "ā"; "ā"; "ā"; "ā§¦"; "ā"; "ā"; "ā©³"; "ā
"; "ā©¬"; "ā"; "ā"; "ā"; ];
["ā"; "ā„²"; "ā¦"; "ā"; "ā¤"; "ā¾"; "ā¤"; "ā¤"; "ā¤³"; ] ;
["ā"; "ā¤"; "ā¾"; "āØ"; "ā¬"; "ā”"; "ā¬"; "ā¤"; "āø"; "ā"; "ā„°"; ] ;
- ["^"; "ā"; "ā”"; ] ;
+ ["^"; "ā"; "ā”"; "ā„"; "āµ"; ] ;
["ā"; "ā§"; "ā¬"; ] ;
["ā"; "ā©"; "ā¬"; "ā¬"; "ā¬"; "ā·"; ] ;
["ā"; "ā³"; "ā¬"; "ā"; ];
["ā"; "ā"; "ā¬"; "ā¬"; ] ;
["ā¤"; "ā²"; "ā¼"; "ā°"; "ā“"; "ā "; "ā"; "ā«"; "ā"; ] ;
- ["_"; "ā"; "ā"; "ā£"; "ā"; "ā"; "ā½"; "ā¼"; "ā»"; "āŗ"; ];
+ ["_"; "ā"; "ā"; "ā£"; "ā"; "ā"; "ā½"; "ā¼"; "ā»"; "āŗ"; "āæ"; ];
["<"; "āŗ"; "ā®"; "ā"; "ā©"; "Ā«"; "ā¬"; "ā®"; "ā°"; ] ;
["("; "āØ"; "āŖ"; "ā²"; "ļ¼"; ];
[")"; "ā©"; "ā«"; "ā³"; "ļ¼"; ];
["{"; "ā“"; "ā¦" ] ;
["}"; "āµ"; "ā¦" ] ;
["ā”"; "ā½"; "āŖ"; "ā¾"; ];
- ["ā"; "ā¢"; "ā§«"; "ā¦"; "ā"; "ā "; ] ;
+ ["Ć¢\97\8a"; "Ć¢Ā¬Ā¦"; "Ć¢\99Ā¢"; "Ć¢Ā§Ā«"; "Ć¢\99Ā¦"; "Ć¢\9f\90"; "Ć¢\9fĀ "; ] ;
[">"; "ā"; "ā§"; "āŖ"; "Ā»"; "ā"; "āÆ"; "ā±"; "āø"; "āŗ"; "ā¶"; "ā"; "ā"; ] ;
["ā„"; "āŖ"; "ā½"; "āŖ“"; "ā„ø"; "ā"; ];
["āØ"; "ā©"; "āŖ"; "ā©"; "ā"; "ā" ] ;
["D"; "Ī"; "š»"; "ā
"; "š"; "š«"; "ā¹"; "š"; ] ;
["e"; "É"; "Īµ"; "Ļµ"; "Š"; "āÆ"; "š"; "ā
"; "š"; "š"; "š"; "ā"; ] ;
["E"; "ā°"; "š¼"; "š"; "āŗ"; ] ;
- ["f"; "Ļ"; "Ļ"; "Ļ"; "āØ"; "š"; "š"; "š"; "š"; "ā"; ] ;
+ ["f"; "Ć\86"; "Ć\88"; "Ć\95"; "Ć¢ĀØ\8d"; "Ć°\9d\95\97"; "Ć°\9d\90\9f"; "Ć°\9d\9b\97"; "Ć°\9d\9b\9f"; "Ć°\9d\9b\99"; "Ć¢\93\95"; ] ;
["F"; "Ī¦"; "ĪØ"; "ā±"; "š½"; "š
"; "š½"; "šæ"; "ā»"; "š"; ] ;
["g"; "Ī³"; "ā"; "š"; "š "; "š"; "ā"; ] ;
["G"; "Ī"; "š¾"; "š"; "šŖ"; "ā¼"; ] ;
projects / helm.git / commitdiff