0

我有带有非归纳定义的 Isabelle 理论（我想对避免归纳的算法进行建模，就像工业开发人员通常所做的那样）和为此定义说明的引理：

theory Maximum
  imports (* Main *)
    "HOL-Library.Multiset"
    "HOL-Library.Code_Target_Numeral"
    "HOL-Library.Code_Target_Nat"
    "HOL-Library.Code_Abstract_Nat"
begin

definition two_integer_max_case_def :: "nat ⇒ nat ⇒ nat" where
"two_integer_max_case_def a b = (case a > b of True ⇒ a | False ⇒ b)"

lemma spec_1:
  fixes a :: nat and b :: nat
  assumes "a > b"
  shows "two_integer_max_case_def a b = a"
  apply (induction b)
  apply (induction a)
  apply simp_all
  done

end

当前的证明状态已经生成了 3 个目标，所有这些目标都与归纳有关（直接应用 simp 失败并显示Failed to apply proof method）：

proof (prove)
goal (3 subgoals):
 1. two_integer_max_case_def 0 0 = 0
 2. ⋀a. two_integer_max_case_def a 0 = a ⟹
         two_integer_max_case_def (Suc a) 0 =
         Suc a
 3. ⋀b. two_integer_max_case_def a b = a ⟹
         two_integer_max_case_def a (Suc b) = a

我的问题是 - 是否有可以避免归纳的证明方法和策略，并且可以应用于这个简单的案例？也许与simp战术家族有关？

4

0 回答 0