src/FOL/IFOL.thy
changeset 11677 ee12f18599e5
parent 9886 897d6602cbfb
child 11734 7a21bf539412
     1.1 --- a/src/FOL/IFOL.thy	Thu Oct 04 15:27:13 2001 +0200
     1.2 +++ b/src/FOL/IFOL.thy	Thu Oct 04 15:28:00 2001 +0200
     1.3 @@ -1,15 +1,16 @@
     1.4  (*  Title:      FOL/IFOL.thy
     1.5      ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1993  University of Cambridge
     1.8 +    Author:     Lawrence C Paulson and Markus Wenzel
     1.9 +*)
    1.10  
    1.11 -Intuitionistic first-order logic.
    1.12 -*)
    1.13 +header {* Intuitionistic first-order logic *}
    1.14  
    1.15  theory IFOL = Pure
    1.16  files ("IFOL_lemmas.ML") ("fologic.ML") ("hypsubstdata.ML") ("intprover.ML"):
    1.17  
    1.18  
    1.19 +subsection {* Syntax and axiomatic basis *}
    1.20 +
    1.21  global
    1.22  
    1.23  classes "term" < logic
    1.24 @@ -40,30 +41,28 @@
    1.25    Ex1           :: "('a => o) => o"             (binder "EX! " 10)
    1.26  
    1.27  
    1.28 -
    1.29  syntax
    1.30    "~="          :: "['a, 'a] => o"              (infixl 50)
    1.31 -
    1.32  translations
    1.33    "x ~= y"      == "~ (x = y)"
    1.34  
    1.35  syntax (symbols)
    1.36 -  Not           :: "o => o"                     ("\\<not> _" [40] 40)
    1.37 -  "op &"        :: "[o, o] => o"                (infixr "\\<and>" 35)
    1.38 -  "op |"        :: "[o, o] => o"                (infixr "\\<or>" 30)
    1.39 -  "op -->"      :: "[o, o] => o"                (infixr "\\<midarrow>\\<rightarrow>" 25)
    1.40 -  "op <->"      :: "[o, o] => o"                (infixr "\\<leftarrow>\\<rightarrow>" 25)
    1.41 -  "ALL "        :: "[idts, o] => o"             ("(3\\<forall>_./ _)" [0, 10] 10)
    1.42 -  "EX "         :: "[idts, o] => o"             ("(3\\<exists>_./ _)" [0, 10] 10)
    1.43 -  "EX! "        :: "[idts, o] => o"             ("(3\\<exists>!_./ _)" [0, 10] 10)
    1.44 -  "op ~="       :: "['a, 'a] => o"              (infixl "\\<noteq>" 50)
    1.45 +  Not           :: "o => o"                     ("\<not> _" [40] 40)
    1.46 +  "op &"        :: "[o, o] => o"                (infixr "\<and>" 35)
    1.47 +  "op |"        :: "[o, o] => o"                (infixr "\<or>" 30)
    1.48 +  "op -->"      :: "[o, o] => o"                (infixr "\<midarrow>\<rightarrow>" 25)
    1.49 +  "op <->"      :: "[o, o] => o"                (infixr "\<leftarrow>\<rightarrow>" 25)
    1.50 +  "ALL "        :: "[idts, o] => o"             ("(3\<forall>_./ _)" [0, 10] 10)
    1.51 +  "EX "         :: "[idts, o] => o"             ("(3\<exists>_./ _)" [0, 10] 10)
    1.52 +  "EX! "        :: "[idts, o] => o"             ("(3\<exists>!_./ _)" [0, 10] 10)
    1.53 +  "op ~="       :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
    1.54  
    1.55  syntax (xsymbols)
    1.56 -  "op -->"      :: "[o, o] => o"                (infixr "\\<longrightarrow>" 25)
    1.57 -  "op <->"      :: "[o, o] => o"                (infixr "\\<longleftrightarrow>" 25)
    1.58 +  "op -->"      :: "[o, o] => o"                (infixr "\<longrightarrow>" 25)
    1.59 +  "op <->"      :: "[o, o] => o"                (infixr "\<longleftrightarrow>" 25)
    1.60  
    1.61  syntax (HTML output)
    1.62 -  Not           :: "o => o"                     ("\\<not> _" [40] 40)
    1.63 +  Not           :: "o => o"                     ("\<not> _" [40] 40)
    1.64  
    1.65  
    1.66  local
    1.67 @@ -116,6 +115,8 @@
    1.68    iff_reflection: "(P<->Q) ==> (P==Q)"
    1.69  
    1.70  
    1.71 +subsection {* Lemmas and proof tools *}
    1.72 +
    1.73  setup Simplifier.setup
    1.74  use "IFOL_lemmas.ML"
    1.75  use "fologic.ML"
    1.76 @@ -124,4 +125,36 @@
    1.77  use "intprover.ML"
    1.78  
    1.79  
    1.80 +subsection {* Atomizing meta-level rules *}
    1.81 +
    1.82 +lemma atomize_all: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
    1.83 +proof (rule equal_intr_rule)
    1.84 +  assume "!!x. P(x)"
    1.85 +  show "ALL x. P(x)" by (rule allI)
    1.86 +next
    1.87 +  assume "ALL x. P(x)"
    1.88 +  thus "!!x. P(x)" by (rule allE)
    1.89 +qed
    1.90 +
    1.91 +lemma atomize_imp: "(A ==> B) == Trueprop (A --> B)"
    1.92 +proof (rule equal_intr_rule)
    1.93 +  assume r: "A ==> B"
    1.94 +  show "A --> B" by (rule impI) (rule r)
    1.95 +next
    1.96 +  assume "A --> B" and A
    1.97 +  thus B by (rule mp)
    1.98 +qed
    1.99 +
   1.100 +lemma atomize_eq: "(x == y) == Trueprop (x = y)"
   1.101 +proof (rule equal_intr_rule)
   1.102 +  assume "x == y"
   1.103 +  show "x = y" by (unfold prems) (rule refl)
   1.104 +next
   1.105 +  assume "x = y"
   1.106 +  thus "x == y" by (rule eq_reflection)
   1.107 +qed
   1.108 +
   1.109 +lemmas atomize = atomize_all atomize_imp
   1.110 +lemmas atomize' = atomize atomize_eq
   1.111 +
   1.112  end