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 4

This is the task corresponding to homework 4.

## Resources

### Definitions File

```theory Defs
imports Main
begin

declare [[names_short]]

datatype ('q, 'a) DA = DA
(states: "'q set")
(transitions: "'q \<Rightarrow> 'a \<Rightarrow> 'q")
(initial: "'q")
(finals: "'q set")

definition "wf_da M \<equiv> (initial M \<in> states M \<and>
finals M \<subseteq> states M \<and>
(\<forall>q a. q \<in> states M \<longrightarrow> transitions M q a \<in> states M))"

type_synonym 'a word = "'a list"
type_synonym 'a lang = "('a word) set"
abbreviation "\<epsilon> \<equiv> []"

inductive run :: "('q, 'a) DA \<Rightarrow> 'q \<Rightarrow> 'a word \<Rightarrow> nat \<Rightarrow> 'q \<Rightarrow> bool"
("_ _ _ \<rightarrow>_ _" [50,50,50,50,50]) where
run_epsilon: "q \<in> states M \<Longrightarrow> M q \<epsilon> \<rightarrow>n q"|
run_zero: "q \<in> states M \<Longrightarrow> M q w \<rightarrow>0 q"|
run_step: "q \<in> states M \<Longrightarrow> M (transitions M q a) as \<rightarrow>n q' \<Longrightarrow> M q (a # as) \<rightarrow>(Suc n) q'"

code_pred run .

abbreviation run_complete :: "('q, 'a) DA \<Rightarrow> 'q \<Rightarrow> 'a word \<Rightarrow> 'q \<Rightarrow> bool"
("_ _ _ \<rightarrow>c _" [50,50,50,50]) where
"M q w \<rightarrow>c q' \<equiv> M q w \<rightarrow>(length w) q'"

definition "lang M \<equiv> {w. \<exists>qf. qf \<in> finals M \<and> M (initial M) w \<rightarrow>c qf}"

datatype sigma = A | B

fun test\<delta> :: "nat \<Rightarrow> sigma \<Rightarrow> nat" where
"test\<delta> q A = 0"|
"test\<delta> q B = 1"

definition "testM \<equiv> DA {0,1} test\<delta> 0 {1}"

consts run_fun :: "('q, 'a) DA \<Rightarrow> 'q \<Rightarrow> 'a word \<Rightarrow> nat \<Rightarrow> 'q"

end```

### Template File

```theory Submission
imports Defs
begin

type_synonym 'a word = "'a list"
type_synonym 'a lang = "('a word) set"

lemma run_determ: "M q w \<rightarrow>n q' \<Longrightarrow> M q w \<rightarrow>n q'' \<Longrightarrow> q' = q''"
sorry

lemma visit_valid_start: "M q w' \<rightarrow>n q'' \<Longrightarrow> q \<in> states M"
sorry

lemma visit_valid_end: "M q w \<rightarrow>n q' \<Longrightarrow> q' \<in> states M"
sorry

lemma run_append: "M q w \<rightarrow>c q' \<Longrightarrow> M q' w' \<rightarrow>c q'' \<Longrightarrow> M q (w @ w') \<rightarrow>c q''"
sorry

lemma run_split: "M q (w @ w') \<rightarrow>c q'' \<Longrightarrow> \<exists>q'. M q w \<rightarrow>c q' \<and> M q' w' \<rightarrow>c q''"
sorry

fun run_fun :: "('q, 'a) DA \<Rightarrow> 'q \<Rightarrow> 'a word \<Rightarrow> nat \<Rightarrow> 'q"  where
"run_fun _ q _ _ = q"

lemma run_complete_to_run_fun :
"M q w \<rightarrow>c q' \<Longrightarrow> run_fun M q w (length w) = q'"
sorry

lemma run_run_fun:
assumes "wf_da M"
and "q \<in> states M"
shows "M q w \<rightarrow>n (run_fun M q w n)"
sorry

value "testM (initial testM) [A,B,B,B] \<rightarrow>c 1"
value "testM (initial testM) [A,B,A,A] \<rightarrow>c 0"

value "testM (initial testM) [A,B,B,B] \<rightarrow>3 1"

value "testM (initial testM) [A,B,B,B] \<rightarrow>6 1"

value "testM (initial testM) [A,B,B,B] \<rightarrow>0 (initial testM)"

lemma lang_testM_subseteq: "lang testM \<subseteq> {w. \<exists>w'. w = w' @ [B]}"
sorry

lemma subseteq_lang_testM: "{w. \<exists>w'. w = w' @ [B]} \<subseteq> lang testM"
sorry

corollary lang_testM_eq: "lang testM = {w. \<exists>w'. w = w' @ [B]}"
sorry

end```

### Check File

```theory Check
imports Submission
begin

lemma run_determ: "M q w \<rightarrow>n q' \<Longrightarrow> M q w \<rightarrow>n q'' \<Longrightarrow> q' = q''"
by (rule Submission.run_determ)

lemma visit_valid_start: "M q w' \<rightarrow>n q'' \<Longrightarrow> q \<in> states M"
by (rule Submission.visit_valid_start)

lemma visit_valid_end: "M q w \<rightarrow>n q' \<Longrightarrow> q' \<in> states M"
by (rule Submission.visit_valid_end)

lemma run_append: "M q w \<rightarrow>c q' \<Longrightarrow> M q' w' \<rightarrow>c q'' \<Longrightarrow> M q (w @ w') \<rightarrow>c q''"
by (rule Submission.run_append)

lemma run_split: "M q (w @ w') \<rightarrow>c q'' \<Longrightarrow> \<exists>q'. M q w \<rightarrow>c q' \<and> M q' w' \<rightarrow>c q''"
by (rule Submission.run_split)

lemma run_complete_to_run_fun: "M q w \<rightarrow>c q' \<Longrightarrow> run_fun M q w (length w) = q'"
by (rule Submission.run_complete_to_run_fun)

lemma run_run_fun: "(wf_da M) \<Longrightarrow> (q \<in> states M) \<Longrightarrow> M q w \<rightarrow>n (run_fun M q w n)"
by (rule Submission.run_run_fun)

lemma lang_testM_subseteq: "lang testM \<subseteq> {w. \<exists>w'. w = w' @ [B]}"
by (rule Submission.lang_testM_subseteq)

lemma subseteq_lang_testM: "{w. \<exists>w'. w = w' @ [B]} \<subseteq> lang testM"
by (rule Submission.subseteq_lang_testM)

end```

Terms and Conditions