src/HOL/Product_Type.thy
changeset 35115 446c5063e4fd
parent 34900 9b12b0824bfe
child 35364 b8c62d60195c
     1.1 --- a/src/HOL/Product_Type.thy	Thu Feb 11 22:55:16 2010 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Thu Feb 11 23:00:22 2010 +0100
     1.3 @@ -180,65 +180,81 @@
     1.4    "_patterns"   :: "[pttrn, patterns] => patterns"      ("_,/ _")
     1.5  
     1.6  translations
     1.7 -  "(x, y)"       == "Pair x y"
     1.8 +  "(x, y)" == "CONST Pair x y"
     1.9    "_tuple x (_tuple_args y z)" == "_tuple x (_tuple_arg (_tuple y z))"
    1.10 -  "%(x,y,zs).b"  == "split(%x (y,zs).b)"
    1.11 -  "%(x,y).b"     == "split(%x y. b)"
    1.12 -  "_abs (Pair x y) t" => "%(x,y).t"
    1.13 +  "%(x, y, zs). b" == "CONST split (%x (y, zs). b)"
    1.14 +  "%(x, y). b" == "CONST split (%x y. b)"
    1.15 +  "_abs (CONST Pair x y) t" => "%(x, y). t"
    1.16    (* The last rule accommodates tuples in `case C ... (x,y) ... => ...'
    1.17       The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *)
    1.18  
    1.19 -(* reconstructs pattern from (nested) splits, avoiding eta-contraction of body*)
    1.20 -(* works best with enclosing "let", if "let" does not avoid eta-contraction   *)
    1.21 +(*reconstruct pattern from (nested) splits, avoiding eta-contraction of body;
    1.22 +  works best with enclosing "let", if "let" does not avoid eta-contraction*)
    1.23  print_translation {*
    1.24 -let fun split_tr' [Abs (x,T,t as (Abs abs))] =
    1.25 -      (* split (%x y. t) => %(x,y) t *)
    1.26 -      let val (y,t') = atomic_abs_tr' abs;
    1.27 -          val (x',t'') = atomic_abs_tr' (x,T,t');
    1.28 -    
    1.29 -      in Syntax.const "_abs" $ (Syntax.const "_pattern" $x'$y) $ t'' end
    1.30 -    | split_tr' [Abs (x,T,(s as Const ("split",_)$t))] =
    1.31 -       (* split (%x. (split (%y z. t))) => %(x,y,z). t *)
    1.32 -       let val (Const ("_abs",_)$(Const ("_pattern",_)$y$z)$t') = split_tr' [t];
    1.33 -           val (x',t'') = atomic_abs_tr' (x,T,t');
    1.34 -       in Syntax.const "_abs"$ 
    1.35 -           (Syntax.const "_pattern"$x'$(Syntax.const "_patterns"$y$z))$t'' end
    1.36 -    | split_tr' [Const ("split",_)$t] =
    1.37 -       (* split (split (%x y z. t)) => %((x,y),z). t *)   
    1.38 -       split_tr' [(split_tr' [t])] (* inner split_tr' creates next pattern *)
    1.39 -    | split_tr' [Const ("_abs",_)$x_y$(Abs abs)] =
    1.40 -       (* split (%pttrn z. t) => %(pttrn,z). t *)
    1.41 -       let val (z,t) = atomic_abs_tr' abs;
    1.42 -       in Syntax.const "_abs" $ (Syntax.const "_pattern" $x_y$z) $ t end
    1.43 -    | split_tr' _ =  raise Match;
    1.44 -in [("split", split_tr')]
    1.45 -end
    1.46 +let
    1.47 +  fun split_tr' [Abs (x, T, t as (Abs abs))] =
    1.48 +        (* split (%x y. t) => %(x,y) t *)
    1.49 +        let
    1.50 +          val (y, t') = atomic_abs_tr' abs;
    1.51 +          val (x', t'') = atomic_abs_tr' (x, T, t');
    1.52 +        in
    1.53 +          Syntax.const @{syntax_const "_abs"} $
    1.54 +            (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
    1.55 +        end
    1.56 +    | split_tr' [Abs (x, T, (s as Const (@{const_syntax split}, _) $ t))] =
    1.57 +        (* split (%x. (split (%y z. t))) => %(x,y,z). t *)
    1.58 +        let
    1.59 +          val Const (@{syntax_const "_abs"}, _) $
    1.60 +            (Const (@{syntax_const "_pattern"}, _) $ y $ z) $ t' = split_tr' [t];
    1.61 +          val (x', t'') = atomic_abs_tr' (x, T, t');
    1.62 +        in
    1.63 +          Syntax.const @{syntax_const "_abs"} $
    1.64 +            (Syntax.const @{syntax_const "_pattern"} $ x' $
    1.65 +              (Syntax.const @{syntax_const "_patterns"} $ y $ z)) $ t''
    1.66 +        end
    1.67 +    | split_tr' [Const (@{const_syntax split}, _) $ t] =
    1.68 +        (* split (split (%x y z. t)) => %((x, y), z). t *)
    1.69 +        split_tr' [(split_tr' [t])] (* inner split_tr' creates next pattern *)
    1.70 +    | split_tr' [Const (@{syntax_const "_abs"}, _) $ x_y $ Abs abs] =
    1.71 +        (* split (%pttrn z. t) => %(pttrn,z). t *)
    1.72 +        let val (z, t) = atomic_abs_tr' abs in
    1.73 +          Syntax.const @{syntax_const "_abs"} $
    1.74 +            (Syntax.const @{syntax_const "_pattern"} $ x_y $ z) $ t
    1.75 +        end
    1.76 +    | split_tr' _ = raise Match;
    1.77 +in [(@{const_syntax split}, split_tr')] end
    1.78  *}
    1.79  
    1.80  (* print "split f" as "\<lambda>(x,y). f x y" and "split (\<lambda>x. f x)" as "\<lambda>(x,y). f x y" *) 
    1.81  typed_print_translation {*
    1.82  let
    1.83 -  fun split_guess_names_tr' _ T [Abs (x,_,Abs _)] = raise Match
    1.84 -    | split_guess_names_tr' _ T  [Abs (x,xT,t)] =
    1.85 +  fun split_guess_names_tr' _ T [Abs (x, _, Abs _)] = raise Match
    1.86 +    | split_guess_names_tr' _ T [Abs (x, xT, t)] =
    1.87          (case (head_of t) of
    1.88 -           Const ("split",_) => raise Match
    1.89 -         | _ => let 
    1.90 -                  val (_::yT::_) = binder_types (domain_type T) handle Bind => raise Match;
    1.91 -                  val (y,t') = atomic_abs_tr' ("y",yT,(incr_boundvars 1 t)$Bound 0); 
    1.92 -                  val (x',t'') = atomic_abs_tr' (x,xT,t');
    1.93 -                in Syntax.const "_abs" $ (Syntax.const "_pattern" $x'$y) $ t'' end)
    1.94 +          Const (@{const_syntax split}, _) => raise Match
    1.95 +        | _ =>
    1.96 +          let 
    1.97 +            val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
    1.98 +            val (y, t') = atomic_abs_tr' ("y", yT, incr_boundvars 1 t $ Bound 0);
    1.99 +            val (x', t'') = atomic_abs_tr' (x, xT, t');
   1.100 +          in
   1.101 +            Syntax.const @{syntax_const "_abs"} $
   1.102 +              (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
   1.103 +          end)
   1.104      | split_guess_names_tr' _ T [t] =
   1.105 -       (case (head_of t) of
   1.106 -           Const ("split",_) => raise Match 
   1.107 -         | _ => let 
   1.108 -                  val (xT::yT::_) = binder_types (domain_type T) handle Bind => raise Match;
   1.109 -                  val (y,t') = 
   1.110 -                        atomic_abs_tr' ("y",yT,(incr_boundvars 2 t)$Bound 1$Bound 0); 
   1.111 -                  val (x',t'') = atomic_abs_tr' ("x",xT,t');
   1.112 -                in Syntax.const "_abs" $ (Syntax.const "_pattern" $x'$y) $ t'' end)
   1.113 +        (case head_of t of
   1.114 +          Const (@{const_syntax split}, _) => raise Match
   1.115 +        | _ =>
   1.116 +          let
   1.117 +            val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
   1.118 +            val (y, t') = atomic_abs_tr' ("y", yT, incr_boundvars 2 t $ Bound 1 $ Bound 0);
   1.119 +            val (x', t'') = atomic_abs_tr' ("x", xT, t');
   1.120 +          in
   1.121 +            Syntax.const @{syntax_const "_abs"} $
   1.122 +              (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
   1.123 +          end)
   1.124      | split_guess_names_tr' _ _ _ = raise Match;
   1.125 -in [("split", split_guess_names_tr')]
   1.126 -end 
   1.127 +in [(@{const_syntax split}, split_guess_names_tr')] end
   1.128  *}
   1.129  
   1.130  
   1.131 @@ -855,10 +871,9 @@
   1.132    Times  (infixr "\<times>" 80)
   1.133  
   1.134  syntax
   1.135 -  "@Sigma" ::"[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" [0, 0, 10] 10)
   1.136 -
   1.137 +  "_Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3SIGMA _:_./ _)" [0, 0, 10] 10)
   1.138  translations
   1.139 -  "SIGMA x:A. B" == "Product_Type.Sigma A (%x. B)"
   1.140 +  "SIGMA x:A. B" == "CONST Sigma A (%x. B)"
   1.141  
   1.142  lemma SigmaI [intro!]: "[| a:A;  b:B(a) |] ==> (a,b) : Sigma A B"
   1.143    by (unfold Sigma_def) blast