src/HOL/ex/ExecutableContent.thy
author haftmann
Tue Sep 18 07:46:00 2007 +0200 (2007-09-18)
changeset 24626 85eceef2edc7
parent 24530 1bac25879117
child 25536 01753a944433
permissions -rw-r--r--
introduced generic concepts for theory interpretators
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@24626
    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"
berghofe@24530
    16
  "~~/src/HOL/Real/RealDef"
haftmann@21917
    17
  GCD
haftmann@21917
    18
  List_Prefix
haftmann@21917
    19
  Nat_Infinity
haftmann@21917
    20
  NatPair
haftmann@24433
    21
  Nested_Environment
haftmann@21917
    22
  Permutation
haftmann@21917
    23
  Primes
haftmann@21917
    24
  Product_ord
haftmann@21917
    25
  SetsAndFunctions
haftmann@21917
    26
  State_Monad
haftmann@21917
    27
  While_Combinator
haftmann@21917
    28
  Word
haftmann@21917
    29
begin
haftmann@21917
    30
haftmann@21917
    31
definition
haftmann@21917
    32
  n :: nat where
haftmann@21917
    33
  "n = 42"
haftmann@21917
    34
haftmann@21917
    35
definition
haftmann@21917
    36
  k :: "int" where
haftmann@21917
    37
  "k = -42"
haftmann@21917
    38
haftmann@21917
    39
datatype mut1 = Tip | Top mut2
haftmann@21917
    40
  and mut2 = Tip | Top mut1
haftmann@21917
    41
haftmann@21917
    42
consts
haftmann@21917
    43
  mut1 :: "mut1 \<Rightarrow> mut1"
haftmann@21917
    44
  mut2 :: "mut2 \<Rightarrow> mut2"
haftmann@21917
    45
haftmann@21917
    46
primrec
haftmann@21917
    47
  "mut1 mut1.Tip = mut1.Tip"
haftmann@21917
    48
  "mut1 (mut1.Top x) = mut1.Top (mut2 x)"
haftmann@21917
    49
  "mut2 mut2.Tip = mut2.Tip"
haftmann@21917
    50
  "mut2 (mut2.Top x) = mut2.Top (mut1 x)"
haftmann@21917
    51
haftmann@21917
    52
definition
haftmann@21917
    53
  "mystring = ''my home is my castle''"
haftmann@21917
    54
haftmann@21917
    55
text {* nested lets and such *}
haftmann@21917
    56
haftmann@21917
    57
definition
haftmann@21917
    58
  "abs_let x = (let (y, z) = x in (\<lambda>u. case u of () \<Rightarrow> (y + y)))"
haftmann@21917
    59
haftmann@21917
    60
definition
haftmann@21917
    61
  "nested_let x = (let (y, z) = x in let w = y z in w * w)"
haftmann@21917
    62
haftmann@21917
    63
definition
haftmann@21917
    64
  "case_let x = (let (y, z) = x in case y of () => z)"
haftmann@21917
    65
haftmann@21917
    66
definition
haftmann@21917
    67
  "base_case f = f list_case"
haftmann@21917
    68
haftmann@21917
    69
definition
haftmann@21917
    70
  "apply_tower = (\<lambda>x. x (\<lambda>x. x (\<lambda>x. x)))"
haftmann@21917
    71
haftmann@21917
    72
definition
haftmann@21917
    73
  "keywords fun datatype x instance funa classa =
haftmann@21917
    74
    Suc fun + datatype * x mod instance - funa - classa"
haftmann@21917
    75
haftmann@21917
    76
hide (open) const keywords
haftmann@21917
    77
haftmann@21917
    78
definition
haftmann@21917
    79
  "shadow keywords = keywords @ [ExecutableContent.keywords 0 0 0 0 0 0]"
haftmann@21917
    80
haftmann@24197
    81
definition
haftmann@24197
    82
  foo :: "rat \<Rightarrow> rat \<Rightarrow> rat \<Rightarrow> rat" where
haftmann@24197
    83
  "foo r s t = (t + s) / t"
haftmann@24197
    84
haftmann@24197
    85
definition
haftmann@24197
    86
  bar :: "rat \<Rightarrow> rat \<Rightarrow> rat \<Rightarrow> bool" where
haftmann@24197
    87
  "bar r s t \<longleftrightarrow> (r - s) \<le> t \<or> (s - t) \<le> r"
haftmann@24197
    88
haftmann@24197
    89
definition
haftmann@24197
    90
  "R1 = Fract 3 7"
haftmann@24197
    91
haftmann@24197
    92
definition
haftmann@24197
    93
  "R2 = Fract (-7) 5"
haftmann@24197
    94
haftmann@24197
    95
definition
haftmann@24197
    96
  "R3 = Fract 11 (-9)"
haftmann@24197
    97
haftmann@24197
    98
definition
haftmann@24197
    99
  "foobar = (foo R1 1 R3, bar R2 0 R3, foo R1 R3 R2)"
haftmann@24197
   100
haftmann@24197
   101
definition
haftmann@24197
   102
  foo' :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real" where
haftmann@24197
   103
  "foo' r s t = (t + s) / t"
haftmann@24197
   104
haftmann@24197
   105
definition
haftmann@24197
   106
  bar' :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> bool" where
haftmann@24197
   107
  "bar' r s t \<longleftrightarrow> (r - s) \<le> t \<or> (s - t) \<le> r"
haftmann@24197
   108
haftmann@24197
   109
definition
haftmann@24197
   110
  "R1' = real_of_rat (Fract 3 7)"
haftmann@24197
   111
haftmann@24197
   112
definition
haftmann@24197
   113
  "R2' = real_of_rat (Fract (-7) 5)"
haftmann@24197
   114
haftmann@24197
   115
definition
haftmann@24197
   116
  "R3' = real_of_rat (Fract 11 (-9))"
haftmann@24197
   117
haftmann@24197
   118
definition
haftmann@24197
   119
  "foobar' = (foo' R1' 1 R3', bar' R2' 0 R3', foo' R1' R3' R2')"
haftmann@24197
   120
haftmann@21917
   121
end