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 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
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
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