Нормальное определение константы в сравнении с определением лямбда-константы

Question

У меня есть эти два определения. Почему они разворачиваются по-разному? Как я могу доказать леммы о "ой"? (И вообще, в чем разница между этими двумя определениями в Изабель, внутри?)

(Пожалуйста, не направляйте меня на внешние ссылки, потому что я обычно завален информацией там.)

  definition "f x y = x+y"
  definition "g ≡ λx y. x+y"

  value "f 1 2" (* "1 + (1 + 1)" :: "'a" *)
  value "g 1 2" (* "1 + (1 + 1)" :: "'a" *)

  value "f 1"   (* "op + 1" :: "'a ⇒ 'a" *)
  value "g 1"   (* "op + 1" :: "'a ⇒ 'a" *)

  value "f"     (* "op +" :: "'a ⇒ 'a ⇒ 'a" *)
  value "g"     (* "op +" :: "'a ⇒ 'a ⇒ 'a" *)


  lemma "f x y≡g x y" 
    apply (simp add:f_def g_def)
  done 

  lemma "f x ≡g x"
    apply (simp add:f_def g_def)
    (* f x ≡ op + x *)
  oops

  lemma "f ≡ g"
    apply (simp add:f_def g_def)
    (* f ≡ op + *)
  oops

Answer 1

Разница между определением с явными аргументами слева (например, f x y = x + y) и один с лямбдами справа (вроде g = (%x y. x + y)) Какое определяющее уравнение вы получите из этого.

Для первых это

f_def: "f ?x ?y = ?x + ?y"

(т. е. это уравнение применимо, только если все аргументы f присутствуют, таким образом, это не применимо к f один или частично f xнапример) и для последнего

g_def: "g = op +"

(где op + это просто синтаксический сахар для %x y. x + y; обратите внимание, что это уравнение, в отличие от первого, применимо к каждому случаю g бы то ни было).

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

1. Атрибут [abs_def] преобразовывает уравнение с аргументами в одно с лямбдами. Например, f_def [abs_def] результаты в f = op +,

2. Лемма ext (для расширения) явно добавляет аргументы в уравнения между функциями.

   ext: "(!!x. ?f x = ?g x) ⟹ ?f = ?g"
   

Для ваших лемм достаточно одного из этих методов. Либо добавить [abs_def] для каждого случая f_def в ваших попытках доказательства или сделайте следующее.

lemma "f x = g x"
apply (intro ext)
apply (simp add: f_def g_def)
done

lemma "f = g"
apply (intro ext)
apply (simp add: f_def g_def)
done

куда intro относится ext как можно чаще (в зависимости от типа функции).

Обратите внимание, что я использовал HOL равенства (op =) а не чистое равенство (op ≡) в приведенных выше доказательствах. Хотя оба логически эквивалентны, лемма ext относится только к первому. Как правило: для Изабель /HOL придерживаться op = когда возможно.