(*  Title:      JinjaThreads/Basic/Set_without_equal.thy
    Author:     Andreas Lochbihler
*)

theory Set_without_equal
imports Main
begin

text ‹
  Adapt @{type "set"} code setup such that @{const "insert"}, 
  @{const "union"}, and @{term "set_of_pred"} do not generate
  sort constraint @{class equal}.
›

definition insert' :: "'a ⇒ 'a set ⇒ 'a set"
where "insert' = Set.insert"

definition union' :: "'a set ⇒ 'a set ⇒ 'a set"
where "union' A B = sup A B"

declare
  insert'_def [symmetric, code_unfold]
  union'_def [symmetric, code_unfold]

lemma insert'_code:
  "insert' x (set xs) = set (x # xs)"
  by (rule set_eqI) (simp add: insert'_def)

lemma union'_code:
  "union' (set xs) (set ys) = set (xs @ ys)"
  by (rule set_eqI) (simp add: union'_def fun_eq_iff)

declare
  insert'_code [code]
  union'_code [code]

text ‹Merge name spaces to avoid cyclic module dependencies›

code_identifier
  code_module Set_without_equal ⇀
    (SML) Set and (Haskell) Set and (OCaml) Set

end

theory Set_Monad
imports 
  Main
  "HOL-Library.Monad_Syntax"
begin

lemma member_SUP: (* FIXME delete candidate: should be subsumed by default simpset as soon as SUP_apply is included *)
  "x ∈ ⋃(f ` A) = (SUP B∈A. (λx. x ∈ f B)) x"
  by auto

abbreviation (input) "of_pred == Predicate.set_of_pred" (* FIXME delte alias *)
abbreviation (input) "of_seq == Predicate.set_of_seq" (* FIXME delte alias *)

lemmas bind_def = Set.bind_def (* FIXME delte alias *)
lemmas bind_bind = Set.bind_bind (* FIXME delte alias *)
lemmas empty_bind = Set.empty_bind (* FIXME delte alias *)
lemmas bind_const = Set.bind_const (* FIXME delte alias *)
lemmas member_of_pred = Predicate.member_set_of_pred (* FIXME delte alias *)
lemmas member_of_seq = Predicate.member_set_of_seq (* FIXME delte alias *)

definition single :: "'a ⇒ 'a set"
  where "single a = {a}"

definition undefined :: "'a set"
  where [simp]: "undefined = Collect HOL.undefined"

declare [[code abort: undefined]]

definition Undefined :: "unit ⇒ 'a set"
  where "Undefined _ = Collect HOL.undefined"

declare [[code abort: Undefined]]

lemma undefined_code [code_unfold]:
  "undefined = Undefined ()"
  by (simp add: Undefined_def)

lemma bind_single [simp, code_unfold]:
  "A ⤜ single = A"
  by (simp add: bind_def single_def)

lemma single_bind [simp, code_unfold]:
  "single a ⤜ B = B a"
  by (simp add: bind_def single_def)

declare Set.empty_bind [code_unfold]

lemma member_single [simp]:
  "x ∈ single a ⟷ x = a"
by (simp add: single_def)

lemma single_sup_simps [simp, code_unfold]:
  shows single_sup: "sup (single a) A = insert a A"
  and sup_single: "sup A (single a) = insert a A"
  by (unfold set_eq_iff) auto

lemma single_code [code]:
  "single a = set [a]"
  by (simp add: set_eq_iff)

end

section ‹Adapting the Isabelle Collection Framework for Jinja Threads›
theory JT_ICF
imports Collections.CollectionsV1
begin

  text ‹Hide stuff that may lead to confusions later›

  hide_const (open) Array
  hide_type (open) array

end

(*  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.Monad_Syntax"
  "HOL-Library.Infinite_Set"
  FinFun.FinFun
begin

unbundle finfun_syntax

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

lemma Suc_add_max_le[simp]:
  "(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"
by(auto simp add: min_def order_less_imp_le)

lemma less_min_eq2:
  "(a :: 'a :: order) > b ⟹ min a b = b"
by(auto simp add: min_def order_less_imp_le)

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 Option_bind_eq_Some_conv:
  "x ⤜ y = Some z ⟷ (∃x'. x = Some x' ∧ y x' = Some z)"
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 simp:fun_upd_apply)(*>*)

lemma rel_option_Some1:
  "rel_option R (Some x) y ⟷ (∃y'. y = Some y' ∧ R x y')"
by(cases y) simp_all

lemma rel_option_Some2:
  "rel_option R x (Some y) ⟷ (∃x'. x = Some x' ∧ R x' y)"
by(cases x) simp_all

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"
  (*<*)by (simp add: list_all2_refl)(*>*)

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])"
  (*<*)by (simp add: list_all2_update_cong)(*>*)

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_induct[consumes 1, case_names Nil Cons]:
  assumes major: "list_all2 P xs ys"
  and Nil: "Q [] []"
  and Cons: "⋀x xs y ys. ⟦ P x y; list_all2 P xs ys; Q xs ys ⟧ ⟹ Q (x # xs) (y # ys)"
  shows "Q xs ys"
using major
by(induct xs arbitrary: ys)(auto simp add: list_all2_Cons1 Nil intro!: Cons)

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_refl_conv:
  "list_all2 P xs xs ⟷ (∀x∈set xs. P x x)"
unfolding list_all2_conv_all_nth Ball_def in_set_conv_nth
by auto

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 nth_Cons_subtract: "0 < n ⟹ (x # xs) ! n = xs ! (n - 1)"
by(auto simp add: nth_Cons split: nat.split)

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)
 apply(simp add: nth_append)
apply(simp add: nth_append)
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"
      by(simp add: replicate_add[THEN sym])
  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)
apply(auto simp add: list_all2_Cons1 Cons_eq_map_conv)
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 take_list_update_beyond:
  "n ≤ m ⟹ take n (xs[m := x]) = take n xs"
by(cases "n ≤ length xs")(rule nth_take_lemma, simp_all)

lemma hd_drop_conv_nth:
  "n < length xs ⟹ hd (drop n xs) = xs ! n"
by(rule hd_drop_conv_nth) (metis list.size(3) not_less0)

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 takeWhile_eq_Nil_conv:
  "takeWhile P xs = [] ⟷ (xs = [] ∨ ¬ P (hd xs))"
by(cases xs) simp_all

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 takeWhile_takeWhile: "takeWhile P (takeWhile Q xs) = takeWhile (λx. P x ∧ Q x) xs"
by(induct xs) simp_all

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 append_is_Nil_conv dropWhile_eq_Cons_conv list.sel(1) neq_Nil_conv takeWhile_dropWhile_id takeWhile_eq_Nil_conv list.sel(3))

lemma dropWhile_eq_same_conv: "dropWhile P xs = xs ⟷ (xs = [] ∨ ¬ P (hd xs))"
by (metis dropWhile.simps(1) eq_Nil_appendI hd_dropWhile takeWhile_dropWhile_id takeWhile_eq_Nil_conv)

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)"
by(auto simp add: fun_eq_iff)

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)"
apply(auto simp add: disj_split[of P])
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

lemma inj_on_image_mem_iff:
  "⟦ inj_on f A; B ⊆ A; a ∈ A ⟧ ⟹ f a ∈ f ` B ⟷ a ∈ B"
by(metis inv_into_f_eq inv_into_image_cancel rev_image_eqI)

lemma sum_hom:
  assumes hom_add [simp]: "⋀a b. f (a + b) = f a + f b"
  and hom_0 [simp]: "f 0 = 0"
  shows "sum (f ∘ h) A = f (sum h A)"
proof(cases "finite A")
  case False thus ?thesis by simp
next
  case True thus ?thesis
    by(induct) simp_all
qed

lemma sum_upto_add_nat:
  "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)"
by(auto simp add: fun_eq_iff)


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

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)"
by(auto simp add: map_le_def)

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"
by(simp add: o_def id_def)

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)
apply(auto simp add: neq_Nil_conv)
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"
by(simp add: fun_eq_iff)

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"

lemma explode_add [simp]:
  "String.explode (s + t) = String.explode s @ String.explode t"
  by (fact plus_literal.rep_eq)

code_printing
  constant concat ⇀
    (SML) "String.concat"
    and (Haskell) "concat"
    and (OCaml) "String.concat \"\""

hide_const (open) concat

end