关于伊莎贝尔重叠归纳定义的推理
Reasoning about overlapping inductive definitions in Isabelle
我想证明 Isabelle 中的以下引理:
lemma "T (Open # xs) ⟹ ¬ S (Open # xs) ⟹ count xs Close ≤ count xs Open"
请找到以下定义:
datatype paren = Open | Close
inductive S where
S_empty: "S []" |
S_append: "S xs ⟹ S ys ⟹ S (xs @ ys)" |
S_paren: "S xs ⟹ S (Open # xs @ [Close])"
inductive T where
T_S: "T []" |
T_append: "T xs ⟹ T ys ⟹ T (xs @ ys)" |
T_paren: "T xs ⟹ T (Open # xs @ [Close])" |
T_left: "T xs ⟹ T (Open # xs)"
引理指出,不平衡的括号结构在删除 Open
括号时可能会导致结构不平衡。
我一直在尝试 "A proof-assistant for Higher-order logic" 书中描述的技术,但到目前为止 none 有效。特别是,我尝试使用规则反转和规则归纳,sledgehammer
和其他技术。
其中一个问题是我还没有了解Isar证明,因此使证明变得复杂。如果你能用简单的应用命令来指导我,我会更愿意。
请在下面找到证明。它并非不可能得到改进:我尝试按照最简单的方法进行证明,并依靠 sledgehammer
来填写细节。
theory so_raoidii
imports Complex_Main
begin
datatype paren = Open | Close
inductive S where
S_empty: "S []" |
S_append: "S xs ⟹ S ys ⟹ S (xs @ ys)" |
S_paren: "S xs ⟹ S (Open # xs @ [Close])"
inductive T where
T_S: "T []" |
T_append: "T xs ⟹ T ys ⟹ T (xs @ ys)" |
T_paren: "T xs ⟹ T (Open # xs @ [Close])" |
T_left: "T xs ⟹ T (Open # xs)"
lemma count_list_lem:
"count_list xsa a = n ⟹
count_list ysa a = m ⟹
count_list (xsa @ ysa) a = n + m"
apply(induction xsa arbitrary: ysa n m)
apply auto
done
lemma T_to_count: "T xs ⟹ count_list xs Close ≤ count_list xs Open"
apply(induction rule: T.induct)
by (simp add: count_list_lem)+
lemma T_to_S_count: "T xs ⟹ count_list xs Close = count_list xs Open ⟹ S xs"
apply(induction rule: T.induct)
apply(auto)
apply(simp add: S_empty)
apply(metis S_append T_to_count add.commute add_le_cancel_right count_list_lem
dual_order.antisym)
apply(simp add: count_list_lem S_paren)
using T_to_count by fastforce
lemma "T (Open # xs) ⟹
¬ S (Open # xs) ⟹
count_list xs Close ≤ count_list xs Open"
apply(cases "T xs")
apply(simp add: T_to_count)
using T_to_S_count T_to_count by fastforce
end
我想证明 Isabelle 中的以下引理:
lemma "T (Open # xs) ⟹ ¬ S (Open # xs) ⟹ count xs Close ≤ count xs Open"
请找到以下定义:
datatype paren = Open | Close
inductive S where
S_empty: "S []" |
S_append: "S xs ⟹ S ys ⟹ S (xs @ ys)" |
S_paren: "S xs ⟹ S (Open # xs @ [Close])"
inductive T where
T_S: "T []" |
T_append: "T xs ⟹ T ys ⟹ T (xs @ ys)" |
T_paren: "T xs ⟹ T (Open # xs @ [Close])" |
T_left: "T xs ⟹ T (Open # xs)"
引理指出,不平衡的括号结构在删除 Open
括号时可能会导致结构不平衡。
我一直在尝试 "A proof-assistant for Higher-order logic" 书中描述的技术,但到目前为止 none 有效。特别是,我尝试使用规则反转和规则归纳,sledgehammer
和其他技术。
其中一个问题是我还没有了解Isar证明,因此使证明变得复杂。如果你能用简单的应用命令来指导我,我会更愿意。
请在下面找到证明。它并非不可能得到改进:我尝试按照最简单的方法进行证明,并依靠 sledgehammer
来填写细节。
theory so_raoidii
imports Complex_Main
begin
datatype paren = Open | Close
inductive S where
S_empty: "S []" |
S_append: "S xs ⟹ S ys ⟹ S (xs @ ys)" |
S_paren: "S xs ⟹ S (Open # xs @ [Close])"
inductive T where
T_S: "T []" |
T_append: "T xs ⟹ T ys ⟹ T (xs @ ys)" |
T_paren: "T xs ⟹ T (Open # xs @ [Close])" |
T_left: "T xs ⟹ T (Open # xs)"
lemma count_list_lem:
"count_list xsa a = n ⟹
count_list ysa a = m ⟹
count_list (xsa @ ysa) a = n + m"
apply(induction xsa arbitrary: ysa n m)
apply auto
done
lemma T_to_count: "T xs ⟹ count_list xs Close ≤ count_list xs Open"
apply(induction rule: T.induct)
by (simp add: count_list_lem)+
lemma T_to_S_count: "T xs ⟹ count_list xs Close = count_list xs Open ⟹ S xs"
apply(induction rule: T.induct)
apply(auto)
apply(simp add: S_empty)
apply(metis S_append T_to_count add.commute add_le_cancel_right count_list_lem
dual_order.antisym)
apply(simp add: count_list_lem S_paren)
using T_to_count by fastforce
lemma "T (Open # xs) ⟹
¬ S (Open # xs) ⟹
count_list xs Close ≤ count_list xs Open"
apply(cases "T xs")
apply(simp add: T_to_count)
using T_to_S_count T_to_count by fastforce
end