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