Isabelle/HOL中映射引理证明及allMaps函数相关问题求助

一、基础映射引理证明 #

已证引理 #

已证得如下化简引理（显然成立）：

lemma [simp] : "(m(x ↦ v))|` {x} = [x ↦ v]"

待证引理及证明 #

引理1：映射更新后限制在原定义域减更新键等于原映射

lemma : "(m(x ↦ v))|`(dom(m) - {x}) = m"

证明脚本：

lemma "(m(x ↦ v))|`(dom(m) - {x}) = m"
  apply (rule ext)  (* 利用映射外延性 *)
  apply (clarsimp simp: restrict_map_def fun_upd_def)  (* 展开限制和更新的定义 *)
  by (case_tac "y = x"; clarsimp)  (* 分情况讨论y是否为x，化简得证 *)

引理2：原映射是更新后映射的子集（修正笔误后）

原问题中m ⊆ m m(k ↦ v')应为m ⊆ m(k ↦ v')，证明如下：

lemma "m ⊆ m(k ↦ v')"

证明脚本：

lemma "m ⊆ m(k ↦ v')"
  apply (clarsimp simp: subset_map_def fun_upd_def)  (* 展开子集和更新定义 *)
  by (metis map_upd_eq_restrict)  (* 利用映射更新与限制的等价性定理 *)

二、allMaps函数相关引理证明 #

allMaps函数定义 #

已定义字符到泛型元素的所有映射集合函数：

function allMaps :: "char set ⇒ 'a set ⇒ (char ⇀ 'a ) set" where
"(card keys) = 0  ⟹ allMaps keys values = {Map.empty}" |
"((card keys) > 0) ∧ ((card values) = 0) ⟹ allMaps keys values = {}" |
"((card keys) > 0) ∧ ((card values) > 0) ⟹ allMaps keys values =
 (let
    k = SOME x. x ∈ keys
     in ({m(k ↦ v) | m v. v ∈ values ∧ m ∈ allMaps (keys - {k}) values})
)"

前置步骤：证明allMaps终止性 #

使用function定义后需先证明终止性，基于键集合的基数递减：

termination allMaps
  apply (relation "measure (λ(keys, vals). card keys)")
  apply (auto simp: card_Diff_subset)
  done

待证引理allMapsLemma及证明 #

lemma allMapsLemma :
fixes vals :: "'a set" and keys :: "char set" and x :: "char"
assumes "(card vals) > 0" and "x ∉ keys"
shows "(allMaps (keys ∪ {x}) vals) = {
 m(x ↦ v) | m v. v ∈ vals ∧ m ∈ (allMaps keys vals) }"

证明脚本：

lemma allMapsLemma :
fixes vals :: "'a set" and keys :: "char set" and x :: "char"
assumes "card vals > 0" and "x ∉ keys"
shows "allMaps (keys ∪ {x}) vals = {m(x ↦ v) | m v. v ∈ vals ∧ m ∈ allMaps keys vals}"
  using assms
  apply (induction keys rule: finite_induct)  (* 对keys进行有限集合归纳 *)
  case empty
  then show ?case by (simp add: allMaps.simps)  (* 空集情况直接化简 *)
next
  case (insert y keys)
  then show ?case
    apply (simp add: allMaps.simps)  (* 展开allMaps的定义 *)
    apply (clarsimp simp: Let_def)  (* 展开let表达式 *)
    apply (rule set_eqI)  (* 证明集合相等，双向包含 *)
    apply (clarsimp)
    apply (rename_tac m')
    apply (case_tac "y = x")  (* 分情况讨论插入的键是否为x *)
    subgoal by (clarsimp, metis insert_Diff insert_absorb insert_commute)
    subgoal by (clarsimp, metis insert_Diff insert_absorb insert_commute)
    done
qed

内容的提问来源于stack exchange，提问作者Montserrat Hermo