fixed translations: CONST;
authorwenzelm
Thu Sep 28 23:42:43 2006 +0200 (2006-09-28)
changeset 207702c583720436e
parent 20769 5d538d3d5e2a
child 20771 89bec28a03c8
fixed translations: CONST;
src/HOL/Hoare/HoareAbort.thy
src/HOL/Hyperreal/Series.thy
src/HOL/Induct/LList.thy
src/HOL/Induct/SList.thy
src/HOL/Library/Coinductive_List.thy
src/HOL/Library/FuncSet.thy
src/HOL/Library/Multiset.thy
src/HOLCF/Porder.thy
     1.1 --- a/src/HOL/Hoare/HoareAbort.thy	Thu Sep 28 23:42:39 2006 +0200
     1.2 +++ b/src/HOL/Hoare/HoareAbort.thy	Thu Sep 28 23:42:43 2006 +0200
     1.3 @@ -255,7 +255,7 @@
     1.4    array_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com"  ("(2_[_] :=/ _)" [70,65] 61)
     1.5  translations
     1.6    "P \<rightarrow> c" == "IF P THEN c ELSE Abort FI"
     1.7 -  "a[i] := v" => "(i < length a) \<rightarrow> (a := list_update a i v)"
     1.8 +  "a[i] := v" => "(i < CONST length a) \<rightarrow> (a := list_update a i v)"
     1.9    (* reverse translation not possible because of duplicate "a" *)
    1.10  
    1.11  text{* Note: there is no special syntax for guarded array access. Thus
     2.1 --- a/src/HOL/Hyperreal/Series.thy	Thu Sep 28 23:42:39 2006 +0200
     2.2 +++ b/src/HOL/Hyperreal/Series.thy	Thu Sep 28 23:42:43 2006 +0200
     2.3 @@ -27,7 +27,7 @@
     2.4  syntax
     2.5    "_suminf" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a" ("\<Sum>_. _" [0, 10] 10)
     2.6  translations
     2.7 -  "\<Sum>i. b" == "suminf (%i. b)"
     2.8 +  "\<Sum>i. b" == "CONST suminf (%i. b)"
     2.9  
    2.10  
    2.11  lemma sumr_diff_mult_const:
     3.1 --- a/src/HOL/Induct/LList.thy	Thu Sep 28 23:42:39 2006 +0200
     3.2 +++ b/src/HOL/Induct/LList.thy	Thu Sep 28 23:42:43 2006 +0200
     3.3 @@ -95,8 +95,11 @@
     3.4  
     3.5  
     3.6  text{* The case syntax for type @{text "'a llist"} *}
     3.7 +syntax  (* FIXME proper case syntax!? *)
     3.8 +  LNil :: logic
     3.9 +  LCons :: logic
    3.10  translations
    3.11 -  "case p of LNil => a | LCons x l => b" == "llist_case a (%x l. b) p"
    3.12 +  "case p of LNil => a | LCons x l => b" == "CONST llist_case a (%x l. b) p"
    3.13  
    3.14  
    3.15  subsubsection{* Sample function definitions.  Item-based ones start with @{text L} *}
     4.1 --- a/src/HOL/Induct/SList.thy	Thu Sep 28 23:42:39 2006 +0200
     4.2 +++ b/src/HOL/Induct/SList.thy	Thu Sep 28 23:42:43 2006 +0200
     4.3 @@ -73,7 +73,7 @@
     4.4  (*Declaring the abstract list constructors*)
     4.5  
     4.6  definition
     4.7 -  Nil       :: "'a list"
     4.8 +  Nil       :: "'a list"                               ("[]")
     4.9     "Nil  = Abs_List(NIL)"
    4.10  
    4.11    "Cons"       :: "['a, 'a list] => 'a list"           (infixr "#" 65)
    4.12 @@ -88,19 +88,16 @@
    4.13     "list_case a f xs = list_rec xs a (%x xs r. f x xs)"
    4.14  
    4.15  (* list Enumeration *)
    4.16 -consts
    4.17 -  "[]"      :: "'a list"                            ("[]")
    4.18  syntax
    4.19    "@list"   :: "args => 'a list"                    ("[(_)]")
    4.20  
    4.21  translations
    4.22    "[x, xs]" == "x#[xs]"
    4.23    "[x]"     == "x#[]"
    4.24 -  "[]"      == "Nil"
    4.25  
    4.26 -  "case xs of Nil => a | y#ys => b" == "list_case(a, %y ys. b, xs)"
    4.27 +  "case xs of [] => a | y#ys => b" == "CONST list_case(a, %y ys. b, xs)"
    4.28  
    4.29 -  
    4.30 +
    4.31  (* *********************************************************************** *)
    4.32  (*                                                                         *)
    4.33  (* Generalized Map Functionals                                             *)
    4.34 @@ -205,8 +202,8 @@
    4.35    "@filter"     :: "[idt, 'a list, bool] => 'a list"     ("(1[_:_ ./ _])")
    4.36  
    4.37  translations
    4.38 -  "[x:xs. P]"   == "filter(%x. P) xs"
    4.39 -  "Alls x:xs. P"== "list_all(%x. P)xs"
    4.40 +  "[x:xs. P]" == "CONST filter(%x. P) xs"
    4.41 +  "Alls x:xs. P" == "CONST list_all(%x. P)xs"
    4.42  
    4.43  
    4.44  lemma ListI: "x : list (range Leaf) ==> x : List"
     5.1 --- a/src/HOL/Library/Coinductive_List.thy	Thu Sep 28 23:42:39 2006 +0200
     5.2 +++ b/src/HOL/Library/Coinductive_List.thy	Thu Sep 28 23:42:43 2006 +0200
     5.3 @@ -196,8 +196,12 @@
     5.4  definition
     5.5    "llist_case c d l =
     5.6      List_case c (\<lambda>x y. d (inv Datatype_Universe.Leaf x) (Abs_llist y)) (Rep_llist l)"
     5.7 +
     5.8 +syntax  (* FIXME? *)
     5.9 +  LNil :: logic
    5.10 +  LCons :: logic
    5.11  translations
    5.12 -  "case p of LNil \<Rightarrow> a | LCons x l \<Rightarrow> b" \<rightleftharpoons> "llist_case a (\<lambda>x l. b) p"
    5.13 +  "case p of LNil \<Rightarrow> a | LCons x l \<Rightarrow> b" \<rightleftharpoons> "CONST llist_case a (\<lambda>x l. b) p"
    5.14  
    5.15  lemma llist_case_LNil [simp]: "llist_case c d LNil = c"
    5.16    by (simp add: llist_case_def LNil_def
     6.1 --- a/src/HOL/Library/FuncSet.thy	Thu Sep 28 23:42:39 2006 +0200
     6.2 +++ b/src/HOL/Library/FuncSet.thy	Thu Sep 28 23:42:43 2006 +0200
     6.3 @@ -39,8 +39,8 @@
     6.4    "_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
     6.5  
     6.6  translations
     6.7 -  "PI x:A. B" == "Pi A (%x. B)"
     6.8 -  "%x:A. f" == "restrict (%x. f) A"
     6.9 +  "PI x:A. B" == "CONST Pi A (%x. B)"
    6.10 +  "%x:A. f" == "CONST restrict (%x. f) A"
    6.11  
    6.12  definition
    6.13    "compose" :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
     7.1 --- a/src/HOL/Library/Multiset.thy	Thu Sep 28 23:42:39 2006 +0200
     7.2 +++ b/src/HOL/Library/Multiset.thy	Thu Sep 28 23:42:43 2006 +0200
     7.3 @@ -40,7 +40,7 @@
     7.4  syntax
     7.5    "_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset"    ("(1{# _ : _./ _#})")
     7.6  translations
     7.7 -  "{#x:M. P#}" == "MCollect M (\<lambda>x. P)"
     7.8 +  "{#x:M. P#}" == "CONST MCollect M (\<lambda>x. P)"
     7.9  
    7.10  definition
    7.11    set_of :: "'a multiset => 'a set"
     8.1 --- a/src/HOLCF/Porder.thy	Thu Sep 28 23:42:39 2006 +0200
     8.2 +++ b/src/HOLCF/Porder.thy	Thu Sep 28 23:42:43 2006 +0200
     8.3 @@ -94,7 +94,7 @@
     8.4    "LUB "	:: "[idts, 'a] \<Rightarrow> 'a"		("(3\<Squnion>_./ _)" [0,10] 10)
     8.5  
     8.6  translations
     8.7 -  "\<Squnion>n. t" == "lub(range(\<lambda>n. t))"
     8.8 +  "\<Squnion>n. t" == "lub(CONST range(\<lambda>n. t))"
     8.9  
    8.10  text {* lubs are unique *}
    8.11