Domain_ex.thy revision 6c871203b5e72e818f1d3de1ce767d675fbe8cfe
ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu(* Title: HOL/HOLCF/Tutorial/Domain_ex.thy
ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu Author: Brian Huffman
ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiuheader {* Domain package examples *}
ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiutheory Domain_ex
ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiudomain d1 = d1a | d1b "d1" "d1"
734257b9ea9fcaa18d4e3627f54f5295a99aa1f7Felix Gabriel Mancelemma "d1b\<cdot>\<bottom>\<cdot>y = \<bottom>" by simp
c038fcf2030a6cfac7a261dee48a9eb29edb78eaFelix Gabriel Mancedomain d2 = d2a | d2b (lazy "d2")
ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiulemma "d2b\<cdot>x \<noteq> \<bottom>" by simp
ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiudomain d3 = d3a | d3b (lazy "d2") "d2"
5180a08007989fd364622fc9bc01f82141643f7bFelix Gabriel Mancelemma "P (d3b\<cdot>x\<cdot>y = \<bottom>) \<longleftrightarrow> P (y = \<bottom>)" by simp
734257b9ea9fcaa18d4e3627f54f5295a99aa1f7Felix Gabriel Mancedomain d4 = d4a | d4b (lazy d4b_left :: "d2") (d4b_right :: "d2")
0be7a9c012366ada63d587898a15c551b499b76dFelix Gabriel Mancelemma "y \<noteq> \<bottom> \<Longrightarrow> d4b_left\<cdot>(d4b\<cdot>x\<cdot>y) = x" by simp
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mancedomain d5 = d5a | d5b (lazy "d5") "d5" (infixl ":#:" 70)
0be7a9c012366ada63d587898a15c551b499b76dFelix Gabriel Mancelemma "d5a \<noteq> x :#: y :#: z" by simp
0be7a9c012366ada63d587898a15c551b499b76dFelix Gabriel Mancedomain ('a, 'b) lazypair (infixl ":*:" 25) =
0be7a9c012366ada63d587898a15c551b499b76dFelix Gabriel Mance lpair (lazy lfst :: 'a) (lazy lsnd :: 'b) (infixl ":*:" 75)
30e9cf458094e5970bc06be667558961c2eccff4Felix Gabriel Mancelemma "\<forall>p::('a :*: 'b). p \<sqsubseteq> lfst\<cdot>p :*: lsnd\<cdot>p"
30e9cf458094e5970bc06be667558961c2eccff4Felix Gabriel Manceby (rule allI, case_tac p, simp_all)
dec48ce9576469185a15c3c58258032823a9c536Felix Gabriel Mancedomain ('a, 'b) d6 = d6 "int lift" "'a \<oplus> 'b u" (lazy "('a :*: 'b) \<times> ('b \<rightarrow> 'a)")
30e9cf458094e5970bc06be667558961c2eccff4Felix Gabriel Mancedomain 'a d7 = d7a "'a d7 \<oplus> int lift" | d7b "'a \<otimes> 'a d7" | d7c (lazy "'a d7 \<rightarrow> 'a")
30e9cf458094e5970bc06be667558961c2eccff4Felix Gabriel Mance -- "Indirect recursion detected, skipping proofs of (co)induction rules"
30e9cf458094e5970bc06be667558961c2eccff4Felix Gabriel Mancedomain 'a slist = SNil | SCons 'a "'a slist"
3e0eb79b52a3078a12531efc3f66d0d94fd9938dFelix Gabriel Mancedomain 'a stree = STip | SBranch "'a stree slist"
3e0eb79b52a3078a12531efc3f66d0d94fd9938dFelix Gabriel Mancedomain d8 = d8a | d8b "d9" and d9 = d9a | d9b (lazy "d8")
30e9cf458094e5970bc06be667558961c2eccff4Felix Gabriel Mancedomain ('a, 'b) list1 = Nil1 | Cons1 'a "('b, 'a) list2"
3e0eb79b52a3078a12531efc3f66d0d94fd9938dFelix Gabriel Mance and ('b, 'a) list2 = Nil2 | Cons2 'b "('a, 'b) list1"
30e9cf458094e5970bc06be667558961c2eccff4Felix Gabriel Mancedomain 'a flattree = Tip | Branch "'a flattree" "'a flattree"
316ef492799cd45fea0f5c26932f49adddfda3f7Felix Gabriel Mancelemma "\<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"
3e0eb79b52a3078a12531efc3f66d0d94fd9938dFelix Gabriel Manceby (rule flattree.induct) -- "no admissibility requirement"
30e9cf458094e5970bc06be667558961c2eccff4Felix Gabriel Mancedomain triv = Triv triv triv
316ef492799cd45fea0f5c26932f49adddfda3f7Felix Gabriel Mancelemma "(x::triv) = \<bottom>" by (induct x, simp_all)
316ef492799cd45fea0f5c26932f49adddfda3f7Felix Gabriel Mancedomain natlist = nnil | ncons (lazy "nat discr") natlist
31a5ba51cd6d24e28a23abf64ce4043a45eabbefFelix Gabriel Mancedomain ('a::predomain) box = Box (lazy 'a)
30e9cf458094e5970bc06be667558961c2eccff4Felix Gabriel Mancedomain ('a::countable) stream = snil | scons (lazy "'a discr") "'a stream"
734257b9ea9fcaa18d4e3627f54f5295a99aa1f7Felix Gabriel Mancedomain 'a tree = Leaf (lazy 'a) | Node (left :: "'a tree") (right :: "'a tree")