Changeset 1949 for src/utilities/option.ma
- Timestamp:
- May 15, 2012, 5:51:25 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/utilities/option.ma
r1882 r1949 13 13 14 14 include "hints_declaration.ma". 15 alias symbol "hint_decl" (instance 1) = "hint_decl_Type1". 15 16 unification hint 0 ≔ X; 16 17 N ≟ max_def Option … … 38 39 ] qed. 39 40 41 lemma opt_safe_proof_irr : ∀A,m,prf1,prf2. 42 opt_safe A m prf1 = opt_safe A m prf2. 43 #A* // qed. 44 40 45 definition opt_try_catch : ∀X.option X → (unit → X) → X ≝ 41 46 λX,m,f.match m with [Some x ⇒ x | None ⇒ f it]. … … 57 62 interpretation "option try and catch" 'trycatch m f = (opt_try_catch ? m f). 58 63 59 definition OptPred ≝ λPdef : Prop.mk_MonadPred Option (λX,P,m.Try ! x ← m ; return P x catch ⇒ Pdef) ???. 60 #X[2:#Y]#P1[1,3:#P2[2:#H]*] normalize /2/ 64 definition OptPred ≝ λPdef : Prop.mk_MonadPred Option 65 (λX,P,x.Try ! y ← x ; return P y catch ⇒ Pdef) 66 (λX,P,m_sig.match m_sig with [ mk_Sig m prf ⇒ match m return λx.Try ! y ← x ; return P y catch ⇒ Pdef → option (Σy.?) with [ Some x ⇒ λprf.Some ? x | None ⇒ λ_.None ? ] prf ]) 67 ????. 68 [ @prf 69 |*: 70 #X[2:#Y]#P1[1,3:#P2[2:#H]] 71 [1,2,4: * [5: *]] normalize /2/ 61 72 qed. 62 73 63 74 definition opt_All : ∀X.(X → Prop) → option X → Prop ≝ m_pred … (OptPred True). 64 75 65 76 lemma opt_All_mp : ∀A,P,Q.(∀x. P x → Q x) → ∀o.opt_All A P o → opt_All ? Q o 66 77 ≝ m_pred_mp …. … … 70 81 lemma opt_Exists_mp : ∀A,P,Q.(∀x. P x → Q x) → ∀o.opt_Exists A P o → opt_Exists ? Q o 71 82 ≝ m_pred_mp …. 72
Note: See TracChangeset
for help on using the changeset viewer.