removed some problems with print translations
authornipkow
Sun Dec 22 15:02:40 2002 +0100 (2002-12-22)
changeset 137643e180bf68496
parent 13763 f94b569cd610
child 13765 e3c444e805c4
removed some problems with print translations
src/HOL/HOL.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Hoare/Hoare.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/HOL.thy	Sun Dec 22 10:43:43 2002 +0100
     1.2 +++ b/src/HOL/HOL.thy	Sun Dec 22 15:02:40 2002 +0100
     1.3 @@ -71,7 +71,7 @@
     1.4  
     1.5  translations
     1.6    "x ~= y"                == "~ (x = y)"
     1.7 -  "THE x. P"              => "The (%x. P)"
     1.8 +  "THE x. P"              == "The (%x. P)"
     1.9    "_Let (_binds b bs) e"  == "_Let b (_Let bs e)"
    1.10    "let x = a in e"        == "Let a (%x. e)"
    1.11  
     2.1 --- a/src/HOL/Hilbert_Choice.thy	Sun Dec 22 10:43:43 2002 +0100
     2.2 +++ b/src/HOL/Hilbert_Choice.thy	Sun Dec 22 15:02:40 2002 +0100
     2.3 @@ -22,7 +22,7 @@
     2.4  syntax
     2.5    "_Eps"        :: "[pttrn, bool] => 'a"    ("(3SOME _./ _)" [0, 10] 10)
     2.6  translations
     2.7 -  "SOME x. P" => "Eps (%x. P)"
     2.8 +  "SOME x. P" == "Eps (%x. P)"
     2.9  
    2.10  print_translation {*
    2.11  (* to avoid eta-contraction of body *)
     3.1 --- a/src/HOL/Hoare/Hoare.thy	Sun Dec 22 10:43:43 2002 +0100
     3.2 +++ b/src/HOL/Hoare/Hoare.thy	Sun Dec 22 15:02:40 2002 +0100
     3.3 @@ -48,15 +48,8 @@
     3.4    "Valid p c q == !s s'. Sem c s s' --> s : p --> s' : q"
     3.5  
     3.6  
     3.7 -nonterminals
     3.8 -  vars
     3.9 -
    3.10  syntax
    3.11 -  ""		     :: "id => vars"		       ("_")
    3.12 -  "_vars" 	     :: "[id, vars] => vars"	       ("_ _")
    3.13 -
    3.14 -syntax
    3.15 - "@hoare_vars" :: "[vars, 'a assn,'a com,'a assn] => bool"
    3.16 + "@hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
    3.17                   ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
    3.18  syntax ("" output)
    3.19   "@hoare"      :: "['a assn,'a com,'a assn] => bool"
    3.20 @@ -65,18 +58,24 @@
    3.21  (** parse translations **)
    3.22  
    3.23  ML{*
    3.24 -fun mk_abstuple []     body = absfree ("x", dummyT, body)
    3.25 -  | mk_abstuple [v]    body = absfree ((fst o dest_Free) v, dummyT, body)
    3.26 -  | mk_abstuple (v::w) body = Syntax.const "split" $
    3.27 -                              absfree ((fst o dest_Free) v, dummyT, mk_abstuple w body);
    3.28 +
    3.29 +local
    3.30 +fun free a = Free(a,dummyT)
    3.31 +fun abs((a,T),body) =
    3.32 +  let val a = absfree(a, dummyT, body)
    3.33 +  in if T = Bound 0 then a else Const(Syntax.constrainAbsC,dummyT) $ a $ T end
    3.34 +in
    3.35  
    3.36 -  
    3.37 -fun mk_fbody v e []      = Syntax.const "Unity"
    3.38 -  | mk_fbody v e [x]     = if v=x then e else x
    3.39 -  | mk_fbody v e (x::xs) = Syntax.const "Pair" $ (if v=x then e else x) $
    3.40 -                           mk_fbody v e xs;
    3.41 +fun mk_abstuple [x] body = abs (x, body)
    3.42 +  | mk_abstuple (x::xs) body =
    3.43 +      Syntax.const "split" $ abs (x, mk_abstuple xs body);
    3.44  
    3.45 -fun mk_fexp v e xs = mk_abstuple xs (mk_fbody v e xs);
    3.46 +fun mk_fbody a e [x as (b,_)] = if a=b then e else free b
    3.47 +  | mk_fbody a e ((b,_)::xs) =
    3.48 +      Syntax.const "Pair" $ (if a=b then e else free b) $ mk_fbody a e xs;
    3.49 +
    3.50 +fun mk_fexp a e xs = mk_abstuple xs (mk_fbody a e xs)
    3.51 +end
    3.52  *}
    3.53  
    3.54  (* bexp_tr & assn_tr *)
    3.55 @@ -88,37 +87,38 @@
    3.56    
    3.57  fun assn_tr r xs = Syntax.const "Collect" $ mk_abstuple xs r;
    3.58  *}
    3.59 -
    3.60  (* com_tr *)
    3.61  ML{*
    3.62 -fun assign_tr [Free (V,_),E] xs = Syntax.const "Basic" $
    3.63 -                                      mk_fexp (Free(V,dummyT)) E xs
    3.64 -  | assign_tr ts _ = raise TERM ("assign_tr", ts);
    3.65 -
    3.66 -fun com_tr (Const("@assign",_) $ Free (V,_) $ E) xs =
    3.67 -               assign_tr [Free (V,dummyT),E] xs
    3.68 +fun com_tr (Const("@assign",_) $ Free (a,_) $ e) xs =
    3.69 +      Syntax.const "Basic" $ mk_fexp a e xs
    3.70    | com_tr (Const ("Basic",_) $ f) xs = Syntax.const "Basic" $ f
    3.71 -  | com_tr (Const ("Seq",_) $ c1 $ c2) xs = Syntax.const "Seq" $
    3.72 -                                                 com_tr c1 xs $ com_tr c2 xs
    3.73 -  | com_tr (Const ("Cond",_) $ b $ c1 $ c2) xs = Syntax.const "Cond" $
    3.74 -                                  bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
    3.75 -  | com_tr (Const ("While",_) $ b $ I $ c) xs = Syntax.const "While" $
    3.76 -                                         bexp_tr b xs $ assn_tr I xs $ com_tr c xs
    3.77 -  | com_tr trm _ = trm;
    3.78 +  | com_tr (Const ("Seq",_) $ c1 $ c2) xs =
    3.79 +      Syntax.const "Seq" $ com_tr c1 xs $ com_tr c2 xs
    3.80 +  | com_tr (Const ("Cond",_) $ b $ c1 $ c2) xs =
    3.81 +      Syntax.const "Cond" $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
    3.82 +  | com_tr (Const ("While",_) $ b $ I $ c) xs =
    3.83 +      Syntax.const "While" $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs
    3.84 +  | com_tr t _ = t (* if t is just a Free/Var *)
    3.85  *}
    3.86  
    3.87  (* triple_tr *)
    3.88  ML{*
    3.89 -fun vars_tr (x as Free _) = [x]
    3.90 -  | vars_tr (Const ("_vars", _) $ (x as Free _) $ vars) = x :: vars_tr vars
    3.91 -  | vars_tr t = raise TERM ("vars_tr", [t]);
    3.92 +local
    3.93 +
    3.94 +fun var_tr(Free(a,_)) = (a,Bound 0) (* Bound 0 = dummy term *)
    3.95 +  | var_tr(Const ("_constrain", _) $ (Free (a,_)) $ T) = (a,T);
    3.96  
    3.97 +fun vars_tr (Const ("_idts", _) $ idt $ vars) = var_tr idt :: vars_tr vars
    3.98 +  | vars_tr t = [var_tr t]
    3.99 +
   3.100 +in
   3.101  fun hoare_vars_tr [vars, pre, prg, post] =
   3.102        let val xs = vars_tr vars
   3.103        in Syntax.const "Valid" $
   3.104 -           assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
   3.105 +         assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
   3.106        end
   3.107    | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts);
   3.108 +end
   3.109  *}
   3.110  
   3.111  parse_translation {* [("@hoare_vars", hoare_vars_tr)] *}
     4.1 --- a/src/HOL/Set.thy	Sun Dec 22 10:43:43 2002 +0100
     4.2 +++ b/src/HOL/Set.thy	Sun Dec 22 15:02:40 2002 +0100
     4.3 @@ -74,15 +74,15 @@
     4.4    "x ~: y"      == "~ (x : y)"
     4.5    "{x, xs}"     == "insert x {xs}"
     4.6    "{x}"         == "insert x {}"
     4.7 -  "{x. P}"      => "Collect (%x. P)"
     4.8 +  "{x. P}"      == "Collect (%x. P)"
     4.9    "UN x y. B"   == "UN x. UN y. B"
    4.10    "UN x. B"     == "UNION UNIV (%x. B)"
    4.11    "INT x y. B"  == "INT x. INT y. B"
    4.12    "INT x. B"    == "INTER UNIV (%x. B)"
    4.13 -  "UN x:A. B"   => "UNION A (%x. B)"
    4.14 -  "INT x:A. B"  => "INTER A (%x. B)"
    4.15 -  "ALL x:A. P"  => "Ball A (%x. P)"
    4.16 -  "EX x:A. P"   => "Bex A (%x. P)"
    4.17 +  "UN x:A. B"   == "UNION A (%x. B)"
    4.18 +  "INT x:A. B"  == "INTER A (%x. B)"
    4.19 +  "ALL x:A. P"  == "Ball A (%x. P)"
    4.20 +  "EX x:A. P"   == "Bex A (%x. P)"
    4.21  
    4.22  syntax (output)
    4.23    "_setle"      :: "'a set => 'a set => bool"             ("op <=")
    4.24 @@ -172,6 +172,7 @@
    4.25          | check (Const ("op &", _) $ (Const ("op =", _) $ Bound m $ e) $ P, n) =
    4.26              n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
    4.27              ((0 upto (n - 1)) subset add_loose_bnos (e, 0, []))
    4.28 +        | check _ = false
    4.29  
    4.30          fun tr' (_ $ abs) =
    4.31            let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr' [abs]