Changeset 1948 for src/ASM/Interpret.ma


Ignore:
Timestamp:
May 15, 2012, 11:13:14 AM (8 years ago)
Author:
mulligan
Message:

Weakened statements of ASM/Assembly.ma and ASM/AssemblyProof.ma, so all lemmas and functions that accepted a sigma before now accept a weakened sigma coupled with a policy. ASM/AssemblyProof.ma compiles until main_thm.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r1946 r1948  
    88    let b ≝ get_index_v ? 8 c 1 ? in
    99      [[ b; b; b; b; b; b; b; b ]] @@ c.
    10   normalize;
    11   repeat (@ (le_S_S ?));
    12   @ (le_O_n);
     10  normalize
     11  repeat (@le_S_S)
     12  @le_O_n
    1313qed.
    1414   
    15 lemma eq_a_to_eq: ∀a,b. eq_a a b = true → a=b.
    16  # a
    17  # b
    18  cases a
    19  cases b
     15lemma eq_a_to_eq:
     16  ∀a,b.
     17    eq_a a b = true → a = b.
     18 #a #b
     19 cases a cases b
    2020 normalize
    21  # K
     21 #K
    2222 try %
    2323 cases (eq_true_false K)
     
    2525
    2626lemma is_a_to_mem_to_is_in:
    27  ∀he,a,m,q. is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true.
    28  # he
    29  # a
    30  # m
    31  # q
     27 ∀he,a,m,q.
     28   is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true.
     29 #he #a #m #q
    3230 elim q
    33  [ normalize
    34    # _
    35    # K
    36    assumption
    37  | # m'
    38    # t
    39    # q'
    40    # II
    41    # H1
    42    # H2
     31 [1:
     32   #_ #K assumption
     33 |2:
     34   #m' #t #q' #II #H1 #H2
    4335   normalize
    44    change with (orb ??) in H2: (??%?);
     36   change with (orb ??) in H2:(??%?);
    4537   cases (inclusive_disjunction_true … H2)
    46    [ # K
    47      < (eq_a_to_eq … K)
    48      > H1
    49      %
    50    | # K
    51      > II
     38   [1:
     39     #K
     40     <(eq_a_to_eq … K) >H1 %
     41   |2:
     42     #K
     43     >II
    5244     try assumption
    5345     cases (is_a t a)
Note: See TracChangeset for help on using the changeset viewer.