1(* Title: HOL/HOLCF/Tutorial/New_Domain.thy 2 Author: Brian Huffman 3*) 4 5section \<open>Definitional domain package\<close> 6 7theory New_Domain 8imports HOLCF 9begin 10 11text \<open> 12 UPDATE: The definitional back-end is now the default mode of the domain 13 package. This file should be merged with \<open>Domain_ex.thy\<close>. 14\<close> 15 16text \<open> 17 Provided that \<open>domain\<close> is the default sort, the \<open>new_domain\<close> 18 package should work with any type definition supported by the old 19 domain package. 20\<close> 21 22domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist") 23 24text \<open> 25 The difference is that the new domain package is completely 26 definitional, and does not generate any axioms. The following type 27 and constant definitions are not produced by the old domain package. 28\<close> 29 30thm type_definition_llist 31thm llist_abs_def llist_rep_def 32 33text \<open> 34 The new domain package also adds support for indirect recursion with 35 user-defined datatypes. This definition of a tree datatype uses 36 indirect recursion through the lazy list type constructor. 37\<close> 38 39domain 'a ltree = Leaf (lazy 'a) | Branch (lazy "'a ltree llist") 40 41text \<open> 42 For indirect-recursive definitions, the domain package is not able to 43 generate a high-level induction rule. (It produces a warning 44 message instead.) The low-level reach lemma (now proved as a 45 theorem, no longer generated as an axiom) can be used to derive 46 other induction rules. 47\<close> 48 49thm ltree.reach 50 51text \<open> 52 The definition of the take function uses map functions associated with 53 each type constructor involved in the definition. A map function 54 for the lazy list type has been generated by the new domain package. 55\<close> 56 57thm ltree.take_rews 58thm llist_map_def 59 60lemma ltree_induct: 61 fixes P :: "'a ltree \<Rightarrow> bool" 62 assumes adm: "adm P" 63 assumes bot: "P \<bottom>" 64 assumes Leaf: "\<And>x. P (Leaf\<cdot>x)" 65 assumes Branch: "\<And>f l. \<forall>x. P (f\<cdot>x) \<Longrightarrow> P (Branch\<cdot>(llist_map\<cdot>f\<cdot>l))" 66 shows "P x" 67proof - 68 have "P (\<Squnion>i. ltree_take i\<cdot>x)" 69 using adm 70 proof (rule admD) 71 fix i 72 show "P (ltree_take i\<cdot>x)" 73 proof (induct i arbitrary: x) 74 case (0 x) 75 show "P (ltree_take 0\<cdot>x)" by (simp add: bot) 76 next 77 case (Suc n x) 78 show "P (ltree_take (Suc n)\<cdot>x)" 79 apply (cases x) 80 apply (simp add: bot) 81 apply (simp add: Leaf) 82 apply (simp add: Branch Suc) 83 done 84 qed 85 qed (simp add: ltree.chain_take) 86 thus ?thesis 87 by (simp add: ltree.reach) 88qed 89 90end 91