# HG changeset patch # User bulwahn # Date 1242461941 -7200 # Node ID beb26c5901f3172d2df7a2a10633236fe5393ab6 # Parent c6efe82fc652b182925580a80e831da515bc49ed# Parent 8448ba49d6816e5666fbbb4ab3846a5e06694c82 merged diff -r c6efe82fc652 -r beb26c5901f3 src/HOLCF/Algebraic.thy --- a/src/HOLCF/Algebraic.thy Fri May 15 15:56:28 2009 +0200 +++ b/src/HOLCF/Algebraic.thy Sat May 16 10:19:01 2009 +0200 @@ -29,6 +29,11 @@ thus "P i j" using step trans by (rule less_Suc_induct) qed +definition + eventual_iterate :: "('a \ 'a::cpo) \ ('a \ 'a)" +where + "eventual_iterate f = eventual (\n. iterate n\f)" + text {* A pre-deflation is like a deflation, but not idempotent. *} locale pre_deflation = @@ -103,9 +108,10 @@ abbreviation d :: "'a \ 'a" where - "d \ eventual (\n. iterate n\f)" + "d \ eventual_iterate f" lemma MOST_d: "MOST n. P (iterate n\f) \ P d" +unfolding eventual_iterate_def using eventually_constant_iterate by (rule MOST_eventual) lemma f_d: "f\(d\x) = d\x" @@ -134,6 +140,7 @@ proof fix x :: 'a have "d \ range (\n. iterate n\f)" + unfolding eventual_iterate_def using eventually_constant_iterate by (rule eventual_mem_range) then obtain n where n: "d = iterate n\f" .. @@ -153,9 +160,17 @@ by (simp add: d_fixed_iff) qed +lemma deflation_d: "deflation d" +using finite_deflation_d +by (rule finite_deflation_imp_deflation) + end -lemma pre_deflation_d_f: +lemma finite_deflation_eventual_iterate: + "pre_deflation d \ finite_deflation (eventual_iterate d)" +by (rule pre_deflation.finite_deflation_d) + +lemma pre_deflation_oo: assumes "finite_deflation d" assumes f: "\x. f\x \ x" shows "pre_deflation (d oo f)" @@ -171,13 +186,13 @@ lemma eventual_iterate_oo_fixed_iff: assumes "finite_deflation d" assumes f: "\x. f\x \ x" - shows "eventual (\n. iterate n\(d oo f))\x = x \ d\x = x \ f\x = x" + shows "eventual_iterate (d oo f)\x = x \ d\x = x \ f\x = x" proof - interpret d: finite_deflation d by fact let ?e = "d oo f" interpret e: pre_deflation "d oo f" using `finite_deflation d` f - by (rule pre_deflation_d_f) + by (rule pre_deflation_oo) let ?g = "eventual (\n. iterate n\?e)" show ?thesis apply (subst e.d_fixed_iff) @@ -192,6 +207,94 @@ done qed +lemma eventual_mono: + assumes A: "eventually_constant A" + assumes B: "eventually_constant B" + assumes below: "\n. A n \ B n" + shows "eventual A \ eventual B" +proof - + from A have "MOST n. A n = eventual A" + by (rule MOST_eq_eventual) + then have "MOST n. eventual A \ B n" + by (rule MOST_mono) (erule subst, rule below) + with B show "eventual A \ eventual B" + by (rule MOST_eventual) +qed + +lemma eventual_iterate_mono: + assumes f: "pre_deflation f" and g: "pre_deflation g" and "f \ g" + shows "eventual_iterate f \ eventual_iterate g" +unfolding eventual_iterate_def +apply (rule eventual_mono) +apply (rule pre_deflation.eventually_constant_iterate [OF f]) +apply (rule pre_deflation.eventually_constant_iterate [OF g]) +apply (rule monofun_cfun_arg [OF `f \ g`]) +done + +lemma cont2cont_eventual_iterate_oo: + assumes d: "finite_deflation d" + assumes cont: "cont f" and below: "\x y. f x\y \ y" + shows "cont (\x. eventual_iterate (d oo f x))" + (is "cont ?e") +proof (rule contI2) + show "monofun ?e" + apply (rule monofunI) + apply (rule eventual_iterate_mono) + apply (rule pre_deflation_oo [OF d below]) + apply (rule pre_deflation_oo [OF d below]) + apply (rule monofun_cfun_arg) + apply (erule cont2monofunE [OF cont]) + done +next + fix Y :: "nat \ 'b" + assume Y: "chain Y" + with cont have fY: "chain (\i. f (Y i))" + by (rule ch2ch_cont) + assume eY: "chain (\i. ?e (Y i))" + have lub_below: "\x. f (\i. Y i)\x \ x" + by (rule admD [OF _ Y], simp add: cont, rule below) + have "deflation (?e (\i. Y i))" + apply (rule pre_deflation.deflation_d) + apply (rule pre_deflation_oo [OF d lub_below]) + done + then show "?e (\i. Y i) \ (\i. ?e (Y i))" + proof (rule deflation.belowI) + fix x :: 'a + assume "?e (\i. Y i)\x = x" + hence "d\x = x" and "f (\i. Y i)\x = x" + by (simp_all add: eventual_iterate_oo_fixed_iff [OF d lub_below]) + hence "(\i. f (Y i)\x) = x" + apply (simp only: cont2contlubE [OF cont Y]) + apply (simp only: contlub_cfun_fun [OF fY]) + done + have "compact (d\x)" + using d by (rule finite_deflation.compact) + then have "compact x" + using `d\x = x` by simp + then have "compact (\i. f (Y i)\x)" + using `(\i. f (Y i)\x) = x` by simp + then have "\n. max_in_chain n (\i. f (Y i)\x)" + by - (rule compact_imp_max_in_chain, simp add: fY, assumption) + then obtain n where n: "max_in_chain n (\i. f (Y i)\x)" .. + then have "f (Y n)\x = x" + using `(\i. f (Y i)\x) = x` fY by (simp add: maxinch_is_thelub) + with `d\x = x` have "?e (Y n)\x = x" + by (simp add: eventual_iterate_oo_fixed_iff [OF d below]) + moreover have "?e (Y n)\x \ (\i. ?e (Y i)\x)" + by (rule is_ub_thelub, simp add: eY) + ultimately have "x \ (\i. ?e (Y i))\x" + by (simp add: contlub_cfun_fun eY) + also have "(\i. ?e (Y i))\x \ x" + apply (rule deflation.below) + apply (rule admD [OF adm_deflation eY]) + apply (rule pre_deflation.deflation_d) + apply (rule pre_deflation_oo [OF d below]) + done + finally show "(\i. ?e (Y i))\x = x" .. + qed +qed + + subsection {* Type constructor for finite deflations *} defaultsort profinite @@ -214,6 +317,10 @@ lemma finite_deflation_Rep_fin_defl: "finite_deflation (Rep_fin_defl d)" using Rep_fin_defl by simp +lemma deflation_Rep_fin_defl: "deflation (Rep_fin_defl d)" +using finite_deflation_Rep_fin_defl +by (rule finite_deflation_imp_deflation) + interpretation Rep_fin_defl: finite_deflation "Rep_fin_defl d" by (rule finite_deflation_Rep_fin_defl) @@ -244,27 +351,69 @@ subsection {* Take function for finite deflations *} definition + defl_approx :: "nat \ ('a \ 'a) \ ('a \ 'a)" +where + "defl_approx i d = eventual_iterate (approx i oo d)" + +lemma finite_deflation_defl_approx: + "deflation d \ finite_deflation (defl_approx i d)" +unfolding defl_approx_def +apply (rule pre_deflation.finite_deflation_d) +apply (rule pre_deflation_oo) +apply (rule finite_deflation_approx) +apply (erule deflation.below) +done + +lemma deflation_defl_approx: + "deflation d \ deflation (defl_approx i d)" +apply (rule finite_deflation_imp_deflation) +apply (erule finite_deflation_defl_approx) +done + +lemma defl_approx_fixed_iff: + "deflation d \ defl_approx i d\x = x \ approx i\x = x \ d\x = x" +unfolding defl_approx_def +apply (rule eventual_iterate_oo_fixed_iff) +apply (rule finite_deflation_approx) +apply (erule deflation.below) +done + +lemma defl_approx_below: + "\a \ b; deflation a; deflation b\ \ defl_approx i a \ defl_approx i b" +apply (rule deflation.belowI) +apply (erule deflation_defl_approx) +apply (simp add: defl_approx_fixed_iff) +apply (erule (1) deflation.belowD) +apply (erule conjunct2) +done + +lemma cont2cont_defl_approx: + assumes cont: "cont f" and below: "\x y. f x\y \ y" + shows "cont (\x. defl_approx i (f x))" +unfolding defl_approx_def +using finite_deflation_approx assms +by (rule cont2cont_eventual_iterate_oo) + +definition fd_take :: "nat \ 'a fin_defl \ 'a fin_defl" where - "fd_take i d = Abs_fin_defl (eventual (\n. iterate n\(approx i oo Rep_fin_defl d)))" + "fd_take i d = Abs_fin_defl (defl_approx i (Rep_fin_defl d))" lemma Rep_fin_defl_fd_take: - "Rep_fin_defl (fd_take i d) = - eventual (\n. iterate n\(approx i oo Rep_fin_defl d))" + "Rep_fin_defl (fd_take i d) = defl_approx i (Rep_fin_defl d)" unfolding fd_take_def apply (rule Abs_fin_defl_inverse [unfolded mem_Collect_eq]) -apply (rule pre_deflation.finite_deflation_d) -apply (rule pre_deflation_d_f) -apply (rule finite_deflation_approx) -apply (rule Rep_fin_defl.below) +apply (rule finite_deflation_defl_approx) +apply (rule deflation_Rep_fin_defl) done lemma fd_take_fixed_iff: "Rep_fin_defl (fd_take i d)\x = x \ approx i\x = x \ Rep_fin_defl d\x = x" unfolding Rep_fin_defl_fd_take -by (rule eventual_iterate_oo_fixed_iff - [OF finite_deflation_approx Rep_fin_defl.below]) +apply (rule defl_approx_fixed_iff) +apply (rule deflation_Rep_fin_defl) +done lemma fd_take_below: "fd_take n d \ d" apply (rule fin_defl_belowI) @@ -463,6 +612,41 @@ interpretation cast: deflation "cast\d" by (rule deflation_cast) +lemma cast_approx: "cast\(approx n\A) = defl_approx n (cast\A)" +apply (rule alg_defl.principal_induct) +apply (rule adm_eq) +apply simp +apply (simp add: cont2cont_defl_approx cast.below) +apply (simp only: approx_alg_defl_principal) +apply (simp only: cast_alg_defl_principal) +apply (simp only: Rep_fin_defl_fd_take) +done + +lemma cast_approx_fixed_iff: + "cast\(approx i\A)\x = x \ approx i\x = x \ cast\A\x = x" +apply (simp only: cast_approx) +apply (rule defl_approx_fixed_iff) +apply (rule deflation_cast) +done + +lemma defl_approx_cast: "defl_approx i (cast\A) = cast\(approx i\A)" +by (rule cast_approx [symmetric]) + +lemma cast_below_imp_below: "cast\A \ cast\B \ A \ B" +apply (rule profinite_below_ext) +apply (drule_tac i=i in defl_approx_below) +apply (rule deflation_cast) +apply (rule deflation_cast) +apply (simp only: defl_approx_cast) +apply (cut_tac x="approx i\A" in alg_defl.compact_imp_principal) +apply (rule compact_approx) +apply (cut_tac x="approx i\B" in alg_defl.compact_imp_principal) +apply (rule compact_approx) +apply clarsimp +apply (simp add: cast_alg_defl_principal) +apply (simp add: below_fin_defl_def) +done + lemma "cast\(\i. alg_defl_principal (Abs_fin_defl (approx i)))\x = x" apply (subst contlub_cfun_arg) apply (rule chainI) diff -r c6efe82fc652 -r beb26c5901f3 src/HOLCF/Tools/domain/domain_extender.ML --- a/src/HOLCF/Tools/domain/domain_extender.ML Fri May 15 15:56:28 2009 +0200 +++ b/src/HOLCF/Tools/domain/domain_extender.ML Sat May 16 10:19:01 2009 +0200 @@ -6,11 +6,13 @@ signature DOMAIN_EXTENDER = sig - val add_domain_cmd: string -> (string list * binding * mixfix * - (binding * (bool * binding option * string) list * mixfix) list) list + val add_domain_cmd: string -> + ((string * string option) list * binding * mixfix * + (binding * (bool * binding option * string) list * mixfix) list) list -> theory -> theory - val add_domain: string -> (string list * binding * mixfix * - (binding * (bool * binding option * typ) list * mixfix) list) list + val add_domain: string -> + ((string * string option) list * binding * mixfix * + (binding * (bool * binding option * typ) list * mixfix) list) list -> theory -> theory end; @@ -22,7 +24,7 @@ (* ----- general testing and preprocessing of constructor list -------------- *) fun check_and_sort_domain (dtnvs : (string * typ list) list) - (cons'' : ((binding * (bool * binding option * typ) list * mixfix) list) list) + (cons'' : (binding * (bool * binding option * typ) list * mixfix) list list) (sg : theory) : ((string * typ list) * (binding * (bool * binding option * typ) list * mixfix) list) list = @@ -73,9 +75,15 @@ quote (string_of_typ sg t) ^ " with different arguments")) | analyse indirect (TVar _) = Imposs "extender:analyse"; - fun check_pcpo T = if pcpo_type sg T then T - else error("Constructor argument type is not of sort pcpo: "^string_of_typ sg T); - val analyse_con = upd_second (map (upd_third (check_pcpo o analyse false))); + fun check_pcpo lazy T = + let val ok = if lazy then cpo_type else pcpo_type + in if ok sg T then T else error + ("Constructor argument type is not of sort pcpo: " ^ + string_of_typ sg T) + end; + fun analyse_arg (lazy, sel, T) = + (lazy, sel, check_pcpo lazy (analyse false T)); + fun analyse_con (b, args, mx) = (b, map analyse_arg args, mx); in ((dname,distinct_typevars), map analyse_con cons') end; in ListPair.map analyse_equation (dtnvs,cons'') end; (* let *) @@ -85,12 +93,16 @@ fun gen_add_domain (prep_typ : theory -> 'a -> typ) (comp_dnam : string) - (eqs''' : (string list * binding * mixfix * + (eqs''' : ((string * string option) list * binding * mixfix * (binding * (bool * binding option * 'a) list * mixfix) list) list) (thy''' : theory) = let + fun readS (SOME s) = Syntax.read_sort_global thy''' s + | readS NONE = Sign.defaultS thy'''; + fun readTFree (a, s) = TFree (a, readS s); + val dtnvs = map (fn (vs,dname:binding,mx,_) => - (dname, map (Syntax.read_typ_global thy''') vs, mx)) eqs'''; + (dname, map readTFree vs, mx)) eqs'''; val cons''' = map (fn (_,_,_,cons) => cons) eqs'''; fun thy_type (dname,tvars,mx) = (dname, length tvars, mx); fun thy_arity (dname,tvars,mx) = (Sign.full_name thy''' dname, map (snd o dest_TFree) tvars, pcpoS); @@ -148,10 +160,10 @@ val cons_decl = P.binding -- Scan.repeat dest_decl -- P.opt_mixfix; -val type_var' = - (P.type_ident ^^ Scan.optional (P.$$$ "::" ^^ P.!!! P.sort) ""); +val type_var' : (string * string option) parser = + (P.type_ident -- Scan.option (P.$$$ "::" |-- P.!!! P.sort)); -val type_args' = +val type_args' : (string * string option) list parser = type_var' >> single || P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") || Scan.succeed []; @@ -164,11 +176,12 @@ Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.and_list1 domain_decl; -fun mk_domain (opt_name : string option, doms : (((string list * binding) * mixfix) * +fun mk_domain (opt_name : string option, + doms : ((((string * string option) list * binding) * mixfix) * ((binding * (bool * binding option * string) list) * mixfix) list) list ) = let val names = map (fn (((_, t), _), _) => Binding.name_of t) doms; - val specs : (string list * binding * mixfix * + val specs : ((string * string option) list * binding * mixfix * (binding * (bool * binding option * string) list * mixfix) list) list = map (fn (((vs, t), mx), cons) => (vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms; diff -r c6efe82fc652 -r beb26c5901f3 src/HOLCF/Tools/domain/domain_library.ML --- a/src/HOLCF/Tools/domain/domain_library.ML Fri May 15 15:56:28 2009 +0200 +++ b/src/HOLCF/Tools/domain/domain_library.ML Sat May 16 10:19:01 2009 +0200 @@ -52,6 +52,7 @@ signature DOMAIN_LIBRARY = sig val Imposs : string -> 'a; + val cpo_type : theory -> typ -> bool; val pcpo_type : theory -> typ -> bool; val string_of_typ : theory -> typ -> string; @@ -190,6 +191,7 @@ | index_vnames([],occupied) = []; in index_vnames(map nonreserved ids, [("O",0),("o",0)]) end; +fun cpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort cpo}); fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort pcpo}); fun string_of_typ sg = Syntax.string_of_typ_global sg o Sign.certify_typ sg; diff -r c6efe82fc652 -r beb26c5901f3 src/HOLCF/Tools/domain/domain_theorems.ML --- a/src/HOLCF/Tools/domain/domain_theorems.ML Fri May 15 15:56:28 2009 +0200 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML Sat May 16 10:19:01 2009 +0200 @@ -12,6 +12,8 @@ sig val theorems: Domain_Library.eq * Domain_Library.eq list -> theory -> thm list * theory; val comp_theorems: bstring * Domain_Library.eq list -> theory -> thm list * theory; + val quiet_mode: bool ref; + val trace_domain: bool ref; end; structure Domain_Theorems :> DOMAIN_THEOREMS =