1(* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(GD_GPL) 9 *) 10 11header "Toplevel Refinement Statement for nondeterministic specification" 12 13theory Refine_nondet_C (* FIXME: broken *) 14imports 15 Refine_C 16 "AInvs.BCorres2_AI" 17begin 18 19definition (in state_rel) 20 cstate_to_AN :: "cstate \<Rightarrow> unit Structures_A.state" 21 where 22 "cstate_to_AN \<equiv> truncate_state \<circ> absKState \<circ> cstate_to_H \<circ> globals" 23definition (in state_rel) 24 "Fin_CN \<equiv> \<lambda>((tc,s),m,e). ((tc, cstate_to_AN s),m,e)" 25 26lemma truncate_trans[simp]: "truncate_state (trans_state f s) = s" 27 by (simp add: trans_state_def) 28 29context kernel 30begin 31 32definition 33 ADT_C' :: "(cstate global_state, unit observable, global_transition) data_type" 34where 35 "ADT_C' \<equiv> \<lparr> Init = Init_C', Fin = Fin_CN, 36 Step = global_automaton do_user_op_C (kernel_call_C False) \<rparr>" 37 38definition 39 ADT_FP_C' :: "(cstate global_state, unit observable, global_transition) data_type" 40where 41 "ADT_FP_C' \<equiv> \<lparr> Init = Init_C', Fin = Fin_CN, 42 Step = global_automaton do_user_op_C (kernel_call_C True) \<rparr>" 43 44lemma refinement2_both_nondet: 45 "\<lparr> Init = Init_C', Fin = Fin_CN, 46 Step = global_automaton do_user_op_C (kernel_call_C fp) \<rparr> 47 \<sqsubseteq> ADT_H'" 48 apply (cut_tac refinement2_both) 49 apply (clarsimp simp add: refines_def execution_def ADT_H'_def ADT_H_def) 50 apply (clarsimp simp add: Fin_CN_def cstate_to_AN_def Fin_C_def cstate_to_A_def Init_C_def) 51 apply (rename_tac js aa ba aaa baa ad bd ae be) 52 apply (drule_tac x=js in spec) 53 apply (drule_tac x=aa in spec) 54 apply (drule_tac x="trans_state (\<lambda>s. undefined) ba" in spec) 55 apply (drule_tac x=aaa in spec) 56 apply (drule_tac x=baa in spec) 57 apply simp 58 apply force 59 done 60 61theorem refinement2_nondet: 62 "ADT_C' \<sqsubseteq> ADT_H'" 63 unfolding ADT_C'_def 64 by (rule refinement2_both_nondet) 65 66theorem fp_refinement_nondet: 67 "ADT_FP_C' \<sqsubseteq> ADT_H'" 68 unfolding ADT_FP_C'_def 69 by (rule refinement2_both_nondet) 70 71theorem seL4_refinement_nondet: 72 "ADT_C' \<sqsubseteq> ADT_A'" 73 by (blast intro: refinement_nondet refinement2_nondet refinement_trans) 74 75theorem seL4_fastpath_refinement_nondet: 76 "ADT_FP_C' \<sqsubseteq> ADT_A'" 77 by (blast intro: refinement_nondet fp_refinement_nondet refinement_trans) 78 79end 80