Changeset 1519

Timestamp:

Nov 21, 2011, 12:10:57 PM (8 years ago)

Author:

campbell

Message:

More syntax updates.

Location:

src/ASM

Files:

• Interpret.ma (modified) (3 diffs)
• StatusProofs.ma (modified) (11 diffs)

src/ASM/Interpret.ma

@@ -40 +40 @@
    # H2
    normalize
-   change in H2: (??%?) with (orb ??)
+   change in H2: (??%?); with (orb ??)
    cases (inclusive_disjunction_true … H2)
    [ # K
@@ -77 +77 @@
    # tl
    # II
-   whd in ⊢ (% → ? → ?)
+   whd in ⊢ (% → ? → ?);
    lapply (refl … (is_in … (he:::tl) a))
-   cases (is_in … (he:::tl) a) in ⊢ (???% → %)
+   cases (is_in … (he:::tl) a) in ⊢ (???% → %);
    [ # K
      # _
      normalize in K;
-     whd in ⊢ (% → ?)
-     lapply (refl … (subvector_with … eq_a (he:::tl) q))
-     cases (subvector_with … eq_a (he:::tl) q) in ⊢ (???% → %)
+     whd in ⊢ (% → ?);
+     lapply (refl … (subvector_with … eq_a (he:::tl) q));
+     cases (subvector_with … eq_a (he:::tl) q) in ⊢ (???% → %);
      [ # K1
        # _
-       change in K1 with ((andb ? (subvector_with …)) = true)
+       change in K1; with ((andb ? (subvector_with …)) = true)
        cases (conjunction_true … K1)
        # K3
@@ -105 +105 @@
      | # K1
        # K2
-       (normalize in K2)
+       (normalize in K2;)
        cases K2;
      ]

src/ASM/StatusProofs.ma

@@ -41 +41 @@
   set_code_memory T U (set_bit_addressable_sfr ? ps x val) code_mem.
   #T #U #ps #code_mem #x #val
-  whd in ⊢ (??%?)
-  whd in ⊢ (???(???%?))
+  whd in ⊢ (??%?);
+  whd in ⊢ (???(???%?));
   cases (eqb ? 128) [ normalize nodelta cases not_implemented
   | normalize nodelta
@@ -115 +115 @@
   #n #l #T #U #ps #code_mem #val * *;
   #x try (#y #H) try #H whd in H; try cases H
-  whd in ⊢ (??(%)?) whd in ⊢ (???(???(%)?)) try %
+  whd in ⊢ (??(%)?); whd in ⊢ (???(???(%)?)); try %
   cases (split bool 4 4 ?) #nu' #nl' normalize nodelta
   cases (split bool 1 3 nu') #bit1' #ignore' normalize nodelta
@@ -137 +137 @@
   #n #l #T #ps #pc #val * *;
   #x try (#y #H) try #H whd in H; try cases H
-  whd in ⊢ (??(%)?) whd in ⊢ (???(??(%)?)) try %
+  whd in ⊢ (??(%)?); whd in ⊢ (???(??(%)?)); try %
   cases (split bool 4 4 ?) #nu' #nl' normalize nodelta
   cases (split bool 1 3 nu') #bit1' #ignore' normalize nodelta
@@ -175 +175 @@
     special_function_registers_8051 T (write_at_stack_pointer T s x)
   = special_function_registers_8051 T s.
- #T #s #x whd in ⊢ (??(??%)?)
+ #T #s #x whd in ⊢ (??(??%)?);
  cases (split ????) #nu #nl normalize nodelta;
  cases (get_index_v bool ????) %
@@ -182 +182 @@
 lemma get_8051_sfr_write_at_stack_pointer:
  ∀T,s,x,y. get_8051_sfr T (write_at_stack_pointer T s x) y = get_8051_sfr T s y.
- #T #s #x #y whd in ⊢ (??%%) >special_function_registers_8051_write_at_stack_pointer @refl
+ #T #s #x #y whd in ⊢ (??%%); >special_function_registers_8051_write_at_stack_pointer @refl
 qed.
 
 lemma code_memory_write_at_stack_pointer:
  ∀T,s,x. code_memory T (write_at_stack_pointer T s x) = code_memory T s.
- #T #s #x whd in ⊢ (??(??%)?)
+ #T #s #x whd in ⊢ (??(??%)?);
  cases (split ????) #nu #nl normalize nodelta;
  cases (get_index_v bool ????) %
@@ -229 +229 @@
 lemma external_ram_write_at_stack_pointer:
  ∀T,s,x. external_ram T (write_at_stack_pointer T s x) = external_ram T s.
- #T #s #x whd in ⊢ (??(??%)?)
+ #T #s #x whd in ⊢ (??(??%)?);
  cases (split ????) #nu #nl normalize nodelta;
  cases (get_index_v bool ????) %
@@ -238 +238 @@
     special_function_registers_8052 T (write_at_stack_pointer T s x)
   = special_function_registers_8052 T s.
- #T #s #x whd in ⊢ (??(??%)?)
+ #T #s #x whd in ⊢ (??(??%)?);
  cases (split ????) #nu #nl normalize nodelta;
  cases (get_index_v bool ????) %
@@ -245 +245 @@
 lemma p1_latch_write_at_stack_pointer:
  ∀T,s,x. p1_latch T (write_at_stack_pointer T s x) = p1_latch T s.
- #T #s #x whd in ⊢ (??(??%)?)
+ #T #s #x whd in ⊢ (??(??%)?);
  cases (split ????) #nu #nl normalize nodelta;
  cases (get_index_v bool ????) %
@@ -252 +252 @@
 lemma p3_latch_write_at_stack_pointer:
  ∀T,s,x. p3_latch T (write_at_stack_pointer T s x) = p3_latch T s.
- #T #s #x whd in ⊢ (??(??%)?)
+ #T #s #x whd in ⊢ (??(??%)?);
  cases (split ????) #nu #nl normalize nodelta;
  cases (get_index_v bool ????) %
@@ -259 +259 @@
 lemma clock_write_at_stack_pointer:
  ∀T,s,x. clock T (write_at_stack_pointer T s x) = clock T s.
- #T #s #x whd in ⊢ (??(??%)?)
+ #T #s #x whd in ⊢ (??(??%)?);
  cases (split ????) #nu #nl normalize nodelta;
  cases (get_index_v bool ????) %
@@ -269 +269 @@
 lemma get_8051_sfr_set_8051_sfr:
  ∀T,s,x,y. get_8051_sfr T (set_8051_sfr ? s x y) x = y.
- #T *; #A #B #C #D #E #F #G #H #I #J *; #y whd in ⊢ (??(??%?)?)
+ #T *; #A #B #C #D #E #F #G #H #I #J *; #y whd in ⊢ (??(??%?)?);
  whd in match get_8051_sfr; normalize nodelta @get_index_v_set_index
 qed.