theory ADT_IF_Refine

lemma Fin_Init_ADT_H:
  "s' \<in> (Init (ADT_H_if uop) s)
   \<Longrightarrow> s' \<in> full_invs_if' \<Longrightarrow> s \<in> Fin (ADT_H_if uop) ` Init (ADT_H_if uop) s" apply (clarsimp simp: ADT_H_if_def) apply (case_tac s) apply simp apply clarsimp apply (simp add: image_def) apply (rule_tac x="((a,b),baa)" in bexI) apply clarsimp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<in> Init (ADT_H_if uop) s; s' \<in> full_invs_if'\<rbrakk> \<Longrightarrow> s \<in> Fin (ADT_H_if uop) ` Init (ADT_H_if uop) s proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>((user_context_of s, b), sys_mode_of s) \<in> full_invs_if'; s' = ((user_context_of s, b), sys_mode_of s); absKState b = internal_state_if s\<rbrakk> \<Longrightarrow> s \<in> (\<lambda>x. case x of (x, xa) \<Rightarrow> (case x of (uc, s) \<Rightarrow> Pair (uc, absKState s)) xa) ` (({user_context_of s} \<times> {s'. absKState s' = internal_state_if s}) \<times> {sys_mode_of s} \<inter> full_invs_if') proof (prove)
goal (1 subgoal):
 1. \<And>b a ba. \<lbrakk>((user_context_of s, b), sys_mode_of s) \<in> full_invs_if'; s' = ((user_context_of s, b), sys_mode_of s); absKState b = internal_state_if s; s = (a, ba)\<rbrakk> \<Longrightarrow> s \<in> (\<lambda>x. case x of (x, xa) \<Rightarrow> (case x of (uc, s) \<Rightarrow> Pair (uc, absKState s)) xa) ` (({user_context_of s} \<times> {s'. absKState s' = internal_state_if s}) \<times> {sys_mode_of s} \<inter> full_invs_if') proof (prove)
goal (1 subgoal):
 1. \<And>b a ba. \<lbrakk>((user_context_of (a, ba), b), sys_mode_of (a, ba)) \<in> full_invs_if'; s' = ((user_context_of (a, ba), b), sys_mode_of (a, ba)); absKState b = snd a; s = (a, ba)\<rbrakk> \<Longrightarrow> (a, ba) \<in> (\<lambda>x. case x of (x, xa) \<Rightarrow> (case x of (uc, s) \<Rightarrow> Pair (uc, absKState s)) xa) ` (({user_context_of (a, ba)} \<times> {s'. absKState s' = snd a}) \<times> {sys_mode_of (a, ba)} \<inter> full_invs_if') proof (prove)
goal (1 subgoal):
 1. \<And>b a baa. \<lbrakk>((a, b), baa) \<in> full_invs_if'; s' = ((a, b), baa); s = ((a, absKState b), baa)\<rbrakk> \<Longrightarrow> ((a, absKState b), baa) \<in> (\<lambda>x. case x of (x, xa) \<Rightarrow> (case x of (uc, s) \<Rightarrow> Pair (uc, absKState s)) xa) ` (({a} \<times> {s'. absKState s' = absKState b}) \<times> {baa} \<inter> full_invs_if') proof (prove)
goal (1 subgoal):
 1. \<And>b a baa. \<lbrakk>((a, b), baa) \<in> full_invs_if'; s' = ((a, b), baa); s = ((a, absKState b), baa)\<rbrakk> \<Longrightarrow> \<exists>x\<in>({a} \<times> {s'. absKState s' = absKState b}) \<times> {baa} \<inter> full_invs_if'. ((a, absKState b), baa) = (case x of (x, xa) \<Rightarrow> (case x of (uc, s) \<Rightarrow> Pair (uc, absKState s)) xa) proof (prove)
goal (2 subgoals):
 1. \<And>b a baa. \<lbrakk>((a, b), baa) \<in> full_invs_if'; s' = ((a, b), baa); s = ((a, absKState b), baa)\<rbrakk> \<Longrightarrow> ((a, absKState b), baa) = (case ((a, b), baa) of (x, xa) \<Rightarrow> (case x of (uc, s) \<Rightarrow> Pair (uc, absKState s)) xa)
 2. \<And>b a baa. \<lbrakk>((a, b), baa) \<in> full_invs_if'; s' = ((a, b), baa); s = ((a, absKState b), baa)\<rbrakk> \<Longrightarrow> ((a, b), baa) \<in> ({a} \<times> {s'. absKState s' = absKState b}) \<times> {baa} \<inter> full_invs_if' proof (prove)
goal (1 subgoal):
 1. \<And>b a baa. \<lbrakk>((a, b), baa) \<in> full_invs_if'; s' = ((a, b), baa); s = ((a, absKState b), baa)\<rbrakk> \<Longrightarrow> ((a, b), baa) \<in> ({a} \<times> {s'. absKState s' = absKState b}) \<times> {baa} \<inter> full_invs_if' proof (prove)
goal:
No subgoals!