src/HOL/ex/ExecutableContent.thy
author haftmann
Fri Aug 24 14:14:20 2007 +0200 (2007-08-24)
changeset 24423 ae9cd0e92423
parent 24197 c9e3cb5e5681
child 24433 4a405457e9d6
permissions -rw-r--r--
overloaded definitions accompanied by explicit constants
haftmann@21917
     1
(*  ID:         $Id$
haftmann@21917
     2
    Author:     Florian Haftmann, TU Muenchen
haftmann@21917
     3
*)
haftmann@21917
     4
haftmann@21917
     5
header {* A huge set of executable constants *}
haftmann@21917
     6
haftmann@21917
     7
theory ExecutableContent
haftmann@21917
     8
imports
haftmann@21917
     9
  Main
haftmann@22521
    10
  Eval
haftmann@23690
    11
  "~~/src/HOL/ex/Records"
haftmann@21917
    12
  AssocList
haftmann@21917
    13
  Binomial
haftmann@21917
    14
  Commutative_Ring
haftmann@23690
    15
  "~~/src/HOL/ex/Commutative_Ring_Complete"
haftmann@24197
    16
  Executable_Rat
haftmann@23016
    17
  Executable_Real
haftmann@21917
    18
  GCD
haftmann@21917
    19
  List_Prefix
haftmann@21917
    20
  Nat_Infinity
haftmann@21917
    21
  NatPair
haftmann@24423
    22
  (*Nested_Environment*)
haftmann@21917
    23
  Permutation
haftmann@21917
    24
  Primes
haftmann@21917
    25
  Product_ord
haftmann@21917
    26
  SetsAndFunctions
haftmann@21917
    27
  State_Monad
haftmann@21917
    28
  While_Combinator
haftmann@21917
    29
  Word
haftmann@21917
    30
begin
haftmann@21917
    31
haftmann@21917
    32
definition
haftmann@21917
    33
  n :: nat where
haftmann@21917
    34
  "n = 42"
haftmann@21917
    35
haftmann@21917
    36
definition
haftmann@21917
    37
  k :: "int" where
haftmann@21917
    38
  "k = -42"
haftmann@21917
    39
haftmann@21917
    40
datatype mut1 = Tip | Top mut2
haftmann@21917
    41
  and mut2 = Tip | Top mut1
haftmann@21917
    42
haftmann@21917
    43
consts
haftmann@21917
    44
  mut1 :: "mut1 \<Rightarrow> mut1"
haftmann@21917
    45
  mut2 :: "mut2 \<Rightarrow> mut2"
haftmann@21917
    46
haftmann@21917
    47
primrec
haftmann@21917
    48
  "mut1 mut1.Tip = mut1.Tip"
haftmann@21917
    49
  "mut1 (mut1.Top x) = mut1.Top (mut2 x)"
haftmann@21917
    50
  "mut2 mut2.Tip = mut2.Tip"
haftmann@21917
    51
  "mut2 (mut2.Top x) = mut2.Top (mut1 x)"
haftmann@21917
    52
haftmann@21917
    53
definition
haftmann@21917
    54
  "mystring = ''my home is my castle''"
haftmann@21917
    55
haftmann@21917
    56
text {* nested lets and such *}
haftmann@21917
    57
haftmann@21917
    58
definition
haftmann@21917
    59
  "abs_let x = (let (y, z) = x in (\<lambda>u. case u of () \<Rightarrow> (y + y)))"
haftmann@21917
    60
haftmann@21917
    61
definition
haftmann@21917
    62
  "nested_let x = (let (y, z) = x in let w = y z in w * w)"
haftmann@21917
    63
haftmann@21917
    64
definition
haftmann@21917
    65
  "case_let x = (let (y, z) = x in case y of () => z)"
haftmann@21917
    66
haftmann@21917
    67
definition
haftmann@21917
    68
  "base_case f = f list_case"
haftmann@21917
    69
haftmann@21917
    70
definition
haftmann@21917
    71
  "apply_tower = (\<lambda>x. x (\<lambda>x. x (\<lambda>x. x)))"
haftmann@21917
    72
haftmann@21917
    73
definition
haftmann@21917
    74
  "keywords fun datatype x instance funa classa =
haftmann@21917
    75
    Suc fun + datatype * x mod instance - funa - classa"
haftmann@21917
    76
haftmann@21917
    77
hide (open) const keywords
haftmann@21917
    78
haftmann@21917
    79
definition
haftmann@21917
    80
  "shadow keywords = keywords @ [ExecutableContent.keywords 0 0 0 0 0 0]"
haftmann@21917
    81
haftmann@24197
    82
definition
haftmann@24197
    83
  foo :: "rat \<Rightarrow> rat \<Rightarrow> rat \<Rightarrow> rat" where
haftmann@24197
    84
  "foo r s t = (t + s) / t"
haftmann@24197
    85
haftmann@24197
    86
definition
haftmann@24197
    87
  bar :: "rat \<Rightarrow> rat \<Rightarrow> rat \<Rightarrow> bool" where
haftmann@24197
    88
  "bar r s t \<longleftrightarrow> (r - s) \<le> t \<or> (s - t) \<le> r"
haftmann@24197
    89
haftmann@24197
    90
definition
haftmann@24197
    91
  "R1 = Fract 3 7"
haftmann@24197
    92
haftmann@24197
    93
definition
haftmann@24197
    94
  "R2 = Fract (-7) 5"
haftmann@24197
    95
haftmann@24197
    96
definition
haftmann@24197
    97
  "R3 = Fract 11 (-9)"
haftmann@24197
    98
haftmann@24197
    99
definition
haftmann@24197
   100
  "foobar = (foo R1 1 R3, bar R2 0 R3, foo R1 R3 R2)"
haftmann@24197
   101
haftmann@24197
   102
definition
haftmann@24197
   103
  foo' :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real" where
haftmann@24197
   104
  "foo' r s t = (t + s) / t"
haftmann@24197
   105
haftmann@24197
   106
definition
haftmann@24197
   107
  bar' :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> bool" where
haftmann@24197
   108
  "bar' r s t \<longleftrightarrow> (r - s) \<le> t \<or> (s - t) \<le> r"
haftmann@24197
   109
haftmann@24197
   110
definition
haftmann@24197
   111
  "R1' = real_of_rat (Fract 3 7)"
haftmann@24197
   112
haftmann@24197
   113
definition
haftmann@24197
   114
  "R2' = real_of_rat (Fract (-7) 5)"
haftmann@24197
   115
haftmann@24197
   116
definition
haftmann@24197
   117
  "R3' = real_of_rat (Fract 11 (-9))"
haftmann@24197
   118
haftmann@24197
   119
definition
haftmann@24197
   120
  "foobar' = (foo' R1' 1 R3', bar' R2' 0 R3', foo' R1' R3' R2')"
haftmann@24197
   121
haftmann@21917
   122
end