1(* ------------------------------------------------------------------------- *)
2(* Involution: Basic                                                         *)
3(* ------------------------------------------------------------------------- *)
4
5(*===========================================================================*)
6
7(* add all dependent libraries for script *)
8open HolKernel boolLib bossLib Parse;
9
10(* declare new theory at start *)
11val _ = new_theory "involute";
12
13(* ------------------------------------------------------------------------- *)
14
15
16(* open dependent theories *)
17(* arithmeticTheory -- load by default *)
18
19(* val _ = load "helperTheory"; *)
20open helperNumTheory;
21open helperSetTheory;
22open helperFunctionTheory;
23open helperTheory; (* for FUNPOW_closure *)
24
25(* arithmeticTheory -- load by default *)
26open arithmeticTheory pred_setTheory;
27
28
29(* ------------------------------------------------------------------------- *)
30(* Involution: Basic Documentation                                           *)
31(* ------------------------------------------------------------------------- *)
32(* Overloading:
33   f endo s            = !x. x IN s ==> f x IN s
34   f involute s        = !x. x IN s ==> f x IN s /\ (f (f x) = x)
35*)
36(*
37
38   Helper Theorem:
39
40   Involution:
41   involute_endo         |- !f s. f involute s ==> f endo s
42   involute_inj          |- !f s. f involute s ==> INJ f s s
43   involute_surj         |- !f s. f involute s ==> SURJ f s s
44   involute_bij          |- !f s. f involute s ==> f PERMUTES s
45   involute_permutes     |- !f s. f involute X ==> f PERMUTES s
46   involute_LINV         |- !f s. f involute s ==> LINV f s involute s
47   involute_FUNPOW       |- !f s x n. f involute s /\ x IN s ==>
48                                      FUNPOW f n x = if EVEN n then x else f x
49   involute_FUNPOW_LINV  |- !f s x n. f involute s /\ x IN s ==>
50                                      FUNPOW (LINV f s) n x = FUNPOW f n x
51   involute_alt          |- !f s. f involute s <=>
52                                  f endo s /\ !x. x IN s ==> FUNPOW f 2 x = x
53
54*)
55
56(* ------------------------------------------------------------------------- *)
57(* Helper Theorem                                                            *)
58(* ------------------------------------------------------------------------- *)
59
60(* ------------------------------------------------------------------------- *)
61(* Involution                                                                *)
62(* ------------------------------------------------------------------------- *)
63
64(* Overload on involution *)
65(*
66val _ = overload_on("involute", ``\f. f o f = I``);
67val _ = clear_overloads_on "involute";
68*)
69
70(* An endofunction has its domain equal to its co-domain. *)
71val _ = overload_on("endo", ``\f s. !x. x IN s ==> f x IN s``);
72val _ = set_fixity "endo" (Infix(NONASSOC, 450)); (* same as relation *)
73
74val _ = overload_on("involute", ``\f s. !x. x IN s ==> f x IN s /\ (f (f x) = x)``);
75val _ = set_fixity "involute" (Infix(NONASSOC, 450)); (* same as relation *)
76
77(* Theorem: f involute s ==> f endo s *)
78(* Proof: by notation *)
79Theorem involute_endo:
80  !f s. f involute s ==> f endo s
81Proof
82  simp[]
83QED
84
85(* Theorem: f involute s ==> INJ f s s *)
86(* Proof:
87   By INJ_DEF, this is to show:
88   (1) !x. x IN s ==> f x IN s, true by f involute s.
89   (2) !x y. x IN s /\ y IN s ==> f x = f y ==> x = y
90               f x = f y
91       ==> f (f x) = f (f y)         by f x IN s, f y IN s
92       ==>       x = y               by f involute s
93*)
94Theorem involute_inj:
95  !f s. f involute s ==> INJ f s s
96Proof
97  metis_tac[INJ_DEF]
98QED
99
100(* Theorem: f involute s ==> SURJ f s s *)
101(* Proof:
102   By SURJ_DEF, this is to show:
103   (1) !x. x IN s ==> f x IN s, true     by f involute s.
104   (2) !x. x IN s ==> ?y. y IN s /\ f y = x
105       Let y = f x, then y IN s          by f involute s
106       and f y = f (f x) = x             by f involute s
107*)
108Theorem involute_surj:
109  !f s. f involute s ==> SURJ f s s
110Proof
111  prove_tac[SURJ_DEF]
112QED
113
114(* Theorem: f involute s ==> f PERMUTES s *)
115(* Proof: by BIJ_DEF, involute_inj, involute_surj *)
116Theorem involute_bij:
117  !f s. f involute s ==> f PERMUTES s
118Proof
119  rw[BIJ_DEF, involute_inj, involute_surj]
120QED
121
122(* Theorem alias *)
123val involute_permutes = save_thm("involute_permutes", involute_bij);
124(* val involute_permutes = |- !f s. f involute s ==> f PERMUTES s: thm *)
125
126(* Theorem: f involute s ==> (LINV f s) involute s *)
127(* Proof:
128       f involute s
129   ==> f PERMUTES s                        by involute_bij
130   ==> (LINV f s) PERMUTES s               by BIJ_LINV_BIJ
131   Thus x IN s ==> LINV f s x IN s         by BIJ_ELEMENT
132   Since f (f x) = x                       by involution
133      so     f x = LINV f s x              by BIJ_LINV_THM
134      or       x = LINV f s (LINV f s x)   by BIJ_LINV_THM
135*)
136Theorem involute_LINV:
137  !f s. f involute s ==> (LINV f s) involute s
138Proof
139  ntac 3 strip_tac >>
140  `f PERMUTES s /\ (LINV f s) PERMUTES s` by rw[involute_bij, BIJ_LINV_BIJ] >>
141  rpt strip_tac >-
142  metis_tac[BIJ_ELEMENT] >>
143  metis_tac[BIJ_LINV_THM]
144QED
145
146(* Theorem: f involute s /\ x IN s ==>
147            FUNPOW f n x = if EVEN n then x else f x *)
148(* Proof:
149   Note FUNPOW f 2 x
150      = f (f x)                    by FUNPOW_2
151      = x                          by involution
152    ==> FUNPOW f (2 * k) x = x     by FUNPOW_MULTIPLE
153
154   If EVEN n, then n = 2 * k       by EVEN_EXISTS
155      Thus FUNPOW f (2 * k) x = x  by above
156   If ~EVEN n, then ODD n.         by EVEN_ODD
157      Thus n = SUC (2 * k)         by ODD_EXISTS
158        FUNPOW f n x
159      = FUNPOW f (SUC (2 * k)) x   by above
160      = f (FUNPOW f (2 * k) x)     by FUNPOW_SUC
161      = f x                        by above
162*)
163Theorem involute_FUNPOW:
164  !f s x n. f involute s /\ x IN s ==>
165            FUNPOW f n x = if EVEN n then x else f x
166Proof
167  rpt strip_tac >>
168  `FUNPOW f 2 x = x` by rw[FUNPOW_2] >>
169  (imp_res_tac FUNPOW_MULTIPLE >> fs[]) >>
170  (Cases_on `EVEN n` >> simp[]) >-
171  metis_tac[EVEN_EXISTS] >>
172  metis_tac[EVEN_ODD, ODD_EXISTS, FUNPOW_SUC]
173QED
174
175(* Theorem: f involute s /\ x IN s ==>
176            FUNPOW (LINV f s) n x = FUNPOW f n x *)
177(* Proof:
178   By induction on n.
179   Base: FUNPOW (LINV f s) 0 x = FUNPOW f 0 x, true by FUNPOW_0
180   Step: FUNPOW (LINV f s) n x = FUNPOW f n x ==>
181         FUNPOW (LINV f s) (SUC n) x = FUNPOW f (SUC n) x
182         Note f PERMUTES s                           by involute_bij
183          and FUNPOW f n x IN s                      by FUNPOW_closure
184         also FUNPOW f (SUC n) x IN s                by FUNPOW_closure
185           FUNPOW (LINV f s) (SUC n) x
186         = LINV f s (FUNPOW (LINV f s) n x)          by FUNPOW_SUC
187         = LINV f s (FUNPOW f n x)                   by induction hypothesis
188         = LINV f s (LINV f s (f (FUNPOW f n x)))    by BIJ_LINV_THM,
189         = LINV f s (LINV f s (FUNPOW f (SUC n) x))  by FUNPOW_SUC
190         = FUNPOW f (SUC n) x                        by involute_LINV
191*)
192Theorem involute_FUNPOW_LINV:
193  !f s x n. f involute s /\ x IN s ==>
194            FUNPOW (LINV f s) n x = FUNPOW f n x
195Proof
196  rpt strip_tac >>
197  Induct_on `n` >-
198  rw[] >>
199  `f PERMUTES s` by rw[involute_bij] >>
200  `FUNPOW f n x IN s /\ FUNPOW f (SUC n) x IN s` by rw[FUNPOW_closure] >>
201  `FUNPOW (LINV f s) (SUC n) x = LINV f s (FUNPOW (LINV f s) n x)` by rw[FUNPOW_SUC] >>
202  `_ = LINV f s (FUNPOW f n x)` by rw[] >>
203  `_ = LINV f s (LINV f s (f (FUNPOW f n x)))` by metis_tac[BIJ_LINV_THM] >>
204  `_ = LINV f s (LINV f s (FUNPOW f (SUC n) x))` by rw[FUNPOW_SUC] >>
205  `_ = FUNPOW f (SUC n) x` by metis_tac[involute_LINV] >>
206  simp[]
207QED
208
209(* Theorem: f involute s <=> f endo s /\ !x. x IN s ==> FUNPOW f 2 x = x *)
210(* Proof:
211       f involute s
212   <=> !x. x IN s ==> f x IN s /\ f (f x) = x        by notation
213   <=> !x. x IN s ==> f x IN s /\ FUNPOW 2 x = x     by FUNPOW_2
214   <=> !x. x IN s ==> f x IN s /\ !x. x IN s ==> FUNPOW 2 x = x
215   <=> f endo s /\  !x. x IN s ==> FUNPOW 2 x = x    by notation
216*)
217Theorem involute_alt:
218  !f s. f involute s <=> f endo s /\ !x. x IN s ==> FUNPOW f 2 x = x
219Proof
220  simp[FUNPOW_2] >>
221  metis_tac[]
222QED
223
224
225
226(* ------------------------------------------------------------------------- *)
227
228(* export theory at end *)
229val _ = export_theory();
230
231(*===========================================================================*)
232