header {* *} theory updates = Main + List: section {* Comments/Markup is not complete yet ... Philipp *} section {* Some Useful Tools *} text {* Cons-operation for an infinite list (a mapping from natural numbers to some arbitrary type). A new value is inserted as head. *} constdefs shiftFun :: "(nat => 'a) => 'a => nat => 'a" "shiftFun f val n == if n=0 then val else f (n-(1::nat))" section {* Syntax *} subsection {* Algebraic Datatypes for Terms, Formulas, Updates *} text {* We use natural numbers for function symbols. For simplicity, a function symbol is uniquely identified with the pair consisting of its number and its arity. This means that the signature (arity) of a symbol is already part of the symbol. *} datatype func = Func nat text {* We define terms, lists of terms, formulas and updates mutually inductive. Variables are identified with natural numbers, and binding variables works following the De Bruijn concept. For some reason, it is not possible to use the lists datatype here (makes problems later when defining the evaluation mapping). Therefore we have our own lists. *} datatype ter = AppVar nat | AppFunc func terList | AppUpdTer update ter | IfThenTer for ter ter | AppUpdNonRec update func terList (* for rewriting *) | AppSubstTer "nat => ter" ter (* for rewriting *) | MinTer for (* for rewriting *) and terList = TerNIL | TerCons ter terList and for = Const bool | AppUpdFor update for | AndFor for for | NotFor for | Eq ter ter | ExQuan for | Less ter ter (* for rewriting *) | AssignsLoc func terList update (* for rewriting *) | AppSubstFor "nat => ter" for (* for rewriting *) and update = Skip | ElUpd func terList ter | ParUpd update update | SeqUpd update update | QuanUpd update | GuardedUpd for update | AppUpdUpd update update (* for rewriting *) | AppSubstUpd "nat => ter" update (* for rewriting *) | RejectUpd update update (* for rewriting *) text {* Mapping over lists of terms *} consts terListMap :: "(ter => ter) => terList => terList" primrec "terListMap f TerNIL = TerNIL" "terListMap f (TerCons t tr) = (TerCons (f t) (terListMap f tr))" subsection {* Substitutions *} text {* Substitutions are mappings from natural numbers (i.e., variables) to terms. Some substitutions that are frequently needed are defined here. Note that we do not define how to apply substitutions here, instead there are syntactic application operators for substitutions (to terms, formulas and updates), and later we give a rewriting system for applying substitutions. Identity: The substitutions that maps each variable to the term consisting of the variable itself. *} constdefs idSubst :: "nat => ter" "idSubst n == AppVar n" text {* Map each variable $n$ to the next variable $n+1$. *} constdefs shiftSubst :: "nat => ter" "shiftSubst n == AppVar (n+(1::nat))" text {* Map variables $n$ ($n>0$) to the previous variable $n-1$, and the lowest variable 0 to itself. *} constdefs shiftDownSubst :: "nat => ter" "shiftDownSubst n == (if n=0 then AppVar 0 else AppVar (n-(1::nat)))" text {* Map variables $n$ ($n>0$) to the next variable $n+1$, and the lowest variable 0 to itself. *} constdefs shiftKeepZeroSubst :: "nat => ter" "shiftKeepZeroSubst n == AppVar (if n=0 then 0 else n+(1::nat))" text {* Map variables $n$ ($n>1$) to themselves, variable $0$ to variable $1$ and variable $1$ to variable $0$. *} constdefs swapSubst :: "nat => ter" "swapSubst n == AppVar (if n=0 then 1 else (if n=1 then 0 else n))" text {* Concatenation of substitutions: First argument (substitution) is applied after second argument. (We are not directly applying substitutions but are only inserting the syntactic substitution application operator.) *} constdefs substAfterSubst :: "(nat => ter) => (nat => ter) => nat => ter" "substAfterSubst s2 s1 n == (AppSubstTer s2 (s1 n))" text {* Operation on substitutions that is needed when substitutions are moved across binders. *} constdefs bvShift :: "(nat => ter) => nat => ter" "bvShift subst == shiftFun (substAfterSubst shiftSubst subst) (AppVar 0)" section {* Semantics *} subsection {* Well-ordered Universes *} text {* Universes can be arbitrary types that are equipped with a well-ordering and that are not empty. *} axclass universe < wellorder constdefs universeEl :: "'a::universe" "universeEl == arbitrary" constdefs universeOrd :: "(('a::universe) * 'a) set" "universeOrd == {(x,y). x 'a" "min s == (SOME iv. iv:s & (ALL iv2 < iv. iv2 ~: s))" text {* Defining properties of the minimum of a subset of the universe. *} lemma minProp : "ext ~= {} ==> ((min ext) : ext & (ALL iv < (min ext). iv ~: ext))" proof - assume "ext ~= {}" from this obtain el where ElExt : "el : ext" by auto have "wf universeOrd" by auto from this ElExt have "EX z:ext. ALL y. (y,z):universeOrd --> y~:ext" by (simp add: wf_eq_minimal, auto) hence "EX z. z:ext & (ALL y (min ext) : ext" by (simp add: minProp) text {* The minimum of a non-empty set is least in the set. *} lemma minIsMin : "ext ~= {} ==> iv < (min ext) ==> iv ~: ext" by (simp add: minProp) lemma minIsMin2 : "ext ~= {} ==> iv : ext ==> (min ext) <= iv" proof - assume AS1: "ext ~= {}" assume AS2: "iv : ext" have "~ (iv < (min ext))" proof (rule ccontr) assume "~ ~ iv < min ext" hence "iv < min ext" by auto from this AS1 have "iv ~: ext" by (simp add: minIsMin) from this AS2 show "False" by auto qed thus "min ext <= iv" by (simp add: linorder_linear) qed text {* Least elements of subsets of the universe are minima. *} lemma minChar: "iv : ext ==> (ALL iv2 < iv. iv2 ~: ext) ==> iv = min ext" proof - assume "iv : ext" moreover hence notEmpty: "ext ~= {}" by auto ultimately have minLeq: "min ext <= iv" by (simp add: minIsMin2) assume noSmallerEls: "ALL iv2 < iv. iv2 ~: ext" have minGeq: "iv <= min ext" proof (rule ccontr) assume "~ (iv <= min ext)" hence "min ext < iv" by auto from this noSmallerEls have "min ext ~: ext" by auto from this notEmpty show "False" by (simp add: minIsIncluded) qed from minLeq minGeq show ?thesis by auto qed subsection {* Structures, Interpretations and Variable Assignments *} text {* Locations are pairs consisting of functions symbols (natural numbers) and a list of individuals. An interpretation is a total mapping from locations to individuals. A variable assignment is a total mapping from variables (natural numbers) to individuals. A semantic update is a partial interpretation, i.e., a partial mapping from locations to individuals. *} types 'a location = "func * ('a list)" 'a funcInter = "('a location) => 'a" 'a varInter = "nat => 'a" 'a funcUpd = "('a location) => ('a option)" text {* A structure consists of an interpretation and a variable assignment. The universe is given as type parameter. *} record 'a semStructure = FuncInter :: "'a funcInter" VarInter :: "'a varInter" text {* Overriding of interpretation or variable assignment with itself has no effect. *} lemma [simp] : "s(| VarInter := VarInter s |) = s" by (cases s, auto) lemma [simp] : "s(| FuncInter := FuncInter s |) = s" by (cases s, auto) subsection {* Working with Interpretations: Overriding *} text {* The overriding operator for total interpretations. The first argument (total interpretation) is overridden by the second argument (partial interpretation). *} constdefs overrideFuncInter :: "('a funcInter) => ('a funcUpd) => ('a funcInter)" "overrideFuncInter fi fu loc == case (fu loc) of None => (fi loc) | Some v => v" text {* The overriding operator for partial interpretations. The first argument (partial interpretation) is overridden by the second argument (partial interpretation). *} constdefs overrideFuncUpd :: "('a funcUpd) => ('a funcUpd) =>('a funcUpd)" "overrideFuncUpd fOld fNew loc == case (fNew loc) of None => (fOld loc) | Some v => (Some v)" text {* Overriding for a whole structure (first argument), which simply means overriding the interpretation of the structure. *} constdefs overrideInter :: "('a semStructure) => ('a funcUpd) => ('a semStructure)" "overrideInter struct upd == struct(| FuncInter := overrideFuncInter (FuncInter struct) upd|)" subsubsection {* Neutral Elements and Associativity *} lemma overrideFuncInterNeutral : "overrideFuncInter fi (%loc. None) = fi" by (rule ext, simp add: overrideFuncInter_def) lemma overrideFuncInterAssoc : "overrideFuncInter (overrideFuncInter fi a) b = overrideFuncInter fi (overrideFuncUpd a b)" by (rule ext, simp add: overrideFuncInter_def overrideFuncUpd_def split: option.splits) lemma overrideFuncUpdNeutralLeft : "overrideFuncUpd (%loc. None) upd = upd" by (rule ext, simp add: overrideFuncUpd_def split: option.splits) lemma overrideFuncUpdNeutralRight : "overrideFuncUpd upd (%loc. None) = upd" by (rule ext, simp add: overrideFuncUpd_def) lemma overrideFuncUpdIdem : "overrideFuncUpd upd upd = upd" by (rule ext, simp add: overrideFuncUpd_def split: option.splits) lemma overrideFuncUpdAssoc : "overrideFuncUpd u1 (overrideFuncUpd u2 u3) = overrideFuncUpd (overrideFuncUpd u1 u2) u3" by (rule ext, simp add: overrideFuncUpd_def split: option.splits) subsection {* Union Operator for Partial Interpretations *} text {* Map a set~$A$ of partial interpretations to the least upper bound $\bigcup A$ (provided that it exists). *} constdefs funcUpdUnion :: "('a funcUpd) set => ('a funcUpd)" "funcUpdUnion upds loc == (if (EX u : upds. u loc ~= None) then Some (SOME val. EX u : upds. u loc = Some val) else None)" text {* If all partial interpretations in a set agree on the value $val$ for a certain location $loc$ (or are undefined in that point), then also the union maps $loc$ to $val$. *} lemma funcUpdUnionConst : "EX u : upds. u loc ~= None ==> (ALL u : upds. u loc ~= None --> u loc = Some val) ==> funcUpdUnion upds loc = Some val" proof - assume setContainsSome : "EX u : upds. u loc ~= None" hence "EX v. EX u : upds. u loc = Some v" by auto hence someProp : "EX u : upds. u loc = Some (SOME v. EX u : upds. u loc = Some v)" by (rule someI_ex) assume "ALL u : upds. u loc ~= None --> u loc = Some val" from this someProp have "(SOME v. EX u : upds. u loc = Some v) = val" by auto from this setContainsSome show ?thesis by (simp add: funcUpdUnion_def) qed text {* Trivial simplification steps. *} lemma funcUpdUnionSingleton[simp] : "funcUpdUnion {upd} = upd" by (rule ext, simp add: funcUpdUnion_def Let_def split: option.splits, auto) lemma funcUpdUnionEmpty[simp] : "funcUpdUnion {} = (%loc. None)" proof (rule ext) fix loc show "funcUpdUnion {} loc = None" by (simp add: funcUpdUnion_def Let_def) qed subsection {* Modifying Variable Assignments *} text {* Add a value for the lowest variable 0, shifting the values of all variables upwards by one. This is needed when evaluating expressions with operators that bind variables. *} constdefs addVarValue :: "('a semStructure) => 'a => ('a semStructure)" "addVarValue struct val == struct(| VarInter := shiftFun (VarInter struct) val |)" text {* The operations for changing the interpretation and for changing the variable assignment commute. *} lemma [simp] : "addVarValue (overrideInter s u) x = overrideInter (addVarValue s x) u" by (simp add: overrideInter_def addVarValue_def) text {* Adding a value for the lowest variable is useless if the variable assignment is overwritten afterwards. *} lemma [simp] : "(addVarValue s x)(| VarInter := vi |) = s(| VarInter := vi |)" by (simp add: addVarValue_def) text {* Some trivial simplification steps. *} lemma [simp] : "s(| VarInter := VarInter (addVarValue s iv) |) = addVarValue s iv" by (cases s, simp add: addVarValue_def) lemma [simp] : "s(| VarInter := VarInter (addVarValue (addVarValue s iv2) iv) |) = addVarValue (addVarValue s iv2) iv" by (cases s, simp add: addVarValue_def) lemma Var0Val: "VarInter (addVarValue s iv) 0 = iv" by (simp add: addVarValue_def shiftFun_def) lemma Var1Val: "VarInter (addVarValue (addVarValue s iv2) iv) (Suc 0) = iv2" by (simp add: addVarValue_def shiftFun_def) lemma Var2Val: "VarInter (addVarValue (addVarValue (addVarValue s iv3) iv2) iv) 2 = iv3" by (simp add: addVarValue_def shiftFun_def) subsection {* Well-founded Recursion for Evaluating Quantified Updates *} text {* The argument of a quantified update is evaluated to a mapping from individuals to partial interpretations. Given this mapping, we obtain the recursion function $FP$ with fixed-point $A=FP(A)=\mu(FP)$. The least upper bound $\bigcup \{A(a) | a\}$ is the value of the quantified update. *} constdefs quanUpdFP :: "('a => (('a::universe) funcUpd)) => ('a => ('a funcUpd)) => ('a => ('a funcUpd))" "quanUpdFP upds f x == let smallerApproxSet = {f y | y. y (('a::universe) funcUpd)) => 'a => ('a funcUpd)" "quanUpdApprox upds == (wfrec universeOrd (quanUpdFP upds))" text {* Join all approximation $A(a)$ in order to obtain the value of the quantified update. *} constdefs quanUpdComplete :: "('a => (('a::universe) funcUpd)) => ('a funcUpd)" "quanUpdComplete upds == funcUpdUnion {quanUpdApprox upds individ | individ. True}" text {* Fixed-point property of $\mu(FP)$: $FP(\mu(FP)) = \mu(FP)$. *} lemma quanUpdFPProp : "quanUpdFP upds (quanUpdApprox upds) = quanUpdApprox upds" proof (rule ext) fix a have AS1 : "quanUpdApprox upds a = quanUpdFP upds (cut (quanUpdApprox upds) universeOrd a) a" by (simp only: quanUpdApprox_def, rule wfrec, simp) also have AS2 : "... = quanUpdFP upds (quanUpdApprox upds) a" proof - have "{cut (quanUpdApprox upds) universeOrd a y |y. y < a} = {(quanUpdApprox upds) y |y. y < a}" by (simp add: cut_def universeOrd_def, auto) thus ?thesis by (simp add: quanUpdFP_def Let_def) qed from AS1 AS2 show "quanUpdFP upds (quanUpdApprox upds) a = quanUpdApprox upds a" by auto qed subsubsection {* Minimum-Characterisation of Quantified Updates *} text {* A different characterisation of the well-ordered clash semantics of quantified updates. Smaller valuations of a variable always dominate larger valuations. The way in which a quantified update assigns a location depends on the smallest valuation of the quantified variable for which the location is assigned. The approximation mapping $A=\mu(FP)$ is monotonic: For $a \leq b$ we have $A(a) \subseteq A(b)$ (considering the partial function $A(a)$ as a set/relation). *} lemma quanUpdApproxPreserve : "iv < iv2 ==> quanUpdApprox upds iv loc = Some val ==> quanUpdApprox upds iv2 loc = Some val" proof - show "!!iv val. iv < iv2 ==> quanUpdApprox upds iv loc = Some val ==> quanUpdApprox upds iv2 loc = Some val" proof (induct "iv2" rule: wf_induct) show "wf universeOrd" by auto next fix iv2 assume Hyp : "ALL iv1. (iv1, iv2) : universeOrd --> (ALL iv val. iv < iv1 --> quanUpdApprox upds iv loc = Some val --> quanUpdApprox upds iv1 loc = Some val)" fix iv val assume ivIv2Cmp : "iv < iv2" hence ivIv2Ord : "(iv, iv2) : universeOrd" by (simp add: universeOrd_def) let ?updsSet = "{quanUpdApprox upds y |y. y < iv2}" assume valIV : "quanUpdApprox upds iv loc = Some val" from this ivIv2Cmp have setContainsSome : "EX u : ?updsSet. u loc ~= None" by auto have "!!x. x < iv2 ==> quanUpdApprox upds x loc ~= None ==> quanUpdApprox upds x loc = Some val" proof - fix x assume "x < iv2" hence xIvOrd : "(x, iv2) : universeOrd" by (simp add: universeOrd_def) assume "quanUpdApprox upds x loc ~= None" from this obtain valX where valXIsSome : "quanUpdApprox upds x loc = Some valX" by auto show "quanUpdApprox upds x loc = Some val" proof cases assume "x = iv" from this valIV show ?thesis by auto next assume xIvUnequal : "x ~= iv" show ?thesis proof cases assume "x < iv" from this Hyp valXIsSome ivIv2Ord have "quanUpdApprox upds iv loc = Some valX" by blast from this valXIsSome valIV show ?thesis by auto next assume "~ x < iv" from this xIvUnequal have "iv < x" by auto from this Hyp valIV xIvOrd show "quanUpdApprox upds x loc = Some val" by blast qed qed qed hence "ALL u : ?updsSet. (u loc ~= None --> u loc = Some val)" by auto from this setContainsSome have "funcUpdUnion ?updsSet loc = Some val" by (simp add: funcUpdUnionConst) from this have "quanUpdFP upds (quanUpdApprox upds) iv2 loc = Some val" by (simp add: quanUpdFP_def Let_def overrideFuncUpd_def) thus "quanUpdApprox upds iv2 loc = Some val" by (simp add: quanUpdFPProp) qed qed text {* Different approximations $A(a)$, $A(b)$ will always agree (but can be defined in more or less points). *} lemma quanUpdApproxUnique : "quanUpdApprox upds iv loc = Some val ==> quanUpdApprox upds iv2 loc = Some val2 ==> val = val2" proof - assume ivVal : "quanUpdApprox upds iv loc = Some val" assume iv2Val : "quanUpdApprox upds iv2 loc = Some val2" show "val = val2" proof cases assume "iv = iv2" from this ivVal iv2Val show ?thesis by auto next assume ivIv2Unequal : "iv ~= iv2" show ?thesis proof cases assume "iv < iv2" from this ivVal have "quanUpdApprox upds iv2 loc = Some val" by (simp add: quanUpdApproxPreserve) from this iv2Val show ?thesis by auto next assume "~ iv < iv2" from this ivIv2Unequal have "iv2 < iv" by auto from this iv2Val have "quanUpdApprox upds iv loc = Some val2" by (simp add: quanUpdApproxPreserve) from this ivVal show ?thesis by auto qed qed qed lemma quanUpdApproxConst : "quanUpdApprox upds iv loc = Some val ==> quanUpdApprox upds iv2 loc ~= None ==> quanUpdApprox upds iv2 loc = Some val" proof - assume ivVal : "quanUpdApprox upds iv loc = Some val" assume "quanUpdApprox upds iv2 loc ~= None" from this obtain val2 where "quanUpdApprox upds iv2 loc = Some val2" by auto moreover from this ivVal have "val = val2" by (simp add: quanUpdApproxUnique) ultimately show "quanUpdApprox upds iv2 loc = Some val" by auto qed text {* If there is an approximation $A(a)$ that is defined in a point $loc$, then the whole quantified updates is defined in that point and has value $A(a)(loc)$. *} lemma quanUpdCompletePreserve : "quanUpdApprox upds iv loc = Some val ==> quanUpdComplete upds loc = Some val" proof - let ?compSet = "{quanUpdApprox upds x | x. True}" assume ivVal : "quanUpdApprox upds iv loc = Some val" hence notNone : "EX u : ?compSet. u loc ~= None" by auto from ivVal have const : "ALL u : ?compSet. u loc ~= None --> u loc = Some val" by (blast intro: quanUpdApproxConst) from notNone const have "funcUpdUnion ?compSet loc = Some val" by (simp add: funcUpdUnionConst) thus ?thesis by (simp add: quanUpdComplete_def) qed text {* A quantified update is not defined in a point $loc$ if and only if the sub-updated is not defined in $loc$ for all valuation of the quantified variable. *} lemma quanUpdCompleteNone : "(quanUpdComplete upds loc = None) = (ALL iv. upds iv loc = None)" proof cases assume AS : "ALL iv. upds iv loc = None" have "ALL iv. quanUpdFP upds (quanUpdApprox upds) iv loc = None" proof (rule allI) fix iv show "quanUpdFP upds (quanUpdApprox upds) iv loc = None" proof (induct "iv" rule: wf_induct) show "wf universeOrd" by auto next fix iv assume "ALL y. (y, iv) : universeOrd --> quanUpdFP upds (quanUpdApprox upds) y loc = None" hence Hyp : "ALL y. (y, iv) : universeOrd --> quanUpdApprox upds y loc = None" by (simp add: quanUpdFPProp) from this AS have "funcUpdUnion {quanUpdApprox upds y |y. y < iv} loc = None" by (simp add: funcUpdUnion_def Let_def universeOrd_def, auto) from this AS show "quanUpdFP upds (quanUpdApprox upds) iv loc = None" by (simp add: quanUpdFP_def Let_def overrideFuncUpd_def) qed qed hence "ALL iv. quanUpdApprox upds iv loc = None" by (simp add: quanUpdFPProp) hence "quanUpdComplete upds loc = None" by (simp add: quanUpdComplete_def funcUpdUnion_def Let_def, auto) from this AS show ?thesis by auto next assume AS : "~ (ALL iv. upds iv loc = None)" from this obtain el where ElNotNone : "upds el loc ~= None" by auto have "quanUpdFP upds (quanUpdApprox upds) el loc ~= None" proof cases assume "funcUpdUnion {quanUpdApprox upds y |y::'a. y < el} loc = None" from this ElNotNone show ?thesis by (simp add: quanUpdFP_def Let_def overrideFuncUpd_def) next assume "funcUpdUnion {quanUpdApprox upds y |y::'a. y < el} loc ~= None" thus ?thesis by (simp add: quanUpdFP_def Let_def overrideFuncUpd_def, auto) qed hence "quanUpdApprox upds el loc ~= None" by (simp add: quanUpdFPProp) from this obtain val where "quanUpdApprox upds el loc = Some val" by auto hence "quanUpdComplete upds loc ~= None" by (simp add: quanUpdCompletePreserve) from this AS show ?thesis by auto qed text {* Finally, the minimum-characterisation (first a helper lemma that excludes the case that the quantified updated is not defined). *} lemma quanUpdCompleteMinHelp : "(quanUpdComplete upds loc ~= None) ==> quanUpdComplete upds loc = upds (min {iv. upds iv loc ~= None}) loc" proof - assume qucAss: "quanUpdComplete upds loc ~= None" have "!!notNoneSet. notNoneSet = {iv. upds iv loc ~= None} ==> quanUpdComplete upds loc = upds (min notNoneSet) loc" proof - fix notNoneSet assume nnsDef: "notNoneSet = {iv. upds iv loc ~= None}" let ?minIV = "min notNoneSet" from nnsDef qucAss have notNoneSetNonEmpty : "notNoneSet ~= {}" by (simp add: quanUpdCompleteNone) from notNoneSetNonEmpty have AS : "!!x. (x < ?minIV ==> x ~: notNoneSet)" by (simp add: minIsMin) from notNoneSetNonEmpty have "?minIV : notNoneSet" by (simp add: minIsIncluded) from this nnsDef obtain val where valDef : "upds ?minIV loc = Some val" by auto have "ALL iv < ?minIV. quanUpdFP upds (quanUpdApprox upds) iv loc = None" proof (rule allI) fix iv show "iv < ?minIV --> quanUpdFP upds (quanUpdApprox upds) iv loc = None" proof (induct "iv" rule: wf_induct) show "wf universeOrd" by auto next fix iv assume HypHelp : "ALL y. (y, iv) : universeOrd --> y < ?minIV --> quanUpdFP upds (quanUpdApprox upds) y loc = None" from HypHelp have HypHelp2 : "ALL y. (y, iv) : universeOrd --> y < ?minIV --> quanUpdApprox upds y loc = None" by (simp add: quanUpdFPProp) show "iv < ?minIV --> quanUpdFP upds (quanUpdApprox upds) iv loc = None" proof (rule impI) assume IVsmall: "iv < ?minIV" from this HypHelp2 have "ALL y. (y, iv) : universeOrd --> quanUpdApprox upds y loc = None" by (simp add: universeOrd_def, auto) hence "funcUpdUnion {quanUpdApprox upds y |y. y < iv} loc = None" by (simp add: funcUpdUnion_def Let_def universeOrd_def, auto) moreover from IVsmall AS have "iv ~: notNoneSet" by auto from this nnsDef have "upds iv loc = None" by auto ultimately show "quanUpdFP upds (quanUpdApprox upds) iv loc = None" by (simp add: quanUpdFP_def Let_def overrideFuncUpd_def) qed qed qed hence "funcUpdUnion {quanUpdApprox upds y |y. y < ?minIV} loc = None" by (simp add: quanUpdFPProp funcUpdUnion_def Let_def universeOrd_def, auto) hence "quanUpdFP upds (quanUpdApprox upds) ?minIV loc = Some val" by (simp add: quanUpdFP_def Let_def overrideFuncUpd_def) hence "quanUpdApprox upds ?minIV loc = Some val" by (simp add: quanUpdFPProp) hence "quanUpdComplete upds loc = Some val" by (simp add: quanUpdCompletePreserve) from this valDef show "quanUpdComplete upds loc = upds (min notNoneSet) loc" by auto qed thus ?thesis by auto qed text {* The minimum-characterisation. *} lemma quanUpdCompleteMin : "quanUpdComplete upds loc = upds (min {iv. upds iv loc ~= None}) loc" proof cases assume "quanUpdComplete upds loc = None" moreover hence "ALL iv. (upds iv loc = None)" by (simp add: quanUpdCompleteNone) hence "upds (min {iv. upds iv loc ~= None}) loc = None" by auto ultimately show ?thesis by auto next assume "quanUpdComplete upds loc ~= None" thus ?thesis by (blast intro: quanUpdCompleteMinHelp) qed subsection {* Evaluation *} text {* We define the evaluation of terms, lists of terms, formulas and updates mutually recursive. Unsolved question: How could this definition be done using recdef? *} consts terVal :: "(('a::universe) semStructure) => ter => 'a" terListVal :: "(('a::universe) semStructure) => terList => ('a list)" forVal :: "(('a::universe) semStructure) => for => bool" updVal :: "(('a::universe) semStructure) => update => ('a funcUpd)" primrec "terListVal s TerNIL = []" "terListVal s (TerCons t tr) = ((terVal s t) # (terListVal s tr))" "terVal s (AppVar v) = VarInter s v" "terVal s (AppFunc f args) = FuncInter s (f, terListVal s args)" "terVal s (AppUpdTer u te) = terVal (overrideInter s (updVal s u)) te" "terVal s (IfThenTer fo te1 te2) = (if forVal s fo then terVal s te1 else terVal s te2)" "terVal s (AppUpdNonRec u f args) = FuncInter (overrideInter s (updVal s u)) (f, (terListVal s args))" "terVal s (AppSubstTer subst target) = terVal (s(| VarInter := (%n. terVal s (subst n)) |)) target" "terVal s (MinTer fo) = (let ext = {iv. forVal (addVarValue s iv) fo} in (if ext={} then min UNIV else min ext))" "forVal s (Const x) = x" "forVal s (AppUpdFor u fo) = (forVal (overrideInter s (updVal s u)) fo)" "forVal s (AndFor fo1 fo2) = ((forVal s fo1) & (forVal s fo2))" "forVal s (NotFor fo) = (~(forVal s fo))" "forVal s (Eq te1 te2) = ((terVal s te1) = (terVal s te2))" "forVal s (ExQuan fo) = (EX iv. (forVal (addVarValue s iv) fo))" "forVal s (Less te1 te2) = ((terVal s te1) < (terVal s te2))" "forVal s (AssignsLoc f args u) = (updVal s u (f, terListVal s args) ~= None)" "forVal s (AppSubstFor subst target) = forVal (s(| VarInter := (%n. terVal s (subst n)) |)) target" "updVal s (Skip) = (%loc. None)" "updVal s (ElUpd f args value) = (let argsV = terListVal s args; valueV = terVal s value; updLoc = (f, argsV) in (%loc. if loc=updLoc then Some valueV else None))" "updVal s (ParUpd left right) = (let leftV = updVal s left; rightV = updVal s right in overrideFuncUpd leftV rightV)" "updVal s (SeqUpd left right) = (let leftV = updVal s left; rightS = (overrideInter s leftV); rightV = updVal rightS right in overrideFuncUpd leftV rightV)" "updVal s (QuanUpd u) = (let innerUpds = (%iv. updVal (addVarValue s iv) u) in quanUpdComplete innerUpds)" "updVal s (GuardedUpd fo u) = (let foV = forVal s fo; uV = updVal s u in if foV then uV else (%loc. None))" "updVal s (AppUpdUpd u u2) = updVal (overrideInter s (updVal s u)) u2" "updVal s (AppSubstUpd subst target) = updVal (s(| VarInter := (%n. terVal s (subst n)) |)) target" "updVal s (RejectUpd u rejectedVals) = (let uV = updVal s u; rejectedValsV = updVal s rejectedVals in (%loc. if rejectedValsV loc = None then uV loc else None))" subsubsection {* Shorthand Notation for Same Value *} constdefs eqUpd :: "(('a::universe) semStructure) => update => update => bool" "eqUpd s u1 u2 == (updVal s u1 = updVal s u2)" constdefs eqTer :: "(('a::universe) semStructure) => ter => ter => bool" "eqTer s te1 te2 == (terVal s te1 = terVal s te2)" constdefs eqTerList :: "(('a::universe) semStructure) => terList => terList => bool" "eqTerList s te1 te2 == (terListVal s te1 = terListVal s te2)" constdefs eqFor :: "(('a::universe) semStructure) => for => for => bool" "eqFor s fo1 fo2 == (forVal s fo1 = forVal s fo2)" subsection {* Comparison of Lists of Terms *} text {* Given two lists of terms, we create a formula (essentially a simple conjunction of equations) that is true if and only if the two lists have the same value. The mapping doing that could be improved a lot, but it suffices \ldots\ we need this comparison of lists of terms for the rewriting rules later on. *} consts cmpTerLists :: "terList => terList => for" primrec "cmpTerLists TerNIL t2 = (Const (if t2=TerNIL then True else False))" "cmpTerLists (TerCons t tr) tl2 = (case tl2 of TerNIL => Const False | (TerCons t2 tr2) => (AndFor (Eq t t2) (cmpTerLists tr tr2)))" text {* Auxiliary lemma for the characteristic property of the comparison formula for term lists. *} lemma cmpTerListsSemHelp: "ALL t2. (forVal s (cmpTerLists t1 t2)) = (terListVal s t1 = terListVal s t2)" apply (induct "t1") defer 8 defer 8 apply (simp) apply (blast)+ proof - show "ALL t2. forVal s (cmpTerLists TerNIL t2) = (terListVal s TerNIL = terListVal s t2)" proof (rule allI) fix t2 show "forVal s (cmpTerLists TerNIL t2) = (terListVal s TerNIL = terListVal s t2)" proof (cases) assume "EX t tr. t2=TerCons t tr" thus ?thesis by auto next assume "~(EX t tr. t2=TerCons t tr)" hence "t2=TerNIL" by (induct "t2", simp, auto) thus ?thesis by auto qed qed next fix ter terList assume AS: "ALL t2. forVal s (cmpTerLists terList t2) = (terListVal s terList = terListVal s t2)" show "ALL t2. forVal s (cmpTerLists (TerCons ter terList) t2) = (terListVal s (TerCons ter terList) = terListVal s t2)" proof (rule allI) fix t2 have "forVal s (cmpTerLists (TerCons ter terList) t2) ==> (terListVal s (TerCons ter terList) = terListVal s t2)" proof - assume AS1: "forVal s (cmpTerLists (TerCons ter terList) t2)" hence "t2~=TerNIL" by auto hence "EX t tr. t2=TerCons t tr" by (induct "t2", simp, auto) from this obtain t and tr where t2Val: "t2=TerCons t tr" by auto from AS1 t2Val AS have "terListVal s terList = terListVal s tr" by auto from this AS1 t2Val show ?thesis by auto qed moreover have "(terListVal s (TerCons ter terList) = terListVal s t2) ==> forVal s (cmpTerLists (TerCons ter terList) t2)" proof - assume AS1: "terListVal s (TerCons ter terList) = terListVal s t2" hence "t2~=TerNIL" by auto hence "EX t tr. t2=TerCons t tr" by (induct "t2", simp, auto) from this obtain t and tr where t2Val: "t2=TerCons t tr" by auto from this AS1 have "terListVal s terList = terListVal s tr" by auto from this AS have "forVal s (cmpTerLists terList tr)" by auto from this AS1 t2Val show "forVal s (cmpTerLists (TerCons ter terList) t2)" by auto qed ultimately show "forVal s (cmpTerLists (TerCons ter terList) t2) = (terListVal s (TerCons ter terList) = terListVal s t2)" by blast qed qed text {* The characteristic property of the comparison formula for term lists. *} lemma cmpTerListsSem: "(forVal s (cmpTerLists t1 t2)) = (terListVal s t1 = terListVal s t2)" by (simp add: cmpTerListsSemHelp) subsection {* Auxiliary Semantic Properties of Substitutions (rather specialised) *} text {* The operation addVarValue'' and the substitution shiftSubst'' cancel out each other. *} lemma [simp] : "terVal (addVarValue s iv) (shiftSubst n) = VarInter s n" by (simp add: addVarValue_def shiftSubst_def shiftFun_def) text {* The same, where the substitution is applied to an update. *} lemma [simp] : "updVal (addVarValue s iv) (AppSubstUpd shiftSubst u) = updVal s u" by (auto) text {* The same, where the substitution is applied to a list of terms. *} lemma [simp] : "(terListVal (addVarValue s iv) (terListMap (AppSubstTer shiftSubst) args)) = (terListVal s args)" by (induct "args", auto) text {* Correspondingly, shiftKeepZeroSubst'' cancels out an inner addVarValue''. *} lemma shiftKeepZeroSubstRed: "(%n. terVal (addVarValue (addVarValue s iv) iv2) (shiftKeepZeroSubst n)) = (VarInter (addVarValue s iv2))" by (rule ext, simp add: addVarValue_def shiftFun_def shiftKeepZeroSubst_def) text {* shiftDownSubst'' can be described by shifting the values of all variables downwards. *} lemma shiftDownSubstRed: "s(| VarInter := %n. terVal s (shiftDownSubst n) |) = addVarValue s (VarInter s 0)" by (cases s, simp add: shiftDownSubst_def addVarValue_def, rule ext, simp add: shiftFun_def) text {* swapSubst'' has the effect of swapping the values of the lowest variables 0 and 1. Here the version of applying the substitution to an update \ldots *} lemma swapSubstChar : "updVal (addVarValue (addVarValue s iv) iv2) (AppSubstUpd swapSubst u) = updVal (addVarValue (addVarValue s iv2) iv) u" proof (rule ext) fix loc have "(%n. shiftFun (shiftFun (VarInter s) iv) iv2 (if n = 0 then 1 else if n = 1 then 0 else n)) = (%n. shiftFun (shiftFun (VarInter s) iv2) iv n)" by (rule ext, simp add: shiftFun_def) thus "updVal (addVarValue (addVarValue s iv) iv2) (AppSubstUpd swapSubst u) loc = updVal (addVarValue (addVarValue s iv2) iv) u loc" by (cases s, simp add: swapSubst_def addVarValue_def) qed text {* \ldots and the even uglier version deep inside the evaluation function. *} lemma swapSubstAddVar: "(%n. VarInter (addVarValue (addVarValue s iv) iv2) (if n = 0 then 1 else if n = 1 then 0 else n)) = VarInter (addVarValue (addVarValue s iv2) iv)" by (rule ext, simp add: addVarValue_def shiftFun_def) text {* Commuting addVarValue'' and a substitution can be done by inserting bvShift''. *} lemma addVarValueBVShift : "addVarValue (s(| VarInter := %n. terVal s (subst n) |)) iv = s(| VarInter := %n. terVal (addVarValue s iv) (bvShift subst n) |)" proof - have "shiftFun (%n. terVal s (subst n)) iv = (%n. terVal (addVarValue s iv) (bvShift subst n))" proof (rule ext) fix n have "0 < n--> terVal s (subst (n-(1::nat))) = terVal (addVarValue s iv) (substAfterSubst shiftSubst subst (n-(1::nat)))" by (simp add: addVarValue_def substAfterSubst_def shiftFun_def shiftSubst_def, cases s, auto) thus "shiftFun (%n. terVal s (subst n)) iv n = terVal (addVarValue s iv) (bvShift subst n)" by (simp add: bvShift_def addVarValue_def shiftFun_def) qed thus ?thesis by (simp add: addVarValue_def) qed subsection {* Relating Substitution and Update Application with Evaluation of Term Lists *} lemma terListAppSubst : "terListVal (s(| VarInter := %n. terVal s (subst n) |)) args = terListVal s (terListMap (AppSubstTer subst) args)" by (induct "args", simp, auto) lemma terListAppUpd : "terListVal (overrideInter s (updVal s u)) args = terListVal s (terListMap (AppUpdTer u) args)" by (induct "args", simp, auto) subsection {* Auxiliary Properties of Parallel Updates *} text {* A parallel update can only \emph{not} assign a location if both sub-updates do \emph{not} assign the location. *} lemma parUpdNoneFirst: "updVal s (ParUpd u1 u2) loc = None ==> updVal s u1 loc = None" by (simp add: Let_def overrideFuncUpd_def split: option.splits) lemma parUpdNoneSec: "updVal s (ParUpd u1 u2) loc = None ==> updVal s u2 loc = None" by (simp add: Let_def overrideFuncUpd_def split: option.splits) text {* The right update in a parallel update always dominates. *} lemma parUpdSec: "updVal s u2 loc = Some val ==> updVal s (ParUpd u1 u2) loc = Some val" by (simp add: Let_def overrideFuncUpd_def split: option.splits) section {* Sets of Terms, Formulas and Updates *} subsection {* Basic Definitions *} text {* We mostly talk about quadruples of sets of terms, sets of lists of terms, sets of formulas and sets of updates. *} record tfuSet = terSet :: "ter set" terListSet :: "terList set" forSet :: "for set" updSet :: "update set" subsection {* Monotonic Closure of Sets *} text {* We define a closure operator on quadruples of sets. The monotonic closure of such a quadruple is the smallest quadruple of sets with the property, for each constructor $f$, that $a \in A$ implies $f(a) \in A$. *} consts terMono :: "tfuSet => ter set" terListMono :: "tfuSet => terList set" forMono :: "tfuSet => for set" updMono :: "tfuSet => update set" inductive "terMono tfu" "terListMono tfu" "forMono tfu" "updMono tfu" intros "a : terSet tfu ==> a : terMono tfu" "a : terListSet tfu ==> a : terListMono tfu" "a : forSet tfu ==> a : forMono tfu" "a : updSet tfu ==> a : updMono tfu" "args : terListMono tfu ==> AppFunc func args : terMono tfu" "u : updMono tfu ==> AppUpdTer u args : terMono tfu" "te : terMono tfu ==> AppUpdTer u te : terMono tfu" "fo : forMono tfu ==> IfThenTer fo te1 te2 : terMono tfu" "te : terMono tfu ==> IfThenTer fo te te2 : terMono tfu" "te : terMono tfu ==> IfThenTer fo te2 te : terMono tfu" "u : updMono tfu ==> AppUpdNonRec u func args : terMono tfu" "args : terListMono tfu ==> AppUpdNonRec u func args : terMono tfu" "te : terMono tfu ==> AppSubstTer (subst(n:=te)) te2 : terMono tfu" "te : terMono tfu ==> AppSubstTer subst te : terMono tfu" "fo : forMono tfu ==> MinTer fo : terMono tfu" "te : terMono tfu ==> TerCons te args : terListMono tfu" "args : terListMono tfu ==> TerCons te args : terListMono tfu" "u : updMono tfu ==> AppUpdFor u fo : forMono tfu" "fo : forMono tfu ==> AppUpdFor u fo : forMono tfu" "fo : forMono tfu ==> AndFor fo fo2 : forMono tfu" "fo : forMono tfu ==> AndFor fo2 fo : forMono tfu" "fo : forMono tfu ==> NotFor fo : forMono tfu" "te : terMono tfu ==> Eq te te2 : forMono tfu" "te : terMono tfu ==> Eq te2 te : forMono tfu" "te : terMono tfu ==> Less te te2 : forMono tfu" "te : terMono tfu ==> Less te2 te : forMono tfu" "fo : forMono tfu ==> ExQuan fo : forMono tfu" "args : terListMono tfu ==> AssignsLoc func args u : forMono tfu" "u : updMono tfu ==> AssignsLoc func args u : forMono tfu" "te : terMono tfu ==> AppSubstFor (subst(n:=te)) fo : forMono tfu" "fo : forMono tfu ==> AppSubstFor subst fo : forMono tfu" "args : terListMono tfu ==> ElUpd func args te : updMono tfu" "te : terMono tfu ==> ElUpd func args te : updMono tfu" "u : updMono tfu ==> ParUpd u u2 : updMono tfu" "u : updMono tfu ==> ParUpd u2 u : updMono tfu" "u : updMono tfu ==> SeqUpd u u2 : updMono tfu" "u : updMono tfu ==> SeqUpd u2 u : updMono tfu" "u : updMono tfu ==> QuanUpd u : updMono tfu" "fo : forMono tfu ==> GuardedUpd fo u : updMono tfu" "u : updMono tfu ==> GuardedUpd fo u : updMono tfu" "u : updMono tfu ==> AppUpdUpd u u2 : updMono tfu" "u : updMono tfu ==> AppUpdUpd u2 u : updMono tfu" "te : terMono tfu ==> AppSubstUpd (subst(n:=te)) u : updMono tfu" "u : updMono tfu ==> AppSubstUpd subst u : updMono tfu" "u : updMono tfu ==> RejectUpd u u2 : updMono tfu" "u : updMono tfu ==> RejectUpd u2 u : updMono tfu" constdefs tfuMono :: "tfuSet => tfuSet" "tfuMono tfu == (| terSet = terMono tfu, terListSet = terListMono tfu, forSet = forMono tfu, updSet = updMono tfu |)" section {* Relations on Terms, Formulas and Updates *} subsection {* Basic Definitions about Relations *} text {* As for sets, in most cases we have to consider a whole quadruple of relations on terms, list of terms, formulas and updates. *} record syntRelFam = syntRelTer :: "(ter * ter) set" syntRelTerList :: "(terList * terList) set" syntRelFor :: "(for * for) set" syntRelUpd :: "(update * update) set" text {* Such a quadruple is called correct'' for a certain structure if all pairs of related entities agree in their values. *} constdefs syntRelFamCorrect :: "(('a::universe) semStructure) => syntRelFam => bool" "syntRelFamCorrect s rt == ALL te1 te2 tl1 tl2 fo1 fo2 u1 u2. ((te1, te2) : syntRelTer rt --> eqTer s te1 te2) & ((tl1, tl2) : syntRelTerList rt --> eqTerList s tl1 tl2) & ((fo1, fo2) : syntRelFor rt --> eqFor s fo1 fo2) & ((u1, u2) : syntRelUpd rt --> eqUpd s u1 u2)" subsection {* Monotonic Closure of Relations; Subterm Property *} text {* We define the monotonic closure of relation quadruples mutually inductively. The result is the smallest relation containing a given syntactic relation that is monotonic, i.e., for all constructors $f$ we have $a \sim b$ implies $f(a) \sim f(b)$. First we define the components of the relation inductively. *} consts terRewrMono :: "syntRelFam => (ter * ter) set" terListRewrMono :: "syntRelFam => (terList * terList) set" forRewrMono :: "syntRelFam => (for * for) set" updRewrMono :: "syntRelFam => (update * update) set" inductive "terRewrMono rt" "terListRewrMono rt" "forRewrMono rt" "updRewrMono rt" intros terRewrMonoSubset: "(a, b) : syntRelTer rt ==> (a, b) : terRewrMono rt" terListRewrMonoSubset: "(a, b) : syntRelTerList rt ==> (a, b) : terListRewrMono rt" forRewrMonoSubset: "(a, b) : syntRelFor rt ==> (a, b) : forRewrMono rt" updRewrMonoSubset: "(a, b) : syntRelUpd rt ==> (a, b) : updRewrMono rt" terRewrMono1: "(terl, terlb) : terListRewrMono rt ==> (AppFunc func terl, AppFunc func terlb) : terRewrMono rt" terRewrMono3: "(u, ub) : updRewrMono rt ==> (AppUpdTer u te, AppUpdTer ub te) : terRewrMono rt" terRewrMono4: "(te, teb) : terRewrMono rt ==> (AppUpdTer u te, AppUpdTer u teb) : terRewrMono rt" terRewrMono5: "(fo, fob) : forRewrMono rt ==> (IfThenTer fo te1 te2, IfThenTer fob te1 te2) : terRewrMono rt" terRewrMono6: "(te, teb) : terRewrMono rt ==> (IfThenTer fo te te2, IfThenTer fo teb te2) : terRewrMono rt" terRewrMono7: "(te, teb) : terRewrMono rt ==> (IfThenTer fo te2 te, IfThenTer fo te2 teb) : terRewrMono rt" terRewrMono8: "(u, ub) : updRewrMono rt ==> (AppUpdNonRec u func terl, AppUpdNonRec ub func terl) : terRewrMono rt" terRewrMono9: "(terl, terlb) : terListRewrMono rt ==> (AppUpdNonRec u func terl, AppUpdNonRec u func terlb) : terRewrMono rt" terRewrMono13: "(te, teb) : terRewrMono rt ==> (AppSubstTer (subst(n:=te)) te2, AppSubstTer (subst(n:=teb)) te2) : terRewrMono rt" terRewrMono11: "(te, teb) : terRewrMono rt ==> (AppSubstTer subst te, AppSubstTer subst teb) : terRewrMono rt" terRewrMono12: "(fo, fob) : forRewrMono rt ==> (MinTer fo, MinTer fob) : terRewrMono rt" terListRewrMono1: "(te, teb) : terRewrMono rt ==> (TerCons te terl, TerCons teb terl) : terListRewrMono rt" terListRewrMono2: "(terl, terlb) : terListRewrMono rt ==> (TerCons te terl, TerCons te terlb) : terListRewrMono rt" forRewrMono1: "(u, ub) : updRewrMono rt ==> (AppUpdFor u fo, AppUpdFor ub fo) : forRewrMono rt" forRewrMono2: "(fo, fob) : forRewrMono rt ==> (AppUpdFor u fo, AppUpdFor u fob) : forRewrMono rt" forRewrMono3: "(fo, fob) : forRewrMono rt ==> (AndFor fo fo2, AndFor fob fo2) : forRewrMono rt" forRewrMono4: "(fo, fob) : forRewrMono rt ==> (AndFor fo2 fo, AndFor fo2 fob) : forRewrMono rt" forRewrMono5: "(fo, fob) : forRewrMono rt ==> (NotFor fo, NotFor fob) : forRewrMono rt" forRewrMono6: "(te, teb) : terRewrMono rt ==> (Eq te te2, Eq teb te2) : forRewrMono rt" forRewrMono7: "(te, teb) : terRewrMono rt ==> (Eq te2 te, Eq te2 teb) : forRewrMono rt" forRewrMono13: "(te, teb) : terRewrMono rt ==> (Less te te2, Less teb te2) : forRewrMono rt" forRewrMono14: "(te, teb) : terRewrMono rt ==> (Less te2 te, Less te2 teb) : forRewrMono rt" forRewrMono8: "(fo, fob) : forRewrMono rt ==> (ExQuan fo, ExQuan fob) : forRewrMono rt" forRewrMono9: "(terl, terlb) : terListRewrMono rt ==> (AssignsLoc func terl u, AssignsLoc func terlb u) : forRewrMono rt" forRewrMono11: "(u, ub) : updRewrMono rt ==> (AssignsLoc func terl u, AssignsLoc func terl ub) : forRewrMono rt" forRewrMono15: "(te, teb) : terRewrMono rt ==> (AppSubstFor (subst(n:=te)) fo, AppSubstFor (subst(n:=teb)) fo) : forRewrMono rt" forRewrMono12: "(fo, fob) : forRewrMono rt ==> (AppSubstFor subst fo, AppSubstFor subst fob) : forRewrMono rt" updRewrMono1: "(terl, terlb) : terListRewrMono rt ==> (ElUpd func terl te, ElUpd func terlb te) : updRewrMono rt" updRewrMono2: "(te, teb) : terRewrMono rt ==> (ElUpd func terl te, ElUpd func terl teb) : updRewrMono rt" updRewrMono4: "(u, ub) : updRewrMono rt ==> (ParUpd u u2, ParUpd ub u2) : updRewrMono rt" updRewrMono5: "(u, ub) : updRewrMono rt ==> (ParUpd u2 u, ParUpd u2 ub) : updRewrMono rt" updRewrMono12: "(u, ub) : updRewrMono rt ==> (SeqUpd u u2, SeqUpd ub u2) : updRewrMono rt" updRewrMono13: "(u, ub) : updRewrMono rt ==> (SeqUpd u2 u, SeqUpd u2 ub) : updRewrMono rt" updRewrMono6: "(u, ub) : updRewrMono rt ==> (QuanUpd u, QuanUpd ub) : updRewrMono rt" updRewrMono7: "(fo, fob) : forRewrMono rt ==> (GuardedUpd fo u, GuardedUpd fob u) : updRewrMono rt" updRewrMono8: "(u, ub) : updRewrMono rt ==> (GuardedUpd fo u, GuardedUpd fo ub) : updRewrMono rt" updRewrMono9: "(u, ub) : updRewrMono rt ==> (AppUpdUpd u u2, AppUpdUpd ub u2) : updRewrMono rt" updRewrMono10: "(u, ub) : updRewrMono rt ==> (AppUpdUpd u2 u, AppUpdUpd u2 ub) : updRewrMono rt" updRewrMono16: "(te, teb) : terRewrMono rt ==> (AppSubstUpd (subst(n:=te)) u, AppSubstUpd (subst(n:=teb)) u) : updRewrMono rt" updRewrMono11: "(u, ub) : updRewrMono rt ==> (AppSubstUpd subst u, AppSubstUpd subst ub) : updRewrMono rt" updRewrMono14: "(u, ub) : updRewrMono rt ==> (RejectUpd u u2, RejectUpd ub u2) : updRewrMono rt" updRewrMono15: "(u, ub) : updRewrMono rt ==> (RejectUpd u2 u, RejectUpd u2 ub) : updRewrMono rt" text {* \ldots\ and then we can define the relation quadruple. *} constdefs rewrMono :: "syntRelFam => syntRelFam" "rewrMono rt == (| syntRelTer = terRewrMono rt, syntRelTerList = terListRewrMono rt, syntRelFor = forRewrMono rt, syntRelUpd = updRewrMono rt |)" subsubsection {* Correctness of Monotonic Closure *} text {* If a syntactic relation is correct for all structures with a fixed universe, the also the monotonic closure of the relation is correct. First, we need two auxiliary lemmas. *} lemma rewrMonoCorrectHelpHelp: "(%na. terVal s (if na = n then te else subst na)) = (%na. terVal s (subst na))(n:=terVal s te)" by (rule ext, simp) lemma rewrMonoCorrectHelp: "ALL s::(('a::universe) semStructure). syntRelFamCorrect s rt ==> ((te1, te2) : terRewrMono rt --> (ALL s::(('a::universe) semStructure). eqTer s te1 te2)) & ((tl1, tl2) : terListRewrMono rt --> (ALL s::(('a::universe) semStructure). eqTerList s tl1 tl2)) & ((fo1, fo2) : forRewrMono rt --> (ALL s::(('a::universe) semStructure). eqFor s fo1 fo2)) & ((u1, u2) : updRewrMono rt --> (ALL s::(('a::universe) semStructure). eqUpd s u1 u2))" apply (rule terRewrMono_terListRewrMono_forRewrMono_updRewrMono.induct) apply (simp_all add: syntRelFamCorrect_def) apply (simp_all add: eqTer_def eqTerList_def eqFor_def eqUpd_def rewrMonoCorrectHelpHelp) done text {* Correctness of syntactic relations is preserved by monotonic closure. *} lemma rewrMonoCorrect: "ALL s::(('a::universe) semStructure). syntRelFamCorrect s rt ==> ALL s::(('a::universe) semStructure). syntRelFamCorrect s (rewrMono rt)" proof - assume "ALL s::(('a::universe) semStructure). syntRelFamCorrect s rt" moreover hence "ALL te1 te2 tl1 tl2 fo1 fo2 u1 u2. ((te1, te2) : terRewrMono rt --> (ALL s::(('a::universe) semStructure). eqTer s te1 te2)) & ((tl1, tl2) : terListRewrMono rt --> (ALL s::(('a::universe) semStructure). eqTerList s tl1 tl2)) & ((fo1, fo2) : forRewrMono rt --> (ALL s::(('a::universe) semStructure). eqFor s fo1 fo2)) & ((u1, u2) : updRewrMono rt --> (ALL s::(('a::universe) semStructure). eqUpd s u1 u2))" by (simp add: rewrMonoCorrectHelp) ultimately show ?thesis by (simp add: syntRelFamCorrect_def rewrMono_def) qed section {* Rewriting Relation for Application of Updates and Substitutions *} subsection {* Definition *} text {* We define the rewriting relation for application of updates and substitutions as a syntactic relation (quadruple). Monotonicity is achieved later by applying the corresponding closure operator. While we formally define the rewriting relation as an inductive set, no inductive constructions are used here. *} consts rewrTerDirect :: "(ter * ter) set" rewrForDirect :: "(for * for) set" rewrUpdDirect :: "(update * update) set" inductive rewrTerDirect intros (* Updates: Application as morphism on terms *) uMorphTer1: "(AppUpdTer u (AppVar var), AppVar var) : rewrTerDirect" uMorphTer2: "(AppUpdTer u (AppFunc func args), AppUpdNonRec u func (terListMap (AppUpdTer u) args)) : rewrTerDirect" uMorphTer4: "(AppUpdTer u (IfThenTer fo te1 te2), IfThenTer (AppUpdFor u fo) (AppUpdTer u te1) (AppUpdTer u te2)) : rewrTerDirect" uMorphTer5: "(AppUpdTer u (MinTer fo), MinTer (AppUpdFor (AppSubstUpd shiftSubst u) fo)) : rewrTerDirect" (* Updates: Application to terms describing locations *) applyUpdToLoc1: "(AppUpdNonRec Skip func args, AppFunc func args) : rewrTerDirect" applyUpdToLoc2: "(AppUpdNonRec (ElUpd func args2 value) func args, IfThenTer (cmpTerLists args2 args) value (AppFunc func args)) : rewrTerDirect" applyUpdToLoc3: "func ~= g ==> (AppUpdNonRec (ElUpd g args2 value) func args, AppFunc func args) : rewrTerDirect" applyUpdToLoc4: "(AppUpdNonRec (ParUpd u1 u2) func args, IfThenTer (AssignsLoc func args u2) (AppUpdNonRec u2 func args) (AppUpdNonRec u1 func args)) : rewrTerDirect" applyUpdToLoc5: "(AppUpdNonRec (QuanUpd u) func args, (AppUpdNonRec (AppSubstUpd (shiftFun idSubst (MinTer (AssignsLoc func (terListMap (AppSubstTer shiftSubst) args) u))) u) func args)) : rewrTerDirect" applyUpdToLoc6: "(AppUpdNonRec (GuardedUpd fo u) func args, IfThenTer fo (AppUpdNonRec u func args) (AppFunc func args)) : rewrTerDirect" (* Substitutions *) applySubstTer1: "(AppSubstTer subst (AppVar var), subst var) : rewrTerDirect" applySubstTer3: "(AppSubstTer subst (AppFunc func args), AppFunc func (terListMap (AppSubstTer subst) args)) : rewrTerDirect" applySubstTer5: "(AppSubstTer subst (IfThenTer fo te1 te2), IfThenTer (AppSubstFor subst fo) (AppSubstTer subst te1) (AppSubstTer subst te2)) : rewrTerDirect" applySubstTer6: "(AppSubstTer subst (MinTer fo), (MinTer (AppSubstFor (bvShift subst) fo))) : rewrTerDirect" inductive rewrForDirect intros (* Updates: Application as morphism on formulas *) uMorphFor1: "(AppUpdFor u (Const bool), Const bool) : rewrForDirect" uMorphFor2: "(AppUpdFor u (AndFor fo1 fo2), AndFor (AppUpdFor u fo1) (AppUpdFor u fo2)) : rewrForDirect" uMorphFor3: "(AppUpdFor u (NotFor fo), NotFor (AppUpdFor u fo)) : rewrForDirect" uMorphFor4: "(AppUpdFor u (Eq te1 te2), Eq (AppUpdTer u te1) (AppUpdTer u te2)) : rewrForDirect" uMorphFor6: "(AppUpdFor u (Less te1 te2), Less (AppUpdTer u te1) (AppUpdTer u te2)) : rewrForDirect" uMorphFor5: "(AppUpdFor u (ExQuan fo), ExQuan (AppUpdFor (AppSubstUpd shiftSubst u) fo)) : rewrForDirect" (* Updates: Derivation of updates locations *) updLocs1: "(AssignsLoc func args Skip, Const False) : rewrForDirect" updLocs2: "(AssignsLoc func args (ElUpd func args2 value), (cmpTerLists args args2)) : rewrForDirect" updLocs3: "func ~= g ==> (AssignsLoc func args (ElUpd g args2 value), Const False) : rewrForDirect" updLocs4: "(AssignsLoc func args (ParUpd u1 u2), NotFor (AndFor (NotFor (AssignsLoc func args u1)) (NotFor (AssignsLoc func args u2)))) : rewrForDirect" updLocs5: "(AssignsLoc func args (QuanUpd u), ExQuan (AssignsLoc func (terListMap (AppSubstTer shiftSubst) args) u)) : rewrForDirect" updLocs6: "(AssignsLoc func args (GuardedUpd fo u), AndFor fo (AssignsLoc func args u)) : rewrForDirect" (* Substitutions *) applySubstFor1: "(AppSubstFor subst (Const b), Const b) : rewrForDirect" applySubstFor2: "(AppSubstFor subst (AndFor fo1 fo2), AndFor (AppSubstFor subst fo1) (AppSubstFor subst fo2)) : rewrForDirect" applySubstFor3: "(AppSubstFor subst (NotFor fo), NotFor (AppSubstFor subst fo)) : rewrForDirect" applySubstFor4: "(AppSubstFor subst (Eq te1 te2), Eq (AppSubstTer subst te1) (AppSubstTer subst te2)) : rewrForDirect" applySubstFor6: "(AppSubstFor subst (Less te1 te2), Less (AppSubstTer subst te1) (AppSubstTer subst te2)) : rewrForDirect" applySubstFor5: "(AppSubstFor subst (ExQuan fo), ExQuan (AppSubstFor (bvShift subst) fo)) : rewrForDirect" inductive rewrUpdDirect intros applySubstUpd1: "(AppSubstUpd subst Skip, Skip) : rewrUpdDirect" applySubstUpd2: "(AppSubstUpd subst (ElUpd f args value), (ElUpd f (terListMap (AppSubstTer subst) args) (AppSubstTer subst value))) : rewrUpdDirect" applySubstUpd3: "(AppSubstUpd subst (ParUpd u1 u2), (ParUpd (AppSubstUpd subst u1) (AppSubstUpd subst u2))) : rewrUpdDirect" applySubstUpd4: "(AppSubstUpd subst (QuanUpd u), (QuanUpd (AppSubstUpd (bvShift subst) u))) : rewrUpdDirect" applySubstUpd5: "(AppSubstUpd subst (GuardedUpd fo u), (GuardedUpd (AppSubstFor subst fo) (AppSubstUpd subst u))) : rewrUpdDirect" applyUpdUpd1: "(AppUpdUpd u Skip, Skip) : rewrUpdDirect" applyUpdUpd2: "(AppUpdUpd u (ElUpd f args value), ElUpd f (terListMap (AppUpdTer u) args) (AppUpdTer u value)) : rewrUpdDirect" applyUpdUpd3: "(AppUpdUpd u (ParUpd u1 u2), ParUpd (AppUpdUpd u u1) (AppUpdUpd u u2)) : rewrUpdDirect" applyUpdUpd4: "(AppUpdUpd u (QuanUpd u2), QuanUpd (AppUpdUpd (AppSubstUpd shiftSubst u) u2)) : rewrUpdDirect" applyUpdUpd5: "(AppUpdUpd u (GuardedUpd fo u2), GuardedUpd (AppUpdFor u fo) (AppUpdUpd u u2)) : rewrUpdDirect" rejectUpd1: "(RejectUpd (Skip) rejU, Skip) : rewrUpdDirect" rejectUpd2: "(RejectUpd (ElUpd f args value) rejU, GuardedUpd (NotFor (AssignsLoc f args rejU)) (ElUpd f args value)) : rewrUpdDirect" rejectUpd3: "(RejectUpd (ParUpd u1 u2) rejU, ParUpd (RejectUpd u1 rejU) (RejectUpd u2 rejU)) : rewrUpdDirect" rejectUpd4: "(RejectUpd (QuanUpd u) rejU, QuanUpd (RejectUpd u (AppSubstUpd shiftSubst rejU))) : rewrUpdDirect" rejectUpd5: "(RejectUpd (GuardedUpd fo u) rejU, GuardedUpd fo (RejectUpd u rejU)) : rewrUpdDirect" seqUpd1: "(SeqUpd u1 u2, ParUpd u1 (AppUpdUpd u1 u2)) : rewrUpdDirect" text {* We do not have any rewriting rules for lists of terms (but monotonicity will add some soon \ldots) *} constdefs rewrDirect :: syntRelFam "rewrDirect == (| syntRelTer = rewrTerDirect, syntRelTerList = {}, syntRelFor = rewrForDirect, syntRelUpd = rewrUpdDirect |)" subsection {* Correctness of the Rewriting System *} text {* We show the correctness of the rewriting rules by rule induction. (Actually, no inductive arguments are used here, it is just a case distinction over the different possible rewriting steps.) *} subsubsection {* Correctness for Rewriting of Terms *} lemma rewrTerDirectCorrect: "(te1, te2) : rewrTerDirect ==> eqTer s te1 te2" proof (induct rule: rewrTerDirect.induct) case uMorphTer1 fix u var show "eqTer s (AppUpdTer u (AppVar var)) (AppVar var)" by (simp add: eqTer_def overrideInter_def) next case uMorphTer2 fix func args u show "eqTer s (AppUpdTer u (AppFunc func args)) (AppUpdNonRec u func (terListMap (AppUpdTer u) args))" by (simp add: eqTer_def terListAppUpd) next case uMorphTer4 fix fo te1 te2 u show "eqTer s (AppUpdTer u (IfThenTer fo te1 te2)) (IfThenTer (AppUpdFor u fo) (AppUpdTer u te1) (AppUpdTer u te2))" by (simp add: eqTer_def) next case uMorphTer5 fix fo u show "eqTer s (AppUpdTer u (MinTer fo)) (MinTer (AppUpdFor (AppSubstUpd shiftSubst u) fo))" by (simp add: eqTer_def Let_def) next case applyUpdToLoc1 fix func args show "eqTer s (AppUpdNonRec Skip func args) (AppFunc func args)" by (simp add: eqTer_def overrideInter_def overrideFuncInterNeutral) next case applyUpdToLoc2 fix func args args2 value show "eqTer s (AppUpdNonRec (ElUpd func args2 value) func args) (IfThenTer (cmpTerLists args2 args) value (AppFunc func args))" by (simp add: eqTer_def Let_def overrideInter_def overrideFuncInter_def cmpTerListsSem) next case applyUpdToLoc3 fix f g args args2 value assume "(f::func) ~= g" thus "eqTer s (AppUpdNonRec (ElUpd g args2 value) f args) (AppFunc f args)" by (simp add: eqTer_def Let_def overrideInter_def overrideFuncInter_def) next case applyUpdToLoc4 fix func args u1 u2 show "eqTer s (AppUpdNonRec (ParUpd u1 u2) func args) (IfThenTer (AssignsLoc func args u2) (AppUpdNonRec u2 func args) (AppUpdNonRec u1 func args))" by (simp add: eqTer_def Let_def overrideInter_def overrideFuncInter_def overrideFuncUpd_def split: option.splits) next case applyUpdToLoc5 fix args::terList fix func::func fix u let ?loc = "(func, terListVal s args)" let ?upds = "%iv. updVal (addVarValue s iv) u" have HELP: "!! te. (%n. terVal s (shiftFun idSubst te n)) = shiftFun (VarInter s) (terVal s te)" by (rule ext, simp add: shiftFun_def idSubst_def) show "eqTer s (AppUpdNonRec (QuanUpd u) func args) (AppUpdNonRec (AppSubstUpd (shiftFun idSubst (MinTer (AssignsLoc func (terListMap (AppSubstTer shiftSubst) args) u))) u) func args)" proof cases assume AS : "ALL x. ?upds x ?loc = None" hence "quanUpdComplete ?upds ?loc = None" by (simp add: quanUpdCompleteNone) from this AS HELP show ?thesis by (simp add: eqTer_def Let_def overrideInter_def overrideFuncInter_def addVarValue_def) next assume AS : "~ (ALL x. ?upds x ?loc = None)" hence "min {iv. ?upds iv ?loc ~= None} = terVal s (MinTer (AssignsLoc func (terListMap (AppSubstTer shiftSubst) args) u))" by (simp add: Let_def, auto) from this AS HELP show ?thesis by (simp add: eqTer_def Let_def addVarValue_def overrideInter_def overrideFuncInter_def quanUpdCompleteMin) qed next case applyUpdToLoc6 fix fo func args u show "eqTer s (AppUpdNonRec (GuardedUpd fo u) func args) (IfThenTer fo (AppUpdNonRec u func args) (AppFunc func args))" by (simp add: eqTer_def Let_def overrideInter_def overrideFuncInter_def) next case applySubstTer1 fix subst var show "eqTer s (AppSubstTer subst (AppVar var)) (subst var)" by (simp add: eqTer_def Let_def) next case applySubstTer3 fix subst func args show "eqTer s (AppSubstTer subst (AppFunc func args)) (AppFunc func (terListMap (AppSubstTer subst) args))" by (simp add: eqTer_def Let_def terListAppSubst) next case applySubstTer5 fix fo subst te1 te2 show "eqTer s (AppSubstTer subst (IfThenTer fo te1 te2)) (IfThenTer (AppSubstFor subst fo) (AppSubstTer subst te1) (AppSubstTer subst te2))" by (simp add: eqTer_def Let_def) next case applySubstTer6 fix fo subst show "eqTer s (AppSubstTer subst (MinTer fo)) (MinTer (AppSubstFor (bvShift subst) fo))" by (simp add: eqTer_def addVarValueBVShift) qed subsubsection {* Correctness for Rewriting of Formulas *} lemma rewrForDirectCorrect: "(fo1, fo2) : rewrForDirect ==> eqFor s fo1 fo2" proof (induct rule: rewrForDirect.induct) case uMorphFor1 fix b u show "eqFor s (AppUpdFor u (Const b)) (Const b)" by (simp add: eqFor_def) next case uMorphFor2 fix fo1 fo2 u show "eqFor s (AppUpdFor u (AndFor fo1 fo2)) (AndFor (AppUpdFor u fo1) (AppUpdFor u fo2))" by (simp add: eqFor_def) next case uMorphFor3 fix fo u show "eqFor s (AppUpdFor u (NotFor fo)) (NotFor (AppUpdFor u fo))" by (simp add: eqFor_def) next case uMorphFor4 fix te1 te2 u show "eqFor s (AppUpdFor u (Eq te1 te2)) (Eq (AppUpdTer u te1) (AppUpdTer u te2))" by (simp add: eqFor_def) next case uMorphFor6 fix te1 te2 u show "eqFor s (AppUpdFor u (Less te1 te2)) (Less (AppUpdTer u te1) (AppUpdTer u te2))" by (simp add: eqFor_def) next case uMorphFor5 fix fo u show "eqFor s (AppUpdFor u (ExQuan fo)) (ExQuan (AppUpdFor (AppSubstUpd shiftSubst u) fo))" by (simp add: eqFor_def) next case updLocs1 fix func args show "eqFor s (AssignsLoc func args Skip) (Const False)" by (simp add: eqFor_def) next case updLocs2 fix func args args2 value show "eqFor s (AssignsLoc func args (ElUpd func args2 value)) (cmpTerLists args args2)" by (simp add: eqFor_def Let_def cmpTerListsSem) next case updLocs3 fix func g args args2 value assume "(func::func) ~= g" thus "eqFor s (AssignsLoc func args (ElUpd g args2 value)) (Const False)" by (simp add: eqFor_def Let_def) next case updLocs4 fix func args u1 u2 show "eqFor s (AssignsLoc func args (ParUpd u1 u2)) (NotFor (AndFor (NotFor (AssignsLoc func args u1)) (NotFor (AssignsLoc func args u2))))" by (simp add: eqFor_def Let_def overrideFuncUpd_def split: option.splits) next case updLocs5 fix func args u show "eqFor s (AssignsLoc func args (QuanUpd u)) (ExQuan (AssignsLoc func (terListMap (AppSubstTer shiftSubst) args) u))" by (simp add: eqFor_def Let_def quanUpdCompleteNone) next case updLocs6 fix fo func args u show "eqFor s (AssignsLoc func args (GuardedUpd fo u)) (AndFor fo (AssignsLoc func args u))" by (simp add: eqFor_def Let_def) next case applySubstFor1 fix b subst show "eqFor s (AppSubstFor subst (Const b)) (Const b)" by (simp add: eqFor_def) next case applySubstFor2 fix fo1 fo2 subst show "eqFor s (AppSubstFor subst (AndFor fo1 fo2)) (AndFor (AppSubstFor subst fo1) (AppSubstFor subst fo2))" by (simp add: eqFor_def) next case applySubstFor3 fix fo subst show "eqFor s (AppSubstFor subst (NotFor fo)) (NotFor (AppSubstFor subst fo))" by (simp add: eqFor_def) next case applySubstFor4 fix te1 te2 subst show "eqFor s (AppSubstFor subst (Eq te1 te2)) (Eq (AppSubstTer subst te1) (AppSubstTer subst te2))" by (simp add: eqFor_def) next case applySubstFor4 fix te1 te2 subst show "eqFor s (AppSubstFor subst (Less te1 te2)) (Less (AppSubstTer subst te1) (AppSubstTer subst te2))" by (simp add: eqFor_def) next case applySubstFor5 fix fo subst show "eqFor s (AppSubstFor subst (ExQuan fo)) (ExQuan (AppSubstFor (bvShift subst) fo))" by (simp add: eqFor_def addVarValueBVShift) qed subsubsection {* Correctness for Rewriting of Updates *} lemma rewrUpdDirectCorrect: "(u1, u2) : rewrUpdDirect ==> eqUpd s u1 u2" proof (induct rule: rewrUpdDirect.induct) case applySubstUpd1 fix subst show "eqUpd s (AppSubstUpd subst Skip) Skip" by (simp add: eqUpd_def) next case applySubstUpd2 fix f subst args value show "eqUpd s (AppSubstUpd subst (ElUpd f args value)) (ElUpd f (terListMap (AppSubstTer subst) args) (AppSubstTer subst value))" by (simp add: eqUpd_def terListAppSubst) next case applySubstUpd3 fix subst u1 u2 show "eqUpd s (AppSubstUpd subst (ParUpd u1 u2)) (ParUpd (AppSubstUpd subst u1) (AppSubstUpd subst u2))" by (simp add: eqUpd_def) next case applySubstUpd4 fix subst u show "eqUpd s (AppSubstUpd subst (QuanUpd u)) (QuanUpd (AppSubstUpd (bvShift subst) u))" by (simp add: eqUpd_def addVarValueBVShift) next case applySubstUpd4 fix fo subst u show "eqUpd s (AppSubstUpd subst (GuardedUpd fo u)) (GuardedUpd (AppSubstFor subst fo) (AppSubstUpd subst u))" by (simp add: eqUpd_def) next case applyUpdUpd1 fix u show "eqUpd s (AppUpdUpd u Skip) Skip" by (simp add: eqUpd_def) next case applyUpdUpd2 fix f args u value show "eqUpd s (AppUpdUpd u (ElUpd f args value)) (ElUpd f (terListMap (AppUpdTer u) args) (AppUpdTer u value))" by (simp add: eqUpd_def Let_def terListAppUpd) next case applyUpdUpd3 fix u u1 u2 show "eqUpd s (AppUpdUpd u (ParUpd u1 u2)) (ParUpd (AppUpdUpd u u1) (AppUpdUpd u u2))" by (simp add: eqUpd_def) next case applyUpdUpd4 fix u u2 show "eqUpd s (AppUpdUpd u (QuanUpd u2)) (QuanUpd (AppUpdUpd (AppSubstUpd shiftSubst u) u2))" by (simp add: eqUpd_def) next case applyUpdUpd5 fix fo u u2 show "eqUpd s (AppUpdUpd u (GuardedUpd fo u2)) (GuardedUpd (AppUpdFor u fo) (AppUpdUpd u u2))" by (simp add: eqUpd_def) next fix u1 u2 show "eqUpd s (SeqUpd u1 u2) (ParUpd u1 (AppUpdUpd u1 u2))" by (simp add: eqUpd_def Let_def) next fix rejU show "eqUpd s (RejectUpd Skip rejU) Skip" by (simp add: eqUpd_def Let_def) next fix args f rejU value show "eqUpd s (RejectUpd (ElUpd f args value) rejU) (GuardedUpd (NotFor (AssignsLoc f args rejU)) (ElUpd f args value))" proof cases assume AS: "updVal s rejU (f, terListVal s args) = None" moreover have "(updVal s (RejectUpd (ElUpd f args value) rejU)) = (updVal s (GuardedUpd (NotFor (AssignsLoc f args rejU)) (ElUpd f args value)))" proof (rule ext) fix loc from AS show "(updVal s (RejectUpd (ElUpd f args value) rejU)) loc = (updVal s (GuardedUpd (NotFor (AssignsLoc f args rejU)) (ElUpd f args value))) loc" by (simp add: eqUpd_def Let_def) qed ultimately show ?thesis by (simp add: eqUpd_def Let_def) next assume AS: "updVal s rejU (f, terListVal s args) ~= None" moreover have "(updVal s (RejectUpd (ElUpd f args value) rejU)) = (updVal s (GuardedUpd (NotFor (AssignsLoc f args rejU)) (ElUpd f args value)))" proof (rule ext) fix loc from AS show "(updVal s (RejectUpd (ElUpd f args value) rejU)) loc = (updVal s (GuardedUpd (NotFor (AssignsLoc f args rejU)) (ElUpd f args value))) loc" by (simp add: eqUpd_def Let_def) qed ultimately show ?thesis by (simp add: eqUpd_def Let_def) qed next fix rejU u1 u2 have "(updVal s (RejectUpd (ParUpd u1 u2) rejU)) = (updVal s (ParUpd (RejectUpd u1 rejU) (RejectUpd u2 rejU)))" by (rule ext, simp add: Let_def overrideFuncUpd_def split: option.splits, auto) thus "eqUpd s (RejectUpd (ParUpd u1 u2) rejU) (ParUpd (RejectUpd u1 rejU) (RejectUpd u2 rejU))" by (simp add: eqUpd_def Let_def) next fix rejU u have "updVal s (RejectUpd (QuanUpd u) rejU) = updVal s (QuanUpd (RejectUpd u (AppSubstUpd shiftSubst rejU)))" proof (rule ext) fix loc let ?uValSimple = "%iv loc. updVal (addVarValue s iv) u loc" let ?uValCompl = "%iv loc. if updVal s rejU loc = None then updVal (addVarValue s iv) u loc else None" show "updVal s (RejectUpd (QuanUpd u) rejU) loc = updVal s (QuanUpd (RejectUpd u (AppSubstUpd shiftSubst rejU))) loc" proof cases assume "updVal s rejU loc = None" moreover hence "quanUpdComplete ?uValSimple loc = quanUpdComplete ?uValCompl loc" by (simp add: Let_def quanUpdCompleteMin) ultimately show ?thesis by (simp add: eqUpd_def Let_def) next assume "updVal s rejU loc ~= None" moreover hence "ALL iv. (?uValCompl iv loc = None)" by auto ultimately show ?thesis by (simp add: eqUpd_def Let_def quanUpdCompleteMin, auto) qed qed thus "eqUpd s (RejectUpd (QuanUpd u) rejU) (QuanUpd (RejectUpd u (AppSubstUpd shiftSubst rejU)))" by (simp add: eqUpd_def Let_def) next fix fo rejU u show "eqUpd s (RejectUpd (GuardedUpd fo u) rejU) (GuardedUpd fo (RejectUpd u rejU))" by (simp add: eqUpd_def Let_def) qed subsubsection {* Then the Whole Relation is Correct *} lemma rewrDirectCorrect : "syntRelFamCorrect s rewrDirect" by (simp add: syntRelFamCorrect_def rewrDirect_def rewrTerDirectCorrect rewrForDirectCorrect rewrUpdDirectCorrect) text {* By an existing lemma, also the monotonic closure of the rewriting relation is correct. *} lemma "syntRelFamCorrect s (rewrMono rewrDirect)" by (simp add: rewrMonoCorrect rewrDirectCorrect) subsection {* Reducible Terms, Formulas and Updates *} text {* An expression is called reducible'' if a rewriting step is possible. *} constdefs redRewrTer :: "ter => bool" "redRewrTer te == (EX te2. (te, te2) : syntRelTer (rewrMono rewrDirect))" constdefs redRewrTerList :: "terList => bool" "redRewrTerList args == (EX args2. (args, args2) : syntRelTerList (rewrMono rewrDirect))" constdefs redRewrFor :: "for => bool" "redRewrFor fo == (EX fo2. (fo, fo2) : syntRelFor (rewrMono rewrDirect))" constdefs redRewrUpd :: "update => bool" "redRewrUpd u == (EX u2. (u, u2) : syntRelUpd (rewrMono rewrDirect))" subsection {* Stupid Auxiliary Lemmas about Monotonic Closure of Rewriting Relation *} lemma [simp,intro] : "(te, te2) : rewrTerDirect ==> (te, te2) : syntRelTer (rewrMono rewrDirect)" by (simp add: rewrDirect_def rewrMono_def terRewrMonoSubset) lemma [simp,intro] : "(fo, fo2) : rewrForDirect ==> (fo, fo2) : syntRelFor (rewrMono rewrDirect)" by (simp add: rewrDirect_def rewrMono_def forRewrMonoSubset) lemma [simp,intro] : "(u, u2) : rewrUpdDirect ==> (u, u2) : syntRelUpd (rewrMono rewrDirect)" by (simp add: rewrDirect_def rewrMono_def updRewrMonoSubset) lemma [simp,intro] : "(te, te2) : rewrTerDirect ==> (te, te2) : terRewrMono rewrDirect" by (simp add: rewrDirect_def rewrMono_def terRewrMonoSubset) lemma [simp,intro] : "(fo, fo2) : rewrForDirect ==> (fo, fo2) : forRewrMono rewrDirect" by (simp add: rewrDirect_def rewrMono_def forRewrMonoSubset) lemma [simp,intro] : "(u, u2) : rewrUpdDirect ==> (u, u2) : updRewrMono rewrDirect" by (simp add: rewrDirect_def rewrMono_def updRewrMonoSubset) (* Terms, formulas that contain updates or substitutions ... *) consts usDirectTer :: "ter set" usDirectFor :: "for set" usDirectUpd :: "update set" inductive usDirectTer intros "AppUpdTer u te : usDirectTer" "AppUpdNonRec u func args : usDirectTer" "AppSubstTer subst te : usDirectTer" inductive usDirectFor intros "AppUpdFor u fo : usDirectFor" "AssignsLoc func args u : usDirectFor" "AppSubstFor subst fo : usDirectFor" inductive usDirectUpd intros "AppSubstUpd subst u : usDirectUpd" "AppUpdUpd u u2 : usDirectUpd" "RejectUpd u u2 : usDirectUpd" "SeqUpd u u2 : usDirectUpd" constdefs usDirect :: "tfuSet" "usDirect == (| terSet = usDirectTer, terListSet = {}, forSet = usDirectFor, updSet = usDirectUpd |)" lemma usDirectTerNonElHelp : "te : usDirectTer ==> te ~= AppVar n & te ~= AppFunc func args" by (induct "te" rule: usDirectTer.induct, auto) lemma updSubstUpdApplicable: " (ALL subst. (redRewrUpd (AppSubstUpd subst u))) & (ALL u2. (redRewrUpd (AppUpdUpd u2 u))) & (ALL u1 u2. (redRewrUpd (SeqUpd u1 u2))) & (ALL u2. (redRewrUpd (RejectUpd u u2)))" apply (induct u) apply (simp) apply (blast)+ apply (simp add: redRewrTer_def redRewrFor_def redRewrUpd_def rewrMono_def, (((blast intro: uMorphTer1 uMorphTer2 uMorphTer4 uMorphTer5 applyUpdToLoc1 applyUpdToLoc2 applyUpdToLoc3 applyUpdToLoc4 applyUpdToLoc5 applyUpdToLoc6 applySubstTer1 applySubstTer3 applySubstTer5 applySubstTer6 uMorphFor1 uMorphFor2 uMorphFor3 uMorphFor4 uMorphFor5 uMorphFor6 updLocs1 updLocs2 updLocs3 updLocs4 updLocs5 updLocs6 applySubstFor1 applySubstFor2 applySubstFor3 applySubstFor4 applySubstFor5 applySubstFor6 applySubstUpd1 applySubstUpd2 applySubstUpd3 applySubstUpd4 applySubstUpd5 applyUpdUpd1 applyUpdUpd2 applyUpdUpd3 applyUpdUpd4 applyUpdUpd5 rejectUpd1 rejectUpd2 rejectUpd3 rejectUpd4 rejectUpd5 seqUpd1) | (blast intro: terRewrMono1 terRewrMono3 terRewrMono4 terRewrMono5 terRewrMono6 terRewrMono7 terRewrMono8 terRewrMono9 terRewrMono11 terRewrMono12 terRewrMono13 terListRewrMono1 terListRewrMono2 forRewrMono1 forRewrMono2 forRewrMono3 forRewrMono4 forRewrMono5 forRewrMono6 forRewrMono7 forRewrMono8 forRewrMono9 forRewrMono11 forRewrMono12 forRewrMono13 forRewrMono14 forRewrMono15 updRewrMono1 updRewrMono2 updRewrMono4 updRewrMono5 updRewrMono6 updRewrMono7 updRewrMono8 updRewrMono9 updRewrMono10 updRewrMono11 updRewrMono12 updRewrMono13 updRewrMono14 updRewrMono15 updRewrMono16))?))+ done lemma updSubstTerApplicable: " (ALL u. (redRewrTer (AppUpdTer u te)) & (ALL subst. (redRewrTer (AppSubstTer subst te)))) & (ALL func args. (redRewrTer (AppUpdNonRec u func args)))" apply (induct te and u) prefer 8 prefer 10 defer 22 apply (simp) apply (simp) apply (simp add: redRewrTer_def redRewrFor_def redRewrUpd_def rewrMono_def, (((blast intro: uMorphTer1 uMorphTer2 uMorphTer4 uMorphTer5 applyUpdToLoc1 applyUpdToLoc2 applyUpdToLoc3 applyUpdToLoc4 applyUpdToLoc5 applyUpdToLoc6 applySubstTer1 applySubstTer3 applySubstTer5 applySubstTer6 uMorphFor1 uMorphFor2 uMorphFor3 uMorphFor4 uMorphFor5 uMorphFor6 updLocs1 updLocs2 updLocs3 updLocs4 updLocs5 updLocs6 applySubstFor1 applySubstFor2 applySubstFor3 applySubstFor4 applySubstFor5 applySubstFor6 applySubstUpd1 applySubstUpd2 applySubstUpd3 applySubstUpd4 applySubstUpd5 applyUpdUpd1 applyUpdUpd2 applyUpdUpd3 applyUpdUpd4 applyUpdUpd5 rejectUpd1 rejectUpd2 rejectUpd3 rejectUpd4 rejectUpd5 seqUpd1) | (blast intro: terRewrMono1 terRewrMono3 terRewrMono4 terRewrMono5 terRewrMono6 terRewrMono7 terRewrMono8 terRewrMono9 terRewrMono11 terRewrMono12 terRewrMono13 terListRewrMono1 terListRewrMono2 forRewrMono1 forRewrMono2 forRewrMono3 forRewrMono4 forRewrMono5 forRewrMono6 forRewrMono7 forRewrMono8 forRewrMono9 forRewrMono11 forRewrMono12 forRewrMono13 forRewrMono14 forRewrMono15 updRewrMono1 updRewrMono2 updRewrMono4 updRewrMono5 updRewrMono6 updRewrMono7 updRewrMono8 updRewrMono9 updRewrMono10 updRewrMono11 updRewrMono12 updRewrMono13 updRewrMono14 updRewrMono15 updRewrMono16))?))+ proof - fix update1 update2 have "redRewrUpd (AppUpdUpd update1 update2)" by (simp add: updSubstUpdApplicable) thus "ALL func args. EX te2. (AppUpdNonRec (AppUpdUpd update1 update2) func args, te2) : terRewrMono rewrDirect" by (simp add: redRewrTer_def redRewrUpd_def rewrMono_def, blast intro: terRewrMono8) next fix fun update have "redRewrUpd (AppSubstUpd fun update)" by (simp add: updSubstUpdApplicable) thus "ALL func args. redRewrTer (AppUpdNonRec (AppSubstUpd fun update) func args)" by (simp add: redRewrTer_def redRewrUpd_def rewrMono_def, blast intro: terRewrMono8) next fix update1 update2 have "redRewrUpd (SeqUpd update1 update2)" by (simp add: updSubstUpdApplicable) thus "ALL func args. redRewrTer (AppUpdNonRec (SeqUpd update1 update2) func args)" by (simp add: redRewrTer_def redRewrUpd_def rewrMono_def, blast intro: terRewrMono8) next fix update1 update2 have "redRewrUpd (RejectUpd update1 update2)" by (simp add: updSubstUpdApplicable) thus "ALL func args. redRewrTer (AppUpdNonRec (RejectUpd update1 update2) func args)" by (simp add: redRewrTer_def redRewrUpd_def rewrMono_def, blast intro: terRewrMono8) qed lemma updSubstForApplicable: " (ALL u. (redRewrFor (AppUpdFor u fo)) & (ALL subst. (redRewrFor (AppSubstFor subst fo)))) & (ALL func args. (redRewrFor (AssignsLoc func args u)))" apply (induct fo and u) defer 22 apply (simp) apply (blast)+ apply (simp add: redRewrTer_def redRewrFor_def redRewrUpd_def rewrMono_def, ((blast intro: uMorphTer1 uMorphTer2 uMorphTer4 uMorphTer5 applyUpdToLoc1 applyUpdToLoc2 applyUpdToLoc3 applyUpdToLoc4 applyUpdToLoc5 applyUpdToLoc6 applySubstTer1 applySubstTer3 applySubstTer5 applySubstTer6 uMorphFor1 uMorphFor2 uMorphFor3 uMorphFor4 uMorphFor5 uMorphFor6 updLocs1 updLocs2 updLocs3 updLocs4 updLocs5 updLocs6 applySubstFor1 applySubstFor2 applySubstFor3 applySubstFor4 applySubstFor5 applySubstFor6 applySubstUpd1 applySubstUpd2 applySubstUpd3 applySubstUpd4 applySubstUpd5 applyUpdUpd1 applyUpdUpd2 applyUpdUpd3 applyUpdUpd4 applyUpdUpd5 rejectUpd1 rejectUpd2 rejectUpd3 rejectUpd4 rejectUpd5 seqUpd1) | (blast intro: terRewrMono1 terRewrMono3 terRewrMono4 terRewrMono5 terRewrMono6 terRewrMono7 terRewrMono8 terRewrMono9 terRewrMono11 terRewrMono12 terRewrMono13 terListRewrMono1 terListRewrMono2 forRewrMono1 forRewrMono2 forRewrMono3 forRewrMono4 forRewrMono5 forRewrMono6 forRewrMono7 forRewrMono8 forRewrMono9 forRewrMono11 forRewrMono12 forRewrMono13 forRewrMono14 forRewrMono15 updRewrMono1 updRewrMono2 updRewrMono4 updRewrMono5 updRewrMono6 updRewrMono7 updRewrMono8 updRewrMono9 updRewrMono10 updRewrMono11 updRewrMono12 updRewrMono13 updRewrMono14 updRewrMono15 updRewrMono16)))+ proof - fix update1 update2 have "redRewrUpd (AppUpdUpd update1 update2)" by (simp add: updSubstUpdApplicable) thus "ALL func args. redRewrFor (AssignsLoc func args (AppUpdUpd update1 update2))" by (simp add: redRewrFor_def redRewrUpd_def rewrMono_def, blast intro: forRewrMono11) next fix fun update have "redRewrUpd (AppSubstUpd fun update)" by (simp add: updSubstUpdApplicable) thus "ALL func args. redRewrFor (AssignsLoc func args (AppSubstUpd fun update))" by (simp add: redRewrFor_def redRewrUpd_def rewrMono_def, blast intro: forRewrMono11) next fix update1 update2 have "redRewrUpd (SeqUpd update1 update2)" by (simp add: updSubstUpdApplicable) thus "ALL func args. redRewrFor (AssignsLoc func args (SeqUpd update1 update2))" by (simp add: redRewrFor_def redRewrUpd_def rewrMono_def, blast intro: forRewrMono11) next fix update1 update2 have "redRewrUpd (RejectUpd update1 update2)" by (simp add: updSubstUpdApplicable) thus "ALL func args. redRewrFor (AssignsLoc func args (RejectUpd update1 update2))" by (simp add: redRewrFor_def redRewrUpd_def rewrMono_def, blast intro: forRewrMono11) qed lemma redRewrTerDirect: "te : usDirectTer ==> redRewrTer te" by (rule usDirectTer.induct, simp_all add: updSubstTerApplicable) lemma redRewrForDirect: "fo : usDirectFor ==> redRewrFor fo" by (rule usDirectFor.induct, simp_all add: updSubstForApplicable) lemma redRewrUpdDirect: "u : usDirectUpd ==> redRewrUpd u" by (rule usDirectUpd.induct, simp_all add: updSubstUpdApplicable) lemma redRewrHelp: " (te : terMono usDirect --> redRewrTer te) & (args : terListMono usDirect --> redRewrTerList args) & (fo : forMono usDirect --> redRewrFor fo) & (u : updMono usDirect --> redRewrUpd u)" apply (rule terMono_terListMono_forMono_updMono.induct) apply (simp add: usDirect_def redRewrTerDirect) apply (simp add: usDirect_def) apply (simp add: usDirect_def redRewrForDirect) apply (simp add: usDirect_def redRewrUpdDirect) apply (simp add: redRewrTer_def redRewrTerList_def redRewrFor_def redRewrUpd_def rewrMono_def, blast intro: terRewrMono1 terRewrMono3 terRewrMono4 terRewrMono5 terRewrMono6 terRewrMono7 terRewrMono8 terRewrMono9 terRewrMono11 terRewrMono12 terRewrMono13 terListRewrMono1 terListRewrMono2 forRewrMono1 forRewrMono2 forRewrMono3 forRewrMono4 forRewrMono5 forRewrMono6 forRewrMono7 forRewrMono8 forRewrMono9 forRewrMono11 forRewrMono12 forRewrMono13 forRewrMono14 forRewrMono15 updRewrMono1 updRewrMono2 updRewrMono4 updRewrMono5 updRewrMono6 updRewrMono7 updRewrMono8 updRewrMono9 updRewrMono10 updRewrMono11 updRewrMono12 updRewrMono13 updRewrMono14 updRewrMono15 updRewrMono16)+ done lemma "te : terSet (tfuMono usDirect) ==> redRewrTer te" by (simp add: tfuMono_def redRewrHelp) lemma "args : terListSet (tfuMono usDirect) ==> redRewrTerList args" by (simp add: tfuMono_def redRewrHelp) lemma "fo : forSet (tfuMono usDirect) ==> redRewrFor fo" by (simp add: tfuMono_def redRewrHelp) lemma "u : updSet (tfuMono usDirect) ==> redRewrUpd u" by (simp add: tfuMono_def redRewrHelp) (* Change a variable assignment in one point *) constdefs changePoint :: "('a semStructure) => nat => 'a => ('a semStructure)" "changePoint struct x v == struct(| VarInter := (VarInter struct)(x:=v) |)" lemma changePoint_ineffective[simp] : "x ~= y ==> VarInter (changePoint s y val) x = VarInter s x" by (simp add: changePoint_def) lemma changePoint_ineffective2[simp] : "FuncInter (changePoint s x val) = FuncInter s" by (simp add: changePoint_def) lemma changePoint_commuteOverride[simp] : "overrideInter (changePoint s x val) upd = changePoint (overrideInter s upd) x val" by (simp add: changePoint_def overrideInter_def) lemma changePoint_elim[simp] : "changePoint (changePoint s x val1) x val2 = changePoint s x val2" by (simp add: changePoint_def overrideInter_def) lemma changePoint_commute[simp] : "x ~= y ==> changePoint (changePoint s x val1) y val2 = changePoint (changePoint s y val2) x val1" by (simp add: changePoint_def overrideInter_def, cases s, auto, rule ext, auto) lemma addVarValueChangePoint: "changePoint (addVarValue s val2) 0 val1 = addVarValue s val1" by (cases s, simp add: addVarValue_def changePoint_def, rule ext, simp add: shiftFun_def) lemma addVarValueChangePointCommute: "addVarValue (changePoint s n val1) val2 = changePoint (addVarValue s val2) (n+1) val1" by (cases s, simp add: addVarValue_def changePoint_def, rule ext, simp add: shiftFun_def, auto) (* Free variables of terms, formulas and updates Substitutions are not handled properly so far *) consts fvTer :: "ter => (nat set)" fvTerList :: "terList => (nat set)" fvFor :: "for => (nat set)" fvUpd :: "update => (nat set)" constdefs crossBinder :: "(nat set) => (nat set)" "crossBinder A == ({ n | n. n+1 : A })" primrec "fvTer (AppVar v) = {v}" "fvTer (AppFunc f args) = (fvTerList args)" "fvTer (AppUpdTer u te) = ((fvUpd u) Un (fvTer te))" "fvTer (IfThenTer fo te1 te2) = ((fvFor fo) Un (fvTer te1) Un (fvTer te2))" "fvTer (AppUpdNonRec u f args) = ((fvUpd u) Un (fvTerList args))" "fvTer (AppSubstTer subst target) = UNIV" (* "fvTer (AppSubstTer subst target) = (UN n : (fvTer target). (fvTer (subst n)))" *) "fvTer (MinTer fo) = (crossBinder (fvFor fo))" "fvTerList TerNIL = {}" "fvTerList (TerCons te args) = ((fvTer te) Un (fvTerList args))" "fvFor (Const b) = {}" "fvFor (AppUpdFor u fo) = ((fvUpd u) Un (fvFor fo))" "fvFor (AndFor fo1 fo2) = ((fvFor fo1) Un (fvFor fo2))" "fvFor (NotFor fo) = (fvFor fo)" "fvFor (Eq te1 te2) = ((fvTer te1) Un (fvTer te2))" "fvFor (Less te1 te2) = ((fvTer te1) Un (fvTer te2))" "fvFor (ExQuan fo) = (crossBinder (fvFor fo))" "fvFor (AssignsLoc f args u) = ((fvTerList args) Un (fvUpd u))" "fvFor (AppSubstFor subst target) = UNIV" (* "fvFor (AppSubstFor subst target) = (UN n : (fvFor target). (fvTer (subst n)))" *) "fvUpd (Skip) = {}" "fvUpd (ElUpd f args value) = ((fvTerList args) Un (fvTer value))" "fvUpd (ParUpd u1 u2) = ((fvUpd u1) Un (fvUpd u2))" "fvUpd (SeqUpd u1 u2) = ((fvUpd u1) Un (fvUpd u2))" "fvUpd (QuanUpd u) = (crossBinder (fvUpd u))" "fvUpd (GuardedUpd fo u) = ((fvFor fo) Un (fvUpd u))" "fvUpd (AppUpdUpd u1 u2) = ((fvUpd u1) Un (fvUpd u2))" "fvUpd (AppSubstUpd subst target) = UNIV" (* "fvUpd (AppSubstUpd subst target) = (UN n : (fvUpd target). (fvTer (subst n)))" *) "fvUpd (RejectUpd u1 u2) = ((fvUpd u1) Un (fvUpd u2))" lemma changePoint_ineffective3 : " (ALL x. ((x ~: (fvTer te)) --> (ALL s. (terVal (changePoint s x val) te) = (terVal s te)))) & (ALL x. ((x ~: (fvTerList args)) --> (ALL s. (terListVal (changePoint s x val) args) = (terListVal s args)))) & (ALL x. ((x ~: (fvFor fo)) --> (ALL s. (forVal (changePoint s x val) fo) = (forVal s fo)))) & (ALL x. ((x ~: (fvUpd u)) --> (ALL s. (updVal (changePoint s x val) u) = (updVal s u))))" by (induct te and args and fo and u, simp_all add: crossBinder_def Let_def addVarValueChangePointCommute) lemma changePointIneffUpd : "(x ~: (fvUpd u)) ==> updVal (changePoint s x val) u = updVal s u" by (simp add: changePoint_ineffective3) lemma changePointIneffTer : "(x ~: (fvTer te)) ==> terVal (changePoint s x val) te = terVal s te" by (simp add: changePoint_ineffective3) lemma changePointIneffTerList : "(x ~: (fvTerList args)) ==> terListVal (changePoint s x val) args = terListVal s args" by (simp add: changePoint_ineffective3) lemma changePointIneffFor : "(x ~: (fvFor fo)) ==> forVal (changePoint s x val) fo = forVal s fo" by (simp add: changePoint_ineffective3) (* Neutral and extremal elements of the update connectives *) consts neutralUpdEls :: "(update * update) set" inductive "neutralUpdEls" intros "(ParUpd Skip u, u) : neutralUpdEls" "(ParUpd u Skip, u) : neutralUpdEls" "(SeqUpd Skip u, u) : neutralUpdEls" "(SeqUpd u Skip, u) : neutralUpdEls" "(GuardedUpd fo Skip, Skip) : neutralUpdEls" "(GuardedUpd (Const False) u, Skip) : neutralUpdEls" "(GuardedUpd (Const True) u, u) : neutralUpdEls" "(QuanUpd Skip, Skip) : neutralUpdEls" "(0 ~: (fvUpd u)) ==> (QuanUpd u, AppSubstUpd shiftDownSubst u) : neutralUpdEls" lemma neutralUpdElsCorrect: "(u1, u2) : neutralUpdEls ==> eqUpd s u1 u2" proof (induct rule: neutralUpdEls.induct) fix u show "eqUpd s (ParUpd Skip u) u" by (simp add: eqUpd_def Let_def overrideFuncUpdNeutralLeft) next fix u show "eqUpd s (ParUpd u Skip) u" by (simp add: eqUpd_def Let_def overrideFuncUpdNeutralRight) next fix u show "eqUpd s (SeqUpd Skip u) u" by (simp add: eqUpd_def Let_def overrideFuncUpdNeutralLeft overrideInter_def overrideFuncInterNeutral) next fix u show "eqUpd s (SeqUpd u Skip) u" by (simp add: eqUpd_def Let_def overrideFuncUpdNeutralRight) next fix fo show "eqUpd s (GuardedUpd fo Skip) Skip" by (simp add: eqUpd_def Let_def) next fix u show "eqUpd s (GuardedUpd (Const False) u) Skip" by (simp add: eqUpd_def Let_def) next fix u show "eqUpd s (GuardedUpd (Const True) u) u" by (simp add: eqUpd_def Let_def) next show "eqUpd s (QuanUpd Skip) Skip" by (simp add: eqUpd_def Let_def, rule ext, simp add: quanUpdCompleteNone) next fix u let ?upds = "%iv. updVal (addVarValue s iv) u" assume "0 ~: fvUpd u" hence "ALL iv1 iv2. updVal (changePoint (addVarValue s iv1) 0 iv2) u = ?upds iv1" by (simp add: changePointIneffUpd) hence "ALL loc. ?upds (VarInter s 0) = ?upds (min {iv. ?upds iv loc ~= None})" by (simp add: addVarValueChangePoint) hence AS: "ALL loc. quanUpdComplete ?upds loc = ?upds (VarInter s 0) loc" by (simp add: quanUpdCompleteMin) have "quanUpdComplete ?upds = ?upds (VarInter s 0)" proof (rule ext) fix loc from AS show "quanUpdComplete ?upds loc = ?upds (VarInter s 0) loc" by blast qed thus "eqUpd s (QuanUpd u) (AppSubstUpd shiftDownSubst u)" by (simp add: eqUpd_def Let_def shiftDownSubstRed) qed (* Normalisation or transformation of Updates *) consts normUpdDirect :: "(update * update) set" inductive normUpdDirect intros "(GuardedUpd fo (QuanUpd u), QuanUpd (GuardedUpd (AppSubstFor shiftSubst fo) u)) : normUpdDirect" "(GuardedUpd fo (ParUpd u1 u2), ParUpd (GuardedUpd fo u1) (GuardedUpd fo u2)) : normUpdDirect" "(GuardedUpd fo1 (GuardedUpd fo2 u), GuardedUpd (AndFor fo1 fo2) u) : normUpdDirect" "(QuanUpd (ParUpd u1 u2), ParUpd (QuanUpd u1) (QuanUpd (RejectUpd u2 (QuanUpd (GuardedUpd (Less (AppVar 0) (AppVar 1)) (AppSubstUpd shiftKeepZeroSubst u1)))))) : normUpdDirect" "(ParUpd (QuanUpd u1) u2, QuanUpd (ParUpd u1 (AppSubstUpd shiftSubst u2))) : normUpdDirect" "(ParUpd u1 (ParUpd u2 u3), ParUpd (ParUpd u1 u2) u3) : normUpdDirect" "(SeqUpd u1 (SeqUpd u2 u3), SeqUpd (SeqUpd u1 u2) u3) : normUpdDirect" "(ParUpd u1 u2, ParUpd u2 (RejectUpd u1 u2)) : normUpdDirect" "(ParUpd u1 u2, ParUpd (RejectUpd u1 u2) u2) : normUpdDirect" "(u, ParUpd u (GuardedUpd fo u)) : normUpdDirect" "(u, ParUpd u (RejectUpd u rejU)) : normUpdDirect" (* Laws that didn't make it into the paper ... *) "(GuardedUpd (ExQuan fo) u, QuanUpd (GuardedUpd fo (AppSubstUpd shiftSubst u))) : normUpdDirect" "(QuanUpd u, QuanUpd (RejectUpd u (QuanUpd (GuardedUpd (Less (AppVar 0) (AppVar 1)) (AppSubstUpd shiftKeepZeroSubst u))))) : normUpdDirect" "(QuanUpd (QuanUpd u), QuanUpd (QuanUpd (RejectUpd (AppSubstUpd swapSubst u) (QuanUpd (GuardedUpd (Less (AppVar 0) (AppVar 1)) (AppSubstUpd shiftKeepZeroSubst (AppSubstUpd shiftKeepZeroSubst (QuanUpd u)))))))) : normUpdDirect" lemma rewrUpdDirectCorrect: "(u1, u2) : normUpdDirect ==> eqUpd s u1 u2" proof (induct rule: normUpdDirect.induct) fix fo u have "empty = quanUpdComplete (%iv. empty)" proof (rule ext) fix loc have "ALL loc iv. ((%iv. empty) iv loc = None)" by auto hence "quanUpdComplete (%iv. empty) loc = None" by (simp add: quanUpdCompleteNone) thus "None = quanUpdComplete (%iv. empty) loc" by auto qed thus "eqUpd s (GuardedUpd fo (QuanUpd u)) (QuanUpd (GuardedUpd (AppSubstFor shiftSubst fo) u))" by (simp add: eqUpd_def Let_def, auto) next fix fo u1 u2 show "eqUpd s (GuardedUpd fo (ParUpd u1 u2)) (ParUpd (GuardedUpd fo u1) (GuardedUpd fo u2))" by (simp add: eqUpd_def Let_def overrideFuncUpdNeutralRight) next fix fo1 fo2 u show "eqUpd s (GuardedUpd fo1 (GuardedUpd fo2 u)) (GuardedUpd (AndFor fo1 fo2) u)" by (simp add: eqUpd_def Let_def) next fix u1 u2 let ?before = "QuanUpd (ParUpd u1 u2)" let ?afterU2 = "RejectUpd u2 (QuanUpd (GuardedUpd (Less (AppVar 0) (AppVar 1)) (AppSubstUpd shiftKeepZeroSubst u1)))" let ?after = "ParUpd (QuanUpd u1) (QuanUpd ?afterU2)" let ?beforeUpds = "%iv. updVal (addVarValue s iv) (ParUpd u1 u2)" have "updVal s ?before = updVal s ?after" proof (rule ext) fix loc show "updVal s ?before loc = updVal s ?after loc" proof cases (************** First case: Update does not assign location "loc" *) assume AS: "updVal s ?before loc = None" hence AS2: "ALL iv. (?beforeUpds iv loc = None)" by (simp add: quanUpdCompleteNone Let_def) from AS2 have "updVal s (QuanUpd u1) loc = None" by (simp add: Let_def quanUpdCompleteNone, blast intro: parUpdNoneFirst) moreover from AS2 have "updVal s (QuanUpd (RejectUpd u2 (QuanUpd (GuardedUpd (Less (AppVar 0) (AppVar 1)) (AppSubstUpd shiftKeepZeroSubst u1))))) loc = None" by (simp add: Let_def quanUpdCompleteNone, blast intro: parUpdNoneSec) ultimately have "updVal s ?after loc = None" by (simp add: Let_def overrideFuncUpd_def) from this AS show ?thesis by auto next (************** Second case: Update assigns location "loc" value "val" *) let ?notNoneSet = "{iv. ?beforeUpds iv loc ~= None}" let ?minIV = "min ?notNoneSet" let ?rejSubUpd = "%iv2 iv. updVal (addVarValue (addVarValue s iv2) iv) (GuardedUpd (Less (AppVar 0) (AppVar 1)) (AppSubstUpd shiftKeepZeroSubst u1))" let ?rejUpd = "%iv2. updVal (addVarValue s iv2) (QuanUpd (GuardedUpd (Less (AppVar 0) (AppVar 1)) (AppSubstUpd shiftKeepZeroSubst u1)))" assume AS: "updVal s ?before loc ~= None" from this obtain val where beforeVal: "updVal s ?before loc = Some val" by auto from this AS have minIVVal: "?beforeUpds ?minIV loc = Some val" by (simp add: Let_def quanUpdCompleteMin) (* Work around some problems with simp: "nns" is set of individuals for which the quantified update assigns "loc" *) obtain nns where nnsDef: "nns = ?notNoneSet" by auto from minIVVal nnsDef have "nns ~= {}" by auto hence "ALL iv2 < (min nns). (iv2 ~: nns)" by (simp add: minIsMin) from this nnsDef have AS2: "ALL iv2 < (min nns). ?beforeUpds iv2 loc = None" by blast from AS2 have "ALL iv2 < (min nns). updVal (addVarValue s iv2) u1 loc = None" by (simp add: Let_def, blast intro: parUpdNoneFirst) from this nnsDef have u1NoneSmall: "ALL iv2 < ?minIV. updVal (addVarValue s iv2) u1 loc = None" by (simp) from AS2 have "ALL iv2 < (min nns). updVal (addVarValue s iv2) u2 loc = None" by (simp add: Let_def, blast intro: parUpdNoneSec) (* End of workaround *) from this nnsDef have u2NoneSmall: "ALL iv2 < ?minIV. updVal (addVarValue s iv2) u2 loc = None" by (simp) show ?thesis proof cases (* Case: the right update "u2" assigns "loc" only for bigger valuations than "u1". Then "u1" is the dominating update. The "reject" operator is then necessary to narrow "u2" *) assume AS2: "updVal (addVarValue s ?minIV) u2 loc = None" from this minIVVal have u1Val: "updVal (addVarValue s ?minIV) u1 loc = Some val" by (simp add: Let_def overrideFuncUpd_def) from u1Val u1NoneSmall have "?minIV = min {iv. updVal (addVarValue s iv) u1 loc ~= None}" by (simp add: minChar) from this u1Val have quanU1Val: "updVal s (QuanUpd u1) loc = Some val" by (simp add: Let_def quanUpdCompleteMin) (* Reject update is effective *) have "!! iv2. ?minIV < iv2 ==> ?rejSubUpd iv2 ?minIV loc ~= None" proof - fix iv2 assume AS: "?minIV < iv2" from AS u1Val show "?rejSubUpd iv2 ?minIV loc ~= None" by (simp add: Let_def shiftKeepZeroSubstRed Var0Val Var1Val) qed hence "!!iv2. ?minIV < iv2 ==> quanUpdComplete (?rejSubUpd iv2) loc ~= None" by (simp add: quanUpdCompleteNone, blast) hence rejUNotNone: "!! iv2. ?minIV < iv2 ==> ?rejUpd iv2 loc ~= None" by (simp add: Let_def) (* "u2" does therefore not contribute *) have "!! iv2. (updVal (addVarValue s iv2) ?afterU2 loc = None)" proof - fix iv2 show "updVal (addVarValue s iv2) ?afterU2 loc = None" proof cases assume "iv2 = ?minIV" from this AS2 show ?thesis by (simp add: Let_def) next assume unEq: "iv2 ~= ?minIV" show ?thesis proof cases assume "iv2 < ?minIV" from this u2NoneSmall show ?thesis by (simp add: Let_def) next assume "~(iv2 < ?minIV)" from this unEq have "?minIV < iv2" by auto from this rejUNotNone have "?rejUpd iv2 loc ~= None" by auto thus ?thesis by (simp add: Let_def, auto) qed qed qed hence "updVal s (QuanUpd ?afterU2) loc = None" by (simp add: Let_def quanUpdCompleteNone) from this quanU1Val beforeVal show ?thesis by (simp add: Let_def overrideFuncUpd_def) next (* Case: the right update "u2" assigns "loc" only for smaller or equally large valuations than "u1". Then "u2" is the dominating update. The "reject" operator has no effect *) assume AS2: "updVal (addVarValue s ?minIV) u2 loc ~= None" have u2Val: "updVal (addVarValue s ?minIV) u2 loc = Some val" proof - from AS2 obtain val2 where A: "updVal (addVarValue s ?minIV) u2 loc = Some val2" by auto hence B: "?beforeUpds ?minIV loc = Some val2" by (blast intro: parUpdSec) from A B minIVVal show ?thesis by auto qed (* Reject update is not effective *) have "ALL iv. ?rejSubUpd ?minIV iv loc = None" proof (rule allI) fix iv show "?rejSubUpd ?minIV iv loc = None" proof cases assume "iv < ?minIV" from this u1NoneSmall show "?rejSubUpd ?minIV iv loc = None" by (simp add: Let_def shiftKeepZeroSubstRed Var0Val Var1Val) next assume "~(iv < ?minIV)" from this u1NoneSmall show "?rejSubUpd ?minIV iv loc = None" by (simp add: Let_def shiftKeepZeroSubstRed Var0Val Var1Val) qed qed hence rejUpdNone: "?rejUpd ?minIV loc = None" by (simp add: quanUpdCompleteNone Let_def) let ?afterU2Val = "%iv. (updVal (addVarValue s iv) ?afterU2)" from u2Val rejUpdNone have afterU2Val: "?afterU2Val ?minIV loc = Some val" by (simp add: Let_def) from u2NoneSmall have "ALL iv2 < ?minIV. ?afterU2Val iv2 loc = None" by (simp add: Let_def) from this afterU2Val have "?minIV = min {iv. ?afterU2Val iv loc ~= None}" by (simp add: minChar) hence "quanUpdComplete ?afterU2Val loc = ?afterU2Val ?minIV loc" by (simp add: quanUpdCompleteMin) from this afterU2Val have "updVal s (QuanUpd ?afterU2) loc = Some val" by (simp add: Let_def) hence "updVal s ?after loc = Some val" by (blast intro: parUpdSec) from this beforeVal show ?thesis by auto qed qed qed thus "eqUpd s ?before ?after" by (simp add: eqUpd_def) next fix u1 u2 have "updVal s (ParUpd (QuanUpd u1) u2) = updVal s (QuanUpd (ParUpd u1 (AppSubstUpd shiftSubst u2)))" proof (rule ext) fix loc show "updVal s (ParUpd (QuanUpd u1) u2) loc = updVal s (QuanUpd (ParUpd u1 (AppSubstUpd shiftSubst u2))) loc" proof cases assume AS: "updVal s u2 loc = None" from AS have "ALL iv. (updVal (addVarValue s iv) (ParUpd u1 (AppSubstUpd shiftSubst u2)) loc = updVal (addVarValue s iv) u1 loc)" by (simp add: Let_def overrideFuncUpd_def) hence "updVal s (QuanUpd (ParUpd u1 (AppSubstUpd shiftSubst u2))) loc = updVal s (QuanUpd u1) loc" by (simp add: Let_def quanUpdCompleteMin) moreover from AS have "updVal s (ParUpd (QuanUpd u1) u2) loc = updVal s (QuanUpd u1) loc" by (simp add: Let_def overrideFuncUpd_def) ultimately show ?thesis by auto next assume "updVal s u2 loc ~= None" from this obtain val where AS: "updVal s u2 loc = Some val" by auto have "ALL iv. (updVal (addVarValue s iv) (ParUpd u1 (AppSubstUpd shiftSubst u2)) loc = Some val)" proof (rule allI) fix iv from AS have "updVal (addVarValue s iv) (AppSubstUpd shiftSubst u2) loc = Some val" by auto thus "updVal (addVarValue s iv) (ParUpd u1 (AppSubstUpd shiftSubst u2)) loc = Some val" by (rule parUpdSec) qed hence "updVal s (QuanUpd (ParUpd u1 (AppSubstUpd shiftSubst u2))) loc = Some val" by (simp add: quanUpdCompleteMin Let_def) moreover from AS have "updVal s (ParUpd (QuanUpd u1) u2) loc = Some val" by (rule parUpdSec) ultimately show ?thesis by auto qed qed thus "eqUpd s (ParUpd (QuanUpd u1) u2) (QuanUpd (ParUpd u1 (AppSubstUpd shiftSubst u2)))" by (simp add: eqUpd_def) next fix u1 u2 u3 show "eqUpd s (ParUpd u1 (ParUpd u2 u3)) (ParUpd (ParUpd u1 u2) u3)" by (simp add: eqUpd_def Let_def overrideFuncUpdAssoc) next fix u1 u2 u3 show "eqUpd s (SeqUpd u1 (SeqUpd u2 u3)) (SeqUpd (SeqUpd u1 u2) u3)" by (simp add: eqUpd_def Let_def overrideInter_def overrideFuncUpdAssoc overrideFuncInterAssoc, cases s, auto) next fix u1 u2 have "updVal s (ParUpd u1 u2) = updVal s (ParUpd u2 (RejectUpd u1 u2))" by (rule ext, simp add: eqUpd_def Let_def overrideFuncUpd_def split: option.splits) thus "eqUpd s (ParUpd u1 u2) (ParUpd u2 (RejectUpd u1 u2))" by(simp add: eqUpd_def) next fix u1 u2 have "updVal s (ParUpd u1 u2) = updVal s (ParUpd (RejectUpd u1 u2) u2)" by (rule ext, simp add: eqUpd_def Let_def overrideFuncUpd_def split: option.splits) thus "eqUpd s (ParUpd u1 u2) (ParUpd (RejectUpd u1 u2) u2)" by(simp add: eqUpd_def) next fix fo u have "updVal s u = updVal s (ParUpd u (GuardedUpd fo u))" by (rule ext, simp add: Let_def overrideFuncUpdIdem overrideFuncUpdNeutralRight) thus "eqUpd s u (ParUpd u (GuardedUpd fo u))" by (simp add: eqUpd_def) next fix rejU u have "updVal s u = updVal s (ParUpd u (RejectUpd u rejU))" by (rule ext, simp add: Let_def overrideFuncUpd_def split: option.splits) thus "eqUpd s u (ParUpd u (RejectUpd u rejU))" by (simp add: eqUpd_def) next fix u let ?before = "QuanUpd u" let ?after = "QuanUpd (RejectUpd u (QuanUpd (GuardedUpd (Less (AppVar 0) (AppVar 1)) (AppSubstUpd shiftKeepZeroSubst u))))" let ?beforeUpds = "%iv. updVal (addVarValue s iv) u" let ?afterUpds = "%iv. updVal (addVarValue s iv) (RejectUpd u (QuanUpd (GuardedUpd (Less (AppVar 0) (AppVar 1)) (AppSubstUpd shiftKeepZeroSubst u))))" have "updVal s ?before = updVal s ?after" proof (rule ext) fix loc show "updVal s ?before loc = updVal s ?after loc" proof cases assume "updVal s ?before loc = None" moreover hence "ALL iv. (?beforeUpds iv loc = None)" by (simp add: quanUpdCompleteNone Let_def) hence "ALL iv. (?afterUpds iv loc = None)" by (simp add: Let_def) hence "updVal s ?after loc = None" by (simp add: quanUpdCompleteNone Let_def) ultimately show ?thesis by auto next let ?notNoneSet = "{iv. ?beforeUpds iv loc ~= None}" let ?minIV = "min ?notNoneSet" assume AS: "updVal s ?before loc ~= None" from this obtain val where beforeVal: "updVal s ?before loc = Some val" by auto from this AS have minIVVal: "?beforeUpds ?minIV loc = Some val" by (simp add: Let_def quanUpdCompleteMin) obtain nns where nnsDef: "nns = ?notNoneSet" by auto from minIVVal nnsDef have "nns ~= {}" by auto hence "ALL iv2 < (min nns). (iv2 ~: nns)" by (simp add: minIsMin) from this nnsDef have UNoneSmall: "ALL iv2 < (min nns). ?beforeUpds iv2 loc = None" by blast let ?rejSubUpd = "%iv2 iv. updVal (addVarValue (addVarValue s iv2) iv) (GuardedUpd (Less (AppVar 0) (AppVar 1)) (AppSubstUpd shiftKeepZeroSubst u))" have "!! iv2. ?rejSubUpd ?minIV iv2 loc = None" proof - fix iv2 show "?rejSubUpd ?minIV iv2 loc = None" proof cases assume "iv2 < min nns" from this UNoneSmall show ?thesis by (simp add: Let_def Var0Val Var1Val shiftKeepZeroSubstRed) next assume "~ iv2 < min nns" from this show ?thesis by (simp add: Let_def Var0Val Var1Val shiftKeepZeroSubstRed nnsDef) qed qed hence "updVal (addVarValue s ?minIV) (QuanUpd (GuardedUpd (Less (AppVar 0) (AppVar 1)) (AppSubstUpd shiftKeepZeroSubst u))) loc = None" by (simp add: quanUpdCompleteNone Let_def) from this minIVVal have afterVal: "?afterUpds ?minIV loc = Some val" by (simp add: Let_def) from UNoneSmall have "ALL iv2 < (min nns). ?afterUpds iv2 loc = None" by (simp add: Let_def) from this nnsDef have "ALL iv2 < ?minIV. ?afterUpds iv2 loc = None" by (simp) from this afterVal have "?minIV = min {iv. ?afterUpds iv loc ~= None}" by (simp add: minChar) hence "quanUpdComplete ?afterUpds loc = ?afterUpds ?minIV loc" by (simp add: quanUpdCompleteMin) from this afterVal have "updVal s ?after loc = Some val" by (simp add: Let_def) from this beforeVal show ?thesis by auto qed qed thus "eqUpd s ?before ?after" by (simp add: eqUpd_def) next fix fo u let ?afterUpds = "%iv. updVal (addVarValue s iv) (GuardedUpd fo (AppSubstUpd shiftSubst u))" have "updVal s (GuardedUpd (ExQuan fo) u) = updVal s (QuanUpd (GuardedUpd fo (AppSubstUpd shiftSubst u)))" proof cases assume AS: "forVal s (ExQuan fo) = False" have "updVal s (QuanUpd (GuardedUpd fo (AppSubstUpd shiftSubst u))) = empty" proof (rule ext) fix loc from AS show "updVal s (QuanUpd (GuardedUpd fo (AppSubstUpd shiftSubst u))) loc = None" by (simp add: quanUpdCompleteNone Let_def) qed from this AS show ?thesis by (simp add: Let_def) next assume AS: "forVal s (ExQuan fo) ~= False" from this obtain goodIV where "forVal (addVarValue s goodIV) fo = True" by auto hence goodIVgood: "?afterUpds goodIV = updVal s u" by (simp add: Let_def) have "quanUpdComplete ?afterUpds = updVal s u" proof (rule ext) fix loc let ?afterNNS = "{iv. ?afterUpds iv loc ~= None}" have qucChar: "quanUpdComplete ?afterUpds loc = ?afterUpds (min ?afterNNS) loc" by (simp add: quanUpdCompleteMin) moreover have "?afterUpds (min ?afterNNS) loc = updVal s u loc" proof cases assume AS: "?afterUpds (min ?afterNNS) loc = None" from this qucChar have "ALL iv. (?afterUpds iv loc = None)" by (simp add: quanUpdCompleteNone) hence "?afterUpds goodIV loc = None" by auto from this AS goodIVgood show ?thesis by auto next assume "?afterUpds (min ?afterNNS) loc ~= None" moreover have "ALL iv. (?afterUpds iv loc ~= None --> ?afterUpds iv loc = updVal s u loc)" by (simp add: Let_def) ultimately show "?afterUpds (min ?afterNNS) loc = updVal s u loc" by auto qed ultimately show "quanUpdComplete ?afterUpds loc = updVal s u loc" by auto qed from this AS show ?thesis by (simp add: Let_def) qed thus "eqUpd s (GuardedUpd (ExQuan fo) u) (QuanUpd (GuardedUpd fo (AppSubstUpd shiftSubst u)))" by (simp add: eqUpd_def) next fix u let ?beforeUpds1 = "%iv. updVal (addVarValue s iv) (QuanUpd u)" let ?beforeUpds2 = "%iv iv2. updVal (addVarValue (addVarValue s iv) iv2) u" let ?before = "(QuanUpd (QuanUpd u))" let ?afterRej = "RejectUpd (AppSubstUpd swapSubst u) (QuanUpd (GuardedUpd (Less (AppVar 0) (AppVar 1)) (AppSubstUpd shiftKeepZeroSubst (AppSubstUpd shiftKeepZeroSubst (QuanUpd u)))))" let ?after = "QuanUpd (QuanUpd ?afterRej)" let ?afterUpds2 = "%iv iv2. updVal (addVarValue (addVarValue s iv) iv2) ?afterRej" let ?afterUpds1 = "%iv2. updVal (addVarValue s iv2) (QuanUpd ?afterRej)" let ?rejSubUpd = "%iv iv2 ivPrime. updVal (addVarValue (addVarValue (addVarValue s iv2) iv) ivPrime) (GuardedUpd (Less (AppVar 0) (AppVar 1)) (AppSubstUpd shiftKeepZeroSubst (AppSubstUpd shiftKeepZeroSubst (QuanUpd u))))" let ?rejUpd = "%iv iv2. updVal (addVarValue (addVarValue s iv2) iv) (QuanUpd (GuardedUpd (Less (AppVar 0) (AppVar 1)) (AppSubstUpd shiftKeepZeroSubst (AppSubstUpd shiftKeepZeroSubst (QuanUpd u)))))" have "updVal s ?before = updVal s ?after" proof (rule ext) fix loc show "updVal s ?before loc = updVal s ?after loc" proof cases (************** First case: Update does not assign location "loc" *) assume AS: "updVal s ?before loc = None" hence "ALL iv. (?beforeUpds1 iv loc = None)" by (simp add: quanUpdCompleteNone Let_def) hence "ALL iv iv2. (?beforeUpds2 iv iv2 loc = None)" by (simp add: quanUpdCompleteNone Let_def) hence AS2: "ALL iv iv2. ?afterUpds2 iv2 iv loc = None" by (simp add: Let_def swapSubst_def swapSubstAddVar) hence "ALL iv. (?afterUpds1 iv loc = None)" by (simp add: quanUpdCompleteNone Let_def) hence "updVal s ?after loc = None" by (simp add: quanUpdCompleteNone Let_def) from this AS show ?thesis by auto next (************** Second case: Update assigns location "loc" value "val" *) let ?notNoneSet1 = "{iv. ?beforeUpds1 iv loc ~= None}" let ?minIV1 = "min ?notNoneSet1" let ?notNoneSet2 = "{iv. ?beforeUpds2 ?minIV1 iv loc ~= None}" let ?minIV2 = "min ?notNoneSet2" assume AS: "updVal s ?before loc ~= None" from this obtain val where beforeVal: "updVal s ?before loc = Some val" by auto from this AS have minIV1Val: "?beforeUpds1 ?minIV1 loc = Some val" by (simp add: Let_def quanUpdCompleteMin) from this AS have minIV2Val: "?beforeUpds2 ?minIV1 ?minIV2 loc = Some val" by (simp add: Let_def quanUpdCompleteMin) (* Work around some problems with simp: "nns1" is set of individuals for which the quantified update "?beforeUpds1" assigns "loc" *) obtain nns1 where nns1Def: "nns1 = ?notNoneSet1" by auto from minIV1Val nns1Def have "nns1 ~= {}" by auto hence "ALL iv < (min nns1). (iv ~: nns1)" by (simp add: minIsMin) from this nns1Def have "ALL iv < (min nns1). ?beforeUpds1 iv loc = None" by blast hence iv1NoneSmallNNS: "ALL iv iv2. (iv < (min nns1) --> ?beforeUpds2 iv iv2 loc = None)" by (simp add: Let_def quanUpdCompleteNone) from this nns1Def have iv1NoneSmall: "ALL iv iv2. (iv < ?minIV1 --> ?beforeUpds2 iv iv2 loc = None)" by (simp) (* Work around some problems with simp: "nns2" is set of individuals for which the quantified update "?beforeUpds2" assigns "loc" *) obtain nns2 where nns2Def: "nns2 = ?notNoneSet2" by auto from minIV2Val nns2Def have "nns2 ~= {}" by auto hence "ALL iv2 < (min nns2). (iv2 ~: nns2)" by (simp add: minIsMin) from this nns1Def nns2Def have "ALL iv2 < (min nns2). ?beforeUpds2 (min nns1) iv2 loc = None" by blast hence iv2NoneSmallNNS: "ALL iv2 < (min nns2). (?beforeUpds2 (min nns1) iv2 loc = None)" by (simp add: Let_def quanUpdCompleteNone) from this nns1Def nns2Def have iv2NoneSmall: "ALL iv2 < ?minIV2. (?beforeUpds2 ?minIV1 iv2 loc = None)" by (blast) (* The (unquantified) update on the right side has the right value *) have afterVal2NNS: "?afterUpds2 (min nns2) (min nns1) loc = Some val" proof - have "ALL ivPrime. ?rejSubUpd (min nns1) (min nns2) ivPrime loc = None" proof (rule allI) fix ivPrime show "?rejSubUpd (min nns1) (min nns2) ivPrime loc = None" proof cases assume "ivPrime < (min nns1)" from this iv1NoneSmallNNS show ?thesis by (simp add: Let_def Var0Val Var1Val shiftKeepZeroSubstRed quanUpdCompleteNone) next assume "~ ivPrime < (min nns1)" thus ?thesis by (simp add: Let_def Var0Val Var1Val) qed qed hence "?rejUpd (min nns1) (min nns2) loc = None" by (simp add: Let_def quanUpdCompleteNone) hence "?afterUpds2 (min nns2) (min nns1) loc = ?beforeUpds2 (min nns1) (min nns2) loc" by (simp add: Let_def Var0Val Var1Val swapSubst_def swapSubstAddVar) from this minIV2Val nns1Def nns2Def show ?thesis by auto qed from iv1NoneSmallNNS have "ALL iv < (min nns1). (?afterUpds2 (min nns2) iv loc = None)" by (simp add: Let_def swapSubst_def swapSubstAddVar) from this afterVal2NNS have "min nns1 = min {iv. ?afterUpds2 (min nns2) iv loc ~= None}" by (simp add: minChar) hence "quanUpdComplete (?afterUpds2 (min nns2)) loc = ?afterUpds2 (min nns2) (min nns1) loc" by (simp add: quanUpdCompleteMin) (* The (half-quantified) update on the right side has the right value *) from this afterVal2NNS have afterVal1NNS: "?afterUpds1 (min nns2) loc = Some val" by (simp add: Let_def) have "ALL iv iv2. (iv2 < (min nns2) --> ?afterUpds2 iv2 iv loc = None)" proof (rule allI, rule allI, rule impI) fix iv iv2 assume iv2Small: "iv2 < (min nns2)" show "?afterUpds2 iv2 iv loc = None" proof cases assume "iv < (min nns1)" from this iv1NoneSmallNNS show ?thesis by (simp add: Let_def swapSubst_def swapSubstAddVar) next assume ivNotSmall: "~ iv < (min nns1)" show ?thesis proof cases assume "iv = (min nns1)" from this iv2Small iv2NoneSmallNNS show ?thesis by (simp add: Let_def swapSubst_def swapSubstAddVar) next assume "iv ~= (min nns1)" from this ivNotSmall have ivBig: "min nns1 < iv" by auto (* Reject update ensures that changing the order of executing the updates is possible without changing the value of the update as a whole *) from minIV1Val nns1Def have "?beforeUpds1 (min nns1) loc = Some val" by auto from this ivBig have "?rejSubUpd iv iv2 (min nns1) loc ~= None" by (simp add: Let_def shiftKeepZeroSubstRed Var0Val Var1Val) hence "quanUpdComplete (?rejSubUpd iv iv2) loc ~= None" by (simp add: quanUpdCompleteNone, blast) hence rejUNotNone: "?rejUpd iv iv2 loc ~= None" by (simp add: Let_def) thus ?thesis by (simp add: Let_def shiftKeepZeroSubstRed, auto) qed qed qed hence "ALL iv2. (iv2 < (min nns2) --> ?afterUpds1 iv2 loc = None)" by (simp add: quanUpdCompleteNone Let_def) from this afterVal1NNS have "min nns2 = min {iv2. ?afterUpds1 iv2 loc ~= None}" by (simp add: minChar) hence "quanUpdComplete ?afterUpds1 loc = ?afterUpds1 (min nns2) loc" by (simp add: quanUpdCompleteMin) from this afterVal1NNS have "updVal s ?after loc = Some val" by (simp add: Let_def) from this beforeVal show ?thesis by auto qed qed thus "eqUpd s ?before ?after" by (simp add: eqUpd_def) qed (* Different semantic equivalence relations on terms, formulas, updates *) (* Call terms, formulas and updates equivalent if their evaluations in all structures (for a certain, fixed universe) coincide *) constdefs semEquivalence :: "(('a::universe) semStructure) => syntRelFam" "semEquivalence (t::(('a::universe) semStructure)) == (| syntRelTer = { (te1, te2). (ALL s::(('a::universe) semStructure). eqTer s te1 te2) }, syntRelTerList = { (args1, args2). (ALL s::(('a::universe) semStructure). eqTerList s args1 args2) }, syntRelFor = { (fo1, fo2). (ALL s::(('a::universe) semStructure). eqFor s fo1 fo2) }, syntRelUpd = { (upd1, upd2). (ALL s::(('a::universe) semStructure). eqUpd s upd1 upd2) } |)" (* Not surprisingly, the relation preserves the meaning of expressions *) lemma "syntRelFamCorrect s (semEquivalence s)" by (simp add: syntRelFamCorrect_def semEquivalence_def) (* The equivalence is also a congruence relation *) lemma "rewrMono (semEquivalence s) = semEquivalence s" proof - have subset: "!!te1 te2 tl1 tl2 fo1 fo2 u1 u2. let se = semEquivalence s in ( ((te1, te2) : syntRelTer (rewrMono se) --> (te1, te2) : syntRelTer se) & ((tl1, tl2) : syntRelTerList (rewrMono se) --> (tl1, tl2) : syntRelTerList se) & ((fo1, fo2) : syntRelFor (rewrMono se) --> (fo1, fo2) : syntRelFor se) & ((u1, u2) : syntRelUpd (rewrMono se) --> (u1, u2) : syntRelUpd se) )" proof - fix te1 te2 tl1 tl2 fo1 fo2 u1 u2 show "let se = semEquivalence s in ( ((te1, te2) : syntRelTer (rewrMono se) --> (te1, te2) : syntRelTer se) & ((tl1, tl2) : syntRelTerList (rewrMono se) --> (tl1, tl2) : syntRelTerList se) & ((fo1, fo2) : syntRelFor (rewrMono se) --> (fo1, fo2) : syntRelFor se) & ((u1, u2) : syntRelUpd (rewrMono se) --> (u1, u2) : syntRelUpd se) )" apply (simp add: Let_def rewrMono_def) apply (rule terRewrMono_terListRewrMono_forRewrMono_updRewrMono.induct) apply (simp_all add: semEquivalence_def eqTer_def eqTerList_def eqUpd_def eqFor_def rewrMonoCorrectHelpHelp) done qed from subset have "syntRelTer (rewrMono (semEquivalence s)) = syntRelTer (semEquivalence s)" by (auto, simp add: Let_def, simp add: rewrMono_def Let_def, blast intro: terRewrMonoSubset) moreover from subset have "syntRelFor (rewrMono (semEquivalence s)) = syntRelFor (semEquivalence s)" by (auto, simp add: Let_def, simp add: rewrMono_def Let_def, blast intro: forRewrMonoSubset) moreover from subset have "syntRelTerList (rewrMono (semEquivalence s)) = syntRelTerList (semEquivalence s)" by (auto, simp add: Let_def, simp add: rewrMono_def Let_def, blast intro: terListRewrMonoSubset) moreover from subset have "syntRelUpd (rewrMono (semEquivalence s)) = syntRelUpd (semEquivalence s)" by (auto, simp add: Let_def, simp add: rewrMono_def Let_def, blast intro: updRewrMonoSubset) ultimately show ?thesis by (auto) qed (* Equivalence modulo definedness *) constdefs idUpd :: "(('a::universe) semStructure) => ('a funcUpd)" "idUpd s loc == Some (FuncInter s loc)" constdefs makeTotal :: "(('a::universe) semStructure) => ('a funcUpd) => ('a funcUpd)" "makeTotal s fu == overrideFuncUpd (idUpd s) fu" constdefs eqUpdModDef :: "(('a::universe) semStructure) => update => update => bool" "eqUpdModDef s u1 u2 == (makeTotal s (updVal s u1) = makeTotal s (updVal s u2))" lemma "eqUpd s u1 u2 ==> eqUpdModDef s u1 u2" by (simp add: eqUpd_def eqUpdModDef_def) constdefs eqUpdModDefUniv :: "(('a::universe) semStructure) => (update * update) set" "eqUpdModDefUniv (t::(('a::universe) semStructure)) == { (u1, u2). (ALL s::(('a::universe) semStructure). eqUpdModDef s u1 u2) }" lemma congrUpdModDefOverrideInter: "eqUpdModDef (s::(('a::universe) semStructure)) u1 u2 ==> overrideInter s (updVal s u1) = overrideInter s (updVal s u2)" proof - assume "eqUpdModDef s u1 u2" hence "overrideInter s (makeTotal s (updVal s u1)) = overrideInter s (makeTotal s (updVal s u2))" by (simp add: eqUpdModDef_def) moreover have "ALL u. (overrideInter s (makeTotal s (updVal s u)) = overrideInter s (updVal s u))" proof (rule allI) fix u have "VarInter (overrideInter s (makeTotal s (updVal s u))) = VarInter (overrideInter s (updVal s u))" by (simp add: overrideInter_def) moreover have "FuncInter (overrideInter s (makeTotal s (updVal s u))) = FuncInter (overrideInter s (updVal s u))" by (rule ext, simp add: overrideInter_def overrideFuncInter_def overrideFuncUpd_def idUpd_def makeTotal_def split: option.splits) ultimately show "overrideInter s (makeTotal s (updVal s u)) = overrideInter s (updVal s u)" by (cases s, simp add: overrideInter_def) qed ultimately show ?thesis by auto qed lemma updModDefTerVal: "(u1, u2) : eqUpdModDefUniv (t::(('a::universe) semStructure)) ==> terVal (s::(('a::universe) semStructure)) (AppUpdTer u1 ter) = terVal (s::(('a::universe) semStructure)) (AppUpdTer u2 ter)" proof - assume "(u1, u2) : eqUpdModDefUniv (t::(('a::universe) semStructure))" hence "overrideInter s (updVal s u1) = overrideInter s (updVal s u2)" by (simp add: eqUpdModDefUniv_def congrUpdModDefOverrideInter) thus ?thesis by auto qed lemma updModDefForVal: "(u1, u2) : eqUpdModDefUniv (t::(('a::universe) semStructure)) ==> forVal (s::(('a::universe) semStructure)) (AppUpdFor u1 fo) = forVal (s::(('a::universe) semStructure)) (AppUpdFor u2 fo)" proof - assume "(u1, u2) : eqUpdModDefUniv (t::(('a::universe) semStructure))" hence "overrideInter s (updVal s u1) = overrideInter s (updVal s u2)" by (simp add: eqUpdModDefUniv_def congrUpdModDefOverrideInter) thus ?thesis by auto qed lemma updModDefUpdVal: "(u1, u2) : eqUpdModDefUniv (t::(('a::universe) semStructure)) ==> updVal (s::(('a::universe) semStructure)) (AppUpdUpd u1 upd) = updVal (s::(('a::universe) semStructure)) (AppUpdUpd u2 upd)" proof - assume "(u1, u2) : eqUpdModDefUniv (t::(('a::universe) semStructure))" hence "overrideInter s (updVal s u1) = overrideInter s (updVal s u2)" by (simp add: eqUpdModDefUniv_def congrUpdModDefOverrideInter) thus ?thesis by auto qed (* Assignments that are equivalent to skip modulo definedness *) lemma "eqUpdModDef s (ElUpd f args (AppFunc f args)) Skip" by (simp add: eqUpdModDef_def makeTotal_def Let_def, rule ext, simp add: overrideFuncUpd_def idUpd_def) (* Characterisation of the functions that equivalence modulo definedness is a congruence for *) consts congrUpdModDef :: "(update * update) set => (update * update) set" inductive "congrUpdModDef rel" intros congrUpdModDefSubset: "(a, b) : rel ==> (a, b) : congrUpdModDef rel" "(u, ub) : congrUpdModDef rel ==> (ParUpd u u2, ParUpd ub u2) : congrUpdModDef rel" "(u, ub) : congrUpdModDef rel ==> (SeqUpd u u2, SeqUpd ub u2) : congrUpdModDef rel" "(u, ub) : congrUpdModDef rel ==> (SeqUpd u2 u, SeqUpd u2 ub) : congrUpdModDef rel" "(u, ub) : congrUpdModDef rel ==> (GuardedUpd fo u, GuardedUpd fo ub) : congrUpdModDef rel" "(u, Skip) : congrUpdModDef rel ==> (QuanUpd u, Skip) : congrUpdModDef rel" lemma "congrUpdModDef (eqUpdModDefUniv (t::(('a::universe) semStructure))) = eqUpdModDefUniv t" proof - have subset: "!!u1 u2. ((u1, u2) : congrUpdModDef (eqUpdModDefUniv t) --> (u1, u2) : eqUpdModDefUniv t)" proof - fix u1 u2 have "(u1, u2) : congrUpdModDef (eqUpdModDefUniv t) ==> (u1, u2) : eqUpdModDefUniv t" apply (rule congrUpdModDef.induct) apply (simp_all add: eqUpdModDefUniv_def) apply (auto) proof - fix u ub u2 fix s :: "(('a::universe) semStructure)" assume "ALL (t::(('a::universe) semStructure)). eqUpdModDef t u ub" thus "eqUpdModDef s (ParUpd u u2) (ParUpd ub u2)" by (simp add: eqUpdModDef_def makeTotal_def Let_def overrideFuncUpdAssoc) next fix u ub u2 fix s :: "(('a::universe) semStructure)" assume "ALL (t::(('a::universe) semStructure)). eqUpdModDef t u ub" moreover hence "(overrideInter s (updVal s u)) = (overrideInter s (updVal s ub))" by (simp add: congrUpdModDefOverrideInter) ultimately show "eqUpdModDef s (SeqUpd u u2) (SeqUpd ub u2)" by (simp add: eqUpdModDef_def makeTotal_def Let_def overrideFuncUpdAssoc) next fix u ub u2 fix s :: "(('a::universe) semStructure)" let ?u2Val = "updVal s u2" let ?sU2Val = "overrideInter s ?u2Val" have LEM: "ALL u. (makeTotal s (overrideFuncUpd ?u2Val (makeTotal ?sU2Val (updVal ?sU2Val u))) = makeTotal s (overrideFuncUpd ?u2Val (updVal ?sU2Val u)))" by (rule allI, rule ext, simp add: makeTotal_def overrideFuncUpd_def overrideInter_def overrideFuncInter_def idUpd_def split: option.splits) assume "ALL (t::(('a::universe) semStructure)). eqUpdModDef t u ub" hence "makeTotal s (overrideFuncUpd ?u2Val (makeTotal ?sU2Val (updVal ?sU2Val u))) = makeTotal s (overrideFuncUpd ?u2Val (makeTotal ?sU2Val (updVal ?sU2Val ub)))" by (simp add: eqUpdModDef_def Let_def) from this LEM show "eqUpdModDef s (SeqUpd u2 u) (SeqUpd u2 ub)" by (simp add: eqUpdModDef_def Let_def) next fix u ub fo fix s :: "(('a::universe) semStructure)" assume "ALL (t::(('a::universe) semStructure)). eqUpdModDef t u ub" thus "eqUpdModDef s (GuardedUpd fo u) (GuardedUpd fo ub)" by (simp add: eqUpdModDef_def Let_def) next fix u fix s :: "(('a::universe) semStructure)" assume AS: "ALL (t::(('a::universe) semStructure)). eqUpdModDef t u Skip" have "makeTotal s (quanUpdComplete (%iv. updVal (addVarValue s iv) u)) = makeTotal s empty" proof (rule ext) fix loc show "makeTotal s (quanUpdComplete (%iv. updVal (addVarValue s iv) u)) loc = makeTotal s empty loc" proof cases assume "quanUpdComplete (%iv. updVal (addVarValue s iv) u) loc = None" thus ?thesis by (simp add: makeTotal_def overrideFuncUpd_def) next let ?notNoneSet = "{iv. updVal (addVarValue s iv) u loc ~= None}" let ?minIV = "min ?notNoneSet" assume "quanUpdComplete (%iv. updVal (addVarValue s iv) u) loc ~= None" from this obtain val where valDef: "quanUpdComplete (%iv. updVal (addVarValue s iv) u) loc = Some val" by auto from this have "updVal (addVarValue s ?minIV) u loc = Some val" by (simp add: Let_def quanUpdCompleteMin) hence "makeTotal (addVarValue s ?minIV) (updVal (addVarValue s ?minIV) u) loc = Some val" by (simp add: makeTotal_def overrideFuncUpd_def) from this AS have "makeTotal (addVarValue s ?minIV) empty loc = Some val" by (simp add: eqUpdModDef_def) from this valDef show ?thesis by (simp add: makeTotal_def overrideFuncUpd_def idUpd_def addVarValue_def) qed qed thus "eqUpdModDef s (QuanUpd u) Skip" by (simp add: eqUpdModDef_def Let_def) qed thus "((u1, u2) : congrUpdModDef (eqUpdModDefUniv t) --> (u1, u2) : eqUpdModDefUniv t)" by auto qed thus ?thesis by (auto, blast intro: congrUpdModDefSubset) qed end