kings-crown/FVELER_Isabelle huggingface dataset:
theory ExampleSystemPolicyFlows

lemma Sys3Affects_correct_fw : "\<lbrakk>x \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel (l)); l \<in> {T3, UT3}\<rbrakk> \<Longrightarrow> x \<in> Sys3Affects" apply (induct x rule:subjectAffects.induct) apply (auto simp:Sys3AuthGraph_def Sys3AuthGraph_aux_def complete_AuthGraph_def Sys3Affects_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l); l \<in> {T3, UT3}\<rbrakk> \<Longrightarrow> x \<in> Sys3Affects proof (prove)
goal (12 subgoals):
 1. l \<in> {T3, UT3} \<Longrightarrow> OrdinaryLabel l \<in> Sys3Affects
 2. \<And>auth l'. \<lbrakk>(OrdinaryLabel l, auth, l') \<in> Sys3AuthGraph; auth \<in> {Control, Write}; l \<in> {T3, UT3}\<rbrakk> \<Longrightarrow> l' \<in> Sys3Affects
 3. \<And>auth l'. \<lbrakk>(OrdinaryLabel l, auth, l') \<in> Sys3AuthGraph; auth \<in> {Receive, Notify, SyncSend, Call, Reset}; l \<in> {T3, UT3}\<rbrakk> \<Longrightarrow> l' \<in> Sys3Affects
 4. \<And>auth ep l' l''. \<lbrakk>(OrdinaryLabel l, auth, ep) \<in> Sys3AuthGraph; auth \<in> {SyncSend, Notify, Call}; (l', Receive, ep) \<in> Sys3AuthGraph; (l', Write, l'') \<in> Sys3AuthGraph; l \<in> {T3, UT3}\<rbrakk> \<Longrightarrow> l'' \<in> Sys3Affects
 5. \<And>ep l'. \<lbrakk>(OrdinaryLabel l, Receive, ep) \<in> Sys3AuthGraph; (l', SyncSend, ep) \<in> Sys3AuthGraph; l \<in> {T3, UT3}\<rbrakk> \<Longrightarrow> l' \<in> Sys3Affects
 6. \<And>l'. \<lbrakk>(l', Reply, OrdinaryLabel l) \<in> Sys3AuthGraph; l \<in> {T3, UT3}\<rbrakk> \<Longrightarrow> l' \<in> Sys3Affects
 7. \<And>l' l''. \<lbrakk>(OrdinaryLabel l, Reply, l') \<in> Sys3AuthGraph; (l', Write, l'') \<in> Sys3AuthGraph; l \<in> {T3, UT3}\<rbrakk> \<Longrightarrow> l'' \<in> Sys3Affects
 8. \<And>l'. \<lbrakk>(OrdinaryLabel l, DeleteDerived, l') \<in> Sys3AuthGraph; l \<in> {T3, UT3}\<rbrakk> \<Longrightarrow> l' \<in> Sys3Affects
 9. \<And>l' l''. \<lbrakk>(OrdinaryLabel l, DeleteDerived, l') \<in> Sys3AuthGraph; (l'', DeleteDerived, l') \<in> Sys3AuthGraph; l \<in> {T3, UT3}\<rbrakk> \<Longrightarrow> l'' \<in> Sys3Affects
 10. \<And>ep l' auth l''. \<lbrakk>(OrdinaryLabel l, Reset, ep) \<in> Sys3AuthGraph; (l', auth, ep) \<in> Sys3AuthGraph; auth \<in> {SyncSend, Receive}; (l', Write, l'') \<in> Sys3AuthGraph; l \<in> {T3, UT3}\<rbrakk> \<Longrightarrow> l'' \<in> Sys3Affects
A total of 12 subgoals... proof (prove)
goal:
No subgoals!
theory ExampleSystemPolicyFlows

lemma Sys3EP3Affects_correct_fw : "x \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel (EP3)) \<Longrightarrow> x \<in> Sys3EP3Affects" apply (induct x rule:subjectAffects.induct) apply (auto simp:Sys3AuthGraph_def Sys3AuthGraph_aux_def complete_AuthGraph_def Sys3EP3Affects_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel EP3) \<Longrightarrow> x \<in> Sys3EP3Affects proof (prove)
goal (12 subgoals):
 1. OrdinaryLabel EP3 \<in> Sys3EP3Affects
 2. \<And>auth l'. \<lbrakk>(OrdinaryLabel EP3, auth, l') \<in> Sys3AuthGraph; auth \<in> {Control, Write}\<rbrakk> \<Longrightarrow> l' \<in> Sys3EP3Affects
 3. \<And>auth l'. \<lbrakk>(OrdinaryLabel EP3, auth, l') \<in> Sys3AuthGraph; auth \<in> {Receive, Notify, SyncSend, Call, Reset}\<rbrakk> \<Longrightarrow> l' \<in> Sys3EP3Affects
 4. \<And>auth ep l' l''. \<lbrakk>(OrdinaryLabel EP3, auth, ep) \<in> Sys3AuthGraph; auth \<in> {SyncSend, Notify, Call}; (l', Receive, ep) \<in> Sys3AuthGraph; (l', Write, l'') \<in> Sys3AuthGraph\<rbrakk> \<Longrightarrow> l'' \<in> Sys3EP3Affects
 5. \<And>ep l'. \<lbrakk>(OrdinaryLabel EP3, Receive, ep) \<in> Sys3AuthGraph; (l', SyncSend, ep) \<in> Sys3AuthGraph\<rbrakk> \<Longrightarrow> l' \<in> Sys3EP3Affects
 6. \<And>l'. (l', Reply, OrdinaryLabel EP3) \<in> Sys3AuthGraph \<Longrightarrow> l' \<in> Sys3EP3Affects
 7. \<And>l' l''. \<lbrakk>(OrdinaryLabel EP3, Reply, l') \<in> Sys3AuthGraph; (l', Write, l'') \<in> Sys3AuthGraph\<rbrakk> \<Longrightarrow> l'' \<in> Sys3EP3Affects
 8. \<And>l'. (OrdinaryLabel EP3, DeleteDerived, l') \<in> Sys3AuthGraph \<Longrightarrow> l' \<in> Sys3EP3Affects
 9. \<And>l' l''. \<lbrakk>(OrdinaryLabel EP3, DeleteDerived, l') \<in> Sys3AuthGraph; (l'', DeleteDerived, l') \<in> Sys3AuthGraph\<rbrakk> \<Longrightarrow> l'' \<in> Sys3EP3Affects
 10. \<And>ep l' auth l''. \<lbrakk>(OrdinaryLabel EP3, Reset, ep) \<in> Sys3AuthGraph; (l', auth, ep) \<in> Sys3AuthGraph; auth \<in> {SyncSend, Receive}; (l', Write, l'') \<in> Sys3AuthGraph\<rbrakk> \<Longrightarrow> l'' \<in> Sys3EP3Affects
A total of 12 subgoals... proof (prove)
goal:
No subgoals!
theory ExampleSystemPolicyFlows

lemma Sys3EP3Affects_correct_bw : "x \<in> Sys3EP3Affects \<Longrightarrow> x \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel (EP3))" by (simp add:Sys3AuthGraph_def Sys3AuthGraph_aux_def complete_AuthGraph_def Sys3EP3Affects_def affects_lrefl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> Sys3EP3Affects \<Longrightarrow> x \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel EP3)
theory ExampleSystemPolicyFlows

lemma Sys3EP3Affects_correct : "subjectAffects Sys3AuthGraph (OrdinaryLabel (EP3)) = Sys3EP3Affects" apply (rule subset_antisym) apply (simp_all add:subsetI Sys3EP3Affects_correct_fw Sys3EP3Affects_correct_bw) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. subjectAffects Sys3AuthGraph (OrdinaryLabel EP3) = Sys3EP3Affects proof (prove)
goal (2 subgoals):
 1. subjectAffects Sys3AuthGraph (OrdinaryLabel EP3) \<subseteq> Sys3EP3Affects
 2. Sys3EP3Affects \<subseteq> subjectAffects Sys3AuthGraph (OrdinaryLabel EP3) proof (prove)
goal:
No subgoals!
theory ExampleSystemPolicyFlows

lemma Sys3Reads_correct : "l \<in> {T3, UT3, EP3} \<Longrightarrow> subjectReads Sys3AuthGraph (OrdinaryLabel (l)) = Sys3Reads" by (auto simp:subsetI Sys3Reads_correct_fw Sys3UT3Reads_correct_bw Sys3T3Reads_correct_bw Sys3EP3Reads_correct_bw)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. l \<in> {T3, UT3, EP3} \<Longrightarrow> subjectReads Sys3AuthGraph (OrdinaryLabel l) = Sys3Reads
theory ExampleSystemPolicyFlows

lemma Sys3Affects_correct : "l \<in> {T3, UT3} \<Longrightarrow> subjectAffects Sys3AuthGraph (OrdinaryLabel (l)) = Sys3Affects" by (auto simp:subsetI Sys3Affects_correct_fw Sys3UT3Affects_correct_bw Sys3T3Affects_correct_bw)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. l \<in> {T3, UT3} \<Longrightarrow> subjectAffects Sys3AuthGraph (OrdinaryLabel l) = Sys3Affects
theory ExampleSystemPolicyFlows

lemma IRQ3Reads : " d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel (IRQ3)) \<Longrightarrow> d = OrdinaryLabel (IRQ3)" apply (simp add: Sys3AuthGraph_def Sys3AuthGraph_aux_def complete_AuthGraph_def) apply (induct d rule: subjectReads.induct, auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel IRQ3) \<Longrightarrow> d = OrdinaryLabel IRQ3 proof (prove)
goal (1 subgoal):
 1. d \<in> subjectReads (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel IRQ3) \<Longrightarrow> d = OrdinaryLabel IRQ3 proof (prove)
goal:
No subgoals!
theory ExampleSystemPolicyFlows

lemma IRQ3Affects : "d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel (IRQ3)) \<Longrightarrow> d = OrdinaryLabel (IRQ3)" apply (simp add: Sys3AuthGraph_def Sys3AuthGraph_aux_def complete_AuthGraph_def) apply (induct d rule: subjectAffects.induct, auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel IRQ3) \<Longrightarrow> d = OrdinaryLabel IRQ3 proof (prove)
goal (1 subgoal):
 1. d \<in> subjectAffects (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel IRQ3) \<Longrightarrow> d = OrdinaryLabel IRQ3 proof (prove)
goal:
No subgoals!
theory ExampleSystemPolicyFlows

lemma IRQ3ReadsAndAffects :
  "\<lbrakk> d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel (l))
   ; d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel (IRQ3))
   \<rbrakk> \<Longrightarrow> l = IRQ3" apply (drule IRQ3Reads) apply (simp add: Sys3AuthGraph_def Sys3AuthGraph_aux_def complete_AuthGraph_def) apply (erule subjectAffects.cases, auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l); d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel IRQ3)\<rbrakk> \<Longrightarrow> l = IRQ3 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l); d = OrdinaryLabel IRQ3\<rbrakk> \<Longrightarrow> l = IRQ3 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>OrdinaryLabel IRQ3 \<in> subjectAffects (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel l); d = OrdinaryLabel IRQ3\<rbrakk> \<Longrightarrow> l = IRQ3 proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma Low_in_subjectReads_High:
  "partition_label Low \<in> subjectReads Sys1AuthGraph (partition_label High)" apply (simp add: Sys1AuthGraph_def reads_read) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label Low \<in> subjectReads Sys1AuthGraph (partition_label High) proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma subjectReads_High: "subjectReads Sys1AuthGraph (partition_label High) = {partition_label High,partition_label Low}" apply(rule equalityI) apply(rule subsetI) apply(erule subjectReads.induct, (fastforce simp: Sys1AuthGraph_def)+) apply(auto intro: Low_in_subjectReads_High) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. subjectReads Sys1AuthGraph (partition_label High) = {partition_label High, partition_label Low} proof (prove)
goal (2 subgoals):
 1. subjectReads Sys1AuthGraph (partition_label High) \<subseteq> {partition_label High, partition_label Low}
 2. {partition_label High, partition_label Low} \<subseteq> subjectReads Sys1AuthGraph (partition_label High) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> subjectReads Sys1AuthGraph (partition_label High) \<Longrightarrow> x \<in> {partition_label High, partition_label Low}
 2. {partition_label High, partition_label Low} \<subseteq> subjectReads Sys1AuthGraph (partition_label High) proof (prove)
goal (1 subgoal):
 1. {partition_label High, partition_label Low} \<subseteq> subjectReads Sys1AuthGraph (partition_label High) proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma High_in_subjectAffects_Low:
  "partition_label High \<in> subjectAffects Sys1AuthGraph (partition_label Low)" apply(rule affects_ep) apply (simp add: Sys1AuthGraph_def) apply (rule disjI1, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label High \<in> subjectAffects Sys1AuthGraph (partition_label Low) proof (prove)
goal (2 subgoals):
 1. (partition_label Low, ?auth, partition_label High) \<in> Sys1AuthGraph
 2. ?auth \<in> {Receive, Notify, SyncSend, Call, Reset} proof (prove)
goal (2 subgoals):
 1. ?auth = Notify \<or> ?auth = Reset
 2. ?auth \<in> {Receive, Notify, SyncSend, Call, Reset} proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma subjectAffects_Low: "subjectAffects Sys1AuthGraph (partition_label Low) = {partition_label Low, partition_label High}" apply(rule equalityI) apply(rule subsetI) apply(erule subjectAffects.induct, (fastforce simp: Sys1AuthGraph_def)+) apply(auto intro: affects_lrefl High_in_subjectAffects_Low) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. subjectAffects Sys1AuthGraph (partition_label Low) = {partition_label Low, partition_label High} proof (prove)
goal (2 subgoals):
 1. subjectAffects Sys1AuthGraph (partition_label Low) \<subseteq> {partition_label Low, partition_label High}
 2. {partition_label Low, partition_label High} \<subseteq> subjectAffects Sys1AuthGraph (partition_label Low) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> subjectAffects Sys1AuthGraph (partition_label Low) \<Longrightarrow> x \<in> {partition_label Low, partition_label High}
 2. {partition_label Low, partition_label High} \<subseteq> subjectAffects Sys1AuthGraph (partition_label Low) proof (prove)
goal (1 subgoal):
 1. {partition_label Low, partition_label High} \<subseteq> subjectAffects Sys1AuthGraph (partition_label Low) proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma subjectAffects_High: "subjectAffects Sys1AuthGraph (partition_label High) = {partition_label High}" apply(rule equalityI) apply(rule subsetI) apply(erule subjectAffects.induct, (fastforce simp: Sys1AuthGraph_def)+) apply(auto intro: affects_lrefl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. subjectAffects Sys1AuthGraph (partition_label High) = {partition_label High} proof (prove)
goal (2 subgoals):
 1. subjectAffects Sys1AuthGraph (partition_label High) \<subseteq> {partition_label High}
 2. {partition_label High} \<subseteq> subjectAffects Sys1AuthGraph (partition_label High) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> subjectAffects Sys1AuthGraph (partition_label High) \<Longrightarrow> x \<in> {partition_label High}
 2. {partition_label High} \<subseteq> subjectAffects Sys1AuthGraph (partition_label High) proof (prove)
goal (1 subgoal):
 1. {partition_label High} \<subseteq> subjectAffects Sys1AuthGraph (partition_label High) proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma subjectAffects_IRQ0: "subjectAffects Sys1AuthGraph (partition_label IRQ0) = {partition_label IRQ0}" apply(rule equalityI) apply(rule subsetI) apply(erule subjectAffects.induct, (fastforce simp: Sys1AuthGraph_def)+) apply(auto intro: affects_lrefl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. subjectAffects Sys1AuthGraph (partition_label IRQ0) = {partition_label IRQ0} proof (prove)
goal (2 subgoals):
 1. subjectAffects Sys1AuthGraph (partition_label IRQ0) \<subseteq> {partition_label IRQ0}
 2. {partition_label IRQ0} \<subseteq> subjectAffects Sys1AuthGraph (partition_label IRQ0) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> subjectAffects Sys1AuthGraph (partition_label IRQ0) \<Longrightarrow> x \<in> {partition_label IRQ0}
 2. {partition_label IRQ0} \<subseteq> subjectAffects Sys1AuthGraph (partition_label IRQ0) proof (prove)
goal (1 subgoal):
 1. {partition_label IRQ0} \<subseteq> subjectAffects Sys1AuthGraph (partition_label IRQ0) proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma partsSubjectAffects_Low: "partsSubjectAffects Sys1AuthGraph Low = {Partition Low, Partition High}" apply(auto simp: partsSubjectAffects_def image_def label_can_affect_partition_def subjectReads subjectAffects_Low | case_tac xa, rename_tac xa)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partsSubjectAffects Sys1AuthGraph Low = {Partition Low, Partition High} proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma partsSubjectAffects_High: "partsSubjectAffects Sys1AuthGraph High = {Partition High}" apply(auto simp: partsSubjectAffects_def image_def label_can_affect_partition_def subjectReads subjectAffects_High | rename_tac xa, case_tac xa)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partsSubjectAffects Sys1AuthGraph High = {Partition High} proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma partsSubjectAffects_IRQ0: "partsSubjectAffects Sys1AuthGraph IRQ0 = {Partition IRQ0}" apply(auto simp: partsSubjectAffects_def image_def label_can_affect_partition_def subjectReads subjectAffects_IRQ0 | rename_tac xa, case_tac xa)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partsSubjectAffects Sys1AuthGraph IRQ0 = {Partition IRQ0} proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma "policyFlows Sys1AuthGraph = example_policy" apply(rule equalityI) apply(rule subsetI) apply(clarsimp simp: example_policy_def) apply(erule policyFlows.cases) apply(case_tac l, auto simp: partsSubjectAffects)[1] apply assumption apply(rule subsetI) apply(clarsimp simp: example_policy_def) apply(elim disjE) apply(fastforce simp: partsSubjectAffects intro: policy_affects) apply(fastforce intro: policy_scheduler) apply(fastforce intro: policyFlows_refl refl_onD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. policyFlows Sys1AuthGraph = example_policy proof (prove)
goal (2 subgoals):
 1. policyFlows Sys1AuthGraph \<subseteq> example_policy
 2. example_policy \<subseteq> policyFlows Sys1AuthGraph proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> policyFlows Sys1AuthGraph \<Longrightarrow> x \<in> example_policy
 2. example_policy \<subseteq> policyFlows Sys1AuthGraph proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) \<in> policyFlows Sys1AuthGraph; a = Partition Low \<longrightarrow> b \<noteq> Partition High; a \<noteq> b\<rbrakk> \<Longrightarrow> a = PSched
 2. example_policy \<subseteq> policyFlows Sys1AuthGraph proof (prove)
goal (3 subgoals):
 1. \<And>a b d l. \<lbrakk>a = Partition Low \<longrightarrow> b \<noteq> Partition High; a \<noteq> b; a = Partition l; b = d; d \<in> partsSubjectAffects Sys1AuthGraph l\<rbrakk> \<Longrightarrow> a = PSched
 2. \<And>a b d. \<lbrakk>a = Partition Low \<longrightarrow> b \<noteq> Partition High; a \<noteq> b; a = PSched; b = d\<rbrakk> \<Longrightarrow> a = PSched
 3. example_policy \<subseteq> policyFlows Sys1AuthGraph proof (prove)
goal (2 subgoals):
 1. \<And>a b d. \<lbrakk>a = Partition Low \<longrightarrow> b \<noteq> Partition High; a \<noteq> b; a = PSched; b = d\<rbrakk> \<Longrightarrow> a = PSched
 2. example_policy \<subseteq> policyFlows Sys1AuthGraph proof (prove)
goal (1 subgoal):
 1. example_policy \<subseteq> policyFlows Sys1AuthGraph proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> example_policy \<Longrightarrow> x \<in> policyFlows Sys1AuthGraph proof (prove)
goal (1 subgoal):
 1. \<And>a b. a = Partition Low \<and> b = Partition High \<or> a = PSched \<or> a = b \<Longrightarrow> (a, b) \<in> policyFlows Sys1AuthGraph proof (prove)
goal (3 subgoals):
 1. \<And>a b. a = Partition Low \<and> b = Partition High \<Longrightarrow> (a, b) \<in> policyFlows Sys1AuthGraph
 2. \<And>a b. a = PSched \<Longrightarrow> (a, b) \<in> policyFlows Sys1AuthGraph
 3. \<And>a b. a = b \<Longrightarrow> (a, b) \<in> policyFlows Sys1AuthGraph proof (prove)
goal (2 subgoals):
 1. \<And>a b. a = PSched \<Longrightarrow> (a, b) \<in> policyFlows Sys1AuthGraph
 2. \<And>a b. a = b \<Longrightarrow> (a, b) \<in> policyFlows Sys1AuthGraph proof (prove)
goal (1 subgoal):
 1. \<And>a b. a = b \<Longrightarrow> (a, b) \<in> policyFlows Sys1AuthGraph proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma "asid_high_bits_of High_asid \<noteq> asid_high_bits_of Low_asid" by (simp add: Low_asid_def asid_high_bits_of_def High_asid_def asid_low_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. asid_high_bits_of High_asid \<noteq> asid_high_bits_of Low_asid
theory Example_Valid_State

lemma nat_to_bl_id [simp]: "nat_to_bl (size (x :: (('a::len) word))) (unat x) = Some (to_bl x)" by (clarsimp simp: nat_to_bl_def to_bl_def le_def word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. nat_to_bl (size x) (unat x) = Some (to_bl x)
theory Example_Valid_State

lemma len_the_nat_to_bl [simp]:
    "length (the_nat_to_bl x y) = x" apply (clarsimp simp: the_nat_to_bl_def nat_to_bl_def) apply safe apply (metis le_def mod_less_divisor nat_zero_less_power_iff zero_less_numeral) apply (clarsimp simp: len_bin_to_bl_aux not_le) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length (the_nat_to_bl x y) = x proof (prove)
goal (1 subgoal):
 1. (2 ^ x \<le> y mod 2 ^ x \<longrightarrow> length (the None) = x) \<and> (\<not> 2 ^ x \<le> y mod 2 ^ x \<longrightarrow> length (bin_to_bl_aux x (int (y mod 2 ^ x)) []) = x) proof (prove)
goal (2 subgoals):
 1. 2 ^ x \<le> y mod 2 ^ x \<Longrightarrow> length (the None) = x
 2. \<not> 2 ^ x \<le> y mod 2 ^ x \<Longrightarrow> length (bin_to_bl_aux x (int (y mod 2 ^ x)) []) = x proof (prove)
goal (1 subgoal):
 1. \<not> 2 ^ x \<le> y mod 2 ^ x \<Longrightarrow> length (bin_to_bl_aux x (int (y mod 2 ^ x)) []) = x proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma tcb_cnode_index_nat_to_bl [simp]:
  "the_nat_to_bl_10 n \<noteq> tcb_cnode_index n" by (clarsimp simp: tcb_cnode_index_def intro!: length_neq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. the_nat_to_bl 10 n \<noteq> tcb_cnode_index n
theory Example_Valid_State

lemma mod_less_self [simp]:
    "a \<le> b mod a \<longleftrightarrow> ((a :: nat) = 0)" by (metis mod_less_divisor nat_neq_iff not_less not_less0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a \<le> b mod a) = (a = 0)
theory Example_Valid_State

lemma split_div_mod:
    "a = (b::nat) \<longleftrightarrow> (a div k = b div k \<and> a mod k = b mod k)" by (metis mult_div_mod_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a = b) = (a div k = b div k \<and> a mod k = b mod k)
theory Example_Valid_State

lemma the_the_eq:
    "\<lbrakk> x \<noteq> None; y \<noteq> None \<rbrakk> \<Longrightarrow> (the x = the y) = (x = y)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> None; y \<noteq> None\<rbrakk> \<Longrightarrow> (the x = the y) = (x = y)
theory Example_Valid_State

lemma the_nat_to_bl_eq [simp]:
    "(the_nat_to_bl n a = the_nat_to_bl m b) \<longleftrightarrow> (n = m \<and> (a mod 2 ^ n = b mod 2 ^ n))" apply (case_tac "n = m") apply (clarsimp simp: the_nat_to_bl_def) apply (subst the_the_eq) apply (clarsimp simp: nat_to_bl_def) apply (clarsimp simp: nat_to_bl_def) apply simp apply simp apply (metis len_the_nat_to_bl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (the_nat_to_bl n a = the_nat_to_bl m b) = (n = m \<and> a mod 2 ^ n = b mod 2 ^ n) proof (prove)
goal (2 subgoals):
 1. n = m \<Longrightarrow> (the_nat_to_bl n a = the_nat_to_bl m b) = (n = m \<and> a mod 2 ^ n = b mod 2 ^ n)
 2. n \<noteq> m \<Longrightarrow> (the_nat_to_bl n a = the_nat_to_bl m b) = (n = m \<and> a mod 2 ^ n = b mod 2 ^ n) proof (prove)
goal (2 subgoals):
 1. n = m \<Longrightarrow> (the (nat_to_bl m (a mod 2 ^ m)) = the (nat_to_bl m (b mod 2 ^ m))) = (a mod 2 ^ m = b mod 2 ^ m)
 2. n \<noteq> m \<Longrightarrow> (the_nat_to_bl n a = the_nat_to_bl m b) = (n = m \<and> a mod 2 ^ n = b mod 2 ^ n) proof (prove)
goal (4 subgoals):
 1. n = m \<Longrightarrow> nat_to_bl m (a mod 2 ^ m) \<noteq> None
 2. n = m \<Longrightarrow> nat_to_bl m (b mod 2 ^ m) \<noteq> None
 3. n = m \<Longrightarrow> (nat_to_bl m (a mod 2 ^ m) = nat_to_bl m (b mod 2 ^ m)) = (a mod 2 ^ m = b mod 2 ^ m)
 4. n \<noteq> m \<Longrightarrow> (the_nat_to_bl n a = the_nat_to_bl m b) = (n = m \<and> a mod 2 ^ n = b mod 2 ^ n) proof (prove)
goal (3 subgoals):
 1. n = m \<Longrightarrow> nat_to_bl m (b mod 2 ^ m) \<noteq> None
 2. n = m \<Longrightarrow> (nat_to_bl m (a mod 2 ^ m) = nat_to_bl m (b mod 2 ^ m)) = (a mod 2 ^ m = b mod 2 ^ m)
 3. n \<noteq> m \<Longrightarrow> (the_nat_to_bl n a = the_nat_to_bl m b) = (n = m \<and> a mod 2 ^ n = b mod 2 ^ n) proof (prove)
goal (2 subgoals):
 1. n = m \<Longrightarrow> (nat_to_bl m (a mod 2 ^ m) = nat_to_bl m (b mod 2 ^ m)) = (a mod 2 ^ m = b mod 2 ^ m)
 2. n \<noteq> m \<Longrightarrow> (the_nat_to_bl n a = the_nat_to_bl m b) = (n = m \<and> a mod 2 ^ n = b mod 2 ^ n) proof (prove)
goal (1 subgoal):
 1. n \<noteq> m \<Longrightarrow> (the_nat_to_bl n a = the_nat_to_bl m b) = (n = m \<and> a mod 2 ^ n = b mod 2 ^ n) proof (prove)
goal (1 subgoal):
 1. n \<noteq> m \<Longrightarrow> the_nat_to_bl n a \<noteq> the_nat_to_bl m b proof (prove)
goal:
No subgoals!