attempt for more concise setup of non-etacontracting binders
authorhaftmann
Tue Jul 21 14:38:07 2009 +0200 (2009-07-21)
changeset 3212053a21a5e6889
parent 32119 a853099fd9ca
child 32121 a7bc3141e599
attempt for more concise setup of non-etacontracting binders
src/HOL/Set.thy
src/Pure/Syntax/syn_trans.ML
     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)"
     2.1 --- a/src/Pure/Syntax/syn_trans.ML	Tue Jul 21 14:36:26 2009 +0200
     2.2 +++ b/src/Pure/Syntax/syn_trans.ML	Tue Jul 21 14:38:07 2009 +0200
     2.3 @@ -8,6 +8,8 @@
     2.4  sig
     2.5    val eta_contract: bool ref
     2.6    val atomic_abs_tr': string * typ * term -> term * term
     2.7 +  val preserve_binder_abs_tr': string -> string -> string * (term list -> term)
     2.8 +  val preserve_binder_abs2_tr': string -> string -> string * (term list -> term)
     2.9    val mk_binder_tr: string * string -> string * (term list -> term)
    2.10    val mk_binder_tr': string * string -> string * (term list -> term)
    2.11    val dependent_tr': string * string -> term list -> term
    2.12 @@ -309,6 +311,14 @@
    2.13      ([], _) => raise Ast.AST ("abs_ast_tr'", asts)
    2.14    | (xs, body) => Ast.Appl [Ast.Constant "_lambda", Ast.fold_ast "_pttrns" xs, body]);
    2.15  
    2.16 +fun preserve_binder_abs_tr' name syn = (name, fn (Abs abs :: ts) =>
    2.17 +  let val (x, t) = atomic_abs_tr' abs
    2.18 +  in list_comb (Lexicon.const syn $ x $ t, ts) end);
    2.19 +
    2.20 +fun preserve_binder_abs2_tr' name syn = (name, fn (A :: Abs abs :: ts) =>
    2.21 +  let val (x, t) = atomic_abs_tr' abs
    2.22 +  in list_comb (Lexicon.const syn $ x $ A $ t, ts) end);
    2.23 +
    2.24  
    2.25  (* binder *)
    2.26