src/Pure/Pure.thy
author wenzelm
Thu Dec 22 00:28:52 2005 +0100 (2005-12-22)
changeset 18466 389a6f9c31f4
parent 18019 d1ff9ebb8bcb
child 18663 8474756e4cbf
permissions -rw-r--r--
added locale meta_conjunction_syntax and various conjunction rules;
     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 "Context.setup ()"
    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   fix X assume r: "(!!x. PROP A(x)) ==> (!!x. PROP B(x)) ==> PROP X"
    44   show "PROP X"
    45   proof (rule r)
    46     fix x
    47     from conj show "PROP A(x)" .
    48     from conj show "PROP B(x)" .
    49   qed
    50 next
    51   assume conj: "(!!x. PROP A(x)) && (!!x. PROP B(x))"
    52   fix x
    53   fix X assume r: "PROP A(x) ==> PROP B(x) ==> PROP X"
    54   show "PROP X"
    55   proof (rule r)
    56     show "PROP A(x)"
    57     proof (rule conj)
    58       assume "!!x. PROP A(x)"
    59       then show "PROP A(x)" .
    60     qed
    61     show "PROP B(x)"
    62     proof (rule conj)
    63       assume "!!x. PROP B(x)"
    64       then show "PROP B(x)" .
    65     qed
    66   qed
    67 qed
    68 
    69 lemma imp_conjunction [unfolded prop_def]:
    70   includes meta_conjunction_syntax
    71   shows "(PROP A ==> PROP prop (PROP B && PROP C)) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
    72 proof (unfold prop_def, rule)
    73   assume conj: "PROP A ==> PROP B && PROP C"
    74   fix X assume r: "(PROP A ==> PROP B) ==> (PROP A ==> PROP C) ==> PROP X"
    75   show "PROP X"
    76   proof (rule r)
    77     assume "PROP A"
    78     from conj [OF `PROP A`] show "PROP B" .
    79     from conj [OF `PROP A`] show "PROP C" .
    80   qed
    81 next
    82   assume conj: "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
    83   assume "PROP A"
    84   fix X assume r: "PROP B ==> PROP C ==> PROP X"
    85   show "PROP X"
    86   proof (rule r)
    87     show "PROP B"
    88     proof (rule conj)
    89       assume "PROP A ==> PROP B"
    90       from this [OF `PROP A`] show "PROP B" .
    91     qed
    92     show "PROP C"
    93     proof (rule conj)
    94       assume "PROP A ==> PROP C"
    95       from this [OF `PROP A`] show "PROP C" .
    96     qed
    97   qed
    98 qed
    99 
   100 lemma conjunction_imp:
   101   includes meta_conjunction_syntax
   102   shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
   103 proof
   104   assume r: "PROP A && PROP B ==> PROP C"
   105   assume "PROP A" and "PROP B"
   106   show "PROP C" by (rule r) -
   107 next
   108   assume r: "PROP A ==> PROP B ==> PROP C"
   109   assume conj: "PROP A && PROP B"
   110   show "PROP C"
   111   proof (rule r)
   112     from conj show "PROP A" .
   113     from conj show "PROP B" .
   114   qed
   115 qed
   116 
   117 lemma conjunction_assoc:
   118   includes meta_conjunction_syntax
   119   shows "((PROP A && PROP B) && PROP C) == (PROP A && (PROP B && PROP C))"
   120   by (rule equal_intr_rule) (unfold imp_conjunction conjunction_imp)
   121 
   122 end