liftingScript.sml

1Theory lifting
2Ancestors
3  transfer
4
5Definition Qt_def:
6  Qt R Abs Rep Tf <=>
7    R = inv Tf O Tf /\
8    (!a b. Tf a b ==> Abs a = b) /\
9    !a. Tf (Rep a) a
10End
11
12Theorem Qt_alt:
13  Qt R Abs Rep Tf <=>
14      (!a. Abs (Rep a) = a) /\
15      (!a. R (Rep a) (Rep a)) /\
16      (!c1 c2. R c1 c2 <=> R c1 c1 /\ R c2 c2 /\ Abs c1 = Abs c2) /\
17      (Tf = \c a. R c c /\ Abs c = a)
18Proof
19  simp[Qt_def, FUN_EQ_THM, relationTheory.inv_DEF, relationTheory.O_DEF] >>
20  metis_tac[]
21QED
22
23Theorem Qt_alt_def2: (* isabelle name *)
24  Qt R Abs Rep Tf <=>
25    (!c a. Tf c a ==> Abs c = a) /\
26    (!a. Tf (Rep a) a) /\
27    !c1 c2. R c1 c2 <=> Tf c1 (Abs c2) /\ Tf c2 (Abs c1)
28Proof
29  simp[Qt_def, FUN_EQ_THM, relationTheory.O_DEF, relationTheory.inv_DEF] >>
30  metis_tac[]
31QED
32
33
34Theorem idQ[simp]:
35  Qt $= I I $=
36Proof
37  simp[Qt_def, FUN_EQ_THM, relationTheory.inv_DEF] >> metis_tac[]
38QED
39
40Theorem R_repabs:
41  Qt R Abs Rep Tf ==> !x. R x x ==> R (Rep (Abs x)) x
42Proof
43  rw[Qt_def,relationTheory.O_DEF,relationTheory.inv_DEF, PULL_EXISTS,IN_DEF]>>
44  metis_tac[]
45QED
46
47Theorem pairQ:
48  Qt R1 Abs1 Rep1 Tf1 /\ Qt R2 Abs2 Rep2 Tf2 ==>
49  Qt (R1 ### R2) (Abs1 ## Abs2) (Rep1 ## Rep2) (Tf1 ### Tf2)
50Proof
51  simp[Qt_def, pairTheory.FORALL_PROD, FUN_EQ_THM, PAIR_REL_def,
52       relationTheory.inv_DEF, relationTheory.O_DEF, pairTheory.EXISTS_PROD] >>
53  metis_tac[]
54QED
55
56Theorem listQ:
57  Qt R Abs Rep Tf ==> Qt (LIST_REL R) (MAP Abs) (MAP Rep) (LIST_REL Tf)
58Proof
59  simp[Qt_def, FUN_EQ_THM, relationTheory.inv_DEF, relationTheory.O_DEF] >>
60  rw[]
61  >- (rename [‘LIST_REL R al bl <=> ?y. _ y /\ _ y’] >>
62      map_every qid_spec_tac [‘bl’, ‘al’] >> Induct_on ‘al’ >>
63      simp[PULL_EXISTS] >> metis_tac[])
64  >- (rename [‘MAP Abs al = bl’] >>
65      pop_assum mp_tac >> map_every qid_spec_tac [‘bl’, ‘al’] >>
66      Induct_on ‘al’ >>
67      simp[PULL_EXISTS] >> metis_tac[])
68  >- (rename [‘LIST_REL Tf (MAP Rep al) al’] >>
69      Induct_on ‘al’ >> simp[PULL_EXISTS])
70QED
71
72Definition map_fun_def:
73  map_fun f g h = g o h o f
74End
75val _ = set_mapped_fixity{fixity = Infixr 501, term_name = "map_fun",
76                          tok = "--->"}
77
78Theorem map_fun_thm[simp]:
79  (f ---> g) h x = g (h (f x))
80Proof
81  simp[map_fun_def]
82QED
83
84Theorem map_fun_I[simp]:
85  (f ---> I) = combin$C $o f /\ (I ---> g) = $o g
86Proof
87  simp[FUN_EQ_THM]
88QED
89
90(* no idea which orientation of this makes most sense *)
91Theorem map_fun_o:
92  (f1 o f2) ---> (g1 o g2) = (f2 ---> g1) o (f1 ---> g2)
93Proof
94  simp[FUN_EQ_THM]
95QED
96
97
98Theorem map_fun_id[simp]:
99  (I ---> I) = I
100Proof
101  simp[FUN_EQ_THM, map_fun_def]
102QED
103
104Theorem funQ:
105  Qt (D : 'a -> 'a -> bool) AbsD (RepD : 'c -> 'a) (TfD : 'a -> 'c -> bool) /\
106  Qt (R : 'b -> 'b -> bool) (AbsR : 'b -> 'd) (RepR : 'd -> 'b)
107     (TfR : 'b -> 'd -> bool) ==>
108  Qt ((D |==> R) : ('a -> 'b) -> ('a -> 'b) -> bool)
109     (RepD ---> AbsR)
110     (AbsD ---> RepR)
111     (TfD |==> TfR)
112Proof
113  simp[Qt_alt_def2, relationTheory.O_DEF, relationTheory.inv_DEF, FUN_EQ_THM,
114       FUN_REL_def, PULL_EXISTS] >> metis_tac[]
115QED
116
117Theorem setQ:
118  Qt (R : 'a -> 'a -> bool) Abs (Rep : 'b -> 'a) Tf ==>
119  Qt (R |==> (=)) (PREIMAGE Rep) (PREIMAGE Abs) (Tf |==> (=))
120Proof
121  strip_tac >> drule (INST_TYPE [beta |-> bool, delta |-> bool] funQ) >>
122  ‘PREIMAGE Rep = Rep ---> I /\ PREIMAGE Abs = Abs ---> I’
123    by simp[FUN_EQ_THM, IN_DEF] >>
124  ntac 2 (pop_assum SUBST1_TAC) >> disch_then irule >> simp[]
125QED
126
127Theorem HK_thm2:
128  Qt R Abs Rep Tf /\ f = Abs t /\ R t t ==> Tf t f
129Proof
130  simp[Qt_alt_def2] >> metis_tac[]
131QED
132
133Theorem Qt_EQ:
134  Qt R Abs Rep Tf ==> (Tf |==> Tf |==> (=)) R $=
135Proof
136  simp[Qt_def, FUN_REL_def, relationTheory.inv_DEF,
137       relationTheory.O_DEF] >> metis_tac[]
138QED
139
140Theorem Qt_right_unique:
141  Qt R Abs Rep Tf ==> right_unique Tf
142Proof
143  simp[Qt_def, right_unique_def, relationTheory.O_DEF, relationTheory.inv_DEF]>>
144  metis_tac[]
145QED
146
147Theorem Qt_surj:
148  Qt R Abs Rep Tf ==> surj Tf
149Proof
150  simp[Qt_def, surj_def, relationTheory.inv_DEF, relationTheory.O_DEF] >>
151  metis_tac[]
152QED