Рассуждения о перекрывающихся индуктивных определениях в Изабель - PullRequest
Новая
       31

Рассуждения о перекрывающихся индуктивных определениях в Изабель

0 голосов
/ 03 ноября 2018

Я хотел бы доказать следующую лемму в Изабель: 

lemma "T (Open # xs) ⟹ ¬ S (Open # xs) ⟹ count xs Close ≤ count xs Open"

Пожалуйста, найдите определения ниже: 

datatype paren = Open | Close

inductive S where
  S_empty: "S []" |
  S_append: "S xs ⟹ S ys ⟹ S (xs @ ys)" |
  S_paren: "S xs ⟹ S (Open # xs @ [Close])"

inductive T where
  T_S: "T []" |
  T_append: "T xs ⟹ T ys ⟹ T (xs @ ys)" |
  T_paren: "T xs ⟹ T (Open # xs @ [Close])" |
  T_left: "T xs ⟹ T (Open # xs)"

Лемма утверждает, что несбалансированная структура скобок может привести к возможно несбалансированной структуре при удалении скобки Open.

Я пробовал методы, описанные в книге «Помощник по доказательству для логики высшего порядка», но пока ни один из них не работает. В частности, я пытался использовать инверсию и наведение правил, sledgehammer и другие методы.

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

1 Ответ

0 голосов
/ 03 ноября 2018

Пожалуйста, найдите доказательство ниже. Маловероятно, что его можно улучшить: я пытался следовать простейшему пути к доказательству и полагался на sledgehammer, чтобы заполнить детали. 

theory so_raoidii
imports  Complex_Main

begin

datatype paren = Open | Close

inductive S where
  S_empty: "S []" |
  S_append: "S xs ⟹ S ys ⟹ S (xs @ ys)" |
  S_paren: "S xs ⟹ S (Open # xs @ [Close])"

inductive T where
  T_S: "T []" |
  T_append: "T xs ⟹ T ys ⟹ T (xs @ ys)" |
  T_paren: "T xs ⟹ T (Open # xs @ [Close])" |
  T_left: "T xs ⟹ T (Open # xs)"

lemma count_list_lem: 
  "count_list xsa a = n ⟹ 
  count_list ysa a = m ⟹ 
  count_list (xsa @ ysa) a = n + m"
  apply(induction xsa arbitrary: ysa n m)
  apply auto
  done

lemma T_to_count: "T xs ⟹ count_list xs Close ≤ count_list xs Open"
  apply(induction rule: T.induct)
  by (simp add: count_list_lem)+

lemma T_to_S_count: "T xs ⟹ count_list xs Close = count_list xs Open ⟹ S xs"
  apply(induction rule: T.induct)
  apply(auto)
  apply(simp add: S_empty)
  apply(metis S_append T_to_count add.commute add_le_cancel_right count_list_lem 
        dual_order.antisym)
  apply(simp add: count_list_lem S_paren)
  using T_to_count by fastforce

lemma "T (Open # xs) ⟹ 
      ¬ S (Open # xs) ⟹ 
      count_list xs Close ≤ count_list xs Open"
  apply(cases "T xs")
  apply(simp add: T_to_count)
  using T_to_S_count T_to_count by fastforce

end
...