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