# Theory Auxiliary

```(*  Title:      JinjaThreads/Basic/Aux.thy
Author:     Andreas Lochbihler, David von Oheimb, Tobias Nipkow

Based on the Jinja theory Common/Aux.thy by David von Oheimb and Tobias Nipkow
*)

section ‹Auxiliary Definitions and Lemmata›

theory Auxiliary
imports
Complex_Main
"HOL-Library.Transitive_Closure_Table"
"HOL-Library.Predicate_Compile_Alternative_Defs"
"HOL-Library.Infinite_Set"
FinFun.FinFun
begin

unbundle finfun_syntax

(* FIXME move and possibly turn into a general simproc *)
"((n::nat) + max i j ≤ m) = (n + i ≤ m ∧ n + j ≤ m)"
(*<*)by arith(*>*)

"(Suc(n + max i j) ≤ m) = (Suc(n + i) ≤ m ∧ Suc(n + j) ≤ m)"
(*<*)by arith(*>*)

lemma less_min_eq1:
"(a :: 'a :: order) < b ⟹ min a b = a"

lemma less_min_eq2:
"(a :: 'a :: order) > b ⟹ min a b = b"

no_notation floor ("⌊_⌋")
notation Some ("(⌊_⌋)")

(*<*)
declare
option.splits[split]
Let_def[simp]
subset_insertI2 [simp]
(*>*)

declare not_Cons_self [no_atp]

lemma Option_bind_eq_None_conv:
"x ⤜ y = None ⟷ x = None ∨ (∃x'. x = Some x' ∧ y x' = None)"
by(cases x) simp_all

lemma map_upds_xchg_snd:
"⟦ length xs ≤ length ys; length xs ≤ length zs; ∀i. i < length xs ⟶ ys ! i = zs ! i ⟧
⟹ f(xs [↦] ys) = f(xs [↦] zs)"
proof(induct xs arbitrary: ys zs f)
case Nil thus ?case by simp
next
case (Cons x xs)
note IH = ‹⋀f ys zs. ⟦ length xs ≤ length ys; length xs ≤ length zs; ∀i<length xs. ys ! i = zs ! i⟧
⟹ f(xs [↦] ys) = f(xs [↦] zs)›
note leny = ‹length (x # xs) ≤ length ys›
note lenz = ‹length (x # xs) ≤ length zs›
note nth = ‹∀i<length (x # xs). ys ! i = zs ! i›
from lenz obtain z zs' where zs [simp]: "zs = z # zs'" by(cases zs, auto)
from leny obtain y ys' where ys [simp]: "ys = y # ys'" by(cases ys, auto)
from lenz leny nth have "(f(x ↦ y))(xs [↦] ys') = (f(x ↦ y))(xs [↦] zs')"
by-(rule IH, auto)
moreover from nth have "y = z" by auto
ultimately show ?case by(simp add: map_upds_def)
qed

subsection ‹‹distinct_fst››

definition
distinct_fst  :: "('a × 'b) list ⇒ bool"
where
"distinct_fst  ≡  distinct ∘ map fst"

lemma distinct_fst_Nil [simp]:
"distinct_fst []"
(*<*)
apply (unfold distinct_fst_def)
apply (simp (no_asm))
done
(*>*)

lemma distinct_fst_Cons [simp]:
"distinct_fst ((k,x)#kxs) = (distinct_fst kxs ∧ (∀y. (k,y) ∉ set kxs))"
(*<*)
apply (unfold distinct_fst_def)
apply (auto simp:image_def)
done
(*>*)

lemma distinct_fstD: "⟦ distinct_fst xs; (x, y) ∈ set xs; (x, z) ∈ set xs ⟧ ⟹ y = z"
by(induct xs) auto

lemma map_of_SomeI:
"⟦ distinct_fst kxs; (k,x) ∈ set kxs ⟧ ⟹ map_of kxs k = Some x"
(*<*)by (induct kxs) (auto)(*>*)

subsection ‹Using @{term list_all2} for relations›

definition
fun_of :: "('a × 'b) set ⇒ 'a ⇒ 'b ⇒ bool"
where
"fun_of S ≡ λx y. (x,y) ∈ S"

text ‹Convenience lemmas›
(*<*)
declare fun_of_def [simp]
(*>*)
lemma rel_list_all2_Cons [iff]:
"list_all2 (fun_of S) (x#xs) (y#ys) =
((x,y) ∈ S ∧ list_all2 (fun_of S) xs ys)"
(*<*)by simp(*>*)

lemma rel_list_all2_Cons1:
"list_all2 (fun_of S) (x#xs) ys =
(∃z zs. ys = z#zs ∧ (x,z) ∈ S ∧ list_all2 (fun_of S) xs zs)"
(*<*)by (cases ys) auto(*>*)

lemma rel_list_all2_Cons2:
"list_all2 (fun_of S) xs (y#ys) =
(∃z zs. xs = z#zs ∧ (z,y) ∈ S ∧ list_all2 (fun_of S) zs ys)"
(*<*)by (cases xs) auto(*>*)

lemma rel_list_all2_refl:
"(⋀x. (x,x) ∈ S) ⟹ list_all2 (fun_of S) xs xs"

lemma rel_list_all2_antisym:
"⟦ (⋀x y. ⟦(x,y) ∈ S; (y,x) ∈ T⟧ ⟹ x = y);
list_all2 (fun_of S) xs ys; list_all2 (fun_of T) ys xs ⟧ ⟹ xs = ys"
(*<*)by (rule list_all2_antisym) auto(*>*)

lemma rel_list_all2_trans:
"⟦ ⋀a b c. ⟦(a,b) ∈ R; (b,c) ∈ S⟧ ⟹ (a,c) ∈ T;
list_all2 (fun_of R) as bs; list_all2 (fun_of S) bs cs⟧
⟹ list_all2 (fun_of T) as cs"
(*<*)by (rule list_all2_trans) auto(*>*)

lemma rel_list_all2_update_cong:
"⟦ i<size xs; list_all2 (fun_of S) xs ys; (x,y) ∈ S ⟧
⟹ list_all2 (fun_of S) (xs[i:=x]) (ys[i:=y])"

lemma rel_list_all2_nthD:
"⟦ list_all2 (fun_of S) xs ys; p < size xs ⟧ ⟹ (xs!p,ys!p) ∈ S"
(*<*)by (drule list_all2_nthD) auto(*>*)

lemma rel_list_all2I:
"⟦ length a = length b; ⋀n. n < length a ⟹ (a!n,b!n) ∈ S ⟧ ⟹ list_all2 (fun_of S) a b"
(*<*)by (erule list_all2_all_nthI) simp(*>*)

(*<*)declare fun_of_def [simp del](*>*)

lemma list_all2_split:
assumes major: "list_all2 P xs ys"
and split: "⋀x y. P x y ⟹ ∃z. Q x z ∧ R z y"
shows "∃zs. list_all2 Q xs zs ∧ list_all2 R zs ys"
using major
by(induct rule: list_all2_induct)(auto dest: split)

lemma list_all2_op_eq [simp]:
"list_all2 (=) xs ys ⟷ xs = ys"
by(induct xs arbitrary: ys)(auto simp add: list_all2_Cons1)

lemmas filter_replicate_conv = filter_replicate

lemma length_greater_Suc_0_conv: "Suc 0 < length xs ⟷ (∃x x' xs'. xs = x # x' # xs')"
by(cases xs, auto simp add: neq_Nil_conv)

lemmas zip_same_conv = zip_same_conv_map

lemma f_nth_set:
"⟦ f (xs ! n) = v; n < length xs ⟧ ⟹ v ∈ f ` set xs"
unfolding set_conv_nth by auto

lemma nth_concat_eqI:
"⟦ n = sum_list (map length (take i xss)) + k; i < length xss; k < length (xss ! i); x = xss ! i ! k ⟧
⟹ concat xss ! n = x"
apply(induct xss arbitrary: n i k)
apply simp
apply simp
apply(case_tac i)
done

lemma replicate_eq_append_conv:
"(replicate n x = xs @ ys) = (∃m≤n. xs = replicate m x ∧ ys = replicate (n-m) x)"
proof(induct n arbitrary: xs ys)
case 0 thus ?case by simp
next
case (Suc n xs ys)
have IH: "⋀xs ys. (replicate n x = xs @ ys) = (∃m≤n. xs = replicate m x ∧ ys = replicate (n - m) x)" by fact
show ?case
proof(unfold replicate_Suc, rule iffI)
assume a: "x # replicate n x = xs @ ys"
show "∃m≤Suc n. xs = replicate m x ∧ ys = replicate (Suc n - m) x"
proof(cases xs)
case Nil
thus ?thesis using a
by(auto)
next
case (Cons X XS)
with a have x: "x = X" and "replicate n x = XS @ ys" by auto
hence "∃m≤n. XS = replicate m x ∧ ys = replicate (n - m) x"
by -(rule IH[THEN iffD1])
then obtain m where "m ≤ n" and XS: "XS = replicate m x" and ys: "ys = replicate (n - m) x" by blast
with x Cons show ?thesis
by(fastforce)
qed
next
assume "∃m≤Suc n. xs = replicate m x ∧ ys = replicate (Suc n - m) x"
then obtain m where m: "m ≤ Suc n" and xs: "xs = replicate m x" and ys: "ys = replicate (Suc n - m) x" by blast
thus "x # replicate n x = xs @ ys"
qed
qed

lemma replicate_Suc_snoc:
"replicate (Suc n) x = replicate n x @ [x]"
by (metis replicate_Suc replicate_append_same)

lemma map_eq_append_conv:
"map f xs = ys @ zs ⟷ (∃ys' zs'. map f ys' = ys ∧ map f zs' = zs ∧ xs = ys' @ zs')"
apply(rule iffI)
apply(metis append_eq_conv_conj append_take_drop_id drop_map take_map)
by(clarsimp)

lemma append_eq_map_conv:
"ys @ zs = map f xs ⟷ (∃ys' zs'. map f ys' = ys ∧ map f zs' = zs ∧ xs = ys' @ zs')"
unfolding map_eq_append_conv[symmetric]
by auto

lemma map_eq_map_conv:
"map f xs = map g ys ⟷ list_all2 (λx y. f x = g y) xs ys"
apply(induct xs arbitrary: ys)
done

lemma map_eq_all_nth_conv:
"map f xs = ys ⟷ length xs = length ys ∧ (∀n < length xs. f (xs ! n) = ys ! n)"
apply(induct xs arbitrary: ys)
apply(fastforce simp add: nth_Cons Suc_length_conv split: nat.splits)+
done

lemma take_eq_take_le_eq:
"⟦ take n xs = take n ys; m ≤ n ⟧ ⟹ take m xs = take m ys"
by(metis min.absorb_iff1 take_take)

lemma set_tl_subset: "set (tl xs) ⊆ set xs"
by(cases xs) auto

lemma tl_conv_drop: "tl xs = drop 1 xs"
by(cases xs) simp_all

lemma takeWhile_eq_Nil_dropWhile_eq_Nil_imp_Nil:
"⟦ takeWhile P xs = []; dropWhile P xs = [] ⟧ ⟹ xs = []"
by (metis dropWhile_eq_drop drop_0 list.size(3))

lemma dropWhile_append1': "dropWhile P xs ≠ [] ⟹ dropWhile P (xs @ ys) = dropWhile P xs @ ys"
by(cases xs) auto

lemma dropWhile_append2': "dropWhile P xs = [] ⟹ dropWhile P (xs @ ys) = dropWhile P ys"
by(simp)

lemma takeWhile_append1': "dropWhile P xs ≠ [] ⟹ takeWhile P (xs @ ys) = takeWhile P xs"
by auto

lemma dropWhile_eq_ConsD:
"dropWhile P xs = y # ys ⟹ y ∈ set xs ∧ ¬ P y"
by(induct xs)(auto split: if_split_asm)

lemma dropWhile_eq_hd_conv: "dropWhile P xs = hd xs # rest ⟷ xs ≠ [] ∧ rest = tl xs ∧ ¬ P (hd xs)"
by (metis append_Nil dropWhile_eq_Cons_conv list.sel(1) neq_Nil_conv takeWhile_dropWhile_id takeWhile_eq_Nil_iff list.sel(3))

lemma subset_code [code_unfold]:
"set xs ⊆ set ys ⟷ (∀x ∈ set xs. x ∈ set ys)"
by(rule Set.subset_eq)

lemma eval_bot [simp]:
"Predicate.eval bot = (λ_. False)"

lemma not_is_emptyE:
assumes "¬ Predicate.is_empty P"
obtains x where "Predicate.eval P x"
using assms
by(fastforce simp add: Predicate.is_empty_def bot_pred_def intro!: pred_iffI)

lemma is_emptyD:
assumes "Predicate.is_empty P"
shows "Predicate.eval P x ⟹ False"
using assms
by(simp add: Predicate.is_empty_def bot_pred_def bot_apply Set.empty_def)

lemma eval_bind_conv:
"Predicate.eval (P ⤜ R) y = (∃x. Predicate.eval P x ∧ Predicate.eval (R x) y)"
by(blast elim: bindE intro: bindI)

lemma eval_single_conv: "Predicate.eval (Predicate.single a) b ⟷ a = b"
by(blast intro: singleI elim: singleE)

lemma conj_asm_conv_imp:
"(A ∧ B ⟹ PROP C) ≡ (A ⟹ B ⟹ PROP C)"
apply(rule equal_intr_rule)
apply(erule meta_mp)
apply(erule (1) conjI)
apply(erule meta_impE)
apply(erule conjunct1)
apply(erule meta_mp)
apply(erule conjunct2)
done

lemma meta_all_eq_conv: "(⋀a. a = b ⟹ PROP P a) ≡ PROP P b"
apply(rule equal_intr_rule)
apply(erule meta_allE)
apply(erule meta_mp)
apply(rule refl)
apply(hypsubst)
apply assumption
done

lemma meta_all_eq_conv2: "(⋀a. b = a ⟹ PROP P a) ≡ PROP P b"
apply(rule equal_intr_rule)
apply(erule meta_allE)
apply(erule meta_mp)
apply(rule refl)
apply(hypsubst)
apply assumption
done

lemma disj_split:
"P (a ∨ b) ⟷ (a ⟶ P True) ∧ (b ⟶ P True) ∧ (¬ a ∧ ¬ b ⟶ P False)"
apply(cases a)
apply(case_tac [!] b)
apply auto
done

lemma disj_split_asm:
"P (a ∨ b) ⟷ ¬ (a ∧ ¬ P True ∨ b ∧ ¬ P True ∨ ¬ a ∧ ¬ b ∧ ¬ P False)"
done

lemma disjCE:
assumes "P ∨ Q"
obtains P | "Q" "¬ P"
using assms by blast

lemma case_option_conv_if:
"(case v of None ⇒ f | Some x ⇒ g x) = (if ∃a. v = Some a then g (the v) else f)"
by(simp)

lemma LetI: "(⋀x. x = t ⟹ P x) ⟹ let x = t in P x"
by(simp)

(* rearrange parameters and premises to allow application of one-point-rules *)
(* adapted from Tools/induct.ML and Isabelle Developer Workshop 2010 *)

simproc_setup rearrange_eqs ("Pure.all t") = ‹
let
fun swap_params_conv ctxt i j cv =
let
fun conv1 0 ctxt = Conv.forall_conv (cv o snd) ctxt
| conv1 k ctxt =
Conv.rewr_conv @{thm swap_params} then_conv
Conv.forall_conv (conv1 (k - 1) o snd) ctxt
fun conv2 0 ctxt = conv1 j ctxt
| conv2 k ctxt = Conv.forall_conv (conv2 (k - 1) o snd) ctxt
in conv2 i ctxt end;

fun swap_prems_conv 0 = Conv.all_conv
| swap_prems_conv i =
Conv.implies_concl_conv (swap_prems_conv (i - 1)) then_conv
Conv.rewr_conv Drule.swap_prems_eq;

fun find_eq ctxt t =
let
val l = length (Logic.strip_params t);
val Hs = Logic.strip_assums_hyp t;
fun find (i, (_ \$ (Const ("HOL.eq", _) \$ Bound j \$ _))) = SOME (i, j)
| find (i, (_ \$ (Const ("HOL.eq", _) \$ _ \$ Bound j))) = SOME (i, j)
| find _ = NONE
in
(case get_first find (map_index I Hs) of
NONE => NONE
| SOME (0, 0) => NONE
| SOME (i, j) => SOME (i, l - j - 1, j))
end;

fun mk_swap_rrule ctxt ct =
(case find_eq ctxt (Thm.term_of ct) of
NONE => NONE
| SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct))
in
fn _ => mk_swap_rrule
end
›
declare [[simproc del: rearrange_eqs]]
lemmas meta_onepoint = meta_all_eq_conv meta_all_eq_conv2

lemma meta_all2_eq_conv: "(⋀a b. a = c ⟹ PROP P a b) ≡ (⋀b. PROP P c b)"
apply(rule equal_intr_rule)
apply(erule meta_allE)+
apply(erule meta_mp)
apply(rule refl)
apply(erule meta_allE)
apply simp
done

lemma meta_all3_eq_conv: "(⋀a b c. a = d ⟹ PROP P a b c) ≡ (⋀b c. PROP P d b c)"
apply(rule equal_intr_rule)
apply(erule meta_allE)+
apply(erule meta_mp)
apply(rule refl)
apply(erule meta_allE)+
apply simp
done

lemma meta_all4_eq_conv: "(⋀a b c d. a = e ⟹ PROP P a b c d) ≡ (⋀b c d. PROP P e b c d)"
apply(rule equal_intr_rule)
apply(erule meta_allE)+
apply(erule meta_mp)
apply(rule refl)
apply(erule meta_allE)+
apply simp
done

lemma meta_all5_eq_conv: "(⋀a b c d e. a = f ⟹ PROP P a b c d e) ≡ (⋀b c d e. PROP P f b c d e)"
apply(rule equal_intr_rule)
apply(erule meta_allE)+
apply(erule meta_mp)
apply(rule refl)
apply(erule meta_allE)+
apply simp
done

"a ≤ b ⟹ sum f {..<(a :: nat)} + sum f {a..<b} = sum f {..<b}"
by (metis atLeast0LessThan le0 sum.atLeastLessThan_concat)

lemma nat_fun_sum_eq_conv:
fixes f :: "'a ⇒ nat"
shows "(λa. f a + g a) = (λa. 0) ⟷ f = (λa .0) ∧ g = (λa. 0)"

lemma in_ran_conv: "v ∈ ran m ⟷ (∃k. m k = Some v)"

lemma map_le_dom_eq_conv_eq:
"⟦ m ⊆⇩m m'; dom m = dom m' ⟧ ⟹ m = m'"
by (metis map_le_antisym map_le_def)

lemma map_leI:
"(⋀k v. f k = Some v ⟹ g k = Some v) ⟹ f ⊆⇩m g"
unfolding map_le_def by auto

lemma map_le_SomeD: "⟦ m ⊆⇩m m'; m x = ⌊y⌋ ⟧ ⟹ m' x = ⌊y⌋"
by(auto simp add: map_le_def dest: bspec)

lemma map_le_same_upd:
"f x = None ⟹ f ⊆⇩m f(x ↦ y)"

lemma map_upd_map_add: "X(V ↦ v) = (X ++ [V ↦ v])"
by(simp)

lemma foldr_filter_conv:
"foldr f (filter P xs) = foldr (λx s. if P x then f x s else s) xs"
by(induct xs)(auto intro: ext)

lemma foldr_insert_conv_set:
"foldr insert xs A = A ∪ set xs"
by(induct xs arbitrary: A) auto

lemma snd_o_Pair_conv_id: "snd o Pair a = id"

lemma if_intro:
"⟦ P ⟹ A; ¬ P ⟹ B ⟧ ⟹ if P then A else B"
by(auto)

lemma ex_set_conv: "(∃x. x ∈ set xs) ⟷ xs ≠ []"
apply(auto)
done

lemma subset_Un1: "A ⊆ B ⟹ A ⊆ B ∪ C" by blast
lemma subset_Un2: "A ⊆ C ⟹ A ⊆ B ∪ C" by blast
lemma subset_insert: "A ⊆ B ⟹ A ⊆ insert a B" by blast
lemma UNION_subsetD: "⟦ (⋃x∈A. f x) ⊆ B; a ∈ A ⟧ ⟹ f a ⊆ B" by blast

lemma Collect_eq_singleton_conv:
"{a. P a} = {a} ⟷ P a ∧ (∀a'. P a' ⟶ a = a')"
by(auto)

lemma Collect_conv_UN_singleton: "{f x|x. x ∈ P} = (⋃x∈P. {f x})"
by blast

lemma if_else_if_else_eq_if_else [simp]:
"(if b then x else if b then y else z) = (if b then x else z)"
by(simp)

lemma rec_prod_split [simp]: "old.rec_prod = case_prod"

lemma inj_Pair_snd [simp]: "inj (Pair x)"
by(rule injI) auto

lemma rtranclp_False [simp]: "(λa b. False)⇧*⇧* = (=)"
by(auto simp add: fun_eq_iff elim: rtranclp_induct)

lemmas rtranclp_induct3 =
rtranclp_induct[where a="(ax, ay, az)" and b="(bx, by, bz)", split_rule, consumes 1, case_names refl step]

lemmas tranclp_induct3 =
tranclp_induct[where a="(ax, ay, az)" and b="(bx, by, bz)", split_rule, consumes 1, case_names refl step]

lemmas rtranclp_induct4 =
rtranclp_induct[where a="(ax, ay, az, aw)" and b="(bx, by, bz, bw)", split_rule, consumes 1, case_names refl step]

lemmas tranclp_induct4 =
tranclp_induct[where a="(ax, ay, az, aw)" and b="(bx, by, bz, bw)", split_rule, consumes 1, case_names refl step]

lemmas converse_tranclp_induct2 =
converse_tranclp_induct [of _ "(ax,ay)" "(bx,by)", split_rule,
consumes 1, case_names base step]

lemma wfP_induct' [consumes 1, case_names wfP]:
"⟦wfP r; ⋀x. (⋀y. r y x ⟹ P y) ⟹ P x⟧ ⟹ P a"
by(blast intro: wfP_induct)

lemma wfP_induct2 [consumes 1, case_names wfP]:
"⟦wfP r; ⋀x x'. (⋀y y'. r (y, y') (x, x') ⟹ P y y') ⟹ P x x' ⟧ ⟹ P x x'"
by(drule wfP_induct'[where P="λ(x, y). P x y"]) blast+

lemma wfP_minimalE:
assumes "wfP r"
and "P x"
obtains z where "P z" "r^** z x" "⋀y. r y z ⟹ ¬ P y"
proof -
let ?Q = "λx'. P x' ∧ r^** x' x"
from ‹P x› have "?Q x" by blast
from ‹wfP r› have "⋀Q. x ∈ Q ⟶ (∃z∈Q. ∀y. r y z ⟶ y ∉ Q)"
unfolding wfP_eq_minimal by blast
from this[rule_format, of "Collect ?Q"] ‹?Q x›
obtain z where "?Q z" and min: "⋀y. r y z ⟹ ¬ ?Q y" by auto
from ‹?Q z› have "P z" "r^** z x" by auto
moreover
{ fix y
assume "r y z"
hence "¬ ?Q y" by(rule min)
moreover from ‹r y z› ‹r^** z x› have "r^** y x"
by(rule converse_rtranclp_into_rtranclp)
ultimately have "¬ P y" by blast }
ultimately show thesis ..
qed

lemma coinduct_set_wf [consumes 3, case_names coinduct, case_conclusion coinduct wait step]:
assumes "mono f" "wf r" "(a, b) ∈ X"
and step: "⋀x b. (x, b) ∈ X ⟹ (∃b'. (b', b) ∈ r ∧ (x, b') ∈ X) ∨ (x ∈ f (fst ` X ∪ gfp f))"
shows "a ∈ gfp f"
proof -
from ‹(a, b) ∈ X› have "a ∈ fst ` X" by(auto intro: rev_image_eqI)
moreover
{ fix a b
assume "(a, b) ∈ X"
with ‹wf r› have "a ∈ f (fst ` X ∪ gfp f)"
by(induct)(blast dest: step) }
hence "fst ` X ⊆ f (fst ` X ∪ gfp f)" by(auto)
ultimately show ?thesis by(rule coinduct_set[OF ‹mono f›])
qed

subsection ‹reflexive transitive closure for label relations›

inductive converse3p :: "('a ⇒ 'b ⇒ 'c ⇒ bool) ⇒ 'c ⇒ 'b ⇒ 'a ⇒ bool"
for r :: "'a ⇒ 'b ⇒ 'c ⇒ bool"
where
converse3pI: "r a b c ⟹ converse3p r c b a"

lemma converse3p_converse3p: "converse3p (converse3p r) = r"
by(auto intro: converse3pI intro!: ext elim: converse3p.cases)

lemma converse3pD: "converse3p r c b a ⟹ r a b c"
by(auto elim: converse3p.cases)

inductive rtrancl3p :: "('a ⇒ 'b ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'b list ⇒ 'a ⇒ bool"
for r :: "'a ⇒ 'b ⇒ 'a ⇒ bool"
where
rtrancl3p_refl [intro!, simp]: "rtrancl3p r a [] a"
| rtrancl3p_step: "⟦ rtrancl3p r a bs a'; r a' b a'' ⟧ ⟹ rtrancl3p r a (bs @ [b]) a''"

lemmas rtrancl3p_induct3 =
rtrancl3p.induct[of _ "(ax,ay,az)" _ "(cx,cy,cz)", split_format (complete),
consumes 1, case_names refl step]

lemmas rtrancl3p_induct4 =
rtrancl3p.induct[of _ "(ax,ay,az,aw)" _ "(cx,cy,cz,cw)", split_format (complete),
consumes 1, case_names refl step]

lemma rtrancl3p_induct4' [consumes 1, case_names refl step]:
assumes major: "rtrancl3p r (ax, (ay, az), aw) bs (cx, (cy, cz), cw)"
and refl: "⋀a aa b ba. P a aa b ba [] a aa b ba"
and step: "⋀a aa b ba bs ab ac bb bc bd ad ae be bf.
⟦ rtrancl3p r (a, (aa, b), ba) bs (ab, (ac, bb), bc);
P a aa b ba bs ab ac bb bc; r (ab, (ac, bb), bc) bd (ad, (ae, be), bf) ⟧
⟹ P a aa b ba (bs @ [bd]) ad ae be bf"
shows "P ax ay az aw bs cx cy cz cw"
using major
apply -
apply(drule_tac P="λ(a, (aa, b), ba) bs (cx, (cy, cz), cw). P a aa b ba bs cx cy cz cw" in rtrancl3p.induct)
by(auto intro: refl step)

lemma rtrancl3p_induct1:
"⟦ rtrancl3p r a bs c; P a; ⋀bs c b d. ⟦ rtrancl3p r a bs c; r c b d; P c ⟧ ⟹ P d ⟧ ⟹ P c"
apply(induct rule: rtrancl3p.induct)
apply(auto)
done

inductive_cases rtrancl3p_cases:
"rtrancl3p r x [] y"
"rtrancl3p r x (b # bs) y"

lemma rtrancl3p_trans [trans]:
assumes one: "rtrancl3p r a bs a'"
and two: "rtrancl3p r a' bs' a''"
shows "rtrancl3p r a (bs @ bs') a''"
using two one
proof(induct rule: rtrancl3p.induct)
case rtrancl3p_refl thus ?case by simp
next
case rtrancl3p_step thus ?case
by(auto simp only: append_assoc[symmetric] intro: rtrancl3p.rtrancl3p_step)
qed

lemma rtrancl3p_step_converse:
assumes step: "r a b a'"
and stepify: "rtrancl3p r a' bs a''"
shows "rtrancl3p r a (b # bs) a''"
using stepify step
proof(induct rule: rtrancl3p.induct)
case rtrancl3p_refl
with rtrancl3p.rtrancl3p_refl[where r=r and a=a] show ?case
by(auto dest: rtrancl3p.rtrancl3p_step simp del: rtrancl3p.rtrancl3p_refl)
next
case rtrancl3p_step thus ?case
unfolding append_Cons[symmetric]
by -(rule rtrancl3p.rtrancl3p_step)
qed

lemma converse_rtrancl3p_step:
"rtrancl3p r a (b # bs) a'' ⟹ ∃a'. r a b a' ∧ rtrancl3p r a' bs a''"
apply(induct bs arbitrary: a'' rule: rev_induct)
apply(erule rtrancl3p.cases)
apply(clarsimp)+
apply(erule rtrancl3p.cases)
apply(clarsimp)
apply(rule_tac x="a''a" in exI)
apply(clarsimp)
apply(clarsimp)
apply(erule rtrancl3p.cases)
apply(clarsimp)
apply(clarsimp)
by(fastforce intro: rtrancl3p_step)

lemma converse_rtrancl3pD:
"rtrancl3p (converse3p r) a' bs a ⟹ rtrancl3p r a (rev bs) a'"
apply(induct rule: rtrancl3p.induct)
apply(fastforce intro: rtrancl3p.intros)
apply(auto dest: converse3pD intro: rtrancl3p_step_converse)
done

lemma rtrancl3p_converseD:
"rtrancl3p r a bs a' ⟹ rtrancl3p (converse3p r) a' (rev bs) a"
proof(induct rule: rtrancl3p.induct)
case rtrancl3p_refl thus ?case
by(auto intro: rtrancl3p.intros)
next
case rtrancl3p_step thus ?case
by(auto intro: rtrancl3p_step_converse converse3p.intros)
qed

lemma rtrancl3p_converse_induct [consumes 1, case_names refl step]:
assumes ih: "rtrancl3p r a bs a''"
and refl: "⋀a. P a [] a"
and step: "⋀a b a' bs a''. ⟦ rtrancl3p r a' bs a''; r a b a'; P a' bs a'' ⟧ ⟹ P a (b # bs) a''"
shows "P a bs a''"
using ih
proof(induct bs arbitrary: a a'')
case Nil thus ?case
by(auto elim: rtrancl3p.cases intro: refl)
next
case Cons thus ?case
by(auto dest!: converse_rtrancl3p_step intro: step)
qed

lemma rtrancl3p_converse_induct' [consumes 1, case_names refl step]:
assumes ih: "rtrancl3p r a bs a''"
and refl: "P a'' []"
and step: "⋀a b a' bs. ⟦ rtrancl3p r a' bs a''; r a b a'; P a' bs ⟧ ⟹ P a (b # bs)"
shows "P a bs"
using rtrancl3p_converse_induct[OF ih, where P="λa bs a'. a' = a'' ⟶ P a bs"]
by(auto intro: refl step)

lemma rtrancl3p_converseE[consumes 1, case_names refl step]:
"⟦ rtrancl3p r a bs a'';
⟦ a = a''; bs = [] ⟧ ⟹ thesis;
⋀bs' b a'. ⟦ bs = b # bs'; r a b a'; rtrancl3p r a' bs' a'' ⟧ ⟹ thesis ⟧
⟹ thesis"
by(induct rule: rtrancl3p_converse_induct)(auto)

lemma rtrancl3p_induct' [consumes 1, case_names refl step]:
assumes major: "rtrancl3p r a bs c"
and refl: "P a [] a"
and step: "⋀bs a' b a''. ⟦ rtrancl3p r a bs a'; P a bs a'; r a' b a'' ⟧
⟹ P a (bs @ [b]) a''"
shows "P a bs c"
proof -
from major have "(P a [] a ∧ (∀bs a' b a''. rtrancl3p r a bs a' ∧ P a bs a' ∧ r a' b a'' ⟶ P a (bs @ [b]) a'')) ⟶ P a bs c"
by-(erule rtrancl3p.induct, blast+)
with refl step show ?thesis by blast
qed

lemma r_into_rtrancl3p:
"r a b a' ⟹ rtrancl3p r a [b] a'"
by(rule rtrancl3p_step_converse) auto

lemma rtrancl3p_appendE:
assumes "rtrancl3p r a (bs @ bs') a''"
obtains a' where "rtrancl3p r a bs a'" "rtrancl3p r a' bs' a''"
using assms
apply(induct a "bs @ bs'" arbitrary: bs rule: rtrancl3p_converse_induct')
apply(fastforce intro: rtrancl3p_step_converse simp add: Cons_eq_append_conv)+
done

lemma rtrancl3p_Cons:
"rtrancl3p r a (b # bs) a' ⟷ (∃a''. r a b a'' ∧ rtrancl3p r a'' bs a')"
by(auto intro: rtrancl3p_step_converse converse_rtrancl3p_step)

lemma rtrancl3p_Nil:
"rtrancl3p r a [] a' ⟷ a = a'"
by(auto elim: rtrancl3p_cases)

definition invariant3p :: "('a ⇒ 'b ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ bool"
where "invariant3p r I ⟷ (∀s tl s'. s ∈ I ⟶ r s tl s' ⟶ s' ∈ I)"

lemma invariant3pI: "(⋀s tl s'. ⟦ s ∈ I; r s tl s' ⟧ ⟹ s' ∈ I) ⟹ invariant3p r I"
unfolding invariant3p_def by blast

lemma invariant3pD: "⋀tl. ⟦ invariant3p r I; r s tl s'; s ∈ I ⟧ ⟹ s' ∈ I"
unfolding invariant3p_def by(blast)

lemma invariant3p_rtrancl3p:
assumes inv: "invariant3p r I"
and rtrancl: "rtrancl3p r a bs a'"
and start: "a ∈ I"
shows "a' ∈ I"
using rtrancl start by(induct)(auto dest: invariant3pD[OF inv])

lemma invariant3p_UNIV [simp, intro!]:
"invariant3p r UNIV"
by(blast intro: invariant3pI)

lemma invarinat3p_empty [simp, intro!]:
"invariant3p r {}"
by(blast intro: invariant3pI)

lemma invariant3p_IntI [simp, intro]:
"⟦ invariant3p r I; invariant3p r J ⟧ ⟹ invariant3p r (I ∩ J)"
by(blast dest: invariant3pD intro: invariant3pI)

subsection ‹Concatenation for @{typ String.literal}›

definition concat :: "String.literal list ⇒ String.literal"
where [code_abbrev, code del]: "concat = sum_list"