Theory Simplification

Up to index of Isabelle/HOL/IsarTut

theory Simplification = Main:
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

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

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

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

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! *}




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


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


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


  xor AA)


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

lemma hd_Cons_tl:

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


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


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