equal
deleted
inserted
replaced
55 continuous function space. However, the domain package does not |
55 continuous function space. However, the domain package does not |
56 generate an induction rule in terms of the constructors. |
56 generate an induction rule in terms of the constructors. |
57 \<close> |
57 \<close> |
58 |
58 |
59 domain 'a d7 = d7a "'a d7 \<oplus> int lift" | d7b "'a \<otimes> 'a d7" | d7c (lazy "'a d7 \<rightarrow> 'a") |
59 domain 'a d7 = d7a "'a d7 \<oplus> int lift" | d7b "'a \<otimes> 'a d7" | d7c (lazy "'a d7 \<rightarrow> 'a") |
60 \<comment> "Indirect recursion detected, skipping proofs of (co)induction rules" |
60 \<comment> \<open>Indirect recursion detected, skipping proofs of (co)induction rules\<close> |
61 |
61 |
62 text \<open>Note that \<open>d7.induct\<close> is absent.\<close> |
62 text \<open>Note that \<open>d7.induct\<close> is absent.\<close> |
63 |
63 |
64 text \<open> |
64 text \<open> |
65 Indirect recursion is also allowed using previously-defined datatypes. |
65 Indirect recursion is also allowed using previously-defined datatypes. |
92 text \<open>Induction rules for flat datatypes have no admissibility side-condition.\<close> |
92 text \<open>Induction rules for flat datatypes have no admissibility side-condition.\<close> |
93 |
93 |
94 domain 'a flattree = Tip | Branch "'a flattree" "'a flattree" |
94 domain 'a flattree = Tip | Branch "'a flattree" "'a flattree" |
95 |
95 |
96 lemma "\<lbrakk>P \<bottom>; P Tip; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>; P x; P y\<rbrakk> \<Longrightarrow> P (Branch\<cdot>x\<cdot>y)\<rbrakk> \<Longrightarrow> P x" |
96 lemma "\<lbrakk>P \<bottom>; P Tip; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>; P x; P y\<rbrakk> \<Longrightarrow> P (Branch\<cdot>x\<cdot>y)\<rbrakk> \<Longrightarrow> P x" |
97 by (rule flattree.induct) \<comment> "no admissibility requirement" |
97 by (rule flattree.induct) \<comment> \<open>no admissibility requirement\<close> |
98 |
98 |
99 text \<open>Trivial datatypes will produce a warning message.\<close> |
99 text \<open>Trivial datatypes will produce a warning message.\<close> |
100 |
100 |
101 domain triv = Triv triv triv |
101 domain triv = Triv triv triv |
102 \<comment> "domain \<open>Domain_ex.triv\<close> is empty!" |
102 \<comment> \<open>domain \<open>Domain_ex.triv\<close> is empty!\<close> |
103 |
103 |
104 lemma "(x::triv) = \<bottom>" by (induct x, simp_all) |
104 lemma "(x::triv) = \<bottom>" by (induct x, simp_all) |
105 |
105 |
106 text \<open>Lazy constructor arguments may have unpointed types.\<close> |
106 text \<open>Lazy constructor arguments may have unpointed types.\<close> |
107 |
107 |