theory week03B_demo_simp
imports Main
begin
text \Simplification\
text \
Lists:
@{term "[]"} empty list
@{term "x#xs"} cons (list with head x and tail xs)
@{term "xs @ ys"} append xs and ys
\
lemma "ys @ [] = []"
apply(simp)
oops
definition
a :: "nat list"
where
"a \ []"
definition
b :: "nat list"
where
"b \ []"
text \simp add, rewriting with definitions\
lemma "xs @ a = xs"
apply (simp add: a_def)
done
text \simp only\
lemma "xs @ a = xs"
apply (simp only: a_def)
apply simp
done
lemma ab [simp]: "a = b" by (simp add: a_def b_def)
lemma ba [simp]: "b = a" by simp
text \simp del, termination\
lemma "a = []"
(*apply (simp add: a_def)
does not terminate *)
apply (simp add: a_def del: ab)
done
text\Simple assumption:\
lemma "xs = [] \ xs @ ys = ys @ xs @ ys"
apply simp
oops
text\Simplification in assumption:\
lemma "\ xs @ zs = ys @ xs; [] @ xs = [] @ [] \ \ ys = zs"
apply simp
done
end