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 *}
```