'case _ of' 非数据类型常量参数，simps_of_case

Question

我正在查看 case 运算符，看看它能为我做什么。

没有问题。考虑到我正在使用的例子，我接受 "it does what it does"，但我会问一些问题以防有更多东西需要学习。

看来 case 运算符不能接受常量参数，除非它们是 datatype 常量。如果不是，它会给出无意义的消息："Error in case expression: type mismatch"。
- 我可以 case 对非数据类型常量进行模式匹配吗？
关键字 simps_of_case 有时会从 case 生成简单规则，有时则不会。
- 对于下面的示例，它只是将 yield2_def 重现为 simp 规则，有什么我应该知道的吗？

我从 How to define a partial function in Isabelle? 中为 simps_of_case 举了一个例子。我似乎在某处了解到 case 是围绕 datatype 设计的，但我找不到我在哪里了解到的。

我在示例中包含了一个简短的理论：

theory i150903a__a0  
imports Complex_Main "~~/src/HOL/Library/Simps_Case_Conv"
begin 
(*************************************************************************)
section{* simps_of_case: Doesn't generate any new simps *}

(*(58)/src/HOL/Lazy_Sequence.thy
[∙) Doesn't generate any new simp rules. Because of 'list_of_lazy_sequence'?*)
definition yield2 :: "'a lazy_sequence => ('a × 'a lazy_sequence) option"
where
  "yield2 xq = (case list_of_lazy_sequence xq of
    [] => None
  | x # xs => Some (x, lazy_sequence_of_list xs))"

thm yield2_def  
find_theorems name: yield2

simps_of_case yield2_simps[simp]: yield2_def

thm yield2_simps
find_theorems name: yield2

(*************************************************************************)
section{* simps_of_case: Does generate new simps *}

(*140813a__SOz__How to define a partial function in Isabelle*)
partial_function (tailrec) oddity :: "nat => nat" where 
  "oddity x = (case x of (Suc (Suc n)) => n | 0 => 0 )"

thm oddity.simps  
find_theorems name: oddity

simps_of_case oddity_simps[simp]: oddity.simps

thm oddity_simps
find_theorems name: oddity

(*************************************************************************)
section{* Case constant arguments must be datatypes? *}

declare[[show_sorts]]
(*Works*)
term "case (x,y) of (None, None) => (0::'a::zero, 0::'b::zero)"

term "case (x,y) of (0::nat, 0::nat) => (0::'a::zero, 0::'b::zero)"

term "case (x,y) of (0::nat, x # xs) => (0::'a::zero, 0::'b::zero)"

term "case (x,y) of (a,b) => (0::'a::zero, 0::'b::zero)"

fun foofun :: "('a::zero, 'b::zero) prod => ('a, 'b) prod" where
  "foofun (x,y) = (case (x,y) of (a,b) => (0,0))"

(*OUTPUT: "Error in case expression: type mismatch"*)  
term "case (x,y) of (0::nat, 0::int) => (0::'a::zero, 0::'b::zero)"

fun foofun :: "('a::zero, 'b::zero) prod => ('a, 'b) prod" where
  "foofun (x,y) = (case (x,y) of (0,0) => (0,0))"

(*************************************************************************)
section{* Theory end *}
end

Answer 1

Case 语法只是糖——它被脱糖为适当 "case combinators" 的嵌套应用程序。数据类型手册在 §2.3 中对此进行了简要提示。据我所知，为了使 case 语法起作用，给定类型必须有一个 case 组合子。现有的案例组合器是例如case_option 和 case_list。现在，如果某些东西没有被定义为数据类型，还有其他方法可以获得该组合器（例如 free_constructors）命令。 int 没有那种设置。
simps_of_case 将 f x = P (case x of ...) 形式的方程式转换为 f pat1 = P ...、f pat2 = P ... 形式的方程式，... 如果您对不是参数列表中的变量的术语进行模式匹配，它不能这样做。在您的示例中，您希望生成什么？

'case _ of' 非数据类型常量参数，simps_of_case

'case _ of' non-datatype constant args, simps_of_case

isabelle