Attic/MyInduction.thy
author Chengsong
Wed, 02 Mar 2022 23:13:59 +0000
changeset 438 a73b2e553804
parent 95 a33d3040bf7e
permissions -rw-r--r--
templateforPhd

theory MyInduction
imports Main
begin

fun itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
"itrev [] ys = ys" |
"itrev (x#xs) ys = itrev xs (x#ys)"

lemma "itrev xs [] = rev xs"
apply(induction xs)
apply(auto)
oops

lemma "itrev xs ys = rev xs @ ys"
apply(induction xs arbitrary: ys)
apply auto
done