(* Title: HOLCF/ex/Fixrec_ex.thy ID: $Id: Fixrec_ex.thy,v 1.1 2005/06/23 20:08:24 huffman Exp $ Author: Brian Huffman *) header {* Fixrec package examples *} theory Fixrec_ex imports HOLCF begin subsection {* basic fixrec examples *} text {* Fixrec patterns can mention any constructor defined by the domain package, as well as any of the following built-in constructors: cpair, spair, sinl, sinr, up, ONE, TT, FF. *} text {* typical usage is with lazy constructors *} consts down :: "'a u -> 'a" fixrec "down·(up·x) = x" text {* with strict constructors, rewrite rules may require side conditions *} consts from_sinl :: "'a ⊕ 'b -> 'a" fixrec "x ≠ ⊥ ==> from_sinl·(sinl·x) = x" text {* lifting can turn a strict constructor into a lazy one *} consts from_sinl_up :: "'a u ⊕ 'b -> 'a" fixrec "from_sinl_up·(sinl·(up·x)) = x" subsection {* fixpat examples *} text {* a type of lazy lists *} domain 'a llist = lNil | lCons (lazy 'a) (lazy "'a llist") text {* zip function for lazy lists *} consts lzip :: "'a llist -> 'b llist -> ('a × 'b) llist" text {* notice that the patterns are not exhaustive *} fixrec "lzip·(lCons·x·xs)·(lCons·y·ys) = lCons·<x,y>·(lzip·xs·ys)" "lzip·lNil·lNil = lNil" text {* fixpat is useful for producing strictness theorems *} text {* note that pattern matching is done in left-to-right order *} fixpat lzip_stricts [simp]: "lzip·⊥·ys" "lzip·lNil·⊥" "lzip·(lCons·x·xs)·⊥" text {* fixpat can also produce rules for missing cases *} fixpat lzip_undefs [simp]: "lzip·lNil·(lCons·y·ys)" "lzip·(lCons·x·xs)·lNil" subsection {* skipping proofs of rewrite rules *} text {* another zip function for lazy lists *} consts lzip2 :: "'a llist -> 'b llist -> ('a × 'b) llist" text {* Notice that this version has overlapping patterns. The second equation cannot be proved as a theorem because it only applies when the first pattern fails. *} fixrec (permissive) "lzip2·(lCons·x·xs)·(lCons·y·ys) = lCons·<x,y>·(lzip·xs·ys)" "lzip2·xs·ys = lNil" text {* Usually fixrec tries to prove all equations as theorems. The "permissive" option overrides this behavior, so fixrec does not produce any simp rules. *} text {* simp rules can be generated later using fixpat *} fixpat lzip2_simps [simp]: "lzip2·(lCons·x·xs)·(lCons·y·ys)" "lzip2·(lCons·x·xs)·lNil" "lzip2·lNil·(lCons·y·ys)" "lzip2·lNil·lNil" fixpat lzip2_stricts [simp]: "lzip2·⊥·ys" "lzip2·(lCons·x·xs)·⊥" subsection {* mutual recursion with fixrec *} text {* tree and forest types *} domain 'a tree = Leaf (lazy 'a) | Branch (lazy "'a forest") and 'a forest = Empty | Trees (lazy "'a tree") "'a forest" consts map_tree :: "('a -> 'b) -> ('a tree -> 'b tree)" map_forest :: "('a -> 'b) -> ('a forest -> 'b forest)" text {* To define mutually recursive functions, separate the equations for each function using the keyword "and". *} fixrec "map_tree·f·(Leaf·x) = Leaf·(f·x)" "map_tree·f·(Branch·ts) = Branch·(map_forest·f·ts)" and "map_forest·f·Empty = Empty" "ts ≠ ⊥ ==> map_forest·f·(Trees·t·ts) = Trees·(map_tree·f·t)·(map_forest·f·ts)" fixpat map_tree_strict [simp]: "map_tree·f·⊥" fixpat map_forest_strict [simp]: "map_forest·f·⊥" text {* Theorems generated: map_tree_def map_forest_def map_tree_unfold map_forest_unfold map_tree_simps map_forest_simps map_tree_map_forest_induct *} end