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