src/HOL/Library/Abstract_Rat.thy
changeset 50282 fe4d4bb9f4c2
parent 47162 9d7d919b9fd8
     1.1 --- a/src/HOL/Library/Abstract_Rat.thy	Thu Nov 29 10:56:59 2012 +0100
     1.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Thu Nov 29 14:05:53 2012 +0100
     1.3 @@ -13,8 +13,8 @@
     1.4  abbreviation Num0_syn :: Num  ("0\<^sub>N")
     1.5    where "0\<^sub>N \<equiv> (0, 0)"
     1.6  
     1.7 -abbreviation Numi_syn :: "int \<Rightarrow> Num"  ("_\<^sub>N")
     1.8 -  where "i\<^sub>N \<equiv> (i, 1)"
     1.9 +abbreviation Numi_syn :: "int \<Rightarrow> Num"  ("'((_)')\<^sub>N")
    1.10 +  where "(i)\<^sub>N \<equiv> (i, 1)"
    1.11  
    1.12  definition isnormNum :: "Num \<Rightarrow> bool" where
    1.13    "isnormNum = (\<lambda>(a,b). (if a = 0 then b = 0 else b > 0 \<and> gcd a b = 1))"
    1.14 @@ -125,7 +125,7 @@
    1.15      (cases "fst x = 0", auto simp add: gcd_commute_int)
    1.16  
    1.17  lemma isnormNum_int[simp]:
    1.18 -  "isnormNum 0\<^sub>N" "isnormNum ((1::int)\<^sub>N)" "i \<noteq> 0 \<Longrightarrow> isnormNum (i\<^sub>N)"
    1.19 +  "isnormNum 0\<^sub>N" "isnormNum ((1::int)\<^sub>N)" "i \<noteq> 0 \<Longrightarrow> isnormNum (i)\<^sub>N"
    1.20    by (simp_all add: isnormNum_def)
    1.21  
    1.22  
    1.23 @@ -151,7 +151,7 @@
    1.24  
    1.25  definition "INum = (\<lambda>(a,b). of_int a / of_int b)"
    1.26  
    1.27 -lemma INum_int [simp]: "INum (i\<^sub>N) = ((of_int i) ::'a::field)" "INum 0\<^sub>N = (0::'a::field)"
    1.28 +lemma INum_int [simp]: "INum (i)\<^sub>N = ((of_int i) ::'a::field)" "INum 0\<^sub>N = (0::'a::field)"
    1.29    by (simp_all add: INum_def)
    1.30  
    1.31  lemma isnormNum_unique[simp]:
    1.32 @@ -512,8 +512,8 @@
    1.33    by (simp add: Nneg_def split_def)
    1.34  
    1.35  lemma Nmul1[simp]:
    1.36 -    "isnormNum c \<Longrightarrow> 1\<^sub>N *\<^sub>N c = c"
    1.37 -    "isnormNum c \<Longrightarrow> c *\<^sub>N (1\<^sub>N) = c"
    1.38 +    "isnormNum c \<Longrightarrow> (1)\<^sub>N *\<^sub>N c = c"
    1.39 +    "isnormNum c \<Longrightarrow> c *\<^sub>N (1)\<^sub>N = c"
    1.40    apply (simp_all add: Nmul_def Let_def split_def isnormNum_def)
    1.41    apply (cases "fst c = 0", simp_all, cases c, simp_all)+
    1.42    done