[STATEMENT]
lemma wf_sig_imp_exe_wf_sig:
  assumes "alist_conds cto" "alist_conds tao" "exe_osig_conds sa"
    "wf_sig (map_of cto, map_of tao, translate_osig sa)"
  shows "(exe_wf_osig sa
    \<and> fst ` set (exetcsigs sa) = fst ` set tao
    \<and> (\<forall>type \<in> fst ` set (exetcsigs sa).
        (\<forall>ars \<in> snd ` set (the (lookup (\<lambda>k. k=type) (exetcsigs sa))) .
        the (lookup (\<lambda>k. k=type) tao) = length ars)))
    \<and> (\<forall>ty \<in> snd ` set cto . typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
fix a b x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
assume p: "alist_conds tao"
      "exe_ars_conds b"
      "dom (map_of (map (apsnd map_of) b)) = dom (map_of tao)"
      "(x, y) \<in> set b"
[PROOF STATE]
proof (state)
this:
alist_conds tao
exe_ars_conds b
dom (map_of (map (apsnd map_of) b)) = dom (map_of tao)
(x, y) \<in> set b

goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
hence "x \<in> fst ` set tao"
[PROOF STATE]
proof (prove)
using this:
alist_conds tao
exe_ars_conds b
dom (map_of (map (apsnd map_of) b)) = dom (map_of tao)
(x, y) \<in> set b

goal (1 subgoal):
 1. x \<in> fst ` set tao
[PROOF STEP]
by (metis domIff dom_map_of_conv_image_fst exe_ars_conds_def
          in_alist_imp_in_map_of option.distinct(1) translate_ars.simps)
[PROOF STATE]
proof (state)
this:
x \<in> fst ` set tao

goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>alist_conds tao; exe_ars_conds ?b2; dom (map_of (map (apsnd map_of) ?b2)) = dom (map_of tao); (?x2, ?y2) \<in> set ?b2\<rbrakk> \<Longrightarrow> ?x2 \<in> fst ` set tao

goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
note 1 = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>alist_conds tao; exe_ars_conds ?b2; dom (map_of (map (apsnd map_of) ?b2)) = dom (map_of tao); (?x2, ?y2) \<in> set ?b2\<rbrakk> \<Longrightarrow> ?x2 \<in> fst ` set tao

goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>alist_conds tao; exe_ars_conds ?b2; dom (map_of (map (apsnd map_of) ?b2)) = dom (map_of tao); (?x2, ?y2) \<in> set ?b2\<rbrakk> \<Longrightarrow> ?x2 \<in> fst ` set tao

goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
fix cl n ar and tcs :: "(String.literal \<times> (String.literal \<times> String.literal set list) list) list"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
assume p: "dom (map_of (map (apsnd map_of) tcs)) = dom (map_of tao)"
      "alist_conds tao"
      "(n, ar) \<in> set tao"
[PROOF STATE]
proof (state)
this:
dom (map_of (map (apsnd map_of) tcs)) = dom (map_of tao)
alist_conds tao
(n, ar) \<in> set tao

goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
obtain mgd where "translate_ars tcs n = Some mgd"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>mgd. translate_ars tcs n = Some mgd \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
dom (map_of (map (apsnd map_of) tcs)) = dom (map_of tao)
alist_conds tao
(n, ar) \<in> set tao

goal (1 subgoal):
 1. (\<And>mgd. translate_ars tcs n = Some mgd \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis Some_eq_map_of_iff domI domIff option.exhaust_sel translate_ars.simps)
[PROOF STATE]
proof (state)
this:
translate_ars tcs n = Some mgd

goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
hence "map_of (map (apsnd map_of) tcs) n = Some mgd"
[PROOF STATE]
proof (prove)
using this:
translate_ars tcs n = Some mgd

goal (1 subgoal):
 1. map_of (map (apsnd map_of) tcs) n = Some mgd
[PROOF STEP]
by (simp add: tcsigs_translate exe_osig_conds_def p)
[PROOF STATE]
proof (state)
this:
map_of (map (apsnd map_of) tcs) n = Some mgd

goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
hence "n \<in> fst ` set (map (apsnd map_of) tcs)"
[PROOF STATE]
proof (prove)
using this:
map_of (map (apsnd map_of) tcs) n = Some mgd

goal (1 subgoal):
 1. n \<in> fst ` set (map (apsnd map_of) tcs)
[PROOF STEP]
by (meson domI domIff map_of_eq_None_iff)
[PROOF STATE]
proof (state)
this:
n \<in> fst ` set (map (apsnd map_of) tcs)

goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<in> fst ` set (map (apsnd map_of) tcs)
[PROOF STEP]
have "n \<in> fst ` set tcs"
[PROOF STATE]
proof (prove)
using this:
n \<in> fst ` set (map (apsnd map_of) tcs)

goal (1 subgoal):
 1. n \<in> fst ` set tcs
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
n \<in> fst ` set tcs

goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>dom (map_of (map (apsnd map_of) ?tcs2)) = dom (map_of tao); alist_conds tao; (?n2, ?ar2) \<in> set tao\<rbrakk> \<Longrightarrow> ?n2 \<in> fst ` set ?tcs2

goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
note 2 = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>dom (map_of (map (apsnd map_of) ?tcs2)) = dom (map_of tao); alist_conds tao; (?n2, ?ar2) \<in> set tao\<rbrakk> \<Longrightarrow> ?n2 \<in> fst ` set ?tcs2

goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>dom (map_of (map (apsnd map_of) ?tcs2)) = dom (map_of tao); alist_conds tao; (?n2, ?ar2) \<in> set tao\<rbrakk> \<Longrightarrow> ?n2 \<in> fst ` set ?tcs2

goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
fix cl tcs n K c Ss
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
assume p: "(n, K) \<in> set tcs"
      "(c, Ss) \<in> set (the (lookup (\<lambda>k. k = n) tcs))"
      "exe_ars_conds tcs"
      "dom (map_of (map (apsnd map_of) tcs)) = dom (map_of tao)"
      "\<forall>type\<in>dom (map_of tao). \<forall>ars\<in>ran (the (map_of (map (apsnd map_of) tcs) type)).
          the (map_of tao type) = length ars"
[PROOF STATE]
proof (state)
this:
(n, K) \<in> set tcs
(c, Ss) \<in> set (the (lookup (\<lambda>k. k = n) tcs))
exe_ars_conds tcs
dom (map_of (map (apsnd map_of) tcs)) = dom (map_of tao)
\<forall>type\<in>dom (map_of tao). \<forall>ars\<in>ran (the (map_of (map (apsnd map_of) tcs) type)). the (map_of tao type) = length ars

goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
have 1: "translate_ars tcs n = Some (map_of K)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. translate_ars tcs n = Some (map_of K)
[PROOF STEP]
using exe_ars_conds_def in_alist_imp_in_map_of p(1-3)
[PROOF STATE]
proof (prove)
using this:
exe_ars_conds ?arss = (alist_conds ?arss \<and> (\<forall>ars\<in>snd ` set ?arss. alist_conds ars))
\<lbrakk>alist_conds ?arss; (?name, ?ars) \<in> set ?arss\<rbrakk> \<Longrightarrow> translate_ars ?arss ?name = Some (map_of ?ars)
(n, K) \<in> set tcs
(c, Ss) \<in> set (the (lookup (\<lambda>k. k = n) tcs))
exe_ars_conds tcs

goal (1 subgoal):
 1. translate_ars tcs n = Some (map_of K)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
translate_ars tcs n = Some (map_of K)

goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
have 2: "map_of K c = Some Ss"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of K c = Some Ss
[PROOF STEP]
using p(1-3)
[PROOF STATE]
proof (prove)
using this:
(n, K) \<in> set tcs
(c, Ss) \<in> set (the (lookup (\<lambda>k. k = n) tcs))
exe_ars_conds tcs

goal (1 subgoal):
 1. map_of K c = Some Ss
[PROOF STEP]
by (metis Some_eq_map_of_iff exe_ars_conds_def image_iff lookup_eq_map_of_ap
          option.sel snd_conv)
[PROOF STATE]
proof (state)
this:
map_of K c = Some Ss

goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
have "the (lookup (\<lambda>k. k = n) tao) = length Ss"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the (lookup (\<lambda>k. k = n) tao) = length Ss
[PROOF STEP]
using 1 2 p(4,5)
[PROOF STATE]
proof (prove)
using this:
translate_ars tcs n = Some (map_of K)
map_of K c = Some Ss
dom (map_of (map (apsnd map_of) tcs)) = dom (map_of tao)
\<forall>type\<in>dom (map_of tao). \<forall>ars\<in>ran (the (map_of (map (apsnd map_of) tcs) type)). the (map_of tao type) = length ars

goal (1 subgoal):
 1. the (lookup (\<lambda>k. k = n) tao) = length Ss
[PROOF STEP]
by (metis domIff lookup_eq_map_of_ap option.distinct(1) option.sel ranI translate_ars.simps)
[PROOF STATE]
proof (state)
this:
the (lookup (\<lambda>k. k = n) tao) = length Ss

goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?n2, ?K2) \<in> set ?tcs2; (?c2, ?Ss2) \<in> set (the (lookup (\<lambda>k. k = ?n2) ?tcs2)); exe_ars_conds ?tcs2; dom (map_of (map (apsnd map_of) ?tcs2)) = dom (map_of tao); \<forall>type\<in>dom (map_of tao). \<forall>ars\<in>ran (the (map_of (map (apsnd map_of) ?tcs2) type)). the (map_of tao type) = length ars\<rbrakk> \<Longrightarrow> the (lookup (\<lambda>k. k = ?n2) tao) = length ?Ss2

goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
note 3 = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?n2, ?K2) \<in> set ?tcs2; (?c2, ?Ss2) \<in> set (the (lookup (\<lambda>k. k = ?n2) ?tcs2)); exe_ars_conds ?tcs2; dom (map_of (map (apsnd map_of) ?tcs2)) = dom (map_of tao); \<forall>type\<in>dom (map_of tao). \<forall>ars\<in>ran (the (map_of (map (apsnd map_of) ?tcs2) type)). the (map_of tao type) = length ars\<rbrakk> \<Longrightarrow> the (lookup (\<lambda>k. k = ?n2) tao) = length ?Ss2

goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
have 1: "wf_osig (translate_osig sa)" "dom (tcsigs (translate_osig sa)) = dom (map_of tao)"
    "(\<forall>type \<in> dom (tcsigs (translate_osig sa)).
    (\<forall>ars \<in> ran (the (tcsigs (translate_osig sa) type)) . the ((map_of tao) type) = length ars))"
    "(\<forall>ty \<in> Map.ran (map_of cto) . wf_type (map_of cto, map_of tao, translate_osig sa) ty)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (wf_osig (translate_osig sa) &&& dom (tcsigs (translate_osig sa)) = dom (map_of tao)) &&& \<forall>type\<in>dom (tcsigs (translate_osig sa)). \<forall>ars\<in>ran (the (tcsigs (translate_osig sa) type)). the (map_of tao type) = length ars &&& \<forall>ty\<in>ran (map_of cto). wf_type (map_of cto, map_of tao, translate_osig sa) ty
[PROOF STEP]
using assms(4)
[PROOF STATE]
proof (prove)
using this:
wf_sig (map_of cto, map_of tao, translate_osig sa)

goal (1 subgoal):
 1. (wf_osig (translate_osig sa) &&& dom (tcsigs (translate_osig sa)) = dom (map_of tao)) &&& \<forall>type\<in>dom (tcsigs (translate_osig sa)). \<forall>ars\<in>ran (the (tcsigs (translate_osig sa) type)). the (map_of tao type) = length ars &&& \<forall>ty\<in>ran (map_of cto). wf_type (map_of cto, map_of tao, translate_osig sa) ty
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wf_osig (translate_osig sa)
dom (tcsigs (translate_osig sa)) = dom (map_of tao)
\<forall>type\<in>dom (tcsigs (translate_osig sa)). \<forall>ars\<in>ran (the (tcsigs (translate_osig sa) type)). the (map_of tao type) = length ars
\<forall>ty\<in>ran (map_of cto). wf_type (map_of cto, map_of tao, translate_osig sa) ty

goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
note pre = 1
[PROOF STATE]
proof (state)
this:
wf_osig (translate_osig sa)
dom (tcsigs (translate_osig sa)) = dom (map_of tao)
\<forall>type\<in>dom (tcsigs (translate_osig sa)). \<forall>ars\<in>ran (the (tcsigs (translate_osig sa) type)). the (map_of tao type) = length ars
\<forall>ty\<in>ran (map_of cto). wf_type (map_of cto, map_of tao, translate_osig sa) ty

goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
have "exe_wf_osig sa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exe_wf_osig sa
[PROOF STEP]
using "1"(1) wf_osig_iff_exe_wf_osig
[PROOF STATE]
proof (prove)
using this:
wf_osig (translate_osig sa)
wf_osig (translate_osig ?oss) = exe_wf_osig ?oss

goal (1 subgoal):
 1. exe_wf_osig sa
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
exe_wf_osig sa

goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
exe_wf_osig sa

goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
have "fst ` set (snd sa) = fst ` set tao"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` set (snd sa) = fst ` set tao
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. fst ` set (snd sa) \<subseteq> fst ` set tao
 2. fst ` set tao \<subseteq> fst ` set (snd sa)
[PROOF STEP]
show "fst ` set (snd sa) \<subseteq> fst ` set tao"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` set (snd sa) \<subseteq> fst ` set tao
[PROOF STEP]
using assms(3-4)
[PROOF STATE]
proof (prove)
using this:
exe_osig_conds sa
wf_sig (map_of cto, map_of tao, translate_osig sa)

goal (1 subgoal):
 1. fst ` set (snd sa) \<subseteq> fst ` set tao
[PROOF STEP]
by (clarsimp simp add: dom_map_of_conv_image_fst exe_ars_conds_def exe_osig_conds_def)
        (metis tcsigs_translate assms(3) domIff in_alist_imp_in_map_of option.simps(3))
[PROOF STATE]
proof (state)
this:
fst ` set (snd sa) \<subseteq> fst ` set tao

goal (1 subgoal):
 1. fst ` set tao \<subseteq> fst ` set (snd sa)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fst ` set tao \<subseteq> fst ` set (snd sa)
[PROOF STEP]
show "fst ` set (snd sa) \<supseteq> fst ` set tao"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` set tao \<subseteq> fst ` set (snd sa)
[PROOF STEP]
using "1"(2) "2" assms(2-3) tcsigs_translate
[PROOF STATE]
proof (prove)
using this:
dom (tcsigs (translate_osig sa)) = dom (map_of tao)
\<lbrakk>dom (map_of (map (apsnd map_of) ?tcs2)) = dom (map_of tao); alist_conds tao; (?n2, ?ar2) \<in> set tao\<rbrakk> \<Longrightarrow> ?n2 \<in> fst ` set ?tcs2
alist_conds tao
exe_osig_conds sa
exe_osig_conds ?oss \<Longrightarrow> tcsigs (translate_osig ?oss) = translate_ars (snd ?oss)

goal (1 subgoal):
 1. fst ` set tao \<subseteq> fst ` set (snd sa)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst ` set tao \<subseteq> fst ` set (snd sa)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
fst ` set (snd sa) = fst ` set tao

goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
fst ` set (snd sa) = fst ` set tao

goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
have "(\<forall>type\<in>fst ` set (snd sa).  \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))).
        the (lookup (\<lambda>k. k = type) tao) = length ars)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars
[PROOF STEP]
proof (standard+, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>type ars. \<lbrakk>type \<in> fst ` set (snd sa); ars \<in> snd ` set (the (lookup (\<lambda>k. k = type) (snd sa)))\<rbrakk> \<Longrightarrow> the (lookup (\<lambda>k. k = type) tao) = length ars
[PROOF STEP]
case (1 n Ss)
[PROOF STATE]
proof (state)
this:
n \<in> fst ` set (snd sa)
Ss \<in> snd ` set (the (lookup (\<lambda>k. k = n) (snd sa)))

goal (1 subgoal):
 1. \<And>type ars. \<lbrakk>type \<in> fst ` set (snd sa); ars \<in> snd ` set (the (lookup (\<lambda>k. k = type) (snd sa)))\<rbrakk> \<Longrightarrow> the (lookup (\<lambda>k. k = type) tao) = length ars
[PROOF STEP]
obtain c where c: "(c, Ss) \<in> set (the (lookup (\<lambda>k. k = n) (snd sa)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c. (c, Ss) \<in> set (the (lookup (\<lambda>k. k = n) (snd sa))) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using "1"(2)
[PROOF STATE]
proof (prove)
using this:
Ss \<in> snd ` set (the (lookup (\<lambda>k. k = n) (snd sa)))

goal (1 subgoal):
 1. (\<And>c. (c, Ss) \<in> set (the (lookup (\<lambda>k. k = n) (snd sa))) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(c, Ss) \<in> set (the (lookup (\<lambda>k. k = n) (snd sa)))

goal (1 subgoal):
 1. \<And>type ars. \<lbrakk>type \<in> fst ` set (snd sa); ars \<in> snd ` set (the (lookup (\<lambda>k. k = type) (snd sa)))\<rbrakk> \<Longrightarrow> the (lookup (\<lambda>k. k = type) tao) = length ars
[PROOF STEP]
have "dom (map_of (map (apsnd map_of) (snd sa))) = dom (map_of tao)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (map_of (map (apsnd map_of) (snd sa))) = dom (map_of tao)
[PROOF STEP]
using assms(3) pre(2) tcsigs_translate
[PROOF STATE]
proof (prove)
using this:
exe_osig_conds sa
dom (tcsigs (translate_osig sa)) = dom (map_of tao)
exe_osig_conds ?oss \<Longrightarrow> tcsigs (translate_osig ?oss) = translate_ars (snd ?oss)

goal (1 subgoal):
 1. dom (map_of (map (apsnd map_of) (snd sa))) = dom (map_of tao)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
dom (map_of (map (apsnd map_of) (snd sa))) = dom (map_of tao)

goal (1 subgoal):
 1. \<And>type ars. \<lbrakk>type \<in> fst ` set (snd sa); ars \<in> snd ` set (the (lookup (\<lambda>k. k = type) (snd sa)))\<rbrakk> \<Longrightarrow> the (lookup (\<lambda>k. k = type) tao) = length ars
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the (lookup (\<lambda>k. k = n) tao) = length Ss
[PROOF STEP]
using assms(3) pre(2) c tcsigs_translate pre(2-3) domI
[PROOF STATE]
proof (prove)
using this:
exe_osig_conds sa
dom (tcsigs (translate_osig sa)) = dom (map_of tao)
(c, Ss) \<in> set (the (lookup (\<lambda>k. k = n) (snd sa)))
exe_osig_conds ?oss \<Longrightarrow> tcsigs (translate_osig ?oss) = translate_ars (snd ?oss)
dom (tcsigs (translate_osig sa)) = dom (map_of tao)
\<forall>type\<in>dom (tcsigs (translate_osig sa)). \<forall>ars\<in>ran (the (tcsigs (translate_osig sa) type)). the (map_of tao type) = length ars
?m ?a = Some ?b \<Longrightarrow> ?a \<in> dom ?m

goal (1 subgoal):
 1. the (lookup (\<lambda>k. k = n) tao) = length Ss
[PROOF STEP]
by (fastforce simp add: exe_osig_conds_def tcsigs_translate[OF assms(3)]
          "1"(1) key_present_imp_eq_lookup_finds_value lookup_present_eq_key'
          split: option.splits intro!: 3[of _ "the (lookup (\<lambda>k. k = n) (snd sa))" "snd sa" c])+
[PROOF STATE]
proof (state)
this:
the (lookup (\<lambda>k. k = n) tao) = length Ss

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars

goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars

goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
have "(\<forall>ty \<in> Map.ran (map_of cto) . wf_type (map_of cto, map_of tao, translate_osig sa) ty)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>ty\<in>ran (map_of cto). wf_type (map_of cto, map_of tao, translate_osig sa) ty
[PROOF STEP]
using "1"(4)
[PROOF STATE]
proof (prove)
using this:
\<forall>ty\<in>ran (map_of cto). wf_type (map_of cto, map_of tao, translate_osig sa) ty

goal (1 subgoal):
 1. \<forall>ty\<in>ran (map_of cto). wf_type (map_of cto, map_of tao, translate_osig sa) ty
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>ty\<in>ran (map_of cto). wf_type (map_of cto, map_of tao, translate_osig sa) ty

goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
exe_wf_osig sa
fst ` set (snd sa) = fst ` set tao
\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars
\<forall>ty\<in>ran (map_of cto). wf_type (map_of cto, map_of tao, translate_osig sa) ty
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
exe_wf_osig sa
fst ` set (snd sa) = fst ` set tao
\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars
\<forall>ty\<in>ran (map_of cto). wf_type (map_of cto, map_of tao, translate_osig sa) ty

goal (1 subgoal):
 1. (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
[PROOF STEP]
by (simp add: assms(1) ran_distinct)
[PROOF STATE]
proof (state)
this:
(exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wf_sig_iff_exe_wf_sig_pre: "alist_conds cto \<Longrightarrow> alist_conds tao \<Longrightarrow> exe_osig_conds sa
  \<Longrightarrow> wf_sig (map_of cto, map_of tao, translate_osig sa) = (exe_wf_osig sa
  \<and> fst ` set (exetcsigs sa) = fst ` set tao
  \<and> (\<forall>type \<in> fst ` set (exetcsigs sa).
      (\<forall>ars \<in> snd ` set (the (lookup (\<lambda>k. k=type) (exetcsigs sa))) .
      the (lookup (\<lambda>k. k=type) tao) = length ars))
  \<and> (\<forall>ty \<in> snd ` set cto . typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>alist_conds cto; alist_conds tao; exe_osig_conds sa\<rbrakk> \<Longrightarrow> wf_sig (map_of cto, map_of tao, translate_osig sa) = (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty))
[PROOF STEP]
using exe_wf_sig_imp_wf_sig wf_sig_imp_exe_wf_sig
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>alist_conds ?cto; alist_conds ?tao; exe_osig_conds ?sa; (exe_wf_osig ?sa \<and> fst ` set (snd ?sa) = fst ` set ?tao \<and> (\<forall>type\<in>fst ` set (snd ?sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd ?sa))). the (lookup (\<lambda>k. k = type) ?tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set ?cto. typ_ok_sig (map_of ?cto, map_of ?tao, translate_osig ?sa) ty)\<rbrakk> \<Longrightarrow> wf_sig (map_of ?cto, map_of ?tao, translate_osig ?sa)
\<lbrakk>alist_conds ?cto; alist_conds ?tao; exe_osig_conds ?sa; wf_sig (map_of ?cto, map_of ?tao, translate_osig ?sa)\<rbrakk> \<Longrightarrow> (exe_wf_osig ?sa \<and> fst ` set (snd ?sa) = fst ` set ?tao \<and> (\<forall>type\<in>fst ` set (snd ?sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd ?sa))). the (lookup (\<lambda>k. k = type) ?tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set ?cto. typ_ok_sig (map_of ?cto, map_of ?tao, translate_osig ?sa) ty)

goal (1 subgoal):
 1. \<lbrakk>alist_conds cto; alist_conds tao; exe_osig_conds sa\<rbrakk> \<Longrightarrow> wf_sig (map_of cto, map_of tao, translate_osig sa) = (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty))
[PROOF STEP]
by meson


[STATEMENT]
lemma wf_sig_iff_exe_wf_sig: "alist_conds cto \<Longrightarrow> alist_conds tao \<Longrightarrow> exe_osig_conds sa
  \<Longrightarrow> wf_sig (map_of cto, map_of tao, translate_osig sa)
  \<longleftrightarrow> exe_wf_sig (ExeSignature cto tao sa)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>alist_conds cto; alist_conds tao; exe_osig_conds sa\<rbrakk> \<Longrightarrow> wf_sig (map_of cto, map_of tao, translate_osig sa) = exe_wf_sig (ExeSignature cto tao sa)
[PROOF STEP]
unfolding exe_wf_sig.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>alist_conds cto; alist_conds tao; exe_osig_conds sa\<rbrakk> \<Longrightarrow> wf_sig (map_of cto, map_of tao, translate_osig sa) = (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars) \<and> Ball (snd ` set cto) (typ_ok_sig (map_of cto, map_of tao, translate_osig sa)))
[PROOF STEP]
using wf_sig_iff_exe_wf_sig_pre
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>alist_conds ?cto; alist_conds ?tao; exe_osig_conds ?sa\<rbrakk> \<Longrightarrow> wf_sig (map_of ?cto, map_of ?tao, translate_osig ?sa) = (exe_wf_osig ?sa \<and> fst ` set (snd ?sa) = fst ` set ?tao \<and> (\<forall>type\<in>fst ` set (snd ?sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd ?sa))). the (lookup (\<lambda>k. k = type) ?tao) = length ars) \<and> (\<forall>ty\<in>snd ` set ?cto. typ_ok_sig (map_of ?cto, map_of ?tao, translate_osig ?sa) ty))

goal (1 subgoal):
 1. \<lbrakk>alist_conds cto; alist_conds tao; exe_osig_conds sa\<rbrakk> \<Longrightarrow> wf_sig (map_of cto, map_of tao, translate_osig sa) = (exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars) \<and> Ball (snd ` set cto) (typ_ok_sig (map_of cto, map_of tao, translate_osig sa)))
[PROOF STEP]
by presburger


[STATEMENT]
lemma typ_arity_lookup_code: "type_arity (translate_signature \<Sigma>) n = lookup (\<lambda>k. k = n) (exetyp_arity_of \<Sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. type_arity (translate_signature \<Sigma>) n = lookup (\<lambda>k. k = n) (exetyp_arity_of \<Sigma>)
[PROOF STEP]
by (cases \<Sigma>) (simp add: lookup_eq_map_of_ap)


[STATEMENT]
lemma typ_ok_sig_code:
  assumes "exe_osig_conds (exesorts \<Sigma>)"
  shows "typ_ok_sig (translate_signature \<Sigma>) ty = exetyp_ok_sig \<Sigma> ty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. typ_ok_sig (translate_signature \<Sigma>) ty = exetyp_ok_sig \<Sigma> ty
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
exe_osig_conds (exesorts \<Sigma>)

goal (1 subgoal):
 1. typ_ok_sig (translate_signature \<Sigma>) ty = exetyp_ok_sig \<Sigma> ty
[PROOF STEP]
apply (induction ty)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set x2; exe_osig_conds (exesorts \<Sigma>)\<rbrakk> \<Longrightarrow> typ_ok_sig (translate_signature \<Sigma>) x2a = exetyp_ok_sig \<Sigma> x2a; exe_osig_conds (exesorts \<Sigma>)\<rbrakk> \<Longrightarrow> typ_ok_sig (translate_signature \<Sigma>) (Ty x1 x2) = exetyp_ok_sig \<Sigma> (Ty x1 x2)
 2. \<And>x1 x2. exe_osig_conds (exesorts \<Sigma>) \<Longrightarrow> typ_ok_sig (translate_signature \<Sigma>) (Tv x1 x2) = exetyp_ok_sig \<Sigma> (Tv x1 x2)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>\<And>x2a. x2a \<in> set x2 \<Longrightarrow> typ_ok_sig (translate_signature \<Sigma>) x2a = exetyp_ok_sig \<Sigma> x2a; exe_osig_conds (exesorts \<Sigma>)\<rbrakk> \<Longrightarrow> (case type_arity (translate_signature \<Sigma>) x1 of None \<Rightarrow> False | Some ar \<Rightarrow> length x2 = ar \<and> list_all (typ_ok_sig (translate_signature \<Sigma>)) x2) = (case lookup (\<lambda>k. k = x1) (exetyp_arity_of \<Sigma>) of None \<Rightarrow> False | Some ar \<Rightarrow> length x2 = ar \<and> list_all (exetyp_ok_sig \<Sigma>) x2)
 2. \<And>x1 x2. exe_osig_conds (exesorts \<Sigma>) \<Longrightarrow> typ_ok_sig (translate_signature \<Sigma>) (Tv x1 x2) = exetyp_ok_sig \<Sigma> (Tv x1 x2)
[PROOF STEP]
apply (auto split: option.splits simp add: wf_sort_def list_all_iff typ_arity_lookup_code)[]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. exe_osig_conds (exesorts \<Sigma>) \<Longrightarrow> typ_ok_sig (translate_signature \<Sigma>) (Tv x1 x2) = exetyp_ok_sig \<Sigma> (Tv x1 x2)
[PROOF STEP]
using wf_sort_code
[PROOF STATE]
proof (prove)
using this:
exe_class_conds ?sub \<Longrightarrow> wf_sort (set ?sub) ?S = exewf_sort ?sub ?S

goal (1 subgoal):
 1. \<And>x1 x2. exe_osig_conds (exesorts \<Sigma>) \<Longrightarrow> typ_ok_sig (translate_signature \<Sigma>) (Tv x1 x2) = exetyp_ok_sig \<Sigma> (Tv x1 x2)
[PROOF STEP]
by (cases \<Sigma>) (simp add: exe_osig_conds_def classes_translate)


[STATEMENT]
lemma exe_wf_sig_code[code]: "exe_wf_sig \<Sigma> = exe_wf_sig' \<Sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exe_wf_sig \<Sigma> = exe_wf_sig' \<Sigma>
[PROOF STEP]
using typ_ok_sig_code
[PROOF STATE]
proof (prove)
using this:
exe_osig_conds (exesorts ?\<Sigma>) \<Longrightarrow> typ_ok_sig (translate_signature ?\<Sigma>) ?ty = exetyp_ok_sig ?\<Sigma> ?ty

goal (1 subgoal):
 1. exe_wf_sig \<Sigma> = exe_wf_sig' \<Sigma>
[PROOF STEP]
by (cases \<Sigma>, simp, metis exesignature.sel(3) translate_signature.simps)


[STATEMENT]
lemma const_type_of_lookup_code: "const_type (translate_signature \<Sigma>) n = lookup (\<lambda>k. k = n) (execonst_type_of \<Sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. const_type (translate_signature \<Sigma>) n = lookup (\<lambda>k. k = n) (execonst_type_of \<Sigma>)
[PROOF STEP]
by (cases \<Sigma>) (simp add: lookup_eq_map_of_ap)


[STATEMENT]
lemma wt_term_code:
  assumes "exe_osig_conds (exesorts \<Sigma>)"
  shows "term_ok' (translate_signature \<Sigma>) t = exeterm_ok' \<Sigma> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. term_ok' (translate_signature \<Sigma>) t = exeterm_ok' \<Sigma> t
[PROOF STEP]
by (induction t) (auto simp add: const_type_of_lookup_code assms typ_ok_sig_code split: option.splits)


[STATEMENT]
lemma exetheory_full_exhaust: "(\<And>const_type typ_arity sorts axioms.
    \<Theta> = (ExeTheory (ExeSignature const_type typ_arity sorts) axioms) \<Longrightarrow> P)
  \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>const_type typ_arity sorts axioms. \<Theta> = ExeTheory (ExeSignature const_type typ_arity sorts) axioms \<Longrightarrow> P) \<Longrightarrow> P
[PROOF STEP]
apply (cases \<Theta>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>\<And>const_type typ_arity sorts axioms. \<Theta> = ExeTheory (ExeSignature const_type typ_arity sorts) axioms \<Longrightarrow> P; \<Theta> = ExeTheory x1 x2\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
subgoal for \<Sigma> axioms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>const_type typ_arity sorts axioms. \<Theta> = ExeTheory (ExeSignature const_type typ_arity sorts) axioms \<Longrightarrow> P; \<Theta> = ExeTheory \<Sigma> axioms\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
apply (cases \<Sigma>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3. \<lbrakk>\<And>const_type typ_arity sorts axioms. \<Theta> = ExeTheory (ExeSignature const_type typ_arity sorts) axioms \<Longrightarrow> P; \<Theta> = ExeTheory \<Sigma> axioms; \<Sigma> = ExeSignature x1 x2 x3\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma illformed_theory_not_wf_theory: "\<not> wf_theory illformed_theory"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> wf_theory ((Map.empty, Map.empty, {}, [STR ''A'' \<mapsto> [STR ''A'' \<mapsto> [insert STR ''A'' full_sort]]]), {})
[PROOF STEP]
by simp


[STATEMENT]
lemma wf_sig_iff_exe_wf_sig': "exe_sig_conds \<Sigma> \<Longrightarrow>
    wf_sig (translate_signature \<Sigma>) \<longleftrightarrow>
    exe_wf_sig \<Sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exe_sig_conds \<Sigma> \<Longrightarrow> wf_sig (translate_signature \<Sigma>) = exe_wf_sig \<Sigma>
[PROOF STEP]
by (metis exe_sig_conds_def exesignature.exhaust_sel wf_sig_iff_exe_wf_sig translate_signature.simps)


[STATEMENT]
lemma wf_sig_imp_exe_wf_sig': "exe_sig_conds \<Sigma> \<Longrightarrow>
    wf_sig (translate_signature \<Sigma>) \<Longrightarrow>
    exe_wf_sig \<Sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>exe_sig_conds \<Sigma>; wf_sig (translate_signature \<Sigma>)\<rbrakk> \<Longrightarrow> exe_wf_sig \<Sigma>
[PROOF STEP]
by (metis exe_sig_conds_def exesignature.exhaust_sel wf_sig_iff_exe_wf_sig translate_signature.simps)


[STATEMENT]
lemma exe_wf_sig_imp_wf_sig': "exe_sig_conds \<Sigma> \<Longrightarrow>
    exe_wf_sig \<Sigma>
    \<Longrightarrow> wf_sig (translate_signature \<Sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>exe_sig_conds \<Sigma>; exe_wf_sig \<Sigma>\<rbrakk> \<Longrightarrow> wf_sig (translate_signature \<Sigma>)
[PROOF STEP]
by (metis exe_sig_conds_def exesignature.exhaust_sel wf_sig_iff_exe_wf_sig translate_signature.simps)


[STATEMENT]
lemma wf_theory_translate_imp_exe_wf_theory:
  assumes "wf_theory (translate_theory a)" shows "exe_wf_theory a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exe_wf_theory a
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. exe_wf_theory a
[PROOF STEP]
have "exe_sig_conds (exesig a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exe_sig_conds (exesig a)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wf_theory (translate_theory a)

goal (1 subgoal):
 1. exe_sig_conds (exesig a)
[PROOF STEP]
by (metis exetheory.collapse illformed_theory_not_wf_theory translate_theory.simps)
[PROOF STATE]
proof (state)
this:
exe_sig_conds (exesig a)

goal (1 subgoal):
 1. exe_wf_theory a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
exe_sig_conds (exesig a)

goal (1 subgoal):
 1. exe_wf_theory a
[PROOF STEP]
have "wf_sig (translate_signature (exesig a))
    \<longleftrightarrow> exe_wf_sig (exesig a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_sig (translate_signature (exesig a)) = exe_wf_sig (exesig a)
[PROOF STEP]
by (simp add: calculation(1) wf_sig_iff_exe_wf_sig')
[PROOF STATE]
proof (state)
this:
wf_sig (translate_signature (exesig a)) = exe_wf_sig (exesig a)

goal (1 subgoal):
 1. exe_wf_theory a
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
exe_sig_conds (exesig a)
wf_sig (translate_signature (exesig a)) = exe_wf_sig (exesig a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
exe_sig_conds (exesig a)
wf_sig (translate_signature (exesig a)) = exe_wf_sig (exesig a)

goal (1 subgoal):
 1. exe_wf_theory a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
exe_sig_conds (exesig a)
wf_sig (translate_signature (exesig a)) = exe_wf_sig (exesig a)
wf_theory (translate_theory a)

goal (1 subgoal):
 1. exe_wf_theory a
[PROOF STEP]
by (cases a rule: exe_wf_theory.cases) (fastforce simp add: image_iff eq_fst_iff)
[PROOF STATE]
proof (state)
this:
exe_wf_theory a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exe_wf_theory_translate_imp_wf_theory:
  assumes "exe_wf_theory a" shows "wf_theory (translate_theory a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_theory (translate_theory a)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_theory (translate_theory a)
[PROOF STEP]
have "exe_sig_conds (exesig a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exe_sig_conds (exesig a)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
exe_wf_theory a

goal (1 subgoal):
 1. exe_sig_conds (exesig a)
[PROOF STEP]
by (metis (full_types) exe_wf_theory.simps exesignature.exhaust_sel exetheory.sel(1) translate_theory.cases)
[PROOF STATE]
proof (state)
this:
exe_sig_conds (exesig a)

goal (1 subgoal):
 1. wf_theory (translate_theory a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
exe_sig_conds (exesig a)

goal (1 subgoal):
 1. wf_theory (translate_theory a)
[PROOF STEP]
hence "
  (\<forall>ty \<in> Map.ran (map_of (execonst_type_of (exesig a))) . typ_ok_sig (translate_signature (exesig a)) ty)
  \<longleftrightarrow> (\<forall>ty \<in> snd ` set (execonst_type_of (exesig a)) . typ_ok_sig (translate_signature (exesig a)) ty)"
[PROOF STATE]
proof (prove)
using this:
exe_sig_conds (exesig a)

goal (1 subgoal):
 1. (\<forall>ty\<in>ran (map_of (execonst_type_of (exesig a))). typ_ok_sig (translate_signature (exesig a)) ty) = (\<forall>ty\<in>snd ` set (execonst_type_of (exesig a)). typ_ok_sig (translate_signature (exesig a)) ty)
[PROOF STEP]
by (simp add: exe_sig_conds_def ran_distinct)
[PROOF STATE]
proof (state)
this:
(\<forall>ty\<in>ran (map_of (execonst_type_of (exesig a))). typ_ok_sig (translate_signature (exesig a)) ty) = (\<forall>ty\<in>snd ` set (execonst_type_of (exesig a)). typ_ok_sig (translate_signature (exesig a)) ty)

goal (1 subgoal):
 1. wf_theory (translate_theory a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<forall>ty\<in>ran (map_of (execonst_type_of (exesig a))). typ_ok_sig (translate_signature (exesig a)) ty) = (\<forall>ty\<in>snd ` set (execonst_type_of (exesig a)). typ_ok_sig (translate_signature (exesig a)) ty)

goal (1 subgoal):
 1. wf_theory (translate_theory a)
[PROOF STEP]
have "wf_sig (translate_signature (exesig a))
    \<longleftrightarrow> exe_wf_sig (exesig a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_sig (translate_signature (exesig a)) = exe_wf_sig (exesig a)
[PROOF STEP]
by (simp add: calculation(1) wf_sig_iff_exe_wf_sig')
[PROOF STATE]
proof (state)
this:
wf_sig (translate_signature (exesig a)) = exe_wf_sig (exesig a)

goal (1 subgoal):
 1. wf_theory (translate_theory a)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
exe_sig_conds (exesig a)
(\<forall>ty\<in>ran (map_of (execonst_type_of (exesig a))). typ_ok_sig (translate_signature (exesig a)) ty) = (\<forall>ty\<in>snd ` set (execonst_type_of (exesig a)). typ_ok_sig (translate_signature (exesig a)) ty)
wf_sig (translate_signature (exesig a)) = exe_wf_sig (exesig a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
exe_sig_conds (exesig a)
(\<forall>ty\<in>ran (map_of (execonst_type_of (exesig a))). typ_ok_sig (translate_signature (exesig a)) ty) = (\<forall>ty\<in>snd ` set (execonst_type_of (exesig a)). typ_ok_sig (translate_signature (exesig a)) ty)
wf_sig (translate_signature (exesig a)) = exe_wf_sig (exesig a)

goal (1 subgoal):
 1. wf_theory (translate_theory a)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
exe_sig_conds (exesig a)
(\<forall>ty\<in>ran (map_of (execonst_type_of (exesig a))). typ_ok_sig (translate_signature (exesig a)) ty) = (\<forall>ty\<in>snd ` set (execonst_type_of (exesig a)). typ_ok_sig (translate_signature (exesig a)) ty)
wf_sig (translate_signature (exesig a)) = exe_wf_sig (exesig a)
exe_wf_theory a

goal (1 subgoal):
 1. wf_theory (translate_theory a)
[PROOF STEP]
by (cases a rule: exe_wf_theory.cases) auto
[PROOF STATE]
proof (state)
this:
wf_theory (translate_theory a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wf_theory_translate_iff_exe_wf_theory:
  "wf_theory (translate_theory a) \<longleftrightarrow> exe_wf_theory a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_theory (translate_theory a) = exe_wf_theory a
[PROOF STEP]
using exe_wf_theory_translate_imp_wf_theory wf_theory_translate_imp_exe_wf_theory
[PROOF STATE]
proof (prove)
using this:
exe_wf_theory ?a \<Longrightarrow> wf_theory (translate_theory ?a)
wf_theory (translate_theory ?a) \<Longrightarrow> exe_wf_theory ?a

goal (1 subgoal):
 1. wf_theory (translate_theory a) = exe_wf_theory a
[PROOF STEP]
by blast


[STATEMENT]
lemma is_std_sig_code: "is_std_sig (translate_signature \<Sigma>) = exeis_std_sig \<Sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_std_sig (translate_signature \<Sigma>) = exeis_std_sig \<Sigma>
[PROOF STEP]
by (cases \<Sigma>) (auto simp add: lookup_eq_map_of_ap)


[STATEMENT]
lemma term_ok'_code:
  assumes "exe_osig_conds (exesorts (ExeSignature cto tao sa))"
  shows "(term_ok' (translate_signature (ExeSignature cto tao sa)) p \<and> typ_of p = Some propT)
    = (exeterm_ok' (ExeSignature cto tao sa) p \<and> typ_of p = Some propT)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (term_ok' (translate_signature (ExeSignature cto tao sa)) p \<and> typ_of p = Some propT) = (exeterm_ok' (ExeSignature cto tao sa) p \<and> typ_of p = Some propT)
[PROOF STEP]
using wt_term_code[OF assms]
[PROOF STATE]
proof (prove)
using this:
term_ok' (translate_signature (ExeSignature cto tao sa)) ?t = exeterm_ok' (ExeSignature cto tao sa) ?t

goal (1 subgoal):
 1. (term_ok' (translate_signature (ExeSignature cto tao sa)) p \<and> typ_of p = Some propT) = (exeterm_ok' (ExeSignature cto tao sa) p \<and> typ_of p = Some propT)
[PROOF STEP]
by force


[STATEMENT]
lemma term_ok_translate_code_step:
  assumes "exe_sig_conds (ExeSignature cto tao sa)"
  shows "(term_ok (translate_theory (ExeTheory (ExeSignature cto tao sa) ax)) p \<and> typ_of p = Some propT)
    = (term_ok' (translate_signature (ExeSignature cto tao sa)) p \<and> typ_of p = Some propT)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (term_ok (translate_theory (ExeTheory (ExeSignature cto tao sa) ax)) p \<and> typ_of p = Some propT) = (term_ok' (translate_signature (ExeSignature cto tao sa)) p \<and> typ_of p = Some propT)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
exe_sig_conds (ExeSignature cto tao sa)

goal (1 subgoal):
 1. (term_ok (translate_theory (ExeTheory (ExeSignature cto tao sa) ax)) p \<and> typ_of p = Some propT) = (term_ok' (translate_signature (ExeSignature cto tao sa)) p \<and> typ_of p = Some propT)
[PROOF STEP]
by (auto simp add: wt_term_def split: if_splits)


[STATEMENT]
lemma term_ok_theory_cond_code:
  assumes "exe_sig_conds (ExeSignature cto tao sa)"
  shows"(\<forall>p \<in> set ax . term_ok (translate_theory (ExeTheory (ExeSignature cto tao sa) ax)) p \<and> typ_of p = Some propT)
    = (\<forall>p \<in> set ax . exeterm_ok' (ExeSignature cto tao sa) p \<and> typ_of p = Some propT)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>p\<in>set ax. term_ok (translate_theory (ExeTheory (ExeSignature cto tao sa) ax)) p \<and> typ_of p = Some propT) = (\<forall>p\<in>set ax. exeterm_ok' (ExeSignature cto tao sa) p \<and> typ_of p = Some propT)
[PROOF STEP]
using assms wf_term_imp_term_ok' exe_sig_conds_def wt_term_code
[PROOF STATE]
proof (prove)
using this:
exe_sig_conds (ExeSignature cto tao sa)
wf_term ?\<Sigma> ?t \<Longrightarrow> term_ok' ?\<Sigma> ?t
exe_sig_conds ?\<Sigma> \<equiv> alist_conds (execonst_type_of ?\<Sigma>) \<and> alist_conds (exetyp_arity_of ?\<Sigma>) \<and> exe_osig_conds (exesorts ?\<Sigma>)
exe_osig_conds (exesorts ?\<Sigma>) \<Longrightarrow> term_ok' (translate_signature ?\<Sigma>) ?t = exeterm_ok' ?\<Sigma> ?t

goal (1 subgoal):
 1. (\<forall>p\<in>set ax. term_ok (translate_theory (ExeTheory (ExeSignature cto tao sa) ax)) p \<and> typ_of p = Some propT) = (\<forall>p\<in>set ax. exeterm_ok' (ExeSignature cto tao sa) p \<and> typ_of p = Some propT)
[PROOF STEP]
by (fastforce simp add: term_ok_translate_code_step wt_term_code wt_term_def)


[STATEMENT]
lemma exe_wf_theory_code[code]: "exe_wf_theory \<Theta> = exe_wf_theory' \<Theta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exe_wf_theory \<Theta> = exe_wf_theory' \<Theta>
[PROOF STEP]
apply (cases \<Theta> rule: exetheory_full_exhaust)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>const_type typ_arity sorts axioms. \<Theta> = ExeTheory (ExeSignature const_type typ_arity sorts) axioms \<Longrightarrow> exe_wf_theory \<Theta> = exe_wf_theory' \<Theta>
[PROOF STEP]
apply (simp only: exe_wf_theory.simps exe_wf_theory'.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>const_type typ_arity sorts axioms. \<Theta> = ExeTheory (ExeSignature const_type typ_arity sorts) axioms \<Longrightarrow> (exe_sig_conds (ExeSignature const_type typ_arity sorts) \<and> (\<forall>p\<in>set axioms. term_ok (translate_theory (ExeTheory (ExeSignature const_type typ_arity sorts) axioms)) p \<and> typ_of p = Some propT) \<and> is_std_sig (translate_signature (ExeSignature const_type typ_arity sorts)) \<and> exe_wf_sig (ExeSignature const_type typ_arity sorts) \<and> eq_axs \<subseteq> set axioms) = (exe_sig_conds (ExeSignature const_type typ_arity sorts) \<and> (\<forall>p\<in>set axioms. exeterm_ok' (ExeSignature const_type typ_arity sorts) p \<and> typ_of p = Some propT) \<and> exeis_std_sig (ExeSignature const_type typ_arity sorts) \<and> exe_wf_sig (ExeSignature const_type typ_arity sorts) \<and> eq_axs \<subseteq> set axioms)
[PROOF STEP]
using term_ok_theory_cond_code is_std_sig_code
[PROOF STATE]
proof (prove)
using this:
exe_sig_conds (ExeSignature ?cto ?tao ?sa) \<Longrightarrow> (\<forall>p\<in>set ?ax. term_ok (translate_theory (ExeTheory (ExeSignature ?cto ?tao ?sa) ?ax)) p \<and> typ_of p = Some propT) = (\<forall>p\<in>set ?ax. exeterm_ok' (ExeSignature ?cto ?tao ?sa) p \<and> typ_of p = Some propT)
is_std_sig (translate_signature ?\<Sigma>) = exeis_std_sig ?\<Sigma>

goal (1 subgoal):
 1. \<And>const_type typ_arity sorts axioms. \<Theta> = ExeTheory (ExeSignature const_type typ_arity sorts) axioms \<Longrightarrow> (exe_sig_conds (ExeSignature const_type typ_arity sorts) \<and> (\<forall>p\<in>set axioms. term_ok (translate_theory (ExeTheory (ExeSignature const_type typ_arity sorts) axioms)) p \<and> typ_of p = Some propT) \<and> is_std_sig (translate_signature (ExeSignature const_type typ_arity sorts)) \<and> exe_wf_sig (ExeSignature const_type typ_arity sorts) \<and> eq_axs \<subseteq> set axioms) = (exe_sig_conds (ExeSignature const_type typ_arity sorts) \<and> (\<forall>p\<in>set axioms. exeterm_ok' (ExeSignature const_type typ_arity sorts) p \<and> typ_of p = Some propT) \<and> exeis_std_sig (ExeSignature const_type typ_arity sorts) \<and> exe_wf_sig (ExeSignature const_type typ_arity sorts) \<and> eq_axs \<subseteq> set axioms)
[PROOF STEP]
by meson


[STATEMENT]
lemma ldistinct_lfilter_ltake[intro]:
  assumes "ldistinct (lfilter P xs)"
  shows "ldistinct (lfilter P (ltake x xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ldistinct (lfilter P (ltake x xs))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ldistinct (lfilter P xs)

goal (1 subgoal):
 1. ldistinct (lfilter P (ltake x xs))
[PROOF STEP]
by(induct xs,force,force
    ,(* sledgehammer found this gem to prove the inductive step via lfilter_lappend_lfinite!
        We will use this strategy ourselves later on *)
     metis lappend_ltake_ldrop ldistinct_lappend lfilter_lappend_lfinite lfinite_LConsI lfinite_ltake)


[STATEMENT]
lemma lfilter_lfind:
  assumes "lfilter P lst \<noteq> LNil"
  shows "P (lst $ lfind P lst)" (is ?g1)
        "P (lst $ y) \<Longrightarrow> lfind P lst \<le> y" (is "?a \<Longrightarrow> ?g2")
        "lfind P lst < llength lst" (is ?g3)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (lst $ lfind P lst) &&& (P (lst $ y) \<Longrightarrow> lfind P lst \<le> y) &&& enat (lfind P lst) < llength lst
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. P (lst $ lfind P lst)
 2. P (lst $ y) \<Longrightarrow> lfind P lst \<le> y
 3. enat (lfind P lst) < llength lst
[PROOF STEP]
let ?I = "{n. enat n < llength lst \<and> P (lst $ n)}"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. P (lst $ lfind P lst)
 2. P (lst $ y) \<Longrightarrow> lfind P lst \<le> y
 3. enat (lfind P lst) < llength lst
[PROOF STEP]
let ?xs = lst
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. P (lst $ lfind P lst)
 2. P (lst $ y) \<Longrightarrow> lfind P lst \<le> y
 3. enat (lfind P lst) < llength lst
[PROOF STEP]
from assms[unfolded lfilter_conv_lnths] lset_LNil
[PROOF STATE]
proof (chain)
picking this:
lnths lst {n. enat n < llength lst \<and> P (lst $ n)} \<noteq> LNil
lset LNil = {}
[PROOF STEP]
have "lset (lnths lst {n. enat n < llength lst \<and> P (lst $ n)}) \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
lnths lst {n. enat n < llength lst \<and> P (lst $ n)} \<noteq> LNil
lset LNil = {}

goal (1 subgoal):
 1. lset (lnths lst {n. enat n < llength lst \<and> P (lst $ n)}) \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lset (lnths lst {n. enat n < llength lst \<and> P (lst $ n)}) \<noteq> {}

goal (3 subgoals):
 1. P (lst $ lfind P lst)
 2. P (lst $ y) \<Longrightarrow> lfind P lst \<le> y
 3. enat (lfind P lst) < llength lst
[PROOF STEP]
hence "{?xs $ i |i. enat i < llength ?xs \<and> i \<in> ?I} \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
lset (lnths lst {n. enat n < llength lst \<and> P (lst $ n)}) \<noteq> {}

goal (1 subgoal):
 1. {lst $ i |i. enat i < llength lst \<and> i \<in> {n. enat n < llength lst \<and> P (lst $ n)}} \<noteq> {}
[PROOF STEP]
using lset_lnths[of ?xs ?I]
[PROOF STATE]
proof (prove)
using this:
lset (lnths lst {n. enat n < llength lst \<and> P (lst $ n)}) \<noteq> {}
lset (lnths lst {n. enat n < llength lst \<and> P (lst $ n)}) = {lst $ i |i. enat i < llength lst \<and> i \<in> {n. enat n < llength lst \<and> P (lst $ n)}}

goal (1 subgoal):
 1. {lst $ i |i. enat i < llength lst \<and> i \<in> {n. enat n < llength lst \<and> P (lst $ n)}} \<noteq> {}
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
{lst $ i |i. enat i < llength lst \<and> i \<in> {n. enat n < llength lst \<and> P (lst $ n)}} \<noteq> {}

goal (3 subgoals):
 1. P (lst $ lfind P lst)
 2. P (lst $ y) \<Longrightarrow> lfind P lst \<le> y
 3. enat (lfind P lst) < llength lst
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{lst $ i |i. enat i < llength lst \<and> i \<in> {n. enat n < llength lst \<and> P (lst $ n)}} \<noteq> {}
[PROOF STEP]
obtain i where p:"P (lst $ i)" "i < llength lst"
[PROOF STATE]
proof (prove)
using this:
{lst $ i |i. enat i < llength lst \<and> i \<in> {n. enat n < llength lst \<and> P (lst $ n)}} \<noteq> {}

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>P (lst $ i); enat i < llength lst\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P (lst $ i)
enat i < llength lst

goal (3 subgoals):
 1. P (lst $ lfind P lst)
 2. P (lst $ y) \<Longrightarrow> lfind P lst \<le> y
 3. enat (lfind P lst) < llength lst
[PROOF STEP]
from p
[PROOF STATE]
proof (chain)
picking this:
P (lst $ i)
enat i < llength lst
[PROOF STEP]
show ?g1
[PROOF STATE]
proof (prove)
using this:
P (lst $ i)
enat i < llength lst

goal (1 subgoal):
 1. P (lst $ lfind P lst)
[PROOF STEP]
using LeastI lfind_def
[PROOF STATE]
proof (prove)
using this:
P (lst $ i)
enat i < llength lst
?P ?k \<Longrightarrow> ?P (LEAST x. ?P x)
lfind ?P ?lst = (LEAST i. ?P (?lst $ i))

goal (1 subgoal):
 1. P (lst $ lfind P lst)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
P (lst $ lfind P lst)

goal (2 subgoals):
 1. P (lst $ y) \<Longrightarrow> lfind P lst \<le> y
 2. enat (lfind P lst) < llength lst
[PROOF STEP]
from p
[PROOF STATE]
proof (chain)
picking this:
P (lst $ i)
enat i < llength lst
[PROOF STEP]
show "?a \<Longrightarrow> ?g2"
[PROOF STATE]
proof (prove)
using this:
P (lst $ i)
enat i < llength lst

goal (1 subgoal):
 1. P (lst $ y) \<Longrightarrow> lfind P lst \<le> y
[PROOF STEP]
using Least_le lfind_def
[PROOF STATE]
proof (prove)
using this:
P (lst $ i)
enat i < llength lst
?P ?k \<Longrightarrow> (LEAST x. ?P x) \<le> ?k
lfind ?P ?lst = (LEAST i. ?P (?lst $ i))

goal (1 subgoal):
 1. P (lst $ y) \<Longrightarrow> lfind P lst \<le> y
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
P (lst $ y) \<Longrightarrow> lfind P lst \<le> y

goal (1 subgoal):
 1. enat (lfind P lst) < llength lst
[PROOF STEP]
from p
[PROOF STATE]
proof (chain)
picking this:
P (lst $ i)
enat i < llength lst
[PROOF STEP]
show ?g3
[PROOF STATE]
proof (prove)
using this:
P (lst $ i)
enat i < llength lst

goal (1 subgoal):
 1. enat (lfind P lst) < llength lst
[PROOF STEP]
using Least_le lfind_def
[PROOF STATE]
proof (prove)
using this:
P (lst $ i)
enat i < llength lst
?P ?k \<Longrightarrow> (LEAST x. ?P x) \<le> ?k
lfind ?P ?lst = (LEAST i. ?P (?lst $ i))

goal (1 subgoal):
 1. enat (lfind P lst) < llength lst
[PROOF STEP]
by (metis enat_ord_simps(1) le_less_trans)
[PROOF STATE]
proof (state)
this:
enat (lfind P lst) < llength lst

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ltake_lfind_lset:
  assumes "x \<in> lset (ltake (enat (lfind P lst)) lst)"
  shows "\<not> P x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> P x
[PROOF STEP]
proof(cases "lfilter P (ltake (enat (lfind P lst)) lst) = LNil")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lfilter P (ltake (enat (lfind P lst)) lst) = LNil \<Longrightarrow> \<not> P x
 2. lfilter P (ltake (enat (lfind P lst)) lst) \<noteq> LNil \<Longrightarrow> \<not> P x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
lfilter P (ltake (enat (lfind P lst)) lst) = LNil

goal (2 subgoals):
 1. lfilter P (ltake (enat (lfind P lst)) lst) = LNil \<Longrightarrow> \<not> P x
 2. lfilter P (ltake (enat (lfind P lst)) lst) \<noteq> LNil \<Longrightarrow> \<not> P x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lfilter P (ltake (enat (lfind P lst)) lst) = LNil
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lfilter P (ltake (enat (lfind P lst)) lst) = LNil

goal (1 subgoal):
 1. \<not> P x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
lfilter P (ltake (enat (lfind P lst)) lst) = LNil
x \<in> lset (ltake (enat (lfind P lst)) lst)

goal (1 subgoal):
 1. \<not> P x
[PROOF STEP]
unfolding lfilter_eq_LNil
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>lset (ltake (enat (lfind P lst)) lst). \<not> P x
x \<in> lset (ltake (enat (lfind P lst)) lst)

goal (1 subgoal):
 1. \<not> P x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> P x

goal (1 subgoal):
 1. lfilter P (ltake (enat (lfind P lst)) lst) \<noteq> LNil \<Longrightarrow> \<not> P x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lfilter P (ltake (enat (lfind P lst)) lst) \<noteq> LNil \<Longrightarrow> \<not> P x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
lfilter P (ltake (enat (lfind P lst)) lst) \<noteq> LNil

goal (1 subgoal):
 1. lfilter P (ltake (enat (lfind P lst)) lst) \<noteq> LNil \<Longrightarrow> \<not> P x
[PROOF STEP]
from assms[unfolded in_lset_conv_lnth]
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. enat n < llength (ltake (enat (lfind P lst)) lst) \<and> ltake (enat (lfind P lst)) lst $ n = x
[PROOF STEP]
obtain n where
    n:"enat n < llength (ltake (enat (lfind P lst)) lst)" "ltake (enat (lfind P lst)) lst $ n = x"
[PROOF STATE]
proof (prove)
using this:
\<exists>n. enat n < llength (ltake (enat (lfind P lst)) lst) \<and> ltake (enat (lfind P lst)) lst $ n = x

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>enat n < llength (ltake (enat (lfind P lst)) lst); ltake (enat (lfind P lst)) lst $ n = x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
enat n < llength (ltake (enat (lfind P lst)) lst)
ltake (enat (lfind P lst)) lst $ n = x

goal (1 subgoal):
 1. lfilter P (ltake (enat (lfind P lst)) lst) \<noteq> LNil \<Longrightarrow> \<not> P x
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
enat n < llength (ltake (enat (lfind P lst)) lst)
ltake (enat (lfind P lst)) lst $ n = x

goal (1 subgoal):
 1. lfilter P (ltake (enat (lfind P lst)) lst) \<noteq> LNil \<Longrightarrow> \<not> P x
[PROOF STEP]
assume a:"P x"
[PROOF STATE]
proof (state)
this:
P x

goal (1 subgoal):
 1. lfilter P (ltake (enat (lfind P lst)) lst) \<noteq> LNil \<Longrightarrow> \<not> P x
[PROOF STEP]
(* The idea of this {block} is that the element n must come after (lfind P lst) by lfilter_lfind(2)
     but this contradicts n(1).
     However, in the last step when writing this proof, sledgehammer found one that didn't use
       any of my previous steps, so here's a one-liner: *)
[PROOF STATE]
proof (state)
this:
P x

goal (1 subgoal):
 1. lfilter P (ltake (enat (lfind P lst)) lst) \<noteq> LNil \<Longrightarrow> \<not> P x
[PROOF STEP]
from n Coinductive_List.lset_ltake False a enat_ord_simps(1) leD lfilter_empty_conv lfilter_lfind(2,3) llength_ltake' lnth_ltake subset_eq
[PROOF STATE]
proof (chain)
picking this:
enat n < llength (ltake (enat (lfind P lst)) lst)
ltake (enat (lfind P lst)) lst $ n = x
lset (ltake ?n ?xs) \<subseteq> lset ?xs
lfilter P (ltake (enat (lfind P lst)) lst) \<noteq> LNil
P x
(enat ?m \<le> enat ?n) = (?m \<le> ?n)
?y \<le> ?x \<Longrightarrow> \<not> ?x < ?y
(lfilter ?P ?xs = LNil) = (\<forall>x\<in>lset ?xs. \<not> ?P x)
\<lbrakk>lfilter ?P ?lst \<noteq> LNil; ?P (?lst $ ?y)\<rbrakk> \<Longrightarrow> lfind ?P ?lst \<le> ?y
lfilter ?P ?lst \<noteq> LNil \<Longrightarrow> enat (lfind ?P ?lst) < llength ?lst
enat ?n < llength ?xs \<Longrightarrow> llength (ltake (enat ?n) ?xs) = enat ?n
enat ?m < ?n \<Longrightarrow> ltake ?n ?xs $ ?m = ?xs $ ?m
(?A \<subseteq> ?B) = (\<forall>x\<in>?A. x \<in> ?B)
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
enat n < llength (ltake (enat (lfind P lst)) lst)
ltake (enat (lfind P lst)) lst $ n = x
lset (ltake ?n ?xs) \<subseteq> lset ?xs
lfilter P (ltake (enat (lfind P lst)) lst) \<noteq> LNil
P x
(enat ?m \<le> enat ?n) = (?m \<le> ?n)
?y \<le> ?x \<Longrightarrow> \<not> ?x < ?y
(lfilter ?P ?xs = LNil) = (\<forall>x\<in>lset ?xs. \<not> ?P x)
\<lbrakk>lfilter ?P ?lst \<noteq> LNil; ?P (?lst $ ?y)\<rbrakk> \<Longrightarrow> lfind ?P ?lst \<le> ?y
lfilter ?P ?lst \<noteq> LNil \<Longrightarrow> enat (lfind ?P ?lst) < llength ?lst
enat ?n < llength ?xs \<Longrightarrow> llength (ltake (enat ?n) ?xs) = enat ?n
enat ?m < ?n \<Longrightarrow> ltake ?n ?xs $ ?m = ?xs $ ?m
(?A \<subseteq> ?B) = (\<forall>x\<in>?A. x \<in> ?B)

goal (1 subgoal):
 1. False
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. lfilter P (ltake (enat (lfind P lst)) lst) \<noteq> LNil \<Longrightarrow> \<not> P x
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
P x \<Longrightarrow> False

goal (1 subgoal):
 1. lfilter P (ltake (enat (lfind P lst)) lst) \<noteq> LNil \<Longrightarrow> \<not> P x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P x \<Longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P x \<Longrightarrow> False

goal (1 subgoal):
 1. \<not> P x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> P x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ltake_lfind_conv:
  assumes "lfilter P lst \<noteq> LNil"
  shows "ltake (lfind P lst) lst = ltakeWhile (Not o P) lst" (is "?t1 = ?t2")
        "ldrop (lfind P lst) lst = ldropWhile (Not o P) lst" (is "?t3 = ?t4")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ltake (enat (lfind P lst)) lst = ltakeWhile (Not \<circ> P) lst &&& ldrop (enat (lfind P lst)) lst = ldropWhile (Not \<circ> P) lst
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ltake (enat (lfind P lst)) lst = ltakeWhile (Not \<circ> P) lst
 2. ldrop (enat (lfind P lst)) lst = ldropWhile (Not \<circ> P) lst
[PROOF STEP]
have lfin:"lfinite ?t1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lfinite (ltake (enat (lfind P lst)) lst)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lfinite (ltake (enat (lfind P lst)) lst)

goal (2 subgoals):
 1. ltake (enat (lfind P lst)) lst = ltakeWhile (Not \<circ> P) lst
 2. ldrop (enat (lfind P lst)) lst = ldropWhile (Not \<circ> P) lst
[PROOF STEP]
have [simp]:"min (enat (lfind P lst)) (llength lst) = (lfind P lst)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min (enat (lfind P lst)) (llength lst) = enat (lfind P lst)
[PROOF STEP]
using lfilter_lfind(3)[OF assms]
[PROOF STATE]
proof (prove)
using this:
enat (lfind P lst) < llength lst

goal (1 subgoal):
 1. min (enat (lfind P lst)) (llength lst) = enat (lfind P lst)
[PROOF STEP]
by (metis min.strict_order_iff)
[PROOF STATE]
proof (state)
this:
min (enat (lfind P lst)) (llength lst) = enat (lfind P lst)

goal (2 subgoals):
 1. ltake (enat (lfind P lst)) lst = ltakeWhile (Not \<circ> P) lst
 2. ldrop (enat (lfind P lst)) lst = ldropWhile (Not \<circ> P) lst
[PROOF STEP]
have l1:"llength ?t1 = lfind P lst"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. llength (ltake (enat (lfind P lst)) lst) = enat (lfind P lst)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
llength (ltake (enat (lfind P lst)) lst) = enat (lfind P lst)

goal (2 subgoals):
 1. ltake (enat (lfind P lst)) lst = ltakeWhile (Not \<circ> P) lst
 2. ldrop (enat (lfind P lst)) lst = ldropWhile (Not \<circ> P) lst
[PROOF STEP]
from ltake_lfind_lset ltakeWhile_all
[PROOF STATE]
proof (chain)
picking this:
?x \<in> lset (ltake (enat (lfind ?P ?lst)) ?lst) \<Longrightarrow> \<not> ?P ?x
\<forall>x\<in>lset ?xs. ?P x \<Longrightarrow> ltakeWhile ?P ?xs = ?xs
[PROOF STEP]
have t:"ltakeWhile (Not o P) ?t1 = ?t1"
[PROOF STATE]
proof (prove)
using this:
?x \<in> lset (ltake (enat (lfind ?P ?lst)) ?lst) \<Longrightarrow> \<not> ?P ?x
\<forall>x\<in>lset ?xs. ?P x \<Longrightarrow> ltakeWhile ?P ?xs = ?xs

goal (1 subgoal):
 1. ltakeWhile (Not \<circ> P) (ltake (enat (lfind P lst)) lst) = ltake (enat (lfind P lst)) lst
[PROOF STEP]
unfolding o_def
[PROOF STATE]
proof (prove)
using this:
?x \<in> lset (ltake (enat (lfind ?P ?lst)) ?lst) \<Longrightarrow> \<not> ?P ?x
\<forall>x\<in>lset ?xs. ?P x \<Longrightarrow> ltakeWhile ?P ?xs = ?xs

goal (1 subgoal):
 1. ltakeWhile (\<lambda>x. \<not> P x) (ltake (enat (lfind P lst)) lst) = ltake (enat (lfind P lst)) lst
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
ltakeWhile (Not \<circ> P) (ltake (enat (lfind P lst)) lst) = ltake (enat (lfind P lst)) lst

goal (2 subgoals):
 1. ltake (enat (lfind P lst)) lst = ltakeWhile (Not \<circ> P) lst
 2. ldrop (enat (lfind P lst)) lst = ldropWhile (Not \<circ> P) lst
[PROOF STEP]
have inset:"lset (ltake (enat (lfind P lst)) lst) \<subseteq> {x. (Not \<circ> P) x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lset (ltake (enat (lfind P lst)) lst) \<subseteq> {x. (Not \<circ> P) x}
[PROOF STEP]
using ltake_lfind_lset[of _ P lst]
[PROOF STATE]
proof (prove)
using this:
?x \<in> lset (ltake (enat (lfind P lst)) lst) \<Longrightarrow> \<not> P ?x

goal (1 subgoal):
 1. lset (ltake (enat (lfind P lst)) lst) \<subseteq> {x. (Not \<circ> P) x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lset (ltake (enat (lfind P lst)) lst) \<subseteq> {x. (Not \<circ> P) x}

goal (2 subgoals):
 1. ltake (enat (lfind P lst)) lst = ltakeWhile (Not \<circ> P) lst
 2. ldrop (enat (lfind P lst)) lst = ldropWhile (Not \<circ> P) lst
[PROOF STEP]
(* for use in ltakeWhile_lappend2 *)
[PROOF STATE]
proof (state)
this:
lset (ltake (enat (lfind P lst)) lst) \<subseteq> {x. (Not \<circ> P) x}

goal (2 subgoals):
 1. ltake (enat (lfind P lst)) lst = ltakeWhile (Not \<circ> P) lst
 2. ldrop (enat (lfind P lst)) lst = ldropWhile (Not \<circ> P) lst
[PROOF STEP]
have isnull:"ltakeWhile (Not \<circ> P) (ldrop (enat (lfind P lst)) lst) = LNil"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ltakeWhile (Not \<circ> P) (ldrop (enat (lfind P lst)) lst) = LNil
[PROOF STEP]
apply(cases "ldrop (enat (lfind P lst)) lst")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ldrop (enat (lfind P lst)) lst = LNil \<Longrightarrow> ltakeWhile (Not \<circ> P) (ldrop (enat (lfind P lst)) lst) = LNil
 2. \<And>x21 x22. ldrop (enat (lfind P lst)) lst = LCons x21 x22 \<Longrightarrow> ltakeWhile (Not \<circ> P) (ldrop (enat (lfind P lst)) lst) = LNil
[PROOF STEP]
using lfilter_lfind(1)[OF assms] lhd_ldrop[OF lfilter_lfind(3)[OF assms]]
[PROOF STATE]
proof (prove)
using this:
P (lst $ lfind P lst)
lhd (ldrop (enat (lfind P lst)) lst) = lst $ the_enat (enat (lfind P lst))

goal (2 subgoals):
 1. ldrop (enat (lfind P lst)) lst = LNil \<Longrightarrow> ltakeWhile (Not \<circ> P) (ldrop (enat (lfind P lst)) lst) = LNil
 2. \<And>x21 x22. ldrop (enat (lfind P lst)) lst = LCons x21 x22 \<Longrightarrow> ltakeWhile (Not \<circ> P) (ldrop (enat (lfind P lst)) lst) = LNil
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ltakeWhile (Not \<circ> P) (ldrop (enat (lfind P lst)) lst) = LNil

goal (2 subgoals):
 1. ltake (enat (lfind P lst)) lst = ltakeWhile (Not \<circ> P) lst
 2. ldrop (enat (lfind P lst)) lst = ldropWhile (Not \<circ> P) lst
[PROOF STEP]
have "ltakeWhile (Not o P) ?t1 = ltakeWhile (Not o P) (lappend ?t1 ?t3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ltakeWhile (Not \<circ> P) (ltake (enat (lfind P lst)) lst) = ltakeWhile (Not \<circ> P) (lappend (ltake (enat (lfind P lst)) lst) (ldrop (enat (lfind P lst)) lst))
[PROOF STEP]
unfolding ltakeWhile_lappend2[OF inset] isnull lappend_LNil2 t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ltake (enat (lfind P lst)) lst = ltake (enat (lfind P lst)) lst
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
ltakeWhile (Not \<circ> P) (ltake (enat (lfind P lst)) lst) = ltakeWhile (Not \<circ> P) (lappend (ltake (enat (lfind P lst)) lst) (ldrop (enat (lfind P lst)) lst))

goal (2 subgoals):
 1. ltake (enat (lfind P lst)) lst = ltakeWhile (Not \<circ> P) lst
 2. ldrop (enat (lfind P lst)) lst = ldropWhile (Not \<circ> P) lst
[PROOF STEP]
hence leneq:"llength ?t1 = llength ?t2"
[PROOF STATE]
proof (prove)
using this:
ltakeWhile (Not \<circ> P) (ltake (enat (lfind P lst)) lst) = ltakeWhile (Not \<circ> P) (lappend (ltake (enat (lfind P lst)) lst) (ldrop (enat (lfind P lst)) lst))

goal (1 subgoal):
 1. llength (ltake (enat (lfind P lst)) lst) = llength (ltakeWhile (Not \<circ> P) lst)
[PROOF STEP]
using t l1 lappend_ltake_ldrop
[PROOF STATE]
proof (prove)
using this:
ltakeWhile (Not \<circ> P) (ltake (enat (lfind P lst)) lst) = ltakeWhile (Not \<circ> P) (lappend (ltake (enat (lfind P lst)) lst) (ldrop (enat (lfind P lst)) lst))
ltakeWhile (Not \<circ> P) (ltake (enat (lfind P lst)) lst) = ltake (enat (lfind P lst)) lst
llength (ltake (enat (lfind P lst)) lst) = enat (lfind P lst)
lappend (ltake ?n ?xs) (ldrop ?n ?xs) = ?xs

goal (1 subgoal):
 1. llength (ltake (enat (lfind P lst)) lst) = llength (ltakeWhile (Not \<circ> P) lst)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
llength (ltake (enat (lfind P lst)) lst) = llength (ltakeWhile (Not \<circ> P) lst)

goal (2 subgoals):
 1. ltake (enat (lfind P lst)) lst = ltakeWhile (Not \<circ> P) lst
 2. ldrop (enat (lfind P lst)) lst = ldropWhile (Not \<circ> P) lst
[PROOF STEP]
have "lappend ?t1 ?t3 = lappend ?t2 ?t4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lappend (ltake (enat (lfind P lst)) lst) (ldrop (enat (lfind P lst)) lst) = lappend (ltakeWhile (Not \<circ> P) lst) (ldropWhile (Not \<circ> P) lst)
[PROOF STEP]
unfolding lappend_ltakeWhile_ldropWhile[of "Not \<circ> P" lst]
               lappend_ltake_ldrop[of "lfind P lst" lst]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lst = lst
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lappend (ltake (enat (lfind P lst)) lst) (ldrop (enat (lfind P lst)) lst) = lappend (ltakeWhile (Not \<circ> P) lst) (ldropWhile (Not \<circ> P) lst)

goal (2 subgoals):
 1. ltake (enat (lfind P lst)) lst = ltakeWhile (Not \<circ> P) lst
 2. ldrop (enat (lfind P lst)) lst = ldropWhile (Not \<circ> P) lst
[PROOF STEP]
from this[unfolded lappend_eq_lappend_conv[OF leneq]] lfin
[PROOF STATE]
proof (chain)
picking this:
ltake (enat (lfind P lst)) lst = ltakeWhile (Not \<circ> P) lst \<and> (lfinite (ltake (enat (lfind P lst)) lst) \<longrightarrow> ldrop (enat (lfind P lst)) lst = ldropWhile (Not \<circ> P) lst)
lfinite (ltake (enat (lfind P lst)) lst)
[PROOF STEP]
show "?t1 = ?t2" "?t3 = ?t4"
[PROOF STATE]
proof (prove)
using this:
ltake (enat (lfind P lst)) lst = ltakeWhile (Not \<circ> P) lst \<and> (lfinite (ltake (enat (lfind P lst)) lst) \<longrightarrow> ldrop (enat (lfind P lst)) lst = ldropWhile (Not \<circ> P) lst)
lfinite (ltake (enat (lfind P lst)) lst)

goal (1 subgoal):
 1. ltake (enat (lfind P lst)) lst = ltakeWhile (Not \<circ> P) lst &&& ldrop (enat (lfind P lst)) lst = ldropWhile (Not \<circ> P) lst
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ltake (enat (lfind P lst)) lst = ltakeWhile (Not \<circ> P) lst
ldrop (enat (lfind P lst)) lst = ldropWhile (Not \<circ> P) lst

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lfilter_hdtl:
  assumes "lfilter P lst \<noteq> LNil"
  shows "\<exists> n. LCons (lhd (lfilter P lst)) LNil = lfilter P (ltake (enat n) lst) \<and>
              ltl (lfilter P lst) = lfilter P (ldrop (enat n) lst)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. LCons (lhd (lfilter P lst)) LNil = lfilter P (ltake (enat n) lst) \<and> ltl (lfilter P lst) = lfilter P (ldrop (enat n) lst)
[PROOF STEP]
proof(standard,standard)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. LCons (lhd (lfilter P lst)) LNil = lfilter P (ltake (enat ?n) lst)
 2. ltl (lfilter P lst) = lfilter P (ldrop (enat ?n) lst)
[PROOF STEP]
note * = lfilter_lfind[OF assms]
[PROOF STATE]
proof (state)
this:
P (lst $ lfind P lst)
P (lst $ ?y) \<Longrightarrow> lfind P lst \<le> ?y
enat (lfind P lst) < llength lst

goal (2 subgoals):
 1. LCons (lhd (lfilter P lst)) LNil = lfilter P (ltake (enat ?n) lst)
 2. ltl (lfilter P lst) = lfilter P (ldrop (enat ?n) lst)
[PROOF STEP]
let ?n = "Suc (lfind P lst)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. LCons (lhd (lfilter P lst)) LNil = lfilter P (ltake (enat ?n) lst)
 2. ltl (lfilter P lst) = lfilter P (ldrop (enat ?n) lst)
[PROOF STEP]
let ?ltake = "ltake (enat ?n) lst"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. LCons (lhd (lfilter P lst)) LNil = lfilter P (ltake (enat ?n) lst)
 2. ltl (lfilter P lst) = lfilter P (ldrop (enat ?n) lst)
[PROOF STEP]
have ltake:"lappend (ltakeWhile (Not \<circ> P) ?ltake) (ldropWhile (Not \<circ> P) ?ltake) = ?ltake"
      (is "lappend ?ltw ?ldw = _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lappend (ltakeWhile (Not \<circ> P) (ltake (enat (Suc (lfind P lst))) lst)) (ldropWhile (Not \<circ> P) (ltake (enat (Suc (lfind P lst))) lst)) = ltake (enat (Suc (lfind P lst))) lst
[PROOF STEP]
using lappend_ltakeWhile_ldropWhile
[PROOF STATE]
proof (prove)
using this:
lappend (ltakeWhile ?P ?xs) (ldropWhile ?P ?xs) = ?xs

goal (1 subgoal):
 1. lappend (ltakeWhile (Not \<circ> P) (ltake (enat (Suc (lfind P lst))) lst)) (ldropWhile (Not \<circ> P) (ltake (enat (Suc (lfind P lst))) lst)) = ltake (enat (Suc (lfind P lst))) lst
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
lappend (ltakeWhile (Not \<circ> P) (ltake (enat (Suc (lfind P lst))) lst)) (ldropWhile (Not \<circ> P) (ltake (enat (Suc (lfind P lst))) lst)) = ltake (enat (Suc (lfind P lst))) lst

goal (2 subgoals):
 1. LCons (lhd (lfilter P lst)) LNil = lfilter P (ltake (enat ?n) lst)
 2. ltl (lfilter P lst) = lfilter P (ldrop (enat ?n) lst)
[PROOF STEP]
have "llength ?ldw \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. llength (ldropWhile (Not \<circ> P) (ltake (enat (Suc (lfind P lst))) lst)) \<le> 1
[PROOF STEP]
unfolding ldropWhile_lappend ltake_Suc_conv_snoc_lnth[OF *(3)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. llength (if \<exists>x\<in>lset (ltake (enat (lfind P lst)) lst). \<not> (Not \<circ> P) x then lappend (ldropWhile (Not \<circ> P) (ltake (enat (lfind P lst)) lst)) (LCons (lst $ lfind P lst) LNil) else if lfinite (ltake (enat (lfind P lst)) lst) then ldropWhile (Not \<circ> P) (LCons (lst $ lfind P lst) LNil) else LNil) \<le> 1
[PROOF STEP]
using ltake_lfind_lset[of _ P lst]
[PROOF STATE]
proof (prove)
using this:
?x \<in> lset (ltake (enat (lfind P lst)) lst) \<Longrightarrow> \<not> P ?x

goal (1 subgoal):
 1. llength (if \<exists>x\<in>lset (ltake (enat (lfind P lst)) lst). \<not> (Not \<circ> P) x then lappend (ldropWhile (Not \<circ> P) (ltake (enat (lfind P lst)) lst)) (LCons (lst $ lfind P lst) LNil) else if lfinite (ltake (enat (lfind P lst)) lst) then ldropWhile (Not \<circ> P) (LCons (lst $ lfind P lst) LNil) else LNil) \<le> 1
[PROOF STEP]
by (auto intro:* simp:one_eSuc)
[PROOF STATE]
proof (state)
this:
llength (ldropWhile (Not \<circ> P) (ltake (enat (Suc (lfind P lst))) lst)) \<le> 1

goal (2 subgoals):
 1. LCons (lhd (lfilter P lst)) LNil = lfilter P (ltake (enat ?n) lst)
 2. ltl (lfilter P lst) = lfilter P (ldrop (enat ?n) lst)
[PROOF STEP]
hence null:"lnull (ltl (ldropWhile (Not \<circ> P) ?ltake))"
[PROOF STATE]
proof (prove)
using this:
llength (ldropWhile (Not \<circ> P) (ltake (enat (Suc (lfind P lst))) lst)) \<le> 1

goal (1 subgoal):
 1. lnull (ltl (ldropWhile (Not \<circ> P) (ltake (enat (Suc (lfind P lst))) lst)))
[PROOF STEP]
unfolding llength_eq_0[symmetric] llength_ltl
[PROOF STATE]
proof (prove)
using this:
llength (ldropWhile (Not \<circ> P) (ltake (enat (Suc (lfind P lst))) lst)) \<le> 1

goal (1 subgoal):
 1. epred (llength (ldropWhile (Not \<circ> P) (ltake (enat (Suc (lfind P lst))) lst))) = 0
[PROOF STEP]
by (metis dual_order.order_iff_strict enat_ile epred_0 epred_1 iless_Suc_eq le_zero_eq one_eSuc one_enat_def)
[PROOF STATE]
proof (state)
this:
lnull (ltl (ldropWhile (Not \<circ> P) (ltake (enat (Suc (lfind P lst))) lst)))

goal (2 subgoals):
 1. LCons (lhd (lfilter P lst)) LNil = lfilter P (ltake (enat ?n) lst)
 2. ltl (lfilter P lst) = lfilter P (ldrop (enat ?n) lst)
[PROOF STEP]
have e:"enat (lfind P lst) < enat (Suc (lfind P lst))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat (lfind P lst) < enat (Suc (lfind P lst))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
enat (lfind P lst) < enat (Suc (lfind P lst))

goal (2 subgoals):
 1. LCons (lhd (lfilter P lst)) LNil = lfilter P (ltake (enat ?n) lst)
 2. ltl (lfilter P lst) = lfilter P (ldrop (enat ?n) lst)
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
P (lst $ lfind P lst)
P (lst $ ?y) \<Longrightarrow> lfind P lst \<le> ?y
enat (lfind P lst) < llength lst
[PROOF STEP]
have "P (?ltake $ lfind P lst)"
[PROOF STATE]
proof (prove)
using this:
P (lst $ lfind P lst)
P (lst $ ?y) \<Longrightarrow> lfind P lst \<le> ?y
enat (lfind P lst) < llength lst

goal (1 subgoal):
 1. P (ltake (enat (Suc (lfind P lst))) lst $ lfind P lst)
[PROOF STEP]
using lnth_ltake[OF e]
[PROOF STATE]
proof (prove)
using this:
P (lst $ lfind P lst)
P (lst $ ?y) \<Longrightarrow> lfind P lst \<le> ?y
enat (lfind P lst) < llength lst
ltake (enat (Suc (lfind P lst))) ?xs $ lfind P lst = ?xs $ lfind P lst

goal (1 subgoal):
 1. P (ltake (enat (Suc (lfind P lst))) lst $ lfind P lst)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
P (ltake (enat (Suc (lfind P lst))) lst $ lfind P lst)

goal (2 subgoals):
 1. LCons (lhd (lfilter P lst)) LNil = lfilter P (ltake (enat ?n) lst)
 2. ltl (lfilter P lst) = lfilter P (ldrop (enat ?n) lst)
[PROOF STEP]
hence nonnull:"\<not> lnull (lfilter P ?ltake)"
[PROOF STATE]
proof (prove)
using this:
P (ltake (enat (Suc (lfind P lst))) lst $ lfind P lst)

goal (1 subgoal):
 1. \<not> lnull (lfilter P (ltake (enat (Suc (lfind P lst))) lst))
[PROOF STEP]
unfolding lnull_lfilter
[PROOF STATE]
proof (prove)
using this:
P (ltake (enat (Suc (lfind P lst))) lst $ lfind P lst)

goal (1 subgoal):
 1. \<not> (\<forall>x\<in>lset (ltake (enat (Suc (lfind P lst))) lst). \<not> P x)
[PROOF STEP]
by (metis "*"(3) e in_lset_conv_lnth leI llength_ltake' ltake_all)
[PROOF STATE]
proof (state)
this:
\<not> lnull (lfilter P (ltake (enat (Suc (lfind P lst))) lst))

goal (2 subgoals):
 1. LCons (lhd (lfilter P lst)) LNil = lfilter P (ltake (enat ?n) lst)
 2. ltl (lfilter P lst) = lfilter P (ldrop (enat ?n) lst)
[PROOF STEP]
show a:"LCons (lhd (lfilter P lst)) LNil = lfilter P ?ltake" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LCons (lhd (lfilter P lst)) LNil = lfilter P (ltake (enat (Suc (lfind P lst))) lst)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. LCons (lhd (lfilter P lst)) LNil = lfilter P (ltake (enat (Suc (lfind P lst))) lst)
[PROOF STEP]
have "lhd (lfilter P ?ltake) = lhd (lfilter P lst)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lhd (lfilter P (ltake (enat (Suc (lfind P lst))) lst)) = lhd (lfilter P lst)
[PROOF STEP]
by(rule lprefix_lhdD[OF lprefix_lfilterI[OF ltake_is_lprefix] nonnull])
[PROOF STATE]
proof (state)
this:
lhd (lfilter P (ltake (enat (Suc (lfind P lst))) lst)) = lhd (lfilter P lst)

goal (1 subgoal):
 1. LCons (lhd (lfilter P lst)) LNil = lfilter P (ltake (enat (Suc (lfind P lst))) lst)
[PROOF STEP]
hence h:"lhd ?lhs = lhd ?rhs"
[PROOF STATE]
proof (prove)
using this:
lhd (lfilter P (ltake (enat (Suc (lfind P lst))) lst)) = lhd (lfilter P lst)

goal (1 subgoal):
 1. lhd (LCons (lhd (lfilter P lst)) LNil) = lhd (lfilter P (ltake (enat (Suc (lfind P lst))) lst))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lhd (LCons (lhd (lfilter P lst)) LNil) = lhd (lfilter P (ltake (enat (Suc (lfind P lst))) lst))

goal (1 subgoal):
 1. LCons (lhd (lfilter P lst)) LNil = lfilter P (ltake (enat (Suc (lfind P lst))) lst)
[PROOF STEP]
have "ltl ?rhs = LNil"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ltl (lfilter P (ltake (enat (Suc (lfind P lst))) lst)) = LNil
[PROOF STEP]
unfolding ltl_lfilter
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lfilter P (ltl (ldropWhile (Not \<circ> P) (ltake (enat (Suc (lfind P lst))) lst))) = LNil
[PROOF STEP]
using null
[PROOF STATE]
proof (prove)
using this:
lnull (ltl (ldropWhile (Not \<circ> P) (ltake (enat (Suc (lfind P lst))) lst)))

goal (1 subgoal):
 1. lfilter P (ltl (ldropWhile (Not \<circ> P) (ltake (enat (Suc (lfind P lst))) lst))) = LNil
[PROOF STEP]
by (metis lfilter_LNil llist.collapse(1))
[PROOF STATE]
proof (state)
this:
ltl (lfilter P (ltake (enat (Suc (lfind P lst))) lst)) = LNil

goal (1 subgoal):
 1. LCons (lhd (lfilter P lst)) LNil = lfilter P (ltake (enat (Suc (lfind P lst))) lst)
[PROOF STEP]
hence t:"ltl ?lhs = ltl ?rhs"
[PROOF STATE]
proof (prove)
using this:
ltl (lfilter P (ltake (enat (Suc (lfind P lst))) lst)) = LNil

goal (1 subgoal):
 1. ltl (LCons (lhd (lfilter P lst)) LNil) = ltl (lfilter P (ltake (enat (Suc (lfind P lst))) lst))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ltl (LCons (lhd (lfilter P lst)) LNil) = ltl (lfilter P (ltake (enat (Suc (lfind P lst))) lst))

goal (1 subgoal):
 1. LCons (lhd (lfilter P lst)) LNil = lfilter P (ltake (enat (Suc (lfind P lst))) lst)
[PROOF STEP]
have flt:"?rhs \<noteq> LNil"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lfilter P (ltake (enat (Suc (lfind P lst))) lst) \<noteq> LNil
[PROOF STEP]
using nonnull
[PROOF STATE]
proof (prove)
using this:
\<not> lnull (lfilter P (ltake (enat (Suc (lfind P lst))) lst))

goal (1 subgoal):
 1. lfilter P (ltake (enat (Suc (lfind P lst))) lst) \<noteq> LNil
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
lfilter P (ltake (enat (Suc (lfind P lst))) lst) \<noteq> LNil

goal (1 subgoal):
 1. LCons (lhd (lfilter P lst)) LNil = lfilter P (ltake (enat (Suc (lfind P lst))) lst)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LCons (lhd (lfilter P lst)) LNil = lfilter P (ltake (enat (Suc (lfind P lst))) lst)
[PROOF STEP]
by(rule llist_eq_lcons[of ?lhs ?rhs,OF _ flt h t],auto)
[PROOF STATE]
proof (state)
this:
LCons (lhd (lfilter P lst)) LNil = lfilter P (ltake (enat (Suc (lfind P lst))) lst)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
LCons (lhd (lfilter P lst)) LNil = lfilter P (ltake (enat (Suc (lfind P lst))) lst)

goal (1 subgoal):
 1. ltl (lfilter P lst) = lfilter P (ldrop (enat (Suc (lfind P lst))) lst)
[PROOF STEP]
from lappend_ltake_ldrop[of ?n lst] lappend_ltakeWhile_ldropWhile[of "Not \<circ> P" lst]
[PROOF STATE]
proof (chain)
picking this:
lappend (ltake (enat (Suc (lfind P lst))) lst) (ldrop (enat (Suc (lfind P lst))) lst) = lst
lappend (ltakeWhile (Not \<circ> P) lst) (ldropWhile (Not \<circ> P) lst) = lst
[PROOF STEP]
have "lappend (ltake ?n lst) (ldrop ?n lst) = lappend (ltakeWhile (Not \<circ> P) lst) (ldropWhile (Not \<circ> P) lst)"
[PROOF STATE]
proof (prove)
using this:
lappend (ltake (enat (Suc (lfind P lst))) lst) (ldrop (enat (Suc (lfind P lst))) lst) = lst
lappend (ltakeWhile (Not \<circ> P) lst) (ldropWhile (Not \<circ> P) lst) = lst

goal (1 subgoal):
 1. lappend (ltake (enat (Suc (lfind P lst))) lst) (ldrop (enat (Suc (lfind P lst))) lst) = lappend (ltakeWhile (Not \<circ> P) lst) (ldropWhile (Not \<circ> P) lst)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lappend (ltake (enat (Suc (lfind P lst))) lst) (ldrop (enat (Suc (lfind P lst))) lst) = lappend (ltakeWhile (Not \<circ> P) lst) (ldropWhile (Not \<circ> P) lst)

goal (1 subgoal):
 1. ltl (lfilter P lst) = lfilter P (ldrop (enat (Suc (lfind P lst))) lst)
[PROOF STEP]
from ltake_lfind_conv(2)[OF assms]
[PROOF STATE]
proof (chain)
picking this:
ldrop (enat (lfind P lst)) lst = ldropWhile (Not \<circ> P) lst
[PROOF STEP]
have "ltl (ldropWhile (Not \<circ> P) lst) = ldrop (enat (Suc (lfind P lst))) lst"
[PROOF STATE]
proof (prove)
using this:
ldrop (enat (lfind P lst)) lst = ldropWhile (Not \<circ> P) lst

goal (1 subgoal):
 1. ltl (ldropWhile (Not \<circ> P) lst) = ldrop (enat (Suc (lfind P lst))) lst
[PROOF STEP]
unfolding ldrop_eSuc_conv_ltl eSuc_enat[symmetric]
[PROOF STATE]
proof (prove)
using this:
ldrop (enat (lfind P lst)) lst = ldropWhile (Not \<circ> P) lst

goal (1 subgoal):
 1. ltl (ldropWhile (Not \<circ> P) lst) = ltl (ldrop (enat (lfind P lst)) lst)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ltl (ldropWhile (Not \<circ> P) lst) = ldrop (enat (Suc (lfind P lst))) lst

goal (1 subgoal):
 1. ltl (lfilter P lst) = lfilter P (ldrop (enat (Suc (lfind P lst))) lst)
[PROOF STEP]
thus "ltl (lfilter P lst) = lfilter P (ldrop (enat ?n) lst)"
[PROOF STATE]
proof (prove)
using this:
ltl (ldropWhile (Not \<circ> P) lst) = ldrop (enat (Suc (lfind P lst))) lst

goal (1 subgoal):
 1. ltl (lfilter P lst) = lfilter P (ldrop (enat (Suc (lfind P lst))) lst)
[PROOF STEP]
unfolding ltl_lfilter
[PROOF STATE]
proof (prove)
using this:
ltl (ldropWhile (Not \<circ> P) lst) = ldrop (enat (Suc (lfind P lst))) lst

goal (1 subgoal):
 1. lfilter P (ltl (ldropWhile (Not \<circ> P) lst)) = lfilter P (ldrop (enat (Suc (lfind P lst))) lst)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
ltl (lfilter P lst) = lfilter P (ldrop (enat (Suc (lfind P lst))) lst)

goal:
No subgoals!
[PROOF STEP]
qed