src/Pure/Pure.thy
 author wenzelm Sat May 15 23:23:45 2010 +0200 (2010-05-15) changeset 36951 985c197f2fe9 parent 29606 fedb8be05f24 child 48638 22d65e375c01 permissions -rw-r--r--
renamed structure ValueParse to Parse_Value;
eliminated old-style structure alias V;
```     1
```
```     2 section {* Further content for the Pure theory *}
```
```     3
```
```     4 subsection {* Meta-level connectives in assumptions *}
```
```     5
```
```     6 lemma meta_mp:
```
```     7   assumes "PROP P ==> PROP Q" and "PROP P"
```
```     8   shows "PROP Q"
```
```     9     by (rule `PROP P ==> PROP Q` [OF `PROP P`])
```
```    10
```
```    11 lemmas meta_impE = meta_mp [elim_format]
```
```    12
```
```    13 lemma meta_spec:
```
```    14   assumes "!!x. PROP P x"
```
```    15   shows "PROP P x"
```
```    16     by (rule `!!x. PROP P x`)
```
```    17
```
```    18 lemmas meta_allE = meta_spec [elim_format]
```
```    19
```
```    20 lemma swap_params:
```
```    21   "(!!x y. PROP P x y) == (!!y x. PROP P x y)" ..
```
```    22
```
```    23
```
```    24 subsection {* Meta-level conjunction *}
```
```    25
```
```    26 lemma all_conjunction:
```
```    27   "(!!x. PROP A x &&& PROP B x) == ((!!x. PROP A x) &&& (!!x. PROP B x))"
```
```    28 proof
```
```    29   assume conj: "!!x. PROP A x &&& PROP B x"
```
```    30   show "(!!x. PROP A x) &&& (!!x. PROP B x)"
```
```    31   proof -
```
```    32     fix x
```
```    33     from conj show "PROP A x" by (rule conjunctionD1)
```
```    34     from conj show "PROP B x" by (rule conjunctionD2)
```
```    35   qed
```
```    36 next
```
```    37   assume conj: "(!!x. PROP A x) &&& (!!x. PROP B x)"
```
```    38   fix x
```
```    39   show "PROP A x &&& PROP B x"
```
```    40   proof -
```
```    41     show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])
```
```    42     show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format])
```
```    43   qed
```
```    44 qed
```
```    45
```
```    46 lemma imp_conjunction:
```
```    47   "(PROP A ==> PROP B &&& PROP C) == (PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
```
```    48 proof
```
```    49   assume conj: "PROP A ==> PROP B &&& PROP C"
```
```    50   show "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
```
```    51   proof -
```
```    52     assume "PROP A"
```
```    53     from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
```
```    54     from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)
```
```    55   qed
```
```    56 next
```
```    57   assume conj: "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
```
```    58   assume "PROP A"
```
```    59   show "PROP B &&& PROP C"
```
```    60   proof -
```
```    61     from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
```
```    62     from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])
```
```    63   qed
```
```    64 qed
```
```    65
```
```    66 lemma conjunction_imp:
```
```    67   "(PROP A &&& PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
```
```    68 proof
```
```    69   assume r: "PROP A &&& PROP B ==> PROP C"
```
```    70   assume ab: "PROP A" "PROP B"
```
```    71   show "PROP C"
```
```    72   proof (rule r)
```
```    73     from ab show "PROP A &&& PROP B" .
```
```    74   qed
```
```    75 next
```
```    76   assume r: "PROP A ==> PROP B ==> PROP C"
```
```    77   assume conj: "PROP A &&& PROP B"
```
```    78   show "PROP C"
```
```    79   proof (rule r)
```
```    80     from conj show "PROP A" by (rule conjunctionD1)
```
```    81     from conj show "PROP B" by (rule conjunctionD2)
```
```    82   qed
```
```    83 qed
```
```    84
```