Homework 8

Definitions File

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

declare [[syntax_ambiguity_warning=false]]
declare [[names_short]]

section \<open>Original big_step\<close>

datatype
  com' = SKIP' 
      | Assign' vname aexp
      | Seq'    com'  com'
      | If'     bexp com' com'
      | While'  bexp com'

inductive
  big_step' :: "com' \<times> state \<Rightarrow> state \<Rightarrow> bool" (infix "\<Rightarrow>" 55)
where
Skip': "(SKIP',s) \<Rightarrow> s" |
Assign': "(Assign' x a,s) \<Rightarrow> s(x := aval a s)" |
Seq': "\<lbrakk> (c\<^sub>1',s\<^sub>1) \<Rightarrow> s\<^sub>2;  (c\<^sub>2',s\<^sub>2) \<Rightarrow> s\<^sub>3 \<rbrakk> \<Longrightarrow> (Seq' c\<^sub>1' c\<^sub>2', s\<^sub>1) \<Rightarrow> s\<^sub>3" |
IfTrue: "\<lbrakk> bval b s;  (c\<^sub>1',s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> (If' b c\<^sub>1' c\<^sub>2', s) \<Rightarrow> t" |
IfFalse: "\<lbrakk> \<not>bval b s;  (c\<^sub>2',s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> (If' b c\<^sub>1' c\<^sub>2', s) \<Rightarrow> t" |
WhileFalse: "\<not>bval b s \<Longrightarrow> (While' b c',s) \<Rightarrow> s" |
WhileTrue:
"\<lbrakk> bval b s\<^sub>1;  (c',s\<^sub>1) \<Rightarrow> s\<^sub>2;  (While' b c', s\<^sub>2) \<Rightarrow> s\<^sub>3 \<rbrakk> 
\<Longrightarrow> (While' b c', s\<^sub>1) \<Rightarrow> s\<^sub>3"

declare big_step'.intros [intro]

lemmas big_step'_induct = big_step'.induct[split_format(complete)]

inductive_cases Skip'E[elim!]: "(SKIP',s) \<Rightarrow> t"
thm Skip'E
inductive_cases Assign'E[elim!]: "(Assign' x a,s) \<Rightarrow> t"
thm Assign'E
inductive_cases Seq'E[elim!]: "(Seq' c\<^sub>1' c\<^sub>2',s1) \<Rightarrow> s3"
thm Seq'E
inductive_cases If'E[elim!]: "(If' b c\<^sub>1' c\<^sub>2',s) \<Rightarrow> t"
thm If'E
inductive_cases While'E[elim]: "(While' b c',s) \<Rightarrow> t"
thm While'E


section \<open>New com and big_step with function calls\<close>

type_synonym pname = string

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)
      | CALL   pname

type_synonym penv = "pname \<Rightarrow> com"

inductive
  big_step :: "penv \<Rightarrow> (com \<times> state) \<Rightarrow> state \<Rightarrow> bool" ("_ \<turnstile> _ \<Rightarrow> _") for pe
where
Skip: "pe \<turnstile> (SKIP,s) \<Rightarrow> s" |
Assign: "pe \<turnstile> (x ::= a,s) \<Rightarrow> s(x := aval a s)" |
Seq: "\<lbrakk> pe \<turnstile> (c\<^sub>1,s\<^sub>1) \<Rightarrow> s\<^sub>2;  pe \<turnstile> (c\<^sub>2,s\<^sub>2) \<Rightarrow> s\<^sub>3 \<rbrakk> \<Longrightarrow> pe \<turnstile> (c\<^sub>1;;c\<^sub>2, s\<^sub>1) \<Rightarrow> s\<^sub>3" |
IfTrue: "\<lbrakk> bval b s;  pe \<turnstile> (c\<^sub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> pe \<turnstile> (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> t" |
IfFalse: "\<lbrakk> \<not>bval b s;  pe \<turnstile> (c\<^sub>2,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> pe \<turnstile> (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> t" |
WhileFalse: "\<not>bval b s \<Longrightarrow> pe \<turnstile> (WHILE b DO c,s) \<Rightarrow> s" |
WhileTrue:
"\<lbrakk> bval b s\<^sub>1;  pe \<turnstile> (c,s\<^sub>1) \<Rightarrow> s\<^sub>2;  pe \<turnstile> (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3 \<rbrakk> 
\<Longrightarrow> pe \<turnstile> (WHILE b DO c, s\<^sub>1) \<Rightarrow> s\<^sub>3" |
Call: "\<lbrakk> pe \<turnstile> (pe p,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> pe \<turnstile> (CALL p, s) \<Rightarrow> t"

declare big_step.intros[intro]

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

inductive_cases SkipE[elim!]: "pe \<turnstile> (SKIP,s) \<Rightarrow> t"
thm SkipE
inductive_cases AssignE[elim!]: "pe \<turnstile> (x ::= a,s) \<Rightarrow> t"
thm AssignE
inductive_cases SeqE[elim!]: "pe \<turnstile> (c1;;c2,s1) \<Rightarrow> s3"
thm SeqE
inductive_cases IfE[elim!]: "pe \<turnstile> (IF b THEN c1 ELSE c2,s) \<Rightarrow> t"
thm IfE
inductive_cases CallE[elim]: "pe \<turnstile> (CALL p,s) \<Rightarrow> t"
thm CallE
inductive_cases WhileE[elim]: "pe \<turnstile> (WHILE b DO c,s) \<Rightarrow> t"
thm WhileE


consts inlines :: "penv \<Rightarrow> com \<Rightarrow> com' \<Rightarrow> bool"

consts rec_pnames :: "penv \<Rightarrow> com \<Rightarrow> pname set"

consts nonrec :: "penv \<Rightarrow> com \<Rightarrow> bool"


end

Template File

theory Submission
  imports Defs
begin

inductive inlines :: "penv \<Rightarrow> com \<Rightarrow> com' \<Rightarrow> bool" for pe 

code_pred inlines .

paragraph \<open>The easy part\<close>

theorem inline_correct: "inlines pe c c' \<Longrightarrow> pe \<turnstile> (c, s) \<Rightarrow> t = (c', s) \<Rightarrow> t"
  sorry

paragraph \<open>The hard part\<close>

definition rec_pnames :: "penv \<Rightarrow> com \<Rightarrow> pname set"  where
  "rec_pnames _ = undefined"

definition nonrec :: "penv \<Rightarrow> com \<Rightarrow> bool"  where
  "nonrec _ = undefined"

lemma example1: "nonrec (\<lambda>p. if p = ''end'' then SKIP else CALL ''end'') (SKIP;;CALL ''proc'')"
  sorry

lemma example2: "\<not>nonrec (\<lambda>_. CALL ''rec'') (CALL ''proc'')"
  sorry

theorem inline_nonrec:
  assumes finite: "finite (rec_pnames pe c)"
      and nonrec: "nonrec pe c"
  shows "\<exists>c'. inlines pe c c'"
  sorry

end

Check File

theory Check
  imports Submission
begin

theorem inline_correct: "inlines pe c c' \<Longrightarrow> pe \<turnstile> (c, s) \<Rightarrow> t = (c', s) \<Rightarrow> t"
  by (rule Submission.inline_correct)

lemma example1: "nonrec (\<lambda>p. if p = ''end'' then SKIP else CALL ''end'') (SKIP;;CALL ''proc'')"
  by (rule Submission.example1)

lemma example2: "\<not>nonrec (\<lambda>_. CALL ''rec'') (CALL ''proc'')"
  by (rule Submission.example2)

theorem inline_nonrec: "(finite (rec_pnames pe c)) \<Longrightarrow> (nonrec pe c) \<Longrightarrow> \<exists>c'. inlines pe c c'"
  by (rule Submission.inline_nonrec)

end