--- a/src/HOL/Analysis/Metric_Arith.thy Mon Oct 28 18:50:40 2019 +0000
+++ b/src/HOL/Analysis/Metric_Arith.thy Mon Oct 28 20:00:36 2019 +0100
@@ -103,7 +103,7 @@
"x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> x = y \<longleftrightarrow> (\<forall>a\<in>s. dist x a = dist y a)"
by auto
-ML_file "metricarith.ml"
+ML_file "metric_arith.ML"
method_setup metric = \<open>
Scan.succeed (SIMPLE_METHOD' o MetricArith.metric_arith_tac)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/metric_arith.ML Mon Oct 28 20:00:36 2019 +0100
@@ -0,0 +1,324 @@
+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_empty ball_insert})
+ 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
--- a/src/HOL/Analysis/metricarith.ml Mon Oct 28 18:50:40 2019 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,324 +0,0 @@
-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_empty ball_insert})
- 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