From: Cosimo Oliboni Date: Thu, 23 Jul 2009 12:13:26 +0000 (+0000) Subject: freescale porting, work in progress X-Git-Tag: make_still_working~3628 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dc74ed7c4af1aa9b90fc5d2f0a86bd7825696e71;p=helm.git freescale porting, work in progress --- diff --git a/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma b/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma index d972fe0ba..1fa93ce72 100755 --- a/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma +++ b/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma @@ -33,107 +33,62 @@ ninductive ast_base_type : Type ≝ | AST_BASE_TYPE_WORD16: ast_base_type | AST_BASE_TYPE_WORD32: ast_base_type. -(*ndefinition ast_base_type_ind - : ΠP:ast_base_type → Prop.P AST_BASE_TYPE_BYTE8 → P AST_BASE_TYPE_WORD16 → P AST_BASE_TYPE_WORD32 → - Πa:ast_base_type.P a ≝ -λP:ast_base_type → Prop.λp:P AST_BASE_TYPE_BYTE8.λp1:P AST_BASE_TYPE_WORD16.λp2:P AST_BASE_TYPE_WORD32. -λa:ast_base_type. - match a with [ AST_BASE_TYPE_BYTE8 ⇒ p | AST_BASE_TYPE_WORD16 ⇒ p1 | AST_BASE_TYPE_WORD32 ⇒ p2 ]. - -ndefinition ast_base_type_rec - : ΠP:ast_base_type → Set.P AST_BASE_TYPE_BYTE8 → P AST_BASE_TYPE_WORD16 → P AST_BASE_TYPE_WORD32 → - Πa:ast_base_type.P a ≝ -λP:ast_base_type → Set.λp:P AST_BASE_TYPE_BYTE8.λp1:P AST_BASE_TYPE_WORD16.λp2:P AST_BASE_TYPE_WORD32. -λa:ast_base_type. - match a with [ AST_BASE_TYPE_BYTE8 ⇒ p | AST_BASE_TYPE_WORD16 ⇒ p1 | AST_BASE_TYPE_WORD32 ⇒ p2 ]. - -ndefinition ast_base_type_rect - : ΠP:ast_base_type → Type.P AST_BASE_TYPE_BYTE8 → P AST_BASE_TYPE_WORD16 → P AST_BASE_TYPE_WORD32 → - Πa:ast_base_type.P a ≝ -λP:ast_base_type → Type.λp:P AST_BASE_TYPE_BYTE8.λp1:P AST_BASE_TYPE_WORD16.λp2:P AST_BASE_TYPE_WORD32. -λa:ast_base_type. - match a with [ AST_BASE_TYPE_BYTE8 ⇒ p | AST_BASE_TYPE_WORD16 ⇒ p1 | AST_BASE_TYPE_WORD32 ⇒ p2 ]. -*) ninductive ast_type : Type ≝ AST_TYPE_BASE: ast_base_type → ast_type | AST_TYPE_ARRAY: ast_type → nat → ast_type | AST_TYPE_STRUCT: ne_list ast_type → ast_type. -nlet rec ast_type_ind_aux (P:ast_type → Prop) - (f:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t))) - (f1:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t))) - (f2:Πt.P t) - (t:ne_list ast_type) on t ≝ +(* principio di eliminazione arricchito *) +nlet rec ast_type_index_aux (P:ast_type → Prop) + (f:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t))) + (f1:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t))) + (f2:Πt.P t) + (t:ne_list ast_type) on t ≝ match t return λt.P (AST_TYPE_STRUCT t) with [ ne_nil h ⇒ f h (f2 h) - | ne_cons h t ⇒ f1 h t (f2 h) (ast_type_ind_aux P f f1 f2 t) + | ne_cons h t ⇒ f1 h t (f2 h) (ast_type_index_aux P f f1 f2 t) ]. -(*nlet rec ast_type_ind (P:ast_type → Prop) - (f:Πb.P (AST_TYPE_BASE b)) - (f1:Πt,n.P t → P (AST_TYPE_ARRAY t n)) - (f2:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t))) - (f3:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t))) - (t:ast_type) on t : P t ≝ +nlet rec ast_type_index (P:ast_type → Prop) + (f:Πb.P (AST_TYPE_BASE b)) + (f1:Πt,n.P t → P (AST_TYPE_ARRAY t n)) + (f2:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t))) + (f3:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t))) + (t:ast_type) on t : P t ≝ match t return λt.P t with [ AST_TYPE_BASE b ⇒ f b - | AST_TYPE_ARRAY t' n ⇒ f1 t' n (ast_type_ind P f f1 f2 f3 t') + | AST_TYPE_ARRAY t' n ⇒ f1 t' n (ast_type_index P f f1 f2 f3 t') | AST_TYPE_STRUCT nl ⇒ match nl with - [ ne_nil h ⇒ f2 h (ast_type_ind P f f1 f2 f3 h) - | ne_cons h t ⇒ f3 h t (ast_type_ind P f f1 f2 f3 h) (ast_type_ind_aux P f2 f3 (ast_type_ind P f f1 f2 f3) t) + [ ne_nil h ⇒ f2 h (ast_type_index P f f1 f2 f3 h) + | ne_cons h t ⇒ f3 h t (ast_type_index P f f1 f2 f3 h) (ast_type_index_aux P f2 f3 (ast_type_index P f f1 f2 f3) t) ] ]. -nlet rec ast_type_rec_aux (P:ast_type → Type[0]) - (f:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t))) - (f1:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t))) - (f2:Πt.P t) - (t:ne_list ast_type) on t ≝ +nlet rec ast_type_rectex_aux (P:ast_type → Type) + (f:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t))) + (f1:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t))) + (f2:Πt.P t) + (t:ne_list ast_type) on t ≝ match t return λt.P (AST_TYPE_STRUCT t) with [ ne_nil h ⇒ f h (f2 h) - | ne_cons h t ⇒ f1 h t (f2 h) (ast_type_rec_aux P f f1 f2 t) + | ne_cons h t ⇒ f1 h t (f2 h) (ast_type_rectex_aux P f f1 f2 t) ]. -nlet rec ast_type_rec (P:ast_type → Set) - (f:Πb.P (AST_TYPE_BASE b)) - (f1:Πt,n.P t → P (AST_TYPE_ARRAY t n)) - (f2:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t))) - (f3:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t))) - (t:ast_type) on t : P t ≝ +nlet rec ast_type_rectex (P:ast_type → Type) + (f:Πb.P (AST_TYPE_BASE b)) + (f1:Πt,n.P t → P (AST_TYPE_ARRAY t n)) + (f2:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t))) + (f3:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t))) + (t:ast_type) on t : P t ≝ match t return λt.P t with [ AST_TYPE_BASE b ⇒ f b - | AST_TYPE_ARRAY t' n ⇒ f1 t' n (ast_type_rec P f f1 f2 f3 t') + | AST_TYPE_ARRAY t' n ⇒ f1 t' n (ast_type_rectex P f f1 f2 f3 t') | AST_TYPE_STRUCT nl ⇒ match nl with - [ ne_nil h ⇒ f2 h (ast_type_rec P f f1 f2 f3 h) - | ne_cons h t ⇒ f3 h t (ast_type_rec P f f1 f2 f3 h) (ast_type_rec_aux P f2 f3 (ast_type_rec P f f1 f2 f3) t) + [ ne_nil h ⇒ f2 h (ast_type_rectex P f f1 f2 f3 h) + | ne_cons h t ⇒ f3 h t (ast_type_rectex P f f1 f2 f3 h) (ast_type_rectex_aux P f2 f3 (ast_type_rectex P f f1 f2 f3) t) ] ]. -nlet rec ast_type_rect_aux (P:ast_type → Type) - (f:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t))) - (f1:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t))) - (f2:Πt.P t) - (t:ne_list ast_type) on t ≝ - match t return λt.P (AST_TYPE_STRUCT t) with - [ ne_nil h ⇒ f h (f2 h) - | ne_cons h t ⇒ f1 h t (f2 h) (ast_type_rect_aux P f f1 f2 t) - ]. - -nlet rec ast_type_rect (P:ast_type → Type) - (f:Πb.P (AST_TYPE_BASE b)) - (f1:Πt,n.P t → P (AST_TYPE_ARRAY t n)) - (f2:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t))) - (f3:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t))) - (t:ast_type) on t : P t ≝ - match t return λt.P t with - [ AST_TYPE_BASE b ⇒ f b - | AST_TYPE_ARRAY t' n ⇒ f1 t' n (ast_type_rect P f f1 f2 f3 t') - | AST_TYPE_STRUCT nl ⇒ match nl with - [ ne_nil h ⇒ f2 h (ast_type_rect P f f1 f2 f3 h) - | ne_cons h t ⇒ f3 h t (ast_type_rect P f f1 f2 f3 h) (ast_type_rect_aux P f2 f3 (ast_type_rect P f f1 f2 f3) t) - ] - ]. -*) ndefinition eq_ast_base_type ≝ λt1,t2:ast_base_type.match t1 with [ AST_BASE_TYPE_BYTE8 ⇒ match t2 with @@ -153,16 +108,7 @@ nlet rec eq_ast_type (t1,t2:ast_type) on t1 ≝ [ AST_TYPE_ARRAY subType2 dim2 ⇒ (eq_ast_type subType1 subType2) ⊗ (eq_nat dim1 dim2) | _ ⇒ false ] | AST_TYPE_STRUCT nelSubType1 ⇒ match t2 with - [ AST_TYPE_STRUCT nelSubType2 ⇒ - match eq_nat (len_neList ? nelSubType1) (len_neList ? nelSubType2) - return λx.eq_nat (len_neList ? nelSubType1) (len_neList ? nelSubType2) = x → bool - with - [ true ⇒ λp:(eq_nat (len_neList ? nelSubType1) (len_neList ? nelSubType2) = true). - fold_right_neList2 ?? (λx1,x2,acc.(eq_ast_type x1 x2)⊗acc) - true nelSubType1 nelSubType2 - (eqnat_to_eq (len_neList ? nelSubType1) (len_neList ? nelSubType2) p) - | false ⇒ λp:(eq_nat (len_neList ? nelSubType1) (len_neList ? nelSubType2) = false).false - ] (refl_eq ? (eq_nat (len_neList ? nelSubType1) (len_neList ? nelSubType2))) + [ AST_TYPE_STRUCT nelSubType2 ⇒ bfold_right_neList2 ? (λx1,x2.eq_ast_type x1 x2) nelSubType1 nelSubType2 | _ ⇒ false ] ]. diff --git a/helm/software/matita/contribs/ng_assembly/compiler/ast_type_lemmas.ma b/helm/software/matita/contribs/ng_assembly/compiler/ast_type_lemmas.ma index 99f0f1b12..d7948c386 100755 --- a/helm/software/matita/contribs/ng_assembly/compiler/ast_type_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/compiler/ast_type_lemmas.ma @@ -41,17 +41,17 @@ ndefinition astbasetype_destruct : astbasetype_destruct_aux. nnormalize; #H; ##[ ##1,5,9: napply (λx:P.x) - ##| ##2,3: napply (False_ind ??); + ##| ##2,3: napply (False_ind (λ_.?) ?); nchange with (match AST_BASE_TYPE_BYTE8 with [ AST_BASE_TYPE_BYTE8 ⇒ False | _ ⇒ True]); nrewrite > H; nnormalize; napply I - ##| ##4,6: napply (False_ind ??); + ##| ##4,6: napply (False_ind (λ_.?) ?); nchange with (match AST_BASE_TYPE_WORD16 with [ AST_BASE_TYPE_WORD16 ⇒ False | _ ⇒ True]); nrewrite > H; nnormalize; napply I - ##| ##7,8: napply (False_ind ??); + ##| ##7,8: napply (False_ind (λ_.?) ?); nchange with (match AST_BASE_TYPE_WORD32 with [ AST_BASE_TYPE_WORD32 ⇒ False | _ ⇒ True]); nrewrite > H; nnormalize; @@ -132,7 +132,7 @@ ndefinition asttype_destruct : asttype_destruct_aux. ##| ##2: #t; #n; #b; nnormalize; #H ##| ##3: #l; #b; nnormalize; #H ##] - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match AST_TYPE_BASE b with [ AST_TYPE_BASE _ ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##2: ncases b2; @@ -140,7 +140,7 @@ ndefinition asttype_destruct : asttype_destruct_aux. ##| ##1: #b; #t; #n; nnormalize; #H ##| ##3: #l; #t; #n; nnormalize; #H ##] - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match AST_TYPE_ARRAY t n with [ AST_TYPE_ARRAY _ _ ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##3: ncases b2; @@ -148,13 +148,63 @@ ndefinition asttype_destruct : asttype_destruct_aux. ##| ##1: #b; #l; nnormalize; #H ##| ##2: #t; #n; #l; nnormalize; #H ##] - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match AST_TYPE_STRUCT l with [ AST_TYPE_STRUCT _ ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. -(* eq_ast lemmas missing *) +nlemma symmetric_eqasttype_aux1 + : ∀nl1,nl2. + (eq_ast_type (AST_TYPE_STRUCT nl1) (AST_TYPE_STRUCT nl2)) = (eq_ast_type (AST_TYPE_STRUCT nl2) (AST_TYPE_STRUCT nl1)) → + (bfold_right_neList2 ? (λx,y.eq_ast_type x y) nl1 nl2) = (bfold_right_neList2 ? (λx,y.eq_ast_type x y) nl2 nl1). + #nl1; #nl2; #H; + napply H. +nqed. + +nlemma symmetric_eqasttype : symmetricT ast_type bool eq_ast_type. + #t1; napply (ast_type_index ????? t1); + ##[ ##1: #b1; #t2; ncases t2; + ##[ ##1: #b2; nchange with ((eq_ast_base_type b1 b2) = (eq_ast_base_type b2 b1)); + nrewrite > (symmetric_eqastbasetype b1 b2); + napply (refl_eq ??) + ##| ##2: #st2; #n2; nnormalize; napply (refl_eq ??) + ##| ##3: #nl2; nnormalize; napply (refl_eq ??) + ##] + ##| ##2: #st1; #n1; #H; #t2; ncases t2; + ##[ ##2: #st2; #n2; nchange with (((eq_ast_type st1 st2)⊗(eq_nat n1 n2)) = ((eq_ast_type st2 st1)⊗(eq_nat n2 n1))); + nrewrite > (symmetric_eqnat n1 n2); + nrewrite > (H st2); + napply (refl_eq ??) + ##| ##1: #b2; nnormalize; napply (refl_eq ??) + ##| ##3: #nl2; nnormalize; napply (refl_eq ??) + ##] + ##| ##3: #hh1; #H; #t2; ncases t2; + ##[ ##3: #nl2; ncases nl2; + ##[ ##1: #hh2; nchange with ((eq_ast_type hh1 hh2) = (eq_ast_type hh2 hh1)); + nrewrite > (H hh2); + napply (refl_eq ??) + ##| ##2: #hh2; #ll2; nnormalize; napply (refl_eq ??) + ##] + ##| ##1: #b2; nnormalize; napply (refl_eq ??) + ##| ##2: #st2; #n2; nnormalize; napply (refl_eq ??) + ##] + ##| ##4: #hh1; #ll1; #H; #H1; #t2; ncases t2; + ##[ ##3: #nl2; ncases nl2; + ##[ ##1: #hh2; nnormalize; napply (refl_eq ??) + ##| ##2: #hh2; #ll2; nnormalize; + nrewrite > (H hh2); + nrewrite > (symmetric_eqasttype_aux1 ll1 ll2 (H1 (AST_TYPE_STRUCT ll2))); + napply (refl_eq ??) + ##] + ##| ##1: #b2; nnormalize; napply (refl_eq ??) + ##| ##2: #st2; #n2; nnormalize; napply (refl_eq ??) + ##] + ##] +nqed. + +... + nlemma isbastbasetype_to_isastbasetype : ∀ast.isb_ast_base_type ast = true → is_ast_base_type ast. #ast; diff --git a/helm/software/matita/contribs/ng_assembly/freescale/aux_bases.ma b/helm/software/matita/contribs/ng_assembly/freescale/aux_bases.ma index 58898142d..1d49e79c5 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/aux_bases.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/aux_bases.ma @@ -37,27 +37,6 @@ ninductive oct : Type ≝ | o6: oct | o7: oct. -(*ndefinition oct_ind : - ΠP:oct → Prop.P o0 → P o1 → P o2 → P o3 → P o4 → P o5 → P o6 → P o7 → Πn:oct.P n ≝ -λP:oct → Prop. -λp:P o0.λp1:P o1.λp2:P o2.λp3:P o3.λp4:P o4.λp5:P o5.λp6:P o6.λp7:P o7.λn:oct. - match n with - [ o0 ⇒ p | o1 ⇒ p1 | o2 ⇒ p2 | o3 ⇒ p3 | o4 ⇒ p4 | o5 ⇒ p5 | o6 ⇒ p6 | o7 ⇒ p7 ]. - -ndefinition oct_rec : - ΠP:oct → Set.P o0 → P o1 → P o2 → P o3 → P o4 → P o5 → P o6 → P o7 → Πn:oct.P n ≝ -λP:oct → Set. -λp:P o0.λp1:P o1.λp2:P o2.λp3:P o3.λp4:P o4.λp5:P o5.λp6:P o6.λp7:P o7.λn:oct. - match n with - [ o0 ⇒ p | o1 ⇒ p1 | o2 ⇒ p2 | o3 ⇒ p3 | o4 ⇒ p4 | o5 ⇒ p5 | o6 ⇒ p6 | o7 ⇒ p7 ]. - -ndefinition oct_rect : - ΠP:oct → Type.P o0 → P o1 → P o2 → P o3 → P o4 → P o5 → P o6 → P o7 → Πn:oct.P n ≝ -λP:oct → Type. -λp:P o0.λp1:P o1.λp2:P o2.λp3:P o3.λp4:P o4.λp5:P o5.λp6:P o6.λp7:P o7.λn:oct. - match n with - [ o0 ⇒ p | o1 ⇒ p1 | o2 ⇒ p2 | o3 ⇒ p3 | o4 ⇒ p4 | o5 ⇒ p5 | o6 ⇒ p6 | o7 ⇒ p7 ]. -*) (* operatore = *) ndefinition eq_oct ≝ λn1,n2:oct. @@ -136,54 +115,6 @@ ninductive bitrigesim : Type ≝ | t1E: bitrigesim | t1F: bitrigesim. -(*ndefinition bitrigesim_ind : - ΠP:bitrigesim → Prop.P t00 → P t01 → P t02 → P t03 → P t04 → P t05 → P t06 → P t07 → - P t08 → P t09 → P t0A → P t0B → P t0C → P t0D → P t0E → P t0F → - P t10 → P t11 → P t12 → P t13 → P t14 → P t15 → P t16 → P t17 → - P t18 → P t19 → P t1A → P t1B → P t1C → P t1D → P t1E → P t1F → Πt:bitrigesim.P t ≝ -λP:bitrigesim → Prop. -λp:P t00.λp1:P t01.λp2:P t02.λp3:P t03.λp4:P t04.λp5:P t05.λp6:P t06.λp7:P t07. -λp8:P t08.λp9:P t09.λp10:P t0A.λp11:P t0B.λp12:P t0C.λp13:P t0D.λp14:P t0E.λp15:P t0F. -λp16:P t10.λp17:P t11.λp18:P t12.λp19:P t13.λp20:P t14.λp21:P t15.λp22:P t16.λp23:P t17. -λp24:P t18.λp25:P t19.λp26:P t1A.λp27:P t1B.λp28:P t1C.λp29:P t1D.λp30:P t1E.λp31:P t1F.λt:bitrigesim. - match t with - [ t00 ⇒ p | t01 ⇒ p1 | t02 ⇒ p2 | t03 ⇒ p3 | t04 ⇒ p4 | t05 ⇒ p5 | t06 ⇒ p6 | t07 ⇒ p7 - | t08 ⇒ p8 | t09 ⇒ p9 | t0A ⇒ p10 | t0B ⇒ p11 | t0C ⇒ p12 | t0D ⇒ p13 | t0E ⇒ p14 | t0F ⇒ p15 - | t10 ⇒ p16 | t11 ⇒ p17 | t12 ⇒ p18 | t13 ⇒ p19 | t14 ⇒ p20 | t15 ⇒ p21 | t16 ⇒ p22 | t17 ⇒ p23 - | t18 ⇒ p24 | t19 ⇒ p25 | t1A ⇒ p26 | t1B ⇒ p27 | t1C ⇒ p28 | t1D ⇒ p29 | t1E ⇒ p30 | t1F ⇒ p31 ]. - -ndefinition bitrigesim_rec : - ΠP:bitrigesim → Set.P t00 → P t01 → P t02 → P t03 → P t04 → P t05 → P t06 → P t07 → - P t08 → P t09 → P t0A → P t0B → P t0C → P t0D → P t0E → P t0F → - P t10 → P t11 → P t12 → P t13 → P t14 → P t15 → P t16 → P t17 → - P t18 → P t19 → P t1A → P t1B → P t1C → P t1D → P t1E → P t1F → Πt:bitrigesim.P t ≝ -λP:bitrigesim → Set. -λp:P t00.λp1:P t01.λp2:P t02.λp3:P t03.λp4:P t04.λp5:P t05.λp6:P t06.λp7:P t07. -λp8:P t08.λp9:P t09.λp10:P t0A.λp11:P t0B.λp12:P t0C.λp13:P t0D.λp14:P t0E.λp15:P t0F. -λp16:P t10.λp17:P t11.λp18:P t12.λp19:P t13.λp20:P t14.λp21:P t15.λp22:P t16.λp23:P t17. -λp24:P t18.λp25:P t19.λp26:P t1A.λp27:P t1B.λp28:P t1C.λp29:P t1D.λp30:P t1E.λp31:P t1F.λt:bitrigesim. - match t with - [ t00 ⇒ p | t01 ⇒ p1 | t02 ⇒ p2 | t03 ⇒ p3 | t04 ⇒ p4 | t05 ⇒ p5 | t06 ⇒ p6 | t07 ⇒ p7 - | t08 ⇒ p8 | t09 ⇒ p9 | t0A ⇒ p10 | t0B ⇒ p11 | t0C ⇒ p12 | t0D ⇒ p13 | t0E ⇒ p14 | t0F ⇒ p15 - | t10 ⇒ p16 | t11 ⇒ p17 | t12 ⇒ p18 | t13 ⇒ p19 | t14 ⇒ p20 | t15 ⇒ p21 | t16 ⇒ p22 | t17 ⇒ p23 - | t18 ⇒ p24 | t19 ⇒ p25 | t1A ⇒ p26 | t1B ⇒ p27 | t1C ⇒ p28 | t1D ⇒ p29 | t1E ⇒ p30 | t1F ⇒ p31 ]. - -ndefinition bitrigesim_rect : - ΠP:bitrigesim → Type.P t00 → P t01 → P t02 → P t03 → P t04 → P t05 → P t06 → P t07 → - P t08 → P t09 → P t0A → P t0B → P t0C → P t0D → P t0E → P t0F → - P t10 → P t11 → P t12 → P t13 → P t14 → P t15 → P t16 → P t17 → - P t18 → P t19 → P t1A → P t1B → P t1C → P t1D → P t1E → P t1F → Πt:bitrigesim.P t ≝ -λP:bitrigesim → Type. -λp:P t00.λp1:P t01.λp2:P t02.λp3:P t03.λp4:P t04.λp5:P t05.λp6:P t06.λp7:P t07. -λp8:P t08.λp9:P t09.λp10:P t0A.λp11:P t0B.λp12:P t0C.λp13:P t0D.λp14:P t0E.λp15:P t0F. -λp16:P t10.λp17:P t11.λp18:P t12.λp19:P t13.λp20:P t14.λp21:P t15.λp22:P t16.λp23:P t17. -λp24:P t18.λp25:P t19.λp26:P t1A.λp27:P t1B.λp28:P t1C.λp29:P t1D.λp30:P t1E.λp31:P t1F.λt:bitrigesim. - match t with - [ t00 ⇒ p | t01 ⇒ p1 | t02 ⇒ p2 | t03 ⇒ p3 | t04 ⇒ p4 | t05 ⇒ p5 | t06 ⇒ p6 | t07 ⇒ p7 - | t08 ⇒ p8 | t09 ⇒ p9 | t0A ⇒ p10 | t0B ⇒ p11 | t0C ⇒ p12 | t0D ⇒ p13 | t0E ⇒ p14 | t0F ⇒ p15 - | t10 ⇒ p16 | t11 ⇒ p17 | t12 ⇒ p18 | t13 ⇒ p19 | t14 ⇒ p20 | t15 ⇒ p21 | t16 ⇒ p22 | t17 ⇒ p23 - | t18 ⇒ p24 | t19 ⇒ p25 | t1A ⇒ p26 | t1B ⇒ p27 | t1C ⇒ p28 | t1D ⇒ p29 | t1E ⇒ p30 | t1F ⇒ p31 ]. -*) (* operatore = *) ndefinition eq_bitrig ≝ λt1,t2:bitrigesim. diff --git a/helm/software/matita/contribs/ng_assembly/freescale/aux_bases_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/aux_bases_lemmas.ma index 7fdd2dae4..d94c475e5 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/aux_bases_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/aux_bases_lemmas.ma @@ -45,49 +45,49 @@ ndefinition oct_destruct : oct_destruct_aux. nelim n1; ##[ ##1: nelim n2; nnormalize; #H; ##[ ##1: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: 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 ??); + ##| ##*: 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 ??); + ##| ##*: 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 ??); + ##| ##*: 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 ??); + ##| ##*: 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 ??); + ##| ##*: 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 ??); + ##| ##*: 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 ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match o7 with [ o7 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -132,7 +132,7 @@ ndefinition bitrigesim_destruct1 : ncases t2; nnormalize; #H; ##[ ##1: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match t00 with [ t00 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -144,7 +144,7 @@ ndefinition bitrigesim_destruct2 : ncases t2; nnormalize; #H; ##[ ##2: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match t01 with [ t01 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -156,7 +156,7 @@ ndefinition bitrigesim_destruct3 : ncases t2; nnormalize; #H; ##[ ##3: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match t02 with [ t02 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -168,7 +168,7 @@ ndefinition bitrigesim_destruct4 : ncases t2; nnormalize; #H; ##[ ##4: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match t03 with [ t03 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -180,7 +180,7 @@ ndefinition bitrigesim_destruct5 : ncases t2; nnormalize; #H; ##[ ##5: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match t04 with [ t04 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -192,7 +192,7 @@ ndefinition bitrigesim_destruct6 : ncases t2; nnormalize; #H; ##[ ##6: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match t05 with [ t05 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -204,7 +204,7 @@ ndefinition bitrigesim_destruct7 : ncases t2; nnormalize; #H; ##[ ##7: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match t06 with [ t06 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -216,7 +216,7 @@ ndefinition bitrigesim_destruct8 : ncases t2; nnormalize; #H; ##[ ##8: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match t07 with [ t07 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -228,7 +228,7 @@ ndefinition bitrigesim_destruct9 : ncases t2; nnormalize; #H; ##[ ##9: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match t08 with [ t08 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -240,7 +240,7 @@ ndefinition bitrigesim_destruct10 : ncases t2; nnormalize; #H; ##[ ##10: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match t09 with [ t09 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -252,7 +252,7 @@ ndefinition bitrigesim_destruct11 : ncases t2; nnormalize; #H; ##[ ##11: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match t0A with [ t0A ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -264,7 +264,7 @@ ndefinition bitrigesim_destruct12 : ncases t2; nnormalize; #H; ##[ ##12: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match t0B with [ t0B ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -276,7 +276,7 @@ ndefinition bitrigesim_destruct13 : ncases t2; nnormalize; #H; ##[ ##13: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match t0C with [ t0C ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -288,7 +288,7 @@ ndefinition bitrigesim_destruct14 : ncases t2; nnormalize; #H; ##[ ##14: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match t0D with [ t0D ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -300,7 +300,7 @@ ndefinition bitrigesim_destruct15 : ncases t2; nnormalize; #H; ##[ ##15: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match t0E with [ t0E ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -312,7 +312,7 @@ ndefinition bitrigesim_destruct16 : ncases t2; nnormalize; #H; ##[ ##16: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match t0F with [ t0F ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -324,7 +324,7 @@ ndefinition bitrigesim_destruct17 : ncases t2; nnormalize; #H; ##[ ##17: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match t10 with [ t10 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -336,7 +336,7 @@ ndefinition bitrigesim_destruct18 : ncases t2; nnormalize; #H; ##[ ##18: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match t11 with [ t11 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -348,7 +348,7 @@ ndefinition bitrigesim_destruct19 : ncases t2; nnormalize; #H; ##[ ##19: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match t12 with [ t12 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -360,7 +360,7 @@ ndefinition bitrigesim_destruct20 : ncases t2; nnormalize; #H; ##[ ##20: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match t13 with [ t13 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -372,7 +372,7 @@ ndefinition bitrigesim_destruct21 : ncases t2; nnormalize; #H; ##[ ##21: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match t14 with [ t14 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -384,7 +384,7 @@ ndefinition bitrigesim_destruct22 : ncases t2; nnormalize; #H; ##[ ##22: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match t15 with [ t15 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -396,7 +396,7 @@ ndefinition bitrigesim_destruct23 : ncases t2; nnormalize; #H; ##[ ##23: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match t16 with [ t16 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -408,7 +408,7 @@ ndefinition bitrigesim_destruct24 : ncases t2; nnormalize; #H; ##[ ##24: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match t17 with [ t17 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -420,7 +420,7 @@ ndefinition bitrigesim_destruct25 : ncases t2; nnormalize; #H; ##[ ##25: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match t18 with [ t18 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -432,7 +432,7 @@ ndefinition bitrigesim_destruct26 : ncases t2; nnormalize; #H; ##[ ##26: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match t19 with [ t19 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -444,7 +444,7 @@ ndefinition bitrigesim_destruct27 : ncases t2; nnormalize; #H; ##[ ##27: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match t1A with [ t1A ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -456,7 +456,7 @@ ndefinition bitrigesim_destruct28 : ncases t2; nnormalize; #H; ##[ ##28: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match t1B with [ t1B ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -468,7 +468,7 @@ ndefinition bitrigesim_destruct29 : ncases t2; nnormalize; #H; ##[ ##29: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match t1C with [ t1C ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -480,7 +480,7 @@ ndefinition bitrigesim_destruct30 : ncases t2; nnormalize; #H; ##[ ##30: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match t1D with [ t1D ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -492,7 +492,7 @@ ndefinition bitrigesim_destruct31 : ncases t2; nnormalize; #H; ##[ ##31: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match t1E with [ t1E ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -504,7 +504,7 @@ ndefinition bitrigesim_destruct32 : ncases t2; nnormalize; #H; ##[ ##32: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match t1F with [ t1F ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -583,7 +583,7 @@ ndefinition bitrigesim_destruct : bitrigesim_destruct_aux. ##| ##31: napply bitrigesim_destruct31 ##| ##32: napply bitrigesim_destruct32 ##] -nqed. +nqed. nlemma symmetric_eqbitrig : symmetricT bitrigesim bool eq_bitrig. #t1; diff --git a/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma index 87a166d17..a83771253 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma @@ -41,13 +41,11 @@ ndefinition bool_destruct : bool_destruct_aux. nnormalize; #H; ##[ ##2: napply (False_ind (λx.?) ?); - (* perche' non napply (False_ind ??); !!! *) nchange with (match true with [ true ⇒ False | false ⇒ True]); nrewrite > H; nnormalize; napply I ##| ##3: napply (False_ind (λx.?) ?); - (* perche' non napply (False_ind ??); !!! *) nchange with (match true with [ true ⇒ False | false ⇒ True]); nrewrite < H; nnormalize; diff --git a/helm/software/matita/contribs/ng_assembly/freescale/byte8.ma b/helm/software/matita/contribs/ng_assembly/freescale/byte8.ma index ed4a47ea3..896bf6e66 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/byte8.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/byte8.ma @@ -32,21 +32,6 @@ nrecord byte8 : Type ≝ b8l: exadecim }. -(*ndefinition byte8_ind : ΠP:byte8 → Prop.(Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1)) → Πb:byte8.P b ≝ -λP:byte8 → Prop.λf:Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1).λb:byte8. - match b with [ mk_byte8 (e:exadecim) (e1:exadecim) ⇒ f e e1 ]. - -ndefinition byte8_rec : ΠP:byte8 → Set.(Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1)) → Πb:byte8.P b ≝ -λP:byte8 → Set.λf:Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1).λb:byte8. - match b with [ mk_byte8 (e:exadecim) (e1:exadecim) ⇒ f e e1 ]. - -ndefinition byte8_rect : ΠP:byte8 → Type.(Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1)) → Πb:byte8.P b ≝ -λP:byte8 → Type.λf:Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1).λb:byte8. - match b with [ mk_byte8 (e:exadecim) (e1:exadecim) ⇒ f e e1 ]. - -ndefinition b8h ≝ λb:byte8.match b with [ mk_byte8 x _ ⇒ x ]. -ndefinition b8l ≝ λb:byte8.match b with [ mk_byte8 _ x ⇒ x ].*) - (* \langle \rangle *) notation "〈x,y〉" non associative with precedence 80 for @{ 'mk_byte8 $x $y }. diff --git a/helm/software/matita/contribs/ng_assembly/freescale/exadecim_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/exadecim_lemmas.ma index 3726219a8..e6be57877 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/exadecim_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/exadecim_lemmas.ma @@ -30,7 +30,7 @@ include "freescale/exadecim.ma". 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 ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match x0 with [ x0 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -39,7 +39,7 @@ 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 ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match x1 with [ x1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -48,7 +48,7 @@ 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 ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match x2 with [ x2 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -57,7 +57,7 @@ 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 ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match x3 with [ x3 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -66,7 +66,7 @@ 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 ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match x4 with [ x4 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -75,7 +75,7 @@ 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 ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match x5 with [ x5 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -84,7 +84,7 @@ 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 ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match x6 with [ x6 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -93,7 +93,7 @@ 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 ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match x7 with [ x7 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -102,7 +102,7 @@ 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 ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match x8 with [ x8 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -111,7 +111,7 @@ 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 ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match x9 with [ x9 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -120,7 +120,7 @@ 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 ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match xA with [ xA ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -129,7 +129,7 @@ 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 ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match xB with [ xB ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -138,7 +138,7 @@ 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 ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match xC with [ xC ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -147,7 +147,7 @@ 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 ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match xD with [ xD ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -156,7 +156,7 @@ 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 ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match xE with [ xE ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -165,7 +165,7 @@ 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 ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match xF with [ xF ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] diff --git a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base.ma b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base.ma index 41de61f29..74b7cc4e2 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base.ma @@ -35,18 +35,6 @@ ninductive mcu_type: Type ≝ | HCS08 : mcu_type | RS08 : mcu_type. -(*ndefinition mcu_type_ind : ΠP:mcu_type → Prop.P HC05 → P HC08 → P HCS08 → P RS08 → Πm:mcu_type.P m ≝ -λP:mcu_type → Prop.λp:P HC05.λp1:P HC08.λp2:P HCS08.λp3:P RS08.λm:mcu_type. - match m with [ HC05 ⇒ p | HC08 ⇒ p1 | HCS08 ⇒ p2 | RS08 ⇒ p3 ]. - -ndefinition mcu_type_rec : ΠP:mcu_type → Set.P HC05 → P HC08 → P HCS08 → P RS08 → Πm:mcu_type.P m ≝ -λP:mcu_type → Set.λp:P HC05.λp1:P HC08.λp2:P HCS08.λp3:P RS08.λm:mcu_type. - match m with [ HC05 ⇒ p | HC08 ⇒ p1 | HCS08 ⇒ p2 | RS08 ⇒ p3 ]. - -ndefinition mcu_type_rect : ΠP:mcu_type → Type.P HC05 → P HC08 → P HCS08 → P RS08 → Πm:mcu_type.P m ≝ -λP:mcu_type → Type.λp:P HC05.λp1:P HC08.λp2:P HCS08.λp3:P RS08.λm:mcu_type. - match m with [ HC05 ⇒ p | HC08 ⇒ p1 | HCS08 ⇒ p2 | RS08 ⇒ p3 ].*) - ndefinition eq_mcutype ≝ λm1,m2:mcu_type. match m1 with @@ -136,99 +124,6 @@ ninductive instr_mode: Type ≝ | MODE_SRT : bitrigesim → instr_mode . -(*ndefinition instr_mode_ind - : ΠP:instr_mode → Prop. - P MODE_INH → P MODE_INHA → P MODE_INHX → P MODE_INHH → P MODE_INHX0ADD → P MODE_INHX1ADD → - P MODE_INHX2ADD → P MODE_IMM1 → P MODE_IMM1EXT → P MODE_IMM2 → P MODE_DIR1 → P MODE_DIR2 → - P MODE_IX0 → P MODE_IX1 → P MODE_IX2 → P MODE_SP1 → P MODE_SP2 → P MODE_DIR1_to_DIR1 → - P MODE_IMM1_to_DIR1 → P MODE_IX0p_to_DIR1 → P MODE_DIR1_to_IX0p → P MODE_INHA_and_IMM1 → - P MODE_INHX_and_IMM1 → P MODE_IMM1_and_IMM1 → P MODE_DIR1_and_IMM1 → P MODE_IX0_and_IMM1 → - P MODE_IX0p_and_IMM1 → P MODE_IX1_and_IMM1 → P MODE_IX1p_and_IMM1 → P MODE_SP1_and_IMM1 → - (Πd:oct.P (MODE_DIRn d)) → (Πd:oct.P (MODE_DIRn_and_IMM1 d)) → (Πd:exadecim.P (MODE_TNY d)) → - (Πd:bitrigesim.P (MODE_SRT d)) → Πi:instr_mode.P i ≝ -λP:instr_mode → Prop. -λp:P MODE_INH.λp1:P MODE_INHA.λp2:P MODE_INHX.λp3:P MODE_INHH.λp4:P MODE_INHX0ADD.λp5:P MODE_INHX1ADD. -λp6:P MODE_INHX2ADD.λp7:P MODE_IMM1.λp8:P MODE_IMM1EXT.λp9:P MODE_IMM2.λp10:P MODE_DIR1.λp11:P MODE_DIR2. -λp12:P MODE_IX0.λp13:P MODE_IX1.λp14:P MODE_IX2.λp15:P MODE_SP1.λp16:P MODE_SP2.λp17:P MODE_DIR1_to_DIR1. -λp18:P MODE_IMM1_to_DIR1.λp19:P MODE_IX0p_to_DIR1.λp20:P MODE_DIR1_to_IX0p.λp21:P MODE_INHA_and_IMM1. -λp22:P MODE_INHX_and_IMM1.λp23:P MODE_IMM1_and_IMM1.λp24:P MODE_DIR1_and_IMM1.λp25:P MODE_IX0_and_IMM1. -λp26:P MODE_IX0p_and_IMM1.λp27:P MODE_IX1_and_IMM1.λp28:P MODE_IX1p_and_IMM1.λp29:P MODE_SP1_and_IMM1. -λf:Πd:oct.P (MODE_DIRn d).λf1:Πd:oct.P (MODE_DIRn_and_IMM1 d).λf2:Πd:exadecim.P (MODE_TNY d). -λf3:Πd:bitrigesim.P (MODE_SRT d).λi:instr_mode. - match i with - [ MODE_INH ⇒ p | MODE_INHA ⇒ p1 | MODE_INHX ⇒ p2 | MODE_INHH ⇒ p3 | MODE_INHX0ADD ⇒ p4 - | MODE_INHX1ADD ⇒ p5 | MODE_INHX2ADD ⇒ p6 | MODE_IMM1 ⇒ p7 | MODE_IMM1EXT ⇒ p8 - | MODE_IMM2 ⇒ p9 | MODE_DIR1 ⇒ p10 | MODE_DIR2 ⇒ p11 | MODE_IX0 ⇒ p12 | MODE_IX1 ⇒ p13 - | MODE_IX2 ⇒ p14 | MODE_SP1 ⇒ p15 | MODE_SP2 ⇒ p16 | MODE_DIR1_to_DIR1 ⇒ p17 - | MODE_IMM1_to_DIR1 ⇒ p18 | MODE_IX0p_to_DIR1 ⇒ p19 | MODE_DIR1_to_IX0p ⇒ p20 - | MODE_INHA_and_IMM1 ⇒ p21 | MODE_INHX_and_IMM1 ⇒ p22 | MODE_IMM1_and_IMM1 ⇒ p23 - | MODE_DIR1_and_IMM1 ⇒ p24 | MODE_IX0_and_IMM1 ⇒ p25 | MODE_IX0p_and_IMM1 ⇒ p26 - | MODE_IX1_and_IMM1 ⇒ p27 | MODE_IX1p_and_IMM1 ⇒ p28 | MODE_SP1_and_IMM1 ⇒ p29 - | MODE_DIRn (d:oct) ⇒ f d | MODE_DIRn_and_IMM1 (d:oct) ⇒ f1 d | MODE_TNY (d:exadecim) ⇒ f2 d - | MODE_SRT (d:bitrigesim) ⇒ f3 d ]. - -ndefinition instr_mode_rec - : ΠP:instr_mode → Set. - P MODE_INH → P MODE_INHA → P MODE_INHX → P MODE_INHH → P MODE_INHX0ADD → P MODE_INHX1ADD → - P MODE_INHX2ADD → P MODE_IMM1 → P MODE_IMM1EXT → P MODE_IMM2 → P MODE_DIR1 → P MODE_DIR2 → - P MODE_IX0 → P MODE_IX1 → P MODE_IX2 → P MODE_SP1 → P MODE_SP2 → P MODE_DIR1_to_DIR1 → - P MODE_IMM1_to_DIR1 → P MODE_IX0p_to_DIR1 → P MODE_DIR1_to_IX0p → P MODE_INHA_and_IMM1 → - P MODE_INHX_and_IMM1 → P MODE_IMM1_and_IMM1 → P MODE_DIR1_and_IMM1 → P MODE_IX0_and_IMM1 → - P MODE_IX0p_and_IMM1 → P MODE_IX1_and_IMM1 → P MODE_IX1p_and_IMM1 → P MODE_SP1_and_IMM1 → - (Πd:oct.P (MODE_DIRn d)) → (Πd:oct.P (MODE_DIRn_and_IMM1 d)) → (Πd:exadecim.P (MODE_TNY d)) → - (Πd:bitrigesim.P (MODE_SRT d)) → Πi:instr_mode.P i ≝ -λP:instr_mode → Set. -λp:P MODE_INH.λp1:P MODE_INHA.λp2:P MODE_INHX.λp3:P MODE_INHH.λp4:P MODE_INHX0ADD.λp5:P MODE_INHX1ADD. -λp6:P MODE_INHX2ADD.λp7:P MODE_IMM1.λp8:P MODE_IMM1EXT.λp9:P MODE_IMM2.λp10:P MODE_DIR1.λp11:P MODE_DIR2. -λp12:P MODE_IX0.λp13:P MODE_IX1.λp14:P MODE_IX2.λp15:P MODE_SP1.λp16:P MODE_SP2.λp17:P MODE_DIR1_to_DIR1. -λp18:P MODE_IMM1_to_DIR1.λp19:P MODE_IX0p_to_DIR1.λp20:P MODE_DIR1_to_IX0p.λp21:P MODE_INHA_and_IMM1. -λp22:P MODE_INHX_and_IMM1.λp23:P MODE_IMM1_and_IMM1.λp24:P MODE_DIR1_and_IMM1.λp25:P MODE_IX0_and_IMM1. -λp26:P MODE_IX0p_and_IMM1.λp27:P MODE_IX1_and_IMM1.λp28:P MODE_IX1p_and_IMM1.λp29:P MODE_SP1_and_IMM1. -λf:Πd:oct.P (MODE_DIRn d).λf1:Πd:oct.P (MODE_DIRn_and_IMM1 d).λf2:Πd:exadecim.P (MODE_TNY d). -λf3:Πd:bitrigesim.P (MODE_SRT d).λi:instr_mode. - match i with - [ MODE_INH ⇒ p | MODE_INHA ⇒ p1 | MODE_INHX ⇒ p2 | MODE_INHH ⇒ p3 | MODE_INHX0ADD ⇒ p4 - | MODE_INHX1ADD ⇒ p5 | MODE_INHX2ADD ⇒ p6 | MODE_IMM1 ⇒ p7 | MODE_IMM1EXT ⇒ p8 - | MODE_IMM2 ⇒ p9 | MODE_DIR1 ⇒ p10 | MODE_DIR2 ⇒ p11 | MODE_IX0 ⇒ p12 | MODE_IX1 ⇒ p13 - | MODE_IX2 ⇒ p14 | MODE_SP1 ⇒ p15 | MODE_SP2 ⇒ p16 | MODE_DIR1_to_DIR1 ⇒ p17 - | MODE_IMM1_to_DIR1 ⇒ p18 | MODE_IX0p_to_DIR1 ⇒ p19 | MODE_DIR1_to_IX0p ⇒ p20 - | MODE_INHA_and_IMM1 ⇒ p21 | MODE_INHX_and_IMM1 ⇒ p22 | MODE_IMM1_and_IMM1 ⇒ p23 - | MODE_DIR1_and_IMM1 ⇒ p24 | MODE_IX0_and_IMM1 ⇒ p25 | MODE_IX0p_and_IMM1 ⇒ p26 - | MODE_IX1_and_IMM1 ⇒ p27 | MODE_IX1p_and_IMM1 ⇒ p28 | MODE_SP1_and_IMM1 ⇒ p29 - | MODE_DIRn (d:oct) ⇒ f d | MODE_DIRn_and_IMM1 (d:oct) ⇒ f1 d | MODE_TNY (d:exadecim) ⇒ f2 d - | MODE_SRT (d:bitrigesim) ⇒ f3 d ]. - -ndefinition instr_mode_rect - : ΠP:instr_mode → Type. - P MODE_INH → P MODE_INHA → P MODE_INHX → P MODE_INHH → P MODE_INHX0ADD → P MODE_INHX1ADD → - P MODE_INHX2ADD → P MODE_IMM1 → P MODE_IMM1EXT → P MODE_IMM2 → P MODE_DIR1 → P MODE_DIR2 → - P MODE_IX0 → P MODE_IX1 → P MODE_IX2 → P MODE_SP1 → P MODE_SP2 → P MODE_DIR1_to_DIR1 → - P MODE_IMM1_to_DIR1 → P MODE_IX0p_to_DIR1 → P MODE_DIR1_to_IX0p → P MODE_INHA_and_IMM1 → - P MODE_INHX_and_IMM1 → P MODE_IMM1_and_IMM1 → P MODE_DIR1_and_IMM1 → P MODE_IX0_and_IMM1 → - P MODE_IX0p_and_IMM1 → P MODE_IX1_and_IMM1 → P MODE_IX1p_and_IMM1 → P MODE_SP1_and_IMM1 → - (Πd:oct.P (MODE_DIRn d)) → (Πd:oct.P (MODE_DIRn_and_IMM1 d)) → (Πd:exadecim.P (MODE_TNY d)) → - (Πd:bitrigesim.P (MODE_SRT d)) → Πi:instr_mode.P i ≝ -λP:instr_mode → Type. -λp:P MODE_INH.λp1:P MODE_INHA.λp2:P MODE_INHX.λp3:P MODE_INHH.λp4:P MODE_INHX0ADD.λp5:P MODE_INHX1ADD. -λp6:P MODE_INHX2ADD.λp7:P MODE_IMM1.λp8:P MODE_IMM1EXT.λp9:P MODE_IMM2.λp10:P MODE_DIR1.λp11:P MODE_DIR2. -λp12:P MODE_IX0.λp13:P MODE_IX1.λp14:P MODE_IX2.λp15:P MODE_SP1.λp16:P MODE_SP2.λp17:P MODE_DIR1_to_DIR1. -λp18:P MODE_IMM1_to_DIR1.λp19:P MODE_IX0p_to_DIR1.λp20:P MODE_DIR1_to_IX0p.λp21:P MODE_INHA_and_IMM1. -λp22:P MODE_INHX_and_IMM1.λp23:P MODE_IMM1_and_IMM1.λp24:P MODE_DIR1_and_IMM1.λp25:P MODE_IX0_and_IMM1. -λp26:P MODE_IX0p_and_IMM1.λp27:P MODE_IX1_and_IMM1.λp28:P MODE_IX1p_and_IMM1.λp29:P MODE_SP1_and_IMM1. -λf:Πd:oct.P (MODE_DIRn d).λf1:Πd:oct.P (MODE_DIRn_and_IMM1 d).λf2:Πd:exadecim.P (MODE_TNY d). -λf3:Πd:bitrigesim.P (MODE_SRT d).λi:instr_mode. - match i with - [ MODE_INH ⇒ p | MODE_INHA ⇒ p1 | MODE_INHX ⇒ p2 | MODE_INHH ⇒ p3 | MODE_INHX0ADD ⇒ p4 - | MODE_INHX1ADD ⇒ p5 | MODE_INHX2ADD ⇒ p6 | MODE_IMM1 ⇒ p7 | MODE_IMM1EXT ⇒ p8 - | MODE_IMM2 ⇒ p9 | MODE_DIR1 ⇒ p10 | MODE_DIR2 ⇒ p11 | MODE_IX0 ⇒ p12 | MODE_IX1 ⇒ p13 - | MODE_IX2 ⇒ p14 | MODE_SP1 ⇒ p15 | MODE_SP2 ⇒ p16 | MODE_DIR1_to_DIR1 ⇒ p17 - | MODE_IMM1_to_DIR1 ⇒ p18 | MODE_IX0p_to_DIR1 ⇒ p19 | MODE_DIR1_to_IX0p ⇒ p20 - | MODE_INHA_and_IMM1 ⇒ p21 | MODE_INHX_and_IMM1 ⇒ p22 | MODE_IMM1_and_IMM1 ⇒ p23 - | MODE_DIR1_and_IMM1 ⇒ p24 | MODE_IX0_and_IMM1 ⇒ p25 | MODE_IX0p_and_IMM1 ⇒ p26 - | MODE_IX1_and_IMM1 ⇒ p27 | MODE_IX1p_and_IMM1 ⇒ p28 | MODE_SP1_and_IMM1 ⇒ p29 - | MODE_DIRn (d:oct) ⇒ f d | MODE_DIRn_and_IMM1 (d:oct) ⇒ f1 d | MODE_TNY (d:exadecim) ⇒ f2 d - | MODE_SRT (d:bitrigesim) ⇒ f3 d ].*) - ndefinition eq_instrmode ≝ λi1,i2:instr_mode. match i1 with @@ -363,117 +258,6 @@ ninductive opcode: Type ≝ | WAIT : opcode (* !!wait mode!! *) . -(*ndefinition opcode_ind - : ΠP:opcode → Prop. - P ADC → P ADD → P AIS → P AIX → P AND → P ASL → P ASR → P BCC → P BCLRn → P BCS → P BEQ → - P BGE → P BGND → P BGT → P BHCC → P BHCS → P BHI → P BIH → P BIL → P BIT → P BLE → P BLS → - P BLT → P BMC → P BMI → P BMS → P BNE → P BPL → P BRA → P BRCLRn → P BRN → P BRSETn → P BSETn → - P BSR → P CBEQA → P CBEQX → P CLC → P CLI → P CLR → P CMP → P COM → P CPHX → P CPX → P DAA → - P DBNZ → P DEC → P DIV → P EOR → P INC → P JMP → P JSR → P LDA → P LDHX → P LDX → P LSR → P MOV → - P MUL → P NEG → P NOP → P NSA → P ORA → P PSHA → P PSHH → P PSHX → P PULA → P PULH → P PULX → - P ROL → P ROR → P RSP → P RTI → P RTS → P SBC → P SEC → P SEI → P SHA → P SLA → P STA → P STHX → - P STOP → P STX → P SUB → P SWI → P TAP → P TAX → P TPA → P TST → P TSX → P TXA → P TXS → P WAIT → - Πo:opcode.P o ≝ -λP:opcode → Prop. -λp:P ADC.λp1:P ADD.λp2:P AIS.λp3:P AIX.λp4:P AND.λp5:P ASL.λp6:P ASR.λp7:P BCC.λp8:P BCLRn.λp9:P BCS. -λp10:P BEQ.λp11:P BGE.λp12:P BGND.λp13:P BGT.λp14:P BHCC.λp15:P BHCS.λp16:P BHI.λp17:P BIH.λp18:P BIL. -λp19:P BIT.λp20:P BLE.λp21:P BLS.λp22:P BLT.λp23:P BMC.λp24:P BMI.λp25:P BMS.λp26:P BNE.λp27:P BPL. -λp28:P BRA.λp29:P BRCLRn.λp30:P BRN.λp31:P BRSETn.λp32:P BSETn.λp33:P BSR.λp34:P CBEQA.λp35:P CBEQX. -λp36:P CLC.λp37:P CLI.λp38:P CLR.λp39:P CMP.λp40:P COM.λp41:P CPHX.λp42:P CPX.λp43:P DAA.λp44:P DBNZ. -λp45:P DEC.λp46:P DIV.λp47:P EOR.λp48:P INC.λp49:P JMP.λp50:P JSR.λp51:P LDA.λp52:P LDHX.λp53:P LDX. -λp54:P LSR.λp55:P MOV.λp56:P MUL.λp57:P NEG.λp58:P NOP.λp59:P NSA.λp60:P ORA.λp61:P PSHA.λp62:P PSHH. -λp63:P PSHX.λp64:P PULA.λp65:P PULH.λp66:P PULX.λp67:P ROL.λp68:P ROR.λp69:P RSP.λp70:P RTI.λp71:P RTS. -λp72:P SBC.λp73:P SEC.λp74:P SEI.λp75:P SHA.λp76:P SLA.λp77:P STA.λp78:P STHX.λp79:P STOP.λp80:P STX. -λp81:P SUB.λp82:P SWI.λp83:P TAP.λp84:P TAX.λp85:P TPA.λp86:P TST.λp87:P TSX.λp88:P TXA.λp89:P TXS. -λp90:P WAIT.λo:opcode. - match o with  - [ ADC ⇒ p | ADD ⇒ p1 | AIS ⇒ p2 | AIX ⇒ p3 | AND ⇒ p4 | ASL ⇒ p5 | ASR ⇒ p6 | BCC ⇒ p7 | BCLRn ⇒ p8 - | BCS ⇒ p9 | BEQ ⇒ p10 | BGE ⇒ p11 | BGND ⇒ p12 | BGT ⇒ p13 | BHCC ⇒ p14 | BHCS ⇒ p15 | BHI ⇒ p16 - | BIH ⇒ p17 | BIL ⇒ p18 | BIT ⇒ p19 | BLE ⇒ p20 | BLS ⇒ p21 | BLT ⇒ p22 | BMC ⇒ p23 | BMI ⇒ p24 - | BMS ⇒ p25 | BNE ⇒ p26 | BPL ⇒ p27 | BRA ⇒ p28 | BRCLRn ⇒ p29 | BRN ⇒ p30 | BRSETn ⇒ p31 | BSETn ⇒ p32 - | BSR ⇒ p33 | CBEQA ⇒ p34 | CBEQX ⇒ p35 | CLC ⇒ p36 | CLI ⇒ p37 | CLR ⇒ p38 | CMP ⇒ p39 | COM ⇒ p40 - | CPHX ⇒ p41 | CPX ⇒ p42 | DAA ⇒ p43 | DBNZ ⇒ p44 | DEC ⇒ p45 | DIV ⇒ p46 | EOR ⇒ p47 | INC ⇒ p48 - | JMP ⇒ p49 | JSR ⇒ p50 | LDA ⇒ p51 | LDHX ⇒ p52 | LDX ⇒ p53 | LSR ⇒ p54 | MOV ⇒ p55 | MUL ⇒ p56 - | NEG ⇒ p57 | NOP ⇒ p58 | NSA ⇒ p59 | ORA ⇒ p60 | PSHA ⇒ p61 | PSHH ⇒ p62 | PSHX ⇒ p63 | PULA ⇒ p64 - | PULH ⇒ p65 | PULX ⇒ p66 | ROL ⇒ p67 | ROR ⇒ p68 | RSP ⇒ p69 | RTI ⇒ p70 | RTS ⇒ p71 | SBC ⇒ p72 - | SEC ⇒ p73 | SEI ⇒ p74 | SHA ⇒ p75 | SLA ⇒ p76 | STA ⇒ p77 | STHX ⇒ p78 | STOP ⇒ p79 | STX ⇒ p80 - | SUB ⇒ p81 | SWI ⇒ p82 | TAP ⇒ p83 | TAX ⇒ p84 | TPA ⇒ p85 | TST ⇒ p86 | TSX ⇒ p87 | TXA ⇒ p88 - | TXS ⇒ p89 | WAIT ⇒ p90 ]. - -ndefinition opcode_rec - : ΠP:opcode → Set. - P ADC → P ADD → P AIS → P AIX → P AND → P ASL → P ASR → P BCC → P BCLRn → P BCS → P BEQ → - P BGE → P BGND → P BGT → P BHCC → P BHCS → P BHI → P BIH → P BIL → P BIT → P BLE → P BLS → - P BLT → P BMC → P BMI → P BMS → P BNE → P BPL → P BRA → P BRCLRn → P BRN → P BRSETn → P BSETn → - P BSR → P CBEQA → P CBEQX → P CLC → P CLI → P CLR → P CMP → P COM → P CPHX → P CPX → P DAA → - P DBNZ → P DEC → P DIV → P EOR → P INC → P JMP → P JSR → P LDA → P LDHX → P LDX → P LSR → P MOV → - P MUL → P NEG → P NOP → P NSA → P ORA → P PSHA → P PSHH → P PSHX → P PULA → P PULH → P PULX → - P ROL → P ROR → P RSP → P RTI → P RTS → P SBC → P SEC → P SEI → P SHA → P SLA → P STA → P STHX → - P STOP → P STX → P SUB → P SWI → P TAP → P TAX → P TPA → P TST → P TSX → P TXA → P TXS → P WAIT → - Πo:opcode.P o ≝ -λP:opcode → Set. -λp:P ADC.λp1:P ADD.λp2:P AIS.λp3:P AIX.λp4:P AND.λp5:P ASL.λp6:P ASR.λp7:P BCC.λp8:P BCLRn.λp9:P BCS. -λp10:P BEQ.λp11:P BGE.λp12:P BGND.λp13:P BGT.λp14:P BHCC.λp15:P BHCS.λp16:P BHI.λp17:P BIH.λp18:P BIL. -λp19:P BIT.λp20:P BLE.λp21:P BLS.λp22:P BLT.λp23:P BMC.λp24:P BMI.λp25:P BMS.λp26:P BNE.λp27:P BPL. -λp28:P BRA.λp29:P BRCLRn.λp30:P BRN.λp31:P BRSETn.λp32:P BSETn.λp33:P BSR.λp34:P CBEQA.λp35:P CBEQX. -λp36:P CLC.λp37:P CLI.λp38:P CLR.λp39:P CMP.λp40:P COM.λp41:P CPHX.λp42:P CPX.λp43:P DAA.λp44:P DBNZ. -λp45:P DEC.λp46:P DIV.λp47:P EOR.λp48:P INC.λp49:P JMP.λp50:P JSR.λp51:P LDA.λp52:P LDHX.λp53:P LDX. -λp54:P LSR.λp55:P MOV.λp56:P MUL.λp57:P NEG.λp58:P NOP.λp59:P NSA.λp60:P ORA.λp61:P PSHA.λp62:P PSHH. -λp63:P PSHX.λp64:P PULA.λp65:P PULH.λp66:P PULX.λp67:P ROL.λp68:P ROR.λp69:P RSP.λp70:P RTI.λp71:P RTS. -λp72:P SBC.λp73:P SEC.λp74:P SEI.λp75:P SHA.λp76:P SLA.λp77:P STA.λp78:P STHX.λp79:P STOP.λp80:P STX. -λp81:P SUB.λp82:P SWI.λp83:P TAP.λp84:P TAX.λp85:P TPA.λp86:P TST.λp87:P TSX.λp88:P TXA.λp89:P TXS. -λp90:P WAIT.λo:opcode. - match o with  - [ ADC ⇒ p | ADD ⇒ p1 | AIS ⇒ p2 | AIX ⇒ p3 | AND ⇒ p4 | ASL ⇒ p5 | ASR ⇒ p6 | BCC ⇒ p7 | BCLRn ⇒ p8 - | BCS ⇒ p9 | BEQ ⇒ p10 | BGE ⇒ p11 | BGND ⇒ p12 | BGT ⇒ p13 | BHCC ⇒ p14 | BHCS ⇒ p15 | BHI ⇒ p16 - | BIH ⇒ p17 | BIL ⇒ p18 | BIT ⇒ p19 | BLE ⇒ p20 | BLS ⇒ p21 | BLT ⇒ p22 | BMC ⇒ p23 | BMI ⇒ p24 - | BMS ⇒ p25 | BNE ⇒ p26 | BPL ⇒ p27 | BRA ⇒ p28 | BRCLRn ⇒ p29 | BRN ⇒ p30 | BRSETn ⇒ p31 | BSETn ⇒ p32 - | BSR ⇒ p33 | CBEQA ⇒ p34 | CBEQX ⇒ p35 | CLC ⇒ p36 | CLI ⇒ p37 | CLR ⇒ p38 | CMP ⇒ p39 | COM ⇒ p40 - | CPHX ⇒ p41 | CPX ⇒ p42 | DAA ⇒ p43 | DBNZ ⇒ p44 | DEC ⇒ p45 | DIV ⇒ p46 | EOR ⇒ p47 | INC ⇒ p48 - | JMP ⇒ p49 | JSR ⇒ p50 | LDA ⇒ p51 | LDHX ⇒ p52 | LDX ⇒ p53 | LSR ⇒ p54 | MOV ⇒ p55 | MUL ⇒ p56 - | NEG ⇒ p57 | NOP ⇒ p58 | NSA ⇒ p59 | ORA ⇒ p60 | PSHA ⇒ p61 | PSHH ⇒ p62 | PSHX ⇒ p63 | PULA ⇒ p64 - | PULH ⇒ p65 | PULX ⇒ p66 | ROL ⇒ p67 | ROR ⇒ p68 | RSP ⇒ p69 | RTI ⇒ p70 | RTS ⇒ p71 | SBC ⇒ p72 - | SEC ⇒ p73 | SEI ⇒ p74 | SHA ⇒ p75 | SLA ⇒ p76 | STA ⇒ p77 | STHX ⇒ p78 | STOP ⇒ p79 | STX ⇒ p80 - | SUB ⇒ p81 | SWI ⇒ p82 | TAP ⇒ p83 | TAX ⇒ p84 | TPA ⇒ p85 | TST ⇒ p86 | TSX ⇒ p87 | TXA ⇒ p88 - | TXS ⇒ p89 | WAIT ⇒ p90 ]. - -ndefinition opcode_rect - : ΠP:opcode → Type. - P ADC → P ADD → P AIS → P AIX → P AND → P ASL → P ASR → P BCC → P BCLRn → P BCS → P BEQ → - P BGE → P BGND → P BGT → P BHCC → P BHCS → P BHI → P BIH → P BIL → P BIT → P BLE → P BLS → - P BLT → P BMC → P BMI → P BMS → P BNE → P BPL → P BRA → P BRCLRn → P BRN → P BRSETn → P BSETn → - P BSR → P CBEQA → P CBEQX → P CLC → P CLI → P CLR → P CMP → P COM → P CPHX → P CPX → P DAA → - P DBNZ → P DEC → P DIV → P EOR → P INC → P JMP → P JSR → P LDA → P LDHX → P LDX → P LSR → P MOV → - P MUL → P NEG → P NOP → P NSA → P ORA → P PSHA → P PSHH → P PSHX → P PULA → P PULH → P PULX → - P ROL → P ROR → P RSP → P RTI → P RTS → P SBC → P SEC → P SEI → P SHA → P SLA → P STA → P STHX → - P STOP → P STX → P SUB → P SWI → P TAP → P TAX → P TPA → P TST → P TSX → P TXA → P TXS → P WAIT → - Πo:opcode.P o ≝ -λP:opcode → Type. -λp:P ADC.λp1:P ADD.λp2:P AIS.λp3:P AIX.λp4:P AND.λp5:P ASL.λp6:P ASR.λp7:P BCC.λp8:P BCLRn.λp9:P BCS. -λp10:P BEQ.λp11:P BGE.λp12:P BGND.λp13:P BGT.λp14:P BHCC.λp15:P BHCS.λp16:P BHI.λp17:P BIH.λp18:P BIL. -λp19:P BIT.λp20:P BLE.λp21:P BLS.λp22:P BLT.λp23:P BMC.λp24:P BMI.λp25:P BMS.λp26:P BNE.λp27:P BPL. -λp28:P BRA.λp29:P BRCLRn.λp30:P BRN.λp31:P BRSETn.λp32:P BSETn.λp33:P BSR.λp34:P CBEQA.λp35:P CBEQX. -λp36:P CLC.λp37:P CLI.λp38:P CLR.λp39:P CMP.λp40:P COM.λp41:P CPHX.λp42:P CPX.λp43:P DAA.λp44:P DBNZ. -λp45:P DEC.λp46:P DIV.λp47:P EOR.λp48:P INC.λp49:P JMP.λp50:P JSR.λp51:P LDA.λp52:P LDHX.λp53:P LDX. -λp54:P LSR.λp55:P MOV.λp56:P MUL.λp57:P NEG.λp58:P NOP.λp59:P NSA.λp60:P ORA.λp61:P PSHA.λp62:P PSHH. -λp63:P PSHX.λp64:P PULA.λp65:P PULH.λp66:P PULX.λp67:P ROL.λp68:P ROR.λp69:P RSP.λp70:P RTI.λp71:P RTS. -λp72:P SBC.λp73:P SEC.λp74:P SEI.λp75:P SHA.λp76:P SLA.λp77:P STA.λp78:P STHX.λp79:P STOP.λp80:P STX. -λp81:P SUB.λp82:P SWI.λp83:P TAP.λp84:P TAX.λp85:P TPA.λp86:P TST.λp87:P TSX.λp88:P TXA.λp89:P TXS. -λp90:P WAIT.λo:opcode. - match o with  - [ ADC ⇒ p | ADD ⇒ p1 | AIS ⇒ p2 | AIX ⇒ p3 | AND ⇒ p4 | ASL ⇒ p5 | ASR ⇒ p6 | BCC ⇒ p7 | BCLRn ⇒ p8 - | BCS ⇒ p9 | BEQ ⇒ p10 | BGE ⇒ p11 | BGND ⇒ p12 | BGT ⇒ p13 | BHCC ⇒ p14 | BHCS ⇒ p15 | BHI ⇒ p16 - | BIH ⇒ p17 | BIL ⇒ p18 | BIT ⇒ p19 | BLE ⇒ p20 | BLS ⇒ p21 | BLT ⇒ p22 | BMC ⇒ p23 | BMI ⇒ p24 - | BMS ⇒ p25 | BNE ⇒ p26 | BPL ⇒ p27 | BRA ⇒ p28 | BRCLRn ⇒ p29 | BRN ⇒ p30 | BRSETn ⇒ p31 | BSETn ⇒ p32 - | BSR ⇒ p33 | CBEQA ⇒ p34 | CBEQX ⇒ p35 | CLC ⇒ p36 | CLI ⇒ p37 | CLR ⇒ p38 | CMP ⇒ p39 | COM ⇒ p40 - | CPHX ⇒ p41 | CPX ⇒ p42 | DAA ⇒ p43 | DBNZ ⇒ p44 | DEC ⇒ p45 | DIV ⇒ p46 | EOR ⇒ p47 | INC ⇒ p48 - | JMP ⇒ p49 | JSR ⇒ p50 | LDA ⇒ p51 | LDHX ⇒ p52 | LDX ⇒ p53 | LSR ⇒ p54 | MOV ⇒ p55 | MUL ⇒ p56 - | NEG ⇒ p57 | NOP ⇒ p58 | NSA ⇒ p59 | ORA ⇒ p60 | PSHA ⇒ p61 | PSHH ⇒ p62 | PSHX ⇒ p63 | PULA ⇒ p64 - | PULH ⇒ p65 | PULX ⇒ p66 | ROL ⇒ p67 | ROR ⇒ p68 | RSP ⇒ p69 | RTI ⇒ p70 | RTS ⇒ p71 | SBC ⇒ p72 - | SEC ⇒ p73 | SEI ⇒ p74 | SHA ⇒ p75 | SLA ⇒ p76 | STA ⇒ p77 | STHX ⇒ p78 | STOP ⇒ p79 | STX ⇒ p80 - | SUB ⇒ p81 | SWI ⇒ p82 | TAP ⇒ p83 | TAX ⇒ p84 | TPA ⇒ p85 | TST ⇒ p86 | TSX ⇒ p87 | TXA ⇒ p88 - | TXS ⇒ p89 | WAIT ⇒ p90 ].*) - ndefinition eq_op ≝ λop1,op2:opcode. match op1 with @@ -529,21 +313,6 @@ ndefinition eq_op ≝ ninductive any_opcode (m:mcu_type) : Type ≝ anyOP : opcode → any_opcode m. -(*ndefinition any_opcode_ind - : Πm:mcu_type.ΠP:any_opcode m → Prop.(Πo:opcode.P (anyOP m o)) → Πa:any_opcode m.P a ≝ -λm:mcu_type.λP:any_opcode m → Prop.λf:Πo:opcode.P (anyOP m o).λa:any_opcode m. - match a with [ anyOP (o:opcode) ⇒ f o ]. - -ndefinition any_opcode_rec - : Πm:mcu_type.ΠP:any_opcode m → Set.(Πo:opcode.P (anyOP m o)) → Πa:any_opcode m.P a ≝ -λm:mcu_type.λP:any_opcode m → Set.λf:Πo:opcode.P (anyOP m o).λa:any_opcode m. - match a with [ anyOP (o:opcode) ⇒ f o ]. - -ndefinition any_opcode_rect - : Πm:mcu_type.ΠP:any_opcode m → Type.(Πo:opcode.P (anyOP m o)) → Πa:any_opcode m.P a ≝ -λm:mcu_type.λP:any_opcode m → Type.λf:Πo:opcode.P (anyOP m o).λa:any_opcode m. - match a with [ anyOP (o:opcode) ⇒ f o ].*) - ndefinition eq_anyop ≝ λm:mcu_type.λop1,op2:any_opcode m. match op1 with [ anyOP op1' ⇒ @@ -555,21 +324,6 @@ ninductive byte8_or_word16 : Type ≝ Byte: byte8 → byte8_or_word16 | Word: word16 → byte8_or_word16. -(*ndefinition byte8_or_word16_ind - : ΠP:byte8_or_word16 → Prop.(Πb:byte8.P (Byte b)) → (Πw:word16.P (Word w)) → Πb:byte8_or_word16.P b ≝ -λP:byte8_or_word16 → Prop.λf:Πb:byte8.P (Byte b).λf1:Πw:word16.P (Word w).λb:byte8_or_word16. - match b with [ Byte (b1:byte8) ⇒ f b1 | Word (w:word16) ⇒ f1 w ]. - -ndefinition byte8_or_word16_rec - : ΠP:byte8_or_word16 → Set.(Πb:byte8.P (Byte b)) → (Πw:word16.P (Word w)) → Πb:byte8_or_word16.P b ≝ -λP:byte8_or_word16 → Set.λf:Πb:byte8.P (Byte b).λf1:Πw:word16.P (Word w).λb:byte8_or_word16. - match b with [ Byte (b1:byte8) ⇒ f b1 | Word (w:word16) ⇒ f1 w ]. - -ndefinition byte8_or_word16_rect - : ΠP:byte8_or_word16 → Type.(Πb:byte8.P (Byte b)) → (Πw:word16.P (Word w)) → Πb:byte8_or_word16.P b ≝ -λP:byte8_or_word16 → Type.λf:Πb:byte8.P (Byte b).λf1:Πw:word16.P (Word w).λb:byte8_or_word16. - match b with [ Byte (b1:byte8) ⇒ f b1 | Word (w:word16) ⇒ f1 w ].*) - ndefinition eq_b8w16 ≝ λbw1,bw2:byte8_or_word16. match bw1 with diff --git a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas.ma index a4394d4f1..371dc4033 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas.ma @@ -41,25 +41,25 @@ ndefinition mcu_type_destruct : mcu_type_destruct_aux. nelim m1; ##[ ##1: nelim m2; nnormalize; #H; ##[ ##1: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match HC05 with [ HC05 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] ##| ##2: nelim m2; nnormalize; #H; ##[ ##2: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match HC08 with [ HC08 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] ##| ##3: nelim m2; nnormalize; #H; ##[ ##3: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match HCS08 with [ HCS08 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] ##| ##4: nelim m2; nnormalize; #H; ##[ ##4: napply (λx:P.x) - ##| ##*: napply (False_ind ??); + ##| ##*: napply (False_ind (λ_.?) ?); nchange with (match RS08 with [ RS08 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] diff --git a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode1.ma b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode1.ma index 9ef4d01b7..8d8f526b7 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode1.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode1.ma @@ -35,11 +35,11 @@ ndefinition instr_mode_destruct1 : nnormalize; ##[ ##1: #H; napply (λx:P.x) ##| ##2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INH with [ MODE_INH ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INH with [ MODE_INH ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -52,11 +52,11 @@ ndefinition instr_mode_destruct2 : nnormalize; ##[ ##2: #H; napply (λx:P.x) ##| ##1,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INHA with [ MODE_INHA ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INHA with [ MODE_INHA ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -69,11 +69,11 @@ ndefinition instr_mode_destruct3 : nnormalize; ##[ ##3: #H; napply (λx:P.x) ##| ##1,2,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INHX with [ MODE_INHX ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INHX with [ MODE_INHX ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -86,11 +86,11 @@ ndefinition instr_mode_destruct4 : nnormalize; ##[ ##4: #H; napply (λx:P.x) ##| ##1,2,3,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INHH with [ MODE_INHH ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INHH with [ MODE_INHH ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -103,11 +103,11 @@ ndefinition instr_mode_destruct5 : nnormalize; ##[ ##5: #H; napply (λx:P.x) ##| ##1,2,3,4,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INHX0ADD with [ MODE_INHX0ADD ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INHX0ADD with [ MODE_INHX0ADD ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -120,11 +120,11 @@ ndefinition instr_mode_destruct6 : nnormalize; ##[ ##6: #H; napply (λx:P.x) ##| ##1,2,3,4,5,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INHX1ADD with [ MODE_INHX1ADD ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INHX1ADD with [ MODE_INHX1ADD ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -137,11 +137,11 @@ ndefinition instr_mode_destruct7 : nnormalize; ##[ ##7: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INHX2ADD with [ MODE_INHX2ADD ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INHX2ADD with [ MODE_INHX2ADD ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -154,11 +154,11 @@ ndefinition instr_mode_destruct8 : nnormalize; ##[ ##8: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IMM1 with [ MODE_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IMM1 with [ MODE_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -171,11 +171,11 @@ ndefinition instr_mode_destruct9 : nnormalize; ##[ ##9: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IMM1EXT with [ MODE_IMM1EXT ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IMM1EXT with [ MODE_IMM1EXT ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -188,11 +188,11 @@ ndefinition instr_mode_destruct10 : nnormalize; ##[ ##10: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IMM2 with [ MODE_IMM2 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IMM2 with [ MODE_IMM2 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -205,11 +205,11 @@ ndefinition instr_mode_destruct11 : nnormalize; ##[ ##11: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_DIR1 with [ MODE_DIR1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_DIR1 with [ MODE_DIR1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -222,11 +222,11 @@ ndefinition instr_mode_destruct12 : nnormalize; ##[ ##12: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_DIR2 with [ MODE_DIR2 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_DIR2 with [ MODE_DIR2 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -239,11 +239,11 @@ ndefinition instr_mode_destruct13 : nnormalize; ##[ ##13: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IX0 with [ MODE_IX0 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IX0 with [ MODE_IX0 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -256,11 +256,11 @@ ndefinition instr_mode_destruct14 : nnormalize; ##[ ##14: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IX1 with [ MODE_IX1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IX1 with [ MODE_IX1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -273,11 +273,11 @@ ndefinition instr_mode_destruct15 : nnormalize; ##[ ##15: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IX2 with [ MODE_IX2 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IX2 with [ MODE_IX2 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -290,11 +290,11 @@ ndefinition instr_mode_destruct16 : nnormalize; ##[ ##16: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_SP1 with [ MODE_SP1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_SP1 with [ MODE_SP1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -307,11 +307,11 @@ ndefinition instr_mode_destruct17 : nnormalize; ##[ ##17: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_SP2 with [ MODE_SP2 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_SP2 with [ MODE_SP2 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -324,11 +324,11 @@ ndefinition instr_mode_destruct18 : nnormalize; ##[ ##18: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_DIR1_to_DIR1 with [ MODE_DIR1_to_DIR1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_DIR1_to_DIR1 with [ MODE_DIR1_to_DIR1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -341,11 +341,11 @@ ndefinition instr_mode_destruct19 : nnormalize; ##[ ##19: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IMM1_to_DIR1 with [ MODE_IMM1_to_DIR1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IMM1_to_DIR1 with [ MODE_IMM1_to_DIR1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -358,11 +358,11 @@ ndefinition instr_mode_destruct20 : nnormalize; ##[ ##20: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IX0p_to_DIR1 with [ MODE_IX0p_to_DIR1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IX0p_to_DIR1 with [ MODE_IX0p_to_DIR1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -375,11 +375,11 @@ ndefinition instr_mode_destruct21 : nnormalize; ##[ ##21: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_DIR1_to_IX0p with [ MODE_DIR1_to_IX0p ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_DIR1_to_IX0p with [ MODE_DIR1_to_IX0p ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -392,11 +392,11 @@ ndefinition instr_mode_destruct22 : nnormalize; ##[ ##22: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INHA_and_IMM1 with [ MODE_INHA_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INHA_and_IMM1 with [ MODE_INHA_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -409,11 +409,11 @@ ndefinition instr_mode_destruct23 : nnormalize; ##[ ##23: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INHX_and_IMM1 with [ MODE_INHX_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_INHX_and_IMM1 with [ MODE_INHX_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -426,11 +426,11 @@ ndefinition instr_mode_destruct24 : nnormalize; ##[ ##24: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IMM1_and_IMM1 with [ MODE_IMM1_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IMM1_and_IMM1 with [ MODE_IMM1_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -443,11 +443,11 @@ ndefinition instr_mode_destruct25 : nnormalize; ##[ ##25: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_DIR1_and_IMM1 with [ MODE_DIR1_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_DIR1_and_IMM1 with [ MODE_DIR1_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -460,11 +460,11 @@ ndefinition instr_mode_destruct26 : nnormalize; ##[ ##26: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IX0_and_IMM1 with [ MODE_IX0_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IX0_and_IMM1 with [ MODE_IX0_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -477,11 +477,11 @@ ndefinition instr_mode_destruct27 : nnormalize; ##[ ##27: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IX0p_and_IMM1 with [ MODE_IX0p_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IX0p_and_IMM1 with [ MODE_IX0p_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -494,11 +494,11 @@ ndefinition instr_mode_destruct28 : nnormalize; ##[ ##28: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IX1_and_IMM1 with [ MODE_IX1_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IX1_and_IMM1 with [ MODE_IX1_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -511,11 +511,11 @@ ndefinition instr_mode_destruct29 : nnormalize; ##[ ##29: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IX1p_and_IMM1 with [ MODE_IX1p_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_IX1p_and_IMM1 with [ MODE_IX1p_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -528,11 +528,11 @@ ndefinition instr_mode_destruct30 : nnormalize; ##[ ##30: #H; napply (λx:P.x) ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_SP1_and_IMM1 with [ MODE_SP1_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_SP1_and_IMM1 with [ MODE_SP1_and_IMM1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -559,11 +559,11 @@ ndefinition instr_mode_destruct31 : ncases i2; nnormalize; ##[ ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_DIRn n1 with [ MODE_DIRn a ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##32,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_DIRn n1 with [ MODE_DIRn n1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31: #n2; @@ -596,11 +596,11 @@ ndefinition instr_mode_destruct32 : ncases i2; nnormalize; ##[ ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_DIRn_and_IMM1 n1 with [ MODE_DIRn_and_IMM1 a ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,33,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_DIRn_and_IMM1 n1 with [ MODE_DIRn_and_IMM1 n1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##32: #n2; @@ -637,11 +637,11 @@ ndefinition instr_mode_destruct33 : ncases i2; nnormalize; ##[ ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_TNY n1 with [ MODE_TNY a ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,34: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_TNY n1 with [ MODE_TNY n1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##33: #n2; @@ -686,11 +686,11 @@ ndefinition instr_mode_destruct34 : ncases i2; nnormalize; ##[ ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_SRT n1 with [ MODE_SRT a ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##31,32,33: #n; #H; - napply (False_ind ??); + napply (False_ind (λ_.?) ?); nchange with (match MODE_SRT n1 with [ MODE_SRT n1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##| ##34: #n2; diff --git a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_opcode1.ma b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_opcode1.ma index d113e8937..f0954a11c 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_opcode1.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_opcode1.ma @@ -30,7 +30,7 @@ include "freescale/opcode_base.ma". ndefinition opcode_destruct1 : Πop2.ΠP:Prop.ADC = op2 → match op2 with [ ADC ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##1: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ADC with [ ADC ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -39,7 +39,7 @@ nqed. ndefinition opcode_destruct2 : Πop2.ΠP:Prop.ADD = op2 → match op2 with [ ADD ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##2: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ADD with [ ADD ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -48,7 +48,7 @@ nqed. ndefinition opcode_destruct3 : Πop2.ΠP:Prop.AIS = op2 → match op2 with [ AIS ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##3: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match AIS with [ AIS ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -57,7 +57,7 @@ nqed. ndefinition opcode_destruct4 : Πop2.ΠP:Prop.AIX = op2 → match op2 with [ AIX ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##4: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match AIX with [ AIX ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -66,7 +66,7 @@ nqed. ndefinition opcode_destruct5 : Πop2.ΠP:Prop.AND = op2 → match op2 with [ AND ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##5: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match AND with [ AND ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -75,7 +75,7 @@ nqed. ndefinition opcode_destruct6 : Πop2.ΠP:Prop.ASL = op2 → match op2 with [ ASL ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##6: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ASL with [ ASL ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -84,7 +84,7 @@ nqed. ndefinition opcode_destruct7 : Πop2.ΠP:Prop.ASR = op2 → match op2 with [ ASR ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##7: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ASR with [ ASR ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -93,7 +93,7 @@ nqed. ndefinition opcode_destruct8 : Πop2.ΠP:Prop.BCC = op2 → match op2 with [ BCC ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##8: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match BCC with [ BCC ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -102,7 +102,7 @@ nqed. ndefinition opcode_destruct9 : Πop2.ΠP:Prop.BCLRn = op2 → match op2 with [ BCLRn ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##9: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match BCLRn with [ BCLRn ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -111,7 +111,7 @@ nqed. ndefinition opcode_destruct10 : Πop2.ΠP:Prop.BCS = op2 → match op2 with [ BCS ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##10: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match BCS with [ BCS ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -120,7 +120,7 @@ nqed. ndefinition opcode_destruct11 : Πop2.ΠP:Prop.BEQ = op2 → match op2 with [ BEQ ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##11: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match BEQ with [ BEQ ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -129,7 +129,7 @@ nqed. ndefinition opcode_destruct12 : Πop2.ΠP:Prop.BGE = op2 → match op2 with [ BGE ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##12: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match BGE with [ BGE ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -138,7 +138,7 @@ nqed. ndefinition opcode_destruct13 : Πop2.ΠP:Prop.BGND = op2 → match op2 with [ BGND ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##13: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match BGND with [ BGND ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -147,7 +147,7 @@ nqed. ndefinition opcode_destruct14 : Πop2.ΠP:Prop.BGT = op2 → match op2 with [ BGT ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##14: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match BGT with [ BGT ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -156,7 +156,7 @@ nqed. ndefinition opcode_destruct15 : Πop2.ΠP:Prop.BHCC = op2 → match op2 with [ BHCC ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##15: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match BHCC with [ BHCC ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -165,7 +165,7 @@ nqed. ndefinition opcode_destruct16 : Πop2.ΠP:Prop.BHCS = op2 → match op2 with [ BHCS ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##16: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match BHCS with [ BHCS ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -174,7 +174,7 @@ nqed. ndefinition opcode_destruct17 : Πop2.ΠP:Prop.BHI = op2 → match op2 with [ BHI ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##17: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match BHI with [ BHI ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -183,7 +183,7 @@ nqed. ndefinition opcode_destruct18 : Πop2.ΠP:Prop.BIH = op2 → match op2 with [ BIH ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##18: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match BIH with [ BIH ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -192,7 +192,7 @@ nqed. ndefinition opcode_destruct19 : Πop2.ΠP:Prop.BIL = op2 → match op2 with [ BIL ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##19: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match BIL with [ BIL ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -201,7 +201,7 @@ nqed. ndefinition opcode_destruct20 : Πop2.ΠP:Prop.BIT = op2 → match op2 with [ BIT ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##20: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match BIT with [ BIT ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -210,7 +210,7 @@ nqed. ndefinition opcode_destruct21 : Πop2.ΠP:Prop.BLE = op2 → match op2 with [ BLE ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##21: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match BLE with [ BLE ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -219,7 +219,7 @@ nqed. ndefinition opcode_destruct22 : Πop2.ΠP:Prop.BLS = op2 → match op2 with [ BLS ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##22: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match BLS with [ BLS ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -228,7 +228,7 @@ nqed. ndefinition opcode_destruct23 : Πop2.ΠP:Prop.BLT = op2 → match op2 with [ BLT ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##23: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match BLT with [ BLT ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -237,7 +237,7 @@ nqed. ndefinition opcode_destruct24 : Πop2.ΠP:Prop.BMC = op2 → match op2 with [ BMC ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##24: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match BMC with [ BMC ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -246,7 +246,7 @@ nqed. ndefinition opcode_destruct25 : Πop2.ΠP:Prop.BMI = op2 → match op2 with [ BMI ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##25: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match BMI with [ BMI ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -255,7 +255,7 @@ nqed. ndefinition opcode_destruct26 : Πop2.ΠP:Prop.BMS = op2 → match op2 with [ BMS ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##26: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match BMS with [ BMS ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -264,7 +264,7 @@ nqed. ndefinition opcode_destruct27 : Πop2.ΠP:Prop.BNE = op2 → match op2 with [ BNE ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##27: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match BNE with [ BNE ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -273,7 +273,7 @@ nqed. ndefinition opcode_destruct28 : Πop2.ΠP:Prop.BPL = op2 → match op2 with [ BPL ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##28: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match BPL with [ BPL ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -282,7 +282,7 @@ nqed. ndefinition opcode_destruct29 : Πop2.ΠP:Prop.BRA = op2 → match op2 with [ BRA ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##29: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match BRA with [ BRA ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -291,7 +291,7 @@ nqed. ndefinition opcode_destruct30 : Πop2.ΠP:Prop.BRCLRn = op2 → match op2 with [ BRCLRn ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##30: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match BRCLRn with [ BRCLRn ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -300,7 +300,7 @@ nqed. ndefinition opcode_destruct31 : Πop2.ΠP:Prop.BRN = op2 → match op2 with [ BRN ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##31: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match BRN with [ BRN ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -309,7 +309,7 @@ nqed. ndefinition opcode_destruct32 : Πop2.ΠP:Prop.BRSETn = op2 → match op2 with [ BRSETn ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##32: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match BRSETn with [ BRSETn ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -318,7 +318,7 @@ nqed. ndefinition opcode_destruct33 : Πop2.ΠP:Prop.BSETn = op2 → match op2 with [ BSETn ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##33: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match BSETn with [ BSETn ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -327,7 +327,7 @@ nqed. ndefinition opcode_destruct34 : Πop2.ΠP:Prop.BSR = op2 → match op2 with [ BSR ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##34: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match BSR with [ BSR ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -336,7 +336,7 @@ nqed. ndefinition opcode_destruct35 : Πop2.ΠP:Prop.CBEQA = op2 → match op2 with [ CBEQA ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##35: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match CBEQA with [ CBEQA ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -345,7 +345,7 @@ nqed. ndefinition opcode_destruct36 : Πop2.ΠP:Prop.CBEQX = op2 → match op2 with [ CBEQX ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##36: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match CBEQX with [ CBEQX ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -354,7 +354,7 @@ nqed. ndefinition opcode_destruct37 : Πop2.ΠP:Prop.CLC = op2 → match op2 with [ CLC ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##37: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match CLC with [ CLC ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -363,7 +363,7 @@ nqed. ndefinition opcode_destruct38 : Πop2.ΠP:Prop.CLI = op2 → match op2 with [ CLI ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##38: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match CLI with [ CLI ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -372,7 +372,7 @@ nqed. ndefinition opcode_destruct39 : Πop2.ΠP:Prop.CLR = op2 → match op2 with [ CLR ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##39: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match CLR with [ CLR ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -381,7 +381,7 @@ nqed. ndefinition opcode_destruct40 : Πop2.ΠP:Prop.CMP = op2 → match op2 with [ CMP ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##40: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match CMP with [ CMP ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -390,7 +390,7 @@ nqed. ndefinition opcode_destruct41 : Πop2.ΠP:Prop.COM = op2 → match op2 with [ COM ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##41: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match COM with [ COM ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -399,7 +399,7 @@ nqed. ndefinition opcode_destruct42 : Πop2.ΠP:Prop.CPHX = op2 → match op2 with [ CPHX ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##42: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match CPHX with [ CPHX ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -408,7 +408,7 @@ nqed. ndefinition opcode_destruct43 : Πop2.ΠP:Prop.CPX = op2 → match op2 with [ CPX ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##43: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match CPX with [ CPX ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -417,7 +417,7 @@ nqed. ndefinition opcode_destruct44 : Πop2.ΠP:Prop.DAA = op2 → match op2 with [ DAA ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##44: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match DAA with [ DAA ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -426,7 +426,7 @@ nqed. ndefinition opcode_destruct45 : Πop2.ΠP:Prop.DBNZ = op2 → match op2 with [ DBNZ ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##45: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match DBNZ with [ DBNZ ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -435,7 +435,7 @@ nqed. ndefinition opcode_destruct46 : Πop2.ΠP:Prop.DEC = op2 → match op2 with [ DEC ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##46: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match DEC with [ DEC ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -444,7 +444,7 @@ nqed. ndefinition opcode_destruct47 : Πop2.ΠP:Prop.DIV = op2 → match op2 with [ DIV ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##47: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match DIV with [ DIV ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -453,7 +453,7 @@ nqed. ndefinition opcode_destruct48 : Πop2.ΠP:Prop.EOR = op2 → match op2 with [ EOR ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##48: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match EOR with [ EOR ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -462,7 +462,7 @@ nqed. ndefinition opcode_destruct49 : Πop2.ΠP:Prop.INC = op2 → match op2 with [ INC ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##49: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match INC with [ INC ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -471,7 +471,7 @@ nqed. ndefinition opcode_destruct50 : Πop2.ΠP:Prop.JMP = op2 → match op2 with [ JMP ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##50: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match JMP with [ JMP ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -480,7 +480,7 @@ nqed. ndefinition opcode_destruct51 : Πop2.ΠP:Prop.JSR = op2 → match op2 with [ JSR ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##51: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match JSR with [ JSR ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -489,7 +489,7 @@ nqed. ndefinition opcode_destruct52 : Πop2.ΠP:Prop.LDA = op2 → match op2 with [ LDA ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##52: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match LDA with [ LDA ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -498,7 +498,7 @@ nqed. ndefinition opcode_destruct53 : Πop2.ΠP:Prop.LDHX = op2 → match op2 with [ LDHX ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##53: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match LDHX with [ LDHX ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -507,7 +507,7 @@ nqed. ndefinition opcode_destruct54 : Πop2.ΠP:Prop.LDX = op2 → match op2 with [ LDX ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##54: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match LDX with [ LDX ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -516,7 +516,7 @@ nqed. ndefinition opcode_destruct55 : Πop2.ΠP:Prop.LSR = op2 → match op2 with [ LSR ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##55: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match LSR with [ LSR ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -525,7 +525,7 @@ nqed. ndefinition opcode_destruct56 : Πop2.ΠP:Prop.MOV = op2 → match op2 with [ MOV ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##56: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match MOV with [ MOV ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -534,7 +534,7 @@ nqed. ndefinition opcode_destruct57 : Πop2.ΠP:Prop.MUL = op2 → match op2 with [ MUL ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##57: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match MUL with [ MUL ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -543,7 +543,7 @@ nqed. ndefinition opcode_destruct58 : Πop2.ΠP:Prop.NEG = op2 → match op2 with [ NEG ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##58: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match NEG with [ NEG ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -552,7 +552,7 @@ nqed. ndefinition opcode_destruct59 : Πop2.ΠP:Prop.NOP = op2 → match op2 with [ NOP ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##59: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match NOP with [ NOP ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -561,7 +561,7 @@ nqed. ndefinition opcode_destruct60 : Πop2.ΠP:Prop.NSA = op2 → match op2 with [ NSA ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##60: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match NSA with [ NSA ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -570,7 +570,7 @@ nqed. ndefinition opcode_destruct61 : Πop2.ΠP:Prop.ORA = op2 → match op2 with [ ORA ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##61: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ORA with [ ORA ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -579,7 +579,7 @@ nqed. ndefinition opcode_destruct62 : Πop2.ΠP:Prop.PSHA = op2 → match op2 with [ PSHA ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##62: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match PSHA with [ PSHA ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -588,7 +588,7 @@ nqed. ndefinition opcode_destruct63 : Πop2.ΠP:Prop.PSHH = op2 → match op2 with [ PSHH ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##63: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match PSHH with [ PSHH ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -597,7 +597,7 @@ nqed. ndefinition opcode_destruct64 : Πop2.ΠP:Prop.PSHX = op2 → match op2 with [ PSHX ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##64: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match PSHX with [ PSHX ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -606,7 +606,7 @@ nqed. ndefinition opcode_destruct65 : Πop2.ΠP:Prop.PULA = op2 → match op2 with [ PULA ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##65: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match PULA with [ PULA ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -615,7 +615,7 @@ nqed. ndefinition opcode_destruct66 : Πop2.ΠP:Prop.PULH = op2 → match op2 with [ PULH ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##66: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match PULH with [ PULH ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -624,7 +624,7 @@ nqed. ndefinition opcode_destruct67 : Πop2.ΠP:Prop.PULX = op2 → match op2 with [ PULX ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##67: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match PULX with [ PULX ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -633,7 +633,7 @@ nqed. ndefinition opcode_destruct68 : Πop2.ΠP:Prop.ROL = op2 → match op2 with [ ROL ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##68: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ROL with [ ROL ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -642,7 +642,7 @@ nqed. ndefinition opcode_destruct69 : Πop2.ΠP:Prop.ROR = op2 → match op2 with [ ROR ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##69: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ROR with [ ROR ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -651,7 +651,7 @@ nqed. ndefinition opcode_destruct70 : Πop2.ΠP:Prop.RSP = op2 → match op2 with [ RSP ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##70: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match RSP with [ RSP ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -660,7 +660,7 @@ nqed. ndefinition opcode_destruct71 : Πop2.ΠP:Prop.RTI = op2 → match op2 with [ RTI ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##71: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match RTI with [ RTI ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -669,7 +669,7 @@ nqed. ndefinition opcode_destruct72 : Πop2.ΠP:Prop.RTS = op2 → match op2 with [ RTS ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##72: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match RTS with [ RTS ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -678,7 +678,7 @@ nqed. ndefinition opcode_destruct73 : Πop2.ΠP:Prop.SBC = op2 → match op2 with [ SBC ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##73: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match SBC with [ SBC ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -687,7 +687,7 @@ nqed. ndefinition opcode_destruct74 : Πop2.ΠP:Prop.SEC = op2 → match op2 with [ SEC ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##74: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match SEC with [ SEC ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -696,7 +696,7 @@ nqed. ndefinition opcode_destruct75 : Πop2.ΠP:Prop.SEI = op2 → match op2 with [ SEI ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##75: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match SEI with [ SEI ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -705,7 +705,7 @@ nqed. ndefinition opcode_destruct76 : Πop2.ΠP:Prop.SHA = op2 → match op2 with [ SHA ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##76: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match SHA with [ SHA ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -714,7 +714,7 @@ nqed. ndefinition opcode_destruct77 : Πop2.ΠP:Prop.SLA = op2 → match op2 with [ SLA ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##77: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match SLA with [ SLA ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -723,7 +723,7 @@ nqed. ndefinition opcode_destruct78 : Πop2.ΠP:Prop.STA = op2 → match op2 with [ STA ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##78: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match STA with [ STA ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -732,7 +732,7 @@ nqed. ndefinition opcode_destruct79 : Πop2.ΠP:Prop.STHX = op2 → match op2 with [ STHX ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##79: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match STHX with [ STHX ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -741,7 +741,7 @@ nqed. ndefinition opcode_destruct80 : Πop2.ΠP:Prop.STOP = op2 → match op2 with [ STOP ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##80: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match STOP with [ STOP ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -750,7 +750,7 @@ nqed. ndefinition opcode_destruct81 : Πop2.ΠP:Prop.STX = op2 → match op2 with [ STX ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##81: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match STX with [ STX ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -759,7 +759,7 @@ nqed. ndefinition opcode_destruct82 : Πop2.ΠP:Prop.SUB = op2 → match op2 with [ SUB ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##82: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match SUB with [ SUB ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -768,7 +768,7 @@ nqed. ndefinition opcode_destruct83 : Πop2.ΠP:Prop.SWI = op2 → match op2 with [ SWI ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##83: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match SWI with [ SWI ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -777,7 +777,7 @@ nqed. ndefinition opcode_destruct84 : Πop2.ΠP:Prop.TAP = op2 → match op2 with [ TAP ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##84: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match TAP with [ TAP ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -786,7 +786,7 @@ nqed. ndefinition opcode_destruct85 : Πop2.ΠP:Prop.TAX = op2 → match op2 with [ TAX ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##85: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match TAX with [ TAX ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -795,7 +795,7 @@ nqed. ndefinition opcode_destruct86 : Πop2.ΠP:Prop.TPA = op2 → match op2 with [ TPA ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##86: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match TPA with [ TPA ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -804,7 +804,7 @@ nqed. ndefinition opcode_destruct87 : Πop2.ΠP:Prop.TST = op2 → match op2 with [ TST ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##87: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match TST with [ TST ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -813,7 +813,7 @@ nqed. ndefinition opcode_destruct88 : Πop2.ΠP:Prop.TSX = op2 → match op2 with [ TSX ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##88: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match TSX with [ TSX ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -822,7 +822,7 @@ nqed. ndefinition opcode_destruct89 : Πop2.ΠP:Prop.TXA = op2 → match op2 with [ TXA ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##89: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match TXA with [ TXA ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -831,7 +831,7 @@ nqed. ndefinition opcode_destruct90 : Πop2.ΠP:Prop.TXS = op2 → match op2 with [ TXS ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##90: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match TXS with [ TXS ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] @@ -840,7 +840,7 @@ nqed. ndefinition opcode_destruct91 : Πop2.ΠP:Prop.WAIT = op2 → match op2 with [ WAIT ⇒ P → P | _ ⇒ P ]. #op2; #P; ncases op2; nnormalize; ##[ ##91: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match WAIT with [ WAIT ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] diff --git a/helm/software/matita/contribs/ng_assembly/freescale/option.ma b/helm/software/matita/contribs/ng_assembly/freescale/option.ma index 4c7a9abb4..fceec48df 100644 --- a/helm/software/matita/contribs/ng_assembly/freescale/option.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/option.ma @@ -30,18 +30,6 @@ ninductive option (A:Type) : Type ≝ None : option A | Some : A → option A. -(*ndefinition option_ind : ΠA:Type.ΠP:option A → Prop.P (None A) → (Πa:A.P (Some A a)) → Πop:option A.P op ≝ -λA:Type.λP:option A → Prop.λp:P (None A).λf:Πa:A.P (Some A a).λop:option A. - match op with [ None ⇒ p | Some (a:A) ⇒ f a ]. - -ndefinition option_rec : ΠA:Type.ΠP:option A → Set.P (None A) → (Πa:A.P (Some A a)) → Πop:option A.P op ≝ -λA:Type.λP:option A → Set.λp:P (None A).λf:Πa:A.P (Some A a).λop:option A. - match op with [ None ⇒ p | Some (a:A) ⇒ f a ]. - -ndefinition option_rect : ΠA:Type.ΠP:option A → Type.P (None A) → (Πa:A.P (Some A a)) → Πop:option A.P op ≝ -λA:Type.λP:option A → Type.λp:P (None A).λf:Πa:A.P (Some A a).λop:option A. - match op with [ None ⇒ p | Some (a:A) ⇒ f a ].*) - ndefinition eq_option ≝ λT.λop1,op2:option T.λf:T → T → bool. match op1 with diff --git a/helm/software/matita/contribs/ng_assembly/freescale/option_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/option_lemmas.ma index 82a33c9f8..c04bc9df0 100644 --- a/helm/software/matita/contribs/ng_assembly/freescale/option_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/option_lemmas.ma @@ -56,8 +56,8 @@ nlemma symmetric_eqoption : (symmetricT T bool f) → (eq_option T op1 op2 f = eq_option T op2 op1 f). #T; #op1; #op2; #f; #H; - napply (option_ind T ??? op1); - napply (option_ind T ??? op2); + nelim op1; + nelim op2; nnormalize; ##[ ##1: napply (refl_eq ??) ##| ##2,3: #H; napply (refl_eq ??) @@ -72,8 +72,8 @@ nlemma eq_to_eqoption : (∀x1,x2:T.x1 = x2 → f x1 x2 = true) → (op1 = op2 → eq_option T op1 op2 f = true). #T; #op1; #op2; #f; #H; - napply (option_ind T ??? op1); - napply (option_ind T ??? op2); + nelim op1; + nelim op2; nnormalize; ##[ ##1: #H1; napply (refl_eq ??) ##| ##2: #a; #H1; nelim (option_destruct_none_some ?? H1) @@ -90,8 +90,8 @@ nlemma eqoption_to_eq : (∀x1,x2:T.f x1 x2 = true → x1 = x2) → (eq_option T op1 op2 f = true → op1 = op2). #T; #op1; #op2; #f; #H; - napply (option_ind T ??? op1); - napply (option_ind T ??? op2); + nelim op1; + nelim op2; nnormalize; ##[ ##1: #H1; napply (refl_eq ??) ##| ##2,3: #a; #H1; napply (bool_destruct ??? H1) diff --git a/helm/software/matita/contribs/ng_assembly/freescale/prod_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/prod_lemmas.ma index 02bd4e138..d6995ec0b 100644 --- a/helm/software/matita/contribs/ng_assembly/freescale/prod_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/prod_lemmas.ma @@ -54,9 +54,9 @@ nlemma symmetric_eqpair : (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; - napply (ProdT_ind T1 T2 ?? p1); + nelim p1; #x1; #y1; - napply (ProdT_ind T1 T2 ?? p2); + nelim p2; #x2; #y2; nnormalize; nrewrite > (H x1 x2); @@ -74,9 +74,9 @@ nlemma eq_to_eqpair : (∀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; - napply (ProdT_ind T1 T2 ?? p1); + nelim p1; #x1; #y1; - napply (ProdT_ind T1 T2 ?? p2); + nelim p2; #x2; #y2; #H; nnormalize; nrewrite > (H1 ?? (pair_destruct_1 ?????? H)); @@ -92,9 +92,9 @@ nlemma eqpair_to_eq : (∀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; - napply (ProdT_ind T1 T2 ?? p1); + nelim p1; #x1; #y1; - napply (ProdT_ind T1 T2 ?? p2); + nelim p2; #x2; #y2; #H; nnormalize in H:(%); nletin K ≝ (H1 x1 x2); @@ -146,9 +146,9 @@ nlemma symmetric_eqtriple : (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; - napply (Prod3T_ind T1 T2 T3 ?? p1); + nelim p1; #x1; #y1; #z1; - napply (Prod3T_ind T1 T2 T3 ?? p2); + nelim p2; #x2; #y2; #z2; nnormalize; nrewrite > (H x1 x2); @@ -172,9 +172,9 @@ nlemma eq_to_eqtriple : (∀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; - napply (Prod3T_ind T1 T2 T3 ?? p1); + nelim p1; #x1; #y1; #z1; - napply (Prod3T_ind T1 T2 T3 ?? p2); + nelim p2; #x2; #y2; #z2; #H; nnormalize; nrewrite > (H1 ?? (triple_destruct_1 ????????? H)); @@ -193,9 +193,9 @@ nlemma eqtriple_to_eq : (∀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; - napply (Prod3T_ind T1 T2 T3 ?? p1); + nelim p1; #x1; #y1; #z1; - napply (Prod3T_ind T1 T2 T3 ?? p2); + nelim p2; #x2; #y2; #z2; #H; nnormalize in H:(%); nletin K ≝ (H1 x1 x2); @@ -262,9 +262,9 @@ nlemma symmetric_eqquadruple : (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; - napply (Prod4T_ind T1 T2 T3 T4 ?? p1); + nelim p1; #x1; #y1; #z1; #v1; - napply (Prod4T_ind T1 T2 T3 T4 ?? p2); + nelim p2; #x2; #y2; #z2; #v2; nnormalize; nrewrite > (H x1 x2); @@ -294,9 +294,9 @@ nlemma eq_to_eqquadruple : (∀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; - napply (Prod4T_ind T1 T2 T3 T4 ?? p1); + nelim p1; #x1; #y1; #z1; #v1; - napply (Prod4T_ind T1 T2 T3 T4 ?? p2); + nelim p2; #x2; #y2; #z2; #v2; #H; nnormalize; nrewrite > (H1 ?? (quadruple_destruct_1 ???????????? H)); @@ -318,9 +318,9 @@ nlemma eqquadruple_to_eq : (∀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; - napply (Prod4T_ind T1 T2 T3 T4 ?? p1); + nelim p1; #x1; #y1; #z1; #v1; - napply (Prod4T_ind T1 T2 T3 T4 ?? p2); + nelim p2; #x2; #y2; #z2; #v2; #H; nnormalize in H:(%); nletin K ≝ (H1 x1 x2); @@ -403,9 +403,9 @@ nlemma symmetric_eqquintuple : (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; - napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p1); + nelim p1; #x1; #y1; #z1; #v1; #w1; - napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p2); + nelim p2; #x2; #y2; #z2; #v2; #w2; nnormalize; nrewrite > (H x1 x2); @@ -441,9 +441,9 @@ nlemma eq_to_eqquintuple : (∀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; - napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p1); + nelim p1; #x1; #y1; #z1; #v1; #w1; - napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p2); + nelim p2; #x2; #y2; #z2; #v2; #w2; #H; nnormalize; nrewrite > (H1 ?? (quintuple_destruct_1 ??????????????? H)); @@ -468,9 +468,9 @@ nlemma eqquintuple_to_eq : (∀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; - napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p1); + nelim p1; #x1; #y1; #z1; #v1; #w1; - napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p2); + nelim p2; #x2; #y2; #z2; #v2; #w2; #H; nnormalize in H:(%); nletin K ≝ (H1 x1 x2); diff --git a/helm/software/matita/contribs/ng_assembly/freescale/theory.ma b/helm/software/matita/contribs/ng_assembly/freescale/theory.ma index 81422d204..6aa2e35b0 100644 --- a/helm/software/matita/contribs/ng_assembly/freescale/theory.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/theory.ma @@ -208,7 +208,8 @@ nlemma list_destruct_nil_cons : ∀T.∀x:T.∀y:list T.nil T = cons T x y → F nqed. nlemma append_nil : ∀T:Type.∀l:list T.(l@[]) = l. - #T; #l; nelim l; + #T; #l; + nelim l; nnormalize; ##[ ##1: napply (refl_eq ??) ##| ##2: #x; #y; #H; @@ -239,4 +240,4 @@ nlemma append_cons_commute : ∀T:Type.∀a:T.∀l,l1:list T.l @ (a::l1) = (l@[a nrewrite > (associative_list T l [a] l1); nnormalize; napply (refl_eq ??). -nqed. \ No newline at end of file +nqed. diff --git a/helm/software/matita/contribs/ng_assembly/freescale/word16.ma b/helm/software/matita/contribs/ng_assembly/freescale/word16.ma index 53d798b35..efc8d9aab 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/word16.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/word16.ma @@ -32,21 +32,6 @@ nrecord word16 : Type ≝ w16l: byte8 }. -(*ndefinition word16_ind : ΠP:word16 → Prop.(Πb:byte8.Πb1:byte8.P (mk_word16 b b1)) → Πw:word16.P w ≝ -λP:word16 → Prop.λf:Πb:byte8.Πb1:byte8.P (mk_word16 b b1).λw:word16. - match w with [ mk_word16 (b:byte8) (b1:byte8) ⇒ f b b1 ]. - -ndefinition word16_rec : ΠP:word16 → Set.(Πb:byte8.Πb1:byte8.P (mk_word16 b b1)) → Πw:word16.P w ≝ -λP:word16 → Set.λf:Πb:byte8.Πb1:byte8.P (mk_word16 b b1).λw:word16. - match w with [ mk_word16 (b:byte8) (b1:byte8) ⇒ f b b1 ]. - -ndefinition word16_rect : ΠP:word16 → Type.(Πb:byte8.Πb1:byte8.P (mk_word16 b b1)) → Πw:word16.P w ≝ -λP:word16 → Type.λf:Πb:byte8.Πb1:byte8.P (mk_word16 b b1).λw:word16. - match w with [ mk_word16 (b:byte8) (b1:byte8) ⇒ f b b1 ]. - -ndefinition w16h ≝ λw:word16.match w with [ mk_word16 x _ ⇒ x ]. -ndefinition w16l ≝ λw:word16.match w with [ mk_word16 _ x ⇒ x ].*) - (* \langle \rangle *) notation "〈x:y〉" non associative with precedence 80 for @{ 'mk_word16 $x $y }. diff --git a/helm/software/matita/contribs/ng_assembly/freescale/word32.ma b/helm/software/matita/contribs/ng_assembly/freescale/word32.ma index 2e0dd8bac..0887f7991 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/word32.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/word32.ma @@ -32,21 +32,6 @@ nrecord word32 : Type ≝ w32l: word16 }. -(*ndefinition word32_ind : ΠP:word32 → Prop.(Πw:word16.Πw1:word16.P (mk_word32 w w1)) → Πdw:word32.P dw ≝ -λP:word32 → Prop.λf:Πw:word16.Πw1:word16.P (mk_word32 w w1).λdw:word32. - match dw with [ mk_word32 (w:word16) (w1:word16) ⇒ f w w1 ]. - -ndefinition word32_rec : ΠP:word32 → Set.(Πw:word16.Πw1:word16.P (mk_word32 w w1)) → Πdw:word32.P dw ≝ -λP:word32 → Set.λf:Πw:word16.Πw1:word16.P (mk_word32 w w1).λdw:word32. - match dw with [ mk_word32 (w:word16) (w1:word16) ⇒ f w w1 ]. - -ndefinition word32_rect : ΠP:word32 → Type.(Πw:word16.Πw1:word16.P (mk_word32 w w1)) → Πdw:word32.P dw ≝ -λP:word32 → Type.λf:Πw:word16.Πw1:word16.P (mk_word32 w w1).λdw:word32. - match dw with [ mk_word32 (w:word16) (w1:word16) ⇒ f w w1 ]. - -ndefinition w32h ≝ λdw:word32.match dw with [ mk_word32 x _ ⇒ x ]. -ndefinition w32l ≝ λdw:word32.match dw with [ mk_word32 _ x ⇒ x ].*) - (* \langle \rangle *) notation "〈x.y〉" non associative with precedence 80 for @{ 'mk_word32 $x $y }. diff --git a/helm/software/matita/contribs/ng_assembly/utility/ascii.ma b/helm/software/matita/contribs/ng_assembly/utility/ascii.ma index 38d2e7f53..19649d6ac 100755 --- a/helm/software/matita/contribs/ng_assembly/utility/ascii.ma +++ b/helm/software/matita/contribs/ng_assembly/utility/ascii.ma @@ -98,58 +98,6 @@ ninductive ascii : Type ≝ | ch_y: ascii | ch_z: ascii. -(*ndefinition ascii_ind - : ΠP:ascii → Prop. - P ch_0 → P ch_1 → P ch_2 → P ch_3 → P ch_4 → P ch_5 → P ch_6 → P ch_7 → P ch_8 → P ch_9 → P ch__ → - P ch_A → P ch_B → P ch_C → P ch_D → P ch_E → P ch_F → P ch_G → P ch_H → P ch_I → P ch_J → P ch_K → - P ch_L → P ch_M → P ch_N → P ch_O → P ch_P → P ch_Q → P ch_R → P ch_S → P ch_T → P ch_U → P ch_V → - P ch_W → P ch_X → P ch_Y → P ch_Z → P ch_a → P ch_b → P ch_c → P ch_d → P ch_e → P ch_f → P ch_g → - P ch_h → P ch_i → P ch_j → P ch_k → P ch_l → P ch_m → P ch_n → P ch_o → P ch_p → P ch_q → P ch_r → - P ch_s → P ch_t → P ch_u → P ch_v → P ch_w → P ch_x → P ch_y → P ch_z → Πa:ascii.P a ≝ -λP:ascii → Prop. -λp:P ch_0.λp1:P ch_1.λp2:P ch_2.λp3:P ch_3.λp4:P ch_4.λp5:P ch_5.λp6:P ch_6.λp7:P ch_7.λp8:P ch_8.λp9:P ch_9. -λp10:P ch__.λp11:P ch_A.λp12:P ch_B.λp13:P ch_C.λp14:P ch_D.λp15:P ch_E.λp16:P ch_F.λp17:P ch_G.λp18:P ch_H. -λp19:P ch_I.λp20:P ch_J.λp21:P ch_K.λp22:P ch_L.λp23:P ch_M.λp24:P ch_N.λp25:P ch_O.λp26:P ch_P.λp27:P ch_Q. -λp28:P ch_R.λp29:P ch_S.λp30:P ch_T.λp31:P ch_U.λp32:P ch_V.λp33:P ch_W.λp34:P ch_X.λp35:P ch_Y.λp36:P ch_Z. -λp37:P ch_a.λp38:P ch_b.λp39:P ch_c.λp40:P ch_d.λp41:P ch_e.λp42:P ch_f.λp43:P ch_g.λp44:P ch_h.λp45:P ch_i. -λp46:P ch_j.λp47:P ch_k.λp48:P ch_l.λp49:P ch_m.λp50:P ch_n.λp51:P ch_o.λp52:P ch_p.λp53:P ch_q.λp54:P ch_r. -λp55:P ch_s.λp56:P ch_t.λp57:P ch_u.λp58:P ch_v.λp59:P ch_w.λp60:P ch_x.λp61:P ch_y.λp62:P ch_z.λa:ascii. - match a with - [ ch_0 ⇒ p | ch_1 ⇒ p1 | ch_2 ⇒ p2 | ch_3 ⇒ p3 | ch_4 ⇒ p4 | ch_5 ⇒ p5 | ch_6 ⇒ p6 | ch_7 ⇒ p7 - | ch_8 ⇒ p8 | ch_9 ⇒ p9 | ch__ ⇒ p10 | ch_A ⇒ p11 | ch_B ⇒ p12 | ch_C ⇒ p13 | ch_D ⇒ p14 | ch_E ⇒ p15 - | ch_F ⇒ p16 | ch_G ⇒ p17 | ch_H ⇒ p18 | ch_I ⇒ p19 | ch_J ⇒ p20 | ch_K ⇒ p21 | ch_L ⇒ p22 | ch_M ⇒ p23 - | ch_N ⇒ p24 | ch_O ⇒ p25 | ch_P ⇒ p26 | ch_Q ⇒ p27 | ch_R ⇒ p28 | ch_S ⇒ p29 | ch_T ⇒ p30 | ch_U ⇒ p31 - | ch_V ⇒ p32 | ch_W ⇒ p33 | ch_X ⇒ p34 | ch_Y ⇒ p35 | ch_Z ⇒ p36 | ch_a ⇒ p37 | ch_b ⇒ p38 | ch_c ⇒ p39 - | ch_d ⇒ p40 | ch_e ⇒ p41 | ch_f ⇒ p42 | ch_g ⇒ p43 | ch_h ⇒ p44 | ch_i ⇒ p45 | ch_j ⇒ p46 | ch_k ⇒ p47 - | ch_l ⇒ p48 | ch_m ⇒ p49 | ch_n ⇒ p50 | ch_o ⇒ p51 | ch_p ⇒ p52 | ch_q ⇒ p53 | ch_r ⇒ p54 | ch_s ⇒ p55 - | ch_t ⇒ p56 | ch_u ⇒ p57 | ch_v ⇒ p58 | ch_w ⇒ p59 | ch_x ⇒ p60 | ch_y ⇒ p61 | ch_z ⇒ p62 ]. - -ndefinition ascii_rect - : ΠP:ascii → Type. - P ch_0 → P ch_1 → P ch_2 → P ch_3 → P ch_4 → P ch_5 → P ch_6 → P ch_7 → P ch_8 → P ch_9 → P ch__ → - P ch_A → P ch_B → P ch_C → P ch_D → P ch_E → P ch_F → P ch_G → P ch_H → P ch_I → P ch_J → P ch_K → - P ch_L → P ch_M → P ch_N → P ch_O → P ch_P → P ch_Q → P ch_R → P ch_S → P ch_T → P ch_U → P ch_V → - P ch_W → P ch_X → P ch_Y → P ch_Z → P ch_a → P ch_b → P ch_c → P ch_d → P ch_e → P ch_f → P ch_g → - P ch_h → P ch_i → P ch_j → P ch_k → P ch_l → P ch_m → P ch_n → P ch_o → P ch_p → P ch_q → P ch_r → - P ch_s → P ch_t → P ch_u → P ch_v → P ch_w → P ch_x → P ch_y → P ch_z → Πa:ascii.P a ≝ -λP:ascii → Type. -λp:P ch_0.λp1:P ch_1.λp2:P ch_2.λp3:P ch_3.λp4:P ch_4.λp5:P ch_5.λp6:P ch_6.λp7:P ch_7.λp8:P ch_8.λp9:P ch_9. -λp10:P ch__.λp11:P ch_A.λp12:P ch_B.λp13:P ch_C.λp14:P ch_D.λp15:P ch_E.λp16:P ch_F.λp17:P ch_G.λp18:P ch_H. -λp19:P ch_I.λp20:P ch_J.λp21:P ch_K.λp22:P ch_L.λp23:P ch_M.λp24:P ch_N.λp25:P ch_O.λp26:P ch_P.λp27:P ch_Q. -λp28:P ch_R.λp29:P ch_S.λp30:P ch_T.λp31:P ch_U.λp32:P ch_V.λp33:P ch_W.λp34:P ch_X.λp35:P ch_Y.λp36:P ch_Z. -λp37:P ch_a.λp38:P ch_b.λp39:P ch_c.λp40:P ch_d.λp41:P ch_e.λp42:P ch_f.λp43:P ch_g.λp44:P ch_h.λp45:P ch_i. -λp46:P ch_j.λp47:P ch_k.λp48:P ch_l.λp49:P ch_m.λp50:P ch_n.λp51:P ch_o.λp52:P ch_p.λp53:P ch_q.λp54:P ch_r. -λp55:P ch_s.λp56:P ch_t.λp57:P ch_u.λp58:P ch_v.λp59:P ch_w.λp60:P ch_x.λp61:P ch_y.λp62:P ch_z.λa:ascii. - match a with - [ ch_0 ⇒ p | ch_1 ⇒ p1 | ch_2 ⇒ p2 | ch_3 ⇒ p3 | ch_4 ⇒ p4 | ch_5 ⇒ p5 | ch_6 ⇒ p6 | ch_7 ⇒ p7 - | ch_8 ⇒ p8 | ch_9 ⇒ p9 | ch__ ⇒ p10 | ch_A ⇒ p11 | ch_B ⇒ p12 | ch_C ⇒ p13 | ch_D ⇒ p14 | ch_E ⇒ p15 - | ch_F ⇒ p16 | ch_G ⇒ p17 | ch_H ⇒ p18 | ch_I ⇒ p19 | ch_J ⇒ p20 | ch_K ⇒ p21 | ch_L ⇒ p22 | ch_M ⇒ p23 - | ch_N ⇒ p24 | ch_O ⇒ p25 | ch_P ⇒ p26 | ch_Q ⇒ p27 | ch_R ⇒ p28 | ch_S ⇒ p29 | ch_T ⇒ p30 | ch_U ⇒ p31 - | ch_V ⇒ p32 | ch_W ⇒ p33 | ch_X ⇒ p34 | ch_Y ⇒ p35 | ch_Z ⇒ p36 | ch_a ⇒ p37 | ch_b ⇒ p38 | ch_c ⇒ p39 - | ch_d ⇒ p40 | ch_e ⇒ p41 | ch_f ⇒ p42 | ch_g ⇒ p43 | ch_h ⇒ p44 | ch_i ⇒ p45 | ch_j ⇒ p46 | ch_k ⇒ p47 - | ch_l ⇒ p48 | ch_m ⇒ p49 | ch_n ⇒ p50 | ch_o ⇒ p51 | ch_p ⇒ p52 | ch_q ⇒ p53 | ch_r ⇒ p54 | ch_s ⇒ p55 - | ch_t ⇒ p56 | ch_u ⇒ p57 | ch_v ⇒ p58 | ch_w ⇒ p59 | ch_x ⇒ p60 | ch_y ⇒ p61 | ch_z ⇒ p62 ]. -*) (* confronto fra ascii *) ndefinition eq_ascii ≝ λc,c':ascii.match c with diff --git a/helm/software/matita/contribs/ng_assembly/utility/ascii_lemmas1.ma b/helm/software/matita/contribs/ng_assembly/utility/ascii_lemmas1.ma index efab13f9d..1c14a9774 100755 --- a/helm/software/matita/contribs/ng_assembly/utility/ascii_lemmas1.ma +++ b/helm/software/matita/contribs/ng_assembly/utility/ascii_lemmas1.ma @@ -37,434 +37,434 @@ nqed. ndefinition ascii_destruct2 : Πc2.ΠP:Prop.ch_1 = c2 → match c2 with [ ch_1 ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##2: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_1 with [ ch_1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_1 with [ ch_1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct3 : Πc2.ΠP:Prop.ch_2 = c2 → match c2 with [ ch_2 ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##3: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_2 with [ ch_2 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_2 with [ ch_2 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct4 : Πc2.ΠP:Prop.ch_3 = c2 → match c2 with [ ch_3 ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##4: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_3 with [ ch_3 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_3 with [ ch_3 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct5 : Πc2.ΠP:Prop.ch_4 = c2 → match c2 with [ ch_4 ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##5: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_4 with [ ch_4 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_4 with [ ch_4 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct6 : Πc2.ΠP:Prop.ch_5 = c2 → match c2 with [ ch_5 ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##6: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_5 with [ ch_5 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_5 with [ ch_5 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct7 : Πc2.ΠP:Prop.ch_6 = c2 → match c2 with [ ch_6 ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##7: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_6 with [ ch_6 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_6 with [ ch_6 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct8 : Πc2.ΠP:Prop.ch_7 = c2 → match c2 with [ ch_7 ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##8: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_7 with [ ch_7 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_7 with [ ch_7 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct9 : Πc2.ΠP:Prop.ch_8 = c2 → match c2 with [ ch_8 ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##9: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_8 with [ ch_8 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_8 with [ ch_8 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct10 : Πc2.ΠP:Prop.ch_9 = c2 → match c2 with [ ch_9 ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##10: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_9 with [ ch_9 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_9 with [ ch_9 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct11 : Πc2.ΠP:Prop.ch__ = c2 → match c2 with [ ch__ ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##11: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch__ with [ ch__ ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch__ with [ ch__ ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct12 : Πc2.ΠP:Prop.ch_A = c2 → match c2 with [ ch_A ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##12: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_A with [ ch_A ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_A with [ ch_A ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct13 : Πc2.ΠP:Prop.ch_B = c2 → match c2 with [ ch_B ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##13: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_B with [ ch_B ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_B with [ ch_B ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct14 : Πc2.ΠP:Prop.ch_C = c2 → match c2 with [ ch_C ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##14: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_C with [ ch_C ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_C with [ ch_C ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct15 : Πc2.ΠP:Prop.ch_D = c2 → match c2 with [ ch_D ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##15: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_D with [ ch_D ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_D with [ ch_D ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct16 : Πc2.ΠP:Prop.ch_E = c2 → match c2 with [ ch_E ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##16: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_E with [ ch_E ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_E with [ ch_E ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct17 : Πc2.ΠP:Prop.ch_F = c2 → match c2 with [ ch_F ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##17: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_F with [ ch_F ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_F with [ ch_F ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct18 : Πc2.ΠP:Prop.ch_G = c2 → match c2 with [ ch_G ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##18: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_G with [ ch_G ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_G with [ ch_G ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct19 : Πc2.ΠP:Prop.ch_H = c2 → match c2 with [ ch_H ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##19: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_H with [ ch_H ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_H with [ ch_H ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct20 : Πc2.ΠP:Prop.ch_I = c2 → match c2 with [ ch_I ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##20: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_I with [ ch_I ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_I with [ ch_I ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct21 : Πc2.ΠP:Prop.ch_J = c2 → match c2 with [ ch_J ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##21: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_J with [ ch_J ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_J with [ ch_J ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct22 : Πc2.ΠP:Prop.ch_K = c2 → match c2 with [ ch_K ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##22: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_K with [ ch_K ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_K with [ ch_K ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct23 : Πc2.ΠP:Prop.ch_L = c2 → match c2 with [ ch_L ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##23: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_L with [ ch_L ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_L with [ ch_L ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct24 : Πc2.ΠP:Prop.ch_M = c2 → match c2 with [ ch_M ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##24: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_M with [ ch_M ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_M with [ ch_M ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct25 : Πc2.ΠP:Prop.ch_N = c2 → match c2 with [ ch_N ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##25: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_N with [ ch_N ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_N with [ ch_N ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct26 : Πc2.ΠP:Prop.ch_O = c2 → match c2 with [ ch_O ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##26: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_O with [ ch_O ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_O with [ ch_O ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct27 : Πc2.ΠP:Prop.ch_P = c2 → match c2 with [ ch_P ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##27: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_P with [ ch_P ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_P with [ ch_P ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct28 : Πc2.ΠP:Prop.ch_Q = c2 → match c2 with [ ch_Q ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##28: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_Q with [ ch_Q ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_Q with [ ch_Q ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct29 : Πc2.ΠP:Prop.ch_R = c2 → match c2 with [ ch_R ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##29: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_R with [ ch_R ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_R with [ ch_R ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct30 : Πc2.ΠP:Prop.ch_S = c2 → match c2 with [ ch_S ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##30: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_S with [ ch_S ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_S with [ ch_S ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct31 : Πc2.ΠP:Prop.ch_T = c2 → match c2 with [ ch_T ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##31: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_T with [ ch_T ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_T with [ ch_T ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct32 : Πc2.ΠP:Prop.ch_U = c2 → match c2 with [ ch_U ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##32: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_U with [ ch_U ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_U with [ ch_U ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct33 : Πc2.ΠP:Prop.ch_V = c2 → match c2 with [ ch_V ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##33: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_V with [ ch_V ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_V with [ ch_V ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct34 : Πc2.ΠP:Prop.ch_W = c2 → match c2 with [ ch_W ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##34: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_W with [ ch_W ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_W with [ ch_W ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct35 : Πc2.ΠP:Prop.ch_X = c2 → match c2 with [ ch_X ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##35: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_X with [ ch_X ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_X with [ ch_X ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct36 : Πc2.ΠP:Prop.ch_Y = c2 → match c2 with [ ch_Y ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##36: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_Y with [ ch_Y ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_Y with [ ch_Y ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct37 : Πc2.ΠP:Prop.ch_Z = c2 → match c2 with [ ch_Z ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##37: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_Z with [ ch_Z ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_Z with [ ch_Z ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct38 : Πc2.ΠP:Prop.ch_a = c2 → match c2 with [ ch_a ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##38: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_a with [ ch_a ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_a with [ ch_a ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct39 : Πc2.ΠP:Prop.ch_b = c2 → match c2 with [ ch_b ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##39: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_b with [ ch_b ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_b with [ ch_b ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct40 : Πc2.ΠP:Prop.ch_c = c2 → match c2 with [ ch_c ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##40: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_c with [ ch_c ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_c with [ ch_c ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct41 : Πc2.ΠP:Prop.ch_d = c2 → match c2 with [ ch_d ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##41: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_d with [ ch_d ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_d with [ ch_d ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct42 : Πc2.ΠP:Prop.ch_e = c2 → match c2 with [ ch_e ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##42: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_e with [ ch_e ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_e with [ ch_e ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct43 : Πc2.ΠP:Prop.ch_f = c2 → match c2 with [ ch_f ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##43: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_f with [ ch_f ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_f with [ ch_f ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct44 : Πc2.ΠP:Prop.ch_g = c2 → match c2 with [ ch_g ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##44: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_g with [ ch_g ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_g with [ ch_g ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct45 : Πc2.ΠP:Prop.ch_h = c2 → match c2 with [ ch_h ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##45: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_h with [ ch_h ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_h with [ ch_h ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct46 : Πc2.ΠP:Prop.ch_i = c2 → match c2 with [ ch_i ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##46: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_i with [ ch_i ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_i with [ ch_i ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct47 : Πc2.ΠP:Prop.ch_j = c2 → match c2 with [ ch_j ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##47: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_j with [ ch_j ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_j with [ ch_j ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct48 : Πc2.ΠP:Prop.ch_k = c2 → match c2 with [ ch_k ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##48: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_k with [ ch_k ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_k with [ ch_k ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct49 : Πc2.ΠP:Prop.ch_l = c2 → match c2 with [ ch_l ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##49: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_l with [ ch_l ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_l with [ ch_l ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct50 : Πc2.ΠP:Prop.ch_m = c2 → match c2 with [ ch_m ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##50: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_m with [ ch_m ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_m with [ ch_m ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct51 : Πc2.ΠP:Prop.ch_n = c2 → match c2 with [ ch_n ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##51: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_n with [ ch_n ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_n with [ ch_n ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct52 : Πc2.ΠP:Prop.ch_o = c2 → match c2 with [ ch_o ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##52: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_o with [ ch_o ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_o with [ ch_o ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct53 : Πc2.ΠP:Prop.ch_p = c2 → match c2 with [ ch_p ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##53: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_p with [ ch_p ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_p with [ ch_p ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct54 : Πc2.ΠP:Prop.ch_q = c2 → match c2 with [ ch_q ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##54: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_q with [ ch_q ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_q with [ ch_q ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct55 : Πc2.ΠP:Prop.ch_r = c2 → match c2 with [ ch_r ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##55: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_r with [ ch_r ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_r with [ ch_r ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct56 : Πc2.ΠP:Prop.ch_s = c2 → match c2 with [ ch_s ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##56: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_s with [ ch_s ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_s with [ ch_s ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct57 : Πc2.ΠP:Prop.ch_t = c2 → match c2 with [ ch_t ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##57: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_t with [ ch_t ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_t with [ ch_t ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct58 : Πc2.ΠP:Prop.ch_u = c2 → match c2 with [ ch_u ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##58: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_u with [ ch_u ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_u with [ ch_u ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct59 : Πc2.ΠP:Prop.ch_v = c2 → match c2 with [ ch_v ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##59: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_v with [ ch_v ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_v with [ ch_v ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct60 : Πc2.ΠP:Prop.ch_w = c2 → match c2 with [ ch_w ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##60: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_w with [ ch_w ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_w with [ ch_w ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct61 : Πc2.ΠP:Prop.ch_x = c2 → match c2 with [ ch_x ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##61: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_x with [ ch_x ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_x with [ ch_x ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct62 : Πc2.ΠP:Prop.ch_y = c2 → match c2 with [ ch_y ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##62: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_y with [ ch_y ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_y with [ ch_y ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. ndefinition ascii_destruct63 : Πc2.ΠP:Prop.ch_z = c2 → match c2 with [ ch_z ⇒ P → P | _ ⇒ P ]. #c2; #P; ncases c2; nnormalize; ##[ ##63: #H; napply (λx:P.x) - ##| ##*: #H; napply (False_ind ??); nchange with (match ch_z with [ ch_z ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I + ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_z with [ ch_z ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I ##] nqed. diff --git a/helm/software/matita/contribs/ng_assembly/utility/string.ma b/helm/software/matita/contribs/ng_assembly/utility/string.ma index ea1c1ccd1..736bbf722 100644 --- a/helm/software/matita/contribs/ng_assembly/utility/string.ma +++ b/helm/software/matita/contribs/ng_assembly/utility/string.ma @@ -23,6 +23,7 @@ include "utility/ascii.ma". include "freescale/theory.ma". include "freescale/nat.ma". +include "utility/utility.ma". (* ************************ *) (* MANIPOLAZIONE DI STRINGA *) @@ -32,41 +33,22 @@ include "freescale/nat.ma". ndefinition aux_str_type ≝ list ascii. (* strcmp *) -nlet rec eq_str (str,str':aux_str_type) ≝ - match str with - [ nil ⇒ match str' with - [ nil => true - | cons _ _ => false ] - | cons h t ⇒ match str' with - [ nil ⇒ false - | cons h' t' ⇒ (eq_ascii h h')⊗(eq_str t t') - ] - ]. +ndefinition eq_str ≝ + bfold_right_list2 ascii (λx,y.eq_ascii x y). (* ************ *) (* STRINGA + ID *) (* ************ *) (* tipo pubblico *) -ninductive aux_strId_type : Type ≝ - STR_ID: aux_str_type → nat → aux_strId_type. - -(*ndefinition aux_strId_type_ind : ΠP:aux_strId_type → Prop.(Πl,n.P (STR_ID l n)) → Πa:aux_strId_type.P a ≝ -λP:aux_strId_type → Prop.λf:Πl,n.P (STR_ID l n).λa:aux_strId_type. - match a with [ STR_ID l n ⇒ f l n ]. - -ndefinition aux_strId_type_rec : ΠP:aux_strId_type → Set.(Πl,n.P (STR_ID l n)) → Πa:aux_strId_type.P a ≝ -λP:aux_strId_type → Set.λf:Πl,n.P (STR_ID l n).λa:aux_strId_type. - match a with [ STR_ID l n ⇒ f l n ]. - -ndefinition aux_strId_type_rect : ΠP:aux_strId_type → Type.(Πl,n.P (STR_ID l n)) → Πa:aux_strId_type.P a ≝ -λP:aux_strId_type → Type.λf:Πl,n.P (STR_ID l n).λa:aux_strId_type. - match a with [ STR_ID l n ⇒ f l n ].*) - -(* getter *) -ndefinition get_name_strId ≝ λsid:aux_strId_type.match sid with [ STR_ID n _ ⇒ n ]. -ndefinition get_id_strId ≝ λsid:aux_strId_type.match sid with [ STR_ID _ d ⇒ d ]. +nrecord strId : Type ≝ + { + str_elem: aux_str_type; + id_elem: nat + }. (* confronto *) ndefinition eq_strId ≝ -λsid,sid':aux_strId_type.(eq_str (get_name_strId sid) (get_name_strId sid'))⊗(eq_nat (get_id_strId sid) (get_id_strId sid')). +λsid,sid':strId. + (eq_str (str_elem sid) (str_elem sid'))⊗ + (eq_nat (id_elem sid) (id_elem sid')). diff --git a/helm/software/matita/contribs/ng_assembly/utility/string_lemmas.ma b/helm/software/matita/contribs/ng_assembly/utility/string_lemmas.ma index 3944d87ad..d00d67bb9 100755 --- a/helm/software/matita/contribs/ng_assembly/utility/string_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/utility/string_lemmas.ma @@ -23,104 +23,62 @@ include "utility/string.ma". include "utility/ascii_lemmas2.ma". include "freescale/nat_lemmas.ma". +include "utility/utility_lemmas.ma". (* ************************ *) (* MANIPOLAZIONE DI STRINGA *) (* ************************ *) -nlemma symmetric_eqstr : symmetricT aux_str_type bool eq_str. - #l1; - napply (list_ind ascii ??? l1); - ##[ ##1: #l2; ncases l2; - ##[ ##1: nnormalize; napply (refl_eq ??) - ##| ##2: #x; #y; nnormalize; napply (refl_eq ??) - ##] - ##| ##2: #x1; #x2; #H; #l2; ncases l2; - ##[ ##1: nnormalize; napply (refl_eq ??) - ##| ##2: #y1; #y2; - nchange with (((eq_ascii x1 y1)⊗(eq_str x2 y2)) = ((eq_ascii y1 x1)⊗(eq_str y2 x2))); - nrewrite > (symmetric_eqascii x1 y1); - nrewrite > (H y2); - napply (refl_eq ??) - ##] - ##] +nlemma symmetric_eqstr : symmetricT (list ascii) bool eq_str. + #s1; #s2; + napply (symmetric_bfoldrightlist2 ascii eq_ascii s1 s2 symmetric_eqascii). nqed. nlemma eqstr_to_eq : ∀s,s'.eq_str s s' = true → s = s'. - #l1; - napply (list_ind ascii ??? l1); - ##[ ##1: #l2; ncases l2; - ##[ ##1: nnormalize; #H; napply (refl_eq ??) - ##| ##2: #x1; #x2; nnormalize; #H; napply (bool_destruct ??? H) - ##] - ##| ##2: #x1; #x2; #H; #l2; ncases l2; - ##[ ##1: nnormalize; #H1; napply (bool_destruct ??? H1) - ##| ##2: #y1; #y2; #H1; - nchange in H1:(%) with (((eq_ascii x1 y1)⊗(eq_str x2 y2)) = true); - nrewrite > (eqascii_to_eq x1 y1 (andb_true_true_l ?? H1)); - nrewrite > (H y2 (andb_true_true_r ?? H1)); - napply (refl_eq ??) - ##] - ##] + #s1; #s2; + napply (bfoldrightlist2_to_eq ascii eq_ascii s1 s2 eqascii_to_eq). nqed. nlemma eq_to_eqstr : ∀s,s'.s = s' → eq_str s s' = true. - #l1; - napply (list_ind ascii ??? l1); - ##[ ##1: #l2; ncases l2; - ##[ ##1: nnormalize; #H; napply (refl_eq ??) - ##| ##2: #x1; #x2; nnormalize; #H; nelim (list_destruct_nil_cons ascii ?? H) - ##] - ##| ##2: #x1; #x2; #H; #l2; ncases l2; - ##[ ##1: #H; nelim (list_destruct_cons_nil ascii ?? H) - ##| ##2: #y1; #y2; #H1; - nrewrite > (list_destruct_1 ascii ???? H1); - nchange with (((eq_ascii y1 y1)⊗(eq_str x2 y2)) = true); - nrewrite > (H y2 (list_destruct_2 ascii ???? H1)); - nrewrite > (eq_to_eqascii y1 y1 (refl_eq ??)); - nnormalize; - napply (refl_eq ??) - ##] - ##] + #s1; #s2; + napply (eq_to_bfoldrightlist2 ascii eq_ascii s1 s2 eq_to_eqascii). nqed. (* ************ *) (* STRINGA + ID *) (* ************ *) -nlemma strid_destruct_1 : ∀x1,x2,y1,y2.STR_ID x1 y1 = STR_ID x2 y2 → x1 = x2. +nlemma strid_destruct_1 : ∀x1,x2,y1,y2.mk_strId x1 y1 = mk_strId x2 y2 → x1 = x2. #x1; #x2; #y1; #y2; #H; - nchange with (match STR_ID x2 y2 with [ STR_ID a _ ⇒ x1 = a ]); + nchange with (match mk_strId x2 y2 with [ mk_strId a _ ⇒ x1 = a ]); nrewrite < H; nnormalize; napply (refl_eq ??). nqed. -nlemma strid_destruct_2 : ∀x1,x2,y1,y2.STR_ID x1 y1 = STR_ID x2 y2 → y1 = y2. +nlemma strid_destruct_2 : ∀x1,x2,y1,y2.mk_strId x1 y1 = mk_strId x2 y2 → y1 = y2. #x1; #x2; #y1; #y2; #H; - nchange with (match STR_ID x2 y2 with [ STR_ID _ b ⇒ y1 = b ]); + nchange with (match mk_strId x2 y2 with [ mk_strId _ b ⇒ y1 = b ]); nrewrite < H; nnormalize; napply (refl_eq ??). nqed. -nlemma symmetric_eqstrid : symmetricT aux_strId_type bool eq_strId. +nlemma symmetric_eqstrid : symmetricT strId bool eq_strId. #si1; #si2; - ncases si1; - #l1; #n1; - ncases si2; - #l2; #n2; - nchange with (((eq_str l1 l2)⊗(eq_nat n1 n2)) = ((eq_str l2 l1)⊗(eq_nat n2 n1))); - nrewrite > (symmetric_eqstr l1 l2); - nrewrite > (symmetric_eqnat n1 n2); + nchange with ( + ((eq_str (str_elem si1) (str_elem si2))⊗(eq_nat (id_elem si1) (id_elem si2))) = + ((eq_str (str_elem si2) (str_elem si1))⊗(eq_nat (id_elem si2) (id_elem si1)))); + nrewrite > (symmetric_eqstr (str_elem si1) (str_elem si2)); + nrewrite > (symmetric_eqnat (id_elem si1) (id_elem si2)); napply (refl_eq ??). -nqed. +nqed. nlemma eqstrid_to_eq : ∀s,s'.eq_strId s s' = true → s = s'. - #si1; #si2; - ncases si1; + #si1; #si2; + nelim si1; #l1; #n1; - ncases si2; + nelim si2; #l2; #n2; #H; nchange in H:(%) with (((eq_str l1 l2)⊗(eq_nat n1 n2)) = true); nrewrite > (eqstr_to_eq l1 l2 (andb_true_true_l ?? H)); @@ -129,10 +87,10 @@ nlemma eqstrid_to_eq : ∀s,s'.eq_strId s s' = true → s = s'. nqed. nlemma eq_to_eqstrid : ∀s,s'.s = s' → eq_strId s s' = true. - #si1; #si2; - ncases si1; + #si1; #si2; + nelim si1; #l1; #n1; - ncases si2; + nelim si2; #l2; #n2; #H; nchange with (((eq_str l1 l2)⊗(eq_nat n1 n2)) = true); nrewrite > (strid_destruct_1 ???? H); diff --git a/helm/software/matita/contribs/ng_assembly/utility/utility.ma b/helm/software/matita/contribs/ng_assembly/utility/utility.ma index 69d88e8cb..17b966503 100755 --- a/helm/software/matita/contribs/ng_assembly/utility/utility.ma +++ b/helm/software/matita/contribs/ng_assembly/utility/utility.ma @@ -33,15 +33,6 @@ ninductive ne_list (A:Type) : Type ≝ | ne_nil: A → ne_list A | ne_cons: A → ne_list A → ne_list A. -(*nlet rec ne_list_ind (A:Type) (P:ne_list A → Prop) (f:Πd.P (ne_nil A d)) (f1:(Πa:A.Πl':ne_list A.P l' → P (ne_cons A a l'))) (l:ne_list A) on l ≝ - match l with [ ne_nil d ⇒ f d | ne_cons h t ⇒ f1 h t (ne_list_ind A P f f1 t) ]. - -nlet rec ne_list_rec (A:Type) (P:ne_list A → Set) (f:Πd.P (ne_nil A d)) (f1:(Πa:A.Πl':ne_list A.P l' → P (ne_cons A a l'))) (l:ne_list A) on l ≝ - match l with [ ne_nil d ⇒ f d | ne_cons h t ⇒ f1 h t (ne_list_rec A P f f1 t) ]. - -nlet rec ne_list_rect (A:Type) (P:ne_list A → Type) (f:Πd.P (ne_nil A d)) (f1:(Πa:A.Πl':ne_list A.P l' → P (ne_cons A a l'))) (l:ne_list A) on l ≝ - match l with [ ne_nil d ⇒ f d | ne_cons h t ⇒ f1 h t (ne_list_rect A P f f1 t) ].*) - (* append *) nlet rec ne_append (A:Type) (l1,l2:ne_list A) on l1 ≝ match l1 with @@ -236,8 +227,8 @@ nqed. nlemma fold_right_list2_aux3 : ∀T.∀h,h',t,t'.len_list T (h::t) = len_list T (h'::t') → len_list T t = len_list T t'. #T; #h; #h'; #t; #t'; - napply (list_ind T ??? t); - napply (list_ind T ??? t'); + nelim t; + nelim t'; ##[ ##1: nnormalize; #H; napply (refl_eq ??) ##| ##2: #a; #l'; #H; #H1; nchange in H1:(%) with ((S O) = (S (S (len_list T l')))); @@ -270,6 +261,15 @@ nlet rec fold_right_list2 (T1,T2:Type) (f:T1 → T1 → T2 → T2) (acc:T2) (l1: ] ]. +nlet rec bfold_right_list2 (T1:Type) (f:T1 → T1 → bool) (l1,l2:list T1) on l1 ≝ + match l1 with + [ nil ⇒ match l2 with + [ nil ⇒ true | cons h t ⇒ false ] + | cons h t ⇒ match l2 with + [ nil ⇒ false | cons h' t' ⇒ (f h h') ⊗ (bfold_right_list2 T1 f t t') + ] + ]. + nlemma fold_right_neList2_aux1 : ∀T.∀h,h',t'.len_neList T «£h» = len_neList T (h'§§t') → False. #T; #h; #h'; #t'; @@ -295,8 +295,8 @@ nqed. nlemma fold_right_neList2_aux3 : ∀T.∀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'; - napply (ne_list_ind T ??? t); - napply (ne_list_ind T ??? t'); + nelim t; + nelim t'; ##[ ##1: nnormalize; #x; #y; #H; napply (refl_eq ??) ##| ##2: #a; #l'; #H; #x; #H1; nchange in H1:(%) with ((S (len_neList T «£x»)) = (S (len_neList T (a§§l')))); @@ -331,6 +331,15 @@ nlet rec fold_right_neList2 (T1,T2:Type) (f:T1 → T1 → T2 → T2) (acc:T2) (l ] ]. +nlet rec bfold_right_neList2 (T1:Type) (f:T1 → T1 → bool) (l1,l2:ne_list T1) on l1 ≝ + match l1 with + [ ne_nil h ⇒ match l2 with + [ ne_nil h' ⇒ f h h' | ne_cons h' t' ⇒ false ] + | ne_cons h t ⇒ match l2 with + [ ne_nil h' ⇒ false | ne_cons h' t' ⇒ (f h h') ⊗ (bfold_right_neList2 T1 f t t') + ] + ]. + (* ******** *) (* naturali *) (* ******** *) diff --git a/helm/software/matita/contribs/ng_assembly/utility/utility_lemmas.ma b/helm/software/matita/contribs/ng_assembly/utility/utility_lemmas.ma index 557cdfbb1..40aaf0b4e 100755 --- a/helm/software/matita/contribs/ng_assembly/utility/utility_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/utility/utility_lemmas.ma @@ -68,7 +68,7 @@ nqed. nlemma symmetric_eqlenlist : ∀T.∀l1,l2:list T.len_list T l1 = len_list T l2 → len_list T l2 = len_list T l1. #T; #l1; - napply (list_ind ???? l1); + nelim l1; ##[ ##1: #l2; ncases l2; nnormalize; ##[ ##1: #H; napply (refl_eq ??) ##| ##2: #h; #t; #H; nelim (nat_destruct_0_S ? H) @@ -86,7 +86,7 @@ nlemma symmetric_foldrightlist2_aux (∀x,y,z.f x y z = f y x z) → fold_right_list2 T1 T2 f acc l1 l2 H1 = fold_right_list2 T1 T2 f acc l2 l1 H2. #T1; #T2; #f; #acc; #l1; - napply (list_ind ???? l1); + nelim l1; ##[ ##1: #l2; ncases l2; ##[ ##1: nnormalize; #H1; #H2; #H3; napply (refl_eq ??) ##| ##2: #h; #l; #H1; #H2; #H3; @@ -117,9 +117,72 @@ nlemma symmetric_foldrightlist2 napply (refl_eq ??). nqed. +nlemma symmetric_bfoldrightlist2 + : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:list T1. + (∀x,y.f x y = f y x) → + bfold_right_list2 T1 f l1 l2 = bfold_right_list2 T1 f l2 l1. + #T; #f; #l1; + nelim l1; + ##[ ##1: #l2; ncases l2; + ##[ ##1: #H; nnormalize; napply (refl_eq ??) + ##| ##2: #hh2; #ll2; #H; nnormalize; napply (refl_eq ??) + ##] + ##| ##2: #hh1; #ll1; #H; #l2; ncases l2; + ##[ ##1: #H1; nnormalize; napply (refl_eq ??) + ##| ##2: #hh2; #ll2; #H1; nnormalize; + nrewrite > (H ll2 H1); + nrewrite > (H1 hh1 hh2); + napply (refl_eq ??) + ##] + ##] +nqed. + +nlemma bfoldrightlist2_to_eq + : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:list T1. + (∀x,y.(f x y = true → x = y)) → + (bfold_right_list2 T1 f l1 l2 = true → l1 = l2). + #T; #f; #l1; + nelim l1; + ##[ ##1: #l2; ncases l2; + ##[ ##1: #H; #H1; napply (refl_eq ??) + ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; napply (bool_destruct ??? H1) + ##] + ##| ##2: #hh1; #ll1; #H; #l2; ncases l2; + ##[ ##1: #H1; nnormalize; #H2; napply (bool_destruct ??? H2) + ##| ##2: #hh2; #ll2; #H1; #H2; + nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = true); + nrewrite > (H1 hh1 hh2 (andb_true_true_l ?? H2)); + nrewrite > (H ll2 H1 (andb_true_true_r ?? H2)); + napply (refl_eq ??) + ##] + ##] +nqed. + +nlemma eq_to_bfoldrightlist2 + : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:list T1. + (∀x,y.(x = y → f x y = true)) → + (l1 = l2 → bfold_right_list2 T1 f l1 l2 = true). + #T; #f; #l1; + nelim l1; + ##[ ##1: #l2; ncases l2; + ##[ ##1: #H; #H1; nnormalize; napply (refl_eq ??) + ##| ##2: #hh2; #ll2; #H; #H1; nelim (list_destruct_nil_cons ??? H1) + ##] + ##| ##2: #hh1; #ll1; #H; #l2; ncases l2; + ##[ ##1: #H1; #H2; nelim (list_destruct_cons_nil ??? H2) + ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize; + nrewrite > (list_destruct_1 ????? H2); + nrewrite > (H1 hh2 hh2 (refl_eq ??)); + nnormalize; + nrewrite > (H ll2 H1 (list_destruct_2 ????? H2)); + napply (refl_eq ??) + ##] + ##] +nqed. + nlemma symmetric_eqlennelist : ∀T.∀l1,l2:ne_list T.len_neList T l1 = len_neList T l2 → len_neList T l2 = len_neList T l1. #T; #l1; - napply (ne_list_ind ???? l1); + nelim l1; ##[ ##1: #h; #l2; ncases l2; nnormalize; ##[ ##1: #H; #H1; napply (refl_eq ??) ##| ##2: #h; #t; #H; nrewrite > H; napply (refl_eq ??) @@ -137,7 +200,7 @@ nlemma symmetric_foldrightnelist2_aux (∀x,y,z.f x y z = f y x z) → fold_right_neList2 T1 T2 f acc l1 l2 H1 = fold_right_neList2 T1 T2 f acc l2 l1 H2. #T1; #T2; #f; #acc; #l1; - napply (ne_list_ind ???? l1); + nelim l1; ##[ ##1: #h; #l2; ncases l2; ##[ ##1: #h1; nnormalize; #H1; #H2; #H3; nrewrite > (H3 h h1 acc); napply (refl_eq ??) ##| ##2: #h1; #l; ncases l; @@ -179,6 +242,71 @@ nlemma symmetric_foldrightnelist2 napply (refl_eq ??). nqed. +nlemma symmetric_bfoldrightnelist2 + : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1. + (∀x,y.f x y = f y x) → + bfold_right_neList2 T1 f l1 l2 = bfold_right_neList2 T1 f l2 l1. + #T; #f; #l1; + nelim l1; + ##[ ##1: #hh1; #l2; ncases l2; + ##[ ##1: #hh2; #H; nnormalize; nrewrite > (H hh1 hh2); napply (refl_eq ??) + ##| ##2: #hh2; #ll2; #H; nnormalize; napply (refl_eq ??) + ##] + ##| ##2: #hh1; #ll1; #H; #l2; ncases l2; + ##[ ##1: #hh2; #H1; nnormalize; napply (refl_eq ??) + ##| ##2: #hh2; #ll2; #H1; nnormalize; + nrewrite > (H ll2 H1); + nrewrite > (H1 hh1 hh2); + napply (refl_eq ??) + ##] + ##] +nqed. + +nlemma bfoldrightnelist2_to_eq + : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1. + (∀x,y.(f x y = true → x = y)) → + (bfold_right_neList2 T1 f l1 l2 = true → l1 = l2). + #T; #f; #l1; + nelim l1; + ##[ ##1: #hh1; #l2; ncases l2; + ##[ ##1: #hh2; #H; #H1; nnormalize in H1:(%); nrewrite > (H hh1 hh2 H1); napply (refl_eq ??) + ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; napply (bool_destruct ??? H1) + ##] + ##| ##2: #hh1; #ll1; #H; #l2; ncases l2; + ##[ ##1: #hh2; #H1; nnormalize; #H2; napply (bool_destruct ??? H2) + ##| ##2: #hh2; #ll2; #H1; #H2; + nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = true); + nrewrite > (H1 hh1 hh2 (andb_true_true_l ?? H2)); + nrewrite > (H ll2 H1 (andb_true_true_r ?? H2)); + napply (refl_eq ??) + ##] + ##] +nqed. + +nlemma eq_to_bfoldrightnelist2 + : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1. + (∀x,y.(x = y → f x y = true)) → + (l1 = l2 → bfold_right_neList2 T1 f l1 l2 = true). + #T; #f; #l1; + nelim l1; + ##[ ##1: #hh1; #l2; ncases l2; + ##[ ##1: #hh2; #H; #H1; nnormalize; + nrewrite > (H hh1 hh2 (nelist_destruct_nil_nil ??? H1)); + napply (refl_eq ??) + ##| ##2: #hh2; #ll2; #H; #H1; nelim (nelist_destruct_nil_cons ???? H1) + ##] + ##| ##2: #hh1; #ll1; #H; #l2; ncases l2; + ##[ ##1: #hh2; #H1; #H2; nelim (nelist_destruct_cons_nil ???? H2) + ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize; + nrewrite > (nelist_destruct_cons_cons_1 ????? H2); + nrewrite > (H1 hh2 hh2 (refl_eq ??)); + nnormalize; + nrewrite > (H ll2 H1 (nelist_destruct_cons_cons_2 ????? H2)); + napply (refl_eq ??) + ##] + ##] +nqed. + nlemma isbemptylist_to_isemptylist : ∀T,l.isb_empty_list T l = true → is_empty_list T l. #T; #l; ncases l;