# HG changeset patch
# User wenzelm
# Date 1002202080 -7200
# Node ID ee12f18599e539df45637afc487d70b31c391b5f
# Parent  d04e96f8b0fdd25e71318f0c397e54bcd0861922
atomize stuff from theory FOL;
tuned;

diff -r d04e96f8b0fd -r ee12f18599e5 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Thu Oct 04 15:27:13 2001 +0200
+++ b/src/FOL/IFOL.thy	Thu Oct 04 15:28:00 2001 +0200
@@ -1,15 +1,16 @@
 (*  Title:      FOL/IFOL.thy
     ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
+    Author:     Lawrence C Paulson and Markus Wenzel
+*)
 
-Intuitionistic first-order logic.
-*)
+header {* Intuitionistic first-order logic *}
 
 theory IFOL = Pure
 files ("IFOL_lemmas.ML") ("fologic.ML") ("hypsubstdata.ML") ("intprover.ML"):
 
 
+subsection {* Syntax and axiomatic basis *}
+
 global
 
 classes "term" < logic
@@ -40,30 +41,28 @@
   Ex1           :: "('a => o) => o"             (binder "EX! " 10)
 
 
-
 syntax
   "~="          :: "['a, 'a] => o"              (infixl 50)
-
 translations
   "x ~= y"      == "~ (x = y)"
 
 syntax (symbols)
-  Not           :: "o => o"                     ("\\<not> _" [40] 40)
-  "op &"        :: "[o, o] => o"                (infixr "\\<and>" 35)
-  "op |"        :: "[o, o] => o"                (infixr "\\<or>" 30)
-  "op -->"      :: "[o, o] => o"                (infixr "\\<midarrow>\\<rightarrow>" 25)
-  "op <->"      :: "[o, o] => o"                (infixr "\\<leftarrow>\\<rightarrow>" 25)
-  "ALL "        :: "[idts, o] => o"             ("(3\\<forall>_./ _)" [0, 10] 10)
-  "EX "         :: "[idts, o] => o"             ("(3\\<exists>_./ _)" [0, 10] 10)
-  "EX! "        :: "[idts, o] => o"             ("(3\\<exists>!_./ _)" [0, 10] 10)
-  "op ~="       :: "['a, 'a] => o"              (infixl "\\<noteq>" 50)
+  Not           :: "o => o"                     ("\<not> _" [40] 40)
+  "op &"        :: "[o, o] => o"                (infixr "\<and>" 35)
+  "op |"        :: "[o, o] => o"                (infixr "\<or>" 30)
+  "op -->"      :: "[o, o] => o"                (infixr "\<midarrow>\<rightarrow>" 25)
+  "op <->"      :: "[o, o] => o"                (infixr "\<leftarrow>\<rightarrow>" 25)
+  "ALL "        :: "[idts, o] => o"             ("(3\<forall>_./ _)" [0, 10] 10)
+  "EX "         :: "[idts, o] => o"             ("(3\<exists>_./ _)" [0, 10] 10)
+  "EX! "        :: "[idts, o] => o"             ("(3\<exists>!_./ _)" [0, 10] 10)
+  "op ~="       :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
 
 syntax (xsymbols)
-  "op -->"      :: "[o, o] => o"                (infixr "\\<longrightarrow>" 25)
-  "op <->"      :: "[o, o] => o"                (infixr "\\<longleftrightarrow>" 25)
+  "op -->"      :: "[o, o] => o"                (infixr "\<longrightarrow>" 25)
+  "op <->"      :: "[o, o] => o"                (infixr "\<longleftrightarrow>" 25)
 
 syntax (HTML output)
-  Not           :: "o => o"                     ("\\<not> _" [40] 40)
+  Not           :: "o => o"                     ("\<not> _" [40] 40)
 
 
 local
@@ -116,6 +115,8 @@
   iff_reflection: "(P<->Q) ==> (P==Q)"
 
 
+subsection {* Lemmas and proof tools *}
+
 setup Simplifier.setup
 use "IFOL_lemmas.ML"
 use "fologic.ML"
@@ -124,4 +125,36 @@
 use "intprover.ML"
 
 
+subsection {* Atomizing meta-level rules *}
+
+lemma atomize_all: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
+proof (rule equal_intr_rule)
+  assume "!!x. P(x)"
+  show "ALL x. P(x)" by (rule allI)
+next
+  assume "ALL x. P(x)"
+  thus "!!x. P(x)" by (rule allE)
+qed
+
+lemma atomize_imp: "(A ==> B) == Trueprop (A --> B)"
+proof (rule equal_intr_rule)
+  assume r: "A ==> B"
+  show "A --> B" by (rule impI) (rule r)
+next
+  assume "A --> B" and A
+  thus B by (rule mp)
+qed
+
+lemma atomize_eq: "(x == y) == Trueprop (x = y)"
+proof (rule equal_intr_rule)
+  assume "x == y"
+  show "x = y" by (unfold prems) (rule refl)
+next
+  assume "x = y"
+  thus "x == y" by (rule eq_reflection)
+qed
+
+lemmas atomize = atomize_all atomize_imp
+lemmas atomize' = atomize atomize_eq
+
 end