theory Rights_AI

lemma validate_vm_rights_def':
  "validate_vm_rights rs =
   (THE rs'. rs' \<subseteq> rs \<and> rs' : valid_vm_rights \<and>
     (\<forall>rs''. rs'' \<subseteq> rs \<longrightarrow> rs'' : valid_vm_rights \<longrightarrow> rs'' \<subseteq> rs'))" apply (rule the_equality[symmetric]) apply  (auto simp add: validate_vm_rights_def valid_vm_rights_def
                       vm_read_write_def vm_read_only_def vm_kernel_only_def)[1] apply (simp add: validate_vm_rights_def valid_vm_rights_def
                 vm_read_write_def vm_read_only_def vm_kernel_only_def) apply safe apply simp+ apply (drule_tac x="{AllowRead, AllowWrite}" in spec, simp+) apply (drule_tac x="{AllowRead, AllowWrite}" in spec, simp+) apply (drule_tac x="{AllowRead, AllowWrite}" in spec, simp+) apply (drule_tac x="{AllowRead}" in spec, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. validate_vm_rights rs = (THE rs'. rs' \<subseteq> rs \<and> rs' \<in> valid_vm_rights \<and> (\<forall>rs''\<subseteq>rs. rs'' \<in> valid_vm_rights \<longrightarrow> rs'' \<subseteq> rs')) proof (prove)
goal (2 subgoals):
 1. validate_vm_rights rs \<subseteq> rs \<and> validate_vm_rights rs \<in> valid_vm_rights \<and> (\<forall>rs''\<subseteq>rs. rs'' \<in> valid_vm_rights \<longrightarrow> rs'' \<subseteq> validate_vm_rights rs)
 2. \<And>rs'. rs' \<subseteq> rs \<and> rs' \<in> valid_vm_rights \<and> (\<forall>rs''\<subseteq>rs. rs'' \<in> valid_vm_rights \<longrightarrow> rs'' \<subseteq> rs') \<Longrightarrow> rs' = validate_vm_rights rs proof (prove)
goal (1 subgoal):
 1. \<And>rs'. rs' \<subseteq> rs \<and> rs' \<in> valid_vm_rights \<and> (\<forall>rs''\<subseteq>rs. rs'' \<in> valid_vm_rights \<longrightarrow> rs'' \<subseteq> rs') \<Longrightarrow> rs' = validate_vm_rights rs proof (prove)
goal (1 subgoal):
 1. \<And>rs'. rs' \<subseteq> rs \<and> (rs' = {AllowRead, AllowWrite} \<or> rs' = {AllowRead} \<or> rs' = {}) \<and> (\<forall>rs''\<subseteq>rs. (rs'' = {AllowRead, AllowWrite} \<longrightarrow> AllowRead \<in> rs' \<and> AllowWrite \<in> rs') \<and> (rs'' = {AllowRead} \<longrightarrow> AllowRead \<in> rs')) \<Longrightarrow> (AllowWrite \<in> rs \<longrightarrow> (AllowRead \<in> rs \<longrightarrow> rs' = {AllowRead, AllowWrite}) \<and> (AllowRead \<notin> rs \<longrightarrow> rs' = {})) \<and> (AllowWrite \<notin> rs \<longrightarrow> (AllowRead \<in> rs \<longrightarrow> rs' = {AllowRead}) \<and> (AllowRead \<notin> rs \<longrightarrow> rs' = {})) proof (prove)
goal (11 subgoals):
 1. \<And>rs' x. \<lbrakk>{AllowRead, AllowWrite} \<subseteq> rs; \<forall>rs''\<subseteq>rs. (rs'' = {AllowRead, AllowWrite} \<longrightarrow> AllowRead \<in> {AllowRead, AllowWrite} \<and> AllowWrite \<in> {AllowRead, AllowWrite}) \<and> (rs'' = {AllowRead} \<longrightarrow> AllowRead \<in> {AllowRead, AllowWrite}); AllowWrite \<in> rs; AllowRead \<notin> rs\<rbrakk> \<Longrightarrow> AllowRead \<in> {}
 2. \<And>rs' x. \<lbrakk>{AllowRead, AllowWrite} \<subseteq> rs; \<forall>rs''\<subseteq>rs. (rs'' = {AllowRead, AllowWrite} \<longrightarrow> AllowRead \<in> {AllowRead, AllowWrite} \<and> AllowWrite \<in> {AllowRead, AllowWrite}) \<and> (rs'' = {AllowRead} \<longrightarrow> AllowRead \<in> {AllowRead, AllowWrite}); AllowWrite \<in> rs; AllowRead \<notin> rs\<rbrakk> \<Longrightarrow> AllowWrite \<in> {}
 3. \<And>rs' x. \<lbrakk>{AllowRead, AllowWrite} \<subseteq> rs; \<forall>rs''\<subseteq>rs. (rs'' = {AllowRead, AllowWrite} \<longrightarrow> AllowRead \<in> {AllowRead, AllowWrite} \<and> AllowWrite \<in> {AllowRead, AllowWrite}) \<and> (rs'' = {AllowRead} \<longrightarrow> AllowRead \<in> {AllowRead, AllowWrite}); AllowWrite \<notin> rs; AllowRead \<in> rs; AllowWrite \<notin> {}\<rbrakk> \<Longrightarrow> AllowWrite = AllowRead
 4. \<And>rs' x. \<lbrakk>{AllowRead, AllowWrite} \<subseteq> rs; \<forall>rs''\<subseteq>rs. (rs'' = {AllowRead, AllowWrite} \<longrightarrow> AllowRead \<in> {AllowRead, AllowWrite} \<and> AllowWrite \<in> {AllowRead, AllowWrite}) \<and> (rs'' = {AllowRead} \<longrightarrow> AllowRead \<in> {AllowRead, AllowWrite}); AllowWrite \<notin> rs; AllowRead \<notin> rs\<rbrakk> \<Longrightarrow> AllowRead \<in> {}
 5. \<And>rs' x. \<lbrakk>{AllowRead, AllowWrite} \<subseteq> rs; \<forall>rs''\<subseteq>rs. (rs'' = {AllowRead, AllowWrite} \<longrightarrow> AllowRead \<in> {AllowRead, AllowWrite} \<and> AllowWrite \<in> {AllowRead, AllowWrite}) \<and> (rs'' = {AllowRead} \<longrightarrow> AllowRead \<in> {AllowRead, AllowWrite}); AllowWrite \<notin> rs; AllowRead \<notin> rs\<rbrakk> \<Longrightarrow> AllowWrite \<in> {}
 6. \<And>rs' x. \<lbrakk>{AllowRead} \<subseteq> rs; \<forall>rs''\<subseteq>rs. (rs'' = {AllowRead, AllowWrite} \<longrightarrow> AllowRead \<in> {AllowRead} \<and> AllowWrite \<in> {AllowRead}) \<and> (rs'' = {AllowRead} \<longrightarrow> AllowRead \<in> {AllowRead}); AllowWrite \<in> rs; AllowRead \<in> rs; AllowWrite \<notin> {}\<rbrakk> \<Longrightarrow> AllowWrite = AllowRead
 7. \<And>rs' x. \<lbrakk>{AllowRead} \<subseteq> rs; \<forall>rs''\<subseteq>rs. (rs'' = {AllowRead, AllowWrite} \<longrightarrow> AllowRead \<in> {AllowRead} \<and> AllowWrite \<in> {AllowRead}) \<and> (rs'' = {AllowRead} \<longrightarrow> AllowRead \<in> {AllowRead}); AllowWrite \<in> rs; AllowRead \<notin> rs\<rbrakk> \<Longrightarrow> AllowRead \<in> {}
 8. \<And>rs' x. \<lbrakk>{AllowRead} \<subseteq> rs; \<forall>rs''\<subseteq>rs. (rs'' = {AllowRead, AllowWrite} \<longrightarrow> AllowRead \<in> {AllowRead} \<and> AllowWrite \<in> {AllowRead}) \<and> (rs'' = {AllowRead} \<longrightarrow> AllowRead \<in> {AllowRead}); AllowWrite \<notin> rs; AllowRead \<notin> rs\<rbrakk> \<Longrightarrow> AllowRead \<in> {}
 9. \<And>rs' x. \<lbrakk>{} \<subseteq> rs; \<forall>rs''\<subseteq>rs. (rs'' = {AllowRead, AllowWrite} \<longrightarrow> AllowRead \<in> {} \<and> AllowWrite \<in> {}) \<and> (rs'' = {AllowRead} \<longrightarrow> AllowRead \<in> {}); AllowWrite \<in> rs; AllowRead \<in> rs\<rbrakk> \<Longrightarrow> AllowRead \<in> {}
 10. \<And>rs' x. \<lbrakk>{} \<subseteq> rs; \<forall>rs''\<subseteq>rs. (rs'' = {AllowRead, AllowWrite} \<longrightarrow> AllowRead \<in> {} \<and> AllowWrite \<in> {}) \<and> (rs'' = {AllowRead} \<longrightarrow> AllowRead \<in> {}); AllowWrite \<in> rs; AllowRead \<in> rs\<rbrakk> \<Longrightarrow> AllowWrite \<in> {}
A total of 11 subgoals... proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<forall>rs''\<subseteq>rs. rs'' \<noteq> {AllowRead, AllowWrite}; AllowWrite \<in> rs; AllowRead \<in> rs\<rbrakk> \<Longrightarrow> False
 2. \<And>rs' x. \<lbrakk>{AllowRead} \<subseteq> rs; \<forall>rs''\<subseteq>rs. (rs'' = {AllowRead, AllowWrite} \<longrightarrow> AllowRead \<in> {AllowRead} \<and> AllowWrite \<in> {AllowRead}) \<and> (rs'' = {AllowRead} \<longrightarrow> AllowRead \<in> {AllowRead}); AllowWrite \<in> rs; AllowRead \<notin> rs\<rbrakk> \<Longrightarrow> AllowRead \<in> {}
 3. \<And>rs' x. \<lbrakk>{AllowRead} \<subseteq> rs; \<forall>rs''\<subseteq>rs. (rs'' = {AllowRead, AllowWrite} \<longrightarrow> AllowRead \<in> {AllowRead} \<and> AllowWrite \<in> {AllowRead}) \<and> (rs'' = {AllowRead} \<longrightarrow> AllowRead \<in> {AllowRead}); AllowWrite \<notin> rs; AllowRead \<notin> rs\<rbrakk> \<Longrightarrow> AllowRead \<in> {}
 4. \<And>rs' x. \<lbrakk>{} \<subseteq> rs; \<forall>rs''\<subseteq>rs. (rs'' = {AllowRead, AllowWrite} \<longrightarrow> AllowRead \<in> {} \<and> AllowWrite \<in> {}) \<and> (rs'' = {AllowRead} \<longrightarrow> AllowRead \<in> {}); AllowWrite \<in> rs; AllowRead \<in> rs\<rbrakk> \<Longrightarrow> AllowRead \<in> {}
 5. \<And>rs' x. \<lbrakk>{} \<subseteq> rs; \<forall>rs''\<subseteq>rs. (rs'' = {AllowRead, AllowWrite} \<longrightarrow> AllowRead \<in> {} \<and> AllowWrite \<in> {}) \<and> (rs'' = {AllowRead} \<longrightarrow> AllowRead \<in> {}); AllowWrite \<in> rs; AllowRead \<in> rs\<rbrakk> \<Longrightarrow> AllowWrite \<in> {}
 6. \<And>rs' x. \<lbrakk>{} \<subseteq> rs; \<forall>rs''\<subseteq>rs. (rs'' = {AllowRead, AllowWrite} \<longrightarrow> AllowRead \<in> {} \<and> AllowWrite \<in> {}) \<and> (rs'' = {AllowRead} \<longrightarrow> AllowRead \<in> {}); AllowWrite \<notin> rs; AllowRead \<in> rs\<rbrakk> \<Longrightarrow> AllowRead \<in> {} proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>rs''\<subseteq>rs. rs'' \<noteq> {AllowRead, AllowWrite} \<and> rs'' \<noteq> {AllowRead}; AllowWrite \<in> rs; AllowRead \<in> rs\<rbrakk> \<Longrightarrow> False
 2. \<And>rs' x. \<lbrakk>{} \<subseteq> rs; \<forall>rs''\<subseteq>rs. (rs'' = {AllowRead, AllowWrite} \<longrightarrow> AllowRead \<in> {} \<and> AllowWrite \<in> {}) \<and> (rs'' = {AllowRead} \<longrightarrow> AllowRead \<in> {}); AllowWrite \<in> rs; AllowRead \<in> rs\<rbrakk> \<Longrightarrow> AllowWrite \<in> {}
 3. \<And>rs' x. \<lbrakk>{} \<subseteq> rs; \<forall>rs''\<subseteq>rs. (rs'' = {AllowRead, AllowWrite} \<longrightarrow> AllowRead \<in> {} \<and> AllowWrite \<in> {}) \<and> (rs'' = {AllowRead} \<longrightarrow> AllowRead \<in> {}); AllowWrite \<notin> rs; AllowRead \<in> rs\<rbrakk> \<Longrightarrow> AllowRead \<in> {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>rs''\<subseteq>rs. rs'' \<noteq> {AllowRead, AllowWrite} \<and> rs'' \<noteq> {AllowRead}; AllowWrite \<in> rs; AllowRead \<in> rs\<rbrakk> \<Longrightarrow> False
 2. \<And>rs' x. \<lbrakk>{} \<subseteq> rs; \<forall>rs''\<subseteq>rs. (rs'' = {AllowRead, AllowWrite} \<longrightarrow> AllowRead \<in> {} \<and> AllowWrite \<in> {}) \<and> (rs'' = {AllowRead} \<longrightarrow> AllowRead \<in> {}); AllowWrite \<notin> rs; AllowRead \<in> rs\<rbrakk> \<Longrightarrow> AllowRead \<in> {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>rs''\<subseteq>rs. rs'' \<noteq> {AllowRead, AllowWrite} \<and> rs'' \<noteq> {AllowRead}; AllowWrite \<notin> rs; AllowRead \<in> rs\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!