added hidden internal_split constant;
authorwenzelm
Fri Feb 02 22:18:10 2001 +0100 (2001-02-02)
changeset 1103283f723e86dac
parent 11031 99c4bed16b9b
child 11033 fc3124a54ca9
added hidden internal_split constant;
tuned;
src/HOL/Product_Type.thy
     1.1 --- a/src/HOL/Product_Type.thy	Fri Feb 02 22:17:31 2001 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Fri Feb 02 22:18:10 2001 +0100
     1.3 @@ -8,10 +8,7 @@
     1.4  *)
     1.5  
     1.6  theory Product_Type = Fun
     1.7 -files 
     1.8 -  ("Tools/split_rule.ML")
     1.9 -  ("Product_Type_lemmas.ML")
    1.10 -:
    1.11 +files ("Product_Type_lemmas.ML") ("Tools/split_rule.ML"):
    1.12  
    1.13  
    1.14  (** products **)
    1.15 @@ -20,13 +17,13 @@
    1.16  
    1.17  constdefs
    1.18    Pair_Rep :: "['a, 'b] => ['a, 'b] => bool"
    1.19 - "Pair_Rep == (%a b. %x y. x=a & y=b)"
    1.20 +  "Pair_Rep == (%a b. %x y. x=a & y=b)"
    1.21  
    1.22  global
    1.23  
    1.24  typedef (Prod)
    1.25    ('a, 'b) "*"          (infixr 20)
    1.26 -    = "{f. ? a b. f = Pair_Rep (a::'a) (b::'b)}"
    1.27 +    = "{f. EX a b. f = Pair_Rep (a::'a) (b::'b)}"
    1.28  proof
    1.29    fix a b show "Pair_Rep a b : ?Prod"
    1.30      by blast
    1.31 @@ -80,7 +77,7 @@
    1.32    "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3\<Sigma> _\<in>_./ _)"   10)
    1.33    "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)
    1.34  
    1.35 -print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))]; *}
    1.36 +print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *}
    1.37  
    1.38  
    1.39  (* definitions *)
    1.40 @@ -89,8 +86,8 @@
    1.41  
    1.42  defs
    1.43    Pair_def:     "Pair a b == Abs_Prod(Pair_Rep a b)"
    1.44 -  fst_def:      "fst p == @a. ? b. p = (a, b)"
    1.45 -  snd_def:      "snd p == @b. ? a. p = (a, b)"
    1.46 +  fst_def:      "fst p == SOME a. EX b. p = (a, b)"
    1.47 +  snd_def:      "snd p == SOME b. EX a. p = (a, b)"
    1.48    split_def:    "split == (%c p. c (fst p) (snd p))"
    1.49    prod_fun_def: "prod_fun f g == split(%x y.(f(x), g(y)))"
    1.50    Sigma_def:    "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
    1.51 @@ -101,7 +98,7 @@
    1.52  
    1.53  global
    1.54  
    1.55 -typedef  unit = "{True}" 
    1.56 +typedef unit = "{True}"
    1.57  proof
    1.58    show "True : ?unit"
    1.59      by blast
    1.60 @@ -115,9 +112,22 @@
    1.61  defs
    1.62    Unity_def:    "() == Abs_unit True"
    1.63  
    1.64 +
    1.65 +
    1.66 +(** lemmas and tool setup **)
    1.67 +
    1.68  use "Product_Type_lemmas.ML"
    1.69  
    1.70 +constdefs
    1.71 +  internal_split :: "('a \<Rightarrow> 'b => 'c) => 'a * 'b => 'c"
    1.72 +  "internal_split == split"
    1.73 +
    1.74 +lemma internal_split_conv: "internal_split c (a, b) = c a b"
    1.75 +  by (simp only: internal_split_def split_conv)
    1.76 +
    1.77 +hide const internal_split
    1.78 +
    1.79  use "Tools/split_rule.ML"
    1.80 -setup split_attributes
    1.81 +setup SplitRule.setup
    1.82  
    1.83  end