theory a2
  (* Download the file RegExp.thy and put it in the same directory as this one: *)
  imports RegExp
begin

section "Question 1: Higher-Order Logic"

lemma hol_a: "\<not>(\<forall>x. P x) \<longleftrightarrow> (\<exists>x. \<not>P x)"
  (*TODO*)
  oops

lemma hol_b: "(\<forall>x. P \<longrightarrow> Q x) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x. Q x))"
  (*TODO*)
  oops

lemma hol_c: "\<forall>x. \<not>f x \<longrightarrow> f (g x) \<Longrightarrow> \<forall>x. f x \<or> f (g x)"
  (*TODO*)
  oops

lemma hol_d: "\<lbrakk>\<forall>x. \<not>f x \<longrightarrow> f (g x); \<exists>x. f x\<rbrakk> \<Longrightarrow> \<exists>x. f x \<and> f (g (g x))"
  (*TODO*)
  oops

lemma hol_e: "(\<forall>x. Q x = P x) \<and> ((\<exists>x. P x) \<longrightarrow> H) \<and> (\<exists>x. Q x) \<longrightarrow> H"
  (*TODO*)
  oops

lemma hol_f: "(\<forall>Q. (\<forall>x. P x \<longrightarrow> Q) \<longrightarrow> Q) \<longrightarrow> (\<exists>x. P x)"
  (*TODO*)
  oops


(*---------------------------------------------------------*) 
section "Question 2: Strings and Regular Expressions"

(* An example string with newline characters *)
definition
  test_str :: string
  where
  "test_str = 
''some
test
abc hello
text''"

definition
  new_line :: char
  where
  "new_line = CHR ''\<newline>''"


(*----------------*)
(* Question 2 (a) *)
primrec
  glue :: "'a \<Rightarrow> 'a list list \<Rightarrow> 'a list"
where
  "glue a [] = TODO"

(* test on some examples *)

(* Define and test on some examples:
  chop :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list list"
*)

(*----------------*)
(* Question 2 (b) *)
primrec
  num_of :: "'a \<Rightarrow> 'a list \<Rightarrow> nat"
  where
  "num_of a [] = TODO"

lemma length_glue:
  "length (glue a xss) = sum_list (map length xss) + length xss - 1"
  (*TODO*)
  oops

lemma length_chop:
  "length (chop x xs) = num_of x xs + 1"
  (*TODO*)
  oops



(*----------------*)
(* Question 2 (c) *)
lemma chop_sep:
  "ls \<in> set (chop a xs) \<Longrightarrow> a \<notin> set ls"
  (*TODO*)
  oops

lemma glue_chop:
  "glue a (chop a xs) = xs"
  (*TODO*)
  oops



(*----------------*)
(* Question 2 (d) *)

(* TODO: define
  any_of :: "regexp list \<Rightarrow> regexp"
*)

lemma lang_any_of[simp]:
  "lang (any_of rs) = \<Union> (lang ` set rs)"
  (* TODO *)
  oops

primrec
  repeat :: "word set \<Rightarrow> nat \<Rightarrow> word set"
  where
  "repeat A 0 = TODO"

lemma star_repeat:
  "star A = (\<Union>n. repeat A n)"
  (* TODO *)
  oops


(*----------------*)
(* Question 2 (e) *)
definition
  matches :: "regexp \<Rightarrow> string \<Rightarrow> bool"
  where
  "matches r w \<equiv> w \<in> lang r"

definition
  matches_sub :: "regexp \<Rightarrow> string \<Rightarrow> bool"
  where
  "matches_sub r = matches TODO"

primrec
  string :: "string \<Rightarrow> regexp"
  where
  "string [] = TODO"

primrec
  is_prefix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
  where
  "is_prefix [] ys = TODO"

primrec
  is_substring :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
  where
  "is_substring xs [] = TODO"

(* TODO: test on some examples *)


lemma matches_sub:
  "matches_sub r xs = (\<exists>xs' ys zs. xs = ys @ xs' @ zs \<and> matches r xs')"
  (* TODO *)
  oops

lemma matches_string[simp]:
  "matches (string xs) ys = (ys = xs)"
  (* TODO *)
  oops

lemma is_substring:
  "is_substring xs ys = (\<exists>bs cs. ys = bs @ xs @ cs)"
  (* TODO *)
  oops

lemma matches_substring:
  "matches_sub (string xs) l = is_substring xs l"
  (* TODO *)
  oops


(*----------------*)
(* Question 2 (f) *)
primrec
  rlen :: "regexp \<Rightarrow> nat option"
  where
  "rlen (Atom a) = TODO"

lemma rlen_string[simp]:
  "rlen (string xs) = Some (length xs)"
  (* TODO *)
  oops

lemma rlen_lang:
  "rlen r = Some n \<Longrightarrow> \<forall>xs \<in> lang r. length xs = n"
  (* TODO *)
  oops



(*---------------------------------------------------------*)
section "Question 3: Normal Forms"

(*----------------*)
(* Question 3 (a) *)
fun
  find_pat :: "'a list \<Rightarrow> 'a list"
  where
  (* TODO *)

value "find_pat ''cababc''"

lemma hd_find_pat[simp]:
  "hd (find_pat xs) = hd xs"
  (* TODO *)
  oops

lemma last_find_pat[simp]:
  "last (find_pat xs) = last xs"
  (* TODO *)
  oops

lemma find_pat_neq:
  "(find_pat xs \<noteq> xs) = (\<exists>as bs x y. xs = as @ x # y # x # bs)"
  (* TODO *)
  oops

lemma find_pat_eq:
  "(find_pat xs = xs) = (\<forall>as bs x y. xs \<noteq> as @ x # y # x # bs)"
  by (metis find_pat_neq)


(*----------------*)
(* Question 3 (b) *)

lemma find_pat_neq_Cons:
  "find_pat xs \<noteq> xs \<Longrightarrow> find_pat (x#xs) \<noteq> x#xs"
  oops (* helper *)

lemma find_pat_eq_Cons:
  "find_pat (x#xs) = x#xs \<Longrightarrow> find_pat xs = xs"
  oops (* helper *)

lemma find_pat_Cons_find_pat:
  "find_pat (x#find_pat xs) = find_pat (find_pat (x#xs))"
  (* TODO *)
  oops

lemma find_pat_app_find_pat:
  "find_pat (find_pat xs @ [x]) = find_pat (find_pat (xs @ [x]))"
  (* TODO *)
  oops

lemma find_pat_appendD:
  "find_pat (xs @ ys) = xs @ ys \<Longrightarrow> find_pat xs = xs"
  oops (* helper *)

lemma find_pat_eq_rev:
  "find_pat xs = xs \<Longrightarrow> find_pat (rev xs) = rev xs"
  (* TODO *)
  oops

lemma find_pat_rev:
  "find_pat xs = xs \<Longrightarrow> find_pat (rev xs @ [x]) = rev (find_pat (x # xs))"
  (* TODO *)
  oops


(*----------------*)
(* Question 3 (c) *)
fun
  nf :: "'a list \<Rightarrow> 'a list"
  where
  "nf xs = (if find_pat xs = xs then xs else nf (find_pat xs))"
  (* Extract a lemma that helps Isabelle to prove termination here. Make it [simp]. *)
  sorry


(* This means simp will not automatically unfold nf. Use "subst nf.simps" to unfold manually. *)
declare nf.simps[simp del]

value "nf ''cabacacb''"


lemma nf_singles[simp]:
  "nf [] = []"
  "nf [x] = [x]"
  "nf [x,y] = [x,y]"
  by (auto simp: nf.simps)

lemma nf_find_pat:
  "nf (find_pat xs) = nf xs"
  (* TODO *)
  oops

lemma nf_fp:
  "find_pat (nf xs) = nf xs"
  (* TODO *)
  oops

lemma nf_nf:
  "nf (nf xs) = nf xs"
  (* TODO *)
  oops

lemma hd_nf:
  "hd (nf xs) = hd xs"
  (* TODO *)
  oops

lemma last_nf:
  "last (nf xs) = last xs"
  (* TODO *)
  oops


(*----------------*)
(* Question 3 (d) *)


lemma find_pat_nf_Cons:
  "find_pat xs = xs \<Longrightarrow> nf (x#xs) = find_pat (x#xs)"
  oops (* helper *)

lemma nf_find_pat_Cons:
  "find_pat xs \<noteq> xs \<Longrightarrow> nf (x # find_pat xs) = nf (x # xs)"
  oops (* helper *)

lemma nf_Cons_nf:
  "nf (x#nf xs) = nf (x#xs)"
  (* TODO *)
  oops

lemma nf_hd_dist:
  "nf (x#xs) = find_pat (x#nf xs)"
  (* TODO *)
  oops

lemma nf_last_dist:
  "nf (xs @ [x]) = find_pat (nf xs @ [x])"
  (* TODO *)
  oops

lemma find_pat_rev_Cons:
  "rev (find_pat (x#nf xs)) = find_pat (rev (x#nf xs))"
  oops (* helper *)

lemma nf_rev:
  "nf (rev xs) = rev (nf xs)"
  (* TODO *)
  oops

end