added print translations tha avoid eta contraction for important binders.
authornipkow
Sun Dec 22 10:43:43 2002 +0100 (2002-12-22)
changeset 13763f94b569cd610
parent 13762 9dd78dab72bc
child 13764 3e180bf68496
added print translations tha avoid eta contraction for important binders.
src/HOL/HOL.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/HOL.thy	Sun Dec 22 10:42:09 2002 +0100
     1.2 +++ b/src/HOL/HOL.thy	Sun Dec 22 10:43:43 2002 +0100
     1.3 @@ -71,10 +71,17 @@
     1.4  
     1.5  translations
     1.6    "x ~= y"                == "~ (x = y)"
     1.7 -  "THE x. P"              == "The (%x. P)"
     1.8 +  "THE x. P"              => "The (%x. P)"
     1.9    "_Let (_binds b bs) e"  == "_Let b (_Let bs e)"
    1.10    "let x = a in e"        == "Let a (%x. e)"
    1.11  
    1.12 +print_translation {*
    1.13 +(* To avoid eta-contraction of body: *)
    1.14 +[("The", fn [Abs abs] =>
    1.15 +     let val (x,t) = atomic_abs_tr' abs
    1.16 +     in Syntax.const "_The" $ x $ t end)]
    1.17 +*}
    1.18 +
    1.19  syntax (output)
    1.20    "="           :: "['a, 'a] => bool"                    (infix 50)
    1.21    "_not_equal"  :: "['a, 'a] => bool"                    (infix "~=" 50)
     2.1 --- a/src/HOL/Hilbert_Choice.thy	Sun Dec 22 10:42:09 2002 +0100
     2.2 +++ b/src/HOL/Hilbert_Choice.thy	Sun Dec 22 10:43:43 2002 +0100
     2.3 @@ -22,7 +22,14 @@
     2.4  syntax
     2.5    "_Eps"        :: "[pttrn, bool] => 'a"    ("(3SOME _./ _)" [0, 10] 10)
     2.6  translations
     2.7 -  "SOME x. P" == "Eps (%x. P)"
     2.8 +  "SOME x. P" => "Eps (%x. P)"
     2.9 +
    2.10 +print_translation {*
    2.11 +(* to avoid eta-contraction of body *)
    2.12 +[("Eps", fn [Abs abs] =>
    2.13 +     let val (x,t) = atomic_abs_tr' abs
    2.14 +     in Syntax.const "_Eps" $ x $ t end)]
    2.15 +*}
    2.16  
    2.17  axioms
    2.18    someI: "P (x::'a) ==> P (SOME x. P x)"
     3.1 --- a/src/HOL/Set.thy	Sun Dec 22 10:42:09 2002 +0100
     3.2 +++ b/src/HOL/Set.thy	Sun Dec 22 10:43:43 2002 +0100
     3.3 @@ -74,15 +74,15 @@
     3.4    "x ~: y"      == "~ (x : y)"
     3.5    "{x, xs}"     == "insert x {xs}"
     3.6    "{x}"         == "insert x {}"
     3.7 -  "{x. P}"      == "Collect (%x. P)"
     3.8 +  "{x. P}"      => "Collect (%x. P)"
     3.9    "UN x y. B"   == "UN x. UN y. B"
    3.10    "UN x. B"     == "UNION UNIV (%x. B)"
    3.11    "INT x y. B"  == "INT x. INT y. B"
    3.12    "INT x. B"    == "INTER UNIV (%x. B)"
    3.13 -  "UN x:A. B"   == "UNION A (%x. B)"
    3.14 -  "INT x:A. B"  == "INTER A (%x. B)"
    3.15 -  "ALL x:A. P"  == "Ball A (%x. P)"
    3.16 -  "EX x:A. P"   == "Bex A (%x. P)"
    3.17 +  "UN x:A. B"   => "UNION A (%x. B)"
    3.18 +  "INT x:A. B"  => "INTER A (%x. B)"
    3.19 +  "ALL x:A. P"  => "Ball A (%x. P)"
    3.20 +  "EX x:A. P"   => "Bex A (%x. P)"
    3.21  
    3.22  syntax (output)
    3.23    "_setle"      :: "'a set => 'a set => bool"             ("op <=")
    3.24 @@ -150,22 +150,36 @@
    3.25    in [("@SetCompr", setcompr_tr)] end;
    3.26  *}
    3.27  
    3.28 +(* To avoid eta-contraction of body: *)
    3.29  print_translation {*
    3.30 -  let
    3.31 -    val ex_tr' = snd (mk_binder_tr' ("Ex", "DUMMY"));
    3.32 -
    3.33 -    fun setcompr_tr' [Abs (_, _, P)] =
    3.34 -      let
    3.35 -        fun check (Const ("Ex", _) $ Abs (_, _, P), n) = check (P, n + 1)
    3.36 -          | check (Const ("op &", _) $ (Const ("op =", _) $ Bound m $ e) $ P, n) =
    3.37 -              if n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
    3.38 -                ((0 upto (n - 1)) subset add_loose_bnos (e, 0, [])) then ()
    3.39 -              else raise Match;
    3.40 +let
    3.41 +  fun btr' syn [A,Abs abs] =
    3.42 +    let val (x,t) = atomic_abs_tr' abs
    3.43 +    in Syntax.const syn $ x $ A $ t end
    3.44 +in
    3.45 +[("Ball", btr' "_Ball"),("Bex", btr' "_Bex"),
    3.46 + ("UNION", btr' "@UNION"),("INTER", btr' "@INTER")]
    3.47 +end
    3.48 +*}
    3.49 +
    3.50 +print_translation {*
    3.51 +let
    3.52 +  val ex_tr' = snd (mk_binder_tr' ("Ex", "DUMMY"));
    3.53 +
    3.54 +  fun setcompr_tr' [Abs (abs as (_, _, P))] =
    3.55 +    let
    3.56 +      fun check (Const ("Ex", _) $ Abs (_, _, P), n) = check (P, n + 1)
    3.57 +        | check (Const ("op &", _) $ (Const ("op =", _) $ Bound m $ e) $ P, n) =
    3.58 +            n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
    3.59 +            ((0 upto (n - 1)) subset add_loose_bnos (e, 0, []))
    3.60  
    3.61          fun tr' (_ $ abs) =
    3.62            let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr' [abs]
    3.63            in Syntax.const "@SetCompr" $ e $ idts $ Q end;
    3.64 -      in check (P, 0); tr' P end;
    3.65 +    in if check (P, 0) then tr' P
    3.66 +       else let val (x,t) = atomic_abs_tr' abs
    3.67 +            in Syntax.const "@Coll" $ x $ t end
    3.68 +    end;
    3.69    in [("Collect", setcompr_tr')] end;
    3.70  *}
    3.71