1theory Datatype_Record_Examples 2imports "HOL-Library.Datatype_Records" 3begin 4 5text \<open>Standard usage\<close> 6 7datatype_record ('a, 'b) foo = 8 field_1 :: 'a 9 field_2 :: 'b 10 11lemma "\<lparr> field_1 = 3, field_2 = () \<rparr> = (make_foo 3 () :: (nat, unit) foo)" .. 12 13lemma "(make_foo a b) \<lparr> field_1 := y \<rparr> = make_foo y b" 14 by (simp add: datatype_record_update) 15 16lemma "(make_foo a b) \<lparr> foo.field_1 := y \<rparr> = make_foo y b" 17 by (simp add: datatype_record_update) 18 19text \<open>Existing datatypes\<close> 20 21datatype x = X (a: int) (b: int) 22 23lemma "\<lparr> a = 1, b = 2 \<rparr> = X 1 2" .. 24 25local_setup \<open>Datatype_Records.mk_update_defs \<^type_name>\<open>x\<close>\<close> 26 27lemma "(X 1 2) \<lparr> b := 3 \<rparr> = X 1 3" 28 by (simp add: datatype_record_update) 29 30text \<open>Nested recursion\<close> 31 32datatype_record 'a container = 33 content :: "'a option" 34 35datatype 'a contrived = Contrived "'a contrived container" 36 37term "Contrived \<lparr> content = None \<rparr>" 38 39text \<open>Supports features of @{command datatype}\<close> 40 41datatype_record (plugins del: code) (dead 'a :: finite, b_set: 'b) rec = 42 field_1 :: 'a 43 field_2 :: 'b 44 45lemma "b_set \<lparr> field_1 = True, field_2 = False \<rparr> = {False}" 46 by simp 47 48text \<open>More tests\<close> 49 50datatype_record ('a, 'b) test1 = 51 field_t11 :: 'a 52 field_t12 :: 'b 53 field_t13 :: nat 54 field_t14 :: int 55 56thm test1.record_simps 57 58definition ID where "ID x = x" 59lemma ID_cong[cong]: "ID x = ID x" by (rule refl) 60 61lemma "update_field_t11 f (update_field_t12 g (update_field_t11 h x)) = ID (update_field_t12 g (update_field_t11 (\<lambda>x. f (h x)) x))" 62 apply (simp only: test1.record_simps) 63 apply (subst ID_def) 64 apply (rule refl) 65 done 66 67end