# HG changeset patch # User bulwahn # Date 1274333810 -7200 # Node ID 8096a4c755ebed71a58debb1237a952361e961be # Parent 4ba91ea2bf6d4d70eeaef26c69732a120a4357cd# Parent 41a22e7c11450a96d45f9653afe79ac112ddf989 merged diff -r 4ba91ea2bf6d -r 8096a4c755eb src/HOL/NSA/Examples/NSPrimes.thy --- a/src/HOL/NSA/Examples/NSPrimes.thy Thu May 20 07:34:45 2010 +0200 +++ b/src/HOL/NSA/Examples/NSPrimes.thy Thu May 20 07:36:50 2010 +0200 @@ -13,9 +13,7 @@ text{*These can be used to derive an alternative proof of the infinitude of primes by considering a property of nonstandard sets.*} -definition - hdvd :: "[hypnat, hypnat] => bool" (infixl "hdvd" 50) where - [transfer_unfold]: "(M::hypnat) hdvd N = ( *p2* (op dvd)) M N" +declare dvd_def [transfer_refold] definition starprime :: "hypnat set" where @@ -49,14 +47,14 @@ (* Goldblatt: Exercise 5.11(2) - p. 57 *) -lemma hdvd_by_all: "\M. \N. 0 < N & (\m. 0 < m & (m::hypnat) <= M --> m hdvd N)" +lemma hdvd_by_all: "\M. \N. 0 < N & (\m. 0 < m & (m::hypnat) <= M --> m dvd N)" by (transfer, rule dvd_by_all) lemmas hdvd_by_all2 = hdvd_by_all [THEN spec, standard] (* Goldblatt: Exercise 5.11(2) - p. 57 *) lemma hypnat_dvd_all_hypnat_of_nat: - "\(N::hypnat). 0 < N & (\n \ -{0::nat}. hypnat_of_nat(n) hdvd N)" + "\(N::hypnat). 0 < N & (\n \ -{0::nat}. hypnat_of_nat(n) dvd N)" apply (cut_tac hdvd_by_all) apply (drule_tac x = whn in spec, auto) apply (rule exI, auto) @@ -70,7 +68,7 @@ (* Goldblatt: Exercise 5.11(3a) - p 57 *) lemma starprime: - "starprime = {p. 1 < p & (\m. m hdvd p --> m = 1 | m = p)}" + "starprime = {p. 1 < p & (\m. m dvd p --> m = 1 | m = p)}" by (transfer, auto simp add: prime_def) lemma prime_two: "prime 2" @@ -88,13 +86,11 @@ apply (rule_tac x = n in exI, auto) apply (drule conjI [THEN not_prime_ex_mk], auto) apply (drule_tac x = m in spec, auto) -apply (rule_tac x = ka in exI) -apply (auto intro: dvd_mult2) done (* Goldblatt Exercise 5.11(3b) - p 57 *) lemma hyperprime_factor_exists [rule_format]: - "!!n. 1 < n ==> (\k \ starprime. k hdvd n)" + "!!n. 1 < n ==> (\k \ starprime. k dvd n)" by (transfer, simp add: prime_factor_exists) (* Goldblatt Exercise 3.10(1) - p. 29 *) @@ -257,14 +253,14 @@ subsection{*Existence of Infinitely Many Primes: a Nonstandard Proof*} -lemma lemma_not_dvd_hypnat_one: "~ (\n \ - {0}. hypnat_of_nat n hdvd 1)" +lemma lemma_not_dvd_hypnat_one: "~ (\n \ - {0}. hypnat_of_nat n dvd 1)" apply auto apply (rule_tac x = 2 in bexI) apply (transfer, auto) done declare lemma_not_dvd_hypnat_one [simp] -lemma lemma_not_dvd_hypnat_one2: "\n \ - {0}. ~ hypnat_of_nat n hdvd 1" +lemma lemma_not_dvd_hypnat_one2: "\n \ - {0}. ~ hypnat_of_nat n dvd 1" apply (cut_tac lemma_not_dvd_hypnat_one) apply (auto simp del: lemma_not_dvd_hypnat_one) done @@ -314,13 +310,13 @@ by (cut_tac hypnat_of_nat_one_not_prime, simp) declare hypnat_one_not_prime [simp] -lemma hdvd_diff: "!!k m n. [| k hdvd m; k hdvd n |] ==> k hdvd (m - n)" -by (transfer, rule dvd_diff) +lemma hdvd_diff: "!!k m n :: hypnat. [| k dvd m; k dvd n |] ==> k dvd (m - n)" +by (transfer, rule dvd_diff_nat) lemma dvd_one_eq_one: "x dvd (1::nat) ==> x = 1" by (unfold dvd_def, auto) -lemma hdvd_one_eq_one: "!!x. x hdvd 1 ==> x = 1" +lemma hdvd_one_eq_one: "!!x. x dvd (1::hypnat) ==> x = 1" by (transfer, rule dvd_one_eq_one) theorem not_finite_prime: "~ finite {p. prime p}" diff -r 4ba91ea2bf6d -r 8096a4c755eb src/HOLCF/Fixrec.thy --- a/src/HOLCF/Fixrec.thy Thu May 20 07:34:45 2010 +0200 +++ b/src/HOLCF/Fixrec.thy Thu May 20 07:36:50 2010 +0200 @@ -65,30 +65,6 @@ == "CONST maybe_when\t1\(\ x. t2)\m" -subsubsection {* Monadic bind operator *} - -definition - bind :: "'a maybe \ ('a \ 'b maybe) \ 'b maybe" where - "bind = (\ m f. case m of fail \ fail | return\x \ f\x)" - -text {* monad laws *} - -lemma bind_strict [simp]: "bind\\\f = \" -by (simp add: bind_def) - -lemma bind_fail [simp]: "bind\fail\f = fail" -by (simp add: bind_def) - -lemma left_unit [simp]: "bind\(return\a)\k = k\a" -by (simp add: bind_def) - -lemma right_unit [simp]: "bind\m\return = m" -by (rule_tac p=m in maybeE, simp_all) - -lemma bind_assoc: - "bind\(bind\m\k)\h = bind\m\(\ a. bind\(k\a)\h)" -by (rule_tac p=m in maybeE, simp_all) - subsubsection {* Run operator *} definition @@ -169,7 +145,7 @@ definition branch :: "('a \ 'b maybe) \ ('b \ 'c) \ ('a \ 'c maybe)" where - "branch p \ \ r x. bind\(p\x)\(\ y. return\(r\y))" + "branch p \ \ r x. maybe_when\fail\(\ y. return\(r\y))\(p\x)" lemma branch_rews: "p\x = \ \ branch p\r\x = \" @@ -277,7 +253,7 @@ definition cpair_pat :: "('a, 'c) pat \ ('b, 'd) pat \ ('a \ 'b, 'c \ 'd) pat" where "cpair_pat p1 p2 = (\(x, y). - bind\(p1\x)\(\ a. bind\(p2\y)\(\ b. return\(a, b))))" + maybe_when\fail\(\ a. maybe_when\fail\(\ b. return\(a, b))\(p2\y))\(p1\x))" definition spair_pat :: @@ -425,7 +401,7 @@ definition as_pat :: "('a \ 'b maybe) \ 'a \ ('a \ 'b) maybe" where - "as_pat p = (\ x. bind\(p\x)\(\ a. return\(x, a)))" + "as_pat p = (\ x. maybe_when\fail\(\ a. return\(x, a))\(p\x))" definition lazy_pat :: "('a \ 'b::pcpo maybe) \ ('a \ 'b maybe)" where @@ -608,7 +584,7 @@ (@{const_name UU}, @{const_name match_UU}) ] *} -hide_const (open) return bind fail run cases +hide_const (open) return fail run cases lemmas [fixrec_simp] = run_strict run_fail run_return diff -r 4ba91ea2bf6d -r 8096a4c755eb src/HOLCF/IsaMakefile --- a/src/HOLCF/IsaMakefile Thu May 20 07:34:45 2010 +0200 +++ b/src/HOLCF/IsaMakefile Thu May 20 07:36:50 2010 +0200 @@ -7,6 +7,7 @@ default: HOLCF images: HOLCF IOA test: HOLCF-IMP HOLCF-ex HOLCF-FOCUS \ + HOLCF-Tutorial \ IOA-ABP IOA-NTP IOA-Modelcheck IOA-Storage IOA-ex all: images test @@ -78,6 +79,19 @@ @$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/HOL HOLCF +## HOLCF-Tutorial + +HOLCF-Tutorial: HOLCF $(LOG)/HOLCF-Tutorial.gz + +$(LOG)/HOLCF-Tutorial.gz: $(OUT)/HOLCF \ + Tutorial/Domain_ex.thy \ + Tutorial/Fixrec_ex.thy \ + Tutorial/New_Domain.thy \ + Tutorial/document/root.tex \ + Tutorial/ROOT.ML + @$(ISABELLE_TOOL) usedir $(OUT)/HOLCF Tutorial + + ## HOLCF-IMP HOLCF-IMP: HOLCF $(LOG)/HOLCF-IMP.gz @@ -95,15 +109,12 @@ ../HOL/Library/Nat_Infinity.thy \ ex/Dagstuhl.thy \ ex/Dnat.thy \ - ex/Domain_ex.thy \ ex/Domain_Proofs.thy \ ex/Fix2.thy \ - ex/Fixrec_ex.thy \ ex/Focus_ex.thy \ ex/Hoare.thy \ ex/Letrec.thy \ ex/Loop.thy \ - ex/New_Domain.thy \ ex/Powerdomain_ex.thy \ ex/Stream.thy \ ex/Strict_Fun.thy \ @@ -201,4 +212,4 @@ $(LOG)/HOLCF-ex.gz $(LOG)/HOLCF-FOCUS.gz $(OUT)/IOA \ $(LOG)/IOA.gz $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz \ $(LOG)/IOA-Modelcheck.gz $(LOG)/IOA-Storage.gz \ - $(LOG)/IOA-ex.gz + $(LOG)/IOA-ex.gz $(LOG)/HOLCF-Tutorial.gz diff -r 4ba91ea2bf6d -r 8096a4c755eb src/HOLCF/Tools/Domain/domain_constructors.ML --- a/src/HOLCF/Tools/Domain/domain_constructors.ML Thu May 20 07:34:45 2010 +0200 +++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Thu May 20 07:36:50 2010 +0200 @@ -952,7 +952,7 @@ val (fun1, fun2, taken) = pat_lhs (pat, args); val defs = @{thm branch_def} :: pat_defs; val goal = mk_trp (mk_strict fun1); - val rules = @{thm Fixrec.bind_strict} :: case_rews; + val rules = @{thms maybe_when_rews} @ case_rews; val tacs = [simp_tac (beta_ss addsimps rules) 1]; in prove thy defs goal (K tacs) end; fun pat_apps (i, (pat, (con, args))) = @@ -967,7 +967,7 @@ val concl = mk_trp (mk_eq (fun1 ` con_app, rhs)); val goal = Logic.list_implies (assms, concl); val defs = @{thm branch_def} :: pat_defs; - val rules = @{thms bind_fail left_unit} @ case_rews; + val rules = @{thms maybe_when_rews} @ case_rews; val tacs = [asm_simp_tac (beta_ss addsimps rules) 1]; in prove thy defs goal (K tacs) end; in map_index pat_app spec end; diff -r 4ba91ea2bf6d -r 8096a4c755eb src/HOLCF/Tools/fixrec.ML --- a/src/HOLCF/Tools/fixrec.ML Thu May 20 07:34:45 2010 +0200 +++ b/src/HOLCF/Tools/fixrec.ML Thu May 20 07:36:50 2010 +0200 @@ -125,10 +125,20 @@ val (lhss, rhss) = ListPair.unzip (map (dest_eqs o snd) spec); val functional = lambda_tuple lhss (mk_tuple rhss); val fixpoint = mk_fix (mk_cabs functional); - + val cont_thm = - Goal.prove lthy [] [] (mk_trp (mk_cont functional)) - (K (simp_tac (simpset_of lthy) 1)); + let + val prop = mk_trp (mk_cont functional); + fun err () = error ( + "Continuity proof failed; please check that cont2cont rules\n" ^ + "are configured for all non-HOLCF constants.\n" ^ + "The error occurred for the goal statement:\n" ^ + Syntax.string_of_term lthy prop); + fun check th = case Thm.nprems_of th of 0 => all_tac th | n => err (); + val tac = simp_tac (simpset_of lthy) 1 THEN check; + in + Goal.prove lthy [] [] prop (K tac) + end; fun one_def (l as Free(n,_)) r = let val b = Long_Name.base_name n diff -r 4ba91ea2bf6d -r 8096a4c755eb src/HOLCF/Tutorial/Domain_ex.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Tutorial/Domain_ex.thy Thu May 20 07:36:50 2010 +0200 @@ -0,0 +1,211 @@ +(* Title: HOLCF/ex/Domain_ex.thy + Author: Brian Huffman +*) + +header {* Domain package examples *} + +theory Domain_ex +imports HOLCF +begin + +text {* Domain constructors are strict by default. *} + +domain d1 = d1a | d1b "d1" "d1" + +lemma "d1b\\\y = \" by simp + +text {* Constructors can be made lazy using the @{text "lazy"} keyword. *} + +domain d2 = d2a | d2b (lazy "d2") + +lemma "d2b\x \ \" by simp + +text {* Strict and lazy arguments may be mixed arbitrarily. *} + +domain d3 = d3a | d3b (lazy "d2") "d2" + +lemma "P (d3b\x\y = \) \ P (y = \)" by simp + +text {* Selectors can be used with strict or lazy constructor arguments. *} + +domain d4 = d4a | d4b (lazy d4b_left :: "d2") (d4b_right :: "d2") + +lemma "y \ \ \ d4b_left\(d4b\x\y) = x" by simp + +text {* Mixfix declarations can be given for data constructors. *} + +domain d5 = d5a | d5b (lazy "d5") "d5" (infixl ":#:" 70) + +lemma "d5a \ x :#: y :#: z" by simp + +text {* Mixfix declarations can also be given for type constructors. *} + +domain ('a, 'b) lazypair (infixl ":*:" 25) = + lpair (lazy lfst :: 'a) (lazy lsnd :: 'b) (infixl ":*:" 75) + +lemma "\p::('a :*: 'b). p \ lfst\p :*: lsnd\p" +by (rule allI, case_tac p, simp_all) + +text {* Non-recursive constructor arguments can have arbitrary types. *} + +domain ('a, 'b) d6 = d6 "int lift" "'a \ 'b u" (lazy "('a :*: 'b) \ ('b \ 'a)") + +text {* + Indirect recusion is allowed for sums, products, lifting, and the + continuous function space. However, the domain package does not + generate an induction rule in terms of the constructors. +*} + +domain 'a d7 = d7a "'a d7 \ int lift" | d7b "'a \ 'a d7" | d7c (lazy "'a d7 \ 'a") + -- "Indirect recursion detected, skipping proofs of (co)induction rules" + +text {* Note that @{text d7.induct} is absent. *} + +text {* + Indirect recursion is also allowed using previously-defined datatypes. +*} + +domain 'a slist = SNil | SCons 'a "'a slist" + +domain 'a stree = STip | SBranch "'a stree slist" + +text {* Mutually-recursive datatypes can be defined using the @{text "and"} keyword. *} + +domain d8 = d8a | d8b "d9" and d9 = d9a | d9b (lazy "d8") + +text {* Non-regular recursion is not allowed. *} +(* +domain ('a, 'b) altlist = ANil | ACons 'a "('b, 'a) altlist" + -- "illegal direct recursion with different arguments" +domain 'a nest = Nest1 'a | Nest2 "'a nest nest" + -- "illegal direct recursion with different arguments" +*) + +text {* + Mutually-recursive datatypes must have all the same type arguments, + not necessarily in the same order. +*} + +domain ('a, 'b) list1 = Nil1 | Cons1 'a "('b, 'a) list2" + and ('b, 'a) list2 = Nil2 | Cons2 'b "('a, 'b) list1" + +text {* Induction rules for flat datatypes have no admissibility side-condition. *} + +domain 'a flattree = Tip | Branch "'a flattree" "'a flattree" + +lemma "\P \; P Tip; \x y. \x \ \; y \ \; P x; P y\ \ P (Branch\x\y)\ \ P x" +by (rule flattree.induct) -- "no admissibility requirement" + +text {* Trivial datatypes will produce a warning message. *} + +domain triv = Triv triv triv + -- "domain @{text Domain_ex.triv} is empty!" + +lemma "(x::triv) = \" by (induct x, simp_all) + +text {* Lazy constructor arguments may have unpointed types. *} + +domain natlist = nnil | ncons (lazy "nat discr") natlist + +text {* Class constraints may be given for type parameters on the LHS. *} + +domain ('a::cpo) box = Box (lazy 'a) + + +subsection {* Generated constants and theorems *} + +domain 'a tree = Leaf (lazy 'a) | Node (left :: "'a tree") (right :: "'a tree") + +lemmas tree_abs_defined_iff = + iso.abs_defined_iff [OF iso.intro [OF tree.abs_iso tree.rep_iso]] + +text {* Rules about ismorphism *} +term tree_rep +term tree_abs +thm tree.rep_iso +thm tree.abs_iso +thm tree.iso_rews + +text {* Rules about constructors *} +term Leaf +term Node +thm Leaf_def Node_def +thm tree.nchotomy +thm tree.exhaust +thm tree.compacts +thm tree.con_rews +thm tree.dist_les +thm tree.dist_eqs +thm tree.inverts +thm tree.injects + +text {* Rules about case combinator *} +term tree_when +thm tree.tree_when_def +thm tree.when_rews + +text {* Rules about selectors *} +term left +term right +thm tree.sel_rews + +text {* Rules about discriminators *} +term is_Leaf +term is_Node +thm tree.dis_rews + +text {* Rules about pattern match combinators *} +term Leaf_pat +term Node_pat +thm tree.pat_rews + +text {* Rules about monadic pattern match combinators *} +term match_Leaf +term match_Node +thm tree.match_rews + +text {* Rules about take function *} +term tree_take +thm tree.take_def +thm tree.take_0 +thm tree.take_Suc +thm tree.take_rews +thm tree.chain_take +thm tree.take_take +thm tree.deflation_take +thm tree.take_below +thm tree.take_lemma +thm tree.lub_take +thm tree.reach +thm tree.finite_induct + +text {* Rules about finiteness predicate *} +term tree_finite +thm tree.finite_def +thm tree.finite (* only generated for flat datatypes *) + +text {* Rules about bisimulation predicate *} +term tree_bisim +thm tree.bisim_def +thm tree.coinduct + +text {* Induction rule *} +thm tree.induct + + +subsection {* Known bugs *} + +text {* Declaring a mixfix with spaces causes some strange parse errors. *} +(* +domain xx = xx ("x y") + -- "Inner syntax error: unexpected end of input" +*) + +text {* + Non-cpo type parameters currently do not work. +*} +(* +domain ('a::type) stream = snil | scons (lazy "'a discr") "'a stream" +*) + +end diff -r 4ba91ea2bf6d -r 8096a4c755eb src/HOLCF/Tutorial/Fixrec_ex.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Tutorial/Fixrec_ex.thy Thu May 20 07:36:50 2010 +0200 @@ -0,0 +1,246 @@ +(* Title: HOLCF/ex/Fixrec_ex.thy + Author: Brian Huffman +*) + +header {* Fixrec package examples *} + +theory Fixrec_ex +imports HOLCF +begin + +subsection {* Basic @{text fixrec} examples *} + +text {* + Fixrec patterns can mention any constructor defined by the domain + package, as well as any of the following built-in constructors: + Pair, spair, sinl, sinr, up, ONE, TT, FF. +*} + +text {* Typical usage is with lazy constructors. *} + +fixrec down :: "'a u \ 'a" +where "down\(up\x) = x" + +text {* With strict constructors, rewrite rules may require side conditions. *} + +fixrec from_sinl :: "'a \ 'b \ 'a" +where "x \ \ \ from_sinl\(sinl\x) = x" + +text {* Lifting can turn a strict constructor into a lazy one. *} + +fixrec from_sinl_up :: "'a u \ 'b \ 'a" +where "from_sinl_up\(sinl\(up\x)) = x" + +text {* Fixrec also works with the HOL pair constructor. *} + +fixrec down2 :: "'a u \ 'b u \ 'a \ 'b" +where "down2\(up\x, up\y) = (x, y)" + + +subsection {* Examples using @{text fixrec_simp} *} + +text {* A type of lazy lists. *} + +domain 'a llist = lNil | lCons (lazy 'a) (lazy "'a llist") + +text {* A zip function for lazy lists. *} + +text {* Notice that the patterns are not exhaustive. *} + +fixrec + lzip :: "'a llist \ 'b llist \ ('a \ 'b) llist" +where + "lzip\(lCons\x\xs)\(lCons\y\ys) = lCons\(x, y)\(lzip\xs\ys)" +| "lzip\lNil\lNil = lNil" + +text {* @{text fixrec_simp} is useful for producing strictness theorems. *} +text {* Note that pattern matching is done in left-to-right order. *} + +lemma lzip_stricts [simp]: + "lzip\\\ys = \" + "lzip\lNil\\ = \" + "lzip\(lCons\x\xs)\\ = \" +by fixrec_simp+ + +text {* @{text fixrec_simp} can also produce rules for missing cases. *} + +lemma lzip_undefs [simp]: + "lzip\lNil\(lCons\y\ys) = \" + "lzip\(lCons\x\xs)\lNil = \" +by fixrec_simp+ + + +subsection {* Pattern matching with bottoms *} + +text {* + As an alternative to using @{text fixrec_simp}, it is also possible + to use bottom as a constructor pattern. When using a bottom + pattern, the right-hand-side must also be bottom; otherwise, @{text + fixrec} will not be able to prove the equation. +*} + +fixrec + from_sinr_up :: "'a \ 'b\<^sub>\ \ 'b" +where + "from_sinr_up\\ = \" +| "from_sinr_up\(sinr\(up\x)) = x" + +text {* + If the function is already strict in that argument, then the bottom + pattern does not change the meaning of the function. For example, + in the definition of @{term from_sinr_up}, the first equation is + actually redundant, and could have been proven separately by + @{text fixrec_simp}. +*} + +text {* + A bottom pattern can also be used to make a function strict in a + certain argument, similar to a bang-pattern in Haskell. +*} + +fixrec + seq :: "'a \ 'b \ 'b" +where + "seq\\\y = \" +| "x \ \ \ seq\x\y = y" + + +subsection {* Skipping proofs of rewrite rules *} + +text {* Another zip function for lazy lists. *} + +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 :: "'a llist \ 'b llist \ ('a \ 'b) llist" +where + "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 @{text fixrec_simp}. *} + +lemma lzip2_simps [simp]: + "lzip2\(lCons\x\xs)\(lCons\y\ys) = lCons\(x, y)\(lzip\xs\ys)" + "lzip2\(lCons\x\xs)\lNil = lNil" + "lzip2\lNil\(lCons\y\ys) = lNil" + "lzip2\lNil\lNil = lNil" +by fixrec_simp+ + +lemma lzip2_stricts [simp]: + "lzip2\\\ys = \" + "lzip2\(lCons\x\xs)\\ = \" +by fixrec_simp+ + + +subsection {* Mutual recursion with @{text 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" + +text {* + To define mutually recursive functions, give multiple type signatures + separated by the keyword @{text "and"}. +*} + +fixrec + map_tree :: "('a \ 'b) \ ('a tree \ 'b tree)" +and + map_forest :: "('a \ 'b) \ ('a forest \ 'b forest)" +where + "map_tree\f\(Leaf\x) = Leaf\(f\x)" +| "map_tree\f\(Branch\ts) = Branch\(map_forest\f\ts)" +| "map_forest\f\Empty = Empty" +| "ts \ \ \ + map_forest\f\(Trees\t\ts) = Trees\(map_tree\f\t)\(map_forest\f\ts)" + +lemma map_tree_strict [simp]: "map_tree\f\\ = \" +by fixrec_simp + +lemma map_forest_strict [simp]: "map_forest\f\\ = \" +by fixrec_simp + +(* + Theorems generated: + @{text map_tree_def} @{thm map_tree_def} + @{text map_forest_def} @{thm map_forest_def} + @{text map_tree.unfold} @{thm map_tree.unfold} + @{text map_forest.unfold} @{thm map_forest.unfold} + @{text map_tree.simps} @{thm map_tree.simps} + @{text map_forest.simps} @{thm map_forest.simps} + @{text map_tree_map_forest.induct} @{thm map_tree_map_forest.induct} +*) + + +subsection {* Looping simp rules *} + +text {* + The defining equations of a fixrec definition are declared as simp + rules by default. In some cases, especially for constants with no + arguments or functions with variable patterns, the defining + equations may cause the simplifier to loop. In these cases it will + be necessary to use a @{text "[simp del]"} declaration. +*} + +fixrec + repeat :: "'a \ 'a llist" +where + [simp del]: "repeat\x = lCons\x\(repeat\x)" + +text {* + We can derive other non-looping simp rules for @{const repeat} by + using the @{text subst} method with the @{text repeat.simps} rule. +*} + +lemma repeat_simps [simp]: + "repeat\x \ \" + "repeat\x \ lNil" + "repeat\x = lCons\y\ys \ x = y \ repeat\x = ys" +by (subst repeat.simps, simp)+ + +lemma llist_when_repeat [simp]: + "llist_when\z\f\(repeat\x) = f\x\(repeat\x)" +by (subst repeat.simps, simp) + +text {* + For mutually-recursive constants, looping might only occur if all + equations are in the simpset at the same time. In such cases it may + only be necessary to declare @{text "[simp del]"} on one equation. +*} + +fixrec + inf_tree :: "'a tree" and inf_forest :: "'a forest" +where + [simp del]: "inf_tree = Branch\inf_forest" +| "inf_forest = Trees\inf_tree\(Trees\inf_tree\Empty)" + + +subsection {* Using @{text fixrec} inside locales *} + +locale test = + fixes foo :: "'a \ 'a" + assumes foo_strict: "foo\\ = \" +begin + +fixrec + bar :: "'a u \ 'a" +where + "bar\(up\x) = foo\x" + +lemma bar_strict: "bar\\ = \" +by fixrec_simp + +end + +end diff -r 4ba91ea2bf6d -r 8096a4c755eb src/HOLCF/Tutorial/New_Domain.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Tutorial/New_Domain.thy Thu May 20 07:36:50 2010 +0200 @@ -0,0 +1,92 @@ +(* Title: HOLCF/ex/New_Domain.thy + Author: Brian Huffman +*) + +header {* Definitional domain package *} + +theory New_Domain +imports HOLCF +begin + +text {* + The definitional domain package only works with representable domains, + i.e. types in class @{text rep}. +*} + +default_sort rep + +text {* + Provided that @{text rep} is the default sort, the @{text new_domain} + package should work with any type definition supported by the old + domain package. +*} + +new_domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist") + +text {* + The difference is that the new domain package is completely + definitional, and does not generate any axioms. The following type + and constant definitions are not produced by the old domain package. +*} + +thm type_definition_llist +thm llist_abs_def llist_rep_def + +text {* + The new domain package also adds support for indirect recursion with + user-defined datatypes. This definition of a tree datatype uses + indirect recursion through the lazy list type constructor. +*} + +new_domain 'a ltree = Leaf (lazy 'a) | Branch (lazy "'a ltree llist") + +text {* + For indirect-recursive definitions, the domain package is not able to + generate a high-level induction rule. (It produces a warning + message instead.) The low-level reach lemma (now proved as a + theorem, no longer generated as an axiom) can be used to derive + other induction rules. +*} + +thm ltree.reach + +text {* + The definition of the take function uses map functions associated with + each type constructor involved in the definition. A map function + for the lazy list type has been generated by the new domain package. +*} + +thm ltree.take_rews +thm llist_map_def + +lemma ltree_induct: + fixes P :: "'a ltree \ bool" + assumes adm: "adm P" + assumes bot: "P \" + assumes Leaf: "\x. P (Leaf\x)" + assumes Branch: "\f l. \x. P (f\x) \ P (Branch\(llist_map\f\l))" + shows "P x" +proof - + have "P (\i. ltree_take i\x)" + using adm + proof (rule admD) + fix i + show "P (ltree_take i\x)" + proof (induct i arbitrary: x) + case (0 x) + show "P (ltree_take 0\x)" by (simp add: bot) + next + case (Suc n x) + show "P (ltree_take (Suc n)\x)" + apply (cases x) + apply (simp add: bot) + apply (simp add: Leaf) + apply (simp add: Branch Suc) + done + qed + qed (simp add: ltree.chain_take) + thus ?thesis + by (simp add: ltree.reach) +qed + +end diff -r 4ba91ea2bf6d -r 8096a4c755eb src/HOLCF/Tutorial/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Tutorial/ROOT.ML Thu May 20 07:36:50 2010 +0200 @@ -0,0 +1,1 @@ +use_thys ["Domain_ex", "Fixrec_ex", "New_Domain"]; diff -r 4ba91ea2bf6d -r 8096a4c755eb src/HOLCF/Tutorial/document/root.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Tutorial/document/root.tex Thu May 20 07:36:50 2010 +0200 @@ -0,0 +1,29 @@ + +% HOLCF/document/root.tex + +\documentclass[11pt,a4paper]{article} +\usepackage{graphicx,isabelle,isabellesym,latexsym} +\usepackage[only,bigsqcap]{stmaryrd} +\usepackage[latin1]{inputenc} +\usepackage{pdfsetup} + +\urlstyle{rm} +%\isabellestyle{it} +\pagestyle{myheadings} + +\begin{document} + +\title{Isabelle/HOLCF Tutorial} +\maketitle + +\tableofcontents + +%\newpage + +%\renewcommand{\isamarkupheader}[1]% +%{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}} + +\parindent 0pt\parskip 0.5ex +\input{session} + +\end{document} diff -r 4ba91ea2bf6d -r 8096a4c755eb src/HOLCF/ex/Domain_ex.thy --- a/src/HOLCF/ex/Domain_ex.thy Thu May 20 07:34:45 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,210 +0,0 @@ -(* Title: HOLCF/ex/Domain_ex.thy - Author: Brian Huffman -*) - -header {* Domain package examples *} - -theory Domain_ex -imports HOLCF -begin - -text {* Domain constructors are strict by default. *} - -domain d1 = d1a | d1b "d1" "d1" - -lemma "d1b\\\y = \