Theory Datatype_Record_Examples

theory Datatype_Record_Examples
imports "HOL-Library.Datatype_Records"
begin

text ‹Standard usage›

datatype_record ('a, 'b) foo =
  field_1 :: 'a
  field_2 :: 'b

lemma "⦇ field_1 = 3, field_2 = () ⦈ = (make_foo 3 () :: (nat, unit) foo)" ..

lemma "(make_foo a b) ⦇ field_1 := y ⦈ = make_foo y b"
  by (simp add: datatype_record_update)

lemma "(make_foo a b) ⦇ foo.field_1 := y ⦈ = make_foo y b"
  by (simp add: datatype_record_update)

text ‹Existing datatypes›

datatype x = X (a: int) (b: int)

lemma "⦇ a = 1, b = 2 ⦈ = X 1 2" ..

local_setup ‹Datatype_Records.mk_update_defs \<^type_name>‹x››

lemma "(X 1 2) ⦇ b := 3 ⦈ = X 1 3"
  by (simp add: datatype_record_update)

text ‹Nested recursion›

datatype_record 'a container =
  content :: "'a option"

datatype 'a contrived = Contrived "'a contrived container"

term "Contrived ⦇ content = None ⦈"

text ‹Supports features of @{command datatype}›

datatype_record (plugins del: code) (dead 'a :: finite, b_set: 'b) rec =
  field_1 :: 'a
  field_2 :: 'b

lemma "b_set ⦇ field_1 = True, field_2 = False ⦈ = {False}"
  by simp

text ‹More tests›

datatype_record ('a, 'b) test1 =
  field_t11 :: 'a
  field_t12 :: 'b
  field_t13 :: nat
  field_t14 :: int

thm test1.record_simps

definition ID where "ID x = x"
lemma ID_cong[cong]: "ID x = ID x" by (rule refl)

lemma "update_field_t11 f (update_field_t12 g (update_field_t11 h x)) = ID (update_field_t12 g (update_field_t11 (λx. f (h x)) x))"
  apply (simp only: test1.record_simps)
  apply (subst ID_def)
  apply (rule refl)
  done

end