fixed numerals;
authorwenzelm
Mon Oct 08 14:29:02 2001 +0200 (2001-10-08)
changeset 11711ecdfd237ffee
parent 11710 f5401162c9f0
child 11712 deb8cac87063
fixed numerals;
doc-src/TutorialI/Inductive/Advanced.thy
doc-src/TutorialI/Misc/natsum.thy
doc-src/TutorialI/Rules/Forward.thy
doc-src/TutorialI/Rules/Tacticals.thy
doc-src/TutorialI/Types/Numbers.thy
doc-src/TutorialI/Types/Records.thy
     1.1 --- a/doc-src/TutorialI/Inductive/Advanced.thy	Mon Oct 08 14:19:42 2001 +0200
     1.2 +++ b/doc-src/TutorialI/Inductive/Advanced.thy	Mon Oct 08 14:29:02 2001 +0200
     1.3 @@ -78,9 +78,9 @@
     1.4  
     1.5  consts integer_arity :: "integer_op \<Rightarrow> nat"
     1.6  primrec
     1.7 -"integer_arity (Number n)        = #0"
     1.8 -"integer_arity UnaryMinus        = #1"
     1.9 -"integer_arity Plus              = #2"
    1.10 +"integer_arity (Number n)        = 0"
    1.11 +"integer_arity UnaryMinus        = 1"
    1.12 +"integer_arity Plus              = 2"
    1.13  
    1.14  consts well_formed_gterm :: "('f \<Rightarrow> nat) \<Rightarrow> 'f gterm set"
    1.15  inductive "well_formed_gterm arity"
     2.1 --- a/doc-src/TutorialI/Misc/natsum.thy	Mon Oct 08 14:19:42 2001 +0200
     2.2 +++ b/doc-src/TutorialI/Misc/natsum.thy	Mon Oct 08 14:29:02 2001 +0200
     2.3 @@ -66,7 +66,7 @@
     2.4  simple arithmetic goals automatically:
     2.5  *}
     2.6  
     2.7 -lemma "\<lbrakk> \<not> m < n; m < n+1 \<rbrakk> \<Longrightarrow> m = n"
     2.8 +lemma "\<lbrakk> \<not> m < n; m < n + (1::nat) \<rbrakk> \<Longrightarrow> m = n"
     2.9  (*<*)by(auto)(*>*)
    2.10  
    2.11  text{*\noindent
    2.12 @@ -75,7 +75,7 @@
    2.13  In consequence, @{text auto} cannot prove this slightly more complex goal:
    2.14  *}
    2.15  
    2.16 -lemma "\<not> m < n \<and> m < n+1 \<Longrightarrow> m = n";
    2.17 +lemma "\<not> m < n \<and> m < n + (1::nat) \<Longrightarrow> m = n";
    2.18  (*<*)by(arith)(*>*)
    2.19  
    2.20  text{*\noindent
     3.1 --- a/doc-src/TutorialI/Rules/Forward.thy	Mon Oct 08 14:19:42 2001 +0200
     3.2 +++ b/doc-src/TutorialI/Rules/Forward.thy	Mon Oct 08 14:29:02 2001 +0200
     3.3 @@ -21,12 +21,12 @@
     3.4  apply (simp add: is_gcd)
     3.5  done
     3.6  
     3.7 -lemma gcd_1 [simp]: "gcd(m,1') = 1'"
     3.8 +lemma gcd_1 [simp]: "gcd(m, Suc 0) = Suc 0"
     3.9  apply simp
    3.10  done
    3.11  
    3.12 -lemma gcd_1_left [simp]: "gcd(1',m) = 1'"
    3.13 -apply (simp add: gcd_commute [of "1'"])
    3.14 +lemma gcd_1_left [simp]: "gcd(Suc 0, m) = Suc 0"
    3.15 +apply (simp add: gcd_commute [of "Suc 0"])
    3.16  done
    3.17  
    3.18  text{*\noindent
    3.19 @@ -125,7 +125,7 @@
    3.20  \rulename{arg_cong}
    3.21  *}
    3.22  
    3.23 -lemma "#2 \<le> u \<Longrightarrow> u*m \<noteq> Suc(u*n)"
    3.24 +lemma "2 \<le> u \<Longrightarrow> u*m \<noteq> Suc(u*n)"
    3.25  apply intro
    3.26  txt{*
    3.27  before using arg_cong
    3.28 @@ -177,7 +177,7 @@
    3.29  by (blast intro: relprime_dvd_mult dvd_trans)
    3.30  
    3.31  
    3.32 -lemma relprime_20_81: "gcd(#20,#81) = 1";
    3.33 +lemma relprime_20_81: "gcd(20,81) = 1";
    3.34  by (simp add: gcd.simps)
    3.35  
    3.36  text {*
    3.37 @@ -199,14 +199,14 @@
    3.38  @{thm[display] dvd_add [OF _ dvd_refl]}
    3.39  *};
    3.40  
    3.41 -lemma "\<lbrakk>(z::int) < #37; #66 < #2*z; z*z \<noteq> #1225; Q(#34); Q(#36)\<rbrakk> \<Longrightarrow> Q(z)";
    3.42 -apply (subgoal_tac "z = #34 \<or> z = #36")
    3.43 +lemma "\<lbrakk>(z::int) < 37; 66 < 2*z; z*z \<noteq> 1225; Q(34); Q(36)\<rbrakk> \<Longrightarrow> Q(z)";
    3.44 +apply (subgoal_tac "z = 34 \<or> z = 36")
    3.45  txt{*
    3.46  the tactic leaves two subgoals:
    3.47  @{subgoals[display,indent=0,margin=65]}
    3.48  *};
    3.49  apply blast
    3.50 -apply (subgoal_tac "z \<noteq> #35")
    3.51 +apply (subgoal_tac "z \<noteq> 35")
    3.52  txt{*
    3.53  the tactic leaves two subgoals:
    3.54  @{subgoals[display,indent=0,margin=65]}
     4.1 --- a/doc-src/TutorialI/Rules/Tacticals.thy	Mon Oct 08 14:19:42 2001 +0200
     4.2 +++ b/doc-src/TutorialI/Rules/Tacticals.thy	Mon Oct 08 14:29:02 2001 +0200
     4.3 @@ -12,7 +12,7 @@
     4.4  by (drule mp, assumption)+
     4.5  
     4.6  text{*ORELSE with REPEAT*}
     4.7 -lemma "\<lbrakk>Q\<longrightarrow>R; P\<longrightarrow>Q; x<#5\<longrightarrow>P;  Suc x < #5\<rbrakk> \<Longrightarrow> R" 
     4.8 +lemma "\<lbrakk>Q\<longrightarrow>R; P\<longrightarrow>Q; x<5\<longrightarrow>P;  Suc x < 5\<rbrakk> \<Longrightarrow> R" 
     4.9  by (drule mp, (assumption|arith))+
    4.10  
    4.11  text{*exercise: what's going on here?*}
     5.1 --- a/doc-src/TutorialI/Types/Numbers.thy	Mon Oct 08 14:19:42 2001 +0200
     5.2 +++ b/doc-src/TutorialI/Types/Numbers.thy	Mon Oct 08 14:29:02 2001 +0200
     5.3 @@ -9,7 +9,7 @@
     5.4  numeric literals; default simprules; can re-orient
     5.5  *}
     5.6  
     5.7 -lemma "#2 * m = m + m"
     5.8 +lemma "2 * m = m + m"
     5.9  txt{*
    5.10  @{subgoals[display,indent=0,margin=65]}
    5.11  *};
    5.12 @@ -17,10 +17,10 @@
    5.13  
    5.14  consts h :: "nat \<Rightarrow> nat"
    5.15  recdef h "{}"
    5.16 -"h i = (if i = #3 then #2 else i)"
    5.17 +"h i = (if i = 3 then 2 else i)"
    5.18  
    5.19  text{*
    5.20 -@{term"h #3 = #2"}
    5.21 +@{term"h 3 = 2"}
    5.22  @{term"h i  = i"}
    5.23  *}
    5.24  
    5.25 @@ -83,7 +83,7 @@
    5.26  *}
    5.27  
    5.28  
    5.29 -lemma "(n-#2)*(n+#2) = n*n - (#4::nat)"
    5.30 +lemma "(n - 2) * (n + 2) = n * n - (4::nat)"
    5.31  apply (clarsimp split: nat_diff_split)
    5.32   --{* @{subgoals[display,indent=0,margin=65]} *}
    5.33  apply (subgoal_tac "n=0 | n=1", force, arith)
    5.34 @@ -167,7 +167,7 @@
    5.35  lemma "abs (x+y) \<le> abs x + abs (y :: int)"
    5.36  by arith
    5.37  
    5.38 -lemma "abs (#2*x) = #2 * abs (x :: int)"
    5.39 +lemma "abs (2*x) = 2 * abs (x :: int)"
    5.40  by (simp add: zabs_def) 
    5.41  
    5.42  text {*REALS
    5.43 @@ -205,10 +205,10 @@
    5.44  \rulename{real_add_divide_distrib}
    5.45  *}
    5.46  
    5.47 -lemma "#3/#4 < (#7/#8 :: real)"
    5.48 +lemma "3/4 < (7/8 :: real)"
    5.49  by simp 
    5.50  
    5.51 -lemma "P ((#3/#4) * (#8/#15 :: real))"
    5.52 +lemma "P ((3/4) * (8/15 :: real))"
    5.53  txt{*
    5.54  @{subgoals[display,indent=0,margin=65]}
    5.55  *};
    5.56 @@ -218,7 +218,7 @@
    5.57  *};
    5.58  oops
    5.59  
    5.60 -lemma "(#3/#4) * (#8/#15) < (x :: real)"
    5.61 +lemma "(3/4) * (8/15) < (x :: real)"
    5.62  txt{*
    5.63  @{subgoals[display,indent=0,margin=65]}
    5.64  *};
    5.65 @@ -228,7 +228,7 @@
    5.66  *};
    5.67  oops
    5.68  
    5.69 -lemma "(#3/#4) * (#10^#15) < (x :: real)"
    5.70 +lemma "(3/4) * (10^15) < (x :: real)"
    5.71  apply simp 
    5.72  oops
    5.73  
     6.1 --- a/doc-src/TutorialI/Types/Records.thy	Mon Oct 08 14:19:42 2001 +0200
     6.2 +++ b/doc-src/TutorialI/Types/Records.thy	Mon Oct 08 14:29:02 2001 +0200
     6.3 @@ -52,10 +52,10 @@
     6.4  
     6.5  constdefs 
     6.6    pt1 :: point
     6.7 -   "pt1 == (| Xcoord = #999, Ycoord = #23 |)"
     6.8 +   "pt1 == (| Xcoord = 999, Ycoord = 23 |)"
     6.9  
    6.10    pt2 :: "(| Xcoord :: int, Ycoord :: int |)" 
    6.11 -   "pt2 == (| Xcoord = #-45, Ycoord = #97 |)" 
    6.12 +   "pt2 == (| Xcoord = -45, Ycoord = 97 |)" 
    6.13  
    6.14  
    6.15  subsubsection {* Some lemmas about records *}
    6.16 @@ -89,7 +89,7 @@
    6.17  
    6.18  constdefs 
    6.19    cpt1 :: cpoint
    6.20 -   "cpt1 == (| Xcoord = #999, Ycoord = #23, col = Green |)"
    6.21 +   "cpt1 == (| Xcoord = 999, Ycoord = 23, col = Green |)"
    6.22  
    6.23  
    6.24  subsection {* Generic operations *}
    6.25 @@ -121,7 +121,7 @@
    6.26    setX :: "[('a::more) point_scheme, int] \<Rightarrow> 'a point_scheme"
    6.27     "setX r a == r (| Xcoord := a |)"
    6.28    extendpt :: "'a \<Rightarrow> ('a::more) point_scheme"
    6.29 -   "extendpt ext == (| Xcoord = #15, Ycoord = 0, ... = ext |)"
    6.30 +   "extendpt ext == (| Xcoord = 15, Ycoord = 0, ... = ext |)"
    6.31       text{*not sure what this is for!*}
    6.32  
    6.33  
    6.34 @@ -129,7 +129,7 @@
    6.35   \medskip Concrete records are type instances of record schemes.
    6.36  *}
    6.37  
    6.38 -lemma "getX (| Xcoord = #64, Ycoord = #36 |) = #64"
    6.39 +lemma "getX (| Xcoord = 64, Ycoord = 36 |) = 64"
    6.40  by (simp add: getX_def) 
    6.41  
    6.42  
    6.43 @@ -138,7 +138,7 @@
    6.44  
    6.45  constdefs
    6.46    incX :: "('a::more) point_scheme \<Rightarrow> 'a point_scheme"
    6.47 -  "incX r == \<lparr>Xcoord = (Xcoord r) + #1, Ycoord = Ycoord r, \<dots> = point.more r\<rparr>"
    6.48 +  "incX r == \<lparr>Xcoord = (Xcoord r) + 1, Ycoord = Ycoord r, \<dots> = point.more r\<rparr>"
    6.49  
    6.50  constdefs
    6.51    setGreen :: "[colour, ('a::more) point_scheme] \<Rightarrow> cpoint"
    6.52 @@ -147,11 +147,11 @@
    6.53  
    6.54  text {* works (I think) for ALL extensions of type point? *}
    6.55  
    6.56 -lemma "incX r = setX r ((getX r) + #1)"
    6.57 +lemma "incX r = setX r ((getX r) + 1)"
    6.58  by (simp add: getX_def setX_def incX_def)
    6.59  
    6.60  text {* An equivalent definition. *}
    6.61 -lemma "incX r = r \<lparr>Xcoord := (Xcoord r) + #1\<rparr>"
    6.62 +lemma "incX r = r \<lparr>Xcoord := (Xcoord r) + 1\<rparr>"
    6.63  by (simp add: incX_def)
    6.64  
    6.65  
    6.66 @@ -160,7 +160,7 @@
    6.67   Functions on @{text point} schemes work for type @{text cpoint} as
    6.68   well.  *}
    6.69  
    6.70 -lemma "getX \<lparr>Xcoord = #23, Ycoord = #10, col = Blue\<rparr> = #23"
    6.71 +lemma "getX \<lparr>Xcoord = 23, Ycoord = 10, col = Blue\<rparr> = 23"
    6.72  by (simp add: getX_def)
    6.73  
    6.74  
    6.75 @@ -170,8 +170,8 @@
    6.76   Function @{term setX} can be applied to type @{typ cpoint}, not just type
    6.77   @{typ point}, and returns a result of the same type!  *}
    6.78  
    6.79 -lemma "setX \<lparr>Xcoord = #12, Ycoord = 0, col = Blue\<rparr> #23 =  
    6.80 -            \<lparr>Xcoord = #23, Ycoord = 0, col = Blue\<rparr>"
    6.81 +lemma "setX \<lparr>Xcoord = 12, Ycoord = 0, col = Blue\<rparr> 23 =  
    6.82 +            \<lparr>Xcoord = 23, Ycoord = 0, col = Blue\<rparr>"
    6.83  by (simp add: setX_def)
    6.84  
    6.85