I agree 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.
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
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
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
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
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
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