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
```     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/Library/Polynomial_GCD_euclidean"
```
```    12   "~~/src/HOL/Data_Structures/Tree_Map"
```
```    13   "~~/src/HOL/Data_Structures/Tree_Set"
```
```    14   "~~/src/HOL/Number_Theory/Eratosthenes"
```
```    15   "~~/src/HOL/ex/Records"
```
```    16 begin
```
```    17
```
```    18 text \<open>Drop technical stuff from @{theory Quickcheck_Narrowing} which is tailored towards Haskell\<close>
```
```    19
```
```    20 setup \<open>
```
```    21 fn thy =>
```
```    22 let
```
```    23   val tycos = Sign.logical_types thy;
```
```    24   val consts = map_filter (try (curry (Axclass.param_of_inst thy)
```
```    25     @{const_name "Quickcheck_Narrowing.partial_term_of"})) tycos;
```
```    26 in fold Code.del_eqns consts thy end
```
```    27 \<close>
```
```    28
```
```    29 text \<open>Simple example for the predicate compiler.\<close>
```
```    30
```
```    31 inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
```
```    32 where
```
```    33   empty: "sublist [] xs"
```
```    34 | drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
```
```    35 | take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)"
```
```    36
```
```    37 code_pred sublist .
```
```    38
```
```    39 text \<open>Avoid popular infix.\<close>
```
```    40
```
```    41 code_reserved SML upto
```
```    42
```
```    43 text \<open>Explicit check in @{text OCaml} for correct precedence of let expressions in list expressions\<close>
```
```    44
```
```    45 definition funny_list :: "bool list"
```
```    46 where
```
```    47   "funny_list = [let b = True in b, False]"
```
```    48
```
```    49 definition funny_list' :: "bool list"
```
```    50 where
```
```    51   "funny_list' = funny_list"
```
```    52
```
```    53 lemma [code]:
```
```    54   "funny_list' = [True, False]"
```
```    55   by (simp add: funny_list_def funny_list'_def)
```
```    56
```
```    57 definition check_list :: unit
```
```    58 where
```
```    59   "check_list = (if funny_list = funny_list' then () else undefined)"
```
```    60
```
```    61 text \<open>Explicit check in @{text Scala} for correct bracketing of abstractions\<close>
```
```    62
```
```    63 definition funny_funs :: "(bool \<Rightarrow> bool) list \<Rightarrow> (bool \<Rightarrow> bool) list"
```
```    64 where
```
```    65   "funny_funs fs = (\<lambda>x. x \<or> True) # (\<lambda>x. x \<or> False) # fs"
```
```    66
```
```    67 end
```