Added print translation for pairs
authorschirmer
Tue Jan 20 13:56:27 2004 +0100 (2004-01-20)
changeset 143593d9948163018
parent 14358 233c5bd5b539
child 14360 e654599b114e
Added print translation for pairs
src/HOL/Product_Type.thy
     1.1 --- a/src/HOL/Product_Type.thy	Tue Jan 20 13:55:22 2004 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Tue Jan 20 13:56:27 2004 +0100
     1.3 @@ -128,6 +128,33 @@
     1.4    "SIGMA x:A. B" => "Sigma A (%x. B)"
     1.5    "A <*> B"      => "Sigma A (_K B)"
     1.6  
     1.7 +(* reconstructs pattern from (nested) splits, avoiding eta-contraction of body*)
     1.8 +(* works best with enclosing "let", if "let" does not avoid eta-contraction   *)
     1.9 +print_translation {*
    1.10 +let fun split_tr' [Abs (x,T,t as (Abs abs))] =
    1.11 +      (* split (%x y. t) => %(x,y) t *)
    1.12 +      let val (y,t') = atomic_abs_tr' abs;
    1.13 +          val (x',t'') = atomic_abs_tr' (x,T,t');
    1.14 +    
    1.15 +      in Syntax.const "_abs" $ (Syntax.const "_pattern" $x'$y) $ t'' end
    1.16 +    | split_tr' [Abs (x,T,(s as Const ("split",_)$t))] =
    1.17 +       (* split (%x. (split (%y z. t))) => %(x,y,z). t *)
    1.18 +       let val (Const ("_abs",_)$(Const ("_pattern",_)$y$z)$t') = split_tr' [t];
    1.19 +           val (x',t'') = atomic_abs_tr' (x,T,t');
    1.20 +       in Syntax.const "_abs"$ 
    1.21 +           (Syntax.const "_pattern"$x'$(Syntax.const "_patterns"$y$z))$t'' end
    1.22 +    | split_tr' [Const ("split",_)$t] =
    1.23 +       (* split (split (%x y z. t)) => %((x,y),z). t *)   
    1.24 +       split_tr' [(split_tr' [t])] (* inner split_tr' creates next pattern *)
    1.25 +    | split_tr' [Const ("_abs",_)$x_y$(Abs abs)] =
    1.26 +       (* split (%pttrn z. t) => %(pttrn,z). t *)
    1.27 +       let val (z,t) = atomic_abs_tr' abs;
    1.28 +       in Syntax.const "_abs" $ (Syntax.const "_pattern" $x_y$z) $ t end
    1.29 +    | split_tr' _ =  raise Match;
    1.30 +in [("split", split_tr')]
    1.31 +end
    1.32 +*}
    1.33 +
    1.34  syntax (xsymbols)
    1.35    "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3\<Sigma> _\<in>_./ _)"   10)
    1.36    "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)