Как сделать пример для проверки rev_app сразу после доказательства леммы. стартовый пример для пользовательской леммы

Question

Предполагается использовать подзаголовок для запуска списка, который определяется let? аа = [1,2] и запустить rev_app на этом аа и показать значение как [2,1]

theory Scratch2 
imports Datatype 
begin 
datatype 'a list = Nil ("[]") 
        | Cons 'a "'a list" (infixr "#" 65) 
(* This is the append function: *) 
primrec app :: "'a list => 'a list => 'a list" (infixr "@" 65) 
where 
"[] @ ys = ys" | 
"(x # xs) @ ys = x # (xs @ ys)" 
primrec rev :: "'a list => 'a list" where 
"rev [] = []" | 
"rev (x # xs) = (rev xs) @ (x # [])" 
primrec itrev :: "'a list => 'a list => 'a list" where 
"itrev [] ys = ys" | 
"itrev (x#xs) ys = itrev xs (x#ys)" 
value "rev (True # False # [])" 
lemma app_Nil2 [simp]: "xs @ [] = xs" 
apply(induct_tac xs) 
apply(auto) 
done 
lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)" 
apply(induct_tac xs) 
apply(auto) 
done 

(1-й пробной)

lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)" 
apply(induct_tac xs) 
thus ?aa by rev_app 
show "rev_app [1; 2]" 

(второй пробный)

value "rev_app [1,2]" 

(3-й проб)

fun ff :: "'a list ⇒ 'a list" 
where "rev(xs @ ys) = (rev ys) @ (rev xs)" 
value "ff [1,2]" 
thus ?aa by rev_app 
show "rev_app [1; 2]" 

end 

Answer 1

Во-первых, вам нужно синтаксис списка перечисления (я просто взял его в SRC/HOL файле/List.thy):

syntax 
    -- {* list Enumeration *} 
    "_list" :: "args => 'a list" ("[(_)]") 

translations 
    "[x, xs]" == "x#[xs]" 
    "[x]" == "x#[]" 

Тогда это один из следующих, что вы» искать?

Предложение 1:

lemma example1: "rev [a, b] = [b, a]" 
    by simp 

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

Предложение 2:

value "rev [a, b]" (* return "[b, a]" *) 

Здесь и в предложении 3, мы просто использует команду value для оценки rev.

Предложение 3:

value "rev [a, b] = [b, a]" (* returns "True" *) 

---

Эта лемма не используются предыдущие предложения:

lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)" 
    apply (induct_tac xs) 
    by simp_all 

Примечания:

• В качестве общего принципа, вы не должны» t импортируйте только пакет «Тип данных», но импортируйте «Main» instea д.
• В вашей первой попытке вы смешаете «применить» (применить ...) и стили «структурированного доказательства» (таким образом ...)
• «таким образом? Aa» не имеет смысла, если «? Aa» является «[1,2]», поскольку аргумент «таким образом» должен быть подцелем, т. е. предложение с булевым значением.
• Чтобы оценить, команда «значение» использует выполнение ML, или если это не удается, нормализация путем оценки.
• В example1, вы можете использовать пользовательские доказательства и, следовательно, Леммы (например: с помощью (простофиля добавить: rev_app)