src/HOL/Codegenerator_Test/Candidates.thy
author hoelzl
Fri Feb 19 13:40:50 2016 +0100 (2016-02-19)
changeset 62378 85ed00c1fe7c
parent 62352 35a9e1cbb5b3
child 62425 d0936b500bf5
permissions -rw-r--r--
generalize more theorems to support enat and ennreal
haftmann@31378
     1
haftmann@31378
     2
(* Author: Florian Haftmann, TU Muenchen *)
haftmann@21917
     3
wenzelm@58889
     4
section {* A huge collection of equations to generate code from *}
haftmann@21917
     5
haftmann@37695
     6
theory Candidates
haftmann@21917
     7
imports
haftmann@27421
     8
  Complex_Main
haftmann@51160
     9
  "~~/src/HOL/Library/Library"
haftmann@51161
    10
  "~~/src/HOL/Library/Sublist_Order"
haftmann@62352
    11
  "~~/src/HOL/Library/Polynomial_GCD_euclidean"
haftmann@61227
    12
  "~~/src/HOL/Data_Structures/Tree_Map"
haftmann@61227
    13
  "~~/src/HOL/Data_Structures/Tree_Set"
haftmann@51173
    14
  "~~/src/HOL/Number_Theory/Eratosthenes"
haftmann@35303
    15
  "~~/src/HOL/ex/Records"
haftmann@21917
    16
begin
haftmann@21917
    17
haftmann@61129
    18
text \<open>Drop technical stuff from @{theory Quickcheck_Narrowing} which is tailored towards Haskell\<close>
haftmann@61129
    19
haftmann@59484
    20
setup \<open>
wenzelm@59842
    21
fn thy =>
haftmann@59484
    22
let
wenzelm@59842
    23
  val tycos = Sign.logical_types thy;
wenzelm@59842
    24
  val consts = map_filter (try (curry (Axclass.param_of_inst thy)
haftmann@59484
    25
    @{const_name "Quickcheck_Narrowing.partial_term_of"})) tycos;
wenzelm@59842
    26
in fold Code.del_eqns consts thy end
haftmann@61129
    27
\<close>
haftmann@61129
    28
haftmann@61129
    29
text \<open>Simple example for the predicate compiler.\<close>
haftmann@59484
    30
haftmann@51161
    31
inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
haftmann@51161
    32
where
haftmann@51161
    33
  empty: "sublist [] xs"
haftmann@51161
    34
| drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
haftmann@51161
    35
| take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)"
haftmann@33500
    36
haftmann@33500
    37
code_pred sublist .
haftmann@33500
    38
haftmann@61129
    39
text \<open>Avoid popular infix.\<close>
haftmann@61129
    40
haftmann@61129
    41
code_reserved SML upto
haftmann@61129
    42
haftmann@61129
    43
text \<open>Explicit check in @{text OCaml} for correct precedence of let expressions in list expressions\<close>
haftmann@61129
    44
haftmann@61129
    45
definition funny_list :: "bool list"
haftmann@61129
    46
where
haftmann@61129
    47
  "funny_list = [let b = True in b, False]"
haftmann@61129
    48
haftmann@61129
    49
definition funny_list' :: "bool list"
haftmann@61129
    50
where
haftmann@61129
    51
  "funny_list' = funny_list"
haftmann@61129
    52
haftmann@61129
    53
lemma [code]:
haftmann@61129
    54
  "funny_list' = [True, False]"
haftmann@61129
    55
  by (simp add: funny_list_def funny_list'_def)
haftmann@61129
    56
haftmann@61129
    57
definition check_list :: unit
haftmann@61129
    58
where
haftmann@61129
    59
  "check_list = (if funny_list = funny_list' then () else undefined)"
haftmann@31378
    60
haftmann@61130
    61
text \<open>Explicit check in @{text Scala} for correct bracketing of abstractions\<close>
haftmann@61130
    62
haftmann@61130
    63
definition funny_funs :: "(bool \<Rightarrow> bool) list \<Rightarrow> (bool \<Rightarrow> bool) list"
haftmann@61130
    64
where
haftmann@61130
    65
  "funny_funs fs = (\<lambda>x. x \<or> True) # (\<lambda>x. x \<or> False) # fs"
haftmann@61130
    66
haftmann@21917
    67
end