# HG changeset patch # User huffman # Date 1287272346 25200 # Node ID 98f2d8280eb4636589524c19d8baac10797433e0 # Parent 8f8f18a8868501be694aa5eadd2d2899b0f64c87# Parent b253319c9a95ad87274fc93eb9782f59ff6ee86e merged diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/Adm.thy --- a/src/HOLCF/Adm.thy Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/Adm.thy Sat Oct 16 16:39:06 2010 -0700 @@ -48,52 +48,52 @@ subsection {* Admissibility of special formulae and propagation *} -lemma adm_not_free: "adm (\x. t)" +lemma adm_const [simp]: "adm (\x. t)" by (rule admI, simp) -lemma adm_conj: "\adm P; adm Q\ \ adm (\x. P x \ Q x)" +lemma adm_conj [simp]: + "\adm (\x. P x); adm (\x. Q x)\ \ adm (\x. P x \ Q x)" by (fast intro: admI elim: admD) -lemma adm_all: "(\y. adm (\x. P x y)) \ adm (\x. \y. P x y)" +lemma adm_all [simp]: + "(\y. adm (\x. P x y)) \ adm (\x. \y. P x y)" by (fast intro: admI elim: admD) -lemma adm_ball: "(\y. y \ A \ adm (\x. P x y)) \ adm (\x. \y\A. P x y)" +lemma adm_ball [simp]: + "(\y. y \ A \ adm (\x. P x y)) \ adm (\x. \y\A. P x y)" by (fast intro: admI elim: admD) -text {* Admissibility for disjunction is hard to prove. It takes 5 Lemmas *} - -lemma adm_disj_lemma1: - "\chain (Y::nat \ 'a::cpo); \i. \j\i. P (Y j)\ - \ chain (\i. Y (LEAST j. i \ j \ P (Y j)))" -apply (rule chainI) -apply (erule chain_mono) -apply (rule Least_le) -apply (rule LeastI2_ex) -apply simp_all -done - -lemmas adm_disj_lemma2 = LeastI_ex [of "\j. i \ j \ P (Y j)", standard] +text {* Admissibility for disjunction is hard to prove. It requires 2 lemmas. *} -lemma adm_disj_lemma3: - "\chain (Y::nat \ 'a::cpo); \i. \j\i. P (Y j)\ \ - (\i. Y i) = (\i. Y (LEAST j. i \ j \ P (Y j)))" - apply (frule (1) adm_disj_lemma1) - apply (rule below_antisym) - apply (rule lub_mono, assumption+) - apply (erule chain_mono) - apply (simp add: adm_disj_lemma2) - apply (rule lub_range_mono, fast, assumption+) -done +lemma adm_disj_lemma1: + assumes adm: "adm P" + assumes chain: "chain Y" + assumes P: "\i. \j\i. P (Y j)" + shows "P (\i. Y i)" +proof - + def f \ "\i. LEAST j. i \ j \ P (Y j)" + have chain': "chain (\i. Y (f i))" + unfolding f_def + apply (rule chainI) + apply (rule chain_mono [OF chain]) + apply (rule Least_le) + apply (rule LeastI2_ex) + apply (simp_all add: P) + done + have f1: "\i. i \ f i" and f2: "\i. P (Y (f i))" + using LeastI_ex [OF P [rule_format]] by (simp_all add: f_def) + have lub_eq: "(\i. Y i) = (\i. Y (f i))" + apply (rule below_antisym) + apply (rule lub_mono [OF chain chain']) + apply (rule chain_mono [OF chain f1]) + apply (rule lub_range_mono [OF _ chain chain']) + apply clarsimp + done + show "P (\i. Y i)" + unfolding lub_eq using adm chain' f2 by (rule admD) +qed -lemma adm_disj_lemma4: - "\adm P; chain Y; \i. \j\i. P (Y j)\ \ P (\i. Y i)" -apply (subst adm_disj_lemma3, assumption+) -apply (erule admD) -apply (simp add: adm_disj_lemma1) -apply (simp add: adm_disj_lemma2) -done - -lemma adm_disj_lemma5: +lemma adm_disj_lemma2: "\n::nat. P n \ Q n \ (\i. \j\i. P j) \ (\i. \j\i. Q j)" apply (erule contrapos_pp) apply (clarsimp, rename_tac a b) @@ -101,28 +101,27 @@ apply simp done -lemma adm_disj: "\adm P; adm Q\ \ adm (\x. P x \ Q x)" +lemma adm_disj [simp]: + "\adm (\x. P x); adm (\x. Q x)\ \ adm (\x. P x \ Q x)" apply (rule admI) -apply (erule adm_disj_lemma5 [THEN disjE]) -apply (erule (2) adm_disj_lemma4 [THEN disjI1]) -apply (erule (2) adm_disj_lemma4 [THEN disjI2]) +apply (erule adm_disj_lemma2 [THEN disjE]) +apply (erule (2) adm_disj_lemma1 [THEN disjI1]) +apply (erule (2) adm_disj_lemma1 [THEN disjI2]) done -lemma adm_imp: "\adm (\x. \ P x); adm Q\ \ adm (\x. P x \ Q x)" +lemma adm_imp [simp]: + "\adm (\x. \ P x); adm (\x. Q x)\ \ adm (\x. P x \ Q x)" by (subst imp_conv_disj, rule adm_disj) -lemma adm_iff: +lemma adm_iff [simp]: "\adm (\x. P x \ Q x); adm (\x. Q x \ P x)\ \ adm (\x. P x = Q x)" by (subst iff_conv_conj_imp, rule adm_conj) -lemma adm_not_conj: - "\adm (\x. \ P x); adm (\x. \ Q x)\ \ adm (\x. \ (P x \ Q x))" -by (simp add: adm_imp) - text {* admissibility and continuity *} -lemma adm_below: "\cont u; cont v\ \ adm (\x. u x \ v x)" +lemma adm_below [simp]: + "\cont (\x. u x); cont (\x. v x)\ \ adm (\x. u x \ v x)" apply (rule admI) apply (simp add: cont2contlubE) apply (rule lub_mono) @@ -131,10 +130,11 @@ apply (erule spec) done -lemma adm_eq: "\cont u; cont v\ \ adm (\x. u x = v x)" -by (simp add: po_eq_conv adm_conj adm_below) +lemma adm_eq [simp]: + "\cont (\x. u x); cont (\x. v x)\ \ adm (\x. u x = v x)" +by (simp add: po_eq_conv) -lemma adm_subst: "\cont t; adm P\ \ adm (\x. P (t x))" +lemma adm_subst: "\cont (\x. t x); adm P\ \ adm (\x. P (t x))" apply (rule admI) apply (simp add: cont2contlubE) apply (erule admD) @@ -142,14 +142,8 @@ apply (erule spec) done -lemma adm_not_below: "cont t \ adm (\x. \ t x \ u)" -apply (rule admI) -apply (drule_tac x=0 in spec) -apply (erule contrapos_nn) -apply (erule rev_below_trans) -apply (erule cont2mono [THEN monofunE]) -apply (erule is_ub_thelub) -done +lemma adm_not_below [simp]: "cont (\x. t x) \ adm (\x. \ t x \ u)" +by (rule admI, simp add: cont2contlubE ch2ch_cont lub_below_iff) subsection {* Compactness *} @@ -190,20 +184,20 @@ text {* admissibility and compactness *} -lemma adm_compact_not_below: "\compact k; cont t\ \ adm (\x. \ k \ t x)" +lemma adm_compact_not_below [simp]: + "\compact k; cont (\x. t x)\ \ adm (\x. \ k \ t x)" unfolding compact_def by (rule adm_subst) -lemma adm_neq_compact: "\compact k; cont t\ \ adm (\x. t x \ k)" -by (simp add: po_eq_conv adm_imp adm_not_below adm_compact_not_below) +lemma adm_neq_compact [simp]: + "\compact k; cont (\x. t x)\ \ adm (\x. t x \ k)" +by (simp add: po_eq_conv) -lemma adm_compact_neq: "\compact k; cont t\ \ adm (\x. k \ t x)" -by (simp add: po_eq_conv adm_imp adm_not_below adm_compact_not_below) +lemma adm_compact_neq [simp]: + "\compact k; cont (\x. t x)\ \ adm (\x. k \ t x)" +by (simp add: po_eq_conv) lemma compact_UU [simp, intro]: "compact \" -by (rule compactI, simp add: adm_not_free) - -lemma adm_not_UU: "cont t \ adm (\x. t x \ \)" -by (simp add: adm_neq_compact) +by (rule compactI, simp) text {* Any upward-closed predicate is admissible. *} @@ -212,9 +206,9 @@ shows "adm P" by (rule admI, drule spec, erule P, erule is_ub_thelub) -lemmas adm_lemmas [simp] = - adm_not_free adm_conj adm_all adm_ball adm_disj adm_imp adm_iff +lemmas adm_lemmas = + adm_const adm_conj adm_all adm_ball adm_disj adm_imp adm_iff adm_below adm_eq adm_not_below - adm_compact_not_below adm_compact_neq adm_neq_compact adm_not_UU + adm_compact_not_below adm_compact_neq adm_neq_compact end diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/Bifinite.thy --- a/src/HOLCF/Bifinite.thy Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/Bifinite.thy Sat Oct 16 16:39:06 2010 -0700 @@ -56,7 +56,7 @@ unfolding approx_def by (simp add: Y) show "(\i. approx i) = ID" unfolding approx_def - by (simp add: lub_distribs Y DEFL [symmetric] cast_DEFL expand_cfun_eq) + by (simp add: lub_distribs Y DEFL [symmetric] cast_DEFL cfun_eq_iff) show "\i. finite_deflation (approx i)" unfolding approx_def apply (rule bifinite.finite_deflation_p_d_e) @@ -228,7 +228,7 @@ next show "cast\DEFL('a \ 'b) = emb oo (prj :: udom \ 'a \ 'b)" unfolding emb_cfun_def prj_cfun_def defl_cfun_def cast_cfun_defl - by (simp add: cast_DEFL oo_def expand_cfun_eq cfun_map_map) + by (simp add: cast_DEFL oo_def cfun_eq_iff cfun_map_map) qed end @@ -287,7 +287,7 @@ next show "cast\DEFL('a \ 'b) = emb oo (prj :: udom \ 'a \ 'b)" unfolding emb_prod_def prj_prod_def defl_prod_def cast_prod_defl - by (simp add: cast_DEFL oo_def expand_cfun_eq cprod_map_map) + by (simp add: cast_DEFL oo_def cfun_eq_iff cprod_map_map) qed end @@ -348,7 +348,7 @@ next show "cast\DEFL('a \ 'b) = emb oo (prj :: udom \ 'a \ 'b)" unfolding emb_sprod_def prj_sprod_def defl_sprod_def cast_sprod_defl - by (simp add: cast_DEFL oo_def expand_cfun_eq sprod_map_map) + by (simp add: cast_DEFL oo_def cfun_eq_iff sprod_map_map) qed end @@ -405,7 +405,7 @@ next show "cast\DEFL('a u) = emb oo (prj :: udom \ 'a u)" unfolding emb_u_def prj_u_def defl_u_def cast_u_defl - by (simp add: cast_DEFL oo_def expand_cfun_eq u_map_map) + by (simp add: cast_DEFL oo_def cfun_eq_iff u_map_map) qed end @@ -425,7 +425,7 @@ by (rule chainI, simp add: FLIFT_mono) lemma lub_lift_approx [simp]: "(\i. lift_approx i) = ID" -apply (rule ext_cfun) +apply (rule cfun_eqI) apply (simp add: contlub_cfun_fun) apply (simp add: lift_approx_def) apply (case_tac x, simp) @@ -440,7 +440,7 @@ lemma finite_deflation_lift_approx: "finite_deflation (lift_approx i)" proof - fix x + fix x :: "'a lift" show "lift_approx i\x \ x" unfolding lift_approx_def by (cases x, simp, simp) @@ -548,7 +548,7 @@ next show "cast\DEFL('a \ 'b) = emb oo (prj :: udom \ 'a \ 'b)" unfolding emb_ssum_def prj_ssum_def defl_ssum_def cast_ssum_defl - by (simp add: cast_DEFL oo_def expand_cfun_eq ssum_map_map) + by (simp add: cast_DEFL oo_def cfun_eq_iff ssum_map_map) qed end diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/Cfun.thy --- a/src/HOLCF/Cfun.thy Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/Cfun.thy Sat Oct 16 16:39:06 2010 -0700 @@ -6,21 +6,15 @@ header {* The type of continuous functions *} theory Cfun -imports Pcpodef Ffun Product_Cpo +imports Pcpodef Fun_Cpo Product_Cpo begin default_sort cpo subsection {* Definition of continuous function type *} -lemma Ex_cont: "\f. cont f" -by (rule exI, rule cont_const) - -lemma adm_cont: "adm cont" -by (rule admI, rule cont_lub_fun) - cpodef (CFun) ('a, 'b) cfun (infixr "->" 0) = "{f::'a => 'b. cont f}" -by (simp_all add: Ex_cont adm_cont) +by (auto intro: cont_const adm_cont) type_notation (xsymbols) cfun ("(_ \/ _)" [1, 0] 0) @@ -176,19 +170,19 @@ text {* Extensionality for continuous functions *} -lemma expand_cfun_eq: "(f = g) = (\x. f\x = g\x)" +lemma cfun_eq_iff: "f = g \ (\x. f\x = g\x)" by (simp add: Rep_CFun_inject [symmetric] fun_eq_iff) -lemma ext_cfun: "(\x. f\x = g\x) \ f = g" -by (simp add: expand_cfun_eq) +lemma cfun_eqI: "(\x. f\x = g\x) \ f = g" +by (simp add: cfun_eq_iff) text {* Extensionality wrt. ordering for continuous functions *} -lemma expand_cfun_below: "f \ g = (\x. f\x \ g\x)" -by (simp add: below_CFun_def expand_fun_below) +lemma cfun_below_iff: "f \ g \ (\x. f\x \ g\x)" +by (simp add: below_CFun_def fun_below_iff) -lemma below_cfun_ext: "(\x. f\x \ g\x) \ f \ g" -by (simp add: expand_cfun_below) +lemma cfun_belowI: "(\x. f\x \ g\x) \ f \ g" +by (simp add: cfun_below_iff) text {* Congruence for continuous function application *} @@ -233,7 +227,7 @@ text {* monotonicity of application *} lemma monofun_cfun_fun: "f \ g \ f\x \ g\x" -by (simp add: expand_cfun_below) +by (simp add: cfun_below_iff) lemma monofun_cfun_arg: "x \ y \ f\x \ f\y" by (rule monofun_Rep_CFun2 [THEN monofunE]) @@ -258,7 +252,7 @@ lemma ch2ch_LAM [simp]: "\\x. chain (\i. S i x); \i. cont (\x. S i x)\ \ chain (\i. \ x. S i x)" -by (simp add: chain_def expand_cfun_below) +by (simp add: chain_def cfun_below_iff) text {* contlub, cont properties of @{term Rep_CFun} in both arguments *} @@ -293,29 +287,6 @@ apply (rule minimal [THEN monofun_cfun_arg]) done -text {* the lub of a chain of continous functions is monotone *} - -lemma lub_cfun_mono: "chain F \ monofun (\x. \i. F i\x)" -apply (drule ch2ch_monofun [OF monofun_Rep_CFun]) -apply (simp add: thelub_fun [symmetric]) -apply (erule monofun_lub_fun) -apply (simp add: monofun_Rep_CFun2) -done - -text {* a lemma about the exchange of lubs for type @{typ "'a -> 'b"} *} - -lemma ex_lub_cfun: - "\chain F; chain Y\ \ (\j. \i. F j\(Y i)) = (\i. \j. F j\(Y i))" -by (simp add: diag_lub) - -text {* the lub of a chain of cont. functions is continuous *} - -lemma cont_lub_cfun: "chain F \ cont (\x. \i. F i\x)" -apply (rule cont2cont_lub) -apply (erule monofun_Rep_CFun [THEN ch2ch_monofun]) -apply (rule cont_Rep_CFun2) -done - text {* type @{typ "'a -> 'b"} is chain complete *} lemma lub_cfun: "chain F \ range F <<| (\ x. \i. F i\x)" @@ -333,18 +304,30 @@ assumes t: "cont (\x. t x)" shows "cont (\x. (f x)\(t x))" proof - - have "cont (\x. Rep_CFun (f x))" - using cont_Rep_CFun f by (rule cont2cont_app3) - thus "cont (\x. (f x)\(t x))" - using cont_Rep_CFun2 t by (rule cont2cont_app2) + have 1: "\y. cont (\x. (f x)\y)" + using cont_Rep_CFun1 f by (rule cont_compose) + show "cont (\x. (f x)\(t x))" + using t cont_Rep_CFun2 1 by (rule cont_apply) qed +text {* + Two specific lemmas for the combination of LCF and HOL terms. + These lemmas are needed in theories that use types like @{typ "'a \ 'b \ 'c"}. +*} + +lemma cont_Rep_CFun_app [simp]: "\cont f; cont g\ \ cont (\x. ((f x)\(g x)) s)" +by (rule cont2cont_Rep_CFun [THEN cont2cont_fun]) + +lemma cont_Rep_CFun_app_app [simp]: "\cont f; cont g\ \ cont (\x. ((f x)\(g x)) s t)" +by (rule cont_Rep_CFun_app [THEN cont2cont_fun]) + + text {* cont2mono Lemma for @{term "%x. LAM y. c1(x)(y)"} *} lemma cont2mono_LAM: "\\x. cont (\y. f x y); \y. monofun (\x. f x y)\ \ monofun (\x. \ y. f x y)" - unfolding monofun_def expand_cfun_below by simp + unfolding monofun_def cfun_below_iff by simp text {* cont2cont Lemma for @{term "%x. LAM y. f x y"} *} @@ -509,7 +492,7 @@ by (simp add: cfcomp1) lemma cfcomp_strict [simp]: "\ oo f = \" -by (simp add: expand_cfun_eq) +by (simp add: cfun_eq_iff) text {* Show that interpretation of (pcpo,@{text "_->_"}) is a category. @@ -520,13 +503,13 @@ *} lemma ID2 [simp]: "f oo ID = f" -by (rule ext_cfun, simp) +by (rule cfun_eqI, simp) lemma ID3 [simp]: "ID oo f = f" -by (rule ext_cfun, simp) +by (rule cfun_eqI, simp) lemma assoc_oo: "f oo (g oo h) = (f oo g) oo h" -by (rule ext_cfun, simp) +by (rule cfun_eqI, simp) subsection {* Map operator for continuous function space *} @@ -539,12 +522,12 @@ unfolding cfun_map_def by simp lemma cfun_map_ID: "cfun_map\ID\ID = ID" -unfolding expand_cfun_eq by simp +unfolding cfun_eq_iff by simp lemma cfun_map_map: "cfun_map\f1\g1\(cfun_map\f2\g2\p) = cfun_map\(\ x. f2\(f1\x))\(\ x. g1\(g2\x))\p" -by (rule ext_cfun) simp +by (rule cfun_eqI) simp subsection {* Strictified functions *} @@ -600,10 +583,10 @@ using f proof (rule cont2cont_Let) fix x show "cont (\y. g x y)" - using g by (rule cont_fst_snd_D2) + using g by (simp add: prod_cont_iff) next fix y show "cont (\x. g x y)" - using g by (rule cont_fst_snd_D1) + using g by (simp add: prod_cont_iff) qed text {* The simple version (suggested by Joachim Breitner) is needed if diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/Completion.thy --- a/src/HOLCF/Completion.thy Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/Completion.thy Sat Oct 16 16:39:06 2010 -0700 @@ -397,7 +397,7 @@ assumes g_mono: "\a b. a \ b \ g a \ g b" assumes below: "\a. f a \ g a" shows "basis_fun f \ basis_fun g" - apply (rule below_cfun_ext) + apply (rule cfun_belowI) apply (simp only: basis_fun_beta f_mono g_mono) apply (rule is_lub_thelub_ex) apply (rule basis_fun_lemma, erule f_mono) diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/Cont.thy --- a/src/HOLCF/Cont.thy Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/Cont.thy Sat Oct 16 16:39:06 2010 -0700 @@ -22,12 +22,6 @@ monofun :: "('a \ 'b) \ bool" -- "monotonicity" where "monofun f = (\x y. x \ y \ f x \ f y)" -(* -definition - contlub :: "('a::cpo \ 'b::cpo) \ bool" -- "first cont. def" where - "contlub f = (\Y. chain Y \ f (\i. Y i) = (\i. f (Y i)))" -*) - definition cont :: "('a::cpo \ 'b::cpo) \ bool" where @@ -176,6 +170,17 @@ "\cont c; cont (\x. f x)\ \ cont (\x. c (f x))" by (rule cont_apply [OF _ _ cont_const]) +text {* Least upper bounds preserve continuity *} + +lemma cont2cont_lub [simp]: + assumes chain: "\x. chain (\i. F i x)" and cont: "\i. cont (\x. F i x)" + shows "cont (\x. \i. F i x)" +apply (rule contI2) +apply (simp add: monofunI cont2monofunE [OF cont] lub_mono chain) +apply (simp add: cont2contlubE [OF cont]) +apply (simp add: diag_lub ch2ch_cont [OF cont] chain) +done + text {* if-then-else is continuous *} lemma cont_if [simp, cont2cont]: @@ -184,7 +189,7 @@ subsection {* Finite chains and flat pcpos *} -text {* monotone functions map finite chains to finite chains *} +text {* Monotone functions map finite chains to finite chains. *} lemma monofun_finch2finch: "\monofun f; finite_chain Y\ \ finite_chain (\n. f (Y n))" @@ -193,12 +198,14 @@ apply (force simp add: max_in_chain_def) done -text {* The same holds for continuous functions *} +text {* The same holds for continuous functions. *} lemma cont_finch2finch: "\cont f; finite_chain Y\ \ finite_chain (\n. f (Y n))" by (rule cont2mono [THEN monofun_finch2finch]) +text {* All monotone functions with chain-finite domain are continuous. *} + lemma chfindom_monofun2cont: "monofun f \ cont (f::'a::chfin \ 'b::cpo)" apply (erule contI2) apply (frule chfin2finch) @@ -208,7 +215,7 @@ apply (force simp add: max_in_chain_def) done -text {* some properties of flat *} +text {* All strict functions with flat domain are continuous. *} lemma flatdom_strict2mono: "f \ = \ \ monofun (f::'a::flat \ 'b::pcpo)" apply (rule monofunI) @@ -219,7 +226,7 @@ lemma flatdom_strict2cont: "f \ = \ \ cont (f::'a::flat \ 'b::pcpo)" by (rule flatdom_strict2mono [THEN chfindom_monofun2cont]) -text {* functions with discrete domain *} +text {* All functions with discrete domain are continuous. *} lemma cont_discrete_cpo [simp, cont2cont]: "cont (f::'a::discrete_cpo \ 'b::cpo)" apply (rule contI) diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/ConvexPD.thy --- a/src/HOLCF/ConvexPD.thy Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/ConvexPD.thy Sat Oct 16 16:39:06 2010 -0700 @@ -331,7 +331,7 @@ lemma monofun_LAM: "\cont f; cont g; \x. f x \ g x\ \ (\ x. f x) \ (\ x. g x)" -by (simp add: expand_cfun_below) +by (simp add: cfun_below_iff) lemma convex_bind_basis_mono: "t \\ u \ convex_bind_basis t \ convex_bind_basis u" @@ -382,7 +382,7 @@ by (induct xs rule: convex_pd_induct, simp_all) lemma convex_map_ID: "convex_map\ID = ID" -by (simp add: expand_cfun_eq ID_def convex_map_ident) +by (simp add: cfun_eq_iff ID_def convex_map_ident) lemma convex_map_map: "convex_map\f\(convex_map\g\xs) = convex_map\(\ x. f\(g\x))\xs" @@ -494,7 +494,7 @@ next show "cast\DEFL('a convex_pd) = emb oo (prj :: udom \ 'a convex_pd)" unfolding emb_convex_pd_def prj_convex_pd_def defl_convex_pd_def cast_convex_defl - by (simp add: cast_DEFL oo_def expand_cfun_eq convex_map_map) + by (simp add: cast_DEFL oo_def cfun_eq_iff convex_map_map) qed end diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/Cprod.thy --- a/src/HOLCF/Cprod.thy Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/Cprod.thy Sat Oct 16 16:39:06 2010 -0700 @@ -51,7 +51,7 @@ unfolding cprod_map_def by simp lemma cprod_map_ID: "cprod_map\ID\ID = ID" -unfolding expand_cfun_eq by auto +unfolding cfun_eq_iff by auto lemma cprod_map_map: "cprod_map\f1\g1\(cprod_map\f2\g2\p) = diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/Deflation.thy --- a/src/HOLCF/Deflation.thy Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/Deflation.thy Sat Oct 16 16:39:06 2010 -0700 @@ -19,7 +19,7 @@ begin lemma below_ID: "d \ ID" -by (rule below_cfun_ext, simp add: below) +by (rule cfun_belowI, simp add: below) text {* The set of fixed points is the same as the range. *} @@ -36,7 +36,7 @@ lemma belowI: assumes f: "\x. d\x = x \ f\x = x" shows "d \ f" -proof (rule below_cfun_ext) +proof (rule cfun_belowI) fix x from below have "f\(d\x) \ f\x" by (rule monofun_cfun_arg) also from idem have "f\(d\x) = d\x" by (rule f) @@ -326,7 +326,7 @@ lemma ep_pair_unique_e_lemma: assumes 1: "ep_pair e1 p" and 2: "ep_pair e2 p" shows "e1 \ e2" -proof (rule below_cfun_ext) +proof (rule cfun_belowI) fix x have "e1\(p\(e2\x)) \ e2\x" by (rule ep_pair.e_p_below [OF 1]) @@ -341,7 +341,7 @@ lemma ep_pair_unique_p_lemma: assumes 1: "ep_pair e p1" and 2: "ep_pair e p2" shows "p1 \ p2" -proof (rule below_cfun_ext) +proof (rule cfun_belowI) fix x have "e\(p1\x) \ x" by (rule ep_pair.e_p_below [OF 1]) @@ -414,9 +414,9 @@ interpret e1p1: ep_pair e1 p1 by fact interpret e2p2: ep_pair e2 p2 by fact fix f show "cfun_map\e1\p2\(cfun_map\p1\e2\f) = f" - by (simp add: expand_cfun_eq) + by (simp add: cfun_eq_iff) fix g show "cfun_map\p1\e2\(cfun_map\e1\p2\g) \ g" - apply (rule below_cfun_ext, simp) + apply (rule cfun_belowI, simp) apply (rule below_trans [OF e2p2.e_p_below]) apply (rule monofun_cfun_arg) apply (rule e1p1.e_p_below) @@ -431,9 +431,9 @@ interpret d2: deflation d2 by fact fix f show "cfun_map\d1\d2\(cfun_map\d1\d2\f) = cfun_map\d1\d2\f" - by (simp add: expand_cfun_eq d1.idem d2.idem) + by (simp add: cfun_eq_iff d1.idem d2.idem) show "cfun_map\d1\d2\f \ f" - apply (rule below_cfun_ext, simp) + apply (rule cfun_belowI, simp) apply (rule below_trans [OF d2.below]) apply (rule monofun_cfun_arg) apply (rule d1.below) @@ -455,7 +455,7 @@ by (simp add: a b) qed show "inj_on ?f (range ?h)" - proof (rule inj_onI, rule ext_cfun, clarsimp) + proof (rule inj_onI, rule cfun_eqI, clarsimp) fix x f g assume "range (\x. (a\x, b\(f\(a\x)))) = range (\x. (a\x, b\(g\(a\x))))" hence "range (\x. (a\x, b\(f\(a\x)))) \ range (\x. (a\x, b\(g\(a\x))))" diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/Domain.thy --- a/src/HOLCF/Domain.thy Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/Domain.thy Sat Oct 16 16:39:06 2010 -0700 @@ -10,7 +10,6 @@ ("Tools/cont_consts.ML") ("Tools/cont_proc.ML") ("Tools/Domain/domain_constructors.ML") - ("Tools/Domain/domain_library.ML") ("Tools/Domain/domain_axioms.ML") ("Tools/Domain/domain_theorems.ML") ("Tools/Domain/domain_extender.ML") @@ -154,7 +153,6 @@ use "Tools/cont_consts.ML" use "Tools/cont_proc.ML" -use "Tools/Domain/domain_library.ML" use "Tools/Domain/domain_axioms.ML" use "Tools/Domain/domain_constructors.ML" use "Tools/Domain/domain_theorems.ML" diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/FOCUS/Buffer.thy --- a/src/HOLCF/FOCUS/Buffer.thy Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/FOCUS/Buffer.thy Sat Oct 16 16:39:06 2010 -0700 @@ -200,7 +200,7 @@ apply ( rule_tac [2] P="(%x. x:B)" in ssubst) prefer 3 apply ( assumption) -apply ( rule_tac [2] ext_cfun) +apply ( rule_tac [2] cfun_eqI) apply ( drule_tac [2] spec) apply ( drule_tac [2] f="rt" in cfun_arg_cong) prefer 2 diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/FOCUS/Fstream.thy --- a/src/HOLCF/FOCUS/Fstream.thy Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/FOCUS/Fstream.thy Sat Oct 16 16:39:06 2010 -0700 @@ -95,7 +95,7 @@ apply (safe) apply (erule_tac [!] contrapos_np) prefer 2 apply (fast elim: DefE) -apply (rule Lift_cases) +apply (rule lift.exhaust) apply (erule (1) notE) apply (safe) apply (drule Def_inject_less_eq [THEN iffD1]) diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/Ffun.thy --- a/src/HOLCF/Ffun.thy Fri Oct 15 17:21:37 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,273 +0,0 @@ -(* Title: HOLCF/FunCpo.thy - Author: Franz Regensburger -*) - -header {* Class instances for the full function space *} - -theory Ffun -imports Cont -begin - -subsection {* Full function space is a partial order *} - -instantiation "fun" :: (type, below) below -begin - -definition - below_fun_def: "(op \) \ (\f g. \x. f x \ g x)" - -instance .. -end - -instance "fun" :: (type, po) po -proof - fix f :: "'a \ 'b" - show "f \ f" - by (simp add: below_fun_def) -next - fix f g :: "'a \ 'b" - assume "f \ g" and "g \ f" thus "f = g" - by (simp add: below_fun_def fun_eq_iff below_antisym) -next - fix f g h :: "'a \ 'b" - assume "f \ g" and "g \ h" thus "f \ h" - unfolding below_fun_def by (fast elim: below_trans) -qed - -text {* make the symbol @{text "<<"} accessible for type fun *} - -lemma expand_fun_below: "(f \ g) = (\x. f x \ g x)" -by (simp add: below_fun_def) - -lemma below_fun_ext: "(\x. f x \ g x) \ f \ g" -by (simp add: below_fun_def) - -subsection {* Full function space is chain complete *} - -text {* function application is monotone *} - -lemma monofun_app: "monofun (\f. f x)" -by (rule monofunI, simp add: below_fun_def) - -text {* chains of functions yield chains in the po range *} - -lemma ch2ch_fun: "chain S \ chain (\i. S i x)" -by (simp add: chain_def below_fun_def) - -lemma ch2ch_lambda: "(\x. chain (\i. S i x)) \ chain S" -by (simp add: chain_def below_fun_def) - -text {* upper bounds of function chains yield upper bound in the po range *} - -lemma ub2ub_fun: - "range S <| u \ range (\i. S i x) <| u x" -by (auto simp add: is_ub_def below_fun_def) - -text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *} - -lemma is_lub_lambda: - assumes f: "\x. range (\i. Y i x) <<| f x" - shows "range Y <<| f" -apply (rule is_lubI) -apply (rule ub_rangeI) -apply (rule below_fun_ext) -apply (rule is_ub_lub [OF f]) -apply (rule below_fun_ext) -apply (rule is_lub_lub [OF f]) -apply (erule ub2ub_fun) -done - -lemma lub_fun: - "chain (S::nat \ 'a::type \ 'b::cpo) - \ range S <<| (\x. \i. S i x)" -apply (rule is_lub_lambda) -apply (rule cpo_lubI) -apply (erule ch2ch_fun) -done - -lemma thelub_fun: - "chain (S::nat \ 'a::type \ 'b::cpo) - \ (\i. S i) = (\x. \i. S i x)" -by (rule lub_fun [THEN thelubI]) - -lemma cpo_fun: - "chain (S::nat \ 'a::type \ 'b::cpo) \ \x. range S <<| x" -by (rule exI, erule lub_fun) - -instance "fun" :: (type, cpo) cpo -by intro_classes (rule cpo_fun) - -instance "fun" :: (finite, finite_po) finite_po .. - -instance "fun" :: (type, discrete_cpo) discrete_cpo -proof - fix f g :: "'a \ 'b" - show "f \ g \ f = g" - unfolding expand_fun_below fun_eq_iff - by simp -qed - -text {* chain-finite function spaces *} - -lemma maxinch2maxinch_lambda: - "(\x. max_in_chain n (\i. S i x)) \ max_in_chain n S" -unfolding max_in_chain_def fun_eq_iff by simp - -lemma maxinch_mono: - "\max_in_chain i Y; i \ j\ \ max_in_chain j Y" -unfolding max_in_chain_def -proof (intro allI impI) - fix k - assume Y: "\n\i. Y i = Y n" - assume ij: "i \ j" - assume jk: "j \ k" - from ij jk have ik: "i \ k" by simp - from Y ij have Yij: "Y i = Y j" by simp - from Y ik have Yik: "Y i = Y k" by simp - from Yij Yik show "Y j = Y k" by auto -qed - -instance "fun" :: (finite, chfin) chfin -proof - fix Y :: "nat \ 'a \ 'b" - let ?n = "\x. LEAST n. max_in_chain n (\i. Y i x)" - assume "chain Y" - hence "\x. chain (\i. Y i x)" - by (rule ch2ch_fun) - hence "\x. \n. max_in_chain n (\i. Y i x)" - by (rule chfin) - hence "\x. max_in_chain (?n x) (\i. Y i x)" - by (rule LeastI_ex) - hence "\x. max_in_chain (Max (range ?n)) (\i. Y i x)" - by (rule maxinch_mono [OF _ Max_ge], simp_all) - hence "max_in_chain (Max (range ?n)) Y" - by (rule maxinch2maxinch_lambda) - thus "\n. max_in_chain n Y" .. -qed - -subsection {* Full function space is pointed *} - -lemma minimal_fun: "(\x. \) \ f" -by (simp add: below_fun_def) - -lemma least_fun: "\x::'a::type \ 'b::pcpo. \y. x \ y" -apply (rule_tac x = "\x. \" in exI) -apply (rule minimal_fun [THEN allI]) -done - -instance "fun" :: (type, pcpo) pcpo -by intro_classes (rule least_fun) - -text {* for compatibility with old HOLCF-Version *} -lemma inst_fun_pcpo: "\ = (\x. \)" -by (rule minimal_fun [THEN UU_I, symmetric]) - -text {* function application is strict in the left argument *} -lemma app_strict [simp]: "\ x = \" -by (simp add: inst_fun_pcpo) - -text {* - The following results are about application for functions in @{typ "'a=>'b"} -*} - -lemma monofun_fun_fun: "f \ g \ f x \ g x" -by (simp add: below_fun_def) - -lemma monofun_fun_arg: "\monofun f; x \ y\ \ f x \ f y" -by (rule monofunE) - -lemma monofun_fun: "\monofun f; monofun g; f \ g; x \ y\ \ f x \ g y" -by (rule below_trans [OF monofun_fun_arg monofun_fun_fun]) - -subsection {* Propagation of monotonicity and continuity *} - -text {* the lub of a chain of monotone functions is monotone *} - -lemma monofun_lub_fun: - "\chain (F::nat \ 'a \ 'b::cpo); \i. monofun (F i)\ - \ monofun (\i. F i)" -apply (rule monofunI) -apply (simp add: thelub_fun) -apply (rule lub_mono) -apply (erule ch2ch_fun) -apply (erule ch2ch_fun) -apply (simp add: monofunE) -done - -text {* the lub of a chain of continuous functions is continuous *} - -lemma cont_lub_fun: - "\chain F; \i. cont (F i)\ \ cont (\i. F i)" -apply (rule contI2) -apply (erule monofun_lub_fun) -apply (simp add: cont2mono) -apply (simp add: thelub_fun cont2contlubE) -apply (simp add: diag_lub ch2ch_fun ch2ch_cont) -done - -lemma cont2cont_lub: - "\chain F; \i. cont (F i)\ \ cont (\x. \i. F i x)" -by (simp add: thelub_fun [symmetric] cont_lub_fun) - -lemma mono2mono_fun: "monofun f \ monofun (\x. f x y)" -apply (rule monofunI) -apply (erule (1) monofun_fun_arg [THEN monofun_fun_fun]) -done - -lemma cont2cont_fun: "cont f \ cont (\x. f x y)" -apply (rule contI2) -apply (erule cont2mono [THEN mono2mono_fun]) -apply (simp add: cont2contlubE) -apply (simp add: thelub_fun ch2ch_cont) -done - -text {* Note @{text "(\x. \y. f x y) = f"} *} - -lemma mono2mono_lambda: - assumes f: "\y. monofun (\x. f x y)" shows "monofun f" -apply (rule monofunI) -apply (rule below_fun_ext) -apply (erule monofunE [OF f]) -done - -lemma cont2cont_lambda [simp]: - assumes f: "\y. cont (\x. f x y)" shows "cont f" -apply (rule contI2) -apply (simp add: mono2mono_lambda cont2mono f) -apply (rule below_fun_ext) -apply (simp add: thelub_fun cont2contlubE [OF f]) -done - -text {* What D.A.Schmidt calls continuity of abstraction; never used here *} - -lemma contlub_lambda: - "(\x::'a::type. chain (\i. S i x::'b::cpo)) - \ (\x. \i. S i x) = (\i. (\x. S i x))" -by (simp add: thelub_fun ch2ch_lambda) - -lemma contlub_abstraction: - "\chain Y; \y. cont (\x.(c::'a::cpo\'b::type\'c::cpo) x y)\ \ - (\y. \i. c (Y i) y) = (\i. (\y. c (Y i) y))" -apply (rule thelub_fun [symmetric]) -apply (simp add: ch2ch_cont) -done - -lemma mono2mono_app: - "\monofun f; \x. monofun (f x); monofun t\ \ monofun (\x. (f x) (t x))" -apply (rule monofunI) -apply (simp add: monofun_fun monofunE) -done - -lemma cont2cont_app: - "\cont f; \x. cont (f x); cont t\ \ cont (\x. (f x) (t x))" -apply (erule cont_apply [where t=t]) -apply (erule spec) -apply (erule cont2cont_fun) -done - -lemmas cont2cont_app2 = cont2cont_app [rule_format] - -lemma cont2cont_app3: "\cont f; cont t\ \ cont (\x. f (t x))" -by (rule cont2cont_app2 [OF cont_const]) - -end diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/Fix.thy --- a/src/HOLCF/Fix.thy Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/Fix.thy Sat Oct 16 16:39:06 2010 -0700 @@ -60,13 +60,7 @@ text {* direct connection between @{term fix} and iteration *} lemma fix_def2: "fix\F = (\i. iterate i\F\\)" -apply (unfold fix_def) -apply (rule beta_cfun) -apply (rule cont2cont_lub) -apply (rule ch2ch_lambda) -apply (rule chain_iterate) -apply simp -done +unfolding fix_def by simp lemma iterate_below_fix: "iterate n\f\\ \ fix\f" unfolding fix_def2 diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/Fun_Cpo.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Fun_Cpo.thy Sat Oct 16 16:39:06 2010 -0700 @@ -0,0 +1,201 @@ +(* Title: HOLCF/Fun_Cpo.thy + Author: Franz Regensburger + Author: Brian Huffman +*) + +header {* Class instances for the full function space *} + +theory Fun_Cpo +imports Adm +begin + +subsection {* Full function space is a partial order *} + +instantiation "fun" :: (type, below) below +begin + +definition + below_fun_def: "(op \) \ (\f g. \x. f x \ g x)" + +instance .. +end + +instance "fun" :: (type, po) po +proof + fix f :: "'a \ 'b" + show "f \ f" + by (simp add: below_fun_def) +next + fix f g :: "'a \ 'b" + assume "f \ g" and "g \ f" thus "f = g" + by (simp add: below_fun_def fun_eq_iff below_antisym) +next + fix f g h :: "'a \ 'b" + assume "f \ g" and "g \ h" thus "f \ h" + unfolding below_fun_def by (fast elim: below_trans) +qed + +lemma fun_below_iff: "f \ g \ (\x. f x \ g x)" +by (simp add: below_fun_def) + +lemma fun_belowI: "(\x. f x \ g x) \ f \ g" +by (simp add: below_fun_def) + +lemma fun_belowD: "f \ g \ f x \ g x" +by (simp add: below_fun_def) + +subsection {* Full function space is chain complete *} + +text {* Function application is monotone. *} + +lemma monofun_app: "monofun (\f. f x)" +by (rule monofunI, simp add: below_fun_def) + +text {* Properties of chains of functions. *} + +lemma fun_chain_iff: "chain S \ (\x. chain (\i. S i x))" +unfolding chain_def fun_below_iff by auto + +lemma ch2ch_fun: "chain S \ chain (\i. S i x)" +by (simp add: chain_def below_fun_def) + +lemma ch2ch_lambda: "(\x. chain (\i. S i x)) \ chain S" +by (simp add: chain_def below_fun_def) + +text {* upper bounds of function chains yield upper bound in the po range *} + +lemma ub2ub_fun: + "range S <| u \ range (\i. S i x) <| u x" +by (auto simp add: is_ub_def below_fun_def) + +text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *} + +lemma is_lub_lambda: + "(\x. range (\i. Y i x) <<| f x) \ range Y <<| f" +unfolding is_lub_def is_ub_def below_fun_def by simp + +lemma lub_fun: + "chain (S::nat \ 'a::type \ 'b::cpo) + \ range S <<| (\x. \i. S i x)" +apply (rule is_lub_lambda) +apply (rule cpo_lubI) +apply (erule ch2ch_fun) +done + +lemma thelub_fun: + "chain (S::nat \ 'a::type \ 'b::cpo) + \ (\i. S i) = (\x. \i. S i x)" +by (rule lub_fun [THEN thelubI]) + +instance "fun" :: (type, cpo) cpo +by intro_classes (rule exI, erule lub_fun) + +subsection {* Chain-finiteness of function space *} + +lemma maxinch2maxinch_lambda: + "(\x. max_in_chain n (\i. S i x)) \ max_in_chain n S" +unfolding max_in_chain_def fun_eq_iff by simp + +lemma maxinch_mono: + "\max_in_chain i Y; i \ j\ \ max_in_chain j Y" +unfolding max_in_chain_def +proof (intro allI impI) + fix k + assume Y: "\n\i. Y i = Y n" + assume ij: "i \ j" + assume jk: "j \ k" + from ij jk have ik: "i \ k" by simp + from Y ij have Yij: "Y i = Y j" by simp + from Y ik have Yik: "Y i = Y k" by simp + from Yij Yik show "Y j = Y k" by auto +qed + +instance "fun" :: (finite, chfin) chfin +proof + fix Y :: "nat \ 'a \ 'b" + let ?n = "\x. LEAST n. max_in_chain n (\i. Y i x)" + assume "chain Y" + hence "\x. chain (\i. Y i x)" + by (rule ch2ch_fun) + hence "\x. \n. max_in_chain n (\i. Y i x)" + by (rule chfin) + hence "\x. max_in_chain (?n x) (\i. Y i x)" + by (rule LeastI_ex) + hence "\x. max_in_chain (Max (range ?n)) (\i. Y i x)" + by (rule maxinch_mono [OF _ Max_ge], simp_all) + hence "max_in_chain (Max (range ?n)) Y" + by (rule maxinch2maxinch_lambda) + thus "\n. max_in_chain n Y" .. +qed + +instance "fun" :: (finite, finite_po) finite_po .. + +instance "fun" :: (type, discrete_cpo) discrete_cpo +proof + fix f g :: "'a \ 'b" + show "f \ g \ f = g" + unfolding fun_below_iff fun_eq_iff + by simp +qed + +subsection {* Full function space is pointed *} + +lemma minimal_fun: "(\x. \) \ f" +by (simp add: below_fun_def) + +instance "fun" :: (type, pcpo) pcpo +by default (fast intro: minimal_fun) + +lemma inst_fun_pcpo: "\ = (\x. \)" +by (rule minimal_fun [THEN UU_I, symmetric]) + +lemma app_strict [simp]: "\ x = \" +by (simp add: inst_fun_pcpo) + +lemma lambda_strict: "(\x. \) = \" +by (rule UU_I, rule minimal_fun) + +subsection {* Propagation of monotonicity and continuity *} + +text {* The lub of a chain of monotone functions is monotone. *} + +lemma adm_monofun: "adm monofun" +by (rule admI, simp add: thelub_fun fun_chain_iff monofun_def lub_mono) + +text {* The lub of a chain of continuous functions is continuous. *} + +lemma adm_cont: "adm cont" +by (rule admI, simp add: thelub_fun fun_chain_iff) + +text {* Function application preserves monotonicity and continuity. *} + +lemma mono2mono_fun: "monofun f \ monofun (\x. f x y)" +by (simp add: monofun_def fun_below_iff) + +lemma cont2cont_fun: "cont f \ cont (\x. f x y)" +apply (rule contI2) +apply (erule cont2mono [THEN mono2mono_fun]) +apply (simp add: cont2contlubE thelub_fun ch2ch_cont) +done + +text {* + Lambda abstraction preserves monotonicity and continuity. + (Note @{text "(\x. \y. f x y) = f"}.) +*} + +lemma mono2mono_lambda: + assumes f: "\y. monofun (\x. f x y)" shows "monofun f" +using f by (simp add: monofun_def fun_below_iff) + +lemma cont2cont_lambda [simp]: + assumes f: "\y. cont (\x. f x y)" shows "cont f" +by (rule contI, rule is_lub_lambda, rule contE [OF f]) + +text {* What D.A.Schmidt calls continuity of abstraction; never used here *} + +lemma contlub_lambda: + "(\x::'a::type. chain (\i. S i x::'b::cpo)) + \ (\x. \i. S i x) = (\i. (\x. S i x))" +by (simp add: thelub_fun ch2ch_lambda) + +end diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/HOLCF.thy --- a/src/HOLCF/HOLCF.thy Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/HOLCF.thy Sat Oct 16 16:39:06 2010 -0700 @@ -15,7 +15,20 @@ ML {* path_add "~~/src/HOLCF/Library" *} -text {* Legacy theorem names *} +text {* Legacy theorem names deprecated after Isabelle2009-2: *} + +lemmas expand_fun_below = fun_below_iff +lemmas below_fun_ext = fun_belowI +lemmas expand_cfun_eq = cfun_eq_iff +lemmas ext_cfun = cfun_eqI +lemmas expand_cfun_below = cfun_below_iff +lemmas below_cfun_ext = cfun_belowI +lemmas monofun_fun_fun = fun_belowD +lemmas monofun_fun_arg = monofunE +lemmas monofun_lub_fun = adm_monofun [THEN admD] +lemmas cont_lub_fun = adm_cont [THEN admD] + +text {* Older legacy theorem names: *} lemmas sq_ord_less_eq_trans = below_eq_trans lemmas sq_ord_eq_less_trans = eq_below_trans diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/IsaMakefile --- a/src/HOLCF/IsaMakefile Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/IsaMakefile Sat Oct 16 16:39:06 2010 -0700 @@ -48,9 +48,9 @@ Deflation.thy \ Domain.thy \ Domain_Aux.thy \ - Ffun.thy \ Fixrec.thy \ Fix.thy \ + Fun_Cpo.thy \ HOLCF.thy \ Lift.thy \ LowerPD.thy \ @@ -74,7 +74,6 @@ Tools/Domain/domain_axioms.ML \ Tools/Domain/domain_constructors.ML \ Tools/Domain/domain_isomorphism.ML \ - Tools/Domain/domain_library.ML \ Tools/Domain/domain_take_proofs.ML \ Tools/Domain/domain_theorems.ML \ Tools/fixrec.ML \ @@ -102,6 +101,7 @@ HOLCF-Library: HOLCF $(LOG)/HOLCF-Library.gz $(LOG)/HOLCF-Library.gz: $(OUT)/HOLCF \ + Library/Defl_Bifinite.thy \ Library/List_Cpo.thy \ Library/Stream.thy \ Library/Strict_Fun.thy \ diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/Library/Defl_Bifinite.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Library/Defl_Bifinite.thy Sat Oct 16 16:39:06 2010 -0700 @@ -0,0 +1,650 @@ +(* Title: HOLCF/Library/Defl_Bifinite.thy + Author: Brian Huffman +*) + +header {* Algebraic deflations are a bifinite domain *} + +theory Defl_Bifinite +imports HOLCF Infinite_Set +begin + +subsection {* Lemmas about MOST *} + +default_sort type + +lemma MOST_INFM: + assumes inf: "infinite (UNIV::'a set)" + shows "MOST x::'a. P x \ INFM x::'a. P x" + unfolding Alm_all_def Inf_many_def + apply (auto simp add: Collect_neg_eq) + apply (drule (1) finite_UnI) + apply (simp add: Compl_partition2 inf) + done + +lemma MOST_SucI: "MOST n. P n \ MOST n. P (Suc n)" +by (rule MOST_inj [OF _ inj_Suc]) + +lemma MOST_SucD: "MOST n. P (Suc n) \ MOST n. P n" +unfolding MOST_nat +apply (clarify, rule_tac x="Suc m" in exI, clarify) +apply (erule Suc_lessE, simp) +done + +lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \ (MOST n. P n)" +by (rule iffI [OF MOST_SucD MOST_SucI]) + +lemma INFM_finite_Bex_distrib: + "finite A \ (INFM y. \x\A. P x y) \ (\x\A. INFM y. P x y)" +by (induct set: finite, simp, simp add: INFM_disj_distrib) + +lemma MOST_finite_Ball_distrib: + "finite A \ (MOST y. \x\A. P x y) \ (\x\A. MOST y. P x y)" +by (induct set: finite, simp, simp add: MOST_conj_distrib) + +lemma MOST_ge_nat: "MOST n::nat. m \ n" +unfolding MOST_nat_le by fast + +subsection {* Eventually constant sequences *} + +definition + eventually_constant :: "(nat \ 'a) \ bool" +where + "eventually_constant S = (\x. MOST i. S i = x)" + +lemma eventually_constant_MOST_MOST: + "eventually_constant S \ (MOST m. MOST n. S n = S m)" +unfolding eventually_constant_def MOST_nat +apply safe +apply (rule_tac x=m in exI, clarify) +apply (rule_tac x=m in exI, clarify) +apply simp +apply fast +done + +lemma eventually_constantI: "MOST i. S i = x \ eventually_constant S" +unfolding eventually_constant_def by fast + +lemma eventually_constant_comp: + "eventually_constant (\i. S i) \ eventually_constant (\i. f (S i))" +unfolding eventually_constant_def +apply (erule exE, rule_tac x="f x" in exI) +apply (erule MOST_mono, simp) +done + +lemma eventually_constant_Suc_iff: + "eventually_constant (\i. S (Suc i)) \ eventually_constant (\i. S i)" +unfolding eventually_constant_def +by (subst MOST_Suc_iff, rule refl) + +lemma eventually_constant_SucD: + "eventually_constant (\i. S (Suc i)) \ eventually_constant (\i. S i)" +by (rule eventually_constant_Suc_iff [THEN iffD1]) + +subsection {* Limits of eventually constant sequences *} + +definition + eventual :: "(nat \ 'a) \ 'a" where + "eventual S = (THE x. MOST i. S i = x)" + +lemma eventual_eqI: "MOST i. S i = x \ eventual S = x" +unfolding eventual_def +apply (rule the_equality, assumption) +apply (rename_tac y) +apply (subgoal_tac "MOST i::nat. y = x", simp) +apply (erule MOST_rev_mp) +apply (erule MOST_rev_mp) +apply simp +done + +lemma MOST_eq_eventual: + "eventually_constant S \ MOST i. S i = eventual S" +unfolding eventually_constant_def +by (erule exE, simp add: eventual_eqI) + +lemma eventual_mem_range: + "eventually_constant S \ eventual S \ range S" +apply (drule MOST_eq_eventual) +apply (simp only: MOST_nat_le, clarify) +apply (drule spec, drule mp, rule order_refl) +apply (erule range_eqI [OF sym]) +done + +lemma eventually_constant_MOST_iff: + assumes S: "eventually_constant S" + shows "(MOST n. P (S n)) \ P (eventual S)" +apply (subgoal_tac "(MOST n. P (S n)) \ (MOST n::nat. P (eventual S))") +apply simp +apply (rule iffI) +apply (rule MOST_rev_mp [OF MOST_eq_eventual [OF S]]) +apply (erule MOST_mono, force) +apply (rule MOST_rev_mp [OF MOST_eq_eventual [OF S]]) +apply (erule MOST_mono, simp) +done + +lemma MOST_eventual: + "\eventually_constant S; MOST n. P (S n)\ \ P (eventual S)" +proof - + assume "eventually_constant S" + hence "MOST n. S n = eventual S" + by (rule MOST_eq_eventual) + moreover assume "MOST n. P (S n)" + ultimately have "MOST n. S n = eventual S \ P (S n)" + by (rule MOST_conj_distrib [THEN iffD2, OF conjI]) + hence "MOST n::nat. P (eventual S)" + by (rule MOST_mono) auto + thus ?thesis by simp +qed + +lemma eventually_constant_MOST_Suc_eq: + "eventually_constant S \ MOST n. S (Suc n) = S n" +apply (drule MOST_eq_eventual) +apply (frule MOST_Suc_iff [THEN iffD2]) +apply (erule MOST_rev_mp) +apply (erule MOST_rev_mp) +apply simp +done + +lemma eventual_comp: + "eventually_constant S \ eventual (\i. f (S i)) = f (eventual (\i. S i))" +apply (rule eventual_eqI) +apply (rule MOST_mono) +apply (erule MOST_eq_eventual) +apply simp +done + +subsection {* Constructing finite deflations by iteration *} + +default_sort cpo + +lemma le_Suc_induct: + assumes le: "i \ j" + assumes step: "\i. P i (Suc i)" + assumes refl: "\i. P i i" + assumes trans: "\i j k. \P i j; P j k\ \ P i k" + shows "P i j" +proof (cases "i = j") + assume "i = j" + thus "P i j" by (simp add: refl) +next + assume "i \ j" + with le have "i < j" by simp + 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 = + fixes f :: "'a \ 'a::cpo" + assumes below: "\x. f\x \ x" + assumes finite_range: "finite (range (\x. f\x))" +begin + +lemma iterate_below: "iterate i\f\x \ x" +by (induct i, simp_all add: below_trans [OF below]) + +lemma iterate_fixed: "f\x = x \ iterate i\f\x = x" +by (induct i, simp_all) + +lemma antichain_iterate_app: "i \ j \ iterate j\f\x \ iterate i\f\x" +apply (erule le_Suc_induct) +apply (simp add: below) +apply (rule below_refl) +apply (erule (1) below_trans) +done + +lemma finite_range_iterate_app: "finite (range (\i. iterate i\f\x))" +proof (rule finite_subset) + show "range (\i. iterate i\f\x) \ insert x (range (\x. f\x))" + by (clarify, case_tac i, simp_all) + show "finite (insert x (range (\x. f\x)))" + by (simp add: finite_range) +qed + +lemma eventually_constant_iterate_app: + "eventually_constant (\i. iterate i\f\x)" +unfolding eventually_constant_def MOST_nat_le +proof - + let ?Y = "\i. iterate i\f\x" + have "\j. \k. ?Y j \ ?Y k" + apply (rule finite_range_has_max) + apply (erule antichain_iterate_app) + apply (rule finite_range_iterate_app) + done + then obtain j where j: "\k. ?Y j \ ?Y k" by fast + show "\z m. \n\m. ?Y n = z" + proof (intro exI allI impI) + fix k + assume "j \ k" + hence "?Y k \ ?Y j" by (rule antichain_iterate_app) + also have "?Y j \ ?Y k" by (rule j) + finally show "?Y k = ?Y j" . + qed +qed + +lemma eventually_constant_iterate: + "eventually_constant (\n. iterate n\f)" +proof - + have "\y\range (\x. f\x). eventually_constant (\i. iterate i\f\y)" + by (simp add: eventually_constant_iterate_app) + hence "\y\range (\x. f\x). MOST i. MOST j. iterate j\f\y = iterate i\f\y" + unfolding eventually_constant_MOST_MOST . + hence "MOST i. MOST j. \y\range (\x. f\x). iterate j\f\y = iterate i\f\y" + by (simp only: MOST_finite_Ball_distrib [OF finite_range]) + hence "MOST i. MOST j. \x. iterate j\f\(f\x) = iterate i\f\(f\x)" + by simp + hence "MOST i. MOST j. \x. iterate (Suc j)\f\x = iterate (Suc i)\f\x" + by (simp only: iterate_Suc2) + hence "MOST i. MOST j. iterate (Suc j)\f = iterate (Suc i)\f" + by (simp only: cfun_eq_iff) + hence "eventually_constant (\i. iterate (Suc i)\f)" + unfolding eventually_constant_MOST_MOST . + thus "eventually_constant (\i. iterate i\f)" + by (rule eventually_constant_SucD) +qed + +abbreviation + d :: "'a \ 'a" +where + "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" +apply (rule MOST_d) +apply (subst iterate_Suc [symmetric]) +apply (rule eventually_constant_MOST_Suc_eq) +apply (rule eventually_constant_iterate_app) +done + +lemma d_fixed_iff: "d\x = x \ f\x = x" +proof + assume "d\x = x" + with f_d [where x=x] + show "f\x = x" by simp +next + assume f: "f\x = x" + have "\n. iterate n\f\x = x" + by (rule allI, rule nat.induct, simp, simp add: f) + hence "MOST n. iterate n\f\x = x" + by (rule ALL_MOST) + thus "d\x = x" + by (rule MOST_d) +qed + +lemma finite_deflation_d: "finite_deflation d" +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" .. + have "iterate n\f\(d\x) = d\x" + using f_d by (rule iterate_fixed) + thus "d\(d\x) = d\x" + by (simp add: n) +next + fix x :: 'a + show "d\x \ x" + by (rule MOST_d, simp add: iterate_below) +next + from finite_range + have "finite {x. f\x = x}" + by (rule finite_range_imp_finite_fixes) + thus "finite {x. d\x = x}" + by (simp add: d_fixed_iff) +qed + +lemma deflation_d: "deflation d" +using finite_deflation_d +by (rule finite_deflation_imp_deflation) + +end + +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)" +proof + interpret d: finite_deflation d by fact + fix x + show "\x. (d oo f)\x \ x" + by (simp, rule below_trans [OF d.below f]) + show "finite (range (\x. (d oo f)\x))" + by (rule finite_subset [OF _ d.finite_range], auto) +qed + +lemma eventual_iterate_oo_fixed_iff: + assumes "finite_deflation d" + assumes f: "\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_oo) + let ?g = "eventual (\n. iterate n\?e)" + show ?thesis + apply (subst e.d_fixed_iff) + apply simp + apply safe + apply (erule subst) + apply (rule d.idem) + apply (rule below_antisym) + apply (rule f) + apply (erule subst, rule d.below) + apply simp + 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 {* Take function for finite deflations *} + +definition + defl_take :: "nat \ (udom \ udom) \ (udom \ udom)" +where + "defl_take i d = eventual_iterate (udom_approx i oo d)" + +lemma finite_deflation_defl_take: + "deflation d \ finite_deflation (defl_take i d)" +unfolding defl_take_def +apply (rule pre_deflation.finite_deflation_d) +apply (rule pre_deflation_oo) +apply (rule finite_deflation_udom_approx) +apply (erule deflation.below) +done + +lemma deflation_defl_take: + "deflation d \ deflation (defl_take i d)" +apply (rule finite_deflation_imp_deflation) +apply (erule finite_deflation_defl_take) +done + +lemma defl_take_fixed_iff: + "deflation d \ defl_take i d\x = x \ udom_approx i\x = x \ d\x = x" +unfolding defl_take_def +apply (rule eventual_iterate_oo_fixed_iff) +apply (rule finite_deflation_udom_approx) +apply (erule deflation.below) +done + +lemma defl_take_below: + "\a \ b; deflation a; deflation b\ \ defl_take i a \ defl_take i b" +apply (rule deflation.belowI) +apply (erule deflation_defl_take) +apply (simp add: defl_take_fixed_iff) +apply (erule (1) deflation.belowD) +apply (erule conjunct2) +done + +lemma cont2cont_defl_take: + assumes cont: "cont f" and below: "\x y. f x\y \ y" + shows "cont (\x. defl_take i (f x))" +unfolding defl_take_def +using finite_deflation_udom_approx assms +by (rule cont2cont_eventual_iterate_oo) + +definition + fd_take :: "nat \ fin_defl \ fin_defl" +where + "fd_take i d = Abs_fin_defl (defl_take i (Rep_fin_defl d))" + +lemma Rep_fin_defl_fd_take: + "Rep_fin_defl (fd_take i d) = defl_take i (Rep_fin_defl d)" +unfolding fd_take_def +apply (rule Abs_fin_defl_inverse [unfolded mem_Collect_eq]) +apply (rule finite_deflation_defl_take) +apply (rule deflation_Rep_fin_defl) +done + +lemma fd_take_fixed_iff: + "Rep_fin_defl (fd_take i d)\x = x \ + udom_approx i\x = x \ Rep_fin_defl d\x = x" +unfolding Rep_fin_defl_fd_take +apply (rule defl_take_fixed_iff) +apply (rule deflation_Rep_fin_defl) +done + +lemma fd_take_below: "fd_take n d \ d" +apply (rule fin_defl_belowI) +apply (simp add: fd_take_fixed_iff) +done + +lemma fd_take_idem: "fd_take n (fd_take n d) = fd_take n d" +apply (rule fin_defl_eqI) +apply (simp add: fd_take_fixed_iff) +done + +lemma fd_take_mono: "a \ b \ fd_take n a \ fd_take n b" +apply (rule fin_defl_belowI) +apply (simp add: fd_take_fixed_iff) +apply (simp add: fin_defl_belowD) +done + +lemma approx_fixed_le_lemma: "\i \ j; udom_approx i\x = x\ \ udom_approx j\x = x" +apply (rule deflation.belowD) +apply (rule finite_deflation_imp_deflation) +apply (rule finite_deflation_udom_approx) +apply (erule chain_mono [OF chain_udom_approx]) +apply assumption +done + +lemma fd_take_chain: "m \ n \ fd_take m a \ fd_take n a" +apply (rule fin_defl_belowI) +apply (simp add: fd_take_fixed_iff) +apply (simp add: approx_fixed_le_lemma) +done + +lemma finite_range_fd_take: "finite (range (fd_take n))" +apply (rule finite_imageD [where f="\a. {x. Rep_fin_defl a\x = x}"]) +apply (rule finite_subset [where B="Pow {x. udom_approx n\x = x}"]) +apply (clarify, simp add: fd_take_fixed_iff) +apply (simp add: finite_deflation.finite_fixes [OF finite_deflation_udom_approx]) +apply (rule inj_onI, clarify) +apply (simp add: set_eq_iff fin_defl_eqI) +done + +lemma fd_take_covers: "\n. fd_take n a = a" +apply (rule_tac x= + "Max ((\x. LEAST n. udom_approx n\x = x) ` {x. Rep_fin_defl a\x = x})" in exI) +apply (rule below_antisym) +apply (rule fd_take_below) +apply (rule fin_defl_belowI) +apply (simp add: fd_take_fixed_iff) +apply (rule approx_fixed_le_lemma) +apply (rule Max_ge) +apply (rule finite_imageI) +apply (rule Rep_fin_defl.finite_fixes) +apply (rule imageI) +apply (erule CollectI) +apply (rule LeastI_ex) +apply (rule approx_chain.compact_eq_approx [OF udom_approx]) +apply (erule subst) +apply (rule Rep_fin_defl.compact) +done + +subsection {* Chain of approx functions on algebraic deflations *} + +definition + defl_approx :: "nat \ defl \ defl" +where + "defl_approx = (\i. defl.basis_fun (\d. defl_principal (fd_take i d)))" + +lemma defl_approx_principal: + "defl_approx i\(defl_principal d) = defl_principal (fd_take i d)" +unfolding defl_approx_def +by (simp add: defl.basis_fun_principal fd_take_mono) + +lemma defl_approx: "approx_chain defl_approx" +proof + show chain: "chain defl_approx" + unfolding defl_approx_def + by (simp add: chainI defl.basis_fun_mono fd_take_mono fd_take_chain) + show idem: "\i x. defl_approx i\(defl_approx i\x) = defl_approx i\x" + apply (induct_tac x rule: defl.principal_induct, simp) + apply (simp add: defl_approx_principal fd_take_idem) + done + show below: "\i x. defl_approx i\x \ x" + apply (induct_tac x rule: defl.principal_induct, simp) + apply (simp add: defl_approx_principal fd_take_below) + done + show lub: "(\i. defl_approx i) = ID" + apply (rule cfun_eqI, rule below_antisym) + apply (simp add: contlub_cfun_fun chain lub_below_iff chain below) + apply (induct_tac x rule: defl.principal_induct, simp) + apply (simp add: contlub_cfun_fun chain) + apply (simp add: compact_below_lub_iff defl.compact_principal chain) + apply (simp add: defl_approx_principal) + apply (subgoal_tac "\i. fd_take i a = a", metis below_refl) + apply (rule fd_take_covers) + done + show "\i. finite {x. defl_approx i\x = x}" + apply (rule finite_range_imp_finite_fixes) + apply (rule_tac B="defl_principal ` range (fd_take i)" in rev_finite_subset) + apply (simp add: finite_range_fd_take) + apply (clarsimp, rename_tac x) + apply (induct_tac x rule: defl.principal_induct) + apply (simp add: adm_mem_finite finite_range_fd_take) + apply (simp add: defl_approx_principal) + done +qed + +subsection {* Algebraic deflations are a bifinite domain *} + +instantiation defl :: bifinite +begin + +definition + "emb = udom_emb defl_approx" + +definition + "prj = udom_prj defl_approx" + +definition + "defl (t::defl itself) = + (\i. defl_principal (Abs_fin_defl (emb oo defl_approx i oo prj)))" + +instance proof + show ep: "ep_pair emb (prj :: udom \ defl)" + unfolding emb_defl_def prj_defl_def + by (rule ep_pair_udom [OF defl_approx]) + show "cast\DEFL(defl) = emb oo (prj :: udom \ defl)" + unfolding defl_defl_def + apply (subst contlub_cfun_arg) + apply (rule chainI) + apply (rule defl.principal_mono) + apply (simp add: below_fin_defl_def) + apply (simp add: Abs_fin_defl_inverse approx_chain.finite_deflation_approx [OF defl_approx] + ep_pair.finite_deflation_e_d_p [OF ep]) + apply (intro monofun_cfun below_refl) + apply (rule chainE) + apply (rule approx_chain.chain_approx [OF defl_approx]) + apply (subst cast_defl_principal) + apply (simp add: Abs_fin_defl_inverse approx_chain.finite_deflation_approx [OF defl_approx] + ep_pair.finite_deflation_e_d_p [OF ep]) + apply (simp add: lub_distribs approx_chain.chain_approx [OF defl_approx] + approx_chain.lub_approx [OF defl_approx]) + done +qed + +end + +end diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/Library/HOLCF_Library.thy --- a/src/HOLCF/Library/HOLCF_Library.thy Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/Library/HOLCF_Library.thy Sat Oct 16 16:39:06 2010 -0700 @@ -1,5 +1,6 @@ theory HOLCF_Library imports + Defl_Bifinite List_Cpo Stream Strict_Fun diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/Library/Stream.thy --- a/src/HOLCF/Library/Stream.thy Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/Library/Stream.thy Sat Oct 16 16:39:06 2010 -0700 @@ -265,7 +265,7 @@ apply (simp add: stream.bisim_def,clarsimp) apply (drule spec, drule spec, drule (1) mp) apply (case_tac "x", simp) - apply (case_tac "x'", simp) + apply (case_tac "y", simp) by auto @@ -508,7 +508,7 @@ by (insert sfilter_def [where 'a='a, THEN eq_reflection, THEN fix_eq2], auto) lemma strict_sfilter: "sfilter\\ = \" -apply (rule ext_cfun) +apply (rule cfun_eqI) apply (subst sfilter_unfold, auto) apply (case_tac "x=UU", auto) by (drule stream_exhaust_eq [THEN iffD1], auto) diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/Library/Strict_Fun.thy --- a/src/HOLCF/Library/Strict_Fun.thy Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/Library/Strict_Fun.thy Sat Oct 16 16:39:06 2010 -0700 @@ -37,13 +37,13 @@ unfolding sfun_rep_beta by (rule Rep_sfun [simplified]) lemma strictify_cancel: "f\\ = \ \ strictify\f = f" - by (simp add: expand_cfun_eq strictify_conv_if) + by (simp add: cfun_eq_iff strictify_conv_if) lemma sfun_abs_sfun_rep: "sfun_abs\(sfun_rep\f) = f" unfolding sfun_abs_def sfun_rep_def apply (simp add: cont_Abs_sfun cont_Rep_sfun) apply (simp add: Rep_sfun_inject [symmetric] Abs_sfun_inverse) - apply (simp add: expand_cfun_eq strictify_conv_if) + apply (simp add: cfun_eq_iff strictify_conv_if) apply (simp add: Rep_sfun [simplified]) done @@ -56,7 +56,7 @@ lemma ep_pair_sfun: "ep_pair sfun_rep sfun_abs" apply default apply (rule sfun_abs_sfun_rep) -apply (simp add: expand_cfun_below strictify_conv_if) +apply (simp add: cfun_below_iff strictify_conv_if) done interpretation sfun: ep_pair sfun_rep sfun_abs @@ -71,14 +71,14 @@ lemma sfun_map_ID: "sfun_map\ID\ID = ID" unfolding sfun_map_def - by (simp add: cfun_map_ID expand_cfun_eq) + by (simp add: cfun_map_ID cfun_eq_iff) lemma sfun_map_map: assumes "f2\\ = \" and "g2\\ = \" shows "sfun_map\f1\g1\(sfun_map\f2\g2\p) = sfun_map\(\ x. f2\(f1\x))\(\ x. g1\(g2\x))\p" unfolding sfun_map_def -by (simp add: expand_cfun_eq strictify_cancel assms cfun_map_map) +by (simp add: cfun_eq_iff strictify_cancel assms cfun_map_map) lemma ep_pair_sfun_map: assumes 1: "ep_pair e1 p1" @@ -193,7 +193,7 @@ next show "cast\DEFL('a \! 'b) = emb oo (prj :: udom \ 'a \! 'b)" unfolding emb_sfun_def prj_sfun_def defl_sfun_def cast_sfun_defl - by (simp add: cast_DEFL oo_def expand_cfun_eq sfun_map_map) + by (simp add: cast_DEFL oo_def cfun_eq_iff sfun_map_map) qed end diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/Lift.thy --- a/src/HOLCF/Lift.thy Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/Lift.thy Sat Oct 16 16:39:06 2010 -0700 @@ -43,12 +43,6 @@ text {* @{term UU} and @{term Def} *} -lemma Lift_exhaust: "x = \ \ (\y. x = Def y)" - by (induct x) simp_all - -lemma Lift_cases: "\x = \ \ P; \a. x = Def a \ P\ \ P" - by (insert Lift_exhaust) blast - lemma not_Undef_is_Def: "(x \ \) = (\y. x = Def y)" by (cases x) simp_all @@ -86,17 +80,6 @@ by (induct x) auto qed -text {* - \medskip Two specific lemmas for the combination of LCF and HOL - terms. -*} - -lemma cont_Rep_CFun_app [simp]: "\cont g; cont f\ \ cont(\x. ((f x)\(g x)) s)" -by (rule cont2cont_Rep_CFun [THEN cont2cont_fun]) - -lemma cont_Rep_CFun_app_app [simp]: "\cont g; cont f\ \ cont(\x. ((f x)\(g x)) s t)" -by (rule cont_Rep_CFun_app [THEN cont2cont_fun]) - subsection {* Further operations *} definition @@ -134,12 +117,12 @@ "(\x. f x \ g x) \ (FLIFT x. f x) \ (FLIFT x. g x)" apply (rule monofunE [where f=flift1]) apply (rule cont2mono [OF cont_flift1]) -apply (simp add: below_fun_ext) +apply (simp add: fun_below_iff) done lemma cont2cont_flift1 [simp, cont2cont]: "\\y. cont (\x. f x y)\ \ cont (\x. FLIFT y. f x y)" -apply (rule cont_flift1 [THEN cont2cont_app3]) +apply (rule cont_flift1 [THEN cont_compose]) apply simp done diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/LowerPD.thy --- a/src/HOLCF/LowerPD.thy Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/LowerPD.thy Sat Oct 16 16:39:06 2010 -0700 @@ -323,7 +323,7 @@ lemma lower_bind_basis_mono: "t \\ u \ lower_bind_basis t \ lower_bind_basis u" -unfolding expand_cfun_below +unfolding cfun_below_iff apply (erule lower_le_induct, safe) apply (simp add: monofun_cfun) apply (simp add: rev_below_trans [OF lower_plus_below1]) @@ -371,7 +371,7 @@ by (induct xs rule: lower_pd_induct, simp_all) lemma lower_map_ID: "lower_map\ID = ID" -by (simp add: expand_cfun_eq ID_def lower_map_ident) +by (simp add: cfun_eq_iff ID_def lower_map_ident) lemma lower_map_map: "lower_map\f\(lower_map\g\xs) = lower_map\(\ x. f\(g\x))\xs" @@ -483,7 +483,7 @@ next show "cast\DEFL('a lower_pd) = emb oo (prj :: udom \ 'a lower_pd)" unfolding emb_lower_pd_def prj_lower_pd_def defl_lower_pd_def cast_lower_defl - by (simp add: cast_DEFL oo_def expand_cfun_eq lower_map_map) + by (simp add: cast_DEFL oo_def cfun_eq_iff lower_map_map) qed end diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/Porder.thy --- a/src/HOLCF/Porder.thy Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/Porder.thy Sat Oct 16 16:39:06 2010 -0700 @@ -344,87 +344,6 @@ lemma lub_chain_maxelem: "\Y i = c; \i. Y i \ c\ \ lub (range Y) = c" by (blast dest: ub_rangeD intro: thelubI is_lubI ub_rangeI) -subsection {* Directed sets *} - -definition directed :: "'a set \ bool" where - "directed S \ (\x. x \ S) \ (\x\S. \y\S. \z\S. x \ z \ y \ z)" - -lemma directedI: - assumes 1: "\z. z \ S" - assumes 2: "\x y. \x \ S; y \ S\ \ \z\S. x \ z \ y \ z" - shows "directed S" - unfolding directed_def using prems by fast - -lemma directedD1: "directed S \ \z. z \ S" - unfolding directed_def by fast - -lemma directedD2: "\directed S; x \ S; y \ S\ \ \z\S. x \ z \ y \ z" - unfolding directed_def by fast - -lemma directedE1: - assumes S: "directed S" - obtains z where "z \ S" - by (insert directedD1 [OF S], fast) - -lemma directedE2: - assumes S: "directed S" - assumes x: "x \ S" and y: "y \ S" - obtains z where "z \ S" "x \ z" "y \ z" - by (insert directedD2 [OF S x y], fast) - -lemma directed_finiteI: - assumes U: "\U. \finite U; U \ S\ \ \z\S. U <| z" - shows "directed S" -proof (rule directedI) - have "finite {}" and "{} \ S" by simp_all - hence "\z\S. {} <| z" by (rule U) - thus "\z. z \ S" by simp -next - fix x y - assume "x \ S" and "y \ S" - hence "finite {x, y}" and "{x, y} \ S" by simp_all - hence "\z\S. {x, y} <| z" by (rule U) - thus "\z\S. x \ z \ y \ z" by simp -qed - -lemma directed_finiteD: - assumes S: "directed S" - shows "\finite U; U \ S\ \ \z\S. U <| z" -proof (induct U set: finite) - case empty - from S have "\z. z \ S" by (rule directedD1) - thus "\z\S. {} <| z" by simp -next - case (insert x F) - from `insert x F \ S` - have xS: "x \ S" and FS: "F \ S" by simp_all - from FS have "\y\S. F <| y" by fact - then obtain y where yS: "y \ S" and Fy: "F <| y" .. - obtain z where zS: "z \ S" and xz: "x \ z" and yz: "y \ z" - using S xS yS by (rule directedE2) - from Fy yz have "F <| z" by (rule is_ub_upward) - with xz have "insert x F <| z" by simp - with zS show "\z\S. insert x F <| z" .. -qed - -lemma not_directed_empty [simp]: "\ directed {}" - by (rule notI, drule directedD1, simp) - -lemma directed_singleton: "directed {x}" - by (rule directedI, auto) - -lemma directed_bin: "x \ y \ directed {x, y}" - by (rule directedI, auto) - -lemma directed_chain: "chain S \ directed (range S)" -apply (rule directedI) -apply (rule_tac x="S 0" in exI, simp) -apply (clarify, rename_tac m n) -apply (rule_tac x="S (max m n)" in bexI) -apply (simp add: chain_mono) -apply simp -done - text {* lemmata for improved admissibility introdution rule *} lemma infinite_chain_adm_lemma: diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/Product_Cpo.thy --- a/src/HOLCF/Product_Cpo.thy Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/Product_Cpo.thy Sat Oct 16 16:39:06 2010 -0700 @@ -267,14 +267,6 @@ apply (simp only: prod_contI) done -lemma cont_fst_snd_D1: - "cont (\p. f (fst p) (snd p)) \ cont (\x. f x y)" -by (drule cont_compose [OF _ cont_pair1], simp) - -lemma cont_fst_snd_D2: - "cont (\p. f (fst p) (snd p)) \ cont (\y. f x y)" -by (drule cont_compose [OF _ cont_pair2], simp) - lemma cont2cont_prod_case' [simp, cont2cont]: assumes f: "cont (\p. f (fst p) (fst (snd p)) (snd (snd p)))" assumes g: "cont (\x. g x)" diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/Representable.thy --- a/src/HOLCF/Representable.thy Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/Representable.thy Sat Oct 16 16:39:06 2010 -0700 @@ -45,7 +45,7 @@ by (simp add: coerce_def) lemma coerce_eq_ID [simp]: "(coerce :: 'a \ 'a) = ID" -by (rule ext_cfun, simp add: beta_coerce) +by (rule cfun_eqI, simp add: beta_coerce) lemma emb_coerce: "DEFL('a) \ DEFL('b) @@ -169,7 +169,7 @@ apply (simp add: emb_prj cast.below) done show "cast\DEFL('a) = emb oo (prj :: udom \ 'a)" - by (rule ext_cfun, simp add: defl emb_prj) + by (rule cfun_eqI, simp add: defl emb_prj) qed lemma typedef_DEFL: @@ -201,10 +201,10 @@ "isodefl d t \ cast\t = emb oo d oo prj" lemma isodeflI: "(\x. cast\t\x = emb\(d\(prj\x))) \ isodefl d t" -unfolding isodefl_def by (simp add: ext_cfun) +unfolding isodefl_def by (simp add: cfun_eqI) lemma cast_isodefl: "isodefl d t \ cast\t = (\ x. emb\(d\(prj\x)))" -unfolding isodefl_def by (simp add: ext_cfun) +unfolding isodefl_def by (simp add: cfun_eqI) lemma isodefl_strict: "isodefl d t \ d\\ = \" unfolding isodefl_def @@ -228,14 +228,14 @@ lemma isodefl_DEFL_imp_ID: "isodefl (d :: 'a \ 'a) DEFL('a) \ d = ID" unfolding isodefl_def apply (simp add: cast_DEFL) -apply (simp add: expand_cfun_eq) +apply (simp add: cfun_eq_iff) apply (rule allI) apply (drule_tac x="emb\x" in spec) apply simp done lemma isodefl_bottom: "isodefl \ \" -unfolding isodefl_def by (simp add: expand_cfun_eq) +unfolding isodefl_def by (simp add: cfun_eq_iff) lemma adm_isodefl: "cont f \ cont g \ adm (\x. isodefl (f x) (g x))" @@ -263,7 +263,7 @@ assumes DEFL: "DEFL('b) = DEFL('a)" shows "isodefl d t \ isodefl (coerce oo d oo coerce :: 'b \ 'b) t" unfolding isodefl_def -apply (simp add: expand_cfun_eq) +apply (simp add: cfun_eq_iff) apply (simp add: emb_coerce coerce_prj DEFL) done diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/Sprod.thy --- a/src/HOLCF/Sprod.thy Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/Sprod.thy Sat Oct 16 16:39:06 2010 -0700 @@ -250,7 +250,7 @@ by (cases "x = \ \ y = \") auto lemma sprod_map_ID: "sprod_map\ID\ID = ID" -unfolding sprod_map_def by (simp add: expand_cfun_eq eta_cfun) +unfolding sprod_map_def by (simp add: cfun_eq_iff eta_cfun) lemma sprod_map_map: "\f1\\ = \; g1\\ = \\ \ diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/Ssum.thy --- a/src/HOLCF/Ssum.thy Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/Ssum.thy Sat Oct 16 16:39:06 2010 -0700 @@ -234,7 +234,7 @@ by (cases "x = \") simp_all lemma ssum_map_ID: "ssum_map\ID\ID = ID" -unfolding ssum_map_def by (simp add: expand_cfun_eq eta_cfun) +unfolding ssum_map_def by (simp add: cfun_eq_iff eta_cfun) lemma ssum_map_map: "\f1\\ = \; g1\\ = \\ \ diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/Tools/Domain/domain_constructors.ML --- a/src/HOLCF/Tools/Domain/domain_constructors.ML Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Sat Oct 16 16:39:06 2010 -0700 @@ -7,26 +7,30 @@ signature DOMAIN_CONSTRUCTORS = sig + type constr_info = + { + iso_info : Domain_Take_Proofs.iso_info, + con_specs : (term * (bool * typ) list) list, + con_betas : thm list, + nchotomy : thm, + exhaust : thm, + compacts : thm list, + con_rews : thm list, + inverts : thm list, + injects : thm list, + dist_les : thm list, + dist_eqs : thm list, + cases : thm list, + sel_rews : thm list, + dis_rews : thm list, + match_rews : thm list + } val add_domain_constructors : binding -> (binding * (bool * binding option * typ) list * mixfix) list -> Domain_Take_Proofs.iso_info -> theory - -> { con_consts : term list, - con_betas : thm list, - nchotomy : thm, - exhaust : thm, - compacts : thm list, - con_rews : thm list, - inverts : thm list, - injects : thm list, - dist_les : thm list, - dist_eqs : thm list, - cases : thm list, - sel_rews : thm list, - dis_rews : thm list, - match_rews : thm list - } * theory; + -> constr_info * theory; end; @@ -39,6 +43,25 @@ infix -->>; infix 9 `; +type constr_info = + { + iso_info : Domain_Take_Proofs.iso_info, + con_specs : (term * (bool * typ) list) list, + con_betas : thm list, + nchotomy : thm, + exhaust : thm, + compacts : thm list, + con_rews : thm list, + inverts : thm list, + injects : thm list, + dist_les : thm list, + dist_eqs : thm list, + cases : thm list, + sel_rews : thm list, + dis_rews : thm list, + match_rews : thm list + } + (************************** miscellaneous functions ***************************) val simple_ss = HOL_basic_ss addsimps simp_thms; @@ -833,6 +856,9 @@ (thy : theory) = let val dname = Binding.name_of dbind; + val _ = writeln ("Proving isomorphism properties of domain "^dname^" ..."); + + val bindings = map #1 spec; (* retrieve facts about rep/abs *) val lhsT = #absT iso_info; @@ -844,6 +870,7 @@ val abs_strict = iso_locale RS @{thm iso.abs_strict}; val rep_defined_iff = iso_locale RS @{thm iso.rep_defined_iff}; val abs_defined_iff = iso_locale RS @{thm iso.abs_defined_iff}; + val iso_rews = [abs_iso_thm, rep_iso_thm, abs_strict, rep_strict]; (* qualify constants and theorems with domain name *) val thy = Sign.add_path dname thy; @@ -857,18 +884,22 @@ in add_constructors con_spec abs_const iso_locale thy end; - val {con_consts, con_betas, exhaust, ...} = con_result; + val {con_consts, con_betas, nchotomy, exhaust, compacts, con_rews, + inverts, injects, dist_les, dist_eqs} = con_result; + + (* prepare constructor spec *) + val con_specs : (term * (bool * typ) list) list = + let + fun prep_arg (lazy, sel, T) = (lazy, T); + fun prep_con c (b, args, mx) = (c, map prep_arg args); + in + map2 prep_con con_consts spec + end; (* define case combinator *) val ((case_const : typ -> term, cases : thm list), thy) = - let - fun prep_arg (lazy, sel, T) = (lazy, T); - fun prep_con c (b, args, mx) = (c, map prep_arg args); - val case_spec = map2 prep_con con_consts spec; - in - add_case_combinator case_spec lhsT dbind + add_case_combinator con_specs lhsT dbind con_betas exhaust iso_locale rep_const thy - end; (* define and prove theorems for selector functions *) val (sel_thms : thm list, thy : theory) = @@ -882,46 +913,61 @@ (* define and prove theorems for discriminator functions *) val (dis_thms : thm list, thy : theory) = - let - val bindings = map #1 spec; - fun prep_arg (lazy, sel, T) = (lazy, T); - fun prep_con c (b, args, mx) = (c, map prep_arg args); - val dis_spec = map2 prep_con con_consts spec; - in - add_discriminators bindings dis_spec lhsT - exhaust case_const cases thy - end + add_discriminators bindings con_specs lhsT + exhaust case_const cases thy; (* define and prove theorems for match combinators *) val (match_thms : thm list, thy : theory) = - let - val bindings = map #1 spec; - fun prep_arg (lazy, sel, T) = (lazy, T); - fun prep_con c (b, args, mx) = (c, map prep_arg args); - val mat_spec = map2 prep_con con_consts spec; - in - add_match_combinators bindings mat_spec lhsT - exhaust case_const cases thy - end + add_match_combinators bindings con_specs lhsT + exhaust case_const cases thy; (* restore original signature path *) val thy = Sign.parent_path thy; + (* bind theorem names in global theory *) + val (_, thy) = + let + fun qualified name = Binding.qualified true name dbind; + val names = "bottom" :: map (fn (b,_,_) => Binding.name_of b) spec; + val dname = fst (dest_Type lhsT); + val simp = Simplifier.simp_add; + val case_names = Rule_Cases.case_names names; + val cases_type = Induct.cases_type dname; + in + Global_Theory.add_thmss [ + ((qualified "iso_rews" , iso_rews ), [simp]), + ((qualified "nchotomy" , [nchotomy] ), []), + ((qualified "exhaust" , [exhaust] ), [case_names, cases_type]), + ((qualified "when_rews" , cases ), [simp]), + ((qualified "compacts" , compacts ), [simp]), + ((qualified "con_rews" , con_rews ), [simp]), + ((qualified "sel_rews" , sel_thms ), [simp]), + ((qualified "dis_rews" , dis_thms ), [simp]), + ((qualified "dist_les" , dist_les ), [simp]), + ((qualified "dist_eqs" , dist_eqs ), [simp]), + ((qualified "inverts" , inverts ), [simp]), + ((qualified "injects" , injects ), [simp]), + ((qualified "match_rews", match_thms ), [simp])] thy + end; + val result = - { con_consts = con_consts, + { + iso_info = iso_info, + con_specs = con_specs, con_betas = con_betas, - nchotomy = #nchotomy con_result, + nchotomy = nchotomy, exhaust = exhaust, - compacts = #compacts con_result, - con_rews = #con_rews con_result, - inverts = #inverts con_result, - injects = #injects con_result, - dist_les = #dist_les con_result, - dist_eqs = #dist_eqs con_result, + compacts = compacts, + con_rews = con_rews, + inverts = inverts, + injects = injects, + dist_les = dist_les, + dist_eqs = dist_eqs, cases = cases, sel_rews = sel_thms, dis_rews = dis_thms, - match_rews = match_thms }; + match_rews = match_thms + }; in (result, thy) end; diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/Tools/Domain/domain_extender.ML --- a/src/HOLCF/Tools/Domain/domain_extender.ML Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML Sat Oct 16 16:39:06 2010 -0700 @@ -35,7 +35,15 @@ structure Domain_Extender :> DOMAIN_EXTENDER = struct -open Domain_Library; +open HOLCF_Library; + +fun first (x,_,_) = x; +fun second (_,x,_) = x; +fun third (_,_,x) = x; + +fun upd_first f (x,y,z) = (f x, y, z); +fun upd_second f (x,y,z) = ( x, f y, z); +fun upd_third f (x,y,z) = ( x, y, f z); (* ----- general testing and preprocessing of constructor list -------------- *) fun check_and_sort_domain @@ -94,22 +102,22 @@ | SOME typevars => if indirect then error ("Indirect recursion of type " ^ - quote (string_of_typ thy t)) + quote (Syntax.string_of_typ_global thy t)) else if dname <> s orelse (** BUG OR FEATURE?: mutual recursion may use different arguments **) remove_sorts typevars = remove_sorts typl then Type(s,map (analyse true) typl) else error ("Direct recursion of type " ^ - quote (string_of_typ thy t) ^ + quote (Syntax.string_of_typ_global thy t) ^ " with different arguments")) - | analyse indirect (TVar _) = Imposs "extender:analyse"; + | analyse indirect (TVar _) = error "extender:analyse"; fun check_pcpo lazy T = let val sort = arg_sort lazy in if Sign.of_sort thy (T, sort) then T else error ("Constructor argument type is not of sort " ^ Syntax.string_of_sort_global thy sort ^ ": " ^ - string_of_typ thy T) + Syntax.string_of_typ_global thy T) end; fun analyse_arg (lazy, sel, T) = (lazy, sel, check_pcpo lazy (analyse false T)); @@ -167,7 +175,7 @@ check_and_sort_domain arg_sort dtnvs' cons'' tmp_thy; val dts : typ list = map (Type o fst) eqs'; - fun mk_arg_typ (lazy, dest_opt, T) = if lazy then mk_uT T else T; + fun mk_arg_typ (lazy, dest_opt, T) = if lazy then mk_upT T else T; fun mk_con_typ (bind, args, mx) = if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args); fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons); @@ -179,28 +187,17 @@ val ((iso_infos, take_info), thy) = add_isos iso_spec thy; - val new_dts : (string * string list) list = - map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs'; - fun one_con (con,args,mx) : cons = - (Binding.name_of con, (* FIXME preverse binding (!?) *) - ListPair.map (fn ((lazy,sel,tp),vn) => - mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp), vn)) - (args, Datatype_Prop.make_tnames (map third args))); - val eqs : eq list = - map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs'; + val (constr_infos, thy) = + thy + |> fold_map (fn ((dbind, (_,cs)), info) => + Domain_Constructors.add_domain_constructors dbind cs info) + (dbinds ~~ eqs' ~~ iso_infos); - val ((rewss, take_rews), theorems_thy) = - thy - |> fold_map (fn (((dbind, eq), (_,cs)), info) => - Domain_Theorems.theorems (eq, eqs) dbind cs info take_info) - (dbinds ~~ eqs ~~ eqs' ~~ iso_infos) - ||>> Domain_Theorems.comp_theorems (comp_dbind, eqs) take_info; + val (take_rews, thy) = + Domain_Theorems.comp_theorems comp_dbind + dbinds take_info constr_infos thy; in - theorems_thy - |> Global_Theory.add_thmss - [((Binding.qualified true "rews" comp_dbind, - flat rewss @ take_rews), [])] - |> snd + thy end; fun define_isos (spec : (binding * mixfix * (typ * typ)) list) = diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Sat Oct 16 16:39:06 2010 -0700 @@ -639,9 +639,8 @@ val (take_info, thy) = Domain_Take_Proofs.define_take_functions (dbinds ~~ iso_infos) thy; - val { take_consts, take_defs, chain_take_thms, take_0_thms, - take_Suc_thms, deflation_take_thms, - finite_consts, finite_defs } = take_info; + val { take_consts, chain_take_thms, take_0_thms, take_Suc_thms, ...} = + take_info; (* least-upper-bound lemma for take functions *) val lub_take_lemma = diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/Tools/Domain/domain_library.ML --- a/src/HOLCF/Tools/Domain/domain_library.ML Fri Oct 15 17:21:37 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,239 +0,0 @@ -(* Title: HOLCF/Tools/Domain/domain_library.ML - Author: David von Oheimb - -Library for domain command. -*) - - -(* infix syntax *) - -infixr 5 -->; -infixr 6 ->>; -infixr 0 ===>; -infixr 0 ==>; -infix 0 ==; -infix 1 ===; -infix 1 ~=; - -infix 9 ` ; -infix 9 `% ; -infix 9 `%%; - - -(* ----- specific support for domain ---------------------------------------- *) - -signature DOMAIN_LIBRARY = -sig - val first : 'a * 'b * 'c -> 'a - val second : 'a * 'b * 'c -> 'b - val third : 'a * 'b * 'c -> 'c - val upd_second : ('b -> 'd) -> 'a * 'b * 'c -> 'a * 'd * 'c - val upd_third : ('c -> 'd) -> 'a * 'b * 'c -> 'a * 'b * 'd - val mapn : (int -> 'a -> 'b) -> int -> 'a list -> 'b list - val atomize : Proof.context -> thm -> thm list - - val Imposs : string -> 'a; - val cpo_type : theory -> typ -> bool; - val pcpo_type : theory -> typ -> bool; - val string_of_typ : theory -> typ -> string; - - (* Creating HOLCF types *) - val mk_ssumT : typ * typ -> typ; - val mk_sprodT : typ * typ -> typ; - val mk_uT : typ -> typ; - val oneT : typ; - val pcpoS : sort; - - (* Creating HOLCF terms *) - val %: : string -> term; - val %%: : string -> term; - val ` : term * term -> term; - val `% : term * string -> term; - val UU : term; - val ID : term; - val list_ccomb : term * term list -> term; - val con_app2 : string -> ('a -> term) -> 'a list -> term; - val prj : ('a -> 'b -> 'a) -> ('a -> 'b -> 'a) -> 'a -> 'b list -> int -> 'a - val proj : term -> 'a list -> int -> term; - - (* Creating propositions *) - val mk_conj : term * term -> term; - val mk_disj : term * term -> term; - val mk_imp : term * term -> term; - val mk_lam : string * term -> term; - val mk_all : string * term -> term; - val mk_ex : string * term -> term; - val mk_constrainall : string * typ * term -> term; - val === : term * term -> term; - val defined : term -> term; - val mk_adm : term -> term; - val lift : ('a -> term) -> 'a list * term -> term; - val lift_defined : ('a -> term) -> 'a list * term -> term; - - (* Creating meta-propositions *) - val mk_trp : term -> term; (* HOLogic.mk_Trueprop *) - val == : term * term -> term; - val ===> : term * term -> term; - val mk_All : string * term -> term; - - (* Domain specifications *) - eqtype arg; - type cons = string * arg list; - type eq = (string * typ list) * cons list; - val mk_arg : (bool * Datatype.dtyp) * string -> arg; - val is_lazy : arg -> bool; - val rec_of : arg -> int; - val dtyp_of : arg -> Datatype.dtyp; - val vname : arg -> string; - val upd_vname : (string -> string) -> arg -> arg; - val is_rec : arg -> bool; - val is_nonlazy_rec : arg -> bool; - val nonlazy : arg list -> string list; - val nonlazy_rec : arg list -> string list; - val %# : arg -> term; - val bound_arg : ''a list -> ''a -> term; (* ''a = arg or string *) - val idx_name : 'a list -> string -> int -> string; - val con_app : string -> arg list -> term; -end; - -structure Domain_Library :> DOMAIN_LIBRARY = -struct - -fun first (x,_,_) = x; -fun second (_,x,_) = x; -fun third (_,_,x) = x; - -fun upd_first f (x,y,z) = (f x, y, z); -fun upd_second f (x,y,z) = ( x, f y, z); -fun upd_third f (x,y,z) = ( x, y, f z); - -fun mapn f n [] = [] - | mapn f n (x::xs) = (f n x) :: mapn f (n+1) xs; - -fun foldr'' f (l,f2) = - let fun itr [] = raise Fail "foldr''" - | itr [a] = f2 a - | itr (a::l) = f(a, itr l) - in itr l end; - -fun atomize ctxt thm = - let - val r_inst = read_instantiate ctxt; - fun at thm = - case concl_of thm of - _$(Const(@{const_name HOL.conj},_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2) - | _$(Const(@{const_name All} ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec)) - | _ => [thm]; - in map zero_var_indexes (at thm) end; - -exception Impossible of string; -fun Imposs msg = raise Impossible ("Domain:"^msg); - -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; - -(* ----- constructor list handling ----- *) - -type arg = - (bool * Datatype.dtyp) * (* (lazy, recursive element) *) - string; (* argument name *) - -type cons = - string * (* operator name of constr *) - arg list; (* argument list *) - -type eq = - (string * (* name of abstracted type *) - typ list) * (* arguments of abstracted type *) - cons list; (* represented type, as a constructor list *) - -val mk_arg = I; - -fun rec_of ((_,dtyp),_) = - case dtyp of Datatype_Aux.DtRec i => i | _ => ~1; -(* FIXME: what about indirect recursion? *) - -fun is_lazy arg = fst (fst arg); -fun dtyp_of arg = snd (fst arg); -val vname = snd; -val upd_vname = apsnd; -fun is_rec arg = rec_of arg >=0; -fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg); -fun nonlazy args = map vname (filter_out is_lazy args); -fun nonlazy_rec args = map vname (filter is_nonlazy_rec args); - - -(* ----- support for type and mixfix expressions ----- *) - -fun mk_uT T = Type(@{type_name "u"}, [T]); -fun mk_sprodT (T, U) = Type(@{type_name sprod}, [T, U]); -fun mk_ssumT (T, U) = Type(@{type_name ssum}, [T, U]); -val oneT = @{typ one}; - -(* ----- support for term expressions ----- *) - -fun %: s = Free(s,dummyT); -fun %# arg = %:(vname arg); -fun %%: s = Const(s,dummyT); - -local open HOLogic in -val mk_trp = mk_Trueprop; -fun mk_conj (S,T) = conj $ S $ T; -fun mk_disj (S,T) = disj $ S $ T; -fun mk_imp (S,T) = imp $ S $ T; -fun mk_lam (x,T) = Abs(x,dummyT,T); -fun mk_all (x,P) = HOLogic.mk_all (x,dummyT,P); -fun mk_ex (x,P) = mk_exists (x,dummyT,P); -fun mk_constrainall (x,typ,P) = %%: @{const_name All} $ (Type.constraint (typ --> boolT) (mk_lam(x,P))); -end - -fun mk_All (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *) - -infixr 0 ===>; fun S ===> T = %%: "==>" $ S $ T; -infix 0 ==; fun S == T = %%: "==" $ S $ T; -infix 1 ===; fun S === T = %%: @{const_name HOL.eq} $ S $ T; -infix 1 ~=; fun S ~= T = HOLogic.mk_not (S === T); - -infix 9 ` ; fun f ` x = %%: @{const_name Rep_CFun} $ f $ x; -infix 9 `% ; fun f`% s = f` %: s; -infix 9 `%%; fun f`%%s = f` %%:s; - -fun mk_adm t = %%: @{const_name adm} $ t; -val ID = %%: @{const_name ID}; -fun mk_strictify t = %%: @{const_name strictify}`t; -fun mk_ssplit t = %%: @{const_name ssplit}`t; -fun mk_sscase (x, y) = %%: @{const_name sscase}`x`y; -fun mk_fup (t,u) = %%: @{const_name fup} ` t ` u; - -val pcpoS = @{sort pcpo}; - -val list_ccomb = Library.foldl (op `); (* continuous version of list_comb *) -fun con_app2 con f args = list_ccomb(%%:con,map f args); -fun con_app con = con_app2 con %#; -fun prj _ _ x ( _::[]) _ = x - | prj _ _ _ [] _ = raise Fail "Domain_Library.prj: empty list" - | prj f1 _ x (_::y::ys) 0 = f1 x y - | prj f1 f2 x (y:: ys) j = prj f1 f2 (f2 x y) ys (j-1); -fun proj x = prj (fn S => K (%%: @{const_name fst} $ S)) (fn S => K (%%: @{const_name snd} $ S)) x; -fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t)); - -val UU = %%: @{const_name UU}; -fun defined t = t ~= UU; -fun cpair (t,u) = %%: @{const_name Pair} $ t $ u; -fun spair (t,u) = %%: @{const_name spair}`t`u; -fun lift_defined f = lift (fn x => defined (f x)); -fun bound_arg vns v = Bound (length vns - find_index (fn v' => v' = v) vns - 1); - -fun cont_eta_contract (Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body)) = - (case cont_eta_contract body of - body' as (Const("Cfun.Rep_CFun",Ta) $ f $ Bound 0) => - if not (member (op =) (loose_bnos f) 0) then incr_boundvars ~1 f - else Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body') - | body' => Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body')) - | cont_eta_contract(f$t) = cont_eta_contract f $ cont_eta_contract t - | cont_eta_contract t = t; - -fun idx_name dnames s n = s^(if length dnames = 1 then "" else string_of_int n); - -end; (* struct *) diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/Tools/Domain/domain_take_proofs.ML --- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Sat Oct 16 16:39:06 2010 -0700 @@ -24,6 +24,7 @@ take_0_thms : thm list, take_Suc_thms : thm list, deflation_take_thms : thm list, + take_strict_thms : thm list, finite_consts : term list, finite_defs : thm list } @@ -35,6 +36,7 @@ take_0_thms : thm list, take_Suc_thms : thm list, deflation_take_thms : thm list, + take_strict_thms : thm list, finite_consts : term list, finite_defs : thm list, lub_take_thms : thm list, @@ -80,6 +82,7 @@ take_0_thms : thm list, take_Suc_thms : thm list, deflation_take_thms : thm list, + take_strict_thms : thm list, finite_consts : term list, finite_defs : thm list }; @@ -92,6 +95,7 @@ take_0_thms : thm list, take_Suc_thms : thm list, deflation_take_thms : thm list, + take_strict_thms : thm list, finite_consts : term list, finite_defs : thm list, lub_take_thms : thm list, @@ -299,7 +303,7 @@ val tac = simp_tac (HOL_basic_ss addsimps rules) 1; val take_0_thm = Goal.prove_global thy [] [] goal (K tac); in - add_qualified_thm "take_0" (dbind, take_0_thm) thy + add_qualified_simp_thm "take_0" (dbind, take_0_thm) thy end; val (take_0_thms, thy) = fold_map prove_take_0 (take_consts ~~ dbinds ~~ dom_eqns) thy; @@ -369,7 +373,7 @@ Drule.zero_var_indexes (@{thm deflation_strict} OF [deflation_take]); in - add_qualified_thm "take_strict" (dbind, take_strict_thm) thy + add_qualified_simp_thm "take_strict" (dbind, take_strict_thm) thy end; val (take_strict_thms, thy) = fold_map prove_take_strict @@ -429,6 +433,7 @@ take_0_thms = take_0_thms, take_Suc_thms = take_Suc_thms, deflation_take_thms = deflation_take_thms, + take_strict_thms = take_strict_thms, finite_consts = finite_consts, finite_defs = finite_defs }; @@ -593,6 +598,7 @@ take_0_thms = #take_0_thms take_info, take_Suc_thms = #take_Suc_thms take_info, deflation_take_thms = #deflation_take_thms take_info, + take_strict_thms = #take_strict_thms take_info, finite_consts = #finite_consts take_info, finite_defs = #finite_defs take_info, lub_take_thms = lub_take_thms, diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/Tools/Domain/domain_theorems.ML --- a/src/HOLCF/Tools/Domain/domain_theorems.ML Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Sat Oct 16 16:39:06 2010 -0700 @@ -9,17 +9,10 @@ signature DOMAIN_THEOREMS = sig - val theorems: - Domain_Library.eq * Domain_Library.eq list -> - binding -> - (binding * (bool * binding option * typ) list * mixfix) list -> - Domain_Take_Proofs.iso_info -> + val comp_theorems : + binding -> binding list -> Domain_Take_Proofs.take_induct_info -> - theory -> thm list * theory; - - val comp_theorems : - binding * Domain_Library.eq list -> - Domain_Take_Proofs.take_induct_info -> + Domain_Constructors.constr_info list -> theory -> thm list * theory val quiet_mode: bool Unsynchronized.ref; @@ -35,18 +28,11 @@ fun message s = if !quiet_mode then () else writeln s; fun trace s = if !trace_domain then tracing s else (); -open Domain_Library; +open HOLCF_Library; infixr 0 ===>; -infixr 0 ==>; infix 0 == ; infix 1 ===; -infix 1 ~= ; -infix 1 <<; -infix 1 ~<<; infix 9 ` ; -infix 9 `% ; -infix 9 `%%; -infixr 9 oo; (* ----- general proof facilities ------------------------------------------- *) @@ -91,340 +77,218 @@ else cut_facts_tac prems 1 :: tacsf context; in pg'' thy defs t tacs end; -(* FIXME!!!!!!!!! *) -(* We should NEVER re-parse variable names as strings! *) -(* The names can conflict with existing constants or other syntax! *) -fun case_UU_tac ctxt rews i v = - InductTacs.case_tac ctxt (v^"=UU") i THEN - asm_simp_tac (HOLCF_ss addsimps rews) i; +(******************************************************************************) +(***************************** proofs about take ******************************) +(******************************************************************************) + +fun take_theorems + (dbinds : binding list) + (take_info : Domain_Take_Proofs.take_induct_info) + (constr_infos : Domain_Constructors.constr_info list) + (thy : theory) : thm list list * theory = +let + val {take_consts, take_Suc_thms, deflation_take_thms, ...} = take_info; + val deflation_thms = Domain_Take_Proofs.get_deflation_thms thy; + + val n = Free ("n", @{typ nat}); + val n' = @{const Suc} $ n; + + local + val newTs = map (#absT o #iso_info) constr_infos; + val subs = newTs ~~ map (fn t => t $ n) take_consts; + fun is_ID (Const (c, _)) = (c = @{const_name ID}) + | is_ID _ = false; + in + fun map_of_arg v T = + let val m = Domain_Take_Proofs.map_of_typ thy subs T; + in if is_ID m then v else mk_capply (m, v) end; + end + + fun prove_take_apps + ((dbind, take_const), constr_info) thy = + let + val {iso_info, con_specs, con_betas, ...} = constr_info; + val {abs_inverse, ...} = iso_info; + fun prove_take_app (con_const, args) = + let + val Ts = map snd args; + val ns = Name.variant_list ["n"] (Datatype_Prop.make_tnames Ts); + val vs = map Free (ns ~~ Ts); + val lhs = mk_capply (take_const $ n', list_ccomb (con_const, vs)); + val rhs = list_ccomb (con_const, map2 map_of_arg vs Ts); + val goal = mk_trp (mk_eq (lhs, rhs)); + val rules = + [abs_inverse] @ con_betas @ @{thms take_con_rules} + @ take_Suc_thms @ deflation_thms @ deflation_take_thms; + val tac = simp_tac (HOL_basic_ss addsimps rules) 1; + in + Goal.prove_global thy [] [] goal (K tac) + end; + val take_apps = map prove_take_app con_specs; + in + yield_singleton Global_Theory.add_thmss + ((Binding.qualified true "take_rews" dbind, take_apps), + [Simplifier.simp_add]) thy + end; +in + fold_map prove_take_apps + (dbinds ~~ take_consts ~~ constr_infos) thy +end; (* ----- general proofs ----------------------------------------------------- *) val all2E = @{lemma "!x y . P x y ==> (P x y ==> R) ==> R" by simp} -fun theorems - (((dname, _), cons) : eq, eqs : eq list) - (dbind : binding) - (spec : (binding * (bool * binding option * typ) list * mixfix) list) - (iso_info : Domain_Take_Proofs.iso_info) - (take_info : Domain_Take_Proofs.take_induct_info) - (thy : theory) = -let - -val _ = message ("Proving isomorphism properties of domain "^dname^" ..."); -val map_tab = Domain_Take_Proofs.get_map_tab thy; - - -(* ----- getting the axioms and definitions --------------------------------- *) - -val ax_abs_iso = #abs_inverse iso_info; -val ax_rep_iso = #rep_inverse iso_info; - -val abs_const = #abs_const iso_info; -val rep_const = #rep_const iso_info; - -local - fun ga s dn = Global_Theory.get_thm thy (dn ^ "." ^ s); -in - val ax_take_0 = ga "take_0" dname; - val ax_take_strict = ga "take_strict" dname; -end; (* local *) - -val {take_Suc_thms, deflation_take_thms, ...} = take_info; - -(* ----- define constructors ------------------------------------------------ *) - -val (result, thy) = - Domain_Constructors.add_domain_constructors dbind spec iso_info thy; - -val con_appls = #con_betas result; -val {nchotomy, exhaust, ...} = result; -val {compacts, con_rews, inverts, injects, dist_les, dist_eqs, ...} = result; -val {sel_rews, ...} = result; -val when_rews = #cases result; -val when_strict = hd when_rews; -val dis_rews = #dis_rews result; -val mat_rews = #match_rews result; - -(* ----- theorems concerning the isomorphism -------------------------------- *) - -val pg = pg' thy; - -val retraction_strict = @{thm retraction_strict}; -val abs_strict = ax_rep_iso RS (allI RS retraction_strict); -val rep_strict = ax_abs_iso RS (allI RS retraction_strict); -val iso_rews = [ax_abs_iso, ax_rep_iso, abs_strict, rep_strict]; - -(* ----- theorems concerning one induction step ----------------------------- *) - -local - fun dc_take dn = %%:(dn^"_take"); - val dnames = map (fst o fst) eqs; - val deflation_thms = Domain_Take_Proofs.get_deflation_thms thy; - - fun copy_of_dtyp tab r dt = - if Datatype_Aux.is_rec_type dt then copy tab r dt else ID - and copy tab r (Datatype_Aux.DtRec i) = r i - | copy tab r (Datatype_Aux.DtTFree a) = ID - | copy tab r (Datatype_Aux.DtType (c, ds)) = - case Symtab.lookup tab c of - SOME f => list_ccomb (%%:f, map (copy_of_dtyp tab r) ds) - | NONE => (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID); - - fun one_take_app (con, args) = - let - fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n"; - fun one_rhs arg = - if Datatype_Aux.is_rec_type (dtyp_of arg) - then copy_of_dtyp map_tab - mk_take (dtyp_of arg) ` (%# arg) - else (%# arg); - val lhs = (dc_take dname $ (%%: @{const_name Suc} $ %:"n")) ` (con_app con args); - val rhs = con_app2 con one_rhs args; - val goal = mk_trp (lhs === rhs); - val rules = - [ax_abs_iso] @ @{thms take_con_rules} - @ take_Suc_thms @ deflation_thms @ deflation_take_thms; - val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1]; - in pg con_appls goal (K tacs) end; - val take_apps = map one_take_app cons; -in - val take_rews = ax_take_0 :: ax_take_strict :: take_apps; -end; - -val case_ns = - "bottom" :: map (fn (b,_,_) => Binding.name_of b) spec; - -fun qualified name = Binding.qualified true name dbind; -val simp = Simplifier.simp_add; - -in - thy - |> Global_Theory.add_thmss [ - ((qualified "iso_rews" , iso_rews ), [simp]), - ((qualified "nchotomy" , [nchotomy] ), []), - ((qualified "exhaust" , [exhaust] ), - [Rule_Cases.case_names case_ns, Induct.cases_type dname]), - ((qualified "when_rews" , when_rews ), [simp]), - ((qualified "compacts" , compacts ), [simp]), - ((qualified "con_rews" , con_rews ), [simp]), - ((qualified "sel_rews" , sel_rews ), [simp]), - ((qualified "dis_rews" , dis_rews ), [simp]), - ((qualified "dist_les" , dist_les ), [simp]), - ((qualified "dist_eqs" , dist_eqs ), [simp]), - ((qualified "inverts" , inverts ), [simp]), - ((qualified "injects" , injects ), [simp]), - ((qualified "take_rews" , take_rews ), [simp]), - ((qualified "match_rews", mat_rews ), [simp])] - |> snd - |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @ - dist_les @ dist_eqs) -end; (* let *) +val case_UU_allI = + @{lemma "(!!x. x ~= UU ==> P x) ==> P UU ==> ALL x. P x" by metis}; (******************************************************************************) (****************************** induction rules *******************************) (******************************************************************************) fun prove_induction - (comp_dbind : binding, eqs : eq list) + (comp_dbind : binding) + (constr_infos : Domain_Constructors.constr_info list) + (take_info : Domain_Take_Proofs.take_induct_info) (take_rews : thm list) - (take_info : Domain_Take_Proofs.take_induct_info) (thy : theory) = let - val comp_dname = Sign.full_name thy comp_dbind; - val dnames = map (fst o fst) eqs; - val conss = map snd eqs; - fun dc_take dn = %%:(dn^"_take"); - val x_name = idx_name dnames "x"; - val P_name = idx_name dnames "P"; - val pg = pg' thy; + val comp_dname = Binding.name_of comp_dbind; + + val iso_infos = map #iso_info constr_infos; + val exhausts = map #exhaust constr_infos; + val con_rews = maps #con_rews constr_infos; + val {take_consts, take_induct_thms, ...} = take_info; - local - fun ga s dn = Global_Theory.get_thm thy (dn ^ "." ^ s); - fun gts s dn = Global_Theory.get_thms thy (dn ^ "." ^ s); - in - val axs_rep_iso = map (ga "rep_iso") dnames; - val axs_abs_iso = map (ga "abs_iso") dnames; - val exhausts = map (ga "exhaust" ) dnames; - val con_rews = maps (gts "con_rews" ) dnames; - end; + val newTs = map #absT iso_infos; + val P_names = Datatype_Prop.indexify_names (map (K "P") newTs); + val x_names = Datatype_Prop.indexify_names (map (K "x") newTs); + val P_types = map (fn T => T --> HOLogic.boolT) newTs; + val Ps = map Free (P_names ~~ P_types); + val xs = map Free (x_names ~~ newTs); + val n = Free ("n", HOLogic.natT); - val {take_consts, ...} = take_info; - val {take_0_thms, take_Suc_thms, chain_take_thms, ...} = take_info; - val {lub_take_thms, finite_defs, reach_thms, ...} = take_info; - val {take_induct_thms, ...} = take_info; - - fun one_con p (con, args) = + fun con_assm defined p (con, args) = let - val P_names = map P_name (1 upto (length dnames)); - val vns = Name.variant_list P_names (map vname args); - val nonlazy_vns = map snd (filter_out (is_lazy o fst) (args ~~ vns)); - fun ind_hyp arg = %:(P_name (1 + rec_of arg)) $ bound_arg args arg; - val t1 = mk_trp (%:p $ con_app2 con (bound_arg args) args); - val t2 = lift ind_hyp (filter is_rec args, t1); - val t3 = lift_defined (bound_arg vns) (nonlazy_vns, t2); - in Library.foldr mk_All (vns, t3) end; + val Ts = map snd args; + val ns = Name.variant_list P_names (Datatype_Prop.make_tnames Ts); + val vs = map Free (ns ~~ Ts); + val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs)); + fun ind_hyp (v, T) t = + case AList.lookup (op =) (newTs ~~ Ps) T of NONE => t + | SOME p' => Logic.mk_implies (mk_trp (p' $ v), t); + val t1 = mk_trp (p $ list_ccomb (con, vs)); + val t2 = fold_rev ind_hyp (vs ~~ Ts) t1; + val t3 = Logic.list_implies (map (mk_trp o mk_defined) nonlazy, t2); + in fold_rev Logic.all vs (if defined then t3 else t2) end; + fun eq_assms ((p, T), cons) = + mk_trp (p $ HOLCF_Library.mk_bottom T) :: map (con_assm true p) cons; + val assms = maps eq_assms (Ps ~~ newTs ~~ map #con_specs constr_infos); - fun one_eq ((p, cons), concl) = - mk_trp (%:p $ UU) ===> Logic.list_implies (map (one_con p) cons, concl); - - fun ind_term concf = Library.foldr one_eq - (mapn (fn n => fn x => (P_name n, x)) 1 conss, - mk_trp (foldr1 mk_conj (mapn concf 1 dnames))); val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews); fun quant_tac ctxt i = EVERY - (mapn (fn n => fn _ => res_inst_tac ctxt [(("x", 0), x_name n)] spec i) 1 dnames); + (map (fn name => res_inst_tac ctxt [(("x", 0), name)] spec i) x_names); - fun ind_prems_tac prems = EVERY - (maps (fn cons => - (resolve_tac prems 1 :: - maps (fn (_,args) => - resolve_tac prems 1 :: - map (K(atac 1)) (nonlazy args) @ - map (K(atac 1)) (filter is_rec args)) - cons)) - conss); - local - fun rec_to ns lazy_rec (n,cons) = forall (exists (fn arg => - is_rec arg andalso not (member (op =) ns (rec_of arg)) andalso - ((rec_of arg = n andalso not (lazy_rec orelse is_lazy arg)) orelse - rec_of arg <> n andalso rec_to (rec_of arg::ns) - (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg)))) - ) o snd) cons; - fun warn (n,cons) = - if rec_to [] false (n,cons) - then (warning ("domain "^List.nth(dnames,n)^" is empty!"); true) - else false; + (* FIXME: move this message to domain_take_proofs.ML *) + val is_finite = #is_finite take_info; + val _ = if is_finite + then message ("Proving finiteness rule for domain "^comp_dname^" ...") + else (); - in - val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs; - val is_emptys = map warn n__eqs; - val is_finite = #is_finite take_info; - val _ = if is_finite - then message ("Proving finiteness rule for domain "^comp_dname^" ...") - else (); - end; val _ = trace " Proving finite_ind..."; val finite_ind = let - fun concf n dn = %:(P_name n) $ (dc_take dn $ %:"n" `%(x_name n)); - val goal = ind_term concf; + val concls = + map (fn ((P, t), x) => P $ mk_capply (t $ n, x)) + (Ps ~~ take_consts ~~ xs); + val goal = mk_trp (foldr1 mk_conj concls); fun tacf {prems, context} = let + (* Prove stronger prems, without definedness side conditions *) + fun con_thm p (con, args) = + let + val subgoal = con_assm false p (con, args); + val rules = prems @ con_rews @ simp_thms; + val simplify = asm_simp_tac (HOL_basic_ss addsimps rules); + fun arg_tac (lazy, _) = + rtac (if lazy then allI else case_UU_allI) 1; + val tacs = + rewrite_goals_tac @{thms atomize_all atomize_imp} :: + map arg_tac args @ + [REPEAT (rtac impI 1), ALLGOALS simplify]; + in + Goal.prove context [] [] subgoal (K (EVERY tacs)) + end; + fun eq_thms (p, cons) = map (con_thm p) cons; + val conss = map #con_specs constr_infos; + val prems' = maps eq_thms (Ps ~~ conss); + val tacs1 = [ quant_tac context 1, simp_tac HOL_ss 1, InductTacs.induct_tac context [[SOME "n"]] 1, simp_tac (take_ss addsimps prems) 1, TRY (safe_tac HOL_cs)]; - fun arg_tac arg = - (* FIXME! case_UU_tac *) - case_UU_tac context (prems @ con_rews) 1 - (List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg); - fun con_tacs (con, args) = - asm_simp_tac take_ss 1 :: - map arg_tac (filter is_nonlazy_rec args) @ - [resolve_tac prems 1] @ - map (K (atac 1)) (nonlazy args) @ - map (K (etac spec 1)) (filter is_rec args); + fun con_tac _ = + asm_simp_tac take_ss 1 THEN + (resolve_tac prems' THEN_ALL_NEW etac spec) 1; fun cases_tacs (cons, exhaust) = res_inst_tac context [(("y", 0), "x")] exhaust 1 :: asm_simp_tac (take_ss addsimps prems) 1 :: - maps con_tacs cons; + map con_tac cons; + val tacs = tacs1 @ maps cases_tacs (conss ~~ exhausts) in - tacs1 @ maps cases_tacs (conss ~~ exhausts) + EVERY (map DETERM tacs) end; - in pg'' thy [] goal tacf end; - -(* ----- theorems concerning finiteness and induction ----------------------- *) - - val global_ctxt = ProofContext.init_global thy; + in Goal.prove_global thy [] assms goal tacf end; val _ = trace " Proving ind..."; val ind = - if is_finite - then (* finite case *) - let - fun concf n dn = %:(P_name n) $ %:(x_name n); - fun tacf {prems, context} = - let - fun finite_tacs (take_induct, fin_ind) = [ - rtac take_induct 1, - rtac fin_ind 1, - ind_prems_tac prems]; - in - TRY (safe_tac HOL_cs) :: - maps finite_tacs (take_induct_thms ~~ atomize global_ctxt finite_ind) - end; - in pg'' thy [] (ind_term concf) tacf end + let + val concls = map (op $) (Ps ~~ xs); + val goal = mk_trp (foldr1 mk_conj concls); + val adms = if is_finite then [] else map (mk_trp o mk_adm) Ps; + fun tacf {prems, context} = + let + fun finite_tac (take_induct, fin_ind) = + rtac take_induct 1 THEN + (if is_finite then all_tac else resolve_tac prems 1) THEN + (rtac fin_ind THEN_ALL_NEW solve_tac prems) 1; + val fin_inds = Project_Rule.projections context finite_ind; + in + TRY (safe_tac HOL_cs) THEN + EVERY (map finite_tac (take_induct_thms ~~ fin_inds)) + end; + in Goal.prove_global thy [] (adms @ assms) goal tacf end - else (* infinite case *) - let - val goal = - let - fun one_adm n _ = mk_trp (mk_adm (%:(P_name n))); - fun concf n dn = %:(P_name n) $ %:(x_name n); - in Logic.list_implies (mapn one_adm 1 dnames, ind_term concf) end; - val cont_rules = - @{thms cont_id cont_const cont2cont_Rep_CFun - cont2cont_fst cont2cont_snd}; - val subgoal = - let - val Ts = map (Type o fst) eqs; - val P_names = Datatype_Prop.indexify_names (map (K "P") dnames); - val x_names = Datatype_Prop.indexify_names (map (K "x") dnames); - val P_types = map (fn T => T --> HOLogic.boolT) Ts; - val Ps = map Free (P_names ~~ P_types); - val xs = map Free (x_names ~~ Ts); - val n = Free ("n", HOLogic.natT); - val goals = - map (fn ((P,t),x) => P $ HOLCF_Library.mk_capply (t $ n, x)) - (Ps ~~ take_consts ~~ xs); - in - HOLogic.mk_Trueprop - (HOLogic.mk_all ("n", HOLogic.natT, foldr1 HOLogic.mk_conj goals)) - end; - fun tacf {prems, context} = - let - val subtac = - EVERY [rtac allI 1, rtac finite_ind 1, ind_prems_tac prems]; - val subthm = Goal.prove context [] [] subgoal (K subtac); - in - map (fn ax_reach => rtac (ax_reach RS subst) 1) reach_thms @ [ - cut_facts_tac (subthm :: take (length dnames) prems) 1, - REPEAT (rtac @{thm conjI} 1 ORELSE - EVERY [etac @{thm admD [OF _ ch2ch_Rep_CFunL]} 1, - resolve_tac chain_take_thms 1, - asm_simp_tac HOL_basic_ss 1]) - ] - end; - in pg'' thy [] goal tacf end; + (* case names for induction rules *) + val dnames = map (fst o dest_Type) newTs; + val case_ns = + let + val adms = + if is_finite then [] else + if length dnames = 1 then ["adm"] else + map (fn s => "adm_" ^ Long_Name.base_name s) dnames; + val bottoms = + if length dnames = 1 then ["bottom"] else + map (fn s => "bottom_" ^ Long_Name.base_name s) dnames; + fun one_eq bot constr_info = + let fun name_of (c, args) = Long_Name.base_name (fst (dest_Const c)); + in bot :: map name_of (#con_specs constr_info) end; + in adms @ flat (map2 one_eq bottoms constr_infos) end; -val case_ns = - let - val adms = - if is_finite then [] else - if length dnames = 1 then ["adm"] else - map (fn s => "adm_" ^ Long_Name.base_name s) dnames; - val bottoms = - if length dnames = 1 then ["bottom"] else - map (fn s => "bottom_" ^ Long_Name.base_name s) dnames; - fun one_eq bot (_,cons) = - bot :: map (fn (c,_) => Long_Name.base_name c) cons; - in adms @ flat (map2 one_eq bottoms eqs) end; - -val inducts = Project_Rule.projections (ProofContext.init_global thy) ind; -fun ind_rule (dname, rule) = - ((Binding.empty, [rule]), - [Rule_Cases.case_names case_ns, Induct.induct_type dname]); + val inducts = Project_Rule.projections (ProofContext.init_global thy) ind; + fun ind_rule (dname, rule) = + ((Binding.empty, rule), + [Rule_Cases.case_names case_ns, Induct.induct_type dname]); in thy - |> snd o Global_Theory.add_thmss [ - ((Binding.qualified true "finite_induct" comp_dbind, [finite_ind]), []), - ((Binding.qualified true "induct" comp_dbind, [ind] ), [])] - |> (snd o Global_Theory.add_thmss (map ind_rule (dnames ~~ inducts))) + |> snd o Global_Theory.add_thms [ + ((Binding.qualified true "finite_induct" comp_dbind, finite_ind), []), + ((Binding.qualified true "induct" comp_dbind, ind ), [])] + |> (snd o Global_Theory.add_thms (map ind_rule (dnames ~~ inducts))) end; (* prove_induction *) (******************************************************************************) @@ -432,166 +296,171 @@ (******************************************************************************) fun prove_coinduction - (comp_dbind : binding, eqs : eq list) - (take_lemmas : thm list) + (comp_dbind : binding, dbinds : binding list) + (constr_infos : Domain_Constructors.constr_info list) + (take_info : Domain_Take_Proofs.take_induct_info) + (take_rews : thm list list) (thy : theory) : theory = let + val iso_infos = map #iso_info constr_infos; + val newTs = map #absT iso_infos; -val dnames = map (fst o fst) eqs; -val comp_dname = Sign.full_name thy comp_dbind; -fun dc_take dn = %%:(dn^"_take"); -val x_name = idx_name dnames "x"; -val n_eqs = length eqs; - -val take_rews = - maps (fn dn => Global_Theory.get_thms thy (dn ^ ".take_rews")) dnames; + val {take_consts, take_0_thms, take_lemma_thms, ...} = take_info; -(* ----- define bisimulation predicate -------------------------------------- *) + val R_names = Datatype_Prop.indexify_names (map (K "R") newTs); + val R_types = map (fn T => T --> T --> boolT) newTs; + val Rs = map Free (R_names ~~ R_types); + val n = Free ("n", natT); + val reserved = "x" :: "y" :: R_names; -local - open HOLCF_Library - val dtypes = map (Type o fst) eqs; - val relprod = mk_tupleT (map (fn tp => tp --> tp --> boolT) dtypes); + (* declare bisimulation predicate *) val bisim_bind = Binding.suffix_name "_bisim" comp_dbind; - val bisim_type = relprod --> boolT; -in + val bisim_type = R_types ---> boolT; val (bisim_const, thy) = Sign.declare_const ((bisim_bind, bisim_type), NoSyn) thy; -end; - -local - fun legacy_infer_term thy t = - singleton (Syntax.check_terms (ProofContext.init_global thy)) (intern_term thy t); - fun legacy_infer_prop thy t = legacy_infer_term thy (Type.constraint propT t); - fun infer_props thy = map (apsnd (legacy_infer_prop thy)); - fun add_defs_i x = Global_Theory.add_defs false (map Thm.no_attributes x); - fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy; + (* define bisimulation predicate *) + local + fun one_con T (con, args) = + let + val Ts = map snd args; + val ns1 = Name.variant_list reserved (Datatype_Prop.make_tnames Ts); + val ns2 = map (fn n => n^"'") ns1; + val vs1 = map Free (ns1 ~~ Ts); + val vs2 = map Free (ns2 ~~ Ts); + val eq1 = mk_eq (Free ("x", T), list_ccomb (con, vs1)); + val eq2 = mk_eq (Free ("y", T), list_ccomb (con, vs2)); + fun rel ((v1, v2), T) = + case AList.lookup (op =) (newTs ~~ Rs) T of + NONE => mk_eq (v1, v2) | SOME r => r $ v1 $ v2; + val eqs = foldr1 mk_conj (map rel (vs1 ~~ vs2 ~~ Ts) @ [eq1, eq2]); + in + Library.foldr mk_ex (vs1 @ vs2, eqs) + end; + fun one_eq ((T, R), cons) = + let + val x = Free ("x", T); + val y = Free ("y", T); + val disj1 = mk_conj (mk_eq (x, mk_bottom T), mk_eq (y, mk_bottom T)); + val disjs = disj1 :: map (one_con T) cons; + in + mk_all (x, mk_all (y, mk_imp (R $ x $ y, foldr1 mk_disj disjs))) + end; + val conjs = map one_eq (newTs ~~ Rs ~~ map #con_specs constr_infos); + val bisim_rhs = lambdas Rs (Library.foldr1 mk_conj conjs); + val bisim_eqn = Logic.mk_equals (bisim_const, bisim_rhs); + in + val (bisim_def_thm, thy) = thy |> + yield_singleton (Global_Theory.add_defs false) + ((Binding.qualified true "bisim_def" comp_dbind, bisim_eqn), []); + end (* local *) - fun one_con (con, args) = + (* prove coinduction lemma *) + val coind_lemma = let - val nonrec_args = filter_out is_rec args; - val rec_args = filter is_rec args; - val recs_cnt = length rec_args; - val allargs = nonrec_args @ rec_args - @ map (upd_vname (fn s=> s^"'")) rec_args; - val allvns = map vname allargs; - fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg; - val vns1 = map (vname_arg "" ) args; - val vns2 = map (vname_arg "'") args; - val allargs_cnt = length nonrec_args + 2*recs_cnt; - val rec_idxs = (recs_cnt-1) downto 0; - val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg) - (allargs~~((allargs_cnt-1) downto 0))); - fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $ - Bound (2*recs_cnt-i) $ Bound (recs_cnt-i); - val capps = - List.foldr - mk_conj - (mk_conj( - Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1), - Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2))) - (mapn rel_app 1 rec_args); + val assm = mk_trp (list_comb (bisim_const, Rs)); + fun one ((T, R), take_const) = + let + val x = Free ("x", T); + val y = Free ("y", T); + val lhs = mk_capply (take_const $ n, x); + val rhs = mk_capply (take_const $ n, y); + in + mk_all (x, mk_all (y, mk_imp (R $ x $ y, mk_eq (lhs, rhs)))) + end; + val goal = + mk_trp (foldr1 mk_conj (map one (newTs ~~ Rs ~~ take_consts))); + val rules = @{thm Rep_CFun_strict1} :: take_0_thms; + fun tacf {prems, context} = + let + val prem' = rewrite_rule [bisim_def_thm] (hd prems); + val prems' = Project_Rule.projections context prem'; + val dests = map (fn th => th RS spec RS spec RS mp) prems'; + fun one_tac (dest, rews) = + dtac dest 1 THEN safe_tac HOL_cs THEN + ALLGOALS (asm_simp_tac (HOL_basic_ss addsimps rews)); + in + rtac @{thm nat.induct} 1 THEN + simp_tac (HOL_ss addsimps rules) 1 THEN + safe_tac HOL_cs THEN + EVERY (map one_tac (dests ~~ take_rews)) + end in - List.foldr - mk_ex - (Library.foldr mk_conj - (map (defined o Bound) nonlazy_idxs,capps)) allvns + Goal.prove_global thy [] [assm] goal tacf end; - fun one_comp n (_,cons) = - mk_all (x_name(n+1), - mk_all (x_name(n+1)^"'", - mk_imp (proj (Bound 2) eqs n $ Bound 1 $ Bound 0, - foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU) - ::map one_con cons)))); - val bisim_eqn = - %%:(comp_dname^"_bisim") == - mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs)); + + (* prove individual coinduction rules *) + fun prove_coind ((T, R), take_lemma) = + let + val x = Free ("x", T); + val y = Free ("y", T); + val assm1 = mk_trp (list_comb (bisim_const, Rs)); + val assm2 = mk_trp (R $ x $ y); + val goal = mk_trp (mk_eq (x, y)); + fun tacf {prems, context} = + let + val rule = hd prems RS coind_lemma; + in + rtac take_lemma 1 THEN + asm_simp_tac (HOL_basic_ss addsimps (rule :: prems)) 1 + end; + in + Goal.prove_global thy [] [assm1, assm2] goal tacf + end; + val coinds = map prove_coind (newTs ~~ Rs ~~ take_lemma_thms); + val coind_binds = map (Binding.qualified true "coinduct") dbinds; in - val (ax_bisim_def, thy) = - yield_singleton add_defs_infer - (Binding.qualified true "bisim_def" comp_dbind, bisim_eqn) thy; -end; (* local *) - -(* ----- theorem concerning coinduction ------------------------------------- *) - -local - val pg = pg' thy; - val xs = mapn (fn n => K (x_name n)) 1 dnames; - fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1); - val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews); - val sproj = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")")); - val _ = trace " Proving coind_lemma..."; - val coind_lemma = - let - fun mk_prj n _ = proj (%:"R") eqs n $ bnd_arg n 0 $ bnd_arg n 1; - fun mk_eqn n dn = - (dc_take dn $ %:"n" ` bnd_arg n 0) === - (dc_take dn $ %:"n" ` bnd_arg n 1); - fun mk_all2 (x,t) = mk_all (x, mk_all (x^"'", t)); - val goal = - mk_trp (mk_imp (%%:(comp_dname^"_bisim") $ %:"R", - Library.foldr mk_all2 (xs, - Library.foldr mk_imp (mapn mk_prj 0 dnames, - foldr1 mk_conj (mapn mk_eqn 0 dnames))))); - fun x_tacs ctxt n x = [ - rotate_tac (n+1) 1, - etac all2E 1, - eres_inst_tac ctxt [(("P", 1), sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1, - TRY (safe_tac HOL_cs), - REPEAT (CHANGED (asm_simp_tac take_ss 1))]; - fun tacs ctxt = [ - rtac impI 1, - InductTacs.induct_tac ctxt [[SOME "n"]] 1, - simp_tac take_ss 1, - safe_tac HOL_cs] @ - flat (mapn (x_tacs ctxt) 0 xs); - in pg [ax_bisim_def] goal tacs end; -in - val _ = trace " Proving coind..."; - val coind = - let - fun mk_prj n x = mk_trp (proj (%:"R") eqs n $ %:x $ %:(x^"'")); - fun mk_eqn x = %:x === %:(x^"'"); - val goal = - mk_trp (%%:(comp_dname^"_bisim") $ %:"R") ===> - Logic.list_implies (mapn mk_prj 0 xs, - mk_trp (foldr1 mk_conj (map mk_eqn xs))); - val tacs = - TRY (safe_tac HOL_cs) :: - maps (fn take_lemma => [ - rtac take_lemma 1, - cut_facts_tac [coind_lemma] 1, - fast_tac HOL_cs 1]) - take_lemmas; - in pg [] goal (K tacs) end; -end; (* local *) - -in thy |> snd o Global_Theory.add_thmss - [((Binding.qualified true "coinduct" comp_dbind, [coind]), [])] + thy |> snd o Global_Theory.add_thms + (map Thm.no_attributes (coind_binds ~~ coinds)) end; (* let *) +(******************************************************************************) +(******************************* main function ********************************) +(******************************************************************************) + fun comp_theorems - (comp_dbind : binding, eqs : eq list) + (comp_dbind : binding) + (dbinds : binding list) (take_info : Domain_Take_Proofs.take_induct_info) + (constr_infos : Domain_Constructors.constr_info list) (thy : theory) = let -val map_tab = Domain_Take_Proofs.get_map_tab thy; +val comp_dname = Binding.name_of comp_dbind; -val dnames = map (fst o fst) eqs; -val comp_dname = Sign.full_name thy comp_dbind; - -(* ----- getting the composite axiom and definitions ------------------------ *) +(* Test for emptiness *) +(* FIXME: reimplement emptiness test +local + open Domain_Library; + val dnames = map (fst o fst) eqs; + val conss = map snd eqs; + fun rec_to ns lazy_rec (n,cons) = forall (exists (fn arg => + is_rec arg andalso not (member (op =) ns (rec_of arg)) andalso + ((rec_of arg = n andalso not (lazy_rec orelse is_lazy arg)) orelse + rec_of arg <> n andalso rec_to (rec_of arg::ns) + (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg)))) + ) o snd) cons; + fun warn (n,cons) = + if rec_to [] false (n,cons) + then (warning ("domain "^List.nth(dnames,n)^" is empty!"); true) + else false; +in + val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs; + val is_emptys = map warn n__eqs; +end; +*) (* Test for indirect recursion *) local - fun indirect_arg arg = - rec_of arg = ~1 andalso Datatype_Aux.is_rec_type (dtyp_of arg); + val newTs = map (#absT o #iso_info) constr_infos; + fun indirect_typ (Type (_, Ts)) = + exists (fn T => member (op =) newTs T orelse indirect_typ T) Ts + | indirect_typ _ = false; + fun indirect_arg (_, T) = indirect_typ T; fun indirect_con (_, args) = exists indirect_arg args; - fun indirect_eq (_, cons) = exists indirect_con cons; + fun indirect_eq cons = exists indirect_con cons; in - val is_indirect = exists indirect_eq eqs; + val is_indirect = exists indirect_eq (map #con_specs constr_infos); val _ = if is_indirect then message "Indirect recursion detected, skipping proofs of (co)induction rules" @@ -600,19 +469,21 @@ (* theorems about take *) -val take_lemmas = #take_lemma_thms take_info; +val (take_rewss, thy) = + take_theorems dbinds take_info constr_infos thy; -val take_rews = - maps (fn dn => Global_Theory.get_thms thy (dn ^ ".take_rews")) dnames; +val {take_lemma_thms, take_0_thms, take_strict_thms, ...} = take_info; + +val take_rews = take_0_thms @ take_strict_thms @ flat take_rewss; (* prove induction rules, unless definition is indirect recursive *) val thy = if is_indirect then thy else - prove_induction (comp_dbind, eqs) take_rews take_info thy; + prove_induction comp_dbind constr_infos take_info take_rews thy; val thy = if is_indirect then thy else - prove_coinduction (comp_dbind, eqs) take_lemmas thy; + prove_coinduction (comp_dbind, dbinds) constr_infos take_info take_rewss thy; in (take_rews, thy) diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/Tools/holcf_library.ML --- a/src/HOLCF/Tools/holcf_library.ML Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/Tools/holcf_library.ML Sat Oct 16 16:39:06 2010 -0700 @@ -24,8 +24,10 @@ val mk_not = HOLogic.mk_not; val mk_conj = HOLogic.mk_conj; val mk_disj = HOLogic.mk_disj; +val mk_imp = HOLogic.mk_imp; fun mk_ex (x, t) = HOLogic.exists_const (fastype_of x) $ Term.lambda x t; +fun mk_all (x, t) = HOLogic.all_const (fastype_of x) $ Term.lambda x t; (*** Basic HOLCF concepts ***) @@ -39,6 +41,9 @@ fun mk_defined t = mk_not (mk_undef t); +fun mk_adm t = + Const (@{const_name adm}, fastype_of t --> boolT) $ t; + fun mk_compact t = Const (@{const_name compact}, fastype_of t --> boolT) $ t; diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/Universal.thy --- a/src/HOLCF/Universal.thy Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/Universal.thy Sat Oct 16 16:39:06 2010 -0700 @@ -988,7 +988,7 @@ done lemma lub_udom_approx [simp]: "(\i. udom_approx i) = ID" -apply (rule ext_cfun, simp add: contlub_cfun_fun) +apply (rule cfun_eqI, simp add: contlub_cfun_fun) apply (rule below_antisym) apply (rule is_lub_thelub) apply (simp) diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/Up.thy --- a/src/HOLCF/Up.thy Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/Up.thy Sat Oct 16 16:39:06 2010 -0700 @@ -303,7 +303,7 @@ unfolding u_map_def by simp lemma u_map_ID: "u_map\ID = ID" -unfolding u_map_def by (simp add: expand_cfun_eq eta_cfun) +unfolding u_map_def by (simp add: cfun_eq_iff eta_cfun) lemma u_map_map: "u_map\f\(u_map\g\p) = u_map\(\ x. f\(g\x))\p" by (induct p) simp_all diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/UpperPD.thy --- a/src/HOLCF/UpperPD.thy Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/UpperPD.thy Sat Oct 16 16:39:06 2010 -0700 @@ -318,7 +318,7 @@ lemma upper_bind_basis_mono: "t \\ u \ upper_bind_basis t \ upper_bind_basis u" -unfolding expand_cfun_below +unfolding cfun_below_iff apply (erule upper_le_induct, safe) apply (simp add: monofun_cfun) apply (simp add: below_trans [OF upper_plus_below1]) @@ -366,7 +366,7 @@ by (induct xs rule: upper_pd_induct, simp_all) lemma upper_map_ID: "upper_map\ID = ID" -by (simp add: expand_cfun_eq ID_def upper_map_ident) +by (simp add: cfun_eq_iff ID_def upper_map_ident) lemma upper_map_map: "upper_map\f\(upper_map\g\xs) = upper_map\(\ x. f\(g\x))\xs" @@ -478,7 +478,7 @@ next show "cast\DEFL('a upper_pd) = emb oo (prj :: udom \ 'a upper_pd)" unfolding emb_upper_pd_def prj_upper_pd_def defl_upper_pd_def cast_upper_defl - by (simp add: cast_DEFL oo_def expand_cfun_eq upper_map_map) + by (simp add: cast_DEFL oo_def cfun_eq_iff upper_map_map) qed end diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/ex/Fix2.thy --- a/src/HOLCF/ex/Fix2.thy Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/ex/Fix2.thy Sat Oct 16 16:39:06 2010 -0700 @@ -16,7 +16,7 @@ lemma lemma1: "fix = gix" -apply (rule ext_cfun) +apply (rule cfun_eqI) apply (rule antisym_less) apply (rule fix_least) apply (rule gix1_def) diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/ex/Focus_ex.thy --- a/src/HOLCF/ex/Focus_ex.thy Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/ex/Focus_ex.thy Sat Oct 16 16:39:06 2010 -0700 @@ -211,7 +211,7 @@ apply (rule_tac x = "f" in exI) apply (erule conjE)+ apply (erule conjI) -apply (rule ext_cfun) +apply (rule cfun_eqI) apply (erule_tac x = "x" in allE) apply (erule exE) apply (erule conjE)+ diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/ex/Hoare.thy --- a/src/HOLCF/ex/Hoare.thy Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/ex/Hoare.thy Sat Oct 16 16:39:06 2010 -0700 @@ -417,7 +417,7 @@ (* ------ the main proof q o p = q ------ *) theorem hoare_main: "q oo p = q" -apply (rule ext_cfun) +apply (rule cfun_eqI) apply (subst cfcomp2) apply (rule hoare_lemma3 [THEN disjE]) apply (erule hoare_lemma23) diff -r b253319c9a95 -r 98f2d8280eb4 src/HOLCF/ex/Pattern_Match.thy --- a/src/HOLCF/ex/Pattern_Match.thy Fri Oct 15 17:21:37 2010 +0100 +++ b/src/HOLCF/ex/Pattern_Match.thy Sat Oct 16 16:39:06 2010 -0700 @@ -359,6 +359,9 @@ ML {* local open HOLCF_Library in +infixr 6 ->>; +infix 9 ` ; + val beta_rules = @{thms beta_cfun cont_id cont_const cont2cont_Rep_CFun cont2cont_LAM'} @ @{thms cont2cont_fst cont2cont_snd cont2cont_Pair};