(* Author: Florian Haftmann, TU Muenchen *)

section ‹A huge collection of equations to generate code from›

theory Candidates
imports
  Basic_Setup
  "HOL-Library.Library"
  "HOL-Library.Sorting_Algorithms"
  "HOL-Library.Subseq_Order"
  "HOL-Library.RBT"
  "HOL-Data_Structures.Tree_Map"
  "HOL-Data_Structures.Tree_Set"
  "HOL-Computational_Algebra.Computational_Algebra"
  "HOL-Computational_Algebra.Polynomial_Factorial"
  "HOL-Number_Theory.Eratosthenes"
  "HOL-Examples.Records"
  "HOL-Examples.Gauss_Numbers"
begin

setup ‹Codegenerator_Test.drop_partial_term_of›

text ‹Simple example for the predicate compiler.›

inductive sublist :: "'a list → 'a list → bool"
where
  empty: "sublist [] xs"
| drop: "sublist ys xs ==> sublist ys (x # xs)"
| take: "sublist ys xs ==> sublist (x # ys) (x # xs)"

code_pred sublist .

text ‹Explicit check in ‹OCaml› for correct precedence of let expressions in list expressions›

definition funny_list :: "bool list"
where
  "funny_list = [let b = True in b, False]"

definition funny_list' :: "bool list"
where
  "funny_list' = funny_list"

lemma [code]:
  "funny_list' = [True, False]"
  by (simp add: funny_list_def funny_list'_def)

definition check_list :: unit
where
  "check_list = (if funny_list = funny_list' then () else undefined)"

text ‹Explicit check in ‹Scala› for correct bracketing of abstractions›

definition funny_funs :: "(bool → bool) list → (bool → bool) list"
where
  "funny_funs fs = (λx. x ∨ True) # (λx. x ∨ False) # fs"

text ‹Explicit checks for strings etc.›

definition ‹hello = ''Hello, world!''›

definition ‹hello2 = String.explode (String.implode hello)›

definition ‹which_hello ⟷ hello ≤ hello2›

end