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 08.2

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

## Resources

### Definitions File

```theory Defs
imports "HOL-IMP.Com"
begin

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)
| Or com com              ("_ OR _" [57,58] 59)
| ASSUME bexp
| Loop com                ("(LOOP _)"   61)

end```

### Template File

```theory Submission
imports Defs
begin

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

type_synonym com_den = "(state × state) set"

definition W :: "(state ⇒ bool) ⇒ com_den ⇒ (com_den ⇒ com_den)" where
"W db dc = (λdw. {(s,t). if db s then (s,t) ∈ dc O dw else s=t})"

fun D :: "com ⇒ com_den" where
"D SKIP   = Id" |
"D (x ::= a) = {(s,t). t = s(x := aval a s)}" |
"D (c1;;c2)  = D(c1) O D(c2)" |
"D (IF b THEN c1 ELSE c2)
= {(s,t). if bval b s then (s,t) ∈ D c1 else (s,t) ∈ D c2}" |
"D (WHILE b DO c) = lfp (W (bval b) (D c))"

lemma W_mono: "mono (W b r)"
by (unfold W_def mono_def) auto

lemma D_While_If:
"D(WHILE b DO c) = D(IF b THEN c;;WHILE b DO c ELSE SKIP)"
proof-
let ?w = "WHILE b DO c" let ?f = "W (bval b) (D c)"
have "D ?w = lfp ?f" by simp
also have "… = ?f (lfp ?f)" by(rule lfp_unfold [OF W_mono])
also have "… = D(IF b THEN c;;?w ELSE SKIP)" by (simp add: W_def)
finally show ?thesis .
qed

abbreviation Big_step :: "com ⇒ com_den" where
"Big_step c ≡ {(s,t). (c,s) ⇒ t}"

theorem denotational_is_big_step:
"(s,t) ∈ D(c)  =  ((c,s) ⇒ t)"
sorry

end```

### Check File

```theory Check
imports Submission
begin

theorem denotational_is_big_step:
"(s,t) ∈ D(c)  =  ((c,s) ⇒ t)"
by (rule Submission.denotational_is_big_step)

end```

Terms and Conditions