484 lemma (in ACe) left_ident [simp]: "e \<cdot> x = x" |
484 lemma (in ACe) left_ident [simp]: "e \<cdot> x = x" |
485 proof - |
485 proof - |
486 have "x \<cdot> e = x" by (rule ident) |
486 have "x \<cdot> e = x" by (rule ident) |
487 thus ?thesis by (subst commute) |
487 thus ?thesis by (subst commute) |
488 qed |
488 qed |
|
489 |
|
490 lemma (in ACIf) idem2: "x \<cdot> (x \<cdot> y) = x \<cdot> y" |
|
491 proof - |
|
492 have "x \<cdot> (x \<cdot> y) = (x \<cdot> x) \<cdot> y" by(simp add:assoc) |
|
493 also have "\<dots> = x \<cdot> y" by(simp add:idem) |
|
494 finally show ?thesis . |
|
495 qed |
|
496 |
|
497 lemmas (in ACIf) ACI = AC idem idem2 |
489 |
498 |
490 text{* Instantiation of locales: *} |
499 text{* Instantiation of locales: *} |
491 |
500 |
492 lemma ACf_add: "ACf (op + :: 'a::comm_monoid_add \<Rightarrow> 'a \<Rightarrow> 'a)" |
501 lemma ACf_add: "ACf (op + :: 'a::comm_monoid_add \<Rightarrow> 'a \<Rightarrow> 'a)" |
493 by(fastsimp intro: ACf.intro add_assoc add_commute) |
502 by(fastsimp intro: ACf.intro add_assoc add_commute) |
1911 lemma (in ACIf) fold1_insert2_def: |
1920 lemma (in ACIf) fold1_insert2_def: |
1912 "\<lbrakk> g \<equiv> fold1 f; finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (g A)" |
1921 "\<lbrakk> g \<equiv> fold1 f; finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (g A)" |
1913 by(simp add:fold1_insert2) |
1922 by(simp add:fold1_insert2) |
1914 |
1923 |
1915 |
1924 |
|
1925 subsubsection{* Semi-Lattices *} |
|
1926 |
|
1927 locale ACIfSL = ACIf + |
|
1928 fixes below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<preceq>" 50) |
|
1929 assumes below_def: "x \<preceq> y = (x\<cdot>y = x)" |
|
1930 |
|
1931 locale ACIfSLlin = ACIfSL + |
|
1932 assumes lin: "x\<cdot>y \<in> {x,y}" |
|
1933 |
|
1934 lemma (in ACIfSL) below_refl[simp]: "x \<preceq> x" |
|
1935 by(simp add: below_def idem) |
|
1936 |
|
1937 lemma (in ACIfSL) below_f_conv[simp]: "x \<preceq> y \<cdot> z = (x \<preceq> y \<and> x \<preceq> z)" |
|
1938 proof |
|
1939 assume "x \<preceq> y \<cdot> z" |
|
1940 hence xyzx: "x \<cdot> (y \<cdot> z) = x" by(simp add: below_def) |
|
1941 have "x \<cdot> y = x" |
|
1942 proof - |
|
1943 have "x \<cdot> y = (x \<cdot> (y \<cdot> z)) \<cdot> y" by(rule subst[OF xyzx], rule refl) |
|
1944 also have "\<dots> = x \<cdot> (y \<cdot> z)" by(simp add:ACI) |
|
1945 also have "\<dots> = x" by(rule xyzx) |
|
1946 finally show ?thesis . |
|
1947 qed |
|
1948 moreover have "x \<cdot> z = x" |
|
1949 proof - |
|
1950 have "x \<cdot> z = (x \<cdot> (y \<cdot> z)) \<cdot> z" by(rule subst[OF xyzx], rule refl) |
|
1951 also have "\<dots> = x \<cdot> (y \<cdot> z)" by(simp add:ACI) |
|
1952 also have "\<dots> = x" by(rule xyzx) |
|
1953 finally show ?thesis . |
|
1954 qed |
|
1955 ultimately show "x \<preceq> y \<and> x \<preceq> z" by(simp add: below_def) |
|
1956 next |
|
1957 assume a: "x \<preceq> y \<and> x \<preceq> z" |
|
1958 hence y: "x \<cdot> y = x" and z: "x \<cdot> z = x" by(simp_all add: below_def) |
|
1959 have "x \<cdot> (y \<cdot> z) = (x \<cdot> y) \<cdot> z" by(simp add:assoc) |
|
1960 also have "x \<cdot> y = x" using a by(simp_all add: below_def) |
|
1961 also have "x \<cdot> z = x" using a by(simp_all add: below_def) |
|
1962 finally show "x \<preceq> y \<cdot> z" by(simp_all add: below_def) |
|
1963 qed |
|
1964 |
|
1965 lemma (in ACIfSLlin) above_f_conv: |
|
1966 "x \<cdot> y \<preceq> z = (x \<preceq> z \<or> y \<preceq> z)" |
|
1967 proof |
|
1968 assume a: "x \<cdot> y \<preceq> z" |
|
1969 have "x \<cdot> y = x \<or> x \<cdot> y = y" using lin[of x y] by simp |
|
1970 thus "x \<preceq> z \<or> y \<preceq> z" |
|
1971 proof |
|
1972 assume "x \<cdot> y = x" hence "x \<preceq> z" by(rule subst)(rule a) thus ?thesis .. |
|
1973 next |
|
1974 assume "x \<cdot> y = y" hence "y \<preceq> z" by(rule subst)(rule a) thus ?thesis .. |
|
1975 qed |
|
1976 next |
|
1977 assume "x \<preceq> z \<or> y \<preceq> z" |
|
1978 thus "x \<cdot> y \<preceq> z" |
|
1979 proof |
|
1980 assume a: "x \<preceq> z" |
|
1981 have "(x \<cdot> y) \<cdot> z = (x \<cdot> z) \<cdot> y" by(simp add:ACI) |
|
1982 also have "x \<cdot> z = x" using a by(simp add:below_def) |
|
1983 finally show "x \<cdot> y \<preceq> z" by(simp add:below_def) |
|
1984 next |
|
1985 assume a: "y \<preceq> z" |
|
1986 have "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)" by(simp add:ACI) |
|
1987 also have "y \<cdot> z = y" using a by(simp add:below_def) |
|
1988 finally show "x \<cdot> y \<preceq> z" by(simp add:below_def) |
|
1989 qed |
|
1990 qed |
|
1991 |
|
1992 |
1916 subsubsection{* Lemmas about {@text fold1} *} |
1993 subsubsection{* Lemmas about {@text fold1} *} |
1917 |
1994 |
1918 lemma (in ACf) fold1_Un: |
1995 lemma (in ACf) fold1_Un: |
1919 assumes A: "finite A" "A \<noteq> {}" |
1996 assumes A: "finite A" "A \<noteq> {}" |
1920 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow> A Int B = {} \<Longrightarrow> |
1997 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow> A Int B = {} \<Longrightarrow> |
1945 case singleton thus ?case by(simp) |
2022 case singleton thus ?case by(simp) |
1946 next |
2023 next |
1947 case insert thus ?case using elem by (force simp add:fold1_insert) |
2024 case insert thus ?case using elem by (force simp add:fold1_insert) |
1948 qed |
2025 qed |
1949 |
2026 |
1950 lemma fold1_le: |
2027 lemma (in ACIfSL) below_fold1_iff: |
1951 assumes ACf: "ACf(f::'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)" |
2028 assumes A: "finite A" "A \<noteq> {}" |
1952 and A: "finite (A)" "A \<noteq> {}" and le: "\<And>x y. f x y \<le> x" |
2029 shows "x \<preceq> fold1 f A = (\<forall>a\<in>A. x \<preceq> a)" |
1953 shows "a \<in> A \<Longrightarrow> fold1 f A \<le> a" |
2030 using A |
|
2031 by(induct rule:finite_ne_induct) simp_all |
|
2032 |
|
2033 lemma (in ACIfSL) fold1_belowI: |
|
2034 assumes A: "finite A" "A \<noteq> {}" |
|
2035 shows "a \<in> A \<Longrightarrow> fold1 f A \<preceq> a" |
1954 using A |
2036 using A |
1955 proof (induct rule:finite_ne_induct) |
2037 proof (induct rule:finite_ne_induct) |
1956 case singleton thus ?case by(simp) |
2038 case singleton thus ?case by simp |
1957 next |
2039 next |
1958 from le have le2: "\<And>x y. f x y \<le> y" by (fastsimp simp:ACf.commute[OF ACf]) |
2040 case (insert x F) |
1959 case (insert x F) thus ?case using le le2 |
2041 from insert(4) have "a = x \<or> a \<in> F" by simp |
1960 by (simp add:ACf.fold1_insert[OF ACf]) (blast intro: le order_trans) |
2042 thus ?case |
1961 qed |
2043 proof |
1962 |
2044 assume "a = x" thus ?thesis using insert by(simp add:below_def ACI) |
1963 lemma fold1_ge: |
2045 next |
1964 assumes ACf: "ACf(f::'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)" |
2046 assume "a \<in> F" |
1965 and A: "finite (A)" "A \<noteq> {}" and ge: "\<And>x y. x \<le> f x y" |
2047 hence bel: "fold1 op \<cdot> F \<preceq> a" by(rule insert) |
1966 shows "a \<in> A \<Longrightarrow> a \<le> fold1 f A" |
2048 have "fold1 op \<cdot> (insert x F) \<cdot> a = x \<cdot> (fold1 op \<cdot> F \<cdot> a)" |
|
2049 using insert by(simp add:below_def ACI) |
|
2050 also have "fold1 op \<cdot> F \<cdot> a = fold1 op \<cdot> F" |
|
2051 using bel by(simp add:below_def ACI) |
|
2052 also have "x \<cdot> \<dots> = fold1 op \<cdot> (insert x F)" |
|
2053 using insert by(simp add:below_def ACI) |
|
2054 finally show ?thesis by(simp add:below_def) |
|
2055 qed |
|
2056 qed |
|
2057 |
|
2058 lemma (in ACIfSLlin) fold1_below_iff: |
|
2059 assumes A: "finite A" "A \<noteq> {}" |
|
2060 shows "fold1 f A \<preceq> x = (\<exists>a\<in>A. a \<preceq> x)" |
1967 using A |
2061 using A |
1968 proof (induct rule:finite_ne_induct) |
2062 by(induct rule:finite_ne_induct)(simp_all add:above_f_conv) |
1969 case singleton thus ?case by(simp) |
|
1970 next |
|
1971 from ge have ge2: "\<And>x y. y \<le> f x y" by (fastsimp simp:ACf.commute[OF ACf]) |
|
1972 case (insert x F) thus ?case using ge ge2 |
|
1973 by (simp add:ACf.fold1_insert[OF ACf]) (blast intro: ge order_trans) |
|
1974 qed |
|
1975 |
2063 |
1976 |
2064 |
1977 subsection{*Min and Max*} |
2065 subsection{*Min and Max*} |
1978 |
2066 |
1979 text{* As an application of @{text fold1} we define the minimal and |
2067 text{* As an application of @{text fold1} we define the minimal and |
1980 maximal element of a (non-empty) set over a linear order. First we |
2068 maximal element of a (non-empty) set over a linear order. *} |
1981 show that @{text min} and @{text max} are ACI: *} |
2069 |
|
2070 constdefs |
|
2071 Min :: "('a::linorder)set => 'a" |
|
2072 "Min == fold1 min" |
|
2073 |
|
2074 Max :: "('a::linorder)set => 'a" |
|
2075 "Max == fold1 max" |
|
2076 |
|
2077 |
|
2078 text{* Before we can do anything, we need to show that @{text min} and |
|
2079 @{text max} are ACI and the ordering is linear: *} |
1982 |
2080 |
1983 lemma ACf_min: "ACf(min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)" |
2081 lemma ACf_min: "ACf(min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)" |
1984 apply(rule ACf.intro) |
2082 apply(rule ACf.intro) |
1985 apply(auto simp:min_def) |
2083 apply(auto simp:min_def) |
1986 done |
2084 done |
2000 apply(rule ACIf.intro[OF ACf_max]) |
2098 apply(rule ACIf.intro[OF ACf_max]) |
2001 apply(rule ACIf_axioms.intro) |
2099 apply(rule ACIf_axioms.intro) |
2002 apply(auto simp:max_def) |
2100 apply(auto simp:max_def) |
2003 done |
2101 done |
2004 |
2102 |
2005 text{* Now we make the definitions: *} |
2103 lemma ACIfSL_min: "ACIfSL(min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) (op \<le>)" |
2006 |
2104 apply(rule ACIfSL.intro) |
2007 constdefs |
2105 apply(rule ACf_min) |
2008 Min :: "('a::linorder)set => 'a" |
2106 apply(rule ACIf.axioms[OF ACIf_min]) |
2009 "Min == fold1 min" |
2107 apply(rule ACIfSL_axioms.intro) |
2010 |
2108 apply(auto simp:min_def) |
2011 Max :: "('a::linorder)set => 'a" |
2109 done |
2012 "Max == fold1 max" |
2110 |
|
2111 lemma ACIfSLlin_min: "ACIfSLlin(min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) (op \<le>)" |
|
2112 apply(rule ACIfSLlin.intro) |
|
2113 apply(rule ACf_min) |
|
2114 apply(rule ACIf.axioms[OF ACIf_min]) |
|
2115 apply(rule ACIfSL.axioms[OF ACIfSL_min]) |
|
2116 apply(rule ACIfSLlin_axioms.intro) |
|
2117 apply(auto simp:min_def) |
|
2118 done |
|
2119 |
|
2120 lemma ACIfSL_max: "ACIfSL(max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) (%x y. y\<le>x)" |
|
2121 apply(rule ACIfSL.intro) |
|
2122 apply(rule ACf_max) |
|
2123 apply(rule ACIf.axioms[OF ACIf_max]) |
|
2124 apply(rule ACIfSL_axioms.intro) |
|
2125 apply(auto simp:max_def) |
|
2126 done |
|
2127 |
|
2128 lemma ACIfSLlin_max: "ACIfSLlin(max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) (%x y. y\<le>x)" |
|
2129 apply(rule ACIfSLlin.intro) |
|
2130 apply(rule ACf_max) |
|
2131 apply(rule ACIf.axioms[OF ACIf_max]) |
|
2132 apply(rule ACIfSL.axioms[OF ACIfSL_max]) |
|
2133 apply(rule ACIfSLlin_axioms.intro) |
|
2134 apply(auto simp:max_def) |
|
2135 done |
2013 |
2136 |
2014 text{* Now we instantiate the recursion equations and declare them |
2137 text{* Now we instantiate the recursion equations and declare them |
2015 simplification rules: *} |
2138 simplification rules: *} |
2016 |
2139 |
2017 declare |
2140 declare |
2031 shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Max A \<in> A" |
2154 shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Max A \<in> A" |
2032 using ACf.fold1_in[OF ACf_max] |
2155 using ACf.fold1_in[OF ACf_max] |
2033 by(fastsimp simp: Max_def max_def) |
2156 by(fastsimp simp: Max_def max_def) |
2034 |
2157 |
2035 lemma Min_le [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> Min A \<le> x" |
2158 lemma Min_le [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> Min A \<le> x" |
2036 by(simp add: Min_def fold1_le[OF ACf_min] min_le_iff_disj) |
2159 by(simp add: Min_def ACIfSL.fold1_belowI[OF ACIfSL_min]) |
2037 |
2160 |
2038 lemma Max_ge [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> x \<le> Max A" |
2161 lemma Max_ge [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> x \<le> Max A" |
2039 by(simp add: Max_def fold1_ge[OF ACf_max] le_max_iff_disj) |
2162 by(simp add: Max_def ACIfSL.fold1_belowI[OF ACIfSL_max]) |
|
2163 |
|
2164 lemma Min_ge_iff[simp]: |
|
2165 "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Min A) = (\<forall>a\<in>A. x \<le> a)" |
|
2166 by(simp add: Min_def ACIfSL.below_fold1_iff[OF ACIfSL_min]) |
|
2167 |
|
2168 lemma Max_le_iff[simp]: |
|
2169 "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Max A \<le> x) = (\<forall>a\<in>A. a \<le> x)" |
|
2170 by(simp add: Max_def ACIfSL.below_fold1_iff[OF ACIfSL_max]) |
|
2171 |
|
2172 lemma Min_le_iff: |
|
2173 "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Min A \<le> x) = (\<exists>a\<in>A. a \<le> x)" |
|
2174 by(simp add: Min_def ACIfSLlin.fold1_below_iff[OF ACIfSLlin_min]) |
|
2175 |
|
2176 lemma Max_ge_iff: |
|
2177 "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Max A) = (\<exists>a\<in>A. x \<le> a)" |
|
2178 by(simp add: Max_def ACIfSLlin.fold1_below_iff[OF ACIfSLlin_max]) |
2040 |
2179 |
2041 end |
2180 end |