src/HOL/ex/CodeCollections.thy

Clarify comment

(*  ID:         $Id$
    Author:     Florian Haftmann, TU Muenchen
*)

header {* Collection classes as examples for code generation *}

theory CodeCollections
imports Main Product_ord List_lexord
begin

fun
  abs_sorted :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
  "abs_sorted cmp [] \<longleftrightarrow> True"
  "abs_sorted cmp [x] \<longleftrightarrow> True"
  "abs_sorted cmp (x#y#xs) \<longleftrightarrow> cmp x y \<and> abs_sorted cmp (y#xs)"

abbreviation (in ord)
  "sorted \<equiv> abs_sorted less_eq"

abbreviation
  "sorted \<equiv> abs_sorted less_eq"

lemma (in order) sorted_weakening:
  assumes "sorted (x # xs)"
  shows "sorted xs"
using prems proof (induct xs)
  case Nil show ?case by simp 
next
  case (Cons x' xs)
  from this have "sorted (x # x' # xs)" by auto
  then show "sorted (x' # xs)"
    by auto
qed

instance unit :: order
  "u \<le> v \<equiv> True"
  "u < v \<equiv> False"
  by default (simp_all add: less_eq_unit_def less_unit_def)

fun le_option' :: "'a\<Colon>order option \<Rightarrow> 'a option \<Rightarrow> bool"
  where "le_option' None y \<longleftrightarrow> True"
  | "le_option' (Some x) None \<longleftrightarrow> False"
  | "le_option' (Some x) (Some y) \<longleftrightarrow> x \<le> y"

instance option :: (order) order
  "x \<le> y \<equiv> le_option' x y"
  "x < y \<equiv> x \<le> y \<and> x \<noteq> y"
proof (default, unfold less_eq_option_def less_option_def)
  fix x
  show "le_option' x x" by (cases x) simp_all
next
  fix x y z
  assume "le_option' x y" "le_option' y z"
  then show "le_option' x z"
    by (cases x, simp_all, cases y, simp_all, cases z, simp_all)
next
  fix x y
  assume "le_option' x y" "le_option' y x"
  then show "x = y"
    by (cases x, simp_all, cases y, simp_all, cases y, simp_all)
next
  fix x y
  show "le_option' x y \<and> x \<noteq> y \<longleftrightarrow> le_option' x y \<and> x \<noteq> y" ..
qed

lemma [simp, code]:
  "None \<le> y \<longleftrightarrow> True"
  "Some x \<le> None \<longleftrightarrow> False"
  "Some v \<le> Some w \<longleftrightarrow> v \<le> w"
  unfolding less_eq_option_def less_option_def le_option'.simps by rule+

lemma forall_all [simp]:
  "list_all P xs \<longleftrightarrow> (\<forall>x\<in>set xs. P x)"
  by (induct xs) auto

lemma exists_ex [simp]:
  "list_ex P xs \<longleftrightarrow> (\<exists>x\<in>set xs. P x)"
  by (induct xs) auto

class finite =
  fixes fin :: "'a list"
  assumes member_fin: "x \<in> set fin"
begin

lemma set_enum_UNIV:
  "set fin = UNIV"
  using member_fin by auto

lemma all_forall [code func, code inline]:
  "(\<forall>x. P x) \<longleftrightarrow> list_all P fin"
  using set_enum_UNIV by simp_all

lemma ex_exists [code func, code inline]:
  "(\<exists>x. P x) \<longleftrightarrow> list_ex P fin"
  using set_enum_UNIV by simp_all

end
  
instance bool :: finite
  "fin == [False, True]"
  by default (simp_all add: fin_bool_def)

instance unit :: finite
  "fin == [()]"
  by default (simp_all add: fin_unit_def)

fun
  product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a * 'b) list"
  where
  "product [] ys = []"
  "product (x#xs) ys = map (Pair x) ys @ product xs ys"

lemma product_all:
  assumes "x \<in> set xs" "y \<in> set ys"
  shows "(x, y) \<in> set (product xs ys)"
using prems proof (induct xs)
  case Nil
  then have False by auto
  then show ?case ..
next
  case (Cons z xs)
  then show ?case
  proof (cases "x = z")
    case True
    with Cons have "(x, y) \<in> set (product (x # xs) ys)" by simp
    with True show ?thesis by simp
  next
    case False
    with Cons have "x \<in> set xs" by auto
    with Cons have "(x, y) \<in> set (product xs ys)" by auto
    then show "(x, y) \<in> set (product (z#xs) ys)" by auto
  qed
qed

instance * :: (finite, finite) finite
  "fin == product fin fin"
apply default
apply (simp_all add: "fin_*_def")
apply (unfold split_paired_all)
apply (rule product_all)
apply (rule finite_class.member_fin)+
done

instance option :: (finite) finite
  "fin == None # map Some fin"
proof (default, unfold fin_option_def)
  fix x :: "'a::finite option"
  show "x \<in> set (None # map Some fin)"
  proof (cases x)
    case None then show ?thesis by auto
  next
    case (Some x) then show ?thesis by (auto intro: finite_class.member_fin)
  qed
qed

consts
  get_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a option"

primrec
  "get_first p [] = None"
  "get_first p (x#xs) = (if p x then Some x else get_first p xs)"

consts
  get_index :: "('a \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> nat option"

primrec
  "get_index p n [] = None"
  "get_index p n (x#xs) = (if p x then Some n else get_index p (Suc n) xs)"

(*definition
  between :: "'a::enum \<Rightarrow> 'a \<Rightarrow> 'a option" where
  "between x y = get_first (\<lambda>z. x << z & z << y) enum"

definition
  index :: "'a::enum \<Rightarrow> nat" where
  "index x = the (get_index (\<lambda>y. y = x) 0 enum)"

definition
  add :: "'a::enum \<Rightarrow> 'a \<Rightarrow> 'a" where
  "add x y =
    (let
      enm = enum
    in enm ! ((index x + index y) mod length enm))"

consts
  sum :: "'a::{enum, infimum} list \<Rightarrow> 'a"

primrec
  "sum [] = inf"
  "sum (x#xs) = add x (sum xs)"*)

(*definition "test1 = sum [None, Some True, None, Some False]"*)
(*definition "test2 = (inf :: nat \<times> unit)"*)
definition "test3 \<longleftrightarrow> (\<exists>x \<Colon> bool option. case x of Some P \<Rightarrow> P | None \<Rightarrow> False)"

code_gen test3 (SML #) (OCaml -) (Haskell -)

end