[STATEMENT]
lemma heap_wellformed_induct [consumes 1, case_names step]:
  assumes "heap_is_wellformed h"
    and step: "\<And>parent. (\<And>children child. h \<turnstile> get_child_nodes parent \<rightarrow>\<^sub>r children
               \<Longrightarrow> child \<in> set children \<Longrightarrow> P (cast child)) \<Longrightarrow> P parent"
  shows "P ptr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ptr
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P ptr
[PROOF STEP]
fix ptr
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P ptr
[PROOF STEP]
have "wf ((parent_child_rel h)\<inverse>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf ((parent_child_rel h)\<inverse>)
[PROOF STEP]
by (simp add: assms(1) finite_acyclic_wf_converse parent_child_rel_acyclic parent_child_rel_finite)
[PROOF STATE]
proof (state)
this:
wf ((parent_child_rel h)\<inverse>)

goal (1 subgoal):
 1. P ptr
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wf ((parent_child_rel h)\<inverse>)
[PROOF STEP]
show "?thesis"
[PROOF STATE]
proof (prove)
using this:
wf ((parent_child_rel h)\<inverse>)

goal (1 subgoal):
 1. P ptr
[PROOF STEP]
proof (induct rule: wf_induct_rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<And>y. (y, x) \<in> (parent_child_rel h)\<inverse> \<Longrightarrow> P y) \<Longrightarrow> P x
[PROOF STEP]
case (less parent)
[PROOF STATE]
proof (state)
this:
(?y, parent) \<in> (parent_child_rel h)\<inverse> \<Longrightarrow> P ?y

goal (1 subgoal):
 1. \<And>x. (\<And>y. (y, x) \<in> (parent_child_rel h)\<inverse> \<Longrightarrow> P y) \<Longrightarrow> P x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(?y, parent) \<in> (parent_child_rel h)\<inverse> \<Longrightarrow> P ?y
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(?y, parent) \<in> (parent_child_rel h)\<inverse> \<Longrightarrow> P ?y

goal (1 subgoal):
 1. P parent
[PROOF STEP]
using assms parent_child_rel_child
[PROOF STATE]
proof (prove)
using this:
(?y, parent) \<in> (parent_child_rel h)\<inverse> \<Longrightarrow> P ?y
heap_is_wellformed h
(\<And>children child. \<lbrakk>h \<turnstile> get_child_nodes ?parent \<rightarrow>\<^sub>r children; child \<in> set children\<rbrakk> \<Longrightarrow> P (cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r child)) \<Longrightarrow> P ?parent
?h \<turnstile> get_child_nodes ?ptr \<rightarrow>\<^sub>r ?children \<Longrightarrow> (?child \<in> set ?children) = ((?ptr, cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r ?child) \<in> parent_child_rel ?h)

goal (1 subgoal):
 1. P parent
[PROOF STEP]
by (meson converse_iff)
[PROOF STATE]
proof (state)
this:
P parent

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P ptr

goal:
No subgoals!
[PROOF STEP]
qed