Homework 08.2

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] 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"
― ‹Your cases here:›

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))"
― ‹Your cases here:›

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