Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

# Homework 05.2

This is the task corresponding to the second part of homework 5.

## Resources

### Definitions File

```theory Defs
imports "HOL-IMP.BExp" "HOL-IMP.Star"
begin

text‹\clearpage›
text ‹\NumHomework{Nondeterminism}{Nov 25}›

datatype
com = SKIP
| Assign vname aexp       ("_ ::= _" [1000, 61] 61)
| Semi   com  com         ("_;;/ _"  [60, 61] 60)
| If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
| While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)
| Or com com              ("_ OR _" [57,58] 59)
| ASSUME bexp

inductive
big_step :: "com × state ⇒ state ⇒ bool" (infix "⇒" 55)
where
Skip:    "(SKIP,s) ⇒ s" |
Assign:  "(x ::= a,s) ⇒ s(x := aval a s)" |
Seq:    "⟦ (c⇩1,s⇩1) ⇒ s⇩2; (c⇩2,s⇩2) ⇒ s⇩3 ⟧ ⟹ (c⇩1;;c⇩2, s⇩1) ⇒ s⇩3" |

IfTrue:  "⟦ bval b s;  (c⇩1,s) ⇒ t ⟧ ⟹ (IF b THEN c⇩1 ELSE c⇩2, s) ⇒ t" |
IfFalse: "⟦ ¬bval b s;  (c⇩2,s) ⇒ t ⟧ ⟹ (IF b THEN c⇩1 ELSE c⇩2, s) ⇒ t" |

WhileFalse: "¬bval b s ⟹ (WHILE b DO c,s) ⇒ s" |
WhileTrue:  "⟦ bval b s⇩1;  (c,s⇩1) ⇒ s⇩2;  (WHILE b DO c, s⇩2) ⇒ s⇩3 ⟧ ⟹ (WHILE b DO c, s⇩1) ⇒ s⇩3" |
OrLeft: "⟦ (c⇩1,s) ⇒ s' ⟧ ⟹ (c⇩1 OR c⇩2,s) ⇒ s'" |
OrRight: "⟦ (c⇩2,s) ⇒ s' ⟧ ⟹ (c⇩1 OR c⇩2,s) ⇒ s'" |
Assume: "bval b s ⟹ (ASSUME b, s) ⇒ s"

declare big_step.intros [intro]

lemmas big_step_induct = big_step.induct[split_format(complete)]

inductive_cases skipE[elim!]: "(SKIP,s) ⇒ t"
thm skipE
inductive_cases AssignE[elim!]: "(x ::= a,s) ⇒ t"
thm AssignE
inductive_cases SeqE[elim!]: "(c1;;c2,s1) ⇒ s3"
thm SeqE
inductive_cases OrE: "(c1 OR c2,s1) ⇒ s3"
thm OrE
inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) ⇒ t"
thm IfE
inductive_cases WhileE[elim]: "(WHILE b DO c,s) ⇒ t"
thm WhileE

end```

### Template File

```theory Submission
imports Defs
begin

inductive
small_step :: "com * state ⇒ com * state ⇒ bool" (infix "→" 55)
where
Assign:  "(x ::= a, s) → (SKIP, s(x := aval a s))" |
Seq1:   "(SKIP;;c⇩2,s) → (c⇩2,s)" |
Seq2:   "(c⇩1,s) → (c⇩1',s') ⟹ (c⇩1;;c⇩2,s) → (c⇩1';;c⇩2,s')" |
IfTrue:  "bval b s ⟹ (IF b THEN c⇩1 ELSE c⇩2,s) → (c⇩1,s)" |
IfFalse: "¬bval b s ⟹ (IF b THEN c⇩1 ELSE c⇩2,s) → (c⇩2,s)" |
While:   "(WHILE b DO c,s) → (IF b THEN c;; WHILE b DO c ELSE SKIP,s)"

abbreviation small_steps :: "com * state ⇒ com * state ⇒ bool" (infix "→*" 55)
where "x →* y == star small_step x y"

lemmas small_step_induct = small_step.induct[split_format(complete)]

declare small_step.intros[simp,intro]

inductive_cases SkipE'[elim!]: "(SKIP,s) → ct"
thm SkipE'
inductive_cases AssignE'[elim!]: "(x::=a,s) → ct"
thm AssignE'
inductive_cases SeqE'[elim]: "(c1;;c2,s) → ct"
thm SeqE'
inductive_cases OrE'[elim]: "(c1 OR c2,s) → ct"
thm OrE'
inductive_cases AssumeE'[elim!]: "(ASSUME b,s) → ct"
thm AssumeE'
inductive_cases IfE'[elim!]: "(IF b THEN c1 ELSE c2,s) → ct"
thm IfE'
inductive_cases WhileE'[elim]: "(WHILE b DO c, s) → ct"
thm WhileE'

text ‹Prove this theorem. Use the theory ‹HOL-IMP.Small_Step› as a template for the proof.›
theorem big_iff_small:
"cs ⇒ t ⟷ cs →* (SKIP,t)"
sorry

definition final where "final cs ⟷ ¬(EX cs'. cs → cs')"

text ‹Does this hold?›
lemma big_iff_small_termination:
"(∃t. cs ⇒ t) ⟷ (∃cs'. cs →* cs' ∧ final cs')"
oops

end```

### Check File

```theory Check
imports Submission
begin

theorem big_iff_small:
"cs ⇒ t ⟷ cs →* (SKIP,t)"
by (rule Submission.big_iff_small)

end```

Terms and Conditions