Определение функции с несколькими привязками в Isabelle - PullRequest
Новая
       46

Определение функции с несколькими привязками в Isabelle

2 голосов
/ 18 июня 2020

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

theory Example
  imports "Nominal2.Nominal2" 
begin


atom_decl vrs

nominal_datatype ty = 
    Top

nominal_datatype trm = 
    Var   "vrs"
  | Abs   x::"vrs" t::"trm" T::"ty" binds x in t T

nominal_function
  fv :: "trm ⇒ vrs set"
where
  "fv (Var x) = {x}"
| "fv (Abs x t T) = (fv t) - {x}"
  using [[simproc del: alpha_lst]]  
  subgoal by(simp add: fv_graph_aux_def eqvt_def eqvt_at_def)
  subgoal by simp
  subgoal for P x
    apply(rule trm.strong_exhaust[of x P]) 
    by( simp_all add: fresh_star_def fresh_Pair)
                apply simp_all
  subgoal for x T t xa Ta ta  
    sorry

end

Мне не удалось показать последнюю цель:

eqvt_at fv_sum C T ⟹ eqvt_at fv_sum C Ta ⟹ [[атом x]] lst. (T, t) = [[атом xa]] lst. (Та, та) ⟹ fv_sum C T - {x} = fv_sum C Ta - {xa}

несмотря на мои дневные усилия.

Решение 

subgoal for x T t xa Ta ta  
  proof -
    assume 1: "[[atom x]]lst. (t, T) = [[atom xa]]lst. (ta, Ta)"
          " eqvt_at fv_sumC t" " eqvt_at fv_sumC ta"
    then have 2: "[[atom x]]lst. t = [[atom xa]]lst. ta"
      by(auto simp add: Abs1_eq_iff'(3) fresh_Pair)      
    show "removeAll x (fv_sumC t) = removeAll xa (fv_sumC ta)"
      apply(rule Abs_lst1_fcb2'[OF 2, of _ "[]"])
         apply (simp add: fresh_removeAll)
        apply (simp add: fresh_star_list(3))
      using 1 Abs_lst1_fcb2' unfolding eqvt_at_def
      by auto
  qed

1 Ответ

1 голос
/ 19 июня 2020

Я рад, что вы смогли найти решение. Тем не менее, я все же хотел бы уточнить комментарий, который я сделал ранее. В частности, я хотел бы подчеркнуть, что nominal_datatype уже автоматически предоставляет очень похожую функцию: это функция fv_trm. Эта функция фактически эквивалентна функции fv в вашем вопросе. Вот грубый набросок (доказательство нужно будет уточнить) теории, которая это демонстрирует: 

theory Scratch
  imports "Nominal2.Nominal2"
begin

atom_decl vrs

nominal_datatype ty = 
  Top

nominal_datatype trm = 
    Var vrs
  | Abs x::vrs t::trm T::ty binds x in t T

lemma supp_ty: "supp (ty::ty) = {}"
  by (metis (full_types) ty.strong_exhaust ty.supp)

lemmas fv_trm = trm.fv_defs[unfolded supp_ty supp_at_base, simplified]

lemma dom_fv_trm: 
  "a ∈ fv_trm x ⟹ a ∈ {a. sort_of a = Sort ''Scratch.vrs'' []}"
  apply(induction rule: trm.induct)
  unfolding fv_trm 
  by auto

lemma inj_on_Abs_vrs: "inj_on Abs_vrs (fv_trm x)"
  using dom_fv_trm by (simp add: Abs_vrs_inject inj_on_def)

definition fv where "fv x = Abs_vrs ` fv_trm x"

lemma fv_Var: "fv (Var x) = {x}"
  unfolding fv_def fv_trm using Rep_vrs_inverse atom_vrs_def by auto

(*I leave it to you to work out the details, 
but Sledgehammer already finds something sensible*)
lemma fv_Abs: "fv (Abs x t T) = fv t - {x}"
  using inj_on_Abs_vrs
  unfolding fv_def fv_trm 
  sorry

end
...