src/Pure/Pure.thy
author wenzelm
Thu Mar 27 14:41:12 2008 +0100 (2008-03-27)
changeset 26426 ddac7ef1e991
parent 23824 8ad7131dbfcf
child 26435 bdce320cd426
permissions -rw-r--r--
reduced to theory body (cf. OuterSyntax.process_file);
     1 (*  Title:      Pure/Pure.thy
     2     ID:         $Id$
     3 *)
     4 
     5 section {* The Pure theory *}
     6 
     7 setup  -- {* Common setup of internal components *}
     8 
     9 
    10 subsection {* Meta-level connectives in assumptions *}
    11 
    12 lemma meta_mp:
    13   assumes "PROP P ==> PROP Q" and "PROP P"
    14   shows "PROP Q"
    15     by (rule `PROP P ==> PROP Q` [OF `PROP P`])
    16 
    17 lemmas meta_impE = meta_mp [elim_format]
    18 
    19 lemma meta_spec:
    20   assumes "!!x. PROP P(x)"
    21   shows "PROP P(x)"
    22     by (rule `!!x. PROP P(x)`)
    23 
    24 lemmas meta_allE = meta_spec [elim_format]
    25 
    26 
    27 subsection {* Embedded terms *}
    28 
    29 locale (open) 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 (open) meta_conjunction_syntax =
    38   fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
    39 
    40 lemma all_conjunction:
    41   includes meta_conjunction_syntax
    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 "(\<And>x. PROP A(x)) && (\<And>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   includes meta_conjunction_syntax
    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   includes meta_conjunction_syntax
    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