Ignore:
Timestamp:
Aug 4, 2011, 1:55:53 PM (9 years ago)
Author:
campbell
Message:

Tidy up branch

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch/Cminor/initialisation.ma

    r1101 r1102  
    44include "Cminor/syntax.ma".
    55include "common/Globalenvs.ma".
     6include "utilities/pair.ma".
     7include "utilities/deppair.ma".
    68
    79(* XXX having to specify the return type in the match is annoying. *)
     
    3941qed.
    4042
    41 lemma unpair : ∀A,B,C,D,x. ∀P:A → B → C. ∀Q:A → B → D.
    42   let 〈a,b〉 ≝ x in 〈P a b, Q a b〉 = 〈P (\fst x) (\snd x), Q (\fst x) (\snd x)〉.
    43 #A #B #C #D * // qed.
    44 
    45 lemma sndredex : ∀A,B,C,D,x. ∀R:D → Prop. ∀P:A → C. ∀Q:A → B → D.
    46   R (Q (\fst x) (\snd x)) → R (\snd (let 〈a,b〉 ≝ x in 〈P a, Q a b〉)).
    47 #A #B #C #D *; normalize /2/
    48 qed.
    49 
    50 lemma sig_stmt_inv : ∀s:Σs:stmt.stmt_inv s.
    51   stmt_inv s.
    52 * #s #p @p
    53 qed.
    54 
    5543definition init_var : ident → region → list init_data → Σs:stmt. stmt_inv s ≝
    5644λid,r,init.
     
    6351| elim init
    6452  [ % //
    65   | #h #t #IH whd in ⊢ (?(???%)) @sndredex % [ % [ % // | @sig_stmt_inv ] | @IH ]
     53  | #h #t #IH whd in ⊢ (?(???%)) @breakup_pair whd in ⊢ (?%) % [ % [ % // | @(use_sig ? stmt_inv) ] | @IH ]
    6654] qed.
    6755
     
    6957λvars. foldr ? (Σs:stmt. stmt_inv s)
    7058  (λvar,s. dp ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst (\fst var))) (\snd (\fst var)) (\snd (\fst (\fst var))))) ?) (dp ? (λx.stmt_inv x ) St_skip (conj ?? I I)) vars.
    71 % [ % [ % // | @sig_stmt_inv ] | @sig_stmt_inv ]
     59% [ % [ % // | @(use_sig ? stmt_inv) ] | @(use_sig ? stmt_inv) ]
    7260qed.
    7361
Note: See TracChangeset for help on using the changeset viewer.