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