This is an automated email from the ASF dual-hosted git repository. yulongzhang pushed a commit to branch master in repository https://gitbox.apache.org/repos/asf/incubator-teaclave-verification.git
commit 8617dc01f470dad2dacb5d53736e30798c28b624 Author: 小狈 <[email protected]> AuthorDate: Wed Mar 17 02:18:32 2021 +0800 Extra lemma proof and add more axioms Signed-off-by: Cao Shuang <[email protected]> --- access_control_module/AttrConf.thy | 327 ++++++++++++++++----- .../interpretation/I_AttrConf.thy | 255 ++++------------ access_control_module/interpretation/I_FMT_MSA.thy | 227 ++++++-------- 3 files changed, 413 insertions(+), 396 deletions(-) diff --git a/access_control_module/AttrConf.thy b/access_control_module/AttrConf.thy index c7ceef2..9c1c149 100644 --- a/access_control_module/AttrConf.thy +++ b/access_control_module/AttrConf.thy @@ -36,65 +36,108 @@ locale AttrConf= assumes ATTRCONFHLR2:"is_attrconf(attr_conf conf attr)" assumes ATTRCONFHLR3:"x=noattrconf\<or>(\<exists>conf attr. x=attr_conf conf attr)" assumes ATTRCONFHLR4:"attr_elem noattr=noelem" - assumes ATTRCONFHLR5:"\<not>find_elem noattrconf attr" - assumes ATTRCONFHLR6:"conf=noattrconf\<and> - attr_elem attr\<noteq>noelem\<and> - attr_elem attrx=attr_elem attr\<Longrightarrow> + assumes ATTRCONFHLR6:"\<not>find_elem noattrconf attr" + assumes ATTRCONFHLR7:"attr_elem attrx=attr_elem attr\<Longrightarrow> find_elem(attr_conf conf attrx) attr" - assumes ATTRCONFHLR7:"conf\<noteq>noattrconf\<and> - attr_elem attr\<noteq>noelem\<and> - attr_elem attrx=attr_elem attr\<Longrightarrow> + assumes ATTRCONFHLR8:"find_elem conf attr\<Longrightarrow> find_elem(attr_conf conf attrx) attr" - assumes ATTRCONFHLR8:"find_elem conf attr\<and> - attr_elem attr=attr_elem attrx\<Longrightarrow> - find_elem conf attrx" - assumes ATTRCONFHLR9:"conf\<noteq>noattrconf\<and> - find_elem conf attr\<Longrightarrow> - find_elem(attr_conf conf attrx) attr" - assumes ATTRCONFHLR10:"\<not>((conf=noattrconf\<and> - attr_elem attr\<noteq>noelem\<and> - attr_elem attrx=attr_elem attr)\<or> - (conf\<noteq>noattrconf\<and> - attr_elem attr\<noteq>noelem\<and> - attr_elem attrx=attr_elem attr)\<or> - (conf\<noteq>noattrconf\<and> - find_elem conf attr))\<Longrightarrow> + assumes ATTRCONFHLR9:"(\<not>find_elem conf attr)\<and> + attr_elem attrx\<noteq>attr_elem attr\<Longrightarrow> \<not>find_elem(attr_conf conf attrx) attr" - assumes ATTRCONFHLR11:"delete_attr noattrconf attr=noattrconf" - assumes ATTRCONFHLR12:"attr_elem attrx=attr_elem attr\<and> - attr_elem attr\<noteq>noelem\<Longrightarrow> - delete_attr(attr_conf conf attrx) attr=conf" - assumes ATTRCONFHLR13:"attr_elem attr=noelem\<Longrightarrow> - delete_attr(attr_conf conf attrx) attr=attr_conf conf attrx" - assumes ATTRCONFHLR14:"attr_elem attrx\<noteq>attr_elem attr\<and> - attr_elem attr\<noteq>noelem\<Longrightarrow> + assumes ATTRCONFHLR10:"delete_attr noattrconf attr=noattrconf" + assumes ATTRCONFHLR11:"attr_elem attrx=attr_elem attr\<Longrightarrow> + delete_attr(attr_conf conf attrx) attr=delete_attr conf attr" + assumes ATTRCONFHLR12:"attr_elem attrx\<noteq>attr_elem attr\<Longrightarrow> delete_attr(attr_conf conf attrx) attr= - attr_conf(delete_attr conf attr) attrx" - assumes ATTRCONFHLR15:"get_attr noattrconf elem=noattr" - assumes ATTRCONFHLR16:"elem\<noteq>noelem\<and> - attr_elem attr=elem\<Longrightarrow> + attr_conf (delete_attr conf attr) attrx" + assumes ATTRCONFHLR13:"get_attr noattrconf elem=noattr" + assumes ATTRCONFHLR14:"attr_elem attr=elem\<Longrightarrow> get_attr(attr_conf conf attr) elem=attr" - assumes ATTRCONFHLR17:"elem=noelem\<Longrightarrow> + assumes ATTRCONFHLR15:"get_attr conf elem=noattr\<and> + attr_elem attr\<noteq>elem\<Longrightarrow> get_attr(attr_conf conf attr) elem=noattr" - assumes ATTRCONFHLR18:"elem\<noteq>noelem\<and> + assumes ATTRCONFHLR16:"get_attr conf elem\<noteq>noattr\<and> attr_elem attr\<noteq>elem\<Longrightarrow> get_attr(attr_conf conf attr) elem=get_attr conf elem" - assumes ATTRCONFHLR19:"\<not>valid_attrconf noattrconf" - assumes ATTRCONFHLR20:"conf=noattrconf\<and> - \<not>find_elem conf attr\<Longrightarrow> + assumes ATTRCONFHLR17:"\<not>valid_attrconf noattrconf" + assumes ATTRCONFHLR18:"attr_elem attr\<noteq>noelem\<and> + conf=noattrconf\<Longrightarrow> valid_attrconf(attr_conf conf attr)" - assumes ATTRCONFHLR21:"conf\<noteq>noattrconf\<and> - \<not>find_elem conf attr\<and> - valid_attrconf conf\<Longrightarrow> + assumes ATTRCONFHLR19:"valid_attrconf conf\<and> + (\<not>find_elem conf attr)\<and> + attr_elem attr\<noteq>noelem\<Longrightarrow> valid_attrconf(attr_conf conf attr)" - assumes ATTRCONFHLR22:"\<not>((conf=noattrconf\<and> - \<not>find_elem conf attr)\<or> - (conf\<noteq>noattrconf\<and> - \<not>find_elem conf attr\<and> - valid_attrconf conf))\<Longrightarrow> + assumes ATTRCONFHLR20:"attr_elem attr=noelem\<Longrightarrow>\<not>valid_attrconf(attr_conf conf attr)" + assumes ATTRCONFHLR21:"conf\<noteq>noattrconf\<and> + \<not>valid_attrconf conf\<Longrightarrow> \<not>valid_attrconf(attr_conf conf attr)" + assumes ATTRCONFHLR22:"conf\<noteq>noattrconf\<and> + find_elem conf attr\<Longrightarrow> + \<not>valid_attrconf(attr_conf conf attr)" + assumes ATTRCONFINDUCT:"\<lbrakk>P noattrconf;\<And>conf1 attr1. P conf1\<Longrightarrow>P(attr_conf conf1 attr1)\<rbrakk>\<Longrightarrow>P conf" begin +lemma find_total:"find_elem conf attr\<or> + attr_elem attrx=attr_elem attr\<Longrightarrow>find_elem(attr_conf conf attrx) attr" +proof (erule disjE) + assume "find_elem conf attr" + from this show "find_elem (attr_conf conf attrx) attr" by (rule ATTRCONFHLR8) +next + assume "attr_elem attrx = attr_elem attr" + from this show "find_elem (attr_conf conf attrx) attr" by (rule ATTRCONFHLR7) +qed + +lemma find_dual: + "find_elem conf attr\<or> + attr_elem attrx=attr_elem attr= + (\<not>((\<not>find_elem conf attr)\<and>attr_elem attrx\<noteq>attr_elem attr))" + by blast + +lemma valid_total:"(attr_elem attr\<noteq>noelem\<and> + conf=noattrconf)\<or> + (valid_attrconf conf\<and> + (\<not>find_elem conf attr)\<and> + attr_elem attr\<noteq>noelem)\<Longrightarrow>valid_attrconf(attr_conf conf attr)" +proof (erule disjE) + assume "attr_elem attr \<noteq> noelem \<and> conf = noattrconf" + from this show "valid_attrconf (attr_conf conf attr)" by (rule ATTRCONFHLR18) +next + assume "valid_attrconf conf \<and> + \<not> find_elem conf attr \<and> attr_elem attr \<noteq> noelem" + from this show "valid_attrconf (attr_conf conf attr)" by (rule ATTRCONFHLR19) +qed + +lemma not_valid_total:"attr_elem attr=noelem\<or> + ((\<not>valid_attrconf conf)\<and> + conf\<noteq>noattrconf)\<or> + (conf\<noteq>noattrconf\<and> + find_elem conf attr)\<Longrightarrow>\<not>valid_attrconf(attr_conf conf attr)" +proof (erule disjE) + assume "attr_elem attr = noelem" + from this show "\<not>valid_attrconf(attr_conf conf attr)" by (rule ATTRCONFHLR20) +next + show "\<not> valid_attrconf conf \<and> + conf \<noteq> noattrconf \<or> + conf \<noteq> noattrconf \<and> + find_elem conf attr \<Longrightarrow> + \<not> valid_attrconf (attr_conf conf attr)" + proof (erule disjE) + assume "\<not> valid_attrconf conf \<and> conf \<noteq> noattrconf" + from this show "\<not> valid_attrconf (attr_conf conf attr)" by (auto simp: ATTRCONFHLR21) + next + assume "conf \<noteq> noattrconf \<and> find_elem conf attr" + from this show "\<not> valid_attrconf (attr_conf conf attr)" by (auto simp: ATTRCONFHLR22) + qed +qed + +lemma valid_dual: + "(attr_elem attr\<noteq>noelem\<and>conf=noattrconf)\<or> + (valid_attrconf conf\<and>(\<not>find_elem conf attr)\<and>attr_elem attr\<noteq>noelem)= + (\<not>(attr_elem attr=noelem\<or> + ((\<not>valid_attrconf conf)\<and>conf\<noteq>noattrconf)\<or> + (conf\<noteq>noattrconf\<and>find_elem conf attr)))" + by blast + lemma ATTRCONFHLR23:"noattrconf\<noteq>attr_conf conf attr" proof fix conf attr @@ -110,19 +153,94 @@ proof - from ATTRCONFHLR3 0 show "\<exists>sconf oconf. x = attr_conf sconf oconf" by blast qed -lemma ATTRCONFHLR25:"conf=noattrconf\<and> - attr_elem attrx\<noteq>attr_elem attr\<Longrightarrow>\<not>find_elem(attr_conf conf attrx) attr" -proof - - assume "conf = noattrconf \<and> attr_elem attrx \<noteq> attr_elem attr" - from this have "\<not>((conf=noattrconf\<and> - attr_elem attr\<noteq>noelem\<and> - attr_elem attrx=attr_elem attr)\<or> - (conf\<noteq>noattrconf\<and> - attr_elem attr\<noteq>noelem\<and> - attr_elem attrx=attr_elem attr)\<or> - (conf\<noteq>noattrconf\<and> - find_elem conf attr))" by blast - from this show "\<not>find_elem(attr_conf conf attrx) attr" by (rule ATTRCONFHLR10) +lemma ATTRCONFHLR25:"valid_attrconf conf\<and> + find_elem conf attr\<Longrightarrow>attr_elem attr\<noteq>noelem" +proof (induction rule:ATTRCONFINDUCT) + show "valid_attrconf noattrconf \<and> find_elem noattrconf attr \<Longrightarrow> + attr_elem attr \<noteq> noelem" by (auto simp:ATTRCONFHLR17) +next + fix conf1 attr1 + show "(valid_attrconf conf1 \<and> find_elem conf1 attr \<Longrightarrow> + attr_elem attr \<noteq> noelem) \<Longrightarrow> + valid_attrconf (attr_conf conf1 attr1) \<and> + find_elem (attr_conf conf1 attr1) attr \<Longrightarrow> + attr_elem attr \<noteq> noelem" + proof (auto) + assume 1:"valid_attrconf conf1 \<and> find_elem conf1 attr \<Longrightarrow> False" + assume 2:"find_elem (attr_conf conf1 attr1) attr" + assume 3:"noelem = attr_elem attr" + assume "valid_attrconf (attr_conf conf1 attr1)" + from this have 4:"(attr_elem attr1\<noteq>noelem\<and> + conf1=noattrconf)\<or> + (valid_attrconf conf1\<and> + (\<not>find_elem conf1 attr1)\<and> + attr_elem attr1\<noteq>noelem)" + proof (rule contrapos_pp) + assume "\<not> (attr_elem attr1 \<noteq> noelem \<and> + conf1 = noattrconf \<or> + valid_attrconf conf1 \<and> + \<not> find_elem conf1 attr1 \<and> + attr_elem attr1 \<noteq> noelem)" + from this have "attr_elem attr1=noelem\<or> + ((\<not>valid_attrconf conf1)\<and> + conf1\<noteq>noattrconf)\<or> + (conf1\<noteq>noattrconf\<and> + find_elem conf1 attr1)" by (auto simp:valid_dual) + from this show "\<not> valid_attrconf (attr_conf conf1 attr1)" by (rule not_valid_total) + qed + from 2 have 2:"find_elem conf1 attr\<or> + attr_elem attr1=attr_elem attr" + proof (rule contrapos_pp) + assume "\<not> (find_elem conf1 attr \<or> + attr_elem attr1 = attr_elem attr)" + from this have "((\<not>find_elem conf1 attr)\<and> + attr_elem attr1\<noteq>attr_elem attr)" by (auto simp:find_dual) + from this show "\<not> find_elem (attr_conf conf1 attr1) attr" by (rule ATTRCONFHLR9) + qed + from 2 3 4 have "(find_elem conf1 attr \<or> + attr_elem attr1 = attr_elem attr)\<and> + (noelem = attr_elem attr)\<and> + (attr_elem attr1 \<noteq> noelem \<and> + conf1 = noattrconf \<or> + valid_attrconf conf1 \<and> + \<not> find_elem conf1 attr1 \<and> + attr_elem attr1 \<noteq> noelem)" by auto + from this show False + proof (auto simp:ATTRCONFHLR6) + from 1 show "noelem = attr_elem attr \<Longrightarrow> + find_elem conf1 attr \<Longrightarrow> + valid_attrconf conf1 \<Longrightarrow> + \<not> find_elem conf1 attr1 \<Longrightarrow> + attr_elem attr1 \<noteq> attr_elem attr \<Longrightarrow> False" by (auto simp:1) + qed + qed +qed + +lemma ATTRCONFHLR26:"find_elem conf attr\<and> + attr_elem attr=attr_elem attrx\<Longrightarrow>find_elem conf attrx" +proof (induction conf rule:ATTRCONFINDUCT) + assume "find_elem noattrconf attr \<and> attr_elem attr = attr_elem attrx" + from this show "find_elem noattrconf attrx" by (auto simp:ATTRCONFHLR6) +next + fix conf1 attr1 + assume 0:"find_elem conf1 attr \<and> + attr_elem attr = attr_elem attrx \<Longrightarrow> + find_elem conf1 attrx" + assume "find_elem (attr_conf conf1 attr1) attr \<and> + attr_elem attr = attr_elem attrx" + from this have 1:"attr_elem attr = attr_elem attrx" + and 2:"find_elem (attr_conf conf1 attr1) attr" by auto + from 2 have 2:"find_elem conf1 attr\<or> + attr_elem attr1=attr_elem attr" + proof (rule contrapos_pp) + assume "\<not> (find_elem conf1 attr \<or> + attr_elem attr1 = attr_elem attr)" + from this have "((\<not>find_elem conf1 attr)\<and> + attr_elem attr1\<noteq>attr_elem attr)" by (auto simp:find_dual) + from this show "\<not> find_elem (attr_conf conf1 attr1) attr" by (rule ATTRCONFHLR9) + qed + from 1 2 show "find_elem (attr_conf conf1 attr1) attrx" + by (auto simp add:0 ATTRCONFHLR8 ATTRCONFHLR7) qed end @@ -142,7 +260,7 @@ locale AttrConfRel=AttrConf noelem noattr noattrconf attr_conf is_attrconf attr_ and get_attr::"'attrconf\<Rightarrow>'element\<Rightarrow>'attr" and valid_attrconf::"'attrconf\<Rightarrow>bool" + fixes rel_subset::"'attrconf\<Rightarrow>'attrconf\<Rightarrow>bool" - assumes ATTRCONFRELHLR1:"\<not>rel_subset confx noattrconf" + assumes ATTRCONFRELHLR1:"rel_subset confx noattrconf" assumes ATTRCONFRELHLR2:"conf=noattrconf\<and> find_elem confx attr\<Longrightarrow> rel_subset confx (attr_conf conf attr)" @@ -150,13 +268,90 @@ locale AttrConfRel=AttrConf noelem noattr noattrconf attr_conf is_attrconf attr_ find_elem confx attr\<and> rel_subset confx conf\<Longrightarrow> rel_subset confx (attr_conf conf attr)" - assumes ATTRCONFRELHLR4:"\<not>((conf\<noteq>noattrconf\<and> - find_elem confx attr\<and> - rel_subset confx conf)\<or> - (conf=noattrconf\<and> - find_elem confx attr))\<Longrightarrow> + assumes ATTRCONFRELHLR4:"\<not>rel_subset confx conf\<Longrightarrow> \<not>rel_subset confx (attr_conf conf attr)" - assumes ATTRCONFRELHLR5:"rel_subset confx conf\<and>find_elem conf attr\<Longrightarrow>find_elem confx attr" + assumes ATTRCONFRELHLR5:"rel_subset confx conf\<and> + \<not>find_elem confx attr\<Longrightarrow> + \<not>rel_subset confx (attr_conf conf attr)" +begin + +lemma rel_subset_total:"(conf=noattrconf\<and> + find_elem confx attr)\<or> + (conf\<noteq>noattrconf\<and> + find_elem confx attr\<and> + rel_subset confx conf)\<Longrightarrow>rel_subset confx (attr_conf conf attr)" +proof (erule disjE) + assume "conf = noattrconf \<and> find_elem confx attr" + from this show "rel_subset confx (attr_conf conf attr)" by (rule ATTRCONFRELHLR2) +next + assume "conf \<noteq> noattrconf \<and> find_elem confx attr \<and> rel_subset confx conf" + from this show "rel_subset confx (attr_conf conf attr)" by (rule ATTRCONFRELHLR3) +qed + +lemma not_rel_subset_total:"(\<not>rel_subset confx conf)\<or> + (rel_subset confx conf\<and>\<not>find_elem confx attr)\<Longrightarrow> + \<not>rel_subset confx (attr_conf conf attr)" +proof (erule disjE) + assume "\<not> rel_subset confx conf" + from this show "\<not> rel_subset confx (attr_conf conf attr)" by (rule ATTRCONFRELHLR4) +next + assume "rel_subset confx conf \<and> \<not> find_elem confx attr" + from this show "\<not> rel_subset confx (attr_conf conf attr)" by (rule ATTRCONFRELHLR5) +qed + +lemma rel_subset_dual: + "(conf=noattrconf\<and>find_elem confx attr)\<or> + (conf\<noteq>noattrconf\<and>find_elem confx attr\<and>rel_subset confx conf)= + (\<not>((\<not>rel_subset confx conf)\<or>(rel_subset confx conf\<and>\<not>find_elem confx attr)))" + by blast + +lemma ATTRCONFRELHLR6:"rel_subset confx conf\<and>find_elem conf attr\<Longrightarrow>find_elem confx attr" +proof (induction conf rule:ATTRCONFINDUCT) + assume "rel_subset confx noattrconf \<and> find_elem noattrconf attr" + from this show "find_elem confx attr" by (auto simp:ATTRCONFHLR6) +next + fix conf1 attr1 + assume 0:"rel_subset confx conf1 \<and> find_elem conf1 attr \<Longrightarrow> + find_elem confx attr" + assume "rel_subset confx (attr_conf conf1 attr1) \<and> + find_elem (attr_conf conf1 attr1) attr" + from this have 1:"rel_subset confx (attr_conf conf1 attr1)" + and 2:"find_elem (attr_conf conf1 attr1) attr" by auto + from 1 have 1:"(conf1=noattrconf\<and> + find_elem confx attr1)\<or> + (conf1\<noteq>noattrconf\<and> + find_elem confx attr1\<and> + rel_subset confx conf1)" + proof (rule contrapos_pp) + assume "\<not> (conf1 = noattrconf \<and> find_elem confx attr1 \<or> + conf1 \<noteq> noattrconf \<and> + find_elem confx attr1 \<and> rel_subset confx conf1)" + from this have "((\<not>rel_subset confx conf1)\<or> + (rel_subset confx conf1\<and>\<not>find_elem confx attr1))" + by (auto simp:rel_subset_dual) + from this show "\<not> rel_subset confx (attr_conf conf1 attr1)" + by (auto simp:not_rel_subset_total) + qed + from 2 have 2:"find_elem conf1 attr\<or> + attr_elem attr1=attr_elem attr" + proof (rule contrapos_pp) + assume "\<not> (find_elem conf1 attr \<or> + attr_elem attr1 = attr_elem attr)" + from this have "((\<not>find_elem conf1 attr)\<and> + attr_elem attr1\<noteq>attr_elem attr)" by (auto simp:find_dual) + from this show "\<not> find_elem (attr_conf conf1 attr1) attr" by (rule ATTRCONFHLR9) + qed + from 1 2 have "(conf1 = noattrconf \<and> + find_elem confx attr1 \<or> + conf1 \<noteq> noattrconf \<and> + find_elem confx attr1 \<and> + rel_subset confx conf1)\<and> + (find_elem conf1 attr \<or> + attr_elem attr1 = attr_elem attr)" by auto + from this show ?thesis by (auto simp add:0 ATTRCONFHLR26 ATTRCONFHLR6) +qed + +end print_locale! AttrConfRel diff --git a/access_control_module/interpretation/I_AttrConf.thy b/access_control_module/interpretation/I_AttrConf.thy index 9e7561c..d4240d6 100644 --- a/access_control_module/interpretation/I_AttrConf.thy +++ b/access_control_module/interpretation/I_AttrConf.thy @@ -24,11 +24,12 @@ begin datatype UsrAttrConf = nousrattrconf | is_usrattrconf:usrattr_conf UsrAttrConf UsrAttr +print_theorems + primrec find_usrid::"UsrAttrConf\<Rightarrow>UsrAttr\<Rightarrow>bool" where "find_usrid nousrattrconf attr= False" | "find_usrid (usrattr_conf conf attrx) attr= -(if usrattr_id attrx=usrattr_id attr\<and> - usrattr_id attr\<noteq>nousrid +(if usrattr_id attrx=usrattr_id attr then True else find_usrid conf attr)" @@ -36,25 +37,20 @@ else find_usrid conf attr)" primrec delete_usrattr::"UsrAttrConf\<Rightarrow>UsrAttr\<Rightarrow>UsrAttrConf" where "delete_usrattr nousrattrconf attr=nousrattrconf" | "delete_usrattr (usrattr_conf conf attrx) attr= -(if usrattr_id attrx=usrattr_id attr\<and> - usrattr_id attr\<noteq>nousrid +(if usrattr_id attrx=usrattr_id attr then -conf -else if usrattr_id attrx\<noteq>usrattr_id attr\<and> - usrattr_id attr\<noteq>nousrid +delete_usrattr conf attr +else if usrattr_id attrx\<noteq>usrattr_id attr then usrattr_conf(delete_usrattr conf attr) attrx else usrattr_conf conf attrx)" - primrec get_usrattr::"UsrAttrConf\<Rightarrow>UsrId\<Rightarrow>UsrAttr" where "get_usrattr nousrattrconf uid=nousrattr" | "get_usrattr (usrattr_conf conf attr) uid= -(if usrattr_id attr=uid\<and> - uid\<noteq>nousrid +(if usrattr_id attr=uid then attr -else if usrattr_id attr\<noteq>uid\<and> - uid\<noteq>nousrid +else if usrattr_id attr\<noteq>uid then get_usrattr conf uid else nousrattr)" @@ -62,11 +58,11 @@ else nousrattr)" primrec valid_usrattrconf::"UsrAttrConf\<Rightarrow>bool" where "valid_usrattrconf nousrattrconf=False" | "valid_usrattrconf (usrattr_conf conf attr)= -(if (\<not>find_usrid conf attr)\<and> +(if usrattr_id attr\<noteq>nousrid\<and> conf=nousrattrconf then True -else if conf\<noteq>nousrattrconf\<and> +else if usrattr_id attr\<noteq>nousrid\<and> (\<not>find_usrid conf attr)\<and> valid_usrattrconf conf then @@ -74,7 +70,7 @@ True else False)" primrec rel_subset_usr::"UsrAttrConf\<Rightarrow>UsrAttrConf\<Rightarrow>bool" where -"rel_subset_usr conf1 nousrattrconf=False" | +"rel_subset_usr conf1 nousrattrconf=True" | "rel_subset_usr conf1 (usrattr_conf conf attr)= (if conf=nousrattrconf\<and> find_usrid conf1 attr @@ -117,72 +113,36 @@ next show "\<not>find_usrid nousrattrconf attr" by auto next fix conf - fix attrx fix attr - show "conf = nousrattrconf \<and> - usrattr_id attr \<noteq> nousrid \<and> - usrattr_id attrx = usrattr_id attr \<Longrightarrow> - find_usrid (usrattr_conf conf attrx) attr" by (auto simp:nousrattr_def) -next - fix conf fix attrx - fix attr - show "conf \<noteq> nousrattrconf \<and> - usrattr_id attr \<noteq> nousrid \<and> - usrattr_id attrx = usrattr_id attr \<Longrightarrow> - find_usrid (usrattr_conf conf attrx) attr" by (auto simp:nousrattr_def) -next - fix conf attr attrx - show "find_usrid conf attr \<and> usrattr_id attr = usrattr_id attrx \<Longrightarrow> - find_usrid conf attrx" - proof (induct conf) - case nousrattrconf - then show ?case by auto - next - case (usrattr_conf conf x2) - then show ?case by auto - qed + show "usrattr_id attrx = usrattr_id attr \<Longrightarrow> + find_usrid (usrattr_conf conf attrx) attr" by auto next fix conf fix attrx fix attr - show "conf \<noteq> nousrattrconf \<and> find_usrid conf attr \<Longrightarrow> + show "find_usrid conf attr \<Longrightarrow> find_usrid (usrattr_conf conf attrx) attr" by auto next - fix conf - fix attrx - fix attr - show "\<not> (conf = nousrattrconf \<and> - usrattr_id attr \<noteq> nousrid \<and> - usrattr_id attrx = usrattr_id attr \<or> - conf \<noteq> nousrattrconf \<and> - usrattr_id attr \<noteq> nousrid \<and> - usrattr_id attrx = usrattr_id attr \<or> - conf \<noteq> nousrattrconf \<and> find_usrid conf attr) \<Longrightarrow> - \<not> find_usrid (usrattr_conf conf attrx) attr" by (auto simp:nousrid_def) + fix conf attr attrx + show "\<not> find_usrid conf attr \<and> + usrattr_id attrx \<noteq> usrattr_id attr \<Longrightarrow> + \<not> find_usrid (usrattr_conf conf attrx) attr" by auto next fix attr show "delete_usrattr nousrattrconf attr = nousrattrconf" by auto next - fix attrx - fix attr fix conf - show "usrattr_id attrx = usrattr_id attr \<and> - usrattr_id attr \<noteq> nousrid \<Longrightarrow> - delete_usrattr (usrattr_conf conf attrx) attr = conf" by auto -next fix attrx fix attr - fix conf - show "usrattr_id attr = nousrid \<Longrightarrow> + show "usrattr_id attrx = usrattr_id attr \<Longrightarrow> delete_usrattr (usrattr_conf conf attrx) attr = - usrattr_conf conf attrx" by auto + delete_usrattr conf attr" by auto next fix attrx fix attr fix conf - show "usrattr_id attrx \<noteq> usrattr_id attr \<and> - usrattr_id attr \<noteq> nousrid \<Longrightarrow> + show "usrattr_id attrx \<noteq> usrattr_id attr \<Longrightarrow> delete_usrattr (usrattr_conf conf attrx) attr = usrattr_conf (delete_usrattr conf attr) attrx" by auto next @@ -192,41 +152,60 @@ next fix attr fix elem fix conf - show "elem \<noteq> nousrid \<and> usrattr_id attr = elem \<Longrightarrow> + show "usrattr_id attr = elem \<Longrightarrow> get_usrattr (usrattr_conf conf attr) elem = attr" by auto next - fix attr fix elem + fix attr fix conf - show "elem = nousrid \<Longrightarrow> + show "get_usrattr conf elem = nousrattr \<and> + usrattr_id attr \<noteq> elem \<Longrightarrow> get_usrattr (usrattr_conf conf attr) elem = nousrattr" by auto next + fix conf fix elem fix attr - fix conf - show "elem \<noteq> nousrid \<and> usrattr_id attr \<noteq> elem \<Longrightarrow> - get_usrattr (usrattr_conf conf attr) elem = - get_usrattr conf elem" by auto + show "get_usrattr conf elem \<noteq> nousrattr \<and> + usrattr_id attr \<noteq> elem \<Longrightarrow> + get_usrattr (usrattr_conf conf attr) elem = get_usrattr conf elem" by auto next show "\<not> valid_usrattrconf nousrattrconf" by auto next fix conf fix attr - show "conf = nousrattrconf \<and> \<not> find_usrid conf attr \<Longrightarrow> + show "usrattr_id attr \<noteq> nousrid \<and> conf = nousrattrconf \<Longrightarrow> valid_usrattrconf (usrattr_conf conf attr)" by auto next fix conf fix attr - show "conf \<noteq> nousrattrconf \<and> - \<not> find_usrid conf attr \<and> valid_usrattrconf conf \<Longrightarrow> + show "valid_usrattrconf conf \<and> + \<not> find_usrid conf attr \<and> usrattr_id attr \<noteq> nousrid \<Longrightarrow> valid_usrattrconf (usrattr_conf conf attr)" by auto next fix conf fix attr - show "\<not> (conf = nousrattrconf \<and> \<not> find_usrid conf attr \<or> - conf \<noteq> nousrattrconf \<and> - \<not> find_usrid conf attr \<and> valid_usrattrconf conf) \<Longrightarrow> + show "usrattr_id attr = nousrid \<Longrightarrow> + \<not> valid_usrattrconf (usrattr_conf conf attr)" by auto +next + fix conf + fix attr + show "conf \<noteq> nousrattrconf \<and> \<not> valid_usrattrconf conf \<Longrightarrow> \<not> valid_usrattrconf (usrattr_conf conf attr)" by auto +next + fix conf + fix attr + show "conf \<noteq> nousrattrconf \<and> find_usrid conf attr \<Longrightarrow> + \<not> valid_usrattrconf (usrattr_conf conf attr)" by auto +next + show "\<And>P conf. + P nousrattrconf \<Longrightarrow> + (\<And>conf1 attr1. P conf1 \<Longrightarrow> P (usrattr_conf conf1 attr1)) \<Longrightarrow> + P conf" + proof (erule UsrAttrConf.induct) + show "\<And>P conf x1 x2. + (\<And>conf1 attr1. P conf1 \<Longrightarrow> P (usrattr_conf conf1 attr1)) \<Longrightarrow> + P x1 \<Longrightarrow> P (usrattr_conf x1 x2)" by auto + qed qed interpretation UsrAttrConfRel : AttrConfRel nousrid nousrattr nousrattrconf usrattr_conf is_usrattrconf @@ -234,7 +213,7 @@ interpretation UsrAttrConfRel : AttrConfRel nousrid nousrattr nousrattrconf usra rel_subset_usr proof fix confx - show "\<not> rel_subset_usr confx nousrattrconf" by auto + show "rel_subset_usr confx nousrattrconf" by auto next fix conf fix confx @@ -252,128 +231,14 @@ next fix conf fix confx fix attr - show "\<not> (conf \<noteq> nousrattrconf \<and> - find_usrid confx attr \<and> rel_subset_usr confx conf \<or> - conf = nousrattrconf \<and> find_usrid confx attr) \<Longrightarrow> + show "\<not> rel_subset_usr confx conf \<Longrightarrow> \<not> rel_subset_usr confx (usrattr_conf conf attr)" by auto next - fix confx conf attr - show "rel_subset_usr confx conf \<and> find_usrid conf attr \<Longrightarrow> - find_usrid confx attr" - proof (induct conf) - case nousrattrconf - then show ?case by auto - next - case (usrattr_conf conf x2) - then show ?case - proof (auto) - show "(rel_subset_usr confx conf \<and> find_usrid conf attr \<Longrightarrow> - find_usrid confx attr) \<Longrightarrow> - if conf = nousrattrconf \<and> find_usrid confx x2 then True - else if conf \<noteq> nousrattrconf \<and> find_usrid confx x2 - then rel_subset_usr confx conf else False \<Longrightarrow> - if usrattr_id x2 = usrattr_id attr \<and> usrattr_id attr \<noteq> nousrid - then True else find_usrid conf attr \<Longrightarrow> - find_usrid confx attr" - proof (split if_split_asm) - show "if usrattr_id x2 = usrattr_id attr \<and> usrattr_id attr \<noteq> nousrid - then True else find_usrid conf attr \<Longrightarrow> - (rel_subset_usr confx conf \<and> find_usrid conf attr \<Longrightarrow> - find_usrid confx attr) \<Longrightarrow> - conf = nousrattrconf \<Longrightarrow> - find_usrid confx x2 \<Longrightarrow> True \<Longrightarrow> find_usrid confx attr" - proof (split if_split_asm) - assume 0:"find_usrid confx x2" - assume 1:"usrattr_id x2 = usrattr_id attr" - from 0 1 show "find_usrid confx attr" - proof (induct confx) - case nousrattrconf - then show ?case by auto - next - case (usrattr_conf confx x2) - then show ?case by auto - qed - next - show "(rel_subset_usr confx conf \<and> find_usrid conf attr \<Longrightarrow> - find_usrid confx attr) \<Longrightarrow> - conf = nousrattrconf \<Longrightarrow> - find_usrid confx x2 \<Longrightarrow> - True \<Longrightarrow> - \<not> (usrattr_id x2 = usrattr_id attr \<and> - usrattr_id attr \<noteq> nousrid) \<Longrightarrow> - find_usrid conf attr \<Longrightarrow> find_usrid confx attr " by auto - qed - next - show "if usrattr_id x2 = usrattr_id attr \<and> usrattr_id attr \<noteq> nousrid - then True else find_usrid conf attr \<Longrightarrow> - (rel_subset_usr confx conf \<and> find_usrid conf attr \<Longrightarrow> - find_usrid confx attr) \<Longrightarrow> - \<not> (conf = nousrattrconf \<and> find_usrid confx x2) \<Longrightarrow> - if conf \<noteq> nousrattrconf \<and> find_usrid confx x2 - then rel_subset_usr confx conf else False \<Longrightarrow> - find_usrid confx attr" - proof (split if_split_asm) - show "(rel_subset_usr confx conf \<and> find_usrid conf attr \<Longrightarrow> - find_usrid confx attr) \<Longrightarrow> - \<not> (conf = nousrattrconf \<and> find_usrid confx x2) \<Longrightarrow> - if conf \<noteq> nousrattrconf \<and> find_usrid confx x2 - then rel_subset_usr confx conf else False \<Longrightarrow> - usrattr_id x2 = usrattr_id attr \<Longrightarrow> - usrattr_id attr \<noteq> nousrid \<Longrightarrow> True \<Longrightarrow> find_usrid confx attr" - proof (split if_split_asm) - show "usrattr_id x2 = usrattr_id attr \<Longrightarrow> - usrattr_id attr \<noteq> nousrid \<Longrightarrow> - True \<Longrightarrow> - (rel_subset_usr confx conf \<and> find_usrid conf attr \<Longrightarrow> - find_usrid confx attr) \<Longrightarrow> - \<not> (conf = nousrattrconf \<and> find_usrid confx x2) \<Longrightarrow> - \<not> (conf \<noteq> nousrattrconf \<and> find_usrid confx x2) \<Longrightarrow> - False \<Longrightarrow> find_usrid confx attr" by auto - next - assume 0:"find_usrid confx x2" - assume 1:"usrattr_id x2 = usrattr_id attr" - from 0 1 show "find_usrid confx attr" - proof (induct confx) - case nousrattrconf - then show ?case by auto - next - case (usrattr_conf confx x2) - then show ?case by auto - qed - qed - next - show "(rel_subset_usr confx conf \<and> find_usrid conf attr \<Longrightarrow> - find_usrid confx attr) \<Longrightarrow> - \<not> (conf = nousrattrconf \<and> find_usrid confx x2) \<Longrightarrow> - if conf \<noteq> nousrattrconf \<and> find_usrid confx x2 - then rel_subset_usr confx conf else False \<Longrightarrow> - \<not> (usrattr_id x2 = usrattr_id attr \<and> - usrattr_id attr \<noteq> nousrid) \<Longrightarrow> - find_usrid conf attr \<Longrightarrow> find_usrid confx attr" - proof (split if_split_asm) - show " \<not> (usrattr_id x2 = usrattr_id attr \<and> - usrattr_id attr \<noteq> nousrid) \<Longrightarrow> - find_usrid conf attr \<Longrightarrow> - (rel_subset_usr confx conf \<and> find_usrid conf attr \<Longrightarrow> - find_usrid confx attr) \<Longrightarrow> - \<not> (conf = nousrattrconf \<and> find_usrid confx x2) \<Longrightarrow> - conf \<noteq> nousrattrconf \<Longrightarrow> - find_usrid confx x2 \<Longrightarrow> - rel_subset_usr confx conf \<Longrightarrow> find_usrid confx attr" by auto - next - show "\<not> (usrattr_id x2 = usrattr_id attr \<and> - usrattr_id attr \<noteq> nousrid) \<Longrightarrow> - find_usrid conf attr \<Longrightarrow> - (rel_subset_usr confx conf \<and> find_usrid conf attr \<Longrightarrow> - find_usrid confx attr) \<Longrightarrow> - \<not> (conf = nousrattrconf \<and> find_usrid confx x2) \<Longrightarrow> - \<not> (conf \<noteq> nousrattrconf \<and> find_usrid confx x2) \<Longrightarrow> - False \<Longrightarrow> find_usrid confx attr" by auto - qed - qed - qed - qed - qed + fix confx + fix conf + fix attr + show "rel_subset_usr confx conf \<and> \<not> find_usrid confx attr \<Longrightarrow> + \<not> rel_subset_usr confx (usrattr_conf conf attr)" by auto qed end diff --git a/access_control_module/interpretation/I_FMT_MSA.thy b/access_control_module/interpretation/I_FMT_MSA.thy index 480fbca..2d92a2b 100644 --- a/access_control_module/interpretation/I_FMT_MSA.thy +++ b/access_control_module/interpretation/I_FMT_MSA.thy @@ -30,8 +30,7 @@ definition subjattr_subjid::"SubjAttr\<Rightarrow>ResrcId" where primrec find_subjid::"SubjAttrConf\<Rightarrow>SubjAttr\<Rightarrow>bool" where "find_subjid nosubjattrconf sattr=False" | "find_subjid (subjattr_conf conf sattrx) sattr= -(if subjattr_subjid sattrx=subjattr_subjid sattr\<and> - subjattr_subjid sattr\<noteq>noresrcid +(if subjattr_subjid sattrx=subjattr_subjid sattr then True else find_subjid conf sattr)" @@ -39,12 +38,10 @@ else find_subjid conf sattr)" primrec delete_subjattr::"SubjAttrConf\<Rightarrow>SubjAttr\<Rightarrow>SubjAttrConf" where "delete_subjattr nosubjattrconf sattr=nosubjattrconf" | "delete_subjattr (subjattr_conf conf sattrx) sattr= -(if subjattr_subjid sattrx=subjattr_subjid sattr\<and> - subjattr_subjid sattr\<noteq>noresrcid +(if subjattr_subjid sattrx=subjattr_subjid sattr then -conf -else if subjattr_subjid sattrx\<noteq>subjattr_subjid sattr\<and> - subjattr_subjid sattr\<noteq>noresrcid +delete_subjattr conf sattr +else if subjattr_subjid sattrx\<noteq>subjattr_subjid sattr then subjattr_conf(delete_subjattr conf sattr) sattrx else subjattr_conf conf sattrx)" @@ -52,12 +49,10 @@ else subjattr_conf conf sattrx)" primrec get_subjattr::"SubjAttrConf\<Rightarrow>ResrcId\<Rightarrow>SubjAttr" where "get_subjattr nosubjattrconf rid=nosubjattr" | "get_subjattr (subjattr_conf conf sattr) rid= -(if subjattr_subjid sattr=rid\<and> - rid\<noteq>noresrcid +(if subjattr_subjid sattr=rid then sattr -else if subjattr_subjid sattr\<noteq>rid\<and> - rid\<noteq>noresrcid +else if subjattr_subjid sattr\<noteq>rid then get_subjattr conf rid else nosubjattr)" @@ -65,11 +60,11 @@ else nosubjattr)" primrec subjattrconf_uniq::"SubjAttrConf\<Rightarrow>bool" where "subjattrconf_uniq nosubjattrconf=False" | "subjattrconf_uniq (subjattr_conf conf sattr)= -(if (\<not>find_subjid conf sattr)\<and> +(if subjattr_subjid sattr\<noteq>noresrcid\<and> conf=nosubjattrconf then True -else if conf\<noteq>nosubjattrconf\<and> +else if subjattr_subjid sattr\<noteq>noresrcid\<and> (\<not>find_subjid conf sattr)\<and> subjattrconf_uniq conf then @@ -126,56 +121,30 @@ next (\<exists>conf attr. x = subjattr_conf conf attr)" by auto qed next - fix attr - show "\<not> find_subjid nosubjattrconf attr" by auto -next show "subjattr_subjid nosubjattr = noresrcid" - by (auto simp:subjattr_subjid_def nosubjattr_def noresrcattr_def) + by (auto simp add:subjattr_subjid_def nosubjattr_def noresrcattr_def) next - fix conf - fix attrx fix attr - show "conf = nosubjattrconf \<and> - subjattr_subjid attr \<noteq> noresrcid \<and> - subjattr_subjid attrx = subjattr_subjid attr \<Longrightarrow> - find_subjid (subjattr_conf conf attrx) attr" by auto + show "\<not> find_subjid nosubjattrconf attr" by auto next - fix conf fix attrx fix attr - show "conf \<noteq> nosubjattrconf \<and> - subjattr_subjid attr \<noteq> noresrcid \<and> - subjattr_subjid attrx = subjattr_subjid attr \<Longrightarrow> - find_subjid (subjattr_conf conf attrx) attr" by auto + fix conf + show "subjattr_subjid attrx = subjattr_subjid attr \<Longrightarrow> + find_subjid (subjattr_conf conf attrx) attr" + by auto next fix conf fix attrx fix attr - show "conf \<noteq> nosubjattrconf \<and> find_subjid conf attr \<Longrightarrow> + show "find_subjid conf attr \<Longrightarrow> find_subjid (subjattr_conf conf attrx) attr" by auto next - fix conf attr attrx - show "find_subjid conf attr \<and> - subjattr_subjid attr = subjattr_subjid attrx \<Longrightarrow> - find_subjid conf attrx" - proof (induct conf) - case nosubjattrconf - then show ?case by auto - next - case (subjattr_conf conf x2) - then show ?case by auto - qed -next fix conf fix attrx fix attr - show "\<not> (conf = nosubjattrconf \<and> - subjattr_subjid attr \<noteq> noresrcid \<and> - subjattr_subjid attrx = subjattr_subjid attr \<or> - conf \<noteq> nosubjattrconf \<and> - subjattr_subjid attr \<noteq> noresrcid \<and> - subjattr_subjid attrx = subjattr_subjid attr \<or> - conf \<noteq> nosubjattrconf \<and> find_subjid conf attr) \<Longrightarrow> + show "\<not> find_subjid conf attr \<and> + subjattr_subjid attrx \<noteq> subjattr_subjid attr \<Longrightarrow> \<not> find_subjid (subjattr_conf conf attrx) attr" by auto next fix attr @@ -184,22 +153,14 @@ next fix attrx fix attr fix conf - show "subjattr_subjid attrx = subjattr_subjid attr \<and> - subjattr_subjid attr \<noteq> noresrcid \<Longrightarrow> - delete_subjattr (subjattr_conf conf attrx) attr = conf" by auto -next - fix attrx - fix attr - fix conf - show "subjattr_subjid attr = noresrcid \<Longrightarrow> + show "subjattr_subjid attrx = subjattr_subjid attr \<Longrightarrow> delete_subjattr (subjattr_conf conf attrx) attr = - subjattr_conf conf attrx" by auto + delete_subjattr conf attr" by auto next fix attrx fix attr fix conf - show "subjattr_subjid attrx \<noteq> subjattr_subjid attr \<and> - subjattr_subjid attr \<noteq> noresrcid \<Longrightarrow> + show "subjattr_subjid attrx \<noteq> subjattr_subjid attr \<Longrightarrow> delete_subjattr (subjattr_conf conf attrx) attr = subjattr_conf (delete_subjattr conf attr) attrx" by auto next @@ -209,19 +170,21 @@ next fix attr fix elem fix conf - show "elem \<noteq> noresrcid \<and> subjattr_subjid attr = elem \<Longrightarrow> + show "subjattr_subjid attr = elem \<Longrightarrow> get_subjattr (subjattr_conf conf attr) elem = attr" by auto next fix attr fix elem fix conf - show "elem = noresrcid \<Longrightarrow> + show "get_subjattr conf elem = nosubjattr \<and> + subjattr_subjid attr \<noteq> elem \<Longrightarrow> get_subjattr (subjattr_conf conf attr) elem = nosubjattr" by auto next fix elem fix attr fix conf - show "elem \<noteq> noresrcid \<and> subjattr_subjid attr \<noteq> elem \<Longrightarrow> + show "get_subjattr conf elem \<noteq> nosubjattr \<and> + subjattr_subjid attr \<noteq> elem \<Longrightarrow> get_subjattr (subjattr_conf conf attr) elem = get_subjattr conf elem" by auto next @@ -229,22 +192,40 @@ next next fix conf fix attr - show "conf = nosubjattrconf \<and> \<not> find_subjid conf attr \<Longrightarrow> + show "subjattr_subjid attr \<noteq> noresrcid \<and> conf = nosubjattrconf \<Longrightarrow> subjattrconf_uniq (subjattr_conf conf attr)" by auto next fix conf fix attr - show "conf \<noteq> nosubjattrconf \<and> - \<not> find_subjid conf attr \<and> subjattrconf_uniq conf \<Longrightarrow> + show "subjattrconf_uniq conf \<and> + \<not> find_subjid conf attr \<and> subjattr_subjid attr \<noteq> noresrcid \<Longrightarrow> subjattrconf_uniq (subjattr_conf conf attr)" by auto next fix conf fix attr - show "\<not> (conf = nosubjattrconf \<and> \<not> find_subjid conf attr \<or> - conf \<noteq> nosubjattrconf \<and> - \<not> find_subjid conf attr \<and> subjattrconf_uniq conf) \<Longrightarrow> + show "subjattr_subjid attr = noresrcid \<Longrightarrow> + \<not> subjattrconf_uniq (subjattr_conf conf attr)" by auto +next + fix conf + fix attr + show "conf \<noteq> nosubjattrconf \<and> \<not> subjattrconf_uniq conf \<Longrightarrow> + \<not> subjattrconf_uniq (subjattr_conf conf attr)" by auto +next + fix conf + fix attr + show "conf \<noteq> nosubjattrconf \<and> find_subjid conf attr \<Longrightarrow> \<not> subjattrconf_uniq (subjattr_conf conf attr)" by auto next + show "\<And>P conf. + P nosubjattrconf \<Longrightarrow> + (\<And>conf1 attr1. P conf1 \<Longrightarrow> P (subjattr_conf conf1 attr1)) \<Longrightarrow> + P conf" + proof (erule SubjAttrConf.induct) + show "\<And>P conf x1 x2. + (\<And>conf1 attr1. P conf1 \<Longrightarrow> P (subjattr_conf conf1 attr1)) \<Longrightarrow> + P x1 \<Longrightarrow> P (subjattr_conf x1 x2)" by auto + qed +next fix sattr show "subjattr_subjid sattr = presrc_id (subj_resrcattr sattr)" by (auto simp:subjattr_subjid_def) @@ -319,8 +300,7 @@ definition objattr_objid::"ObjAttr\<Rightarrow>ResrcId" where primrec find_objid::"ObjAttrConf\<Rightarrow>ObjAttr\<Rightarrow>bool" where "find_objid noobjattrconf oattr=False" | "find_objid (objattr_conf conf oattrx) oattr= -(if objattr_objid oattrx=objattr_objid oattr \<and> - objattr_objid oattr\<noteq>noresrcid +(if objattr_objid oattrx=objattr_objid oattr then True else find_objid conf oattr)" @@ -328,12 +308,10 @@ else find_objid conf oattr)" primrec delete_objattr::"ObjAttrConf\<Rightarrow>ObjAttr\<Rightarrow>ObjAttrConf" where "delete_objattr noobjattrconf oattr=noobjattrconf" | "delete_objattr (objattr_conf conf oattrx) oattr= -(if objattr_objid oattrx=objattr_objid oattr \<and> - objattr_objid oattr\<noteq>noresrcid +(if objattr_objid oattrx=objattr_objid oattr then -conf -else if objattr_objid oattrx\<noteq>objattr_objid oattr \<and> - objattr_objid oattr\<noteq>noresrcid +delete_objattr conf oattr +else if objattr_objid oattrx\<noteq>objattr_objid oattr then objattr_conf(delete_objattr conf oattr) oattrx else objattr_conf conf oattrx)" @@ -341,12 +319,10 @@ else objattr_conf conf oattrx)" primrec get_objattr::"ObjAttrConf\<Rightarrow>ResrcId\<Rightarrow>ObjAttr" where "get_objattr noobjattrconf rid=noobjattr" | "get_objattr (objattr_conf conf oattr) rid= -(if objattr_objid oattr=rid \<and> - rid\<noteq>noresrcid +(if objattr_objid oattr=rid then oattr -else if objattr_objid oattr\<noteq>rid \<and> - rid\<noteq>noresrcid +else if objattr_objid oattr\<noteq>rid then get_objattr conf rid else noobjattr)" @@ -354,11 +330,11 @@ else noobjattr)" primrec valid_objattrconf::"ObjAttrConf\<Rightarrow>bool" where "valid_objattrconf noobjattrconf=False" | "valid_objattrconf (objattr_conf conf oattr)= -(if (\<not>find_objid conf oattr)\<and> +(if objattr_objid oattr\<noteq>noresrcid\<and> conf=noobjattrconf then True -else if conf\<noteq>noobjattrconf\<and> +else if objattr_objid oattr\<noteq>noresrcid\<and> (\<not>find_objid conf oattr)\<and> valid_objattrconf conf then @@ -405,47 +381,19 @@ next fix conf fix attrx fix attr - show "conf = noobjattrconf \<and> - objattr_objid attr \<noteq> noresrcid \<and> - objattr_objid attrx = objattr_objid attr \<Longrightarrow> - find_objid (objattr_conf conf attrx) attr" by auto -next - fix conf - fix attrx - fix attr - show "conf \<noteq> noobjattrconf \<and> - objattr_objid attr \<noteq> noresrcid \<and> - objattr_objid attrx = objattr_objid attr \<Longrightarrow> + show "objattr_objid attrx = objattr_objid attr \<Longrightarrow> find_objid (objattr_conf conf attrx) attr" by auto next fix conf fix attrx fix attr - show "conf \<noteq> noobjattrconf \<and> find_objid conf attr \<Longrightarrow> - find_objid (objattr_conf conf attrx) attr" by auto -next - fix conf attr attrx - show "find_objid conf attr \<and> - objattr_objid attr = objattr_objid attrx \<Longrightarrow> - find_objid conf attrx" - proof (induct conf) - case noobjattrconf - then show ?case by auto - next - case (objattr_conf conf x2) - then show ?case by auto - qed + show "find_objid conf attr \<Longrightarrow> find_objid (objattr_conf conf attrx) attr" by auto next fix conf fix attrx fix attr - show "\<not> (conf = noobjattrconf \<and> - objattr_objid attr \<noteq> noresrcid \<and> - objattr_objid attrx = objattr_objid attr \<or> - conf \<noteq> noobjattrconf \<and> - objattr_objid attr \<noteq> noresrcid \<and> - objattr_objid attrx = objattr_objid attr \<or> - conf \<noteq> noobjattrconf \<and> find_objid conf attr) \<Longrightarrow> + show "\<not> find_objid conf attr \<and> + objattr_objid attrx \<noteq> objattr_objid attr \<Longrightarrow> \<not> find_objid (objattr_conf conf attrx) attr" by auto next fix attr @@ -454,22 +402,14 @@ next fix attrx fix attr fix conf - show "objattr_objid attrx = objattr_objid attr \<and> - objattr_objid attr \<noteq> noresrcid \<Longrightarrow> - delete_objattr (objattr_conf conf attrx) attr = conf" by auto -next - fix attrx - fix attr - fix conf - show "objattr_objid attr = noresrcid \<Longrightarrow> + show "objattr_objid attrx = objattr_objid attr \<Longrightarrow> delete_objattr (objattr_conf conf attrx) attr = - objattr_conf conf attrx" by auto + delete_objattr conf attr" by auto next fix attrx fix attr fix conf - show "objattr_objid attrx \<noteq> objattr_objid attr \<and> - objattr_objid attr \<noteq> noresrcid \<Longrightarrow> + show "objattr_objid attrx \<noteq> objattr_objid attr \<Longrightarrow> delete_objattr (objattr_conf conf attrx) attr = objattr_conf (delete_objattr conf attr) attrx" by auto next @@ -479,42 +419,59 @@ next fix attr fix elem fix conf - show "elem \<noteq> noresrcid \<and> objattr_objid attr = elem \<Longrightarrow> + show "objattr_objid attr = elem \<Longrightarrow> get_objattr (objattr_conf conf attr) elem = attr" by auto next fix attr fix elem fix conf - show "elem = noresrcid \<Longrightarrow> + show "get_objattr conf elem = noobjattr \<and> objattr_objid attr \<noteq> elem \<Longrightarrow> get_objattr (objattr_conf conf attr) elem = noobjattr" by auto next fix elem fix attr fix conf - show "elem \<noteq> noresrcid \<and> objattr_objid attr \<noteq> elem \<Longrightarrow> - get_objattr (objattr_conf conf attr) elem = - get_objattr conf elem" by auto + show "get_objattr conf elem \<noteq> noobjattr \<and> objattr_objid attr \<noteq> elem \<Longrightarrow> + get_objattr (objattr_conf conf attr) elem = get_objattr conf elem" by auto next show "\<not> valid_objattrconf noobjattrconf" by auto next fix conf fix attr - show "conf = noobjattrconf \<and> \<not> find_objid conf attr \<Longrightarrow> + show "objattr_objid attr \<noteq> noresrcid \<and> conf = noobjattrconf \<Longrightarrow> valid_objattrconf (objattr_conf conf attr)" by auto next fix conf fix attr - show "conf \<noteq> noobjattrconf \<and> - \<not> find_objid conf attr \<and> valid_objattrconf conf \<Longrightarrow> + show "valid_objattrconf conf \<and> + \<not> find_objid conf attr \<and> objattr_objid attr \<noteq> noresrcid \<Longrightarrow> valid_objattrconf (objattr_conf conf attr)" by auto next fix conf fix attr - show "\<not> (conf = noobjattrconf \<and> \<not> find_objid conf attr \<or> - conf \<noteq> noobjattrconf \<and> - \<not> find_objid conf attr \<and> valid_objattrconf conf) \<Longrightarrow> + show "objattr_objid attr = noresrcid \<Longrightarrow> + \<not> valid_objattrconf (objattr_conf conf attr)" by auto +next + fix conf + fix attr + show "conf \<noteq> noobjattrconf \<and> \<not> valid_objattrconf conf \<Longrightarrow> \<not> valid_objattrconf (objattr_conf conf attr)" by auto next + fix conf + fix attr + show "conf \<noteq> noobjattrconf \<and> find_objid conf attr \<Longrightarrow> + \<not> valid_objattrconf (objattr_conf conf attr)" by auto +next + show "\<And>P conf. + P noobjattrconf \<Longrightarrow> + (\<And>conf1 attr1. P conf1 \<Longrightarrow> P (objattr_conf conf1 attr1)) \<Longrightarrow> + P conf" + proof (erule ObjAttrConf.induct) + show "\<And>P conf x1 x2. + (\<And>conf1 attr1. P conf1 \<Longrightarrow> P (objattr_conf conf1 attr1)) \<Longrightarrow> + P x1 \<Longrightarrow> P (objattr_conf x1 x2)" by auto + qed +next fix oattr show "objattr_objid oattr = presrc_id (obj_resrcattr oattr)" by (auto simp:objattr_objid_def) --------------------------------------------------------------------- To unsubscribe, e-mail: [email protected] For additional commands, e-mail: [email protected]
