# HG changeset patch # User huffman # Date 1289440568 28800 # Node ID 8e92772bc0e834667f3a59c4c983a03ef9ab4d4a # Parent 2ed71459136e85f1540d70d463a636c048b2d6e5 move map functions to new theory file Map_Functions; add theory file Plain_HOLCF diff -r 2ed71459136e -r 8e92772bc0e8 src/HOLCF/Algebraic.thy --- a/src/HOLCF/Algebraic.thy Wed Nov 10 14:59:52 2010 -0800 +++ b/src/HOLCF/Algebraic.thy Wed Nov 10 17:56:08 2010 -0800 @@ -5,7 +5,7 @@ header {* Algebraic deflations *} theory Algebraic -imports Universal +imports Universal Map_Functions begin subsection {* Type constructor for finite deflations *} diff -r 2ed71459136e -r 8e92772bc0e8 src/HOLCF/Bifinite.thy --- a/src/HOLCF/Bifinite.thy Wed Nov 10 14:59:52 2010 -0800 +++ b/src/HOLCF/Bifinite.thy Wed Nov 10 17:56:08 2010 -0800 @@ -5,7 +5,7 @@ header {* Bifinite domains *} theory Bifinite -imports Algebraic Cprod Sprod Ssum Up Lift One Tr Countable +imports Algebraic Map_Functions Countable begin subsection {* Class of bifinite domains *} diff -r 2ed71459136e -r 8e92772bc0e8 src/HOLCF/Cfun.thy --- a/src/HOLCF/Cfun.thy Wed Nov 10 14:59:52 2010 -0800 +++ b/src/HOLCF/Cfun.thy Wed Nov 10 17:56:08 2010 -0800 @@ -479,24 +479,6 @@ lemma assoc_oo: "f oo (g oo h) = (f oo g) oo h" by (rule cfun_eqI, simp) -subsection {* Map operator for continuous function space *} - -definition - cfun_map :: "('b \ 'a) \ ('c \ 'd) \ ('a \ 'c) \ ('b \ 'd)" -where - "cfun_map = (\ a b f x. b\(f\(a\x)))" - -lemma cfun_map_beta [simp]: "cfun_map\a\b\f\x = b\(f\(a\x))" -unfolding cfun_map_def by simp - -lemma cfun_map_ID: "cfun_map\ID\ID = ID" -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 cfun_eqI) simp - subsection {* Strictified functions *} default_sort pcpo diff -r 2ed71459136e -r 8e92772bc0e8 src/HOLCF/Completion.thy --- a/src/HOLCF/Completion.thy Wed Nov 10 14:59:52 2010 -0800 +++ b/src/HOLCF/Completion.thy Wed Nov 10 17:56:08 2010 -0800 @@ -5,7 +5,7 @@ header {* Defining algebraic domains by ideal completion *} theory Completion -imports Cfun +imports Plain_HOLCF begin subsection {* Ideals over a preorder *} diff -r 2ed71459136e -r 8e92772bc0e8 src/HOLCF/Cprod.thy --- a/src/HOLCF/Cprod.thy Wed Nov 10 14:59:52 2010 -0800 +++ b/src/HOLCF/Cprod.thy Wed Nov 10 17:56:08 2010 -0800 @@ -5,7 +5,7 @@ header {* The cpo of cartesian products *} theory Cprod -imports Deflation +imports Cfun begin default_sort cpo @@ -40,61 +40,4 @@ lemma csplit_Pair [simp]: "csplit\f\(x, y) = f\x\y" by (simp add: csplit_def) -subsection {* Map operator for product type *} - -definition - cprod_map :: "('a \ 'b) \ ('c \ 'd) \ 'a \ 'c \ 'b \ 'd" -where - "cprod_map = (\ f g p. (f\(fst p), g\(snd p)))" - -lemma cprod_map_Pair [simp]: "cprod_map\f\g\(x, y) = (f\x, g\y)" -unfolding cprod_map_def by simp - -lemma cprod_map_ID: "cprod_map\ID\ID = ID" -unfolding cfun_eq_iff by auto - -lemma cprod_map_map: - "cprod_map\f1\g1\(cprod_map\f2\g2\p) = - cprod_map\(\ x. f1\(f2\x))\(\ x. g1\(g2\x))\p" -by (induct p) simp - -lemma ep_pair_cprod_map: - assumes "ep_pair e1 p1" and "ep_pair e2 p2" - shows "ep_pair (cprod_map\e1\e2) (cprod_map\p1\p2)" -proof - interpret e1p1: ep_pair e1 p1 by fact - interpret e2p2: ep_pair e2 p2 by fact - fix x show "cprod_map\p1\p2\(cprod_map\e1\e2\x) = x" - by (induct x) simp - fix y show "cprod_map\e1\e2\(cprod_map\p1\p2\y) \ y" - by (induct y) (simp add: e1p1.e_p_below e2p2.e_p_below) -qed - -lemma deflation_cprod_map: - assumes "deflation d1" and "deflation d2" - shows "deflation (cprod_map\d1\d2)" -proof - interpret d1: deflation d1 by fact - interpret d2: deflation d2 by fact - fix x - show "cprod_map\d1\d2\(cprod_map\d1\d2\x) = cprod_map\d1\d2\x" - by (induct x) (simp add: d1.idem d2.idem) - show "cprod_map\d1\d2\x \ x" - by (induct x) (simp add: d1.below d2.below) -qed - -lemma finite_deflation_cprod_map: - assumes "finite_deflation d1" and "finite_deflation d2" - shows "finite_deflation (cprod_map\d1\d2)" -proof (rule finite_deflation_intro) - interpret d1: finite_deflation d1 by fact - interpret d2: finite_deflation d2 by fact - have "deflation d1" and "deflation d2" by fact+ - thus "deflation (cprod_map\d1\d2)" by (rule deflation_cprod_map) - have "{p. cprod_map\d1\d2\p = p} \ {x. d1\x = x} \ {y. d2\y = y}" - by clarsimp - thus "finite {p. cprod_map\d1\d2\p = p}" - by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes) -qed - end diff -r 2ed71459136e -r 8e92772bc0e8 src/HOLCF/Deflation.thy --- a/src/HOLCF/Deflation.thy Wed Nov 10 14:59:52 2010 -0800 +++ b/src/HOLCF/Deflation.thy Wed Nov 10 17:56:08 2010 -0800 @@ -5,7 +5,7 @@ header {* Continuous deflations and ep-pairs *} theory Deflation -imports Cfun +imports Plain_HOLCF begin default_sort cpo @@ -405,93 +405,4 @@ end -subsection {* Map operator for continuous functions *} - -lemma ep_pair_cfun_map: - assumes "ep_pair e1 p1" and "ep_pair e2 p2" - shows "ep_pair (cfun_map\p1\e2) (cfun_map\e1\p2)" -proof - 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: cfun_eq_iff) - fix g show "cfun_map\p1\e2\(cfun_map\e1\p2\g) \ g" - 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) - done -qed - -lemma deflation_cfun_map: - assumes "deflation d1" and "deflation d2" - shows "deflation (cfun_map\d1\d2)" -proof - interpret d1: deflation d1 by fact - 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: cfun_eq_iff d1.idem d2.idem) - show "cfun_map\d1\d2\f \ f" - apply (rule cfun_belowI, simp) - apply (rule below_trans [OF d2.below]) - apply (rule monofun_cfun_arg) - apply (rule d1.below) - done -qed - -lemma finite_range_cfun_map: - assumes a: "finite (range (\x. a\x))" - assumes b: "finite (range (\y. b\y))" - shows "finite (range (\f. cfun_map\a\b\f))" (is "finite (range ?h)") -proof (rule finite_imageD) - let ?f = "\g. range (\x. (a\x, g\x))" - show "finite (?f ` range ?h)" - proof (rule finite_subset) - let ?B = "Pow (range (\x. a\x) \ range (\y. b\y))" - show "?f ` range ?h \ ?B" - by clarsimp - show "finite ?B" - by (simp add: a b) - qed - show "inj_on ?f (range ?h)" - 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))))" - by (rule equalityD1) - hence "(a\x, b\(f\(a\x))) \ range (\x. (a\x, b\(g\(a\x))))" - by (simp add: subset_eq) - then obtain y where "(a\x, b\(f\(a\x))) = (a\y, b\(g\(a\y)))" - by (rule rangeE) - thus "b\(f\(a\x)) = b\(g\(a\x))" - by clarsimp - qed -qed - -lemma finite_deflation_cfun_map: - assumes "finite_deflation d1" and "finite_deflation d2" - shows "finite_deflation (cfun_map\d1\d2)" -proof (rule finite_deflation_intro) - interpret d1: finite_deflation d1 by fact - interpret d2: finite_deflation d2 by fact - have "deflation d1" and "deflation d2" by fact+ - thus "deflation (cfun_map\d1\d2)" by (rule deflation_cfun_map) - have "finite (range (\f. cfun_map\d1\d2\f))" - using d1.finite_range d2.finite_range - by (rule finite_range_cfun_map) - thus "finite {f. cfun_map\d1\d2\f = f}" - by (rule finite_range_imp_finite_fixes) -qed - -text {* Finite deflations are compact elements of the function space *} - -lemma finite_deflation_imp_compact: "finite_deflation d \ compact d" -apply (frule finite_deflation_imp_deflation) -apply (subgoal_tac "compact (cfun_map\d\d\d)") -apply (simp add: cfun_map_def deflation.idem eta_cfun) -apply (rule finite_deflation.compact) -apply (simp only: finite_deflation_cfun_map) -done - end diff -r 2ed71459136e -r 8e92772bc0e8 src/HOLCF/Domain_Aux.thy --- a/src/HOLCF/Domain_Aux.thy Wed Nov 10 14:59:52 2010 -0800 +++ b/src/HOLCF/Domain_Aux.thy Wed Nov 10 17:56:08 2010 -0800 @@ -5,7 +5,7 @@ header {* Domain package support *} theory Domain_Aux -imports Ssum Sprod Fixrec +imports Map_Functions Fixrec uses ("Tools/Domain/domain_take_proofs.ML") begin diff -r 2ed71459136e -r 8e92772bc0e8 src/HOLCF/Fixrec.thy --- a/src/HOLCF/Fixrec.thy Wed Nov 10 14:59:52 2010 -0800 +++ b/src/HOLCF/Fixrec.thy Wed Nov 10 17:56:08 2010 -0800 @@ -5,7 +5,7 @@ header "Package for defining recursive functions in HOLCF" theory Fixrec -imports Cprod Sprod Ssum Up One Tr Fix +imports Plain_HOLCF uses ("Tools/holcf_library.ML") ("Tools/fixrec.ML") diff -r 2ed71459136e -r 8e92772bc0e8 src/HOLCF/IsaMakefile --- a/src/HOLCF/IsaMakefile Wed Nov 10 14:59:52 2010 -0800 +++ b/src/HOLCF/IsaMakefile Wed Nov 10 17:56:08 2010 -0800 @@ -54,9 +54,11 @@ HOLCF.thy \ Lift.thy \ LowerPD.thy \ + Map_Functions.thy \ One.thy \ Pcpodef.thy \ Pcpo.thy \ + Plain_HOLCF.thy \ Porder.thy \ Powerdomains.thy \ Product_Cpo.thy \ diff -r 2ed71459136e -r 8e92772bc0e8 src/HOLCF/Map_Functions.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Map_Functions.thy Wed Nov 10 17:56:08 2010 -0800 @@ -0,0 +1,383 @@ +(* Title: HOLCF/Map_Functions.thy + Author: Brian Huffman +*) + +header {* Map functions for various types *} + +theory Map_Functions +imports Deflation +begin + +subsection {* Map operator for continuous function space *} + +default_sort cpo + +definition + cfun_map :: "('b \ 'a) \ ('c \ 'd) \ ('a \ 'c) \ ('b \ 'd)" +where + "cfun_map = (\ a b f x. b\(f\(a\x)))" + +lemma cfun_map_beta [simp]: "cfun_map\a\b\f\x = b\(f\(a\x))" +unfolding cfun_map_def by simp + +lemma cfun_map_ID: "cfun_map\ID\ID = ID" +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 cfun_eqI) simp + +lemma ep_pair_cfun_map: + assumes "ep_pair e1 p1" and "ep_pair e2 p2" + shows "ep_pair (cfun_map\p1\e2) (cfun_map\e1\p2)" +proof + 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: cfun_eq_iff) + fix g show "cfun_map\p1\e2\(cfun_map\e1\p2\g) \ g" + 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) + done +qed + +lemma deflation_cfun_map: + assumes "deflation d1" and "deflation d2" + shows "deflation (cfun_map\d1\d2)" +proof + interpret d1: deflation d1 by fact + 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: cfun_eq_iff d1.idem d2.idem) + show "cfun_map\d1\d2\f \ f" + apply (rule cfun_belowI, simp) + apply (rule below_trans [OF d2.below]) + apply (rule monofun_cfun_arg) + apply (rule d1.below) + done +qed + +lemma finite_range_cfun_map: + assumes a: "finite (range (\x. a\x))" + assumes b: "finite (range (\y. b\y))" + shows "finite (range (\f. cfun_map\a\b\f))" (is "finite (range ?h)") +proof (rule finite_imageD) + let ?f = "\g. range (\x. (a\x, g\x))" + show "finite (?f ` range ?h)" + proof (rule finite_subset) + let ?B = "Pow (range (\x. a\x) \ range (\y. b\y))" + show "?f ` range ?h \ ?B" + by clarsimp + show "finite ?B" + by (simp add: a b) + qed + show "inj_on ?f (range ?h)" + 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))))" + by (rule equalityD1) + hence "(a\x, b\(f\(a\x))) \ range (\x. (a\x, b\(g\(a\x))))" + by (simp add: subset_eq) + then obtain y where "(a\x, b\(f\(a\x))) = (a\y, b\(g\(a\y)))" + by (rule rangeE) + thus "b\(f\(a\x)) = b\(g\(a\x))" + by clarsimp + qed +qed + +lemma finite_deflation_cfun_map: + assumes "finite_deflation d1" and "finite_deflation d2" + shows "finite_deflation (cfun_map\d1\d2)" +proof (rule finite_deflation_intro) + interpret d1: finite_deflation d1 by fact + interpret d2: finite_deflation d2 by fact + have "deflation d1" and "deflation d2" by fact+ + thus "deflation (cfun_map\d1\d2)" by (rule deflation_cfun_map) + have "finite (range (\f. cfun_map\d1\d2\f))" + using d1.finite_range d2.finite_range + by (rule finite_range_cfun_map) + thus "finite {f. cfun_map\d1\d2\f = f}" + by (rule finite_range_imp_finite_fixes) +qed + +text {* Finite deflations are compact elements of the function space *} + +lemma finite_deflation_imp_compact: "finite_deflation d \ compact d" +apply (frule finite_deflation_imp_deflation) +apply (subgoal_tac "compact (cfun_map\d\d\d)") +apply (simp add: cfun_map_def deflation.idem eta_cfun) +apply (rule finite_deflation.compact) +apply (simp only: finite_deflation_cfun_map) +done + +subsection {* Map operator for product type *} + +definition + cprod_map :: "('a \ 'b) \ ('c \ 'd) \ 'a \ 'c \ 'b \ 'd" +where + "cprod_map = (\ f g p. (f\(fst p), g\(snd p)))" + +lemma cprod_map_Pair [simp]: "cprod_map\f\g\(x, y) = (f\x, g\y)" +unfolding cprod_map_def by simp + +lemma cprod_map_ID: "cprod_map\ID\ID = ID" +unfolding cfun_eq_iff by auto + +lemma cprod_map_map: + "cprod_map\f1\g1\(cprod_map\f2\g2\p) = + cprod_map\(\ x. f1\(f2\x))\(\