src/Pure/Pure.thy
author wenzelm
Thu Jan 19 21:22:15 2006 +0100 (2006-01-19)
changeset 18710 527aa560a9e0
parent 18663 8474756e4cbf
child 18836 3a1e4ee72075
permissions -rw-r--r--
tuned comments;
     1 (*  Title:      Pure/Pure.thy
     2     ID:         $Id$
     3 
     4 The actual Pure theory.
     5 *)
     6 
     7 header {* The Pure theory *}
     8 
     9 theory Pure
    10 imports ProtoPure
    11 begin
    12 
    13 subsection {* Common setup of internal components *}
    14 
    15 setup
    16 
    17 
    18 subsection {* Meta-level connectives in assumptions *}
    19 
    20 lemma meta_mp:
    21   assumes "PROP P ==> PROP Q" and "PROP P"
    22   shows "PROP Q"
    23     by (rule `PROP P ==> PROP Q` [OF `PROP P`])
    24 
    25 lemma meta_spec:
    26   assumes "!!x. PROP P(x)"
    27   shows "PROP P(x)"
    28     by (rule `!!x. PROP P(x)`)
    29 
    30 lemmas meta_allE = meta_spec [elim_format]
    31 
    32 
    33 subsection {* Meta-level conjunction *}
    34 
    35 locale (open) meta_conjunction_syntax =
    36   fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
    37 
    38 parse_translation {*
    39   [("\<^fixed>meta_conjunction", fn [t, u] => Logic.mk_conjunction (t, u))]
    40 *}
    41 
    42 lemma all_conjunction:
    43   includes meta_conjunction_syntax
    44   shows "(!!x. PROP A(x) && PROP B(x)) == ((!!x. PROP A(x)) && (!!x. PROP B(x)))"
    45 proof
    46   assume conj: "!!x. PROP A(x) && PROP B(x)"
    47   fix X assume r: "(!!x. PROP A(x)) ==> (!!x. PROP B(x)) ==> PROP X"
    48   show "PROP X"
    49   proof (rule r)
    50     fix x
    51     from conj show "PROP A(x)" .
    52     from conj show "PROP B(x)" .
    53   qed
    54 next
    55   assume conj: "(!!x. PROP A(x)) && (!!x. PROP B(x))"
    56   fix x
    57   fix X assume r: "PROP A(x) ==> PROP B(x) ==> PROP X"
    58   show "PROP X"
    59   proof (rule r)
    60     show "PROP A(x)"
    61     proof (rule conj)
    62       assume "!!x. PROP A(x)"
    63       then show "PROP A(x)" .
    64     qed
    65     show "PROP B(x)"
    66     proof (rule conj)
    67       assume "!!x. PROP B(x)"
    68       then show "PROP B(x)" .
    69     qed
    70   qed
    71 qed
    72 
    73 lemma imp_conjunction [unfolded prop_def]:
    74   includes meta_conjunction_syntax
    75   shows "(PROP A ==> PROP prop (PROP B && PROP C)) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
    76 proof (unfold prop_def, rule)
    77   assume conj: "PROP A ==> PROP B && PROP C"
    78   fix X assume r: "(PROP A ==> PROP B) ==> (PROP A ==> PROP C) ==> PROP X"
    79   show "PROP X"
    80   proof (rule r)
    81     assume "PROP A"
    82     from conj [OF `PROP A`] show "PROP B" .
    83     from conj [OF `PROP A`] show "PROP C" .
    84   qed
    85 next
    86   assume conj: "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
    87   assume "PROP A"
    88   fix X assume r: "PROP B ==> PROP C ==> PROP X"
    89   show "PROP X"
    90   proof (rule r)
    91     show "PROP B"
    92     proof (rule conj)
    93       assume "PROP A ==> PROP B"
    94       from this [OF `PROP A`] show "PROP B" .
    95     qed
    96     show "PROP C"
    97     proof (rule conj)
    98       assume "PROP A ==> PROP C"
    99       from this [OF `PROP A`] show "PROP C" .
   100     qed
   101   qed
   102 qed
   103 
   104 lemma conjunction_imp:
   105   includes meta_conjunction_syntax
   106   shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
   107 proof
   108   assume r: "PROP A && PROP B ==> PROP C"
   109   assume "PROP A" and "PROP B"
   110   show "PROP C" by (rule r) -
   111 next
   112   assume r: "PROP A ==> PROP B ==> PROP C"
   113   assume conj: "PROP A && PROP B"
   114   show "PROP C"
   115   proof (rule r)
   116     from conj show "PROP A" .
   117     from conj show "PROP B" .
   118   qed
   119 qed
   120 
   121 lemma conjunction_assoc:
   122   includes meta_conjunction_syntax
   123   shows "((PROP A && PROP B) && PROP C) == (PROP A && (PROP B && PROP C))"
   124   by (rule equal_intr_rule) (unfold imp_conjunction conjunction_imp)
   125 
   126 end