# Theory Refine_Heuristics

```section ‹Data Refinement Heuristics›
theory Refine_Heuristics
imports Refine_Basic
begin

text ‹
This theory contains some heuristics to automatically prove
data refinement goals that are left over by the refinement condition
generator.
›

text ‹
The theorem collection ‹refine_hsimp› contains additional simplifier
rules that are useful to discharge typical data refinement goals.
›

ML ‹
structure refine_heuristics_simps = Named_Thms
( val name = @{binding refine_hsimp}
val description = "Refinement Framework: " ^
"Data refinement heuristics simp rules" );
›

setup ‹refine_heuristics_simps.setup›

subsection ‹Type Based Heuristics›
text ‹
This heuristics instantiates schematic data refinement relations based
on their type. Both, the left hand side and right hand side type are
considered.
›

text ‹The heuristics works by proving goals of the form
‹RELATES ?R›, thereby instantiating ‹?R›.›
definition RELATES :: "('a×'b) set ⇒ bool" where "RELATES R ≡ True"
lemma RELATESI: "RELATES R" by (simp add: RELATES_def)

ML ‹
structure Refine_dref_type = struct
structure pattern_rules = Named_Thms
( val name = @{binding refine_dref_pattern}
val description = "Refinement Framework: " ^
"Pattern rules to recognize refinement goal" );

structure RELATES_rules = Named_Thms (
val name = @{binding refine_dref_RELATES}
val description = "Refinement Framework: " ^
"Type based heuristics introduction rules"
);

val tracing =
Attrib.setup_config_bool @{binding refine_dref_tracing} (K false);

(* Check whether term contains schematic variable *)
fun
has_schematic (Var _) = true |
has_schematic (Abs (_,_,t)) = has_schematic t |
has_schematic (t1\$t2) = has_schematic t1 orelse has_schematic t2 |
has_schematic _ = false;

(* Match proof states where the conclusion of some goal has the specified
shape *)
fun match_goal_shape_tac (shape:term->bool) (ctxt:Proof.context) i thm =
if Thm.nprems_of thm >= i then
let
val t = HOLogic.dest_Trueprop (Logic.concl_of_goal (Thm.prop_of thm) i);
in
(if shape t then all_tac thm else no_tac thm)
end
else
no_tac thm;

fun output_failed_msg ctxt failed_t = let
val failed_t_str = Pretty.string_of
(Syntax.pretty_term (Config.put show_types true ctxt) failed_t);
val msg = "Failed to resolve refinement goal \n  " ^ failed_t_str;
val _ = if Config.get ctxt tracing then Output.tracing msg else ();
in () end;

(* Try to apply patternI-rules, ensure that produced first subgoal
contains a schematic variable, and then solve it using
refine_dref_RELATES-rules. *)
fun type_tac ctxt =
ALL_GOALS_FWD (TRY o (
resolve_tac ctxt (pattern_rules.get ctxt) THEN'
match_goal_shape_tac has_schematic ctxt THEN'
(SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt (RELATES_rules.get ctxt)))
ORELSE' (fn i => fn st => let
val failed_t =
HOLogic.dest_Trueprop (Logic.concl_of_goal (Thm.prop_of st) i);
val _ = output_failed_msg ctxt failed_t;
in no_tac st end)
)
));

end;
›

setup ‹Refine_dref_type.RELATES_rules.setup›
setup ‹Refine_dref_type.pattern_rules.setup›

method_setup refine_dref_type =
‹Scan.lift (Args.mode "trace" -- Args.mode "nopost")
>> (fn (tracing,nopost) =>
fn ctxt => (let
val ctxt =
if tracing then Config.put Refine_dref_type.tracing true ctxt else ctxt;
in
SIMPLE_METHOD (CHANGED (
Refine_dref_type.type_tac ctxt
THEN (if nopost then all_tac else ALLGOALS (TRY o Refine.post_tac ctxt))))
end))
›
"Use type-based heuristics to instantiate data refinement relations"

(*method_setup refine_dref_type_only =
{* Scan.succeed (fn ctxt => SIMPLE_METHOD (CHANGED (
Refine_dref_type.type_tac ctxt))) *}
"Use type-based heuristics to instantiate data refinement relations.
No postprocessing."*)

subsection ‹Patterns›
text ‹
This section defines the patterns that are recognized as data refinement
goals.
›

lemma RELATESI_memb[refine_dref_pattern]:
"RELATES R ⟹ (a,b)∈R ⟹ (a,b)∈R" .
lemma RELATESI_refspec[refine_dref_pattern]:
"RELATES R ⟹ S ≤⇓R S' ⟹ S ≤⇓R S'" .

text ‹Allows refine-rules to add ‹RELATES› goals if they introduce hidden relations›
lemma RELATES_pattern[refine_dref_pattern]: "RELATES R ⟹ RELATES R" .
lemmas [refine_hsimp] = RELATES_def

subsection ‹Refinement Relations›
text ‹
In this section, we define some general purpose refinement relations, e.g.,
for product types and sets.
›

lemma Id_RELATES [refine_dref_RELATES]: "RELATES Id" by (simp add: RELATES_def)

lemma prod_rel_RELATES[refine_dref_RELATES]:
"RELATES Ra ⟹ RELATES Rb ⟹ RELATES (⟨Ra,Rb⟩prod_rel)"

declare prod_rel_sv[refine_hsimp]
lemma prod_rel_iff[refine_hsimp]:
"((a,b),(a',b'))∈⟨A,B⟩prod_rel ⟷ (a,a')∈A ∧ (b,b')∈B"
by (auto simp: prod_rel_def)

lemmas [refine_hsimp] = prod_rel_id_simp

lemma option_rel_RELATES[refine_dref_RELATES]:
"RELATES Ra ⟹ RELATES (⟨Ra⟩option_rel)"

declare option_rel_sv[refine_hsimp]

lemmas [refine_hsimp] = option_rel_id_simp

lemmas [refine_hsimp] = set_rel_sv set_rel_csv

lemma set_rel_RELATES[refine_dref_RELATES]:
"RELATES R ⟹ RELATES (⟨R⟩set_rel)" by (simp add: RELATES_def)

lemma set_rel_empty_eq: "(S,S')∈⟨X⟩set_rel ⟹ S={} ⟷ S'={}"
by (auto simp: set_rel_def)

lemma set_rel_sngD: "({a},{b})∈⟨R⟩set_rel ⟹ (a,b)∈R"
by (auto simp: set_rel_def)

(*lemmas [refine_hsimp] = set_rel_empty set_rel_union set_rel_insert
set_rel_diff*)

(*lemmas [refine_hsimp] = prod_set_eq_is_Id*)

lemma Image_insert[refine_hsimp]:
"(a,b)∈R ⟹ single_valued R ⟹ R``insert a A = insert b (R``A)"
by (auto dest: single_valuedD)

lemmas [refine_hsimp] = Image_Un

lemma Image_Diff[refine_hsimp]:
"single_valued (converse R) ⟹ R``(A-B) = R``A - R``B"
by (auto dest: single_valuedD)

lemma Image_Inter[refine_hsimp]:
"single_valued (converse R) ⟹ R``(A∩B) = R``A ∩ R``B"
by (auto dest: single_valuedD)

lemma list_rel_RELATES[refine_dref_RELATES]:
"RELATES R ⟹ RELATES (⟨R⟩list_rel)" by (simp add: RELATES_def)

lemmas [refine_hsimp] = list_rel_sv_iff list_rel_simp

lemma RELATES_nres_rel[refine_dref_RELATES]: "RELATES R ⟹ RELATES (⟨R⟩nres_rel)"