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