summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/Pure/Pure.thy

author | wenzelm |

Thu, 22 Dec 2005 00:28:52 +0100 | |

changeset 18466 | 389a6f9c31f4 |

parent 18019 | d1ff9ebb8bcb |

child 18663 | 8474756e4cbf |

permissions | -rw-r--r-- |

added locale meta_conjunction_syntax and various conjunction rules;

(* Title: Pure/Pure.thy ID: $Id$ *) header {* The Pure theory *} theory Pure imports ProtoPure begin setup "Context.setup ()" subsection {* Meta-level connectives in assumptions *} lemma meta_mp: assumes "PROP P ==> PROP Q" and "PROP P" shows "PROP Q" by (rule `PROP P ==> PROP Q` [OF `PROP P`]) lemma meta_spec: assumes "!!x. PROP P(x)" shows "PROP P(x)" by (rule `!!x. PROP P(x)`) lemmas meta_allE = meta_spec [elim_format] subsection {* Meta-level conjunction *} locale (open) meta_conjunction_syntax = fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2) parse_translation {* [("\<^fixed>meta_conjunction", fn [t, u] => Logic.mk_conjunction (t, u))] *} lemma all_conjunction: includes meta_conjunction_syntax shows "(!!x. PROP A(x) && PROP B(x)) == ((!!x. PROP A(x)) && (!!x. PROP B(x)))" proof assume conj: "!!x. PROP A(x) && PROP B(x)" fix X assume r: "(!!x. PROP A(x)) ==> (!!x. PROP B(x)) ==> PROP X" show "PROP X" proof (rule r) fix x from conj show "PROP A(x)" . from conj show "PROP B(x)" . qed next assume conj: "(!!x. PROP A(x)) && (!!x. PROP B(x))" fix x fix X assume r: "PROP A(x) ==> PROP B(x) ==> PROP X" show "PROP X" proof (rule r) show "PROP A(x)" proof (rule conj) assume "!!x. PROP A(x)" then show "PROP A(x)" . qed show "PROP B(x)" proof (rule conj) assume "!!x. PROP B(x)" then show "PROP B(x)" . qed qed qed lemma imp_conjunction [unfolded prop_def]: includes meta_conjunction_syntax shows "(PROP A ==> PROP prop (PROP B && PROP C)) == (PROP A ==> PROP B) && (PROP A ==> PROP C)" proof (unfold prop_def, rule) assume conj: "PROP A ==> PROP B && PROP C" fix X assume r: "(PROP A ==> PROP B) ==> (PROP A ==> PROP C) ==> PROP X" show "PROP X" proof (rule r) assume "PROP A" from conj [OF `PROP A`] show "PROP B" . from conj [OF `PROP A`] show "PROP C" . qed next assume conj: "(PROP A ==> PROP B) && (PROP A ==> PROP C)" assume "PROP A" fix X assume r: "PROP B ==> PROP C ==> PROP X" show "PROP X" proof (rule r) show "PROP B" proof (rule conj) assume "PROP A ==> PROP B" from this [OF `PROP A`] show "PROP B" . qed show "PROP C" proof (rule conj) assume "PROP A ==> PROP C" from this [OF `PROP A`] show "PROP C" . qed qed qed lemma conjunction_imp: includes meta_conjunction_syntax shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)" proof assume r: "PROP A && PROP B ==> PROP C" assume "PROP A" and "PROP B" show "PROP C" by (rule r) - next assume r: "PROP A ==> PROP B ==> PROP C" assume conj: "PROP A && PROP B" show "PROP C" proof (rule r) from conj show "PROP A" . from conj show "PROP B" . qed qed lemma conjunction_assoc: includes meta_conjunction_syntax shows "((PROP A && PROP B) && PROP C) == (PROP A && (PROP B && PROP C))" by (rule equal_intr_rule) (unfold imp_conjunction conjunction_imp) end