(* Progetto FreeScale *)
(* *)
(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Ultima modifica: 05/08/2009 *)
+(* Sviluppo: 2008-2010 *)
(* *)
(* ********************************************************************** *)
include "common/list.ma".
-include "num/bool_lemmas.ma".
+include "common/nat_lemmas.ma".
+include "common/prod.ma".
-nlet rec nmember_list (T:Type) (elem:T) (f:T → T → bool) (l:list T) on l ≝
+nlet rec nmember_natList (elem:nat) (l:ne_list nat) on l ≝
match l with
- [ nil ⇒ true
- | cons h t ⇒ match f elem h with
- [ true ⇒ false | false ⇒ nmember_list T elem f t ]
+ [ ne_nil h ⇒ ⊖(eq_nat elem h)
+ | ne_cons h t ⇒ match eq_nat elem h with
+ [ true ⇒ false | false ⇒ nmember_natList elem t ]
].
(* elem presente una ed una sola volta in l *)
-nlet rec member_list (T:Type) (elem:T) (f:T → T → bool) (l:list T) on l ≝
+nlet rec member_natList (elem:nat) (l:ne_list nat) on l ≝
match l with
- [ nil ⇒ false
- | cons h t ⇒ match f elem h with
- [ true ⇒ nmember_list T elem f t | false ⇒ member_list T elem f t ]
+ [ ne_nil h ⇒ eq_nat elem h
+ | ne_cons h t ⇒ match eq_nat elem h with
+ [ true ⇒ nmember_natList elem t | false ⇒ member_natList elem t ]
].
-(* tutti gli atomi dell'universo che poi saranno raggruppati in sottouniversi *)
-ninductive UN : Type ≝
-(* quaternari[4] 1-4 *)
- uq0 : UN
-| uq1 : UN
-| uq2 : UN
-| uq3 : UN
-
-(* ottali[8] 5-12 *)
-| uo0 : UN
-| uo1 : UN
-| uo2 : UN
-| uo3 : UN
-| uo4 : UN
-| uo5 : UN
-| uo6 : UN
-| uo7 : UN
-
-(* esadecimali[16] 13-28 *)
-| ux0 : UN
-| ux1 : UN
-| ux2 : UN
-| ux3 : UN
-| ux4 : UN
-| ux5 : UN
-| ux6 : UN
-| ux7 : UN
-| ux8 : UN
-| ux9 : UN
-| uxA : UN
-| uxB : UN
-| uxC : UN
-| uxD : UN
-| uxE : UN
-| uxF : UN
-
-(* bitrigesimali[32] 29-60 *)
-| ut00 : UN
-| ut01 : UN
-| ut02 : UN
-| ut03 : UN
-| ut04 : UN
-| ut05 : UN
-| ut06 : UN
-| ut07 : UN
-| ut08 : UN
-| ut09 : UN
-| ut0A : UN
-| ut0B : UN
-| ut0C : UN
-| ut0D : UN
-| ut0E : UN
-| ut0F : UN
-| ut10 : UN
-| ut11 : UN
-| ut12 : UN
-| ut13 : UN
-| ut14 : UN
-| ut15 : UN
-| ut16 : UN
-| ut17 : UN
-| ut18 : UN
-| ut19 : UN
-| ut1A : UN
-| ut1B : UN
-| ut1C : UN
-| ut1D : UN
-| ut1E : UN
-| ut1F : UN
-
-(* ascii[63] 61-123 *)
-| uch_0 : UN
-| uch_1 : UN
-| uch_2 : UN
-| uch_3 : UN
-| uch_4 : UN
-| uch_5 : UN
-| uch_6 : UN
-| uch_7 : UN
-| uch_8 : UN
-| uch_9 : UN
-| uch__ : UN
-| uch_A : UN
-| uch_B : UN
-| uch_C : UN
-| uch_D : UN
-| uch_E : UN
-| uch_F : UN
-| uch_G : UN
-| uch_H : UN
-| uch_I : UN
-| uch_J : UN
-| uch_K : UN
-| uch_L : UN
-| uch_M : UN
-| uch_N : UN
-| uch_O : UN
-| uch_P : UN
-| uch_Q : UN
-| uch_R : UN
-| uch_S : UN
-| uch_T : UN
-| uch_U : UN
-| uch_V : UN
-| uch_W : UN
-| uch_X : UN
-| uch_Y : UN
-| uch_Z : UN
-| uch_a : UN
-| uch_b : UN
-| uch_c : UN
-| uch_d : UN
-| uch_e : UN
-| uch_f : UN
-| uch_g : UN
-| uch_h : UN
-| uch_i : UN
-| uch_j : UN
-| uch_k : UN
-| uch_l : UN
-| uch_m : UN
-| uch_n : UN
-| uch_o : UN
-| uch_p : UN
-| uch_q : UN
-| uch_r : UN
-| uch_s : UN
-| uch_t : UN
-| uch_u : UN
-| uch_v : UN
-| uch_w : UN
-| uch_x : UN
-| uch_y : UN
-| uch_z : UN
-
-(* opcode[91] 124-214 *)
-| uADC : UN
-| uADD : UN
-| uAIS : UN
-| uAIX : UN
-| uAND : UN
-| uASL : UN
-| uASR : UN
-| uBCC : UN
-| uBCLRn : UN
-| uBCS : UN
-| uBEQ : UN
-| uBGE : UN
-| uBGND : UN
-| uBGT : UN
-| uBHCC : UN
-| uBHCS : UN
-| uBHI : UN
-| uBIH : UN
-| uBIL : UN
-| uBIT : UN
-| uBLE : UN
-| uBLS : UN
-| uBLT : UN
-| uBMC : UN
-| uBMI : UN
-| uBMS : UN
-| uBNE : UN
-| uBPL : UN
-| uBRA : UN
-| uBRCLRn : UN
-| uBRN : UN
-| uBRSETn : UN
-| uBSETn : UN
-| uBSR : UN
-| uCBEQA : UN
-| uCBEQX : UN
-| uCLC : UN
-| uCLI : UN
-| uCLR : UN
-| uCMP : UN
-| uCOM : UN
-| uCPHX : UN
-| uCPX : UN
-| uDAA : UN
-| uDBNZ : UN
-| uDEC : UN
-| uDIV : UN
-| uEOR : UN
-| uINC : UN
-| uJMP : UN
-| uJSR : UN
-| uLDA : UN
-| uLDHX : UN
-| uLDX : UN
-| uLSR : UN
-| uMOV : UN
-| uMUL : UN
-| uNEG : UN
-| uNOP : UN
-| uNSA : UN
-| uORA : UN
-| uPSHA : UN
-| uPSHH : UN
-| uPSHX : UN
-| uPULA : UN
-| uPULH : UN
-| uPULX : UN
-| uROL : UN
-| uROR : UN
-| uRSP : UN
-| uRTI : UN
-| uRTS : UN
-| uSBC : UN
-| uSEC : UN
-| uSEI : UN
-| uSHA : UN
-| uSLA : UN
-| uSTA : UN
-| uSTHX : UN
-| uSTOP : UN
-| uSTX : UN
-| uSUB : UN
-| uSWI : UN
-| uTAP : UN
-| uTAX : UN
-| uTPA : UN
-| uTST : UN
-| uTSX : UN
-| uTXA : UN
-| uTXS : UN
-| uWAIT : UN
-.
-
-(* funzione di uguaglianza sugli atomi *)
-ndefinition eq_UN ≝
-λu1,u2.match u1 with
- [ uq0 ⇒ match u2 with [ uq0 ⇒ true | _ ⇒ false ]
- | uq1 ⇒ match u2 with [ uq1 ⇒ true | _ ⇒ false ]
- | uq2 ⇒ match u2 with [ uq2 ⇒ true | _ ⇒ false ]
- | uq3 ⇒ match u2 with [ uq3 ⇒ true | _ ⇒ false ]
-
- | uo0 ⇒ match u2 with [ uo0 ⇒ true | _ ⇒ false ]
- | uo1 ⇒ match u2 with [ uo1 ⇒ true | _ ⇒ false ]
- | uo2 ⇒ match u2 with [ uo2 ⇒ true | _ ⇒ false ]
- | uo3 ⇒ match u2 with [ uo3 ⇒ true | _ ⇒ false ]
- | uo4 ⇒ match u2 with [ uo4 ⇒ true | _ ⇒ false ]
- | uo5 ⇒ match u2 with [ uo5 ⇒ true | _ ⇒ false ]
- | uo6 ⇒ match u2 with [ uo6 ⇒ true | _ ⇒ false ]
- | uo7 ⇒ match u2 with [ uo7 ⇒ true | _ ⇒ false ]
-
- | ux0 ⇒ match u2 with [ ux0 ⇒ true | _ ⇒ false ]
- | ux1 ⇒ match u2 with [ ux1 ⇒ true | _ ⇒ false ]
- | ux2 ⇒ match u2 with [ ux2 ⇒ true | _ ⇒ false ]
- | ux3 ⇒ match u2 with [ ux3 ⇒ true | _ ⇒ false ]
- | ux4 ⇒ match u2 with [ ux4 ⇒ true | _ ⇒ false ]
- | ux5 ⇒ match u2 with [ ux5 ⇒ true | _ ⇒ false ]
- | ux6 ⇒ match u2 with [ ux6 ⇒ true | _ ⇒ false ]
- | ux7 ⇒ match u2 with [ ux7 ⇒ true | _ ⇒ false ]
- | ux8 ⇒ match u2 with [ ux8 ⇒ true | _ ⇒ false ]
- | ux9 ⇒ match u2 with [ ux9 ⇒ true | _ ⇒ false ]
- | uxA ⇒ match u2 with [ uxA ⇒ true | _ ⇒ false ]
- | uxB ⇒ match u2 with [ uxB ⇒ true | _ ⇒ false ]
- | uxC ⇒ match u2 with [ uxC ⇒ true | _ ⇒ false ]
- | uxD ⇒ match u2 with [ uxD ⇒ true | _ ⇒ false ]
- | uxE ⇒ match u2 with [ uxE ⇒ true | _ ⇒ false ]
- | uxF ⇒ match u2 with [ uxF ⇒ true | _ ⇒ false ]
-
- | ut00 ⇒ match u2 with [ ut00 ⇒ true | _ ⇒ false ]
- | ut01 ⇒ match u2 with [ ut01 ⇒ true | _ ⇒ false ]
- | ut02 ⇒ match u2 with [ ut02 ⇒ true | _ ⇒ false ]
- | ut03 ⇒ match u2 with [ ut03 ⇒ true | _ ⇒ false ]
- | ut04 ⇒ match u2 with [ ut04 ⇒ true | _ ⇒ false ]
- | ut05 ⇒ match u2 with [ ut05 ⇒ true | _ ⇒ false ]
- | ut06 ⇒ match u2 with [ ut06 ⇒ true | _ ⇒ false ]
- | ut07 ⇒ match u2 with [ ut07 ⇒ true | _ ⇒ false ]
- | ut08 ⇒ match u2 with [ ut08 ⇒ true | _ ⇒ false ]
- | ut09 ⇒ match u2 with [ ut09 ⇒ true | _ ⇒ false ]
- | ut0A ⇒ match u2 with [ ut0A ⇒ true | _ ⇒ false ]
- | ut0B ⇒ match u2 with [ ut0B ⇒ true | _ ⇒ false ]
- | ut0C ⇒ match u2 with [ ut0C ⇒ true | _ ⇒ false ]
- | ut0D ⇒ match u2 with [ ut0D ⇒ true | _ ⇒ false ]
- | ut0E ⇒ match u2 with [ ut0E ⇒ true | _ ⇒ false ]
- | ut0F ⇒ match u2 with [ ut0F ⇒ true | _ ⇒ false ]
- | ut10 ⇒ match u2 with [ ut10 ⇒ true | _ ⇒ false ]
- | ut11 ⇒ match u2 with [ ut11 ⇒ true | _ ⇒ false ]
- | ut12 ⇒ match u2 with [ ut12 ⇒ true | _ ⇒ false ]
- | ut13 ⇒ match u2 with [ ut13 ⇒ true | _ ⇒ false ]
- | ut14 ⇒ match u2 with [ ut14 ⇒ true | _ ⇒ false ]
- | ut15 ⇒ match u2 with [ ut15 ⇒ true | _ ⇒ false ]
- | ut16 ⇒ match u2 with [ ut16 ⇒ true | _ ⇒ false ]
- | ut17 ⇒ match u2 with [ ut17 ⇒ true | _ ⇒ false ]
- | ut18 ⇒ match u2 with [ ut18 ⇒ true | _ ⇒ false ]
- | ut19 ⇒ match u2 with [ ut19 ⇒ true | _ ⇒ false ]
- | ut1A ⇒ match u2 with [ ut1A ⇒ true | _ ⇒ false ]
- | ut1B ⇒ match u2 with [ ut1B ⇒ true | _ ⇒ false ]
- | ut1C ⇒ match u2 with [ ut1C ⇒ true | _ ⇒ false ]
- | ut1D ⇒ match u2 with [ ut1D ⇒ true | _ ⇒ false ]
- | ut1E ⇒ match u2 with [ ut1E ⇒ true | _ ⇒ false ]
- | ut1F ⇒ match u2 with [ ut1F ⇒ true | _ ⇒ false ]
-
- | uch_0 ⇒ match u2 with [ uch_0 ⇒ true | _ ⇒ false ]
- | uch_1 ⇒ match u2 with [ uch_1 ⇒ true | _ ⇒ false ]
- | uch_2 ⇒ match u2 with [ uch_2 ⇒ true | _ ⇒ false ]
- | uch_3 ⇒ match u2 with [ uch_3 ⇒ true | _ ⇒ false ]
- | uch_4 ⇒ match u2 with [ uch_4 ⇒ true | _ ⇒ false ]
- | uch_5 ⇒ match u2 with [ uch_5 ⇒ true | _ ⇒ false ]
- | uch_6 ⇒ match u2 with [ uch_6 ⇒ true | _ ⇒ false ]
- | uch_7 ⇒ match u2 with [ uch_7 ⇒ true | _ ⇒ false ]
- | uch_8 ⇒ match u2 with [ uch_8 ⇒ true | _ ⇒ false ]
- | uch_9 ⇒ match u2 with [ uch_9 ⇒ true | _ ⇒ false ]
- | uch__ ⇒ match u2 with [ uch__ ⇒ true | _ ⇒ false ]
- | uch_A ⇒ match u2 with [ uch_A ⇒ true | _ ⇒ false ]
- | uch_B ⇒ match u2 with [ uch_B ⇒ true | _ ⇒ false ]
- | uch_C ⇒ match u2 with [ uch_C ⇒ true | _ ⇒ false ]
- | uch_D ⇒ match u2 with [ uch_D ⇒ true | _ ⇒ false ]
- | uch_E ⇒ match u2 with [ uch_E ⇒ true | _ ⇒ false ]
- | uch_F ⇒ match u2 with [ uch_F ⇒ true | _ ⇒ false ]
- | uch_G ⇒ match u2 with [ uch_G ⇒ true | _ ⇒ false ]
- | uch_H ⇒ match u2 with [ uch_H ⇒ true | _ ⇒ false ]
- | uch_I ⇒ match u2 with [ uch_I ⇒ true | _ ⇒ false ]
- | uch_J ⇒ match u2 with [ uch_J ⇒ true | _ ⇒ false ]
- | uch_K ⇒ match u2 with [ uch_K ⇒ true | _ ⇒ false ]
- | uch_L ⇒ match u2 with [ uch_L ⇒ true | _ ⇒ false ]
- | uch_M ⇒ match u2 with [ uch_M ⇒ true | _ ⇒ false ]
- | uch_N ⇒ match u2 with [ uch_N ⇒ true | _ ⇒ false ]
- | uch_O ⇒ match u2 with [ uch_O ⇒ true | _ ⇒ false ]
- | uch_P ⇒ match u2 with [ uch_P ⇒ true | _ ⇒ false ]
- | uch_Q ⇒ match u2 with [ uch_Q ⇒ true | _ ⇒ false ]
- | uch_R ⇒ match u2 with [ uch_R ⇒ true | _ ⇒ false ]
- | uch_S ⇒ match u2 with [ uch_S ⇒ true | _ ⇒ false ]
- | uch_T ⇒ match u2 with [ uch_T ⇒ true | _ ⇒ false ]
- | uch_U ⇒ match u2 with [ uch_U ⇒ true | _ ⇒ false ]
- | uch_V ⇒ match u2 with [ uch_V ⇒ true | _ ⇒ false ]
- | uch_W ⇒ match u2 with [ uch_W ⇒ true | _ ⇒ false ]
- | uch_X ⇒ match u2 with [ uch_X ⇒ true | _ ⇒ false ]
- | uch_Y ⇒ match u2 with [ uch_Y ⇒ true | _ ⇒ false ]
- | uch_Z ⇒ match u2 with [ uch_Z ⇒ true | _ ⇒ false ]
- | uch_a ⇒ match u2 with [ uch_a ⇒ true | _ ⇒ false ]
- | uch_b ⇒ match u2 with [ uch_b ⇒ true | _ ⇒ false ]
- | uch_c ⇒ match u2 with [ uch_c ⇒ true | _ ⇒ false ]
- | uch_d ⇒ match u2 with [ uch_d ⇒ true | _ ⇒ false ]
- | uch_e ⇒ match u2 with [ uch_e ⇒ true | _ ⇒ false ]
- | uch_f ⇒ match u2 with [ uch_f ⇒ true | _ ⇒ false ]
- | uch_g ⇒ match u2 with [ uch_g ⇒ true | _ ⇒ false ]
- | uch_h ⇒ match u2 with [ uch_h ⇒ true | _ ⇒ false ]
- | uch_i ⇒ match u2 with [ uch_i ⇒ true | _ ⇒ false ]
- | uch_j ⇒ match u2 with [ uch_j ⇒ true | _ ⇒ false ]
- | uch_k ⇒ match u2 with [ uch_k ⇒ true | _ ⇒ false ]
- | uch_l ⇒ match u2 with [ uch_l ⇒ true | _ ⇒ false ]
- | uch_m ⇒ match u2 with [ uch_m ⇒ true | _ ⇒ false ]
- | uch_n ⇒ match u2 with [ uch_n ⇒ true | _ ⇒ false ]
- | uch_o ⇒ match u2 with [ uch_o ⇒ true | _ ⇒ false ]
- | uch_p ⇒ match u2 with [ uch_p ⇒ true | _ ⇒ false ]
- | uch_q ⇒ match u2 with [ uch_q ⇒ true | _ ⇒ false ]
- | uch_r ⇒ match u2 with [ uch_r ⇒ true | _ ⇒ false ]
- | uch_s ⇒ match u2 with [ uch_s ⇒ true | _ ⇒ false ]
- | uch_t ⇒ match u2 with [ uch_t ⇒ true | _ ⇒ false ]
- | uch_u ⇒ match u2 with [ uch_u ⇒ true | _ ⇒ false ]
- | uch_v ⇒ match u2 with [ uch_v ⇒ true | _ ⇒ false ]
- | uch_w ⇒ match u2 with [ uch_w ⇒ true | _ ⇒ false ]
- | uch_x ⇒ match u2 with [ uch_x ⇒ true | _ ⇒ false ]
- | uch_y ⇒ match u2 with [ uch_y ⇒ true | _ ⇒ false ]
- | uch_z ⇒ match u2 with [ uch_z ⇒ true | _ ⇒ false ]
-
- | uADC ⇒ match u2 with [ uADC ⇒ true | _ ⇒ false ]
- | uADD ⇒ match u2 with [ uADD ⇒ true | _ ⇒ false ]
- | uAIS ⇒ match u2 with [ uAIS ⇒ true | _ ⇒ false ]
- | uAIX ⇒ match u2 with [ uAIX ⇒ true | _ ⇒ false ]
- | uAND ⇒ match u2 with [ uAND ⇒ true | _ ⇒ false ]
- | uASL ⇒ match u2 with [ uASL ⇒ true | _ ⇒ false ]
- | uASR ⇒ match u2 with [ uASR ⇒ true | _ ⇒ false ]
- | uBCC ⇒ match u2 with [ uBCC ⇒ true | _ ⇒ false ]
- | uBCLRn ⇒ match u2 with [ uBCLRn ⇒ true | _ ⇒ false ]
- | uBCS ⇒ match u2 with [ uBCS ⇒ true | _ ⇒ false ]
- | uBEQ ⇒ match u2 with [ uBEQ ⇒ true | _ ⇒ false ]
- | uBGE ⇒ match u2 with [ uBGE ⇒ true | _ ⇒ false ]
- | uBGND ⇒ match u2 with [ uBGND ⇒ true | _ ⇒ false ]
- | uBGT ⇒ match u2 with [ uBGT ⇒ true | _ ⇒ false ]
- | uBHCC ⇒ match u2 with [ uBHCC ⇒ true | _ ⇒ false ]
- | uBHCS ⇒ match u2 with [ uBHCS ⇒ true | _ ⇒ false ]
- | uBHI ⇒ match u2 with [ uBHI ⇒ true | _ ⇒ false ]
- | uBIH ⇒ match u2 with [ uBIH ⇒ true | _ ⇒ false ]
- | uBIL ⇒ match u2 with [ uBIL ⇒ true | _ ⇒ false ]
- | uBIT ⇒ match u2 with [ uBIT ⇒ true | _ ⇒ false ]
- | uBLE ⇒ match u2 with [ uBLE ⇒ true | _ ⇒ false ]
- | uBLS ⇒ match u2 with [ uBLS ⇒ true | _ ⇒ false ]
- | uBLT ⇒ match u2 with [ uBLT ⇒ true | _ ⇒ false ]
- | uBMC ⇒ match u2 with [ uBMC ⇒ true | _ ⇒ false ]
- | uBMI ⇒ match u2 with [ uBMI ⇒ true | _ ⇒ false ]
- | uBMS ⇒ match u2 with [ uBMS ⇒ true | _ ⇒ false ]
- | uBNE ⇒ match u2 with [ uBNE ⇒ true | _ ⇒ false ]
- | uBPL ⇒ match u2 with [ uBPL ⇒ true | _ ⇒ false ]
- | uBRA ⇒ match u2 with [ uBRA ⇒ true | _ ⇒ false ]
- | uBRCLRn ⇒ match u2 with [ uBRCLRn ⇒ true | _ ⇒ false ]
- | uBRN ⇒ match u2 with [ uBRN ⇒ true | _ ⇒ false ]
- | uBRSETn ⇒ match u2 with [ uBRSETn ⇒ true | _ ⇒ false ]
- | uBSETn ⇒ match u2 with [ uBSETn ⇒ true | _ ⇒ false ]
- | uBSR ⇒ match u2 with [ uBSR ⇒ true | _ ⇒ false ]
- | uCBEQA ⇒ match u2 with [ uCBEQA ⇒ true | _ ⇒ false ]
- | uCBEQX ⇒ match u2 with [ uCBEQX ⇒ true | _ ⇒ false ]
- | uCLC ⇒ match u2 with [ uCLC ⇒ true | _ ⇒ false ]
- | uCLI ⇒ match u2 with [ uCLI ⇒ true | _ ⇒ false ]
- | uCLR ⇒ match u2 with [ uCLR ⇒ true | _ ⇒ false ]
- | uCMP ⇒ match u2 with [ uCMP ⇒ true | _ ⇒ false ]
- | uCOM ⇒ match u2 with [ uCOM ⇒ true | _ ⇒ false ]
- | uCPHX ⇒ match u2 with [ uCPHX ⇒ true | _ ⇒ false ]
- | uCPX ⇒ match u2 with [ uCPX ⇒ true | _ ⇒ false ]
- | uDAA ⇒ match u2 with [ uDAA ⇒ true | _ ⇒ false ]
- | uDBNZ ⇒ match u2 with [ uDBNZ ⇒ true | _ ⇒ false ]
- | uDEC ⇒ match u2 with [ uDEC ⇒ true | _ ⇒ false ]
- | uDIV ⇒ match u2 with [ uDIV ⇒ true | _ ⇒ false ]
- | uEOR ⇒ match u2 with [ uEOR ⇒ true | _ ⇒ false ]
- | uINC ⇒ match u2 with [ uINC ⇒ true | _ ⇒ false ]
- | uJMP ⇒ match u2 with [ uJMP ⇒ true | _ ⇒ false ]
- | uJSR ⇒ match u2 with [ uJSR ⇒ true | _ ⇒ false ]
- | uLDA ⇒ match u2 with [ uLDA ⇒ true | _ ⇒ false ]
- | uLDHX ⇒ match u2 with [ uLDHX ⇒ true | _ ⇒ false ]
- | uLDX ⇒ match u2 with [ uLDX ⇒ true | _ ⇒ false ]
- | uLSR ⇒ match u2 with [ uLSR ⇒ true | _ ⇒ false ]
- | uMOV ⇒ match u2 with [ uMOV ⇒ true | _ ⇒ false ]
- | uMUL ⇒ match u2 with [ uMUL ⇒ true | _ ⇒ false ]
- | uNEG ⇒ match u2 with [ uNEG ⇒ true | _ ⇒ false ]
- | uNOP ⇒ match u2 with [ uNOP ⇒ true | _ ⇒ false ]
- | uNSA ⇒ match u2 with [ uNSA ⇒ true | _ ⇒ false ]
- | uORA ⇒ match u2 with [ uORA ⇒ true | _ ⇒ false ]
- | uPSHA ⇒ match u2 with [ uPSHA ⇒ true | _ ⇒ false ]
- | uPSHH ⇒ match u2 with [ uPSHH ⇒ true | _ ⇒ false ]
- | uPSHX ⇒ match u2 with [ uPSHX ⇒ true | _ ⇒ false ]
- | uPULA ⇒ match u2 with [ uPULA ⇒ true | _ ⇒ false ]
- | uPULH ⇒ match u2 with [ uPULH ⇒ true | _ ⇒ false ]
- | uPULX ⇒ match u2 with [ uPULX ⇒ true | _ ⇒ false ]
- | uROL ⇒ match u2 with [ uROL ⇒ true | _ ⇒ false ]
- | uROR ⇒ match u2 with [ uROR ⇒ true | _ ⇒ false ]
- | uRSP ⇒ match u2 with [ uRSP ⇒ true | _ ⇒ false ]
- | uRTI ⇒ match u2 with [ uRTI ⇒ true | _ ⇒ false ]
- | uRTS ⇒ match u2 with [ uRTS ⇒ true | _ ⇒ false ]
- | uSBC ⇒ match u2 with [ uSBC ⇒ true | _ ⇒ false ]
- | uSEC ⇒ match u2 with [ uSEC ⇒ true | _ ⇒ false ]
- | uSEI ⇒ match u2 with [ uSEI ⇒ true | _ ⇒ false ]
- | uSHA ⇒ match u2 with [ uSHA ⇒ true | _ ⇒ false ]
- | uSLA ⇒ match u2 with [ uSLA ⇒ true | _ ⇒ false ]
- | uSTA ⇒ match u2 with [ uSTA ⇒ true | _ ⇒ false ]
- | uSTHX ⇒ match u2 with [ uSTHX ⇒ true | _ ⇒ false ]
- | uSTOP ⇒ match u2 with [ uSTOP ⇒ true | _ ⇒ false ]
- | uSTX ⇒ match u2 with [ uSTX ⇒ true | _ ⇒ false ]
- | uSUB ⇒ match u2 with [ uSUB ⇒ true | _ ⇒ false ]
- | uSWI ⇒ match u2 with [ uSWI ⇒ true | _ ⇒ false ]
- | uTAP ⇒ match u2 with [ uTAP ⇒ true | _ ⇒ false ]
- | uTAX ⇒ match u2 with [ uTAX ⇒ true | _ ⇒ false ]
- | uTPA ⇒ match u2 with [ uTPA ⇒ true | _ ⇒ false ]
- | uTST ⇒ match u2 with [ uTST ⇒ true | _ ⇒ false ]
- | uTSX ⇒ match u2 with [ uTSX ⇒ true | _ ⇒ false ]
- | uTXA ⇒ match u2 with [ uTXA ⇒ true | _ ⇒ false ]
- | uTXS ⇒ match u2 with [ uTXS ⇒ true | _ ⇒ false ]
- | uWAIT ⇒ match u2 with [ uWAIT ⇒ true | _ ⇒ false ]
-
- ].
-
(* costruttore di un sottouniverso:
S_EL cioe' uno qualsiasi degli elementi del sottouniverso
- S_KO cioe' il caso impossibile
*)
-ninductive S_UN (l:list UN) : Type ≝
- S_EL : Πx:UN.((member_list UN x eq_UN l) = true) → (∀y.eq_UN x y = true → x = y) → S_UN l
-| S_KO : False → S_UN l.
+ninductive S_UN (l:ne_list nat) : Type ≝
+ S_EL : Πx:nat.((member_natList x l) = true) → S_UN l.
-ndefinition getelem : ∀l.∀e:S_UN l.UN.
+ndefinition getelem : ∀l.∀e:S_UN l.nat.
#l; #s; nelim s;
- ##[ ##1: #u; #dim1; #dim2; napply u
- ##| ##2: #F; nelim F
- ##]
+ #u; #dim;
+ napply u.
nqed.
-ndefinition eq_SUN ≝ λl.λx,y:S_UN l.eq_UN (getelem ? x) (getelem ? y).
-
-ndefinition getdim1 : ∀l.∀e:S_UN l.member_list UN (getelem ? e) eq_UN l = true.
- #l; #s; nelim s;
- ##[ ##2: #F; nelim F
- ##| ##1: #u; #dim1; #dim2; napply dim1
- ##]
-nqed.
+ndefinition eq_SUN ≝ λl.λx,y:S_UN l.eq_nat (getelem ? x) (getelem ? y).
-ndefinition getdim2 : ∀l.∀e:S_UN l.(∀y.eq_UN (getelem ? e) y = true → (getelem ? e) = y).
+ndefinition getdim : ∀l.∀e:S_UN l.member_natList (getelem ? e) l = true.
#l; #s; nelim s;
- ##[ ##2: #F; nelim F
- ##| ##1: #u; #dim1; #dim2; napply dim2
- ##]
+ #u; #dim;
+ napply dim.
nqed.
nlemma SUN_destruct_1
- : ∀l.∀e1,e2.∀dim11,dim21.∀dim12,dim22.S_EL l e1 dim11 dim12 = S_EL l e2 dim21 dim22 → e1 = e2.
- #l; #e1; #e2; #dim11; #dim21; #dim12; #dim22; #H;
- nchange with (match S_EL l e2 dim21 dim22 with [ S_EL a _ _ ⇒ e1 = a | S_KO _ ⇒ False ]);
+ : ∀l.∀e1,e2.∀dim1,dim2.S_EL l e1 dim1 = S_EL l e2 dim2 → e1 = e2.
+ #l; #e1; #e2; #dim1; #dim2; #H;
+ nchange with (match S_EL l e2 dim2 with [ S_EL a _ ⇒ e1 = a ]);
nrewrite < H;
nnormalize;
napply refl_eq.
nqed.
-ndefinition UN_destruct : ∀x,y.∀P:Prop.x = y → match eq_UN x y with [ true ⇒ P → P | false ⇒ P ].
- #x; #y; #P; #H;
- nrewrite > H;
- nelim y;
- nnormalize;
- napply (λx.x).
-nqed.
-
+(* destruct universale *)
ndefinition SUN_destruct : ∀l.∀x,y:S_UN l.∀P:Prop.x = y → match eq_SUN l x y with [ true ⇒ P → P | false ⇒ P ].
#l; #x; nelim x;
- ##[ ##2: #F; nelim F
- ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
- ##[ ##2: #F; nelim F
- ##| ##1: #u2; #dim21; #dim22; #P;
- nchange with (? → (match eq_UN u1 u2 with [ true ⇒ P → P | false ⇒ P ]));
- #H; napply (UN_destruct u1 u2);
- napply (SUN_destruct_1 l … H)
- ##]
- ##]
-nqed.
-
-nlemma eq_to_eqUN : ∀e1,e2.e1 = e2 → eq_UN e1 e2 = true.
- #e1; #e2; #H;
- nrewrite > H;
- nelim e2;
+ #u1; #dim1;
+ #y; nelim y;
+ #u2; #dim2;
+ #P;
+ nchange with (? → (match eq_nat u1 u2 with [ true ⇒ P → P | false ⇒ P ]));
+ #H;
+ nrewrite > (SUN_destruct_1 l … H);
+ nrewrite > (eq_to_eqnat u2 u2 (refl_eq …));
nnormalize;
- napply refl_eq.
+ napply (λx.x).
nqed.
+(* eq_to_eqxx universale *)
nlemma eq_to_eqSUN : ∀l.∀x,y:S_UN l.x = y → eq_SUN l x y = true.
#l; #x; nelim x;
- ##[ ##2: #F; nelim F
- ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
- ##[ ##2: #F; nelim F
- ##| ##1: #u2; #dim21; #dim22;
- nchange with (? → eq_UN u1 u2 = true);
- #H; napply (eq_to_eqUN u1 u2);
- napply (SUN_destruct_1 l … H)
- ##]
- ##]
-nqed.
-
-nlemma neqUN_to_neq : ∀e1,e2.eq_UN e1 e2 = false → e1 ≠ e2.
- #e1; #e2; #H;
- napply (not_to_not (e1 = e2) (eq_UN e1 e2 = true) …);
- ##[ ##1: napply (eq_to_eqUN e1 e2)
- ##| ##2: napply (eqfalse_to_neqtrue … H)
- ##]
+ #u1; #dim1;
+ #y; nelim y;
+ #u2; #dim2;
+ nchange with (? → eq_nat u1 u2 = true);
+ #H; napply (eq_to_eqnat u1 u2);
+ napply (SUN_destruct_1 l … H).
nqed.
+(* neqxx_to_neq universale *)
nlemma neqSUN_to_neq : ∀l.∀x,y:S_UN l.eq_SUN l x y = false → x ≠ y.
- #l; #x; nelim x;
- ##[ ##2: #F; nelim F
- ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
- ##[ ##2: #F; nelim F
- ##| ##1: #u2; #dim21; #dim22;
- nchange with ((eq_UN u1 u2 = false) → ?);
- #H; nnormalize; #H1;
- napply (neqUN_to_neq u1 u2 H);
- napply (SUN_destruct_1 l … H1)
- ##]
- ##]
-nqed.
-
-naxiom SUN_construct
- : ∀l.∀u.
- ∀dim11,dim21:(member_list UN u eq_UN l = true).
- ∀dim12,dim22:(∀y0.(eq_UN u y0 = true) → (u = y0)).
- ((S_EL l u dim11 dim12) = (S_EL l u dim21 dim22)).
-
-nlemma eqgetelem_to_eq : ∀l.∀x,y:S_UN l.(getelem ? x) = (getelem ? y) → x = y.
- #l; #x; nelim x;
- ##[ ##2: #F; nelim F
- ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
- ##[ ##2: #F; nelim F
- ##| ##1: #u2; #dim21; #dim22;
- nchange with (u1 = u2 → ?); #H;
- nrewrite > H in dim11:(%) dim12:(%) ⊢ %; #dim11; #dim12;
- napply (SUN_construct l u2 dim11 dim21 dim12 dim22);
- ##]
+ #l; #n1; #n2; #H;
+ napply (not_to_not (n1 = n2) (eq_SUN l n1 n2 = true) …);
+ ##[ ##1: napply (eq_to_eqSUN l n1 n2)
+ ##| ##2: napply (eqfalse_to_neqtrue … H)
##]
nqed.
-nlemma neq_to_neqgetelem : ∀l.∀x,y:S_UN l.x ≠ y → (getelem ? x) ≠ (getelem ? y).
- #l; #x; nelim x;
- ##[ ##2: #F; nelim F
- ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
- ##[ ##2: #F; nelim F
- ##| ##1: #u2; #dim21; #dim22; #H;
- napply (not_to_not ((getelem l ?) = (getelem l ?))
- ((S_EL l u1 dim11 dim12) = (S_EL l u2 dim21 dim22)) ?);
- ##[ ##1: napply H
- ##| ##2: napply (eqgetelem_to_eq l …)
- ##]
- ##]
- ##]
-nqed.
+(* eqxx_to_eq universale *)
+(* !!! evidente ma come si fa? *)
+naxiom eqSUN_to_eq_aux : ∀l,x,y.((getelem l x) = (getelem l y)) → x = y.
nlemma eqSUN_to_eq : ∀l.∀x,y:S_UN l.eq_SUN l x y = true → x = y.
- #l; #x; nelim x;
- ##[ ##2: #F; nelim F
- ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
- ##[ ##2: #F; nelim F
- ##| ##1: #u2; #dim21; #dim22;
- nchange with ((eq_UN u1 u2 = true) → ?); #H;
- nrewrite > (eqgetelem_to_eq l (S_EL l u1 dim11 dim12) (S_EL l u2 dim21 dim22) (dim12 u2 H));
- napply refl_eq
- ##]
- ##]
+ #l; #x; #y;
+ nchange with ((eq_nat (getelem ? x) (getelem ? y) = true) → x = y);
+ #H; napply (eqSUN_to_eq_aux l x y (eqnat_to_eq … H)).
nqed.
+(* neq_to_neqxx universale *)
nlemma neq_to_neqSUN : ∀l.∀x,y:S_UN l.x ≠ y → eq_SUN l x y = false.
- #l; #x; nelim x;
- ##[ ##2: #F; nelim F
- ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
- ##[ ##2: #F; nelim F
- ##| ##1: #u2; #dim21; #dim22; #H;
- napply neqtrue_to_eqfalse;
- napply (not_to_not ?? (eqSUN_to_eq l ??) ?) ;
- napply H
- ##]
- ##]
+ #l; #n1; #n2; #H;
+ napply (neqtrue_to_eqfalse (eq_SUN l n1 n2));
+ napply (not_to_not (eq_SUN l n1 n2 = true) (n1 = n2) ? H);
+ napply (eqSUN_to_eq l n1 n2).
nqed.
+(* decidibilita' universale *)
nlemma decidable_SUN : ∀l.∀x,y:S_UN l.decidable (x = y).
- #l; #x; nelim x;
- ##[ ##2: #F; nelim F
- ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
- ##[ ##2: #F; nelim F
- ##| ##1: #u2; #dim21; #dim22; nnormalize;
- napply (or2_elim … (decidable_bexpr (eq_SUN l (S_EL l u1 dim11 dim12) (S_EL l u2 dim21 dim22))));
- ##[ ##1: #H; napply (or2_intro1 (? = ?) (? ≠ ?) (eqSUN_to_eq l … H))
- ##| ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) (neqSUN_to_neq l … H))
+ #l; #x; #y; nnormalize;
+ napply (or2_elim (eq_SUN l x y = true) (eq_SUN l x y = false) ? (decidable_bexpr ?));
+ ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqSUN_to_eq l … H))
+ ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqSUN_to_neq l … H))
##]
nqed.
+(* simmetria di uguaglianza universale *)
nlemma symmetric_eqSUN : ∀l.symmetricT (S_UN l) bool (eq_SUN l).
- #l; #x; nelim x;
- ##[ ##2: #F; nelim F
- ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
- ##[ ##2: #F; nelim F
- ##| ##1: #u2; #dim21; #dim22;
- napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_SUN l (S_EL l u1 dim11 dim12) (S_EL l u2 dim21 dim22)));
+ #l; #n1; #n2;
+ napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_SUN l n1 n2));
##[ ##1: #H; nrewrite > H; napply refl_eq
- ##| ##2: #H; nrewrite > (neq_to_neqSUN l … H);
- napply (symmetric_eq ? (eq_SUN l ??) false);
- napply (neq_to_neqSUN l … (symmetric_neq … H))
+ ##| ##2: #H; nrewrite > (neq_to_neqSUN l n1 n2 H);
+ napply (symmetric_eq ? (eq_SUN l n2 n1) false);
+ napply (neq_to_neqSUN l n2 n1 (symmetric_neq ? n1 n2 H))
##]
nqed.
+
+(* scheletro di funzione generica ad 1 argomento *)
+nlet rec farg1_auxT (T:Type) (l:ne_list nat) on l ≝
+ match l with
+ [ ne_nil _ ⇒ T
+ | ne_cons _ t ⇒ ProdT T (farg1_auxT T t)
+ ].
+
+nlemma farg1_auxDim : ∀h,t,x.eq_nat x h = false → member_natList x (h§§t) = true → member_natList x t = true.
+ #h; #t; #x; #H; #H1;
+ nnormalize in H1:(%);
+ nrewrite > H in H1:(%);
+ nnormalize;
+ napply (λx.x).
+nqed.
+
+nlet rec farg1 (T:Type) (l:ne_list nat) on l ≝
+ match l with
+ [ ne_nil h ⇒ λarg:farg1_auxT T «£h».λx:S_UN «£h».arg
+ | ne_cons h t ⇒ λarg:farg1_auxT T (h§§t).λx:S_UN (h§§t).
+ match eq_nat (getelem ? x) h
+ return λy.eq_nat (getelem ? x) h = y → ?
+ with
+ [ true ⇒ λp:(eq_nat (getelem ? x) h = true).fst … arg
+ | false ⇒ λp:(eq_nat (getelem ? x) h = false).
+ farg1 T t
+ (snd … arg)
+ (S_EL t (getelem ? x) (farg1_auxDim h t (getelem ? x) p (getdim ? x)))
+ ] (refl_eq ? (eq_nat (getelem ? x) h))
+ ].
+
+(* scheletro di funzione generica a 2 argomenti *)
+nlet rec farg2 (T:Type) (l,lfix:ne_list nat) on l ≝
+ match l with
+ [ ne_nil h ⇒ λarg:farg1_auxT (farg1_auxT T lfix) «£h».λx:S_UN «£h».farg1 T lfix arg
+ | ne_cons h t ⇒ λarg:farg1_auxT (farg1_auxT T lfix) (h§§t).λx:S_UN (h§§t).
+ match eq_nat (getelem ? x) h
+ return λy.eq_nat (getelem ? x) h = y → ?
+ with
+ [ true ⇒ λp:(eq_nat (getelem ? x) h = true).farg1 T lfix (fst … arg)
+ | false ⇒ λp:(eq_nat (getelem ? x) h = false).
+ farg2 T t lfix
+ (snd … arg)
+ (S_EL t (getelem ? x) (farg1_auxDim h t (getelem ? x) p (getdim ? x)))
+ ] (refl_eq ? (eq_nat (getelem ? x) h))
+ ].
+
+(* esempio0: universo ottale *)
+ndefinition oct0 ≝ O.
+ndefinition oct1 ≝ nat1.
+ndefinition oct2 ≝ nat2.
+ndefinition oct3 ≝ nat3.
+ndefinition oct4 ≝ nat4.
+ndefinition oct5 ≝ nat5.
+ndefinition oct6 ≝ nat6.
+ndefinition oct7 ≝ nat7.
+
+ndefinition oct_UN ≝ « oct0 ; oct1 ; oct2 ; oct3 ; oct4 ; oct5 ; oct6 £ oct7 ».
+
+ndefinition uoct0 ≝ S_EL oct_UN oct0 (refl_eq …).
+ndefinition uoct1 ≝ S_EL oct_UN oct1 (refl_eq …).
+ndefinition uoct2 ≝ S_EL oct_UN oct2 (refl_eq …).
+ndefinition uoct3 ≝ S_EL oct_UN oct3 (refl_eq …).
+ndefinition uoct4 ≝ S_EL oct_UN oct4 (refl_eq …).
+ndefinition uoct5 ≝ S_EL oct_UN oct5 (refl_eq …).
+ndefinition uoct6 ≝ S_EL oct_UN oct6 (refl_eq …).
+ndefinition uoct7 ≝ S_EL oct_UN oct7 (refl_eq …).
+
+(* esempio1: NOT ottale *)
+ndefinition octNOT ≝
+ farg1 (S_UN oct_UN) oct_UN
+ (pair … uoct7 (pair … uoct6 (pair … uoct5 (pair … uoct4 (pair … uoct3 (pair … uoct2 (pair … uoct1 uoct0))))))).
+
+(* esempio2: AND ottale *)
+ndefinition octAND0 ≝ pair … uoct0 (pair … uoct0 (pair … uoct0 (pair … uoct0 (pair … uoct0 (pair … uoct0 (pair … uoct0 uoct0)))))).
+ndefinition octAND1 ≝ pair … uoct0 (pair … uoct1 (pair … uoct0 (pair … uoct1 (pair … uoct0 (pair … uoct1 (pair … uoct0 uoct1)))))).
+ndefinition octAND2 ≝ pair … uoct0 (pair … uoct0 (pair … uoct2 (pair … uoct2 (pair … uoct0 (pair … uoct0 (pair … uoct2 uoct2)))))).
+ndefinition octAND3 ≝ pair … uoct0 (pair … uoct1 (pair … uoct2 (pair … uoct3 (pair … uoct0 (pair … uoct1 (pair … uoct2 uoct3)))))).
+ndefinition octAND4 ≝ pair … uoct0 (pair … uoct0 (pair … uoct0 (pair … uoct0 (pair … uoct4 (pair … uoct4 (pair … uoct4 uoct4)))))).
+ndefinition octAND5 ≝ pair … uoct0 (pair … uoct1 (pair … uoct0 (pair … uoct1 (pair … uoct4 (pair … uoct5 (pair … uoct4 uoct5)))))).
+ndefinition octAND6 ≝ pair … uoct0 (pair … uoct0 (pair … uoct2 (pair … uoct2 (pair … uoct4 (pair … uoct4 (pair … uoct6 uoct6)))))).
+ndefinition octAND7 ≝ pair … uoct0 (pair … uoct1 (pair … uoct2 (pair … uoct3 (pair … uoct4 (pair … uoct5 (pair … uoct6 uoct7)))))).
+
+ndefinition octAND ≝
+ farg2 (S_UN oct_UN) oct_UN oct_UN
+ (pair … octAND0 (pair … octAND1 (pair … octAND2 (pair … octAND3 (pair … octAND4 (pair … octAND5 (pair … octAND6 octAND7))))))).
+
+(* ora e' possibile fare
+ octNOT uoctX
+ octAND uoctX uoctY
+*)
projects / helm.git / blobdiff