theory week04A_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