Homework 05.2

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




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