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.