Theory Autoref_Tagging
section ‹Tagging of Terms›
theory Autoref_Tagging
imports "../Lib/Refine_Lib"
begin
text ‹
We provide a mechanism to tag terms, that supports relator annotations,
and introduces tags to protect operations, function applications, and
abstractions from automatic beta and eta conversions.
›
ML ‹
structure Autoref_Tag_Defs = Named_Thms (
val name = @{binding autoref_tag_defs}
val description = "Autoref: Definitions of internal tags"
)
›
setup Autoref_Tag_Defs.setup
text ‹General protection tag›
definition PROTECT where [simp, autoref_tag_defs]: "PROTECT x ≡ x"
text ‹General annotation tag›
typedecl annot
definition ANNOT :: "'a ⇒ annot ⇒ 'a"
where [simp, autoref_tag_defs]: "ANNOT x a ≡ x"
text ‹Operation-tag, Autoref does not look beyond this›
definition OP where [simp, autoref_tag_defs]: "OP x ≡ x"
text ‹Protected function application›
definition APP (infixl "$" 900) where [simp, autoref_tag_defs]: "f$a ≡ f a"
text ‹Protected abstraction›
abbreviation ABS :: "('a⇒'b)⇒'a⇒'b" (binder "λ''" 10)
where "ABS f ≡ PROTECT (λx. PROTECT (f x))"
lemma ABS_beta: "(λ'x. f x)$x ≡ f x" by simp
lemma ABS_eta: "λ'x. (f$x) ≡ f" by simp
text ‹This tag is used to highlight failures during operation
identification›
definition "ID_FAIL x ≡ x"
notation (output) ID_FAIL ("FAIL *** _ ***")
text ‹Relator annotation›
consts rel_annot :: "('c×'a) set ⇒ annot"
abbreviation rel_ANNOT :: "'a ⇒ ('c × 'a) set ⇒ 'a" (infix ":::" 10)
where "t:::R ≡ ANNOT t (rel_annot R)"
lemma rel_ANNOT_eq: "t ≡ t:::R" by simp
text ‹Indirect annotation›
typedecl rel_name
consts ind_annot :: "rel_name ⇒ annot"
abbreviation ind_ANNOT :: "'a ⇒ rel_name ⇒ 'a" (infix "::#" 10)
where "t::#s ≡ ANNOT t (ind_annot s)"
ML ‹
signature AUTOREF_TAGGING = sig
val term_of_tagged: term -> term
val is_valid_tagged: term -> bool
val mk_APP: term -> term -> term
val mk_OP: term -> term
val lambda': string * typ -> term -> term
val list_APP: term * term list -> term
val strip_app: term -> term * term list
val untag_conv: Proof.context -> conv
val mk_APP_conv: conv
val mk_OP_conv: conv
val mk_ABS_conv: Proof.context -> conv
val mk_ANNOT_conv: cterm -> conv
val mk_rel_ANNOT_conv: Proof.context -> cterm -> conv
val ABS_beta_conv: Proof.context -> conv
val rhs_conv: (Proof.context -> conv) -> Proof.context -> conv
end
structure Autoref_Tagging :AUTOREF_TAGGING = struct
fun term_of_tagged (Free v) = Free v
| term_of_tagged (Var v) = Var v
| term_of_tagged (Bound i) = Bound i
| term_of_tagged @{mpat "OP ?t"} = t
| term_of_tagged @{mpat "ANNOT ?t _"} = term_of_tagged t
| term_of_tagged @{mpat "?f$?x"} = term_of_tagged f $ term_of_tagged x
| term_of_tagged @{mpat "PROTECT (λx. PROTECT ?t)"}
= Abs (x,x_T,term_of_tagged t)
| term_of_tagged @{mpat (typs) "PROTECT (PROTECT::?'v_T⇒_)"}
= Abs ("x",T,Bound 0)
| term_of_tagged t = raise TERM ("term_of_tagged",[t])
fun is_valid_tagged (Free _) = true
| is_valid_tagged (Var _) = true
| is_valid_tagged (Bound _) = true
| is_valid_tagged @{mpat "OP _"} = true
| is_valid_tagged @{mpat "ANNOT ?t _"} = is_valid_tagged t
| is_valid_tagged @{mpat "?f$?x"}
= is_valid_tagged f andalso is_valid_tagged x
| is_valid_tagged @{mpat "PROTECT (λ_. PROTECT ?t)"} = is_valid_tagged t
| is_valid_tagged @{mpat "PROTECT PROTECT"} = true
| is_valid_tagged _ = false
fun mk_APP f x = let
val fT = fastype_of f
val xT = fastype_of x
val rT = range_type fT
in
Const (@{const_name APP},fT --> xT --> rT)$f$x
end;
fun mk_OP x = let
val T = fastype_of x
in
Const(@{const_name OP},T-->T)$x
end
fun lambda' (name,T) t = let
val tT = fastype_of t
val t' = Const (@{const_name PROTECT},tT --> tT)$
abstract_over (Free (name,T), t)
val t' =
Const (@{const_name PROTECT},(T --> tT) --> T --> tT)$Abs (name,T,t')
in
t'
end
val list_APP = Library.foldl (uncurry mk_APP)
fun strip_app t = let
fun strip_app_aux @{mpat "?f$?x"} args = strip_app_aux f (x::args)
| strip_app_aux t args = (t,args)
in strip_app_aux t [] end
fun untag_conv ctxt = Raw_Simplifier.rewrite ctxt
true (Autoref_Tag_Defs.get ctxt)
fun ABS_beta_conv ctxt = Raw_Simplifier.rewrite ctxt
true @{thms ABS_beta}
val mk_PROTECT_conv = Conv.rewr_conv @{thm PROTECT_def[symmetric]}
val mk_APP_conv = Conv.rewr_conv @{thm APP_def[symmetric]}
val mk_OP_conv = Conv.rewr_conv @{thm OP_def[symmetric]}
fun mk_ABS_conv ctxt = Conv.abs_conv (K mk_PROTECT_conv) ctxt
then_conv mk_PROTECT_conv
fun mk_ANNOT_conv a ct = let
val Tt = Thm.ctyp_of_cterm ct
val thm = Thm.instantiate' [SOME Tt] [SOME ct,SOME a]
@{thm ANNOT_def[symmetric]}
in
thm
end
fun mk_rel_ANNOT_conv ctxt a ct = let
val T = Thm.typ_of_cterm a
val (Tc,Ta) = HOLogic.dest_setT T
|> HOLogic.dest_prodT
|> apply2 (Thm.ctyp_of ctxt)
val thm = Thm.instantiate' [SOME Ta, SOME Tc] [SOME ct,SOME a]
@{thm rel_ANNOT_eq}
in
thm
end
fun rhs_conv conv ctxt ct = let
open Conv Refine_Util
in
case Logic.strip_imp_concl (Thm.term_of ct) of
@{mpat "Trueprop ((_,_)∈_)"} =>
HOL_concl_conv (fn ctxt => (arg1_conv (arg_conv (conv ctxt)))) ctxt ct
| _ => raise CTERM ("rhs_conv",[ct])
end
end
›
ML_val ‹
Autoref_Tagging.mk_ANNOT_conv @{cterm "bar::annot"} @{cterm "foo::'a::type"};
›
ML_val ‹
Autoref_Tagging.mk_rel_ANNOT_conv @{context}
@{cterm "bar::('c×'a) set"} @{cterm "foo::'a::type"}
›
end