From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 14 Jan 2008 17:02:46 +0000 (+0000)
Subject: more lemmas, til 3.26
X-Git-Tag: make_still_working~5667
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ea7c93bf4177982ff09d429a3a818e8b5f937ea1;p=helm.git

more lemmas, til 3.26
---

diff --git a/helm/software/matita/dama/TODO b/helm/software/matita/dama/TODO
new file mode 100644
index 000000000..6e2ccdd68
--- /dev/null
+++ b/helm/software/matita/dama/TODO
@@ -0,0 +1,2 @@
+changing file resets the display-notation ref, but not the GUI tick
+mettere una maction in tutti i body (ma forse non basta)
diff --git a/helm/software/matita/dama/infsup.ma b/helm/software/matita/dama/infsup.ma
index ef436f889..05b497cc5 100644
--- a/helm/software/matita/dama/infsup.ma
+++ b/helm/software/matita/dama/infsup.ma
@@ -32,4 +32,42 @@ elim (Sx Hxn) (_ Hx); elim (Sy Hxn) (_ Hy);
 apply (tends_uniq ?? xn ?? Hx Hy);
 qed.
 
-(* 3.21 *)
+definition shift : ∀R.∀ml:mlattice R.∀xn:sequence ml.nat → sequence ml ≝
+ λR.λml:mlattice R.λxn:sequence ml.λm:nat.λn.xn (n+m).
+ 
+definition ank ≝
+  λR.λml:mlattice R.λxn:sequence ml.λk:nat.
+    let rec ank_aux (i : nat) ≝
+      match i with 
+      [ O ⇒ (shift ?? xn k) O
+      | S n1 ⇒ (shift ?? xn k) (S n1) ∧ ank_aux n1]
+    in ank_aux.
+    
+definition bnk ≝
+  λR.λml:mlattice R.λxn:sequence ml.λk:nat.
+    let rec bnk_aux (i : nat) ≝
+      match i with 
+      [ O ⇒ (shift ?? xn k) O
+      | S n1 ⇒ (shift ?? xn k) (S n1) ∨ bnk_aux n1]
+    in bnk_aux.
+    
+lemma ank_decreasing: 
+  ∀R.∀ml:mlattice R.∀xn:sequence ml.∀m.decreasing ? (ank ?? xn m).
+intros (R ml xn m); unfold; intro n; simplify; apply lem;
+qed.
+
+(* 3.26 *)
+lemma ankS:
+  ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n:nat.
+    ((ank ?? xn k) (S n)) ≈ (xn k ∧ ank ?? xn (S k) n).
+intros (R ml xn k n); elim n; simplify; [apply meet_comm]  
+simplify in H; apply (Eq≈ ? (feq_ml ???? (H))); clear H;
+apply (Eq≈ ? (meet_assoc ????));    
+apply (Eq≈ ?? (eq_sym ??? (meet_assoc ????)));
+apply feq_mr; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
+simplify; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
+apply meet_comm;
+qed.    
+   
+   
+   
\ No newline at end of file
diff --git a/helm/software/matita/dama/lattice.ma b/helm/software/matita/dama/lattice.ma
index 787ee3e8e..66f14b942 100644
--- a/helm/software/matita/dama/lattice.ma
+++ b/helm/software/matita/dama/lattice.ma
@@ -62,6 +62,12 @@ intros (l a b c H); unfold eq in H ⊢ %; unfold Not in H ⊢ %;
 intro H1; apply H; clear H; apply (strong_extm ???? H1);
 qed.
 
+lemma feq_mr: ∀ml:lattice.∀a,b,c:ml. a ≈ b → (a ∧ c) ≈ (b ∧ c).
+intros (l a b c H); 
+apply (Eq≈ ? (meet_comm ???)); apply (Eq≈ ?? (meet_comm ???));
+apply feq_ml; assumption;
+qed.
+
 lemma feq_jl: ∀ml:lattice.∀a,b,c:ml. a ≈ b → (c ∨ a) ≈ (c ∨ b).
 intros (l a b c H); unfold eq in H ⊢ %; unfold Not in H ⊢ %;
 intro H1; apply H; clear H; apply (strong_extj ???? H1);
@@ -83,5 +89,11 @@ apply (Eq≈ (b∨(b∧a)) ? (feq_jl ???? (meet_comm ???)));
 apply eq_sym; apply absorbjm;
 qed.
 
-
+lemma lem: ∀ml:lattice.∀a,b:ml.(a ∧ b) ≤ b.
+intros; unfold le; unfold excess_of_lattice; unfold excl; simplify;
+intro H; apply (ap_coreflexive ? (a∧b));
+apply (Ap≫ (a∧(b∧b)) (feq_ml ???? (meet_refl ? b)));
+apply (Ap≫ ? (meet_assoc ????)); assumption;
+qed.
+