src/HOL/Product_Type.thy
changeset 14359 3d9948163018
parent 14337 e13731554e50
child 14565 c6dc17aab88a
equal deleted inserted replaced
14358:233c5bd5b539 14359:3d9948163018
   125   (* The last rule accommodates tuples in `case C ... (x,y) ... => ...'
   125   (* The last rule accommodates tuples in `case C ... (x,y) ... => ...'
   126      The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *)
   126      The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *)
   127 
   127 
   128   "SIGMA x:A. B" => "Sigma A (%x. B)"
   128   "SIGMA x:A. B" => "Sigma A (%x. B)"
   129   "A <*> B"      => "Sigma A (_K B)"
   129   "A <*> B"      => "Sigma A (_K B)"
       
   130 
       
   131 (* reconstructs pattern from (nested) splits, avoiding eta-contraction of body*)
       
   132 (* works best with enclosing "let", if "let" does not avoid eta-contraction   *)
       
   133 print_translation {*
       
   134 let fun split_tr' [Abs (x,T,t as (Abs abs))] =
       
   135       (* split (%x y. t) => %(x,y) t *)
       
   136       let val (y,t') = atomic_abs_tr' abs;
       
   137           val (x',t'') = atomic_abs_tr' (x,T,t');
       
   138     
       
   139       in Syntax.const "_abs" $ (Syntax.const "_pattern" $x'$y) $ t'' end
       
   140     | split_tr' [Abs (x,T,(s as Const ("split",_)$t))] =
       
   141        (* split (%x. (split (%y z. t))) => %(x,y,z). t *)
       
   142        let val (Const ("_abs",_)$(Const ("_pattern",_)$y$z)$t') = split_tr' [t];
       
   143            val (x',t'') = atomic_abs_tr' (x,T,t');
       
   144        in Syntax.const "_abs"$ 
       
   145            (Syntax.const "_pattern"$x'$(Syntax.const "_patterns"$y$z))$t'' end
       
   146     | split_tr' [Const ("split",_)$t] =
       
   147        (* split (split (%x y z. t)) => %((x,y),z). t *)   
       
   148        split_tr' [(split_tr' [t])] (* inner split_tr' creates next pattern *)
       
   149     | split_tr' [Const ("_abs",_)$x_y$(Abs abs)] =
       
   150        (* split (%pttrn z. t) => %(pttrn,z). t *)
       
   151        let val (z,t) = atomic_abs_tr' abs;
       
   152        in Syntax.const "_abs" $ (Syntax.const "_pattern" $x_y$z) $ t end
       
   153     | split_tr' _ =  raise Match;
       
   154 in [("split", split_tr')]
       
   155 end
       
   156 *}
   130 
   157 
   131 syntax (xsymbols)
   158 syntax (xsymbols)
   132   "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3\<Sigma> _\<in>_./ _)"   10)
   159   "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3\<Sigma> _\<in>_./ _)"   10)
   133   "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)
   160   "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)
   134 
   161