src/Pure/Pure.thy
author wenzelm
Sun Jan 29 19:23:43 2006 +0100 (2006-01-29)
changeset 18836 3a1e4ee72075
parent 18710 527aa560a9e0
child 19048 2b875dd5eb4c
permissions -rw-r--r--
tuned proofs;
     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   unfolding prop_def
    77 proof
    78   assume conj: "PROP A ==> PROP B && PROP C"
    79   fix X assume r: "(PROP A ==> PROP B) ==> (PROP A ==> PROP C) ==> PROP X"
    80   show "PROP X"
    81   proof (rule r)
    82     assume "PROP A"
    83     from conj [OF `PROP A`] show "PROP B" .
    84     from conj [OF `PROP A`] show "PROP C" .
    85   qed
    86 next
    87   assume conj: "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
    88   assume "PROP A"
    89   fix X assume r: "PROP B ==> PROP C ==> PROP X"
    90   show "PROP X"
    91   proof (rule r)
    92     show "PROP B"
    93     proof (rule conj)
    94       assume "PROP A ==> PROP B"
    95       from this [OF `PROP A`] show "PROP B" .
    96     qed
    97     show "PROP C"
    98     proof (rule conj)
    99       assume "PROP A ==> PROP C"
   100       from this [OF `PROP A`] show "PROP C" .
   101     qed
   102   qed
   103 qed
   104 
   105 lemma conjunction_imp:
   106   includes meta_conjunction_syntax
   107   shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
   108 proof
   109   assume r: "PROP A && PROP B ==> PROP C"
   110   assume "PROP A" and "PROP B"
   111   show "PROP C" by (rule r) -
   112 next
   113   assume r: "PROP A ==> PROP B ==> PROP C"
   114   assume conj: "PROP A && PROP B"
   115   show "PROP C"
   116   proof (rule r)
   117     from conj show "PROP A" .
   118     from conj show "PROP B" .
   119   qed
   120 qed
   121 
   122 lemma conjunction_assoc:
   123   includes meta_conjunction_syntax
   124   shows "((PROP A && PROP B) && PROP C) == (PROP A && (PROP B && PROP C))"
   125   unfolding conjunction_imp .
   126 
   127 end