419 definition lor_o (infixl "||" 50) where |
419 definition lor_o (infixl "||" 50) where |
420 "x || y <-> --(-- x && -- y)" |
420 "x || y <-> --(-- x && -- y)" |
421 |
421 |
422 end |
422 end |
423 |
423 |
424 interpretation x: logic_o "op &" "Not" |
424 interpretation x!: logic_o "op &" "Not" |
425 where bool_logic_o: "logic_o.lor_o(op &, Not, x, y) <-> x | y" |
425 where bool_logic_o: "logic_o.lor_o(op &, Not, x, y) <-> x | y" |
426 proof - |
426 proof - |
427 show bool_logic_o: "PROP logic_o(op &, Not)" by unfold_locales fast+ |
427 show bool_logic_o: "PROP logic_o(op &, Not)" by unfold_locales fast+ |
428 show "logic_o.lor_o(op &, Not, x, y) <-> x | y" |
428 show "logic_o.lor_o(op &, Not, x, y) <-> x | y" |
429 by (unfold logic_o.lor_o_def [OF bool_logic_o]) fast |
429 by (unfold logic_o.lor_o_def [OF bool_logic_o]) fast |
430 qed |
430 qed |
431 |
431 |
432 thm x.lor_o_def bool_logic_o |
432 thm x.lor_o_def bool_logic_o |
433 |
433 |
|
434 lemma lor_triv: "z <-> z" .. |
|
435 |
434 lemma (in logic_o) lor_triv: "x || y <-> x || y" by fast |
436 lemma (in logic_o) lor_triv: "x || y <-> x || y" by fast |
435 |
437 |
436 thm x.lor_triv |
438 thm lor_triv [where z = True] (* Check strict prefix. *) |
|
439 x.lor_triv |
437 |
440 |
438 |
441 |
439 subsection {* Interpretation in proofs *} |
442 subsection {* Interpretation in proofs *} |
440 |
443 |
441 lemma True |
444 lemma True |