Homework 4

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