added print translation for split: split f --> %(x,y). f x y
authorschirmer
Sat Dec 18 17:12:45 2004 +0100 (2004-12-18)
changeset 15422cbdddc0efadf
parent 15421 fcf747c0b6b8
child 15423 761a4f8e6ad6
added print translation for split: split f --> %(x,y). f x y
src/HOL/Product_Type.thy
     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"