src/HOL/Set.thy
changeset 32120 53a21a5e6889
parent 32117 0762b9ad83df
child 32135 f645b51e8e54
     1.1 --- a/src/HOL/Set.thy	Tue Jul 21 14:36:26 2009 +0200
     1.2 +++ b/src/HOL/Set.thy	Tue Jul 21 14:38:07 2009 +0200
     1.3 @@ -291,14 +291,10 @@
     1.4    in [("@SetCompr", setcompr_tr)] end;
     1.5  *}
     1.6  
     1.7 -(* To avoid eta-contraction of body: *)
     1.8 -print_translation {*
     1.9 -let
    1.10 -  fun btr' syn [A, Abs abs] =
    1.11 -    let val (x, t) = atomic_abs_tr' abs
    1.12 -    in Syntax.const syn $ x $ A $ t end
    1.13 -in [(@{const_syntax Ball}, btr' "_Ball"), (@{const_syntax Bex}, btr' "_Bex")] end
    1.14 -*}
    1.15 +print_translation {* [
    1.16 +Syntax.preserve_binder_abs2_tr' @{const_syntax Ball} "_Ball",
    1.17 +Syntax.preserve_binder_abs2_tr' @{const_syntax Bex} "_Bex"
    1.18 +] *} -- {* to avoid eta-contraction of body *}
    1.19  
    1.20  print_translation {*
    1.21  let
    1.22 @@ -1036,17 +1032,10 @@
    1.23    "INF x. B"     == "INF x:CONST UNIV. B"
    1.24    "INF x:A. B"   == "CONST INFI A (%x. B)"
    1.25  
    1.26 -(* To avoid eta-contraction of body: *)
    1.27 -print_translation {*
    1.28 -let
    1.29 -  fun btr' syn (A :: Abs abs :: ts) =
    1.30 -    let val (x,t) = atomic_abs_tr' abs
    1.31 -    in list_comb (Syntax.const syn $ x $ A $ t, ts) end
    1.32 -  val const_syntax_name = Sign.const_syntax_name @{theory} o fst o dest_Const
    1.33 -in
    1.34 -[(const_syntax_name @{term SUPR}, btr' "_SUP"),(const_syntax_name @{term "INFI"}, btr' "_INF")]
    1.35 -end
    1.36 -*}
    1.37 +print_translation {* [
    1.38 +Syntax.preserve_binder_abs2_tr' @{const_syntax SUPR} "_SUP",
    1.39 +Syntax.preserve_binder_abs2_tr' @{const_syntax INFI} "_INF"
    1.40 +] *} -- {* to avoid eta-contraction of body *}
    1.41  
    1.42  context complete_lattice
    1.43  begin
    1.44 @@ -1096,6 +1085,24 @@
    1.45    "\<not> \<Squnion>{}"
    1.46    unfolding Sup_bool_def by auto
    1.47  
    1.48 +lemma INFI_bool_eq:
    1.49 +  "INFI = Ball"
    1.50 +proof (rule ext)+
    1.51 +  fix A :: "'a set"
    1.52 +  fix P :: "'a \<Rightarrow> bool"
    1.53 +  show "(INF x:A. P x) \<longleftrightarrow> (\<forall>x \<in> A. P x)"
    1.54 +    by (auto simp add: Ball_def INFI_def Inf_bool_def)
    1.55 +qed
    1.56 +
    1.57 +lemma SUPR_bool_eq:
    1.58 +  "SUPR = Bex"
    1.59 +proof (rule ext)+
    1.60 +  fix A :: "'a set"
    1.61 +  fix P :: "'a \<Rightarrow> bool"
    1.62 +  show "(SUP x:A. P x) \<longleftrightarrow> (\<exists>x \<in> A. P x)"
    1.63 +    by (auto simp add: Bex_def SUPR_def Sup_bool_def)
    1.64 +qed
    1.65 +
    1.66  instantiation "fun" :: (type, complete_lattice) complete_lattice
    1.67  begin
    1.68  
    1.69 @@ -1185,14 +1192,9 @@
    1.70    subscripts in Proof General.
    1.71  *}
    1.72  
    1.73 -(* To avoid eta-contraction of body: *)
    1.74 -print_translation {*
    1.75 -let
    1.76 -  fun btr' syn [A, Abs abs] =
    1.77 -    let val (x, t) = atomic_abs_tr' abs
    1.78 -    in Syntax.const syn $ x $ A $ t end
    1.79 -in [(@{const_syntax UNION}, btr' "@UNION")] end
    1.80 -*}
    1.81 +print_translation {* [
    1.82 +Syntax.preserve_binder_abs2_tr' @{const_syntax UNION} "@UNION"
    1.83 +] *} -- {* to avoid eta-contraction of body *}
    1.84  
    1.85  lemma SUPR_set_eq:
    1.86    "(SUP x:S. f x) = (\<Union>x\<in>S. f x)"
    1.87 @@ -1295,14 +1297,9 @@
    1.88    "INT x. B"    == "INT x:CONST UNIV. B"
    1.89    "INT x:A. B"  == "CONST INTER A (%x. B)"
    1.90  
    1.91 -(* To avoid eta-contraction of body: *)
    1.92 -print_translation {*
    1.93 -let
    1.94 -  fun btr' syn [A, Abs abs] =
    1.95 -    let val (x, t) = atomic_abs_tr' abs
    1.96 -    in Syntax.const syn $ x $ A $ t end
    1.97 -in [(@{const_syntax INTER}, btr' "@INTER")] end
    1.98 -*}
    1.99 +print_translation {* [
   1.100 +Syntax.preserve_binder_abs2_tr' @{const_syntax INTER} "@INTER"
   1.101 +] *} -- {* to avoid eta-contraction of body *}
   1.102  
   1.103  lemma INFI_set_eq:
   1.104    "(INF x:S. f x) = (\<Inter>x\<in>S. f x)"