Применить метод, если и только если он решает текущую задачу

Question

Иногда, когда я пишу доказательства применить стиле, я хотел способ модифицировать метод доказательства foo к

Попробуйте foo на первый Цель. Если он решает цель, хорошо; если он не решает его, вернитесь в исходное состояние и не получится.

Это произошло в следующем коде:

qed (subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail)+ 

После некоторого изменения дальше, вызов simp не будет в полной мере решить задачу больше, и тогда это будет цикл. Если бы я мог указано что-то вроде

qed (solve_goal(subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail))+ 

или (альтернативный вариант предложил synatx)

qed ((subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail)!)+ 

или (может быть, даже лучше, синтаксис)

qed ((subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail)[1!])+ 

он остановился бы на первый гол, не был разрешен этим сценарием.

Answer 1

С появлением Eisbach proof script language, это теперь поддерживается , После импорта "~~/src/HOL/Eisbach/Eisbach", можно заменить

apply foo 

с

apply (solves ‹foo›) 

и линия потерпит неудачу, если solves производит какие-либо новые цели. Это может быть объединен с [1], как в

apply (solves ‹(auto)[1]›) 

при желании.

Определение solves на самом деле довольно просто:

method solves methods m = (m; fail) 

Answer 2

Изабель не имеет такого комбинатора, который тоже я пропустил. Часто я могу избежать необходимости в таком комбинаторе, если я заменил auto или simp звонки на fastforce или force (которые имеют поведение с ошибкой или неудачей).

Таким образом, если simp в вашем примере предполагается решить задачу (без зацикливания),

qed (subst fibs.simps, (subst fib.simps)?, fastforce simp: nth_zipWith nth_tail)+ 

может быть более надежным вариантом.

Answer 3

Язык Isar Isabelle не предусматривает эту функцию; это намеренное и не ошибка, как объяснено on the isabelle developer list:

Изар язык доказательства метод был разработан определенный путь, чтобы прибыть в «stilized» характеристики некоторых оперативных аспектов в доказательство текста. Он исключил любые виды программирования или сложного управления объектами .

Answer 4

Хотя нет встроенной тактики или комбинатора доступны, вы можете реализовать его самостоятельно следующий образом:

ML {* 
fun solved_tac thm = 
    if nprems_of thm = 0 then Seq.single thm else Seq.empty 
*} 

method_setup solved = {* 
    Scan.succeed (K (SIMPLE_METHOD solved_tac)) 
*} 

Это создает новый метод solved, который будет успешным, если текущая цель была полностью решена , или сбой, если осталось еще одно или несколько подцелей.

Он может быть использован, например, следующим образом:

lemma "a ∨ ¬ a " 
    apply ((rule disjI1, solved) | (simp, solved)) 
    done 

Без пункта solved, Isabelle отберет rule disjI1 сторону apply шага, оставив вас с неразрешимой целью.С предложением solved в каждой стороне Изабель пытается использовать rule disjI1 и, когда он не может решить цель, переключается на simp, который затем успешно завершен.

Это может использоваться, чтобы решить индивидуальные цели, используя синтаксис Isabelle's (...)[1]. Например, следующий оператор будет пытаться решить столько подцели, как это возможно с помощью simp, но оставит подцель неизменным, если simp не сможет полностью решить:

apply ((simp, solved)[1])+