signature METRIC_ARITH = sig
val metric_arith_tac : Proof.context -> int -> tactic
val trace: bool Config.T
end
structure MetricArith : METRIC_ARITH = struct
fun default d x = case x of SOME y => SOME y | NONE => d
(* apply f to both cterms in ct_pair, merge results *)
fun app_union_ct_pair f ct_pair = uncurry (union (op aconvc)) (apply2 f ct_pair)
val trace = Attrib.setup_config_bool \<^binding>\<open>metric_trace\<close> (K false)
fun trace_tac ctxt msg =
if Config.get ctxt trace then print_tac ctxt msg
else all_tac
fun argo_trace_ctxt ctxt =
if Config.get ctxt trace
then Config.map (Argo_Tactic.trace) (K "basic") ctxt
else ctxt
fun IF_UNSOLVED' tac i = IF_UNSOLVED (tac i)
fun REPEAT' tac i = REPEAT (tac i)
fun frees ct = Drule.cterm_add_frees ct []
fun free_in v ct = member (op aconvc) (frees ct) v
(* build a cterm set with elements cts of type ty *)
fun mk_ct_set ctxt ty =
map Thm.term_of #>
HOLogic.mk_set ty #>
Thm.cterm_of ctxt
fun prenex_tac ctxt =
let
val prenex_simps = Proof_Context.get_thms ctxt @{named_theorems metric_prenex}
val prenex_ctxt = put_simpset HOL_basic_ss ctxt addsimps prenex_simps
in
simp_tac prenex_ctxt THEN'
K (trace_tac ctxt "Prenex form")
end
fun nnf_tac ctxt =
let
val nnf_simps = Proof_Context.get_thms ctxt @{named_theorems metric_nnf}
val nnf_ctxt = put_simpset HOL_basic_ss ctxt addsimps nnf_simps
in
simp_tac nnf_ctxt THEN'
K (trace_tac ctxt "NNF form")
end
fun unfold_tac ctxt =
asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps (
Proof_Context.get_thms ctxt @{named_theorems metric_unfold}))
fun pre_arith_tac ctxt =
simp_tac (put_simpset HOL_basic_ss ctxt addsimps (
Proof_Context.get_thms ctxt @{named_theorems metric_pre_arith})) THEN'
K (trace_tac ctxt "Prepared for decision procedure")
fun dist_refl_sym_tac ctxt =
let
val refl_sym_simps = @{thms dist_self dist_commute add_0_right add_0_left simp_thms}
val refl_sym_ctxt = put_simpset HOL_basic_ss ctxt addsimps refl_sym_simps
in
simp_tac refl_sym_ctxt THEN'
K (trace_tac ctxt ("Simplified using " ^ @{make_string} refl_sym_simps))
end
fun is_exists ct =
case Thm.term_of ct of
Const (\<^const_name>\<open>HOL.Ex\<close>,_)$_ => true
| Const (\<^const_name>\<open>Trueprop\<close>,_)$_ => is_exists (Thm.dest_arg ct)
| _ => false
fun is_forall ct =
case Thm.term_of ct of
Const (\<^const_name>\<open>HOL.All\<close>,_)$_ => true
| Const (\<^const_name>\<open>Trueprop\<close>,_)$_ => is_forall (Thm.dest_arg ct)
| _ => false
fun dist_ty mty = mty --> mty --> \<^typ>\<open>real\<close>
(* find all free points in ct of type metric_ty *)
fun find_points ctxt metric_ty ct =
let
fun find ct =
(if Thm.typ_of_cterm ct = metric_ty then [ct] else []) @ (
case Thm.term_of ct of
_ $ _ =>
app_union_ct_pair find (Thm.dest_comb ct)
| Abs (_, _, _) =>
(* ensure the point doesn't contain the bound variable *)
let val (var, bod) = Thm.dest_abs NONE ct in
filter (free_in var #> not) (find bod)
end
| _ => [])
val points = find ct
in
case points of
[] =>
(* if no point can be found, invent one *)
let
val free_name = Term.variant_frees (Thm.term_of ct) [("x", metric_ty)]
in
map (Free #> Thm.cterm_of ctxt) free_name
end
| _ => points
end
(* find all cterms "dist x y" in ct, where x and y have type metric_ty *)
fun find_dist metric_ty ct =
let
val dty = dist_ty metric_ty
fun find ct =
case Thm.term_of ct of
Const (\<^const_name>\<open>dist\<close>, ty) $ _ $ _ =>
if ty = dty then [ct] else []
| _ $ _ =>
app_union_ct_pair find (Thm.dest_comb ct)
| Abs (_, _, _) =>
let val (var, bod) = Thm.dest_abs NONE ct in
filter (free_in var #> not) (find bod)
end
| _ => []
in
find ct
end
(* find all "x=y", where x has type metric_ty *)
fun find_eq metric_ty ct =
let
fun find ct =
case Thm.term_of ct of
Const (\<^const_name>\<open>HOL.eq\<close>, ty) $ _ $ _ =>
if fst (dest_funT ty) = metric_ty
then [ct]
else app_union_ct_pair find (Thm.dest_binop ct)
| _ $ _ => app_union_ct_pair find (Thm.dest_comb ct)
| Abs (_, _, _) =>
let val (var, bod) = Thm.dest_abs NONE ct in
filter (free_in var #> not) (find bod)
end
| _ => []
in
find ct
end
(* rewrite ct of the form "dist x y" using maxdist_thm *)
fun maxdist_conv ctxt fset_ct ct =
let
val (xct, yct) = Thm.dest_binop ct
val solve_prems =
rule_by_tactic ctxt (ALLGOALS (simp_tac (put_simpset HOL_ss ctxt
addsimps @{thms finite.emptyI finite_insert empty_iff insert_iff})))
val image_simp =
Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms image_empty image_insert})
val dist_refl_sym_simp =
Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms dist_commute dist_self})
val algebra_simp =
Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps
@{thms diff_self diff_0_right diff_0 abs_zero abs_minus_cancel abs_minus_commute})
val insert_simp =
Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms insert_absorb2 insert_commute})
val sup_simp =
Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms cSup_singleton Sup_insert_insert})
val real_abs_dist_simp =
Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms real_abs_dist})
val maxdist_thm =
@{thm maxdist_thm} |>
infer_instantiate' ctxt [SOME fset_ct, SOME xct, SOME yct] |>
solve_prems
in
((Conv.rewr_conv maxdist_thm) then_conv
(* SUP to Sup *)
image_simp then_conv
dist_refl_sym_simp then_conv
algebra_simp then_conv
(* eliminate duplicate terms in set *)
insert_simp then_conv
(* Sup to max *)
sup_simp then_conv
real_abs_dist_simp) ct
end
(* rewrite ct of the form "x=y" using metric_eq_thm *)
fun metric_eq_conv ctxt fset_ct ct =
let
val (xct, yct) = Thm.dest_binop ct
val solve_prems =
rule_by_tactic ctxt (ALLGOALS (simp_tac (put_simpset HOL_ss ctxt
addsimps @{thms empty_iff insert_iff})))
val ball_simp =
Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps
@{thms Set.ball_simps(7) Set.ball_simps(5)})
val dist_refl_sym_simp =
Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms dist_commute dist_self})
val metric_eq_thm =
@{thm metric_eq_thm} |>
infer_instantiate' ctxt [SOME xct, SOME fset_ct, SOME yct] |>
solve_prems
in
((Conv.rewr_conv metric_eq_thm) then_conv
(* convert \<forall>x\<in>{x\<^sub>1,...,x\<^sub>n}. P x to P x\<^sub>1 \<and> ... \<and> P x\<^sub>n *)
ball_simp then_conv
dist_refl_sym_simp) ct
end
(* build list of theorems "0 \<le> dist x y" for all dist terms in ct *)
fun augment_dist_pos ctxt metric_ty ct =
let fun inst dist_ct =
let val (xct, yct) = Thm.dest_binop dist_ct
in infer_instantiate' ctxt [SOME xct, SOME yct] @{thm zero_le_dist} end
in map inst (find_dist metric_ty ct) end
fun top_sweep_rewrs_tac ctxt thms =
CONVERSION (Conv.top_sweep_conv (K (Conv.rewrs_conv thms)) ctxt)
(* apply maxdist_conv and metric_eq_conv to the goal, thereby embedding the goal in (\<real>\<^sup>n,dist\<^sub>\<infinity>) *)
fun embedding_tac ctxt metric_ty i goal =
let
val ct = (Thm.cprem_of goal 1)
val points = find_points ctxt metric_ty ct
val fset_ct = mk_ct_set ctxt metric_ty points
(* embed all subterms of the form "dist x y" in (\<real>\<^sup>n,dist\<^sub>\<infinity>) *)
val eq1 = map (maxdist_conv ctxt fset_ct) (find_dist metric_ty ct)
(* replace point equality by equality of components in \<real>\<^sup>n *)
val eq2 = map (metric_eq_conv ctxt fset_ct) (find_eq metric_ty ct)
in
( K (trace_tac ctxt "Embedding into \<real>\<^sup>n") THEN' top_sweep_rewrs_tac ctxt (eq1 @ eq2))i goal
end
(* decision procedure for linear real arithmetic *)
fun lin_real_arith_tac ctxt metric_ty i goal =
let
val dist_thms = augment_dist_pos ctxt metric_ty (Thm.cprem_of goal 1)
val ctxt' = argo_trace_ctxt ctxt
in (Argo_Tactic.argo_tac ctxt' dist_thms) i goal end
fun basic_metric_arith_tac ctxt metric_ty =
HEADGOAL (dist_refl_sym_tac ctxt THEN'
IF_UNSOLVED' (embedding_tac ctxt metric_ty) THEN'
IF_UNSOLVED' (pre_arith_tac ctxt) THEN'
IF_UNSOLVED' (lin_real_arith_tac ctxt metric_ty))
(* tries to infer the metric space from ct from dist terms,
if no dist terms are present, equality terms will be used *)
fun guess_metric ctxt ct =
let
fun find_dist ct =
case Thm.term_of ct of
Const (\<^const_name>\<open>dist\<close>, ty) $ _ $ _ => SOME (fst (dest_funT ty))
| _ $ _ =>
let val (s, t) = Thm.dest_comb ct in
default (find_dist t) (find_dist s)
end
| Abs (_, _, _) => find_dist (snd (Thm.dest_abs NONE ct))
| _ => NONE
fun find_eq ct =
case Thm.term_of ct of
Const (\<^const_name>\<open>HOL.eq\<close>, ty) $ x $ _ =>
let val (l, r) = Thm.dest_binop ct in
if Sign.of_sort (Proof_Context.theory_of ctxt) (type_of x, \<^sort>\<open>metric_space\<close>)
then SOME (fst (dest_funT ty))
else default (find_dist r) (find_eq l)
end
| _ $ _ =>
let val (s, t) = Thm.dest_comb ct in
default (find_eq t) (find_eq s)
end
| Abs (_, _, _) => find_eq (snd (Thm.dest_abs NONE ct))
| _ => NONE
in
case default (find_eq ct) (find_dist ct) of
SOME ty => ty
| NONE => error "No Metric Space was found"
end
(* eliminate \<exists> by proving the goal for a single witness from the metric space *)
fun elim_exists ctxt goal =
let
val ct = Thm.cprem_of goal 1
val metric_ty = guess_metric ctxt ct
val points = find_points ctxt metric_ty ct
fun try_point ctxt pt =
let val ex_rule = infer_instantiate' ctxt [NONE, SOME pt] @{thm exI}
in
HEADGOAL (resolve_tac ctxt [ex_rule] ORELSE'
(* variable doesn't occur in body *)
resolve_tac ctxt @{thms exI}) THEN
trace_tac ctxt ("Removed existential quantifier, try " ^ @{make_string} pt) THEN
try_points ctxt
end
and try_points ctxt goal = (
if is_exists (Thm.cprem_of goal 1) then
FIRST (map (try_point ctxt) points)
else if is_forall (Thm.cprem_of goal 1) then
HEADGOAL (resolve_tac ctxt @{thms HOL.allI} THEN'
Subgoal.FOCUS (fn {context = ctxt', ...} =>
trace_tac ctxt "Removed universal quantifier" THEN
try_points ctxt') ctxt)
else basic_metric_arith_tac ctxt metric_ty) goal
in
try_points ctxt goal
end
fun metric_arith_tac ctxt =
(* unfold common definitions to get rid of sets *)
unfold_tac ctxt THEN'
(* remove all meta-level connectives *)
IF_UNSOLVED' (Object_Logic.full_atomize_tac ctxt) THEN'
(* convert goal to prenex form *)
IF_UNSOLVED' (prenex_tac ctxt) THEN'
(* and NNF to ? *)
IF_UNSOLVED' (nnf_tac ctxt) THEN'
(* turn all universally quantified variables into free variables, by focusing the subgoal *)
REPEAT' (resolve_tac ctxt @{thms HOL.allI}) THEN'
IF_UNSOLVED' (SUBPROOF (fn {context=ctxt', ...} =>
trace_tac ctxt' "Focused on subgoal" THEN
elim_exists ctxt') ctxt)
end