Как применить стандарт ко всем подцелям в Изабель? - PullRequest
Новая
       18

Как применить стандарт ко всем подцелям в Изабель?

1 голос
/ 11 марта 2020

Чтобы доказать равенство «A = B», можно доказать два включения «A ⊆ B» и «B ⊆ A». Теперь я использую метод «стандарт», чтобы превратить эту цель в цель «исправить x в A и показать, что x в B». Однако я не знаю, как это сделать на всех подцелях.

Как я могу сделать это в Изабель?

1 Ответ

1 голос
/ 11 марта 2020

Я решил добавить комментарий peq к моему ответу

, если вы импортируете HOL-Eisbach.Eisbach, вы можете использовать apply (all ‹standard›)

Если в результате применения метода из одной цели возникает несколько целей, вы можете использовать точку с запятой ; (структурная структура: см. Раздел 6.4 в Isar-ref), чтобы применить следующий метод ко всем возникающим подзадачам. , т.е. 

lemma "(A::'a set) = B ∧ (C::'a set) = D"
  apply(intro conjI; standard; standard)
  done

LEGACY (метод all из HOL-Eisbach включает в себя функциональность tacti c ниже: см. выше)

Учитывая, что вы знакомы В отношении Изабель / ML я хотел бы предложить следующие тактики c (вы можете sh адаптировать / улучшить их в соответствии с вашими потребностями - это всего лишь идея): 

ML‹
fun multistandard_tac ctxt = 
  ALLGOALS (fn i => SELECT_GOAL (Classical.standard_tac ctxt []) i)
›

lemma "(A::'a set) = B" and "(C::'a set) = D"
  apply(tactic‹multistandard_tac @{context}›)
  apply(tactic‹multistandard_tac @{context}›)
  done

(*
goal (4 subgoals):
 1. ⋀x. x ∈ A ⟹ x ∈ B
 2. ⋀x. x ∈ B ⟹ x ∈ A
 3. ⋀x. x ∈ C ⟹ x ∈ D
 4. ⋀x. x ∈ D ⟹ x ∈ C
*)

Of Конечно, из него должно быть достаточно легко создать метод.

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

lemma "(A::'a set) = B"
  apply(intro subset_antisym subsetI)
  done

Надеюсь, должно быть достаточно легко увидеть, как вы можете применять этот метод одновременно к нескольким подцелям.

...