src/FOLP/ex/If.thy
changeset 35416 d8d7d1b785af
parent 25991 31b38a39e589
child 35762 af3ff2ba4c54
equal deleted inserted replaced
35342:4dc65845eab3 35416:d8d7d1b785af
     2 
     2 
     3 theory If
     3 theory If
     4 imports FOLP
     4 imports FOLP
     5 begin
     5 begin
     6 
     6 
     7 constdefs
     7 definition "if" :: "[o,o,o]=>o" where
     8   "if" :: "[o,o,o]=>o"
       
     9   "if(P,Q,R) == P&Q | ~P&R"
     8   "if(P,Q,R) == P&Q | ~P&R"
    10 
     9 
    11 lemma ifI:
    10 lemma ifI:
    12   assumes "!!x. x : P ==> f(x) : Q"  "!!x. x : ~P ==> g(x) : R"
    11   assumes "!!x. x : P ==> f(x) : Q"  "!!x. x : ~P ==> g(x) : R"
    13   shows "?p : if(P,Q,R)"
    12   shows "?p : if(P,Q,R)"