Theory AOT_Definitions
1theory AOT_Definitions
2 imports AOT_semantics
3begin
4
5section‹Definitions of AOT›
6
7AOT_theorem "conventions:1": ‹φ & ψ ≡⇩d⇩f ¬(φ → ¬ψ)›
8 using AOT_conj.
9AOT_theorem "conventions:2": ‹φ ∨ ψ ≡⇩d⇩f ¬φ → ψ›
10 using AOT_disj.
11AOT_theorem "conventions:3": ‹φ ≡ ψ ≡⇩d⇩f (φ → ψ) & (ψ → φ)›
12 using AOT_equiv.
13AOT_theorem "conventions:4": ‹∃α φ{α} ≡⇩d⇩f ¬∀α ¬φ{α}›
14 using AOT_exists.
15AOT_theorem "conventions:5": ‹◇φ ≡⇩d⇩f ¬□¬φ›
16 using AOT_dia.
17
18declare "conventions:1"[AOT_defs] "conventions:2"[AOT_defs]
19 "conventions:3"[AOT_defs] "conventions:4"[AOT_defs]
20 "conventions:5"[AOT_defs]
21
22notepad
23begin
24 fix φ ψ χ
25 text‹\linelabel{precedence}›
26 have "conventions3[1]": ‹«φ → ψ ≡ ¬ψ → ¬φ» = «(φ → ψ) ≡ (¬ψ → ¬φ)»›
27 by blast
28 have "conventions3[2]": ‹«φ & ψ → χ» = «(φ & ψ) → χ»›
29 and ‹«φ ∨ ψ → χ» = «(φ ∨ ψ) → χ»›
30 by blast+
31 have "conventions3[3]": ‹«φ ∨ ψ & χ» = «(φ ∨ ψ) & χ»›
32 and ‹«φ & ψ ∨ χ» = «(φ & ψ) ∨ χ»›
33 by blast+
34end
35
36
37AOT_theorem "existence:1": ‹κ↓ ≡⇩d⇩f ∃F [F]κ›
38 by (simp add: AOT_sem_denotes AOT_sem_exists AOT_model_equiv_def)
39 (metis AOT_sem_denotes AOT_sem_exe AOT_sem_lambda_beta AOT_sem_lambda_denotes)
40AOT_theorem "existence:2": ‹Π↓ ≡⇩d⇩f ∃x⇩1...∃x⇩n x⇩1...x⇩n[Π]›
41 using AOT_sem_denotes AOT_sem_enc_denotes AOT_sem_universal_encoder
42 by (simp add: AOT_sem_denotes AOT_sem_exists AOT_model_equiv_def) blast
43AOT_theorem "existence:2[1]": ‹Π↓ ≡⇩d⇩f ∃x x[Π]›
44 using "existence:2"[of Π] by simp
45AOT_theorem "existence:2[2]": ‹Π↓ ≡⇩d⇩f ∃x∃y xy[Π]›
46 using "existence:2"[of Π]
47 by (simp add: AOT_sem_denotes AOT_sem_exists AOT_model_equiv_def
48 AOT_model_denotes_prod_def)
49AOT_theorem "existence:2[3]": ‹Π↓ ≡⇩d⇩f ∃x∃y∃z xyz[Π]›
50 using "existence:2"[of Π]
51 by (simp add: AOT_sem_denotes AOT_sem_exists AOT_model_equiv_def
52 AOT_model_denotes_prod_def)
53AOT_theorem "existence:2[4]": ‹Π↓ ≡⇩d⇩f ∃x⇩1∃x⇩2∃x⇩3∃x⇩4 x⇩1x⇩2x⇩3x⇩4[Π]›
54 using "existence:2"[of Π]
55 by (simp add: AOT_sem_denotes AOT_sem_exists AOT_model_equiv_def
56 AOT_model_denotes_prod_def)
57
58AOT_theorem "existence:3": ‹φ↓ ≡⇩d⇩f [λx φ]↓›
59 by (simp add: AOT_sem_denotes AOT_model_denotes_𝗈_def AOT_model_equiv_def
60 AOT_model_lambda_denotes)
61
62declare "existence:1"[AOT_defs] "existence:2"[AOT_defs] "existence:2[1]"[AOT_defs]
63 "existence:2[2]"[AOT_defs] "existence:2[3]"[AOT_defs]
64 "existence:2[4]"[AOT_defs] "existence:3"[AOT_defs]
65
66
67AOT_theorem "oa:1": ‹O! =⇩d⇩f [λx ◇E!x]› using AOT_ordinary .
68AOT_theorem "oa:2": ‹A! =⇩d⇩f [λx ¬◇E!x]› using AOT_abstract .
69
70declare "oa:1"[AOT_defs] "oa:2"[AOT_defs]
71
72AOT_theorem "identity:1":
73 ‹x = y ≡⇩d⇩f ([O!]x & [O!]y & □∀F ([F]x ≡ [F]y)) ∨
74 ([A!]x & [A!]y & □∀F (x[F] ≡ y[F]))›
75 unfolding AOT_model_equiv_def
76 using AOT_sem_ind_eq[of _ x y]
77 by (simp add: AOT_sem_ordinary AOT_sem_abstract AOT_sem_conj
78 AOT_sem_box AOT_sem_equiv AOT_sem_forall AOT_sem_disj AOT_sem_eq
79 AOT_sem_denotes)
80
81AOT_theorem "identity:2":
82 ‹F = G ≡⇩d⇩f F↓ & G↓ & □∀x(x[F] ≡ x[G])›
83 using AOT_sem_enc_eq[of _ F G]
84 by (auto simp: AOT_model_equiv_def AOT_sem_imp AOT_sem_denotes AOT_sem_eq
85 AOT_sem_conj AOT_sem_forall AOT_sem_box AOT_sem_equiv)
86
87AOT_theorem "identity:3[2]":
88 ‹F = G ≡⇩d⇩f F↓ & G↓ & ∀y([λz [F]zy] = [λz [G]zy] & [λz [F]yz] = [λz [G]yz])›
89 by (auto simp: AOT_model_equiv_def AOT_sem_proj_id_prop[of _ F G]
90 AOT_sem_proj_id_prod_def AOT_sem_conj AOT_sem_denotes
91 AOT_sem_forall AOT_sem_unary_proj_id AOT_model_denotes_prod_def)
92AOT_theorem "identity:3[3]":
93 ‹F = G ≡⇩d⇩f F↓ & G↓ & ∀y⇩1∀y⇩2([λz [F]zy⇩1y⇩2] = [λz [G]zy⇩1y⇩2] &
94 [λz [F]y⇩1zy⇩2] = [λz [G]y⇩1zy⇩2] &
95 [λz [F]y⇩1y⇩2z] = [λz [G]y⇩1y⇩2z])›
96 by (auto simp: AOT_model_equiv_def AOT_sem_proj_id_prop[of _ F G]
97 AOT_sem_proj_id_prod_def AOT_sem_conj AOT_sem_denotes
98 AOT_sem_forall AOT_sem_unary_proj_id AOT_model_denotes_prod_def)
99AOT_theorem "identity:3[4]":
100 ‹F = G ≡⇩d⇩f F↓ & G↓ & ∀y⇩1∀y⇩2∀y⇩3([λz [F]zy⇩1y⇩2y⇩3] = [λz [G]zy⇩1y⇩2y⇩3] &
101 [λz [F]y⇩1zy⇩2y⇩3] = [λz [G]y⇩1zy⇩2y⇩3] &
102 [λz [F]y⇩1y⇩2zy⇩3] = [λz [G]y⇩1y⇩2zy⇩3] &
103 [λz [F]y⇩1y⇩2y⇩3z] = [λz [G]y⇩1y⇩2y⇩3z])›
104 by (auto simp: AOT_model_equiv_def AOT_sem_proj_id_prop[of _ F G]
105 AOT_sem_proj_id_prod_def AOT_sem_conj AOT_sem_denotes
106 AOT_sem_forall AOT_sem_unary_proj_id AOT_model_denotes_prod_def)
107AOT_theorem "identity:3":
108 ‹F = G ≡⇩d⇩f F↓ & G↓ & ∀x⇩1...∀x⇩n «AOT_sem_proj_id x⇩1x⇩n (λ τ . AOT_exe F τ)
109 (λ τ . AOT_exe G τ)»›
110 by (auto simp: AOT_model_equiv_def AOT_sem_proj_id_prop[of _ F G]
111 AOT_sem_proj_id_prod_def AOT_sem_conj AOT_sem_denotes
112 AOT_sem_forall AOT_sem_unary_proj_id AOT_model_denotes_prod_def)
113
114AOT_theorem "identity:4":
115 ‹p = q ≡⇩d⇩f p↓ & q↓ & [λx p] = [λx q]›
116 by (auto simp: AOT_model_equiv_def AOT_sem_eq AOT_sem_denotes AOT_sem_conj
117 AOT_model_lambda_denotes AOT_sem_lambda_eq_prop_eq)
118
119declare "identity:1"[AOT_defs] "identity:2"[AOT_defs] "identity:3[2]"[AOT_defs]
120 "identity:3[3]"[AOT_defs] "identity:3[4]"[AOT_defs] "identity:3"[AOT_defs]
121 "identity:4"[AOT_defs]
122
123AOT_define AOT_nonidentical :: ‹τ ⇒ τ ⇒ φ› (infixl "≠" 50)
124 "=-infix": ‹τ ≠ σ ≡⇩d⇩f ¬(τ = σ)›
125
126context AOT_meta_syntax
127begin
128notation AOT_nonidentical (infixl "❙≠" 50)
129end
130context AOT_no_meta_syntax
131begin
132no_notation AOT_nonidentical (infixl "❙≠" 50)
133end
134
135
136text‹The following are purely technical pseudo-definitions required due to
137 our internal implementation of n-ary relations and ellipses using tuples.›
138AOT_theorem tuple_denotes: ‹«(τ,τ')»↓ ≡⇩d⇩f τ↓ & τ'↓›
139 by (simp add: AOT_model_denotes_prod_def AOT_model_equiv_def
140 AOT_sem_conj AOT_sem_denotes)
141AOT_theorem tuple_identity_1: ‹«(τ,τ')» = «(σ, σ')» ≡⇩d⇩f (τ = σ) & (τ' = σ')›
142 by (auto simp: AOT_model_equiv_def AOT_sem_conj AOT_sem_eq
143 AOT_model_denotes_prod_def AOT_sem_denotes)
144AOT_theorem tuple_forall: ‹∀α⇩1...∀α⇩n φ{α⇩1...α⇩n} ≡⇩d⇩f ∀α⇩1(∀α⇩2...∀α⇩n φ{«(α⇩1, α⇩2α⇩n)»})›
145 by (auto simp: AOT_model_equiv_def AOT_sem_forall AOT_sem_denotes
146 AOT_model_denotes_prod_def)
147AOT_theorem tuple_exists: ‹∃α⇩1...∃α⇩n φ{α⇩1...α⇩n} ≡⇩d⇩f ∃α⇩1(∃α⇩2...∃α⇩n φ{«(α⇩1, α⇩2α⇩n)»})›
148 by (auto simp: AOT_model_equiv_def AOT_sem_exists AOT_sem_denotes
149 AOT_model_denotes_prod_def)
150declare tuple_denotes[AOT_defs] tuple_identity_1[AOT_defs] tuple_forall[AOT_defs]
151 tuple_exists[AOT_defs]
152
153end
154