[STATEMENT]
lemma dfs_reachable_correct: "dfs_reachable D w\<^sub>0 \<longleftrightarrow> Collect D \<inter> E\<^sup>* `` set w\<^sub>0 \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.dfs_reachable D w\<^sub>0 = (Collect D \<inter> (E_of_succ succ)\<^sup>* `` set w\<^sub>0 \<noteq> {})
[PROOF STEP]
unfolding dfs_reachable_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let (V, w, brk) = while (\<lambda>(V, w, brk). \<not> brk \<and> w \<noteq> []) (\<lambda>(V, w, uu_). case w of v # w \<Rightarrow> if D v then (V, v # w, True) else if v \<in> V then (V, w, False) else let V = insert v V; w = succ v @ w in (V, w, False)) ({}, w\<^sub>0, False) in brk) = (Collect D \<inter> (E_of_succ succ)\<^sup>* `` set w\<^sub>0 \<noteq> {})
[PROOF STEP]
apply (rule while_rule[where
    P="\<lambda>(V,w,brk). dfs_reachable_invar D V (set w) brk \<and> finite V"
    and r="measure (\<lambda>V. card (E\<^sup>* `` (set w\<^sub>0) - V)) <*lex*> measure length <*lex*> measure (\<lambda>True\<Rightarrow>0 | False\<Rightarrow>1)"
    ])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. case ({}, w\<^sub>0, False) of (V, w, brk) \<Rightarrow> local.dfs_reachable_invar D V (set w) brk \<and> finite V
 2. \<And>s. \<lbrakk>case s of (V, w, brk) \<Rightarrow> local.dfs_reachable_invar D V (set w) brk \<and> finite V; case s of (V, w, brk) \<Rightarrow> \<not> brk \<and> w \<noteq> []\<rbrakk> \<Longrightarrow> case case s of (V, v # wa, uu_) \<Rightarrow> if D v then (V, v # wa, True) else if v \<in> V then (V, wa, False) else let V = insert v V; w = succ v @ wa in (V, w, False) of (V, w, brk) \<Rightarrow> local.dfs_reachable_invar D V (set w) brk \<and> finite V
 3. \<And>s. \<lbrakk>case s of (V, w, brk) \<Rightarrow> local.dfs_reachable_invar D V (set w) brk \<and> finite V; \<not> (case s of (V, w, brk) \<Rightarrow> \<not> brk \<and> w \<noteq> [])\<rbrakk> \<Longrightarrow> (let a = s in case a of (V, w, brk) \<Rightarrow> brk) = ({a. D a} \<inter> (E_of_succ succ)\<^sup>* `` set w\<^sub>0 \<noteq> {})
 4. wf (measure (\<lambda>V. card ((E_of_succ succ)\<^sup>* `` set w\<^sub>0 - V)) <*lex*> measure length <*lex*> measure (\<lambda>x. case x of True \<Rightarrow> 0 | False \<Rightarrow> 1))
 5. \<And>s. \<lbrakk>case s of (V, w, brk) \<Rightarrow> local.dfs_reachable_invar D V (set w) brk \<and> finite V; case s of (V, w, brk) \<Rightarrow> \<not> brk \<and> w \<noteq> []\<rbrakk> \<Longrightarrow> (case s of (V, v # wa, uu_) \<Rightarrow> if D v then (V, v # wa, True) else if v \<in> V then (V, wa, False) else let V = insert v V; w = succ v @ wa in (V, w, False), s) \<in> measure (\<lambda>V. card ((E_of_succ succ)\<^sup>* `` set w\<^sub>0 - V)) <*lex*> measure length <*lex*> measure (\<lambda>x. case x of True \<Rightarrow> 0 | False \<Rightarrow> 1)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case ({}, w\<^sub>0, False) of (V, w, brk) \<Rightarrow> local.dfs_reachable_invar D V (set w) brk \<and> finite V
[PROOF STEP]
by (auto simp: dfs_reachable_invar_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>case s of (V, w, brk) \<Rightarrow> local.dfs_reachable_invar D V (set w) brk \<and> finite V; case s of (V, w, brk) \<Rightarrow> \<not> brk \<and> w \<noteq> []\<rbrakk> \<Longrightarrow> case case s of (V, v # wa, uu_) \<Rightarrow> if D v then (V, v # wa, True) else if v \<in> V then (V, wa, False) else let V = insert v V; w = succ v @ wa in (V, w, False) of (V, w, brk) \<Rightarrow> local.dfs_reachable_invar D V (set w) brk \<and> finite V
 2. \<And>s. \<lbrakk>case s of (V, w, brk) \<Rightarrow> local.dfs_reachable_invar D V (set w) brk \<and> finite V; \<not> (case s of (V, w, brk) \<Rightarrow> \<not> brk \<and> w \<noteq> [])\<rbrakk> \<Longrightarrow> (let a = s in case a of (V, w, brk) \<Rightarrow> brk) = ({a. D a} \<inter> (E_of_succ succ)\<^sup>* `` set w\<^sub>0 \<noteq> {})
 3. wf (measure (\<lambda>V. card ((E_of_succ succ)\<^sup>* `` set w\<^sub>0 - V)) <*lex*> measure length <*lex*> measure (\<lambda>x. case x of True \<Rightarrow> 0 | False \<Rightarrow> 1))
 4. \<And>s. \<lbrakk>case s of (V, w, brk) \<Rightarrow> local.dfs_reachable_invar D V (set w) brk \<and> finite V; case s of (V, w, brk) \<Rightarrow> \<not> brk \<and> w \<noteq> []\<rbrakk> \<Longrightarrow> (case s of (V, v # wa, uu_) \<Rightarrow> if D v then (V, v # wa, True) else if v \<in> V then (V, wa, False) else let V = insert v V; w = succ v @ wa in (V, w, False), s) \<in> measure (\<lambda>V. card ((E_of_succ succ)\<^sup>* `` set w\<^sub>0 - V)) <*lex*> measure length <*lex*> measure (\<lambda>x. case x of True \<Rightarrow> 0 | False \<Rightarrow> 1)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>case s_ of (V, w, brk) \<Rightarrow> local.dfs_reachable_invar D V (set w) brk \<and> finite V; case s_ of (V, w, brk) \<Rightarrow> \<not> brk \<and> w \<noteq> []\<rbrakk> \<Longrightarrow> case case s_ of (V, v # wa, uu_) \<Rightarrow> if D v then (V, v # wa, True) else if v \<in> V then (V, wa, False) else let V = insert v V; w = succ v @ wa in (V, w, False) of (V, w, brk) \<Rightarrow> local.dfs_reachable_invar D V (set w) brk \<and> finite V
[PROOF STEP]
apply (auto simp: neq_Nil_conv succ_as_E[of succ] split: if_splits)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>V b ba y ys. \<lbrakk>s_ = (V, y # ys, False); \<not> ba; local.dfs_reachable_invar D V (insert y (set ys)) False; finite V; D y; b\<rbrakk> \<Longrightarrow> local.dfs_reachable_invar D V (insert y (set ys)) True
 2. \<And>V a b ba y. \<lbrakk>s_ = (V, y # a, False); \<not> ba; local.dfs_reachable_invar D V (insert y (set a)) False; finite V; \<not> D y; y \<in> V; \<not> b\<rbrakk> \<Longrightarrow> local.dfs_reachable_invar D V (set a) False
 3. \<And>b x ba y ys. \<lbrakk>s_ = (x, y # ys, False); \<not> ba; local.dfs_reachable_invar D x (insert y (set ys)) False; finite x; \<not> D y; y \<notin> x; \<not> b\<rbrakk> \<Longrightarrow> local.dfs_reachable_invar D (insert y x) (E_of_succ succ `` {y} \<union> set ys) False
[PROOF STEP]
by (auto simp: dfs_reachable_invar_def Image_iff intro: rtrancl.rtrancl_into_rtrancl)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>case s of (V, w, brk) \<Rightarrow> local.dfs_reachable_invar D V (set w) brk \<and> finite V; \<not> (case s of (V, w, brk) \<Rightarrow> \<not> brk \<and> w \<noteq> [])\<rbrakk> \<Longrightarrow> (let a = s in case a of (V, w, brk) \<Rightarrow> brk) = ({a. D a} \<inter> (E_of_succ succ)\<^sup>* `` set w\<^sub>0 \<noteq> {})
 2. wf (measure (\<lambda>V. card ((E_of_succ succ)\<^sup>* `` set w\<^sub>0 - V)) <*lex*> measure length <*lex*> measure (\<lambda>x. case x of True \<Rightarrow> 0 | False \<Rightarrow> 1))
 3. \<And>s. \<lbrakk>case s of (V, w, brk) \<Rightarrow> local.dfs_reachable_invar D V (set w) brk \<and> finite V; case s of (V, w, brk) \<Rightarrow> \<not> brk \<and> w \<noteq> []\<rbrakk> \<Longrightarrow> (case s of (V, v # wa, uu_) \<Rightarrow> if D v then (V, v # wa, True) else if v \<in> V then (V, wa, False) else let V = insert v V; w = succ v @ wa in (V, w, False), s) \<in> measure (\<lambda>V. card ((E_of_succ succ)\<^sup>* `` set w\<^sub>0 - V)) <*lex*> measure length <*lex*> measure (\<lambda>x. case x of True \<Rightarrow> 0 | False \<Rightarrow> 1)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>case s_ of (V, w, brk) \<Rightarrow> local.dfs_reachable_invar D V (set w) brk \<and> finite V; \<not> (case s_ of (V, w, brk) \<Rightarrow> \<not> brk \<and> w \<noteq> [])\<rbrakk> \<Longrightarrow> (let a = s_ in case a of (V, w, brk) \<Rightarrow> brk) = ({a. D a} \<inter> (E_of_succ succ)\<^sup>* `` set w\<^sub>0 \<noteq> {})
[PROOF STEP]
by (fastforce simp: dfs_reachable_invar_def dest: Image_closed_trancl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. wf (measure (\<lambda>V. card ((E_of_succ succ)\<^sup>* `` set w\<^sub>0 - V)) <*lex*> measure length <*lex*> measure (\<lambda>x. case x of True \<Rightarrow> 0 | False \<Rightarrow> 1))
 2. \<And>s. \<lbrakk>case s of (V, w, brk) \<Rightarrow> local.dfs_reachable_invar D V (set w) brk \<and> finite V; case s of (V, w, brk) \<Rightarrow> \<not> brk \<and> w \<noteq> []\<rbrakk> \<Longrightarrow> (case s of (V, v # wa, uu_) \<Rightarrow> if D v then (V, v # wa, True) else if v \<in> V then (V, wa, False) else let V = insert v V; w = succ v @ wa in (V, w, False), s) \<in> measure (\<lambda>V. card ((E_of_succ succ)\<^sup>* `` set w\<^sub>0 - V)) <*lex*> measure length <*lex*> measure (\<lambda>x. case x of True \<Rightarrow> 0 | False \<Rightarrow> 1)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (measure (\<lambda>V. card ((E_of_succ succ)\<^sup>* `` set w\<^sub>0 - V)) <*lex*> measure length <*lex*> measure (\<lambda>x. case x of True \<Rightarrow> 0 | False \<Rightarrow> 1))
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>case s of (V, w, brk) \<Rightarrow> local.dfs_reachable_invar D V (set w) brk \<and> finite V; case s of (V, w, brk) \<Rightarrow> \<not> brk \<and> w \<noteq> []\<rbrakk> \<Longrightarrow> (case s of (V, v # wa, uu_) \<Rightarrow> if D v then (V, v # wa, True) else if v \<in> V then (V, wa, False) else let V = insert v V; w = succ v @ wa in (V, w, False), s) \<in> measure (\<lambda>V. card ((E_of_succ succ)\<^sup>* `` set w\<^sub>0 - V)) <*lex*> measure length <*lex*> measure (\<lambda>x. case x of True \<Rightarrow> 0 | False \<Rightarrow> 1)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>case s_ of (V, w, brk) \<Rightarrow> local.dfs_reachable_invar D V (set w) brk \<and> finite V; case s_ of (V, w, brk) \<Rightarrow> \<not> brk \<and> w \<noteq> []\<rbrakk> \<Longrightarrow> (case s_ of (V, v # wa, uu_) \<Rightarrow> if D v then (V, v # wa, True) else if v \<in> V then (V, wa, False) else let V = insert v V; w = succ v @ wa in (V, w, False), s_) \<in> measure (\<lambda>V. card ((E_of_succ succ)\<^sup>* `` set w\<^sub>0 - V)) <*lex*> measure length <*lex*> measure (\<lambda>x. case x of True \<Rightarrow> 0 | False \<Rightarrow> 1)
[PROOF STEP]
by (auto simp: neq_Nil_conv card_decreases)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Some_eq_map_option [iff]: "(Some y = map_option f xo) = (\<exists>z. xo = Some z \<and> f z = y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Some y = map_option f xo) = (\<exists>z. xo = Some z \<and> f z = y)
[PROOF STEP]
by (auto simp add: map_option_case split: option.split)


[STATEMENT]
lemma tab_succ_correct: "E_of_succ (tab_succ l) = set l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E_of_succ (tab_succ l) = set l
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. E_of_succ (tab_succ l) = set l
[PROOF STEP]
have "set (Mapping.lookup_default [] (fold (\<lambda>(u,v). Mapping.map_default u [] (Cons v)) l m) u) = set l `` {u} \<union> set (Mapping.lookup_default [] m u)"
    for m u
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (Mapping.lookup_default [] (fold (\<lambda>(u, v). Mapping.map_default u [] ((#) v)) l m) u) = set l `` {u} \<union> set (Mapping.lookup_default [] m u)
[PROOF STEP]
apply (induction l arbitrary: m)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m. set (Mapping.lookup_default [] (fold (\<lambda>(u, v). Mapping.map_default u [] ((#) v)) [] m) u) = set [] `` {u} \<union> set (Mapping.lookup_default [] m u)
 2. \<And>a l m. (\<And>m. set (Mapping.lookup_default [] (fold (\<lambda>(u, v). Mapping.map_default u [] ((#) v)) l m) u) = set l `` {u} \<union> set (Mapping.lookup_default [] m u)) \<Longrightarrow> set (Mapping.lookup_default [] (fold (\<lambda>(u, v). Mapping.map_default u [] ((#) v)) (a # l) m) u) = set (a # l) `` {u} \<union> set (Mapping.lookup_default [] m u)
[PROOF STEP]
by (auto
      simp: Mapping.lookup_default_def Mapping.map_default_def Mapping.default_def
      simp: lookup_map_entry' lookup_update' keys_is_none_rep Option.is_none_def
      split: if_splits
    )
[PROOF STATE]
proof (state)
this:
set (Mapping.lookup_default [] (fold (\<lambda>(u, v). Mapping.map_default u [] ((#) v)) l ?m) ?u) = set l `` {?u} \<union> set (Mapping.lookup_default [] ?m ?u)

goal (1 subgoal):
 1. E_of_succ (tab_succ l) = set l
[PROOF STEP]
from this[where m=Mapping.empty]
[PROOF STATE]
proof (chain)
picking this:
set (Mapping.lookup_default [] (fold (\<lambda>(u, v). Mapping.map_default u [] ((#) v)) l Mapping.empty) ?u) = set l `` {?u} \<union> set (Mapping.lookup_default [] Mapping.empty ?u)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set (Mapping.lookup_default [] (fold (\<lambda>(u, v). Mapping.map_default u [] ((#) v)) l Mapping.empty) ?u) = set l `` {?u} \<union> set (Mapping.lookup_default [] Mapping.empty ?u)

goal (1 subgoal):
 1. E_of_succ (tab_succ l) = set l
[PROOF STEP]
by (auto simp: E_of_succ_def tab_succ_def lookup_default_empty)
[PROOF STATE]
proof (state)
this:
E_of_succ (tab_succ l) = set l

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_imp_finite_dfs_reachable:
  "\<lbrakk>finite E; finite S\<rbrakk> \<Longrightarrow> finite (E\<^sup>*``S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite E; finite S\<rbrakk> \<Longrightarrow> finite (E\<^sup>* `` S)
[PROOF STEP]
apply (rule finite_subset[where B="S \<union> (Relation.Domain E \<union> Relation.Range E)"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>finite E; finite S\<rbrakk> \<Longrightarrow> E\<^sup>* `` S \<subseteq> S \<union> (Relation.Domain E \<union> Range E)
 2. \<lbrakk>finite E; finite S\<rbrakk> \<Longrightarrow> finite (S \<union> (Relation.Domain E \<union> Range E))
[PROOF STEP]
apply (auto simp: intro: finite_Domain finite_Range elim: rtranclE)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma dfs_reachable_tab_succ_correct: "dfs_reachable (tab_succ l) D vs\<^sub>0 \<longleftrightarrow> Collect D \<inter> (set l)\<^sup>*``set vs\<^sub>0 \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dfs_reachable (tab_succ l) D vs\<^sub>0 = (Collect D \<inter> (set l)\<^sup>* `` set vs\<^sub>0 \<noteq> {})
[PROOF STEP]
apply (subst dfs_reachable_correct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite ((E_of_succ (tab_succ l))\<^sup>* `` set vs\<^sub>0)
 2. (Collect D \<inter> (E_of_succ (tab_succ l))\<^sup>* `` set vs\<^sub>0 \<noteq> {}) = (Collect D \<inter> (set l)\<^sup>* `` set vs\<^sub>0 \<noteq> {})
[PROOF STEP]
by (simp_all add: tab_succ_correct finite_imp_finite_dfs_reachable)


[STATEMENT]
lemma ty_term'_correct_aux: "ty_term' varT objT t = ty_term varT (Mapping.lookup objT) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ty_term' varT objT t = ty_term varT (Mapping.lookup objT) t
[PROOF STEP]
by (cases t) auto


[STATEMENT]
lemma ty_term'_correct[simp]: "ty_term' varT objT = ty_term varT (Mapping.lookup objT)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ty_term' varT objT = ty_term varT (Mapping.lookup objT)
[PROOF STEP]
using ty_term'_correct_aux
[PROOF STATE]
proof (prove)
using this:
ty_term' ?varT ?objT ?t = ty_term ?varT (Mapping.lookup ?objT) ?t

goal (1 subgoal):
 1. ty_term' varT objT = ty_term varT (Mapping.lookup objT)
[PROOF STEP]
by auto


[STATEMENT]
lemma of_type_refine1: "of_type oT T \<longleftrightarrow> (\<forall>pt\<in>set (primitives oT). of_type1 pt T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_type oT T = (\<forall>pt\<in>set (primitives oT). of_type1 pt T)
[PROOF STEP]
unfolding of_type_def of_type1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (set (primitives oT) \<subseteq> subtype_rel\<^sup>* `` set (primitives T)) = (\<forall>pt\<in>set (primitives oT). pt \<in> subtype_rel\<^sup>* `` set (primitives T))
[PROOF STEP]
by auto


[STATEMENT]
lemma subtype_rel_impl: "subtype_rel = E_of_succ (tab_succ (map subtype_edge (types D)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subtype_rel = E_of_succ (tab_succ (map subtype_edge (types D)))
[PROOF STEP]
by (simp add: tab_succ_correct subtype_rel_def)


[STATEMENT]
lemma of_type1_impl: "of_type1 pt T \<longleftrightarrow> dfs_reachable (tab_succ (map subtype_edge (types D))) ((=)pt) (primitives T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_type1 pt T = dfs_reachable (tab_succ (map subtype_edge (types D))) ((=) pt) (primitives T)
[PROOF STEP]
by (simp add: subtype_rel_impl of_type1_def dfs_reachable_tab_succ_correct tab_succ_correct)


[STATEMENT]
lemma of_type_impl_correct: "of_type_impl STG oT T \<longleftrightarrow> of_type oT T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_type_impl STG oT T = of_type oT T
[PROOF STEP]
unfolding of_type1_impl STG_def of_type_impl_def of_type_refine1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>pt\<in>set (primitives oT). dfs_reachable (tab_succ (map subtype_edge (types D))) ((=) pt) (primitives T)) = (\<forall>pt\<in>set (primitives oT). dfs_reachable (tab_succ (map subtype_edge (types D))) ((=) pt) (primitives T))
[PROOF STEP]
..


[STATEMENT]
lemma mp_objT_correct[simp]: "Mapping.lookup mp_constT = constT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.lookup mp_constT = constT
[PROOF STEP]
unfolding mp_constT_def constT_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.lookup (Mapping.of_alist (consts D)) = map_of (consts D)
[PROOF STEP]
by transfer (simp add: Map_To_Mapping.map_apply_def)


[STATEMENT]
lemma is_of_type'_correct: "is_of_type' STG v T = is_of_type ty_ent v T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_of_type' STG v T = is_of_type ty_ent v T
[PROOF STEP]
unfolding is_of_type'_def is_of_type_def of_type_impl_correct
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case ty_ent v of None \<Rightarrow> False | Some vT \<Rightarrow> of_type vT T) = (case ty_ent v of None \<Rightarrow> False | Some vT \<Rightarrow> of_type vT T)
[PROOF STEP]
..


[STATEMENT]
lemma wf_pred_atom'_correct: "wf_pred_atom' STG pvs = wf_pred_atom ty_ent pvs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_pred_atom' STG pvs = wf_pred_atom ty_ent pvs
[PROOF STEP]
by (cases pvs) (auto simp: is_of_type'_correct[abs_def] split:option.split)


[STATEMENT]
lemma wf_atom'_correct: "wf_atom' STG a = wf_atom ty_ent a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_atom' STG a = wf_atom ty_ent a
[PROOF STEP]
by (cases a) (auto simp: wf_pred_atom'_correct is_of_type'_correct[abs_def] split: option.splits)


[STATEMENT]
lemma wf_fmla'_correct: "wf_fmla' STG \<phi> \<longleftrightarrow> wf_fmla ty_ent \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_fmla' STG \<phi> = wf_fmla ty_ent \<phi>
[PROOF STEP]
by (induction \<phi> rule: wf_fmla.induct) (auto simp: wf_atom'_correct)


[STATEMENT]
lemma wf_fmla_atom1'_correct: "wf_fmla_atom1' STG \<phi> = wf_fmla_atom ty_ent \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_fmla_atom1' STG \<phi> = wf_fmla_atom ty_ent \<phi>
[PROOF STEP]
by (cases \<phi> rule: wf_fmla_atom.cases) (auto
        simp: wf_atom'_correct is_of_type'_correct[abs_def] split: option.splits)


[STATEMENT]
lemma wf_effect'_correct: "wf_effect' STG e = wf_effect ty_ent e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_effect' STG e = wf_effect ty_ent e
[PROOF STEP]
by (cases e) (auto simp: wf_fmla_atom1'_correct)


[STATEMENT]
lemma wf_action_schema'_correct: "wf_action_schema' STG mp_constT s = wf_action_schema s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_action_schema' STG mp_constT s = wf_action_schema s
[PROOF STEP]
by (cases s) (auto simp: wf_fmla'_correct wf_effect'_correct)


[STATEMENT]
lemma wf_domain'_correct: "wf_domain' STG mp_constT = wf_domain"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_domain' STG mp_constT = wf_domain
[PROOF STEP]
unfolding wf_domain_def wf_domain'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (wf_types \<and> distinct (map pred (predicates D)) \<and> Ball (set (predicates D)) wf_predicate_decl \<and> distinct (map fst (consts D)) \<and> (\<forall>(n, y)\<in>set (consts D). wf_type y) \<and> distinct (map ast_action_schema.name (actions D)) \<and> (\<forall>a\<in>set (actions D). wf_action_schema' STG mp_constT a)) = (wf_types \<and> distinct (map pred (predicates D)) \<and> Ball (set (predicates D)) wf_predicate_decl \<and> distinct (map fst (consts D)) \<and> (\<forall>(n, y)\<in>set (consts D). wf_type y) \<and> distinct (map ast_action_schema.name (actions D)) \<and> Ball (set (actions D)) wf_action_schema)
[PROOF STEP]
by (auto simp: wf_action_schema'_correct)


[STATEMENT]
lemma apply_effect_exec_refine[simp]:
    "apply_effect_exec (Effect (a) (d)) s
    = apply_effect (Effect (a) (d)) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_effect_exec (Effect a d) s = apply_effect (Effect a d) s
[PROOF STEP]
proof(induction a arbitrary: s)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. apply_effect_exec (Effect [] d) s = apply_effect (Effect [] d) s
 2. \<And>a1 a2 s. (\<And>s. apply_effect_exec (Effect a2 d) s = apply_effect (Effect a2 d) s) \<Longrightarrow> apply_effect_exec (Effect (a1 # a2) d) s = apply_effect (Effect (a1 # a2) d) s
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>s. apply_effect_exec (Effect [] d) s = apply_effect (Effect [] d) s
 2. \<And>a1 a2 s. (\<And>s. apply_effect_exec (Effect a2 d) s = apply_effect (Effect a2 d) s) \<Longrightarrow> apply_effect_exec (Effect (a1 # a2) d) s = apply_effect (Effect (a1 # a2) d) s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_effect_exec (Effect [] d) s = apply_effect (Effect [] d) s
[PROOF STEP]
proof(induction d arbitrary: s)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. apply_effect_exec (Effect [] []) s = apply_effect (Effect [] []) s
 2. \<And>a d s. (\<And>s. apply_effect_exec (Effect [] d) s = apply_effect (Effect [] d) s) \<Longrightarrow> apply_effect_exec (Effect [] (a # d)) s = apply_effect (Effect [] (a # d)) s
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>s. apply_effect_exec (Effect [] []) s = apply_effect (Effect [] []) s
 2. \<And>a d s. (\<And>s. apply_effect_exec (Effect [] d) s = apply_effect (Effect [] d) s) \<Longrightarrow> apply_effect_exec (Effect [] (a # d)) s = apply_effect (Effect [] (a # d)) s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_effect_exec (Effect [] []) s = apply_effect (Effect [] []) s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
apply_effect_exec (Effect [] []) s = apply_effect (Effect [] []) s

goal (1 subgoal):
 1. \<And>a d s. (\<And>s. apply_effect_exec (Effect [] d) s = apply_effect (Effect [] d) s) \<Longrightarrow> apply_effect_exec (Effect [] (a # d)) s = apply_effect (Effect [] (a # d)) s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a d s. (\<And>s. apply_effect_exec (Effect [] d) s = apply_effect (Effect [] d) s) \<Longrightarrow> apply_effect_exec (Effect [] (a # d)) s = apply_effect (Effect [] (a # d)) s
[PROOF STEP]
case (Cons a d)
[PROOF STATE]
proof (state)
this:
apply_effect_exec (Effect [] d) ?s32 = apply_effect (Effect [] d) ?s32

goal (1 subgoal):
 1. \<And>a d s. (\<And>s. apply_effect_exec (Effect [] d) s = apply_effect (Effect [] d) s) \<Longrightarrow> apply_effect_exec (Effect [] (a # d)) s = apply_effect (Effect [] (a # d)) s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
apply_effect_exec (Effect [] d) ?s32 = apply_effect (Effect [] d) ?s32
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
apply_effect_exec (Effect [] d) ?s32 = apply_effect (Effect [] d) ?s32

goal (1 subgoal):
 1. apply_effect_exec (Effect [] (a # d)) s = apply_effect (Effect [] (a # d)) s
[PROOF STEP]
by (auto simp add: image_def)
[PROOF STATE]
proof (state)
this:
apply_effect_exec (Effect [] (a # d)) s = apply_effect (Effect [] (a # d)) s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
apply_effect_exec (Effect [] d) s = apply_effect (Effect [] d) s

goal (1 subgoal):
 1. \<And>a1 a2 s. (\<And>s. apply_effect_exec (Effect a2 d) s = apply_effect (Effect a2 d) s) \<Longrightarrow> apply_effect_exec (Effect (a1 # a2) d) s = apply_effect (Effect (a1 # a2) d) s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a1 a2 s. (\<And>s. apply_effect_exec (Effect a2 d) s = apply_effect (Effect a2 d) s) \<Longrightarrow> apply_effect_exec (Effect (a1 # a2) d) s = apply_effect (Effect (a1 # a2) d) s
[PROOF STEP]
case (Cons a a)
[PROOF STATE]
proof (state)
this:
apply_effect_exec (Effect a d) ?s32 = apply_effect (Effect a d) ?s32

goal (1 subgoal):
 1. \<And>a1 a2 s. (\<And>s. apply_effect_exec (Effect a2 d) s = apply_effect (Effect a2 d) s) \<Longrightarrow> apply_effect_exec (Effect (a1 # a2) d) s = apply_effect (Effect (a1 # a2) d) s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
apply_effect_exec (Effect a d) ?s32 = apply_effect (Effect a d) ?s32
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
apply_effect_exec (Effect a d) ?s32 = apply_effect (Effect a d) ?s32

goal (1 subgoal):
 1. apply_effect_exec (Effect (aa__ # a) d) s = apply_effect (Effect (aa__ # a) d) s
[PROOF STEP]
proof(induction d arbitrary: s)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. (\<And>s. apply_effect_exec (Effect a []) s = apply_effect (Effect a []) s) \<Longrightarrow> apply_effect_exec (Effect (aa__ # a) []) s = apply_effect (Effect (aa__ # a) []) s
 2. \<And>a d s. \<lbrakk>\<And>s. (\<And>s. apply_effect_exec (Effect a d) s = apply_effect (Effect a d) s) \<Longrightarrow> apply_effect_exec (Effect (aa__ # a) d) s = apply_effect (Effect (aa__ # a) d) s; \<And>s. apply_effect_exec (Effect a (a # d)) s = apply_effect (Effect a (a # d)) s\<rbrakk> \<Longrightarrow> apply_effect_exec (Effect (aa__ # a) (a # d)) s = apply_effect (Effect (aa__ # a) (a # d)) s
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
apply_effect_exec (Effect a []) ?s32 = apply_effect (Effect a []) ?s32

goal (2 subgoals):
 1. \<And>s. (\<And>s. apply_effect_exec (Effect a []) s = apply_effect (Effect a []) s) \<Longrightarrow> apply_effect_exec (Effect (aa__ # a) []) s = apply_effect (Effect (aa__ # a) []) s
 2. \<And>a d s. \<lbrakk>\<And>s. (\<And>s. apply_effect_exec (Effect a d) s = apply_effect (Effect a d) s) \<Longrightarrow> apply_effect_exec (Effect (aa__ # a) d) s = apply_effect (Effect (aa__ # a) d) s; \<And>s. apply_effect_exec (Effect a (a # d)) s = apply_effect (Effect a (a # d)) s\<rbrakk> \<Longrightarrow> apply_effect_exec (Effect (aa__ # a) (a # d)) s = apply_effect (Effect (aa__ # a) (a # d)) s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
apply_effect_exec (Effect a []) ?s32 = apply_effect (Effect a []) ?s32
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
apply_effect_exec (Effect a []) ?s32 = apply_effect (Effect a []) ?s32

goal (1 subgoal):
 1. apply_effect_exec (Effect (aa__ # a) []) s = apply_effect (Effect (aa__ # a) []) s
[PROOF STEP]
by (auto; metis Set.insert_def sup_assoc insert_iff)
[PROOF STATE]
proof (state)
this:
apply_effect_exec (Effect (aa__ # a) []) s = apply_effect (Effect (aa__ # a) []) s

goal (1 subgoal):
 1. \<And>a d s. \<lbrakk>\<And>s. (\<And>s. apply_effect_exec (Effect a d) s = apply_effect (Effect a d) s) \<Longrightarrow> apply_effect_exec (Effect (aa__ # a) d) s = apply_effect (Effect (aa__ # a) d) s; \<And>s. apply_effect_exec (Effect a (a # d)) s = apply_effect (Effect a (a # d)) s\<rbrakk> \<Longrightarrow> apply_effect_exec (Effect (aa__ # a) (a # d)) s = apply_effect (Effect (aa__ # a) (a # d)) s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a d s. \<lbrakk>\<And>s. (\<And>s. apply_effect_exec (Effect a d) s = apply_effect (Effect a d) s) \<Longrightarrow> apply_effect_exec (Effect (aa__ # a) d) s = apply_effect (Effect (aa__ # a) d) s; \<And>s. apply_effect_exec (Effect a (a # d)) s = apply_effect (Effect a (a # d)) s\<rbrakk> \<Longrightarrow> apply_effect_exec (Effect (aa__ # a) (a # d)) s = apply_effect (Effect (aa__ # a) (a # d)) s
[PROOF STEP]
case (Cons a d)
[PROOF STATE]
proof (state)
this:
(\<And>s. apply_effect_exec (Effect ab__ d) s = apply_effect (Effect ab__ d) s) \<Longrightarrow> apply_effect_exec (Effect (aa__ # ab__) d) ?s32 = apply_effect (Effect (aa__ # ab__) d) ?s32
apply_effect_exec (Effect ab__ (a # d)) ?s32 = apply_effect (Effect ab__ (a # d)) ?s32

goal (1 subgoal):
 1. \<And>a d s. \<lbrakk>\<And>s. (\<And>s. apply_effect_exec (Effect ab__ d) s = apply_effect (Effect ab__ d) s) \<Longrightarrow> apply_effect_exec (Effect (aa__ # ab__) d) s = apply_effect (Effect (aa__ # ab__) d) s; \<And>s. apply_effect_exec (Effect ab__ (a # d)) s = apply_effect (Effect ab__ (a # d)) s\<rbrakk> \<Longrightarrow> apply_effect_exec (Effect (aa__ # ab__) (a # d)) s = apply_effect (Effect (aa__ # ab__) (a # d)) s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<And>s. apply_effect_exec (Effect ab__ d) s = apply_effect (Effect ab__ d) s) \<Longrightarrow> apply_effect_exec (Effect (aa__ # ab__) d) ?s32 = apply_effect (Effect (aa__ # ab__) d) ?s32
apply_effect_exec (Effect ab__ (a # d)) ?s32 = apply_effect (Effect ab__ (a # d)) ?s32
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<And>s. apply_effect_exec (Effect ab__ d) s = apply_effect (Effect ab__ d) s) \<Longrightarrow> apply_effect_exec (Effect (aa__ # ab__) d) ?s32 = apply_effect (Effect (aa__ # ab__) d) ?s32
apply_effect_exec (Effect ab__ (a # d)) ?s32 = apply_effect (Effect ab__ (a # d)) ?s32

goal (1 subgoal):
 1. apply_effect_exec (Effect (aa__ # ab__) (a # d)) s = apply_effect (Effect (aa__ # ab__) (a # d)) s
[PROOF STEP]
by (auto simp: Un_commute minus_set_fold union_set_fold)
[PROOF STATE]
proof (state)
this:
apply_effect_exec (Effect (aa__ # ab__) (a # d)) s = apply_effect (Effect (aa__ # ab__) (a # d)) s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
apply_effect_exec (Effect (aa__ # a) d) s = apply_effect (Effect (aa__ # a) d) s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mp_objT_correct[simp]: "Mapping.lookup mp_objT = objT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.lookup mp_objT = objT
[PROOF STEP]
unfolding mp_objT_def objT_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.lookup (Mapping.of_alist (consts D @ objects P)) = map_of (consts D @ objects P)
[PROOF STEP]
by transfer (simp add: Map_To_Mapping.map_apply_def)


[STATEMENT]
lemma is_obj_of_type_impl_correct[simp]:
    "is_obj_of_type_impl STG mp_objT = is_obj_of_type"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_obj_of_type_impl STG mp_objT = is_obj_of_type
[PROOF STEP]
apply (intro ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. is_obj_of_type_impl STG mp_objT x xa = is_obj_of_type x xa
[PROOF STEP]
apply (auto simp: is_obj_of_type_impl_def is_obj_of_type_def of_type_impl_correct split: option.split)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma wf_fact'_correct[simp]: "wf_fact' mp_objT STG = wf_fact"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_fact' mp_objT STG = wf_fact
[PROOF STEP]
by (auto simp: wf_fact'_def wf_fact_def wf_pred_atom'_correct[abs_def])


[STATEMENT]
lemma wf_fmla_atom2'_correct[simp]:
    "wf_fmla_atom2' mp_objT STG \<phi> = wf_fmla_atom objT \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_fmla_atom2' mp_objT STG \<phi> = wf_fmla_atom objT \<phi>
[PROOF STEP]
apply (cases \<phi> rule: wf_fmla_atom.cases)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>a vs. \<phi> = Atom (predAtm a vs) \<Longrightarrow> wf_fmla_atom2' mp_objT STG \<phi> = wf_fmla_atom objT \<phi>
 2. \<And>va vb. \<phi> = Atom (atom.Eq va vb) \<Longrightarrow> wf_fmla_atom2' mp_objT STG \<phi> = wf_fmla_atom objT \<phi>
 3. \<phi> = \<bottom> \<Longrightarrow> wf_fmla_atom2' mp_objT STG \<phi> = wf_fmla_atom objT \<phi>
 4. \<And>v. \<phi> = \<^bold>\<not> v \<Longrightarrow> wf_fmla_atom2' mp_objT STG \<phi> = wf_fmla_atom objT \<phi>
 5. \<And>v va. \<phi> = v \<^bold>\<and> va \<Longrightarrow> wf_fmla_atom2' mp_objT STG \<phi> = wf_fmla_atom objT \<phi>
 6. \<And>v va. \<phi> = v \<^bold>\<or> va \<Longrightarrow> wf_fmla_atom2' mp_objT STG \<phi> = wf_fmla_atom objT \<phi>
 7. \<And>v va. \<phi> = v \<^bold>\<rightarrow> va \<Longrightarrow> wf_fmla_atom2' mp_objT STG \<phi> = wf_fmla_atom objT \<phi>
[PROOF STEP]
by (auto simp: wf_fmla_atom2'_def wf_fact_def split: option.splits)


[STATEMENT]
lemma wf_problem'_correct:
    "wf_problem' STG mp_constT mp_objT = wf_problem"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_problem' STG mp_constT mp_objT = wf_problem
[PROOF STEP]
unfolding wf_problem_def wf_problem'_def wf_world_model_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (wf_domain' STG mp_constT \<and> distinct (map fst (objects P) @ map fst (consts D)) \<and> (\<forall>(n, y)\<in>set (objects P). wf_type y) \<and> distinct (init P) \<and> (\<forall>f\<in>set (init P). wf_fmla_atom2' mp_objT STG f) \<and> wf_fmla' (Mapping.lookup mp_objT) STG (goal P)) = (wf_domain \<and> distinct (map fst (objects P) @ map fst (consts D)) \<and> (\<forall>(n, y)\<in>set (objects P). wf_type y) \<and> distinct (init P) \<and> Ball (set (init P)) (wf_fmla_atom objT) \<and> wf_fmla objT (goal P))
[PROOF STEP]
by (auto simp: wf_domain'_correct wf_fmla'_correct)


[STATEMENT]
lemma wf_effect_inst_weak:
    fixes a args
    defines "ai \<equiv> instantiate_action_schema a args"
    assumes A: "action_params_match a args"
      "wf_action_schema a"
    shows "wf_effect_inst (effect ai)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_effect_inst (ground_action.effect ai)
[PROOF STEP]
using wf_instantiate_action_schema[OF A]
[PROOF STATE]
proof (prove)
using this:
wf_ground_action (instantiate_action_schema a args)

goal (1 subgoal):
 1. wf_effect_inst (ground_action.effect ai)
[PROOF STEP]
unfolding ai_def[symmetric]
[PROOF STATE]
proof (prove)
using this:
wf_ground_action ai

goal (1 subgoal):
 1. wf_effect_inst (ground_action.effect ai)
[PROOF STEP]
by (cases ai) (auto simp: wf_effect_inst_alt)


[STATEMENT]
lemma resolve_action_wf:
    assumes "resolve_action_schema n = Some a"
    shows "wf_action_schema a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_action_schema a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_action_schema a
[PROOF STEP]
from wf_domain
[PROOF STATE]
proof (chain)
picking this:
wf_domain
[PROOF STEP]
have
      X1: "distinct (map ast_action_schema.name (actions D))"
      and X2: "\<forall>a\<in>set (actions D). wf_action_schema a"
[PROOF STATE]
proof (prove)
using this:
wf_domain

goal (1 subgoal):
 1. distinct (map ast_action_schema.name (actions D)) &&& Ball (set (actions D)) wf_action_schema
[PROOF STEP]
unfolding wf_domain_def
[PROOF STATE]
proof (prove)
using this:
wf_types \<and> distinct (map pred (predicates D)) \<and> Ball (set (predicates D)) wf_predicate_decl \<and> distinct (map fst (consts D)) \<and> (\<forall>(n, y)\<in>set (consts D). wf_type y) \<and> distinct (map ast_action_schema.name (actions D)) \<and> Ball (set (actions D)) wf_action_schema

goal (1 subgoal):
 1. distinct (map ast_action_schema.name (actions D)) &&& Ball (set (actions D)) wf_action_schema
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct (map ast_action_schema.name (actions D))
Ball (set (actions D)) wf_action_schema

goal (1 subgoal):
 1. wf_action_schema a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_action_schema a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
resolve_action_schema n = Some a

goal (1 subgoal):
 1. wf_action_schema a
[PROOF STEP]
unfolding resolve_action_schema_def
[PROOF STATE]
proof (prove)
using this:
index_by ast_action_schema.name (actions D) n = Some a

goal (1 subgoal):
 1. wf_action_schema a
[PROOF STEP]
by (auto simp add: index_by_eq_Some_eq[OF X1] X2)
[PROOF STATE]
proof (state)
this:
wf_action_schema a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma holds_for_wf_fmlas:
    assumes "wm_basic s"
    shows "holds s F \<longleftrightarrow> close_world s \<TTurnstile> F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. holds s F = s \<^sup>c\<TTurnstile>\<^sub>= F
[PROOF STEP]
unfolding holds_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valuation s \<Turnstile> F = s \<^sup>c\<TTurnstile>\<^sub>= F
[PROOF STEP]
using assms valuation_iff_close_world
[PROOF STATE]
proof (prove)
using this:
wm_basic s
wm_basic ?M \<Longrightarrow> valuation ?M \<Turnstile> ?\<phi> = ?M \<^sup>c\<TTurnstile>\<^sub>= ?\<phi>

goal (1 subgoal):
 1. valuation s \<Turnstile> F = s \<^sup>c\<TTurnstile>\<^sub>= F
[PROOF STEP]
by blast


[STATEMENT]
lemma (in wf_ast_problem) en_exE_return_iff:
    assumes "wm_basic s"
    shows "en_exE a s = Inr s'
      \<longleftrightarrow> plan_action_enabled a s \<and> s' = execute_plan_action a s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (en_exE a s = Inr s') = (plan_action_enabled a s \<and> s' = execute_plan_action a s)
[PROOF STEP]
apply (cases a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. a = PAction x1 x2 \<Longrightarrow> (en_exE a s = Inr s') = (plan_action_enabled a s \<and> s' = execute_plan_action a s)
[PROOF STEP]
using assms holds_for_wf_fmlas wf_domain
[PROOF STATE]
proof (prove)
using this:
wm_basic s
wm_basic ?s \<Longrightarrow> holds ?s ?F = ?s \<^sup>c\<TTurnstile>\<^sub>= ?F
wf_domain

goal (1 subgoal):
 1. \<And>x1 x2. a = PAction x1 x2 \<Longrightarrow> (en_exE a s = Inr s') = (plan_action_enabled a s \<and> s' = execute_plan_action a s)
[PROOF STEP]
unfolding plan_action_enabled_def execute_plan_action_def
      and execute_ground_action_def en_exE_def wf_domain_def
[PROOF STATE]
proof (prove)
using this:
wm_basic s
wm_basic ?s \<Longrightarrow> holds ?s ?F = ?s \<^sup>c\<TTurnstile>\<^sub>= ?F
wf_types \<and> distinct (map pred (predicates D)) \<and> Ball (set (predicates D)) wf_predicate_decl \<and> distinct (map fst (consts D)) \<and> (\<forall>(n, y)\<in>set (consts D). wf_type y) \<and> distinct (map ast_action_schema.name (actions D)) \<and> Ball (set (actions D)) wf_action_schema

goal (1 subgoal):
 1. \<And>x1 x2. a = PAction x1 x2 \<Longrightarrow> ((case a of PAction n args \<Rightarrow> \<lambda>s. resolve_action_schemaE n \<bind> (\<lambda>a. check (action_params_match a args) (ERRS ''Parameter mismatch'') \<bind> (\<lambda>_. let ai = instantiate_action_schema a args in check (wf_effect_inst (ground_action.effect ai)) (ERRS ''Effect not well-formed'') \<bind> (\<lambda>_. check (holds s (ground_action.precondition ai)) (ERRS ''Precondition not satisfied'') \<bind> (\<lambda>_. Inr (apply_effect (ground_action.effect ai) s)))))) s = Inr s') = ((wf_plan_action a \<and> s \<^sup>c\<TTurnstile>\<^sub>= ground_action.precondition (resolve_instantiate a)) \<and> s' = apply_effect (ground_action.effect (resolve_instantiate a)) s)
[PROOF STEP]
by (auto
        split: option.splits
        simp: resolve_action_schemaE_def return_iff)


[STATEMENT]
lemma (in wf_ast_problem) wf_en_exE2_eq:
    shows "en_exE2 STG mp_objT pa s = en_exE pa s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. en_exE2 STG mp_objT pa s = en_exE pa s
[PROOF STEP]
apply (cases pa; simp add: en_exE2_def en_exE_def Let_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. pa = PAction x1 x2 \<Longrightarrow> resolve_action_schemaE x1 \<bind> (\<lambda>a. check (list_all2 is_obj_of_type x2 (map snd (parameters a))) (ERRS ''Parameter mismatch'') \<bind> (\<lambda>_. check (holds s (ground_action.precondition (instantiate_action_schema a x2))) (ERRS ''Precondition not satisfied'') \<bind> (\<lambda>_. Inr (apply_effect (ground_action.effect (instantiate_action_schema a x2)) s)))) = resolve_action_schemaE x1 \<bind> (\<lambda>a. check (action_params_match a x2) (ERRS ''Parameter mismatch'') \<bind> (\<lambda>_. check (wf_effect_inst (ground_action.effect (instantiate_action_schema a x2))) (ERRS ''Effect not well-formed'') \<bind> (\<lambda>_. check (holds s (ground_action.precondition (instantiate_action_schema a x2))) (ERRS ''Precondition not satisfied'') \<bind> (\<lambda>_. Inr (apply_effect (ground_action.effect (instantiate_action_schema a x2)) s)))))
[PROOF STEP]
apply (auto
      simp: return_iff resolve_action_schemaE_def resolve_action_wf
      simp: wf_effect_inst_weak action_params_match_def
      split: error_monad_bind_split)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in wf_ast_problem) en_exE2_return_iff:
    assumes "wm_basic M"
    shows "en_exE2 STG mp_objT a M = Inr M'
      \<longleftrightarrow> plan_action_enabled a M \<and> M' = execute_plan_action a M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (en_exE2 STG mp_objT a M = Inr M') = (plan_action_enabled a M \<and> M' = execute_plan_action a M)
[PROOF STEP]
unfolding wf_en_exE2_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (en_exE a M = Inr M') = (plan_action_enabled a M \<and> M' = execute_plan_action a M)
[PROOF STEP]
apply (subst en_exE_return_iff)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. wm_basic M
 2. (plan_action_enabled a M \<and> M' = execute_plan_action a M) = (plan_action_enabled a M \<and> M' = execute_plan_action a M)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wm_basic M

goal (2 subgoals):
 1. wm_basic M
 2. (plan_action_enabled a M \<and> M' = execute_plan_action a M) = (plan_action_enabled a M \<and> M' = execute_plan_action a M)
[PROOF STEP]
by (auto)


[STATEMENT]
lemma (in wf_ast_problem) en_exE2_return_iff_compact_notation:
    "\<lbrakk>wm_basic s\<rbrakk> \<Longrightarrow>
      en_exE2 STG mp_objT a s = Inr s'
      \<longleftrightarrow> plan_action_enabled a s \<and> s' = execute_plan_action a s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wm_basic s \<Longrightarrow> (en_exE2 STG mp_objT a s = Inr s') = (plan_action_enabled a s \<and> s' = execute_plan_action a s)
[PROOF STEP]
using en_exE2_return_iff
[PROOF STATE]
proof (prove)
using this:
wm_basic ?M \<Longrightarrow> (en_exE2 STG mp_objT ?a ?M = Inr ?M') = (plan_action_enabled ?a ?M \<and> ?M' = execute_plan_action ?a ?M)

goal (1 subgoal):
 1. wm_basic s \<Longrightarrow> (en_exE2 STG mp_objT a s = Inr s') = (plan_action_enabled a s \<and> s' = execute_plan_action a s)
[PROOF STEP]
.


[STATEMENT]
lemma valid_plan_from1_refine: "valid_plan_from s \<pi>s = valid_plan_from1 s \<pi>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_plan_from s \<pi>s = valid_plan_from1 s \<pi>s
[PROOF STEP]
proof(induction \<pi>s arbitrary: s)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. valid_plan_from s [] = valid_plan_from1 s []
 2. \<And>a \<pi>s s. (\<And>s. valid_plan_from s \<pi>s = valid_plan_from1 s \<pi>s) \<Longrightarrow> valid_plan_from s (a # \<pi>s) = valid_plan_from1 s (a # \<pi>s)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>s. valid_plan_from s [] = valid_plan_from1 s []
 2. \<And>a \<pi>s s. (\<And>s. valid_plan_from s \<pi>s = valid_plan_from1 s \<pi>s) \<Longrightarrow> valid_plan_from s (a # \<pi>s) = valid_plan_from1 s (a # \<pi>s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_plan_from s [] = valid_plan_from1 s []
[PROOF STEP]
by (auto simp add: plan_action_path_def valid_plan_from_def)
[PROOF STATE]
proof (state)
this:
valid_plan_from s [] = valid_plan_from1 s []

goal (1 subgoal):
 1. \<And>a \<pi>s s. (\<And>s. valid_plan_from s \<pi>s = valid_plan_from1 s \<pi>s) \<Longrightarrow> valid_plan_from s (a # \<pi>s) = valid_plan_from1 s (a # \<pi>s)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a \<pi>s s. (\<And>s. valid_plan_from s \<pi>s = valid_plan_from1 s \<pi>s) \<Longrightarrow> valid_plan_from s (a # \<pi>s) = valid_plan_from1 s (a # \<pi>s)
[PROOF STEP]
case (Cons a \<pi>s)
[PROOF STATE]
proof (state)
this:
valid_plan_from ?s32 \<pi>s = valid_plan_from1 ?s32 \<pi>s

goal (1 subgoal):
 1. \<And>a \<pi>s s. (\<And>s. valid_plan_from s \<pi>s = valid_plan_from1 s \<pi>s) \<Longrightarrow> valid_plan_from s (a # \<pi>s) = valid_plan_from1 s (a # \<pi>s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
valid_plan_from ?s32 \<pi>s = valid_plan_from1 ?s32 \<pi>s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
valid_plan_from ?s32 \<pi>s = valid_plan_from1 ?s32 \<pi>s

goal (1 subgoal):
 1. valid_plan_from s (a # \<pi>s) = valid_plan_from1 s (a # \<pi>s)
[PROOF STEP]
by (auto
        simp: valid_plan_from_def plan_action_path_def plan_action_enabled_def
        simp: execute_ground_action_def execute_plan_action_def)
[PROOF STATE]
proof (state)
this:
valid_plan_from s (a # \<pi>s) = valid_plan_from1 s (a # \<pi>s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in wf_ast_problem) wf_actions_only_add_atoms:
    "\<lbrakk> wm_basic s; wf_plan_action a \<rbrakk>
      \<Longrightarrow> wm_basic (execute_plan_action a s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wm_basic s; wf_plan_action a\<rbrakk> \<Longrightarrow> wm_basic (execute_plan_action a s)
[PROOF STEP]
using wf_problem wf_domain
[PROOF STATE]
proof (prove)
using this:
wf_problem
wf_domain

goal (1 subgoal):
 1. \<lbrakk>wm_basic s; wf_plan_action a\<rbrakk> \<Longrightarrow> wm_basic (execute_plan_action a s)
[PROOF STEP]
unfolding wf_problem_def wf_domain_def
[PROOF STATE]
proof (prove)
using this:
(wf_types \<and> distinct (map pred (predicates D)) \<and> Ball (set (predicates D)) wf_predicate_decl \<and> distinct (map fst (consts D)) \<and> (\<forall>(n, y)\<in>set (consts D). wf_type y) \<and> distinct (map ast_action_schema.name (actions D)) \<and> Ball (set (actions D)) wf_action_schema) \<and> distinct (map fst (objects P) @ map fst (consts D)) \<and> (\<forall>(n, y)\<in>set (objects P). wf_type y) \<and> distinct (init P) \<and> wf_world_model (set (init P)) \<and> wf_fmla objT (goal P)
wf_types \<and> distinct (map pred (predicates D)) \<and> Ball (set (predicates D)) wf_predicate_decl \<and> distinct (map fst (consts D)) \<and> (\<forall>(n, y)\<in>set (consts D). wf_type y) \<and> distinct (map ast_action_schema.name (actions D)) \<and> Ball (set (actions D)) wf_action_schema

goal (1 subgoal):
 1. \<lbrakk>wm_basic s; wf_plan_action a\<rbrakk> \<Longrightarrow> wm_basic (execute_plan_action a s)
[PROOF STEP]
apply (cases a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>wm_basic s; wf_plan_action a; (wf_types \<and> distinct (map pred (predicates D)) \<and> Ball (set (predicates D)) wf_predicate_decl \<and> distinct (map fst (consts D)) \<and> (\<forall>(n, y)\<in>set (consts D). wf_type y) \<and> distinct (map ast_action_schema.name (actions D)) \<and> Ball (set (actions D)) wf_action_schema) \<and> distinct (map fst (objects P) @ map fst (consts D)) \<and> (\<forall>(n, y)\<in>set (objects P). wf_type y) \<and> distinct (init P) \<and> wf_world_model (set (init P)) \<and> wf_fmla objT (goal P); wf_types \<and> distinct (map pred (predicates D)) \<and> Ball (set (predicates D)) wf_predicate_decl \<and> distinct (map fst (consts D)) \<and> (\<forall>(n, y)\<in>set (consts D). wf_type y) \<and> distinct (map ast_action_schema.name (actions D)) \<and> Ball (set (actions D)) wf_action_schema; a = PAction x1 x2\<rbrakk> \<Longrightarrow> wm_basic (execute_plan_action a s)
[PROOF STEP]
apply (clarsimp
      split: option.splits
      simp: wf_fmla_atom_alt execute_plan_action_def wm_basic_def
      simp: execute_ground_action_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x2a aa. \<lbrakk>a = PAction x1 x2; \<forall>a\<in>s. is_predAtom a; distinct (map fst (objects P)); wf_types; fst ` set (objects P) \<inter> fst ` set (consts D) = {}; distinct (map pred (predicates D)); \<forall>x\<in>set (objects P). case x of (n, x) \<Rightarrow> wf_type x; Ball (set (predicates D)) wf_predicate_decl; distinct (init P); distinct (map fst (consts D)); wf_world_model (set (init P)); wf_fmla objT (goal P); \<forall>x\<in>set (consts D). case x of (n, x) \<Rightarrow> wf_type x; distinct (map ast_action_schema.name (actions D)); Ball (set (actions D)) wf_action_schema; resolve_action_schema x1 = Some x2a; aa \<in> apply_effect (ground_action.effect (instantiate_action_schema x2a x2)) s; action_params_match x2a x2; wf_effect_inst (ground_action.effect (instantiate_action_schema x2a x2))\<rbrakk> \<Longrightarrow> is_predAtom aa
[PROOF STEP]
subgoal for n args schema fmla
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a = PAction n args; \<forall>a\<in>s. is_predAtom a; distinct (map fst (objects P)); wf_types; fst ` set (objects P) \<inter> fst ` set (consts D) = {}; distinct (map pred (predicates D)); \<forall>x\<in>set (objects P). case x of (n, x) \<Rightarrow> wf_type x; Ball (set (predicates D)) wf_predicate_decl; distinct (init P); distinct (map fst (consts D)); wf_world_model (set (init P)); wf_fmla objT (goal P); \<forall>x\<in>set (consts D). case x of (n, x) \<Rightarrow> wf_type x; distinct (map ast_action_schema.name (actions D)); Ball (set (actions D)) wf_action_schema; resolve_action_schema n = Some schema; fmla \<in> apply_effect (ground_action.effect (instantiate_action_schema schema args)) s; action_params_match schema args; wf_effect_inst (ground_action.effect (instantiate_action_schema schema args))\<rbrakk> \<Longrightarrow> is_predAtom fmla
[PROOF STEP]
apply (cases "effect (instantiate_action_schema schema args)"; simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>a = PAction n args; \<forall>a\<in>s. is_predAtom a; distinct (map fst (objects P)); wf_types; fst ` set (objects P) \<inter> fst ` set (consts D) = {}; distinct (map pred (predicates D)); \<forall>x\<in>set (objects P). case x of (n, x) \<Rightarrow> wf_type x; Ball (set (predicates D)) wf_predicate_decl; distinct (init P); distinct (map fst (consts D)); wf_world_model (set (init P)); wf_fmla objT (goal P); \<forall>x\<in>set (consts D). case x of (n, x) \<Rightarrow> wf_type x; distinct (map ast_action_schema.name (actions D)); Ball (set (actions D)) wf_action_schema; resolve_action_schema n = Some schema; fmla \<in> s \<and> fmla \<notin> set x2 \<or> fmla \<in> set x1; action_params_match schema args; \<forall>x\<in>set x1 \<union> set x2. wf_fmla_atom objT x; ground_action.effect (instantiate_action_schema schema args) = Effect x1 x2\<rbrakk> \<Longrightarrow> is_predAtom fmla
[PROOF STEP]
by (metis ground_action.sel(2) ast_domain.wf_effect.simps
            ast_domain.wf_fmla_atom_alt resolve_action_wf
            wf_ground_action.elims(2) wf_instantiate_action_schema)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in wf_ast_problem) valid_plan_fromE_return_iff[return_iff]:
    assumes "wm_basic s"
    shows "valid_plan_fromE STG mp_objT k s \<pi>s = Inr () \<longleftrightarrow> valid_plan_from s \<pi>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (valid_plan_fromE STG mp_objT k s \<pi>s = Inr ()) = valid_plan_from s \<pi>s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wm_basic s

goal (1 subgoal):
 1. (valid_plan_fromE STG mp_objT k s \<pi>s = Inr ()) = valid_plan_from s \<pi>s
[PROOF STEP]
unfolding valid_plan_from1_refine
[PROOF STATE]
proof (prove)
using this:
wm_basic s

goal (1 subgoal):
 1. (valid_plan_fromE STG mp_objT k s \<pi>s = Inr ()) = valid_plan_from1 s \<pi>s
[PROOF STEP]
proof (induction stg\<equiv>STG mp\<equiv>mp_objT k s \<pi>s rule: valid_plan_fromE.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>si s. wm_basic s \<Longrightarrow> (valid_plan_fromE STG mp_objT si s [] = Inr ()) = valid_plan_from1 s []
 2. \<And>si s \<pi> \<pi>s. \<lbrakk>\<And>y. \<lbrakk>(try en_exE2 STG mp_objT \<pi> s catch (\<lambda>x. Inl (ERR ((((shows ''at step '' \<circ>\<circ>\<circ> shows_prec) 0 si \<circ>\<circ>\<circ> shows_prec) 0 '': '' \<circ>\<circ> x) ())))) = Inr y; wm_basic y\<rbrakk> \<Longrightarrow> (valid_plan_fromE STG mp_objT (si + 1) y \<pi>s = Inr ()) = valid_plan_from1 y \<pi>s; wm_basic s\<rbrakk> \<Longrightarrow> (valid_plan_fromE STG mp_objT si s (\<pi> # \<pi>s) = Inr ()) = valid_plan_from1 s (\<pi> # \<pi>s)
[PROOF STEP]
case (1 si s)
[PROOF STATE]
proof (state)
this:
wm_basic s

goal (2 subgoals):
 1. \<And>si s. wm_basic s \<Longrightarrow> (valid_plan_fromE STG mp_objT si s [] = Inr ()) = valid_plan_from1 s []
 2. \<And>si s \<pi> \<pi>s. \<lbrakk>\<And>y. \<lbrakk>(try en_exE2 STG mp_objT \<pi> s catch (\<lambda>x. Inl (ERR ((((shows ''at step '' \<circ>\<circ>\<circ> shows_prec) 0 si \<circ>\<circ>\<circ> shows_prec) 0 '': '' \<circ>\<circ> x) ())))) = Inr y; wm_basic y\<rbrakk> \<Longrightarrow> (valid_plan_fromE STG mp_objT (si + 1) y \<pi>s = Inr ()) = valid_plan_from1 y \<pi>s; wm_basic s\<rbrakk> \<Longrightarrow> (valid_plan_fromE STG mp_objT si s (\<pi> # \<pi>s) = Inr ()) = valid_plan_from1 s (\<pi> # \<pi>s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wm_basic s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
wm_basic s

goal (1 subgoal):
 1. (valid_plan_fromE STG mp_objT si s [] = Inr ()) = valid_plan_from1 s []
[PROOF STEP]
using wf_problem holds_for_wf_fmlas
[PROOF STATE]
proof (prove)
using this:
wm_basic s
wf_problem
wm_basic ?s \<Longrightarrow> holds ?s ?F = ?s \<^sup>c\<TTurnstile>\<^sub>= ?F

goal (1 subgoal):
 1. (valid_plan_fromE STG mp_objT si s [] = Inr ()) = valid_plan_from1 s []
[PROOF STEP]
by (auto
        simp: return_iff Let_def wf_en_exE2_eq wf_problem_def
        split: plan_action.split)
[PROOF STATE]
proof (state)
this:
(valid_plan_fromE STG mp_objT si s [] = Inr ()) = valid_plan_from1 s []

goal (1 subgoal):
 1. \<And>si s \<pi> \<pi>s. \<lbrakk>\<And>y. \<lbrakk>(try en_exE2 STG mp_objT \<pi> s catch (\<lambda>x. Inl (ERR ((((shows ''at step '' \<circ>\<circ>\<circ> shows_prec) 0 si \<circ>\<circ>\<circ> shows_prec) 0 '': '' \<circ>\<circ> x) ())))) = Inr y; wm_basic y\<rbrakk> \<Longrightarrow> (valid_plan_fromE STG mp_objT (si + 1) y \<pi>s = Inr ()) = valid_plan_from1 y \<pi>s; wm_basic s\<rbrakk> \<Longrightarrow> (valid_plan_fromE STG mp_objT si s (\<pi> # \<pi>s) = Inr ()) = valid_plan_from1 s (\<pi> # \<pi>s)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>si s \<pi> \<pi>s. \<lbrakk>\<And>y. \<lbrakk>(try en_exE2 STG mp_objT \<pi> s catch (\<lambda>x. Inl (ERR ((((shows ''at step '' \<circ>\<circ>\<circ> shows_prec) 0 si \<circ>\<circ>\<circ> shows_prec) 0 '': '' \<circ>\<circ> x) ())))) = Inr y; wm_basic y\<rbrakk> \<Longrightarrow> (valid_plan_fromE STG mp_objT (si + 1) y \<pi>s = Inr ()) = valid_plan_from1 y \<pi>s; wm_basic s\<rbrakk> \<Longrightarrow> (valid_plan_fromE STG mp_objT si s (\<pi> # \<pi>s) = Inr ()) = valid_plan_from1 s (\<pi> # \<pi>s)
[PROOF STEP]
case (2 si s \<pi> \<pi>s)
[PROOF STATE]
proof (state)
this:
\<lbrakk>(try en_exE2 STG mp_objT \<pi> s catch (\<lambda>x. Inl (ERR ((((shows ''at step '' \<circ>\<circ>\<circ> shows_prec) 0 si \<circ>\<circ>\<circ> shows_prec) 0 '': '' \<circ>\<circ> x) ())))) = Inr ?y32; wm_basic ?y32\<rbrakk> \<Longrightarrow> (valid_plan_fromE STG mp_objT (si + 1) ?y32 \<pi>s = Inr ()) = valid_plan_from1 ?y32 \<pi>s
wm_basic s

goal (1 subgoal):
 1. \<And>si s \<pi> \<pi>s. \<lbrakk>\<And>y. \<lbrakk>(try en_exE2 STG mp_objT \<pi> s catch (\<lambda>x. Inl (ERR ((((shows ''at step '' \<circ>\<circ>\<circ> shows_prec) 0 si \<circ>\<circ>\<circ> shows_prec) 0 '': '' \<circ>\<circ> x) ())))) = Inr y; wm_basic y\<rbrakk> \<Longrightarrow> (valid_plan_fromE STG mp_objT (si + 1) y \<pi>s = Inr ()) = valid_plan_from1 y \<pi>s; wm_basic s\<rbrakk> \<Longrightarrow> (valid_plan_fromE STG mp_objT si s (\<pi> # \<pi>s) = Inr ()) = valid_plan_from1 s (\<pi> # \<pi>s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(try en_exE2 STG mp_objT \<pi> s catch (\<lambda>x. Inl (ERR ((((shows ''at step '' \<circ>\<circ>\<circ> shows_prec) 0 si \<circ>\<circ>\<circ> shows_prec) 0 '': '' \<circ>\<circ> x) ())))) = Inr ?y32; wm_basic ?y32\<rbrakk> \<Longrightarrow> (valid_plan_fromE STG mp_objT (si + 1) ?y32 \<pi>s = Inr ()) = valid_plan_from1 ?y32 \<pi>s
wm_basic s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(try en_exE2 STG mp_objT \<pi> s catch (\<lambda>x. Inl (ERR ((((shows ''at step '' \<circ>\<circ>\<circ> shows_prec) 0 si \<circ>\<circ>\<circ> shows_prec) 0 '': '' \<circ>\<circ> x) ())))) = Inr ?y32; wm_basic ?y32\<rbrakk> \<Longrightarrow> (valid_plan_fromE STG mp_objT (si + 1) ?y32 \<pi>s = Inr ()) = valid_plan_from1 ?y32 \<pi>s
wm_basic s

goal (1 subgoal):
 1. (valid_plan_fromE STG mp_objT si s (\<pi> # \<pi>s) = Inr ()) = valid_plan_from1 s (\<pi> # \<pi>s)
[PROOF STEP]
apply (clarsimp
        simp: return_iff en_exE2_return_iff
        split: plan_action.split)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>plan_action_enabled \<pi> s; wm_basic (execute_plan_action \<pi> s)\<rbrakk> \<Longrightarrow> (valid_plan_fromE STG mp_objT (Suc si) (execute_plan_action \<pi> s) \<pi>s = Inr ()) = valid_plan_from1 (execute_plan_action \<pi> s) \<pi>s; wm_basic s\<rbrakk> \<Longrightarrow> (plan_action_enabled \<pi> s \<and> valid_plan_fromE STG mp_objT (Suc si) (execute_plan_action \<pi> s) \<pi>s = Inr ()) = (plan_action_enabled \<pi> s \<and> valid_plan_from1 (execute_plan_action \<pi> s) \<pi>s)
[PROOF STEP]
by (meson ast_problem.plan_action_enabled_def wf_actions_only_add_atoms)
[PROOF STATE]
proof (state)
this:
(valid_plan_fromE STG mp_objT si s (\<pi> # \<pi>s) = Inr ()) = valid_plan_from1 s (\<pi> # \<pi>s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma check_all_list_return_iff[return_iff]: "check_all_list P l msg msgf = Inr () \<longleftrightarrow> (\<forall>x\<in>set l. P x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (check_all_list P l msg msgf = Inr ()) = (\<forall>x\<in>set l. P x)
[PROOF STEP]
unfolding check_all_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((try forallM (\<lambda>x. check (P x) (\<lambda>_. ((shows msg \<circ>\<circ>\<circ> shows_prec) 0 '': '' \<circ>\<circ> msgf) x)) l catch (\<lambda>x. Inl (snd x))) = Inr ()) = (\<forall>x\<in>set l. P x)
[PROOF STEP]
by (induction l) (auto)


[STATEMENT]
lemma check_wf_types_return_iff[return_iff]: "check_wf_types D = Inr () \<longleftrightarrow> ast_domain.wf_types D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (check_wf_types D = Inr ()) = ast_domain.wf_types D
[PROOF STEP]
unfolding ast_domain.wf_types_def check_wf_types_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (check_all_list (\<lambda>(uu_, t). t = ''object'' \<or> t \<in> fst ` set (types D)) (types D) ''Undeclared supertype'' (shows \<circ> snd) = Inr ()) = (snd ` set (types D) \<subseteq> insert ''object'' (fst ` set (types D)))
[PROOF STEP]
by (force simp: return_iff)


[STATEMENT]
lemma check_wf_domain_return_iff[return_iff]:
  "check_wf_domain D stg conT = Inr () \<longleftrightarrow> ast_domain.wf_domain' D stg conT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (check_wf_domain D stg conT = Inr ()) = ast_domain.wf_domain' D stg conT
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (check_wf_domain D stg conT = Inr ()) = ast_domain.wf_domain' D stg conT
[PROOF STEP]
interpret ast_domain D
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (check_wf_domain D stg conT = Inr ()) = wf_domain' stg conT
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (check_wf_domain D stg conT = Inr ()) = wf_domain' stg conT
[PROOF STEP]
unfolding check_wf_domain_def wf_domain'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (check_wf_types D \<bind> (\<lambda>_. check (distinct (map pred (predicates D))) (ERRS ''Duplicate predicate declaration'') \<bind> (\<lambda>_. check_all_list wf_predicate_decl (predicates D) ''Malformed predicate declaration'' (shows \<circ> predicate.name \<circ> pred) \<bind> (\<lambda>_. check (distinct (map fst (consts D))) (ERRS ''Duplicate constant declaration'') \<bind> (\<lambda>_. check (\<forall>(n, y)\<in>set (consts D). wf_type y) (ERRS ''Malformed type'') \<bind> (\<lambda>_. check (distinct (map ast_action_schema.name (actions D))) (ERRS ''Duplicate action name'') \<bind> (\<lambda>_. check_all_list (wf_action_schema' stg conT) (actions D) ''Malformed action'' (shows \<circ> ast_action_schema.name))))))) = Inr ()) = (wf_types \<and> distinct (map pred (predicates D)) \<and> Ball (set (predicates D)) wf_predicate_decl \<and> distinct (map fst (consts D)) \<and> (\<forall>(n, y)\<in>set (consts D). wf_type y) \<and> distinct (map ast_action_schema.name (actions D)) \<and> (\<forall>a\<in>set (actions D). wf_action_schema' stg conT a))
[PROOF STEP]
by (auto simp: return_iff)
[PROOF STATE]
proof (state)
this:
(check_wf_domain D stg conT = Inr ()) = wf_domain' stg conT

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma check_wf_problem_return_iff[return_iff]:
  "check_wf_problem P stg conT mp = Inr () \<longleftrightarrow> ast_problem.wf_problem' P stg conT mp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (check_wf_problem P stg conT mp = Inr ()) = ast_problem.wf_problem' P stg conT mp
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (check_wf_problem P stg conT mp = Inr ()) = ast_problem.wf_problem' P stg conT mp
[PROOF STEP]
interpret ast_problem P
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (check_wf_problem P stg conT mp = Inr ()) = wf_problem' stg conT mp
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (check_wf_problem P stg conT mp = Inr ()) = wf_problem' stg conT mp
[PROOF STEP]
unfolding check_wf_problem_def wf_problem'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((let D = D in (try check_wf_domain D stg conT catch (\<lambda>x. Inl (prepend_err_msg ''Domain not well-formed'' x))) \<bind> (\<lambda>_. check (distinct (map fst (objects P) @ map fst (consts D))) (ERRS ''Duplicate object declaration'') \<bind> (\<lambda>_. check (\<forall>(n, T)\<in>set (objects P). ast_domain.wf_type D T) (ERRS ''Malformed type'') \<bind> (\<lambda>_. check (distinct (init P)) (ERRS ''Duplicate fact in initial state'') \<bind> (\<lambda>_. check (\<forall>f\<in>set (init P). wf_fmla_atom2' mp stg f) (ERRS ''Malformed formula in initial state'') \<bind> (\<lambda>_. check (ast_domain.wf_fmla' D (Mapping.lookup mp) stg (goal P)) (ERRS ''Malformed goal formula''))))))) = Inr ()) = (wf_domain' stg conT \<and> distinct (map fst (objects P) @ map fst (consts D)) \<and> (\<forall>(n, y)\<in>set (objects P). wf_type y) \<and> distinct (init P) \<and> (\<forall>f\<in>set (init P). wf_fmla_atom2' mp stg f) \<and> wf_fmla' (Mapping.lookup mp) stg (goal P))
[PROOF STEP]
by (auto simp: return_iff)
[PROOF STATE]
proof (state)
this:
(check_wf_problem P stg conT mp = Inr ()) = wf_problem' stg conT mp

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem check_plan_return_iff[return_iff]: "check_plan P \<pi>s = Inr ()
  \<longleftrightarrow> ast_problem.wf_problem P \<and> ast_problem.valid_plan P \<pi>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (check_plan P \<pi>s = Inr ()) = (ast_problem.wf_problem P \<and> ast_problem.valid_plan P \<pi>s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (check_plan P \<pi>s = Inr ()) = (ast_problem.wf_problem P \<and> ast_problem.valid_plan P \<pi>s)
[PROOF STEP]
interpret ast_problem P
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (check_plan P \<pi>s = Inr ()) = (wf_problem \<and> valid_plan \<pi>s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (check_plan P \<pi>s = Inr ()) = (wf_problem \<and> valid_plan \<pi>s)
[PROOF STEP]
unfolding check_plan_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((try (let stg = STG; conT = mp_constT; mp = mp_objT in check_wf_problem P stg conT mp \<bind> (\<lambda>_. valid_plan_fromE stg mp 1 I \<pi>s)) catch (\<lambda>x. Inl (String.implode (x () [])))) = Inr ()) = (wf_problem \<and> valid_plan \<pi>s)
[PROOF STEP]
by (auto
      simp: return_iff wf_world_model_def wf_fmla_atom_alt I_def wf_problem_def isOK_iff
      simp: wf_problem'_correct ast_problem.I_def ast_problem.valid_plan_def wm_basic_def
      )
[PROOF STATE]
proof (state)
this:
(check_plan P \<pi>s = Inr ()) = (wf_problem \<and> valid_plan \<pi>s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sorted_no_stutter_eq_distinct: "sorted l \<Longrightarrow> no_stutter l \<longleftrightarrow> distinct l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted l \<Longrightarrow> no_stutter l = distinct l
[PROOF STEP]
apply (induction l rule: no_stutter.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. sorted [] \<Longrightarrow> no_stutter [] = distinct []
 2. \<And>uu_. sorted [uu_] \<Longrightarrow> no_stutter [uu_] = distinct [uu_]
 3. \<And>a b l. \<lbrakk>sorted (b # l) \<Longrightarrow> no_stutter (b # l) = distinct (b # l); sorted (a # b # l)\<rbrakk> \<Longrightarrow> no_stutter (a # b # l) = distinct (a # b # l)
[PROOF STEP]
apply (auto simp: )
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [code_unfold]: "distinct = distinct_ds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct = distinct_ds
[PROOF STEP]
apply (intro ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. distinct x = distinct_ds x
[PROOF STEP]
unfolding distinct_ds_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. distinct x = no_stutter (ord_class.quicksort x)
[PROOF STEP]
apply (auto simp: sorted_no_stutter_eq_distinct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma det_interchange_rows:
shows "det (interchange_rows A i j) = of_int (if i = j then 1 else -1) * det A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (interchange_rows A i j) = of_int (if i = j then 1 else - 1) * det A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. det (interchange_rows A i j) = of_int (if i = j then 1 else - 1) * det A
[PROOF STEP]
have "(interchange_rows A i j) = (\<chi> a. A $ (Transposition.transpose i j) a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interchange_rows A i j = (\<chi>a. A $ Transposition.transpose i j a)
[PROOF STEP]
unfolding interchange_rows_def Transposition.transpose_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>ia ja. if ia = i then A $ j $ ja else if ia = j then A $ i $ ja else A $ ia $ ja) = (\<chi>a. A $ (if a = i then j else if a = j then i else a))
[PROOF STEP]
by vector
[PROOF STATE]
proof (state)
this:
interchange_rows A i j = (\<chi>a. A $ Transposition.transpose i j a)

goal (1 subgoal):
 1. det (interchange_rows A i j) = of_int (if i = j then 1 else - 1) * det A
[PROOF STEP]
hence "det(interchange_rows A i j) = det(\<chi> a. A$(Transposition.transpose i j) a)"
[PROOF STATE]
proof (prove)
using this:
interchange_rows A i j = (\<chi>a. A $ Transposition.transpose i j a)

goal (1 subgoal):
 1. det (interchange_rows A i j) = det (\<chi>a. A $ Transposition.transpose i j a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
det (interchange_rows A i j) = det (\<chi>a. A $ Transposition.transpose i j a)

goal (1 subgoal):
 1. det (interchange_rows A i j) = of_int (if i = j then 1 else - 1) * det A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (interchange_rows A i j) = det (\<chi>a. A $ Transposition.transpose i j a)

goal (1 subgoal):
 1. det (interchange_rows A i j) = of_int (if i = j then 1 else - 1) * det A
[PROOF STEP]
have "... = of_int (sign (Transposition.transpose i j)) * det A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (\<chi>a. A $ Transposition.transpose i j a) = of_int (sign (Transposition.transpose i j)) * det A
[PROOF STEP]
by (rule det_permute_rows[of "Transposition.transpose i j" A], simp add: permutes_swap_id)
[PROOF STATE]
proof (state)
this:
det (\<chi>a. A $ Transposition.transpose i j a) = of_int (sign (Transposition.transpose i j)) * det A

goal (1 subgoal):
 1. det (interchange_rows A i j) = of_int (if i = j then 1 else - 1) * det A
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
det (interchange_rows A i j) = of_int (sign (Transposition.transpose i j)) * det A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
det (interchange_rows A i j) = of_int (sign (Transposition.transpose i j)) * det A

goal (1 subgoal):
 1. det (interchange_rows A i j) = of_int (if i = j then 1 else - 1) * det A
[PROOF STEP]
unfolding sign_swap_id
[PROOF STATE]
proof (prove)
using this:
det (interchange_rows A i j) = of_int (if i = j then 1 else - 1) * det A

goal (1 subgoal):
 1. det (interchange_rows A i j) = of_int (if i = j then 1 else - 1) * det A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
det (interchange_rows A i j) = of_int (if i = j then 1 else - 1) * det A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma det_mult_row:
shows "det (mult_row A a k) = k * det A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (mult_row A a k) = k * det A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. det (mult_row A a k) = k * det A
[PROOF STEP]
have A_rw: "(\<chi> i. if i = a then A$a else A$i) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>i. if i = a then A $ a else A $ i) = A
[PROOF STEP]
by vector
[PROOF STATE]
proof (state)
this:
(\<chi>i. if i = a then A $ a else A $ i) = A

goal (1 subgoal):
 1. det (mult_row A a k) = k * det A
[PROOF STEP]
have "(mult_row A a k) = (\<chi> i. if i = a then k *s A $ a else A $ i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_row A a k = (\<chi>i. if i = a then k *s A $ a else A $ i)
[PROOF STEP]
unfolding mult_row_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>i j. if i = a then k * A $ a $ j else A $ i $ j) = (\<chi>i. if i = a then k *s A $ a else A $ i)
[PROOF STEP]
by vector
[PROOF STATE]
proof (state)
this:
mult_row A a k = (\<chi>i. if i = a then k *s A $ a else A $ i)

goal (1 subgoal):
 1. det (mult_row A a k) = k * det A
[PROOF STEP]
hence "det(mult_row A a k) = det(\<chi> i. if i = a then k *s A $ a else A $ i)"
[PROOF STATE]
proof (prove)
using this:
mult_row A a k = (\<chi>i. if i = a then k *s A $ a else A $ i)

goal (1 subgoal):
 1. det (mult_row A a k) = det (\<chi>i. if i = a then k *s A $ a else A $ i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
det (mult_row A a k) = det (\<chi>i. if i = a then k *s A $ a else A $ i)

goal (1 subgoal):
 1. det (mult_row A a k) = k * det A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (mult_row A a k) = det (\<chi>i. if i = a then k *s A $ a else A $ i)

goal (1 subgoal):
 1. det (mult_row A a k) = k * det A
[PROOF STEP]
have "... =  k * det(\<chi> i. if i = a then A$a else A$i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (\<chi>i. if i = a then k *s A $ a else A $ i) = k * det (\<chi>i. if i = a then A $ a else A $ i)
[PROOF STEP]
unfolding det_row_mul
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k * det (\<chi>i. if i = a then A $ a else A $ i) = k * det (\<chi>i. if i = a then A $ a else A $ i)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
det (\<chi>i. if i = a then k *s A $ a else A $ i) = k * det (\<chi>i. if i = a then A $ a else A $ i)

goal (1 subgoal):
 1. det (mult_row A a k) = k * det A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (\<chi>i. if i = a then k *s A $ a else A $ i) = k * det (\<chi>i. if i = a then A $ a else A $ i)

goal (1 subgoal):
 1. det (mult_row A a k) = k * det A
[PROOF STEP]
have "... = k * det A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k * det (\<chi>i. if i = a then A $ a else A $ i) = k * det A
[PROOF STEP]
unfolding A_rw
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k * det A = k * det A
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
k * det (\<chi>i. if i = a then A $ a else A $ i) = k * det A

goal (1 subgoal):
 1. det (mult_row A a k) = k * det A
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
det (mult_row A a k) = k * det A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
det (mult_row A a k) = k * det A

goal (1 subgoal):
 1. det (mult_row A a k) = k * det A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
det (mult_row A a k) = k * det A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma det_row_add':
assumes i_not_j: "i \<noteq> j"
shows "det (row_add A i j q) = det A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (row_add A i j q) = det A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. det (row_add A i j q) = det A
[PROOF STEP]
have "(row_add A i j q) = (\<chi> k. if k = i then row i A + q *s row j A else row k A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add A i j q = (\<chi>k. if k = i then row i A + q *s row j A else row k A)
[PROOF STEP]
unfolding row_add_def row_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>ia ja. if ia = i then A $ i $ ja + q * A $ j $ ja else A $ ia $ ja) = (\<chi>k. if k = i then vec_lambda (($) (A $ i)) + q *s vec_lambda (($) (A $ j)) else vec_lambda (($) (A $ k)))
[PROOF STEP]
by vector
[PROOF STATE]
proof (state)
this:
row_add A i j q = (\<chi>k. if k = i then row i A + q *s row j A else row k A)

goal (1 subgoal):
 1. det (row_add A i j q) = det A
[PROOF STEP]
hence "det(row_add A i j q) = det(\<chi> k. if k = i then row i A + q *s row j A else row k A)"
[PROOF STATE]
proof (prove)
using this:
row_add A i j q = (\<chi>k. if k = i then row i A + q *s row j A else row k A)

goal (1 subgoal):
 1. det (row_add A i j q) = det (\<chi>k. if k = i then row i A + q *s row j A else row k A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
det (row_add A i j q) = det (\<chi>k. if k = i then row i A + q *s row j A else row k A)

goal (1 subgoal):
 1. det (row_add A i j q) = det A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (row_add A i j q) = det (\<chi>k. if k = i then row i A + q *s row j A else row k A)

goal (1 subgoal):
 1. det (row_add A i j q) = det A
[PROOF STEP]
have "... = det A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (\<chi>k. if k = i then row i A + q *s row j A else row k A) = det A
[PROOF STEP]
unfolding det_row_operation[OF i_not_j]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det A = det A
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
det (\<chi>k. if k = i then row i A + q *s row j A else row k A) = det A

goal (1 subgoal):
 1. det (row_add A i j q) = det A
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
det (row_add A i j q) = det A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
det (row_add A i j q) = det A

goal (1 subgoal):
 1. det (row_add A i j q) = det A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
det (row_add A i j q) = det A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma det_interchange_columns:
shows "det (interchange_columns A i j) = of_int (if i = j then 1 else -1) * det A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (interchange_columns A i j) = of_int (if i = j then 1 else - 1) * det A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. det (interchange_columns A i j) = of_int (if i = j then 1 else - 1) * det A
[PROOF STEP]
have "(interchange_columns A i j) = (\<chi> a b. A $ a $ (Transposition.transpose i j) b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interchange_columns A i j = (\<chi>a b. A $ a $ Transposition.transpose i j b)
[PROOF STEP]
unfolding interchange_columns_def Transposition.transpose_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>ia ja. if ja = i then A $ ia $ j else if ja = j then A $ ia $ i else A $ ia $ ja) = (\<chi>a b. A $ a $ (if b = i then j else if b = j then i else b))
[PROOF STEP]
by vector
[PROOF STATE]
proof (state)
this:
interchange_columns A i j = (\<chi>a b. A $ a $ Transposition.transpose i j b)

goal (1 subgoal):
 1. det (interchange_columns A i j) = of_int (if i = j then 1 else - 1) * det A
[PROOF STEP]
hence "det(interchange_columns A i j) = det(\<chi> a b. A $ a $ (Transposition.transpose i j) b)"
[PROOF STATE]
proof (prove)
using this:
interchange_columns A i j = (\<chi>a b. A $ a $ Transposition.transpose i j b)

goal (1 subgoal):
 1. det (interchange_columns A i j) = det (\<chi>a b. A $ a $ Transposition.transpose i j b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
det (interchange_columns A i j) = det (\<chi>a b. A $ a $ Transposition.transpose i j b)

goal (1 subgoal):
 1. det (interchange_columns A i j) = of_int (if i = j then 1 else - 1) * det A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (interchange_columns A i j) = det (\<chi>a b. A $ a $ Transposition.transpose i j b)

goal (1 subgoal):
 1. det (interchange_columns A i j) = of_int (if i = j then 1 else - 1) * det A
[PROOF STEP]
have "... = of_int (sign (Transposition.transpose i j)) * det A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (\<chi>a b. A $ a $ Transposition.transpose i j b) = of_int (sign (Transposition.transpose i j)) * det A
[PROOF STEP]
by (rule det_permute_columns[of "Transposition.transpose i j" A], simp add: permutes_swap_id)
[PROOF STATE]
proof (state)
this:
det (\<chi>a b. A $ a $ Transposition.transpose i j b) = of_int (sign (Transposition.transpose i j)) * det A

goal (1 subgoal):
 1. det (interchange_columns A i j) = of_int (if i = j then 1 else - 1) * det A
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
det (interchange_columns A i j) = of_int (sign (Transposition.transpose i j)) * det A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
det (interchange_columns A i j) = of_int (sign (Transposition.transpose i j)) * det A

goal (1 subgoal):
 1. det (interchange_columns A i j) = of_int (if i = j then 1 else - 1) * det A
[PROOF STEP]
unfolding sign_swap_id
[PROOF STATE]
proof (prove)
using this:
det (interchange_columns A i j) = of_int (if i = j then 1 else - 1) * det A

goal (1 subgoal):
 1. det (interchange_columns A i j) = of_int (if i = j then 1 else - 1) * det A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
det (interchange_columns A i j) = of_int (if i = j then 1 else - 1) * det A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma det_mult_columns:
shows "det (mult_column A a k) = k * det A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (mult_column A a k) = k * det A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. det (mult_column A a k) = k * det A
[PROOF STEP]
have "mult_column A a k = transpose (mult_row (transpose A) a k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_column A a k = Finite_Cartesian_Product.transpose (mult_row (Finite_Cartesian_Product.transpose A) a k)
[PROOF STEP]
unfolding transpose_def mult_row_def mult_column_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>i j. if j = a then A $ i $ j * k else A $ i $ j) = (\<chi>i j. (\<chi>i j. if i = a then k * (\<chi>i j. A $ j $ i) $ a $ j else (\<chi>i j. A $ j $ i) $ i $ j) $ j $ i)
[PROOF STEP]
by vector
[PROOF STATE]
proof (state)
this:
mult_column A a k = Finite_Cartesian_Product.transpose (mult_row (Finite_Cartesian_Product.transpose A) a k)

goal (1 subgoal):
 1. det (mult_column A a k) = k * det A
[PROOF STEP]
hence "det (mult_column A a k) = det (transpose (mult_row (transpose A) a k))"
[PROOF STATE]
proof (prove)
using this:
mult_column A a k = Finite_Cartesian_Product.transpose (mult_row (Finite_Cartesian_Product.transpose A) a k)

goal (1 subgoal):
 1. det (mult_column A a k) = det (Finite_Cartesian_Product.transpose (mult_row (Finite_Cartesian_Product.transpose A) a k))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
det (mult_column A a k) = det (Finite_Cartesian_Product.transpose (mult_row (Finite_Cartesian_Product.transpose A) a k))

goal (1 subgoal):
 1. det (mult_column A a k) = k * det A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (mult_column A a k) = det (Finite_Cartesian_Product.transpose (mult_row (Finite_Cartesian_Product.transpose A) a k))

goal (1 subgoal):
 1. det (mult_column A a k) = k * det A
[PROOF STEP]
have "... = det (mult_row (transpose A) a k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (Finite_Cartesian_Product.transpose (mult_row (Finite_Cartesian_Product.transpose A) a k)) = det (mult_row (Finite_Cartesian_Product.transpose A) a k)
[PROOF STEP]
unfolding det_transpose
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (mult_row (Finite_Cartesian_Product.transpose A) a k) = det (mult_row (Finite_Cartesian_Product.transpose A) a k)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
det (Finite_Cartesian_Product.transpose (mult_row (Finite_Cartesian_Product.transpose A) a k)) = det (mult_row (Finite_Cartesian_Product.transpose A) a k)

goal (1 subgoal):
 1. det (mult_column A a k) = k * det A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (Finite_Cartesian_Product.transpose (mult_row (Finite_Cartesian_Product.transpose A) a k)) = det (mult_row (Finite_Cartesian_Product.transpose A) a k)

goal (1 subgoal):
 1. det (mult_column A a k) = k * det A
[PROOF STEP]
have "... = k * det (transpose A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (mult_row (Finite_Cartesian_Product.transpose A) a k) = k * det (Finite_Cartesian_Product.transpose A)
[PROOF STEP]
unfolding det_mult_row
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k * det (Finite_Cartesian_Product.transpose A) = k * det (Finite_Cartesian_Product.transpose A)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
det (mult_row (Finite_Cartesian_Product.transpose A) a k) = k * det (Finite_Cartesian_Product.transpose A)

goal (1 subgoal):
 1. det (mult_column A a k) = k * det A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (mult_row (Finite_Cartesian_Product.transpose A) a k) = k * det (Finite_Cartesian_Product.transpose A)

goal (1 subgoal):
 1. det (mult_column A a k) = k * det A
[PROOF STEP]
have "... = k * det A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k * det (Finite_Cartesian_Product.transpose A) = k * det A
[PROOF STEP]
unfolding det_transpose
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k * det A = k * det A
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
k * det (Finite_Cartesian_Product.transpose A) = k * det A

goal (1 subgoal):
 1. det (mult_column A a k) = k * det A
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
det (mult_column A a k) = k * det A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
det (mult_column A a k) = k * det A

goal (1 subgoal):
 1. det (mult_column A a k) = k * det A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
det (mult_column A a k) = k * det A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma det_column_add:
assumes i_not_j: "i \<noteq> j"
shows "det (column_add A i j q) = det A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (column_add A i j q) = det A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. det (column_add A i j q) = det A
[PROOF STEP]
have "(column_add A i j q) = (transpose (row_add (transpose A) i j q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. column_add A i j q = Finite_Cartesian_Product.transpose (row_add (Finite_Cartesian_Product.transpose A) i j q)
[PROOF STEP]
unfolding transpose_def column_add_def row_add_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>ia ja. if ja = i then A $ ia $ i + A $ ia $ j * q else A $ ia $ ja) = (\<chi>ia ja. (\<chi>ia ja. if ia = i then (\<chi>i j. A $ j $ i) $ i $ ja + q * (\<chi>i j. A $ j $ i) $ j $ ja else (\<chi>i j. A $ j $ i) $ ia $ ja) $ ja $ ia)
[PROOF STEP]
by vector
[PROOF STATE]
proof (state)
this:
column_add A i j q = Finite_Cartesian_Product.transpose (row_add (Finite_Cartesian_Product.transpose A) i j q)

goal (1 subgoal):
 1. det (column_add A i j q) = det A
[PROOF STEP]
hence "det (column_add A i j q) = det (transpose (row_add (transpose A) i j q))"
[PROOF STATE]
proof (prove)
using this:
column_add A i j q = Finite_Cartesian_Product.transpose (row_add (Finite_Cartesian_Product.transpose A) i j q)

goal (1 subgoal):
 1. det (column_add A i j q) = det (Finite_Cartesian_Product.transpose (row_add (Finite_Cartesian_Product.transpose A) i j q))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
det (column_add A i j q) = det (Finite_Cartesian_Product.transpose (row_add (Finite_Cartesian_Product.transpose A) i j q))

goal (1 subgoal):
 1. det (column_add A i j q) = det A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (column_add A i j q) = det (Finite_Cartesian_Product.transpose (row_add (Finite_Cartesian_Product.transpose A) i j q))

goal (1 subgoal):
 1. det (column_add A i j q) = det A
[PROOF STEP]
have "... = det (row_add (transpose A) i j q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (Finite_Cartesian_Product.transpose (row_add (Finite_Cartesian_Product.transpose A) i j q)) = det (row_add (Finite_Cartesian_Product.transpose A) i j q)
[PROOF STEP]
unfolding det_transpose
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (row_add (Finite_Cartesian_Product.transpose A) i j q) = det (row_add (Finite_Cartesian_Product.transpose A) i j q)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
det (Finite_Cartesian_Product.transpose (row_add (Finite_Cartesian_Product.transpose A) i j q)) = det (row_add (Finite_Cartesian_Product.transpose A) i j q)

goal (1 subgoal):
 1. det (column_add A i j q) = det A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (Finite_Cartesian_Product.transpose (row_add (Finite_Cartesian_Product.transpose A) i j q)) = det (row_add (Finite_Cartesian_Product.transpose A) i j q)

goal (1 subgoal):
 1. det (column_add A i j q) = det A
[PROOF STEP]
have "... = det A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (row_add (Finite_Cartesian_Product.transpose A) i j q) = det A
[PROOF STEP]
unfolding det_row_add'[OF i_not_j] det_transpose
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det A = det A
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
det (row_add (Finite_Cartesian_Product.transpose A) i j q) = det A

goal (1 subgoal):
 1. det (column_add A i j q) = det A
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
det (column_add A i j q) = det A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
det (column_add A i j q) = det A

goal (1 subgoal):
 1. det (column_add A i j q) = det A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
det (column_add A i j q) = det A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma det_row_add_iterate_upt_n:
fixes A::"'a::{comm_ring_1}^'n::{mod_type}^'n::{mod_type}"
assumes n: "n<nrows A"
shows "det (row_add_iterate A n i j) = det A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (row_add_iterate A n i j) = det A
[PROOF STEP]
using n
[PROOF STATE]
proof (prove)
using this:
n < nrows A

goal (1 subgoal):
 1. det (row_add_iterate A n i j) = det A
[PROOF STEP]
proof (induct n arbitrary: A)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>A. 0 < nrows A \<Longrightarrow> det (row_add_iterate A 0 i j) = det A
 2. \<And>n A. \<lbrakk>\<And>A. n < nrows A \<Longrightarrow> det (row_add_iterate A n i j) = det A; Suc n < nrows A\<rbrakk> \<Longrightarrow> det (row_add_iterate A (Suc n) i j) = det A
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 < nrows A

goal (2 subgoals):
 1. \<And>A. 0 < nrows A \<Longrightarrow> det (row_add_iterate A 0 i j) = det A
 2. \<And>n A. \<lbrakk>\<And>A. n < nrows A \<Longrightarrow> det (row_add_iterate A n i j) = det A; Suc n < nrows A\<rbrakk> \<Longrightarrow> det (row_add_iterate A (Suc n) i j) = det A
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (row_add_iterate A 0 i j) = det A
[PROOF STEP]
unfolding row_add_iterate.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (if i = (0::'n) then A else row_add A (0::'n) i (- A $ (0::'n) $ j)) = det A
[PROOF STEP]
using det_row_add'[of 0 i A]
[PROOF STATE]
proof (prove)
using this:
(0::'n) \<noteq> i \<Longrightarrow> det (row_add A (0::'n) i ?q) = det A

goal (1 subgoal):
 1. det (if i = (0::'n) then A else row_add A (0::'n) i (- A $ (0::'n) $ j)) = det A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
det (row_add_iterate A 0 i j) = det A

goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. n < nrows A \<Longrightarrow> det (row_add_iterate A n i j) = det A; Suc n < nrows A\<rbrakk> \<Longrightarrow> det (row_add_iterate A (Suc n) i j) = det A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. n < nrows A \<Longrightarrow> det (row_add_iterate A n i j) = det A; Suc n < nrows A\<rbrakk> \<Longrightarrow> det (row_add_iterate A (Suc n) i j) = det A
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
n < nrows ?A \<Longrightarrow> det (row_add_iterate ?A n i j) = det ?A
Suc n < nrows A

goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. n < nrows A \<Longrightarrow> det (row_add_iterate A n i j) = det A; Suc n < nrows A\<rbrakk> \<Longrightarrow> det (row_add_iterate A (Suc n) i j) = det A
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (row_add_iterate A (Suc n) i j) = det A
[PROOF STEP]
unfolding row_add_iterate.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (if Suc n = mod_type_class.to_nat i then row_add_iterate A n i j else row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j) = det A
[PROOF STEP]
proof (auto)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Suc n = mod_type_class.to_nat i \<Longrightarrow> det (row_add_iterate A n i j) = det A
 2. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> det (row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j) = det A
[PROOF STEP]
show "det (row_add_iterate A n i j) = det A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (row_add_iterate A n i j) = det A
[PROOF STEP]
using Suc.hyps Suc.prems
[PROOF STATE]
proof (prove)
using this:
n < nrows ?A \<Longrightarrow> det (row_add_iterate ?A n i j) = det ?A
Suc n < nrows A

goal (1 subgoal):
 1. det (row_add_iterate A n i j) = det A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
det (row_add_iterate A n i j) = det A

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> det (row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j) = det A
[PROOF STEP]
assume Suc_n_not_i: "Suc n \<noteq> to_nat i"
[PROOF STATE]
proof (state)
this:
Suc n \<noteq> mod_type_class.to_nat i

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> det (row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j) = det A
[PROOF STEP]
have "det (row_add_iterate (row_add A (from_nat (Suc n)) i (- A $ from_nat (Suc n) $ j)) n i j)
= det (row_add A (from_nat (Suc n)) i (- A $ from_nat (Suc n) $ j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j) = det (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j))
[PROOF STEP]
proof (rule Suc.hyps, unfold nrows_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n < CARD('n)
[PROOF STEP]
show " n < CARD('n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < CARD('n)
[PROOF STEP]
using Suc.prems
[PROOF STATE]
proof (prove)
using this:
Suc n < nrows A

goal (1 subgoal):
 1. n < CARD('n)
[PROOF STEP]
unfolding nrows_def
[PROOF STATE]
proof (prove)
using this:
Suc n < CARD('n)

goal (1 subgoal):
 1. n < CARD('n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n < CARD('n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
det (row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j) = det (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j))

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> det (row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j) = det A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j) = det (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j))

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> det (row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j) = det A
[PROOF STEP]
have "... = det A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) = det A
[PROOF STEP]
proof (rule det_row_add',rule ccontr, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mod_type_class.from_nat (Suc n) = i \<Longrightarrow> False
[PROOF STEP]
assume "from_nat (Suc n) = i"
[PROOF STATE]
proof (state)
this:
mod_type_class.from_nat (Suc n) = i

goal (1 subgoal):
 1. mod_type_class.from_nat (Suc n) = i \<Longrightarrow> False
[PROOF STEP]
hence "to_nat (from_nat (Suc n)::'n) = to_nat i"
[PROOF STATE]
proof (prove)
using this:
mod_type_class.from_nat (Suc n) = i

goal (1 subgoal):
 1. mod_type_class.to_nat (mod_type_class.from_nat (Suc n)) = mod_type_class.to_nat i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat (mod_type_class.from_nat (Suc n)) = mod_type_class.to_nat i

goal (1 subgoal):
 1. mod_type_class.from_nat (Suc n) = i \<Longrightarrow> False
[PROOF STEP]
hence "(Suc n) = to_nat i"
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat (mod_type_class.from_nat (Suc n)) = mod_type_class.to_nat i

goal (1 subgoal):
 1. Suc n = mod_type_class.to_nat i
[PROOF STEP]
unfolding to_nat_from_nat_id[OF Suc.prems[unfolded nrows_def]]
[PROOF STATE]
proof (prove)
using this:
Suc n = mod_type_class.to_nat i

goal (1 subgoal):
 1. Suc n = mod_type_class.to_nat i
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Suc n = mod_type_class.to_nat i

goal (1 subgoal):
 1. mod_type_class.from_nat (Suc n) = i \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
Suc n = mod_type_class.to_nat i

goal (1 subgoal):
 1. False
[PROOF STEP]
using Suc_n_not_i
[PROOF STATE]
proof (prove)
using this:
Suc n = mod_type_class.to_nat i
Suc n \<noteq> mod_type_class.to_nat i

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
det (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) = det A

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> det (row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j) = det A
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
det (row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j) = det A
[PROOF STEP]
show "det (row_add_iterate (row_add A (from_nat (Suc n)) i (- A $ from_nat (Suc n) $ j)) n i j) = det A"
[PROOF STATE]
proof (prove)
using this:
det (row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j) = det A

goal (1 subgoal):
 1. det (row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j) = det A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
det (row_add_iterate (row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j) = det A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
det (row_add_iterate A (Suc n) i j) = det A

goal:
No subgoals!
[PROOF STEP]
qed