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