Ignore:
Timestamp:
May 9, 2012, 6:30:41 PM (8 years ago)
Author:
campbell
Message:

Tidy up labelling simulation stuff a bit.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/extralib.ma

    r1882 r1930  
    114114qed.
    115115
     116(* Replace decision functions by result. *)
     117
     118lemma dec_true: ∀P:Prop.∀f:P + ¬P.∀p:P.∀Q:(P + ¬P) → Type[0]. (∀p'.Q (inl ?? p')) → Q f.
     119#P #f #p #Q #H cases f;
     120[ @H
     121| #np cut False [ @(absurd ? p np) | * ]
     122] qed.
     123
     124lemma dec_false: ∀P:Prop.∀f:P + ¬P.∀p:¬P.∀Q:(P + ¬P) → Type[0]. (∀p'.Q (inr ?? p')) → Q f.
     125#P #f #p #Q #H cases f;
     126[ #np cut False [ @(absurd ? np p) | * ]
     127| @H
     128] qed.
     129
     130
    116131lemma not_exists_forall:
    117132  ∀k:ℕ.∀P:ℕ → Prop.¬(∃x.x < k ∧ P x) → ∀x.x < k → ¬P x.
Note: See TracChangeset for help on using the changeset viewer.