Changeset 3553 for LTS/imp.ma


Ignore:
Timestamp:
Apr 10, 2015, 3:08:55 PM (5 years ago)
Author:
pellitta
Message:

inizio prima compilazione

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/imp.ma

    r3548 r3553  
    5454
    5555(* is ex_falso in the standard libary? *)
    56 lemma ex_falso_quodlibet:∀P:Prop.False→ P.
    57 #P #F cases F qed.
     56(*lemma ex_falso_quodlibet:∀P:Prop.False→ P.
     57#P #F cases F qed.*)
     58lemma ex_falso_quodlibet:False→ ∀P:Prop.P.
     59#F cases F qed.
    5860
    5961(* what about this? *)
     
    6264
    6365lemma contradiction:∀P.P→¬P→ (∀A:Prop.A).
    64 #P #H #Hn #A @(ex_falso_quodlibet A (absurd P H Hn)) qed.
     66#P #H #Hn #A @(ex_falso_quodlibet (absurd P H Hn)) qed.
    6567
    6668(*
     
    7577@(contradiction (?=?) (refl …) H) qed.
    7678
     79lemma neq_bool:∀b1,b2.b1=(notb b2)→(b1≠b2).* * normalize #H /2 by sym_not_eq/ qed.
     80
    7781lemma eqb_refl:∀T:DeqSet.∀t:T.(t==t)=true.
    7882#T #t @(\b ?) % qed. (* inversion(t==t) #H try(%) lapply(\Pf H) #ABS @(contradiction …) [@(t=t)|@refl|@ABS] qed.*)
     
    8084lemma eqb_sym:∀T:DeqSet.∀t1,t2:T.(t1==t2)=(t2==t1).
    8185#T #t1 #t2 inversion(t1==t2) #INV [lapply(\P INV)|lapply(\Pf INV)] #H [>H >eqb_refl %
    82 |elim H #H' inversion(t2==t1) #INV2 [lapply(\P INV2) #ABS destruct @(contradiction ((t1==t1)=true) INV2 ?)
     86|inversion(t2==t1) #INV2 [lapply(\P INV2) #ABS destruct @(contradiction ((t1==t1)=true) INV2 ?)
    8387/2 by /|%] qed.
     88
     89lemma neq_refl_false:∀T.∀t:T.(t≠t)→ ∀P:Prop.P.
     90#T #t #H @(contradiction (t=t) (refl …) H) qed.
     91
     92lemma neqb_refl_false:∀T:DeqSet.∀t:T.(t==t)=false→ ∀P:Prop.P.
     93#T #t #ABS @(contradiction ((t==t)=true) (eqb_refl …) ?) @neq_bool whd in match(¬true);
     94assumption qed.
    8495
    8596(* Syntax *)
     
    559570definition Lt:expr → expr → condition≝λe1,e2.Not (Geq e2 e1).
    560571
     572(* Abitare tipo Program *)
     573
     574  (* Abitare tipo Instructions *)
     575 
     576definition imp_Instructions≝Instructions imp_state_params.
     577
     578definition imp_signature≝signature imp_state_params imp_state_params.
     579
     580check CallCostLabel
     581
     582definition imp_envitem:(env_item imp_env_params imp_instr_params)≝
    561583
    562584(* | mIfThenElse1:
Note: See TracChangeset for help on using the changeset viewer.