theory Invariants_H

lemma loop_split:
  assumes loop: "m \<turnstile> c \<leadsto>\<^sup>+ c"
  and    split: "m \<turnstile> c \<leadsto>\<^sup>+ c'"
  shows  "m \<turnstile> c' \<leadsto>\<^sup>+ c" using split loop proof induct case base thus ?case by (auto dest: next_single_value elim: tranclE2) next case (step y z) hence "m \<turnstile> y \<leadsto>\<^sup>+ c" by simp hence "m \<turnstile> z \<leadsto>\<^sup>* c" using step.hyps by (auto dest: next_single_value elim: tranclE2 intro: trancl_into_rtrancl) thus ?case using step.prems by (cases rule: next_rtrancl_tranclE, simp_all) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> c' \<leadsto>\<^sup>+ c proof (prove)
using this:
m \<turnstile> c \<leadsto>\<^sup>+ c'
m \<turnstile> c \<leadsto>\<^sup>+ c

goal (1 subgoal):
 1. m \<turnstile> c' \<leadsto>\<^sup>+ c proof (state)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>m \<turnstile> c \<leadsto> y; m \<turnstile> c \<leadsto>\<^sup>+ c\<rbrakk> \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>+ c
 2. \<And>y z. \<lbrakk>m \<turnstile> c \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; m \<turnstile> c \<leadsto>\<^sup>+ c \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>+ c; m \<turnstile> c \<leadsto>\<^sup>+ c\<rbrakk> \<Longrightarrow> m \<turnstile> z \<leadsto>\<^sup>+ c proof (state)
this:
m \<turnstile> c \<leadsto> y_
m \<turnstile> c \<leadsto>\<^sup>+ c

goal (2 subgoals):
 1. \<And>y. \<lbrakk>m \<turnstile> c \<leadsto> y; m \<turnstile> c \<leadsto>\<^sup>+ c\<rbrakk> \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>+ c
 2. \<And>y z. \<lbrakk>m \<turnstile> c \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; m \<turnstile> c \<leadsto>\<^sup>+ c \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>+ c; m \<turnstile> c \<leadsto>\<^sup>+ c\<rbrakk> \<Longrightarrow> m \<turnstile> z \<leadsto>\<^sup>+ c proof (prove)
using this:
m \<turnstile> c \<leadsto> y_
m \<turnstile> c \<leadsto>\<^sup>+ c

goal (1 subgoal):
 1. m \<turnstile> y_ \<leadsto>\<^sup>+ c proof (state)
this:
m \<turnstile> y_ \<leadsto>\<^sup>+ c

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m \<turnstile> c \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; m \<turnstile> c \<leadsto>\<^sup>+ c \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>+ c; m \<turnstile> c \<leadsto>\<^sup>+ c\<rbrakk> \<Longrightarrow> m \<turnstile> z \<leadsto>\<^sup>+ c proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m \<turnstile> c \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; m \<turnstile> c \<leadsto>\<^sup>+ c \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>+ c; m \<turnstile> c \<leadsto>\<^sup>+ c\<rbrakk> \<Longrightarrow> m \<turnstile> z \<leadsto>\<^sup>+ c proof (state)
this:
m \<turnstile> c \<leadsto>\<^sup>+ y
m \<turnstile> y \<leadsto> z
m \<turnstile> c \<leadsto>\<^sup>+ c \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>+ c
m \<turnstile> c \<leadsto>\<^sup>+ c

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m \<turnstile> c \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; m \<turnstile> c \<leadsto>\<^sup>+ c \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>+ c; m \<turnstile> c \<leadsto>\<^sup>+ c\<rbrakk> \<Longrightarrow> m \<turnstile> z \<leadsto>\<^sup>+ c proof (prove)
using this:
m \<turnstile> c \<leadsto>\<^sup>+ y
m \<turnstile> y \<leadsto> z
m \<turnstile> c \<leadsto>\<^sup>+ c \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>+ c
m \<turnstile> c \<leadsto>\<^sup>+ c

goal (1 subgoal):
 1. m \<turnstile> y \<leadsto>\<^sup>+ c proof (state)
this:
m \<turnstile> y \<leadsto>\<^sup>+ c

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m \<turnstile> c \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; m \<turnstile> c \<leadsto>\<^sup>+ c \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>+ c; m \<turnstile> c \<leadsto>\<^sup>+ c\<rbrakk> \<Longrightarrow> m \<turnstile> z \<leadsto>\<^sup>+ c proof (prove)
using this:
m \<turnstile> y \<leadsto>\<^sup>+ c

goal (1 subgoal):
 1. m \<turnstile> z \<leadsto>\<^sup>* c proof (prove)
using this:
m \<turnstile> y \<leadsto>\<^sup>+ c
m \<turnstile> c \<leadsto>\<^sup>+ y
m \<turnstile> y \<leadsto> z
m \<turnstile> c \<leadsto>\<^sup>+ c \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>+ c

goal (1 subgoal):
 1. m \<turnstile> z \<leadsto>\<^sup>* c proof (state)
this:
m \<turnstile> z \<leadsto>\<^sup>* c

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m \<turnstile> c \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; m \<turnstile> c \<leadsto>\<^sup>+ c \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>+ c; m \<turnstile> c \<leadsto>\<^sup>+ c\<rbrakk> \<Longrightarrow> m \<turnstile> z \<leadsto>\<^sup>+ c proof (prove)
using this:
m \<turnstile> z \<leadsto>\<^sup>* c

goal (1 subgoal):
 1. m \<turnstile> z \<leadsto>\<^sup>+ c proof (prove)
using this:
m \<turnstile> z \<leadsto>\<^sup>* c
m \<turnstile> c \<leadsto>\<^sup>+ c

goal (1 subgoal):
 1. m \<turnstile> z \<leadsto>\<^sup>+ c proof (state)
this:
m \<turnstile> z \<leadsto>\<^sup>+ c

goal:
No subgoals!