src/Doc/Tutorial/Recdef/simplification.thy
changeset 58860 fee7cfa69c50
parent 48985 5386df44a037
child 62392 747d36865c2c
     1.1 --- a/src/Doc/Tutorial/Recdef/simplification.thy	Sat Nov 01 11:40:55 2014 +0100
     1.2 +++ b/src/Doc/Tutorial/Recdef/simplification.thy	Sat Nov 01 14:20:38 2014 +0100
     1.3 @@ -1,5 +1,5 @@
     1.4  (*<*)
     1.5 -theory simplification imports Main begin;
     1.6 +theory simplification imports Main begin
     1.7  (*>*)
     1.8  
     1.9  text{*
    1.10 @@ -12,9 +12,9 @@
    1.11  Let us look at an example:
    1.12  *}
    1.13  
    1.14 -consts gcd :: "nat\<times>nat \<Rightarrow> nat";
    1.15 +consts gcd :: "nat\<times>nat \<Rightarrow> nat"
    1.16  recdef gcd "measure (\<lambda>(m,n).n)"
    1.17 -  "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))";
    1.18 +  "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
    1.19  
    1.20  text{*\noindent
    1.21  According to the measure function, the second argument should decrease with
    1.22 @@ -50,10 +50,10 @@
    1.23  following alternative definition suggests itself:
    1.24  *}
    1.25  
    1.26 -consts gcd1 :: "nat\<times>nat \<Rightarrow> nat";
    1.27 +consts gcd1 :: "nat\<times>nat \<Rightarrow> nat"
    1.28  recdef gcd1 "measure (\<lambda>(m,n).n)"
    1.29    "gcd1 (m, 0) = m"
    1.30 -  "gcd1 (m, n) = gcd1(n, m mod n)";
    1.31 +  "gcd1 (m, n) = gcd1(n, m mod n)"
    1.32  
    1.33  
    1.34  text{*\noindent
    1.35 @@ -65,9 +65,9 @@
    1.36  which is also available for @{typ bool} and is not split automatically:
    1.37  *}
    1.38  
    1.39 -consts gcd2 :: "nat\<times>nat \<Rightarrow> nat";
    1.40 +consts gcd2 :: "nat\<times>nat \<Rightarrow> nat"
    1.41  recdef gcd2 "measure (\<lambda>(m,n).n)"
    1.42 -  "gcd2(m,n) = (case n=0 of True \<Rightarrow> m | False \<Rightarrow> gcd2(n,m mod n))";
    1.43 +  "gcd2(m,n) = (case n=0 of True \<Rightarrow> m | False \<Rightarrow> gcd2(n,m mod n))"
    1.44  
    1.45  text{*\noindent
    1.46  This is probably the neatest solution next to pattern matching, and it is
    1.47 @@ -78,12 +78,12 @@
    1.48  these lemmas:
    1.49  *}
    1.50  
    1.51 -lemma [simp]: "gcd (m, 0) = m";
    1.52 -apply(simp);
    1.53 +lemma [simp]: "gcd (m, 0) = m"
    1.54 +apply(simp)
    1.55  done
    1.56  
    1.57 -lemma [simp]: "n \<noteq> 0 \<Longrightarrow> gcd(m, n) = gcd(n, m mod n)";
    1.58 -apply(simp);
    1.59 +lemma [simp]: "n \<noteq> 0 \<Longrightarrow> gcd(m, n) = gcd(n, m mod n)"
    1.60 +apply(simp)
    1.61  done
    1.62  
    1.63  text{*\noindent