summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Fri, 26 Oct 2001 23:59:13 +0200 | |

changeset 11953 | f98623fdf6ef |

parent 11952 | b10f1e8862f4 |

child 11954 | 3d1780208bf3 |

atomize_conj;

src/FOL/IFOL.thy | file | annotate | diff | comparison | revisions | |

src/HOL/HOL.thy | file | annotate | diff | comparison | revisions |

--- a/src/FOL/IFOL.thy Fri Oct 26 23:58:21 2001 +0200 +++ b/src/FOL/IFOL.thy Fri Oct 26 23:59:13 2001 +0200 @@ -158,6 +158,21 @@ thus "x == y" by (rule eq_reflection) qed +lemma atomize_conj [atomize]: "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)" +proof (rule equal_intr_rule) + assume "!!C. (A ==> B ==> PROP C) ==> PROP C" + show "A & B" by (rule conjI) +next + fix C + assume "A & B" + assume "A ==> B ==> PROP C" + thus "PROP C" + proof this + show A by (rule conjunct1) + show B by (rule conjunct2) + qed +qed + declare atomize_all [symmetric, rulify] atomize_imp [symmetric, rulify]

--- a/src/HOL/HOL.thy Fri Oct 26 23:58:21 2001 +0200 +++ b/src/HOL/HOL.thy Fri Oct 26 23:59:13 2001 +0200 @@ -232,6 +232,21 @@ thus "x == y" by (rule eq_reflection) qed +lemma atomize_conj [atomize]: "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)" +proof (rule equal_intr_rule) + assume "!!C. (A ==> B ==> PROP C) ==> PROP C" + show "A & B" by (rule conjI) +next + fix C + assume "A & B" + assume "A ==> B ==> PROP C" + thus "PROP C" + proof this + show A by (rule conjunct1) + show B by (rule conjunct2) + qed +qed + subsubsection {* Classical Reasoner setup *}