| (* |
| * Licensed to the Apache Software Foundation (ASF) under one |
| * or more contributor license agreements. See the NOTICE file |
| * distributed with this work for additional information |
| * regarding copyright ownership. The ASF licenses this file |
| * to you under the Apache License, Version 2.0 (the |
| * "License"); you may not use this file except in compliance |
| * with the License. You may obtain a copy of the License at |
| * |
| * http://www.apache.org/licenses/LICENSE-2.0 |
| * |
| * Unless required by applicable law or agreed to in writing, |
| * software distributed under the License is distributed on an |
| * "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY |
| * KIND, either express or implied. See the License for the |
| * specific language governing permissions and limitations |
| * under the License. |
| *) |
| |
| theory AttrConf |
| imports Main |
| begin |
| |
| locale AttrConf= |
| fixes noelem::'element |
| and noattr::'attr |
| and noattrconf::"'attrconf" |
| and attr_conf::"'attrconf\<Rightarrow>'attr\<Rightarrow>'attrconf" |
| and is_attrconf::"'attrconf\<Rightarrow>bool" |
| and attr_elem::"'attr\<Rightarrow>'element" |
| and find_elem::"'attrconf\<Rightarrow>'attr\<Rightarrow>bool" |
| and delete_attr::"'attrconf\<Rightarrow>'attr\<Rightarrow>'attrconf" |
| and get_attr::"'attrconf\<Rightarrow>'element\<Rightarrow>'attr" |
| and valid_attrconf::"'attrconf\<Rightarrow>bool" |
| assumes ATTRCONFHLR1:"\<not>is_attrconf noattrconf" |
| 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 ATTRCONFHLR6:"\<not>find_elem noattrconf attr" |
| assumes ATTRCONFHLR7:"attr_elem attrx=attr_elem attr\<Longrightarrow> |
| find_elem(attr_conf conf attrx) attr" |
| assumes ATTRCONFHLR8:"find_elem conf attr\<Longrightarrow> |
| find_elem(attr_conf conf attrx) attr" |
| 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 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 ATTRCONFHLR13:"get_attr noattrconf elem=noattr" |
| assumes ATTRCONFHLR14:"attr_elem attr=elem\<Longrightarrow> |
| get_attr(attr_conf conf attr) elem=attr" |
| assumes ATTRCONFHLR16:"attr_elem attr\<noteq>elem\<Longrightarrow> |
| get_attr(attr_conf conf attr) elem=get_attr conf elem" |
| assumes ATTRCONFHLR17:"\<not>valid_attrconf noattrconf" |
| assumes ATTRCONFHLR18:"attr_elem attr\<noteq>noelem\<and> |
| conf=noattrconf\<Longrightarrow> |
| valid_attrconf(attr_conf conf attr)" |
| 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 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 find_inverse: |
| "find_elem(attr_conf conf attrx) attr\<Longrightarrow>find_elem conf attr\<or> |
| attr_elem attrx=attr_elem attr" |
| proof - |
| assume "find_elem(attr_conf conf attrx) attr" |
| from this show "find_elem conf attr\<or> |
| attr_elem attrx=attr_elem attr" |
| proof (rule contrapos_pp) |
| assume "\<not> (find_elem conf attr \<or> attr_elem attrx = attr_elem attr)" |
| from this have "(\<not>find_elem conf attr)\<and>attr_elem attrx\<noteq>attr_elem attr" |
| by (auto simp:find_dual) |
| from this show "\<not> find_elem (attr_conf conf attrx) attr" |
| by (auto simp:ATTRCONFHLR9) |
| qed |
| qed |
| |
| lemma not_find_inverse: |
| "\<not>find_elem(attr_conf conf attrx) attr\<Longrightarrow>(\<not>find_elem conf attr)\<and> |
| attr_elem attrx\<noteq>attr_elem attr" |
| proof - |
| assume "\<not>find_elem(attr_conf conf attrx) attr" |
| from this show "(\<not>find_elem conf attr)\<and> |
| attr_elem attrx\<noteq>attr_elem attr" |
| proof (rule contrapos_pp) |
| assume "\<not> (\<not> find_elem conf attr \<and> attr_elem attrx \<noteq> attr_elem attr)" |
| from this have "find_elem conf attr\<or> |
| attr_elem attrx=attr_elem attr" by auto |
| from this show "\<not> \<not> find_elem (attr_conf conf attrx) attr" |
| by (auto simp:find_total) |
| qed |
| qed |
| |
| 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 valid_inverse: |
| "valid_attrconf(attr_conf conf attr)\<Longrightarrow>(attr_elem attr\<noteq>noelem\<and> |
| conf=noattrconf)\<or> |
| (valid_attrconf conf\<and> |
| (\<not>find_elem conf attr)\<and> |
| attr_elem attr\<noteq>noelem)" |
| proof - |
| assume "valid_attrconf(attr_conf conf attr)" |
| from this show "(attr_elem attr\<noteq>noelem\<and> |
| conf=noattrconf)\<or> |
| (valid_attrconf conf\<and> |
| (\<not>find_elem conf attr)\<and> |
| attr_elem attr\<noteq>noelem)" |
| proof (rule contrapos_pp) |
| assume "\<not> (attr_elem attr \<noteq> noelem \<and> conf = noattrconf \<or> |
| valid_attrconf conf \<and> |
| \<not> find_elem conf attr \<and> attr_elem attr \<noteq> noelem)" |
| from this have "attr_elem attr=noelem\<or> |
| ((\<not>valid_attrconf conf)\<and>conf\<noteq>noattrconf)\<or> |
| (conf\<noteq>noattrconf\<and>find_elem conf attr)" |
| by (auto simp:valid_dual) |
| from this show "\<not> valid_attrconf (attr_conf conf attr)" |
| by (auto simp:not_valid_total) |
| qed |
| qed |
| |
| lemma not_valid_inverse: |
| "\<not>valid_attrconf(attr_conf conf attr)\<Longrightarrow>attr_elem attr=noelem\<or> |
| ((\<not>valid_attrconf conf)\<and> |
| conf\<noteq>noattrconf)\<or> |
| (conf\<noteq>noattrconf\<and> |
| find_elem conf attr)" |
| proof - |
| assume "\<not>valid_attrconf(attr_conf conf attr)" |
| from this show "attr_elem attr=noelem\<or> |
| ((\<not>valid_attrconf conf)\<and> |
| conf\<noteq>noattrconf)\<or> |
| (conf\<noteq>noattrconf\<and> |
| find_elem conf attr)" |
| proof (rule contrapos_pp) |
| assume "\<not> (attr_elem attr = noelem \<or> |
| \<not> valid_attrconf conf \<and> conf \<noteq> noattrconf \<or> |
| conf \<noteq> noattrconf \<and> find_elem conf attr)" |
| from this have "(attr_elem attr\<noteq>noelem\<and>conf=noattrconf)\<or> |
| (valid_attrconf conf\<and>(\<not>find_elem conf attr)\<and>attr_elem attr\<noteq>noelem)" |
| by auto |
| from this show "\<not> \<not> valid_attrconf (attr_conf conf attr)" |
| by (auto simp:valid_total) |
| qed |
| qed |
| |
| lemma ATTRCONFHLR23:"noattrconf\<noteq>attr_conf conf attr" |
| proof |
| fix conf attr |
| assume 0:"noattrconf=attr_conf conf attr" |
| from ATTRCONFHLR1 have "\<not>is_attrconf(attr_conf conf attr)" by(auto simp: 0) |
| from this show "False" by (auto simp: ATTRCONFHLR2) |
| qed |
| |
| lemma ATTRCONFHLR24:"x\<noteq>noattrconf\<Longrightarrow>\<exists>conf attr. x=attr_conf conf attr" |
| proof - |
| fix x |
| assume 0:"x\<noteq>noattrconf" |
| from ATTRCONFHLR3 0 show "\<exists>sconf oconf. x = attr_conf sconf oconf" by blast |
| qed |
| |
| 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)" by (auto simp:valid_inverse) |
| from 2 have 2:"find_elem conf1 attr\<or> |
| attr_elem attr1=attr_elem attr" by (auto simp:find_inverse) |
| 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" by (auto simp:find_inverse) |
| from 1 2 show "find_elem (attr_conf conf1 attr1) attrx" |
| by (auto simp add:0 ATTRCONFHLR8 ATTRCONFHLR7) |
| qed |
| |
| lemma ATTRCONFHLR27:"find_elem conf attr\<and> |
| \<not>find_elem conf attrx\<Longrightarrow>attr_elem attr\<noteq>attr_elem attrx" |
| proof |
| show "find_elem conf attr \<and> \<not> find_elem conf attrx \<Longrightarrow> |
| attr_elem attr = attr_elem attrx \<Longrightarrow> False" |
| by (auto simp:ATTRCONFHLR26) |
| qed |
| |
| lemma ATTRCONFHLR28:"valid_attrconf conf\<and> |
| find_elem conf attr\<and> |
| attr_elem attr=elem\<Longrightarrow>attr_elem(get_attr conf elem)=elem" |
| proof (induction conf rule:ATTRCONFINDUCT) |
| show "valid_attrconf noattrconf \<and> |
| find_elem noattrconf attr \<and> attr_elem attr = elem \<Longrightarrow> |
| attr_elem (get_attr noattrconf elem) = elem" by (auto simp:ATTRCONFHLR17) |
| next |
| fix conf1 attr1 |
| assume 0:"valid_attrconf conf1 \<and> |
| find_elem conf1 attr \<and> attr_elem attr = elem \<Longrightarrow> |
| attr_elem (get_attr conf1 elem) = elem" |
| assume "valid_attrconf (attr_conf conf1 attr1) \<and> |
| find_elem (attr_conf conf1 attr1) attr \<and> attr_elem attr = elem" |
| from this have 1:"valid_attrconf (attr_conf conf1 attr1)" |
| and 2:"find_elem (attr_conf conf1 attr1) attr" |
| and 3:"attr_elem attr = elem" by auto |
| from 1 have 1:"(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 simp:valid_inverse) |
| from 2 have 2:"find_elem conf1 attr\<or> |
| attr_elem attr1=attr_elem attr" by (auto simp:find_inverse) |
| from 1 2 3 show "attr_elem (get_attr (attr_conf conf1 attr1) elem) = elem" |
| proof - |
| show "attr_elem attr1 \<noteq> noelem \<and> conf1 = noattrconf \<or> |
| valid_attrconf conf1 \<and> |
| \<not> find_elem conf1 attr1 \<and> attr_elem attr1 \<noteq> noelem \<Longrightarrow> |
| find_elem conf1 attr \<or> attr_elem attr1 = attr_elem attr \<Longrightarrow> |
| attr_elem attr = elem \<Longrightarrow> |
| attr_elem (get_attr (attr_conf conf1 attr1) elem) = elem" |
| proof (erule disjE)+ |
| show "attr_elem attr = elem \<Longrightarrow> |
| attr_elem attr1 \<noteq> noelem \<and> conf1 = noattrconf \<Longrightarrow> |
| find_elem conf1 attr \<Longrightarrow> |
| attr_elem (get_attr (attr_conf conf1 attr1) elem) = elem" |
| by (auto simp:ATTRCONFHLR6) |
| next |
| show "attr_elem attr = elem \<Longrightarrow> |
| attr_elem attr1 \<noteq> noelem \<and> conf1 = noattrconf \<Longrightarrow> |
| attr_elem attr1 = attr_elem attr \<Longrightarrow> |
| attr_elem (get_attr (attr_conf conf1 attr1) elem) = elem" |
| by (auto simp:ATTRCONFHLR14) |
| next |
| show "find_elem conf1 attr \<or> attr_elem attr1 = attr_elem attr \<Longrightarrow> |
| attr_elem attr = elem \<Longrightarrow> |
| valid_attrconf conf1 \<and> |
| \<not> find_elem conf1 attr1 \<and> attr_elem attr1 \<noteq> noelem \<Longrightarrow> |
| attr_elem (get_attr (attr_conf conf1 attr1) elem) = elem" |
| proof (erule disjE) |
| show "attr_elem attr = elem \<Longrightarrow> |
| valid_attrconf conf1 \<and> |
| \<not> find_elem conf1 attr1 \<and> attr_elem attr1 \<noteq> noelem \<Longrightarrow> |
| attr_elem attr1 = attr_elem attr \<Longrightarrow> |
| attr_elem (get_attr (attr_conf conf1 attr1) elem) = elem" |
| by (auto simp:ATTRCONFHLR14) |
| next |
| assume 1:"attr_elem attr = elem" |
| assume "valid_attrconf conf1 \<and> |
| \<not> find_elem conf1 attr1 \<and> attr_elem attr1 \<noteq> noelem" |
| from this have 2:"valid_attrconf conf1" |
| and 3:"\<not> find_elem conf1 attr1" |
| and 4:"attr_elem attr1 \<noteq> noelem" by auto |
| assume 5:"find_elem conf1 attr" |
| from 5 3 1 have 6:"elem\<noteq>attr_elem attr1" |
| by (auto simp:ATTRCONFHLR27) |
| from this have 6:"get_attr(attr_conf conf1 attr1) elem=get_attr conf1 elem" |
| by (auto simp:ATTRCONFHLR16) |
| show ?thesis |
| proof (simp add:6) |
| from 2 5 1 show "attr_elem (get_attr conf1 elem) = elem" by (auto simp:0) |
| qed |
| qed |
| qed |
| qed |
| qed |
| |
| lemma ATTRCONFHLR29:"\<not>find_elem conf attr\<Longrightarrow>\<not>find_elem (delete_attr conf attr) attr" |
| proof (induction conf rule:ATTRCONFINDUCT) |
| show "\<not> find_elem noattrconf attr \<Longrightarrow> |
| \<not> find_elem (delete_attr noattrconf attr) attr" |
| by (auto simp add:ATTRCONFHLR10) |
| next |
| fix conf1 attr1 |
| assume 0:"\<not> find_elem conf1 attr \<Longrightarrow> |
| \<not> find_elem (delete_attr conf1 attr) attr" |
| assume 1:"\<not> find_elem (attr_conf conf1 attr1) attr" |
| from this have 1:"(\<not>find_elem conf1 attr)\<and> |
| attr_elem attr1\<noteq>attr_elem attr" by (auto simp:not_find_inverse) |
| from this have 1:"\<not>find_elem conf1 attr" |
| and 2:"attr_elem attr1\<noteq>attr_elem attr" by auto |
| from 2 have 3:"delete_attr(attr_conf conf1 attr1) attr= |
| attr_conf (delete_attr conf1 attr) attr1" by (auto simp:ATTRCONFHLR12) |
| show "\<not> find_elem (delete_attr (attr_conf conf1 attr1) attr) attr" |
| proof (simp add:3;rule ATTRCONFHLR9) |
| from 1 2 show "\<not> find_elem (delete_attr conf1 attr) attr \<and> |
| attr_elem attr1 \<noteq> attr_elem attr" by (auto simp:0) |
| qed |
| qed |
| |
| lemma ATTRCONFHLR30:"\<not>find_elem conf attr\<and> |
| attr_elem attr=attr_elem attrx\<Longrightarrow>\<not>find_elem conf attrx" |
| proof |
| assume "\<not> find_elem conf attr \<and> attr_elem attr = attr_elem attrx" |
| from this have 0:"\<not> find_elem conf attr" |
| and 1:"attr_elem attr = attr_elem attrx" by auto |
| assume "find_elem conf attrx" |
| from this 1 have "find_elem conf attr" by (auto simp:ATTRCONFHLR26) |
| from this 0 show False by auto |
| qed |
| |
| lemma ATTRCONFHLR31:"valid_attrconf conf\<and> |
| find_elem conf attr\<Longrightarrow>\<not>find_elem(delete_attr conf attr) attr" |
| proof (induction conf rule:ATTRCONFINDUCT) |
| show "valid_attrconf noattrconf \<and> find_elem noattrconf attr \<Longrightarrow> |
| \<not> find_elem (delete_attr noattrconf attr) attr" |
| by (auto simp:ATTRCONFHLR17) |
| next |
| fix conf1 |
| fix attr1 |
| assume 0:"valid_attrconf conf1 \<and> find_elem conf1 attr \<Longrightarrow> |
| \<not> find_elem (delete_attr conf1 attr) attr" |
| assume "valid_attrconf (attr_conf conf1 attr1) \<and> |
| find_elem (attr_conf conf1 attr1) attr" |
| from this have 1:"valid_attrconf (attr_conf conf1 attr1)" |
| and 2:"find_elem (attr_conf conf1 attr1) attr" by auto |
| from 1 have 1:"(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 simp:valid_inverse) |
| from 2 have 2:"find_elem conf1 attr\<or> |
| attr_elem attr1=attr_elem attr" by (auto simp:find_inverse) |
| from 1 2 show "\<not> find_elem (delete_attr (attr_conf conf1 attr1) attr) attr" |
| proof - |
| show "attr_elem attr1 \<noteq> noelem \<and> conf1 = noattrconf \<or> |
| valid_attrconf conf1 \<and> |
| \<not> find_elem conf1 attr1 \<and> attr_elem attr1 \<noteq> noelem \<Longrightarrow> |
| find_elem conf1 attr \<or> attr_elem attr1 = attr_elem attr \<Longrightarrow> |
| \<not> find_elem (delete_attr (attr_conf conf1 attr1) attr) attr" |
| proof (erule disjE)+ |
| show "attr_elem attr1 \<noteq> noelem \<and> conf1 = noattrconf \<Longrightarrow> |
| find_elem conf1 attr \<Longrightarrow> |
| \<not> find_elem (delete_attr (attr_conf conf1 attr1) attr) attr" |
| by (auto simp:ATTRCONFHLR6) |
| next |
| assume "attr_elem attr1 \<noteq> noelem \<and> conf1 = noattrconf" |
| from this have 1:"conf1 = noattrconf" by auto |
| assume "attr_elem attr1 = attr_elem attr" |
| from this have 2:"delete_attr(attr_conf conf1 attr1) attr=delete_attr conf1 attr" |
| by (auto simp:ATTRCONFHLR11) |
| show "\<not> find_elem (delete_attr (attr_conf conf1 attr1) attr) attr" |
| proof (auto simp:2) |
| show "find_elem (delete_attr conf1 attr) attr \<Longrightarrow> False" |
| by (auto simp add:1 ATTRCONFHLR10 ATTRCONFHLR6) |
| qed |
| next |
| show "find_elem conf1 attr \<or> attr_elem attr1 = attr_elem attr \<Longrightarrow> |
| valid_attrconf conf1 \<and> |
| \<not> find_elem conf1 attr1 \<and> attr_elem attr1 \<noteq> noelem \<Longrightarrow> |
| \<not> find_elem (delete_attr (attr_conf conf1 attr1) attr) attr" |
| proof (erule disjE)+ |
| assume "valid_attrconf conf1 \<and> |
| \<not> find_elem conf1 attr1 \<and> attr_elem attr1 \<noteq> noelem" |
| from this have 1:"valid_attrconf conf1" |
| and 2:"\<not> find_elem conf1 attr1" |
| and 3:"attr_elem attr1 \<noteq> noelem" by auto |
| assume 4:"find_elem conf1 attr" |
| from 4 2 have 6:"attr_elem attr\<noteq>attr_elem attr1" by (auto simp:ATTRCONFHLR27) |
| from this have 5:"delete_attr(attr_conf conf1 attr1) attr= |
| attr_conf (delete_attr conf1 attr) attr1" |
| by (auto simp:ATTRCONFHLR12) |
| show "\<not> find_elem (delete_attr (attr_conf conf1 attr1) attr) attr" |
| proof (simp add:5;rule ATTRCONFHLR9) |
| from 1 4 6 show "\<not> find_elem (delete_attr conf1 attr) attr \<and> |
| attr_elem attr1 \<noteq> attr_elem attr" |
| by (auto simp:0) |
| qed |
| next |
| assume "valid_attrconf conf1 \<and> |
| \<not> find_elem conf1 attr1 \<and> |
| attr_elem attr1 \<noteq> noelem" |
| from this have 1:"valid_attrconf conf1" |
| and 2:"\<not> find_elem conf1 attr1" |
| and 3:"attr_elem attr1 \<noteq> noelem" by auto |
| assume 4:"attr_elem attr1 = attr_elem attr" |
| from this have 5:"delete_attr(attr_conf conf1 attr1) attr=delete_attr conf1 attr" |
| by (auto simp:ATTRCONFHLR11) |
| show "\<not> find_elem (delete_attr (attr_conf conf1 attr1) attr) attr" |
| proof (simp add:5;rule ATTRCONFHLR29) |
| from 2 4 show "\<not> find_elem conf1 attr" by (auto simp:ATTRCONFHLR30) |
| qed |
| qed |
| qed |
| qed |
| qed |
| |
| end |
| |
| print_locale! AttrConf |
| |
| locale AttrConfRel=AttrConf noelem noattr noattrconf attr_conf is_attrconf attr_elem |
| find_elem delete_attr get_attr valid_attrconf |
| for noelem::'element |
| and noattr::'attr |
| and noattrconf::"'attrconf" |
| and attr_conf::"'attrconf\<Rightarrow>'attr\<Rightarrow>'attrconf" |
| and is_attrconf::"'attrconf\<Rightarrow>bool" |
| and attr_elem::"'attr\<Rightarrow>'element" |
| and find_elem::"'attrconf\<Rightarrow>'attr\<Rightarrow>bool" |
| and delete_attr::"'attrconf\<Rightarrow>'attr\<Rightarrow>'attrconf" |
| and get_attr::"'attrconf\<Rightarrow>'element\<Rightarrow>'attr" |
| and valid_attrconf::"'attrconf\<Rightarrow>bool" + |
| fixes rel_subset::"'attrconf\<Rightarrow>'attrconf\<Rightarrow>bool" |
| assumes ATTRCONFRELHLR1:"rel_subset confx noattrconf" |
| assumes ATTRCONFRELHLR2:"conf=noattrconf\<and> |
| find_elem confx attr\<Longrightarrow> |
| rel_subset confx (attr_conf conf attr)" |
| assumes ATTRCONFRELHLR3:"conf\<noteq>noattrconf\<and> |
| find_elem confx attr\<and> |
| rel_subset confx conf\<Longrightarrow> |
| rel_subset confx (attr_conf conf attr)" |
| assumes ATTRCONFRELHLR4:"\<not>rel_subset confx conf\<Longrightarrow> |
| \<not>rel_subset confx (attr_conf conf 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 |
| |
| locale AttrConfDisj = arg1:AttrConf noelem noattr_arg1 noattrconf_arg1 attr_conf_arg1 is_attrconf_arg1 |
| attr_elem_arg1 find_elem_arg1 delete_attr_arg1 get_attr_arg1 |
| valid_attrconf_arg1 + |
| arg2:AttrConf noelem noattr_arg2 noattrconf_arg2 attr_conf_arg2 is_attrconf_arg2 |
| attr_elem_arg2 find_elem_arg2 delete_attr_arg2 get_attr_arg2 |
| valid_attrconf_arg2 |
| for noelem::'element |
| and noattr_arg1::'attr1 |
| and noattrconf_arg1::"'attrconf1" |
| and attr_conf_arg1::"'attrconf1\<Rightarrow>'attr1\<Rightarrow>'attrconf1" |
| and is_attrconf_arg1::"'attrconf1\<Rightarrow>bool" |
| and attr_elem_arg1::"'attr1\<Rightarrow>'element" |
| and find_elem_arg1::"'attrconf1\<Rightarrow>'attr1\<Rightarrow>bool" |
| and delete_attr_arg1::"'attrconf1\<Rightarrow>'attr1\<Rightarrow>'attrconf1" |
| and get_attr_arg1::"'attrconf1\<Rightarrow>'element\<Rightarrow>'attr1" |
| and valid_attrconf_arg1::"'attrconf1\<Rightarrow>bool" |
| and noattr_arg2::'attr2 |
| and noattrconf_arg2::"'attrconf2" |
| and attr_conf_arg2::"'attrconf2\<Rightarrow>'attr2\<Rightarrow>'attrconf2" |
| and is_attrconf_arg2::"'attrconf2\<Rightarrow>bool" |
| and attr_elem_arg2::"'attr2\<Rightarrow>'element" |
| and find_elem_arg2::"'attrconf2\<Rightarrow>'attr2\<Rightarrow>bool" |
| and delete_attr_arg2::"'attrconf2\<Rightarrow>'attr2\<Rightarrow>'attrconf2" |
| and get_attr_arg2::"'attrconf2\<Rightarrow>'element\<Rightarrow>'attr2" |
| and valid_attrconf_arg2::"'attrconf2\<Rightarrow>bool"+ |
| fixes rel_disjoint::"'attrconf1\<Rightarrow>'attrconf2\<Rightarrow>bool" |
| assumes ATTRCONFDISJHLR1:"rel_disjoint conf1 noattrconf_arg2" |
| assumes ATTRCONFDISJHLR2:"get_attr_arg1 conf1 (attr_elem_arg2 attr2)=noattr_arg1\<and> |
| rel_disjoint conf1 conf2\<Longrightarrow> |
| rel_disjoint conf1 (attr_conf_arg2 conf2 attr2)" |
| assumes ATTRCONFDISJHLR3:"get_attr_arg1 conf1 (attr_elem_arg2 attr2)\<noteq>noattr_arg1\<and> |
| rel_disjoint conf1 conf2\<Longrightarrow> |
| \<not>rel_disjoint conf1 (attr_conf_arg2 conf2 attr2)" |
| assumes ATTRCONFDISJHLR4:"get_attr_arg1 conf1 (attr_elem_arg2 attr2)=noattr_arg1\<and> |
| \<not>rel_disjoint conf1 conf2\<Longrightarrow> |
| \<not>rel_disjoint conf1 (attr_conf_arg2 conf2 attr2)" |
| |
| print_locale! AttrConfDisj |
| |
| end |
