Условные правила перезаписи с неизвестными в состоянии

Question

В моей теории у меня есть несколько более крупных определений, из которых я получаю некоторые простые свойства, используя леммы.

Моя проблема заключается в том, что лемы для получения свойств не используются упростителем, и я должен их вручную создавать. Есть ли способ сделать это более автоматическим?

Минимальный пример показан ниже:

definition complexFact :: "int ⇒ int ⇒ int ⇒ bool" where 
"complexFact x y z ≡ x = y + z" 

lemma useComplexFact: "complexFact x y z ⟹ x = y + z" 
by (simp add: complexFact_def) 

lemma example_1: 
assumes cf: "complexFact a b c" 
shows "a = b + c" 
apply (simp add: cf useComplexFact) (* easy, works *) 
done 

lemma example_2a: 
assumes cf: "complexFact a b c" 
shows "a - b = c" 
apply (simp add: cf useComplexFact) (* does not work *) 
oops 

lemma example_2b: 
assumes cf: "complexFact a b c" 
shows "a - b = c" 
apply (simp add: useComplexFact[OF cf]) (* works *) 
done 

lemma example_2c: 
assumes cf: "complexFact a b c" 
shows "a - b = c" 
apply (subst useComplexFact) (* manually it also works*) 
apply (subst cf) 
apply simp+ 
done 

я нашел следующий пункт в справочном руководстве, так что я думаю, я мог бы решить мою проблему с помощью пользовательского решателя. Тем не менее, я никогда не касался внутренней части ML Изабель и не знаю, с чего начать.

Переписывание не создает неизвестные. Например, переписывание в одиночку не может доказать a ∈? A, поскольку для этого требуется создание экземпляра? A. Решатель , однако, является произвольной тактикой и может создавать неизвестные , как это угодно. Это единственный способ, которым Упрощенный может обрабатывать правило условного перезаписи , условие которого содержит дополнительные переменные.

Answer 1

Упрощение Isabelle само по себе никогда не создает неизвестных в предположениях условных правил перезаписи. Однако решатели могут это сделать, а самый надежный - assumption. Так что если complex_fact a b c буквально появляется в предположениях цели (вместо того, чтобы быть добавленным к симпсету с simp add: или с [simp]), решатель допусков запускает и создает неизвестные. Однако в предположениях он будет использовать только первый экземпляр complex_fact. Поэтому, если их несколько, они не будут пытаться их использовать. Таким образом, это лучше писать

lemma 
    assumes cf: "complexFact a b c" 
    shows "a = b + c" 
    using cf 
    apply(simp add: useComplexFact) 

Вторая проблема с вашим примером является то, что a = b + c с a, b и c быть свободным не является хорошим правилом переписан, так как символ головы на левой стороне не является постоянной, но свободной переменной a. Поэтому упрощение не будет использовать уравнение a = b + c для замены a на b + c, но для замены буквальных вхождений уравнения a = b + c с True. Вы можете увидеть эту предварительную обработку в следе простейшего (включите его локально с using [[simp_trace]]). Вот почему example_1 работает, а другие нет. Если вы можете изменить свою левую сторону таким образом, чтобы в качестве символа головы была константа, тогда некоторая достойная защита от ошибок должна быть возможна без написания пользовательского решателя.

Кроме того, вы можете сделать некоторую (ограниченную) форму форвардного рассуждения, используя useComplexFact как правило уничтожения. То есть,

using assms 
apply(auto dest!: useComplexFact) 

также может работать в некоторых случаях. Однако это довольно близко к раскрытию определения с точки зрения масштабируемости.

Answer 2

Вы можете указать в определении, что он должен автоматически подаваться в Simplifier, предваряя [simp]: так:

definition complexFact :: "int ⇒ int ⇒ int ⇒ bool" where 
[simp]: "complexFact x y z ≡ x = y + z" 

Теперь все ваши примеры Лемма должна быть разрешима непосредственно using cf by simp.