From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 4 Mar 2008 16:42:17 +0000 (+0000)
Subject: New syntax for patterns.
X-Git-Tag: make_still_working~5568
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=289d8d049e72beef41c17930f13727b5049981a2;p=helm.git

New syntax for patterns.
---

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.