1structure pflLib = 2struct 3 4open HolKernel boolLib bossLib ; 5open arithmeticTheory optionTheory; 6 7val ERR = mk_HOL_ERR "pflLib"; 8 9val MAX_LE_THM = Q.prove 10(`!m n. m <= MAX m n /\ n <= MAX m n`, 11 RW_TAC arith_ss [MAX_DEF]); 12 13val IS_SOME_EXISTS = Q.prove 14(`!x. IS_SOME x = ?y. x = SOME y`, 15 Cases THEN METIS_TAC [optionTheory.IS_SOME_DEF]); 16 17fun GOAL_REWRITE_TAC rws = 18 RULE_ASSUM_TAC (REWRITE_RULE rws) THEN REWRITE_TAC rws; 19 20(*---------------------------------------------------------------------------*) 21(* Prove lemma of the form *) 22(* *) 23(* IS_SOME (ifn d args) ==> (ifn d args = ifn (SUC d) args) *) 24(* *) 25(*---------------------------------------------------------------------------*) 26 27fun DLEM_TAC ifn_def ifn_some_thm = 28(Ho_Rewrite.REWRITE_TAC [IS_SOME_EXISTS,GSYM LEFT_FORALL_IMP_THM] THEN 29 Induct THEN REPEAT GEN_TAC THENL 30 [STRIP_TAC THEN IMP_RES_TAC ifn_some_thm THEN 31 POP_ASSUM MP_TAC THEN REWRITE_TAC [], 32 ONCE_REWRITE_TAC [ifn_def] THEN BasicProvers.EVERY_CASE_TAC THEN 33 GOAL_REWRITE_TAC [SUC_SUB1,NOT_SOME_NONE, NOT_NONE_SOME, IS_SOME_DEF] THEN 34 STRIP_TAC THEN RES_THEN MP_TAC THEN RW_TAC (srw_ss()) []]) 35 handle e => raise ERR "DLEM_TAC" "unable to prove stability lemma"; 36 37fun dest_args [] = raise ERR 38 "dest_args" 39 "not enough args in function application" 40 | dest_args (d::t) = (d,t); 41 42fun basic_lemmas ifn_def rdepth_thm = 43 let open optionSyntax numSyntax 44 val ifn_app = lhs(snd(strip_forall(concl ifn_def))) 45 val (ifn,args) = strip_comb ifn_app 46 val (d,args') = dest_args args 47 val argfrees = free_varsl args 48 val is_some_ifn_goal = 49 list_mk_forall(args, mk_imp(mk_is_some ifn_app, 50 mk_neg(mk_eq(d,zero_tm)))) 51 val is_some_ifn_thm = 52 prove(is_some_ifn_goal, Cases THEN RW_TAC std_ss [Once ifn_def]) 53 handle e => raise ERR "is_some_ifn_thm" "tactic failed" 54 val ty = dest_option (type_of ifn_app) 55 val a = variant argfrees (mk_var("a",ty)) 56 val ifn_some_goal = list_mk_forall(args@[a], 57 mk_imp(mk_eq(ifn_app,mk_some a), 58 mk_neg(mk_eq(d,zero_tm)))) 59 val ifn_some_thm = prove(ifn_some_goal, ACCEPT_TAC 60 (Ho_Rewrite.PURE_REWRITE_RULE 61 [IS_SOME_EXISTS,GSYM LEFT_FORALL_IMP_THM] 62 is_some_ifn_thm)) 63 handle e => raise ERR "is_ifn_some_thm" "tactic failed" 64 val ifn_dlem_goal = 65 list_mk_forall(args, 66 mk_imp(mk_is_some ifn_app, 67 mk_eq (ifn_app, 68 list_mk_comb(ifn,mk_suc d::args')))) 69 val ifn_dlem = prove(ifn_dlem_goal,DLEM_TAC ifn_def ifn_some_thm) 70 handle e => raise ERR "ifn_dlem" "tactic failed" 71 val d1 = variant argfrees (mk_var("d1",num)) 72 val ifn_mono_goal = 73 list_mk_forall(d::d1::args', 74 mk_imp(mk_conj(mk_is_some ifn_app,mk_leq(d,d1)), 75 mk_eq(ifn_app,list_mk_comb(ifn,d1::args')))) 76 val ifn_mono_thm = prove(ifn_mono_goal, 77 REWRITE_TAC [LESS_EQ_EXISTS] THEN REPEAT STRIP_TAC 78 THEN BasicProvers.VAR_EQ_TAC 79 THEN Induct_on `p` THEN REWRITE_TAC [ADD_CLAUSES] 80 THEN POP_ASSUM SUBST_ALL_TAC 81 THEN MATCH_MP_TAC ifn_dlem THEN ASM_REWRITE_TAC[]) 82 handle e => raise ERR "ifn_mono_thm" "tactic failed" 83 val rdepth_tm = fst(strip_comb(fst(dest_leq(snd(dest_imp 84 (snd(dest_forall (snd(dest_conj(snd(dest_imp 85 (snd(strip_forall (concl rdepth_thm)))))))))))))) 86 val rdepth_app = list_mk_comb(rdepth_tm,args') 87 val ifn_norm_goal = 88 list_mk_forall(args, 89 mk_imp(mk_is_some ifn_app, 90 mk_eq(ifn_app, 91 list_mk_comb(ifn,rdepth_app::args')))) 92 val ifn_norm_thm = prove(ifn_norm_goal, 93 REPEAT STRIP_TAC THEN IMP_RES_TAC rdepth_thm 94 THEN MATCH_MP_TAC (GSYM ifn_mono_thm) 95 THEN ASM_REWRITE_TAC []) 96 handle e => raise ERR "ifn_norm_thm" "tactic failed" 97 val ifn_determ_goal = 98 list_mk_forall(d::d1::args', 99 mk_imp(mk_conj(mk_is_some(ifn_app), 100 mk_is_some(list_mk_comb(ifn,d1::args'))), 101 mk_eq(ifn_app,list_mk_comb(ifn,d1::args')))) 102 val ifn_determ_thm = prove(ifn_determ_goal, 103 REPEAT STRIP_TAC THEN IMP_RES_TAC ifn_norm_thm 104 THEN ASM_REWRITE_TAC[]) 105 handle e => raise ERR "ifn_determ_thm" "tactic failed" 106 in 107 (is_some_ifn_thm, ifn_some_thm,ifn_dlem,ifn_mono_thm, 108 ifn_norm_thm, ifn_determ_thm) 109 end 110 handle e => raise wrap_exn "basic_lemmas" "proof failed" e; 111 112 113(* 114val (is_some_ifn_thm, _, ifn_mono_thm, 115 ifn_norm_thm, ifn_determ_thm) = basic_lemmas ifn_def rdepth_thm; 116*) 117 118end; 119