# Re: [isabelle] promble with "Min_Un theorem"

ÓÎÕä wrote:

Hi,
There is "Min_Un theorm" in isabelle. The concrete description is given as follow:
Finite_Set.linorder_class.Min_Un: \<lbrakk>finite ?A; ?A \<noteq> {}; finite ?B; ?B \<noteq> {}\<rbrakk> \<Longrightarrow> Min (?A \<union> ?B) = min (Min ?A) (Min ?B)

` When I proof a lemma, i think i need use "Min_Un theorem", but i don't succes ,though i try it for many times. the following are my theory:
``
``
``
`

`The first problem in your theory is, that your function declarations
``introduce simplification loops.
``You should explicitely erase the looping rules from the simpset, and
``replace them by safer ones.
`(See the isabelle tutorial on function definition for details).

`
``
``(*--------------(sum i j xs) 0\<le>i\<le>j\<le>n-------------*)
`function set_sum :: "nat \<Rightarrow> nat list \<Rightarrow> nat set"
where
"set_sum n xs = ( case n of 0 \<Rightarrow> {} | Suc(m) \<Rightarrow> (set_sum m xs)\<union>(set (list_sum 0 (Suc m) xs) ) )"
by pat_completeness auto
termination
by (relation "measure (\<lambda>(n,_). n )") auto
(*--------------min of set_sum-------------------*)

`
`

`Try this (equivalent) definition instead, it makes the case-distinction
``explicit using pattern matching. And thus introduces safe simplification
``rules.
`
(*--------------(sum i j xs) 0\<le>i\<le>j\<le>n-------------*)
fun set_sum :: "nat \<Rightarrow> nat list \<Rightarrow> nat set"
where
"set_sum 0 xs = {}" |
"set_sum (Suc m) xs = (set_sum m xs)\<union>(set (list_sum 0 (Suc m) xs))"

lemma recur1 : "i>0\<and>(size xs)>i \<Longrightarrow> (min (minsum i xs) (ms (Suc i) xs)) = (minsum (Suc i) xs)"

`
`

Now you could go with:
apply (unfold minsum.simps )
apply (unfold ms.simps)

`apply (simp del: sum.simps list_sum.simps) -- (Or do a declare
``sum.simps[simp_del] and declare list_sum.simps[simp del] after the def.
``of those functions.)
`apply (rule Min_Un[symmetric])
apply simp_all

`However, this leaves one subgoal, resulting from your
``list_sum_not_null-lemma not to be appropriate for the generated subgoal
``(There's a (Suc i) in the generated subgoal, where your lemma has only
``an (i)).
`
Hope this helps,
Peter

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*