Event-B Proof Obligations

I have a problem in Event-B to discharge proof obligations. In my work, I want to formalize the specification of memory protection requirements to check the consistency between them. In order to do that, I used Event-B Context to formalize the system's structure and used Event-B Machine to describe the requirements. Each requirement is described in both Invariant and Event. Event-B will check each pair requirement to find the inconsistency.
However, it cannot prove that two requirements are consistent: 1: "Read access from NonTrusted to the data_section of other OS_Apps is may_prevent"
2: "Read and Write access from an OS_App to its own data_section are shall_permit"

This is my work. Firstly, in the context file, I describe the structure of the system and the access control:
1. System's Structure:
We have 2 types of OS_Application: Trusted and NonTrusted.
2 types of OS_Objects: Tasks and ISRs.
2 types of ISRs: Category_1 and Category_2.
Each OS_Object belongs to one OS_App: ContainerOf ∈ OS_Obj → OS_App
Each OS_App has a code section: AppCode ∈ OS_App → CodeSection
Memory has 2 parts: DataSection and Stack
OS_App and OS_Obj may have DataSection:

AppData ∈ OS_App ⇸ DataSecs
ObjData ∈ OS_Obj ⇸ DataSecs

OS_Obj has their own Stack: ObjStack ∈ OS_Obj → Stacks

2. Access Control:
The Access is from Subjects to Objects:
Subjects include: OS_App and OS_Obj
Objects include: Code_Section, and Memory
In the below code, line 20 describes: "The stack for these objects, by definition, belongs only to the owner object and there is therefore no need to share stack data between objects, even if those objects belong to the same OS-Application."

line 21 describes: "Code sections are either private to an OS-Application or can be shared between all OS-Applications"
line 22, 23 describe: "OS-Applications can have private data sections and Tasks/ISRs can have private data sections."
line 24 describes: "OS-Application's private data sections are shared by all Tasks/ISRs belonging to that OS-Application. "

By the analysis, I define the context as follows:

1:  OS_Obj ⊆ Subjects   
2:  OS_App ⊆ Subjects ∖ OS_Obj
3:  Tasks ⊆ OS_Obj
4:  ISRs ⊆ OS_Obj∖Tasks
5:  Category_1_ISRs ⊆ ISRs
6:  Category_2_ISRs = ISRs ∖ Category_1_ISRs
7:  Trusted_OS ⊆ OS_App
8:  NonTrusted_OS = OS_App ∖ Trusted_OS
9:  CodeSection ⊆ Objects
10: Memory ⊆ Objects ∖ CodeSection
11: DataSecs ⊆ Memory
12: Stacks ⊆ Memory ∖ DataSecs
13: partition(actions_set, {initact}, {read}, {write}, {execute})
14: partition(status_set, {initStt}, {shall_prevent}, {shall_permit}, {may_prevent}, {may_permit})
15: ObjData ∈ OS_Obj ⇸ DataSecs
16: ObjStack ∈ OS_Obj → Stacks
17: AppCode ∈ OS_App → CodeSection
18: AppData ∈ OS_App ⇸ DataSecs
19: ContainerOf ∈ OS_Obj → OS_App 
20: ∀obj1,obj2 · (obj1 ∈ OS_Obj ∧ obj2 ∈ OS_Obj ∧ (obj1 ≠ obj2) ⇒ (ObjStack(obj1) ≠ ObjStack(obj2)))
21: ∀app1, app2 · (app1 ∈ OS_App ∧ app2 ∈ OS_App ∧ app1 ≠ app2) ⇒ AppCode(app1) = AppCode(app2)
22: ∀app1, app2 · (app1 ∈ dom(AppData) ∧ app2 ∈ dom(AppData) ∧ app1 ≠ app2) ⇒ AppData(app1) ≠ AppData(app2)
23: ∀ obj1, obj2 · (obj1 ∈ dom(ObjData) ∧ obj2 ∈ dom(ObjData) ∧ obj1 ≠ obj2) ⇒ ObjData(obj1) ≠ ObjData(obj2)
24: ∀ obj, app · (app ∈ dom(AppData) ∧ obj ∈ OS_Obj ∧ obj ∈ dom(ObjData) ∧ app ≠ ContainerOf(obj)) ⇒ ObjData(obj) ≠ AppData(app)
25: ∀ app, app1, app2 · (app ∈ dom(AppData) ∧ app2 ∈ dom(AppData) ∧ app1 ∈ NonTrusted_OS ∧ app = app1 ∧ app1 ≠ app2 ∧ AppData(app) = AppData(app2)) ⇒ ⊥

Secondly, In the Machine file, I describe:

prf_1:  ∀app1, app2 · ((action = read) ∧ app1 ∈ NonTrusted_OS ∧ app2 ∈ dom(AppData) 
∧ app1 ≠ app2 ∧ src = app1 ∧ dst = AppData(app2) 
∧ status ≠ initStt) ⇒ status = may_prevent 

prf_2: ∀app · ((action = read ∨ action = write) ∧ app ∈ dom(AppData) 
∧ src = app ∧ dst = AppData(app) ∧ status ≠ initStt) ⇒ status = shall_permit

And two events: Two events
After that, the event-B generates Proof Obligations and try to prove the consistency. However, that two requirements are inconsistent as follows: undischarged Proof Obligation
In the Goal box: It cannot prove that:
A = (¬(app∈dom(AppData) ∧ app1=app ∧ AppData(app2)=AppData(app))) is true.
However, in requirement no.2, we have: app1 ≠ app2
=> app ≠ app2 (because app1=app) => AppData(app2) ≠ AppData(app) Therefore, (app∈dom(AppData) ∧ app1=app ∧ AppData(app2)=AppData(app) = FALSE
then A = (¬(app∈dom(AppData) ∧ app1=app ∧ AppData(app2)=AppData(app))) = TRUE.

Could you give me some hints or comment, please?

Solution

I'm a bit guessing here since your given model is quite long and it's not obvious what is going wrong or what should be proven. You might improve your question by removing the not used stuff.

You want to prove

¬(app∈dom(AppData) ∧ app1=app ∧ AppData(app2)=AppData(app))

(I do not understand the part A=, the right side is a predicate, not an expression.)

Let's apply a case distinction on app∈dom(AppData) ∧ app1=app:

If it is false, then the whole predicate is trivially true.
If it is true, we have it as an additional hypothesis and it remains to prove (*):
```
¬(AppData(app2)=AppData(app1))
```

From your screenshot, we can see that app1 ≠ app2, so to instantiate axiom 22 you still need app2∈dom(AppData) to get the needed result AppData(app2)≠AppData(app1). It is not visible in your screenshot, but might be there somewhere.

(*): Maybe you can achieve this by introducing an hypothesis ¬(AppData(app2)=AppData(app1)) (by "ah"). Afterwards you can use this and the hypothesis from the case distinction above to prove your goal.

Just a comment: The axioms 22 and 23 can be completely replaced by defining the functions AppData and ObjData as injective, e.g. ObjData ∈ OS_Obj -+>> DataSecs. This would not only make the spec more readable, I think the provers can handle those better than quantified statements.