src/HOL/ex/Codegenerator.thy
changeset 21404 eb85850d3eb7
parent 21319 cf814e36f788
child 21420 8b15e5e66813
     1.1 --- a/src/HOL/ex/Codegenerator.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/HOL/ex/Codegenerator.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -11,23 +11,27 @@
     1.4  subsection {* booleans *}
     1.5  
     1.6  definition
     1.7 -  xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
     1.8 +  xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
     1.9    "xor p q = ((p | q) & \<not> (p & q))"
    1.10  
    1.11  subsection {* natural numbers *}
    1.12  
    1.13  definition
    1.14 -  n :: nat
    1.15 +  n :: nat where
    1.16    "n = 42"
    1.17  
    1.18  subsection {* pairs *}
    1.19  
    1.20  definition
    1.21 -  swap :: "'a * 'b \<Rightarrow> 'b * 'a"
    1.22 +  swap :: "'a * 'b \<Rightarrow> 'b * 'a" where
    1.23    "swap p = (let (x, y) = p in (y, x))"
    1.24 -  appl :: "('a \<Rightarrow> 'b) * 'a \<Rightarrow> 'b"
    1.25 +
    1.26 +definition
    1.27 +  appl :: "('a \<Rightarrow> 'b) * 'a \<Rightarrow> 'b" where
    1.28    "appl p = (let (f, x) = p in f x)"
    1.29 -  snd_three :: "'a * 'b * 'c => 'b"
    1.30 +
    1.31 +definition
    1.32 +  snd_three :: "'a * 'b * 'c => 'b" where
    1.33    "snd_three a = id (\<lambda>(a, b, c). b) a"
    1.34  
    1.35  lemma [code]:
    1.36 @@ -41,7 +45,7 @@
    1.37  subsection {* integers *}
    1.38  
    1.39  definition
    1.40 -  k :: "int"
    1.41 +  k :: "int" where
    1.42    "k = -42"
    1.43  
    1.44  function
    1.45 @@ -59,9 +63,11 @@
    1.46  subsection {* lists *}
    1.47  
    1.48  definition
    1.49 -  ps :: "nat list"
    1.50 +  ps :: "nat list" where
    1.51    "ps = [2, 3, 5, 7, 11]"
    1.52 -  qs :: "nat list"
    1.53 +
    1.54 +definition
    1.55 +  qs :: "nat list" where
    1.56    "qs == rev ps"
    1.57  
    1.58  subsection {* mutual datatypes *}