1
2open HolKernel Parse boolLib bossLib pairLib pairSyntax pairTheory PairRules;
3
4(*---------------------------------------------------------------------------------*)
5
6val _ = new_theory "ACF";
7
8(*---------------------------------------------------------------------------*)
9(* Convert HOL programs to combinator-based pseudo-ASTs                      *)
10(* Term programs is translated to equivalent A-Combinator Forms (ACF)        *)
11(*---------------------------------------------------------------------------*)
12
13val sc_def =
14  Define
15   `sc (f1:'a->'b) (f2:'b->'c) = \x. f2(f1 x)`;
16
17val cj_def =
18 Define
19   `cj f1 f2 f3 = \x. if f1 x then f2 x else f3 x`;
20
21val tr_def =
22 TotalDefn.DefineSchema
23   `tr (x:'a) = if f1 x then x else tr (f2 x)`;
24
25val tr_ind = fetch "-" "tr_ind";
26
27(*---------------------------------------------------------------------------*)
28(* HOL programs is converted to sc, tr and cj structures                     *)
29(*---------------------------------------------------------------------------*)
30
31val tr_INTRO = store_thm
32("tr_INTRO",
33 ``!f f1 f2.
34     (!x:'a. f x = if f1(x) then x else f(f2 x))
35     ==> (?R. WF R /\ (!x. ~f1 x ==> R (f2 x) x))
36     ==> (f:'a->'a = tr f1 f2)``,
37
38  REPEAT (GEN_TAC ORELSE STRIP_TAC) THEN
39  ONCE_REWRITE_TAC [FUN_EQ_THM] THEN
40  HO_MATCH_MP_TAC tr_ind THEN
41  GEN_TAC THEN STRIP_TAC THEN
42  IMP_RES_TAC (DISCH_ALL tr_def) THEN
43  POP_ASSUM (fn th => ONCE_REWRITE_TAC[th]) THEN
44  METIS_TAC[]
45 );
46
47val rec_INTRO = store_thm
48("rec_INTRO",
49 ``!f f1 f2 f3.
50     (!x:'a. f x = if f1(x) then f2(x) else f(f3 x))
51     ==> (?R. WF R /\ (!x. ~f1 x ==> R (f3 x) x))
52     ==> (f:'a->'b = sc (tr f1 f3) f2)``,
53
54  REPEAT (GEN_TAC ORELSE STRIP_TAC) THEN
55  ONCE_REWRITE_TAC [FUN_EQ_THM] THEN
56  GEN_TAC THEN
57  IMP_RES_TAC  relationTheory.WF_INDUCTION_THM THEN
58  POP_ASSUM (MATCH_MP_TAC o SIMP_RULE std_ss [] o
59          Q.SPEC `\x. f x = sc (tr f1 f3) f2 x`) THEN
60  REPEAT STRIP_TAC THEN
61  Cases_on `f1 x` THENL [
62    METIS_TAC [sc_def, DISCH_ALL tr_def],
63
64    IMP_RES_TAC (DISCH_ALL tr_def) THEN
65    METIS_TAC [sc_def]
66  ]
67 );
68
69
70(*---------------------------------------------------------------------------------*)
71
72val _ = export_theory();
73