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

Question

Я смотрел на оператора case, чтобы посмотреть, что он может сделать для меня.

Нет проблем. Учитывая примеры, с которыми я работаю, я согласен с тем, что «он делает то, что он делает», но я задаю несколько вопросов, если есть чему поучиться.

1. Оказывается, что оператор case не может принимать аргументы, которые являются постоянными, если они не datatype константы. Если это не так, это дает неинформативное сообщение: «Ошибка в выражении случая: несоответствие типа».
   • Могу ли я получить case для соответствия шаблону по константе не-типа данных?
2. Ключевое слово simps_of_case иногда производит правила simp от case, а иногда и нет.
   • Есть ли что-то, что я должен знать о примере ниже, где он просто воспроизводит yield2_def в качестве правила simp?

Я взял один пример simps_of_case из How to define a partial function in Isabelle?. Кажется, что я узнал где-то, что 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

1. синтаксис случая только сахар - он получает обессахаренный к вложенному применению соответствующих «дела комбинаторов». Справочник типа данных кратко намекает на это в п. 2.3. Насколько я знаю, для синтаксиса case должен быть комбинатор case для заданного типа. Существующие комбинаторы событий являются, например, case_option и case_list. Теперь, если что-то не определено как тип данных, есть другие способы получить эту комбинатор (например, команду free_constructors). int не имеет такой настройки.

2. simps_of_case преобразует уравнение вида f x = P (case x of ...) в уравнения вида f pat1 = P ..., f pat2 = P ... ... Если вы по шаблону на срок, который не является переменной из списка аргументов, он не может сделать это , В вашем примере, что вы ожидали получить?