# [isabelle] rule induction question

```Hi all,

```
I've been using the book Concrete Semantics (http://www21.in.tum.de/~nipkow/Concrete-Semantics/) as a tutorial.
```
Currently, I'm trying to prove the following.
"⟦(WHILE b DO c,s)⇒t⟧⟹(WHILE b DO (c;;IF b THEN c ELSE SKIP),s)⇒t"

```
In other words, I want to prove that I can unroll the loop and end up in the same final state.
```
```
At some point in the proof, I'm in a "subtree" (also another WHILE loop) of the original WHILE b DO c. I want to be able to apply the induction hypothesis and get an unrolled loop for that subtree.
```
```
I looked at some examples of rule induction on the web and in the Programming and Proving book. I tried structuring the proofs that way and also used cases, but am still stuck.
```
```
The version of the theory that I'm sending here uses "proof -". It helps me being explicit what I'm trying to do since I'm new to Isabelle.
```
```
I've laid out the whole proof and skipped the parts where I needed the induction hypothesis with "sorry".
```
Would anybody mind taking a look, please?

```
The code is below. I've marked the places that I need help with "(* NEED INDUCTION HYPOTHESIS *)".
```
Thank you,
Amarin

========================
Semantics.thy
========================
theory Semantics imports Main begin

type_synonym vname = string
type_synonym val = int
type_synonym state = "vname ⇒ val"

datatype aexp = N int | V vname
fun aval :: "aexp ⇒ state ⇒ val" where
"aval (N n) s = n" |
"aval (V x) s = s x"

datatype bexp = Bc bool
fun bval :: "bexp ⇒ state ⇒ bool" where
"bval (Bc v) s = v"

datatype
com = SKIP
| Assign vname aexp       ("_ ::= _" [1000, 61] 61)
| Seq    com  com         ("_;;/ _"  [60, 61] 60)
| If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
| While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)

inductive
big_step :: "com × state ⇒ state ⇒ bool" (infix "⇒" 55)
where
Skip: "(SKIP,s) ⇒ s" |
Assign: "(x ::= a,s) ⇒ s(x := aval a s)" |
Seq: "⟦ (c1,s1) ⇒ s2;  (c2,s2) ⇒ s3 ⟧ ⟹ (c1;;c2, s1) ⇒ s3" |
IfTrue: "⟦ bval b s;  (c1,s) ⇒ t ⟧ ⟹ (IF b THEN c1 ELSE c2, s) ⇒ t" |
IfFalse: "⟦ ¬bval b s;  (c2,s) ⇒ t ⟧ ⟹ (IF b THEN c1 ELSE c2, s) ⇒ t" |
WhileFalse: "⟦¬bval b s⟧ ⟹ (WHILE b DO c,s) ⇒ s" |
WhileTrue: "⟦ bval b s1;  (c,s1) ⇒ s2;  (WHILE b DO c,s2) ⇒ s3 ⟧
⟹ (WHILE b DO c, s1) ⇒ s3"

declare big_step.intros [intro]
lemmas big_step_induct = big_step.induct[split_format(complete)]
inductive_cases SkipE[elim!]: "(SKIP,s) ⇒ t"
inductive_cases AssignE[elim!]: "(x ::= a,s) ⇒ t"
inductive_cases SeqE[elim!]: "(c1;;c2,s1) ⇒ s3"
inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) ⇒ t"
inductive_cases WhileE[elim]: "(WHILE b DO c,s) ⇒ t"

theorem big_step_determ: "⟦ (c,s) ⇒ t; (c,s) ⇒ u ⟧ ⟹ u = t"
by (induction arbitrary: u as3 rule: big_step_induct) blast+

lemma unroll_while:
"⟦(WHILE b DO c,s)⇒t⟧⟹(WHILE b DO (c;;IF b THEN c ELSE SKIP),s)⇒t"
proof -
fix b s c t
assume assms: "(WHILE b DO c,s)⇒t"
let ?thesis = "(WHILE b DO (c;;IF b THEN c ELSE SKIP),s)⇒t"
{
assume true1: "bval b s"
```
obtain i where i1:"(c,s)⇒i" and i2:"(WHILE b DO c,i)⇒t" using assms true1 by auto
```    {
assume true2: "bval b i"
```
obtain i' where i3:"(c,i)⇒i'" and i4:"(WHILE b DO c,i')⇒t" using i2 true2 by auto have body:"(c;;IF b THEN c ELSE SKIP,s) ⇒ i'" using i1 i3 true2 by auto
```      have loop:"(WHILE b DO (c;;IF b THEN c ELSE SKIP),i') ⇒ t" using i4
sorry (* NEED INDUCTION HYPOTHESIS *)
have ?thesis using body loop true1 by auto
} moreover
{
assume false2: "¬bval b i"
have body:"(c;;IF b THEN c ELSE SKIP,s) ⇒ i" using i1 false2 by auto
have loop:"(WHILE b DO (c;;IF b THEN c ELSE SKIP),i) ⇒ t" using i2
sorry (* NEED INDUCTION HYPOTHESIS *)
have ?thesis using body loop true1 by auto
}
ultimately have "(WHILE b DO (c;;IF b THEN c ELSE SKIP),s)⇒t" by metis
} moreover {
assume false1: "¬bval b s"
have final1:"(WHILE b DO c,s)⇒s" using false1 by auto
```
have final2:"(WHILE b DO (c;;IF b THEN c ELSE SKIP),s)⇒s" using false1 by auto
```    have eq:"s=t" using assms final1 big_step_determ by auto
have ?thesis using final2 eq by auto
} ultimately show ?thesis by metis
qed

end

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.