From d3c72253769956a8af10e6ea990ed34c92999e58 Mon Sep 17 00:00:00 2001 From: Cosimo Oliboni Date: Tue, 4 Aug 2009 12:30:22 +0000 Subject: [PATCH] freescale porting, work in progress --- .../contribs/ng_assembly/common/option.ma | 43 + .../ng_assembly/common/option_lemmas.ma | 134 ++ .../contribs/ng_assembly/common/prod.ma | 109 ++ .../ng_assembly/common/prod_lemmas.ma | 499 ++++++ .../contribs/ng_assembly/common/theory.ma | 230 +++ .../matita/contribs/ng_assembly/depends | 76 +- .../matita/contribs/ng_assembly/num/bool.ma | 78 + .../contribs/ng_assembly/num/bool_lemmas.ma | 193 +++ .../contribs/ng_assembly/num/exadecim.ma | 1419 +++++++++++++++++ .../ng_assembly/num/exadecim_lemmas.ma | 483 ++++++ .../matita/contribs/ng_assembly/num/oct.ma | 78 + .../contribs/ng_assembly/num/oct_lemmas.ma | 143 ++ .../contribs/ng_assembly/num/quatern.ma | 66 + .../ng_assembly/num/quatern_lemmas.ma | 115 ++ .../contribs/ng_assembly/test_errori.ma | 9 +- 15 files changed, 3607 insertions(+), 68 deletions(-) create mode 100644 helm/software/matita/contribs/ng_assembly/common/option.ma create mode 100644 helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma create mode 100644 helm/software/matita/contribs/ng_assembly/common/prod.ma create mode 100644 helm/software/matita/contribs/ng_assembly/common/prod_lemmas.ma create mode 100644 helm/software/matita/contribs/ng_assembly/common/theory.ma create mode 100755 helm/software/matita/contribs/ng_assembly/num/bool.ma create mode 100755 helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma create mode 100755 helm/software/matita/contribs/ng_assembly/num/exadecim.ma create mode 100755 helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma create mode 100755 helm/software/matita/contribs/ng_assembly/num/oct.ma create mode 100755 helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma create mode 100755 helm/software/matita/contribs/ng_assembly/num/quatern.ma create mode 100755 helm/software/matita/contribs/ng_assembly/num/quatern_lemmas.ma diff --git a/helm/software/matita/contribs/ng_assembly/common/option.ma b/helm/software/matita/contribs/ng_assembly/common/option.ma new file mode 100644 index 000000000..cbd1c4907 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/common/option.ma @@ -0,0 +1,43 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* ********************************************************************** *) + +include "num/bool.ma". + +(* ****** *) +(* OPTION *) +(* ****** *) + +ninductive option (A:Type) : Type ≝ + None : option A +| Some : A → option A. + +ndefinition eq_option ≝ +λT.λop1,op2:option T.λf:T → T → bool. + match op1 with + [ None ⇒ match op2 with [ None ⇒ true | Some _ ⇒ false ] + | Some x1 ⇒ match op2 with [ None ⇒ false | Some x2 ⇒ f x1 x2 ] + ]. + +(* option map = match ... with [ None ⇒ None ? | Some .. ⇒ .. ] *) +ndefinition opt_map ≝ +λT1,T2:Type.λt:option T1.λf:T1 → option T2. + match t with [ None ⇒ None ? | Some x ⇒ (f x) ]. diff --git a/helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma new file mode 100644 index 000000000..c157bfa11 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma @@ -0,0 +1,134 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* ********************************************************************** *) + +include "common/option.ma". +include "num/bool_lemmas.ma". + +(* ****** *) +(* OPTION *) +(* ****** *) + +nlemma option_destruct_some_some : ∀T.∀x1,x2:T.Some T x1 = Some T x2 → x1 = x2. + #T; #x1; #x2; #H; + nchange with (match Some T x2 with [ None ⇒ False | Some a ⇒ x1 = a ]); + nrewrite < H; + nnormalize; + napply refl_eq. +nqed. + +nlemma option_destruct_some_none : ∀T.∀x:T.Some T x = None T → False. + #T; #x; #H; + nchange with (match Some T x with [ None ⇒ True | Some a ⇒ False ]); + nrewrite > H; + nnormalize; + napply I. +nqed. + +nlemma option_destruct_none_some : ∀T.∀x:T.None T = Some T x → False. + #T; #x; #H; + nchange with (match Some T x with [ None ⇒ True | Some a ⇒ False ]); + nrewrite < H; + nnormalize; + napply I. +nqed. + +nlemma symmetric_eqoption : +∀T:Type.∀op1,op2:option T.∀f:T → T → bool. + (symmetricT T bool f) → + (eq_option T op1 op2 f = eq_option T op2 op1 f). + #T; #op1; #op2; #f; #H; + nelim op1; + nelim op2; + nnormalize; + ##[ ##1: napply refl_eq + ##| ##2,3: #H; napply refl_eq + ##| ##4: #a; #a0; + nrewrite > (H a0 a); + napply refl_eq + ##] +nqed. + +nlemma eq_to_eqoption : +∀T.∀op1,op2:option T.∀f:T → T → bool. + (∀x1,x2:T.x1 = x2 → f x1 x2 = true) → + (op1 = op2 → eq_option T op1 op2 f = true). + #T; #op1; #op2; #f; #H; + nelim op1; + nelim op2; + nnormalize; + ##[ ##1: #H1; napply refl_eq + ##| ##2: #a; #H1; nelim (option_destruct_none_some ?? H1) + ##| ##3: #a; #H1; nelim (option_destruct_some_none ?? H1) + ##| ##4: #a; #a0; #H1; + nrewrite > (H … (option_destruct_some_some … H1)); + napply refl_eq + ##] +nqed. + +nlemma eqoption_to_eq : +∀T.∀op1,op2:option T.∀f:T → T → bool. + (∀x1,x2:T.f x1 x2 = true → x1 = x2) → + (eq_option T op1 op2 f = true → op1 = op2). + #T; #op1; #op2; #f; #H; + nelim op1; + nelim op2; + nnormalize; + ##[ ##1: #H1; napply refl_eq + ##| ##2,3: #a; #H1; napply (bool_destruct … H1) + ##| ##4: #a; #a0; #H1; + nrewrite > (H … H1); + napply refl_eq + ##] +nqed. + +nlemma neq_to_neqoption : +∀T.∀op1,op2:option T.∀f:T → T → bool. + (∀x1,x2:T.x1 ≠ x2 → f x1 x2 = false) → + (op1 ≠ op2 → eq_option T op1 op2 f = false). + #T; #op1; #op2; #f; #H; + nelim op1; + nelim op2; + nnormalize; + ##[ ##1: #H1; napply False_ind; napply (H1 (refl_eq …)) + ##| ##2,3: #a; #H1; napply refl_eq + ##| ##4: #a; #a0; #H1; + napply H; + napply (neqf_to_neq … a0 a (λx.Some ? x) H1) + ##] +nqed. + +nlemma neqoption_to_neq : +∀T.∀op1,op2:option T.∀f:T → T → bool. + (∀x1,x2:T.f x1 x2 = false → x1 ≠ x2) → + (eq_option T op1 op2 f = false → op1 ≠ op2). + #T; #op1; #op2; #f; #H; + nelim op1; + nelim op2; + nnormalize; + ##[ ##1: #H1; napply (bool_destruct … H1) + ##| ##2: #a; #H1; #H2; napply (option_destruct_none_some ? a H2) + ##| ##3: #a; #H1; #H2; napply (option_destruct_some_none ? a H2) + ##| ##4: #a; #a0; #H1; #H2; + napply (H a0 a H1); + napply (option_destruct_some_some ? a0 a H2) + ##] +nqed. diff --git a/helm/software/matita/contribs/ng_assembly/common/prod.ma b/helm/software/matita/contribs/ng_assembly/common/prod.ma new file mode 100644 index 000000000..39f79e96e --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/common/prod.ma @@ -0,0 +1,109 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* ********************************************************************** *) + +include "num/bool.ma". + +(* ***** *) +(* TUPLE *) +(* ***** *) + +ninductive ProdT (T1:Type) (T2:Type) : Type ≝ + pair : T1 → T2 → ProdT T1 T2. + +ndefinition fst ≝ +λT1,T2:Type.λp:ProdT T1 T2.match p with [ pair x _ ⇒ x ]. + +ndefinition snd ≝ +λT1,T2:Type.λp:ProdT T1 T2.match p with [ pair _ x ⇒ x ]. + +ndefinition eq_pair ≝ +λT1,T2:Type.λp1,p2:ProdT T1 T2. +λf1:T1 → T1 → bool.λf2:T2 → T2 → bool. + match p1 with [ pair x1 y1 ⇒ + match p2 with [ pair x2 y2 ⇒ + (f1 x1 x2) ⊗ (f2 y1 y2) ]]. + +ninductive Prod3T (T1:Type) (T2:Type) (T3:Type) : Type ≝ +triple : T1 → T2 → T3 → Prod3T T1 T2 T3. + +ndefinition fst3T ≝ +λT1.λT2.λT3.λp:Prod3T T1 T2 T3.match p with [ triple x _ _ ⇒ x ]. + +ndefinition snd3T ≝ +λT1.λT2.λT3.λp:Prod3T T1 T2 T3.match p with [ triple _ x _ ⇒ x ]. + +ndefinition thd3T ≝ +λT1.λT2.λT3.λp:Prod3T T1 T2 T3.match p with [ triple _ _ x ⇒ x ]. + +ndefinition eq_triple ≝ +λT1,T2,T3:Type.λp1,p2:Prod3T T1 T2 T3. +λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.λf3:T3 → T3 → bool. + match p1 with [ triple x1 y1 z1 ⇒ + match p2 with [ triple x2 y2 z2 ⇒ + (f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ]]. + +ninductive Prod4T (T1:Type) (T2:Type) (T3:Type) (T4:Type) : Type ≝ +quadruple : T1 → T2 → T3 → T4 → Prod4T T1 T2 T3 T4. + +ndefinition fst4T ≝ +λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple x _ _ _ ⇒ x ]. + +ndefinition snd4T ≝ +λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple _ x _ _ ⇒ x ]. + +ndefinition thd4T ≝ +λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple _ _ x _ ⇒ x ]. + +ndefinition fth4T ≝ +λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple _ _ _ x ⇒ x ]. + +ndefinition eq_quadruple ≝ +λT1,T2,T3,T4:Type.λp1,p2:Prod4T T1 T2 T3 T4. +λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.λf3:T3 → T3 → bool.λf4:T4 → T4 → bool. + match p1 with [ quadruple x1 y1 z1 w1 ⇒ + match p2 with [ quadruple x2 y2 z2 w2 ⇒ + (f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 w1 w2) ]]. + +ninductive Prod5T (T1:Type) (T2:Type) (T3:Type) (T4:Type) (T5:Type) : Type ≝ +quintuple : T1 → T2 → T3 → T4 → T5 → Prod5T T1 T2 T3 T4 T5. + +ndefinition fst5T ≝ +λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple x _ _ _ _ ⇒ x ]. + +ndefinition snd5T ≝ +λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ x _ _ _ ⇒ x ]. + +ndefinition thd5T ≝ +λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ _ x _ _ ⇒ x ]. + +ndefinition frth5T ≝ +λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ _ _ x _ ⇒ x ]. + +ndefinition ffth5T ≝ +λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ _ _ _ x ⇒ x ]. + +ndefinition eq_quintuple ≝ +λT1,T2,T3,T4,T5:Type.λp1,p2:Prod5T T1 T2 T3 T4 T5. +λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.λf3:T3 → T3 → bool.λf4:T4 → T4 → bool.λf5:T5 → T5 → bool. + match p1 with [ quintuple x1 y1 z1 w1 v1 ⇒ + match p2 with [ quintuple x2 y2 z2 w2 v2 ⇒ + (f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 w1 w2) ⊗ (f5 v1 v2) ]]. diff --git a/helm/software/matita/contribs/ng_assembly/common/prod_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/prod_lemmas.ma new file mode 100644 index 000000000..9083f2b4d --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/common/prod_lemmas.ma @@ -0,0 +1,499 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* ********************************************************************** *) + +include "common/prod.ma". +include "num/bool_lemmas.ma". + +(* ***** *) +(* TUPLE *) +(* ***** *) + +nlemma pair_destruct_1 : +∀T1,T2.∀x1,x2:T1.∀y1,y2:T2. + pair T1 T2 x1 y1 = pair T1 T2 x2 y2 → x1 = x2. + #T1; #T2; #x1; #x2; #y1; #y2; #H; + nchange with (match pair T1 T2 x2 y2 with [ pair a _ ⇒ x1 = a ]); + nrewrite < H; + nnormalize; + napply refl_eq. +nqed. + +nlemma pair_destruct_2 : +∀T1,T2.∀x1,x2:T1.∀y1,y2:T2. + pair T1 T2 x1 y1 = pair T1 T2 x2 y2 → y1 = y2. + #T1; #T2; #x1; #x2; #y1; #y2; #H; + nchange with (match pair T1 T2 x2 y2 with [ pair _ b ⇒ y1 = b ]); + nrewrite < H; + nnormalize; + napply refl_eq. +nqed. + +nlemma symmetric_eqpair : +∀T1,T2:Type.∀p1,p2:ProdT T1 T2. +∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool. + (symmetricT T1 bool f1) → + (symmetricT T2 bool f2) → + (eq_pair T1 T2 p1 p2 f1 f2 = eq_pair T1 T2 p2 p1 f1 f2). + #T1; #T2; #p1; #p2; #f1; #f2; #H; #H1; + nelim p1; + #x1; #y1; + nelim p2; + #x2; #y2; + nnormalize; + nrewrite > (H x1 x2); + ncases (f1 x2 x1); + nnormalize; + ##[ ##1: nrewrite > (H1 y1 y2); napply refl_eq + ##| ##2: napply refl_eq + ##] +nqed. + +nlemma eq_to_eqpair : +∀T1,T2.∀p1,p2:ProdT T1 T2. +∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool. + (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) → + (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) → + (p1 = p2 → eq_pair T1 T2 p1 p2 f1 f2 = true). + #T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2; + nelim p1; + #x1; #y1; + nelim p2; + #x2; #y2; #H; + nnormalize; + nrewrite > (H1 … (pair_destruct_1 … H)); + nnormalize; + nrewrite > (H2 … (pair_destruct_2 … H)); + napply refl_eq. +nqed. + +nlemma eqpair_to_eq : +∀T1,T2.∀p1,p2:ProdT T1 T2. +∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool. + (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) → + (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) → + (eq_pair T1 T2 p1 p2 f1 f2 = true → p1 = p2). + #T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2; + nelim p1; + #x1; #y1; + nelim p2; + #x2; #y2; #H; + nnormalize in H:(%); + nletin K ≝ (H1 x1 x2); + ncases (f1 x1 x2) in H:(%) K:(%); + nnormalize; + #H3; + ##[ ##2: napply (bool_destruct … H3) ##] + #H4; + nrewrite > (H4 (refl_eq …)); + nrewrite > (H2 y1 y2 H3); + napply refl_eq. +nqed. + +nlemma triple_destruct_1 : +∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3. + triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → x1 = x2. + #T1; #T2; #T3; #x1; #x2; #y1; #y2; #z1; #z2; #H; + nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple a _ _ ⇒ x1 = a ]); + nrewrite < H; + nnormalize; + napply refl_eq. +nqed. + +nlemma triple_destruct_2 : +∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3. + triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → y1 = y2. + #T1; #T2; #T3; #x1; #x2; #y1; #y2; #z1; #z2; #H; + nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple _ b _ ⇒ y1 = b ]); + nrewrite < H; + nnormalize; + napply refl_eq. +nqed. + +nlemma triple_destruct_3 : +∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3. + triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → z1 = z2. + #T1; #T2; #T3; #x1; #x2; #y1; #y2; #z1; #z2; #H; + nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple _ _ c ⇒ z1 = c ]); + nrewrite < H; + nnormalize; + napply refl_eq. +nqed. + +nlemma symmetric_eqtriple : +∀T1,T2,T3:Type.∀p1,p2:Prod3T T1 T2 T3. +∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool. + (symmetricT T1 bool f1) → + (symmetricT T2 bool f2) → + (symmetricT T3 bool f3) → + (eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = eq_triple T1 T2 T3 p2 p1 f1 f2 f3). + #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H; #H1; #H2; + nelim p1; + #x1; #y1; #z1; + nelim p2; + #x2; #y2; #z2; + nnormalize; + nrewrite > (H x1 x2); + ncases (f1 x2 x1); + nnormalize; + ##[ ##1: nrewrite > (H1 y1 y2); + ncases (f2 y2 y1); + nnormalize; + ##[ ##1: nrewrite > (H2 z1 z2); napply refl_eq + ##| ##2: napply refl_eq + ##] + ##| ##2: napply refl_eq + ##] +nqed. + +nlemma eq_to_eqtriple : +∀T1,T2,T3.∀p1,p2:Prod3T T1 T2 T3. +∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool. + (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) → + (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) → + (∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) → + (p1 = p2 → eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = true). + #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3; + nelim p1; + #x1; #y1; #z1; + nelim p2; + #x2; #y2; #z2; #H; + nnormalize; + nrewrite > (H1 … (triple_destruct_1 … H)); + nnormalize; + nrewrite > (H2 … (triple_destruct_2 … H)); + nnormalize; + nrewrite > (H3 … (triple_destruct_3 … H)); + napply refl_eq. +nqed. + +nlemma eqtriple_to_eq : +∀T1,T2,T3.∀p1,p2:Prod3T T1 T2 T3. +∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool. + (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) → + (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) → + (∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) → + (eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = true → p1 = p2). + #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3; + nelim p1; + #x1; #y1; #z1; + nelim p2; + #x2; #y2; #z2; #H; + nnormalize in H:(%); + nletin K ≝ (H1 x1 x2); + ncases (f1 x1 x2) in H:(%) K:(%); + nnormalize; + ##[ ##2: #H4; napply (bool_destruct … H4) ##] + nletin K1 ≝ (H2 y1 y2); + ncases (f2 y1 y2) in K1:(%) ⊢ %; + nnormalize; + ##[ ##2: #H4; #H5; napply (bool_destruct … H5) ##] + #H4; #H5; #H6; + nrewrite > (H4 (refl_eq …)); + nrewrite > (H6 (refl_eq …)); + nrewrite > (H3 z1 z2 H5); + napply refl_eq. +nqed. + +nlemma quadruple_destruct_1 : +∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4. + quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → x1 = x2. + #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H; + nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple a _ _ _ ⇒ x1 = a ]); + nrewrite < H; + nnormalize; + napply refl_eq. +nqed. + +nlemma quadruple_destruct_2 : +∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4. + quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → y1 = y2. + #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H; + nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ b _ _ ⇒ y1 = b ]); + nrewrite < H; + nnormalize; + napply refl_eq. +nqed. + +nlemma quadruple_destruct_3 : +∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4. + quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → z1 = z2. + #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H; + nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ _ c _ ⇒ z1 = c ]); + nrewrite < H; + nnormalize; + napply refl_eq. +nqed. + +nlemma quadruple_destruct_4 : +∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4. + quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → v1 = v2. + #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H; + nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ _ _ d ⇒ v1 = d ]); + nrewrite < H; + nnormalize; + napply refl_eq. +nqed. + +nlemma symmetric_eqquadruple : +∀T1,T2,T3,T4:Type.∀p1,p2:Prod4T T1 T2 T3 T4. +∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool. + (symmetricT T1 bool f1) → + (symmetricT T2 bool f2) → + (symmetricT T3 bool f3) → + (symmetricT T4 bool f4) → + (eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = eq_quadruple T1 T2 T3 T4 p2 p1 f1 f2 f3 f4). + #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H; #H1; #H2; #H3; + nelim p1; + #x1; #y1; #z1; #v1; + nelim p2; + #x2; #y2; #z2; #v2; + nnormalize; + nrewrite > (H x1 x2); + ncases (f1 x2 x1); + nnormalize; + ##[ ##1: nrewrite > (H1 y1 y2); + ncases (f2 y2 y1); + nnormalize; + ##[ ##1: nrewrite > (H2 z1 z2); + ncases (f3 z2 z1); + nnormalize; + ##[ ##1: nrewrite > (H3 v1 v2); napply refl_eq + ##| ##2: napply refl_eq + ##] + ##| ##2: napply refl_eq + ##] + ##| ##2: napply refl_eq + ##] +nqed. + +nlemma eq_to_eqquadruple : +∀T1,T2,T3,T4.∀p1,p2:Prod4T T1 T2 T3 T4. +∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool. + (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) → + (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) → + (∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) → + (∀v1,v2:T4.v1 = v2 → f4 v1 v2 = true) → + (p1 = p2 → eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = true). + #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4; + nelim p1; + #x1; #y1; #z1; #v1; + nelim p2; + #x2; #y2; #z2; #v2; #H; + nnormalize; + nrewrite > (H1 … (quadruple_destruct_1 … H)); + nnormalize; + nrewrite > (H2 … (quadruple_destruct_2 … H)); + nnormalize; + nrewrite > (H3 … (quadruple_destruct_3 … H)); + nnormalize; + nrewrite > (H4 … (quadruple_destruct_4 … H)); + napply refl_eq. +nqed. + +nlemma eqquadruple_to_eq : +∀T1,T2,T3,T4.∀p1,p2:Prod4T T1 T2 T3 T4. +∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool. + (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) → + (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) → + (∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) → + (∀v1,v2:T4.f4 v1 v2 = true → v1 = v2) → + (eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = true → p1 = p2). + #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4; + nelim p1; + #x1; #y1; #z1; #v1; + nelim p2; + #x2; #y2; #z2; #v2; #H; + nnormalize in H:(%); + nletin K ≝ (H1 x1 x2); + ncases (f1 x1 x2) in H:(%) K:(%); + nnormalize; + ##[ ##2: #H5; napply (bool_destruct … H5) ##] + nletin K1 ≝ (H2 y1 y2); + ncases (f2 y1 y2) in K1:(%) ⊢ %; + nnormalize; + ##[ ##2: #H5; #H6; napply (bool_destruct … H6) ##] + nletin K2 ≝ (H3 z1 z2); + ncases (f3 z1 z2) in K2:(%) ⊢ %; + nnormalize; + ##[ ##2: #H5; #H6; #H7; napply (bool_destruct … H7) ##] + #H5; #H6; #H7; #H8; + nrewrite > (H5 (refl_eq …)); + nrewrite > (H6 (refl_eq …)); + nrewrite > (H8 (refl_eq …)); + nrewrite > (H4 v1 v2 H7); + napply refl_eq. +nqed. + +nlemma quintuple_destruct_1 : +∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5. + quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → x1 = x2. + #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H; + nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple a _ _ _ _ ⇒ x1 = a ]); + nrewrite < H; + nnormalize; + napply refl_eq. +nqed. + +nlemma quintuple_destruct_2 : +∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5. + quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → y1 = y2. + #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H; + nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ b _ _ _ ⇒ y1 = b ]); + nrewrite < H; + nnormalize; + napply refl_eq. +nqed. + +nlemma quintuple_destruct_3 : +∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5. + quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → z1 = z2. + #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H; + nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ c _ _ ⇒ z1 = c ]); + nrewrite < H; + nnormalize; + napply refl_eq. +nqed. + +nlemma quintuple_destruct_4 : +∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5. + quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → v1 = v2. + #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H; + nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ _ d _ ⇒ v1 = d ]); + nrewrite < H; + nnormalize; + napply refl_eq. +nqed. + +nlemma quintuple_destruct_5 : +∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5. + quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → w1 = w2. + #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H; + nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ _ _ e ⇒ w1 = e ]); + nrewrite < H; + nnormalize; + napply refl_eq. +nqed. + +nlemma symmetric_eqquintuple : +∀T1,T2,T3,T4,T5:Type.∀p1,p2:Prod5T T1 T2 T3 T4 T5. +∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool. + (symmetricT T1 bool f1) → + (symmetricT T2 bool f2) → + (symmetricT T3 bool f3) → + (symmetricT T4 bool f4) → + (symmetricT T5 bool f5) → + (eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = eq_quintuple T1 T2 T3 T4 T5 p2 p1 f1 f2 f3 f4 f5). + #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H; #H1; #H2; #H3; #H4; + nelim p1; + #x1; #y1; #z1; #v1; #w1; + nelim p2; + #x2; #y2; #z2; #v2; #w2; + nnormalize; + nrewrite > (H x1 x2); + ncases (f1 x2 x1); + nnormalize; + ##[ ##1: nrewrite > (H1 y1 y2); + ncases (f2 y2 y1); + nnormalize; + ##[ ##1: nrewrite > (H2 z1 z2); + ncases (f3 z2 z1); + nnormalize; + ##[ ##1: nrewrite > (H3 v1 v2); + ncases (f4 v2 v1); + nnormalize; + ##[ ##1: nrewrite > (H4 w1 w2); napply refl_eq + ##| ##2: napply refl_eq + ##] + ##| ##2: napply refl_eq + ##] + ##| ##2: napply refl_eq + ##] + ##| ##2: napply refl_eq + ##] +nqed. + +nlemma eq_to_eqquintuple : +∀T1,T2,T3,T4,T5.∀p1,p2:Prod5T T1 T2 T3 T4 T5. +∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool. + (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) → + (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) → + (∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) → + (∀v1,v2:T4.v1 = v2 → f4 v1 v2 = true) → + (∀w1,w2:T5.w1 = w2 → f5 w1 w2 = true) → + (p1 = p2 → eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = true). + #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5; + nelim p1; + #x1; #y1; #z1; #v1; #w1; + nelim p2; + #x2; #y2; #z2; #v2; #w2; #H; + nnormalize; + nrewrite > (H1 … (quintuple_destruct_1 … H)); + nnormalize; + nrewrite > (H2 … (quintuple_destruct_2 … H)); + nnormalize; + nrewrite > (H3 … (quintuple_destruct_3 … H)); + nnormalize; + nrewrite > (H4 … (quintuple_destruct_4 … H)); + nnormalize; + nrewrite > (H5 … (quintuple_destruct_5 … H)); + napply refl_eq. +nqed. + +nlemma eqquintuple_to_eq : +∀T1,T2,T3,T4,T5.∀p1,p2:Prod5T T1 T2 T3 T4 T5. +∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool. + (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) → + (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) → + (∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) → + (∀v1,v2:T4.f4 v1 v2 = true → v1 = v2) → + (∀w1,w2:T5.f5 w1 w2 = true → w1 = w2) → + (eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = true → p1 = p2). + #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5; + nelim p1; + #x1; #y1; #z1; #v1; #w1; + nelim p2; + #x2; #y2; #z2; #v2; #w2; #H; + nnormalize in H:(%); + nletin K ≝ (H1 x1 x2); + ncases (f1 x1 x2) in H:(%) K:(%); + nnormalize; + ##[ ##2: #H6; napply (bool_destruct … H6) ##] + nletin K1 ≝ (H2 y1 y2); + ncases (f2 y1 y2) in K1:(%) ⊢ %; + nnormalize; + ##[ ##2: #H6; #H7; napply (bool_destruct … H7) ##] + nletin K2 ≝ (H3 z1 z2); + ncases (f3 z1 z2) in K2:(%) ⊢ %; + nnormalize; + ##[ ##2: #H6; #H7; #H8; napply (bool_destruct … H8) ##] + nletin K3 ≝ (H4 v1 v2); + ncases (f4 v1 v2) in K3:(%) ⊢ %; + nnormalize; + ##[ ##2: #H6; #H7; #H8; #H9; napply (bool_destruct … H9) ##] + #H6; #H7; #H8; #H9; #H10; + nrewrite > (H6 (refl_eq …)); + nrewrite > (H7 (refl_eq …)); + nrewrite > (H8 (refl_eq …)); + nrewrite > (H10 (refl_eq …)); + nrewrite > (H5 w1 w2 H9); + napply refl_eq. +nqed. diff --git a/helm/software/matita/contribs/ng_assembly/common/theory.ma b/helm/software/matita/contribs/ng_assembly/common/theory.ma new file mode 100644 index 000000000..0cdc02a4c --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/common/theory.ma @@ -0,0 +1,230 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* ********************************************************************** *) + +universe constraint Type[0] < Type[1]. + +(* ********************************** *) +(* SOTTOINSIEME MINIMALE DELLA TEORIA *) +(* ********************************** *) + +(* logic/connectives.ma *) + +ninductive True: Prop ≝ + I : True. + +ninductive False: Prop ≝. + +ndefinition Not: Prop → Prop ≝ +λA.(A → False). + +interpretation "logical not" 'not x = (Not x). + +nlemma absurd : ∀A,C:Prop.A → ¬A → C. + #A; #C; #H; + nnormalize; + #H1; + nelim (H1 H); +nqed. + +nlemma not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A. + #A; #B; #H; + nnormalize; + #H1; #H2; + nelim (H1 (H H2)). +nqed. + +nlemma prop_to_nnprop : ∀P.P → ¬¬P. + #P; nnormalize; #H; #H1; + napply (H1 H). +nqed. + +(* +naxiom RAA : ∀P:Prop.∀f:(¬P) → False.P. + +nlemma nnprop_to_prop : ∀P.(¬¬P) → P. + #P; nchange with (((¬P) → False) → P); + #H; napply (RAA P H). +nqed. +*) + +ninductive And (A,B:Prop) : Prop ≝ + conj : A → B → (And A B). + +interpretation "logical and" 'and x y = (And x y). + +nlemma proj1: ∀A,B:Prop.A ∧ B → A. + #A; #B; #H; + (* \ldots al posto di ??? *) + napply (And_ind A B … H); + #H1; #H2; + napply H1. +nqed. + +nlemma proj2: ∀A,B:Prop.A ∧ B → B. + #A; #B; #H; + napply (And_ind A B … H); + #H1; #H2; + napply H2. +nqed. + +ninductive Or (A,B:Prop) : Prop ≝ + or_introl : A → (Or A B) +| or_intror : B → (Or A B). + +interpretation "logical or" 'or x y = (Or x y). + +ndefinition decidable : Prop → Prop ≝ λA:Prop.A ∨ ¬A. + +(* +nlemma decidable_prop : ∀P:Prop.decidable P. + #P; nnormalize; + napply RAA; + #H; + napply (absurd (P ∨ (¬P)) …); + ##[ ##2: napply H + ##| ##1: napply (or_intror P (¬P)); + napply RAA; + #H1; + napply (absurd (P ∨ (¬P)) …); + ##[ ##2: napply H + ##| ##1: napply (or_introl P (¬P)); + napply (nnprop_to_prop P H1) + ##] + ##] +nqed. + +nlemma terzo_escluso : ∀P,G:Prop.∀ft:P → G.∀ff:(¬P) → G.G. + #P; #G; nnormalize; + #H; #H1; + napply (Or_ind P (P → False) ? H H1 ?); + napply (decidable_prop P). +nqed. +*) + +nlemma or_elim : ∀P,Q,G:Prop.Or P Q → ∀fp:P → G.∀fq:Q → G.G. + #P; #Q; #G; #H; #H1; #H2; + napply (Or_ind P Q ? H1 H2 ?); + napply H. +nqed. + +ninductive ex (A:Type) (Q:A → Prop) : Prop ≝ + ex_intro: ∀x:A.Q x → ex A Q. + +interpretation "exists" 'exists x = (ex ? x). + +ninductive ex2 (A:Type) (Q,R:A → Prop) : Prop ≝ + ex_intro2: ∀x:A.Q x → R x → ex2 A Q R. + +ndefinition iff ≝ +λA,B.(A → B) ∧ (B → A). + +(* higher_order_defs/relations *) + +ndefinition relation : Type → Type ≝ +λA:Type.A → A → Prop. + +ndefinition reflexive : ∀A:Type.∀R:relation A.Prop ≝ +λA.λR.∀x:A.R x x. + +ndefinition symmetric : ∀A:Type.∀R:relation A.Prop ≝ +λA.λR.∀x,y:A.R x y → R y x. + +ndefinition transitive : ∀A:Type.∀R:relation A.Prop ≝ +λA.λR.∀x,y,z:A.R x y → R y z → R x z. + +ndefinition irreflexive : ∀A:Type.∀R:relation A.Prop ≝ +λA.λR.∀x:A.¬ (R x x). + +ndefinition cotransitive : ∀A:Type.∀R:relation A.Prop ≝ +λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y. + +ndefinition tight_apart : ∀A:Type.∀eq,ap:relation A.Prop ≝ +λA.λeq,ap.∀x,y:A. (¬ (ap x y) → eq x y) ∧ (eq x y → ¬ (ap x y)). + +ndefinition antisymmetric : ∀A:Type.∀R:relation A.Prop ≝ +λA.λR.∀x,y:A.R x y → ¬ (R y x). + +(* logic/equality.ma *) + +ninductive eq (A:Type) (x:A) : A → Prop ≝ + refl_eq : eq A x x. + +interpretation "leibnitz's equality" 'eq t x y = (eq t x y). + +interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)). + +nlemma eq_f : ∀T1,T2:Type.∀x,y:T1.∀f:T1 → T2.x = y → (f x) = (f y). + #T1; #T2; #x; #y; #f; #H; + nrewrite < H; + napply refl_eq. +nqed. + +nlemma eq_f2 : ∀T1,T2,T3:Type.∀x1,y1:T1.∀x2,y2:T2.∀f:T1 → T2 → T3.x1 = y1 → x2 = y2 → f x1 x2 = f y1 y2. + #T1; #T2; #T3; #x1; #y1; #x2; #y2; #f; #H1; #H2; + nrewrite < H1; + nrewrite < H2; + napply refl_eq. +nqed. + +nlemma neqf_to_neq : ∀T1,T2:Type.∀x,y:T1.∀f:T1 → T2.((f x) ≠ (f y)) → x ≠ y. + #T1; #T2; #x; #y; #f; + nnormalize; #H; #H1; + napply (H (eq_f … H1)). +nqed. + +(* +nlemma neqf2_to_neq : ∀T1,T2,T3:Type.∀x1,y1:T1.∀x2,y2:T2.∀f:T1 → T2 → T3.f x1 x2 ≠ f y1 y2 → (x1 ≠ y1) ∨ (x2 ≠ y2). + #T1; #T2; #T3; #x1; #y1; #x2; #y2; #f; nnormalize; #H; + napply (terzo_escluso (x1 = y1) …); + ##[ ##2: #H1; napply (or_introl … H1) + ##| ##1: #H1; napply (terzo_escluso (x2 = y2) …) + ##[ ##2: #H2; napply (or_intror … H2) + ##| ##1: #H2; nrewrite < H1 in H:(%); + nrewrite < H2; #H; + nelim (H (refl_eq …)) + ##] + ##] +nqed. +*) + +nlemma symmetric_eq: ∀A:Type. symmetric A (eq A). + #A; + nnormalize; + #x; #y; #H; + nrewrite < H; + napply refl_eq. +nqed. + +nlemma eq_elim_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y. + #A; #x; #P; #H; #y; #H1; + nrewrite < (symmetric_eq … H1); + napply H. +nqed. + +ndefinition relationT : Type → Type → Type ≝ +λA,T:Type.A → A → T. + +ndefinition symmetricT: ∀A,T:Type.∀R:relationT A T.Prop ≝ +λA,T.λR.∀x,y:A.R x y = R y x. + +ndefinition associative : ∀A:Type.∀R:relationT A A.Prop ≝ +λA.λR.∀x,y,z:A.R (R x y) z = R x (R y z). diff --git a/helm/software/matita/contribs/ng_assembly/depends b/helm/software/matita/contribs/ng_assembly/depends index 3db4d02d8..8e0fddce2 100644 --- a/helm/software/matita/contribs/ng_assembly/depends +++ b/helm/software/matita/contribs/ng_assembly/depends @@ -1,62 +1,14 @@ -freescale/byte8.ma freescale/bitrigesim.ma freescale/exadecim.ma -freescale/status.ma freescale/memory_abs.ma freescale/opcode_base.ma freescale/prod.ma -freescale/memory_bits.ma freescale/memory_trees.ma -utility/ascii_lemmas1.ma freescale/theory.ma utility/ascii.ma -freescale/byte8_lemmas.ma freescale/byte8.ma freescale/exadecim_lemmas.ma -utility/string_lemmas.ma utility/ascii_lemmas2.ma utility/string.ma utility/utility_lemmas.ma -freescale/table_HCS08_tests.ma freescale/table_HCS08.ma -freescale/multivm.ma freescale/load_write.ma -freescale/opcode_base_lemmas.ma freescale/bool_lemmas.ma freescale/opcode_base.ma -compiler/ast_type_lemmas.ma compiler/ast_type.ma utility/utility_lemmas.ma -freescale/table_HC05_tests.ma freescale/table_HC05.ma -freescale/option.ma freescale/bool.ma -freescale/bool.ma freescale/pts.ma -freescale/bool_lemmas.ma freescale/bool.ma freescale/theory.ma -freescale/opcode_base_lemmas_opcode1.ma freescale/bool_lemmas.ma freescale/opcode_base.ma -freescale/memory_func.ma freescale/memory_struct.ma freescale/option.ma freescale/theory.ma freescale/word16.ma -freescale/load_write.ma freescale/model.ma freescale/translation.ma -freescale/bitrigesim.ma freescale/bool.ma -freescale/table_RS08.ma freescale/opcode.ma -freescale/oct.ma freescale/bool.ma -freescale/option_lemmas.ma freescale/bool_lemmas.ma freescale/option.ma -freescale/table_RS08_tests.ma freescale/table_RS08.ma -freescale/translation.ma freescale/option.ma freescale/table_HC05.ma freescale/table_HC08.ma freescale/table_HCS08.ma freescale/table_RS08.ma -freescale/medium_tests_tools.ma freescale/multivm.ma -utility/utility_lemmas.ma utility/utility.ma -freescale/memory_abs.ma freescale/memory_bits.ma freescale/memory_func.ma freescale/memory_trees.ma -freescale/bitrigesim_lemmas.ma freescale/bitrigesim.ma freescale/bool_lemmas.ma -test_errori.ma compiler/ast_type_lemmas.ma freescale/byte8_lemmas.ma utility/utility.ma -freescale/memory_struct.ma freescale/byte8.ma freescale/oct.ma -freescale/model.ma freescale/status.ma -freescale/table_HC05.ma freescale/opcode.ma -freescale/quatern_lemmas.ma freescale/bool_lemmas.ma freescale/quatern.ma -freescale/exadecim_lemmas.ma freescale/bool_lemmas.ma freescale/exadecim.ma -compiler/ast_type.ma utility/utility.ma -freescale/word16.ma freescale/byte8.ma -utility/ascii.ma freescale/bool.ma -freescale/memory_trees.ma freescale/memory_struct.ma freescale/option.ma freescale/theory.ma freescale/word16.ma -freescale/pts.ma -freescale/opcode_base_lemmas_instrmode2.ma freescale/opcode_base_lemmas_instrmode1.ma -freescale/opcode_base_lemmas1.ma freescale/opcode_base_lemmas_instrmode2.ma freescale/opcode_base_lemmas_opcode2.ma freescale/word16_lemmas.ma -freescale/table_HC08.ma freescale/opcode.ma -freescale/prod.ma freescale/bool.ma -utility/string.ma freescale/theory.ma utility/ascii.ma utility/utility.ma -freescale/table_HCS08.ma freescale/opcode.ma -freescale/word32.ma freescale/word16.ma -freescale/prod_lemmas.ma freescale/bool_lemmas.ma freescale/prod.ma -freescale/opcode_base.ma freescale/bitrigesim.ma freescale/oct.ma freescale/theory.ma freescale/word16.ma -freescale/word32_lemmas.ma freescale/word16_lemmas.ma freescale/word32.ma -freescale/status_lemmas.ma freescale/opcode_base_lemmas1.ma freescale/option_lemmas.ma freescale/prod_lemmas.ma freescale/status.ma freescale/word16_lemmas.ma -utility/ascii_lemmas2.ma freescale/bool_lemmas.ma utility/ascii_lemmas1.ma -freescale/micro_tests.ma freescale/multivm.ma freescale/status_lemmas.ma -freescale/table_HC08_tests.ma freescale/table_HC08.ma -utility/utility.ma freescale/option.ma freescale/theory.ma -freescale/quatern.ma freescale/bool.ma -freescale/opcode_base_lemmas_instrmode1.ma freescale/bitrigesim_lemmas.ma freescale/exadecim_lemmas.ma freescale/oct_lemmas.ma freescale/opcode_base.ma -freescale/word16_lemmas.ma freescale/byte8_lemmas.ma freescale/word16.ma -freescale/exadecim.ma freescale/bool.ma freescale/oct.ma freescale/prod.ma freescale/quatern.ma -freescale/theory.ma freescale/pts.ma -freescale/opcode_base_lemmas_opcode2.ma freescale/opcode_base_lemmas_opcode1.ma -freescale/medium_tests.ma freescale/medium_tests_tools.ma utility/utility.ma -freescale/opcode.ma freescale/opcode_base.ma -freescale/oct_lemmas.ma freescale/bool_lemmas.ma freescale/oct.ma +num/exadecim.ma common/prod.ma num/bool.ma num/oct.ma num/quatern.ma +common/option.ma num/bool.ma +test_errori.ma +common/theory.ma +num/quatern.ma num/bool.ma +common/prod.ma num/bool.ma +num/bool.ma common/theory.ma +num/quatern_lemmas.ma num/bool_lemmas.ma num/quatern.ma +common/option_lemmas.ma common/option.ma num/bool_lemmas.ma +common/prod_lemmas.ma common/prod.ma num/bool_lemmas.ma +num/oct_lemmas.ma num/bool_lemmas.ma num/oct.ma +num/bool_lemmas.ma num/bool.ma +num/exadecim_lemmas.ma num/bool_lemmas.ma num/exadecim.ma +num/oct.ma num/bool.ma diff --git a/helm/software/matita/contribs/ng_assembly/num/bool.ma b/helm/software/matita/contribs/ng_assembly/num/bool.ma new file mode 100755 index 000000000..a4fa2eea9 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/num/bool.ma @@ -0,0 +1,78 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* ********************************************************************** *) + +include "common/theory.ma". + +(* ******** *) +(* BOOLEANI *) +(* ******** *) + +ninductive bool : Type ≝ + true : bool +| false : bool. + +(* operatori booleani *) + +ndefinition eq_bool ≝ +λb1,b2:bool.match b1 with + [ true ⇒ match b2 with [ true ⇒ true | false ⇒ false ] + | false ⇒ match b2 with [ true ⇒ false | false ⇒ true ] + ]. + +ndefinition not_bool ≝ +λb:bool.match b with [ true ⇒ false | false ⇒ true ]. + +ndefinition and_bool ≝ +λb1,b2:bool.match b1 with + [ true ⇒ b2 | false ⇒ false ]. + +ndefinition or_bool ≝ +λb1,b2:bool.match b1 with + [ true ⇒ true | false ⇒ b2 ]. + +ndefinition xor_bool ≝ +λb1,b2:bool.match b1 with + [ true ⇒ not_bool b2 + | false ⇒ b2 ]. + +(* \ominus *) +notation "hvbox(⊖ a)" non associative with precedence 36 + for @{ 'not_bool $a }. +interpretation "not_bool" 'not_bool x = (not_bool x). + +(* \otimes *) +notation "hvbox(a break ⊗ b)" left associative with precedence 35 + for @{ 'and_bool $a $b }. +interpretation "and_bool" 'and_bool x y = (and_bool x y). + +(* \oplus *) +notation "hvbox(a break ⊕ b)" left associative with precedence 34 + for @{ 'or_bool $a $b }. +interpretation "or_bool" 'or_bool x y = (or_bool x y). + +(* \odot *) +notation "hvbox(a break ⊙ b)" left associative with precedence 33 + for @{ 'xor_bool $a $b }. +interpretation "xor_bool" 'xor_bool x y = (xor_bool x y). + +ndefinition boolRelation : Type → Type ≝ +λA:Type.A → A → bool. diff --git a/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma new file mode 100755 index 000000000..25d855d31 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma @@ -0,0 +1,193 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* ********************************************************************** *) + +include "num/bool.ma". + +(* ******** *) +(* BOOLEANI *) +(* ******** *) + +ndefinition bool_destruct_aux ≝ +Πb1,b2:bool.ΠP:Prop.b1 = b2 → + match b1 with + [ true ⇒ match b2 with [ true ⇒ P → P | false ⇒ P ] + | false ⇒ match b2 with [ true ⇒ P | false ⇒ P → P ] + ]. + +ndefinition bool_destruct : bool_destruct_aux. + #b1; #b2; #P; + nelim b1; + nelim b2; + nnormalize; + #H; + ##[ ##2: napply False_ind; + nchange with (match true with [ true ⇒ False | false ⇒ True]); + nrewrite > H; + nnormalize; + napply I + ##| ##3: napply False_ind; + nchange with (match true with [ true ⇒ False | false ⇒ True]); + nrewrite < H; + nnormalize; + napply I + ##| ##1,4: napply (λx:P.x) + ##] +nqed. + +nlemma symmetric_eqbool : symmetricT bool bool eq_bool. + #b1; #b2; + nelim b1; + nelim b2; + nnormalize; + napply refl_eq. +nqed. + +nlemma symmetric_andbool : symmetricT bool bool and_bool. + #b1; #b2; + nelim b1; + nelim b2; + nnormalize; + napply refl_eq. +nqed. + +nlemma associative_andbool : ∀b1,b2,b3.((b1 ⊗ b2) ⊗ b3) = (b1 ⊗ (b2 ⊗ b3)). + #b1; #b2; #b3; + nelim b1; + nelim b2; + nelim b3; + nnormalize; + napply refl_eq. +nqed. + +nlemma symmetric_orbool : symmetricT bool bool or_bool. + #b1; #b2; + nelim b1; + nelim b2; + nnormalize; + napply refl_eq. +nqed. + +nlemma associative_orbool : ∀b1,b2,b3.((b1 ⊕ b2) ⊕ b3) = (b1 ⊕ (b2 ⊕ b3)). + #b1; #b2; #b3; + nelim b1; + nelim b2; + nelim b3; + nnormalize; + napply refl_eq. +nqed. + +nlemma symmetric_xorbool : symmetricT bool bool xor_bool. + #b1; #b2; + nelim b1; + nelim b2; + nnormalize; + napply refl_eq. +nqed. + +nlemma associative_xorbool : ∀b1,b2,b3.((b1 ⊙ b2) ⊙ b3) = (b1 ⊙ (b2 ⊙ b3)). + #b1; #b2; #b3; + nelim b1; + nelim b2; + nelim b3; + nnormalize; + napply refl_eq. +nqed. + +nlemma eqbool_to_eq : ∀b1,b2:bool.(eq_bool b1 b2 = true) → (b1 = b2). + #b1; #b2; + ncases b1; + ncases b2; + nnormalize; + ##[ ##1,4: #H; napply refl_eq + ##| ##*: #H; napply (bool_destruct … H) + ##] +nqed. + +nlemma eq_to_eqbool : ∀b1,b2.b1 = b2 → eq_bool b1 b2 = true. + #b1; #b2; + ncases b1; + ncases b2; + nnormalize; + ##[ ##1,4: #H; napply refl_eq + ##| ##*: #H; napply (bool_destruct … H) + ##] +nqed. + +nlemma neqbool_to_neq : ∀b1,b2:bool.(eq_bool b1 b2 = false) → (b1 ≠ b2). + #b1; #b2; + ncases b1; + ncases b2; + nnormalize; + ##[ ##1,4: #H; napply (bool_destruct … H) + ##| ##*: #H; #H1; napply (bool_destruct … H1) + ##] +nqed. + +nlemma neq_to_neqbool : ∀b1,b2.b1 ≠ b2 → eq_bool b1 b2 = false. + #b1; #b2; + ncases b1; + ncases b2; + nnormalize; + ##[ ##1,4: #H; napply False_ind; napply (H (refl_eq …)) + ##| ##*: #H; napply refl_eq + ##] +nqed. + +nlemma andb_true_true_l: ∀b1,b2.(b1 ⊗ b2) = true → b1 = true. + #b1; #b2; + ncases b1; + ncases b2; + nnormalize; + ##[ ##1,2: #H; napply refl_eq + ##| ##*: #H; napply (bool_destruct … H) + ##] +nqed. + +nlemma andb_true_true_r: ∀b1,b2.(b1 ⊗ b2) = true → b2 = true. + #b1; #b2; + ncases b1; + ncases b2; + nnormalize; + ##[ ##1,3: #H; napply refl_eq + ##| ##*: #H; napply (bool_destruct … H) + ##] +nqed. + +nlemma orb_false_false_l : ∀b1,b2:bool.(b1 ⊕ b2) = false → b1 = false. + #b1; #b2; + ncases b1; + ncases b2; + nnormalize; + ##[ ##4: #H; napply refl_eq + ##| ##*: #H; napply (bool_destruct … H) + ##] +nqed. + +nlemma orb_false_false_r : ∀b1,b2:bool.(b1 ⊕ b2) = false → b2 = false. + #b1; #b2; + ncases b1; + ncases b2; + nnormalize; + ##[ ##4: #H; napply refl_eq + ##| ##*: #H; napply (bool_destruct … H) + ##] +nqed. diff --git a/helm/software/matita/contribs/ng_assembly/num/exadecim.ma b/helm/software/matita/contribs/ng_assembly/num/exadecim.ma new file mode 100755 index 000000000..10019b379 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/num/exadecim.ma @@ -0,0 +1,1419 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* ********************************************************************** *) + +include "num/bool.ma". +include "num/quatern.ma". +include "num/oct.ma". +include "common/prod.ma". + +(* *********** *) +(* ESADECIMALI *) +(* *********** *) + +ninductive exadecim : Type ≝ + x0: exadecim +| x1: exadecim +| x2: exadecim +| x3: exadecim +| x4: exadecim +| x5: exadecim +| x6: exadecim +| x7: exadecim +| x8: exadecim +| x9: exadecim +| xA: exadecim +| xB: exadecim +| xC: exadecim +| xD: exadecim +| xE: exadecim +| xF: exadecim. + +(* operatore = *) +ndefinition eq_ex ≝ +λe1,e2:exadecim. + match e1 with + [ x0 ⇒ match e2 with [ x0 ⇒ true | _ ⇒ false ] + | x1 ⇒ match e2 with [ x1 ⇒ true | _ ⇒ false ] + | x2 ⇒ match e2 with [ x2 ⇒ true | _ ⇒ false ] + | x3 ⇒ match e2 with [ x3 ⇒ true | _ ⇒ false ] + | x4 ⇒ match e2 with [ x4 ⇒ true | _ ⇒ false ] + | x5 ⇒ match e2 with [ x5 ⇒ true | _ ⇒ false ] + | x6 ⇒ match e2 with [ x6 ⇒ true | _ ⇒ false ] + | x7 ⇒ match e2 with [ x7 ⇒ true | _ ⇒ false ] + | x8 ⇒ match e2 with [ x8 ⇒ true | _ ⇒ false ] + | x9 ⇒ match e2 with [ x9 ⇒ true | _ ⇒ false ] + | xA ⇒ match e2 with [ xA ⇒ true | _ ⇒ false ] + | xB ⇒ match e2 with [ xB ⇒ true | _ ⇒ false ] + | xC ⇒ match e2 with [ xC ⇒ true | _ ⇒ false ] + | xD ⇒ match e2 with [ xD ⇒ true | _ ⇒ false ] + | xE ⇒ match e2 with [ xE ⇒ true | _ ⇒ false ] + | xF ⇒ match e2 with [ xF ⇒ true | _ ⇒ false ] + ]. + +(* operatore < *) +ndefinition lt_ex ≝ +λe1,e2:exadecim. + match e1 with + [ x0 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true + | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true + | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x1 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true + | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true + | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x2 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true + | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true + | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x3 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true + | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x4 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true + | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x5 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true + | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x6 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true + | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x7 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true + | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x8 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true + | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x9 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true + | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | xA ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true + | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | xB ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | xC ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | xD ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ] + | xE ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ] + | xF ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + ]. + +(* operatore ≤ *) +ndefinition le_ex ≝ +λe1,e2:exadecim. + match e1 with + [ x0 ⇒ match e2 with + [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true + | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true + | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x1 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true + | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true + | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x2 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true + | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true + | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x3 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true + | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true + | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x4 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true + | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x5 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true + | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x6 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true + | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x7 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true + | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x8 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true + | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x9 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true + | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | xA ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true + | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | xB ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true + | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | xC ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | xD ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | xE ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ] + | xF ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ] + ]. + +(* operatore > *) +ndefinition gt_ex ≝ +λe1,e2:exadecim. + match e1 with + [ x0 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | x1 ⇒ match e2 with + [ x0 ⇒ true | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | x2 ⇒ match e2 with + [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | x3 ⇒ match e2 with + [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | x4 ⇒ match e2 with + [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | x5 ⇒ match e2 with + [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true + | x4 ⇒ true | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | x6 ⇒ match e2 with + [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true + | x4 ⇒ true | x5 ⇒ true | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | x7 ⇒ match e2 with + [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true + | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | x8 ⇒ match e2 with + [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true + | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | x9 ⇒ match e2 with + [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true + | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | xA ⇒ match e2 with + [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true + | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | xB ⇒ match e2 with + [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true + | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | xC ⇒ match e2 with + [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true + | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | xD ⇒ match e2 with + [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true + | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true + | xC ⇒ true | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | xE ⇒ match e2 with + [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true + | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true + | xC ⇒ true | xD ⇒ true | xE ⇒ false | xF ⇒ false ] + | xF ⇒ match e2 with + [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true + | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true + | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ false ] + ]. + +(* operatore ≥ *) +ndefinition ge_ex ≝ +λe1,e2:exadecim. + match e1 with + [ x0 ⇒ match e2 with + [ x0 ⇒ true | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | x1 ⇒ match e2 with + [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | x2 ⇒ match e2 with + [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | x3 ⇒ match e2 with + [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | x4 ⇒ match e2 with + [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true + | x4 ⇒ true | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | x5 ⇒ match e2 with + [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true + | x4 ⇒ true | x5 ⇒ true | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | x6 ⇒ match e2 with + [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true + | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | x7 ⇒ match e2 with + [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true + | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | x8 ⇒ match e2 with + [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true + | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | x9 ⇒ match e2 with + [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true + | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | xA ⇒ match e2 with + [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true + | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | xB ⇒ match e2 with + [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true + | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | xC ⇒ match e2 with + [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true + | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true + | xC ⇒ true | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | xD ⇒ match e2 with + [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true + | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true + | xC ⇒ true | xD ⇒ true | xE ⇒ false | xF ⇒ false ] + | xE ⇒ match e2 with + [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true + | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true + | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ false ] + | xF ⇒ match e2 with + [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true + | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true + | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + ]. + +(* operatore and *) +ndefinition and_ex ≝ +λe1,e2:exadecim.match e1 with + [ x0 ⇒ match e2 with + [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0 + | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x0 | x7 ⇒ x0 + | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x0 | xB ⇒ x0 + | xC ⇒ x0 | xD ⇒ x0 | xE ⇒ x0 | xF ⇒ x0 ] + | x1 ⇒ match e2 with + [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1 + | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x0 | x7 ⇒ x1 + | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x0 | xB ⇒ x1 + | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x0 | xF ⇒ x1 ] + | x2 ⇒ match e2 with + [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2 + | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x2 | x7 ⇒ x2 + | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x2 | xB ⇒ x2 + | xC ⇒ x0 | xD ⇒ x0 | xE ⇒ x2 | xF ⇒ x2 ] + | x3 ⇒ match e2 with + [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 + | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3 + | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 + | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ] + | x4 ⇒ match e2 with + [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0 + | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x4 | x7 ⇒ x4 + | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x0 | xB ⇒ x0 + | xC ⇒ x4 | xD ⇒ x4 | xE ⇒ x4 | xF ⇒ x4 ] + | x5 ⇒ match e2 with + [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1 + | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x4 | x7 ⇒ x5 + | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x0 | xB ⇒ x1 + | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x4 | xF ⇒ x5 ] + | x6 ⇒ match e2 with + [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2 + | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6 + | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x2 | xB ⇒ x2 + | xC ⇒ x4 | xD ⇒ x4 | xE ⇒ x6 | xF ⇒ x6 ] + | x7 ⇒ match e2 with + [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 + | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7 + | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 + | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ] + | x8 ⇒ match e2 with + [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0 + | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x0 | x7 ⇒ x0 + | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ x8 | xB ⇒ x8 + | xC ⇒ x8 | xD ⇒ x8 | xE ⇒ x8 | xF ⇒ x8 ] + | x9 ⇒ match e2 with + [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1 + | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x0 | x7 ⇒ x1 + | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ x8 | xB ⇒ x9 + | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ x8 | xF ⇒ x9 ] + | xA ⇒ match e2 with + [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2 + | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x2 | x7 ⇒ x2 + | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA + | xC ⇒ x8 | xD ⇒ x8 | xE ⇒ xA | xF ⇒ xA ] + | xB ⇒ match e2 with + [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 + | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3 + | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB + | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ] + | xC ⇒ match e2 with + [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0 + | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x4 | x7 ⇒ x4 + | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ x8 | xB ⇒ x8 + | xC ⇒ xC | xD ⇒ xC | xE ⇒ xC | xF ⇒ xC ] + | xD ⇒ match e2 with + [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1 + | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x4 | x7 ⇒ x5 + | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ x8 | xB ⇒ x9 + | xC ⇒ xC | xD ⇒ xD | xE ⇒ xC | xF ⇒ xD ] + | xE ⇒ match e2 with + [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2 + | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6 + | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA + | xC ⇒ xC | xD ⇒ xC | xE ⇒ xE | xF ⇒ xE ] + | xF ⇒ match e2 with + [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 + | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7 + | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB + | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ] + ]. + +(* operatore or *) +ndefinition or_ex ≝ +λe1,e2:exadecim.match e1 with + [ x0 ⇒ match e2 with + [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 + | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7 + | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB + | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ] + | x1 ⇒ match e2 with + [ x0 ⇒ x1 | x1 ⇒ x1 | x2 ⇒ x3 | x3 ⇒ x3 + | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7 + | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB + | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ] + | x2 ⇒ match e2 with + [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x2 | x3 ⇒ x3 + | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x6 | x7 ⇒ x7 + | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xA | xB ⇒ xB + | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ] + | x3 ⇒ match e2 with + [ x0 ⇒ x3 | x1 ⇒ x3 | x2 ⇒ x3 | x3 ⇒ x3 + | x4 ⇒ x7 | x5 ⇒ x7 | x6 ⇒ x7 | x7 ⇒ x7 + | x8 ⇒ xB | x9 ⇒ xB | xA ⇒ xB | xB ⇒ xB + | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ] + | x4 ⇒ match e2 with + [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 + | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7 + | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF + | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ] + | x5 ⇒ match e2 with + [ x0 ⇒ x5 | x1 ⇒ x5 | x2 ⇒ x7 | x3 ⇒ x7 + | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7 + | x8 ⇒ xD | x9 ⇒ xD | xA ⇒ xF | xB ⇒ xF + | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ] + | x6 ⇒ match e2 with + [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x6 | x3 ⇒ x7 + | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x6 | x7 ⇒ x7 + | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xE | xB ⇒ xF + | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ] + | x7 ⇒ match e2 with + [ x0 ⇒ x7 | x1 ⇒ x7 | x2 ⇒ x7 | x3 ⇒ x7 + | x4 ⇒ x7 | x5 ⇒ x7 | x6 ⇒ x7 | x7 ⇒ x7 + | x8 ⇒ xF | x9 ⇒ xF | xA ⇒ xF | xB ⇒ xF + | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ] + | x8 ⇒ match e2 with + [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB + | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF + | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB + | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ] + | x9 ⇒ match e2 with + [ x0 ⇒ x9 | x1 ⇒ x9 | x2 ⇒ xB | x3 ⇒ xB + | x4 ⇒ xD | x5 ⇒ xD | x6 ⇒ xF | x7 ⇒ xF + | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB + | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ] + | xA ⇒ match e2 with + [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xA | x3 ⇒ xB + | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xE | x7 ⇒ xF + | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xA | xB ⇒ xB + | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ] + | xB ⇒ match e2 with + [ x0 ⇒ xB | x1 ⇒ xB | x2 ⇒ xB | x3 ⇒ xB + | x4 ⇒ xF | x5 ⇒ xF | x6 ⇒ xF | x7 ⇒ xF + | x8 ⇒ xB | x9 ⇒ xB | xA ⇒ xB | xB ⇒ xB + | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ] + | xC ⇒ match e2 with + [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF + | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF + | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF + | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ] + | xD ⇒ match e2 with + [ x0 ⇒ xD | x1 ⇒ xD | x2 ⇒ xF | x3 ⇒ xF + | x4 ⇒ xD | x5 ⇒ xD | x6 ⇒ xF | x7 ⇒ xF + | x8 ⇒ xD | x9 ⇒ xD | xA ⇒ xF | xB ⇒ xF + | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ] + | xE ⇒ match e2 with + [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ xE | x3 ⇒ xF + | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xE | x7 ⇒ xF + | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xE | xB ⇒ xF + | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ] + | xF ⇒ match e2 with + [ x0 ⇒ xF | x1 ⇒ xF | x2 ⇒ xF | x3 ⇒ xF + | x4 ⇒ xF | x5 ⇒ xF | x6 ⇒ xF | x7 ⇒ xF + | x8 ⇒ xF | x9 ⇒ xF | xA ⇒ xF | xB ⇒ xF + | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ] + ]. + +(* operatore xor *) +ndefinition xor_ex ≝ +λe1,e2:exadecim.match e1 with + [ x0 ⇒ match e2 with + [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 + | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7 + | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB + | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ] + | x1 ⇒ match e2 with + [ x0 ⇒ x1 | x1 ⇒ x0 | x2 ⇒ x3 | x3 ⇒ x2 + | x4 ⇒ x5 | x5 ⇒ x4 | x6 ⇒ x7 | x7 ⇒ x6 + | x8 ⇒ x9 | x9 ⇒ x8 | xA ⇒ xB | xB ⇒ xA + | xC ⇒ xD | xD ⇒ xC | xE ⇒ xF | xF ⇒ xE ] + | x2 ⇒ match e2 with + [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x0 | x3 ⇒ x1 + | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x4 | x7 ⇒ x5 + | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ x8 | xB ⇒ x9 + | xC ⇒ xE | xD ⇒ xF | xE ⇒ xC | xF ⇒ xD ] + | x3 ⇒ match e2 with + [ x0 ⇒ x3 | x1 ⇒ x2 | x2 ⇒ x1 | x3 ⇒ x0 + | x4 ⇒ x7 | x5 ⇒ x6 | x6 ⇒ x5 | x7 ⇒ x4 + | x8 ⇒ xB | x9 ⇒ xA | xA ⇒ x9 | xB ⇒ x8 + | xC ⇒ xF | xD ⇒ xE | xE ⇒ xD | xF ⇒ xC ] + | x4 ⇒ match e2 with + [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 + | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3 + | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF + | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ] + | x5 ⇒ match e2 with + [ x0 ⇒ x5 | x1 ⇒ x4 | x2 ⇒ x7 | x3 ⇒ x6 + | x4 ⇒ x1 | x5 ⇒ x0 | x6 ⇒ x3 | x7 ⇒ x2 + | x8 ⇒ xD | x9 ⇒ xC | xA ⇒ xF | xB ⇒ xE + | xC ⇒ x9 | xD ⇒ x8 | xE ⇒ xB | xF ⇒ xA ] + | x6 ⇒ match e2 with + [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x4 | x3 ⇒ x5 + | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x0 | x7 ⇒ x1 + | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xC | xB ⇒ xD + | xC ⇒ xA | xD ⇒ xB | xE ⇒ x8 | xF ⇒ x9 ] + | x7 ⇒ match e2 with + [ x0 ⇒ x7 | x1 ⇒ x6 | x2 ⇒ x5 | x3 ⇒ x4 + | x4 ⇒ x3 | x5 ⇒ x2 | x6 ⇒ x1 | x7 ⇒ x0 + | x8 ⇒ xF | x9 ⇒ xE | xA ⇒ xD | xB ⇒ xC + | xC ⇒ xB | xD ⇒ xA | xE ⇒ x9 | xF ⇒ x8 ] + | x8 ⇒ match e2 with + [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB + | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF + | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 + | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ] + | x9 ⇒ match e2 with + [ x0 ⇒ x9 | x1 ⇒ x8 | x2 ⇒ xB | x3 ⇒ xA + | x4 ⇒ xD | x5 ⇒ xC | x6 ⇒ xF | x7 ⇒ xE + | x8 ⇒ x1 | x9 ⇒ x0 | xA ⇒ x3 | xB ⇒ x2 + | xC ⇒ x5 | xD ⇒ x4 | xE ⇒ x7 | xF ⇒ x6 ] + | xA ⇒ match e2 with + [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ x8 | x3 ⇒ x9 + | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xC | x7 ⇒ xD + | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x0 | xB ⇒ x1 + | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x4 | xF ⇒ x5 ] + | xB ⇒ match e2 with + [ x0 ⇒ xB | x1 ⇒ xA | x2 ⇒ x9 | x3 ⇒ x8 + | x4 ⇒ xF | x5 ⇒ xE | x6 ⇒ xD | x7 ⇒ xC + | x8 ⇒ x3 | x9 ⇒ x2 | xA ⇒ x1 | xB ⇒ x0 + | xC ⇒ x7 | xD ⇒ x6 | xE ⇒ x5 | xF ⇒ x4 ] + | xC ⇒ match e2 with + [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF + | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB + | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 + | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ] + | xD ⇒ match e2 with + [ x0 ⇒ xD | x1 ⇒ xC | x2 ⇒ xF | x3 ⇒ xE + | x4 ⇒ x9 | x5 ⇒ x8 | x6 ⇒ xB | x7 ⇒ xA + | x8 ⇒ x5 | x9 ⇒ x4 | xA ⇒ x7 | xB ⇒ x6 + | xC ⇒ x1 | xD ⇒ x0 | xE ⇒ x3 | xF ⇒ x2 ] + | xE ⇒ match e2 with + [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ xC | x3 ⇒ xD + | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ x8 | x7 ⇒ x9 + | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x4 | xB ⇒ x5 + | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x0 | xF ⇒ x1 ] + | xF ⇒ match e2 with + [ x0 ⇒ xF | x1 ⇒ xE | x2 ⇒ xD | x3 ⇒ xC + | x4 ⇒ xB | x5 ⇒ xA | x6 ⇒ x9 | x7 ⇒ x8 + | x8 ⇒ x7 | x9 ⇒ x6 | xA ⇒ x5 | xB ⇒ x4 + | xC ⇒ x3 | xD ⇒ x2 | xE ⇒ x1 | xF ⇒ x0 ] + ]. + +(* operatore rotazione destra con carry *) +ndefinition rcr_ex ≝ +λe:exadecim.λc:bool.match c with + [ true ⇒ match e with + [ x0 ⇒ pair exadecim bool x8 false | x1 ⇒ pair exadecim bool x8 true + | x2 ⇒ pair exadecim bool x9 false | x3 ⇒ pair exadecim bool x9 true + | x4 ⇒ pair exadecim bool xA false | x5 ⇒ pair exadecim bool xA true + | x6 ⇒ pair exadecim bool xB false | x7 ⇒ pair exadecim bool xB true + | x8 ⇒ pair exadecim bool xC false | x9 ⇒ pair exadecim bool xC true + | xA ⇒ pair exadecim bool xD false | xB ⇒ pair exadecim bool xD true + | xC ⇒ pair exadecim bool xE false | xD ⇒ pair exadecim bool xE true + | xE ⇒ pair exadecim bool xF false | xF ⇒ pair exadecim bool xF true ] + | false ⇒ match e with + [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x0 true + | x2 ⇒ pair exadecim bool x1 false | x3 ⇒ pair exadecim bool x1 true + | x4 ⇒ pair exadecim bool x2 false | x5 ⇒ pair exadecim bool x2 true + | x6 ⇒ pair exadecim bool x3 false | x7 ⇒ pair exadecim bool x3 true + | x8 ⇒ pair exadecim bool x4 false | x9 ⇒ pair exadecim bool x4 true + | xA ⇒ pair exadecim bool x5 false | xB ⇒ pair exadecim bool x5 true + | xC ⇒ pair exadecim bool x6 false | xD ⇒ pair exadecim bool x6 true + | xE ⇒ pair exadecim bool x7 false | xF ⇒ pair exadecim bool x7 true ] + ]. + +(* operatore shift destro *) +ndefinition shr_ex ≝ +λe:exadecim.match e with + [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x0 true + | x2 ⇒ pair exadecim bool x1 false | x3 ⇒ pair exadecim bool x1 true + | x4 ⇒ pair exadecim bool x2 false | x5 ⇒ pair exadecim bool x2 true + | x6 ⇒ pair exadecim bool x3 false | x7 ⇒ pair exadecim bool x3 true + | x8 ⇒ pair exadecim bool x4 false | x9 ⇒ pair exadecim bool x4 true + | xA ⇒ pair exadecim bool x5 false | xB ⇒ pair exadecim bool x5 true + | xC ⇒ pair exadecim bool x6 false | xD ⇒ pair exadecim bool x6 true + | xE ⇒ pair exadecim bool x7 false | xF ⇒ pair exadecim bool x7 true ]. + +(* operatore rotazione destra *) +ndefinition ror_ex ≝ +λe:exadecim.match e with + [ x0 ⇒ x0 | x1 ⇒ x8 | x2 ⇒ x1 | x3 ⇒ x9 + | x4 ⇒ x2 | x5 ⇒ xA | x6 ⇒ x3 | x7 ⇒ xB + | x8 ⇒ x4 | x9 ⇒ xC | xA ⇒ x5 | xB ⇒ xD + | xC ⇒ x6 | xD ⇒ xE | xE ⇒ x7 | xF ⇒ xF ]. + +(* operatore rotazione destra n-volte *) +nlet rec ror_ex_n (e:exadecim) (n:quatern) (r:rec_quatern n) on r ≝ + match r with + [ qu_O ⇒ e + | qu_S t n' ⇒ ror_ex_n (ror_ex e) t n' ]. + +(* operatore rotazione sinistra con carry *) +ndefinition rcl_ex ≝ +λe:exadecim.λc:bool.match c with + [ true ⇒ match e with + [ x0 ⇒ pair exadecim bool x1 false | x1 ⇒ pair exadecim bool x3 false + | x2 ⇒ pair exadecim bool x5 false | x3 ⇒ pair exadecim bool x7 false + | x4 ⇒ pair exadecim bool x9 false | x5 ⇒ pair exadecim bool xB false + | x6 ⇒ pair exadecim bool xD false | x7 ⇒ pair exadecim bool xF false + | x8 ⇒ pair exadecim bool x1 true | x9 ⇒ pair exadecim bool x3 true + | xA ⇒ pair exadecim bool x5 true | xB ⇒ pair exadecim bool x7 true + | xC ⇒ pair exadecim bool x9 true | xD ⇒ pair exadecim bool xB true + | xE ⇒ pair exadecim bool xD true | xF ⇒ pair exadecim bool xF true ] + | false ⇒ match e with + [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x2 false + | x2 ⇒ pair exadecim bool x4 false | x3 ⇒ pair exadecim bool x6 false + | x4 ⇒ pair exadecim bool x8 false | x5 ⇒ pair exadecim bool xA false + | x6 ⇒ pair exadecim bool xC false | x7 ⇒ pair exadecim bool xE false + | x8 ⇒ pair exadecim bool x0 true | x9 ⇒ pair exadecim bool x2 true + | xA ⇒ pair exadecim bool x4 true | xB ⇒ pair exadecim bool x6 true + | xC ⇒ pair exadecim bool x8 true | xD ⇒ pair exadecim bool xA true + | xE ⇒ pair exadecim bool xC true | xF ⇒ pair exadecim bool xE true ] + ]. + +(* operatore shift sinistro *) +ndefinition shl_ex ≝ +λe:exadecim.match e with + [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x2 false + | x2 ⇒ pair exadecim bool x4 false | x3 ⇒ pair exadecim bool x6 false + | x4 ⇒ pair exadecim bool x8 false | x5 ⇒ pair exadecim bool xA false + | x6 ⇒ pair exadecim bool xC false | x7 ⇒ pair exadecim bool xE false + | x8 ⇒ pair exadecim bool x0 true | x9 ⇒ pair exadecim bool x2 true + | xA ⇒ pair exadecim bool x4 true | xB ⇒ pair exadecim bool x6 true + | xC ⇒ pair exadecim bool x8 true | xD ⇒ pair exadecim bool xA true + | xE ⇒ pair exadecim bool xC true | xF ⇒ pair exadecim bool xE true ]. + +(* operatore rotazione sinistra *) +ndefinition rol_ex ≝ +λe:exadecim.match e with + [ x0 ⇒ x0 | x1 ⇒ x2 | x2 ⇒ x4 | x3 ⇒ x6 + | x4 ⇒ x8 | x5 ⇒ xA | x6 ⇒ xC | x7 ⇒ xE + | x8 ⇒ x1 | x9 ⇒ x3 | xA ⇒ x5 | xB ⇒ x7 + | xC ⇒ x9 | xD ⇒ xB | xE ⇒ xD | xF ⇒ xF ]. + +(* operatore rotazione sinistra n-volte *) +nlet rec rol_ex_n (e:exadecim) (n:quatern) (r:rec_quatern n) on r ≝ + match r with + [ qu_O ⇒ e + | qu_S t n' ⇒ rol_ex_n (rol_ex e) t n' ]. + +(* operatore not/complemento a 1 *) +ndefinition not_ex ≝ +λe:exadecim.match e with + [ x0 ⇒ xF | x1 ⇒ xE | x2 ⇒ xD | x3 ⇒ xC + | x4 ⇒ xB | x5 ⇒ xA | x6 ⇒ x9 | x7 ⇒ x8 + | x8 ⇒ x7 | x9 ⇒ x6 | xA ⇒ x5 | xB ⇒ x4 + | xC ⇒ x3 | xD ⇒ x2 | xE ⇒ x1 | xF ⇒ x0 ]. + +(* operatore somma con data+carry → data+carry *) +ndefinition plus_ex_dc_dc ≝ +λe1,e2:exadecim.λc:bool. + match c with + [ true ⇒ match e1 with + [ x0 ⇒ match e2 with + [ x0 ⇒ pair … x1 false | x1 ⇒ pair … x2 false | x2 ⇒ pair … x3 false | x3 ⇒ pair … x4 false + | x4 ⇒ pair … x5 false | x5 ⇒ pair … x6 false | x6 ⇒ pair … x7 false | x7 ⇒ pair … x8 false + | x8 ⇒ pair … x9 false | x9 ⇒ pair … xA false | xA ⇒ pair … xB false | xB ⇒ pair … xC false + | xC ⇒ pair … xD false | xD ⇒ pair … xE false | xE ⇒ pair … xF false | xF ⇒ pair … x0 true ] + | x1 ⇒ match e2 with + [ x0 ⇒ pair … x2 false | x1 ⇒ pair … x3 false | x2 ⇒ pair … x4 false | x3 ⇒ pair … x5 false + | x4 ⇒ pair … x6 false | x5 ⇒ pair … x7 false | x6 ⇒ pair … x8 false | x7 ⇒ pair … x9 false + | x8 ⇒ pair … xA false | x9 ⇒ pair … xB false | xA ⇒ pair … xC false | xB ⇒ pair … xD false + | xC ⇒ pair … xE false | xD ⇒ pair … xF false | xE ⇒ pair … x0 true | xF ⇒ pair … x1 true ] + | x2 ⇒ match e2 with + [ x0 ⇒ pair … x3 false | x1 ⇒ pair … x4 false | x2 ⇒ pair … x5 false | x3 ⇒ pair … x6 false + | x4 ⇒ pair … x7 false | x5 ⇒ pair … x8 false | x6 ⇒ pair … x9 false | x7 ⇒ pair … xA false + | x8 ⇒ pair … xB false | x9 ⇒ pair … xC false | xA ⇒ pair … xD false | xB ⇒ pair … xE false + | xC ⇒ pair … xF false | xD ⇒ pair … x0 true | xE ⇒ pair … x1 true | xF ⇒ pair … x2 true ] + | x3 ⇒ match e2 with + [ x0 ⇒ pair … x4 false | x1 ⇒ pair … x5 false | x2 ⇒ pair … x6 false | x3 ⇒ pair … x7 false + | x4 ⇒ pair … x8 false | x5 ⇒ pair … x9 false | x6 ⇒ pair … xA false | x7 ⇒ pair … xB false + | x8 ⇒ pair … xC false | x9 ⇒ pair … xD false | xA ⇒ pair … xE false | xB ⇒ pair … xF false + | xC ⇒ pair … x0 true | xD ⇒ pair … x1 true | xE ⇒ pair … x2 true | xF ⇒ pair … x3 true ] + | x4 ⇒ match e2 with + [ x0 ⇒ pair … x5 false | x1 ⇒ pair … x6 false | x2 ⇒ pair … x7 false | x3 ⇒ pair … x8 false + | x4 ⇒ pair … x9 false | x5 ⇒ pair … xA false | x6 ⇒ pair … xB false | x7 ⇒ pair … xC false + | x8 ⇒ pair … xD false | x9 ⇒ pair … xE false | xA ⇒ pair … xF false | xB ⇒ pair … x0 true + | xC ⇒ pair … x1 true | xD ⇒ pair … x2 true | xE ⇒ pair … x3 true | xF ⇒ pair … x4 true ] + | x5 ⇒ match e2 with + [ x0 ⇒ pair … x6 false | x1 ⇒ pair … x7 false | x2 ⇒ pair … x8 false | x3 ⇒ pair … x9 false + | x4 ⇒ pair … xA false | x5 ⇒ pair … xB false | x6 ⇒ pair … xC false | x7 ⇒ pair … xD false + | x8 ⇒ pair … xE false | x9 ⇒ pair … xF false | xA ⇒ pair … x0 true | xB ⇒ pair … x1 true + | xC ⇒ pair … x2 true | xD ⇒ pair … x3 true | xE ⇒ pair … x4 true | xF ⇒ pair … x5 true ] + | x6 ⇒ match e2 with + [ x0 ⇒ pair … x7 false | x1 ⇒ pair … x8 false | x2 ⇒ pair … x9 false | x3 ⇒ pair … xA false + | x4 ⇒ pair … xB false | x5 ⇒ pair … xC false | x6 ⇒ pair … xD false | x7 ⇒ pair … xE false + | x8 ⇒ pair … xF false | x9 ⇒ pair … x0 true | xA ⇒ pair … x1 true | xB ⇒ pair … x2 true + | xC ⇒ pair … x3 true | xD ⇒ pair … x4 true | xE ⇒ pair … x5 true | xF ⇒ pair … x6 true ] + | x7 ⇒ match e2 with + [ x0 ⇒ pair … x8 false | x1 ⇒ pair … x9 false | x2 ⇒ pair … xA false | x3 ⇒ pair … xB false + | x4 ⇒ pair … xC false | x5 ⇒ pair … xD false | x6 ⇒ pair … xE false | x7 ⇒ pair … xF false + | x8 ⇒ pair … x0 true | x9 ⇒ pair … x1 true | xA ⇒ pair … x2 true | xB ⇒ pair … x3 true + | xC ⇒ pair … x4 true | xD ⇒ pair … x5 true | xE ⇒ pair … x6 true | xF ⇒ pair … x7 true ] + | x8 ⇒ match e2 with + [ x0 ⇒ pair … x9 false | x1 ⇒ pair … xA false | x2 ⇒ pair … xB false | x3 ⇒ pair … xC false + | x4 ⇒ pair … xD false | x5 ⇒ pair … xE false | x6 ⇒ pair … xF false | x7 ⇒ pair … x0 true + | x8 ⇒ pair … x1 true | x9 ⇒ pair … x2 true | xA ⇒ pair … x3 true | xB ⇒ pair … x4 true + | xC ⇒ pair … x5 true | xD ⇒ pair … x6 true | xE ⇒ pair … x7 true | xF ⇒ pair … x8 true ] + | x9 ⇒ match e2 with + [ x0 ⇒ pair … xA false | x1 ⇒ pair … xB false | x2 ⇒ pair … xC false | x3 ⇒ pair … xD false + | x4 ⇒ pair … xE false | x5 ⇒ pair … xF false | x6 ⇒ pair … x0 true | x7 ⇒ pair … x1 true + | x8 ⇒ pair … x2 true | x9 ⇒ pair … x3 true | xA ⇒ pair … x4 true | xB ⇒ pair … x5 true + | xC ⇒ pair … x6 true | xD ⇒ pair … x7 true | xE ⇒ pair … x8 true | xF ⇒ pair … x9 true ] + | xA ⇒ match e2 with + [ x0 ⇒ pair … xB false | x1 ⇒ pair … xC false | x2 ⇒ pair … xD false | x3 ⇒ pair … xE false + | x4 ⇒ pair … xF false | x5 ⇒ pair … x0 true | x6 ⇒ pair … x1 true | x7 ⇒ pair … x2 true + | x8 ⇒ pair … x3 true | x9 ⇒ pair … x4 true | xA ⇒ pair … x5 true | xB ⇒ pair … x6 true + | xC ⇒ pair … x7 true | xD ⇒ pair … x8 true | xE ⇒ pair … x9 true | xF ⇒ pair … xA true ] + | xB ⇒ match e2 with + [ x0 ⇒ pair … xC false | x1 ⇒ pair … xD false | x2 ⇒ pair … xE false | x3 ⇒ pair … xF false + | x4 ⇒ pair … x0 true | x5 ⇒ pair … x1 true | x6 ⇒ pair … x2 true | x7 ⇒ pair … x3 true + | x8 ⇒ pair … x4 true | x9 ⇒ pair … x5 true | xA ⇒ pair … x6 true | xB ⇒ pair … x7 true + | xC ⇒ pair … x8 true | xD ⇒ pair … x9 true | xE ⇒ pair … xA true | xF ⇒ pair … xB true ] + | xC ⇒ match e2 with + [ x0 ⇒ pair … xD false | x1 ⇒ pair … xE false | x2 ⇒ pair … xF false | x3 ⇒ pair … x0 true + | x4 ⇒ pair … x1 true | x5 ⇒ pair … x2 true | x6 ⇒ pair … x3 true | x7 ⇒ pair … x4 true + | x8 ⇒ pair … x5 true | x9 ⇒ pair … x6 true | xA ⇒ pair … x7 true | xB ⇒ pair … x8 true + | xC ⇒ pair … x9 true | xD ⇒ pair … xA true | xE ⇒ pair … xB true | xF ⇒ pair … xC true ] + | xD ⇒ match e2 with + [ x0 ⇒ pair … xE false | x1 ⇒ pair … xF false | x2 ⇒ pair … x0 true | x3 ⇒ pair … x1 true + | x4 ⇒ pair … x2 true | x5 ⇒ pair … x3 true | x6 ⇒ pair … x4 true | x7 ⇒ pair … x5 true + | x8 ⇒ pair … x6 true | x9 ⇒ pair … x7 true | xA ⇒ pair … x8 true | xB ⇒ pair … x9 true + | xC ⇒ pair … xA true | xD ⇒ pair … xB true | xE ⇒ pair … xC true | xF ⇒ pair … xD true ] + | xE ⇒ match e2 with + [ x0 ⇒ pair … xF false | x1 ⇒ pair … x0 true | x2 ⇒ pair … x1 true | x3 ⇒ pair … x2 true + | x4 ⇒ pair … x3 true | x5 ⇒ pair … x4 true | x6 ⇒ pair … x5 true | x7 ⇒ pair … x6 true + | x8 ⇒ pair … x7 true | x9 ⇒ pair … x8 true | xA ⇒ pair … x9 true | xB ⇒ pair … xA true + | xC ⇒ pair … xB true | xD ⇒ pair … xC true | xE ⇒ pair … xD true | xF ⇒ pair … xE true ] + | xF ⇒ match e2 with + [ x0 ⇒ pair … x0 true | x1 ⇒ pair … x1 true | x2 ⇒ pair … x2 true | x3 ⇒ pair … x3 true + | x4 ⇒ pair … x4 true | x5 ⇒ pair … x5 true | x6 ⇒ pair … x6 true | x7 ⇒ pair … x7 true + | x8 ⇒ pair … x8 true | x9 ⇒ pair … x9 true | xA ⇒ pair … xA true | xB ⇒ pair … xB true + | xC ⇒ pair … xC true | xD ⇒ pair … xD true | xE ⇒ pair … xE true | xF ⇒ pair … xF true ] + ] + | false ⇒ match e1 with + [ x0 ⇒ match e2 with + [ x0 ⇒ pair … x0 false | x1 ⇒ pair … x1 false | x2 ⇒ pair … x2 false | x3 ⇒ pair … x3 false + | x4 ⇒ pair … x4 false | x5 ⇒ pair … x5 false | x6 ⇒ pair … x6 false | x7 ⇒ pair … x7 false + | x8 ⇒ pair … x8 false | x9 ⇒ pair … x9 false | xA ⇒ pair … xA false | xB ⇒ pair … xB false + | xC ⇒ pair … xC false | xD ⇒ pair … xD false | xE ⇒ pair … xE false | xF ⇒ pair … xF false ] + | x1 ⇒ match e2 with + [ x0 ⇒ pair … x1 false | x1 ⇒ pair … x2 false | x2 ⇒ pair … x3 false | x3 ⇒ pair … x4 false + | x4 ⇒ pair … x5 false | x5 ⇒ pair … x6 false | x6 ⇒ pair … x7 false | x7 ⇒ pair … x8 false + | x8 ⇒ pair … x9 false | x9 ⇒ pair … xA false | xA ⇒ pair … xB false | xB ⇒ pair … xC false + | xC ⇒ pair … xD false | xD ⇒ pair … xE false | xE ⇒ pair … xF false | xF ⇒ pair … x0 true ] + | x2 ⇒ match e2 with + [ x0 ⇒ pair … x2 false | x1 ⇒ pair … x3 false | x2 ⇒ pair … x4 false | x3 ⇒ pair … x5 false + | x4 ⇒ pair … x6 false | x5 ⇒ pair … x7 false | x6 ⇒ pair … x8 false | x7 ⇒ pair … x9 false + | x8 ⇒ pair … xA false | x9 ⇒ pair … xB false | xA ⇒ pair … xC false | xB ⇒ pair … xD false + | xC ⇒ pair … xE false | xD ⇒ pair … xF false | xE ⇒ pair … x0 true | xF ⇒ pair … x1 true ] + | x3 ⇒ match e2 with + [ x0 ⇒ pair … x3 false | x1 ⇒ pair … x4 false | x2 ⇒ pair … x5 false | x3 ⇒ pair … x6 false + | x4 ⇒ pair … x7 false | x5 ⇒ pair … x8 false | x6 ⇒ pair … x9 false | x7 ⇒ pair … xA false + | x8 ⇒ pair … xB false | x9 ⇒ pair … xC false | xA ⇒ pair … xD false | xB ⇒ pair … xE false + | xC ⇒ pair … xF false | xD ⇒ pair … x0 true | xE ⇒ pair … x1 true | xF ⇒ pair … x2 true ] + | x4 ⇒ match e2 with + [ x0 ⇒ pair … x4 false | x1 ⇒ pair … x5 false | x2 ⇒ pair … x6 false | x3 ⇒ pair … x7 false + | x4 ⇒ pair … x8 false | x5 ⇒ pair … x9 false | x6 ⇒ pair … xA false | x7 ⇒ pair … xB false + | x8 ⇒ pair … xC false | x9 ⇒ pair … xD false | xA ⇒ pair … xE false | xB ⇒ pair … xF false + | xC ⇒ pair … x0 true | xD ⇒ pair … x1 true | xE ⇒ pair … x2 true | xF ⇒ pair … x3 true ] + | x5 ⇒ match e2 with + [ x0 ⇒ pair … x5 false | x1 ⇒ pair … x6 false | x2 ⇒ pair … x7 false | x3 ⇒ pair … x8 false + | x4 ⇒ pair … x9 false | x5 ⇒ pair … xA false | x6 ⇒ pair … xB false | x7 ⇒ pair … xC false + | x8 ⇒ pair … xD false | x9 ⇒ pair … xE false | xA ⇒ pair … xF false | xB ⇒ pair … x0 true + | xC ⇒ pair … x1 true | xD ⇒ pair … x2 true | xE ⇒ pair … x3 true | xF ⇒ pair … x4 true ] + | x6 ⇒ match e2 with + [ x0 ⇒ pair … x6 false | x1 ⇒ pair … x7 false | x2 ⇒ pair … x8 false | x3 ⇒ pair … x9 false + | x4 ⇒ pair … xA false | x5 ⇒ pair … xB false | x6 ⇒ pair … xC false | x7 ⇒ pair … xD false + | x8 ⇒ pair … xE false | x9 ⇒ pair … xF false | xA ⇒ pair … x0 true | xB ⇒ pair … x1 true + | xC ⇒ pair … x2 true | xD ⇒ pair … x3 true | xE ⇒ pair … x4 true | xF ⇒ pair … x5 true ] + | x7 ⇒ match e2 with + [ x0 ⇒ pair … x7 false | x1 ⇒ pair … x8 false | x2 ⇒ pair … x9 false | x3 ⇒ pair … xA false + | x4 ⇒ pair … xB false | x5 ⇒ pair … xC false | x6 ⇒ pair … xD false | x7 ⇒ pair … xE false + | x8 ⇒ pair … xF false | x9 ⇒ pair … x0 true | xA ⇒ pair … x1 true | xB ⇒ pair … x2 true + | xC ⇒ pair … x3 true | xD ⇒ pair … x4 true | xE ⇒ pair … x5 true | xF ⇒ pair … x6 true ] + | x8 ⇒ match e2 with + [ x0 ⇒ pair … x8 false | x1 ⇒ pair … x9 false | x2 ⇒ pair … xA false | x3 ⇒ pair … xB false + | x4 ⇒ pair … xC false | x5 ⇒ pair … xD false | x6 ⇒ pair … xE false | x7 ⇒ pair … xF false + | x8 ⇒ pair … x0 true | x9 ⇒ pair … x1 true | xA ⇒ pair … x2 true | xB ⇒ pair … x3 true + | xC ⇒ pair … x4 true | xD ⇒ pair … x5 true | xE ⇒ pair … x6 true | xF ⇒ pair … x7 true ] + | x9 ⇒ match e2 with + [ x0 ⇒ pair … x9 false | x1 ⇒ pair … xA false | x2 ⇒ pair … xB false | x3 ⇒ pair … xC false + | x4 ⇒ pair … xD false | x5 ⇒ pair … xE false | x6 ⇒ pair … xF false | x7 ⇒ pair … x0 true + | x8 ⇒ pair … x1 true | x9 ⇒ pair … x2 true | xA ⇒ pair … x3 true | xB ⇒ pair … x4 true + | xC ⇒ pair … x5 true | xD ⇒ pair … x6 true | xE ⇒ pair … x7 true | xF ⇒ pair … x8 true ] + | xA ⇒ match e2 with + [ x0 ⇒ pair … xA false | x1 ⇒ pair … xB false | x2 ⇒ pair … xC false | x3 ⇒ pair … xD false + | x4 ⇒ pair … xE false | x5 ⇒ pair … xF false | x6 ⇒ pair … x0 true | x7 ⇒ pair … x1 true + | x8 ⇒ pair … x2 true | x9 ⇒ pair … x3 true | xA ⇒ pair … x4 true | xB ⇒ pair … x5 true + | xC ⇒ pair … x6 true | xD ⇒ pair … x7 true | xE ⇒ pair … x8 true | xF ⇒ pair … x9 true ] + | xB ⇒ match e2 with + [ x0 ⇒ pair … xB false | x1 ⇒ pair … xC false | x2 ⇒ pair … xD false | x3 ⇒ pair … xE false + | x4 ⇒ pair … xF false | x5 ⇒ pair … x0 true | x6 ⇒ pair … x1 true | x7 ⇒ pair … x2 true + | x8 ⇒ pair … x3 true | x9 ⇒ pair … x4 true | xA ⇒ pair … x5 true | xB ⇒ pair … x6 true + | xC ⇒ pair … x7 true | xD ⇒ pair … x8 true | xE ⇒ pair … x9 true | xF ⇒ pair … xA true ] + | xC ⇒ match e2 with + [ x0 ⇒ pair … xC false | x1 ⇒ pair … xD false | x2 ⇒ pair … xE false | x3 ⇒ pair … xF false + | x4 ⇒ pair … x0 true | x5 ⇒ pair … x1 true | x6 ⇒ pair … x2 true | x7 ⇒ pair … x3 true + | x8 ⇒ pair … x4 true | x9 ⇒ pair … x5 true | xA ⇒ pair … x6 true | xB ⇒ pair … x7 true + | xC ⇒ pair … x8 true | xD ⇒ pair … x9 true | xE ⇒ pair … xA true | xF ⇒ pair … xB true ] + | xD ⇒ match e2 with + [ x0 ⇒ pair … xD false | x1 ⇒ pair … xE false | x2 ⇒ pair … xF false | x3 ⇒ pair … x0 true + | x4 ⇒ pair … x1 true | x5 ⇒ pair … x2 true | x6 ⇒ pair … x3 true | x7 ⇒ pair … x4 true + | x8 ⇒ pair … x5 true | x9 ⇒ pair … x6 true | xA ⇒ pair … x7 true | xB ⇒ pair … x8 true + | xC ⇒ pair … x9 true | xD ⇒ pair … xA true | xE ⇒ pair … xB true | xF ⇒ pair … xC true ] + | xE ⇒ match e2 with + [ x0 ⇒ pair … xE false | x1 ⇒ pair … xF false | x2 ⇒ pair … x0 true | x3 ⇒ pair … x1 true + | x4 ⇒ pair … x2 true | x5 ⇒ pair … x3 true | x6 ⇒ pair … x4 true | x7 ⇒ pair … x5 true + | x8 ⇒ pair … x6 true | x9 ⇒ pair … x7 true | xA ⇒ pair … x8 true | xB ⇒ pair … x9 true + | xC ⇒ pair … xA true | xD ⇒ pair … xB true | xE ⇒ pair … xC true | xF ⇒ pair … xD true ] + | xF ⇒ match e2 with + [ x0 ⇒ pair … xF false | x1 ⇒ pair … x0 true | x2 ⇒ pair … x1 true | x3 ⇒ pair … x2 true + | x4 ⇒ pair … x3 true | x5 ⇒ pair … x4 true | x6 ⇒ pair … x5 true | x7 ⇒ pair … x6 true + | x8 ⇒ pair … x7 true | x9 ⇒ pair … x8 true | xA ⇒ pair … x9 true | xB ⇒ pair … xA true + | xC ⇒ pair … xB true | xD ⇒ pair … xC true | xE ⇒ pair … xD true | xF ⇒ pair … xE true ] + ]]. + +(* operatore somma con data → data+carry *) +ndefinition plus_ex_d_dc ≝ +λe1,e2:exadecim. + match e1 with + [ x0 ⇒ match e2 with + [ x0 ⇒ pair … x0 false | x1 ⇒ pair … x1 false | x2 ⇒ pair … x2 false | x3 ⇒ pair … x3 false + | x4 ⇒ pair … x4 false | x5 ⇒ pair … x5 false | x6 ⇒ pair … x6 false | x7 ⇒ pair … x7 false + | x8 ⇒ pair … x8 false | x9 ⇒ pair … x9 false | xA ⇒ pair … xA false | xB ⇒ pair … xB false + | xC ⇒ pair … xC false | xD ⇒ pair … xD false | xE ⇒ pair … xE false | xF ⇒ pair … xF false ] + | x1 ⇒ match e2 with + [ x0 ⇒ pair … x1 false | x1 ⇒ pair … x2 false | x2 ⇒ pair … x3 false | x3 ⇒ pair … x4 false + | x4 ⇒ pair … x5 false | x5 ⇒ pair … x6 false | x6 ⇒ pair … x7 false | x7 ⇒ pair … x8 false + | x8 ⇒ pair … x9 false | x9 ⇒ pair … xA false | xA ⇒ pair … xB false | xB ⇒ pair … xC false + | xC ⇒ pair … xD false | xD ⇒ pair … xE false | xE ⇒ pair … xF false | xF ⇒ pair … x0 true ] + | x2 ⇒ match e2 with + [ x0 ⇒ pair … x2 false | x1 ⇒ pair … x3 false | x2 ⇒ pair … x4 false | x3 ⇒ pair … x5 false + | x4 ⇒ pair … x6 false | x5 ⇒ pair … x7 false | x6 ⇒ pair … x8 false | x7 ⇒ pair … x9 false + | x8 ⇒ pair … xA false | x9 ⇒ pair … xB false | xA ⇒ pair … xC false | xB ⇒ pair … xD false + | xC ⇒ pair … xE false | xD ⇒ pair … xF false | xE ⇒ pair … x0 true | xF ⇒ pair … x1 true ] + | x3 ⇒ match e2 with + [ x0 ⇒ pair … x3 false | x1 ⇒ pair … x4 false | x2 ⇒ pair … x5 false | x3 ⇒ pair … x6 false + | x4 ⇒ pair … x7 false | x5 ⇒ pair … x8 false | x6 ⇒ pair … x9 false | x7 ⇒ pair … xA false + | x8 ⇒ pair … xB false | x9 ⇒ pair … xC false | xA ⇒ pair … xD false | xB ⇒ pair … xE false + | xC ⇒ pair … xF false | xD ⇒ pair … x0 true | xE ⇒ pair … x1 true | xF ⇒ pair … x2 true ] + | x4 ⇒ match e2 with + [ x0 ⇒ pair … x4 false | x1 ⇒ pair … x5 false | x2 ⇒ pair … x6 false | x3 ⇒ pair … x7 false + | x4 ⇒ pair … x8 false | x5 ⇒ pair … x9 false | x6 ⇒ pair … xA false | x7 ⇒ pair … xB false + | x8 ⇒ pair … xC false | x9 ⇒ pair … xD false | xA ⇒ pair … xE false | xB ⇒ pair … xF false + | xC ⇒ pair … x0 true | xD ⇒ pair … x1 true | xE ⇒ pair … x2 true | xF ⇒ pair … x3 true ] + | x5 ⇒ match e2 with + [ x0 ⇒ pair … x5 false | x1 ⇒ pair … x6 false | x2 ⇒ pair … x7 false | x3 ⇒ pair … x8 false + | x4 ⇒ pair … x9 false | x5 ⇒ pair … xA false | x6 ⇒ pair … xB false | x7 ⇒ pair … xC false + | x8 ⇒ pair … xD false | x9 ⇒ pair … xE false | xA ⇒ pair … xF false | xB ⇒ pair … x0 true + | xC ⇒ pair … x1 true | xD ⇒ pair … x2 true | xE ⇒ pair … x3 true | xF ⇒ pair … x4 true ] + | x6 ⇒ match e2 with + [ x0 ⇒ pair … x6 false | x1 ⇒ pair … x7 false | x2 ⇒ pair … x8 false | x3 ⇒ pair … x9 false + | x4 ⇒ pair … xA false | x5 ⇒ pair … xB false | x6 ⇒ pair … xC false | x7 ⇒ pair … xD false + | x8 ⇒ pair … xE false | x9 ⇒ pair … xF false | xA ⇒ pair … x0 true | xB ⇒ pair … x1 true + | xC ⇒ pair … x2 true | xD ⇒ pair … x3 true | xE ⇒ pair … x4 true | xF ⇒ pair … x5 true ] + | x7 ⇒ match e2 with + [ x0 ⇒ pair … x7 false | x1 ⇒ pair … x8 false | x2 ⇒ pair … x9 false | x3 ⇒ pair … xA false + | x4 ⇒ pair … xB false | x5 ⇒ pair … xC false | x6 ⇒ pair … xD false | x7 ⇒ pair … xE false + | x8 ⇒ pair … xF false | x9 ⇒ pair … x0 true | xA ⇒ pair … x1 true | xB ⇒ pair … x2 true + | xC ⇒ pair … x3 true | xD ⇒ pair … x4 true | xE ⇒ pair … x5 true | xF ⇒ pair … x6 true ] + | x8 ⇒ match e2 with + [ x0 ⇒ pair … x8 false | x1 ⇒ pair … x9 false | x2 ⇒ pair … xA false | x3 ⇒ pair … xB false + | x4 ⇒ pair … xC false | x5 ⇒ pair … xD false | x6 ⇒ pair … xE false | x7 ⇒ pair … xF false + | x8 ⇒ pair … x0 true | x9 ⇒ pair … x1 true | xA ⇒ pair … x2 true | xB ⇒ pair … x3 true + | xC ⇒ pair … x4 true | xD ⇒ pair … x5 true | xE ⇒ pair … x6 true | xF ⇒ pair … x7 true ] + | x9 ⇒ match e2 with + [ x0 ⇒ pair … x9 false | x1 ⇒ pair … xA false | x2 ⇒ pair … xB false | x3 ⇒ pair … xC false + | x4 ⇒ pair … xD false | x5 ⇒ pair … xE false | x6 ⇒ pair … xF false | x7 ⇒ pair … x0 true + | x8 ⇒ pair … x1 true | x9 ⇒ pair … x2 true | xA ⇒ pair … x3 true | xB ⇒ pair … x4 true + | xC ⇒ pair … x5 true | xD ⇒ pair … x6 true | xE ⇒ pair … x7 true | xF ⇒ pair … x8 true ] + | xA ⇒ match e2 with + [ x0 ⇒ pair … xA false | x1 ⇒ pair … xB false | x2 ⇒ pair … xC false | x3 ⇒ pair … xD false + | x4 ⇒ pair … xE false | x5 ⇒ pair … xF false | x6 ⇒ pair … x0 true | x7 ⇒ pair … x1 true + | x8 ⇒ pair … x2 true | x9 ⇒ pair … x3 true | xA ⇒ pair … x4 true | xB ⇒ pair … x5 true + | xC ⇒ pair … x6 true | xD ⇒ pair … x7 true | xE ⇒ pair … x8 true | xF ⇒ pair … x9 true ] + | xB ⇒ match e2 with + [ x0 ⇒ pair … xB false | x1 ⇒ pair … xC false | x2 ⇒ pair … xD false | x3 ⇒ pair … xE false + | x4 ⇒ pair … xF false | x5 ⇒ pair … x0 true | x6 ⇒ pair … x1 true | x7 ⇒ pair … x2 true + | x8 ⇒ pair … x3 true | x9 ⇒ pair … x4 true | xA ⇒ pair … x5 true | xB ⇒ pair … x6 true + | xC ⇒ pair … x7 true | xD ⇒ pair … x8 true | xE ⇒ pair … x9 true | xF ⇒ pair … xA true ] + | xC ⇒ match e2 with + [ x0 ⇒ pair … xC false | x1 ⇒ pair … xD false | x2 ⇒ pair … xE false | x3 ⇒ pair … xF false + | x4 ⇒ pair … x0 true | x5 ⇒ pair … x1 true | x6 ⇒ pair … x2 true | x7 ⇒ pair … x3 true + | x8 ⇒ pair … x4 true | x9 ⇒ pair … x5 true | xA ⇒ pair … x6 true | xB ⇒ pair … x7 true + | xC ⇒ pair … x8 true | xD ⇒ pair … x9 true | xE ⇒ pair … xA true | xF ⇒ pair … xB true ] + | xD ⇒ match e2 with + [ x0 ⇒ pair … xD false | x1 ⇒ pair … xE false | x2 ⇒ pair … xF false | x3 ⇒ pair … x0 true + | x4 ⇒ pair … x1 true | x5 ⇒ pair … x2 true | x6 ⇒ pair … x3 true | x7 ⇒ pair … x4 true + | x8 ⇒ pair … x5 true | x9 ⇒ pair … x6 true | xA ⇒ pair … x7 true | xB ⇒ pair … x8 true + | xC ⇒ pair … x9 true | xD ⇒ pair … xA true | xE ⇒ pair … xB true | xF ⇒ pair … xC true ] + | xE ⇒ match e2 with + [ x0 ⇒ pair … xE false | x1 ⇒ pair … xF false | x2 ⇒ pair … x0 true | x3 ⇒ pair … x1 true + | x4 ⇒ pair … x2 true | x5 ⇒ pair … x3 true | x6 ⇒ pair … x4 true | x7 ⇒ pair … x5 true + | x8 ⇒ pair … x6 true | x9 ⇒ pair … x7 true | xA ⇒ pair … x8 true | xB ⇒ pair … x9 true + | xC ⇒ pair … xA true | xD ⇒ pair … xB true | xE ⇒ pair … xC true | xF ⇒ pair … xD true ] + | xF ⇒ match e2 with + [ x0 ⇒ pair … xF false | x1 ⇒ pair … x0 true | x2 ⇒ pair … x1 true | x3 ⇒ pair … x2 true + | x4 ⇒ pair … x3 true | x5 ⇒ pair … x4 true | x6 ⇒ pair … x5 true | x7 ⇒ pair … x6 true + | x8 ⇒ pair … x7 true | x9 ⇒ pair … x8 true | xA ⇒ pair … x9 true | xB ⇒ pair … xA true + | xC ⇒ pair … xB true | xD ⇒ pair … xC true | xE ⇒ pair … xD true | xF ⇒ pair … xE true ] + ]. + +(* operatore somma con data+carry → data *) +ndefinition plus_ex_dc_d ≝ +λe1,e2:exadecim.λc:bool. + match c with + [ true ⇒ match e1 with + [ x0 ⇒ match e2 with + [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8 + | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ] + | x1 ⇒ match e2 with + [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x4 | x3 ⇒ x5 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x8 | x7 ⇒ x9 + | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xC | xB ⇒ xD | xC ⇒ xE | xD ⇒ xF | xE ⇒ x0 | xF ⇒ x1 ] + | x2 ⇒ match e2 with + [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA + | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ] + | x3 ⇒ match e2 with + [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB + | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ] + | x4 ⇒ match e2 with + [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC + | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ] + | x5 ⇒ match e2 with + [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD + | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ] + | x6 ⇒ match e2 with + [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE + | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ] + | x7 ⇒ match e2 with + [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF + | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ] + | x8 ⇒ match e2 with + [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0 + | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ] + | x9 ⇒ match e2 with + [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1 + | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ] + | xA ⇒ match e2 with + [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2 + | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ] + | xB ⇒ match e2 with + [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3 + | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ] + | xC ⇒ match e2 with + [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4 + | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ] + | xD ⇒ match e2 with + [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5 + | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ] + | xE ⇒ match e2 with + [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6 + | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ] + | xF ⇒ match e2 with + [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7 + | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ] + ] + | false ⇒ match e1 with + [ x0 ⇒ match e2 with + [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7 + | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ] + | x1 ⇒ match e2 with + [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8 + | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ] + | x2 ⇒ match e2 with + [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x4 | x3 ⇒ x5 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x8 | x7 ⇒ x9 + | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xC | xB ⇒ xD | xC ⇒ xE | xD ⇒ xF | xE ⇒ x0 | xF ⇒ x1 ] + | x3 ⇒ match e2 with + [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA + | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ] + | x4 ⇒ match e2 with + [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB + | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ] + | x5 ⇒ match e2 with + [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC + | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ] + | x6 ⇒ match e2 with + [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD + | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ] + | x7 ⇒ match e2 with + [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE + | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ] + | x8 ⇒ match e2 with + [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF + | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ] + | x9 ⇒ match e2 with + [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0 + | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ] + | xA ⇒ match e2 with + [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1 + | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ] + | xB ⇒ match e2 with + [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2 + | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ] + | xC ⇒ match e2 with + [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3 + | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ] + | xD ⇒ match e2 with + [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4 + | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ] + | xE ⇒ match e2 with + [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5 + | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ] + | xF ⇒ match e2 with + [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6 + | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ] + ]]. + +(* operatore somma con data → data *) +ndefinition plus_ex_d_d ≝ +λe1,e2:exadecim. + match e1 with + [ x0 ⇒ match e2 with + [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7 + | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ] + | x1 ⇒ match e2 with + [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8 + | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ] + | x2 ⇒ match e2 with + [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x4 | x3 ⇒ x5 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x8 | x7 ⇒ x9 + | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xC | xB ⇒ xD | xC ⇒ xE | xD ⇒ xF | xE ⇒ x0 | xF ⇒ x1 ] + | x3 ⇒ match e2 with + [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA + | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ] + | x4 ⇒ match e2 with + [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB + | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ] + | x5 ⇒ match e2 with + [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC + | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ] + | x6 ⇒ match e2 with + [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD + | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ] + | x7 ⇒ match e2 with + [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE + | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ] + | x8 ⇒ match e2 with + [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF + | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ] + | x9 ⇒ match e2 with + [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0 + | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ] + | xA ⇒ match e2 with + [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1 + | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ] + | xB ⇒ match e2 with + [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2 + | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ] + | xC ⇒ match e2 with + [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3 + | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ] + | xD ⇒ match e2 with + [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4 + | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ] + | xE ⇒ match e2 with + [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5 + | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ] + | xF ⇒ match e2 with + [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6 + | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ] + ]. + +(* operatore somma con data+carry → carry *) +ndefinition plus_ex_dc_c ≝ +λe1,e2:exadecim.λc:bool. + match c with + [ true ⇒ match e1 with + [ x0 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ] + | x1 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ] + | x2 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x3 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x4 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x5 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x6 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x7 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x8 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x9 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | xA ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | xB ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | xC ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | xD ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | xE ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | xF ⇒ match e2 with + [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + ] + | false ⇒ match e1 with + [ x0 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | x1 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ] + | x2 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ] + | x3 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x4 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x5 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x6 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x7 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x8 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x9 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | xA ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | xB ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | xC ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | xD ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | xE ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | xF ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + ]]. + +(* operatore somma con data → carry *) +ndefinition plus_ex_d_c ≝ +λe1,e2:exadecim. + match e1 with + [ x0 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | x1 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ] + | x2 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ] + | x3 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x4 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x5 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x6 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x7 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x8 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | x9 ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | xA ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | xB ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | xC ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | xD ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | xE ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + | xF ⇒ match e2 with + [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] + ]. + +(* operatore Most Significant Bit *) +ndefinition MSB_ex ≝ +λe:exadecim.match e with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true + | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]. + +(* operatore predecessore *) +ndefinition pred_ex ≝ +λe:exadecim. + match e with + [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6 + | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ]. + +(* operatore successore *) +ndefinition succ_ex ≝ +λe:exadecim. + match e with + [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8 + | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ]. + +(* operatore neg/complemento a 2 *) +ndefinition compl_ex ≝ +λe:exadecim.match e with + [ x0 ⇒ x0 | x1 ⇒ xF | x2 ⇒ xE | x3 ⇒ xD + | x4 ⇒ xC | x5 ⇒ xB | x6 ⇒ xA | x7 ⇒ x9 + | x8 ⇒ x8 | x9 ⇒ x7 | xA ⇒ x6 | xB ⇒ x5 + | xC ⇒ x4 | xD ⇒ x3 | xE ⇒ x2 | xF ⇒ x1 ]. + +(* iteratore sugli esadecimali *) +ndefinition forall_ex ≝ λP. + P x0 ⊗ P x1 ⊗ P x2 ⊗ P x3 ⊗ P x4 ⊗ P x5 ⊗ P x6 ⊗ P x7 ⊗ + P x8 ⊗ P x9 ⊗ P xA ⊗ P xB ⊗ P xC ⊗ P xD ⊗ P xE ⊗ P xF. + +(* esadecimali ricorsivi *) +ninductive rec_exadecim : exadecim → Type ≝ + ex_O : rec_exadecim x0 +| ex_S : ∀n.rec_exadecim n → rec_exadecim (succ_ex n). + +(* esadecimali → esadecimali ricorsivi *) +ndefinition ex_to_recex ≝ +λn.match n return λx.rec_exadecim x with + [ x0 ⇒ ex_O + | x1 ⇒ ex_S ? ex_O + | x2 ⇒ ex_S ? (ex_S ? ex_O) + | x3 ⇒ ex_S ? (ex_S ? (ex_S ? ex_O)) + | x4 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))) + | x5 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))) + | x6 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))) + | x7 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))) + | x8 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))) + | x9 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))) + | xA ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))))) + | xB ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))))) + | xC ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))))))) + | xD ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))))))) + | xE ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))))))))) + | xF ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))))))))) + ]. + +(* quaternari → esadecimali *) +ndefinition ex_of_qu ≝ +λn.match n with + [ q0 ⇒ x0 | q1 ⇒ x1 | q2 ⇒ x2 | q3 ⇒ x3 ]. + +(* ottali → esadecimali *) +ndefinition ex_of_oct ≝ +λn.match n with + [ o0 ⇒ x0 | o1 ⇒ x1 | o2 ⇒ x2 | o3 ⇒ x3 | o4 ⇒ x4 | o5 ⇒ x5 | o6 ⇒ x6 | o7 ⇒ x7 ]. diff --git a/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma new file mode 100755 index 000000000..a556b2d9e --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma @@ -0,0 +1,483 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* ********************************************************************** *) + +include "num/exadecim.ma". +include "num/bool_lemmas.ma". + +(* *********** *) +(* ESADECIMALI *) +(* *********** *) + +ndefinition exadecim_destruct1 : Πe2.ΠP:Prop.ΠH:x0 = e2.match e2 with [ x0 ⇒ P → P | _ ⇒ P ]. + #e2; #P; ncases e2; nnormalize; #H; + ##[ ##1: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match x0 with [ x0 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition exadecim_destruct2 : Πe2.ΠP:Prop.ΠH:x1 = e2.match e2 with [ x1 ⇒ P → P | _ ⇒ P ]. + #e2; #P; ncases e2; nnormalize; #H; + ##[ ##2: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match x1 with [ x1 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition exadecim_destruct3 : Πe2.ΠP:Prop.ΠH:x2 = e2.match e2 with [ x2 ⇒ P → P | _ ⇒ P ]. + #e2; #P; ncases e2; nnormalize; #H; + ##[ ##3: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match x2 with [ x2 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition exadecim_destruct4 : Πe2.ΠP:Prop.ΠH:x3 = e2.match e2 with [ x3 ⇒ P → P | _ ⇒ P ]. + #e2; #P; ncases e2; nnormalize; #H; + ##[ ##4: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match x3 with [ x3 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition exadecim_destruct5 : Πe2.ΠP:Prop.ΠH:x4 = e2.match e2 with [ x4 ⇒ P → P | _ ⇒ P ]. + #e2; #P; ncases e2; nnormalize; #H; + ##[ ##5: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match x4 with [ x4 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition exadecim_destruct6 : Πe2.ΠP:Prop.ΠH:x5 = e2.match e2 with [ x5 ⇒ P → P | _ ⇒ P ]. + #e2; #P; ncases e2; nnormalize; #H; + ##[ ##6: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match x5 with [ x5 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition exadecim_destruct7 : Πe2.ΠP:Prop.ΠH:x6 = e2.match e2 with [ x6 ⇒ P → P | _ ⇒ P ]. + #e2; #P; ncases e2; nnormalize; #H; + ##[ ##7: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match x6 with [ x6 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition exadecim_destruct8 : Πe2.ΠP:Prop.ΠH:x7 = e2.match e2 with [ x7 ⇒ P → P | _ ⇒ P ]. + #e2; #P; ncases e2; nnormalize; #H; + ##[ ##8: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match x7 with [ x7 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition exadecim_destruct9 : Πe2.ΠP:Prop.ΠH:x8 = e2.match e2 with [ x8 ⇒ P → P | _ ⇒ P ]. + #e2; #P; ncases e2; nnormalize; #H; + ##[ ##9: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match x8 with [ x8 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition exadecim_destruct10 : Πe2.ΠP:Prop.ΠH:x9 = e2.match e2 with [ x9 ⇒ P → P | _ ⇒ P ]. + #e2; #P; ncases e2; nnormalize; #H; + ##[ ##10: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match x9 with [ x9 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition exadecim_destruct11 : Πe2.ΠP:Prop.ΠH:xA = e2.match e2 with [ xA ⇒ P → P | _ ⇒ P ]. + #e2; #P; ncases e2; nnormalize; #H; + ##[ ##11: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match xA with [ xA ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition exadecim_destruct12 : Πe2.ΠP:Prop.ΠH:xB = e2.match e2 with [ xB ⇒ P → P | _ ⇒ P ]. + #e2; #P; ncases e2; nnormalize; #H; + ##[ ##12: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match xB with [ xB ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition exadecim_destruct13 : Πe2.ΠP:Prop.ΠH:xC = e2.match e2 with [ xC ⇒ P → P | _ ⇒ P ]. + #e2; #P; ncases e2; nnormalize; #H; + ##[ ##13: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match xC with [ xC ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition exadecim_destruct14 : Πe2.ΠP:Prop.ΠH:xD = e2.match e2 with [ xD ⇒ P → P | _ ⇒ P ]. + #e2; #P; ncases e2; nnormalize; #H; + ##[ ##14: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match xD with [ xD ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition exadecim_destruct15 : Πe2.ΠP:Prop.ΠH:xE = e2.match e2 with [ xE ⇒ P → P | _ ⇒ P ]. + #e2; #P; ncases e2; nnormalize; #H; + ##[ ##15: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match xE with [ xE ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition exadecim_destruct16 : Πe2.ΠP:Prop.ΠH:xF = e2.match e2 with [ xF ⇒ P → P | _ ⇒ P ]. + #e2; #P; ncases e2; nnormalize; #H; + ##[ ##16: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match xF with [ xF ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition exadecim_destruct_aux ≝ +Πe1,e2.ΠP:Prop.ΠH:e1 = e2. + match e1 with + [ x0 ⇒ match e2 with [ x0 ⇒ P → P | _ ⇒ P ] + | x1 ⇒ match e2 with [ x1 ⇒ P → P | _ ⇒ P ] + | x2 ⇒ match e2 with [ x2 ⇒ P → P | _ ⇒ P ] + | x3 ⇒ match e2 with [ x3 ⇒ P → P | _ ⇒ P ] + | x4 ⇒ match e2 with [ x4 ⇒ P → P | _ ⇒ P ] + | x5 ⇒ match e2 with [ x5 ⇒ P → P | _ ⇒ P ] + | x6 ⇒ match e2 with [ x6 ⇒ P → P | _ ⇒ P ] + | x7 ⇒ match e2 with [ x7 ⇒ P → P | _ ⇒ P ] + | x8 ⇒ match e2 with [ x8 ⇒ P → P | _ ⇒ P ] + | x9 ⇒ match e2 with [ x9 ⇒ P → P | _ ⇒ P ] + | xA ⇒ match e2 with [ xA ⇒ P → P | _ ⇒ P ] + | xB ⇒ match e2 with [ xB ⇒ P → P | _ ⇒ P ] + | xC ⇒ match e2 with [ xC ⇒ P → P | _ ⇒ P ] + | xD ⇒ match e2 with [ xD ⇒ P → P | _ ⇒ P ] + | xE ⇒ match e2 with [ xE ⇒ P → P | _ ⇒ P ] + | xF ⇒ match e2 with [ xF ⇒ P → P | _ ⇒ P ] + ]. + +ndefinition exadecim_destruct : exadecim_destruct_aux. + #e1; ncases e1; + ##[ ##1: napply exadecim_destruct1 + ##| ##2: napply exadecim_destruct2 + ##| ##3: napply exadecim_destruct3 + ##| ##4: napply exadecim_destruct4 + ##| ##5: napply exadecim_destruct5 + ##| ##6: napply exadecim_destruct6 + ##| ##7: napply exadecim_destruct7 + ##| ##8: napply exadecim_destruct8 + ##| ##9: napply exadecim_destruct9 + ##| ##10: napply exadecim_destruct10 + ##| ##11: napply exadecim_destruct11 + ##| ##12: napply exadecim_destruct12 + ##| ##13: napply exadecim_destruct13 + ##| ##14: napply exadecim_destruct14 + ##| ##15: napply exadecim_destruct15 + ##| ##16: napply exadecim_destruct16 + ##] +nqed. + +nlemma symmetric_eqex : symmetricT exadecim bool eq_ex. + #e1; #e2; + nelim e1; + nelim e2; + nnormalize; + napply refl_eq. +nqed. + +nlemma symmetric_andex : symmetricT exadecim exadecim and_ex. + #e1; #e2; + nelim e1; + nelim e2; + nnormalize; + napply refl_eq. +nqed. + +nlemma associative_andex : ∀e1,e2,e3.(and_ex (and_ex e1 e2) e3) = (and_ex e1 (and_ex e2 e3)). + #e1; #e2; #e3; + nelim e1; + ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq + ##] +nqed. + +nlemma symmetric_orex : symmetricT exadecim exadecim or_ex. + #e1; #e2; + nelim e1; + nelim e2; + nnormalize; + napply refl_eq. +nqed. + +nlemma associative_orex : ∀e1,e2,e3.(or_ex (or_ex e1 e2) e3) = (or_ex e1 (or_ex e2 e3)). + #e1; #e2; #e3; + nelim e1; + ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq + ##] +nqed. + +nlemma symmetric_xorex : symmetricT exadecim exadecim xor_ex. + #e1; #e2; + nelim e1; + nelim e2; + nnormalize; + napply refl_eq. +nqed. + +nlemma associative_xorex : ∀e1,e2,e3.(xor_ex (xor_ex e1 e2) e3) = (xor_ex e1 (xor_ex e2 e3)). + #e1; #e2; #e3; + nelim e1; + ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq + ##] +nqed. + +nlemma symmetric_plusex_dc_dc : ∀e1,e2,c.plus_ex_dc_dc e1 e2 c = plus_ex_dc_dc e2 e1 c. + #e1; #e2; #c; + nelim e1; + nelim e2; + nelim c; + nnormalize; + napply refl_eq. +nqed. + +nlemma plusex_dc_dc_to_dc_d : ∀e1,e2,c.fst … (plus_ex_dc_dc e1 e2 c) = plus_ex_dc_d e1 e2 c. + #e1; #e2; #c; + nelim e1; + nelim e2; + nelim c; + nnormalize; + napply refl_eq. +nqed. + +nlemma plusex_dc_dc_to_dc_c : ∀e1,e2,c.snd … (plus_ex_dc_dc e1 e2 c) = plus_ex_dc_c e1 e2 c. + #e1; #e2; #c; + nelim e1; + nelim e2; + nelim c; + nnormalize; + napply refl_eq. +nqed. + +nlemma plusex_dc_dc_to_d_dc : ∀e1,e2.plus_ex_dc_dc e1 e2 false = plus_ex_d_dc e1 e2. + #e1; #e2; + nelim e1; + nelim e2; + nnormalize; + napply refl_eq. +nqed. + +nlemma plusex_dc_dc_to_d_d : ∀e1,e2.fst … (plus_ex_dc_dc e1 e2 false) = plus_ex_d_d e1 e2. + #e1; #e2; + nelim e1; + nelim e2; + nnormalize; + napply refl_eq. +nqed. + +nlemma plusex_dc_dc_to_d_c : ∀e1,e2.snd … (plus_ex_dc_dc e1 e2 false) = plus_ex_d_c e1 e2. + #e1; #e2; + nelim e1; + nelim e2; + nnormalize; + napply refl_eq. +nqed. + +nlemma symmetric_plusex_dc_d : ∀e1,e2,c.plus_ex_dc_d e1 e2 c = plus_ex_dc_d e2 e1 c. + #e1; #e2; #c; + nelim e1; + nelim e2; + nelim c; + nnormalize; + napply refl_eq. +nqed. + +nlemma symmetric_plusex_dc_c : ∀e1,e2,c.plus_ex_dc_c e1 e2 c = plus_ex_dc_c e2 e1 c. + #e1; #e2; #c; + nelim e1; + nelim e2; + nelim c; + nnormalize; + napply refl_eq. +nqed. + +nlemma symmetric_plusex_d_dc : ∀e1,e2.plus_ex_d_dc e1 e2 = plus_ex_d_dc e2 e1. + #e1; #e2; + nelim e1; + nelim e2; + nnormalize; + napply refl_eq. +nqed. + +nlemma plusex_d_dc_to_d_d : ∀e1,e2.fst … (plus_ex_d_dc e1 e2) = plus_ex_d_d e1 e2. + #e1; #e2; + nelim e1; + nelim e2; + nnormalize; + napply refl_eq. +nqed. + +nlemma plusex_d_dc_to_d_c : ∀e1,e2.snd … (plus_ex_d_dc e1 e2) = plus_ex_d_c e1 e2. + #e1; #e2; + nelim e1; + nelim e2; + nnormalize; + napply refl_eq. +nqed. + +nlemma symmetric_plusex_d_d : ∀e1,e2.plus_ex_d_d e1 e2 = plus_ex_d_d e2 e1. + #e1; #e2; + nelim e1; + nelim e2; + nnormalize; + napply refl_eq. +nqed. + +nlemma associative_plusex_d_d : ∀e1,e2,e3.(plus_ex_d_d (plus_ex_d_d e1 e2) e3) = (plus_ex_d_d e1 (plus_ex_d_d e2 e3)). + #e1; #e2; #e3; + nelim e1; + ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq + ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq + ##] +nqed. + +nlemma symmetric_plusex_d_c : ∀e1,e2.plus_ex_d_c e1 e2 = plus_ex_d_c e2 e1. + #e1; #e2; + nelim e1; + nelim e2; + nnormalize; + napply refl_eq. +nqed. + +nlemma eqex_to_eq : ∀e1,e2:exadecim.(eq_ex e1 e2 = true) → (e1 = e2). + #e1; #e2; + ncases e1; + ncases e2; + nnormalize; + ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply refl_eq + ##| ##*: #H; napply (bool_destruct … H) + ##] +nqed. + +nlemma eq_to_eqex : ∀e1,e2.e1 = e2 → eq_ex e1 e2 = true. + #m1; #m2; + ncases m1; + ncases m2; + nnormalize; + ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply refl_eq + ##| ##*: #H; napply (exadecim_destruct … H) + ##] +nqed. + +nlemma neqex_to_neq : ∀e1,e2:exadecim.(eq_ex e1 e2 = false) → (e1 ≠ e2). + #e1; #e2; + ncases e1; + ncases e2; + nnormalize; + ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply (bool_destruct … H) + ##| ##*: #H; #H1; napply (exadecim_destruct … H1) + ##] +nqed. + +nlemma neq_to_neqex : ∀e1,e2.e1 ≠ e2 → eq_ex e1 e2 = false. + #e1; #e2; + ncases e1; + ncases e2; + nnormalize; + ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply False_ind; napply (H (refl_eq …)) + ##| ##*: #H; napply refl_eq + ##] +nqed. diff --git a/helm/software/matita/contribs/ng_assembly/num/oct.ma b/helm/software/matita/contribs/ng_assembly/num/oct.ma new file mode 100755 index 000000000..4d6a99596 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/num/oct.ma @@ -0,0 +1,78 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* ********************************************************************** *) + +include "num/bool.ma". + +(* ****** *) +(* OTTALI *) +(* ****** *) + +ninductive oct : Type ≝ + o0: oct +| o1: oct +| o2: oct +| o3: oct +| o4: oct +| o5: oct +| o6: oct +| o7: oct. + +(* operatore = *) +ndefinition eq_oct ≝ +λn1,n2:oct. + match n1 with + [ o0 ⇒ match n2 with [ o0 ⇒ true | _ ⇒ false ] + | o1 ⇒ match n2 with [ o1 ⇒ true | _ ⇒ false ] + | o2 ⇒ match n2 with [ o2 ⇒ true | _ ⇒ false ] + | o3 ⇒ match n2 with [ o3 ⇒ true | _ ⇒ false ] + | o4 ⇒ match n2 with [ o4 ⇒ true | _ ⇒ false ] + | o5 ⇒ match n2 with [ o5 ⇒ true | _ ⇒ false ] + | o6 ⇒ match n2 with [ o6 ⇒ true | _ ⇒ false ] + | o7 ⇒ match n2 with [ o7 ⇒ true | _ ⇒ false ] + ]. + +(* iteratore sugli ottali *) +ndefinition forall_oct ≝ λP. + P o0 ⊗ P o1 ⊗ P o2 ⊗ P o3 ⊗ P o4 ⊗ P o5 ⊗ P o6 ⊗ P o7. + +(* operatore successore *) +ndefinition succ_oct ≝ +λn.match n with + [ o0 ⇒ o1 | o1 ⇒ o2 | o2 ⇒ o3 | o3 ⇒ o4 | o4 ⇒ o5 | o5 ⇒ o6 | o6 ⇒ o7 | o7 ⇒ o0 ]. + +(* ottali ricorsivi *) +ninductive rec_oct : oct → Type ≝ + oc_O : rec_oct o0 +| oc_S : ∀n.rec_oct n → rec_oct (succ_oct n). + +(* ottali → ottali ricorsivi *) +ndefinition oct_to_recoct ≝ +λn.match n return λx.rec_oct x with + [ o0 ⇒ oc_O + | o1 ⇒ oc_S ? oc_O + | o2 ⇒ oc_S ? (oc_S ? oc_O) + | o3 ⇒ oc_S ? (oc_S ? (oc_S ? oc_O)) + | o4 ⇒ oc_S ? (oc_S ? (oc_S ? (oc_S ? oc_O))) + | o5 ⇒ oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? oc_O)))) + | o6 ⇒ oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? oc_O))))) + | o7 ⇒ oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? oc_O)))))) + ]. diff --git a/helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma new file mode 100755 index 000000000..7aa0ff208 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma @@ -0,0 +1,143 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* ********************************************************************** *) + +include "num/oct.ma". +include "num/bool_lemmas.ma". + +(* ****** *) +(* OTTALI *) +(* ****** *) + +ndefinition oct_destruct_aux ≝ +Πn1,n2:oct.ΠP:Prop.n1 = n2 → + match n1 with + [ o0 ⇒ match n2 with [ o0 ⇒ P → P | _ ⇒ P ] + | o1 ⇒ match n2 with [ o1 ⇒ P → P | _ ⇒ P ] + | o2 ⇒ match n2 with [ o2 ⇒ P → P | _ ⇒ P ] + | o3 ⇒ match n2 with [ o3 ⇒ P → P | _ ⇒ P ] + | o4 ⇒ match n2 with [ o4 ⇒ P → P | _ ⇒ P ] + | o5 ⇒ match n2 with [ o5 ⇒ P → P | _ ⇒ P ] + | o6 ⇒ match n2 with [ o6 ⇒ P → P | _ ⇒ P ] + | o7 ⇒ match n2 with [ o7 ⇒ P → P | _ ⇒ P ] + ]. + +ndefinition oct_destruct : oct_destruct_aux. + #n1; #n2; #P; + nelim n1; + ##[ ##1: nelim n2; nnormalize; #H; + ##[ ##1: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match o0 with [ o0 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] + ##| ##2: nelim n2; nnormalize; #H; + ##[ ##2: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match o1 with [ o1 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] + ##| ##3: nelim n2; nnormalize; #H; + ##[ ##3: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match o2 with [ o2 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] + ##| ##4: nelim n2; nnormalize; #H; + ##[ ##4: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match o3 with [ o3 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] + ##| ##5: nelim n2; nnormalize; #H; + ##[ ##5: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match o4 with [ o4 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] + ##| ##6: nelim n2; nnormalize; #H; + ##[ ##6: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match o5 with [ o5 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] + ##| ##7: nelim n2; nnormalize; #H; + ##[ ##7: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match o6 with [ o6 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] + ##| ##8: nelim n2; nnormalize; #H; + ##[ ##8: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match o7 with [ o7 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] + ##] +nqed. + +nlemma symmetric_eqoct : symmetricT oct bool eq_oct. + #n1; #n2; + nelim n1; + nelim n2; + nnormalize; + napply refl_eq. +nqed. + +nlemma eqoct_to_eq : ∀n1,n2.eq_oct n1 n2 = true → n1 = n2. + #n1; #n2; + ncases n1; + ncases n2; + nnormalize; + ##[ ##1,10,19,28,37,46,55,64: #H; napply refl_eq + ##| ##*: #H; napply (bool_destruct … H) + ##] +nqed. + +nlemma eq_to_eqoct : ∀n1,n2.n1 = n2 → eq_oct n1 n2 = true. + #n1; #n2; + ncases n1; + ncases n2; + nnormalize; + ##[ ##1,10,19,28,37,46,55,64: #H; napply refl_eq + ##| ##*: #H; napply (oct_destruct … H) + ##] +nqed. + +nlemma neqoct_to_neq : ∀n1,n2.eq_oct n1 n2 = false → n1 ≠ n2. + #n1; #n2; + ncases n1; + ncases n2; + nnormalize; + ##[ ##1,10,19,28,37,46,55,64: #H; napply (bool_destruct … H) + ##| ##*: #H; #H1; napply (oct_destruct … H1) + ##] +nqed. + +nlemma neq_to_neqoct : ∀n1,n2.n1 ≠ n2 → eq_oct n1 n2 = false. + #n1; #n2; + ncases n1; + ncases n2; + nnormalize; + ##[ ##1,10,19,28,37,46,55,64: #H; napply False_ind; napply (H (refl_eq …)) + ##| ##*: #H; napply refl_eq + ##] +nqed. diff --git a/helm/software/matita/contribs/ng_assembly/num/quatern.ma b/helm/software/matita/contribs/ng_assembly/num/quatern.ma new file mode 100755 index 000000000..02a94e6ff --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/num/quatern.ma @@ -0,0 +1,66 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* ********************************************************************** *) + +include "num/bool.ma". + +(* ********** *) +(* QUATERNARI *) +(* ********** *) + +ninductive quatern : Type ≝ + q0 : quatern +| q1 : quatern +| q2 : quatern +| q3 : quatern. + +(* operatore = *) +ndefinition eq_qu ≝ +λn1,n2:quatern. + match n1 with + [ q0 ⇒ match n2 with [ q0 ⇒ true | _ ⇒ false ] + | q1 ⇒ match n2 with [ q1 ⇒ true | _ ⇒ false ] + | q2 ⇒ match n2 with [ q2 ⇒ true | _ ⇒ false ] + | q3 ⇒ match n2 with [ q3 ⇒ true | _ ⇒ false ] + ]. + +(* iteratore sui quaternari *) +ndefinition forall_qu ≝ λP. + P q0 ⊗ P q1 ⊗ P q2 ⊗ P q3. + +(* operatore successorre *) +ndefinition succ_qu ≝ +λn.match n with + [ q0 ⇒ q1 | q1 ⇒ q2 | q2 ⇒ q3 | q3 ⇒ q0 ]. + +(* quaternari ricorsivi *) +ninductive rec_quatern : quatern → Type ≝ + qu_O : rec_quatern q0 +| qu_S : ∀n.rec_quatern n → rec_quatern (succ_qu n). + +(* quaternari → quaternari ricorsivi *) +ndefinition qu_to_recqu ≝ +λn.match n return λx.rec_quatern x with + [ q0 ⇒ qu_O + | q1 ⇒ qu_S ? qu_O + | q2 ⇒ qu_S ? (qu_S ? qu_O) + | q3 ⇒ qu_S ? (qu_S ? (qu_S ? qu_O)) + ]. diff --git a/helm/software/matita/contribs/ng_assembly/num/quatern_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/quatern_lemmas.ma new file mode 100755 index 000000000..66a75cc53 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/num/quatern_lemmas.ma @@ -0,0 +1,115 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* ********************************************************************** *) + +include "num/quatern.ma". +include "num/bool_lemmas.ma". + +(* ********** *) +(* QUATERNARI *) +(* ********** *) + +ndefinition quatern_destruct_aux ≝ +Πn1,n2:quatern.ΠP:Prop.n1 = n2 → + match n1 with + [ q0 ⇒ match n2 with [ q0 ⇒ P → P | _ ⇒ P ] + | q1 ⇒ match n2 with [ q1 ⇒ P → P | _ ⇒ P ] + | q2 ⇒ match n2 with [ q2 ⇒ P → P | _ ⇒ P ] + | q3 ⇒ match n2 with [ q3 ⇒ P → P | _ ⇒ P ] + ]. + +ndefinition quatern_destruct : quatern_destruct_aux. + #n1; #n2; #P; + nelim n1; + ##[ ##1: nelim n2; nnormalize; #H; + ##[ ##1: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match q0 with [ q0 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] + ##| ##2: nelim n2; nnormalize; #H; + ##[ ##2: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match q1 with [ q1 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] + ##| ##3: nelim n2; nnormalize; #H; + ##[ ##3: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match q2 with [ q2 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] + ##| ##4: nelim n2; nnormalize; #H; + ##[ ##4: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match q3 with [ q3 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] + ##] +nqed. + +nlemma symmetric_eqqu : symmetricT quatern bool eq_qu. + #n1; #n2; + nelim n1; + nelim n2; + nnormalize; + napply refl_eq. +nqed. + +nlemma eqqu_to_eq : ∀n1,n2.eq_qu n1 n2 = true → n1 = n2. + #n1; #n2; + ncases n1; + ncases n2; + nnormalize; + ##[ ##1,6,11,16: #H; napply refl_eq + ##| ##*: #H; napply (bool_destruct … H) + ##] +nqed. + +nlemma eq_to_eqqu : ∀n1,n2.n1 = n2 → eq_qu n1 n2 = true. + #n1; #n2; + ncases n1; + ncases n2; + nnormalize; + ##[ ##1,6,11,16: #H; napply refl_eq + ##| ##*: #H; napply (quatern_destruct … H) + ##] +nqed. + +nlemma neqqu_to_neq : ∀n1,n2.eq_qu n1 n2 = false → n1 ≠ n2. + #n1; #n2; + ncases n1; + ncases n2; + nnormalize; + ##[ ##1,6,11,16: #H; napply (bool_destruct … H) + ##| ##*: #H; #H1; napply (quatern_destruct … H1) + ##] +nqed. + +nlemma neq_to_neqqu : ∀n1,n2.n1 ≠ n2 → eq_qu n1 n2 = false. + #n1; #n2; + ncases n1; + ncases n2; + nnormalize; + ##[ ##1,6,11,16: #H; napply False_ind; napply (H (refl_eq …)) + ##| ##*: #H; napply refl_eq + ##] +nqed. diff --git a/helm/software/matita/contribs/ng_assembly/test_errori.ma b/helm/software/matita/contribs/ng_assembly/test_errori.ma index 155b6073f..4236c5c63 100644 --- a/helm/software/matita/contribs/ng_assembly/test_errori.ma +++ b/helm/software/matita/contribs/ng_assembly/test_errori.ma @@ -1,7 +1,6 @@ -include "utility/utility.ma". +(*include "utility/utility.ma". -(* nlemma fold_right_neList2_aux3 : \forall T. \forall h,h',t,t'.len_neList T (h§§t) = len_neList T (h'§§t') → len_neList T t = len_neList T t'. #T; #h; #h'; #t; #t'; @@ -22,9 +21,8 @@ nlemma fold_right_neList2_aux3 : nchange in H2:(%) with ((S (len_neList T (a§§l1))) = (S (len_neList T (a§§l)))); *) -include "freescale/byte8_lemmas.ma". +(*include "freescale/byte8_lemmas.ma". -(* nlemma associative_plusb8_aux : \forall e1,e2,e3,e4. match plus_ex_d_dc e2 e4 with @@ -70,9 +68,8 @@ nlemma associative_plusb8 (*...*) *) -include "compiler/ast_type_lemmas.ma". +(*include "compiler/ast_type_lemmas.ma". -(* nlemma symmetric_eqasttype_aux1 : ∀x1,x2,y2.eq_nat (len_neList ast_type («£x1»)) (len_neList ast_type (x2§§y2)) = false. #x1; #x2; #y2; ncases y2; nnormalize; -- 2.39.2