src/HOL/Product_Type.thy
 changeset 15422 cbdddc0efadf parent 15404 a9a762f586b5 child 15481 fc075ae929e4
```     1.1 --- a/src/HOL/Product_Type.thy	Sat Dec 18 17:10:49 2004 +0100
1.2 +++ b/src/HOL/Product_Type.thy	Sat Dec 18 17:12:45 2004 +0100
1.3 @@ -78,9 +78,9 @@
1.4  qed
1.5
1.6  syntax (xsymbols)
1.7 -  "*"      :: "[type, type] => type"         ("(_ \\<times>/ _)" [21, 20] 20)
1.8 +  "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
1.9  syntax (HTML output)
1.10 -  "*"      :: "[type, type] => type"         ("(_ \\<times>/ _)" [21, 20] 20)
1.11 +  "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
1.12
1.13  local
1.14
1.15 @@ -157,12 +157,40 @@
1.16  end
1.17  *}
1.18
1.19 -text{*Deleted x-symbol and html support using @{text"\\<Sigma>"} (Sigma) because of the danger of confusion with Sum.*}
1.20 +
1.21 +(* print "split f" as "\<lambda>(x,y). f x y" and "split (\<lambda>x. f x)" as "\<lambda>(x,y). f x y" *)
1.22 +typed_print_translation {*
1.23 +let
1.24 +  fun split_guess_names_tr' _ T [Abs (x,_,Abs _)] = raise Match
1.25 +    | split_guess_names_tr' _ T  [Abs (x,xT,t)] =
1.26 +        (case (head_of t) of
1.27 +           Const ("split",_) => raise Match
1.28 +         | _ => let
1.29 +                  val (_::yT::_) = binder_types (domain_type T) handle Bind => raise Match;
1.30 +                  val (y,t') = atomic_abs_tr' ("y",yT,(incr_boundvars 1 t)\$Bound 0);
1.31 +                  val (x',t'') = atomic_abs_tr' (x,xT,t');
1.32 +                in Syntax.const "_abs" \$ (Syntax.const "_pattern" \$x'\$y) \$ t'' end)
1.33 +    | split_guess_names_tr' _ T [t] =
1.34 +       (case (head_of t) of
1.35 +           Const ("split",_) => raise Match
1.36 +         | _ => let
1.37 +                  val (xT::yT::_) = binder_types (domain_type T) handle Bind => raise Match;
1.38 +                  val (y,t') =
1.39 +                        atomic_abs_tr' ("y",yT,(incr_boundvars 2 t)\$Bound 1\$Bound 0);
1.40 +                  val (x',t'') = atomic_abs_tr' ("x",xT,t');
1.41 +                in Syntax.const "_abs" \$ (Syntax.const "_pattern" \$x'\$y) \$ t'' end)
1.42 +    | split_guess_names_tr' _ _ _ = raise Match;
1.43 +in [("split", split_guess_names_tr')]
1.44 +end
1.45 +*}
1.46 +
1.47 +text{*Deleted x-symbol and html support using @{text"\<Sigma>"} (Sigma) because of the danger of confusion with Sum.*}
1.48 +
1.49  syntax (xsymbols)
1.50 -  "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \\<times> _" [81, 80] 80)
1.51 +  "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)
1.52
1.53  syntax (HTML output)
1.54 -  "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \\<times> _" [81, 80] 80)
1.55 +  "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)
1.56
1.57  print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *}
1.58
1.59 @@ -612,7 +640,7 @@
1.60    by (unfold Sigma_def) blast
1.61
1.62  text {*
1.63 -  Elimination of @{term "(a, b) : A \\<times> B"} -- introduces no
1.64 +  Elimination of @{term "(a, b) : A \<times> B"} -- introduces no
1.65    eigenvariables.
1.66  *}
1.67
1.68 @@ -629,8 +657,8 @@
1.69    by blast
1.70
1.71  lemma Sigma_cong:
1.72 -     "\\<lbrakk>A = B; !!x. x \\<in> B \\<Longrightarrow> C x = D x\\<rbrakk>
1.73 -      \\<Longrightarrow> (SIGMA x: A. C x) = (SIGMA x: B. D x)"
1.74 +     "\<lbrakk>A = B; !!x. x \<in> B \<Longrightarrow> C x = D x\<rbrakk>
1.75 +      \<Longrightarrow> (SIGMA x: A. C x) = (SIGMA x: B. D x)"
1.76  by auto
1.77
1.78  lemma Sigma_mono: "[| A <= C; !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D"
```