# 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

```

• References:

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