tuned;
authorwenzelm
Mon Oct 15 20:33:42 2001 +0200 (2001-10-15)
changeset 11777b03c8a3fcc6d
parent 11776 d4f9de0bde28
child 11778 37efbe093d3c
tuned;
src/HOL/Product_Type.thy
     1.1 --- a/src/HOL/Product_Type.thy	Mon Oct 15 20:33:05 2001 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Mon Oct 15 20:33:42 2001 +0200
     1.3 @@ -2,18 +2,17 @@
     1.4      ID:         $Id$
     1.5      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.6      Copyright   1992  University of Cambridge
     1.7 +*)
     1.8  
     1.9 -Ordered Pairs and the Cartesian product type.
    1.10 -The unit type.
    1.11 -*)
    1.12 +header {* Finite products (including unit) *}
    1.13  
    1.14  theory Product_Type = Fun
    1.15  files ("Product_Type_lemmas.ML") ("Tools/split_rule.ML"):
    1.16  
    1.17  
    1.18 -(** products **)
    1.19 +subsection {* Products *}
    1.20  
    1.21 -(* type definition *)
    1.22 +subsubsection {* Type definition *}
    1.23  
    1.24  constdefs
    1.25    Pair_Rep :: "['a, 'b] => ['a, 'b] => bool"
    1.26 @@ -34,8 +33,12 @@
    1.27  syntax (HTML output)
    1.28    "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
    1.29  
    1.30 +local
    1.31  
    1.32 -(* abstract constants and syntax *)
    1.33 +
    1.34 +subsubsection {* Abstract constants and syntax *}
    1.35 +
    1.36 +global
    1.37  
    1.38  consts
    1.39    fst      :: "'a * 'b => 'a"
    1.40 @@ -45,8 +48,12 @@
    1.41    Pair     :: "['a, 'b] => 'a * 'b"
    1.42    Sigma    :: "['a set, 'a => 'b set] => ('a * 'b) set"
    1.43  
    1.44 +local
    1.45  
    1.46 -(* patterns -- extends pre-defined type "pttrn" used in abstractions *)
    1.47 +text {*
    1.48 +  Patterns -- extends pre-defined type @{typ pttrn} used in
    1.49 +  abstractions.
    1.50 +*}
    1.51  
    1.52  nonterminals
    1.53    tuple_args patterns
    1.54 @@ -80,9 +87,7 @@
    1.55  print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *}
    1.56  
    1.57  
    1.58 -(* definitions *)
    1.59 -
    1.60 -local
    1.61 +subsubsection {* Definitions *}
    1.62  
    1.63  defs
    1.64    Pair_def:     "Pair a b == Abs_Prod(Pair_Rep a b)"
    1.65 @@ -93,8 +98,7 @@
    1.66    Sigma_def:    "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
    1.67  
    1.68  
    1.69 -
    1.70 -(** unit **)
    1.71 +subsection {* Unit *}
    1.72  
    1.73  typedef unit = "{True}"
    1.74  proof
    1.75 @@ -107,15 +111,15 @@
    1.76    "() == Abs_unit True"
    1.77  
    1.78  
    1.79 -
    1.80 -(** lemmas and tool setup **)
    1.81 +subsection {* Lemmas and tool setup *}
    1.82  
    1.83  use "Product_Type_lemmas.ML"
    1.84  
    1.85  lemma pair_imageI [intro]: "(a, b) : A ==> f a b : (%(a, b). f a b) ` A"
    1.86 -apply (rule_tac x = "(a,b)" in image_eqI)
    1.87 -apply  auto
    1.88 -done
    1.89 +  apply (rule_tac x = "(a, b)" in image_eqI)
    1.90 +   apply auto
    1.91 +  done
    1.92 +
    1.93  
    1.94  constdefs
    1.95    internal_split :: "('a => 'b => 'c) => 'a * 'b => 'c"