(* NOTATION FOR DELAYED UPDATING ********************************************)
-notation "hvbox( @ break term 76 u . break term 75 t )"
- non associative with precedence 75
+notation "hvbox( @ break term 71 u . break term 70 t )"
+ non associative with precedence 70
for @{ 'At $u $t }.
(* NOTATION FOR DELAYED UPDATING ********************************************)
notation "hvbox( ๐๐ )"
- non associative with precedence 75
+ non associative with precedence 70
for @{ 'ClassDPhi }.
(* NOTATION FOR DELAYED UPDATING ********************************************)
notation "hvbox( ๐ )"
- non associative with precedence 75
+ non associative with precedence 70
for @{ 'EdgeLabelA }.
(* NOTATION FOR DELAYED UPDATING ********************************************)
notation "hvbox( ๐ )"
- non associative with precedence 75
+ non associative with precedence 70
for @{ 'EdgeLabelL }.
(* NOTATION FOR DELAYED UPDATING ********************************************)
notation "hvbox( ๐ฆ )"
- non associative with precedence 75
+ non associative with precedence 70
for @{ 'EdgeLabelS }.
(* NOTATION FOR DELAYED UPDATING ********************************************)
notation "hvbox( # break term 90 n )"
- non associative with precedence 75
+ non associative with precedence 70
for @{ 'Hash $n }.
(* NOTATION FOR DELAYED UPDATING ********************************************)
-notation "hvbox( ๐. break term 75 t )"
- non associative with precedence 75
+notation "hvbox( ๐. break term 70 t )"
+ non associative with precedence 70
for @{ 'Lamda $t }.
(* NOTATION FOR DELAYED UPDATING ********************************************)
notation "hvbox( ๐ฑโจ break term 46 a โฉ )"
- non associative with precedence 75
+ non associative with precedence 70
for @{ 'NodeLabelD $a }.
(* NOTATION FOR DELAYED UPDATING ********************************************)
-notation "hvbox( ๐ break term 76 n. break term 75 t )"
- non associative with precedence 75
+notation "hvbox( ๐ break term 76 n. break term 70 t )"
+ non associative with precedence 70
for @{ 'Phi $n $t }.
(* NOTATION FOR DELAYED UPDATING ********************************************)
-notation "hvbox( โ[ term 46 t1 ] break term 75 t2 )"
- non associative with precedence 75
+notation "hvbox( โ[ term 46 t1 ] break term 70 t2 )"
+ non associative with precedence 70
for @{ 'UpArrow $t1 $t2 }.
(* NOTATION FOR DELAYED UPDATING ********************************************)
notation < "hvbox( โโจ term 46 k, break term 46 p, break term 46 f โฉ )"
- non associative with precedence 75
+ non associative with precedence 70
for @{ 'UpArrow $S $k $p $f }.
notation > "hvbox( โโจ term 46 k, break term 46 p, break term 46 f โฉ )"
- non associative with precedence 75
+ non associative with precedence 70
for @{ 'UpArrow ? $k $p $f }.
notation > "hvbox( โ{ term 46 S }โจ break term 46 k, break term 46 p, break term 46 f โฉ )"
- non associative with precedence 75
+ non associative with precedence 70
for @{ 'UpArrow $S $k $p $f }.
(* NOTATION FOR DELAYED UPDATING ********************************************)
-notation "hvbox( โต term 75 t )"
- non associative with precedence 75
+notation "hvbox( โต term 70 t )"
+ non associative with precedence 70
for @{ 'UpTriangle $t }.
(* *)
(**************************************************************************)
+include "delayed_updating/syntax/path_depth.ma".
include "delayed_updating/syntax/path_structure.ma".
include "delayed_updating/syntax/path_balanced.ma".
include "delayed_updating/substitution/fsubst.ma".
(* DELAYED FOCUSED REDUCTION ************************************************)
inductive dfr (p) (q) (t): predicate preterm โ
-| dfr_beta (b) (n):
- let r โ pโ๐โbโ๐โqโ๐ฑโจnโฉ in
+| dfr_beta (b):
+ let r โ pโ๐โbโ๐โqโ๐ฑโจโโqโโฉ in
r ฯต t โ โโb โ dfr p q t (t[โrโtโ(pโ๐ฆ)])
.
lemma dfr_lift_bi (f) (p) (q) (t1) (t2):
t1 โก๐๐[p,q] t2 โ โ[f]t1 โก๐[โp,โq] โ[f]t2.
#f #p #q #t1 #t2
-* #b #n #Hr #Hb
+* #b #Hr #Hb
(* *)
(**************************************************************************)
+include "delayed_updating/syntax/path_depth.ma".
include "delayed_updating/syntax/path_structure.ma".
include "delayed_updating/syntax/path_balanced.ma".
include "delayed_updating/substitution/fsubst.ma".
(* IMMEDIATE FOCUSED REDUCTION ************************************************)
inductive ifr (p) (q) (t): predicate preterm โ
-| ifr_beta (b) (n):
+| ifr_beta (b):
let r โ pโ๐โbโ๐โq in
- rโ๐ฑโจnโฉ ฯต t โ โโb โ ifr p q t (t[โrโโ[๐ฎโจnโฉ]tโ(pโ๐ฆ)])
+ rโ๐ฑโจโโqโโฉ ฯต t โ โโb โ ifr p q t (t[โrโโ[๐ฎโจโโqโโฉ]tโ(pโ๐ฆ)])
.
interpretation
(* Note: inner numeric labels are not liftable, so they are removed *)
rec definition lift_gen (A:Type[0]) (k:lift_continuation A) (p) (f) on p โ
match p with
-[ list_empty โ k ๐ f
+[ list_empty โ k (๐) f
| list_lcons l q โ
match l with
[ label_node_d n โ
(* Basic constructions ******************************************************)
lemma lift_empty (A) (k) (f):
- k ๐ f = โ{A}โจk, ๐, fโฉ.
+ k (๐) f = โ{A}โจk, ๐, fโฉ.
// qed.
lemma lift_d_empty_sn (A) (k) (n) (f):
(* Advanced eliminations with path ******************************************)
lemma path_ind_lift (Q:predicate โฆ):
- Q ๐ โ
- (โn. Q ๐ โ Q (๐ฑโจnโฉโ๐)) โ
+ Q (๐) โ
+ (โn. Q (๐) โ Q (๐ฑโจnโฉโ๐)) โ
(โn,l,p. Q (lโp) โ Q (๐ฑโจnโฉโlโp)) โ
(โp. Q p โ Q (๐โp)) โ
(โp. Q p โ Q (๐โp)) โ
(* BY-DEPTH DELAYED (BDD) TERM **********************************************)
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_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
.
(* This condition applies to a structural path *)
inductive pbc: predicate path โ
-| pbc_empty: pbc ๐
+| pbc_empty: pbc (๐)
| pbc_redex: โb. pbc b โ pbc (๐โbโ๐)
| pbc_after: โb1,b2. pbc b1 โ pbc b2 โ pbc (b1โb2)
.
--- /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 "ground/arith/nat_succ.ma".
+include "ground/notation/functions/verticalbars_1.ma".
+
+(* DEPTH FOR PATH ***********************************************************)
+
+rec definition depth (p) on p: nat โ
+match p with
+[ list_empty โ ๐
+| list_lcons l q โ
+ match l with
+ [ label_node_d _ โ depth q
+ | label_edge_L โ โ(depth q)
+ | label_edge_A โ depth q
+ | label_edge_S โ depth q
+ ]
+].
+
+interpretation
+ "depth (path)"
+ 'VerticalBars p = (depth p).
+
+(* Basic constructions ******************************************************)
+
+lemma depth_empty: ๐ = โ๐โ.
+// qed.
+
+lemma depth_d (q) (n): โqโ = โ๐ฑโจnโฉโqโ.
+// qed.
+
+lemma depth_L (q): โโqโ = โ๐โqโ.
+// qed.
+
+lemma depth_A (q): โqโ = โ๐โqโ.
+// qed.
+
+lemma depth_S (q): โqโ = โ๐ฆโqโ.
+// qed.
(* *)
(**************************************************************************)
+include "ground/notation/functions/verticalbars_1.ma".
include "ground/lib/list.ma".
include "ground/arith/nat_succ.ma".
interpretation
"length (lists)"
- 'card l = (list_length ? l).
+ 'VerticalBars l = (list_length ? l).
(* Basic constructions ******************************************************)
-lemma list_length_empty (A:Type[0]): |list_empty A| = ๐.
+lemma list_length_empty (A:Type[0]):
+ โlist_empty Aโ = ๐.
// qed.
-lemma list_length_lcons (A:Type[0]) (l:list A) (a:A): |aโจฎl| = โ|l|.
+lemma list_length_lcons (A:Type[0]) (l:list A) (a:A):
+ โaโจฎlโ = โโlโ.
// qed.
(* Basic inversions *********************************************************)
lemma list_length_inv_zero_dx (A:Type[0]) (l:list A):
- |l| = ๐ โ l = โ.
+ โlโ = ๐ โ l = โ.
#A * // #a #l >list_length_lcons #H
elim (eq_inv_nsucc_zero โฆ H)
qed-.
lemma list_length_inv_zero_sn (A:Type[0]) (l:list A):
- (๐) = |l| โ l = โ.
+ (๐) = โlโ โ l = โ.
/2 width=1 by list_length_inv_zero_dx/ qed-.
lemma list_length_inv_succ_dx (A:Type[0]) (l:list A) (x):
- |l| = โx โ
- โโtl,a. x = |tl| & l = a โจฎ tl.
+ โlโ = โx โ
+ โโtl,a. x = โtlโ & l = a โจฎ tl.
#A *
[ #x >list_length_empty #H
elim (eq_inv_zero_nsucc โฆ H)
qed-.
lemma list_length_inv_succ_sn (A:Type[0]) (l:list A) (x):
- โx = |l| โ
- โโtl,a. x = |tl| & l = a โจฎ tl.
+ โx = โlโ โ
+ โโtl,a. x = โtlโ & l = a โจฎ tl.
/2 width=1 by list_length_inv_succ_dx/ qed-.
(* EQUIVALENCE FOR SUBSETS **************************************************)
-definition subset_eq (A): relation2 ๐ซโจAโฉ ๐ซโจAโฉ โ
+definition subset_eq (A): relation2 (๐ซโจAโฉ) (๐ซโจAโฉ) โ
ฮปu1,u2. โงโง u1 โ u2 & u2 โ u1.
interpretation
(* INCLUSION FOR SUBSETS ****************************************************)
-definition subset_le (A): relation2 ๐ซโจAโฉ ๐ซโจAโฉ โ
+definition subset_le (A): relation2 (๐ซโจAโฉ) (๐ซโจAโฉ) โ
ฮปu1,u2. โp. p ฯต u1 โ p ฯต u2.
interpretation
(* GROUND NOTATION **********************************************************)
notation < "hvbox( โ )"
- non associative with precedence 75
+ non associative with precedence 70
for @{ 'CircledElementE $S }.
notation > "hvbox( โ )"
- non associative with precedence 75
+ non associative with precedence 70
for @{ 'CircledElementE ? }.
notation > "hvbox( โ{ term 46 S } )"
- non associative with precedence 75
+ non associative with precedence 70
for @{ 'CircledElementE $S }.
(* GROUND NOTATION **********************************************************)
-notation "hvbox( โ term 75 T )"
- non associative with precedence 75
+notation "hvbox( โ term 70 T )"
+ non associative with precedence 70
for @{ 'DownArrow $T }.
(* GROUND NOTATION **********************************************************)
-notation < "hvbox( โ term 75 a )"
- non associative with precedence 75
+notation < "hvbox( โ term 70 a )"
+ non associative with precedence 70
for @{ 'DownHarpoonLeft $S $a }.
-notation > "hvbox( โ term 75 a )"
- non associative with precedence 75
+notation > "hvbox( โ term 70 a )"
+ non associative with precedence 70
for @{ 'DownHarpoonLeft ? $a }.
-notation > "hvbox( โ{ term 46 S } break term 75 a )"
- non associative with precedence 75
+notation > "hvbox( โ{ term 46 S } break term 70 a )"
+ non associative with precedence 70
for @{ 'DownHarpoonLeft $S $a }.
(* GROUND NOTATION **********************************************************)
-notation < "hvbox( โ term 75 a )"
- non associative with precedence 75
+notation < "hvbox( โ term 70 a )"
+ non associative with precedence 70
for @{ 'DownHarpoonRight $S $a }.
-notation > "hvbox( โ term 75 a )"
- non associative with precedence 75
+notation > "hvbox( โ term 70 a )"
+ non associative with precedence 70
for @{ 'DownHarpoonRight ? $a }.
-notation > "hvbox( โ{ term 46 S } break term 75 a )"
- non associative with precedence 75
+notation > "hvbox( โ{ term 46 S } break term 70 a )"
+ non associative with precedence 70
for @{ 'DownHarpoonRight $S $a }.
(* GROUND NOTATION **********************************************************)
-notation < "hvbox( โ*[ break term 46 n ] break term 75 a )"
- non associative with precedence 75
+notation < "hvbox( โ*[ break term 46 n ] break term 70 a )"
+ non associative with precedence 70
for @{ 'DownHarpoonRightStar $S $n $a }.
-notation > "hvbox( โ*[ break term 46 n ] break term 75 a )"
- non associative with precedence 75
+notation > "hvbox( โ*[ break term 46 n ] break term 70 a )"
+ non associative with precedence 70
for @{ 'DownHarpoonRightStar ? $n $a }.
-notation > "hvbox( โ*{ term 46 S }[ break term 46 n ] break term 75 a )"
- non associative with precedence 75
+notation > "hvbox( โ*{ term 46 S }[ break term 46 n ] break term 70 a )"
+ non associative with precedence 70
for @{ 'DownHarpoonRightStar $S $n $a }.
(* GROUND NOTATION **********************************************************)
-notation "hvbox( โซฐ term 75 T )"
- non associative with precedence 75
+notation "hvbox( โซฐ term 70 T )"
+ non associative with precedence 70
for @{ 'DownSpoon $T }.
(* GROUND NOTATION **********************************************************)
-notation "hvbox( โซฐ *[ term 46 n ] break term 75 T )"
- non associative with precedence 75
+notation "hvbox( โซฐ *[ term 46 n ] break term 70 T )"
+ non associative with precedence 70
for @{ 'DownSpoonStar $n $T }.
(* GROUND NOTATION **********************************************************)
notation "hvbox( ๐โจ term 46 d, break term 46 h โฉ )"
- non associative with precedence 75
+ non associative with precedence 70
for @{ 'ElementB $d $h }.
(* GROUND NOTATION **********************************************************)
notation "๐"
- non associative with precedence 75
+ non associative with precedence 70
for @{ 'ElementE }.
(* GROUND NOTATION **********************************************************)
notation "hvbox( ๐ข )"
- non associative with precedence 75
+ non associative with precedence 70
for @{ 'ElementI }.
(* GROUND NOTATION **********************************************************)
notation "hvbox( ๐ญโจ break term 46 a โฉ )"
- non associative with precedence 75
+ non associative with precedence 70
for @{ 'ElementT $a }.
(* GROUND NOTATION **********************************************************)
notation "hvbox( ๐ฎ โจ break term 46 a โฉ )"
- non associative with precedence 75
+ non associative with precedence 70
for @{ 'ElementU $a }.
(* GROUND NOTATION **********************************************************)
notation "โ"
- non associative with precedence 75
+ non associative with precedence 70
for @{ 'Infinity }.
(* GROUND NOTATION **********************************************************)
notation "โป"
- non associative with precedence 75
+ non associative with precedence 70
for @{'no}.
(* GROUND NOTATION **********************************************************)
notation "๐"
- non associative with precedence 75
+ non associative with precedence 70
for @{ 'One }.
(* GROUND NOTATION **********************************************************)
notation "๐๐"
- non associative with precedence 75
+ non associative with precedence 70
for @{ 'OneZero }.
(* GROUND NOTATION **********************************************************)
notation "hvbox( ๐ซ โจ break term 46 S โฉ )"
- non associative with precedence 75
+ non associative with precedence 70
for @{ 'PowerClass $S }.
(* GROUND NOTATION **********************************************************)
notation "hvbox ( โฉ term 46 x1, break term 46 x2 , break term 46 x3, break term 46 x4 โช )"
- non associative with precedence 75
+ non associative with precedence 70
for @{ 'Tuple $x1 $x2 $x3 $x4 }.
(* GROUND NOTATION **********************************************************)
notation "๐"
- non associative with precedence 75
+ non associative with precedence 70
for @{ 'Two }.
(* GROUND NOTATION **********************************************************)
-notation "hvbox( โ term 75 T )"
- non associative with precedence 75
+notation "hvbox( โ term 70 T )"
+ non associative with precedence 70
for @{ 'UpArrow $T }.
(* GROUND NOTATION **********************************************************)
-notation "hvbox( โ*[ term 46 n ] break term 75 T )"
- non associative with precedence 75
+notation "hvbox( โ*[ term 46 n ] break term 70 T )"
+ non associative with precedence 70
for @{ 'UpArrowStar $n $T }.
(* GROUND NOTATION **********************************************************)
-notation "hvbox( โ* term 75 T )"
- non associative with precedence 75
+notation "hvbox( โ* term 70 T )"
+ non associative with precedence 70
for @{ 'UpDownArrowStar $T }.
(* GROUND NOTATION **********************************************************)
-notation "hvbox( โซฏ term 75 T )"
- non associative with precedence 75
+notation "hvbox( โซฏ term 70 T )"
+ non associative with precedence 70
for @{ 'UpSpoon $T }.
(* GROUND NOTATION **********************************************************)
-notation "hvbox( โซฏ*[ term 46 n ] break term 75 T )"
- non associative with precedence 75
+notation "hvbox( โซฏ*[ term 46 n ] break term 70 T )"
+ non associative with precedence 70
for @{ 'UpSpoonStar $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 *)
+(* *)
+(**************************************************************************)
+
+(* GROUND NOTATION **********************************************************)
+
+notation "hvbox( โ term 46 C โ )"
+ non associative with precedence 70
+ for @{ 'VerticalBars $C }.
(* GROUND NOTATION **********************************************************)
notation "โ"
- non associative with precedence 75
+ non associative with precedence 70
for @{'yes}.
(* GROUND NOTATION **********************************************************)
notation "๐"
- non associative with precedence 75
+ non associative with precedence 70
for @{ 'Zero }.
(* GROUND NOTATION **********************************************************)
notation "๐๐"
- non associative with precedence 75
+ non associative with precedence 70
for @{ 'ZeroOne }.
(* GROUND NOTATION **********************************************************)
notation "๐๐"
- non associative with precedence 75
+ non associative with precedence 70
for @{ 'ZeroZero }.
(*** at_div_id_dx *)
theorem pr_pat_div_id_dx (f):
- H_pr_pat_div f ๐ข ๐ข f.
+ H_pr_pat_div f (๐ข ) (๐ข) f.
#f #jf #j0 #j #Hf #H0
lapply (pr_pat_id_des โฆ H0) -H0 #H destruct
/2 width=3 by ex2_intro/
(*** at_div_id_sn *)
theorem pr_pat_div_id_sn (f):
- H_pr_pat_div ๐ข f f ๐ข.
+ H_pr_pat_div (๐ข) f f (๐ข).
/3 width=6 by pr_pat_div_id_dx, pr_pat_div_comm/ qed-.
let predefined_classes = [
["&"; "โ
"; ];
- ["|"; "โฅ"; ];
+ ["|"; "รข\9d\98"; "รข\88ยฅ"; ];
["!"; "ยก"; "โซฏ"; "โซฐ"; "โ"; "โซฑ"; ];
["?"; "ยฟ"; "โธฎ"; ];
[":"; "โ"; ];
projects / helm.git / commitdiff