# HG changeset patch
# User nipkow
# Date 1040565760 -3600
# Node ID 3e180bf68496257e581e95ec48d442ce518f44b5
# Parent  f94b569cd6109d36e0592c98f4486ee6c0d4ca56
removed some problems with print translations

diff -r f94b569cd610 -r 3e180bf68496 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sun Dec 22 10:43:43 2002 +0100
+++ b/src/HOL/HOL.thy	Sun Dec 22 15:02:40 2002 +0100
@@ -71,7 +71,7 @@
 
 translations
   "x ~= y"                == "~ (x = y)"
-  "THE x. P"              => "The (%x. P)"
+  "THE x. P"              == "The (%x. P)"
   "_Let (_binds b bs) e"  == "_Let b (_Let bs e)"
   "let x = a in e"        == "Let a (%x. e)"
 
diff -r f94b569cd610 -r 3e180bf68496 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Sun Dec 22 10:43:43 2002 +0100
+++ b/src/HOL/Hilbert_Choice.thy	Sun Dec 22 15:02:40 2002 +0100
@@ -22,7 +22,7 @@
 syntax
   "_Eps"        :: "[pttrn, bool] => 'a"    ("(3SOME _./ _)" [0, 10] 10)
 translations
-  "SOME x. P" => "Eps (%x. P)"
+  "SOME x. P" == "Eps (%x. P)"
 
 print_translation {*
 (* to avoid eta-contraction of body *)
diff -r f94b569cd610 -r 3e180bf68496 src/HOL/Hoare/Hoare.thy
--- a/src/HOL/Hoare/Hoare.thy	Sun Dec 22 10:43:43 2002 +0100
+++ b/src/HOL/Hoare/Hoare.thy	Sun Dec 22 15:02:40 2002 +0100
@@ -48,15 +48,8 @@
   "Valid p c q == !s s'. Sem c s s' --> s : p --> s' : q"
 
 
-nonterminals
-  vars
-
 syntax
-  ""		     :: "id => vars"		       ("_")
-  "_vars" 	     :: "[id, vars] => vars"	       ("_ _")
-
-syntax
- "@hoare_vars" :: "[vars, 'a assn,'a com,'a assn] => bool"
+ "@hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
                  ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
 syntax ("" output)
  "@hoare"      :: "['a assn,'a com,'a assn] => bool"
@@ -65,18 +58,24 @@
 (** parse translations **)
 
 ML{*
-fun mk_abstuple []     body = absfree ("x", dummyT, body)
-  | mk_abstuple [v]    body = absfree ((fst o dest_Free) v, dummyT, body)
-  | mk_abstuple (v::w) body = Syntax.const "split" $
-                              absfree ((fst o dest_Free) v, dummyT, mk_abstuple w body);
+
+local
+fun free a = Free(a,dummyT)
+fun abs((a,T),body) =
+  let val a = absfree(a, dummyT, body)
+  in if T = Bound 0 then a else Const(Syntax.constrainAbsC,dummyT) $ a $ T end
+in
 
-  
-fun mk_fbody v e []      = Syntax.const "Unity"
-  | mk_fbody v e [x]     = if v=x then e else x
-  | mk_fbody v e (x::xs) = Syntax.const "Pair" $ (if v=x then e else x) $
-                           mk_fbody v e xs;
+fun mk_abstuple [x] body = abs (x, body)
+  | mk_abstuple (x::xs) body =
+      Syntax.const "split" $ abs (x, mk_abstuple xs body);
 
-fun mk_fexp v e xs = mk_abstuple xs (mk_fbody v e xs);
+fun mk_fbody a e [x as (b,_)] = if a=b then e else free b
+  | mk_fbody a e ((b,_)::xs) =
+      Syntax.const "Pair" $ (if a=b then e else free b) $ mk_fbody a e xs;
+
+fun mk_fexp a e xs = mk_abstuple xs (mk_fbody a e xs)
+end
 *}
 
 (* bexp_tr & assn_tr *)
@@ -88,37 +87,38 @@
   
 fun assn_tr r xs = Syntax.const "Collect" $ mk_abstuple xs r;
 *}
-
 (* com_tr *)
 ML{*
-fun assign_tr [Free (V,_),E] xs = Syntax.const "Basic" $
-                                      mk_fexp (Free(V,dummyT)) E xs
-  | assign_tr ts _ = raise TERM ("assign_tr", ts);
-
-fun com_tr (Const("@assign",_) $ Free (V,_) $ E) xs =
-               assign_tr [Free (V,dummyT),E] xs
+fun com_tr (Const("@assign",_) $ Free (a,_) $ e) xs =
+      Syntax.const "Basic" $ mk_fexp a e xs
   | com_tr (Const ("Basic",_) $ f) xs = Syntax.const "Basic" $ f
-  | com_tr (Const ("Seq",_) $ c1 $ c2) xs = Syntax.const "Seq" $
-                                                 com_tr c1 xs $ com_tr c2 xs
-  | com_tr (Const ("Cond",_) $ b $ c1 $ c2) xs = Syntax.const "Cond" $
-                                  bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
-  | com_tr (Const ("While",_) $ b $ I $ c) xs = Syntax.const "While" $
-                                         bexp_tr b xs $ assn_tr I xs $ com_tr c xs
-  | com_tr trm _ = trm;
+  | com_tr (Const ("Seq",_) $ c1 $ c2) xs =
+      Syntax.const "Seq" $ com_tr c1 xs $ com_tr c2 xs
+  | com_tr (Const ("Cond",_) $ b $ c1 $ c2) xs =
+      Syntax.const "Cond" $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
+  | com_tr (Const ("While",_) $ b $ I $ c) xs =
+      Syntax.const "While" $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs
+  | com_tr t _ = t (* if t is just a Free/Var *)
 *}
 
 (* triple_tr *)
 ML{*
-fun vars_tr (x as Free _) = [x]
-  | vars_tr (Const ("_vars", _) $ (x as Free _) $ vars) = x :: vars_tr vars
-  | vars_tr t = raise TERM ("vars_tr", [t]);
+local
+
+fun var_tr(Free(a,_)) = (a,Bound 0) (* Bound 0 = dummy term *)
+  | var_tr(Const ("_constrain", _) $ (Free (a,_)) $ T) = (a,T);
 
+fun vars_tr (Const ("_idts", _) $ idt $ vars) = var_tr idt :: vars_tr vars
+  | vars_tr t = [var_tr t]
+
+in
 fun hoare_vars_tr [vars, pre, prg, post] =
       let val xs = vars_tr vars
       in Syntax.const "Valid" $
-           assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
+         assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
       end
   | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts);
+end
 *}
 
 parse_translation {* [("@hoare_vars", hoare_vars_tr)] *}
diff -r f94b569cd610 -r 3e180bf68496 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sun Dec 22 10:43:43 2002 +0100
+++ b/src/HOL/Set.thy	Sun Dec 22 15:02:40 2002 +0100
@@ -74,15 +74,15 @@
   "x ~: y"      == "~ (x : y)"
   "{x, xs}"     == "insert x {xs}"
   "{x}"         == "insert x {}"
-  "{x. P}"      => "Collect (%x. P)"
+  "{x. P}"      == "Collect (%x. P)"
   "UN x y. B"   == "UN x. UN y. B"
   "UN x. B"     == "UNION UNIV (%x. B)"
   "INT x y. B"  == "INT x. INT y. B"
   "INT x. B"    == "INTER UNIV (%x. B)"
-  "UN x:A. B"   => "UNION A (%x. B)"
-  "INT x:A. B"  => "INTER A (%x. B)"
-  "ALL x:A. P"  => "Ball A (%x. P)"
-  "EX x:A. P"   => "Bex A (%x. P)"
+  "UN x:A. B"   == "UNION A (%x. B)"
+  "INT x:A. B"  == "INTER A (%x. B)"
+  "ALL x:A. P"  == "Ball A (%x. P)"
+  "EX x:A. P"   == "Bex A (%x. P)"
 
 syntax (output)
   "_setle"      :: "'a set => 'a set => bool"             ("op <=")
@@ -172,6 +172,7 @@
         | check (Const ("op &", _) $ (Const ("op =", _) $ Bound m $ e) $ P, n) =
             n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
             ((0 upto (n - 1)) subset add_loose_bnos (e, 0, []))
+        | check _ = false
 
         fun tr' (_ $ abs) =
           let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr' [abs]