src/HOL/Product_Type.thy
changeset 15422 cbdddc0efadf
parent 15404 a9a762f586b5
child 15481 fc075ae929e4
equal deleted inserted replaced
15421:fcf747c0b6b8 15422:cbdddc0efadf
    76   fix a b show "Pair_Rep a b : ?Prod"
    76   fix a b show "Pair_Rep a b : ?Prod"
    77     by blast
    77     by blast
    78 qed
    78 qed
    79 
    79 
    80 syntax (xsymbols)
    80 syntax (xsymbols)
    81   "*"      :: "[type, type] => type"         ("(_ \\<times>/ _)" [21, 20] 20)
    81   "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
    82 syntax (HTML output)
    82 syntax (HTML output)
    83   "*"      :: "[type, type] => type"         ("(_ \\<times>/ _)" [21, 20] 20)
    83   "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
    84 
    84 
    85 local
    85 local
    86 
    86 
    87 
    87 
    88 subsubsection {* Abstract constants and syntax *}
    88 subsubsection {* Abstract constants and syntax *}
   155     | split_tr' _ =  raise Match;
   155     | split_tr' _ =  raise Match;
   156 in [("split", split_tr')]
   156 in [("split", split_tr')]
   157 end
   157 end
   158 *}
   158 *}
   159 
   159 
   160 text{*Deleted x-symbol and html support using @{text"\\<Sigma>"} (Sigma) because of the danger of confusion with Sum.*}
   160 
       
   161 (* print "split f" as "\<lambda>(x,y). f x y" and "split (\<lambda>x. f x)" as "\<lambda>(x,y). f x y" *) 
       
   162 typed_print_translation {*
       
   163 let
       
   164   fun split_guess_names_tr' _ T [Abs (x,_,Abs _)] = raise Match
       
   165     | split_guess_names_tr' _ T  [Abs (x,xT,t)] =
       
   166         (case (head_of t) of
       
   167            Const ("split",_) => raise Match
       
   168          | _ => let 
       
   169                   val (_::yT::_) = binder_types (domain_type T) handle Bind => raise Match;
       
   170                   val (y,t') = atomic_abs_tr' ("y",yT,(incr_boundvars 1 t)$Bound 0); 
       
   171                   val (x',t'') = atomic_abs_tr' (x,xT,t');
       
   172                 in Syntax.const "_abs" $ (Syntax.const "_pattern" $x'$y) $ t'' end)
       
   173     | split_guess_names_tr' _ T [t] =
       
   174        (case (head_of t) of
       
   175            Const ("split",_) => raise Match 
       
   176          | _ => let 
       
   177                   val (xT::yT::_) = binder_types (domain_type T) handle Bind => raise Match;
       
   178                   val (y,t') = 
       
   179                         atomic_abs_tr' ("y",yT,(incr_boundvars 2 t)$Bound 1$Bound 0); 
       
   180                   val (x',t'') = atomic_abs_tr' ("x",xT,t');
       
   181                 in Syntax.const "_abs" $ (Syntax.const "_pattern" $x'$y) $ t'' end)
       
   182     | split_guess_names_tr' _ _ _ = raise Match;
       
   183 in [("split", split_guess_names_tr')]
       
   184 end 
       
   185 *}
       
   186 
       
   187 text{*Deleted x-symbol and html support using @{text"\<Sigma>"} (Sigma) because of the danger of confusion with Sum.*}
       
   188 
   161 syntax (xsymbols)
   189 syntax (xsymbols)
   162   "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \\<times> _" [81, 80] 80)
   190   "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)
   163 
   191 
   164 syntax (HTML output)
   192 syntax (HTML output)
   165   "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \\<times> _" [81, 80] 80)
   193   "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)
   166 
   194 
   167 print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *}
   195 print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *}
   168 
   196 
   169 
   197 
   170 subsubsection {* Definitions *}
   198 subsubsection {* Definitions *}
   610      |] ==> P"
   638      |] ==> P"
   611   -- {* The general elimination rule. *}
   639   -- {* The general elimination rule. *}
   612   by (unfold Sigma_def) blast
   640   by (unfold Sigma_def) blast
   613 
   641 
   614 text {*
   642 text {*
   615   Elimination of @{term "(a, b) : A \\<times> B"} -- introduces no
   643   Elimination of @{term "(a, b) : A \<times> B"} -- introduces no
   616   eigenvariables.
   644   eigenvariables.
   617 *}
   645 *}
   618 
   646 
   619 lemma SigmaD1: "(a, b) : Sigma A B ==> a : A"
   647 lemma SigmaD1: "(a, b) : Sigma A B ==> a : A"
   620 by blast
   648 by blast
   627         [| a:A;  b:B(a) |] ==> P
   655         [| a:A;  b:B(a) |] ==> P
   628      |] ==> P"
   656      |] ==> P"
   629   by blast
   657   by blast
   630 
   658 
   631 lemma Sigma_cong:
   659 lemma Sigma_cong:
   632      "\\<lbrakk>A = B; !!x. x \\<in> B \\<Longrightarrow> C x = D x\\<rbrakk>
   660      "\<lbrakk>A = B; !!x. x \<in> B \<Longrightarrow> C x = D x\<rbrakk>
   633       \\<Longrightarrow> (SIGMA x: A. C x) = (SIGMA x: B. D x)"
   661       \<Longrightarrow> (SIGMA x: A. C x) = (SIGMA x: B. D x)"
   634 by auto
   662 by auto
   635 
   663 
   636 lemma Sigma_mono: "[| A <= C; !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D"
   664 lemma Sigma_mono: "[| A <= C; !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D"
   637   by blast
   665   by blast
   638 
   666