summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--backends/hol4/Test.sml30
1 files changed, 25 insertions, 5 deletions
diff --git a/backends/hol4/Test.sml b/backends/hol4/Test.sml
index a01211d0..ef110cb1 100644
--- a/backends/hol4/Test.sml
+++ b/backends/hol4/Test.sml
@@ -763,7 +763,7 @@ val t = “u32_to_int (int_to_u32 3)”
val th = (UNDISCH_ALL o SPEC_ALL) int_to_u32_id
*)
-fun instantiate_dep_rewrites (th : thm) (t : term) : thm list =
+fun instantiate_dep_rewrites_in_terms (th : thm) (tl : term list) : thm list =
let
val th = (UNDISCH_ALL o SPEC_ALL) th;
(* We use a map when storing the theorems, to avoid storing the same theorem twice *)
@@ -776,7 +776,7 @@ fun instantiate_dep_rewrites (th : thm) (t : term) : thm list =
end
handle HOL_ERR _ => ();
(* Explore the term *)
- val _ = dep_apply_in_subterms try_instantiate (Redblackset.empty String.compare) t;
+ val _ = app (dep_apply_in_subterms try_instantiate (Redblackset.empty String.compare)) tl;
in
map snd (Redblackmap.listItems (!inst_thms))
end
@@ -794,8 +794,7 @@ fun apply_dep_rewrites_tac (prove_premise : tactic) (then_tac : thm_tactic) (th
fn (asms, g) =>
let
(* Discharge the assumptions so that the goal is one single term *)
- val dg = list_mk_imp (asms, g)
- val thms = instantiate_dep_rewrites th dg;
+ val thms = instantiate_dep_rewrites_in_terms th (g :: asms);
val thms = map thm_to_conj_implies thms;
(* Apply each theorem *)
in
@@ -884,6 +883,13 @@ val rewrite_all_int_conversion_ids : tactic =
*)
val massage : tactic = assume_bounds_for_all_int_vars >> rewrite_all_int_conversion_ids
+(*
+SIMP_CONV arith_ss [ADD] “1 + (x : num)”
+SIMP_CONV list_ss [ADD, EL] “EL (Num (1+x)) (t::list_t_v ls)”
+
+m “1 + x = SUC x”
+*)
+
Theorem nth_lem:
!(ls : 't list_t) (i : u32).
u32_to_int i < int_of_num (LENGTH (list_t_v ls)) ==>
@@ -903,7 +909,21 @@ Proof
imp_res_tac U32_SUB_EQ >> fs [st_ex_bind_def, list_t_v_def] >> rw [] >>
massage >> fs [] >> rw [] >>
(* Finish the proof by recursion *)
- (* TODO: automate (it should be in massage) *)
+ (* TODO: automate (it should be in massage).
+
+ Steps:
+ - rewrite: x = y - 1 => Num y = SUC x
+
+ TODO: generalize?
+ - x = y - z ==> 0 <= x ==> Num y = z + x
+ - then apply rewriting such as ADD (1 + ...)?
+ - or: two versions of the theorem, and we prioritize the first one:
+ x = y - 1 ==> 0 <= x ==> Num y = SUC z
+ x = y - z ==> 0 <= x ==> Num y = y - z
+ - or: EL (x + 1) ls = EL (SUC x) ls
+ (and other theorems like this)
+ (but there will be a loooot of theorems)
+ *)
qspec_then ‘u32_to_int z’ imp_res_tac NUM_SUB_1_EQ >> rw [] >> rfs [] >>
(* TODO: automate this: we should be able to analyze the ‘nth ls z’,
notice there is a quantified assumption in the context,