Email Gateway (Aug 18 2022 at 12:34): Email Gateway (Aug 18 2022 at 12:34):From: 游珍 <yucy0405@163.com>
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:
theory minsum
imports Main
begin
fun sum :: "nat \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat"
where
"sum i j xs = (if j\<ge>size xs then 0 else (if i>j then 0 else (\<Sum>k\<in>{i..<Suc j}. (xs !k))))"
(------------(sum k j xs) i\<le>k\<le>j----------------)
function list_sum :: "nat \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat list"
where
"list_sum i j xs =(if j\<ge>size xs then [] else ( if i>j then [] else (sum i j xs)#(list_sum (Suc i) j xs) ))"
by pat_completeness auto
termination
by (relation "measure (\<lambda>(i,j,_). j + 1 - i)") auto
(-------------- min of list_sum-----------------)
fun ms :: "nat \<Rightarrow> nat list \<Rightarrow> nat"
where
"ms j xs = Min (set (list_sum 0 j xs))"
(--------------(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-------------------)
fun minsum :: "nat \<Rightarrow> nat list \<Rightarrow> nat"
where
"minsum n xs = Min (set_sum n xs)"
lemma finite_list_sum [simp] : "finite (set (list_sum i j xs))"
apply (induct i)
apply simp
apply simp
done
lemma finite_set_sum [simp] : "finite (set_sum n xs)"
apply (induct n)
apply simp
apply simp
done
lemma list_sum_not_null [simp]: "i>0\<and>(size xs)>i \<Longrightarrow> (set (list_sum 0 i xs)) \<noteq> {}"
apply auto
done
lemma set_sum_not_null [simp]: "i>0\<and>(size xs)>i \<Longrightarrow> (set_sum i xs) \<noteq> {}"
apply (induct i)
apply auto
done
lemma recur1 : "i>0\<and>(size xs)>i \<Longrightarrow> (min (minsum i xs) (ms (Suc i) xs)) = (minsum (Suc i) xs)"
apply (unfold minsum.simps )
apply (unfold ms.simps)
apply ( ???????? Min_Un)
After I excute the command "apply (unfold ms.simps)", I got a goal as follows:
goal (1 subgoal):
0 < i \<and> i < length xs \<Longrightarrow>
min (Min (set_sum i xs)) (Min (set (list_sum 0 (Suc i) xs))) = Min (set_sum (Suc i) xs)
In order to get the result:
"0 < i \<and> i < length xs \<Longrightarrow>
Min (set_sum i xs)\<union> (set (list_sum 0 (Suc i) xs))= Min (set_sum (Suc i) xs)"
I try to use a theorem "Min_Un" providede for isabelle. Before using "Min_Un",I proof four lemmas, which are "finite_list_sum", "finite_set_sum", "list_sum_not_null" and "set_sum_not_null".
However, i still don not success by using "apply (rule Min_Un)","apply (simp add:Min_Un)" or "apply (subst Min_Un)", I don't know how to use it. Maybe the theorem "Min_Un" is not suitable to apply in my proof, Need help !
Thanks for your attention!
yucy
prombleletter2.thy
Email Gateway (Aug 18 2022 at 12:34):From: Peter Lammich <peter.lammich@uni-muenster.de>
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
Last updated: May 03 2024 at 12:27 UTC