X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcontribs%2FPOPLmark%2FFsub%2Futil.ma;fp=matita%2Fcontribs%2FPOPLmark%2FFsub%2Futil.ma;h=bd7018d3c4488bc03aa3cfbeac5e459b09650035;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1

diff --git a/matita/contribs/POPLmark/Fsub/util.ma b/matita/contribs/POPLmark/Fsub/util.ma
new file mode 100644
index 000000000..bd7018d3c
--- /dev/null
+++ b/matita/contribs/POPLmark/Fsub/util.ma
@@ -0,0 +1,58 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/Fsub/util".
+include "logic/equality.ma".
+include "nat/compare.ma".
+include "list/list.ma".
+include "list/in.ma".
+
+(*** useful definitions and lemmas not really related to Fsub ***)
+
+definition max \def 
+\lambda m,n.
+  match (leb m n) with
+     [true \Rightarrow n
+     |false \Rightarrow m]. 
+     
+lemma le_n_max_m_n: \forall m,n:nat. n \le max m n.
+intros.
+unfold max.
+apply (leb_elim m n)
+  [simplify.intros.apply le_n
+  |simplify.intros.autobatch
+  ]
+qed.
+  
+lemma le_m_max_m_n: \forall m,n:nat. m \le max m n.
+intros.
+unfold max.
+apply (leb_elim m n)
+  [simplify.intro.assumption
+  |simplify.intros.autobatch
+  ]
+qed.  
+
+notation > "hvbox(x ∈ l)"
+  non associative with precedence 30 for @{ 'inlist $x $l }.
+notation < "hvbox(x \nbsp ∈ \nbsp l)"
+  non associative with precedence 30 for @{ 'inlist $x $l }.
+interpretation "item in list" 'inlist x l =
+  (cic:/matita/list/in/in_list.ind#xpointer(1/1) _ x l).
+
+lemma max_case : \forall m,n.(max m n) = match (leb m n) with
+      [ true \Rightarrow n
+      | false \Rightarrow m ].
+intros;elim m;simplify;reflexivity;
+qed.
\ No newline at end of file