src/HOL/Import/MakeEqual.thy
author wenzelm
Fri Dec 17 17:43:54 2010 +0100 (2010-12-17)
changeset 41229 d797baa3d57c
parent 16417 9bc16273c2d4
child 41589 bbd861837ebc
permissions -rw-r--r--
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
     1 (*  Title:      HOL/Import/MakeEqual.thy
     2     ID:         $Id$
     3     Author:     Sebastian Skalberg (TU Muenchen)
     4 *)
     5 
     6 theory MakeEqual imports Main
     7   uses "shuffler.ML" begin
     8 
     9 setup Shuffler.setup
    10 
    11 lemma conj_norm [shuffle_rule]: "(A & B ==> PROP C) == ([| A ; B |] ==> PROP C)"
    12 proof
    13   assume "A & B ==> PROP C" A B
    14   thus "PROP C"
    15     by auto
    16 next
    17   assume "[| A; B |] ==> PROP C" "A & B"
    18   thus "PROP C"
    19     by auto
    20 qed
    21 
    22 lemma imp_norm [shuffle_rule]: "(Trueprop (A --> B)) == (A ==> B)"
    23 proof
    24   assume "A --> B" A
    25   thus B ..
    26 next
    27   assume "A ==> B"
    28   thus "A --> B"
    29     by auto
    30 qed
    31 
    32 lemma all_norm [shuffle_rule]: "(Trueprop (ALL x. P x)) == (!!x. P x)"
    33 proof
    34   fix x
    35   assume "ALL x. P x"
    36   thus "P x" ..
    37 next
    38   assume "!!x. P x"
    39   thus "ALL x. P x"
    40     ..
    41 qed
    42 
    43 lemma ex_norm [shuffle_rule]: "(EX x. P x ==> PROP Q) == (!!x. P x ==> PROP Q)"
    44 proof
    45   fix x
    46   assume ex: "EX x. P x ==> PROP Q"
    47   assume "P x"
    48   hence "EX x. P x" ..
    49   with ex show "PROP Q" .
    50 next
    51   assume allx: "!!x. P x ==> PROP Q"
    52   assume "EX x. P x"
    53   hence p: "P (SOME x. P x)"
    54     ..
    55   from allx
    56   have "P (SOME x. P x) ==> PROP Q"
    57     .
    58   with p
    59   show "PROP Q"
    60     by auto
    61 qed
    62 
    63 lemma eq_norm [shuffle_rule]: "Trueprop (t = u) == (t == u)"
    64 proof
    65   assume "t = u"
    66   thus "t == u" by simp
    67 next
    68   assume "t == u"
    69   thus "t = u"
    70     by simp
    71 qed
    72 
    73 end