Up to index of Isabelle/HOL/IsarTut

theory Simplification = Main: text {* Beginning chapter 3. Simplification in Isar is a different breed of cat from that in Isabelle. In Isabelle you can try to simplify a goal, see what redults, and then either work on the result or retract the simplification. In Isar, a (sub) goal must be stated more or less explicitly and then simplification either proves it or it doesn't. If it doesn't, you have a problem. *} lemma "[| xs @ zs = ys @ xs; [] @ xs = [] @ [] |] ==> ys = zs" by simp lemma "!x. f x = g (f (g x)) ==> f [] = f [] @ []" by (simp (no_asm)) text {* Let's see how to do that one stepwise. *} lemma "!x. f x = g (f (g x)) ==> f [] = f [] @ []" proof - show ?thesis by simp qed text {* Just introducing the proof block does not change the goal state in any way. Saying ``show ?thesis'', however, strips away all the assumptions (everything to the left of the meta-implication) leaving a goal that does not lead the simplifier into a rabbit hole. This example reveals something important about the semantics of the Isar proof language. If a statement appears in the premises of a goal you can move it to the ``prems'' theorem register using ``assume''. You can then strip it out of the local goal state by entering a ``show'' or ``have'' context and recover it when needed by mentioning ``prems'' appropriately. I hate to say it, but this is starting to make sense. *} constdefs xor:: "bool => bool => bool" "xor A B == (A & ~B) | (~A & B)" lemma "xor A (~A)" by (simp add: xor_def) text {* Try opening the proof above by saying ``proof (simp only: xor\_def).'' To finish from there you would have to utter a ``show'' clause that reiterates the ``simplified'' goal, a real pain in the tush. Isar really wants you to reason forwards. On the other hand: *} lemma "(let xs = [] in xs@ys@xs) = ys" proof (simp only: Let_def) show "[] @ ys @ [] = ys" by simp qed text {* That was pretty painless. Of course it could have been done as a one-liner. *} lemma hd_Cons_tl [simp]: "xs ~= [] ==> hd xs # tl xs = xs" by (cases xs, simp, simp) lemma "xs ~= [] ==> hd(rev xs)#tl(rev xs) = rev xs" by simp text {* Aside: you can get a lot of practice with the subgoal proof stuff by misspelling a couple of words in your theorem statement. The following lemma is solved in one step by simp, but let's break it down anyway. Without the ``intro'' method you get a single goal that is a conjunction of implications, a real booger to work with! *} lemma "!xs. if xs = [] then rev xs = [] else rev xs ~= []" proof (split split_if, intro) fix xs assume "xs = []" from prems show "xs = []" by simp next --{* Now this is interesting! It wants us to show False, which is how it says we need to show that the premises are mutually contradictory. Hmmmmm... Getting the right combination of incantations for this one is tricky! *} fix xs assume "xs ~= []" "rev xs = []" from prems show False by simp qed text {* To keep the unification happy you have to assume all the premises you need verbatim, then hack around on them in the subgoal. No shortcuts allowed by assuming something ``obviously'' equivalent but in a more convenient form! I have a feeling I'm missing something really important, and it probably has something to do with the ``rule'' method. I'm skipping the little section on arithmetic. ProofGeneral users can turn on tracing (as well as most of the other uses of the ``ML'' directive) from the menu. Try the example with simplification tracing (in ``Isabelle/Isar$\rightarrow$Settings'') turned on: *} lemma "rev [a] = []" proof simp oops text {* After the simp step you would expect to see a trace. Where is it? You have to go to the ``Buffers'' menu and pick the ``isabelle/isar'' buffer to see it. The ``oops'' gets us out of dodge so that the theory document can continue. Be sure to turn tracing back off, it really slows things down! *} end

**lemma**

[| xs @ zs = ys @ xs; [] @ xs = [] @ [] |] ==> ys = zs

**lemma**

ALL x. f x = g (f (g x)) ==> f [] = f [] @ []

**lemma**

ALL x. f x = g (f (g x)) ==> f [] = f [] @ []

**lemma**

xor A (¬ A)

**lemma**

(let xs = [] in xs @ ys @ xs) = ys

**lemma** *hd_Cons_tl:*

xs ~= [] ==> hd xs # tl xs = xs

**lemma**

xs ~= [] ==> hd (rev xs) # tl (rev xs) = rev xs

**lemma**

ALL xs. if xs = [] then rev xs = [] else rev xs ~= []