Theory AOT_Definitions

1theory AOT_Definitions
2  imports AOT_semantics
3begin
4
5section‹Definitions of AOT›
6
7AOT_theorem "conventions:1": φ & ψ df ¬(φ  ¬ψ)
8  using AOT_conj.
9AOT_theorem "conventions:2": φ  ψ df ¬φ  ψ
10  using AOT_disj.
11AOT_theorem "conventions:3": φ  ψ df (φ  ψ) & (ψ  φ)
12  using AOT_equiv.
13AOT_theorem "conventions:4": α φ{α} df ¬α ¬φ{α}
14  using AOT_exists.
15AOT_theorem "conventions:5": φ df ¬¬φ
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+ ― ‹Note that PLM instead generally uses parenthesis in these cases.›
34end
35
36
37AOT_theorem "existence:1": κ df 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": Π df x1...∃xn x1...xn[Π]
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]": Π df x x[Π]
44  using "existence:2"[of Π] by simp
45AOT_theorem "existence:2[2]": Π df xy 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]": Π df xyz 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]": Π df x1x2x3x4 x1x2x3x4[Π]
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": φ df 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! =df x E!x] using AOT_ordinary .
68AOT_theorem "oa:2": A! =df x ¬E!x] using AOT_abstract .
69
70declare "oa:1"[AOT_defs] "oa:2"[AOT_defs]
71
72AOT_theorem "identity:1":
73  x = y df ([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 df 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 df 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 df F & G & y1y2(z [F]zy1y2] = z [G]zy1y2] &
94                              z [F]y1zy2] = z [G]y1zy2] &
95                              z [F]y1y2z] = z [G]y1y2z])
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 df F & G & y1y2y3(z [F]zy1y2y3] = z [G]zy1y2y3] &
101                                z [F]y1zy2y3] = z [G]y1zy2y3] &
102                                z [F]y1y2zy3] = z [G]y1y2zy3] &
103                                z [F]y1y2y3z] = z [G]y1y2y3z])
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 df F & G & x1...∀xn «AOT_sem_proj_id x1xn (λ τ . 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 df 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": τ  σ df ¬(τ = σ)
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: «(τ,τ')» df τ & τ'
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: «(τ,τ')» = «(σ, σ')» df (τ = σ) & (τ' = σ')
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} df α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} df α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