converted to regular application syntax;
authorwenzelm
Sun May 18 17:03:23 2008 +0200 (2008-05-18 ago)
changeset 26958ed3a58a9eae1
parent 26957 e3f04fdd994d
child 26959 f8f2df3e4d83
converted to regular application syntax;
src/FOL/ex/First_Order_Logic.thy
src/Pure/Pure.thy
     1.1 --- a/src/FOL/ex/First_Order_Logic.thy	Sun May 18 17:03:20 2008 +0200
     1.2 +++ b/src/FOL/ex/First_Order_Logic.thy	Sun May 18 17:03:23 2008 +0200
     1.3 @@ -110,7 +110,7 @@
     1.4    equal :: "i \<Rightarrow> i \<Rightarrow> o"  (infixl "=" 50)
     1.5  where
     1.6    refl [intro]: "x = x" and
     1.7 -  subst: "x = y \<Longrightarrow> P(x) \<Longrightarrow> P(y)"
     1.8 +  subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y"
     1.9  
    1.10  theorem trans [trans]: "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"
    1.11    by (rule subst)
    1.12 @@ -128,32 +128,32 @@
    1.13    All :: "(i \<Rightarrow> o) \<Rightarrow> o"  (binder "\<forall>" 10) and
    1.14    Ex :: "(i \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" 10)
    1.15  where
    1.16 -  allI [intro]: "(\<And>x. P(x)) \<Longrightarrow> \<forall>x. P(x)" and
    1.17 -  allD [dest]: "\<forall>x. P(x) \<Longrightarrow> P(a)" and
    1.18 -  exI [intro]: "P(a) \<Longrightarrow> \<exists>x. P(x)" and
    1.19 -  exE [elim]: "\<exists>x. P(x) \<Longrightarrow> (\<And>x. P(x) \<Longrightarrow> C) \<Longrightarrow> C"
    1.20 +  allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x" and
    1.21 +  allD [dest]: "\<forall>x. P x \<Longrightarrow> P a" and
    1.22 +  exI [intro]: "P a \<Longrightarrow> \<exists>x. P x" and
    1.23 +  exE [elim]: "\<exists>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> C) \<Longrightarrow> C"
    1.24  
    1.25  
    1.26 -lemma "(\<exists>x. P(f(x))) \<longrightarrow> (\<exists>y. P(y))"
    1.27 +lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"
    1.28  proof
    1.29 -  assume "\<exists>x. P(f(x))"
    1.30 -  then show "\<exists>y. P(y)"
    1.31 +  assume "\<exists>x. P (f x)"
    1.32 +  then show "\<exists>y. P y"
    1.33    proof
    1.34 -    fix x assume "P(f(x))"
    1.35 +    fix x assume "P (f x)"
    1.36      then show ?thesis ..
    1.37    qed
    1.38  qed
    1.39  
    1.40 -lemma "(\<exists>x. \<forall>y. R(x, y)) \<longrightarrow> (\<forall>y. \<exists>x. R(x, y))"
    1.41 +lemma "(\<exists>x. \<forall>y. R x y) \<longrightarrow> (\<forall>y. \<exists>x. R x y)"
    1.42  proof
    1.43 -  assume "\<exists>x. \<forall>y. R(x, y)"
    1.44 -  then show "\<forall>y. \<exists>x. R(x, y)"
    1.45 +  assume "\<exists>x. \<forall>y. R x y"
    1.46 +  then show "\<forall>y. \<exists>x. R x y"
    1.47    proof
    1.48 -    fix x assume a: "\<forall>y. R(x, y)"
    1.49 +    fix x assume a: "\<forall>y. R x y"
    1.50      show ?thesis
    1.51      proof
    1.52 -      fix y from a have "R(x, y)" ..
    1.53 -      then show "\<exists>x. R(x, y)" ..
    1.54 +      fix y from a have "R x y" ..
    1.55 +      then show "\<exists>x. R x y" ..
    1.56      qed
    1.57    qed
    1.58  qed
     2.1 --- a/src/Pure/Pure.thy	Sun May 18 17:03:20 2008 +0200
     2.2 +++ b/src/Pure/Pure.thy	Sun May 18 17:03:23 2008 +0200
     2.3 @@ -14,14 +14,14 @@
     2.4  lemmas meta_impE = meta_mp [elim_format]
     2.5  
     2.6  lemma meta_spec:
     2.7 -  assumes "!!x. PROP P(x)"
     2.8 -  shows "PROP P(x)"
     2.9 -    by (rule `!!x. PROP P(x)`)
    2.10 +  assumes "!!x. PROP P x"
    2.11 +  shows "PROP P x"
    2.12 +    by (rule `!!x. PROP P x`)
    2.13  
    2.14  lemmas meta_allE = meta_spec [elim_format]
    2.15  
    2.16  lemma swap_params:
    2.17 -  "(!!x y. PROP P(x, y)) == (!!y x. PROP P(x, y))" ..
    2.18 +  "(!!x y. PROP P x y) == (!!y x. PROP P x y)" ..
    2.19  
    2.20  
    2.21  subsection {* Embedded terms *}
    2.22 @@ -39,22 +39,22 @@
    2.23  
    2.24  lemma all_conjunction:
    2.25    includes meta_conjunction_syntax
    2.26 -  shows "(!!x. PROP A(x) && PROP B(x)) == ((!!x. PROP A(x)) && (!!x. PROP B(x)))"
    2.27 +  shows "(!!x. PROP A x && PROP B x) == ((!!x. PROP A x) && (!!x. PROP B x))"
    2.28  proof
    2.29 -  assume conj: "!!x. PROP A(x) && PROP B(x)"
    2.30 -  show "(!!x. PROP A(x)) && (!!x. PROP B(x))"
    2.31 +  assume conj: "!!x. PROP A x && PROP B x"
    2.32 +  show "(!!x. PROP A x) && (!!x. PROP B x)"
    2.33    proof -
    2.34      fix x
    2.35 -    from conj show "PROP A(x)" by (rule conjunctionD1)
    2.36 -    from conj show "PROP B(x)" by (rule conjunctionD2)
    2.37 +    from conj show "PROP A x" by (rule conjunctionD1)
    2.38 +    from conj show "PROP B x" by (rule conjunctionD2)
    2.39    qed
    2.40  next
    2.41 -  assume conj: "(!!x. PROP A(x)) && (!!x. PROP B(x))"
    2.42 +  assume conj: "(!!x. PROP A x) && (!!x. PROP B x)"
    2.43    fix x
    2.44 -  show "PROP A(x) && PROP B(x)"
    2.45 +  show "PROP A x && PROP B x"
    2.46    proof -
    2.47 -    show "PROP A(x)" by (rule conj [THEN conjunctionD1, rule_format])
    2.48 -    show "PROP B(x)" by (rule conj [THEN conjunctionD2, rule_format])
    2.49 +    show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])
    2.50 +    show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format])
    2.51    qed
    2.52  qed
    2.53