Theory BoolExp

Up to index of Isabelle/HOL/IsarTut

theory BoolExp = Main:
theory BoolExp = Main:

text {* Tracing the development beginning in section 2.4.5.

Proving the trivial lemma about cases over lists is actually
very tricky in Isar.  Let's see why.

Note that I've rewritten the final term of the case
expression slightly, just to make it slightly less trivial (at
least formally). *}

lemma "(case xs of [] => [] | y#ys => y#ys) = xs" (is "?P xs")
proof (cases xs)
-- {* So far, so good, but if you now ask it to show ?P [] it
gives a warning (in the minibuffer, the last line of the window)
and the proof won't go through.  Here's what you have to say: *}
   assume "xs=[]" from prems show ?thesis by simp
next
   fix a list assume "xs=a#list" from prems show ?thesis by simp
qed

text {* This looks like a massive step backwards from the Isabelle
style proofs presented in the tutorial, but the tables will be turned
when the theorems get deeper.  I hope.  

Here comes the boolexp stuff. *}

datatype boolex = Const bool | Var nat | Neg boolex
                | And boolex boolex

consts value:: "boolex => (nat => bool) => bool"
primrec
"value (Const b) env = b"
"value (Var x) env = env x"
"value (Neg b) env = (~value b env)"
"value (And b c) env = (value b env & value c env)"

datatype ifex = CIF bool | VIF nat | IF ifex ifex ifex
consts valif:: "ifex => (nat => bool) => bool"
primrec
"valif (CIF b) env = b"
"valif (VIF x) env = env x"
"valif (IF b t e) env = (if valif b env then valif t env else valif e env)"

consts bool2if:: "boolex => ifex"
primrec
"bool2if (Const b) = CIF b"
"bool2if (Var x) = VIF x"
"bool2if (Neg b) = IF (bool2if b) (CIF False) (CIF True)"
"bool2if (And b c) = IF (bool2if b) (bool2if c) (CIF False)"

lemma "valif (bool2if b) env = value b env" (is "?P b")
proof (induct b)
  fix v show "?P (Const v)" by simp
next
  fix x show "?P (Var x)" by simp
next
  fix b assume "?P b" from prems show "?P (Neg b)" by simp
next
  fix b c assume "?P b" "?P c"
  from prems show "?P (And b c)" by simp
qed

consts normif:: "ifex => ifex => ifex => ifex"
       norm::   "ifex => ifex"
       normal:: "ifex => bool"

primrec
"normif (CIF b)   t e  = IF (CIF b) t e"
"normif (VIF x)   t e  = IF (VIF x) t e"
normif_rdef:
"normif (IF b t e) u f = normif b (normif t u f) (normif e u f)"

primrec
"norm (CIF b) = CIF b"
"norm (VIF x) = VIF x"
"norm (IF b t e) = normif b (norm t) (norm e)"

lemma [simp]: "!t e. valif (normif b t e) env = 
                           valif (IF b t e) env" (is "?P b")
proof (induct b)
   fix v show "?P (CIF v)" by simp
next
   fix x show "?P (VIF x)" by simp
next
   fix x y z assume "?P x" "?P y" "?P z"
   from prems show "?P (IF x y z)" by simp
qed

text {* That looks simple, but it took a real
struggle to get it right.  If you mess up anything
in the last stanza it fails, leading you into a tangled
and very messy subproof.  In particular, using a symbol
for IF x y z like we did for a\#list in the trivial list
cases lemma fails.  Why????? *}

theorem "valif (norm b) env = valif b env" (is "?P b")
proof (induct b)
  fix v show "?P (CIF v)" by simp
next
  fix x show "?P (VIF x)" by simp
next
  fix b t e assume "?P b" "?P t" "?P e"
  from prems show "?P (IF b t e)" by simp
qed

primrec
"normal (CIF b) = True"
"normal (VIF x) = True"
"normal (IF b t e) = (normal t & normal e &
    (case b of CIF b => True | VIF x => True | IF x y z => False))"

lemma [simp]: "!t e. normal(normif b t e) = (normal t & normal e)" (is "?P b")
proof (induct b)
   fix v show "?P (CIF v)" by simp
next
   fix x show "?P (VIF x)" by simp
next
   fix x y z assume "?P x" "?P y" "?P z"
   from prems show "?P (IF x y z)" by simp
qed

theorem "normal (norm b)" (is "?P b")
proof (induct b)
   fix v show "?P (CIF v)" by simp
next
   fix x show "?P (VIF x)" by simp
next
   fix x y z assume "?P x" "?P y" "?P z"
   from prems show "?P (IF x y z)" by simp
qed

text {* Now that I'm getting the hang of  it this
isn't so bad.  The time I spent with Isabelle 
proof scripts is getting in the way: you have
to think very formally about quantification in Isar,
and with the ProofGeneral front end you can't always
see why an obvious statement isn't working out.
Watch the minibuffer for the warning that what
you are trying to prove does not satisfy a goal.
The warning happens when you say ``show'', but
you don't get an error until later. 

Something similar happens in the development of
a calculation sequence: the ``also'' command applies
transitivity rules to what you ``have'' so far.  If
those rules can't deduce any new facts, the ``also''
fails!  When that happens, say ``moreover'' instead;
that will just append your new fact without trying
to reason about it.

On to the exercise, strengthening the definition
of normal.  The modified predicate test function
simply changes the result for CIF in the case.  *}

consts normyl:: "ifex => bool"
primrec
"normyl (CIF b) = True"
"normyl (VIF x) = True"
"normyl (IF b t e) = (normyl t & normyl e &
    (case b of CIF b => False | VIF x => True | IF x y z => False))"

text {* As a preliminary step, let's prove that normyl is stronger
than normal. For that, we need a lemma to help pierce the case
structure embedded in the definition.  *}

lemma normx: "!y z. normyl (IF x y z) --> (normyl x & normyl y & normyl z)"
                      (is "?P x")
proof (cases x)
   fix v assume "x = CIF v" from prems show "?P x" by simp
next
   fix n assume "x = VIF n" from prems show "?P x" by simp
next
   fix b t e assume "x = IF b t e"
   from prems show "?P x" by simp
qed

text {* I've figured something out. The induct and cases 
methods build very different goals!  Isabelle has a lot
of metatheorems that will restructure the goals willy-nilly
so you don't notice.  In Isar, it matters.  Set up a simple
goal (doesn't have to be true) and look at the first
subgoal generated by each method.  Cases leaves your
predicate intact but inserts a symbol binding into the
premises, while induct rewrites
the predicate and leaves the premesis alone.  Wild. 

This is important since proving an implication should
be as easy as ``assume premis, show conclusion'' but
depending on how the predicate has been decorated it
may not like it.  I am not happy with the higher level
unification that is (not) happening in Isar.  

A direct consequence of the cases/induct issue is that
if you begin a proof using cases and decide to change
to induction you probably will have to modify your
proof of the base case, even though it is logically
identical to the first cases case.  Harumph.

I am not going to try to prove strictly stronger,
since the management of an existence proof is beyond
what I want to tackle right now.  Onward, then: *}

theorem "normyl x --> normal x" (is "?P x")
proof (induct x)
  fix v show "?P (CIF v)" by simp
next
  fix n show "?P (VIF n)" by simp
next
  fix p q r assume "?P p" "?P q" "?P r"
  show "?P (IF p q r)" (is "?Q p")
  proof (cases p)
    fix v assume "p = CIF v" from prems show "?Q p" by simp
  next
    fix n assume "p = VIF n" from prems show "?Q p" by simp
  next
    fix a b c assume "p = IF a b c" from prems show "?Q p" by simp
  qed
qed

text {* Well, we didn't need the lemma after all.  This last
proof nicely illustrates the assymetry between cases and induct. 

As an aside, everything from ``proof (cases p)'' down
can be replaced with 
``by (cases p, simp\_all add: prems) qed''.  That is starting
to look a lot more like an Isabelle proof.  

Now to normylize an expression. *}

consts normyf:: "ifex => ifex => ifex => ifex"
       normy::  "ifex => ifex"

text {* The key to the exercise, of course, is
to simulate the effect of IF on constants: *}

primrec
"normyf (CIF b)   t e  = (if b then t else e)"
"normyf (VIF x)   t e  = IF (VIF x) t e"
normyf_rdef:
"normyf (IF b t e) u f = normyf b (normyf t u f) (normyf e u f)"

primrec
"normy (CIF v) = CIF v"
"normy (VIF x) = VIF x"
"normy (IF b t e) = normyf b (normy t) (normy e)"

text {* A note about incremental proof development:
the proofs shown work, you aren't seeing the many,
many proofs that don't work.

If you try to say ``from prems show foo by simp,'' say,
and it doesn't work, you have to replace the ``by simp''
clause with a proof block.  To get it to accept the keyword
proof, you also must remove the ``from prems'' clause!!! *}

lemma [simp]: "!t e. valif (normyf b t e) env = 
                           valif (IF b t e) env" (is "?P b")
proof (induct b)
  fix v show "?P (CIF v)" by simp
next
  fix x show "?P (VIF x)" by simp
next
  fix x y z assume "?P x" "?P y" "?P z"
  from prems show "?P (IF x y z)" by simp
qed

theorem "valif (normy x) env = valif x env" (is "?P x")
proof (induct x)
  fix v show "?P (CIF v)" by simp
next
  fix n show "?P (VIF n)" by simp
next
  fix b t e assume "?P b" "?P t" "?P e"
  show "?P (IF b t e)" (is "?Q b")
-- {* None of the single-step automatic methods
seem to work here.  Applying simp experimentally
shows that it is splitting the equality relation
on truth-valued expressions into a pair of implications.
That's overkill, since we want a purely formal (i.e. syntactic)
proof.  Apparently we need to guide it: *}
     proof (cases b)
        fix v assume "b = CIF v" from prems show "?Q b" by simp
     next
        fix n assume "b = VIF n" from prems show "?Q b" by simp
     next
        fix x y z assume "b = IF x y z"
        from prems show "?Q b" by simp
  qed
qed

end

lemma

  list_case [] op # xs = xs

lemma

  valif (bool2if b) env = value b env

lemma

  ALL t e. valif (normif b t e) env = valif (IF b t e) env

theorem

  valif (norm b) env = valif b env

lemma

  ALL t e. normal (normif b t e) = (normal t & normal e)

theorem

  normal (norm b)

lemma normx:

  ALL y z. normyl (IF x y z) --> normyl x & normyl y & normyl z

theorem

  normyl x --> normal x

lemma

  ALL t e. valif (normyf b t e) env = valif (IF b t e) env

theorem

  valif (normy x) env = valif x env