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 @ 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