# Theory RExp_Var

theory RExp_Var
imports Equivalence_Checking
```(*  Title:       Enable Checking of Equivalence of Regular Expressions with Variables
Author:      Max Haslbeck
Reference:   http://www4.in.tum.de/lehre/vorlesungen/theo/SS10/vorlesung.shtml p.96ff
*)
section ‹Equivalence of Regular Expression with Variables›

theory RExp_Var
imports "Regular-Sets.Equivalence_Checking"
begin

(* even Atoms → normal Atoms
odd Atoms → Variables *)
fun castdown :: "nat rexp ⇒ nat rexp" where
"castdown Zero = Zero"
| "castdown One = One"
| "castdown (Plus a b) = Plus (castdown a) (castdown b)"
| "castdown (Times a b) = Times (castdown a) (castdown b)"
| "castdown (Star a) = Star (castdown a)"
| "castdown (Atom x) = (Atom (x div 2))"

fun castup :: "nat rexp ⇒ nat rexp" where
"castup Zero = Zero"
| "castup One = One"
| "castup (Plus a b) = Plus (castup a) (castup b)"
| "castup (Times a b) = Times (castup a) (castup b)"
| "castup (Star a) = Star (castup a)"
| "castup (Atom x) = Atom (2*x)"

lemma "castdown (castup r) = r"
apply(induct r) by(auto)

fun substvar :: "nat ⇒ (nat ⇒ ((nat rexp) option)) ⇒ nat rexp" where
"substvar i σ = (case σ i of Some x ⇒ x
| None ⇒ Atom (2*i+1))"

fun w2rexp :: "nat list ⇒ nat rexp" where
"w2rexp [] = One"
| "w2rexp (a#as) = Times (Atom a) (w2rexp as)"

lemma "lang (w2rexp as) = { as }"
apply(induct as)
apply(simp)

fun subst :: "nat rexp ⇒ (nat ⇒ nat rexp option) ⇒ nat rexp" where
"subst Zero _ = Zero"
| "subst One _ = One"
| "subst (Atom i) σ = (if i mod 2 = 0 then Atom i else substvar (i div 2) σ)"
| "subst (Plus a b) σ = Plus (subst a σ) (subst b σ)"
| "subst (Times a b) σ = Times (subst a σ) (subst b σ)"
| "subst (Star a) σ = Star (subst a σ)"

lemma subst_w2rexp: "lang (subst (w2rexp (xs @ ys)) σ) = lang (subst (w2rexp xs) σ) @@ lang (subst (w2rexp ys) σ)"
proof(induct xs)
case (Cons x xs)
have "lang (subst (w2rexp ((x # xs) @ ys)) σ)
= lang (subst (Times (Atom x) (w2rexp (xs @ ys))) σ)" by simp
also have "… = lang (Times (subst (Atom x) σ) (subst (w2rexp (xs @ ys)) σ))" by simp
also have "… = lang (subst (Atom x) σ) @@ (lang (subst (w2rexp (xs @ ys)) σ))" by simp
also have "… = lang (subst (Atom x) σ) @@ ( lang (subst (w2rexp xs) σ) @@ lang (subst (w2rexp ys) σ) )" by(simp only: Cons)
also have "… = lang (Times (subst (Atom x) σ) (subst (w2rexp xs) σ)) @@ lang (subst (w2rexp ys) σ) "
apply(simp del: subst.simps) by(rule conc_assoc[symmetric])
also have "… = lang (subst (Times (Atom x) (w2rexp xs)) σ) @@ lang (subst (w2rexp ys) σ)" by simp
also have "… = lang (subst (w2rexp (x # xs)) σ) @@ lang (subst (w2rexp ys) σ)" by simp
finally show ?case .
qed simp

fun substW :: "nat list ⇒ (nat ⇒ nat rexp option) ⇒ nat rexp" where
"substW as σ = subst (w2rexp as) σ"

fun substL :: "nat lang ⇒ (nat ⇒ nat rexp option) ⇒ nat rexp set" where
"substL S σ = {substW a σ|a. a ∈ S}"

fun L :: "nat rexp set ⇒ nat lang" where
"L S = (⋃r∈S. lang r)"

lemma L_mono: "S1 ⊆ S2 ⟹ L S1 ⊆ L S2"
apply(simp) by blast

definition concS :: "'b rexp set ⇒ 'b rexp set ⇒ 'b rexp set" where
"concS S1 S2 = {Times a b|a b. a∈S1 ∧ b∈S2}"

lemma substL_conc: "L (substL (L1 @@ L2) σ) = L (concS (substL L1 σ) (substL L2 σ))"
apply(auto)
proof (goal_cases)
case (1 x xs ys)
show ?case
apply(rule exI[where x="Times (subst (w2rexp xs) σ) (subst (w2rexp ys) σ)"])
apply(simp)
apply(safe)
apply(rule exI[where x="xs"]) apply(simp add: 1(2))
apply(rule exI[where x="ys"]) apply(simp add: 1(3))
using 1(1) subst_w2rexp by auto
next
case (2 x xs ys)
show ?case
apply(rule exI[where x="subst (w2rexp (xs @ ys)) σ"])
apply(safe)
apply(rule exI[where x="xs@ys"]) apply(simp)
apply(rule exI[where x="xs"])
apply(rule exI[where x="ys"]) using 2(2,3) apply(simp)
using 2(1) subst_w2rexp by(auto)
qed

lemma L_conc: "L(concS M1 M2) = (L M1) @@ (L M2)"
proof -
have "L(concS M1 M2) = (⋃x∈{Times a b |a b. a ∈ M1 ∧ b ∈ M2}. lang x)" unfolding concS_def by(simp)
also have "… = (⋃{lang (Times a b) |a b. a ∈ M1 ∧ b ∈ M2} )" by blast
also have "… = (⋃{lang a @@ lang b |a b. a ∈ M1 ∧ b ∈ M2} )" by simp
also have "… = (⋃{{xs@ys | xs ys. xs ∈ lang a & ys ∈ lang b} |a b. a ∈ M1 ∧ b ∈ M2} )" unfolding conc_def by simp
also have "… = {xs@ys | xs ys. xs∈ (⋃r∈M1. lang r) ∧ ys ∈ (⋃r∈M2. lang r) }" by blast
also have "… = {xs@ys | xs ys. xs∈ L(M1) ∧ ys ∈ L(M2) }" by simp
also have "… = (L M1) @@ (L M2)" unfolding conc_def by simp
finally show ?thesis .
qed

lemma "L(M1 ∪ M2) = (L M1) ∪ (L M2)"
by simp

fun verund :: "'b rexp list ⇒ 'b rexp" where
"verund [] = Zero"
| "verund [r] = r"
| "verund (r#rs) = Plus r (verund rs)"

lemma lang_verund: "r ∈ L (set rs) = (r ∈ lang (verund rs))"
apply(induct rs)
apply(simp)
apply(case_tac rs) by auto

lemma obtainit:
assumes "r ∈ lang (verund rs)"
shows "∃x∈(set (rs::nat rexp list)). r ∈ lang x"
proof -
from assms have "r ∈ L (set rs)" by(simp only: lang_verund)
then show ?thesis by(auto)
qed

lemma lang_verund4: "L (set rs) = lang (verund rs)"
apply(induct rs)
apply(simp)
apply(case_tac rs) by auto

lemma lang_verund1: "r ∈ L (set rs) ⟹ r ∈ lang (verund rs)"
apply(induct rs)
apply(simp)
apply(case_tac rs) by auto
lemma lang_verund2: "r ∈ lang (verund rs) ⟹ r ∈ L (set rs)"
apply(induct rs)
apply(simp)
apply(case_tac rs) by auto

definition starS :: "'b rexp set ⇒ 'b rexp set" where
"starS S = {Star (verund xs)|xs. set xs ⊆ S}"

lemma "[] ∈ L (starS S)"
unfolding starS_def apply(simp)
apply(rule exI[where x="Star(verund [])"])
apply(simp)
apply(rule exI[where x="[]"])
by (simp)

lemma power_mono: "L1 ⊆ L2 ⟹ (L1::'a lang) ^^ n ⊆ L2 ^^ n"
apply(auto) apply(induct n) by(auto simp: conc_def)

lemma star_mono: "L1 ⊆ L2 ⟹ star L1 ⊆ star L2"
apply (rule UN_mono)
apply (auto simp: power_mono)
done

lemma Lstar: "L(starS M) = star ( L(M) )"
unfolding starS_def apply(auto)
proof (goal_cases)
case (1 x xs)
from 1(2) have "L (set xs) ⊆ L (M)" by(rule L_mono)
then have a: "star (L (set xs)) ⊆ star (L (M))" by (rule star_mono)
from 1(1) obtain n where "x ∈ (lang (verund xs)) ^^ n" unfolding star_def by(auto)
thm lang_verund4
then have "x ∈ (L (set xs)) ^^ n" by(simp only: lang_verund4)
then have "x ∈ star (L (set xs))" unfolding star_def by auto
with a have "x ∈ star (L (M))" by auto
then show "x ∈ star (⋃x∈M. lang x)" unfolding starS_def by auto
next
case (2 x)
then obtain n where "x ∈ (⋃x∈M. lang x) ^^ n" unfolding star_def by auto
then show ?case
proof (induct n arbitrary: x)
case 0
then have t: "x=[]" by(simp)
show ?case
apply(rule exI[where x="Star Zero"])
apply(auto simp: t) apply(rule exI[where x="[]"]) by(simp)
next
case (Suc n)
from Suc(2) have t: "x ∈ (⋃a∈M. lang a) @@ (⋃a∈M. lang a) ^^ n" by (simp)
then obtain A B where x: "x = A @ B" and A: "A ∈ (⋃a∈M. lang a)" and B: "B ∈ (⋃a∈M. lang a) ^^ n" by(auto simp: conc_def)
then obtain m where am: "A ∈ lang m" and mM: "m∈M" by(auto)
from Suc(1)[OF B] obtain b bs where "b = Star (verund bs)" and bsM: "set bs ⊆ M" "B ∈ lang b" by auto
then have Bin:  "B ∈ lang (Star (verund bs))" by simp
let ?c = "Star (verund (m#bs))"

have ac: "lang m ⊆ lang (Star (verund (m # bs)))"
apply(cases bs) by(auto)
have ad: "(lang (Star (verund bs))) ⊆ lang (Star (verund (m # bs)))"
apply (rule UN_mono)
apply simp_all
proof -
fix n
have t: "(lang (verund bs) ^^ n) ⊆ (lang m ∪ lang (verund bs)) ^^ n"
by (rule power_mono) simp
then show "lang (verund bs) ^^ n
⊆ lang (verund (m # bs)) ^^ n" by (cases bs) simp_all
qed

from Bin am mM x have "x ∈ lang m @@ (lang (Star (verund bs)))" by auto
then have " x ∈ lang (Star (verund (m # bs))) @@ lang (Star (verund (m # bs)))" using ac ad by blast
then have x_in: "x ∈ lang (Star (verund (m # bs)))" by (auto)

show ?case
apply(rule exI[where x="?c"])
apply(safe)
apply(rule exI[where x="m#bs"]) apply(simp add: bsM mM)
by(fact x_in)
qed
qed

lemma substL_star: "L (substL (star L1) σ) = L (starS (substL L1 σ))"
apply (simp add: concS_def conc_def starS_def star_def)
apply auto unfolding star_def
proof -
fix x a n
assume "x ∈ lang (subst (w2rexp a) σ)"
moreover assume "a ∈ L1 ^^ n"
ultimately show "∃xa. (∃xs. xa = Star (verund xs) ∧ set xs
⊆ {subst (w2rexp a) σ | a. a ∈ L1}) ∧ x ∈ lang xa"
proof(induct n arbitrary: x a)
case 0
then have "a=[]" by auto
with 0 show ?case apply(simp)
apply(rule exI[where x="Star (Zero)"])
apply(simp)
apply(rule exI[where x="[]"])
by(simp)
next
case (Suc n)
then have a1: "a ∈ L1 @@ L1 ^^ n" by auto
then obtain A B where a2: "a = A @ B" and A: "A ∈ L1" and B: "B ∈ L1 ^^ n" by auto

thm subst_w2rexp
from Suc(2) have "x ∈ lang (subst (w2rexp A) σ) @@ lang (subst (w2rexp B) σ)" unfolding a2
by(simp only: subst_w2rexp)
then obtain x1 x2 where x: "x = x1@x2" and x1: "x1 ∈ lang (subst (w2rexp A) σ)"
and  x2: "x2 ∈ lang (subst (w2rexp B) σ)" by auto
from Suc(1)[OF x2 B] obtain R li where
R: "R = Star (verund li)" and li: "set li ⊆ {subst (w2rexp a) σ |a. a ∈ L1}"
and x2R: "x2 ∈ lang R" by auto

show ?case
apply(rule exI[where x="Star (verund ((subst (w2rexp A) σ)#li))"])
apply(simp)
apply(safe)
apply(rule exI[where x="((subst (w2rexp A) σ)#li)"])
apply(rule exI[where x="A"]) apply(simp add: A)
unfolding x
proof (goal_cases)
case 1
let ?L = "(lang (subst (w2rexp A) σ) ∪ lang (verund li))"
have t1: "x1 ∈ ?L" using x1 star_mono by blast
have t2: "x2 ∈ star ?L" using x2R R star_mono apply(simp) by blast
have "x1 @ x2 ∈ (?L @@ star ?L)" using t1 t2 by auto
then show ?case
apply(cases li) by(auto)
qed
qed
next
fix x and xs :: "nat rexp list"
assume "x ∈ (⋃n. lang (verund xs) ^^ n)"
then obtain n where "x ∈ lang (verund xs) ^^ n" by auto
moreover assume "set xs ⊆ {subst (w2rexp a) σ |a. a ∈ L1}"
ultimately show "∃xa. (∃a. xa = subst (w2rexp a) σ ∧
(∃n. a ∈ L1 ^^ n)) ∧ x ∈ lang xa"
proof (induct n arbitrary: x)
case 0
then have xe: "x=[]" by auto
show ?case
apply(rule exI[where x="One"])
apply(rule exI[where x="[]"])
apply(simp)
apply(rule exI[where x="0"])
by(simp)
next
case (Suc n)
then have "x ∈ lang (verund xs) @@ (lang (verund xs) ^^ n)" by auto
then obtain x1 x2 where x: "x=x1@x2" and x1: "x1∈lang (verund xs)"
and x2: "x2 ∈ (lang (verund xs) ^^ n)" by auto
from obtainit [OF x1] obtain el
where "el ∈ set xs" and "x1 ∈ lang el" by auto
with Suc.prems obtain elem
where x1elem: "x1 ∈ lang (subst (w2rexp elem) σ)"
and elemL1: "elem ∈ L1" by auto
from Suc.hyps [OF x2 Suc.prems(2)] obtain R word n where
R: "R = subst (w2rexp word) σ" and word: "word ∈ L1 ^^ n" and x2: "x2 ∈ lang R" by auto

show ?case
apply(rule exI[where x="subst (w2rexp (elem@word)) σ"])
apply(safe)
apply(rule exI[where x="elem@word"])
apply(simp)
apply(rule exI[where x="Suc n"])
proof (goal_cases)
case 1
have "elem ∈ L1" by(fact elemL1)
with word
show "elem @ word ∈ L1 ^^ Suc n" by simp
next
case 2
have "x1 ∈ lang (subst (w2rexp elem) σ)" by(fact x1elem)
with x2[unfolded R] show ?case unfolding x apply(simp only: subst_w2rexp) by blast
qed
qed
qed

lemma substituitionslemma:
fixes E :: "nat rexp"
shows "L (substL ( lang(E) ) σ) = lang (subst E σ)"
proof (induct E)
case (Star e)
have "L (substL (lang (Star e)) σ) = L (substL (star (lang e)) σ)" by auto
also have "… = L (starS (substL (lang e) σ))" by(simp only: substL_star)
also have "… = star ( L (substL (lang e) σ))" by(simp only: Lstar)
also have "… = star (lang (subst e σ))" by(simp only: Star)
also have "… = lang ((subst (Star e) σ))" by auto
finally show ?case .
next
case (Plus e1 e2)
have "L (substL (lang (Plus e1 e2)) σ) = L (substL (lang e1 ∪ lang e2) σ)" by simp
also have "… =  L ( substL (lang e1) σ ∪ substL (lang e2) σ)" by auto
also have "… = L (substL (lang e1) σ) ∪ L (substL (lang e2) σ)" by auto
also have "… = lang (subst e1 σ) ∪ lang (subst e2 σ)" by(simp only: Plus)
also have "… = lang (subst (Plus e1 e2) σ)" by auto
finally show ?case .
next
case (Times e1 e2)
have "L (substL (lang (Times e1 e2)) σ) = L (substL (lang e1 @@ lang e2) σ)" by(simp)
also have "… =  L (concS (substL (lang e1) σ) (substL (lang e2) σ))" by(simp only: substL_conc)
thm L_conc
also have "… = L (substL (lang e1) σ) @@ L (substL (lang e2) σ)" by(simp only: L_conc)
also have "… = lang (subst e1 σ) @@ lang (subst e2 σ)" by(simp only: Times)
also have "… = lang (Times (subst e1 σ) (subst e2 σ))" by auto
also have "… = lang (subst (Times e1 e2) σ)" by auto
finally show ?case .
qed simp_all

corollary lift: "lang e1 = lang e2 ⟹ lang (subst e1 σ) = lang (subst e2 σ)"
proof -
assume eq: "lang e1 = lang e2"
thm substituitionslemma
have "lang (subst e1 σ) = L (substL (lang e1) σ)" by(simp only: substituitionslemma)
also have "… = L (substL (lang e2) σ)" using eq by simp
also have "… = lang (subst e2 σ)" by(simp only: substituitionslemma)
finally show ?thesis .
qed

subsection ‹Examples›

lemma "lang (Plus (Atom (x::nat)) (Atom x))  = lang (Atom x)"
proof -
let ?σ = "(λi. (if i=0 then Some (Atom x) else None))"
let ?e1 = "Plus (Atom 1) (Atom 1)"
let ?e2 = "Atom 1"
have "lang (Plus (Atom x) (Atom x)) = lang (subst ?e1 ?σ)" by (simp)
thm soundness
also have "… = lang (subst ?e2 ?σ)"
apply(rule lift)
apply(rule soundness)
by eval
also have "… = lang (Atom x)" by auto
finally show ?thesis .
qed

fun seq :: "'a rexp list ⇒ 'a rexp" where
"seq [] = One" |
"seq [r] = r" |
"seq (r#rs) = Times r (seq rs)"

abbreviation question where "question x == Plus x One"

definition "L_4cases (x::nat) y=
verund [seq[question (Atom x),(Atom y), (Atom y)],
seq[question (Atom x),(Atom y),(Atom x),Star(Times (Atom y)(Atom x)),(Atom y),(Atom y)],
seq[question (Atom x),(Atom y),(Atom x),Star(Times (Atom y)(Atom x)),(Atom x)],
seq[(Atom x),(Atom x)] ]"

definition "L_A x y = seq[question (Atom x),(Atom y), (Atom y)]"
definition "L_B x y = seq[question (Atom x),(Atom y),(Atom x),Star(Times (Atom y)(Atom x)),(Atom y),(Atom y)]"
definition "L_C x y = seq[question (Atom x),(Atom y),(Atom x),Star(Times (Atom y)(Atom x)),(Atom x)]"
definition "L_D x y = seq[(Atom x),(Atom x)]"

lemma "L_4cases x y = verund [L_A x y, L_B x y, L_C x y, L_D x y]"
unfolding L_A_def L_B_def L_C_def L_D_def L_4cases_def by auto

definition "L_lasthasxx x y = (Plus (seq[question (Atom x), Star(Times (Atom y)(Atom x)),(Atom y),(Atom y)])
(seq[question (Atom y), Star(Times(Atom x) (Atom y)),(Atom x),(Atom x)]))"

lemma lastxx_com: "lang (L_lasthasxx (x::nat) y) = lang (L_lasthasxx y x)" (is "lang ?A = lang ?B")
proof -
let ?σ = "(λi. (if i=0 then Some (Atom x) else (if i=1 then Some (Atom y) else None)))"

let ?e1 = "Plus (seq[Plus (Atom 1) One, Star(Times (Atom 3) (Atom 1)),(Atom 3),(Atom 3)])
(seq[Plus (Atom 3) One, Star(Times (Atom 1) (Atom 3)),(Atom 1),(Atom 1)])"
let ?e2 = "Plus (seq[Plus (Atom 3) One, Star(Times (Atom 1) (Atom 3)),(Atom 1),(Atom 1)])
(seq[Plus (Atom 1) One, Star(Times (Atom 3) (Atom 1)),(Atom 3),(Atom 3)])"
have "lang ?A = lang (subst ?e1 ?σ)" by(simp add: L_lasthasxx_def)
thm soundness
also have "… = lang (subst ?e2 ?σ)"
apply(rule lift)
apply(rule soundness)
by eval
also have "… = lang ?B" by (simp add: L_lasthasxx_def)
finally show ?thesis .
qed

lemma lastxx_is_4cases: "lang (L_4cases x y) = lang (L_lasthasxx x y)" (is "lang ?A = lang ?B")
proof -
let ?σ = "(λi. (if i=0 then Some (Atom x) else (if i=1 then Some (Atom y) else None)))"

let ?e1 = "(Plus (seq[Plus (Atom 1) One,(Atom 3), (Atom 3)])
(Plus (seq[Plus (Atom 1) One,(Atom 3),(Atom 1),Star(Times (Atom 3) (Atom 1)),(Atom 3),(Atom 3)])
(Plus (seq[Plus (Atom 1) One,(Atom 3),(Atom 1),Star(Times (Atom 3) (Atom 1)),(Atom 1)])
(seq[(Atom 1),(Atom 1)]))))"
let ?e2 = "Plus (seq[Plus (Atom 1) One, Star(Times (Atom 3) (Atom 1)),(Atom 3),(Atom 3)])
(seq[Plus (Atom 3) One, Star(Times (Atom 1) (Atom 3)),(Atom 1),(Atom 1)])"
have "lang ?A = lang (subst ?e1 ?σ)" by (simp add: L_4cases_def)
thm soundness
also have "… = lang (subst ?e2 ?σ)"
apply(rule lift)
apply(rule soundness)
by eval
also have "… = lang ?B" by (simp add: L_lasthasxx_def)
finally show ?thesis .
qed

definition "myUNIV x y = Star (Plus (Atom x) (Atom y))"

lemma myUNIV_alle: "lang (myUNIV x y) = {xs. set xs ⊆ {x,y}}"
proof -
have "star {[y], [x]}  = {concat ws |ws. set ws ⊆ {[y], [x]}}" by(simp only: star_conv_concat)
also have "… = {xs. set xs ⊆ {x, y}}" apply(auto) apply(cases "x=y") apply(simp)
apply(case_tac ws)
apply(simp)
apply(auto)
proof (goal_cases)
case (1 as)
then show ?case
proof (induct as)
case (Cons a as)
then have as: "set as ⊆ {x,y}" and axy: "a ∈ {x,y}" by auto
from Cons(1)[OF as] obtain ws where asco: "as = concat ws" and ws: "set ws ⊆ {[y],[x]}" by auto
show ?case
apply(rule exI[where x="[a]#ws"])
using axy by(auto simp add: asco ws)
qed (rule exI[where x="[]"], simp)
qed
finally show ?thesis by(simp add: myUNIV_def)
qed

definition "nodouble x y = (Plus
(seq[question (Atom x), Star(Times(Atom y)(Atom x)),(Atom y)])
(seq[question (Atom y), Star(Times(Atom x) (Atom y)),(Atom x)]))"

lemma myUNIV_char: "lang (myUNIV (x::nat) y) = lang (Times (Star (L_lasthasxx x y)) (Plus One (nodouble x y)))" (is "lang ?A = lang ?B")
proof -
let ?σ = "(λi. (if i=0 then Some (Atom x) else (if i=1 then Some (Atom y) else None)))"

let ?e1 = "Star (Plus (Atom 1) (Atom 3))"
let ?e2 = "(Times (Star (Plus (seq [Plus (Atom 1) One, Star  (Times (Atom 3) (Atom 1)), Atom 3, Atom 3])
(seq [Plus (Atom 3) One, Star (Times (Atom 1) (Atom 3)), Atom 1, Atom 1])))
(Plus One
(Plus
(seq
[Plus (Atom 1)
One,
Star
(Times (Atom 3)
(Atom 1)),
Atom 3])
(seq
[Plus (Atom 3)
One,
Star
(Times (Atom 1)
(Atom 3)),
Atom 1]))))"
have "lang ?A = lang (subst ?e1 ?σ)" by(simp add: myUNIV_def)
thm soundness
also have "… = lang (subst ?e2 ?σ)"
apply(rule lift)
apply(rule soundness)
by eval
also have "… = lang ?B" by (simp add: L_lasthasxx_def nodouble_def)
finally show ?thesis .
qed

definition "mycasexxy x y = Plus (seq[Star (Plus (Atom x) (Atom y)), Atom x, Atom x, Atom y])
(seq[Star (Plus (Atom x) (Atom y)), Atom y, Atom y, Atom x])"
definition "mycasexyx x y = Plus (seq[Star (Plus (Atom x) (Atom y)), Atom x, Atom y, Atom x])
(seq[Star (Plus (Atom x) (Atom y)), Atom y, Atom x, Atom y])"
definition "mycasexx x y = Plus (seq[Star (Plus (Atom x) (Atom y)), Atom x,  Atom x])
(seq[Star (Plus (Atom x) (Atom y)), Atom y, Atom y])"
definition "mycasexy x y = Plus (seq[Atom x,  Atom y]) (seq[Atom y, Atom x])"
definition "mycasex x y = Plus (Atom y) (Atom x)"

definition "mycases x y = Plus
(mycasexxy x y)
(Plus (mycasexyx x y)
(Plus (mycasexx x y)
(Plus (mycasexy x y) (Plus (mycasex x y) (One)))))"

lemma mycases_char: "lang (myUNIV (x::nat) y) = lang (mycases x y)" (is "lang ?A = lang ?B")
proof -
let ?σ = "(λi. (if i=0 then Some (Atom x) else (if i=1 then Some (Atom y) else None)))"

let ?e1 = "Star (Plus (Atom 1) (Atom 3))"
let ?e2 = "Plus (Plus (seq [Star (Plus (Atom 1) (Atom 3)), Atom 1, Atom 1, Atom 3])
(seq [Star (Plus (Atom 1) (Atom 3)), Atom 3, Atom 3, Atom 1]))
(Plus (Plus (seq [Star (Plus (Atom 1) (Atom 3)), Atom 1, Atom 3, Atom 1])
(seq [Star (Plus (Atom 1) (Atom 3)), Atom 3, Atom 1, Atom 3]))
(Plus (Plus (seq [Star (Plus (Atom 1) (Atom 3)), Atom 1, Atom 1])
(seq [Star (Plus (Atom 1) (Atom 3)), Atom 3, Atom 3]))
(Plus (Plus (seq [Atom 1, Atom 3]) (seq [Atom 3, Atom 1])) (Plus (Plus (Atom 3) (Atom 1)) One))))"

have "lang ?A = lang (subst ?e1 ?σ)" by(simp add: myUNIV_def)
thm soundness
also have "… = lang (subst ?e2 ?σ)"
apply(rule lift)
apply(rule soundness)
by eval
also have "… = lang ?B" by (simp add:  mycases_def mycasexxy_def mycasexyx_def
mycasexx_def mycasex_def mycasexy_def)
finally show ?thesis .
qed

end
```