src/Pure/Pure.thy
author ballarin
Tue Oct 28 11:03:07 2008 +0100 (2008-10-28)
changeset 28699 32b6a8f12c1c
parent 27681 8cedebf55539
child 28856 5e009a80fe6d
permissions -rw-r--r--
Removed 'includes meta_term_syntax' and 'includes meta_conjunction_syntax'.
     1 (*  Title:      Pure/Pure.thy
     2     ID:         $Id$
     3 *)
     4 
     5 section {* Further content for the Pure theory *}
     6 
     7 subsection {* Meta-level connectives in assumptions *}
     8 
     9 lemma meta_mp:
    10   assumes "PROP P ==> PROP Q" and "PROP P"
    11   shows "PROP Q"
    12     by (rule `PROP P ==> PROP Q` [OF `PROP P`])
    13 
    14 lemmas meta_impE = meta_mp [elim_format]
    15 
    16 lemma meta_spec:
    17   assumes "!!x. PROP P x"
    18   shows "PROP P x"
    19     by (rule `!!x. PROP P x`)
    20 
    21 lemmas meta_allE = meta_spec [elim_format]
    22 
    23 lemma swap_params:
    24   "(!!x y. PROP P x y) == (!!y x. PROP P x y)" ..
    25 
    26 
    27 subsection {* Embedded terms *}
    28 
    29 locale meta_term_syntax =
    30   fixes meta_term :: "'a => prop"  ("TERM _")
    31 
    32 lemmas [intro?] = termI
    33 
    34 
    35 subsection {* Meta-level conjunction *}
    36 
    37 locale meta_conjunction_syntax =
    38   fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
    39 
    40 lemma all_conjunction:
    41   fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
    42   shows "(!!x. PROP A x && PROP B x) == ((!!x. PROP A x) && (!!x. PROP B x))"
    43 proof
    44   assume conj: "!!x. PROP A x && PROP B x"
    45   show "(!!x. PROP A x) && (!!x. PROP B x)"
    46   proof -
    47     fix x
    48     from conj show "PROP A x" by (rule conjunctionD1)
    49     from conj show "PROP B x" by (rule conjunctionD2)
    50   qed
    51 next
    52   assume conj: "(!!x. PROP A x) && (!!x. PROP B x)"
    53   fix x
    54   show "PROP A x && PROP B x"
    55   proof -
    56     show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])
    57     show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format])
    58   qed
    59 qed
    60 
    61 lemma imp_conjunction:
    62   fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
    63   shows "(PROP A ==> PROP B && PROP C) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
    64 proof
    65   assume conj: "PROP A ==> PROP B && PROP C"
    66   show "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
    67   proof -
    68     assume "PROP A"
    69     from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
    70     from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)
    71   qed
    72 next
    73   assume conj: "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
    74   assume "PROP A"
    75   show "PROP B && PROP C"
    76   proof -
    77     from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
    78     from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])
    79   qed
    80 qed
    81 
    82 lemma conjunction_imp:
    83   fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
    84   shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
    85 proof
    86   assume r: "PROP A && PROP B ==> PROP C"
    87   assume ab: "PROP A" "PROP B"
    88   show "PROP C"
    89   proof (rule r)
    90     from ab show "PROP A && PROP B" .
    91   qed
    92 next
    93   assume r: "PROP A ==> PROP B ==> PROP C"
    94   assume conj: "PROP A && PROP B"
    95   show "PROP C"
    96   proof (rule r)
    97     from conj show "PROP A" by (rule conjunctionD1)
    98     from conj show "PROP B" by (rule conjunctionD2)
    99   qed
   100 qed
   101