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 "dest_args" "not enough args in function application" 38 | dest_args (d::t) = (d,t); 39 40fun basic_lemmas ifn_def rdepth_thm = 41 let open optionSyntax numSyntax 42 val ifn_app = lhs(snd(strip_forall(concl ifn_def))) 43 val (ifn,args) = strip_comb ifn_app 44 val (d,args') = dest_args args 45 val argfrees = free_varsl args 46 val is_some_ifn_goal = 47 list_mk_forall(args, mk_imp(mk_is_some ifn_app, 48 mk_neg(mk_eq(d,zero_tm)))) 49 val is_some_ifn_thm = 50 prove(is_some_ifn_goal, Cases THEN RW_TAC std_ss [Once ifn_def]) 51 handle e => raise ERR "is_some_ifn_thm" "tactic failed" 52 val ty = dest_option (type_of ifn_app) 53 val a = variant argfrees (mk_var("a",ty)) 54 val ifn_some_goal = list_mk_forall(args@[a], 55 mk_imp(mk_eq(ifn_app,mk_some a), 56 mk_neg(mk_eq(d,zero_tm)))) 57 val ifn_some_thm = prove(ifn_some_goal, ACCEPT_TAC 58 (Ho_Rewrite.PURE_REWRITE_RULE [IS_SOME_EXISTS,GSYM LEFT_FORALL_IMP_THM] 59 is_some_ifn_thm)) 60 handle e => raise ERR "is_ifn_some_thm" "tactic failed" 61 val ifn_dlem_goal = list_mk_forall(args, 62 mk_imp(mk_is_some ifn_app, 63 mk_eq (ifn_app,list_mk_comb(ifn,mk_suc d::args')))) 64 val ifn_dlem = prove(ifn_dlem_goal,DLEM_TAC ifn_def ifn_some_thm) 65 handle e => raise ERR "ifn_dlem" "tactic failed" 66 val d1 = variant argfrees (mk_var("d1",num)) 67 val ifn_mono_goal = list_mk_forall(d::d1::args', 68 mk_imp(mk_conj(mk_is_some ifn_app,mk_leq(d,d1)), 69 mk_eq(ifn_app,list_mk_comb(ifn,d1::args')))) 70 val ifn_mono_thm = prove(ifn_mono_goal, 71 REWRITE_TAC [LESS_EQ_EXISTS] THEN REPEAT STRIP_TAC 72 THEN BasicProvers.VAR_EQ_TAC 73 THEN Induct_on `p` THEN REWRITE_TAC [ADD_CLAUSES] 74 THEN POP_ASSUM SUBST_ALL_TAC 75 THEN MATCH_MP_TAC ifn_dlem THEN ASM_REWRITE_TAC[]) 76 handle e => raise ERR "ifn_mono_thm" "tactic failed" 77 val rdepth_tm = fst(strip_comb(fst(dest_leq(snd(dest_imp 78 (snd(dest_forall (snd(dest_conj(snd(dest_imp 79 (snd(strip_forall (concl rdepth_thm)))))))))))))) 80 val rdepth_app = list_mk_comb(rdepth_tm,args') 81 val ifn_norm_goal = list_mk_forall(args, 82 mk_imp(mk_is_some ifn_app, 83 mk_eq(ifn_app, list_mk_comb(ifn,rdepth_app::args')))) 84 val ifn_norm_thm = prove(ifn_norm_goal, 85 REPEAT STRIP_TAC THEN IMP_RES_TAC rdepth_thm 86 THEN MATCH_MP_TAC (GSYM ifn_mono_thm) 87 THEN ASM_REWRITE_TAC []) 88 handle e => raise ERR "ifn_norm_thm" "tactic failed" 89 val ifn_determ_goal = list_mk_forall(d::d1::args', 90 mk_imp(mk_conj(mk_is_some(ifn_app), 91 mk_is_some(list_mk_comb(ifn,d1::args'))), 92 mk_eq(ifn_app,list_mk_comb(ifn,d1::args')))) 93 val ifn_determ_thm = prove(ifn_determ_goal, 94 REPEAT STRIP_TAC THEN IMP_RES_TAC ifn_norm_thm 95 THEN ASM_REWRITE_TAC[]) 96 handle e => raise ERR "ifn_determ_thm" "tactic failed" 97 in 98 (is_some_ifn_thm, ifn_some_thm,ifn_dlem,ifn_mono_thm,ifn_norm_thm, ifn_determ_thm) 99 end 100 handle e => raise wrap_exn "basic_lemmas" "proof failed" e; 101 102 103(* 104val (is_some_ifn_thm, _, ifn_mono_thm, 105 ifn_norm_thm, ifn_determ_thm) = basic_lemmas ifn_def rdepth_thm; 106*) 107 108end; 109