Theory TypeSystemTactics
theory TypeSystemTactics
imports "../Compositionality"
"../TypeSystem"
"HOL-Eisbach.Eisbach_Tools"
begin
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
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)›
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 assign⇩2_tac =
wrap ‹rule assign⇩2›,
simp,
solves ‹rule aexpr; simp›,
(fastforce),
simp,
simp
method assign⇩1_tac =
wrap ‹rule assign⇩1,
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› |
assign⇩1_tac|
assign⇩2_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› |
assign⇩2_tac |
if_tac ‹call_by_name "has_type_tac'"› |
assign⇩1_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