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