Theory Refine_Monadic.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)"
  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,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)"
  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 (⟨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)"
  by (simp add: RELATES_def)
  
end