kings-crown/FVELER_Isabelle huggingface dataset:
theory ProveGraphRefine

lemma align_td_signed_word:
  "align_td (typ_info_t TYPE (('a :: len8) signed word))
    = align_td (typ_info_t TYPE (('a :: len8) word))" using arg_cong[where f=align_td, OF typ_uinfo_t_signed_word[where 'a='a]] by (simp add: typ_uinfo_t_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. align_td (typ_info_t TYPE('a signed word)) = align_td (typ_info_t TYPE('a word)) proof (prove)
using this:
align_td (typ_uinfo_t TYPE('a signed word)) = align_td (typ_uinfo_t TYPE('a word))

goal (1 subgoal):
 1. align_td (typ_info_t TYPE('a signed word)) = align_td (typ_info_t TYPE('a word))
theory ProveGraphRefine

lemma size_td_signed_word:
  "size_td (typ_info_t TYPE (('a :: len8) signed word))
    = size_td (typ_info_t TYPE (('a :: len8) word))" by (simp add: typ_info_word)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. size_td (typ_info_t TYPE('a signed word)) = size_td (typ_info_t TYPE('a word))
theory ProveGraphRefine

lemma pointer_inverse_safe_sign:
  "ptr_inverse_safe (ptr :: (('a :: len8) signed word ptr))
    = ptr_inverse_safe (ptr_coerce ptr :: 'a word ptr)" by (simp add: fun_eq_iff ptr_inverse_safe_def s_footprint_def
                c_guard_def ptr_aligned_def c_null_guard_def
                typ_uinfo_t_signed_word align_td_signed_word align_of_def
                size_of_def size_td_signed_word)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr_inverse_safe ptr = ptr_inverse_safe (PTR_COERCE('a signed word \<rightarrow> 'a word) ptr)
theory ProveGraphRefine

lemma ptr_equalities_to_ptr_val:
  "(Ptr addr = p) = (addr = ptr_val p)"
  "(p = Ptr addr) = (ptr_val p = addr)" by (simp | cases p)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (PTR('a) addr = p) = (addr = ptr_val p) &&& (p = PTR('a) addr) = (ptr_val p = addr)
theory ProveGraphRefine

lemma unat_ucast_if_up:
  "unat (ucast (x :: ('a :: len) word) :: ('b :: len) word)
    = (if len_of TYPE('a) \<le> len_of TYPE('b) then unat x else unat x mod 2 ^ len_of TYPE ('b))" apply (simp, safe intro!: unat_ucast unat_ucast_upcast) apply (simp add: is_up_def source_size_def target_size_def word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (UCAST('a \<rightarrow> 'b) x) = (if LENGTH('a) \<le> LENGTH('b) then unat x else unat x mod 2 ^ LENGTH('b)) proof (prove)
goal (1 subgoal):
 1. LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> is_up UCAST('a \<rightarrow> 'b) proof (prove)
goal:
No subgoals!
theory ProveGraphRefine

lemma Collect_const_mem:
  "(x \<in> (if P then UNIV else {})) = P" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x \<in> (if P then UNIV else {})) = P
theory ProveGraphRefine

lemma typ_uinfo_t_diff_from_typ_name:
  "typ_name (typ_info_t TYPE ('a :: c_type)) \<noteq> typ_name (typ_info_t TYPE('b :: c_type))
    \<Longrightarrow> typ_uinfo_t (aty :: 'a itself) \<noteq> typ_uinfo_t (bty :: 'b itself)" by (clarsimp simp: typ_uinfo_t_def td_diff_from_typ_name)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. typ_name (typ_info_t TYPE('a)) \<noteq> typ_name (typ_info_t TYPE('b)) \<Longrightarrow> typ_uinfo_t aty \<noteq> typ_uinfo_t bty
theory ProveGraphRefine

lemma machine_word_truncate_noop:
  "unat x < Suc n \<Longrightarrow> machine_word_truncate_nat n x = x" by (simp add: machine_word_truncate_nat_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat x < Suc n \<Longrightarrow> machine_word_truncate_nat n x = x
theory ProveGraphRefine

lemma fold_of_nat_eq_Ifs_proof:
  "\<lbrakk> unat (x :: machine_word) \<notin> set ns \<Longrightarrow> y = z;
      \<And>n. n \<in> set ns \<Longrightarrow> x = of_nat n \<Longrightarrow> f n = z \<rbrakk>
    \<Longrightarrow> foldr (\<lambda>n v. if x = of_nat n then f n else v) ns y = z" apply (induct ns) apply simp apply (atomize(full)) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat x \<notin> set ns \<Longrightarrow> y = z; \<And>n. \<lbrakk>n \<in> set ns; x = word_of_nat n\<rbrakk> \<Longrightarrow> f n = z\<rbrakk> \<Longrightarrow> foldr (\<lambda>n. If (x = word_of_nat n) (f n)) ns y = z proof (prove)
goal (2 subgoals):
 1. \<lbrakk>unat x \<notin> set [] \<Longrightarrow> y = z; \<And>n. \<lbrakk>n \<in> set []; x = word_of_nat n\<rbrakk> \<Longrightarrow> f n = z\<rbrakk> \<Longrightarrow> foldr (\<lambda>n. If (x = word_of_nat n) (f n)) [] y = z
 2. \<And>x1 ns. \<lbrakk>\<lbrakk>unat x \<notin> set ns \<Longrightarrow> y = z; \<And>n. \<lbrakk>n \<in> set ns; x = word_of_nat n\<rbrakk> \<Longrightarrow> f n = z\<rbrakk> \<Longrightarrow> foldr (\<lambda>n. If (x = word_of_nat n) (f n)) ns y = z; unat x \<notin> set (x1 # ns) \<Longrightarrow> y = z; \<And>n. \<lbrakk>n \<in> set (x1 # ns); x = word_of_nat n\<rbrakk> \<Longrightarrow> f n = z\<rbrakk> \<Longrightarrow> foldr (\<lambda>n. If (x = word_of_nat n) (f n)) (x1 # ns) y = z proof (prove)
goal (1 subgoal):
 1. \<And>x1 ns. \<lbrakk>\<lbrakk>unat x \<notin> set ns \<Longrightarrow> y = z; \<And>n. \<lbrakk>n \<in> set ns; x = word_of_nat n\<rbrakk> \<Longrightarrow> f n = z\<rbrakk> \<Longrightarrow> foldr (\<lambda>n. If (x = word_of_nat n) (f n)) ns y = z; unat x \<notin> set (x1 # ns) \<Longrightarrow> y = z; \<And>n. \<lbrakk>n \<in> set (x1 # ns); x = word_of_nat n\<rbrakk> \<Longrightarrow> f n = z\<rbrakk> \<Longrightarrow> foldr (\<lambda>n. If (x = word_of_nat n) (f n)) (x1 # ns) y = z proof (prove)
goal (1 subgoal):
 1. \<forall>x1 ns. ((unat x \<notin> set ns \<longrightarrow> y = z) \<longrightarrow> (\<forall>n. n \<in> set ns \<longrightarrow> x = word_of_nat n \<longrightarrow> f n = z) \<longrightarrow> foldr (\<lambda>n. If (x = word_of_nat n) (f n)) ns y = z) \<longrightarrow> (unat x \<notin> set (x1 # ns) \<longrightarrow> y = z) \<longrightarrow> (\<forall>n. n \<in> set (x1 # ns) \<longrightarrow> x = word_of_nat n \<longrightarrow> f n = z) \<longrightarrow> foldr (\<lambda>n. If (x = word_of_nat n) (f n)) (x1 # ns) y = z proof (prove)
goal:
No subgoals!
theory ProveGraphRefine

lemma fold_of_nat_eq_Ifs[simplified word_bits_conv]:
  "m < 2 ^ word_bits
    \<Longrightarrow> foldr (\<lambda>n v. if x = of_nat n then f n else v) [0 ..< m] (f m)
        = f (unat (machine_word_truncate_nat m x))" apply (rule fold_of_nat_eq_Ifs_proof) apply (simp_all add: machine_word_truncate_nat_def word_bits_def take_bit_nat_eq_self unat_of_nat) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m < 2 ^ word_bits \<Longrightarrow> foldr (\<lambda>n. If (x = word_of_nat n) (f n)) [0..<m] (f m) = f (unat (machine_word_truncate_nat m x)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m < 2 ^ word_bits; unat x \<notin> set [0..<m]\<rbrakk> \<Longrightarrow> f m = f (unat (machine_word_truncate_nat m x))
 2. \<And>n. \<lbrakk>m < 2 ^ word_bits; n \<in> set [0..<m]; x = word_of_nat n\<rbrakk> \<Longrightarrow> f n = f (unat (machine_word_truncate_nat m x)) proof (prove)
goal:
No subgoals!
theory ProveGraphRefine

lemma less_is_non_zero_p1':
  fixes a :: "'a :: len word"
  shows "a < k \<Longrightarrow> 1 + a \<noteq> 0" by (metis less_is_non_zero_p1 add.commute)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a < k \<Longrightarrow> 1 + a \<noteq> 0
theory ProveGraphRefine

lemma array_index_update_If:
  "i < CARD ('b :: finite)
    \<Longrightarrow> Arrays.index (Arrays.update arr j x) i
        = (if i = j then x else Arrays.index (arr :: ('a['b])) i)" by simp

\<comment> \<open>Of the assumptions, only pos is needed to prove the conclusion.
    The guard assumptions are there to ensure that when used as a simp rule,
    the RHS array pointer gets an appropriate type.\<close>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. i < CARD('b) \<Longrightarrow> Arrays.update arr j x.[i] = (if i = j then x else arr.[i])
theory ProveGraphRefine

lemma ptr_safe_ptr_add_array_ptr_index_int:
  assumes guard: "ptr_safe (Ptr p::('a['b]) ptr) htd" (* "nat i < CARD('b)" *)
  assumes pos: "0 \<le> i"
  shows "(Ptr p::'a::c_type ptr) +\<^sub>p i = array_ptr_index (Ptr p::('a['b::finite]) ptr) False (nat i)" using pos by (simp add: array_ptr_index_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. PTR('a) p +\<^sub>p i = array_ptr_index (PTR('a['b]) p) False (nat i) proof (prove)
using this:
0 \<le> i

goal (1 subgoal):
 1. PTR('a) p +\<^sub>p i = array_ptr_index (PTR('a['b]) p) False (nat i)
theory ProveGraphRefine

lemma ptr_safe_ptr_add_array_ptr_index_sint:
  assumes guard: "ptr_safe (Ptr p::('a['b]) ptr) htd" "i <s of_nat CARD('b)"
  assumes pos: "0 <=s i"
  shows "(Ptr p::'a::c_type ptr) +\<^sub>p sint i = array_ptr_index (Ptr p::('a['b::finite]) ptr) False (unat i)" using pos by (simp add: array_ptr_index_def int_unat sint_eq_uint word_sle_msb_le)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. PTR('a) p +\<^sub>p sint i = array_ptr_index (PTR('a['b]) p) False (unat i) proof (prove)
using this:
0 \<le>s i

goal (1 subgoal):
 1. PTR('a) p +\<^sub>p sint i = array_ptr_index (PTR('a['b]) p) False (unat i)
theory ProveGraphRefine

lemma ptr_safe_Array_element_0:
  "ptr_safe (PTR('a::mem_type['b::finite]) p) htd \<Longrightarrow> ptr_safe (PTR('a) p) htd" by (drule ptr_safe_Array_element[where coerce=False and n=0]; simp add: array_ptr_index_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr_safe (PTR('a['b]) p) htd \<Longrightarrow> ptr_safe (PTR('a) p) htd
theory SEL4GlobalsSwap

lemma globals_update_id:
  "globals_update id = id" by (rule ext, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. globals_update id = id
theory SEL4GlobalsSwap

lemma globals_update_eq_iff:
  "(globals_update f s = globals_update g s)
        = (f (globals s) = g (globals s))" apply (rule iffI) apply (drule_tac f=globals in arg_cong) apply simp apply (rule state.fold_congs, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (globals_update f s = globals_update g s) = (f (globals s) = g (globals s)) proof (prove)
goal (2 subgoals):
 1. globals_update f s = globals_update g s \<Longrightarrow> f (globals s) = g (globals s)
 2. f (globals s) = g (globals s) \<Longrightarrow> globals_update f s = globals_update g s proof (prove)
goal (2 subgoals):
 1. globals (globals_update f s) = globals (globals_update g s) \<Longrightarrow> f (globals s) = g (globals s)
 2. f (globals s) = g (globals s) \<Longrightarrow> globals_update f s = globals_update g s proof (prove)
goal (1 subgoal):
 1. f (globals s) = g (globals s) \<Longrightarrow> globals_update f s = globals_update g s proof (prove)
goal:
No subgoals!
theory SEL4GlobalsSwap

lemma global_acc_valid:
  "global_acc_valid t_hrs_' t_hrs_'_update" by (simp add: global_acc_valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global_acc_valid t_hrs_' t_hrs_'_update
theory SEL4GlobalsSwap

lemma t_hrs_ghost'state_update_globals_swap[simp]:
  "t_hrs_' (gswap (ghost'state_'_update f gs)) = t_hrs_' (gswap gs)" by (simp add: ghost'state_update_globals_swap)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. t_hrs_' (gswap (ghost'state_'_update f gs)) = t_hrs_' (gswap gs)
theory SEL4GlobalsSwap

lemma t_hrs_phantom_machine_state_'_update_globals_swap[simp]:
  "t_hrs_' (gswap (phantom_machine_state_'_update f gs)) = t_hrs_' (gswap gs)" by (simp add: phantom_machine_state_'_update_globals_swap)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. t_hrs_' (gswap (phantom_machine_state_'_update f gs)) = t_hrs_' (gswap gs)
theory SEL4GlobalsSwap

lemma globals_swap_twice[simp]:
  "gswap (gswap gs) = gs" by (metis globals_swap_twice_helper globals_list_distinct
            globals_list_valid global_acc_valid)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gswap (gswap gs) = gs
theory SEL4GlobalsSwap

lemma t_hrs_'_update_hmu_triv[simp]:
  "f (hrs_mem (t_hrs_' gs)) = hrs_mem (t_hrs_' gs)
    \<Longrightarrow> t_hrs_'_update (hrs_mem_update f) gs = gs" by (cases gs, auto simp add: hrs_mem_update_def hrs_mem_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f (hrs_mem (t_hrs_' gs)) = hrs_mem (t_hrs_' gs) \<Longrightarrow> t_hrs_'_update (hrs_mem_update f) gs = gs
theory SEL4GlobalsSwap

lemma t_hrs_'_heap_update_id[simp]:
  fixes p :: "'a::packed_type ptr"
  shows "t_hrs_'_update (hrs_mem_update (heap_update p ((h_val (hrs_mem (t_hrs_' s)) p)))) s = s" by (simp add: heap_update_id)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. t_hrs_'_update (hrs_mem_update (heap_update p (h_val (hrs_mem (t_hrs_' s)) p))) s = s
theory SimplExport

lemma field_lvalue_offset_eq:
  "field_lookup (typ_info_t TYPE('a :: c_type)) f 0 = Some v
        \<Longrightarrow> field_lvalue (ptr :: 'a ptr) f = ptr_val ptr + of_nat (snd v)" apply (cases v, simp, drule field_lookup_offset_eq) apply (simp add: field_lvalue_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. field_lookup (typ_info_t TYPE('a)) f 0 = Some v \<Longrightarrow> &(ptr\<rightarrow>f) = ptr_val ptr + word_of_nat (snd v) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>v = (a, b); field_offset TYPE('a) f = b\<rbrakk> \<Longrightarrow> &(ptr\<rightarrow>f) = ptr_val ptr + word_of_nat b proof (prove)
goal:
No subgoals!
theory ArchSEL4SimplExport

lemma ctzl_body_refines:
  "simple_simpl_refines \<Gamma> (Guard ImpossibleSpec \<lbrace>\<acute>x___unsigned_long \<noteq> 0\<rbrace>
    (\<acute>ret__long :== ucast (bv_ctz (\<acute>x___unsigned_long)))) ctzl_body" apply (simp add: ctzl_body_def) apply (rule simple_simpl_refines_guarded_Basic_guarded_spec_body) apply (clarsimp simp: bv_ctz_def meq_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. simple_simpl_refines \<Gamma> (Guard ImpossibleSpec \<lbrace>\<acute>x___unsigned_long \<noteq> 0\<rbrace> (\<acute>ret__long :== UCAST(32 \<rightarrow> 32 signed) (bv_ctz \<acute>x___unsigned_long))) kernel_all_global_addresses.ctzl_body proof (prove)
goal (1 subgoal):
 1. simple_simpl_refines \<Gamma> (Guard ImpossibleSpec \<lbrace>0 < \<acute>x___unsigned_long\<rbrace> (\<acute>ret__long :== UCAST(32 \<rightarrow> 32 signed) (bv_ctz \<acute>x___unsigned_long))) (guarded_spec_body ImpossibleSpec ({(s', t). (0 < x___unsigned_long_' s' \<longrightarrow> ret__long_' t = word_of_nat (word_ctz (x___unsigned_long_' s'))) \<and> 0 < x___unsigned_long_' s'} \<inter> {(s, t). t may_not_modify_globals s})) proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (s, s') \<in> {(s', t). (0 < x___unsigned_long_' s' \<longrightarrow> ret__long_' t = word_of_nat (word_ctz (x___unsigned_long_' s'))) \<and> 0 < x___unsigned_long_' s'} \<inter> {(s, t). t may_not_modify_globals s} \<longrightarrow> s \<in> \<lbrace>0 < \<acute>x___unsigned_long\<rbrace> \<and> (s, s\<lparr>ret__long_' := UCAST(32 \<rightarrow> 32 signed) (bv_ctz (x___unsigned_long_' s))\<rparr>) \<in> {(s', t). (0 < x___unsigned_long_' s' \<longrightarrow> ret__long_' t = word_of_nat (word_ctz (x___unsigned_long_' s'))) \<and> 0 < x___unsigned_long_' s'} \<inter> {(s, t). t may_not_modify_globals s} proof (prove)
goal:
No subgoals!
theory ArchSEL4SimplExport

lemma clzl_body_refines:
  "simple_simpl_refines \<Gamma> (Guard ImpossibleSpec \<lbrace>\<acute>x___unsigned_long \<noteq> 0\<rbrace>
    (\<acute>ret__long :== ucast (bv_clz (\<acute>x___unsigned_long)))) clzl_body" apply (simp add: clzl_body_def) apply (rule simple_simpl_refines_guarded_Basic_guarded_spec_body) apply (clarsimp simp: bv_clz_def meq_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. simple_simpl_refines \<Gamma> (Guard ImpossibleSpec \<lbrace>\<acute>x___unsigned_long \<noteq> 0\<rbrace> (\<acute>ret__long :== UCAST(32 \<rightarrow> 32 signed) (bv_clz \<acute>x___unsigned_long))) kernel_all_global_addresses.clzl_body proof (prove)
goal (1 subgoal):
 1. simple_simpl_refines \<Gamma> (Guard ImpossibleSpec \<lbrace>0 < \<acute>x___unsigned_long\<rbrace> (\<acute>ret__long :== UCAST(32 \<rightarrow> 32 signed) (bv_clz \<acute>x___unsigned_long))) (guarded_spec_body ImpossibleSpec ({(s', t). (0 < x___unsigned_long_' s' \<longrightarrow> ret__long_' t = word_of_nat (word_clz (x___unsigned_long_' s'))) \<and> 0 < x___unsigned_long_' s'} \<inter> {(s, t). t may_not_modify_globals s})) proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (s, s') \<in> {(s', t). (0 < x___unsigned_long_' s' \<longrightarrow> ret__long_' t = word_of_nat (word_clz (x___unsigned_long_' s'))) \<and> 0 < x___unsigned_long_' s'} \<inter> {(s, t). t may_not_modify_globals s} \<longrightarrow> s \<in> \<lbrace>0 < \<acute>x___unsigned_long\<rbrace> \<and> (s, s\<lparr>ret__long_' := UCAST(32 \<rightarrow> 32 signed) (bv_clz (x___unsigned_long_' s))\<rparr>) \<in> {(s', t). (0 < x___unsigned_long_' s' \<longrightarrow> ret__long_' t = word_of_nat (word_clz (x___unsigned_long_' s'))) \<and> 0 < x___unsigned_long_' s'} \<inter> {(s, t). t may_not_modify_globals s} proof (prove)
goal:
No subgoals!
theory GenericTag

lemma generic_tagP_I:
  "P \<Longrightarrow> generic_tag ns tag P" by (simp add: remove_generic_tag)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow> generic_tag ns tag P
theory GenericTag

lemma generic_tag_True:
  "generic_tag ns tag True" by (simp add: remove_generic_tag)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. generic_tag ns tag True
theory GenericTag

lemma generic_tag_cong:
  "x = x' \<Longrightarrow> generic_tag ns tag x = generic_tag ns tag x'" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x = x' \<Longrightarrow> generic_tag ns tag x = generic_tag ns tag x'
theory Wellformed_CAMKES

lemma wellformed_method_ann:
  "wellformed_method m =
    check_wellformed (wellformed_method, m)
      (m_name m \<notin> set (map p_name (m_parameters m)) \<and>
       distinct (map p_name (m_parameters m)))" by (simp only: wellformed_method_def remove_generic_tag simp_thms)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. wellformed_method m = check_wellformed (wellformed_method, m) (m_name m \<notin> set (map p_name (m_parameters m)) \<and> distinct (map p_name (m_parameters m)))
theory Wellformed_CAMKES

lemma wellformed_procedure_ann:
  "wellformed_procedure i =
     check_wellformed (wellformed_procedure, i)
       ((\<forall>x \<in> set i. wellformed_method x) \<and>
        distinct (map m_name i))" by (simp only: wellformed_procedure_def remove_generic_tag simp_thms)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. wellformed_procedure i = check_wellformed (wellformed_procedure, i) ((\<forall>x\<in>set i. wellformed_method x) \<and> distinct (map m_name i))
theory Wellformed_CAMKES

lemma wellformed_event_ann:
  "wellformed_event e =
     check_wellformed (wellformed_event, e) (e < 32)" by (simp only: wellformed_event_def remove_generic_tag simp_thms)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. wellformed_event e = check_wellformed (wellformed_event, e) (e < 32)
theory Wellformed_CAMKES

lemma wellformed_component_ann:
  "wellformed_component c = check_wellformed (wellformed_component, c) (
    \<comment> \<open>No symbol collisions\<close>
    (let names = map fst (requires c) @ map fst (provides c) @ map fst (dataports c) @
                 map fst (emits c) @ map fst (consumes c)
     in check_wellformed (wellformed_component, ''distinct'', names) (distinct names)) \<and>
    \<comment> \<open>No C symbol collisions.\<close>
    (\<forall>x \<in> set (requires c). wellformed_procedure (snd (snd x))) \<and>
    (\<forall>x \<in> set (provides c). wellformed_procedure (snd x)) \<and>
    \<comment> \<open>Events valid.\<close>
    (\<forall>x \<in> set (emits c). wellformed_event (snd x)) \<and>
    (\<forall>x \<in> set (consumes c). wellformed_event (snd (snd x))) \<and>
    \<comment> \<open>Dataports valid.\<close>
    (\<forall>x \<in> set (dataports c). wellformed_dataport (snd x))
   )" by (simp only: wellformed_component_def remove_generic_tag simp_thms Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. wellformed_component c = check_wellformed (wellformed_component, c) ((let names = map fst (requires c) @ map fst (provides c) @ map fst (dataports c) @ map fst (emits c) @ map fst (consumes c) in check_wellformed (wellformed_component, ''distinct'', names) (distinct names)) \<and> (\<forall>x\<in>set (requires c). wellformed_procedure (snd (snd x))) \<and> (\<forall>x\<in>set (provides c). wellformed_procedure (snd x)) \<and> (\<forall>x\<in>set (emits c). wellformed_event (snd x)) \<and> (\<forall>x\<in>set (consumes c). wellformed_event (snd (snd x))) \<and> (\<forall>x\<in>set (dataports c). wellformed_dataport (snd x)))
theory Wellformed_CAMKES

lemma refs_valid_procedures_ann:
  "refs_valid_procedures component_instance procedures conns =
     (\<forall>(name, (req, proc)) \<in> set procedures.
      req = InterfaceRequired \<longrightarrow>
      check_wellformed (refs_valid_procedures, name)
        (proc \<noteq> [] \<longrightarrow> (\<exists>1 z \<in> (concat (map (\<lambda>y. conn_from (snd y)) conns)). z = (component_instance, name))))" by (simp only: refs_valid_procedures_def remove_generic_tag simp_thms)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. refs_valid_procedures component_instance procedures conns = (\<forall>(name, req, proc)\<in>set procedures. req = InterfaceRequired \<longrightarrow> check_wellformed (refs_valid_procedures, name) (proc \<noteq> [] \<longrightarrow> (\<exists>1 z\<in>concat (map (\<lambda>y. conn_from (snd y)) conns). z = (component_instance, name))))
theory Wellformed_CAMKES

lemma refs_valid_connections_ann:
  "refs_valid_connections conns comps =
     (\<forall>x \<in> set conns. check_wellformed (refs_valid_connections, (fst x))
                          (refs_valid_connection (snd x) comps))" by (simp only: refs_valid_connections_def remove_generic_tag simp_thms)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. refs_valid_connections conns comps = (\<forall>x\<in>set conns. check_wellformed (refs_valid_connections, fst x) (refs_valid_connection (snd x) comps))