src/Pure/Pure.thy
author haftmann
Fri, 25 Jul 2008 12:03:32 +0200
changeset 27681 8cedebf55539
parent 26958 ed3a58a9eae1
child 28699 32b6a8f12c1c
permissions -rw-r--r--
dropped locale (open)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15803
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Pure.thy
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
     3
*)
15803
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
     4
26435
bdce320cd426 eliminated delayed theory setup
wenzelm
parents: 26426
diff changeset
     5
section {* Further content for the Pure theory *}
20627
30da2841553e revert to previous version;
wenzelm
parents: 20596
diff changeset
     6
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
     7
subsection {* Meta-level connectives in assumptions *}
15803
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
     8
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
     9
lemma meta_mp:
18019
wenzelm
parents: 15824
diff changeset
    10
  assumes "PROP P ==> PROP Q" and "PROP P"
15803
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    11
  shows "PROP Q"
18019
wenzelm
parents: 15824
diff changeset
    12
    by (rule `PROP P ==> PROP Q` [OF `PROP P`])
15803
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    13
23432
cec811764a38 added meta_impE
nipkow
parents: 22933
diff changeset
    14
lemmas meta_impE = meta_mp [elim_format]
cec811764a38 added meta_impE
nipkow
parents: 22933
diff changeset
    15
15803
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    16
lemma meta_spec:
26958
ed3a58a9eae1 converted to regular application syntax;
wenzelm
parents: 26572
diff changeset
    17
  assumes "!!x. PROP P x"
ed3a58a9eae1 converted to regular application syntax;
wenzelm
parents: 26572
diff changeset
    18
  shows "PROP P x"
ed3a58a9eae1 converted to regular application syntax;
wenzelm
parents: 26572
diff changeset
    19
    by (rule `!!x. PROP P x`)
15803
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    20
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    21
lemmas meta_allE = meta_spec [elim_format]
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    22
26570
dbc458262f4c added swap_params;
wenzelm
parents: 26435
diff changeset
    23
lemma swap_params:
26958
ed3a58a9eae1 converted to regular application syntax;
wenzelm
parents: 26572
diff changeset
    24
  "(!!x y. PROP P x y) == (!!y x. PROP P x y)" ..
26570
dbc458262f4c added swap_params;
wenzelm
parents: 26435
diff changeset
    25
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    26
21625
fa8a7de5da28 added some support for embedded terms;
wenzelm
parents: 20627
diff changeset
    27
subsection {* Embedded terms *}
fa8a7de5da28 added some support for embedded terms;
wenzelm
parents: 20627
diff changeset
    28
27681
8cedebf55539 dropped locale (open)
haftmann
parents: 26958
diff changeset
    29
locale meta_term_syntax =
21625
fa8a7de5da28 added some support for embedded terms;
wenzelm
parents: 20627
diff changeset
    30
  fixes meta_term :: "'a => prop"  ("TERM _")
fa8a7de5da28 added some support for embedded terms;
wenzelm
parents: 20627
diff changeset
    31
fa8a7de5da28 added some support for embedded terms;
wenzelm
parents: 20627
diff changeset
    32
lemmas [intro?] = termI
fa8a7de5da28 added some support for embedded terms;
wenzelm
parents: 20627
diff changeset
    33
fa8a7de5da28 added some support for embedded terms;
wenzelm
parents: 20627
diff changeset
    34
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    35
subsection {* Meta-level conjunction *}
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    36
27681
8cedebf55539 dropped locale (open)
haftmann
parents: 26958
diff changeset
    37
locale meta_conjunction_syntax =
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    38
  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    39
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    40
lemma all_conjunction:
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    41
  includes meta_conjunction_syntax
26958
ed3a58a9eae1 converted to regular application syntax;
wenzelm
parents: 26572
diff changeset
    42
  shows "(!!x. PROP A x && PROP B x) == ((!!x. PROP A x) && (!!x. PROP B x))"
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    43
proof
26958
ed3a58a9eae1 converted to regular application syntax;
wenzelm
parents: 26572
diff changeset
    44
  assume conj: "!!x. PROP A x && PROP B x"
ed3a58a9eae1 converted to regular application syntax;
wenzelm
parents: 26572
diff changeset
    45
  show "(!!x. PROP A x) && (!!x. PROP B x)"
19121
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    46
  proof -
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    47
    fix x
26958
ed3a58a9eae1 converted to regular application syntax;
wenzelm
parents: 26572
diff changeset
    48
    from conj show "PROP A x" by (rule conjunctionD1)
ed3a58a9eae1 converted to regular application syntax;
wenzelm
parents: 26572
diff changeset
    49
    from conj show "PROP B x" by (rule conjunctionD2)
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    50
  qed
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    51
next
26958
ed3a58a9eae1 converted to regular application syntax;
wenzelm
parents: 26572
diff changeset
    52
  assume conj: "(!!x. PROP A x) && (!!x. PROP B x)"
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    53
  fix x
26958
ed3a58a9eae1 converted to regular application syntax;
wenzelm
parents: 26572
diff changeset
    54
  show "PROP A x && PROP B x"
19121
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    55
  proof -
26958
ed3a58a9eae1 converted to regular application syntax;
wenzelm
parents: 26572
diff changeset
    56
    show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])
ed3a58a9eae1 converted to regular application syntax;
wenzelm
parents: 26572
diff changeset
    57
    show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format])
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    58
  qed
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    59
qed
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    60
19121
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    61
lemma imp_conjunction:
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    62
  includes meta_conjunction_syntax
19121
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    63
  shows "(PROP A ==> PROP B && PROP C) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
18836
3a1e4ee72075 tuned proofs;
wenzelm
parents: 18710
diff changeset
    64
proof
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    65
  assume conj: "PROP A ==> PROP B && PROP C"
19121
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    66
  show "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    67
  proof -
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    68
    assume "PROP A"
19121
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    69
    from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    70
    from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    71
  qed
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    72
next
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    73
  assume conj: "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    74
  assume "PROP A"
19121
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    75
  show "PROP B && PROP C"
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    76
  proof -
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    77
    from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    78
    from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    79
  qed
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    80
qed
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    81
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    82
lemma conjunction_imp:
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    83
  includes meta_conjunction_syntax
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    84
  shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    85
proof
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    86
  assume r: "PROP A && PROP B ==> PROP C"
22933
338c7890c96f tuned proofs;
wenzelm
parents: 21627
diff changeset
    87
  assume ab: "PROP A" "PROP B"
338c7890c96f tuned proofs;
wenzelm
parents: 21627
diff changeset
    88
  show "PROP C"
338c7890c96f tuned proofs;
wenzelm
parents: 21627
diff changeset
    89
  proof (rule r)
338c7890c96f tuned proofs;
wenzelm
parents: 21627
diff changeset
    90
    from ab show "PROP A && PROP B" .
338c7890c96f tuned proofs;
wenzelm
parents: 21627
diff changeset
    91
  qed
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    92
next
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    93
  assume r: "PROP A ==> PROP B ==> PROP C"
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    94
  assume conj: "PROP A && PROP B"
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    95
  show "PROP C"
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    96
  proof (rule r)
19121
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    97
    from conj show "PROP A" by (rule conjunctionD1)
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    98
    from conj show "PROP B" by (rule conjunctionD2)
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    99
  qed
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
   100
qed
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
   101