theory week04A_demo_intro imports Main begin lemma div_0: "0 div (x::nat) = 0" apply(rule semidom_divide_class.div_0) done thm mult_0 (* All goals up to now have been solvable using intro/elim rules only. Rules that are equalities (like those above) can be used as intro rules for goals that match their shape. *) lemma "\ x::nat. x div 2 = 0" apply(rule_tac x=0 in exI) apply(rule div_0) done (* However, using these rules as intro rules cannot solve the following goal. Instead, we need to use these rules to rewrite the left- and right-hand sides of the equality to match each other. *) lemma "\ x::nat. (x div 2) * 2 = 0 * x" apply(rule_tac x=0 in exI) thm ssubst thm ssubst[OF div_0] apply(rule ssubst[OF div_0]) apply(rule ssubst[OF mult_0[where n=2]]) apply(rule ssubst[OF mult_0[where n=0]]) apply(rule refl) done (* this rewriting is automated by Isabelle's rewrite-engine, called the simplifier. This is what we will be learning about today. *) lemma "\ x::nat. (x div 2) * 2 = 0 * x" apply(rule_tac x=0 in exI) apply(simp only: div_0 mult_0) done (* REMINDER: automated tactics (like the simp and blast etc.) work best when they don't have to instantiate schematic variables, since automation often fails when the automated tactics cannot find the right instantiations. You should instantiate schematic variables in the rules that introduce them before applying those rules. *) lemma "\ x::nat. (x div 2) * 2 = 0 * x" apply(rule exI) apply(simp only: div_0 mult_0) oops end