src/Pure/Pure.thy
author wenzelm
Fri May 11 01:07:10 2007 +0200 (2007-05-11)
changeset 22933 338c7890c96f
parent 21627 b822c7e61701
child 23432 cec811764a38
permissions -rw-r--r--
tuned proofs;
wenzelm@15803
     1
(*  Title:      Pure/Pure.thy
wenzelm@15803
     2
    ID:         $Id$
wenzelm@18466
     3
*)
wenzelm@15803
     4
wenzelm@18466
     5
header {* The Pure theory *}
wenzelm@15803
     6
wenzelm@15803
     7
theory Pure
wenzelm@15803
     8
imports ProtoPure
wenzelm@15803
     9
begin
wenzelm@19800
    10
wenzelm@19048
    11
setup  -- {* Common setup of internal components *}
wenzelm@15803
    12
wenzelm@20627
    13
wenzelm@18466
    14
subsection {* Meta-level connectives in assumptions *}
wenzelm@15803
    15
wenzelm@15803
    16
lemma meta_mp:
wenzelm@18019
    17
  assumes "PROP P ==> PROP Q" and "PROP P"
wenzelm@15803
    18
  shows "PROP Q"
wenzelm@18019
    19
    by (rule `PROP P ==> PROP Q` [OF `PROP P`])
wenzelm@15803
    20
wenzelm@15803
    21
lemma meta_spec:
wenzelm@18019
    22
  assumes "!!x. PROP P(x)"
wenzelm@15803
    23
  shows "PROP P(x)"
wenzelm@18019
    24
    by (rule `!!x. PROP P(x)`)
wenzelm@15803
    25
wenzelm@15803
    26
lemmas meta_allE = meta_spec [elim_format]
wenzelm@15803
    27
wenzelm@18466
    28
wenzelm@21625
    29
subsection {* Embedded terms *}
wenzelm@21625
    30
wenzelm@21625
    31
locale (open) meta_term_syntax =
wenzelm@21625
    32
  fixes meta_term :: "'a => prop"  ("TERM _")
wenzelm@21625
    33
wenzelm@21625
    34
parse_translation {*
wenzelm@21627
    35
  [("\<^fixed>meta_term", fn [t] => Const ("ProtoPure.term", dummyT --> propT) $ t)]
wenzelm@21625
    36
*}
wenzelm@21625
    37
wenzelm@21625
    38
lemmas [intro?] = termI
wenzelm@21625
    39
wenzelm@21625
    40
wenzelm@18466
    41
subsection {* Meta-level conjunction *}
wenzelm@18466
    42
wenzelm@18466
    43
locale (open) meta_conjunction_syntax =
wenzelm@18466
    44
  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
wenzelm@18466
    45
wenzelm@18466
    46
parse_translation {*
wenzelm@18466
    47
  [("\<^fixed>meta_conjunction", fn [t, u] => Logic.mk_conjunction (t, u))]
wenzelm@18466
    48
*}
wenzelm@18466
    49
wenzelm@18466
    50
lemma all_conjunction:
wenzelm@18466
    51
  includes meta_conjunction_syntax
wenzelm@18466
    52
  shows "(!!x. PROP A(x) && PROP B(x)) == ((!!x. PROP A(x)) && (!!x. PROP B(x)))"
wenzelm@18466
    53
proof
wenzelm@18466
    54
  assume conj: "!!x. PROP A(x) && PROP B(x)"
wenzelm@19121
    55
  show "(\<And>x. PROP A(x)) && (\<And>x. PROP B(x))"
wenzelm@19121
    56
  proof -
wenzelm@18466
    57
    fix x
wenzelm@19121
    58
    from conj show "PROP A(x)" by (rule conjunctionD1)
wenzelm@19121
    59
    from conj show "PROP B(x)" by (rule conjunctionD2)
wenzelm@18466
    60
  qed
wenzelm@18466
    61
next
wenzelm@18466
    62
  assume conj: "(!!x. PROP A(x)) && (!!x. PROP B(x))"
wenzelm@18466
    63
  fix x
wenzelm@19121
    64
  show "PROP A(x) && PROP B(x)"
wenzelm@19121
    65
  proof -
wenzelm@19121
    66
    show "PROP A(x)" by (rule conj [THEN conjunctionD1, rule_format])
wenzelm@19121
    67
    show "PROP B(x)" by (rule conj [THEN conjunctionD2, rule_format])
wenzelm@18466
    68
  qed
wenzelm@18466
    69
qed
wenzelm@18466
    70
wenzelm@19121
    71
lemma imp_conjunction:
wenzelm@18466
    72
  includes meta_conjunction_syntax
wenzelm@19121
    73
  shows "(PROP A ==> PROP B && PROP C) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
wenzelm@18836
    74
proof
wenzelm@18466
    75
  assume conj: "PROP A ==> PROP B && PROP C"
wenzelm@19121
    76
  show "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
wenzelm@19121
    77
  proof -
wenzelm@18466
    78
    assume "PROP A"
wenzelm@19121
    79
    from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
wenzelm@19121
    80
    from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)
wenzelm@18466
    81
  qed
wenzelm@18466
    82
next
wenzelm@18466
    83
  assume conj: "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
wenzelm@18466
    84
  assume "PROP A"
wenzelm@19121
    85
  show "PROP B && PROP C"
wenzelm@19121
    86
  proof -
wenzelm@19121
    87
    from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
wenzelm@19121
    88
    from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])
wenzelm@18466
    89
  qed
wenzelm@18466
    90
qed
wenzelm@18466
    91
wenzelm@18466
    92
lemma conjunction_imp:
wenzelm@18466
    93
  includes meta_conjunction_syntax
wenzelm@18466
    94
  shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
wenzelm@18466
    95
proof
wenzelm@18466
    96
  assume r: "PROP A && PROP B ==> PROP C"
wenzelm@22933
    97
  assume ab: "PROP A" "PROP B"
wenzelm@22933
    98
  show "PROP C"
wenzelm@22933
    99
  proof (rule r)
wenzelm@22933
   100
    from ab show "PROP A && PROP B" .
wenzelm@22933
   101
  qed
wenzelm@18466
   102
next
wenzelm@18466
   103
  assume r: "PROP A ==> PROP B ==> PROP C"
wenzelm@18466
   104
  assume conj: "PROP A && PROP B"
wenzelm@18466
   105
  show "PROP C"
wenzelm@18466
   106
  proof (rule r)
wenzelm@19121
   107
    from conj show "PROP A" by (rule conjunctionD1)
wenzelm@19121
   108
    from conj show "PROP B" by (rule conjunctionD2)
wenzelm@18466
   109
  qed
wenzelm@18466
   110
qed
wenzelm@18466
   111
wenzelm@15803
   112
end