Up to index of Isabelle/HOL/IsarTut

theory Recursion = Main: text {* Beginning with section 3.4.1 *} datatype 'a aexp = IF "'a bexp" "'a aexp" "'a aexp" | Sum "'a aexp" "'a aexp" | Diff "'a aexp" "'a aexp" | Var 'a | Num nat and 'a bexp = Less "'a aexp" "'a aexp" | And "'a bexp" "'a bexp" | Neg "'a bexp" consts evala:: "'a aexp => ('a => nat) => nat" evalb:: "'a bexp => ('a => nat) => bool" primrec "evala (IF b a1 a2) env = (if evalb b env then evala a1 env else evala a2 env)" "evala (Sum a1 a2) env = evala a1 env + evala a2 env" "evala (Diff a1 a2) env = evala a1 env - evala a2 env" "evala (Var a) env = env a" "evala (Num n) env = n" "evalb (Less a1 a2) env = (evala a1 env < evala a2 env)" "evalb (And b1 b2) env = (evalb b1 env & evalb b2 env)" "evalb (Neg b) env = (~ evalb b env)" consts substa:: "('a => 'b aexp) => 'a aexp => 'b aexp" substb:: "('a => 'b aexp) => 'a bexp => 'b bexp" text {* Perhaps there are too many a's and b's running around here. *} primrec "substa s (IF b a1 a2) = IF (substb s b) (substa s a1) (substa s a2)" "substa s (Sum a1 a2) = Sum (substa s a1) (substa s a2)" "substa s (Diff a1 a2) = Diff (substa s a1) (substa s a2)" "substa s (Var a) = s a" "substa s (Num n) = Num n" "substb s (Less a1 a2) = Less (substa s a1) (substa s a2)" "substb s (And b1 b2) = And (substb s b1) (substb s b2)" "substb s (Neg b) = Neg (substb s b)" theorem "evala (substa s a) env = evala a (%x. evala (s x) env) & evalb (substb s b) env = evalb b (%x. evala (s x) env)" (is "?P a b") by (induct a and b, auto) text {* A one-line proof for a two-line theorem! Since there is nothing but structural recursion going on in substitution it is nice that theorems about it can be proved by pure structural induction without a lot of rigamarole. The conditional constructs in the operationally defined functions are what make proofs about evaluation hard(er). *} text {* Exercise 3.4.1, normalizing binary expressions *} consts normala:: "'a aexp => bool" normalb:: "'a bexp => bool" primrec "normala (IF b a1 a2) = (normalb b & normala a1 & normala a2)" "normala (Sum a1 a2) = (normala a1 & normala a2)" "normala (Diff a1 a2) = (normala a1 & normala a2)" "normala (Var a) = True" "normala (Num n) = True" "normalb (Less a1 a2) = (normala a1 & normala a2)" "normalb (And b1 b2) = False" "normalb (Neg b) = False" text {* Remark -- it would be interesting to take this farther by defining "canonical" as having all the IFs confined to the outermost layer of the construct, so that all interior arithmetic expressions are IF-free. *} consts norma:: "'a aexp => 'a aexp" normif:: "'a bexp => 'a aexp => 'a aexp => 'a aexp" primrec "norma (IF b a1 a2) = normif b (norma a1) (norma a2)" "norma (Sum a1 a2) = Sum (norma a1) (norma a2)" "norma (Diff a1 a2) = Diff (norma a1) (norma a2)" "norma (Var a) = Var a" "norma (Num n) = Num n" "normif (Less a1 a2) t e = IF (Less (norma a1) (norma a2)) t e" "normif (And b1 b2) t e = normif b1 (normif b2 t e) e" "normif (Neg b) t e = normif b e t" theorem "normala (norma (a::'a aexp)) & (!t e. normala (normif (b::'a bexp) t e) = (normala t & normala e))" by (induct a and b, auto) text {* OK, I think I see what was happening. I'd make a mistake in the theory or the theorem statement, then when a ``by'' proof attempt failed I'd try to expand it. Eventually I'd get down to a subgoal that I could see was broken and I'd go fix the theory. Then the expanded proof would go through, but I didn't know how to formulate the one-line incantation and get rid of all the intermediate stuff. I will keep going, since I have not yet reached the point where I gave up on Isabelle scripts. *} text {* Section 3.4.2, Nested Recursion. *} datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f) term list" consts subst :: "('a => ('b,'f)term) => ('a,'f)term => ('b,'f)term" substs:: "('a => ('b,'f)term) => ('a,'f)term list => ('b,'f)term list" primrec "subst s (Var x) = s x" subst_App: "subst s (App f ts) = App f (substs s ts)" "substs s [] = []" "substs s (t#ts) = subst s t # substs s ts" lemma "subst Var t = (t ::('v,'f)term) & substs Var ts = (ts ::('v,'f)term list)" by (induct_tac t and ts, auto) text {* Hmmm.... induct\_tac works but induct does not! Something about the types having incompatible induction rules. Let's see if we can prove it without resorting to the tactic. Or at least see what it is doing. How do I get this thing to show me the rules it is trying to use? *} lemma "subst Var t = (t::('v,'f)term) & substs Var ts = (ts::('v,'f)term list)" (is "?P t & ?Q ts" is "?R t ts") proof (induct_tac t and ts) fix v show "?P (Var v)" by simp next show "?Q []" by simp next fix f ts assume "?Q ts" show "?P (App f ts)" by simp next fix t ts assume "?P t" "?Q ts" from prems show "?Q (t#ts)" by simp qed text {* OK, I had to go home, read ahead in the tutorial, and sleep, but I got it done (using @{text induct_tac}.) Isar is extremely picky about what you try to assume. For example, if you try to assume @{text "?R t ts"} in the last step, the show does not go on!. *} text {* Note for introductory remarks: A proposition containing @{text "==>"} is a claim that the right-hand-side can be proved from the left hand side. A proposition based on @{text "-->"} on the other hand is a \emph{predicate} and you are claiming that in all cases (in the quantification context) the predicate evaluates to @{term True}. In Isabelle implications are pretty much automatically elevated to meta-implications but in Isar you should try to say what you mean in the first place. *} text {* Second note: some not-so-old proverbs, part one: Isabelle proofs are unreadable. Isar proofs are unwritable. You can have anything you want but you can only show a pending goal at Isar's Restaurant. You can't even show a pending goal if you've assumed something or fixed something that Isar doesn't like or failed to fix something that Isar does like. How do you know it didn't like your assumption? The show gives a warning. Then when you finish proving the claim you get a really cryptic error message and apparent progress stops. More meta-musings: You use @{text rule} to \emph{undo} the effect of a rule. This is because we're fundamentally working backwards. The fundamental rule for proof by contradiction is called @{text classical}. The classical reasoner is called @{text clarify} if you don't want it to simplify. If you do it's called @{text clarsimp}. So far so good, but if you want to allow goal splitting they are called @{text safe} and @{text auto}, respectively. The rules for contrapositives don't rewrite an implication in your goal -- they re-arrange the list of hypotheses, swapping one of them for the goal. To turn an implication into the equivalent disjunction or its contrapositive you need another rule, the name of which escapes me at the moment. But it is a safe bet you'd never guess it correctly in less than three tries! A rule, by the way, is nothing more than a proved proposition involving schematic variables and where the outermost operator is meta-implication. Applying a rule forwards means that if you can match up the left-hand-side of the rule with stuff in the left-hand-side of your goal then you can add the right-hand- side of the rule to the left-hand side of your goal. Got that? Good. Applying a rule \emph{backwards} means that if the right-hand-side of your goal can be matched with the right-hand-side of the rule, the right-hand-side of your goal is \emph{replaced} by the left-hand-side of the rule. There is some hocus-pocus having to do with matching up pieces on the left too, but the take-home from that is if you don't like what @{text rule} does, try @{text frule}. But wait, there's more! If the rule you're trying to use backwards is one that, if applied frontwards, would introduce a symbol that already appears in your goal you can use @{text rule}. If on the other hand you want to convert your goal to one that uses a particular symbol, you use the \emph{elimination} rule for that symbol with @{text erule}. There, piece of cake. I don't understand why people are intimidated by this stuff. Fundamentally, the objective in either Isabelle or Isar is to eliminate goals. A goal is eliminated most basically by the @{text assumption} method, which works only if the right-hand-side appears among the terms on the left-hand-side verbatim. Since matching a theorem against your goal allows you to insert the RHS into the LHS, @{text "by rule thm_foo"} is the next-most-fundamental way of eliminating a goal. All @{text by} does is run the given method, try to eliminate all pending (sub)goals by @{text assumption}, and fail if the goals don't go away. Once the list of goals is empty you get to say @{text qed} in Isar or @{text done} in Isabelle, except that @{text by} says that for you. *} text {* Now Exercise 3.4.2 The goal is to show that substitustion and a certain kind of composition commute. The first challenge is to cleanly model the composition. Since @{text "g a"} is an expression it can't be an argument to @{term f}. On the other hand, we don't want the supposed composition to be trivially equivalent to nested substitution. Let's try this: *} constdefs subcomp:: "('b => ('v,'f) term) => ('a => ('b,'f) term) => ('a => ('v,'f) term)" "subcomp f g == (%a. subst f (g a))" theorem "subst (subcomp f g) (t ::('a,'f)term) = ( subst f ( subst g t)) & substs (subcomp f g) (ts::('a,'f)term list)=(substs f (substs g ts))" (is "?P t & ?Q ts") by (simp add: subcomp_def, induct_tac t and ts, auto) text {* OK, so that's a three-line Isabelle proof collapsed into a one-line Isar proof in an unsubtle manner. Sue me, once you've fixed @{text induct} so it works here. Exercise 3.4.3 As the tutorial suggests, it is very hard to get it to accept a functional definition directly. Let's just do it the easy way: *} consts trev:: "('v,'f)term => ('v,'f)term" trevs:: "('v,'f)term list => ('v,'f)term list" primrec "trev (Var v) = Var v" "trev (App f ts) = App f (trevs ts)" "trevs [] = []" "trevs (t#ts) = (trevs ts)@[trev t]" lemma trevs_map: "trevs ts = map trev (rev ts)" by (induct ts, auto) theorem "trev (trev t) = (t::('v,'f)term) & trevs (trevs ts) = (ts::('v,'f)term list)" (is "?P t & ?Q ts") by (induct_tac t and ts, auto simp: trevs_map) text {* Is it obvious yet that I've been reading ahead into chapter four? *} datatype ('a,'i)bigtree = Tip | Br 'a "'i => ('a,'i)bigtree" consts map_bt:: "('a => 'b) => ('a,'i)bigtree => ('b,'i)bigtree" primrec "map_bt f Tip = Tip" map_bt_rdef: "map_bt f (Br a F) = Br (f a) (%i. map_bt f (F i))" lemma "map_bt (g o f) T = map_bt g (map_bt f T)" (is "?P T") proof (induct T) -- {* At last, a case where @{text induct} works! *} show "?P Tip" by simp next fix a fun show "?P (Br a fun)" apply (simp add: o_def) apply (intro) -- {* I want @{text lambdaI} here, but that's not the right name. Fortunately, @{text intro} alone does what I want. *} apply (cases "fun i") oops text {* Well, that was fun. That theorm is provable in one step. What magic incantation is missing from the more explicit text? The world may never know ... *} lemma "map_bt (g o f) T = map_bt g (map_bt f T)" by (induct T, auto) end

**theorem**

evala (substa s a) env = evala a (%x. evala (s x) env) & evalb (substb s b) env = evalb b (%x. evala (s x) env)

**theorem**

normala (norma a) & (ALL t e. normala (normif b t e) = (normala t & normala e))

**lemma**

subst term.Var t = t & substs term.Var ts = ts

**lemma**

subst term.Var t = t & substs term.Var ts = ts

**theorem**

subst (subcomp f g) t = subst f (subst g t) & substs (subcomp f g) ts = substs f (substs g ts)

**lemma** *trevs_map:*

trevs ts = map trev (rev ts)

**theorem**

trev (trev t) = t & trevs (trevs ts) = ts

**lemma**

map_bt (g o f) T = map_bt g (map_bt f T)