src/HOL/Prod.thy
changeset 1660 8cb42cd97579
parent 1655 5be64540f275
child 1672 2c109cd2fdd0
     1.1 --- a/src/HOL/Prod.thy	Wed Apr 17 11:46:10 1996 +0200
     1.2 +++ b/src/HOL/Prod.thy	Wed Apr 17 17:59:58 1996 +0200
     1.3 @@ -53,10 +53,16 @@
     1.4  
     1.5    "%(x,y,zs).b"   == "split(%x (y,zs).b)"
     1.6    "%(x,y).b"      == "split(%x y.b)"
     1.7 +(*<<<<<<< Prod.thy*)
     1.8 +(* The <= direction fails if split has more than one argument because
     1.9 +   ast-matching fails. Otherwise it would work fine *)
    1.10 +
    1.11 +(*=======*)
    1.12  
    1.13    "SIGMA x:A. B"  =>  "Sigma A (%x.B)"
    1.14    "A Times B"     =>  "Sigma A (_K B)"
    1.15  
    1.16 +(*>>>>>>> 1.13*)
    1.17  defs
    1.18    Pair_def      "Pair a b == Abs_Prod(Pair_Rep a b)"
    1.19    fst_def       "fst(p) == @a. ? b. p = (a, b)"
    1.20 @@ -80,8 +86,39 @@
    1.21  (* end 8bit 1 *)
    1.22  
    1.23  end
    1.24 +(*<<<<<<< Prod.thy*)
    1.25 +(*
    1.26 +ML
    1.27 +
    1.28 +local open Syntax
    1.29 +
    1.30 +fun pttrn(_ $ s $ t) = const"@pttrn" $ s $ t;
    1.31 +fun pttrns s t = const"@pttrns" $ s $ t;
    1.32 +
    1.33 +fun split2(Abs(x,T,t)) =
    1.34 +      let val (pats,u) = split1 t
    1.35 +      in (pttrns (Free(x,T)) pats, subst_bounds([free x],u)) end
    1.36 +  | split2(Const("split",_) $ r) =
    1.37 +      let val (pats,s) = split2(r)
    1.38 +          val (pats2,t) = split1(s)
    1.39 +      in (pttrns (pttrn pats) pats2, t) end
    1.40 +and split1(Abs(x,T,t)) =  (Free(x,T), subst_bounds([free x],t))
    1.41 +  | split1(Const("split",_)$t) = split2(t);
    1.42 +
    1.43 +fun split_tr'(t::args) =
    1.44 +  let val (pats,ft) = split2(t)
    1.45 +  in list_comb(const"_lambda" $ pttrn pats $ ft, args) end;
    1.46 +
    1.47 +in
    1.48 +
    1.49 +val print_translation = [("split", split_tr')];
    1.50 +
    1.51 +end;
    1.52 +*)
    1.53 +(*=======*)
    1.54  
    1.55  ML
    1.56  
    1.57  val print_translation = [("Sigma", dependent_tr' ("@Sigma", "@Times"))];
    1.58  
    1.59 +(*>>>>>>> 1.13*)