src/HOL/Codegenerator_Test/Candidates.thy
author paulson <lp15@cam.ac.uk>
Tue Mar 17 12:23:56 2015 +0000 (2015-03-17)
changeset 59731 7fccaeec22f0
parent 59484 a130ae7a9398
child 59733 cd945dc13bec
permissions -rw-r--r--
Merge
     1 
     2 (* Author: Florian Haftmann, TU Muenchen *)
     3 
     4 section {* A huge collection of equations to generate code from *}
     5 
     6 theory Candidates
     7 imports
     8   Complex_Main
     9   "~~/src/HOL/Library/Library"
    10   "~~/src/HOL/Library/Sublist_Order"
    11   "~~/src/HOL/Number_Theory/Eratosthenes"
    12   "~~/src/HOL/ex/Records"
    13 begin
    14 
    15 setup \<open>
    16 let
    17   val tycos = (#log_types o Type.rep_tsig o Sign.tsig_of) @{theory};
    18   val consts = map_filter (try (curry (Axclass.param_of_inst @{theory})
    19     @{const_name "Quickcheck_Narrowing.partial_term_of"})) tycos;
    20 in fold Code.del_eqns consts end
    21 \<close> -- \<open>drop technical stuff from @{text Quickcheck_Narrowing} which is tailored towards Haskell\<close>
    22 
    23 inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    24 where
    25   empty: "sublist [] xs"
    26 | drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
    27 | take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)"
    28 
    29 code_pred sublist .
    30 
    31 lemma [code]:  -- {* for the generic factorial function *}
    32   fixes XXX :: "'a :: semiring_numeral_div"
    33   shows
    34    "fact 0       = (1 :: 'a)"
    35    "fact (Suc n) = (of_nat (Suc n) * fact n :: 'a)"
    36  by simp_all
    37 
    38 code_reserved SML upto -- {* avoid popular infix *}
    39 
    40 end