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