# HG changeset patch # User wenzelm # Date 1572289236 -3600 # Node ID bbe5fe8bba71be06f73736db0a6ce179e357b995 # Parent 70fb697be418850f4d59c70fd4a0b74df1d0cf29# Parent e8207714d505ad06d9b10ec3012ace2856a5b1b4 merged diff -r 70fb697be418 -r bbe5fe8bba71 src/HOL/Analysis/Metric_Arith.thy --- 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 \ s \ y \ s \ x = y \ (\a\s. dist x a = dist y a)" by auto -ML_file "metricarith.ml" +ML_file "metric_arith.ML" method_setup metric = \ Scan.succeed (SIMPLE_METHOD' o MetricArith.metric_arith_tac) diff -r 70fb697be418 -r bbe5fe8bba71 src/HOL/Analysis/metric_arith.ML --- /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>\metric_trace\ (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>\HOL.Ex\,_)$_ => true + | Const (\<^const_name>\Trueprop\,_)$_ => is_exists (Thm.dest_arg ct) + | _ => false + +fun is_forall ct = + case Thm.term_of ct of + Const (\<^const_name>\HOL.All\,_)$_ => true + | Const (\<^const_name>\Trueprop\,_)$_ => is_forall (Thm.dest_arg ct) + | _ => false + +fun dist_ty mty = mty --> mty --> \<^typ>\real\ + +(* 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>\dist\, 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>\HOL.eq\, 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 \x\{x\<^sub>1,...,x\<^sub>n}. P x to P x\<^sub>1 \ ... \ P x\<^sub>n *) + ball_simp then_conv + dist_refl_sym_simp) ct + end + +(* build list of theorems "0 \ 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 (\\<^sup>n,dist\<^sub>\) *) +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 (\\<^sup>n,dist\<^sub>\) *) + val eq1 = map (maxdist_conv ctxt fset_ct) (find_dist metric_ty ct) + (* replace point equality by equality of components in \\<^sup>n *) + val eq2 = map (metric_eq_conv ctxt fset_ct) (find_eq metric_ty ct) + in + ( K (trace_tac ctxt "Embedding into \\<^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>\dist\, 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>\HOL.eq\, ty) $ x $ _ => + let val (l, r) = Thm.dest_binop ct in + if Sign.of_sort (Proof_Context.theory_of ctxt) (type_of x, \<^sort>\metric_space\) + 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 \ 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 diff -r 70fb697be418 -r bbe5fe8bba71 src/HOL/Analysis/metricarith.ml --- 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>\metric_trace\ (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>\HOL.Ex\,_)$_ => true - | Const (\<^const_name>\Trueprop\,_)$_ => is_exists (Thm.dest_arg ct) - | _ => false - -fun is_forall ct = - case Thm.term_of ct of - Const (\<^const_name>\HOL.All\,_)$_ => true - | Const (\<^const_name>\Trueprop\,_)$_ => is_forall (Thm.dest_arg ct) - | _ => false - -fun dist_ty mty = mty --> mty --> \<^typ>\real\ - -(* 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>\dist\, 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>\HOL.eq\, 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 \x\{x\<^sub>1,...,x\<^sub>n}. P x to P x\<^sub>1 \ ... \ P x\<^sub>n *) - ball_simp then_conv - dist_refl_sym_simp) ct - end - -(* build list of theorems "0 \ 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 (\\<^sup>n,dist\<^sub>\) *) -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 (\\<^sup>n,dist\<^sub>\) *) - val eq1 = map (maxdist_conv ctxt fset_ct) (find_dist metric_ty ct) - (* replace point equality by equality of components in \\<^sup>n *) - val eq2 = map (metric_eq_conv ctxt fset_ct) (find_eq metric_ty ct) - in - ( K (trace_tac ctxt "Embedding into \\<^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>\dist\, 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>\HOL.eq\, ty) $ x $ _ => - let val (l, r) = Thm.dest_binop ct in - if Sign.of_sort (Proof_Context.theory_of ctxt) (type_of x, \<^sort>\metric_space\) - 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 \ 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