# HG changeset patch
# User haftmann
# Date 1248179887 -7200
# Node ID 53a21a5e6889006ce8daf688e3ca46ec506b8e9d
# Parent  a853099fd9ca52010f84a34c63cde3255952ebdc
attempt for more concise setup of non-etacontracting binders

diff -r a853099fd9ca -r 53a21a5e6889 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Jul 21 14:36:26 2009 +0200
+++ b/src/HOL/Set.thy	Tue Jul 21 14:38:07 2009 +0200
@@ -291,14 +291,10 @@
   in [("@SetCompr", setcompr_tr)] end;
 *}
 
-(* To avoid eta-contraction of body: *)
-print_translation {*
-let
-  fun btr' syn [A, Abs abs] =
-    let val (x, t) = atomic_abs_tr' abs
-    in Syntax.const syn $ x $ A $ t end
-in [(@{const_syntax Ball}, btr' "_Ball"), (@{const_syntax Bex}, btr' "_Bex")] end
-*}
+print_translation {* [
+Syntax.preserve_binder_abs2_tr' @{const_syntax Ball} "_Ball",
+Syntax.preserve_binder_abs2_tr' @{const_syntax Bex} "_Bex"
+] *} -- {* to avoid eta-contraction of body *}
 
 print_translation {*
 let
@@ -1036,17 +1032,10 @@
   "INF x. B"     == "INF x:CONST UNIV. B"
   "INF x:A. B"   == "CONST INFI A (%x. B)"
 
-(* To avoid eta-contraction of body: *)
-print_translation {*
-let
-  fun btr' syn (A :: Abs abs :: ts) =
-    let val (x,t) = atomic_abs_tr' abs
-    in list_comb (Syntax.const syn $ x $ A $ t, ts) end
-  val const_syntax_name = Sign.const_syntax_name @{theory} o fst o dest_Const
-in
-[(const_syntax_name @{term SUPR}, btr' "_SUP"),(const_syntax_name @{term "INFI"}, btr' "_INF")]
-end
-*}
+print_translation {* [
+Syntax.preserve_binder_abs2_tr' @{const_syntax SUPR} "_SUP",
+Syntax.preserve_binder_abs2_tr' @{const_syntax INFI} "_INF"
+] *} -- {* to avoid eta-contraction of body *}
 
 context complete_lattice
 begin
@@ -1096,6 +1085,24 @@
   "\<not> \<Squnion>{}"
   unfolding Sup_bool_def by auto
 
+lemma INFI_bool_eq:
+  "INFI = Ball"
+proof (rule ext)+
+  fix A :: "'a set"
+  fix P :: "'a \<Rightarrow> bool"
+  show "(INF x:A. P x) \<longleftrightarrow> (\<forall>x \<in> A. P x)"
+    by (auto simp add: Ball_def INFI_def Inf_bool_def)
+qed
+
+lemma SUPR_bool_eq:
+  "SUPR = Bex"
+proof (rule ext)+
+  fix A :: "'a set"
+  fix P :: "'a \<Rightarrow> bool"
+  show "(SUP x:A. P x) \<longleftrightarrow> (\<exists>x \<in> A. P x)"
+    by (auto simp add: Bex_def SUPR_def Sup_bool_def)
+qed
+
 instantiation "fun" :: (type, complete_lattice) complete_lattice
 begin
 
@@ -1185,14 +1192,9 @@
   subscripts in Proof General.
 *}
 
-(* To avoid eta-contraction of body: *)
-print_translation {*
-let
-  fun btr' syn [A, Abs abs] =
-    let val (x, t) = atomic_abs_tr' abs
-    in Syntax.const syn $ x $ A $ t end
-in [(@{const_syntax UNION}, btr' "@UNION")] end
-*}
+print_translation {* [
+Syntax.preserve_binder_abs2_tr' @{const_syntax UNION} "@UNION"
+] *} -- {* to avoid eta-contraction of body *}
 
 lemma SUPR_set_eq:
   "(SUP x:S. f x) = (\<Union>x\<in>S. f x)"
@@ -1295,14 +1297,9 @@
   "INT x. B"    == "INT x:CONST UNIV. B"
   "INT x:A. B"  == "CONST INTER A (%x. B)"
 
-(* To avoid eta-contraction of body: *)
-print_translation {*
-let
-  fun btr' syn [A, Abs abs] =
-    let val (x, t) = atomic_abs_tr' abs
-    in Syntax.const syn $ x $ A $ t end
-in [(@{const_syntax INTER}, btr' "@INTER")] end
-*}
+print_translation {* [
+Syntax.preserve_binder_abs2_tr' @{const_syntax INTER} "@INTER"
+] *} -- {* to avoid eta-contraction of body *}
 
 lemma INFI_set_eq:
   "(INF x:S. f x) = (\<Inter>x\<in>S. f x)"
diff -r a853099fd9ca -r 53a21a5e6889 src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Tue Jul 21 14:36:26 2009 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Tue Jul 21 14:38:07 2009 +0200
@@ -8,6 +8,8 @@
 sig
   val eta_contract: bool ref
   val atomic_abs_tr': string * typ * term -> term * term
+  val preserve_binder_abs_tr': string -> string -> string * (term list -> term)
+  val preserve_binder_abs2_tr': string -> string -> string * (term list -> term)
   val mk_binder_tr: string * string -> string * (term list -> term)
   val mk_binder_tr': string * string -> string * (term list -> term)
   val dependent_tr': string * string -> term list -> term
@@ -309,6 +311,14 @@
     ([], _) => raise Ast.AST ("abs_ast_tr'", asts)
   | (xs, body) => Ast.Appl [Ast.Constant "_lambda", Ast.fold_ast "_pttrns" xs, body]);
 
+fun preserve_binder_abs_tr' name syn = (name, fn (Abs abs :: ts) =>
+  let val (x, t) = atomic_abs_tr' abs
+  in list_comb (Lexicon.const syn $ x $ t, ts) end);
+
+fun preserve_binder_abs2_tr' name syn = (name, fn (A :: Abs abs :: ts) =>
+  let val (x, t) = atomic_abs_tr' abs
+  in list_comb (Lexicon.const syn $ x $ A $ t, ts) end);
+
 
 (* binder *)