src/Pure/Pure.thy
author haftmann
Fri Nov 10 07:44:47 2006 +0100 (2006-11-10)
changeset 21286 b5e7b80caa6a
parent 20627 30da2841553e
child 21625 fa8a7de5da28
permissions -rw-r--r--
introduces canonical AList functions for loop_tacs
     1 (*  Title:      Pure/Pure.thy
     2     ID:         $Id$
     3 *)
     4 
     5 header {* The Pure theory *}
     6 
     7 theory Pure
     8 imports ProtoPure
     9 begin
    10 
    11 setup  -- {* Common setup of internal components *}
    12 
    13 
    14 subsection {* Meta-level connectives in assumptions *}
    15 
    16 lemma meta_mp:
    17   assumes "PROP P ==> PROP Q" and "PROP P"
    18   shows "PROP Q"
    19     by (rule `PROP P ==> PROP Q` [OF `PROP P`])
    20 
    21 lemma meta_spec:
    22   assumes "!!x. PROP P(x)"
    23   shows "PROP P(x)"
    24     by (rule `!!x. PROP P(x)`)
    25 
    26 lemmas meta_allE = meta_spec [elim_format]
    27 
    28 
    29 subsection {* Meta-level conjunction *}
    30 
    31 locale (open) meta_conjunction_syntax =
    32   fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
    33 
    34 parse_translation {*
    35   [("\<^fixed>meta_conjunction", fn [t, u] => Logic.mk_conjunction (t, u))]
    36 *}
    37 
    38 lemma all_conjunction:
    39   includes meta_conjunction_syntax
    40   shows "(!!x. PROP A(x) && PROP B(x)) == ((!!x. PROP A(x)) && (!!x. PROP B(x)))"
    41 proof
    42   assume conj: "!!x. PROP A(x) && PROP B(x)"
    43   show "(\<And>x. PROP A(x)) && (\<And>x. PROP B(x))"
    44   proof -
    45     fix x
    46     from conj show "PROP A(x)" by (rule conjunctionD1)
    47     from conj show "PROP B(x)" by (rule conjunctionD2)
    48   qed
    49 next
    50   assume conj: "(!!x. PROP A(x)) && (!!x. PROP B(x))"
    51   fix x
    52   show "PROP A(x) && PROP B(x)"
    53   proof -
    54     show "PROP A(x)" by (rule conj [THEN conjunctionD1, rule_format])
    55     show "PROP B(x)" by (rule conj [THEN conjunctionD2, rule_format])
    56   qed
    57 qed
    58 
    59 lemma imp_conjunction:
    60   includes meta_conjunction_syntax
    61   shows "(PROP A ==> PROP B && PROP C) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
    62 proof
    63   assume conj: "PROP A ==> PROP B && PROP C"
    64   show "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
    65   proof -
    66     assume "PROP A"
    67     from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
    68     from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)
    69   qed
    70 next
    71   assume conj: "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
    72   assume "PROP A"
    73   show "PROP B && PROP C"
    74   proof -
    75     from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
    76     from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])
    77   qed
    78 qed
    79 
    80 lemma conjunction_imp:
    81   includes meta_conjunction_syntax
    82   shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
    83 proof
    84   assume r: "PROP A && PROP B ==> PROP C"
    85   assume "PROP A" and "PROP B"
    86   show "PROP C" by (rule r) -
    87 next
    88   assume r: "PROP A ==> PROP B ==> PROP C"
    89   assume conj: "PROP A && PROP B"
    90   show "PROP C"
    91   proof (rule r)
    92     from conj show "PROP A" by (rule conjunctionD1)
    93     from conj show "PROP B" by (rule conjunctionD2)
    94   qed
    95 qed
    96 
    97 end