added
authorhaftmann
Thu Dec 28 10:04:10 2006 +0100 (2006-12-28)
changeset 2191712b8fde1f9c0
parent 21916 68c848f636bb
child 21918 71e312d6d19a
added
src/HOL/ex/ExecutableContent.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/ex/ExecutableContent.thy	Thu Dec 28 10:04:10 2006 +0100
     1.3 @@ -0,0 +1,78 @@
     1.4 +(*  ID:         $Id$
     1.5 +    Author:     Florian Haftmann, TU Muenchen
     1.6 +*)
     1.7 +
     1.8 +header {* A huge set of executable constants *}
     1.9 +
    1.10 +theory ExecutableContent
    1.11 +imports
    1.12 +  Main
    1.13 +  "~~/src/HOL/ex/Records"
    1.14 +  AssocList
    1.15 +  Binomial
    1.16 +  Commutative_Ring
    1.17 +  GCD
    1.18 +  List_Prefix
    1.19 +  Nat_Infinity
    1.20 +  NatPair
    1.21 +  Nested_Environment
    1.22 +  Permutation
    1.23 +  Primes
    1.24 +  Product_ord
    1.25 +  SetsAndFunctions
    1.26 +  State_Monad
    1.27 +  While_Combinator
    1.28 +  Word
    1.29 +begin
    1.30 +
    1.31 +definition
    1.32 +  n :: nat where
    1.33 +  "n = 42"
    1.34 +
    1.35 +definition
    1.36 +  k :: "int" where
    1.37 +  "k = -42"
    1.38 +
    1.39 +datatype mut1 = Tip | Top mut2
    1.40 +  and mut2 = Tip | Top mut1
    1.41 +
    1.42 +consts
    1.43 +  mut1 :: "mut1 \<Rightarrow> mut1"
    1.44 +  mut2 :: "mut2 \<Rightarrow> mut2"
    1.45 +
    1.46 +primrec
    1.47 +  "mut1 mut1.Tip = mut1.Tip"
    1.48 +  "mut1 (mut1.Top x) = mut1.Top (mut2 x)"
    1.49 +  "mut2 mut2.Tip = mut2.Tip"
    1.50 +  "mut2 (mut2.Top x) = mut2.Top (mut1 x)"
    1.51 +
    1.52 +definition
    1.53 +  "mystring = ''my home is my castle''"
    1.54 +
    1.55 +text {* nested lets and such *}
    1.56 +
    1.57 +definition
    1.58 +  "abs_let x = (let (y, z) = x in (\<lambda>u. case u of () \<Rightarrow> (y + y)))"
    1.59 +
    1.60 +definition
    1.61 +  "nested_let x = (let (y, z) = x in let w = y z in w * w)"
    1.62 +
    1.63 +definition
    1.64 +  "case_let x = (let (y, z) = x in case y of () => z)"
    1.65 +
    1.66 +definition
    1.67 +  "base_case f = f list_case"
    1.68 +
    1.69 +definition
    1.70 +  "apply_tower = (\<lambda>x. x (\<lambda>x. x (\<lambda>x. x)))"
    1.71 +
    1.72 +definition
    1.73 +  "keywords fun datatype x instance funa classa =
    1.74 +    Suc fun + datatype * x mod instance - funa - classa"
    1.75 +
    1.76 +hide (open) const keywords
    1.77 +
    1.78 +definition
    1.79 +  "shadow keywords = keywords @ [ExecutableContent.keywords 0 0 0 0 0 0]"
    1.80 +
    1.81 +end