src/Pure/Pure.thy
changeset 28856 5e009a80fe6d
parent 28699 32b6a8f12c1c
child 29606 fedb8be05f24
     1.1 --- a/src/Pure/Pure.thy	Wed Nov 19 18:15:31 2008 +0100
     1.2 +++ b/src/Pure/Pure.thy	Thu Nov 20 00:03:47 2008 +0100
     1.3 @@ -24,34 +24,22 @@
     1.4    "(!!x y. PROP P x y) == (!!y x. PROP P x y)" ..
     1.5  
     1.6  
     1.7 -subsection {* Embedded terms *}
     1.8 -
     1.9 -locale meta_term_syntax =
    1.10 -  fixes meta_term :: "'a => prop"  ("TERM _")
    1.11 -
    1.12 -lemmas [intro?] = termI
    1.13 -
    1.14 -
    1.15  subsection {* Meta-level conjunction *}
    1.16  
    1.17 -locale meta_conjunction_syntax =
    1.18 -  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
    1.19 -
    1.20  lemma all_conjunction:
    1.21 -  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
    1.22 -  shows "(!!x. PROP A x && PROP B x) == ((!!x. PROP A x) && (!!x. PROP B x))"
    1.23 +  "(!!x. PROP A x &&& PROP B x) == ((!!x. PROP A x) &&& (!!x. PROP B x))"
    1.24  proof
    1.25 -  assume conj: "!!x. PROP A x && PROP B x"
    1.26 -  show "(!!x. PROP A x) && (!!x. PROP B x)"
    1.27 +  assume conj: "!!x. PROP A x &&& PROP B x"
    1.28 +  show "(!!x. PROP A x) &&& (!!x. PROP B x)"
    1.29    proof -
    1.30      fix x
    1.31      from conj show "PROP A x" by (rule conjunctionD1)
    1.32      from conj show "PROP B x" by (rule conjunctionD2)
    1.33    qed
    1.34  next
    1.35 -  assume conj: "(!!x. PROP A x) && (!!x. PROP B x)"
    1.36 +  assume conj: "(!!x. PROP A x) &&& (!!x. PROP B x)"
    1.37    fix x
    1.38 -  show "PROP A x && PROP B x"
    1.39 +  show "PROP A x &&& PROP B x"
    1.40    proof -
    1.41      show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])
    1.42      show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format])
    1.43 @@ -59,20 +47,19 @@
    1.44  qed
    1.45  
    1.46  lemma imp_conjunction:
    1.47 -  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
    1.48 -  shows "(PROP A ==> PROP B && PROP C) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
    1.49 +  "(PROP A ==> PROP B &&& PROP C) == (PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
    1.50  proof
    1.51 -  assume conj: "PROP A ==> PROP B && PROP C"
    1.52 -  show "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
    1.53 +  assume conj: "PROP A ==> PROP B &&& PROP C"
    1.54 +  show "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
    1.55    proof -
    1.56      assume "PROP A"
    1.57      from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
    1.58      from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)
    1.59    qed
    1.60  next
    1.61 -  assume conj: "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
    1.62 +  assume conj: "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
    1.63    assume "PROP A"
    1.64 -  show "PROP B && PROP C"
    1.65 +  show "PROP B &&& PROP C"
    1.66    proof -
    1.67      from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
    1.68      from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])
    1.69 @@ -80,18 +67,17 @@
    1.70  qed
    1.71  
    1.72  lemma conjunction_imp:
    1.73 -  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
    1.74 -  shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
    1.75 +  "(PROP A &&& PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
    1.76  proof
    1.77 -  assume r: "PROP A && PROP B ==> PROP C"
    1.78 +  assume r: "PROP A &&& PROP B ==> PROP C"
    1.79    assume ab: "PROP A" "PROP B"
    1.80    show "PROP C"
    1.81    proof (rule r)
    1.82 -    from ab show "PROP A && PROP B" .
    1.83 +    from ab show "PROP A &&& PROP B" .
    1.84    qed
    1.85  next
    1.86    assume r: "PROP A ==> PROP B ==> PROP C"
    1.87 -  assume conj: "PROP A && PROP B"
    1.88 +  assume conj: "PROP A &&& PROP B"
    1.89    show "PROP C"
    1.90    proof (rule r)
    1.91      from conj show "PROP A" by (rule conjunctionD1)