summaryrefslogtreecommitdiff
path: root/backends/hol4/divDefLib.sml
diff options
context:
space:
mode:
Diffstat (limited to 'backends/hol4/divDefLib.sml')
-rw-r--r--backends/hol4/divDefLib.sml356
1 files changed, 136 insertions, 220 deletions
diff --git a/backends/hol4/divDefLib.sml b/backends/hol4/divDefLib.sml
index ef18d14f..abf8908d 100644
--- a/backends/hol4/divDefLib.sml
+++ b/backends/hol4/divDefLib.sml
@@ -7,12 +7,10 @@ open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory
open primitivesLib
(* TODO:
-pred_def_thms -> pred_defs
-pred_def_thm -> pred_def
raw_def_thms -> raw_defs
raw_def_thm -> raw_def
-fuel_defs_thm -> fuel_defs (and split the theorem)
+fuel_defs -> fuel_defs (and split the theorem)
*)
(* TODO: move *)
@@ -105,60 +103,6 @@ fun mk_diverge_tm (ty : hol_type) : term =
diverge_tm
end
-(*
-(* TODO: move *)
-fun strip_pair_type (ty : hol_type) : hol_type list =
- let
- val {Args=args, Thy=thy, Tyop=tyop} = dest_thy_type ty
- in
- if thy = "pair" andalso tyop = "prod" then
- case args of
- [x, y] => x :: strip_pair_type y
- | _ => failwith "Unexpected"
- else [ty]
- end
- handle HOL_ERR _ => [ty]
-
-fun list_mk_pair_type (tys : hol_type list) : hol_type =
- case tys of
- [] => failwith "Unexpected"
- | [x] => x
- | x :: tys =>
- mk_thy_type {Args = [x, list_mk_pair_type tys], Thy="pair", Tyop="prod"}
-
-fun strip_sum_type (ty : hol_type) : hol_type list =
- let
- val {Args=args, Thy=thy, Tyop=tyop} = dest_thy_type ty
- in
- if thy = "sum" andalso tyop = "sum" then
- case args of
- [x, y] => x :: strip_sum_type y
- | _ => failwith "Unexpected"
- else [ty]
- end
- handle HOL_ERR _ => [ty]
-
-fun list_mk_sum_type (tys : hol_type list) : hol_type =
- case tys of
- [] => failwith "Unexpected"
- | [x] => x
- | x :: tys =>
- mk_thy_type {Args = [x, list_mk_sum_type tys], Thy="sum", Tyop="sum"}
-*)
-
-
-(*
-val ty = “: ('a # 'b) # num # int”
-strip_pair_type ty
-list_mk_pair_type (strip_pair_type ty)
-
-val ty = “: ('a + 'b) + num + int”
-strip_sum_type ty
-list_mk_sum_type (strip_sum_type ty)
-
-val ty = “: (num # 'a # bool) + (num # int # bool) + (num # 'a)”
-*)
-
(* Small utility: we sometimes need to generate a termination measure for
the fuel definitions.
@@ -242,7 +186,7 @@ val num_ty::rem_tys = tys
val (tuple_var, tuple_case) = hd tuple_cases
*)
-fun mk_fuel_defs (def_tms : term list) : thm =
+fun mk_fuel_defs (def_tms : term list) : thm list =
let
(* Retrieve the identifiers.
@@ -323,22 +267,14 @@ fun mk_fuel_defs (def_tms : term list) : thm =
val temp_def = Hol_defn def_name ‘^fuel_defs_conj’
Defn.tgoal temp_def
*)
- val fuel_defs_thm = tDefine def_name ‘^fuel_defs_conj’ prove_termination_tac
+ val fuel_defs = tDefine def_name ‘^fuel_defs_conj’ prove_termination_tac
in
- fuel_defs_thm
+ CONJUNCTS fuel_defs
end
(*
-val (asms, g) = top_goal ()
-
-val rty = ref “:num”
-val ty = !rty
-(hd o snd o dest_type) ty
-*)
-
-(*
-val (fuel_tms, fuel_defs_thm) = mk_fuel_defs def_tms
-val fuel_def_tms = map (snd o strip_forall) ((strip_conj o concl) fuel_defs_thm)
+val (fuel_tms, fuel_defs) = mk_fuel_defs def_tms
+val fuel_def_tms = map (snd o strip_forall) ((strip_conj o concl) fuel_defs)
val (def_tm, fuel_def_tm) = hd (zip def_tms fuel_def_tms)
*)
@@ -373,7 +309,7 @@ fun mk_fuel_predicate_defs (def_tm, fuel_def_tm) : thm =
end
(*
-val pred_def_thms = map mk_fuel_predicate_defs (zip def_tms fuel_def_tms)
+val pred_defs = map mk_fuel_predicate_defs (zip def_tms fuel_def_tms)
*)
(* Tactic which makes progress in a proof by making a case disjunction (we use
@@ -381,26 +317,7 @@ val pred_def_thms = map mk_fuel_predicate_defs (zip def_tms fuel_def_tms)
fun case_progress (asms, g) =
let
val scrut = (strip_all_cases_get_scrutinee o lhs) g
- in Cases_on ‘^scrut’ (asms, g) end
-
-(* Tactic to prove the fuel monotonicity theorem - TODO: move below *)
-fun prove_fuel_mono_tac (pred_def_thms : thm list) (fuel_defs_thm : thm) =
- Induct_on ‘^fuel_var0’ >-(
- (* The ___P predicates are false: n is 0 *)
- fs pred_def_thms >>
- fs [is_diverge_def] >>
- pure_once_rewrite_tac [fuel_defs_thm] >> fs []) >>
- gen_tac >>
- Cases_on ‘^fuel_var1’ >-(
- (* Contradiction: SUC n < 0 *)
- rw [] >> exfalso >> int_tac) >>
- fs pred_def_thms >>
- fs [is_diverge_def] >>
- pure_once_rewrite_tac [fuel_defs_thm] >> fs [bind_def] >>
- (* Split the goals *)
- rw [] >>
- (* Explore all the paths *)
- rpt (case_progress >> fs [])
+ in Cases_on ‘^scrut’ (asms, g) end
(* Prove the fuel monotonicity properties.
@@ -411,10 +328,10 @@ fun prove_fuel_mono_tac (pred_def_thms : thm list) (fuel_defs_thm : thm) =
(!i. n <= m ==> odd___P i n ==> odd___fuel n i = odd___fuel m i)
]}
*)
-fun prove_fuel_mono (pred_def_thms : thm list) (fuel_defs_thm : thm) : thm =
+fun prove_fuel_mono (pred_defs : thm list) (fuel_defs : thm list) : thm =
let
- val pred_tms = map (lhs o snd o strip_forall o concl) pred_def_thms
- val fuel_tms = map (lhs o snd o strip_forall o concl) (CONJUNCTS fuel_defs_thm)
+ val pred_tms = map (lhs o snd o strip_forall o concl) pred_defs
+ val fuel_tms = map (lhs o snd o strip_forall o concl) fuel_defs
val pred_fuel_tms = zip pred_tms fuel_tms
(* Generate terms of the shape:
!i. n <= m ==> even___P i n ==> even___fuel n i = even___fuel m i
@@ -439,13 +356,31 @@ fun prove_fuel_mono (pred_def_thms : thm list) (fuel_defs_thm : thm) : thm =
val fuel_eq_tms = list_mk_conj fuel_eq_tms
(* Qantify over the fuels *)
val fuel_eq_tms = list_mk_forall ([fuel_var0, fuel_var1], fuel_eq_tms)
+ (* The tactic for the proof *)
+ val prove_tac =
+ Induct_on ‘^fuel_var0’ >-(
+ (* The ___P predicates are false: n is 0 *)
+ fs pred_defs >>
+ fs [is_diverge_def] >>
+ pure_once_rewrite_tac fuel_defs >> fs []) >>
+ gen_tac >>
+ Cases_on ‘^fuel_var1’ >-(
+ (* Contradiction: SUC n < 0 *)
+ rw [] >> exfalso >> int_tac) >>
+ fs pred_defs >>
+ fs [is_diverge_def] >>
+ pure_once_rewrite_tac fuel_defs >> fs [bind_def] >>
+ (* Split the goals *)
+ rw [] >>
+ (* Explore all the paths *)
+ rpt (case_progress >> fs [])
in
(* Prove *)
- save_goal_and_prove (fuel_eq_tms, prove_fuel_mono_tac pred_def_thms fuel_defs_thm)
+ save_goal_and_prove (fuel_eq_tms, prove_tac)
end
(*
-val fuel_mono_thm = prove_fuel_mono pred_def_thms fuel_defs_thm
+val fuel_mono_thm = prove_fuel_mono pred_defs fuel_defs
*)
(* Prove the property about the least upper bound.
@@ -460,13 +395,13 @@ val fuel_mono_thm = prove_fuel_mono pred_def_thms fuel_defs_thm
TODO: merge with other functions? (prove_pred_imp_fuel_eq_raw_thms)
*)
-fun prove_least_fuel_mono (pred_def_thms : thm list) (fuel_mono_thm : thm) : thm list =
+fun prove_least_fuel_mono (pred_defs : thm list) (fuel_mono_thm : thm) : thm list =
let
val thl = (CONJUNCTS o SPECL [fuel_var0, fuel_var1]) fuel_mono_thm
- fun mk_least_fuel_thm (pred_def_thm, mono_thm) : thm =
+ fun mk_least_fuel_thm (pred_def, mono_thm) : thm =
let
(* Retrieve the predicate, without the fuel *)
- val pred_tm = (lhs o snd o strip_forall o concl) pred_def_thm
+ val pred_tm = (lhs o snd o strip_forall o concl) pred_def
val (pred_tm, args) = strip_comb pred_tm
val args = rev (tl (rev args))
val pred_tm = list_mk_comb (pred_tm, args)
@@ -485,7 +420,7 @@ fun prove_least_fuel_mono (pred_def_thms : thm list) (fuel_mono_thm : thm) : thm
th
end
in
- map mk_least_fuel_thm (zip pred_def_thms thl)
+ map mk_least_fuel_thm (zip pred_defs thl)
end
(* Prove theorems of the shape:
@@ -496,11 +431,11 @@ fun prove_least_fuel_mono (pred_def_thms : thm list) (fuel_mono_thm : thm) : thm
TODO: merge with other functions? (prove_pred_imp_fuel_eq_raw_thms)
*)
-fun prove_least_pred_thms (pred_def_thms : thm list) : thm list =
+fun prove_least_pred_thms (pred_defs : thm list) : thm list =
let
- fun prove_least_pred_thm (pred_def_thm : thm) : thm =
+ fun prove_least_pred_thm (pred_def : thm) : thm =
let
- val pred_tm = (lhs o snd o strip_forall o concl) pred_def_thm
+ val pred_tm = (lhs o snd o strip_forall o concl) pred_def
val (pred_no_fuel_tm, args) = strip_comb pred_tm
val args = rev (tl (rev args))
val pred_no_fuel_tm = list_mk_comb (pred_no_fuel_tm, args)
@@ -529,12 +464,12 @@ fun prove_least_pred_thms (pred_def_thms : thm list) : thm list =
save_goal_and_prove (tm, prove_tac)
end
in
- map prove_least_pred_thm pred_def_thms
+ map prove_least_pred_thm pred_defs
end
(*
-val least_pred_thms = prove_least_pred_thms pred_def_thms
+val least_pred_thms = prove_least_pred_thms pred_defs
val least_pred_thm = hd least_pred_thms
*)
@@ -545,11 +480,11 @@ val least_pred_thm = hd least_pred_thms
!n i. even___P i n ==> even___P i ($LEAST (even___P i))
]}
*)
-fun prove_pred_n_imp_pred_least_thms (pred_def_thms : thm list) : thm list =
+fun prove_pred_n_imp_pred_least_thms (pred_defs : thm list) : thm list =
let
- fun prove_pred_n_imp_pred_least (pred_def_thm : thm) : thm =
+ fun prove_pred_n_imp_pred_least (pred_def : thm) : thm =
let
- val pred_tm = (lhs o snd o strip_forall o concl) pred_def_thm
+ val pred_tm = (lhs o snd o strip_forall o concl) pred_def
val (pred_no_fuel_tm, args) = strip_comb pred_tm
val args = rev (tl (rev args))
val pred_no_fuel_tm = list_mk_comb (pred_no_fuel_tm, args)
@@ -575,12 +510,12 @@ fun prove_pred_n_imp_pred_least_thms (pred_def_thms : thm list) : thm list =
save_goal_and_prove (tm, prove_tac)
end
in
- map prove_pred_n_imp_pred_least pred_def_thms
+ map prove_pred_n_imp_pred_least pred_defs
end
(*
-val (pred_def_thm, mono_thm) = hd (zip pred_def_thms thl)
-val least_fuel_mono_thms = prove_least_fuel_mono pred_def_thms fuel_defs_thm fuel_mono_thm
+val (pred_def, mono_thm) = hd (zip pred_defs thl)
+val least_fuel_mono_thms = prove_least_fuel_mono pred_defs fuel_defs fuel_mono_thm
val least_fuel_mono_thm = hd least_fuel_mono_thms
*)
@@ -591,16 +526,16 @@ val least_fuel_mono_thm = hd least_fuel_mono_thms
even i = if (?n. even___P i n) then even___P ($LEAST (even___P i)) i else Diverge
]}
*)
-fun define_raw_defs (def_tms : term list) (pred_def_thms : thm list) (fuel_defs_thm : thm) : thm list =
+fun define_raw_defs (def_tms : term list) (pred_defs : thm list) (fuel_defs : thm list) : thm list =
let
- fun define_raw_def (def_tm, (pred_def_thm, fuel_def_thm)) : thm =
+ fun define_raw_def (def_tm, (pred_def, fuel_def)) : thm =
let
val app = lhs def_tm
- val pred_tm = (lhs o snd o strip_forall o concl) pred_def_thm
+ val pred_tm = (lhs o snd o strip_forall o concl) pred_def
(* Make the “?n. even___P i n” term *)
val exists_fuel_tm = mk_exists (fuel_var0, pred_tm)
(* Make the “even___fuel ($LEAST (even___P i)) i” term *)
- val fuel_tm = (lhs o snd o strip_forall o concl) fuel_def_thm
+ val fuel_tm = (lhs o snd o strip_forall o concl) fuel_def
val (pred_tm, args) = strip_comb pred_tm
val args = rev (tl (rev args))
val pred_tm = list_mk_comb (pred_tm, args)
@@ -616,48 +551,40 @@ fun define_raw_defs (def_tms : term list) (pred_def_thms : thm list) (fuel_defs_
Define ‘^raw_def_tm’
end
in
- map define_raw_def (zip def_tms (zip pred_def_thms (CONJUNCTS fuel_defs_thm)))
+ map define_raw_def (zip def_tms (zip pred_defs fuel_defs))
end
(*
-val raw_def_thms = define_raw_defs def_tms pred_def_thms fuel_defs_thm
+val raw_defs = define_raw_defs def_tms pred_defs fuel_defs
*)
-(*
-val pred_def_thm = hd pred_def_thms
-
-val pred_n_imp_pred_least_thms = prove_pred_n_imp_pred_least_thms pred_def_thms
-
-val pred_n_imp_pred_least_thm = hd pred_n_imp_pred_least_thms
-*)
-
(* Prove theorems of the shape:
!n i. even___P i n ==> even___fuel n i = even i
*)
-fun prove_pred_imp_fuel_eq_raw_def_thms
- (pred_def_thms : thm list)
+fun prove_pred_imp_fuel_eq_raw_defs
+ (pred_defs : thm list)
(fuel_def_tms : term list)
(least_fuel_mono_thms : thm list)
(least_pred_thms : thm list)
(pred_n_imp_pred_least_thms : thm list)
- (raw_def_thms : thm list) :
+ (raw_defs : thm list) :
thm list =
let
- fun prove_thm (pred_def_thm,
+ fun prove_thm (pred_def,
(fuel_def_tm,
(least_fuel_mono_thm,
(least_pred_thm,
- (pred_n_imp_pred_least_thm, raw_def_thm))))) : thm =
+ (pred_n_imp_pred_least_thm, raw_def))))) : thm =
let
(* Generate: “even___P i n” *)
- val pred_tm = (lhs o snd o strip_forall o concl) pred_def_thm
+ val pred_tm = (lhs o snd o strip_forall o concl) pred_def
val (pred_no_fuel_tm, args) = strip_comb pred_tm
val args = rev (tl (rev args))
(* Generate: “even___fuel n i” *)
val fuel_tm = lhs fuel_def_tm
(* Generate: “even i” *)
- val raw_def_tm = (lhs o snd o strip_forall o concl) raw_def_thm
+ val raw_def_tm = (lhs o snd o strip_forall o concl) raw_def
(* Generate: “even___fuel n i = even i” *)
val tm = mk_eq (fuel_tm, raw_def_tm)
(* Add the implication *)
@@ -669,7 +596,7 @@ fun prove_pred_imp_fuel_eq_raw_def_thms
val prove_tac =
rpt gen_tac >>
strip_tac >>
- fs raw_def_thms >>
+ fs raw_defs >>
(* Case on ‘?n. even___P i n’ *)
CASE_TAC >> fs [] >>
(* Use the monotonicity property *)
@@ -680,23 +607,15 @@ fun prove_pred_imp_fuel_eq_raw_def_thms
save_goal_and_prove (tm, prove_tac)
end
in
- map prove_thm (zip pred_def_thms (zip fuel_def_tms (zip least_fuel_mono_thms
- (zip least_pred_thms (zip pred_n_imp_pred_least_thms raw_def_thms)))))
+ map prove_thm (zip pred_defs (zip fuel_def_tms (zip least_fuel_mono_thms
+ (zip least_pred_thms (zip pred_n_imp_pred_least_thms raw_defs)))))
end
(*
-val pred_imp_fuel_eq_raw_def_thms =
- prove_pred_imp_fuel_eq_raw_def_thms
- pred_def_thms fuel_def_tms least_fuel_mono_thms least_pred_thms
- pred_n_imp_pred_least_thms raw_def_thms
-
-val (pred_def_thm,
- (fuel_def_tm,
- (least_fuel_mono_thm,
- (least_pred_thm,
- (pred_n_imp_pred_least_thm, raw_def_thm))))) =
- hd (zip pred_def_thms (zip fuel_def_tms (zip least_fuel_mono_thms
- (zip least_pred_thms (zip pred_n_imp_pred_least_thms raw_def_thms)))))
+val pred_imp_fuel_eq_raw_defs =
+ prove_pred_imp_fuel_eq_raw_defs
+ pred_defs fuel_def_tms least_fuel_mono_thms least_pred_thms
+ pred_n_imp_pred_least_thms raw_defs
*)
@@ -754,8 +673,8 @@ val expand_defs = gen_expand_defs def_tms
*)
fun mk_termination_diverge_tms
(def_tms : term list)
- (pred_def_thms : thm list)
- (raw_def_thms : thm list)
+ (pred_defs : thm list)
+ (raw_defs : thm list)
(expand_defs : thm list) :
(term * term) list =
let
@@ -769,33 +688,33 @@ fun mk_termination_diverge_tms
where on the left we have *variables* and on the right we have
the "raw" definitions.
*)
- fun mk_fun_subst (def_tm, raw_def_thm) =
+ fun mk_fun_subst (def_tm, raw_def) =
let
val var = (fst o strip_comb o lhs) def_tm
- val f = (fst o strip_comb o lhs o snd o strip_forall o concl) raw_def_thm
+ val f = (fst o strip_comb o lhs o snd o strip_forall o concl) raw_def
in
(var |-> f)
end
- val fun_subst = map mk_fun_subst (zip def_tms raw_def_thms)
+ val fun_subst = map mk_fun_subst (zip def_tms raw_defs)
- fun mk_tm (pred_def_thm, (raw_def_thm, expand_def)) :
+ fun mk_tm (pred_def, (raw_def, expand_def)) :
term * term =
let
(* “even___P i n” *)
- val pred_tm = (lhs o snd o strip_forall o concl) pred_def_thm
+ val pred_tm = (lhs o snd o strip_forall o concl) pred_def
(* “even i = even___expand even odd i” *)
val expand_tm = (lhs o snd o strip_forall o concl) expand_def
val expand_tm = subst fun_subst expand_tm
- val fun_tm = (lhs o snd o strip_forall o concl) raw_def_thm
+ val fun_tm = (lhs o snd o strip_forall o concl) raw_def
val fun_eq_tm = mk_eq (fun_tm, expand_tm)
in (pred_tm, fun_eq_tm) end
in
- map mk_tm (zip pred_def_thms (zip raw_def_thms expand_defs))
+ map mk_tm (zip pred_defs (zip raw_defs expand_defs))
end
(*
val term_div_tms =
- mk_termination_diverge_tms pred_def_thms raw_def_thms expand_defs
+ mk_termination_diverge_tms pred_defs raw_defs expand_defs
*)
(* Prove the termination lemmas:
@@ -808,26 +727,26 @@ val term_div_tms =
*)
fun prove_termination_thms
(term_div_tms : (term * term) list)
- (fuel_defs_thm : thm)
- (pred_def_thms : thm list)
- (raw_def_thms : thm list)
+ (fuel_defs : thm list)
+ (pred_defs : thm list)
+ (raw_defs : thm list)
(expand_defs : thm list)
(pred_n_imp_pred_least_thms : thm list)
- (pred_imp_fuel_eq_raw_def_thms : thm list)
+ (pred_imp_fuel_eq_raw_defs : thm list)
: thm list =
let
(* Create a map from functions in the recursive group to lemmas
to apply *)
- fun mk_rec_fun_eq_pair (fuel_def_thm, eq_th) =
+ fun mk_rec_fun_eq_pair (fuel_def, eq_th) =
let
- val rfun = (get_fun_name_from_app o lhs o snd o strip_forall o concl) fuel_def_thm
+ val rfun = (get_fun_name_from_app o lhs o snd o strip_forall o concl) fuel_def
in
(rfun, eq_th)
end
val rec_fun_eq_map =
Redblackmap.fromList const_name_compare (
map mk_rec_fun_eq_pair
- (zip (CONJUNCTS fuel_defs_thm) pred_imp_fuel_eq_raw_def_thms))
+ (zip fuel_defs pred_imp_fuel_eq_raw_defs))
(* Small tactic which rewrites the recursive calls *)
fun rewrite_rec_call (asms, g) =
@@ -844,7 +763,7 @@ fun prove_termination_thms
val eq_th = INST var_s (INST_TYPE ty_s eq_th)
val eq_th = thm_to_conj_implies eq_th
(* Some tactics *)
- val premise_tac = fs pred_def_thms >> fs [is_diverge_def]
+ val premise_tac = fs pred_defs >> fs [is_diverge_def]
in
(* Apply the theorem, prove the premise, and rewrite *)
(prove_premise_then premise_tac assume_tac eq_th >> fs []) (asms, g)
@@ -870,7 +789,7 @@ fun prove_termination_thms
disch_tac >>
(* Expand the raw definition and get rid of the ‘?n ...’ *)
- pure_once_rewrite_tac raw_def_thms >>
+ pure_once_rewrite_tac raw_defs >>
pure_asm_rewrite_tac [] >>
(* Simplify *)
@@ -884,14 +803,14 @@ fun prove_termination_thms
last_x_assum ignore_tac >>
(* Expand *)
- fs pred_def_thms >>
+ fs pred_defs >>
fs [is_diverge_def] >>
fs expand_defs >>
(* We need to be a bit careful when expanding the definitions which use fuel:
it can make the simplifier loop. *)
rpt (pop_assum mp_tac) >>
- pure_once_rewrite_tac [fuel_defs_thm] >>
+ pure_once_rewrite_tac fuel_defs >>
rpt disch_tac >>
(* Expand the binds *)
@@ -909,17 +828,9 @@ fun prove_termination_thms
(*
val termination_thms =
- prove_termination_thms term_div_tms fuel_defs_thm pred_def_thms
- raw_def_thms expand_defs pred_n_imp_pred_least_thms
- pred_imp_fuel_eq_raw_def_thms
-
-val expand_def = hd expand_defs
-
-val all_args = (zip pred_def_thms (zip raw_def_thms (zip expand_defs pred_n_imp_pred_least_thms)))
-val (pred_def_thm, (raw_def_thm, (expand_def, pred_n_imp_pred_least_thm))) = hd all_args
-val (pred_def_thm, (raw_def_thm, (expand_def, pred_n_imp_pred_least_thm))) = hd (tl all_args)
-
-set_goal ([], tm)
+ prove_termination_thms term_div_tms fuel_defs pred_defs
+ raw_defs expand_defs pred_n_imp_pred_least_thms
+ pred_imp_fuel_eq_raw_defs
*)
(* Prove the divergence lemmas:
@@ -937,18 +848,18 @@ set_goal ([], tm)
*)
fun prove_divergence_thms
(term_div_tms : (term * term) list)
- (fuel_defs_thm : thm)
- (pred_def_thms : thm list)
- (raw_def_thms : thm list)
+ (fuel_defs : thm list)
+ (pred_defs : thm list)
+ (raw_defs : thm list)
(expand_defs : thm list)
: thm list =
let
(* Create a set containing the names of all the functions in the recursive group *)
- fun get_rec_fun_id (fuel_def_thm : thm) =
- (get_fun_name_from_app o lhs o snd o strip_forall o concl) fuel_def_thm
+ fun get_rec_fun_id (fuel_def : thm) =
+ (get_fun_name_from_app o lhs o snd o strip_forall o concl) fuel_def
val rec_fun_set =
Redblackset.fromList const_name_compare (
- map get_rec_fun_id raw_def_thms)
+ map get_rec_fun_id raw_defs)
(* Small tactic which rewrites the recursive calls *)
fun rewrite_rec_call (asms, g) =
@@ -971,18 +882,18 @@ fun prove_divergence_thms
a conversion to rewrite “odd i” to a term which contains
the “?n. odd___P i n” we are looking for.
*)
- val exists_g = (rhs o concl) (PURE_REWRITE_CONV raw_def_thms scrut)
+ val exists_g = (rhs o concl) (PURE_REWRITE_CONV raw_defs scrut)
val (_, exists_g, _) = TypeBase.dest_case exists_g
(* The tactic to prove the subgoal *)
val prove_sg_tac =
- pure_rewrite_tac raw_def_thms >>
+ pure_rewrite_tac raw_defs >>
Cases_on ‘^exists_g’ >> pure_asm_rewrite_tac [] >> fs [] >>
(* There must only remain the positive case (i.e., “?n. ...”):
we have a contradiction *)
exfalso >>
(* The end of the proof is done by opening the definitions *)
pop_assum mp_tac >>
- fs pred_def_thms >> fs [is_diverge_def]
+ fs pred_defs >> fs [is_diverge_def]
in
(SUBGOAL_THEN g assume_tac >- prove_sg_tac >> fs []) (asms, g)
end
@@ -1012,7 +923,7 @@ fun prove_divergence_thms
val prove_tac =
rpt gen_tac >>
- pure_rewrite_tac raw_def_thms >>
+ pure_rewrite_tac raw_defs >>
rpt disch_tac >>
(* This allows to simplify the “?n. even___P i n” *)
@@ -1021,14 +932,14 @@ fun prove_divergence_thms
last_x_assum ignore_tac >>
(* Expand *)
- fs pred_def_thms >> fs [is_diverge_def] >>
+ fs pred_defs >> fs [is_diverge_def] >>
fs expand_defs >>
(* We need to be a bit careful when expanding the definitions which use fuel:
it can make the simplifier loop.
*)
pop_assum mp_tac >>
- pure_once_rewrite_tac [fuel_defs_thm] >>
+ pure_once_rewrite_tac fuel_defs >>
rpt disch_tac >> fs [] >>
(* Evaluate all the paths *)
@@ -1044,16 +955,10 @@ fun prove_divergence_thms
val divergence_thms =
prove_divergence_thms
term_div_tms
- fuel_defs_thm
- pred_def_thms
- raw_def_thms
+ fuel_defs
+ pred_defs
+ raw_defs
expand_defs
-
-val (pred_tm, fun_eq_tm) = hd term_div_tms
-
-set_goal ([], tm)
-
-val (asms, g) = top_goal ()
*)
(* Prove the final lemmas:
@@ -1070,7 +975,7 @@ fun prove_final_eqs
(term_div_tms : (term * term) list)
(termination_thms : thm list)
(divergence_thms : thm list)
- (raw_def_thms : thm list)
+ (raw_defs : thm list)
: thm list =
let
fun prove_one ((pred_tm, fun_eq_tm), (termination_thm, divergence_thm)) : thm =
@@ -1078,7 +983,7 @@ fun prove_final_eqs
val (_, args) = strip_comb (lhs fun_eq_tm)
val g = list_mk_forall (args, fun_eq_tm)
(* We make a case disjunction of the subgoal: “exists n. even___P i n” *)
- val exists_g = (rhs o concl) (PURE_REWRITE_CONV raw_def_thms (lhs fun_eq_tm))
+ val exists_g = (rhs o concl) (PURE_REWRITE_CONV raw_defs (lhs fun_eq_tm))
val (_, exists_g, _) = TypeBase.dest_case exists_g
val prove_tac =
rpt gen_tac >>
@@ -1125,20 +1030,19 @@ fun DefineDiv (def_qt : term quotation) =
if i = 0 then Return T else odd_fuel (i - 1))
]}
*)
- (* TODO: list of theorems *)
- val fuel_defs_thm = mk_fuel_defs def_tms
+ val fuel_defs = mk_fuel_defs def_tms
(* Generate the predicate definitions.
{[ even___P n i = = ~is_diverge (even___fuel n i) ]}
*)
- val fuel_def_tms = map (snd o strip_forall) ((strip_conj o concl) fuel_defs_thm)
- val pred_def_thms = map mk_fuel_predicate_defs (zip def_tms fuel_def_tms)
+ val fuel_def_tms = map (snd o strip_forall o concl) fuel_defs
+ val pred_defs = map mk_fuel_predicate_defs (zip def_tms fuel_def_tms)
(* Prove the monotonicity property for the fuel, all at once
*)
- val fuel_mono_thm = prove_fuel_mono pred_def_thms fuel_defs_thm
+ val fuel_mono_thm = prove_fuel_mono pred_defs fuel_defs
(* Prove the individual fuel functions - TODO: update
@@ -1146,21 +1050,21 @@ fun DefineDiv (def_qt : term quotation) =
!n i. $LEAST (even___P i) <= n ==> even___fuel n i = even___fuel ($LEAST (even___P i)) i
]}
*)
- val least_fuel_mono_thms = prove_least_fuel_mono pred_def_thms fuel_mono_thm
+ val least_fuel_mono_thms = prove_least_fuel_mono pred_defs fuel_mono_thm
(*
{[
!n i. even___P i n ==> $LEAST (even___P i) <= n
]}
*)
- val least_pred_thms = prove_least_pred_thms pred_def_thms
+ val least_pred_thms = prove_least_pred_thms pred_defs
(*
{[
!n i. even___P i n ==> even___P i ($LEAST (even___P i))
]}
*)
- val pred_n_imp_pred_least_thms = prove_pred_n_imp_pred_least_thms pred_def_thms
+ val pred_n_imp_pred_least_thms = prove_pred_n_imp_pred_least_thms pred_defs
(*
"Raw" definitions:
@@ -1169,30 +1073,30 @@ fun DefineDiv (def_qt : term quotation) =
even i = if (?n. even___P i n) then even___P ($LEAST (even___P i)) i else Diverge
]}
*)
- val raw_def_thms = define_raw_defs def_tms pred_def_thms fuel_defs_thm
+ val raw_defs = define_raw_defs def_tms pred_defs fuel_defs
(*
!n i. even___P i n ==> even___fuel n i = even i
*)
- val pred_imp_fuel_eq_raw_def_thms =
- prove_pred_imp_fuel_eq_raw_def_thms
- pred_def_thms fuel_def_tms least_fuel_mono_thms
- least_pred_thms pred_n_imp_pred_least_thms raw_def_thms
+ val pred_imp_fuel_eq_raw_defs =
+ prove_pred_imp_fuel_eq_raw_defs
+ pred_defs fuel_def_tms least_fuel_mono_thms
+ least_pred_thms pred_n_imp_pred_least_thms raw_defs
(* "Expand" definitions *)
val expand_defs = gen_expand_defs def_tms
(* Small utility *)
- val term_div_tms = mk_termination_diverge_tms def_tms pred_def_thms raw_def_thms expand_defs
+ val term_div_tms = mk_termination_diverge_tms def_tms pred_defs raw_defs expand_defs
(* Termination theorems *)
val termination_thms =
- prove_termination_thms term_div_tms fuel_defs_thm pred_def_thms
- raw_def_thms expand_defs pred_n_imp_pred_least_thms pred_imp_fuel_eq_raw_def_thms
+ prove_termination_thms term_div_tms fuel_defs pred_defs
+ raw_defs expand_defs pred_n_imp_pred_least_thms pred_imp_fuel_eq_raw_defs
(* Divergence theorems *)
val divergence_thms =
- prove_divergence_thms term_div_tms fuel_defs_thm pred_def_thms raw_def_thms expand_defs
+ prove_divergence_thms term_div_tms fuel_defs pred_defs raw_defs expand_defs
(* Final theorems:
@@ -1201,8 +1105,20 @@ fun DefineDiv (def_qt : term quotation) =
⊢ ∀i. odd i = odd___E even odd i
]}
*)
- val final_eqs = prove_final_eqs term_div_tms termination_thms divergence_thms raw_def_thms
+ val final_eqs = prove_final_eqs term_div_tms termination_thms divergence_thms raw_defs
in
(* We return the final equations, which act as rewriting theorems *)
final_eqs
end
+
+(*
+val def_qt = ‘
+ (even (i : int) : bool result =
+ if i = 0 then Return T else odd (i - 1)) /\
+ (odd (i : int) : bool result =
+ if i = 0 then Return F else even (i - 1))
+’
+
+val even_def = DefineDiv def_qt
+
+*)
generated by cgit v1.2.3 (git 2.25.1) at 2025-11-04 07:19:19 +0000