kings-crown/FVELER_Isabelle huggingface dataset:
theory Syscall_C

lemma ucast_maxIRQ_is_less:
  "SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ < UCAST(10 \<rightarrow> 32) irq \<Longrightarrow> scast Kernel_C.maxIRQ < irq" apply (clarsimp simp: scast_def Kernel_C.maxIRQ_def) apply (subgoal_tac "LENGTH(10) \<le> LENGTH(32)") apply (drule less_ucast_ucast_less[where x= "0x9F" and y="irq"]) by (simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ < UCAST(10 \<rightarrow> 32) irq \<Longrightarrow> SCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ < irq proof (prove)
goal (1 subgoal):
 1. 0x9F < UCAST(10 \<rightarrow> 32) irq \<Longrightarrow> 0x9F < irq proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0x9F < UCAST(10 \<rightarrow> 32) irq; LENGTH(10) \<le> LENGTH(32)\<rbrakk> \<Longrightarrow> 0x9F < irq
 2. 0x9F < UCAST(10 \<rightarrow> 32) irq \<Longrightarrow> LENGTH(10) \<le> LENGTH(32) proof (prove)
goal (3 subgoals):
 1. 0x9F < UCAST(10 \<rightarrow> 32) irq \<Longrightarrow> 0x9F < UCAST(10 \<rightarrow> 32) irq
 2. \<lbrakk>0x9F < UCAST(10 \<rightarrow> 32) irq; UCAST(32 \<rightarrow> 10) 0x9F < irq\<rbrakk> \<Longrightarrow> 0x9F < irq
 3. 0x9F < UCAST(10 \<rightarrow> 32) irq \<Longrightarrow> LENGTH(10) \<le> LENGTH(32)
theory Syscall_C

lemma scast_maxIRQ_is_not_less: "(\<not> (Kernel_C.maxIRQ) <s (ucast \<circ> (ucast :: irq \<Rightarrow> 16 word)) b)  \<Longrightarrow> \<not> (scast Kernel_C.maxIRQ < b)" apply (subgoal_tac "sint (ucast Kernel_C.maxIRQ :: 32 sword) \<ge> sint (ucast (ucast b))";
         simp only: Kernel_C.maxIRQ_def word_sless_def word_sle_def) apply (uint_arith) apply (subst (asm) sint_ucast_uint[where b=b and 'c=32  and 'b=16 and uc=ucast and uc'=ucast and uuc="ucast \<circ> ucast", simplified];
          simp add: is_up_def target_size source_size) apply (cases "sint maxIRQ \<le> sint (UCAST(10 \<rightarrow> 32 signed) b)"; simp add: maxIRQ_def sint_uint) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> Kernel_C.maxIRQ <s (UCAST(16 \<rightarrow> 32 signed) \<circ> UCAST(10 \<rightarrow> 16)) b \<Longrightarrow> \<not> SCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ < b proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> (sint 0x9F \<le> sint ((UCAST(16 \<rightarrow> 32 signed) \<circ> UCAST(10 \<rightarrow> 16)) b) \<and> 0x9F \<noteq> (UCAST(16 \<rightarrow> 32 signed) \<circ> UCAST(10 \<rightarrow> 16)) b); sint (UCAST(?'b3 \<rightarrow> ?'a3) (UCAST(10 \<rightarrow> ?'b3) b)) \<le> sint (UCAST(32 signed \<rightarrow> 32 signed) 0x9F)\<rbrakk> \<Longrightarrow> \<not> SCAST(32 signed \<rightarrow> 10) 0x9F < b
 2. \<not> (sint 0x9F \<le> sint ((UCAST(16 \<rightarrow> 32 signed) \<circ> UCAST(10 \<rightarrow> 16)) b) \<and> 0x9F \<noteq> (UCAST(16 \<rightarrow> 32 signed) \<circ> UCAST(10 \<rightarrow> 16)) b) \<Longrightarrow> sint (UCAST(?'b3 \<rightarrow> ?'a3) (UCAST(10 \<rightarrow> ?'b3) b)) \<le> sint (UCAST(32 signed \<rightarrow> 32 signed) 0x9F) proof (prove)
goal (2 subgoals):
 1. \<And>i ia ib. \<lbrakk>sint (UCAST(?'b3 \<rightarrow> ?'a3) (UCAST(10 \<rightarrow> ?'b3) b)) \<le> signed_take_bit (LENGTH(32 signed) - Suc 0) 159; 0 \<le> i; i < 2 ^ LENGTH(32 signed); signed_take_bit (LENGTH(32 signed) - Suc 0) 159 \<le> sint (UCAST(16 \<rightarrow> 32 signed) (UCAST(10 \<rightarrow> 16) b)) \<longrightarrow> int (take_bit LENGTH(32 signed) 159) = i; 0 \<le> ia; ia < 2 ^ LENGTH(10); 0 \<le> ib; ib < 2 ^ LENGTH(10); ib < ia; uint (UCAST(16 \<rightarrow> 32 signed) (UCAST(10 \<rightarrow> 16) b)) = i; uint b = ia; uint (word_of_int (signed_take_bit (LENGTH(32 signed) - Suc 0) 159)) = ib\<rbrakk> \<Longrightarrow> False
 2. \<not> (sint 0x9F \<le> sint ((UCAST(16 \<rightarrow> 32 signed) \<circ> UCAST(10 \<rightarrow> 16)) b) \<and> 0x9F \<noteq> (UCAST(16 \<rightarrow> 32 signed) \<circ> UCAST(10 \<rightarrow> 16)) b) \<Longrightarrow> sint (UCAST(?'b3 \<rightarrow> ?'a3) (UCAST(10 \<rightarrow> ?'b3) b)) \<le> sint (UCAST(32 signed \<rightarrow> 32 signed) 0x9F) proof (prove)
goal (1 subgoal):
 1. \<not> (sint 0x9F \<le> sint ((UCAST(16 \<rightarrow> 32 signed) \<circ> UCAST(10 \<rightarrow> 16)) b) \<and> 0x9F \<noteq> (UCAST(16 \<rightarrow> 32 signed) \<circ> UCAST(10 \<rightarrow> 16)) b) \<Longrightarrow> sint (UCAST(16 \<rightarrow> 32 signed) (UCAST(10 \<rightarrow> 16) b)) \<le> sint (UCAST(32 signed \<rightarrow> 32 signed) 0x9F) proof (prove)
goal:
No subgoals!
theory Syscall_C

lemma ucast_maxIRQ_is_not_less:
  "\<not> (SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ < UCAST(10 \<rightarrow> 32) irq) \<Longrightarrow> \<not> (scast Kernel_C.maxIRQ < irq)" apply (clarsimp simp: scast_def Kernel_C.maxIRQ_def) apply (subgoal_tac "LENGTH(10) \<le> LENGTH(32)") prefer 2 apply simp apply (erule notE) using ucast_up_mono by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ < UCAST(10 \<rightarrow> 32) irq \<Longrightarrow> \<not> SCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ < irq proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> 0x9F < UCAST(10 \<rightarrow> 32) irq; 0x9F < irq\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> 0x9F < UCAST(10 \<rightarrow> 32) irq; 0x9F < irq; LENGTH(10) \<le> LENGTH(32)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<not> 0x9F < UCAST(10 \<rightarrow> 32) irq; 0x9F < irq\<rbrakk> \<Longrightarrow> LENGTH(10) \<le> LENGTH(32) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> 0x9F < UCAST(10 \<rightarrow> 32) irq; 0x9F < irq\<rbrakk> \<Longrightarrow> LENGTH(10) \<le> LENGTH(32)
 2. \<lbrakk>\<not> 0x9F < UCAST(10 \<rightarrow> 32) irq; 0x9F < irq; LENGTH(10) \<le> LENGTH(32)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> 0x9F < UCAST(10 \<rightarrow> 32) irq; 0x9F < irq; LENGTH(10) \<le> LENGTH(32)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0x9F < irq; LENGTH(10) \<le> LENGTH(32)\<rbrakk> \<Longrightarrow> 0x9F < UCAST(10 \<rightarrow> 32) irq proof (prove)
using this:
\<lbrakk>LENGTH(?'a) \<le> LENGTH(?'b); ?x < ?y\<rbrakk> \<Longrightarrow> UCAST(?'a \<rightarrow> ?'b) ?x < UCAST(?'a \<rightarrow> ?'b) ?y

goal (1 subgoal):
 1. \<lbrakk>0x9F < irq; LENGTH(10) \<le> LENGTH(32)\<rbrakk> \<Longrightarrow> 0x9F < UCAST(10 \<rightarrow> 32) irq
theory Syscall_C

lemma ccorres_handleReserveIRQ:
  "ccorres dc xfdc \<top> UNIV hs (handleReservedIRQ irq) (Call handleReservedIRQ_'proc)" apply cinit apply (rule ccorres_return_Skip) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>_. True) UNIV hs (handleReservedIRQ irq) (Call handleReservedIRQ_'proc) proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q5 ?Q'5 (SKIP # hs) (return ()) SKIP
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q5 s \<and> s' \<in> ?Q'5 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> True \<and> s' \<in> UNIV proof (prove)
goal:
No subgoals!
theory ADT_C

lemma Basic_sem_eq:
  "\<Gamma>\<turnstile>\<langle>Basic f,s\<rangle> \<Rightarrow> s' = ((\<exists>t. s = Normal t \<and> s' = Normal (f t)) \<or> (\<forall>t. s \<noteq> Normal t \<and> s' = s))" apply (rule iffI) apply (erule exec_elim_cases, simp_all)[1] apply clarsimp apply (erule disjE) apply clarsimp apply (rule exec.Basic) apply clarsimp apply (cases s, auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>Basic f,s\<rangle> \<Rightarrow> s' = ((\<exists>t. s = Normal t \<and> s' = Normal (f t)) \<or> (\<forall>t. s \<noteq> Normal t \<and> s' = s)) proof (prove)
goal (2 subgoals):
 1. \<Gamma>\<turnstile> \<langle>Basic f,s\<rangle> \<Rightarrow> s' \<Longrightarrow> (\<exists>t. s = Normal t \<and> s' = Normal (f t)) \<or> (\<forall>t. s \<noteq> Normal t \<and> s' = s)
 2. (\<exists>t. s = Normal t \<and> s' = Normal (f t)) \<or> (\<forall>t. s \<noteq> Normal t \<and> s' = s) \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Basic f,s\<rangle> \<Rightarrow> s' proof (prove)
goal (1 subgoal):
 1. (\<exists>t. s = Normal t \<and> s' = Normal (f t)) \<or> (\<forall>t. s \<noteq> Normal t \<and> s' = s) \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Basic f,s\<rangle> \<Rightarrow> s' proof (prove)
goal (1 subgoal):
 1. (\<exists>t. s = Normal t \<and> s' = Normal (f t)) \<or> (\<forall>t. s \<noteq> Normal t) \<and> s' = s \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Basic f,s\<rangle> \<Rightarrow> s' proof (prove)
goal (2 subgoals):
 1. \<exists>t. s = Normal t \<and> s' = Normal (f t) \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Basic f,s\<rangle> \<Rightarrow> s'
 2. (\<forall>t. s \<noteq> Normal t) \<and> s' = s \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Basic f,s\<rangle> \<Rightarrow> s' proof (prove)
goal (2 subgoals):
 1. \<And>t. \<lbrakk>s' = Normal (f t); s = Normal t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Basic f,Normal t\<rangle> \<Rightarrow> Normal (f t)
 2. (\<forall>t. s \<noteq> Normal t) \<and> s' = s \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Basic f,s\<rangle> \<Rightarrow> s' proof (prove)
goal (1 subgoal):
 1. (\<forall>t. s \<noteq> Normal t) \<and> s' = s \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Basic f,s\<rangle> \<Rightarrow> s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>t. s \<noteq> Normal t; s' = s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Basic f,s\<rangle> \<Rightarrow> s proof (prove)
goal:
No subgoals!
theory ADT_C

lemma ccontext_rel_to_C:
  "ccontext_relation uc (to_user_context_C uc)" apply (clarsimp simp: ccontext_relation_def to_user_context_C_def) apply (rule arg_cong [where f=uc]) apply (simp add: register_to_H_def inv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccontext_relation uc (to_user_context_C uc) proof (prove)
goal (1 subgoal):
 1. \<And>r. uc r = uc (register_to_H (register_from_H r)) proof (prove)
goal (1 subgoal):
 1. \<And>r. r = register_to_H (register_from_H r) proof (prove)
goal:
No subgoals!
theory ADT_C

lemma from_user_context_C:
  "ccontext_relation uc uc' \<Longrightarrow> from_user_context_C uc' = uc" by (auto simp: ccontext_relation_def from_user_context_C_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccontext_relation uc uc' \<Longrightarrow> from_user_context_C uc' = uc
theory ADT_C

lemma cirqstate_cancel:
  "cirqstate_to_H \<circ> irqstate_to_C = id" apply (rule ext) apply (case_tac x) apply (auto simp: cirqstate_to_H_def Kernel_C.IRQInactive_def
                    Kernel_C.IRQTimer_def Kernel_C.IRQSignal_def
                    Kernel_C.IRQReserved_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cirqstate_to_H \<circ> irqstate_to_C = id proof (prove)
goal (1 subgoal):
 1. \<And>x. (cirqstate_to_H \<circ> irqstate_to_C) x = id x proof (prove)
goal (4 subgoals):
 1. \<And>x. x = irqstate.IRQInactive \<Longrightarrow> (cirqstate_to_H \<circ> irqstate_to_C) x = id x
 2. \<And>x. x = irqstate.IRQSignal \<Longrightarrow> (cirqstate_to_H \<circ> irqstate_to_C) x = id x
 3. \<And>x. x = irqstate.IRQTimer \<Longrightarrow> (cirqstate_to_H \<circ> irqstate_to_C) x = id x
 4. \<And>x. x = irqstate.IRQReserved \<Longrightarrow> (cirqstate_to_H \<circ> irqstate_to_C) x = id x proof (prove)
goal:
No subgoals!
theory ADT_C

lemma cint_rel_to_H:
  "irqs_masked' s \<Longrightarrow>
   cinterrupt_relation (ksInterruptState s) n t \<Longrightarrow>
   cint_state_to_H n t = (ksInterruptState s)" apply (simp add: irqs_masked'_def) apply (cases "ksInterruptState s") apply (rename_tac "fun") apply (clarsimp simp: cinterrupt_relation_def cint_state_to_H_def
                        ARM.maxIRQ_def Kernel_C.maxIRQ_def) apply (rule ext) apply clarsimp apply (drule spec, erule impE, assumption) apply (drule_tac s="irqstate_to_C (fun i)" in sym,
         simp add: cirqstate_cancel[THEN fun_cong, simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>irqs_masked' s; cinterrupt_relation (ksInterruptState s) n t\<rbrakk> \<Longrightarrow> cint_state_to_H n t = ksInterruptState s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>irq>local.maxIRQ. intStateIRQTable (ksInterruptState s) irq = irqstate.IRQInactive; cinterrupt_relation (ksInterruptState s) n t\<rbrakk> \<Longrightarrow> cint_state_to_H n t = ksInterruptState s proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>\<forall>irq>local.maxIRQ. intStateIRQTable (ksInterruptState s) irq = irqstate.IRQInactive; cinterrupt_relation (ksInterruptState s) n t; ksInterruptState s = InterruptState x1 x2\<rbrakk> \<Longrightarrow> cint_state_to_H n t = ksInterruptState s proof (prove)
goal (1 subgoal):
 1. \<And>x1 fun. \<lbrakk>\<forall>irq>local.maxIRQ. intStateIRQTable (ksInterruptState s) irq = irqstate.IRQInactive; cinterrupt_relation (ksInterruptState s) n t; ksInterruptState s = InterruptState x1 fun\<rbrakk> \<Longrightarrow> cint_state_to_H n t = ksInterruptState s proof (prove)
goal (1 subgoal):
 1. \<And>x1 fun. \<lbrakk>\<forall>irq>0x9F. fun irq = irqstate.IRQInactive; ksInterruptState s = InterruptState x1 fun; n = PTR('b) x1; \<forall>irq\<le>0x9F. irqstate_to_C (fun irq) = t.[unat irq]\<rbrakk> \<Longrightarrow> (\<lambda>i. if i \<le> 0x9F then cirqstate_to_H (t.[unat i]) else irqstate.IRQInactive) = fun proof (prove)
goal (1 subgoal):
 1. \<And>x1 fun i. \<lbrakk>\<forall>irq>0x9F. fun irq = irqstate.IRQInactive; ksInterruptState s = InterruptState x1 fun; n = PTR('b) x1; \<forall>irq\<le>0x9F. irqstate_to_C (fun irq) = t.[unat irq]\<rbrakk> \<Longrightarrow> (if i \<le> 0x9F then cirqstate_to_H (t.[unat i]) else irqstate.IRQInactive) = fun i proof (prove)
goal (1 subgoal):
 1. \<And>x1 fun i. \<lbrakk>\<forall>irq>0x9F. fun irq = irqstate.IRQInactive; ksInterruptState s = InterruptState x1 fun; n = PTR('b) x1; \<forall>irq\<le>0x9F. irqstate_to_C (fun irq) = t.[unat irq]; i \<le> 0x9F\<rbrakk> \<Longrightarrow> cirqstate_to_H (t.[unat i]) = fun i proof (prove)
goal (1 subgoal):
 1. \<And>x1 fun i. \<lbrakk>\<forall>irq>0x9F. fun irq = irqstate.IRQInactive; ksInterruptState s = InterruptState x1 fun; n = PTR('b) x1; i \<le> 0x9F; irqstate_to_C (fun i) = t.[unat i]\<rbrakk> \<Longrightarrow> cirqstate_to_H (t.[unat i]) = fun i proof (prove)
goal:
No subgoals!
theory ADT_C

lemma projectKO_opt_UserData [simp]:
  "projectKO_opt KOUserData = Some UserData" by (simp add: projectKO_opts_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. projectKO_opt KOUserData = Some UserData
theory ADT_C

lemma ucast_ucast_mask_pageBits_shift:
  "ucast (ucast (p && mask pageBits >> 2) :: 10 word) = p && mask pageBits >> 2" apply (rule word_eqI) apply (auto simp: word_size nth_ucast nth_shiftr pageBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST(10 \<rightarrow> 'a) (UCAST('a \<rightarrow> 10) (p && mask pageBits >> 2)) = p && mask pageBits >> 2 proof (prove)
goal (1 subgoal):
 1. \<And>n. n < size (UCAST(10 \<rightarrow> 'a) (UCAST('a \<rightarrow> 10) (p && mask pageBits >> 2))) \<longrightarrow> UCAST(10 \<rightarrow> 'a) (UCAST('a \<rightarrow> 10) (p && mask pageBits >> 2)) !! n = (p && mask pageBits >> 2) !! n proof (prove)
goal:
No subgoals!
theory ADT_C

lemma unat_ucast_mask_pageBits_shift:
  "unat (ucast (p && mask pageBits >> 2) :: 10 word) = unat ((p::word32) && mask pageBits >> 2)" apply (simp only: unat_ucast) apply (rule Divides.mod_less, simp) apply (rule unat_less_power) apply (simp add: word_bits_def) apply (rule shiftr_less_t2n) apply (rule order_le_less_trans [OF word_and_le1]) apply (simp add: pageBits_def mask_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (UCAST(32 \<rightarrow> 10) (p && mask pageBits >> 2)) = unat (p && mask pageBits >> 2) proof (prove)
goal (1 subgoal):
 1. unat (p && mask pageBits >> 2) mod 2 ^ LENGTH(10) = unat (p && mask pageBits >> 2) proof (prove)
goal (1 subgoal):
 1. unat (p && mask pageBits >> 2) < 2 ^ LENGTH(10) proof (prove)
goal (2 subgoals):
 1. LENGTH(10) < LENGTH(32)
 2. p && mask pageBits >> 2 < 2 ^ LENGTH(10) proof (prove)
goal (1 subgoal):
 1. p && mask pageBits >> 2 < 2 ^ LENGTH(10) proof (prove)
goal (1 subgoal):
 1. p && mask pageBits < 2 ^ (2 + LENGTH(10)) proof (prove)
goal (1 subgoal):
 1. mask pageBits < 2 ^ (2 + LENGTH(10)) proof (prove)
goal:
No subgoals!
theory ADT_C

lemma array_relation_to_map:
  "array_relation r n a c \<Longrightarrow> \<forall>i\<le>n. r (a i) (the (array_to_map n c i))" by (simp add: array_relation_def array_to_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. array_relation r n a c \<Longrightarrow> \<forall>i\<le>n. r (a i) (the (array_to_map n c i))
theory ADT_C

lemma array_map_conv_def2:
  "array_map_conv f n c \<equiv> \<lambda>i. if i\<le>n then f (index c (unat i)) else None" by (rule eq_reflection, rule ext) (simp add: array_map_conv_def map_comp_def
                                               array_to_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. array_map_conv f n c \<equiv> \<lambda>i. if i \<le> n then f (c.[unat i]) else None
theory ADT_C

lemma array_relation_map_conv2:
  "array_relation r n a c \<Longrightarrow> \<forall>x. \<forall>y\<in>range a. r y x \<longrightarrow> (f x) = y \<Longrightarrow>
   \<forall>i>n. a i = None \<Longrightarrow> array_map_conv f n c = a" by (rule ext) (simp add: array_relation_def array_map_conv_def2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>array_relation r n a c; \<forall>x. \<forall>y\<in>range a. r y x \<longrightarrow> f x = y; \<forall>i>n. a i = None\<rbrakk> \<Longrightarrow> array_map_conv f n c = a
theory ADT_C

lemma eq_option_to_ptr_rev:
  "Some 0 \<notin> A \<Longrightarrow>
   \<forall>x. \<forall>y\<in>A. ((=) \<circ> option_to_ptr) y x \<longrightarrow>
              (if x=NULL then None else Some (ptr_val x)) = y" apply (clarsimp simp: option_to_ptr_def option_to_0_def split: option.splits) apply (auto intro: word_gt_0[THEN iffD2]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Some 0 \<notin> A \<Longrightarrow> \<forall>x. \<forall>y\<in>A. ((=) \<circ> option_to_ptr) y x \<longrightarrow> (if x = NULL then None else Some (ptr_val x)) = y proof (prove)
goal (1 subgoal):
 1. \<And>x. Some 0 \<notin> A \<Longrightarrow> (x = NULL \<longrightarrow> (\<forall>y\<in>A. \<forall>x2. y = Some x2 \<longrightarrow> 0 < x2)) \<and> (x \<noteq> NULL \<longrightarrow> (\<forall>y\<in>A. \<forall>x2. y = Some x2 \<longrightarrow> PTR('a) x2 = x \<longrightarrow> ptr_val x = x2)) proof (prove)
goal:
No subgoals!
theory ADT_C

lemma tcb_queue_rel'_unique:
  "hp NULL = None \<Longrightarrow>
   tcb_queue_relation' gn gp hp as pp cp \<Longrightarrow>
   tcb_queue_relation' gn gp hp as' pp cp \<Longrightarrow> as' = as" apply (clarsimp simp: tcb_queue_relation'_def split: if_split_asm) apply (clarsimp simp: neq_Nil_conv) apply (clarsimp simp: neq_Nil_conv) apply (erule(2) tcb_queue_rel_unique) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>hp NULL = None; tcb_queue_relation' gn gp hp as pp cp; tcb_queue_relation' gn gp hp as' pp cp\<rbrakk> \<Longrightarrow> as' = as proof (prove)
goal (3 subgoals):
 1. \<lbrakk>pp = NULL; hp NULL = None; as' = []; as \<noteq> []; cp = NULL; tcb_queue_relation gn gp hp as NULL NULL; tcb_ptr_to_ctcb_ptr (last as) = NULL\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>tcb_queue_relation gn gp hp as' (tcb_ptr_to_ctcb_ptr (last as')) (tcb_ptr_to_ctcb_ptr (last as')); hp (tcb_ptr_to_ctcb_ptr (last as')) = None; as' \<noteq> []; as = []; cp = tcb_ptr_to_ctcb_ptr (last as'); pp = tcb_ptr_to_ctcb_ptr (last as'); NULL = tcb_ptr_to_ctcb_ptr (last as')\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>tcb_queue_relation gn gp hp as' NULL pp; hp NULL = None; as' \<noteq> []; as \<noteq> []; cp = tcb_ptr_to_ctcb_ptr (last as'); tcb_queue_relation gn gp hp as NULL pp; tcb_ptr_to_ctcb_ptr (last as) = tcb_ptr_to_ctcb_ptr (last as')\<rbrakk> \<Longrightarrow> as' = as proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tcb_queue_relation gn gp hp as' (tcb_ptr_to_ctcb_ptr (last as')) (tcb_ptr_to_ctcb_ptr (last as')); hp (tcb_ptr_to_ctcb_ptr (last as')) = None; as' \<noteq> []; as = []; cp = tcb_ptr_to_ctcb_ptr (last as'); pp = tcb_ptr_to_ctcb_ptr (last as'); NULL = tcb_ptr_to_ctcb_ptr (last as')\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>tcb_queue_relation gn gp hp as' NULL pp; hp NULL = None; as' \<noteq> []; as \<noteq> []; cp = tcb_ptr_to_ctcb_ptr (last as'); tcb_queue_relation gn gp hp as NULL pp; tcb_ptr_to_ctcb_ptr (last as) = tcb_ptr_to_ctcb_ptr (last as')\<rbrakk> \<Longrightarrow> as' = as proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation gn gp hp as' NULL pp; hp NULL = None; as' \<noteq> []; as \<noteq> []; cp = tcb_ptr_to_ctcb_ptr (last as'); tcb_queue_relation gn gp hp as NULL pp; tcb_ptr_to_ctcb_ptr (last as) = tcb_ptr_to_ctcb_ptr (last as')\<rbrakk> \<Longrightarrow> as' = as proof (prove)
goal:
No subgoals!
theory ADT_C

lemma cpspace_cte_relation_unique:
  assumes "cpspace_cte_relation ah ch" "cpspace_cte_relation ah' ch"
  shows   "map_to_ctes ah' = map_to_ctes ah" apply (rule cmap_relation_unique[OF inj_Ptr _ assms]) by (clarsimp simp: ccte_relation_def Some_the[symmetric]) (drule sym, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map_to_ctes ah' = map_to_ctes ah proof (prove)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>ccte_relation x z; ccte_relation y z\<rbrakk> \<Longrightarrow> x = y
theory ADT_C

lemma inj_tcb_ptr_to_ctcb_ptr: "inj tcb_ptr_to_ctcb_ptr" by (simp add: inj_on_def tcb_ptr_to_ctcb_ptr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj tcb_ptr_to_ctcb_ptr
theory ADT_C

lemma ccontext_relation_imp_eq:
  "ccontext_relation f x \<Longrightarrow> ccontext_relation g x \<Longrightarrow> f=g" by (rule ext) (simp add: ccontext_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccontext_relation f x; ccontext_relation g x\<rbrakk> \<Longrightarrow> f = g
theory ADT_C

lemma carch_tcb_relation_imp_eq:
  "carch_tcb_relation f x \<Longrightarrow> carch_tcb_relation g x \<Longrightarrow> f = g" apply (cases f) apply (cases g) apply (simp add: carch_tcb_relation_def ccontext_relation_imp_eq atcbContextGet_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>carch_tcb_relation f x; carch_tcb_relation g x\<rbrakk> \<Longrightarrow> f = g proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>carch_tcb_relation f x; carch_tcb_relation g x; f = ArchThread xa\<rbrakk> \<Longrightarrow> f = g proof (prove)
goal (1 subgoal):
 1. \<And>xa xaa. \<lbrakk>carch_tcb_relation f x; carch_tcb_relation g x; f = ArchThread xa; g = ArchThread xaa\<rbrakk> \<Longrightarrow> f = g proof (prove)
goal:
No subgoals!