equal
deleted
inserted
replaced
5 |
5 |
6 header {* First-Order Logic: the 'if' example *} |
6 header {* First-Order Logic: the 'if' example *} |
7 |
7 |
8 theory If imports FOL begin |
8 theory If imports FOL begin |
9 |
9 |
10 constdefs |
10 definition "if" :: "[o,o,o]=>o" where |
11 "if" :: "[o,o,o]=>o" |
|
12 "if(P,Q,R) == P&Q | ~P&R" |
11 "if(P,Q,R) == P&Q | ~P&R" |
13 |
12 |
14 lemma ifI: |
13 lemma ifI: |
15 "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)" |
14 "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)" |
16 apply (simp add: if_def, blast) |
15 apply (simp add: if_def, blast) |