Up to index of Isabelle/HOL/IsarTut

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