src/Pure/Pure.thy
author wenzelm
Wed, 21 Jan 2009 23:21:44 +0100
changeset 29606 fedb8be05f24
parent 28856 5e009a80fe6d
child 48638 22d65e375c01
permissions -rw-r--r--
removed Ids;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15803
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
     1
26435
bdce320cd426 eliminated delayed theory setup
wenzelm
parents: 26426
diff changeset
     2
section {* Further content for the Pure theory *}
20627
30da2841553e revert to previous version;
wenzelm
parents: 20596
diff changeset
     3
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
     4
subsection {* Meta-level connectives in assumptions *}
15803
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
     5
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
     6
lemma meta_mp:
18019
wenzelm
parents: 15824
diff changeset
     7
  assumes "PROP P ==> PROP Q" and "PROP P"
15803
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
     8
  shows "PROP Q"
18019
wenzelm
parents: 15824
diff changeset
     9
    by (rule `PROP P ==> PROP Q` [OF `PROP P`])
15803
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    10
23432
cec811764a38 added meta_impE
nipkow
parents: 22933
diff changeset
    11
lemmas meta_impE = meta_mp [elim_format]
cec811764a38 added meta_impE
nipkow
parents: 22933
diff changeset
    12
15803
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    13
lemma meta_spec:
26958
ed3a58a9eae1 converted to regular application syntax;
wenzelm
parents: 26572
diff changeset
    14
  assumes "!!x. PROP P x"
ed3a58a9eae1 converted to regular application syntax;
wenzelm
parents: 26572
diff changeset
    15
  shows "PROP P x"
ed3a58a9eae1 converted to regular application syntax;
wenzelm
parents: 26572
diff changeset
    16
    by (rule `!!x. PROP P x`)
15803
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    17
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    18
lemmas meta_allE = meta_spec [elim_format]
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    19
26570
dbc458262f4c added swap_params;
wenzelm
parents: 26435
diff changeset
    20
lemma swap_params:
26958
ed3a58a9eae1 converted to regular application syntax;
wenzelm
parents: 26572
diff changeset
    21
  "(!!x y. PROP P x y) == (!!y x. PROP P x y)" ..
26570
dbc458262f4c added swap_params;
wenzelm
parents: 26435
diff changeset
    22
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    23
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    24
subsection {* Meta-level conjunction *}
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    25
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    26
lemma all_conjunction:
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28699
diff changeset
    27
  "(!!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
    28
proof
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28699
diff changeset
    29
  assume conj: "!!x. PROP A x &&& PROP B x"
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28699
diff changeset
    30
  show "(!!x. PROP A x) &&& (!!x. PROP B x)"
19121
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    31
  proof -
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    32
    fix x
26958
ed3a58a9eae1 converted to regular application syntax;
wenzelm
parents: 26572
diff changeset
    33
    from conj show "PROP A x" by (rule conjunctionD1)
ed3a58a9eae1 converted to regular application syntax;
wenzelm
parents: 26572
diff changeset
    34
    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
    35
  qed
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    36
next
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28699
diff changeset
    37
  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
    38
  fix x
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28699
diff changeset
    39
  show "PROP A x &&& PROP B x"
19121
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    40
  proof -
26958
ed3a58a9eae1 converted to regular application syntax;
wenzelm
parents: 26572
diff changeset
    41
    show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])
ed3a58a9eae1 converted to regular application syntax;
wenzelm
parents: 26572
diff changeset
    42
    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
    43
  qed
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    44
qed
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    45
19121
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    46
lemma imp_conjunction:
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28699
diff changeset
    47
  "(PROP A ==> PROP B &&& PROP C) == (PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
18836
3a1e4ee72075 tuned proofs;
wenzelm
parents: 18710
diff changeset
    48
proof
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28699
diff changeset
    49
  assume conj: "PROP A ==> PROP B &&& PROP C"
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28699
diff changeset
    50
  show "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
19121
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    51
  proof -
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    52
    assume "PROP A"
19121
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    53
    from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    54
    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
    55
  qed
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    56
next
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28699
diff changeset
    57
  assume conj: "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    58
  assume "PROP A"
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28699
diff changeset
    59
  show "PROP B &&& PROP C"
19121
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    60
  proof -
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    61
    from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    62
    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
    63
  qed
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    64
qed
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    65
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    66
lemma conjunction_imp:
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28699
diff changeset
    67
  "(PROP A &&& PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    68
proof
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28699
diff changeset
    69
  assume r: "PROP A &&& PROP B ==> PROP C"
22933
338c7890c96f tuned proofs;
wenzelm
parents: 21627
diff changeset
    70
  assume ab: "PROP A" "PROP B"
338c7890c96f tuned proofs;
wenzelm
parents: 21627
diff changeset
    71
  show "PROP C"
338c7890c96f tuned proofs;
wenzelm
parents: 21627
diff changeset
    72
  proof (rule r)
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28699
diff changeset
    73
    from ab show "PROP A &&& PROP B" .
22933
338c7890c96f tuned proofs;
wenzelm
parents: 21627
diff changeset
    74
  qed
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    75
next
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    76
  assume r: "PROP A ==> PROP B ==> PROP C"
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28699
diff changeset
    77
  assume conj: "PROP A &&& PROP B"
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    78
  show "PROP C"
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    79
  proof (rule r)
19121
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    80
    from conj show "PROP A" by (rule conjunctionD1)
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    81
    from conj show "PROP B" by (rule conjunctionD2)
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    82
  qed
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    83
qed
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    84