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