Skip to content
Permalink
Browse files

Fix drule applications by using old_drule from preamble

  • Loading branch information...
mn200 committed Aug 13, 2019
1 parent 8057740 commit df1f93720f2c2199f983713e5b4358e95ccdced0
@@ -11,6 +11,8 @@ val _ = new_theory"bvl_inlineProof";

val _ = set_grammar_ancestry [ "bvlSem", "bvlProps", "bvl_inline" ];

val drule = old_drule

(* removal of ticks *)

val state_rel_def = Define `
@@ -21,6 +21,7 @@ val _ = set_grammar_ancestry
val _ = Parse.hide"str";

val handle_ok_def = bvl_handleProofTheory.handle_ok_def;
val drule = old_drule

(* value relation *)
val _ = temp_overload_on ("num_stubs", ``bvl_num_stubs``)
@@ -2239,6 +2239,9 @@ max_print_depth := 800
fun say0 pfx s g = (print (pfx ^ ": " ^ s ^ "\n"); ALL_TAC g)
val say = say0 "calls_correct";


val drule = old_drule

Theorem calls_correct:
(∀tmp xs env1 s0 g0 g env2 ^t0 ys res s l l1 g1.
tmp = (xs,env1,s0) ∧
@@ -369,7 +369,7 @@ Proof
\\ rveq \\ fs [] \\ rveq \\ fs []
\\ fs [Once case_eq_thms] \\ rveq \\ fs[]
THEN1 (fs [code_rel_def])
\\ drule (Q.SPEC `vs` lookup_vars_lemma)
\\ drule_then (qspec_then ‘vs’ mp_tac) lookup_vars_lemma
\\ CASE_TAC \\ strip_tac
\\ fs [] \\ rveq \\ fs [code_rel_def]
\\ imp_res_tac lookup_vars_SOME \\ fs[])
@@ -412,7 +412,7 @@ Proof
\\ rveq \\ fs [] \\ rveq \\ fs [code_locs_def]
\\ fs [Once case_eq_thms] \\ rveq \\ fs[]
THEN1 (fs [code_rel_def, SUBSET_DEF] \\ rw[] \\ fs[])
\\ drule (Q.SPEC `vs` lookup_vars_lemma)
\\ drule_then (qspec_then `vs` mp_tac) lookup_vars_lemma
\\ CASE_TAC \\ strip_tac
\\ fs [] \\ rveq \\ fs [code_rel_def]
\\ imp_res_tac lookup_vars_SOME \\ fs[]
@@ -509,7 +509,7 @@ Proof
\\ rveq \\ fs [] \\ rveq \\ fs []
\\ fs [Once case_eq_thms] \\ rveq
THEN1 (fs [code_rel_def])
\\ drule (Q.SPEC `vs` lookup_vars_lemma)
\\ drule_then (qspec_then ‘vs’ mp_tac) lookup_vars_lemma
\\ CASE_TAC \\ strip_tac
\\ fs [] \\ rveq \\ fs [code_rel_def])
THEN1 (* Letrec *)
@@ -533,7 +533,7 @@ Proof
\\ fs [EL_MAP]
\\ pairarg_tac
\\ fs [f_rel_def, code_rel_def])
\\ drule (Q.SPEC `x` lookup_vars_lemma)
\\ drule_then (qspec_then ‘x’ mp_tac) lookup_vars_lemma
\\ CASE_TAC \\ fs [] \\ rveq \\ fs []
\\ strip_tac \\ fs []
\\ first_x_assum irule \\ fs []
@@ -638,7 +638,7 @@ Proof
\\ imp_res_tac state_rel_IMP_max_app_EQ \\ fs []
\\ IF_CASES_TAC \\ fs [] \\ rveq \\ fs []
\\ Cases_on `vsopt` \\ fs [] \\ rveq \\ fs []
\\ drule (Q.SPEC `x` lookup_vars_lemma) \\ strip_tac
\\ drule_then (qspec_then ‘x’ mp_tac) lookup_vars_lemma \\ strip_tac
\\ Cases_on `lookup_vars x env2` \\ fs [] \\ rveq \\ fs []
\\ fs [code_rel_def])
THEN1 (* Letrec *)
@@ -668,7 +668,7 @@ Proof
\\ strip_tac \\ fs []
\\ `!l1 l2. LIST_REL v_rel l1 l2 ==> LIST_REL v_rel
(GENLIST (Recclosure loc [] l1 fns') (LENGTH fns') ++ env1)
(GENLIST (Recclosure loc [] l2 (MAP (\(num_args, x).
(GENLIST (Recclosure loc [] l2 (MAP (λ(num_args, x).
(num_args, HD (remove_ticks [x]))) fns'))
(LENGTH fns') ++ env2)` by
(qpat_x_assum `LIST_REL _ _ _` mp_tac
@@ -28,6 +28,8 @@ val _ = set_grammar_ancestry
"backendProps", "ffi", "lprefix_lub"
];

val drule = old_drule

val _ = temp_bring_to_front_overload"evaluate"{Name="evaluate",Thy="bvlSem"};
val _ = temp_bring_to_front_overload"num_stubs"{Name="num_stubs",Thy="clos_to_bvl"};
val _ = temp_bring_to_front_overload"compile_exps"{Name="compile_exps",Thy="clos_to_bvl"};
@@ -26,6 +26,7 @@ val _ = hide "next";

val _ = temp_overload_on("FALSE_CONST",``Const (n2w 2:'a word)``)
val _ = temp_overload_on("TRUE_CONST",``Const (n2w 18:'a word)``)
val drule = old_drule

(* TODO: move *)
val _ = type_abbrev("state", ``:('a,'c,'ffi)wordSem$state``)
@@ -13,6 +13,8 @@ val good_dimindex_def = labPropsTheory.good_dimindex_def;

val _ = new_theory "data_to_word_memoryProof";

val drule = old_drule

(* TODO: move? *)
val clean_tac = rpt var_eq_tac \\ rpt (qpat_x_assum `T` kall_tac)
fun rpt_drule th = drule (th |> GEN_ALL) \\ rpt (disch_then drule \\ fs [])
@@ -15,6 +15,7 @@ val _ = set_grammar_ancestry ["misc","ffi","bag","flatProps","patProps",
"flat_to_pat","backendProps","backend_common"];

val _ = Parse.hide"U";
val drule = old_drule

val pmatch_flat_def = flatSemTheory.pmatch_def

@@ -10,6 +10,7 @@ open preamble ffiTheory BasicProvers
local open stack_removeProofTheory in end

val _ = new_theory "lab_to_targetProof";
val drule = old_drule

fun say0 pfx s g = (print (pfx ^ ": " ^ s ^ "\n"); ALL_TAC g)

@@ -11,6 +11,7 @@ val _ = new_theory"pat_to_closProof"
val _ = set_grammar_ancestry
["patLang", "patSem", "patProps", "pat_to_clos",
"closLang", "closSem", "closProps"];
val drule = old_drule

(* value translation *)

@@ -20,6 +20,7 @@ val _ = set_grammar_ancestry["stack_alloc", "stackLang", "stackSem", "stackProps
];
val _ = temp_overload_on("good_dimindex", ``labProps$good_dimindex``);
val _ = temp_bring_to_front_overload"compile"{Thy="stack_alloc",Name="compile"};
val drule = old_drule

(* TODO: move and join with stack_remove *)

@@ -15,6 +15,7 @@ val _ = new_theory"stack_removeProof";

val word_shift_def = backend_commonTheory.word_shift_def
val _ = temp_overload_on ("num_stubs", ``stack_num_stubs``)
val drule = old_drule

(* TODO: move *)

@@ -24,6 +24,7 @@ val index_list_def = Define `
(index_list [] n = []) /\
(index_list (x::xs) n = (n + LENGTH xs,x) :: index_list xs n)`

val drule = old_drule
Theorem LENGTH_index_list:
!l n. LENGTH (index_list l n) = LENGTH l
Proof
@@ -19,6 +19,7 @@ val is_phy_var_tac =
metis_tac[arithmeticTheory.MOD_EQ_0];

val rmd_thms = (remove_dead_conventions |>SIMP_RULE std_ss [LET_THM,FORALL_AND_THM])|>CONJUNCTS
val drule = old_drule

Theorem FST_compile_single[simp]:
FST (compile_single a b c d e) = FST (FST e)
@@ -531,5 +531,39 @@ in
(REWR_CONV set_cons THENC RAND_CONV set_conv)
)
end
local
fun BRING_NAME_TO_FRONT_CONV n t =
let val (vs, b) = strip_forall t
in
case vs of
[] => NO_CONV
| v::rest => if #1 (dest_var v) = n then ALL_CONV
else BINDER_CONV (BRING_NAME_TO_FRONT_CONV n) THENC
SWAP_VARS_CONV
end t

fun SPECtop th =
let val (v, _) = dest_forall (concl th)
in
SPEC v th
end

fun SPECnames [] th = th
| SPECnames (n::ns) th =
case Lib.total (CONV_RULE (BRING_NAME_TO_FRONT_CONV n)) th of
NONE => SPECnames ns th
| SOME th' => SPECnames ns (SPECtop th')

fun specnames_then fvnms ttac th = ttac (SPECnames fvnms th)
in
fun old_drule_then ttac th =
let val fvnames = map (#1 o dest_var) (th |> concl |> free_vars)
in
drule_then (specnames_then fvnames ttac) th
end
val old_drule = old_drule_then mp_tac

end


end

0 comments on commit df1f937

Please sign in to comment.
You can’t perform that action at this time.