From 289d8d049e72beef41c17930f13727b5049981a2 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 4 Mar 2008 16:42:17 +0000 Subject: [PATCH] New syntax for patterns. --- .../library/freescale/medium_tests_lemmas.ma | 60 +++++++++---------- 1 file changed, 30 insertions(+), 30 deletions(-) diff --git a/helm/software/matita/library/freescale/medium_tests_lemmas.ma b/helm/software/matita/library/freescale/medium_tests_lemmas.ma index c7ae9a74e..e708f57bc 100644 --- a/helm/software/matita/library/freescale/medium_tests_lemmas.ma +++ b/helm/software/matita/library/freescale/medium_tests_lemmas.ma @@ -150,70 +150,70 @@ lemma execute_HCS08_LDHX_maIMM2 : intros; whd in ⊢ (? ? % ?); - whd in ⊢ (? ? match % in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?); + whd in ⊢ (? ? match % return ? with [_⇒?|_⇒?|_⇒?] ?); rewrite > H; - whd in ⊢ (? ? match % in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?); - whd in ⊢ (? ? match match % in fetch_result return ? with [FetchERR⇒?|FetchOK⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?); + whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?); + whd in ⊢ (? ? match match % in fetch_result return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?); rewrite > H1; - whd in ⊢ (? ? match match % in fetch_result return ? with [FetchERR⇒?|FetchOK⇒?] in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?); - change in ⊢ (? ? match % in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?) with + whd in ⊢ (? ? match match % in fetch_result return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?); + change in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?) with (match (quadrupleT (any_opcode HCS08) ??? LDHX MODE_IMM2 〈x4,x5〉 〈x0,x3〉) with  [quadrupleT pseudo mode _ tot_clk ⇒ match eq_b8 〈x0,x1〉 tot_clk with  [ true ⇒ tick_execute HCS08 t s pseudo mode (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)) | false ⇒ TickOK (any_status HCS08 t) (set_clk_desc HCS08 t s (Some ? (quintupleT ????? 〈x0,x1〉 pseudo mode tot_clk (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))))]]); - change in ⊢ (? ? match % in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?) with + change in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?) with (match eq_b8 〈x0,x1〉 〈x0,x3〉 with  [ true ⇒ tick_execute HCS08 t s (anyOP HCS08 LDHX) MODE_IMM2 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)) | false ⇒ TickOK (any_status HCS08 t) (set_clk_desc HCS08 t s (Some ? (quintupleT ????? 〈x0,x1〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))))]); - whd in ⊢ (? ? match % in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?); + whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?); letin status1 ≝ (set_clk_desc HCS08 t s (Some ? (quintupleT ????? 〈x0,x1〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s))))); change in ⊢ (? ? % ?) with (match 2 with  [ O ⇒ TickOK ? status1 | S (n':nat) ⇒ execute HCS08 t (tick HCS08 t status1) n']); - whd in ⊢ (? ? match ? in nat return ? with [O⇒?|S (n':?)⇒? ? ? % ?] ?); - unfold status1 in ⊢ (? ? match ? in nat return ? with [O⇒? |S (n':?)⇒ ? ? ? match ? ? ? % in option return ? with [None⇒?|Some⇒?] ?] ?); + whd in ⊢ (? ? match ? return ? with [_⇒?|_⇒λ_:?.? ? ? % ?] ?); + unfold status1 in ⊢ (? ? match ? in nat return ? with [_⇒? |_ ⇒ λ_.? ? ? match ? ? ? % in option return ? with [_⇒?|_⇒?] ?] ?); rewrite > (get_set_clk_desc HCS08 t s (Some ? (quintupleT ????? 〈x0,x1〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s))))); - whd in ⊢ (? ? match ? in nat return ? with [O⇒?|S (n':?)⇒? ? ? % ?] ?); - normalize in ⊢ (? ? match ? in nat return ? with [O⇒?|S (n':?)⇒? ? ? (? ? (? ? ? ? (? ? (? ? ? ? ? ? % ? ? ? ?)))) ?] ?); - whd in ⊢ (? ? match ? in nat return ? with [O⇒?|S (n':?)⇒%] ?); + whd in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_.? ? ? % ?] ?); + normalize in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_.? ? ? (? ? (? ? ? ? (? ? (? ? ? ? ? ? % ? ? ? ?)))) ?] ?); + whd in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_.%] ?); - unfold status1 in ⊢ (? ? match ? in nat return ? with [O⇒?|S (n':?)⇒? ? ? (? ? (? ? ? % ?)) ?] ?); + unfold status1 in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_.? ? ? (? ? (? ? ? % ?)) ?] ?); rewrite > (set_set_clk_desc HCS08 t s (Some ? (quintupleT ????? 〈x0,x1〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))) (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s))))) - in ⊢ (? ? match ? in nat return ? with [O⇒?|S (n':?)⇒? ? ? (? ? %) ?] ?); + in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_.? ? ? (? ? %) ?] ?); letin status2 ≝ (set_clk_desc HCS08 t s (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s))))); change in ⊢ (? ? % ?) with (match 1 with  [ O ⇒ TickOK ? status2 | S (n':nat) ⇒ execute HCS08 t (tick HCS08 t status2) n']); - whd in ⊢ (? ? match ? in nat return ? with [O⇒?|S (n':?)⇒? ? ? % ?] ?); - unfold status2 in ⊢ (? ? match ? in nat return ? with [O⇒? |S (n':?)⇒ ? ? ? match ? ? ? % in option return ? with [None⇒?|Some⇒?] ?] ?); + whd in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_.? ? ? % ?] ?); + unfold status2 in ⊢ (? ? match ? in nat return ? with [_⇒? |_⇒ λ_. ? ? ? match ? ? ? % in option return ? with [_⇒?|_⇒?] ?] ?); rewrite > (get_set_clk_desc HCS08 t s (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s))))); - whd in ⊢ (? ? match ? in nat return ? with [O⇒?|S (n':?)⇒? ? ? % ?] ?); - change in ⊢ (? ? match ? in nat return ? with [O⇒? |S (n':?)⇒? ? ? match % in option return ? with [None⇒?|Some⇒?] ?] ?) with + whd in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_.? ? ? % ?] ?); + change in ⊢ (? ? match ? in nat return ? with [_⇒? |_⇒λ_.? ? ? match % in option return ? with [_⇒?|_⇒?] ?] ?) with (execute_LDHX HCS08 t status2 MODE_IMM2 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s))); - whd in ⊢ (? ? match ? in nat return ? with [O⇒? |S (n':?)⇒? ? ? match % in option return ? with [None⇒?|Some⇒?] ?] ?); - whd in ⊢ (? ? match ? in nat return ? with [O⇒? |S (n':?)⇒ ? ? ? match match % in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] ?] ?); + whd in ⊢ (? ? match ? in nat return ? with [_⇒? |_⇒λ_.? ? ? match % in option return ? with [_⇒?|_⇒?] ?] ?); + whd in ⊢ (? ? match ? in nat return ? with [_⇒? |_⇒ λ_.? ? ? match match % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] ?] ?); - unfold status2 in ⊢ (? ? match ? in nat return ? with [O⇒?|S (n':?)⇒ ? ? ? match match match ? ? ? % ? in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] ?] ?); + unfold status2 in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_. ? ? ? match match match ? ? ? % ? in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] ?] ?); rewrite > (memory_filter_read_set_clk_desc HCS08 t s (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)) (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s))))) - in ⊢ (? ? match ? in nat return ? with [O⇒?|S (n':?)⇒ ? ? ? match match match % in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] ?] ?); - rewrite > H2 in ⊢ (? ? match ? in nat return ? with [O⇒?|S (n':?)⇒ ? ? ? match match match % in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] ?] ?); - whd in ⊢ (? ? match ? in nat return ? with [O⇒? |S (n':?)⇒ ? ? ? match match % in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] ?] ?); + in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_. ? ? ? match match match % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] ?] ?); + rewrite > H2 in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_. ? ? ? match match match % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] ?] ?); + whd in ⊢ (? ? match ? in nat return ? with [_⇒? |_⇒λ_. ? ? ? match match % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] ?] ?); - unfold status2 in ⊢ (? ? match ? in nat return ? with [O⇒?|S (n':?)⇒ ? ? ? match match match % in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] ?] ?); + unfold status2 in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_. ? ? ? match match match % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] ?] ?); rewrite > (filtered_inc_set_clk_desc HCS08 t s (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))) (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s))) - in ⊢ (? ? match ? in nat return ? with [O⇒?|S (n':?)⇒ ? ? ? match match match ? ? ? ? % in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] ?] ?); + in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_. ? ? ? match match match ? ? ? ? % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] ?] ?); rewrite > (memory_filter_read_set_clk_desc HCS08 t s (filtered_inc_w16 HCS08 t s (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s))) (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s))))) - in ⊢ (? ? match ? in nat return ? with [O⇒?|S (n':?)⇒ ? ? ? match match match % in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] ?] ?); - rewrite > H3 in ⊢ (? ? match ? in nat return ? with [O⇒?|S (n':?)⇒ ? ? ? match match match % in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] in option return ? with [None⇒?|Some⇒?] ?] ?); + in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_. ? ? ? match match match % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] ?] ?); + rewrite > H3 in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_. ? ? ? match match match % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] ?] ?); - whd in ⊢ (? ? match ? in nat return ? with [O⇒?|S (n':?)⇒? ? ? % ?] ?); + whd in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_.? ? ? % ?] ?); change in ⊢ (? ? % ?) with (TickOK ? (set_clk_desc HCS08 t @@ -244,7 +244,7 @@ lemma execute_HCS08_LDHX_maIMM2 : rewrite > (set_clk_desc_set_pc_reg HCS08 t (setweak_v_flag HCS08 t (setweak_n_flag HCS08 t (set_z_flag HCS08 t (set_alu HCS08 t s (set_indX_16_reg_HC08 (alu HCS08 t s) 〈bhigh:blow〉)) (eq_w16 〈bhigh:blow〉 〈〈x0,x0〉:〈x0,x0〉〉)) (MSB_w16 〈bhigh:blow〉)) false) (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))) (filtered_plus_w16 HCS08 t s (get_pc_reg HCS08 t s) 3)); rewrite > (set_set_clk_desc HCS08 t (set_pc_reg HCS08 t (setweak_v_flag HCS08 t (setweak_n_flag HCS08 t (set_z_flag HCS08 t (set_alu HCS08 t s (set_indX_16_reg_HC08 (alu HCS08 t s) 〈bhigh:blow〉)) (eq_w16 〈bhigh:blow〉 〈〈x0,x0〉:〈x0,x0〉〉)) (MSB_w16 〈bhigh:blow〉)) false) (filtered_plus_w16 HCS08 t s (get_pc_reg HCS08 t s) 3)) (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))) (None ?)); rewrite > (set_clk_f_set_clk_desc HCS08 t s (λtmps.set_pc_reg HCS08 t (setweak_v_flag HCS08 t (setweak_n_flag HCS08 t (set_z_flag HCS08 t (set_alu HCS08 t tmps (set_indX_16_reg_HC08 (alu HCS08 t tmps) 〈bhigh:blow〉)) (eq_w16 〈bhigh:blow〉 〈〈x0,x0〉:〈x0,x0〉〉)) (MSB_w16 〈bhigh:blow〉)) false) (filtered_plus_w16 HCS08 t tmps (get_pc_reg HCS08 t tmps) 3))) in ⊢ (? ? (? ? %) ?); - [2: elim H; reflexivity ] + [2: assumption ] reflexivity. qed. -- 2.39.2