judgment Trueprop;
authorwenzelm
Sun Oct 14 19:59:15 2001 +0200 (2001-10-14)
changeset 1174717a6dcd6f3cf
parent 11746 9bf11f1de9d6
child 11748 06eb315831ff
judgment Trueprop;
proper declarations of atomize rules;
src/FOL/IFOL.thy
     1.1 --- a/src/FOL/IFOL.thy	Sat Oct 13 21:46:53 2001 +0200
     1.2 +++ b/src/FOL/IFOL.thy	Sun Oct 14 19:59:15 2001 +0200
     1.3 @@ -18,9 +18,10 @@
     1.4  
     1.5  typedecl o
     1.6  
     1.7 -consts
     1.8 +judgment
     1.9 +  Trueprop      :: "o => prop"                  ("(_)" 5)
    1.10  
    1.11 -  Trueprop      :: "o => prop"                  ("(_)" 5)
    1.12 +consts
    1.13    True          :: o
    1.14    False         :: o
    1.15  
    1.16 @@ -130,7 +131,7 @@
    1.17  
    1.18  subsection {* Atomizing meta-level rules *}
    1.19  
    1.20 -lemma atomize_all: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
    1.21 +lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
    1.22  proof (rule equal_intr_rule)
    1.23    assume "!!x. P(x)"
    1.24    show "ALL x. P(x)" by (rule allI)
    1.25 @@ -139,7 +140,7 @@
    1.26    thus "!!x. P(x)" by (rule allE)
    1.27  qed
    1.28  
    1.29 -lemma atomize_imp: "(A ==> B) == Trueprop (A --> B)"
    1.30 +lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A --> B)"
    1.31  proof (rule equal_intr_rule)
    1.32    assume r: "A ==> B"
    1.33    show "A --> B" by (rule impI) (rule r)
    1.34 @@ -148,7 +149,7 @@
    1.35    thus B by (rule mp)
    1.36  qed
    1.37  
    1.38 -lemma atomize_eq: "(x == y) == Trueprop (x = y)"
    1.39 +lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)"
    1.40  proof (rule equal_intr_rule)
    1.41    assume "x == y"
    1.42    show "x = y" by (unfold prems) (rule refl)
    1.43 @@ -157,7 +158,4 @@
    1.44    thus "x == y" by (rule eq_reflection)
    1.45  qed
    1.46  
    1.47 -lemmas atomize = atomize_all atomize_imp
    1.48 -lemmas atomize' = atomize atomize_eq
    1.49 -
    1.50  end