Theory TypeSystemTactics

theory TypeSystemTactics
imports "../Compositionality"
        "../TypeSystem"
        "HOL-Eisbach.Eisbach_Tools"
begin

(* Some Eisbach magic to get around Eisbach and locales not getting along *)

ML structure Data = Proof_Data
(
  type T = morphism
  fun init _ = Morphism.identity;
);

method_setup wrap = 
  Method.text_closure >> (fn text => fn ctxt =>
    let
      val morph = Data.get ctxt;

      fun safe_fact thms =
        perhaps (try (Morphism.fact morph)) thms;
       
      val morph' = Morphism.morphism "safe" 
        {binding = [K (Morphism.binding morph)],
         fact = [K safe_fact],
         term = [K (Morphism.term morph)],
         typ = [K (Morphism.typ morph)]}
      
      val text' = Method.map_source (map (Token.transform morph')) text;
    in Method.evaluate_runtime text' ctxt end)

method_setup print_headgoal = 
  Scan.succeed (fn ctxt =>
  SIMPLE_METHOD
    (SUBGOAL (fn (t,_) => 
    (Output.writeln 
    (Pretty.string_of (Syntax.pretty_term ctxt t)); all_tac)) 1))

named_theorems aexpr and bexpr and prog and custom_if
context sifum_types_assign
begin

(* More Eisbach magic to get around Eisbach and mutual recursion not getting along *)

method_setup call_by_name = Scan.lift Parse.string >> 
  (fn str => fn ctxt => 
    case (try (Method.check_src ctxt) (Token.make_src (str, Position.none) [])) of
    SOME src => Method.evaluate (Method.Source src) ctxt
    | _ => Method.fail)

(* Eisbach tactics for partially automating has_type proofs *)

method seq_tac 
  methods tac = 
  (wrap rule seq_type, tac, tac) 

method anno_tac 
  methods tac = 
  (wrap rule anno_type[OF HOL.refl HOL.refl HOL.refl], 
         clarsimp, 
        tac, 
       simp, 
      fastforce simp: add_anno_def subtype_def pred_entailment_def 
                      pred_def bot_Sec_def[symmetric],
     simp add: add_anno_def,
    simp) 


method assign2_tac =
     wrap rule assign2, 
        simp, 
       solves rule aexpr; simp, 
      (fastforce),
     simp,
    simp


method assign1_tac =
   wrap rule assign1,
        simp,
       simp,
      solves rule aexpr;  simp,
      simp,
     clarsimp simp: subtype_def pred_def,
    simp

method assign𝒞_tac =
   wrap rule assign𝒞,
        simp,
       solves rule aexpr; simp, 
       (solves simp), 
      (solves simp | (clarsimp, fast)),
     (solves simp)?,
    simp

method if_tac 
  methods tac = 
  wrap rule if_type', 
        solves rule bexpr, simp, 
       solves simp,
      solves tac, 
     solves tac, 
    solves clarsimp, fastforce

method has_type_no_if_tac' 
  declares aexpr bexpr= 
 (seq_tac call_by_name "has_type_no_if_tac'" |
   anno_tac call_by_name "has_type_no_if_tac'" |
   wrap rule skip_type | 
   wrap rule stop_type |
   assign1_tac| 
   assign2_tac | 
   assign𝒞_tac)?

method has_type_no_if_tac
  uses prog 
  declares aexpr bexpr = 
  (intro exI, unfold prog, has_type_no_if_tac')

method has_type_tac'
  declares aexpr bexpr= 
  (seq_tac call_by_name "has_type_tac'" |
   anno_tac call_by_name "has_type_tac'" |
   wrap rule skip_type | 
   wrap rule stop_type |
   assign2_tac |
   if_tac call_by_name "has_type_tac'" | 
   assign1_tac | 
   assign𝒞_tac)?




method has_type_tac uses prog declares aexpr bexpr = 
  (intro exI, unfold prog, has_type_tac')


method if_type_tac 
  declares bexpr custom_if =
   (wrap rule custom_if, 
            rule bexpr, 
           simp?, 
          simp?,
         has_type_tac', 
        has_type_tac', 
       (* 
        Check if this work for other cases? 
        If so just give the rest of this method a time out.
        Otherwise, remove from tac and add as explicit lemma proof *)
        (clarsimp simp: context_equiv_def type_equiv_def subtype_def)?,
       (clarsimp simp: context_equiv_def type_equiv_def subtype_def)?,
      (simp add: subset_entailment)?,
     (simp add: subset_entailment)?,
    (clarsimp,
    (subst tyenv_wellformed_def) ,
    (clarsimp simp: mds_consistent_def types_wellformed_def type_wellformed_def types_stable_def),
    (fastforce simp: tyenv_wellformed_def mds_consistent_def))?,
   (clarsimp,
   (subst tyenv_wellformed_def) ,
   (clarsimp simp: mds_consistent_def types_wellformed_def type_wellformed_def types_stable_def),
   (fastforce simp: tyenv_wellformed_def mds_consistent_def))?)


declaration fn phi => Context.mapping I (Data.put phi)


end

end