Theory Refine_Heuristics

section ‹Data Refinement Heuristics›
theory Refine_Heuristics
imports Refine_Basic

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

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

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 *)
    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
        val t = HOLogic.dest_Trueprop (Logic.concl_of_goal (Thm.prop_of thm) i);
        (if shape t then all_tac thm else no_tac thm)
      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 =
      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)


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; 
        Refine_dref_type.type_tac ctxt 
        THEN (if nopost then all_tac else ALLGOALS (TRY o Refine.post_tac ctxt))))
  "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 

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,Rbprod_rel)"
  by (simp add: RELATES_def prod_rel_def)

declare prod_rel_sv[refine_hsimp]
lemma prod_rel_iff[refine_hsimp]: 
  "((a,b),(a',b'))A,Bprod_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 (Raoption_rel)"
  by (simp add: RELATES_def option_rel_def)

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 (Rset_rel)" by (simp add: RELATES_def)

lemma set_rel_empty_eq: "(S,S')Xset_rel  S={}  S'={}"
  by (auto simp: set_rel_def)

lemma set_rel_sngD: "({a},{b})Rset_rel  (a,b)R"
  by (auto simp: set_rel_def)

(*lemmas [refine_hsimp] = set_rel_empty set_rel_union set_rel_insert

(*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``(AB) = R``A  R``B"
  by (auto dest: single_valuedD)

lemma list_rel_RELATES[refine_dref_RELATES]: 
  "RELATES R  RELATES (Rlist_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 (Rnres_rel)"
  by (simp add: RELATES_def)