| (* |
| * Copyright 2018, Data61 |
| * Commonwealth Scientific and Industrial Research Organisation (CSIRO) |
| * ABN 41 687 119 230. |
| * |
| * This software may be distributed and modified according to the terms of |
| * the BSD 2-Clause license. Note that NO WARRANTY is provided. |
| * See "LICENSE_BSD2.txt" for details. |
| * |
| * @TAG(DATA61_BSD) |
| *) |
| |
| theory SpecialisedLemmaTactic |
| imports |
| "Cogent.CogentHelper" |
| "Cogent.ML_Old" |
| "Cogent_Corres" |
| "Specialised_Lemma_Utils" |
| begin |
| |
| context update_sem_init |
| begin |
| |
| ML\<open> fun corres_take_boxed_tac ctxt = let |
| val val_rels = ValRelSimp.get ctxt; |
| val type_rels = TypeRelSimp.get ctxt; |
| val is_valids = IsValidSimp.get ctxt; |
| val heap_simps = HeapSimp.get ctxt; |
| val gets = Proof_Context.get_thms ctxt |
| val get = Proof_Context.get_thm ctxt |
| val facts' = maps gets |
| ["state_rel_def", "heap_rel_def", "val_rel_ptr_def", "type_rel_ptr_def", "heap_rel_ptr_meta"] |
| val facts = facts' @ is_valids @ heap_simps |
| in EVERY' [ |
| asm_full_simp_tac ((put_simpset HOL_basic_ss ctxt) addsimps [get "val_rel_ptr_def"]), |
| REPEAT_ALL_NEW (etac @{thm exE}), |
| ((rtac (get "corres_take_boxed") ORELSE' rtac (get "corres_member_boxed")) |
| THEN_ALL_NEW (TRY o atac) |
| THEN_ALL_NEW asm_full_simp_tac ctxt |
| THEN_ALL_NEW clarsimp_tac (ctxt addsimps facts) |
| THEN_ALL_NEW (rtac (get "u_t_p_recE") THEN' atac) |
| THEN_ALL_NEW clarsimp_tac (ctxt addSDs (gets "type_repr_uval_repr")) |
| THEN_ALL_NEW (ftac (get "all_heap_rel_ptrD") THEN' atac) |
| THEN_ALL_NEW clarsimp_tac (ctxt addsimps type_rels addsimps val_rels) |
| ) ] end |
| \<close> |
| |
| ML\<open> fun corres_put_boxed_tac ctxt = let |
| val gets = Proof_Context.get_thms ctxt |
| val get = Proof_Context.get_thm ctxt |
| val type_rels = TypeRelSimp.get ctxt; |
| val val_rels = ValRelSimp.get ctxt; |
| val is_valids = IsValidSimp.get ctxt; |
| val heap_simps = HeapSimp.get ctxt; |
| val facts1 = get "val_rel_ptr_def" :: @{thms gets_to_return return_bind} |
| val facts2 = maps gets |
| ["state_rel_def", "heap_rel_def", "val_rel_ptr_def", "type_rel_ptr_def", "heap_rel_ptr_meta"] |
| val facts3 = facts2 @ is_valids @ heap_simps |
| fun trace str i t = (@{print tracing} str; @{print tracing} t; Seq.succeed t) |
| in |
| EVERY' [ |
| asm_full_simp_tac ((put_simpset HOL_basic_ss ctxt) addsimps facts1), |
| REPEAT_ALL_NEW (etac @{thm exE}), |
| ((rtac (get "corres_put_boxed" |> Simplifier.rewrite_rule ctxt @{thms gets_to_return[THEN eq_reflection]}) |
| THEN' simp_tac ctxt |
| THEN' atac THEN' atac THEN' atac) |
| THEN_ALL_NEW asm_full_simp_tac ctxt), |
| clarsimp_tac (ctxt addsimps facts3), |
| (rtac (get "u_t_p_recE") THEN' atac) THEN_ALL_NEW asm_full_simp_tac ctxt, |
| clarsimp_tac (ctxt addSDs (gets "type_repr_uval_repr") |
| addsimps type_rels), |
| (ftac (get "all_heap_rel_ptrD") THEN' atac) |
| THEN_ALL_NEW asm_full_simp_tac (ctxt addsimps type_rels), |
| clarsimp_tac ctxt, |
| REPEAT_ALL_NEW (rtac @{thm conjI}) |
| THEN_ALL_NEW ((rtac (get "all_heap_rel_updE") THEN' atac THEN' atac) |
| THEN_ALL_NEW distinct_subgoal_tac |
| THEN_ALL_NEW asm_simp_tac (ctxt addsimps val_rels @ type_rels) |
| THEN_ALL_NEW asm_simp_tac (ctxt addsimps @{thms map_update list_update_eq_id} |
| delsimps @{thms length_0_conv length_greater_0_conv}) |
| THEN_ALL_NEW clarsimp_tac (ctxt addsimps val_rels @ type_rels) |
| ) |
| ] |
| ORELSE' |
| EVERY' [ |
| asm_full_simp_tac ((put_simpset HOL_basic_ss ctxt) addsimps facts1), |
| REPEAT_ALL_NEW (etac @{thm exE}), |
| ((rtac (get "corres_put_boxed" |> Simplifier.rewrite_rule ctxt @{thms gets_to_return[THEN eq_reflection]}) |
| THEN' simp_tac ctxt |
| THEN' atac THEN' atac THEN' atac) |
| THEN_ALL_NEW asm_full_simp_tac ctxt), |
| clarsimp_tac (ctxt addsimps facts3), |
| (rtac (get "u_t_p_recE") THEN' atac) THEN_ALL_NEW asm_full_simp_tac ctxt, |
| clarsimp_tac (ctxt addSDs (gets "type_repr_uval_repr") |
| addsimps type_rels), |
| (ftac (get "all_heap_rel_ptrD") THEN' atac) |
| THEN_ALL_NEW asm_full_simp_tac (ctxt addsimps type_rels), |
| ((rtac (get "all_heap_rel_updE") THEN' atac THEN' atac) |
| THEN_ALL_NEW distinct_subgoal_tac |
| THEN_ALL_NEW asm_simp_tac (ctxt addsimps val_rels @ type_rels) |
| THEN_ALL_NEW asm_simp_tac (ctxt addsimps @{thms map_update list_update_eq_id} |
| delsimps @{thms length_0_conv length_greater_0_conv}) |
| THEN_ALL_NEW clarsimp_tac (ctxt addsimps val_rels @ type_rels) |
| ) |
| ] |
| end |
| \<close> |
| |
| ML\<open> fun corres_let_put_boxed_tac ctxt = let |
| val gets = Proof_Context.get_thms ctxt |
| val get = Proof_Context.get_thm ctxt |
| val type_rels = TypeRelSimp.get ctxt; |
| val val_rels = ValRelSimp.get ctxt; |
| val is_valids = IsValidSimp.get ctxt; |
| val heap_simps = HeapSimp.get ctxt; |
| val facts1 = get "val_rel_ptr_def" :: @{thms gets_to_return return_bind} |
| val facts2 = maps gets |
| ["state_rel_def", "heap_rel_def", "val_rel_ptr_def", "type_rel_ptr_def", "heap_rel_ptr_meta"] |
| val facts3 = facts2 @ is_valids @ heap_simps |
| in |
| EVERY' [ |
| asm_full_simp_tac ((put_simpset HOL_basic_ss ctxt) addsimps facts1), |
| REPEAT_ALL_NEW (etac @{thm exE}), |
| ((rtac (get "corres_let_put_boxed") THEN' simp_tac ctxt THEN' atac THEN' atac THEN' atac) |
| THEN_ALL_NEW asm_full_simp_tac ctxt), |
| clarsimp_tac (ctxt addsimps facts3), |
| (rtac (get "u_t_p_recE") THEN' atac) THEN_ALL_NEW asm_full_simp_tac ctxt, |
| clarsimp_tac (ctxt addSDs (gets "type_repr_uval_repr") |
| addsimps type_rels), |
| (ftac (get "all_heap_rel_ptrD") THEN' atac) |
| THEN_ALL_NEW asm_full_simp_tac (ctxt addsimps type_rels), |
| clarsimp_tac ctxt, |
| REPEAT_ALL_NEW (rtac @{thm conjI}) |
| THEN_ALL_NEW ((rtac (get "all_heap_rel_updE") THEN' atac THEN' atac) |
| THEN_ALL_NEW distinct_subgoal_tac |
| THEN_ALL_NEW asm_simp_tac (ctxt addsimps val_rels @ type_rels) |
| THEN_ALL_NEW asm_simp_tac (ctxt addsimps @{thms map_update list_update_eq_id} |
| delsimps @{thms length_0_conv length_greater_0_conv}) |
| THEN_ALL_NEW clarsimp_tac (ctxt addsimps val_rels @ type_rels) |
| ) |
| ] |
| ORELSE' |
| EVERY' [ |
| asm_full_simp_tac ((put_simpset HOL_basic_ss ctxt) addsimps facts1), |
| REPEAT_ALL_NEW (etac @{thm exE}), |
| ((rtac (get "corres_let_put_boxed") THEN' simp_tac ctxt THEN' atac THEN' atac THEN' atac) |
| THEN_ALL_NEW asm_full_simp_tac ctxt), |
| clarsimp_tac (ctxt addsimps facts3), |
| (rtac (get "u_t_p_recE") THEN' atac) THEN_ALL_NEW asm_full_simp_tac ctxt, |
| clarsimp_tac (ctxt addSDs (gets "type_repr_uval_repr") |
| addsimps type_rels), |
| (ftac (get "all_heap_rel_ptrD") THEN' atac) |
| THEN_ALL_NEW asm_full_simp_tac (ctxt addsimps type_rels), |
| ((rtac (get "all_heap_rel_updE") THEN' atac THEN' atac) |
| THEN_ALL_NEW distinct_subgoal_tac |
| THEN_ALL_NEW asm_simp_tac (ctxt addsimps val_rels @ type_rels) |
| THEN_ALL_NEW asm_simp_tac (ctxt addsimps @{thms map_update list_update_eq_id} |
| delsimps @{thms length_0_conv length_greater_0_conv}) |
| THEN_ALL_NEW clarsimp_tac (ctxt addsimps val_rels @ type_rels) |
| ) |
| ] |
| end |
| \<close> |
| |
| ML\<open> fun corres_take_unboxed_tac ctxt = let |
| val get = Proof_Context.get_thm ctxt |
| in asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps (ValRelSimp.get ctxt)) 1 |
| THEN (REPEAT_ALL_NEW (eresolve_tac ctxt @{thms exE conjE}) 1) |
| THEN rtac (get "corres_take_unboxed") 1 |
| THEN ALLGOALS (TRY o atac) |
| THEN ALLGOALS (clarsimp_tac (ctxt addsimps ValRelSimp.get ctxt @ TypeRelSimp.get ctxt)) |
| end |
| \<close> |
| |
| ML\<open> fun corres_case_tac ctxt = SUBGOAL (fn (t, i) => let |
| val vr_simps = ValRelSimp.get ctxt |
| val vr_simp_idx = make_thm_index scrape_C_types vr_simps |
| val vr_simps = lookup_thm_index vr_simp_idx (scrape_C_types_term t) |
| val thm = Proof_Context.get_thm ctxt "corres_case" |
| val xs = Term.add_frees t [] |> filter (fn (s, _) => s = "x'") |
| val xrawvar = case xs of [] => raise TERM ("corres_case_tac: no x'", [t]) |
| | _ => hd xs |
| val x = Thm.cterm_of ctxt (Free xrawvar) |
| val thm = Drule.infer_instantiate ctxt [(("x'", 0), x)] thm (* TODO check 0 is the one we want here! It should be, hopefully. *) |
| val tag_simps = Proof_Context.get_thms ctxt "tag_t_defs" |
| in rtac thm |
| THEN_ALL_NEW (TRY o atac) |
| THEN_ALL_NEW asm_full_simp_tac (ctxt addsimps vr_simps) |
| THEN_ALL_NEW clarsimp_tac ctxt |
| THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (etac @{thm disjE})) |
| THEN_ALL_NEW clarsimp_tac (ctxt addsimps vr_simps addsimps tag_simps) |
| end i) |
| \<close> |
| |
| end |
| |
| end |
