| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/AOT/ (Archive of formal Proofs Version 2026-5©) Datei vom 29.4.2026 mit Größe 130 kB |
|
Quellcode-Bibliothek AOT_semantics.thy Sprache: Isabelle |
|||||||||||||||||||||||||
|
(*<*) theory AOT_semantics imports AOT_syntax begin (*>*) section‹Abstract Semantics for AOT› specification(AOT_denotes) ― ‹Relate object level denoting to meta-denoting. AOT's definitions of denoting will become derivable at each type.› AOT_sem_denotes: ‹[w ⊨ τ↓] = AOT_model_denotes τ› by (rule exI[where x=‹λ τ . ε\o w . AOT_model_denotes τ›]) (simp add: AOT_model_proposition_choice_simp) lemma AOT_sem_var_induct[induct type: AOT_var]: assumes AOT_denoting_term_case: ‹∧ τ . [v ⊨ τ↓] ==> [v ⊨ φ{τ}]› shows ‹[v ⊨ φ{α}]› by (simp add: AOT_denoting_term_case AOT_sem_denotes AOT_term_of_var) text‹\linelabel{AOT_imp_spec}› specification(AOT_imp) AOT_sem_imp: ‹[w ⊨ φ → ψ] = ([w ⊨ φ] ⟶ [w ⊨ ψ])› by (rule exI[where x=‹λ φ ψ . ε\o w . ([w ⊨ φ] ⟶ [w ⊨ ψ])›]) (simp add: AOT_model_proposition_choice_simp) specification(AOT_not) AOT_sem_not: ‹[w ⊨ ¬φ] = (¬[w ⊨ φ])› by (rule exI[where x=‹λ φ . ε\o w . ¬[w ⊨ φ]›]) (simp add: AOT_model_proposition_choice_simp) text‹\linelabel{AOT_box_spec}› specification(AOT_box) AOT_sem_box: ‹[w ⊨ ◻φ] = (∀ w . [w ⊨ φ])› by (rule exI[where x=‹λ φ . ε\o w . ∀ w . [w ⊨ φ]›]) (simp add: AOT_model_proposition_choice_simp) text‹\linelabel{AOT_act_spec}› specification(AOT_act) AOT_sem_act: ‹[w ⊨ \Aφ] = [w0 ⊨ φ]› by (rule exI[where x=‹λ φ . ε\o w . [w0 ⊨ φ]›]) (simp add: AOT_model_proposition_choice_simp) text‹Derived semantics for basic defined connectives.› lemma AOT_sem_conj: ‹[w ⊨ φ & ψ] = ([w ⊨ φ] ∧ [w ⊨ ψ])› using AOT_conj AOT_model_equiv_def AOT_sem_imp AOT_sem_not by auto lemma AOT_sem_equiv: ‹[w ⊨ φ ≡ ψ] = ([w ⊨ φ] = [w ⊨ ψ])› using AOT_equiv AOT_sem_conj AOT_model_equiv_def AOT_sem_imp by auto lemma AOT_sem_disj: ‹[w ⊨ φ ∨ ψ] = ([w ⊨ φ] ∨ [w ⊨ ψ])› using AOT_disj AOT_model_equiv_def AOT_sem_imp AOT_sem_not by auto lemma AOT_sem_dia: ‹[w ⊨ ♢φ] = (∃ w . [w ⊨ φ])› using AOT_dia AOT_sem_box AOT_model_equiv_def AOT_sem_not by auto specification(AOT_forall) AOT_sem_forall: ‹[w ⊨ ∀α φ{α}] = (∀ τ . [w ⊨ τ↓] ⟶ [w ⊨ φ{τ}])› by (rule exI[where x=‹λ op . ε\o w . ∀ τ . [w ⊨ τ↓] ⟶ [w ⊨ «op τ¬]›]) (simp add: AOT_model_proposition_choice_simp) lemma AOT_sem_exists: ‹[w ⊨ ∃α φ{α}] = (∃ τ . [w ⊨ τ↓] ∧ [w ⊨ φ{τ}])› unfolding AOT_exists[unfolded AOT_model_equiv_def, THEN spec] by (simp add: AOT_sem_forall AOT_sem_not) text‹\linelabel{AOT_eq_spec}› specification(AOT_eq) ― ‹Relate identity to denoting identity in the meta-logic. AOT's definitions of identity will become derivable at each type.› AOT_sem_eq: ‹[w ⊨ τ = τ'] = ([w ⊨ τ↓] ∧ [w ⊨ τ'↓] ∧ τ = τ')› by (rule exI[where x=‹λ τ τ' . ε\o w . [w ⊨ τ↓] ∧ [w ⊨ τ'↓] ∧ τ = τ'›]) (simp add: AOT_model_proposition_choice_simp) text‹\linelabel{AOT_desc_spec}› specification(AOT_desc) ― ‹Descriptions denote, if there is a unique denoting object satisfying the matrix in the actual world.› AOT_sem_desc_denotes: ‹[w ⊨ \ιx(φ{x})↓] = (∃! κ . [w0 ⊨ κ↓] ∧ [w0 ⊨ φ{κ}])› ― ‹Denoting descriptions satisfy their matrix in the actual world.› AOT_sem_desc_prop: ‹[w ⊨ \ιx(φ{x})↓] ==> [w0 ⊨ φ{\ιx(φ{x})}]› ― ‹Uniqueness of denoting descriptions.› AOT_sem_desc_unique: ‹[w ⊨ \ιx(φ{x})↓] ==> [w ⊨ κ↓] ==> [w0 ⊨ φ{κ}] ==> [w ⊨ \ιx(φ{x}) = κ]› proof - have ‹∃x::'a . ¬AOT_model_denotes x› using AOT_model_nondenoting_ex by blast text‹Note that we may choose a distinct non-denoting object for each matrix. We do this explicitly merely to convince ourselves that our specification can still be satisfied.› then obtain nondenoting :: ‹('a → o) → 'a› where nondenoting: ‹∀ φ . ¬AOT_model_denotes (nondenoting φ)› by fast define desc where ‹desc = (λ φ . if (∃! κ . [w0 ⊨ κ↓] ∧ [w0 ⊨ φ{κ}]) then (THE κ . [w0 ⊨ κ↓] ∧ [w0 ⊨ φ{κ}]) else nondenoting φ)› { fix φ :: ‹'a → o› assume ex1: ‹∃! κ . [w0 ⊨ κ↓] ∧ [w0 ⊨ φ{κ}]› then obtain κ where x_prop: "[w0 ⊨ κ↓] ∧ [w0 ⊨ φ{κ}]" unfolding AOT_sem_denotes by blast moreover have "(desc φ) = κ" unfolding desc_def using x_prop ex1 by fastforce ultimately have "[w0 ⊨ «desc φ¬↓] ∧ [w0 ⊨ «φ (desc φ)¬]" by blast } note 1 = this moreover { fix φ :: ‹'a → o› assume nex1: ‹∄! κ . [w0 ⊨ κ↓] ∧ [w0 ⊨ φ{κ}]› hence "(desc φ) = nondenoting φ" by (simp add: desc_def AOT_sem_denotes) hence "[w ⊨ ¬«desc φ¬↓]" for w by (simp add: AOT_sem_denotes nondenoting AOT_sem_not) } ultimately have desc_denotes_simp: ‹[w ⊨ «desc φ¬↓] = (∃! κ . [w0 ⊨ κ↓] ∧ [w0 ⊨ φ{κ}])› for φ w by (simp add: AOT_sem_denotes desc_def nondenoting) have ‹(∀φ w. [w ⊨ «desc φ¬↓] = (∃!κ. [w0 ⊨ κ↓] ∧ [w0 ⊨ φ{κ}])) ∧ (∀φ w. [w ⊨ «desc φ¬↓] ⟶ [w0 ⊨ «φ (desc φ)¬]) ∧ (∀φ w κ. [w ⊨ «desc φ¬↓] ⟶ [w ⊨ κ↓] ⟶ [w0 ⊨ φ{κ}] ⟶ [w ⊨ «desc φ¬ = κ])› by (insert 1; auto simp: desc_denotes_simp AOT_sem_eq AOT_sem_denotes desc_def nondenoting) thus ?thesis by (safe intro!: exI[where x=desc]; presburger) qed text‹\linelabel{AOT_exe_lambda_spec}› specification(AOT_exe AOT_lambda) ― ‹Truth conditions of exemplification formulas.› AOT_sem_exe: ‹[w ⊨ [Π]κ1...κn] = ([w ⊨ Π↓] ∧ [w ⊨ κ1...κn↓] ∧ [w ⊨ «Rep_rel Π κ1κn¬])› ― ‹\eta-conversion for denoting terms; equivalent to AOT's axiom› AOT_sem_lambda_eta: ‹[w ⊨ Π↓] ==> [w ⊨ [λν1...νn [Π]ν1...νn] = Π]› ― ‹\beta-conversion; equivalent to AOT's axiom› AOT_sem_lambda_beta: ‹[w ⊨ [λν1...νn φ{ν1...νn}]↓] ==> [w ⊨ κ1...κn↓] ==> [w ⊨ [λν1...νn φ{ν1...νn}]κ1...κn] = [w ⊨ φ{κ1...κn}]› ― ‹Necessary and sufficient conditions for relations to denote. Equivalent to a theorem of AOT and used to derive the base cases of denoting relations (cqt.2).› AOT_sem_lambda_denotes: ‹[w ⊨ [λν1...νn φ{ν1...νn}]↓] = (∀ v κ1κn κ1'κn' . [v ⊨ κ1...κn↓] ∧ [v ⊨ κ1'...κn'↓] ∧ (∀ Π v . [v ⊨ Π↓] ⟶ [v ⊨ [Π]κ1...κn] = [v ⊨ [Π]κ1'...κn']) ⟶ [v ⊨ φ{κ1...κn}] = [v ⊨ φ{κ1'...κn'}])› ― ‹Equivalent to AOT's coexistence axiom.› AOT_sem_lambda_coex: ‹[w ⊨ [λν1...νn φ{ν1...νn}]↓] ==> (∀ w κ1κn . [w ⊨ κ1...κn↓] ⟶ [w ⊨ φ{κ1...κn}] = [w ⊨ ψ{κ1...κn}]) ==> [w ⊨ [λν1...νn ψ{ν1...νn}]↓]› ― ‹Only the unary case of the following should hold, but our specification has to range over all types. We might move @{const AOT_exe} and @{const AOT_lambda} to type classes in the future to solve this.› AOT_sem_lambda_eq_prop_eq: ‹«[λν1...νn φ]¬ = «[λν1...νn ψ]¬ ==> φ = ψ› ― ‹The following is solely required for validating n-ary relation identity and has the danger of implying artifactual theorems. Possibly avoidable by moving @{const AOT_exe} and @{const AOT_lambda} to type classes.› AOT_sem_exe_denoting: ‹[w ⊨ Π↓] ==> AOT_exe Π κs = Rep_rel Π κs› ― ‹The following is required for validating the base cases of denoting relations (cqt.2). A version of this meta-logical identity will become derivable in future versions of AOT, so this will ultimately not result in artifactual theorems.› AOT_sem_exe_equiv: ‹AOT_model_term_equiv x y ==> AOT_exe Π x = AOT_exe Π y› proof - have ‹∃ x :: <'a> . ¬AOT_model_denotes x› by (rule exI[where x=‹Abs_rel (λ x . ε\o w. True)›]) (meson AOT_model_denotes_rel.abs_eq AOT_model_nondenoting_ex AOT_model_proposition_choice_simp) define exe :: ‹<'a> → 'a → o› where ‹exe ≡ λ Π κs . if AOT_model_denotes Π then Rep_rel Π κs else (ε\o w . False)› define lambda :: ‹('a→o) → <'a>› where ‹lambda ≡ λ φ . if AOT_model_denotes (Abs_rel φ) then (Abs_rel φ) else if (∀ κ κ' w . (AOT_model_denotes κ ∧ AOT_model_term_equiv κ κ') ⟶ [w ⊨ «φ κ¬] = [w ⊨ «φ κ'¬]) then Abs_rel (fix_irregular (λ x . if AOT_model_denotes x then φ (SOME y . AOT_model_term_equiv x y) else (ε\o w . False))) else Abs_rel φ› have fix_irregular_denoting_simp[simp]: ‹fix_irregular (λx. if AOT_model_denotes x then φ x else ψ x) κ = φ κ› if ‹AOT_model_denotes κ› for κ :: 'a and φ ψ by (simp add: that fix_irregular_denoting) have denoting_eps_cong[cong]: ‹[w ⊨ «φ (Eps (AOT_model_term_equiv κ))¬] = [w ⊨ «φ κ¬]› if ‹AOT_model_denotes κ› and ‹∀ κ κ'. AOT_model_denotes κ ∧ AOT_model_term_equiv κ κ' ⟶ (∀w. [w ⊨ «φ κ¬] = [w ⊨ «φ κ'¬])› for w :: w and κ :: 'a and φ :: ‹'a→o› using that AOT_model_term_equiv_eps(2) by blast have exe_rep_rel: ‹[w ⊨ «exe Π κ1κn¬] = ([w ⊨ Π↓] ∧ [w ⊨ κ1...κn↓] ∧ [w ⊨ «Rep_rel Π κ1κn¬])› for w Π κ1κn by (metis AOT_model_denotes_rel.rep_eq exe_def AOT_sem_denotes AOT_model_proposition_choice_simp) moreover have ‹[w ⊨ «Π¬↓] ==> [w ⊨ «lambda (exe Π)¬ = «Π¬]› for Π w by (auto simp: Rep_rel_inverse lambda_def AOT_sem_denotes AOT_sem_eq AOT_model_denotes_rel_def Abs_rel_inverse exe_def) moreover have lambda_denotes_beta: ‹[w ⊨ «exe (lambda φ) κ ¬] = [w ⊨ «φ κ¬]› if ‹[w ⊨ «lambda φ¬↓]› and ‹[w ⊨ «κ¬↓]› for φ κ w using that unfolding exe_def AOT_sem_denotes by (auto simp: lambda_def Abs_rel_inverse split: if_split_asm) moreover have lambda_denotes_simp: ‹[w ⊨ «lambda φ¬↓] = (∀ v κ1κn κ1'κn' . [v ⊨ κ1...κn↓] ∧ [v ⊨ κ1'...κn'↓] ∧ (∀ Π v . [v ⊨ Π↓] ⟶ [v ⊨ «exe Π κ1κn¬] = [v ⊨ «exe Π κ1'κn'¬]) ⟶ [v ⊨ φ{κ1...κn}] = [v ⊨ φ{κ1'...κn'}])› for φ w proof assume ‹[w ⊨ «lambda φ¬↓]› hence ‹AOT_model_denotes (lambda φ)› unfolding AOT_sem_denotes by simp moreover have ‹[w ⊨ «φ κ¬] ==> [w ⊨ «φ κ'¬]› and ‹[w ⊨ «φ κ'¬] ==> [w ⊨ «φ κ¬]› if ‹AOT_model_denotes κ› and ‹AOT_model_term_equiv κ κ'› for w κ κ' by (metis (no_types, lifting) AOT_model_denotes_rel.abs_eq lambda_def that calculation)+ ultimately show ‹∀ v κ1κn κ1'κn' . [v ⊨ κ1...κn↓] ∧ [v ⊨ κ1'...κn'↓] ∧ (∀ Π v . [v ⊨ Π↓] ⟶ [v ⊨ «exe Π κ1κn¬] = [v ⊨ «exe Π κ1'κn'¬]) ⟶ [v ⊨ φ{κ1...κn}] = [v ⊨ φ{κ1'...κn'}]› unfolding AOT_sem_denotes by (metis (no_types) AOT_sem_denotes lambda_denotes_beta) next assume ‹∀ v κ1κn κ1'κn' . [v ⊨ κ1...κn↓] ∧ [v ⊨ κ1'...κn'↓] ∧ (∀ Π v . [v ⊨ Π↓] ⟶ [v ⊨ «exe Π κ1κn¬] = [v ⊨ «exe Π κ1'κn'¬]) ⟶ [v ⊨ φ{κ1...κn}] = [v ⊨ φ{κ1'...κn'}]› hence ‹[w ⊨ «φ κ¬] = [w ⊨ «φ κ'¬]› if ‹AOT_model_denotes κ ∧ AOT_model_denotes κ' ∧ AOT_model_term_equiv κ κ'› for w κ κ' using that by (auto simp: AOT_sem_denotes) (meson AOT_model_term_equiv_rel_equiv AOT_sem_denotes exe_rep_rel)+ hence ‹[w ⊨ «φ κ¬] = [w ⊨ «φ κ'¬]› if ‹AOT_model_denotes κ ∧ AOT_model_term_equiv κ κ'› for w κ κ' using that AOT_model_term_equiv_denotes by blast hence ‹AOT_model_denotes (lambda φ)› by (auto simp: lambda_def Abs_rel_inverse AOT_model_denotes_rel.abs_eq AOT_model_irregular_equiv AOT_model_term_equiv_eps(3) AOT_model_term_equiv_regular fix_irregular_def AOT_sem_denotes AOT_model_term_equiv_denotes AOT_model_proposition_choice_simp AOT_model_irregular_false split: if_split_asm intro: AOT_model_irregular_eqI) thus ‹[w ⊨ «lambda φ¬↓]› by (simp add: AOT_sem_denotes) qed moreover have ‹[w ⊨ «lambda ψ¬↓]› if ‹[w ⊨ «lambda φ¬↓]› and ‹∀ w κ1κn . [w ⊨ κ1...κn↓] ⟶ [w ⊨ φ{κ1...κn}] = [w ⊨ ψ{κ1...κn}]› for φ ψ w using that unfolding lambda_denotes_simp by auto moreover have ‹[w ⊨ Π↓] ==> exe Π κs = Rep_rel Π κs› for Π κs w by (simp add: exe_def AOT_sem_denotes) moreover have ‹lambda (λx. p) = lambda (λx. q) ==> p = q› for p q unfolding lambda_def by (auto split: if_split_asm simp: Abs_rel_inject fix_irregular_def) (meson AOT_model_irregular_nondenoting AOT_model_denoting_ex)+ moreover have ‹AOT_model_term_equiv x y ==> exe Π x = exe Π y› for x y Π unfolding exe_def by (meson AOT_model_denotes_rel.rep_eq) note calculation = calculation this show ?thesis apply (safe intro!: exI[where x=exe] exI[where x=lambda]) using calculation apply simp_all using lambda_denotes_simp by blast+ qed lemma AOT_model_lambda_denotes: ‹AOT_model_denotes (AOT_lambda φ) = (∀ v κ κ' . AOT_model_denotes κ ∧ AOT_model_denotes κ' ∧ AOT_model_term_equiv κ κ' ⟶ [v ⊨ «φ κ¬] = [v ⊨ «φ κ'¬])› proof(safe) fix v and κ κ' :: 'a assume ‹AOT_model_denotes (AOT_lambda φ)› hence 1: ‹AOT_model_denotes κ1κn ∧ AOT_model_denotes κ1'κn' ∧ (∀Π v. AOT_model_denotes Π ⟶ [v ⊨ [Π]κ1...κn] = [v ⊨ [Π]κ1'...κn']) ⟶ [v ⊨ φ{κ1...κn}] = [v ⊨ φ{κ1'...κn'}]› for κ1κn κ1'κn' v using AOT_sem_lambda_denotes[simplified AOT_sem_denotes] by blast { fix v and κ1κn κ1'κn' :: 'a assume d: ‹AOT_model_denotes κ1κn ∧ AOT_model_denotes κ1'κn' ∧ AOT_model_term_equiv κ1κn κ1'κn'› hence ‹∀Π w. AOT_model_denotes Π ⟶ [w ⊨ [Π]κ1...κn] = [w ⊨ [Π]κ1'...κn']› by (metis AOT_sem_exe_equiv) hence ‹[v ⊨ φ{κ1...κn}] = [v ⊨ φ{κ1'...κn'}]› using d 1 by auto } moreover assume ‹AOT_model_denotes κ› moreover assume ‹AOT_model_denotes κ'› moreover assume ‹AOT_model_term_equiv κ κ'› ultimately show ‹[v ⊨ «φ κ¬] ==> [v ⊨ «φ κ'¬]› and ‹[v ⊨ «φ κ'¬] ==> [v ⊨ «φ κ¬]› by auto next assume 0: ‹∀ v κ κ' . AOT_model_denotes κ ∧ AOT_model_denotes κ' ∧ AOT_model_term_equiv κ κ' ⟶ [v ⊨ «φ κ¬] = [v ⊨ «φ κ'¬]› { fix κ1κn κ1'κn' :: 'a assume den: ‹AOT_model_denotes κ1κn› moreover assume den': ‹AOT_model_denotes κ1'κn'› assume ‹∀Π v . AOT_model_denotes Π ⟶ [v ⊨ [Π]κ1...κn] = [v ⊨ [Π]κ1'...κn']› hence ‹∀Π v . AOT_model_denotes Π ⟶ [v ⊨ «Rep_rel Π κ1κn¬] = [v ⊨ «Rep_rel Π κ1'κn'¬]› by (simp add: AOT_sem_denotes AOT_sem_exe den den') hence "AOT_model_term_equiv κ1κn κ1'κn'" unfolding AOT_model_term_equiv_rel_equiv[OF den, OF den'] by argo hence ‹[v ⊨ φ{κ1...κn}] = [v ⊨ φ{κ1'...κn'}]› for v using den den' 0 by blast } thus ‹AOT_model_denotes (AOT_lambda φ)› unfolding AOT_sem_lambda_denotes[simplified AOT_sem_denotes] by blast qed specification (AOT_lambda0) AOT_sem_lambda0: "AOT_lambda0 φ = φ" by (rule exI[where x=‹λx. x›]) simp specification(AOT_concrete) AOT_sem_concrete: ‹[w ⊨ [E!]κ] = AOT_model_concrete w κ› by (rule exI[where x=‹AOT_var_of_term (Abs_rel (λ x . ε\o w . AOT_model_concrete w x))›]; subst AOT_var_of_term_inverse) (auto simp: AOT_model_unary_regular AOT_model_concrete_denotes AOT_model_concrete_equiv AOT_model_regular_κ_def AOT_model_proposition_choice_simp AOT_sem_exe Abs_rel_inverse AOT_model_denotes_rel_def AOT_sem_denotes) lemma AOT_sem_equiv_defI: assumes ‹∧ v . [v ⊨ φ] ==> [v ⊨ ψ]› and ‹∧ v . [v ⊨ ψ] ==> [v ⊨ φ]› shows ‹AOT_model_equiv_def φ ψ› using AOT_model_equiv_def assms by blast lemma AOT_sem_id_defI: assumes ‹∧ α v . [v ⊨ «σ α¬↓] ==> [v ⊨ «τ α¬ = «σ α¬]› assumes ‹∧ α v . ¬[v ⊨ «σ α¬↓] ==> [v ⊨ ¬«τ α¬↓]› shows ‹AOT_model_id_def τ σ› using assms unfolding AOT_sem_denotes AOT_sem_eq AOT_sem_not using AOT_model_id_def[THEN iffD2] by metis lemma AOT_sem_id_def2I: assumes ‹∧ α β v . [v ⊨ «σ α β¬↓] ==> [v ⊨ «τ α β¬ = «σ α β¬]› assumes ‹∧ α β v . ¬[v ⊨ «σ α β¬↓] ==> [v ⊨ ¬«τ α β¬↓]› shows ‹AOT_model_id_def (case_prod τ) (case_prod σ)› apply (rule AOT_sem_id_defI) using assms by (auto simp: AOT_sem_conj AOT_sem_not AOT_sem_eq AOT_sem_denotes AOT_model_denotes_prod_def) lemma AOT_sem_id_defE1: assumes ‹AOT_model_id_def τ σ› and ‹[v ⊨ «σ α¬↓]› shows ‹[v ⊨ «τ α¬ = «σ α¬]› using assms by (simp add: AOT_model_id_def AOT_sem_denotes AOT_sem_eq) lemma AOT_sem_id_defE2: assumes ‹AOT_model_id_def τ σ› and ‹¬[v ⊨ «σ α¬↓]› shows ‹¬[v ⊨ «τ α¬↓]› using assms by (simp add: AOT_model_id_def AOT_sem_denotes AOT_sem_eq) lemma AOT_sem_id_def0I: assumes ‹∧ v . [v ⊨ σ↓] ==> [v ⊨ τ = σ]› and ‹∧ v . ¬[v ⊨ σ↓] ==> [v ⊨ ¬τ↓]› shows ‹AOT_model_id_def (case_unit τ) (case_unit σ)› apply (rule AOT_sem_id_defI) using assms by (simp_all add: AOT_sem_conj AOT_sem_eq AOT_sem_not AOT_sem_denotes AOT_model_denotes_unit_def case_unit_Unity) lemma AOT_sem_id_def0E1: assumes ‹AOT_model_id_def (case_unit τ) (case_unit σ)› and ‹[v ⊨ σ↓]› shows ‹[v ⊨ τ = σ]› by (metis (full_types) AOT_sem_id_defE1 assms(1) assms(2) case_unit_Unity) lemma AOT_sem_id_def0E2: assumes ‹AOT_model_id_def (case_unit τ) (case_unit σ)› and ‹¬[v ⊨ σ↓]› shows ‹¬[v ⊨ τ↓]› by (metis AOT_sem_id_defE2 assms(1) assms(2) case_unit_Unity) lemma AOT_sem_id_def0E3: assumes ‹AOT_model_id_def (case_unit τ) (case_unit σ)› and ‹[v ⊨ σ↓]› shows ‹[v ⊨ τ↓]› using AOT_sem_id_def0E1[OF assms] by (simp add: AOT_sem_eq AOT_sem_denotes) lemma AOT_sem_ordinary_def_denotes: ‹[w ⊨ [λx ♢[E!]x]↓]› unfolding AOT_sem_denotes AOT_model_lambda_denotes by (auto simp: AOT_sem_dia AOT_model_concrete_equiv AOT_sem_concrete AOT_sem_denotes) lemma AOT_sem_abstract_def_denotes: ‹[w ⊨ [λx ¬♢[E!]x]↓]› unfolding AOT_sem_denotes AOT_model_lambda_denotes by (auto simp: AOT_sem_dia AOT_model_concrete_equiv AOT_sem_concrete AOT_sem_denotes AOT_sem_not) text‹Relation identity is constructed using an auxiliary abstract projection mechanism with suitable instantiations for @{typ κ} and products.› class AOT_RelationProjection = fixes AOT_sem_proj_id :: ‹'a::AOT_IndividualTerm → ('a → o) → ('a → o) → o› assumes AOT_sem_proj_id_prop: ‹[v ⊨ Π = Π'] = [v ⊨ Π↓ & Π'↓ & ∀α («AOT_sem_proj_id α (λ τ . «[Π]τ¬) (λ τ . «[Π']τ¬)¬) and AOT_sem_proj_id_refl: ‹[v ⊨ τ↓] ==> [v ⊨ [λν1...νn φ{ν1...νn}] = [λν1...νn φ{ν1...νn}]] ==> [v ⊨ «AOT_sem_proj_id τ φ φ¬]› class AOT_UnaryRelationProjection = AOT_RelationProjection + assumes AOT_sem_unary_proj_id: ‹AOT_sem_proj_id κ φ ψ = «[λν1...νn φ{ν1...νn}] = [λν1...νn ψ{ν1...νn}]¬› instantiation κ :: AOT_UnaryRelationProjection begin definition AOT_sem_proj_id_κ :: ‹κ → (κ → o) → (κ → o) → o› where ‹AOT_sem_proj_id_κ κ φ ψ = «[λz φ{z}] = [λz ψ{z}]¬› instance proof show ‹[v ⊨ Π = Π'] = [v ⊨ Π↓ & Π'↓ & ∀α («AOT_sem_proj_id α (λ τ . «[Π]τ¬) (λ τ . «[Π']τ¬)¬) for v and Π Π' :: ‹<\<kappa>>› unfolding AOT_sem_proj_id_κ_def by (simp add: AOT_sem_eq AOT_sem_conj AOT_sem_denotes AOT_sem_forall) (metis AOT_sem_denotes AOT_model_denoting_ex AOT_sem_eq AOT_sem_lambda_eta) next show ‹AOT_sem_proj_id κ φ ψ = «[λν1...νn φ{ν1...νn}] = [λν1...νn ψ{ν1...νn}]¬› for κ :: κ and φ ψ unfolding AOT_sem_proj_id_κ_def .. next show ‹[v ⊨ «AOT_sem_proj_id τ φ φ¬]› if ‹[v ⊨ τ↓]› and ‹[v ⊨ [λν1...νn φ{ν1...νn}] = [λν1...νn φ{ν1...νn}]]› for τ :: κ and v φ using that by (simp add: AOT_sem_proj_id_κ_def AOT_sem_eq) qed end instantiation prod :: ("{AOT_UnaryRelationProjection, AOT_UnaryIndividualTerm}", AOT_RelationProjection AOT_RelationProjection begin definition AOT_sem_proj_id_prod :: ‹'a×'b → ('a×'b → o) → ('a×'b → o) → o› where ‹AOT_sem_proj_id_prod ≡ λ (x,y) φ ψ . «[λz «φ (z,y)¬] = [λz «ψ (z,y)¬] & «AOT_sem_proj_id y (λ a . φ (x,a)) (λ a . ψ (x,a))¬¬› instance proof text‹This is the main proof that allows to derive the definition of n-ary relation identity. We need to show that our defined projection identity implies relation identity for relations on pairs of individual terms.› fix v and Π Π' :: ‹<'a×'b>› have AOT_meta_proj_denotes1: ‹AOT_model_denotes (Abs_rel (λz. AOT_exe Π (z, β)))› if ‹AOT_model_denotes Π› for Π :: ‹<'a×'b>› and β using that unfolding AOT_model_denotes_rel.rep_eq apply (simp add: Abs_rel_inverse AOT_meta_prod_equivI(2) AOT_sem_denotes that) by (metis (no_types, lifting) AOT_meta_prod_equivI(2) AOT_model_denotes_prod_def AOT_model_unary_regular AOT_sem_exe AOT_sem_exe_equiv case_prodD) { fix κ :: 'a and Π :: ‹<'a×'b>› assume Π_denotes: ‹AOT_model_denotes Π› assume α_denotes: ‹AOT_model_denotes κ› hence ‹AOT_exe Π (κ, x) = AOT_exe Π (κ, y)› if ‹AOT_model_term_equiv x y› for x y :: 'b by (simp add: AOT_meta_prod_equivI(1) AOT_sem_exe_equiv that) moreover have ‹AOT_model_denotes κ1'κn'› if ‹[w ⊨ [Π]κ κ1'...κn']› for w κ1'κn' by (metis that AOT_model_denotes_prod_def AOT_sem_exe AOT_sem_denotes case_prodD) moreover { fix x :: 'b assume x_irregular: ‹¬AOT_model_regular x› hence prod_irregular: ‹¬AOT_model_regular (κ, x)› by (metis (no_types, lifting) AOT_model_irregular_nondenoting AOT_model_regular_prod_def case_prodD) hence ‹(¬AOT_model_denotes κ ∨ ¬AOT_model_regular x) ∧ (AOT_model_denotes κ ∨ ¬AOT_model_denotes x)› unfolding AOT_model_regular_prod_def by blast hence x_nonden: ‹¬AOT_model_regular x› by (simp add: α_denotes) have ‹Rep_rel Π (κ, x) = AOT_model_irregular (Rep_rel Π) (κ, x)› using AOT_model_denotes_rel.rep_eq Π_denotes prod_irregular by blast moreover have ‹AOT_model_irregular (Rep_rel Π) (κ, x) = AOT_model_irregular (λz. Rep_rel Π (κ, z)) x› using Π_denotes x_irregular prod_irregular x_nonden using AOT_model_irregular_prod_generic apply (induct arbitrary: Π x rule: AOT_model_irregular_prod.induct) by (auto simp: α_denotes AOT_model_irregular_nondenoting AOT_model_regular_prod_def AOT_meta_prod_equivI(2) AOT_model_denotes_rel.rep_eq AOT_model_term_equiv_eps(1) intro!: AOT_model_irregular_eqI) ultimately have ‹AOT_exe Π (κ, x) = AOT_model_irregular (λz. AOT_exe Π (κ, z)) x› unfolding AOT_sem_exe_denoting[simplified AOT_sem_denotes, OF Π_denotes] by auto } ultimately have ‹AOT_model_denotes (Abs_rel (λz. AOT_exe Π (κ, z)))› by (simp add: Abs_rel_inverse AOT_model_denotes_rel.rep_eq) } note AOT_meta_proj_denotes2 = this { fix κ1'κn' :: 'b and Π :: ‹<'a×'b>› assume Π_denotes: ‹AOT_model_denotes Π› assume β_denotes: ‹AOT_model_denotes κ1'κn'› hence ‹AOT_exe Π (x, κ1'κn') = AOT_exe Π (y, κ1'κn')› if ‹AOT_model_term_equiv x y› for x y :: 'a by (simp add: AOT_meta_prod_equivI(2) AOT_sem_exe_equiv that) moreover have ‹AOT_model_denotes κ› if ‹[w ⊨ [Π]κ κ1'...κn']› for w κ by (metis that AOT_model_denotes_prod_def AOT_sem_exe AOT_sem_denotes case_prodD) moreover { fix x :: 'a assume ‹¬AOT_model_regular x› hence ‹False› using AOT_model_unary_regular by blast hence ‹AOT_exe Π (x,κ1'κn') = AOT_model_irregular (λz. AOT_exe Π (z,κ1'κn')) x› unfolding AOT_sem_exe_denoting[simplified AOT_sem_denotes, OF Π_denotes] by auto } ultimately have ‹AOT_model_denotes (Abs_rel (λz. AOT_exe Π (z,κ1'κn')))› by (simp add: Abs_rel_inverse AOT_model_denotes_rel.rep_eq) } note AOT_meta_proj_denotes1 = this { assume Π_denotes: ‹AOT_model_denotes Π› assume Π'_denotes: ‹AOT_model_denotes Π'› have Π_proj2_den: ‹AOT_model_denotes (Abs_rel (λz. Rep_rel Π (α, z)))› if ‹AOT_model_denotes α› for α using that AOT_meta_proj_denotes2[OF Π_denotes] AOT_sem_exe_denoting[simplified AOT_sem_denotes,OF Π_denotes] by simp have Π'_proj2_den: ‹AOT_model_denotes (Abs_rel (λz. Rep_rel Π' (α, z)))› if ‹AOT_model_denotes α› for α using that AOT_meta_proj_denotes2[OF Π'_denotes] AOT_sem_exe_denoting[simplified AOT_sem_denotes,OF Π'_denotes] by simp have Π_proj1_den: ‹AOT_model_denotes (Abs_rel (λz. Rep_rel Π (z, α)))› if ‹AOT_model_denotes α› for α using that AOT_meta_proj_denotes1[OF Π_denotes] AOT_sem_exe_denoting[simplified AOT_sem_denotes,OF Π_denotes] by simp have Π'_proj1_den: ‹AOT_model_denotes (Abs_rel (λz. Rep_rel Π' (z, α)))› if ‹AOT_model_denotes α› for α using that AOT_meta_proj_denotes1[OF Π'_denotes] AOT_sem_exe_denoting[simplified AOT_sem_denotes,OF Π'_denotes] by simp { fix κ :: 'a and κ1'κn' :: 'b assume ‹Π = Π'› assume ‹AOT_model_denotes (κ,κ1'κn')› hence ‹AOT_model_denotes κ› and beta_denotes: ‹AOT_model_denotes κ1'κn'› by (auto simp: AOT_model_denotes_prod_def) have ‹AOT_model_denotes «[λz [Π]z κ1'...κn']¬› by (rule AOT_model_lambda_denotes[THEN iffD2]) (metis AOT_sem_exe_denoting AOT_meta_prod_equivI(2) AOT_model_denotes_rel.rep_eq AOT_sem_denotes AOT_sem_exe_denoting Π_denotes) moreover have ‹«[λz [Π]z κ1'...κn']¬ = «[λz [Π']z κ1'...κn']¬› by (simp add: ‹Π = Π'›) moreover have ‹[v ⊨ «AOT_sem_proj_id κ1'κn' (λκ1'κn'. «[Π]κ κ1'...κn'¬) (λκ1'κn'. «[Π']κ κ1'...κn'¬)¬]› unfolding ‹Π = Π'› using beta_denotes by (rule AOT_sem_proj_id_refl[unfolded AOT_sem_denotes]; simp add: AOT_sem_denotes AOT_sem_eq AOT_model_lambda_denotes) (metis AOT_meta_prod_equivI(1) AOT_model_denotes_rel.rep_eq AOT_sem_exe AOT_sem_exe_denoting Π'_denotes) ultimately have ‹[v ⊨ «AOT_sem_proj_id (κ,κ1'κn') (λ κ1κn . «[Π]κ1...κn¬) (λ κ1κn . «[Π']κ1...κn¬)¬]› unfolding AOT_sem_proj_id_prod_def by (simp add: AOT_sem_denotes AOT_sem_conj AOT_sem_eq) } moreover { assume ‹∧ α . AOT_model_denotes α ==> [v ⊨ «AOT_sem_proj_id α (λ κ1κn . «[Π]κ1...κn¬) (λ κ1κn . «[Π']κ1...κn¬)¬]› hence 0: ‹AOT_model_denotes κ ==> AOT_model_denotes κ1'κn' ==> AOT_model_denotes «[λz [Π]z κ1'...κn']¬ ∧ AOT_model_denotes «[λz [Π']z κ1'...κn']¬ ∧ «[λz [Π]z κ1'...κn']¬ = «[λz [Π']z κ1'...κn']¬ ∧ [v ⊨ «AOT_sem_proj_id κ1'κn' (λκ1κn. «[Π]κ κ1...κn¬) (λκ1κn. «[Π']κ κ1...κn¬)¬]› for κ κ1'κn' unfolding AOT_sem_proj_id_prod_def by (auto simp: AOT_sem_denotes AOT_sem_conj AOT_sem_eq AOT_model_denotes_prod_def) obtain αden :: 'a and βden :: 'b where αden: ‹AOT_model_denotes αden› and βden: ‹AOT_model_denotes βden› using AOT_model_denoting_ex by metis { fix κ :: 'a assume αdenotes: ‹AOT_model_denotes κ› have 1: ‹[v ⊨ «AOT_sem_proj_id κ1'κn' (λκ1'κn'. «[Π]κ κ1'...κn'¬) (λκ1'κn'. «[Π']κ κ1'...κn'¬)¬]› if ‹AOT_model_denotes κ1'κn'› for κ1'κn' using that 0 using αdenotes by blast hence ‹[v ⊨ «AOT_sem_proj_id β (λz. Rep_rel Π (κ, z)) (λz. Rep_rel Π' (κ, z))¬]› if ‹AOT_model_denotes β› for β using that unfolding AOT_sem_exe_denoting[simplified AOT_sem_denotes, OF Π_denotes] AOT_sem_exe_denoting[simplified AOT_sem_denotes, OF Π'_denotes] by blast hence ‹Abs_rel (λz. Rep_rel Π (κ, z)) = Abs_rel (λz. Rep_rel Π' (κ, z))› using AOT_sem_proj_id_prop[of v ‹Abs_rel (λz. Rep_rel Π (κ, z))› ‹Abs_rel (λz. Rep_rel Π' (κ, z))›, simplified AOT_sem_eq AOT_sem_conj AOT_sem_forall AOT_sem_denotes, THEN iffD2] Π_proj2_den[OF αdenotes] Π'_proj2_den[OF αdenotes] unfolding AOT_sem_exe_denoting[simplified AOT_sem_denotes, OF Π_denotes] AOT_sem_exe_denoting[simplified AOT_sem_denotes, OF Π_proj2_den[OF αdenotes]] AOT_sem_exe_denoting[simplified AOT_sem_denotes, OF Π'_proj2_den[OF αdenotes]] by (metis Abs_rel_inverse UNIV_I) hence "Rep_rel Π (κ,β) = Rep_rel Π' (κ,β)" for β by (simp add: Abs_rel_inject[simplified]) meson } note αdenotes = this { fix κ1'κn' :: 'b assume βden: ‹AOT_model_denotes κ1'κn'› have 1: ‹«[λz [Π]z κ1'...κn']¬ = «[λz [Π']z κ1'...κn']¬› using 0 βden AOT_model_denoting_ex by blast hence ‹Abs_rel (λz. Rep_rel Π (z, κ1'κn')) = Abs_rel (λz. Rep_rel Π' (z, κ1'κn'))› (is ‹?a = ?b›) apply (safe intro!: AOT_sem_proj_id_prop[of v ‹?a› ‹?b›, simplified AOT_sem_eq AOT_sem_conj AOT_sem_forall AOT_sem_denotes, THEN iffD2, THEN conjunct2, THEN conjunct2] Π_proj1_den[OF βden] Π'_proj1_den[OF βden]) unfolding AOT_sem_exe_denoting[simplified AOT_sem_denotes, OF Π_denotes] AOT_sem_exe_denoting[simplified AOT_sem_denotes, OF Π'_denotes] AOT_sem_exe_denoting[simplified AOT_sem_denotes, OF Π_proj1_den[OF βden]] AOT_sem_exe_denoting[simplified AOT_sem_denotes, OF Π'_proj1_den[OF βden]] by (subst (0 1) Abs_rel_inverse; simp?) (metis (no_types, lifting) AOT_model_denotes_rel.abs_eq AOT_model_lambda_denotes AOT_sem_denotes AOT_sem_eq AOT_sem_unary_proj_id Π_proj1_den[OF βden]) hence ‹Rep_rel Π (x,κ1'κn') = Rep_rel Π' (x,κ1'κn')› for x by (simp add: Abs_rel_inject) metis } note βdenotes = this { fix α :: 'a and β :: 'b assume ‹AOT_model_regular (α, β)› moreover { assume ‹AOT_model_denotes α ∧ AOT_model_regular β› hence ‹Rep_rel Π (α,β) = Rep_rel Π' (α,β)› using αdenotes by presburger } moreover { assume ‹¬AOT_model_denotes α ∧ AOT_model_denotes β› hence ‹Rep_rel Π (α,β) = Rep_rel Π' (α,β)› by (simp add: βdenotes) } ultimately have ‹Rep_rel Π (α,β) = Rep_rel Π' (α,β)› by (metis (no_types, lifting) AOT_model_regular_prod_def case_prodD) } hence ‹Rep_rel Π = Rep_rel Π'› using Π_denotes[unfolded AOT_model_denotes_rel.rep_eq, THEN conjunct2, THEN conjunct2, THEN spec, THEN mp] using Π'_denotes[unfolded AOT_model_denotes_rel.rep_eq, THEN conjunct2, THEN conjunct2, THEN spec, THEN mp] using AOT_model_irregular_eqI[of ‹Rep_rel Π› ‹Rep_rel Π'› ‹(_,_)›] using AOT_model_irregular_nondenoting by fastforce hence ‹Π = Π'› by (rule Rep_rel_inject[THEN iffD1]) } ultimately have ‹Π = Π' = (∀ κ . AOT_model_denotes κ ⟶ [v ⊨ «AOT_sem_proj_id κ (λ κ1κn . «[Π]κ1...κn¬) (λ κ1κn . «[Π']κ1...κn¬)¬])› by auto } thus ‹[v ⊨ Π = Π'] = [v ⊨ Π↓ & Π'↓ & ∀α («AOT_sem_proj_id α (λ κ1κn . «[Π]κ1...κn¬) (λ κ1κn . «[Π']κ1...κn¬)¬)]› by (auto simp: AOT_sem_eq AOT_sem_denotes AOT_sem_forall AOT_sem_conj) next fix v and φ :: ‹'a×'b→o› and τ :: ‹'a×'b› assume ‹[v ⊨ τ↓]› moreover assume ‹[v ⊨ [λz1...zn «φ z1zn¬] = [λz1...zn «φ z1zn¬]]› ultimately show ‹[v ⊨ «AOT_sem_proj_id τ φ φ¬]› unfolding AOT_sem_proj_id_prod_def using AOT_sem_proj_id_refl[of v "snd τ" "λb. φ (fst τ, b)"] by (auto simp: AOT_sem_eq AOT_sem_conj AOT_sem_denotes AOT_model_denotes_prod_def AOT_model_lambda_denotes AOT_meta_prod_equivI) qed end text‹Sanity-check to verify that n-ary relation identity follows.› lemma ‹[v ⊨ Π = Π'] = [v ⊨ Π↓ & Π'↓ & ∀x∀y([λz [Π]z y] = [λz [λz [Π]x z] = [λz [Π']x z])] for Π :: ‹<\<kappa>×κ>› by (auto simp: AOT_sem_proj_id_prop[of v Π Π'] AOT_sem_proj_id_prod_def AOT_sem_conj AOT_sem_denotes AOT_sem_forall AOT_sem_unary_proj_id AOT_model_denotes_prod_def) lemma ‹[v ⊨ Π = Π'] = [v ⊨ Π↓ & Π'↓ & ∀x1∀x2∀x3 ( [λz [Π]z x2 x3] = [λz [Π']z x2 x3] & [λz [Π]x1 z x3] = [λz [Π']x1 z x3] & [λz [Π]x1 x2 z] = [λz [Π']x1 x2 z])]› for Π :: ‹<\<kappa>×κ×κ>› by (auto simp: AOT_sem_proj_id_prop[of v Π Π'] AOT_sem_proj_id_prod_def AOT_sem_conj AOT_sem_denotes AOT_sem_forall AOT_sem_unary_proj_id AOT_model_denotes_prod_def) lemma ‹[v ⊨ Π = Π'] = [v ⊨ Π↓ & Π'↓ & ∀x1∀x2∀x3∀x4 ( [λz [Π]z x2 x3 x4] = [λz [Π']z x2 x3 x4] & [λz [Π]x1 z x3 x4] = [λz [Π']x1 z x3 x4] & [\<lambda>z [\<Pi>]x\<^sub>1 x\<^sub>2 z x\<^sub>4] = [\<lambda>z [\<Pi>']x\<^sub>1 x\<^sub>2 z x\<^sub>4] &n> [\<lambda>z [\<Pi>]x\<^sub>1 x\<^sub>2 x\<^sub>3 z] = [\<lambda>z [\<Pi>']x\<^sub>1 x\<^sub>2 x\<^sub>3 z])]\<c for \<Pi> :: \<open><\<kappa>\<times>\<kappa>\<times>\<kappa>\<times>\<kappa>>\<close> by (auto simp: AOT_sem_proj_id_prop[of v \<Pi> \<Pi>'] AOT_sem_proj_id_prod_def AOT_sem_conj AOT_sem_denotes AOT_sem_forall AOT_sem_unary_proj_id AOT_model_denotes_prod_def) text\<open>n-ary Encoding is constructed using a similar mechanism as n-ary relation identity using an auxiliary notion of projection-encoding.\<close> class AOT_Enc = fixes AOT_enc :: \<open>'a \<Rightarrow> <'a::AOT_IndividualTerm> \<Rightarrow> \<o>\<close> and AOT_proj_enc :: \<open>'a \<Rightarrow> ('a \<Rightarrow> \<o>) \<Rightarrow> \<o>\<close> assumes AOT_sem_enc_denotes: \<open>[v \<Turnstile> \<guillemotleft>AOT_enc \<kappa>\<^sub>1\<kappa>\<^sub>n \<Pi>\<guillemotright> assumes AOT_sem_enc_proj_enc: \<open>[v \<Turnstile> \<guillemotleft>AOT_enc \<kappa>\<^sub>1\<kappa>\<^sub>n \<Pi>\<guillemotright> [v \<Turnstile> \<Pi>\<down> & \<guillemotleft>AOT_proj_enc \<kappa>\<^sub>1\<kappa>\<^sub>n (\<la assumes AOT_sem_proj_enc_denotes: \<open>[v \<Turnstile> \<guillemotleft>AOT_proj_enc \<kappa>\<^sub>1\<kappa>\<^sub>n \<phi>\<guillemo assumes AOT_sem_enc_nec: \<open>[v \<Turnstile> \<guillemotleft>AOT_enc \<kappa>\<^sub>1\<kappa>\<^sub>n \<Pi>\<guillemotright> assumes AOT_sem_proj_enc_nec: \<open>[v \<Turnstile> \<guillemotleft>AOT_proj_enc \<kappa>\<^sub>1\<kappa>\<^sub>n \<phi>\<guillemo assumes AOT_sem_universal_encoder: \<open>\<exists> \<kappa>\<^sub>1\<kappa>\<^sub>n. [v \<Turnstile> \<kappa>\<^sub>1...\<kappa>\<^sub>n\<dow (\<forall> \<phi> . [v \<Turnstile> [\<lambda>z\<^sub>1...z\<^sub>n \<phi>{z\<^sub>1...z\<^sub>n}]\<down>] AOT_syntax_print_translations "_AOT_enc (_AOT_individual_term \<kappa>) (_AOT_relation_term \<Pi>)" <= "CONST AOT_enc \<kapp context AOT_meta_syntax begin notation AOT_enc (\<open>\<^bold>\<lbrace>_,_\<^bold>\<rbrace>\<close>) end context AOT_no_meta_syntax begin no_notation AOT_enc (\<open>\<^bold>\<lbrace>_,_\<^bold>\<rbrace>\<close>) end text\<open>Unary encoding additionally has to satisfy the axioms of unary encoding and the definition of property identity.\<close> class AOT_UnaryEnc = AOT_UnaryIndividualTerm + assumes AOT_sem_enc_eq: \<open>[v \<Turnstile> \<Pi>\<down> & \<Pi>'\<down> & \<box>\<forall>\< and AOT_sem_A_objects: \<open>[v \<Turnstile> \<exists>x (\<not>\<diamond>[E!]x & \<forall>F (x and AOT_sem_unary_proj_enc: \<open>AOT_proj_enc x \<psi> = AOT_enc x \<guillemotleft>[\<lambda>z and AOT_sem_nocoder: \<open>[v \<Turnstile> [E!]\<kappa>] \<Longrightarrow> \<not>[w \<Turnstile> \<g and AOT_sem_ind_eq: \<open>([v \<Turnstile> \<kappa>\<down>] \<and> [v \<Turnstile> \<kappa>'\<down>] \<an (([v \<Turnstile> [\<lambda>x \<diamond>[E!]x]\<kappa>] \<and> [v \<Turnstile> [\<lambda>x \<diamond>[E!]x]\<kappa>'] \<and> (\<forall> v \<Pi> . [v \<Turnstile> \<Pi>\<down>] \<longrightarrow> [v \<Turnstile> [\<Pi>]\<kappa>] = [v \<Tur \<or> ([v \<Turnstile> [\<lambda>x \<not>\<diamond>[E!]x]\<kappa>] \<and> [v \<Turnstile> [\<lambda>x \<not>\<diamond>[E!]x]\<kappa>'] \<and> (\<forall> v \<Pi> . [v \<Turnstile> \<Pi>\<down>] \<longrightarrow> [v \<Turnstile> \<kappa>[\<Pi>]] = [v \<Tur (* only extended models *) and : \<open>AOT_ExtendedModel \<Longrightarrow> [v \<Turnstile> [\<lambda>x \<not>\<diamond>[E!]x]\<kappa>] \<Longrightarrow *@lm_init:pointer to \<>x \not\diamond><kappa>' <> (<And \<Pi>' [ \Turnstile \Pi'<down> <> (<And> .[w \Turnstile> [\<Pi>']\<kappa>] = [w \<Turnstile> [\<Pi>']\<kap [v \<Turnstile> \<Pi>\<down>] \<Longrightarrow> <> \Pi'.[v \Turnstile> <>'\down> \<Longrightarrow>(\<And <\^sub>.[ \<urnstile>[<x <>E]]<kappa>\^ub>]\Longr (\<And> w . [w \<Turnstile> [\<Pi>']\<kappa>\<^sub>0] = [w \<Turnstile> [\<Pi java.lang.StringIndexOutO (And><>' v\Turnstile <Pi>\<down> \<Longrightarrow>(<And>\<kappa\<sub>0.[v \lambda>x \diamond>E]x]\kap (>w.[w\<Turnstile> [\Pi']<kappa>\<^sub>] <> [\Pi>]\<kappa><sub0) <Longrightarrow> [v \<Turnstile> \<kappa> and : \java.lang.StringIndexOutOfBoundsException: Range [17, 16) out of bounds for len \Turnstile> [<> \<not><>E]]<]\<ongrightarrow> [v \<Turnstile> [\<lambda *java.lang.StringIndexOutOfBoundsException: Index 0 out of b (<>'[\Turnstile<'down < (\<And>w. [w \Turnstile>[\<Pi>']<kappa> =[w <Turnstile>[\<i']\<kappa>])\<Longri [v \<Turnstile> \<Pi>\<down>] \<Longrightarrow> \<exists> \<Pi>' . [v \<Turnstile> \<Pi>'\<down>] \<and> [v \<Turnstile> \<kappa>[\<Pi>']] \<and> <Turnstile>[\<lambda> \<[!x]<kappa><^sub>]\longrightarrow> <forall> w. [ <Turnstile> [\Pi>']<><sub>] =[ \Turnstile [\<Pi>\<kappa><sub>])\Longrightarrow> \<exists> \<Pi>' . [v \<Turnstile> \<Pi>'\<down>] \<and> [v \<Turnstile> \<kappa>'[\<Pi>']] \<and> (\<forall> \<kappa>\<^sub>0 . [v \<Turnstile> [\<lambda>x \<diamond>[E!]x]\<kappa>\<^sub>0] \<longrighta (\<forall> w . [w \<Turnstile> [\<Pi>']\<kappa>\<^sub>0] = [w \<Turnstile> [\<Pi>]\<kappa>\<^sub>0]))\<close> text\<open>We specify encoding to align with the model-construction of encoding.\<close> consts AOT_sem_enc_\<kappa> :: \<open>\<kappa> \<Rightarrow> <\<kappa>> \<Rightarrow> \<o>\<close> specification(AOT_sem_enc_\<kappa>) AOT_sem_enc_\<kappa>: \<open>[v \<Turnstile> \<guillemotleft>AOT_sem_enc_\<kappa> \<kappa> \<Pi>\<guillemotright>] = (AOT_model_denotes \<kappa> \<and> AOT_model_denotes \<Pi> \<and> AOT_model_enc \<kappa> \<Pi>)\<clos by (rule exI[where x=\<open>\<lambda> \<kappa> \<Pi> . \<epsilon>\<^sub>\<o> w . AOT_model_denotes \<kappa> AOT_model_enc \<kappa> \<Pi>\<close>]) (simp add: AOT_model_proposition_choice_simp AOT_model_enc_\<kappa>_def \<kappa>.case_eq text\<open>We show that @{typ \<kappa>} satisfies the generic properties of n-ary encoding.\<clo instantiation \<kappa> :: AOT_Enc begin definition AOT_enc_\<kappa> :: \<open>\<kappa> \<Rightarrow> <\<kappa>> \<Rightarrow> \<o>\<close> where \<open>AOT_enc_\<kappa> \<equiv> AOT_sem_enc_\<kappa>\<close> definition AOT_proj_enc_\<kappa> :: \<open>\<kappa> \<Rightarrow> (\<kappa> \<Rightarrow> \<o>) \<Right \<open>AOT_proj_enc_\<kappa> \<equiv> \<lambda> \<kappa> \<phi> . AOT_enc \<kappa> \<guillemotleft>[\<lam lemma AOT_enc_\<kappa>_meta: \<open>[v \<Turnstile> \<kappa>[\<Pi>]] = (AOT_model_denotes \<kappa> \<and> AOT_model_denotes \<Pi> \<a for \<kappa>::\<kappa> using AOT_sem_enc_\<kappa> unfolding AOT_enc_\<kappa>_def by auto instance proof fix v and \<kappa> :: \<kappa> and \<Pi> show \<open>[v \<Turnstile> \<guillemotleft>AOT_enc \<kappa> \<Pi>\<guillemotright>] \<Longrightarr unfolding AOT_sem_denotes using AOT_enc_\<kappa>_meta by blast next fix v and \<kappa> :: \<kappa> and \<Pi> show \<open>[v \<Turnstile> \<kappa>[\<Pi>]] = [v \<Turnstile> \<Pi>\<down> & \<guillemotleft>AOT_pr proof assume enc: \<open>[v \<Turnstile> \<kappa>[\<Pi>]]\<close> hence \<Pi>_denotes: \<open>AOT_model_denotes \<Pi>\<close> by (simp add: AOT_enc_\<kappa>_meta) hence \<Pi>_eta_denotes: \<open>AOT_model_denotes \<guillemotleft>[\<lambda>z [\<Pi>]z]\<guille using AOT_sem_denotes AOT_sem_eq AOT_sem_lambda_eta by metis show \<open>[v \<Turnstile> \<Pi>\<down> & \<guillemotleft>AOT_proj_enc \<kappa> (\<lambda> \<kapp using AOT_sem_lambda_eta[simplified AOT_sem_denotes AOT_sem_eq, OF \<Pi>_denotes] using \<Pi>_eta_denotes \<Pi>_denotes by (simp add: AOT_sem_conj AOT_sem_denotes AOT_proj_enc_\<kappa>_def enc) next assume \<open>[v \<Turnstile> \<Pi>\<down> & \<guillemotleft>AOT_proj_enc \<kappa> (\<lambda> \<ka hence \<Pi>_denotes: "AOT_model_denotes \<Pi>" and eta_enc: "[v \<Turnstile> \<kappa>[\<lambda>z [\< by (auto simp: AOT_sem_conj AOT_sem_denotes AOT_proj_enc_\<kappa>_def) thus \<open>[v \<Turnstile> \<kappa>[\<Pi>]]\<close> using AOT_sem_lambda_eta[simplified AOT_sem_denotes AOT_sem_eq, OF \<Pi>_denotes] by auto qed next show \<open>[v \<Turnstile> \<guillemotleft>AOT_proj_enc \<kappa> \<phi>\<guillemotright>] \<Longri by (simp add: AOT_enc_\<kappa>_meta AOT_sem_denotes AOT_proj_enc_\<kappa>_def) next fix v w and \<kappa> :: \<kappa> and \<Pi> assume \<open>[v \<Turnstile> \<kappa>[\<Pi>]]\<close> thus \<open>[w \<Turnstile> \<kappa>[\<Pi>]]\<close> by (simp add: AOT_enc_\<kappa>_meta) next fix v w and \<kappa> :: \<kappa> and \<phi> assume \<open>[v \<Turnstile> \<guillemotleft>AOT_proj_enc \<kappa> \<phi>\<guillemotright>]\<clos thus \<open>[w \<Turnstile> \<guillemotleft>AOT_proj_enc \<kappa> \<phi>\<guillemotright>]\<close> by (simp add: AOT_enc_\<kappa>_meta AOT_proj_enc_\<kappa>_def) next show \<open>\<exists>\<kappa>::\<kappa>. [v \<Turnstile> \<kappa>\<down>] \<and> (\<forall> \<Pi> . [v \<Turnst (\<forall> \<phi> . [v \<Turnstile> [\<lambda>z \<phi>{z}]\<down>] \<longrightarrow> [v \<Turnstile> \<guil by (rule exI[where x=\<open>\<alpha>\<kappa> UNIV\<close>]) (simp add: AOT_sem_denotes AOT_enc_\<kappa>_meta AOT_model_enc_\<kappa>_def AOT_model_denotes_\<kappa>_def AOT_proj_enc_\<kappa>_def) qed end text\<open>We show that @{typ \<kappa>} satisfies the properties of unary encoding.\<close> instantiation \<kappa> :: AOT_UnaryEnc begin instance proof fix v and \<Pi> \<Pi>' :: \<open><\<kappa>>\<close> show \<open>[v \<Turnstile> \<Pi>\<down> & \<Pi>'\<down> & \<box>\<forall>\<nu> (\<nu>[\<Pi>] \<equiv> \< apply (simp add: AOT_sem_forall AOT_sem_eq AOT_sem_imp AOT_sem_equiv AOT_enc_\<kappa>_meta AOT_sem_conj AOT_sem_denotes AOT_sem_box) using AOT_meta_A_objects_\<kappa> by fastforce next fix v and \<phi>:: \<open><\<kappa>> \<Rightarrow> \<o>\<close> show \<open>[v \<Turnstile> \<exists>x (\<not>\<diamond>[E!]x & \<forall>F (x[F] \<equiv> \<phi>{F}) using AOT_model_A_objects[of "\<lambda> \<Pi> . [v \<Turnstile> \<phi>{\<Pi>}]"] by (auto simp: AOT_sem_denotes AOT_sem_exists AOT_sem_conj AOT_sem_not AOT_sem_dia AOT_sem_concrete AOT_enc_\<kappa>_meta AOT_sem_equiv AOT_sem_forall) next show \<open>AOT_proj_enc x \<psi> = AOT_enc x (AOT_lambda \<psi>)\<close> for x :: \<kappa> and \<psi> by (simp add: AOT_proj_enc_\<kappa>_def) next show \<open>[v \<Turnstile> [E!]\<kappa>] \<Longrightarrow> \<not> [w \<Turnstile> \<kappa>[\<Pi>]]\<clos by (simp add: AOT_enc_\<kappa>_meta AOT_sem_concrete AOT_model_nocoder) next fix v and \<kappa> \<kappa>' :: \<kappa> show \<open>([v \<Turnstile> \<kappa>\<down>] \<and> [v \<Turnstile> \<kappa>'\<down>] \<and> \<kappa> = \<kappa> (([v \<Turnstile> [\<lambda>x \<diamond>[E!]x]\<kappa>] \<and> [v \<Turnstile> [\<lambda>x \<diamond>[E!]x]\<kappa>'] \<and> (\<forall> v \<Pi> . [v \<Turnstile> \<Pi>\<down>] \<longrightarrow> [v \<Turnstile> [\<Pi>]\<kappa>] = [v \<Tur \<or> ([v \<Turnstile> [\<lambda>x \<not>\<diamond>[E!]x]\<kappa>] \<and> [v \<Turnstile> [\<lambda>x \<not>\<diamond>[E!]x]\<kappa>'] \<and> (\<forall> v \<Pi> . [v \<Turnstile> \<Pi>\<down>] \<longrightarrow> [v \<Turnstile> \<kappa>[\<Pi>]] = [v \<Tur (is \<open>?lhs = (?ordeq \<or> ?abseq)\<close>) proof - { assume 0: \<open>[v \<Turnstile> \<kappa>\<down>] \<and> [v \<Turnstile> \<kappa>'\<down>] \<and> \<kappa> = \<ka { assume \<open>is_\<omega>\<kappa> \<kappa>'\<close> hence \<open>[v \<Turnstile> [\<lambda>x \<diamond>[E!]x]\<kappa>']\<close> apply (subst AOT_sem_lambda_beta[OF AOT_sem_ordinary_def_denotes, of v \<kappa>']) apply (simp add: "0") apply (simp add: AOT_sem_dia) using AOT_sem_concrete AOT_model_\<omega>_concrete_in_some_world is_\<omega>\<kappa>_def b hence \<open>?ordeq\<close> unfolding 0[THEN conjunct2, THEN conjunct2] by auto } moreover { assume \<open>is_\<alpha>\<kappa> \<kappa>'\<close> hence \<open>[v \<Turnstile> [\<lambda>x \<not>\<diamond>[E!]x]\<kappa>']\<close> apply (subst AOT_sem_lambda_beta[OF AOT_sem_abstract_def_denotes, of v \<kappa>']) apply (simp add: "0") apply (simp add: AOT_sem_not AOT_sem_dia) using AOT_sem_concrete is_\<alpha>\<kappa>_def by force hence \<open>?abseq\<close> unfolding 0[THEN conjunct2, THEN conjunct2] by auto } ultimately have \<open>?ordeq \<or> ?abseq\<close> by (meson "0" AOT_sem_denotes AOT_model_denotes_\<kappa>_def \<kappa>.exhaust_disc) } moreover { assume ordeq: \<open>?ordeq\<close> hence \<kappa>_denotes: \<open>[v \<Turnstile> \<kappa>\<down>]\<close> and \<kappa>'_denotes: \<open>[ by (simp add: AOT_sem_denotes AOT_sem_exe)+ hence \<open>is_\<omega>\<kappa> \<kappa>\<close> and \<open>is_\<omega>\<kappa> \<kappa>'\<close> by (metis AOT_model_concrete_\<kappa>.simps(2) AOT_model_denotes_\<kappa>_def AOT_sem_concrete AOT_sem_denotes AOT_sem_dia AOT_sem_lambda_beta AOT_sem_ordinary_def_denotes \<kappa>.collapse(2) \<kappa>.exhaust_disc ordeq)+ have denotes: \<open>[v \<Turnstile> [\<lambda>z \<guillemotleft>\<epsilon>\<^sub>\<o> w . \<kappa>\<upsi unfolding AOT_sem_denotes AOT_model_lambda_denotes by (simp add: AOT_model_term_equiv_\<kappa>_def) hence "[v \<Turnstile> [\<lambda>z \<guillemotleft>\<epsilon>\<^sub>\<o> w . \<kappa>\<upsilon> z = \<kappa> using ordeq by (simp add: AOT_sem_denotes) hence \<open>[v \<Turnstile> \<guillemotleft>\<kappa>\<guillemotright>\<down>] \<and> [v \<Turnstile> \< unfolding AOT_sem_lambda_beta[OF denotes, OF \<kappa>_denotes] AOT_sem_lambda_beta[OF denotes, OF \<kappa>'_denotes] using \<kappa>'_denotes \<open>is_\<omega>\<kappa> \<kappa>'\<close> \<open>is_\<omega>\<kappa> \<kappa>\< AOT_model_proposition_choice_simp by force } moreover { assume 0: \<open>?abseq\<close> hence \<kappa>_denotes: \<open>[v \<Turnstile> \<kappa>\<down>]\<close> and \<kappa>'_denotes: \<open>[ by (simp add: AOT_sem_denotes AOT_sem_exe)+ hence \<open>\<not>is_\<omega>\<kappa> \<kappa>\<close> and \<open>\<not>is_\<omega>\<kappa> \<kappa>'\<clos by (metis AOT_model_\<omega>_concrete_in_some_world AOT_model_concrete_\<kappa>.simps(1 AOT_sem_concrete AOT_sem_dia AOT_sem_exe AOT_sem_lambda_beta AOT_sem_not \<kappa>.collapse(1) 0)+ hence \<open>is_\<alpha>\<kappa> \<kappa>\<close> and \<open>is_\<alpha>\<kappa> \<kappa>'\<close> by (meson AOT_sem_denotes AOT_model_denotes_\<kappa>_def \<kappa>.exhaust_disc \<kappa>_denotes \<kappa>'_denotes)+ then obtain x y where \<kappa>_def: \<open>\<kappa> = \<alpha>\<kappa> x\<close> and \<kappa>'_def: \<open>\< using is_\<alpha>\<kappa>_def by auto { fix r assume \<open>r \<in> x\<close> hence \<open>[v \<Turnstile> \<kappa>[\<guillemotleft>urrel_to_rel r\<guillemotright>]]\<close> unfolding \<kappa>_def unfolding AOT_enc_\<kappa>_meta unfolding AOT_model_enc_\<kappa>_def apply (simp add: AOT_model_denotes_\<kappa>_def) by (metis (mono_tags) AOT_rel_equiv_def Quotient_def urrel_quotient) hence \<open>[v \<Turnstile> \<kappa>'[\<guillemotleft>urrel_to_rel r\<guillemotright>]]\<close> using AOT_enc_\<kappa>_meta 0 by (metis AOT_sem_enc_denotes) hence \<open>r \<in> y\<close> unfolding \<kappa>'_def unfolding AOT_enc_\<kappa>_meta unfolding AOT_model_enc_\<kappa>_def apply (simp add: AOT_model_denotes_\<kappa>_def) using Quotient_abs_rep urrel_quotient by fastforce } moreover { fix r assume \<open>r \<in> y\<close> hence \<open>[v \<Turnstile> \<kappa>'[\<guillemotleft>urrel_to_rel r\<guillemotright>]]\<close> unfolding \<kappa>'_def unfolding AOT_enc_\<kappa>_meta unfolding AOT_model_enc_\<kappa>_def apply (simp add: AOT_model_denotes_\<kappa>_def) by (metis (mono_tags) AOT_rel_equiv_def Quotient_def urrel_quotient) hence \<open>[v \<Turnstile> \<kappa>[\<guillemotleft>urrel_to_rel r\<guillemotright>]]\<close> using AOT_enc_\<kappa>_meta 0 by (metis AOT_sem_enc_denotes) hence \<open>r \<in> x\<close> unfolding \<kappa>_def unfolding AOT_enc_\<kappa>_meta unfolding AOT_model_enc_\<kappa>_def apply (simp add: AOT_model_denotes_\<kappa>_def) using Quotient_abs_rep urrel_quotient by fastforce } ultimately have "x = y" by blast hence \<open>[v \<Turnstile> \<kappa>\<down>] \<and> [v \<Turnstile> \<kappa>'\<down>] \<and> \<kappa> = \<kappa> using \<kappa>'_def \<kappa>'_denotes \<kappa>_def by blast } ultimately show ?thesis unfolding AOT_sem_denotes by auto qed (* Only extended model *) next fix v and \<kappa> \<kappa>' :: \<kappa> and \<Pi> \<Pi>' :: \<open><\<kappa>>\<close> assume ext: \<open>AOT_ExtendedModel\<close> assume \<open>[v \<Turnstile> [\<lambda>x \<not>\<diamond>[E!]x]\<kappa>]\<close> hence \<open>is_\<alpha>\<kappa> \<kappa>\<close> by (metis AOT_model_\<omega>_concrete_in_some_world AOT_model_concrete_\<kappa>.simps(1 AOT_model_denotes_\<kappa>_def AOT_sem_concrete AOT_sem_denotes AOT_sem_dia AOT_sem_exe AOT_sem_lambda_beta AOT_sem_not \<kappa>.collapse(1) \<kappa>.exhaust_disc) hence \<kappa>_abs: \<open>\<not>(\<exists> w . AOT_model_concrete w \<kappa>)\<close> using is_\<alpha>\<kappa>_def by fastforce have \<kappa>_den: \<open>AOT_model_denotes \<kappa>\<close> by (simp add: AOT_model_denotes_\<kappa>_def \<kappa>.distinct_disc(5) \<open>is_\<alpha>\<kap assume \<open>[v \<Turnstile> [\<lambda>x \<not>\<diamond>[E!]x]\<kappa>']\<close> hence \<open>is_\<alpha>\<kappa> \<kappa>'\<close> by (metis AOT_model_\<omega>_concrete_in_some_world AOT_model_concrete_\<kappa>.simps(1 AOT_model_denotes_\<kappa>_def AOT_sem_concrete AOT_sem_denotes AOT_sem_dia AOT_sem_exe AOT_sem_lambda_beta AOT_sem_not \<kappa>.collapse(1) \<kappa>.exhaust_disc) hence \<kappa>'_abs: \<open>\<not>(\<exists> w . AOT_model_concrete w \<kappa>')\<close> using is_\<alpha>\<kappa>_def by fastforce have \<kappa>'_den: \<open>AOT_model_denotes \<kappa>'\<close> by (meson AOT_model_denotes_\<kappa>_def \<kappa>.distinct_disc(6) \<open>is_\<alpha>\<kappa> \< assume \<open>[v \<Turnstile> \<Pi>'\<down>] \<Longrightarrow> [w \<Turnstile> [\<Pi>']\<kappa>] = [w \<Tur hence indist: \<open>[v \<Turnstile> \<guillemotleft>Rep_rel \<Pi>' \<kappa>\<guillemotright>] = [v \< if \<open>AOT_model_denotes \<Pi>'\<close> for \<Pi>' v by (metis AOT_sem_denotes AOT_sem_exe \<kappa>'_den \<kappa>_den that) assume \<kappa>_enc_cond: \<open>[v \<Turnstile> \<Pi>'\<down>] \<Longrightarrow> (\<And> \<kappa>\<^sub>0 w. [v \<Turnstile> [\<lambda>x \<diamond>[E!]x]\<kappa>\<^sub>0] \<Longrightarr [w \<Turnstile> [\<Pi>']\<kappa>\<^sub>0] = [w \<Turnstile> [\<Pi>]\<kappa>\<^sub>0]) \<Longrightarrow> [v \<Turnstile> \<kappa>[\<Pi>']]\<close> for \<Pi>' assume \<Pi>_den': \<open>[v \<Turnstile> \<Pi>\<down>]\<close> hence \<Pi>_den: \<open>AOT_model_denotes \<Pi>\<close> using AOT_sem_denotes by blast { fix \<Pi>' :: \<open><\<kappa>>\<close> assume \<Pi>'_den: \<open>AOT_model_denotes \<Pi>'\<close> hence \<Pi>'_den': \<open>[v \<Turnstile> \<Pi>'\<down>]\<close> by (simp add: AOT_sem_denotes) assume 1: \<open>\<exists>w. AOT_model_concrete w x \<Longrightarrow> [v \<Turnstile> \<guillemotleft>Rep_rel \<Pi>' x\<guillemotright>] = [v \<Turnstile> \<guillemotlef { fix \<kappa>\<^sub>0 :: \<kappa> and w assume \<open>[v \<Turnstile> [\<lambda>x \<diamond>[E!]x]\<kappa>\<^sub>0]\<close> hence \<open>is_\<omega>\<kappa> \<kappa>\<^sub>0\<close> by (smt (z3) AOT_model_concrete_\<kappa>.simps(2) AOT_model_denotes_\<kappa>_def AOT_sem_concrete AOT_sem_denotes AOT_sem_dia AOT_sem_exe AOT_sem_lambda_beta \<kappa>.exhaust_disc is_\<alpha>\<kappa>_def) then obtain x where x_prop: \<open>\<kappa>\<^sub>0 = \<omega>\<kappa> x\<close> using is_\<omega>\<kappa>_def by blast have \<open>\<exists>w . AOT_model_concrete w (\<omega>\<kappa> x)\<close> by (simp add: AOT_model_\<omega>_concrete_in_some_world) hence \<open>[v \<Turnstile> \<guillemotleft>Rep_rel \<Pi>' (\<omega>\<kappa> x)\<guillemotright>] = [ using 1 by blast hence \<open>[w \<Turnstile> [\<Pi>']\<kappa>\<^sub>0] = [w \<Turnstile> [\<Pi>]\<kappa>\<^sub>0]\<close> un by (simp add: AOT_sem_exe AOT_sem_denotes AOT_model_denotes_\<kappa>_def \<Pi>'_den \<Pi>_den) } note 2 = this have \<open>[v \<Turnstile> \<kappa>[\<Pi>']]\<close> using \<kappa>_enc_cond[OF \<Pi>'_den', OF 2] by metis hence \<open>AOT_model_enc \<kappa> \<Pi>'\<close> using AOT_enc_\<kappa>_meta by blast } note \<kappa>_enc_cond = this hence \<open>AOT_model_denotes \<Pi>' \<Longrightarrow> (\<And>v x. \<exists>w. AOT_model_concrete w x \<Longrightarrow> [v \<Turnstile> \<guillemotleft>Rep_rel \<Pi>' x\<guillemotright>] = [v \<Turnstile> \<guillemotlef AOT_model_enc \<kappa> \<Pi>'\<close> for \<Pi>' by blast assume \<Pi>'_den': \<open>[v \<Turnstile> \<Pi>'\<down>]\<close> hence \<Pi>'_den: \<open>AOT_model_denotes \<Pi>'\<close> using AOT_sem_denotes by blast assume ord_indist: \<open>[v \<Turnstile> [\<lambda>x \<diamond>[E!]x]\<kappa>\<^sub>0] \<Longright [w \<Turnstile> [\<Pi>']\<kappa>\<^sub>0] = [w \<Turnstile> [\<Pi>]\<kappa>\<^sub>0]\<close> for \<kappa>\<^s { fix w and \<kappa>\<^sub>0 :: \<kappa> assume 0: \<open>\<exists>w. AOT_model_concrete w \<kappa>\<^sub>0\<close> hence \<open>[v \<Turnstile> [\<lambda>x \<diamond>[E!]x]\<kappa>\<^sub>0]\<close> using AOT_model_concrete_denotes AOT_sem_concrete AOT_sem_denotes AOT_sem_dia AOT_sem_lambda_beta AOT_sem_ordinary_def_denotes by blast hence \<open>[w \<Turnstile> [\<Pi>']\<kappa>\<^sub>0] = [w \<Turnstile> [\<Pi>]\<kappa>\<^sub>0]\<close> using ord_indist by metis hence \<open>[w \<Turnstile> \<guillemotleft>Rep_rel \<Pi>' \<kappa>\<^sub>0\<guillemotright>] = [w \<T by (metis AOT_model_concrete_denotes AOT_sem_denotes AOT_sem_exe \<Pi>'_den \<Pi>_den 0) } note ord_indist = this have \<open>AOT_model_enc \<kappa>' \<Pi>'\<close> using AOT_model_enc_indistinguishable_all [OF ext, OF \<kappa>_den, OF \<kappa>_abs, OF \<kappa>'_den, OF \<kappa>'_abs, OF \<Pi>_den] indist \<kappa>_enc_cond \<Pi>'_den ord_indist by blast thus \<open>[v \<Turnstile> \<kappa>'[\<Pi>']]\<close> using AOT_enc_\<kappa>_meta \<Pi>'_den \<kappa>'_den by blast next fix v and \<kappa> \<kappa>' :: \<kappa> and \<Pi> \<Pi>' :: \<open><\<kappa>>\<close> assume ext: \<open>AOT_ExtendedModel\<close> assume \<open>[v \<Turnstile> [\<lambda>x \<not>\<diamond>[E!]x]\<kappa>]\<close> hence \<open>is_\<alpha>\<kappa> \<kappa>\<close> by (metis AOT_model_\<omega>_concrete_in_some_world AOT_model_concrete_\<kappa>.simps(1 AOT_model_denotes_\<kappa>_def AOT_sem_concrete AOT_sem_denotes AOT_sem_dia AOT_sem_exe AOT_sem_lambda_beta AOT_sem_not \<kappa>.collapse(1) \<kappa>.exhaust_disc) hence \<kappa>_abs: \<open>\<not>(\<exists> w . AOT_model_concrete w \<kappa>)\<close> using is_\<alpha>\<kappa>_def by fastforce have \<kappa>_den: \<open>AOT_model_denotes \<kappa>\<close> by (simp add: AOT_model_denotes_\<kappa>_def \<kappa>.distinct_disc(5) \<open>is_\<alpha>\<kap assume \<open>[v \<Turnstile> [\<lambda>x \<not>\<diamond>[E!]x]\<kappa>']\<close> hence \<open>is_\<alpha>\<kappa> \<kappa>'\<close> by (metis AOT_model_\<omega>_concrete_in_some_world AOT_model_concrete_\<kappa>.simps(1 AOT_model_denotes_\<kappa>_def AOT_sem_concrete AOT_sem_denotes AOT_sem_dia AOT_sem_exe AOT_sem_lambda_beta AOT_sem_not \<kappa>.collapse(1) \<kappa>.exhaust_disc) hence \<kappa>'_abs: \<open>\<not>(\<exists> w . AOT_model_concrete w \<kappa>')\<close> using is_\<alpha>\<kappa>_def by fastforce have \<kappa>'_den: \<open>AOT_model_denotes \<kappa>'\<close> by (meson AOT_model_denotes_\<kappa>_def \<kappa>.distinct_disc(6) \<open>is_\<alpha>\<kappa> \< assume \<open>[v \<Turnstile> \<Pi>'\<down>] \<Longrightarrow> [w \<Turnstile> [\<Pi>']\<kappa>] = [w \<Tur hence indist: \<open>[v \<Turnstile> \<guillemotleft>Rep_rel \<Pi>' \<kappa>\<guillemotright>] = [v \< if \<open>AOT_model_denotes \<Pi>'\<close> for \<Pi>' v by (metis AOT_sem_denotes AOT_sem_exe \<kappa>'_den \<kappa>_den that) assume \<Pi>_den': \<open>[v \<Turnstile> \<Pi>\<down>]\<close> hence \<Pi>_den: \<open>AOT_model_denotes \<Pi>\<close> using AOT_sem_denotes by blast assume \<open>\<exists>\<Pi>'. [v \<Turnstile> \<Pi>'\<down>] \<and> [v \<Turnstile> \<kappa>[\<Pi>']] \<and> (\<forall>\<kappa>\<^sub>0. [v \<Turnstile> [\<lambda>x \<diamond>[E!]x]\<kappa>\<^sub>0] \<longrighta (\<forall>w. [w \<Turnstile> [\<Pi>']\<kappa>\<^sub>0] = [w \<Turnstile> [\<Pi>]\<kappa>\<^sub>0]))\<close> then obtain \<Pi>' where \<Pi>'_den: \<open>[v \<Turnstile> \<Pi>'\<down>]\<close> and \<Pi>'_enc: \<open>[v \<Turnstile> \<kappa>[\<Pi>']]\<close> and \<Pi>'_prop: \<open>\<forall>\<kappa>\<^sub>0. [v \<Turnstile> [\<lambda>x \<diamond>[E!]x]\<kappa>\<^su (\<forall>w. [w \<Turnstile> [\<Pi>']\<kappa>\<^sub>0] = [w \<Turnstile> [\<Pi>]\<kappa>\<^sub>0])\<close> by blast have \<open>AOT_model_denotes \<Pi>'\<close> using AOT_enc_\<kappa>_meta \<Pi>'_enc by force moreover have \<open>AOT_model_enc \<kappa> \<Pi>'\<close> using AOT_enc_\<kappa>_meta \<Pi>'_enc by blast moreover have \<open>(\<exists>w. AOT_model_concrete w \<kappa>\<^sub>0) \<Longrightarrow> [v \<Turnstile> \<guillemotleft>Rep_rel \<Pi>' \<kappa>\<^sub>0\<guillemotright>] = [v \<Turnstile> \<g proof - assume 0: \<open>\<exists>w. AOT_model_concrete w \<kappa>\<^sub>0\<close> hence \<open>[v \<Turnstile> [\<lambda>x \<diamond>[E!]x]\<kappa>\<^sub>0]\<close> for v using AOT_model_concrete_denotes AOT_sem_concrete AOT_sem_denotes AOT_sem_dia AOT_sem_lambda_beta AOT_sem_ordinary_def_denotes by blast hence \<open>\<forall>w. [w \<Turnstile> [\<Pi>']\<kappa>\<^sub>0] = [w \<Turnstile> [\<Pi>]\<kappa>\<^sub>0 thus \<open>[v \<Turnstile> \<guillemotleft>Rep_rel \<Pi>' \<kappa>\<^sub>0\<guillemotright>] = [v \<Tu by (meson "0" AOT_model_concrete_denotes AOT_sem_denotes AOT_sem_exe \<Pi>_den calculation(1)) qed ultimately have \<open>\<exists>\<Pi>'. AOT_model_denotes \<Pi>' \<and> AOT_model_enc \<kappa> \<Pi>' \< (\<forall>v x. (\<exists>w. AOT_model_concrete w x) \<longrightarrow> [v \<Turnstile> \<guillemotleft>Rep_rel \<Pi>' x\<guillemotright>] = [v \<Turnstile> \<guillemotlef by blast hence ‹∃Π'. AOT_model_denotes Π' ∧ AOT_model_enc κ' Π' ∧ (∀v x. (∃w. AOT_model_concrete w x) ⟶ [v ⊨ «Rep_rel Π' x¬] = [v ⊨ «Rep_rel Π x¬])› using AOT_model_enc_indistinguishable_ex [OF ext, OF κ_den, OF κ_abs, OF κ'_den, OF κ'_abs, OF Π_den] indist by blast then obtain Π'' where Π''_den: ‹AOT_model_denotes Π''› and Π''_enc: ‹AOT_model_enc κ' Π''› and Π''_prop: ‹(∃w. AOT_model_concrete w x) ==> [v ⊨ «Rep_rel Π'' x¬] = [v ⊨ «Rep_rel Π x¬]› for v x by blast have ‹[v ⊨ Π''↓]› by (simp add: AOT_sem_denotes Π''_den) moreover have ‹[v ⊨ κ'[Π'']]› by (simp add: AOT_enc_κ_meta Π''_den Π''_enc κ'_den) moreover have ‹[v ⊨ [λx ♢[E!]x]κ0] ==> (∀w. [w ⊨ [Π'']κ0] = [w ⊨ [Π]κ0])› for κ0 proof - assume ‹[v ⊨ [λx ♢[E!]x]κ0]› hence ‹∃w. AOT_model_concrete w κ0› by (metis AOT_sem_concrete AOT_sem_dia AOT_sem_exe AOT_sem_lambda_beta) thus ‹∀w. [w ⊨ [Π'']κ0] = [w ⊨ [Π]κ0]› using Π''_prop by (metis AOT_sem_denotes AOT_sem_exe Π''_den Π_den) qed ultimately show ‹∃Π'. [v ⊨ Π'↓] ∧ [v ⊨ κ'[Π']] ∧ (∀κ0. [v ⊨ [λx ♢[E!]x]κ0] ⟶ (∀w. [w ⊨ [Π']κ0] = [w ⊨ [Π]κ0]))› by (safe intro!: exI[where x=Π'']) blast+ ‹Define encoding for products using projection-encoding.› prod :: (AOT_UnaryEnc, AOT_Enc) AOT_Enc AOT_proj_enc_prod :: ‹'a×'b → ('a×'b → o) → o› where ‹AOT_proj_enc_prod ≡ λ (κ,κ') φ . «κ[λν «φ (ν,κ')¬] & «AOT_proj_enc κ' (λν. φ (κ,ν))¬¬› AOT_enc_prod :: ‹'a×'b → <'a×'b> → o› where ‹AOT_enc_prod ≡ λ κ Π . «Π↓ & «AOT_proj_enc κ (λ κ1'κn'. «[Π]κ1'. proof show ‹[v ⊨ κ1...κn[Π]] ==> [v ⊨ κ1...κn↓] ∧ [v ⊨ Π↓]› for v and κ1κn :: ‹'a×'b› and Π unfolding AOT_enc_prod_def apply (induct κ1κn; simp add: AOT_sem_conj AOT_sem_denotes AOT_proj_enc_prod_def) by (metis AOT_sem_denotes AOT_model_denotes_prod_def AOT_sem_enc_denotes AOT_sem_proj_enc_denotes case_prodI) show ‹[v ⊨ κ1...κn[Π]] = [v ⊨ «Π¬↓ & «AOT_proj_enc κ1κn (λ κ1κn. «[Π]κ1...κn¬)¬]› for v and κ1κn :: ‹'a×'b› and Π unfolding AOT_enc_prod_def .. show ‹[v ⊨ «AOT_proj_enc κs φ¬] ==> [v ⊨ «κs¬↓]› for v and κs :: ‹'a×'b› and φ by (metis (mono_tags, lifting) AOT_sem_conj AOT_sem_denotes AOT_model_denotes_prod_def AOT_sem_enc_denotes AOT_sem_proj_enc_denotes AOT_proj_enc_prod_def case_prod_unfold) fix v w Π and κ1κn :: ‹'a×'b› show ‹[w ⊨ κ1...κn[Π]]› if ‹[v ⊨ κ1...κn[Π]]› for v w Π and κ1κn :: ‹'a×'b› by (metis (mono_tags, lifting) AOT_enc_prod_def AOT_sem_enc_proj_enc AOT_sem_conj AOT_sem_denotes AOT_sem_proj_enc_nec AOT_proj_enc_prod_def case_prod_unfold that) show ‹[w ⊨ «AOT_proj_enc κ1κn φ¬]› if ‹[v ⊨ «AOT_proj_enc κ1κn φ¬]› for v w φ and κ1κn :: ‹'a×'b› by (metis (mono_tags, lifting) that AOT_sem_enc_proj_enc AOT_sem_conj AOT_sem_denotes AOT_sem_proj_enc_nec AOT_proj_enc_prod_def case_prod_unfold) fix v obtain κ :: 'a where a_prop: ‹[v ⊨ κ↓] ∧ (∀ Π . [v ⊨ Π↓] ⟶ [v ⊨ κ[Π]])› using AOT_sem_universal_encoder by blast obtain κthaN WARRAN is provided. ‹ [v ⊨ «AOT_proj_enc κ1'κn' φ¬])› using AOT_sem_universal_encoder by blast have ‹AOT_model_denotes «[λν1...νn [«Π¬]ν1...νn κ1'...κn']¬› if ‹AOT_model_denotes Π› for Π :: ‹<'a‹"Lamport:2002"›) and closely unfolding AOT_model_lambda_denotes by (metis AOT_meta_prod_equivI(2) AOT_sem_exe_equiv) moreover have ‹AOT_model_denotes «[λν1...νn [«Π¬]κ ν1...νn]¬› if ‹AOT_model_denotes Π› for Π :: ‹<'a‹"AptFrancezDeRoever:1980"›, unfolding AOT_model_lambda_denotes by (metis AOT_meta_prod_equivI(1) AOT_sem_exe_equiv) ultimately have 1: ‹[v ⊨ «(κ,κ1'κn')¬↓]› and 2: ‹(∀ Π . [v ⊨ Π↓] ⟶ [v ⊨ κ κ1'...κn'[Π]])› using a_prop b_prop by (auto simp: AOT_sem_denotes AOT_enc_κ_meta AOT_model_enc_κ_def AOT_model_denotes_κ_def AOT_model_denotes_prod_def AOT_enc_prod_def AOT_proj_enc_prod_def AOT_sem_conj) have ‹AOT_model_denotes «[λz1...zn «φ (z1zn, κ1'κn')¬]¬› if ‹AOT_model_denotes «[λz1...zm φ{z1...zm}]¬› for φ :: ‹'a×'b → o› using that unfolding AOT_model_lambda_denotes by (metis (no_types, lifting) AOT_sem_denotes AOT_model_denotes_prod_def AOT_meta_prod_equivI(2) b_prop case_prodI) moreover have ‹AOT_model_denotes «[λz1...zn «φ (κ, z1zn)¬]¬› if ‹AOT_model_denotes «[λz1...zm φ{z1...zm}]¬› for φ :: ‹'a×'b → o› using that unfolding AOT_model_lambda_denotes by (metis (no_types, lifting) AOT_sem_denotes AOT_model_denotes_prod_def AOT_meta_prod_equivI(1) a_prop case_prodI) ultimately have 3: ‹[v ⊨ «(κ,κ1'κn')¬↓] ∧ (∀ φ . [v ⊨ [λz1...zn φ{z1...zn}]↓] ⟶ [v ⊨ «AOT_proj_enc (κ,κ1'κn') φ¬])› using a_prop b_prop by (auto simp: AOT_sem_denotes AOT_enc_κ_meta AOT_model_enc_κ_def AOT_model_denotes_κ_def AOT_enc_prod_def AOT_proj_enc_prod_def AOT_sem_conj AOT_model_denotes_prod_def) show ‹∃κ1κn::'a×'b. [v ⊨ κ1...κn↓] ∧ (∀ Π . [v ⊨ Π↓] ⟶ [v ⊨ κ1...κn[Π]]) ∧ (∀ φ . [v ⊨ [λz1...zn «φ z1zn¬]↓] ⟶ [v ⊨ «AOT_proj_enc κ1κn φ¬])› apply (rule exI[where x=‹(κ,κ1'κn')›]) using 1 2 3 by blast ‹Sanity-check to verify that n-ary encoding follows.› ‹[v ⊨ κ1κ2[Π]] = [v ⊨ Π↓ & κ1[λν [Π]νκ2] & κ2[λν [Π]κ1ν]]› for κ1 :: "'a::AOT_UnaryEnc" and κ2 :: "'b::AOT_UnaryEnc" by (simp add: AOT_sem_conj AOT_enc_prod_def AOT_proj_enc_prod_def AOT_sem_unary_proj_enc) ‹[v ⊨ κ1κ2κ3[Π]] = [v ⊨ Π↓ & κ1[λν [Π]νκ2κ3] & κ2[λν [Π]κ1νκ3] & κ3[λν [Π]κ1κ2ν]]› for κ1 κ2 κ3 :: "'a::AOT_UnaryEnc" by (simp add: AOT_sem_conj AOT_enc_prod_def AOT_proj_enc_prod_def AOT_sem_unary_proj_enc) AOT_sem_vars_denote: ‹[v ⊨ α1...αn↓]› by induct simp ‹Combine the introduced type classes and register them as type constraints for individual terms.› AOT_κs = AOT_IndividualTerm + AOT_RelationProjection + AOT_Enc AOT_κ = AOT_κs + AOT_UnaryIndividualTerm + AOT_UnaryRelationProjection + AOT_UnaryEnc κ :: AOT_κ by standard prod :: (AOT_κ, AOT_κs) AOT_κs by standard Individual: ‹_::AOT_κ› ‹_::AOT_κs› and Relation: ‹<_: ‹We define semantic predicates to capture the conditions of cqt.2 (i.e. the base cases of denoting terms) on matrices of @{text λ}-expressions.› AOT_instance_of_cqt_2 :: ‹('a::AOT_κs → o) → bool› where ‹ AOT_model_term_equiv x y ⟶ φ x = φ y› AOT_instance_of_cqt_2_exe_arg :: ‹('a::AOT_κs → 'b::AOT_κs) → bool› where ‹AOT_instance_of_cqt_2_exe_arg ≡ λ AOT_model_denotes x ∧ AOT_model_denotes y ∧ AOT_model_term_equiv x y ⟶ AOT_model_term_equiv (φ x) (φ y)› ‹@{text λ}-expressions with a matrix that satisfies our predicate denote.› AOT_sem_cqt_2: assumes ‹AOT_instance_of_cqt_2 φ› shows ‹[v ⊨ [λν1...νn φ{ν1...νn}]↓]› using assms by (metis AOT_instance_of_cqt_2_def AOT_model_lambda_denotes AOT_sem_denotes) AOT_instance_of_cqt_2 :: ‹id_position → AOT_prop› (‹INSTANCE'_OF'_CQT'_2'(_')›) ‹Prove introduction rules for the predicates that match the natura restrictions of the axiom. AOT_instance_of_cqt_2_intro AOT_l unfolding prerun_def by (metis (full_types) i old.unit.exhaust system ‹AOT_instance_of_cqt_2 (λα. φ)› by (simp add: AOT_instance_of_cqt_2_def AOT_sem_denotes AOT_model_lambda_denotes AOT_instance_of_cqt_2_intros_not[AOT_instance_of_cqt_2_intro]: assumes ‹ shows ‹AOT_instance_of_cqt_2 (λ using assms by (metis (no_types, lifting) AOT_instance_of_cqt_2_def) java.lang.StringIndexOutOfBoundsException: Range [38, 5) out of bounds for lengt java.lang.StringIndexOutOfBoundsException: Range [11, 9) out of bounds for lengt shows ‹AOT_instance_of_cqt_2 (λτ. «φ{τ} → ψ{τ}¬)› using assms by (auto simp: AOT_instance_of_cqt_2_def AOT_sem_denotes AOT_model_lambda_denotes AOT_sem_imp) AOT_instance_of_cqt_2_intros_box[AOT_instance_of_cqt_2_intro]: assumes ‹AOT_instance_of_cqt_2 φ› shows ‹ using assms by (auto simp: AOT_instance_of_cqt_2_def AOT_sem_denotes AOT_model_lambda_denotes AOT_sem_box) AOT_instance_of_cqt_2_intros_act[AOT_instance_of_cqt_2_intro]: assumes ‹AOT_instance_of_cqt_2 φ› shows ‹AOT_instance_of_cqt_2 (λτ. «directly executed (\Srefsec:cimp-decompo}).Weals using assms by (auto simp: AOT_instance_of_cqt_2_def AOT_sem_denotes AOT_model_lambda_denotes AOT_sem_act) AOT_instance_of_cqt_2_intros_diamond[AOT_instance_of_cqt_2_intro]: assumes ‹AOT_instance_of_cqt_2 φ› shows ‹ using assms by (auto simp: AOT_instance_of_cqt_2_def AOT_sem_denotes AOT_model_lambda_denotes AOT_sem_dia) AOT_instance_o]: \openAOT\phi>\ an \openAOT_ \<><java.lang.StringIndexOutOfBoundsException: Range [ using assms by (auto simp: AOT_instance_of_cqt_2_def AOT_sem_denotes AOT_model_lambda_denotes AOT_sem_conj) AOT_instance_of_cqt_2_intros_disj[AOT_instance_of_cqt_2_intro]: assumes ‹AOT_instance_of_cqt_2 φ› and ‹AOT_instance_of_cqt_2 ψ› shows ‹ using assms by (auto simp: AOT_instance_of_cqt_2_def AOT_sem_denotes AOT_model_lambda_denotes AOT_sem_disj)) AOT_instance_of_cqt_2_intros_equib[AOT_instance_of_cqt_2_intro]: assumes ‹AOT_instance_of_cqt_2 φ› and ‹ java.lang.StringIndexOutOfBoundsException: Range [8, 7) out of bounds for length using assms by (auto simp: AOT_instance_of_cqt_2_def AOT_sem_denotes AOT_model_lambda_denotes AOT_sem_equiv) AOT_instance_of_cqt_2_intros_forall[AOT_instance_of_cqt_2_intro]: assumes ‹∧ α . AOT_instance_of_cqt_2 (Φ α)› shows ‹AOT_instance_of_cqt_2 (λτ. «∀α Φ{α,τ}¬)› assms by (auto simp: AOT_instance_of_cqt_2_def AOT_sem_denotes AOT_model_lambda_denotes AOT_sem_forall) assumes ‹∧ α . AOT_instance_of_cqt_2 (Φ shows ‹AOT_instance_of_cqt_2 (λτ. «∃α Φ{α,τ}¬ using assms by (auto simp: AOT_instance_of_cqt_2_def AOT_sem_denote "decompose_com (c1;; c2 AOT_instance_of_cqt_2_intros_exe_arg_self[AOT_in shows "ictxt c' = c" ‹AOT_instance_of_cqt_2_exe_arg (λx. x)› unfolding AOT_instance_of_cqt_2_exe_arg_def AOT_instance_of_cqt_2_def AOT_sem_lambda_denotes by (auto simp: AOT_model_term_equiv_part_equivp equivp_reflp AOT_sem_denotes) AOT_instance_of_cqt_2_intros_exe_arg_const[AOT_instance_of_cqt_2_intro]: ‹ unfolding AOT_instance_of_cqt_2_exe_arg_def AOT_instance_of_cqt_2_def by (auto simp: AOT_model_term_equiv_part_equivp equivp_reflp AOT_sem_denotes AOT_sem_lambda_denotes) AOT_instance_of_cqt_2_intros_exe_arg_fst[AOT_instance_of_cqt_2_intro]: <>OT_instance_of_cqt_2_exe_arg unfolding AOT_instance_of_cqt_2_exe_arg_def AOT_instance_of_cqt_2_def :AOT_model_term_equiv_prod_def case_prod_beta) AOT_instance_of_cqt_2_intros_exe_arg_snd[AOT_instance_of_cqt_2_intro]: ‹ unfolding AOT_instance_of_cqt_2_exe_arg_def AOT_instance_of_cqt_2_def by (simp add: AOT_model_term_equiv_prod_def AOT_sem_denotes AOT_sem_lambda_denot AOT_instance_of_cqt_2_intros_exe_arg_Pair[AOT_instance_of_cqt_2_intro]: assumes ‹AOT_instance_of_cqt_2_exe_arg φ› and ‹ shows ‹AOT_instance_of_cqt_2_exe_arg (λτ. Pair (φ"(c, ictxt, fctxt) ∈ decomposeLS s using assms unfolding AOT_instance_of_cqt_2_exe_arg_def AOT_instance_of_cqt_2_def AOT_sem_denotes AOT_sem_lambda_denotes AOT_model_term_equiv_prod_def AOT_model_denotes_prod_def AOT_instance_of_cqt_2_intros_desc[AOT_instance_of_cqt_2_intro]: assumes ‹∧z :: 'a::AOT_κdecompose) shows ‹AOT_instance_of_cqt_2_exe_arg (λassumes "basic_com c" - have 0: ‹∧ κ κ'. AOT_model_denotes κ ∧ AOT_model_denotes κ' ∧ AOT_model_term_equiv κ κ' ==> Φ z κ using assms unfolding AOT_instance_of_cqt_2_def AOT_sem_denotes AOT_model_lambda_denotes by force { fix κ κ' have ‹«\ιz(Φ{z,κ})¬ = assumes "reachable_state sys sh" if ‹AOT_model_denotes κ ∧ AOT_model_denotes κ' ∧obtains c cs aft using 0[OF that] by auto java.lang.StringIndexOutOfBoundsException: Range [0, 97) out of bounds for lengt by (metis AOT_instance_of_cqt_2_exe_arg_def AOT_instance_of_cqt_2_intros_exe_arg_const java.lang.StringIndexOutOfBoundsException: Index 34 out of bounds for length 7 AOT_model_term_equiv_eps(1)) ultimately have ‹AOT_model_term_equiv «\ιz(Φ{z,κ})¬) subsetD[OF reachable_state_fragm if ‹AOT_model_denotes κ ∧ AOT_model_denotes κ' ∧ AOT_model_term_equiv κ κ'›small) using that by simp } thus ?thesis using 0 unfolding AOT_instance_of_cqt_2_exe_arg_def by simp AOT_instance_of_cqt_2_intros_exe_const[AOT_instance_of_cqt_2_intro]: assumes ‹ shows ‹AOT_instance_of_cqt_2 (λx :: 'b::AOT_κs. AOT_exe Π (κs x))› using assms unfolding AOT_instance_of_cqt_2_def AOT_sem_denotes AOT_model_lambda_denotes AOT_sem_disj AOT_sem_conj AOT_sem_not AOT_sem_box AOT_sem_act AOT_instance_of_cqt_2_exe_arg_def AOT_sem_equiv AOT_sem_imp AOT_sem_forall AOT_sem_exists AOT_sem_dia by (auto intro!: AOT_sem_exe_equiv) AOT_instance_of_cqt_2_intros_exe_lam[AOT_instance_of_cqt_2_intro]: assumes ‹Intuitively w we need to discharge a proofobligatio for either @{const and ‹AOT_instance_of_cqt_2_exe_arg κs› shows focus on @{const "Request"}s as we expect to have more local java.lang.StringIndexOutOfBoundsException: Range [40, 39) out of bounds for leng - { fix x y :: 'b assume ‹AOT_model_denotes x› moreover assume ‹AOT_model_denotes y› moreover assume ‹AOT_model_term_equiv x y› moreover have 1: ‹φ x = φ y› using assms calculation unfolding AOT_instance_of_cqt_2_def by blast ultimately have ‹location, 'proc, , 'qestion, 'state) programs AOT_exe (AOT_lambda (φ y)) (κs y)›Rightarrow> ('answe, 'ocation, 'questio, 'sate) unfolding 1 apply (safe intro!: AOT_sem_exe_equiv) by (metis AOT_instance_of_cqt_2_exe_arg_def assms(2)) } ?thesis unfolding AOT_instance_of_cqt_2_def AOT_instance_of_cqt_2_exe_arg_def blast AOT_instance_of_cqt_2_intro_prod[AOT_instance_of_cqt_2_intro]: assumes ‹∧ x . AOT_instance_of_cqt_2 (φ x)› and ‹∧ x . AOT_instance_of_cqt_2 (λ z . φ z x)› shows ‹AOT_instance_of_cqt_2 (λ(x,y) . φ x y)› using assms unfolding AOT_instance_of_cqt_2_def by (auto simp add: AOT_model_lambda_denotes AOT_sem_denotes AOT_model_denotes_prod_def AOT_model_term_equiv_prod_def) ‹ to @{attribute AOT_instance_of_cqt_2_intro}. They will be added with the next planned extension of axiom cqt:2.› AOT_instance_of_cqt_2_intro_next AOT_instance_of_cqt_2_enc_arg :: ‹('a::AOT_κs → 'b::AOT_κs) → bool› where ‹AOT_instance_of_cqt_2_enc_arg ≡ λ φ . ∀ x y z . AOT_model_denotes x ∧ AOT_model_denotes y ∧ AOT_model_term_equiv x y \<|" AOT_enc (φ x) z = AOT_enc (φ y) z› AOT_instance_of_cqt_2_enc_rel :: ‹('a::AOT_κs → <'b ‹ c1 aft AOT_model_denotes x ∧ AOT_model_denotes y ∧ AOT_mode ∪ FI, lcond (atC c1) (a AOT_enc z (φ x) = AOT_enc z (φ y) AOT_instance_of_cqt_2_intros_enc[AOT_instance_of_cqt_2_intro_next]: assumes ‹AOT_instance_of_cqt_2_enc_rel Π› and ‹AOT_instance_of_cqt_2_enc_arg κvcg_ shows ‹AOT_instance_of_cqt_2 (λx . AOT_enc (κs x) «[«Π x¬]¬)› using assms unfolding AOT_instance_of_cqt_2_def AOT_sem_denotes AOT_model_lambda_denotes AOT_instance_of_cqt_2_enc_rel_def AOT_sem_not AOT_sem_box AOT_sem_act AOT_sem_dia AOT_sem_conj AOT_sem_disj AOT_sem_equiv AOT_sem_imp AOT_sem_forall AOT_sem_exists AOT_instance_of_cqt_2_enc_arg_def fastforce+ AOT_instance_of_cqt_2_enc_arg_intro_const[AOT_instance_of_cqt_2_intro_next]: ‹AOT_instance_of_cqt_2_enc_arg (λx. c)› unfolding by simp AOT_instance_of_cqt_2_enc_arg_intro_desc[AOT_instance_of_cqt_2_intro_next]: assumes ‹ \openAOT_instance_of_cqt_2_enc_ar (\lambda> \kappa>:: 'b::AOT_🚫 - have 0: ‹∧b AOT_model_term_equiv κ Φ z κ = Φ z κ'› for z using assms java.lang.StringIndexOutOfBoundsException: Range [14, 13) out of bounds for leng AOT_sem_denotes AOT_model_lambda_denotes by force { fix κ κ' apapply (clarsimp simp: prerun_def state_prop_def) have ‹« met (ful) I ol.un.exha system_sta.urje) if ‹AOT_model_denotes κ using 0[OF that] by auto } thus ?thesis using 0 unfolding AOT_instance_of_cqt_2_enc_arg_def by meson AOT_instance_of_cqt_2_enc_rel_intro[AOT_instance_of_cqt_2_intro_next]: assumes ‹∧ κ . AOT_instance_of_cqt_2 (λκ' :: 'b::AOT_κs . φ κ κ')› assumes ‹∧ κ' . AOT_instance_of_cqt_2 (λκ :: 'a::AOT_κs . φ κ κ')› shows ‹AOT_instance_of_cqt_2_enc_rel (λκ :: 'a::AOT_κs. AOT_lambda (λκ'. φ κ κ'))› - { fix x y :: 'a and z ::'b assume ‹AOT_model_term_equiv x y› moreover assume ‹AOT_model_denotes x› moreover assume ‹AOT_model_denotes y› ultimately have ‹φ x = φ y› using assms unfolding AOT_instance_of_cqt_2_def by blast hence ‹AOT_enc z (AOT_lambda (φ x)) = AOT_enc z (AOT_lambda (φ y))› by simp } thus ?thesis unfolding AOT_instance_of_cqt_2_enc_rel_def by auto ‹Further restrict unary individual variables to type @{typ κ} (rather than class @{class AOT_κ} only) and define being ordinary and being abstract.› Individual: ‹κ› ‹_::AOT_κs› AOT_ordinary :: ‹Π› (‹O!›) ‹O! =df [λx ♢E!x]› AOT_ordinary[AOT del, AOT_defs del] AOT_abstract :: ‹Π› (‹A!›) ‹A! =df [λx ¬♢E!x]› AOT_abstract[AOT del, AOT_defs del] AOT_meta_syntax AOT_ordinary (‹O!›) notation AOT_abstract (\<open>\<^bold>A\<^bold>!\<close>) end context AOT_no_meta_syntax begin no_notation AOT_ordinary (\<open>\<^bold>O\<^bold>!\<close>) no_notation AOT_abstract (\<open>\<^bold>A\<^bold>!\<close>) end no_translations "_AOT_concrete" => "CONST AOT_term_of_var (CONST AOT_concrete)" parse_translation\<open> [(\<^syntax_const>\<open>_AOT_concrete\<close>, fn _ => fn [] => Const (\<^const_name>\<open>AOT_term_of_var\<close>, dummyT) $ Const (\<^const_name>\<open>AOT_concrete\<close>, \<^typ>\<open><\<kappa>> AOT_var\<close>))] \<close> text\<open>Auxiliary lemmata.\<close> lemma AOT_sem_ordinary: "\<guillemotleft>O!\<guillemotright> = \<guillemotleft>[\<lambda>x \<d using AOT_ordinary[THEN AOT_sem_id_def0E1] AOT_sem_ordinary_def_denotes by (auto simp: AOT_sem_eq) lemma AOT_sem_abstract: "\<guillemotleft>A!\<guillemotright> = \<guillemotleft>[\<lambda>x \<n using AOT_abstract[THEN AOT_sem_id_def0E1] AOT_sem_abstract_def_denotes by (auto simp: AOT_sem_eq) lemma AOT_sem_ordinary_denotes: \<open>[w \<Turnstile> O!\<down>]\<close> by (simp add: AOT_sem_ordinary AOT_sem_ordinary_def_denotes) lemma AOT_meta_abstract_denotes: \<open>[w \<Turnstile> A!\<down>]\<close> by (simp add: AOT_sem_abstract AOT_sem_abstract_def_denotes) lemma AOT_model_abstract_\<alpha>\<kappa>: \<open>\<exists> a . \<kappa> = \<alpha>\<kappa> a\<close> if \< using that[unfolded AOT_sem_abstract, simplified AOT_meta_abstract_denotes[unfolded AOT_sem_abstract, THEN AOT_sem_lambda_beta, OF that[simplified AOT_sem_exe, THEN conjunct2, THEN conjunct1]]] apply (simp add: AOT_sem_not AOT_sem_dia AOT_sem_concrete) by (metis AOT_model_\<omega>_concrete_in_some_world AOT_model_concrete_\<kappa>.simps(1 AOT_model_denotes_\<kappa>_def AOT_sem_denotes AOT_sem_exe \<kappa>.exhaust_disc is_\<alpha>\<kappa>_def is_\<omega>\<kappa>_def that) lemma AOT_model_ordinary_\<omega>\<kappa>: \<open>\<exists> a . \<kappa> = \<omega>\<kappa> a\<close> if \< using that[unfolded AOT_sem_ordinary, simplified AOT_sem_ordinary_denotes[unfolded AOT_sem_ordinary, THEN AOT_sem_lambda_beta, OF that[simplified AOT_sem_exe, THEN conjunct2, THEN conjunct1]]] apply (simp add: AOT_sem_dia AOT_sem_concrete) by (metis AOT_model_concrete_\<kappa>.simps(2) AOT_model_concrete_\<kappa>.simps(3) \<kappa>.exhaust_disc is_\<alpha>\<kappa>_def is_\<omega>\<kappa>_def is_null\<kappa>_def) lemma AOT_model_\<omega>\<kappa>_ordinary: \<open>[v \<Turnstile> O!\<guillemotleft>\<omega>\<kap by (metis AOT_model_abstract_\<alpha>\<kappa> AOT_model_denotes_\<kappa>_def AOT_sem_abstr AOT_sem_denotes AOT_sem_ind_eq AOT_sem_ordinary \<kappa>.disc(7) \<kappa>.distinct(1)) lemma AOT_model_\<alpha>\<kappa>_ordinary: \<open>[v \<Turnstile> A!\<guillemotleft>\<alpha>\<kap by (metis AOT_model_denotes_\<kappa>_def AOT_model_ordinary_\<omega>\<kappa> AOT_sem_abstr AOT_sem_denotes AOT_sem_ind_eq AOT_sem_ordinary \<kappa>.disc(8) \<kappa>.distinct(1)) AOT_theorem prod_denotesE: assumes \<open>\<guillemotleft>(\<kappa>\<^sub>1,\<kappa>\<^sub>2)\<g using assms by (simp add: AOT_sem_denotes AOT_sem_conj AOT_model_denotes_prod_def) declare prod_denotesE[AOT del] AOT_theorem prod_denotesI: assumes \<open>\<kappa>\<^sub>1\<down> & \<kappa>\<^sub>2\<down>\<cl using assms by (simp add: AOT_sem_denotes AOT_sem_conj AOT_model_denotes_prod_def) declare prod_denotesI[AOT del] text\<open>Prepare the derivation of the additional axioms that are validated by our extended models.\<close> locale AOT_ExtendedModel = assumes AOT_ExtendedModel: \<open>AOT_ExtendedModel\<close> begin lemma AOT_sem_indistinguishable_ord_enc_all: assumes \<Pi>_den: \<open>[v \<Turnstile> \<Pi>\<down>]\<close> assumes Ax: \<open>[v \<Turnstile> A!x]\<close> assumes Ay: \<open>[v \<Turnstile> A!y]\<close> assumes indist: \<open>[v \<Turnstile> \<forall>F \<box>([F]x \<equiv> [F]y)]\<close> shows \<open>[v \<Turnstile> \<forall>G(\<forall>z(O!z \<rightarrow> \<box>([G]z \<equiv> [\<Pi>]z)) \<rightar [v \<Turnstile> \<forall>G(\<forall>z(O!z \<rightarrow> \<box>([G]z \<equiv> [\<Pi>]z)) \<rightarrow> y[ proof - have 0: \<open>[v \<Turnstile> [\<lambda>x \<not>\<diamond>[E!]x]x]\<close> using Ax by (simp add: AOT_sem_abstract) have 1: \<open>[v \<Turnstile> [\<lambda>x \<not>\<diamond>[E!]x]y]\<close> using Ay by (simp add: AOT_sem_abstract) { assume \<open>[v \<Turnstile> \<forall>G(\<forall>z (O!z \<rightarrow> \<box>([G]z \<equiv> [\<Pi>]z)) \<r hence 3: \<open>[v \<Turnstile> \<forall>G(\<forall>z([\<lambda>x \<diamond>[E!]x]z \<rightarrow> \<bo by (simp add: AOT_sem_ordinary) { fix \<Pi>' :: \<open><\<kappa>>\<close> assume 1: \<open>[v \<Turnstile> \<Pi>'\<down>]\<close> assume 2: \<open>[v \<Turnstile> [\<lambda>x \<diamond>[E!]x]z \<rightarrow> \<box>([\<Pi>']z \<equiv> [\< have \<open>[v \<Turnstile> x[\<Pi>']]\<close> using 3 by (auto simp: AOT_sem_forall AOT_sem_imp AOT_sem_box AOT_sem_denotes) (metis (no_types, lifting) 1 2 AOT_term_of_var_cases AOT_sem_box AOT_sem_denotes AOT_sem_imp) } note 3 = this fix \<Pi>' :: \<open><\<kappa>>\<close> assume \<Pi>_den: \<open>[v \<Turnstile> \<Pi>'\<down>]\<close> assume 4: \<open>[v \<Turnstile> \<forall>z (O!z \<rightarrow> \<box>([\<Pi>']z \<equiv> [\<Pi>]z))]\<clos { fix \<kappa>\<^sub>0 assume \<open>[v \<Turnstile> [\<lambda>x \<diamond>[E!]x]\<kappa>\<^sub>0]\<close> hence \<open>[v \<Turnstile> O!\<kappa>\<^sub>0]\<close> using AOT_sem_ordinary by metis moreover have \<open>[v \<Turnstile> \<kappa>\<^sub>0\<down>]\<close> using calculation by (simp add: AOT_sem_exe) ultimately have \<open>[v \<Turnstile> \<box>([\<Pi>']\<kappa>\<^sub>0 \<equiv> [\<Pi>]\<kappa>\<^sub>0)]\< using 4 by (auto simp: AOT_sem_forall AOT_sem_imp) } note 4 = this { fix \<Pi>'' :: \<open><\<kappa>>\<close> assume \<open>[v \<Turnstile> \<Pi>''\<down>]\<close> moreover assume \<open>[w \<Turnstile> [\<Pi>'']\<kappa>\<^sub>0] = [w \<Turnstile> [\<Pi>']\<kappa>\<^su ultimately have 5: \<open>[v \<Turnstile> x[\<Pi>'']]\<close> using 4 3 by (auto simp: AOT_sem_imp AOT_sem_equiv AOT_sem_box) } note 5 = this have \<open>[v \<Turnstile> y[\<Pi>']]\<close> apply (rule AOT_sem_enc_indistinguishable_all[OF AOT_ExtendedModel]) apply (fact 0) by (auto simp: 5 0 1 \<Pi>_den indist[simplified AOT_sem_forall AOT_sem_box AOT_sem_equiv]) } moreover { { assume \<open>[v \<Turnstile> \<forall>G(\<forall>z (O!z \<rightarrow> \<box>([G]z \<equiv> [\<Pi>]z)) \<r hence 3: \<open>[v \<Turnstile> \<forall>G(\<forall>z ([\<lambda>x \<diamond>[E!]x]z \<rightarrow> \<bo by (simp add: AOT_sem_ordinary) { fix \<Pi>' :: \<open><\<kappa>>\<close> assume 1: \<open>[v \<Turnstile> \<Pi>'\<down>]\<close> assume 2: \<open>[v \<Turnstile> [\<lambda>x \<diamond>[E!]x]z \<rightarrow> \<box>([\<Pi>']z \<equiv> [\< have \<open>[v \<Turnstile> y[\<Pi>']]\<close> using 3 apply (simp add: AOT_sem_forall AOT_sem_imp AOT_sem_box AOT_sem_denotes) by (metis (no_types, lifting) 1 2 AOT_model.AOT_term_of_var_cases AOT_sem_box AOT_sem_denotes AOT_sem_imp) } note 3 = this fix \<Pi>' :: \<open><\<kappa>>\<close> assume \<Pi>_den: \<open>[v \<Turnstile> \<Pi>'\<down>]\<close> assume 4: \<open>[v \<Turnstile> \<forall>z (O!z \<rightarrow> \<box>([\<Pi>']z \<equiv> [\<Pi>]z))]\<clos { fix \<kappa>\<^sub>0 assume \<open>[v \<Turnstile> [\<lambda>x \<diamond>[E!]x]\<kappa>\<^sub>0]\<close> hence \<open>[v \<Turnstile> O!\<kappa>\<^sub>0]\<close> using AOT_sem_ordinary by metis moreover have \<open>[v \<Turnstile> \<kappa>\<^sub>0\<down>]\<close> using calculation by (simp add: AOT_sem_exe) ultimately have \<open>[v \<Turnstile> \<box>([\<Pi>']\<kappa>\<^sub>0 \<equiv> [\<Pi>]\<kappa>\<^sub>0)]\< using 4 by (auto simp: AOT_sem_forall AOT_sem_imp) } note 4 = this { fix \<Pi>'' :: \<open><\<kappa>>\<close> assume \<open>[v \<Turnstile> \<Pi>''\<down>]\<close> moreover assume \<open>[w \<Turnstile> [\<Pi>'']\<kappa>\<^sub>0] = [w \<Turnstile> [\<Pi>']\<kappa>\<^su ultimately have \<open>[v \<Turnstile> y[\<Pi>'']]\<close> using 3 4 by (auto simp: AOT_sem_imp AOT_sem_equiv AOT_sem_box) } note 5 = this have \<open>[v \<Turnstile> x[\<Pi>']]\<close> apply (rule AOT_sem_enc_indistinguishable_all[OF AOT_ExtendedModel]) apply (fact 1) by (auto simp: 5 0 1 \<Pi>_den indist[simplified AOT_sem_forall AOT_sem_box AOT_sem_equiv]) } } ultimately show \<open>[v \<Turnstile> \<forall>G (\<forall>z (O!z \<rightarrow> \<box>([G]z \<equiv> [\< [v \<Turnstile> \<forall>G (\<forall>z (O!z \<rightarrow> \<box>([G]z \<equiv> [\<Pi>]z)) \<rightarrow> y[ by (auto simp: AOT_sem_forall AOT_sem_imp) qed lemma AOT_sem_indistinguishable_ord_enc_ex: assumes \<Pi>_den: \<open>[v \<Turnstile> \<Pi>\<down>]\<close> assumes Ax: \<open>[v \<Turnstile> A!x]\<close> assumes Ay: \<open>[v \<Turnstile> A!y]\<close> assumes indist: \<open>[v \<Turnstile> \<forall>F \<box>([F]x \<equiv> [F]y)]\<close> shows \<open>[v \<Turnstile> \<exists>G(\<forall>z (O!z \<rightarrow> \<box>([G]z \<equiv> [\<Pi>]z)) &an> x[G])] = [v \<Turnstile> \<exists>G(\<forall>z(O!z \<rightarrow> \<box>([G]z \<equiv> [\<Pi>]z)) & y[G])]\< proof - have Aux: \<open>[v \<Turnstile> [\<lambda>x \<diamond>[E!]x]\<kappa>] = ([v \<Turnstile> [\<lambda>x \<d using AOT_sem_exe by blast AOT_modally_strict { fix x y AOT_assume \<Pi>_den: \<open>[\<Pi>]\<down>\<close> AOT_assume 2: \<open>\<forall>F \<box>([F]x \<equiv> [F]y)\<close> AOT_assume \<open>A!x\<close> AOT_hence 0: \<open>[\<lambda>x \<not>\<diamond>[E!]x]x\<close> by (simp add: AOT_sem_abstract) AOT_assume \<open>A!y\<close> AOT_hence 1: \<open>[\<lambda>x \<not>\<diamond>[E!]x]y\<close> by (simp add: AOT_sem_abstract) { AOT_assume \<open>\<exists>G(\<forall>z (O!z \<rightarrow> \<box>([G]z \<equiv> [\<Pi>]z)) & x[G] then AOT_obtain \<Pi>' where \<Pi>'_den: \<open>\<Pi>'\<down>\<close> and \<Pi>'_indist: \<open>\<forall>z (O!z \<rightarrow> \<box>([\<Pi>']z \<equiv> [\<Pi>]z))\<close> and x_enc_\<Pi>': \<open>x[\<Pi>']\<close> by (meson AOT_sem_conj AOT_sem_exists) { fix \<kappa>\<^sub>0 AOT_assume \<open>[\<lambda>x \<diamond>[E!]x]\<kappa>\<^sub>0\<close> AOT_hence \<open>\<box>([\<Pi>']\<kappa>\<^sub>0 \<equiv> [\<Pi>]\<kappa>\<^sub>0)\<close> using \<Pi>'_indist by (auto simp: AOT_sem_exe AOT_sem_imp AOT_sem_exists AOT_sem_conj AOT_sem_ordinary AOT_sem_forall) } note 3 = this AOT_have \<open>\<forall>z ([\<lambda>x \<diamond>[E!]x]z \<rightarrow> \<box>([\<Pi>']z \<equiv> [\<Pi>] using \<Pi>'_indist by (simp add: AOT_sem_ordinary) AOT_obtain \<Pi>'' where \<Pi>''_den: \<open>\<Pi>''\<down>\<close> and \<Pi>''_indist: \<open>[\<lambda>x \<diamond>[E!]x]\<kappa>\<^sub>0 \<rightarrow> \<box>([\<Pi>'']\<kap y_enc_\<Pi>'': \<open>y[\<Pi>'']\<close> for \<kappa>\<^sub>0 using AOT_sem_enc_indistinguishable_ex[OF AOT_ExtendedModel, OF 0, OF 1, rotated, OF \<Pi>_den, OF exI[where x=\<Pi>'], OF conjI, OF \<Pi>'_den, OF conjI, OF x_enc_\<Pi>', OF allI, OF impI, OF 3[simplified AOT_sem_box AOT_sem_equiv], simplified, OF 2[simplified AOT_sem_forall AOT_sem_equiv AOT_sem_box, THEN spec, THEN mp, THEN spec], simplified] unfolding AOT_sem_imp AOT_sem_box AOT_sem_equiv by blast { AOT_have \<open>\<Pi>''\<down>\<close> and \<open>\<forall>x ([\<lambda>x \<diamond>[E!]x]x \<rightarrow> \<box>([\<Pi>'']x \<equiv> [\<Pi>]x))\< and \<open>y[\<Pi>'']\<close> apply (simp add: \<Pi>''_den) apply (simp add: AOT_sem_forall \<Pi>''_indist) by (simp add: y_enc_\<Pi>'') } note 2 = this AOT_have \<open>\<exists>G(\<forall>z (O!z \<rightarrow> \<box>([G]z \<equiv> [\<Pi>]z)) & y[G])\< apply (simp add: AOT_sem_exists AOT_sem_ordinary AOT_sem_imp AOT_sem_box AOT_sem_forall AOT_sem_equiv AOT_sem_conj) using 2[simplified AOT_sem_box AOT_sem_equiv AOT_sem_imp AOT_sem_forall] by blast } } note 0 = this AOT_modally_strict { { fix x y AOT_assume \<Pi>_den: \<open>[\<Pi>]\<down>\<close> moreover AOT_assume \<open>\<forall>F \<box>([F]x \<equiv> [F]y)\<close> moreover AOT_have \<open>\<forall>F \<box>([F]y \<equiv> [F]x)\<close> using calculation(2) by (auto simp: AOT_sem_forall AOT_sem_box AOT_sem_equiv) moreover AOT_assume \<open>A!x\<close> moreover AOT_assume \<open>A!y\<close> ultimately AOT_have \<open>\<exists>G (\<forall>z (O!z \<rightarrow> \<box>([G]z \<equiv> [\<Pi>]z)) &pan> x[G]) \<equiv> \<exists>G (\<forall>z (O!z \<rightarrow> \<box>([G]z \<equiv> [\<Pi>]z)) & y[G])\<close> using 0 by (auto simp: AOT_sem_equiv) } have 1: \<open>[v \<Turnstile> \<forall>F \<box>([F]y \<equiv> [F]x)]\<close> using indist by (auto simp: AOT_sem_forall AOT_sem_box AOT_sem_equiv) thus \<open>[v \<Turnstile> \<exists>G (\<forall>z (O!z \<rightarrow> \<box>([G]z \<equiv> [\<Pi>]z)) &n> x[G])] = [v \<Turnstile> \<exists>G (\<forall>z (O!z \<rightarrow> \<box>([G]z \<equiv> [\<Pi>]z)) & y[G])]\< using assms by (auto simp: AOT_sem_imp AOT_sem_conj AOT_sem_equiv 0) } qed end (* Collect all theorems that are not in Main and not declared [AOT] and store them in a blacklist. *) setup\<open>setup_AOT_no_atp\<close> bundle AOT_no_atp begin declare AOT_no_atp[no_atp] end (* Can be used as: "including AOT_no_atp sledgehammer" or "sledgehammer(del: AOT_no_atp) *) (*<*) end (*>*)
¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.117Bemerkung: (vorverarbeitet am 2026-11-04) ¤*Bot Zugriff |
|
||||||||||||||||||||||||
2026-11-01