src/FOL/IFOL.thy
author wenzelm
Sat Apr 08 22:51:06 2006 +0200 (2006-04-08)
changeset 19363 667b5ea637dd
parent 19120 353d349740de
child 19380 b808efaa5828
permissions -rw-r--r--
refined 'abbreviation';
     1 (*  Title:      FOL/IFOL.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson and Markus Wenzel
     4 *)
     5 
     6 header {* Intuitionistic first-order logic *}
     7 
     8 theory IFOL
     9 imports Pure
    10 uses ("IFOL_lemmas.ML") ("fologic.ML") ("hypsubstdata.ML") ("intprover.ML")
    11 begin
    12 
    13 
    14 subsection {* Syntax and axiomatic basis *}
    15 
    16 global
    17 
    18 classes "term"
    19 finalconsts term_class
    20 defaultsort "term"
    21 
    22 typedecl o
    23 
    24 judgment
    25   Trueprop      :: "o => prop"                  ("(_)" 5)
    26 
    27 consts
    28   True          :: o
    29   False         :: o
    30 
    31   (* Connectives *)
    32 
    33   "op ="        :: "['a, 'a] => o"              (infixl "=" 50)
    34 
    35   Not           :: "o => o"                     ("~ _" [40] 40)
    36   "op &"        :: "[o, o] => o"                (infixr "&" 35)
    37   "op |"        :: "[o, o] => o"                (infixr "|" 30)
    38   "op -->"      :: "[o, o] => o"                (infixr "-->" 25)
    39   "op <->"      :: "[o, o] => o"                (infixr "<->" 25)
    40 
    41   (* Quantifiers *)
    42 
    43   All           :: "('a => o) => o"             (binder "ALL " 10)
    44   Ex            :: "('a => o) => o"             (binder "EX " 10)
    45   Ex1           :: "('a => o) => o"             (binder "EX! " 10)
    46 
    47 
    48 abbreviation
    49   not_equal     :: "['a, 'a] => o"              (infixl "~=" 50)
    50   "x ~= y == ~ (x = y)"
    51 
    52 abbreviation (xsymbols)
    53   not_equal     :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
    54   "x \<noteq> y == ~ (x = y)"
    55 
    56 abbreviation (HTML output)
    57   not_equal     :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
    58   "not_equal == xsymbols.not_equal"
    59 
    60 syntax (xsymbols)
    61   Not           :: "o => o"                     ("\<not> _" [40] 40)
    62   "op &"        :: "[o, o] => o"                (infixr "\<and>" 35)
    63   "op |"        :: "[o, o] => o"                (infixr "\<or>" 30)
    64   "ALL "        :: "[idts, o] => o"             ("(3\<forall>_./ _)" [0, 10] 10)
    65   "EX "         :: "[idts, o] => o"             ("(3\<exists>_./ _)" [0, 10] 10)
    66   "EX! "        :: "[idts, o] => o"             ("(3\<exists>!_./ _)" [0, 10] 10)
    67   "op -->"      :: "[o, o] => o"                (infixr "\<longrightarrow>" 25)
    68   "op <->"      :: "[o, o] => o"                (infixr "\<longleftrightarrow>" 25)
    69 
    70 syntax (HTML output)
    71   Not           :: "o => o"                     ("\<not> _" [40] 40)
    72   "op &"        :: "[o, o] => o"                (infixr "\<and>" 35)
    73   "op |"        :: "[o, o] => o"                (infixr "\<or>" 30)
    74   "ALL "        :: "[idts, o] => o"             ("(3\<forall>_./ _)" [0, 10] 10)
    75   "EX "         :: "[idts, o] => o"             ("(3\<exists>_./ _)" [0, 10] 10)
    76   "EX! "        :: "[idts, o] => o"             ("(3\<exists>!_./ _)" [0, 10] 10)
    77 
    78 
    79 local
    80 
    81 finalconsts
    82   False All Ex
    83   "op ="
    84   "op &"
    85   "op |"
    86   "op -->"
    87 
    88 axioms
    89 
    90   (* Equality *)
    91 
    92   refl:         "a=a"
    93 
    94   (* Propositional logic *)
    95 
    96   conjI:        "[| P;  Q |] ==> P&Q"
    97   conjunct1:    "P&Q ==> P"
    98   conjunct2:    "P&Q ==> Q"
    99 
   100   disjI1:       "P ==> P|Q"
   101   disjI2:       "Q ==> P|Q"
   102   disjE:        "[| P|Q;  P ==> R;  Q ==> R |] ==> R"
   103 
   104   impI:         "(P ==> Q) ==> P-->Q"
   105   mp:           "[| P-->Q;  P |] ==> Q"
   106 
   107   FalseE:       "False ==> P"
   108 
   109   (* Quantifiers *)
   110 
   111   allI:         "(!!x. P(x)) ==> (ALL x. P(x))"
   112   spec:         "(ALL x. P(x)) ==> P(x)"
   113 
   114   exI:          "P(x) ==> (EX x. P(x))"
   115   exE:          "[| EX x. P(x);  !!x. P(x) ==> R |] ==> R"
   116 
   117   (* Reflection *)
   118 
   119   eq_reflection:  "(x=y)   ==> (x==y)"
   120   iff_reflection: "(P<->Q) ==> (P==Q)"
   121 
   122 
   123 text{*Thanks to Stephan Merz*}
   124 theorem subst:
   125   assumes eq: "a = b" and p: "P(a)"
   126   shows "P(b)"
   127 proof -
   128   from eq have meta: "a \<equiv> b"
   129     by (rule eq_reflection)
   130   from p show ?thesis
   131     by (unfold meta)
   132 qed
   133 
   134 
   135 defs
   136   (* Definitions *)
   137 
   138   True_def:     "True  == False-->False"
   139   not_def:      "~P    == P-->False"
   140   iff_def:      "P<->Q == (P-->Q) & (Q-->P)"
   141 
   142   (* Unique existence *)
   143 
   144   ex1_def:      "Ex1(P) == EX x. P(x) & (ALL y. P(y) --> y=x)"
   145 
   146 
   147 subsection {* Lemmas and proof tools *}
   148 
   149 use "IFOL_lemmas.ML"
   150 
   151 ML {*
   152 structure ProjectRule = ProjectRuleFun
   153 (struct
   154   val conjunct1 = thm "conjunct1";
   155   val conjunct2 = thm "conjunct2";
   156   val mp = thm "mp";
   157 end)
   158 *}
   159 
   160 use "fologic.ML"
   161 use "hypsubstdata.ML"
   162 setup hypsubst_setup
   163 use "intprover.ML"
   164 
   165 
   166 subsection {* Intuitionistic Reasoning *}
   167 
   168 lemma impE':
   169   assumes 1: "P --> Q"
   170     and 2: "Q ==> R"
   171     and 3: "P --> Q ==> P"
   172   shows R
   173 proof -
   174   from 3 and 1 have P .
   175   with 1 have Q by (rule impE)
   176   with 2 show R .
   177 qed
   178 
   179 lemma allE':
   180   assumes 1: "ALL x. P(x)"
   181     and 2: "P(x) ==> ALL x. P(x) ==> Q"
   182   shows Q
   183 proof -
   184   from 1 have "P(x)" by (rule spec)
   185   from this and 1 show Q by (rule 2)
   186 qed
   187 
   188 lemma notE':
   189   assumes 1: "~ P"
   190     and 2: "~ P ==> P"
   191   shows R
   192 proof -
   193   from 2 and 1 have P .
   194   with 1 show R by (rule notE)
   195 qed
   196 
   197 lemmas [Pure.elim!] = disjE iffE FalseE conjE exE
   198   and [Pure.intro!] = iffI conjI impI TrueI notI allI refl
   199   and [Pure.elim 2] = allE notE' impE'
   200   and [Pure.intro] = exI disjI2 disjI1
   201 
   202 setup {* ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac) *}
   203 
   204 
   205 lemma iff_not_sym: "~ (Q <-> P) ==> ~ (P <-> Q)"
   206   by iprover
   207 
   208 lemmas [sym] = sym iff_sym not_sym iff_not_sym
   209   and [Pure.elim?] = iffD1 iffD2 impE
   210 
   211 
   212 lemma eq_commute: "a=b <-> b=a"
   213 apply (rule iffI) 
   214 apply (erule sym)+
   215 done
   216 
   217 
   218 subsection {* Atomizing meta-level rules *}
   219 
   220 lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
   221 proof
   222   assume "!!x. P(x)"
   223   show "ALL x. P(x)" ..
   224 next
   225   assume "ALL x. P(x)"
   226   thus "!!x. P(x)" ..
   227 qed
   228 
   229 lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A --> B)"
   230 proof
   231   assume "A ==> B"
   232   thus "A --> B" ..
   233 next
   234   assume "A --> B" and A
   235   thus B by (rule mp)
   236 qed
   237 
   238 lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)"
   239 proof
   240   assume "x == y"
   241   show "x = y" by (unfold prems) (rule refl)
   242 next
   243   assume "x = y"
   244   thus "x == y" by (rule eq_reflection)
   245 qed
   246 
   247 lemma atomize_iff [atomize]: "(A == B) == Trueprop (A <-> B)"
   248 proof
   249   assume "A == B"
   250   show "A <-> B" by (unfold prems) (rule iff_refl)
   251 next
   252   assume "A <-> B"
   253   thus "A == B" by (rule iff_reflection)
   254 qed
   255 
   256 lemma atomize_conj [atomize]:
   257   includes meta_conjunction_syntax
   258   shows "(A && B) == Trueprop (A & B)"
   259 proof
   260   assume conj: "A && B"
   261   show "A & B"
   262   proof (rule conjI)
   263     from conj show A by (rule conjunctionD1)
   264     from conj show B by (rule conjunctionD2)
   265   qed
   266 next
   267   assume conj: "A & B"
   268   show "A && B"
   269   proof -
   270     from conj show A ..
   271     from conj show B ..
   272   qed
   273 qed
   274 
   275 lemmas [symmetric, rulify] = atomize_all atomize_imp
   276   and [symmetric, defn] = atomize_all atomize_imp atomize_eq atomize_iff
   277 
   278 
   279 subsection {* Calculational rules *}
   280 
   281 lemma forw_subst: "a = b ==> P(b) ==> P(a)"
   282   by (rule ssubst)
   283 
   284 lemma back_subst: "P(a) ==> a = b ==> P(b)"
   285   by (rule subst)
   286 
   287 text {*
   288   Note that this list of rules is in reverse order of priorities.
   289 *}
   290 
   291 lemmas basic_trans_rules [trans] =
   292   forw_subst
   293   back_subst
   294   rev_mp
   295   mp
   296   trans
   297 
   298 subsection {* ``Let'' declarations *}
   299 
   300 nonterminals letbinds letbind
   301 
   302 constdefs
   303   Let :: "['a::{}, 'a => 'b] => ('b::{})"
   304     "Let(s, f) == f(s)"
   305 
   306 syntax
   307   "_bind"       :: "[pttrn, 'a] => letbind"           ("(2_ =/ _)" 10)
   308   ""            :: "letbind => letbinds"              ("_")
   309   "_binds"      :: "[letbind, letbinds] => letbinds"  ("_;/ _")
   310   "_Let"        :: "[letbinds, 'a] => 'a"             ("(let (_)/ in (_))" 10)
   311 
   312 translations
   313   "_Let(_binds(b, bs), e)"  == "_Let(b, _Let(bs, e))"
   314   "let x = a in e"          == "Let(a, %x. e)"
   315 
   316 
   317 lemma LetI: 
   318     assumes prem: "(!!x. x=t ==> P(u(x)))"
   319     shows "P(let x=t in u(x))"
   320 apply (unfold Let_def)
   321 apply (rule refl [THEN prem])
   322 done
   323 
   324 ML
   325 {*
   326 val Let_def = thm "Let_def";
   327 val LetI = thm "LetI";
   328 *}
   329 
   330 end