Theory Refine_Util
section "General Utilities"
theory Refine_Util
imports Refine_Util_Bootstrap1 Mpat_Antiquot Mk_Term_Antiquot
begin
definition conv_tag where "conv_tag n x == x"
lemma shift_lambda_left: "(f ≡ λx. g x) ⟹ (⋀x. f x ≡ g x)" by simp
ML ‹
infix 0 THEN_ELSE' THEN_ELSE_COMB'
infix 1 THEN_ALL_NEW_FWD THEN_INTERVAL
infix 2 ORELSE_INTERVAL
infix 3 ->>
signature BASIC_REFINE_UTIL = sig
include BASIC_REFINE_UTIL
val RSm: Proof.context -> thm -> thm -> thm
val is_Abs: term -> bool
val is_Comb: term -> bool
val has_Var: term -> bool
val is_TFree: typ -> bool
val is_def_thm: thm -> bool
type tactic' = int -> tactic
type itactic = int -> int -> tactic
val IF_EXGOAL: (int -> tactic) -> tactic'
val COND': (term -> bool) -> tactic'
val CONCL_COND': (term -> bool) -> tactic'
val THEN_ELSE': tactic' * (tactic' * tactic') -> tactic'
val THEN_ELSE_COMB':
tactic' * ((tactic'*tactic'->tactic') * tactic' * tactic') -> tactic'
val INTERVAL_FWD: tactic' -> int -> int -> tactic
val THEN_ALL_NEW_FWD: tactic' * tactic' -> tactic'
val REPEAT_ALL_NEW_FWD: tactic' -> tactic'
val REPEAT_DETERM': tactic' -> tactic'
val REPEAT': tactic' -> tactic'
val ALL_GOALS_FWD': tactic' -> tactic'
val ALL_GOALS_FWD: tactic' -> tactic
val APPEND_LIST': tactic' list -> tactic'
val SINGLE_INTERVAL: itactic -> tactic'
val THEN_INTERVAL: itactic * itactic -> itactic
val ORELSE_INTERVAL: itactic * itactic -> itactic
val CAN': tactic' -> tactic'
val NTIMES': tactic' -> int -> tactic'
val TRY_SOLVED': tactic' -> tactic'
val CASES': (tactic' * tactic) list -> tactic'
val WITH_subgoal: (term -> tactic') -> tactic'
val WITH_concl: Proof.context -> (term -> tactic') -> tactic'
val TRADE: (Proof.context -> tactic') -> Proof.context -> tactic'
val fo_rtac: thm -> Proof.context -> tactic'
val fo_resolve_tac: thm list -> Proof.context -> tactic'
val rprems_tac: Proof.context -> tactic'
val rprem_tac: int -> Proof.context -> tactic'
val elim_all_tac: Proof.context -> thm list -> tactic
val prefer_tac: int -> tactic
val insert_subgoal_tac: cterm -> tactic'
val insert_subgoals_tac: cterm list -> tactic'
val eqsubst_inst_tac: Proof.context -> bool -> int list
-> ((indexname * Position.T) * string) list -> thm -> int -> tactic
val eqsubst_inst_meth: (Proof.context -> Proof.method) context_parser
val ->> : 'a context_parser *('a * Context.generic -> 'b * Context.generic)
-> 'b context_parser
end
signature REFINE_UTIL = sig
include BASIC_REFINE_UTIL
val order_by: ('a * 'a -> order) -> ('b -> 'a) -> 'b list -> 'b list
val build_res_net: thm list -> (int * thm) Net.net
val fo_matchp: theory -> cterm -> term -> term list option
val fo_matches: theory -> cterm -> term -> bool
val anorm_typ: typ -> typ
val anorm_term: term -> term
val import_cterms: bool -> cterm list -> Proof.context ->
cterm list * Proof.context
val subsume_sort: ('a -> term) -> theory -> 'a list -> 'a list
val subsume_sort_gen: ('a -> term) -> Context.generic
-> 'a list -> 'a list
val mk_compN1: typ list -> int -> term -> term -> term
val mk_compN: int -> term -> term -> term
val dest_itselfT: typ -> typ
val dummify_tvars: term -> term
val shift_lambda_left: thm -> thm
val shift_lambda_leftN: int -> thm -> thm
val list_binop_left: 'a -> ('a * 'a -> 'a) -> 'a list -> 'a
val fold_binop_left: ('c -> 'b * 'c) -> ('a -> 'c -> 'b * 'c) -> ('b * 'b -> 'b)
-> 'a list -> 'c -> 'b * 'c
val strip_prodT_left: typ -> typ list
val list_prodT_left: typ list -> typ
val mk_ltuple: term list -> term
val fix_left_tuple_from_Ts: string -> typ list -> Proof.context -> term * Proof.context
val lambda_tuple: term list -> term -> term
val instantiate_tuples: Proof.context -> (indexname*typ) list -> thm -> thm
val instantiate_tuples_from_term_tac: Proof.context -> term -> tactic
val instantiate_tuples_subgoal_tac: Proof.context -> tactic'
val abs_def: Proof.context -> thm -> thm
val repeat_rule: (thm -> thm) -> thm -> thm
val changed_rule: (thm -> thm) -> thm -> thm
val try_rule: (thm -> thm) -> thm -> thm
val trade_rule: (Proof.context -> thm -> thm) -> Proof.context -> thm -> thm
val RS_fst: thm -> thm list -> thm
val OF_fst: thm list -> thm list -> thm
val trace_conv: conv
val monitor_conv: string -> conv -> conv
val monitor_conv': string -> (Proof.context -> conv) -> Proof.context -> conv
val fixup_vars: cterm -> thm -> thm
val fixup_vars_conv: conv -> conv
val fixup_vars_conv': (Proof.context -> conv) -> Proof.context -> conv
val pat_conv': cterm -> (string -> Proof.context -> conv) -> Proof.context
-> conv
val pat_conv: cterm -> (Proof.context -> conv) -> Proof.context -> conv
val HOL_concl_conv: (Proof.context -> conv) -> Proof.context -> conv
val import_conv: (Proof.context -> conv) -> Proof.context -> conv
val fix_conv: Proof.context -> conv -> conv
val ite_conv: conv -> conv -> conv -> conv
val cfg_trace_f_tac_conv: bool Config.T
val f_tac_conv: Proof.context -> (term -> term) -> (Proof.context -> tactic) -> conv
val fcomb_conv: conv -> conv
val fsub_conv: (Proof.context -> conv) -> Proof.context -> conv
val ftop_conv: (Proof.context -> conv) -> Proof.context -> conv
val parse_bool_config: string -> bool Config.T -> bool context_parser
val parse_paren_list: 'a context_parser -> 'a list context_parser
val parse_paren_lists: 'a context_parser -> 'a list list context_parser
val parse_bool_config': string -> bool Config.T -> Token.T list -> (bool Config.T * bool) * Token.T list
val parse_paren_list': 'a parser -> Token.T list -> 'a list * Token.T list
val apply_configs: ('a Config.T * 'a) list -> Proof.context -> Proof.context
end
structure Refine_Util: REFINE_UTIL = struct
open Basic_Refine_Util
fun RSm ctxt thA thB = let
val (thA, ctxt') = ctxt
|> Variable.declare_thm thA
|> Variable.declare_thm thB
|> yield_singleton (apfst snd oo Variable.import true) thA
val thm = thA RS thB
val thm = singleton (Variable.export ctxt' ctxt) thm
|> Drule.zero_var_indexes
in
thm
end
fun is_Abs (Abs _) = true | is_Abs _ = false
fun is_Comb (_$_) = true | is_Comb _ = false
fun has_Var (Var _) = true
| has_Var (Abs (_,_,t)) = has_Var t
| has_Var (t1$t2) = has_Var t1 orelse has_Var t2
| has_Var _ = false
fun is_TFree (TFree _) = true
| is_TFree _ = false
fun is_def_thm thm = case thm |> Thm.prop_of of
Const (@{const_name "Pure.eq"},_)$_$_ => true | _ => false
type tactic' = int -> tactic
type itactic = int -> int -> tactic
fun IF_EXGOAL tac i st = if i <= Thm.nprems_of st then
tac i st
else no_tac st;
fun COND' P = IF_EXGOAL (fn i => fn st =>
(if P (Thm.prop_of st |> curry Logic.nth_prem i) then
all_tac st else no_tac st)
handle TERM _ => no_tac st
| Pattern.MATCH => no_tac st
)
fun CONCL_COND' P = COND' (strip_all_body #> Logic.strip_imp_concl #> P)
fun (tac1 THEN_ELSE' (tac2,tac3)) x = tac1 x THEN_ELSE (tac2 x,tac3 x);
fun (tac1 THEN_ELSE_COMB' (comb,tac2,tac_else)) i st = let
val rseq = tac1 i st
in
case seq_is_empty rseq of
(true,_) => tac_else i st
| (false,rseq) => comb (K(K( rseq )), tac2) i st
end
fun INTERVAL_FWD tac l u st =
if l>u then all_tac st
else (tac l THEN (fn st' => let
val ofs = Thm.nprems_of st' - Thm.nprems_of st;
in
if ofs < ~1 then raise THM (
"INTERVAL_FWD: Tac solved more than one goal",~1,[st,st'])
else INTERVAL_FWD tac (l+1+ofs) (u+ofs) st'
end)) st;
fun (tac1 THEN_ALL_NEW_FWD tac2) i st =
(tac1 i
THEN (fn st' => INTERVAL_FWD tac2 i (i + Thm.nprems_of st' - Thm.nprems_of st) st')
) st;
fun REPEAT_ALL_NEW_FWD tac =
tac THEN_ALL_NEW_FWD (TRY o (fn i => REPEAT_ALL_NEW_FWD tac i));
fun REPEAT_DETERM' tac i st = let
val n = Thm.nprems_of st
in
REPEAT_DETERM (COND (has_fewer_prems n) no_tac (tac i)) st
end
fun REPEAT' tac i st = let
val n = Thm.nprems_of st
in
REPEAT (COND (has_fewer_prems n) no_tac (tac i)) st
end
fun ALL_GOALS_FWD' tac i st =
(tac i THEN (fn st' =>
let
val i' = i + Thm.nprems_of st' + 1 - Thm.nprems_of st;
in
if i' <= Thm.nprems_of st' then
ALL_GOALS_FWD' tac i' st'
else
all_tac st'
end
)) st;
fun ALL_GOALS_FWD tac = ALL_GOALS_FWD' tac 1;
fun APPEND_LIST' tacs = fold_rev (curry (op APPEND')) tacs (K no_tac);
fun SINGLE_INTERVAL tac i = tac i i
fun ((tac1:itactic) THEN_INTERVAL (tac2:itactic)) =
(fn i => fn j => fn st =>
( tac1 i j
THEN (fn st' => tac2 i (j + Thm.nprems_of st' - Thm.nprems_of st) st')
) st
):itactic
fun tac1 ORELSE_INTERVAL tac2 = (fn i => fn j => tac1 i j ORELSE tac2 i j)
fun CAN' tac i st =
case tac i st |> Seq.pull of
NONE => Seq.empty
| SOME _ => Seq.single st
fun NTIMES' _ 0 _ st = Seq.single st
| NTIMES' tac n i st = (tac THEN' NTIMES' tac (n-1)) i st
fun fo_rtac thm = Subgoal.FOCUS (fn {context = ctxt, concl, ...} =>
let
val concl_pat = Drule.strip_imp_concl (Thm.cprop_of thm)
val insts = Thm.first_order_match (concl_pat, concl)
in
resolve_tac ctxt [Drule.instantiate_normalize insts thm] 1
end handle Pattern.MATCH => no_tac )
fun fo_resolve_tac thms ctxt =
FIRST' (map (fn thm => fo_rtac thm ctxt) thms);
fun rprems_tac ctxt = Goal.norm_hhf_tac ctxt THEN' CSUBGOAL (fn (goal, i) =>
let
fun non_atomic (Const (@{const_name Pure.imp}, _) $ _ $ _) = true
| non_atomic (Const (@{const_name Pure.all}, _) $ _) = true
| non_atomic _ = false;
val ((_, goal'), ctxt') = Variable.focus_cterm NONE goal ctxt;
val goal'' = Drule.cterm_rule
(singleton (Variable.export ctxt' ctxt)) goal';
val Rs = filter (non_atomic o Thm.term_of)
(Drule.strip_imp_prems goal'');
val ethms = Rs |> map (fn R =>
(Simplifier.norm_hhf ctxt (Thm.trivial R)));
in eresolve_tac ctxt ethms i end
);
fun rprem_tac n ctxt = Goal.norm_hhf_tac ctxt THEN' CSUBGOAL (fn (goal, i) =>
let
val ((_, goal'), ctxt') = Variable.focus_cterm NONE goal ctxt;
val goal'' = Drule.cterm_rule
(singleton (Variable.export ctxt' ctxt)) goal';
val R = nth (Drule.strip_imp_prems goal'') (n - 1)
val rl = Simplifier.norm_hhf ctxt (Thm.trivial R)
in
eresolve_tac ctxt [rl] i
end
);
fun elim_all_tac ctxt thms = ALLGOALS (REPEAT_ALL_NEW (ematch_tac ctxt thms))
fun prefer_tac i = defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1)
fun order_by ord f = sort (ord o apply2 f)
local
fun insert_krl (krl as (_,th)) =
Net.insert_term (K false) (Thm.concl_of th, krl);
in
fun build_res_net rls =
fold_rev insert_krl (tag_list 1 rls) Net.empty;
end
fun insert_subgoals_tac cts i = PRIMITIVE (
Thm.permute_prems 0 (i - 1)
#> fold_rev Thm.implies_intr cts
#> Thm.permute_prems 0 (~i + 1)
)
fun insert_subgoal_tac ct i = insert_subgoals_tac [ct] i
local
fun eqsubst_tac' ctxt asm =
if asm then EqSubst.eqsubst_asm_tac ctxt else EqSubst.eqsubst_tac ctxt
fun subst_method inst_tac tac =
Args.goal_spec --
Scan.lift (Args.mode "asm" -- Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
Scan.optional (Scan.lift
(Parse.and_list1
(Parse.position Args.var -- (Args.$$$ "=" |-- Parse.!!! Parse.embedded_inner_syntax)) --|
Args.$$$ "in")) [] --
Attrib.thms >>
(fn (((quant, (asm, occL)), insts), thms) => fn ctxt => METHOD
(fn facts =>
if null insts then
quant (Method.insert_tac ctxt facts THEN' tac ctxt asm occL thms)
else
(case thms of
[thm] => quant (
Method.insert_tac ctxt facts THEN' inst_tac ctxt asm occL insts thm)
| _ => error "Cannot have instantiations with multiple rules")));
in
fun eqsubst_inst_tac ctxt asm occL insts thm =
Subgoal.FOCUS (
fn {context=ctxt,...} => let
val ctxt' = ctxt |> Proof_Context.set_mode Proof_Context.mode_schematic
val thm' = thm |> Rule_Insts.read_instantiate ctxt' insts []
in eqsubst_tac' ctxt asm occL [thm'] 1 end
) ctxt
val eqsubst_inst_meth = subst_method eqsubst_inst_tac eqsubst_tac'
end
fun fo_matchp thy cpat t = let
fun ignore (Var ((name,_),_)) = String.isPrefix "_" name
| ignore _ = true;
val pat = Thm.term_of cpat;
val pvars = fold_aterms (
fn t => fn l => if is_Var t andalso not (ignore t)
then t::l else l
) pat [] |> rev
val inst = Pattern.first_order_match thy (pat,t)
(Vartab.empty,Vartab.empty);
in SOME (map (Envir.subst_term inst) pvars) end
handle Pattern.MATCH => NONE;
val fo_matches = is_some ooo fo_matchp
fun anorm_typ ty = let
val instT = Term.add_tvarsT ty []
|> map_index (fn (i,(n,s)) => (n,TVar (("t"^string_of_int i,0),s)))
val ty = Term.typ_subst_TVars instT ty;
in ty end;
fun anorm_term t = let
val instT = Term.add_tvars t []
|> map_index (fn (i,(n,s)) => (n,TVar (("t"^string_of_int i,0),s)))
val t = Term.subst_TVars instT t;
val inst = Term.add_vars t []
|> map_index (fn (i,(n,s)) => (n,Var (("v"^string_of_int i,0),s)))
val t = Term.subst_Vars inst t;
in t end;
fun import_cterms is_open cts ctxt = let
val ts = map Thm.term_of cts
val (ts', ctxt') = Variable.import_terms is_open ts ctxt
val cts' = map (Thm.cterm_of ctxt) ts'
in (cts', ctxt') end
fun subsume_sort f thy items = let
val rhss = map (Envir.beta_eta_contract o f) items
fun freqf thy net rhs = Net.match_term net rhs
|> filter (fn p => Pattern.matches thy (p,rhs))
|> length
val net = fold
(fn rhs => Net.insert_term_safe (op =) (rhs,rhs)) rhss Net.empty
val freqs = map (freqf thy net) rhss
val res = freqs ~~ items
|> sort (rev_order o int_ord o apply2 fst)
|> map snd
in res end
fun subsume_sort_gen f = subsume_sort f o Context.theory_of
fun mk_comp1 env (f, g) =
let
val fT = fastype_of1 (env, f);
val gT = fastype_of1 (env, g);
val compT = fT --> gT --> domain_type gT --> range_type fT;
in Const ("Fun.comp", compT) $ f $ g end;
fun mk_compN1 _ 0 f g = f$g
| mk_compN1 env 1 f g = mk_comp1 env (f, g)
| mk_compN1 env n f g = let
val T = fastype_of1 (env, g) |> domain_type
val g = incr_boundvars 1 g $ Bound 0
val env = T::env
in
Abs ("x"^string_of_int n,T,mk_compN1 env (n-1) f g)
end
val mk_compN = mk_compN1 []
fun abs_def ctxt = Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def
fun trace_conv ct = (tracing (@{make_string} ct); Conv.all_conv ct);
fun monitor_conv msg conv ct = let
val _ = tracing (msg ^ " (gets): " ^ @{make_string} ct);
val res = \<^try>‹conv ct
catch exc =>
(tracing (msg ^ " (raises): " ^ @{make_string} exc);
Exn.reraise exc)›
val _ = tracing (msg ^ " (yields): " ^ @{make_string} res);
in res end
fun monitor_conv' msg conv ctxt ct = monitor_conv msg (conv ctxt) ct
fun fixup_vars ct thm = let
val lhs = Thm.lhs_of thm
val inst = Thm.first_order_match (lhs,ct)
val thm' = Thm.instantiate inst thm
in thm' end
fun fixup_vars_conv conv ct = fixup_vars ct (conv ct)
fun fixup_vars_conv' conv ctxt = fixup_vars_conv (conv ctxt)
local
fun tag_ct ctxt name ct = let
val t = Thm.term_of ct;
val ty = fastype_of t;
val t' = Const (@{const_name conv_tag},@{typ unit}-->ty-->ty)
$Free (name,@{typ unit})$t;
val ct' = Thm.cterm_of ctxt t';
in ct' end
fun mpat_conv pat ctxt ct = let
val (tym,tm) = Thm.first_order_match (pat,ct);
val tm' = Vars.map (fn ((name, _), _) => tag_ct ctxt name) tm;
val ct' = Thm.instantiate_cterm (tym, tm') pat;
val goal = Logic.mk_equals (apply2 Thm.term_of (ct, ct'))
val goal_ctxt = Variable.declare_term goal ctxt
val rthm =
Goal.prove_internal goal_ctxt [] (Thm.cterm_of ctxt goal)
(K (simp_tac (put_simpset HOL_basic_ss goal_ctxt addsimps @{thms conv_tag_def}) 1))
|> Goal.norm_result ctxt
in
fixup_vars ct rthm
end handle Pattern.MATCH
=> raise (CTERM ("mpat_conv: No match",[pat,ct]));
fun tag_conv cnv ctxt ct = case Thm.term_of ct of
Const (@{const_name conv_tag},_)$Free(name,_)$_ => (
(Conv.rewr_conv (@{thm conv_tag_def}) then_conv (cnv name) ctxt) ct)
| _ => Conv.all_conv ct;
fun all_tag_conv cnv = Conv.bottom_conv (tag_conv cnv);
in
fun pat_conv' cpat cnv ctxt =
mpat_conv cpat ctxt
then_conv (all_tag_conv cnv ctxt);
fun pat_conv cpat conv = pat_conv' cpat
(fn name => case name of "HOLE" => conv | _ => K Conv.all_conv);
end
fun HOL_concl_conv cnv = Conv.params_conv ~1
(fn ctxt => Conv.concl_conv ~1 (
HOLogic.Trueprop_conv (cnv ctxt)));
fun import_conv conv ctxt ct = let
val (ct',ctxt') = yield_singleton (import_cterms true) ct ctxt
val res = conv ctxt' ct'
val res' = singleton (Variable.export ctxt' ctxt) res |> fixup_vars ct
in res' end
fun fix_conv ctxt conv ct = let
val thm = conv ct
val eq = Logic.mk_equals (Thm.term_of ct, Thm.term_of ct) |> head_of
in if (Thm.term_of (Thm.lhs_of thm) aconv Thm.term_of ct)
then thm
else thm RS Thm.trivial (Thm.mk_binop (Thm.cterm_of ctxt eq) ct (Thm.rhs_of thm))
end
fun ite_conv cv cv1 cv2 ct =
let
val eq1 = SOME (cv ct)
handle THM _ => NONE
| CTERM _ => NONE
| TERM _ => NONE
| TYPE _ => NONE;
val res = case eq1 of
NONE => cv2 ct
| SOME eq1 => let val eq2 = cv1 (Thm.rhs_of eq1) in
if Thm.is_reflexive eq1 then eq2
else if Thm.is_reflexive eq2 then eq1
else Thm.transitive eq1 eq2
end
in res end
val cfg_trace_f_tac_conv =
Attrib.setup_config_bool @{binding trace_f_tac_conv} (K false)
fun f_tac_conv ctxt f tac ct = let
val t = Thm.term_of ct
val t' = f t
val goal = Logic.mk_equals (t,t')
val _ = if Config.get ctxt cfg_trace_f_tac_conv then
tracing (Syntax.string_of_term ctxt goal)
else ()
val goal_ctxt = Variable.declare_term goal ctxt
val thm = Goal.prove_internal ctxt [] (Thm.cterm_of ctxt goal) (K (tac goal_ctxt))
in
thm
end
fun (p->>f) ctks = let
val (res,(context,tks)) = p ctks
val (res,context) = f (res, context)
in
(res,(context,tks))
end
fun parse_bool_config name cfg = (
Scan.lift (Args.$$$ name)
->> (apsnd (Config.put_generic cfg true) #>> K true)
||
Scan.lift (Args.$$$ ("no_"^name))
->> (apsnd (Config.put_generic cfg false) #>> K false)
)
fun parse_paren_list p =
Scan.lift (
Args.$$$ "(") |-- Parse.enum1' "," p --| Scan.lift (Args.$$$ ")"
)
fun parse_paren_lists p = Scan.repeat (parse_paren_list p)
val _ = Theory.setup
(Method.setup @{binding fo_rule}
(Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' (
fo_resolve_tac thms ctxt)))
"resolve using first-order matching"
#>
Method.setup @{binding rprems}
(Scan.lift (Scan.option Parse.nat) >> (fn i => fn ctxt =>
SIMPLE_METHOD' (
case i of
NONE => rprems_tac ctxt
| SOME i => rprem_tac i ctxt
))
)
"resolve with premises"
#> Method.setup @{binding elim_all}
(Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (elim_all_tac ctxt thms)))
"repeteadly apply elimination rules to all subgoals"
#> Method.setup @{binding subst_tac} eqsubst_inst_meth
"single-step substitution (dynamic instantiation)"
#> Method.setup @{binding clarsimp_all} (
Method.sections Clasimp.clasimp_modifiers >> K (fn ctxt => SIMPLE_METHOD (
CHANGED_PROP (ALLGOALS (Clasimp.clarsimp_tac ctxt))))
) "simplify and clarify all subgoals")
fun TRY_SOLVED' tac i st = let
val res = tac i st
val solved = Seq.filter (fn st' => Thm.nprems_of st' < Thm.nprems_of st) res
in
case Seq.pull solved of
SOME _ => solved
| NONE => res
end
local
fun CASES_aux [] = no_tac
| CASES_aux ((tac1, tac2)::cs) = tac1 1 THEN_ELSE (tac2, CASES_aux cs)
in
val CASES' = SELECT_GOAL o CASES_aux
end
fun WITH_subgoal tac =
CONVERSION Thm.eta_conversion THEN'
IF_EXGOAL (fn i => fn st => tac (nth (Thm.prems_of st) (i - 1)) i st)
fun WITH_concl ctxt tac =
CONVERSION Thm.eta_conversion THEN'
IF_EXGOAL (fn i => fn st =>
tac (Logic.concl_of_goal (Thm.prop_of st) i) i st
)
fun TRADE tac ctxt i st = let
val orig_ctxt = ctxt
val (st,ctxt) = yield_singleton (apfst snd oo Variable.import true) st ctxt
val seq = tac ctxt i st
|> Seq.map (singleton (Variable.export ctxt orig_ctxt))
in
seq
end
fun fcomb_conv conv = let open Conv in
arg_conv conv else_conv fun_conv conv
end
fun fsub_conv conv ctxt = let
open Conv
in
fcomb_conv (conv ctxt) else_conv
abs_conv (conv o snd) ctxt else_conv
no_conv
end
fun ftop_conv conv ctxt ct =
(conv ctxt else_conv fsub_conv (ftop_conv conv) ctxt) ct
fun repeat_rule n thm = case try n thm of
SOME thm => repeat_rule n thm
| NONE => thm
fun changed_rule n thm = let
val thm' = n thm
in
if Thm.eq_thm_prop (thm, thm') then raise THM ("Same",~1,[thm,thm'])
else thm'
end
fun try_rule n thm = case try n thm of
SOME thm => thm | NONE => thm
fun trade_rule f ctxt thm =
singleton (Variable.trade (map o f) ctxt) thm
fun RS_fst thm thms = let
fun r [] = raise THM ("RS_fst, no matches",~1,thm::thms)
| r (thm'::thms) = case try (op RS) (thm,thm') of
NONE => r thms | SOME thm => thm
in
r thms
end
fun OF_fst thms insts = let
fun r [] = raise THM ("OF_fst, no matches",length thms,thms@insts)
| r (thm::thms) = case try (op OF) (thm,insts) of
NONE => r thms | SOME thm => thm
in
r thms
end
fun list_binop_left z f = let
fun r [] = z
| r [T] = T
| r (T::Ts) = f (r Ts,T)
in
fn l => r (rev l)
end
fun fold_binop_left z i f = let
fun r [] ctxt = z ctxt
| r [T] ctxt = i T ctxt
| r (T::Ts) ctxt = let
val (Ti,ctxt) = i T ctxt
val (Tsi,ctxt) = r Ts ctxt
in
(f (Tsi,Ti),ctxt)
end
in
fn l => fn ctxt => r (rev l) ctxt
end
fun strip_prodT_left (Type (@{type_name Product_Type.prod},[A,B])) = strip_prodT_left A @ [B]
| strip_prodT_left (Type (@{type_name Product_Type.unit},[])) = []
| strip_prodT_left T = [T]
val list_prodT_left = list_binop_left HOLogic.unitT HOLogic.mk_prodT
val mk_ltuple = list_binop_left HOLogic.unit HOLogic.mk_prod
fun fix_left_tuple_from_Ts name = fold_binop_left
(fn ctxt => (@{term "()"},ctxt))
(fn T => fn ctxt => let
val (x,ctxt) = yield_singleton Variable.variant_fixes name ctxt
val x = Free (x,T)
in
(x,ctxt)
end)
HOLogic.mk_prod
val dummify_tvars = map_types (map_type_tvar (K dummyT))
fun dest_itselfT (Type (@{type_name itself},[A])) = A
| dest_itselfT T = raise TYPE("dest_itselfT",[T],[])
fun shift_lambda_left thm = thm RS @{thm shift_lambda_left}
fun shift_lambda_leftN i = funpow i shift_lambda_left
fun parse_bool_config' name cfg =
(Args.$$$ name #>> K (cfg,true))
|| (Args.$$$ ("no_"^name) #>> K (cfg,false))
fun parse_paren_list' p = Scan.optional (Args.parens (Parse.enum1 "," p)) []
fun apply_configs l ctxt = fold (fn (cfg,v) => fn ctxt => Config.put cfg v ctxt) l ctxt
fun lambda_tuple [] t = t
| lambda_tuple (@{mpat "(?a,?b)"}::l) t = let
val body = lambda_tuple (a::b::l) t
in
@{mk_term "case_prod ?body"}
end
| lambda_tuple (x::l) t = lambda x (lambda_tuple l t)
fun get_tuple_inst ctxt (iname,T) = let
val (argTs,T) = strip_type T
fun cr (Type (@{type_name prod},[T1,T2])) ctxt = let
val (x1,ctxt) = cr T1 ctxt
val (x2,ctxt) = cr T2 ctxt
in
(HOLogic.mk_prod (x1,x2), ctxt)
end
| cr T ctxt = let
val (name, ctxt) = yield_singleton Variable.variant_fixes "x" ctxt
in
(Free (name,T),ctxt)
end
val ctxt = Variable.set_body false ctxt
val (args,ctxt) = fold_map cr argTs ctxt
fun fl (@{mpat "(?x,?y)"}) = fl x @ fl y
| fl t = [t]
val fargs = flat (map fl args)
val fTs = map fastype_of fargs
val v = Var (iname,fTs ---> T)
val v = list_comb (v,fargs)
val v = lambda_tuple args v
in
Thm.cterm_of ctxt v
end
fun instantiate_tuples ctxt inTs = let
val inst = inTs ~~ map (get_tuple_inst ctxt) inTs
in
Thm.instantiate (TVars.empty, Vars.make inst)
end
val _ = COND'
fun instantiate_tuples_from_term_tac ctxt t st = let
val vars = Term.add_vars t []
in
PRIMITIVE (instantiate_tuples ctxt vars) st
end
fun instantiate_tuples_subgoal_tac ctxt = WITH_subgoal (fn t => K (instantiate_tuples_from_term_tac ctxt t))
end
structure Basic_Refine_Util: BASIC_REFINE_UTIL = Refine_Util
open Basic_Refine_Util
›
attribute_setup zero_var_indexes = ‹
Scan.succeed (Thm.rule_attribute [] (K Drule.zero_var_indexes))
› "Set variable indexes to zero, renaming to avoid clashes"
end