theory Invoke_C

lemma label_in_CNodeInv_ranges:
  "(label < scast Kernel_C.CNodeRevoke \<or> scast Kernel_C.CNodeSaveCaller < label)
      = (gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller])"
  "(scast Kernel_C.CNodeCopy \<le> label \<and> label \<le> scast Kernel_C.CNodeMutate)
      = (gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate])" apply (simp_all add: upto_enum_def fromEnum_def enum_gen_invocation_labels
                  del: upt.simps) apply (simp_all add: atLeastLessThanSuc) apply (simp_all add: toEnum_def enum_invocation_label enum_gen_invocation_labels) apply (simp_all flip: gen_invocation_type_eq) apply (simp_all add: invocation_eq_use_types_sym invocation_label_defs) apply (simp_all add: unat_arith_simps) apply arith+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (label < SCAST(32 signed \<rightarrow> 32) Kernel_C.CNodeRevoke \<or> SCAST(32 signed \<rightarrow> 32) Kernel_C.CNodeSaveCaller < label) = (gen_invocation_type label \<notin> set [gen_invocation_labels.CNodeRevoke .e. gen_invocation_labels.CNodeSaveCaller]) &&& (SCAST(32 signed \<rightarrow> 32) Kernel_C.CNodeCopy \<le> label \<and> label \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.CNodeMutate) = (gen_invocation_type label \<in> set [gen_invocation_labels.CNodeCopy .e. gen_invocation_labels.CNodeMutate]) proof (prove)
goal (2 subgoals):
 1. (label < SCAST(32 signed \<rightarrow> 32) Kernel_C.CNodeRevoke \<or> SCAST(32 signed \<rightarrow> 32) Kernel_C.CNodeSaveCaller < label) = (gen_invocation_type label \<notin> toEnum ` {Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))..<Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))))))))))})
 2. (SCAST(32 signed \<rightarrow> 32) Kernel_C.CNodeCopy \<le> label \<and> label \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.CNodeMutate) = (gen_invocation_type label \<in> toEnum ` {Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))))..<Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))))))))}) proof (prove)
goal (2 subgoals):
 1. (label < SCAST(32 signed \<rightarrow> 32) Kernel_C.CNodeRevoke \<or> SCAST(32 signed \<rightarrow> 32) Kernel_C.CNodeSaveCaller < label) = (gen_invocation_type label \<noteq> toEnum (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))))))))) \<and> gen_invocation_type label \<noteq> toEnum (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))))))))) \<and> gen_invocation_type label \<noteq> toEnum (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))))))) \<and> gen_invocation_type label \<noteq> toEnum (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))))))) \<and> gen_invocation_type label \<noteq> toEnum (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))))) \<and> gen_invocation_type label \<noteq> toEnum (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))))) \<and> gen_invocation_type label \<noteq> toEnum (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))) \<and> gen_invocation_type label \<noteq> toEnum (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))) \<and> gen_invocation_type label \<noteq> toEnum (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))
 2. (SCAST(32 signed \<rightarrow> 32) Kernel_C.CNodeCopy \<le> label \<and> label \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.CNodeMutate) = (gen_invocation_type label = toEnum (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))))))) \<or> gen_invocation_type label = toEnum (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))))))) \<or> gen_invocation_type label = toEnum (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))))) \<or> gen_invocation_type label = toEnum (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))))) proof (prove)
goal (2 subgoals):
 1. (label < SCAST(32 signed \<rightarrow> 32) Kernel_C.CNodeRevoke \<or> SCAST(32 signed \<rightarrow> 32) Kernel_C.CNodeSaveCaller < label) = (gen_invocation_type label \<noteq> gen_invocation_labels.CNodeSaveCaller \<and> gen_invocation_type label \<noteq> gen_invocation_labels.CNodeRotate \<and> gen_invocation_type label \<noteq> gen_invocation_labels.CNodeMutate \<and> gen_invocation_type label \<noteq> gen_invocation_labels.CNodeMove \<and> gen_invocation_type label \<noteq> gen_invocation_labels.CNodeMint \<and> gen_invocation_type label \<noteq> gen_invocation_labels.CNodeCopy \<and> gen_invocation_type label \<noteq> gen_invocation_labels.CNodeCancelBadgedSends \<and> gen_invocation_type label \<noteq> gen_invocation_labels.CNodeDelete \<and> gen_invocation_type label \<noteq> gen_invocation_labels.CNodeRevoke)
 2. (SCAST(32 signed \<rightarrow> 32) Kernel_C.CNodeCopy \<le> label \<and> label \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.CNodeMutate) = (gen_invocation_type label = gen_invocation_labels.CNodeMutate \<or> gen_invocation_type label = gen_invocation_labels.CNodeMove \<or> gen_invocation_type label = gen_invocation_labels.CNodeMint \<or> gen_invocation_type label = gen_invocation_labels.CNodeCopy) proof (prove)
goal (2 subgoals):
 1. (label < SCAST(32 signed \<rightarrow> 32) Kernel_C.CNodeRevoke \<or> SCAST(32 signed \<rightarrow> 32) Kernel_C.CNodeSaveCaller < label) = (invocation_type label \<noteq> GenInvocationLabel gen_invocation_labels.CNodeSaveCaller \<and> invocation_type label \<noteq> GenInvocationLabel gen_invocation_labels.CNodeRotate \<and> invocation_type label \<noteq> GenInvocationLabel gen_invocation_labels.CNodeMutate \<and> invocation_type label \<noteq> GenInvocationLabel gen_invocation_labels.CNodeMove \<and> invocation_type label \<noteq> GenInvocationLabel gen_invocation_labels.CNodeMint \<and> invocation_type label \<noteq> GenInvocationLabel gen_invocation_labels.CNodeCopy \<and> invocation_type label \<noteq> GenInvocationLabel gen_invocation_labels.CNodeCancelBadgedSends \<and> invocation_type label \<noteq> GenInvocationLabel gen_invocation_labels.CNodeDelete \<and> invocation_type label \<noteq> GenInvocationLabel gen_invocation_labels.CNodeRevoke)
 2. (SCAST(32 signed \<rightarrow> 32) Kernel_C.CNodeCopy \<le> label \<and> label \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.CNodeMutate) = (invocation_type label = GenInvocationLabel gen_invocation_labels.CNodeMutate \<or> invocation_type label = GenInvocationLabel gen_invocation_labels.CNodeMove \<or> invocation_type label = GenInvocationLabel gen_invocation_labels.CNodeMint \<or> invocation_type label = GenInvocationLabel gen_invocation_labels.CNodeCopy) proof (prove)
goal (2 subgoals):
 1. (label < 0x10 \<or> 0x18 < label) = (label \<noteq> 0x18 \<and> label \<noteq> 0x17 \<and> label \<noteq> 0x16 \<and> label \<noteq> 0x15 \<and> label \<noteq> 0x14 \<and> label \<noteq> 0x13 \<and> label \<noteq> 0x12 \<and> label \<noteq> 0x11 \<and> label \<noteq> 0x10)
 2. (0x13 \<le> label \<and> label \<le> 0x16) = (label = 0x16 \<or> label = 0x15 \<or> label = 0x14 \<or> label = 0x13) proof (prove)
goal (2 subgoals):
 1. (unat label < 16 \<or> 24 < unat label) = (unat label \<noteq> 24 \<and> unat label \<noteq> 23 \<and> unat label \<noteq> 22 \<and> unat label \<noteq> 21 \<and> unat label \<noteq> 20 \<and> unat label \<noteq> 19 \<and> unat label \<noteq> 18 \<and> unat label \<noteq> 17 \<and> unat label \<noteq> 16)
 2. (19 \<le> unat label \<and> unat label \<le> 22) = (unat label = 22 \<or> unat label = 21 \<or> unat label = 20 \<or> unat label = 19) proof (prove)
goal:
No subgoals!