diff --git a/thys/Eval_FO/Eval_FO.thy b/thys/Eval_FO/Eval_FO.thy --- a/thys/Eval_FO/Eval_FO.thy +++ b/thys/Eval_FO/Eval_FO.thy @@ -1,168 +1,168 @@ theory Eval_FO - imports Infinite FO + imports "HOL-Library.Infinite_Typeclass" FO begin datatype 'a eval_res = Fin "'a table" | Infin | Wf_error locale eval_fo = fixes wf :: "('a :: infinite, 'b) fo_fmla \ ('b \ nat \ 'a list set) \ 't \ bool" and abs :: "('a fo_term) list \ 'a table \ 't" and rep :: "'t \ 'a table" and res :: "'t \ 'a eval_res" and eval_bool :: "bool \ 't" and eval_eq :: "'a fo_term \ 'a fo_term \ 't" and eval_neg :: "nat list \ 't \ 't" and eval_conj :: "nat list \ 't \ nat list \ 't \ 't" and eval_ajoin :: "nat list \ 't \ nat list \ 't \ 't" and eval_disj :: "nat list \ 't \ nat list \ 't \ 't" and eval_exists :: "nat \ nat list \ 't \ 't" and eval_forall :: "nat \ nat list \ 't \ 't" assumes fo_rep: "wf \ I t \ rep t = proj_sat \ I" and fo_res_fin: "wf \ I t \ finite (rep t) \ res t = Fin (rep t)" and fo_res_infin: "wf \ I t \ \finite (rep t) \ res t = Infin" and fo_abs: "finite (I (r, length ts)) \ wf (Pred r ts) I (abs ts (I (r, length ts)))" and fo_bool: "wf (Bool b) I (eval_bool b)" and fo_eq: "wf (Eqa trm trm') I (eval_eq trm trm')" and fo_neg: "wf \ I t \ wf (Neg \) I (eval_neg (fv_fo_fmla_list \) t)" and fo_conj: "wf \ I t\ \ wf \ I t\ \ (case \ of Neg \' \ False | _ \ True) \ wf (Conj \ \) I (eval_conj (fv_fo_fmla_list \) t\ (fv_fo_fmla_list \) t\)" and fo_ajoin: "wf \ I t\ \ wf \' I t\' \ wf (Conj \ (Neg \')) I (eval_ajoin (fv_fo_fmla_list \) t\ (fv_fo_fmla_list \') t\')" and fo_disj: "wf \ I t\ \ wf \ I t\ \ wf (Disj \ \) I (eval_disj (fv_fo_fmla_list \) t\ (fv_fo_fmla_list \) t\)" and fo_exists: "wf \ I t \ wf (Exists i \) I (eval_exists i (fv_fo_fmla_list \) t)" and fo_forall: "wf \ I t \ wf (Forall i \) I (eval_forall i (fv_fo_fmla_list \) t)" begin fun eval_fmla :: "('a, 'b) fo_fmla \ ('a table, 'b) fo_intp \ 't" where "eval_fmla (Pred r ts) I = abs ts (I (r, length ts))" | "eval_fmla (Bool b) I = eval_bool b" | "eval_fmla (Eqa t t') I = eval_eq t t'" | "eval_fmla (Neg \) I = eval_neg (fv_fo_fmla_list \) (eval_fmla \ I)" | "eval_fmla (Conj \ \) I = (let ns\ = fv_fo_fmla_list \; ns\ = fv_fo_fmla_list \; X\ = eval_fmla \ I in case \ of Neg \' \ let X\' = eval_fmla \' I in eval_ajoin ns\ X\ (fv_fo_fmla_list \') X\' | _ \ eval_conj ns\ X\ ns\ (eval_fmla \ I))" | "eval_fmla (Disj \ \) I = eval_disj (fv_fo_fmla_list \) (eval_fmla \ I) (fv_fo_fmla_list \) (eval_fmla \ I)" | "eval_fmla (Exists i \) I = eval_exists i (fv_fo_fmla_list \) (eval_fmla \ I)" | "eval_fmla (Forall i \) I = eval_forall i (fv_fo_fmla_list \) (eval_fmla \ I)" lemma eval_fmla_correct: fixes \ :: "('a :: infinite, 'b) fo_fmla" assumes "wf_fo_intp \ I" shows "wf \ I (eval_fmla \ I)" using assms proof (induction \ I rule: eval_fmla.induct) case (1 r ts I) then show ?case using fo_abs by auto next case (2 b I) then show ?case using fo_bool by auto next case (3 t t' I) then show ?case using fo_eq by auto next case (4 \ I) then show ?case using fo_neg by auto next case (5 \ \ I) have fins: "wf_fo_intp \ I" "wf_fo_intp \ I" using 5(10) by auto have eval\: "wf \ I (eval_fmla \ I)" using 5(1)[OF _ _ fins(1)] by auto show ?case proof (cases "\\'. \ = Neg \'") case True then obtain \' where \_def: "\ = Neg \'" by auto have fin: "wf_fo_intp \' I" using fins(2) by (auto simp: \_def) have eval\': "wf \' I (eval_fmla \' I)" using 5(5)[OF _ _ _ \_def fin] by auto show ?thesis unfolding \_def using fo_ajoin[OF eval\ eval\'] by auto next case False then have eval\: "wf \ I (eval_fmla \ I)" using 5 fins(2) by (cases \) auto have eval: "eval_fmla (Conj \ \) I = eval_conj (fv_fo_fmla_list \) (eval_fmla \ I) (fv_fo_fmla_list \) (eval_fmla \ I)" using False by (auto simp: Let_def split: fo_fmla.splits) show "wf (Conj \ \) I (eval_fmla (Conj \ \) I)" using fo_conj[OF eval\ eval\, folded eval] False by (auto split: fo_fmla.splits) qed next case (6 \ \ I) then show ?case using fo_disj by auto next case (7 i \ I) then show ?case using fo_exists by auto next case (8 i \ I) then show ?case using fo_forall by auto qed definition eval :: "('a, 'b) fo_fmla \ ('a table, 'b) fo_intp \ 'a eval_res" where "eval \ I = (if wf_fo_intp \ I then res (eval_fmla \ I) else Wf_error)" lemma eval_fmla_proj_sat: fixes \ :: "('a :: infinite, 'b) fo_fmla" assumes "wf_fo_intp \ I" shows "rep (eval_fmla \ I) = proj_sat \ I" using eval_fmla_correct[OF assms] by (auto simp: fo_rep) lemma eval_sound: fixes \ :: "('a :: infinite, 'b) fo_fmla" assumes "eval \ I = Fin Z" shows "Z = proj_sat \ I" proof - have "wf \ I (eval_fmla \ I)" using eval_fmla_correct assms by (auto simp: eval_def split: if_splits) then show ?thesis using assms fo_res_fin fo_res_infin by (fastforce simp: eval_def fo_rep split: if_splits) qed lemma eval_complete: fixes \ :: "('a :: infinite, 'b) fo_fmla" assumes "eval \ I = Infin" shows "infinite (proj_sat \ I)" proof - have "wf \ I (eval_fmla \ I)" using eval_fmla_correct assms by (auto simp: eval_def split: if_splits) then show ?thesis using assms fo_res_fin by (auto simp: eval_def fo_rep split: if_splits) qed end end diff --git a/thys/Eval_FO/Infinite.thy b/thys/Eval_FO/Infinite.thy deleted file mode 100644 --- a/thys/Eval_FO/Infinite.thy +++ /dev/null @@ -1,32 +0,0 @@ -theory Infinite - imports Main -begin - -class infinite = - assumes infinite_UNIV: "infinite (UNIV :: 'a set)" -begin - -lemma arb_element: "finite Y \ \x :: 'a. x \ Y" - using ex_new_if_finite infinite_UNIV - by blast - -lemma arb_finite_subset: "finite Y \ \X :: 'a set. Y \ X = {} \ finite X \ n \ card X" -proof - - assume fin: "finite Y" - then obtain X where "X \ UNIV - Y" "finite X" "n \ card X" - using infinite_UNIV - by (metis Compl_eq_Diff_UNIV finite_compl infinite_arbitrarily_large order_refl) - then show ?thesis - by auto -qed - -lemma arb_countable_map: "finite Y \ \f :: (nat \ 'a). inj f \ range f \ UNIV - Y" - using infinite_UNIV - by (auto simp: infinite_countable_subset) - -end - -instance nat :: infinite - by standard auto - -end diff --git a/thys/Eval_FO/ROOT b/thys/Eval_FO/ROOT --- a/thys/Eval_FO/ROOT +++ b/thys/Eval_FO/ROOT @@ -1,17 +1,16 @@ chapter AFP session Eval_FO = Containers + options [timeout=600] theories Ailamazyan_Code Ailamazyan Cluster Eval_FO FO - Infinite Mapping_Code document_files "root.tex" "root.bib" export_files (in ".") [2] "Eval_FO.Ailamazyan_Code:code/**" diff --git a/thys/Winding_Number_Eval/Missing_Analysis.thy b/thys/Winding_Number_Eval/Missing_Analysis.thy --- a/thys/Winding_Number_Eval/Missing_Analysis.thy +++ b/thys/Winding_Number_Eval/Missing_Analysis.thy @@ -1,153 +1,139 @@ (* Author: Wenda Li *) section \Some useful lemmas in analysis\ theory Missing_Analysis imports "HOL-Complex_Analysis.Complex_Analysis" begin subsection \More about paths\ lemma pathfinish_offset[simp]: "pathfinish (\t. g t - z) = pathfinish g - z" unfolding pathfinish_def by simp lemma pathstart_offset[simp]: "pathstart (\t. g t - z) = pathstart g - z" unfolding pathstart_def by simp lemma pathimage_offset[simp]: fixes g :: "_ \ 'b::topological_group_add" shows "p \ path_image (\t. g t - z) \ p+z \ path_image g " unfolding path_image_def by (auto simp:algebra_simps) lemma path_offset[simp]: fixes g :: "_ \ 'b::topological_group_add" shows "path (\t. g t - z) \ path g" unfolding path_def proof assume "continuous_on {0..1} (\t. g t - z)" - hence "continuous_on {0..1} (\t. (g t - z) + z)" - apply (rule continuous_intros) - by (intro continuous_intros) + hence "continuous_on {0..1} (\t. (g t - z) + z)" + using continuous_on_add continuous_on_const by blast then show "continuous_on {0..1} g" by auto qed (auto intro:continuous_intros) lemma not_on_circlepathI: assumes "cmod (z-z0) \ \r\" shows "z \ path_image (part_circlepath z0 r st tt)" -proof (rule ccontr) - assume "\ z \ path_image (part_circlepath z0 r st tt)" - then have "z\path_image (part_circlepath z0 r st tt)" by simp - then obtain t where "t\{0..1}" and *:"z = z0 + r * exp (\ * (linepath st tt t))" - unfolding path_image_def image_def part_circlepath_def by blast - define \ where "\ = linepath st tt t" - then have "z-z0 = r * exp (\ * \)" using * by auto - then have "cmod (z-z0) = cmod (r * exp (\ * \))" by auto - also have "\ = \r\ * cmod (exp (\ * \))" by (simp add: norm_mult) - also have "\ = \r\" by auto - finally have "cmod (z-z0) = \r\" . - then show False using assms by auto -qed + using assms + by (auto simp add: path_image_def image_def part_circlepath_def norm_mult) lemma circlepath_inj_on: assumes "r>0" shows "inj_on (circlepath z r) {0..<1}" proof (rule inj_onI) fix x y assume asm: "x \ {0..<1}" "y \ {0..<1}" "circlepath z r x = circlepath z r y" define c where "c=2 * pi * \" have "c\0" unfolding c_def by auto from asm(3) have "exp (c * x) =exp (c * y)" unfolding circlepath c_def using \r>0\ by auto then obtain n where "c * x =c * (y + of_int n)" by (auto simp add:exp_eq c_def algebra_simps) then have "x=y+n" using \c\0\ by (meson mult_cancel_left of_real_eq_iff) then show "x=y" using asm(1,2) by auto qed subsection \More lemmas related to @{term winding_number}\ lemma winding_number_comp: assumes "open s" "f holomorphic_on s" "path_image \ \ s" "valid_path \" "z \ path_image (f \ \)" shows "winding_number (f \ \) z = 1/(2*pi*\)* contour_integral \ (\w. deriv f w / (f w - z))" proof - obtain spikes where "finite spikes" and \_diff: "\ C1_differentiable_on {0..1} - spikes" using \valid_path \\ unfolding valid_path_def piecewise_C1_differentiable_on_def by auto have "valid_path (f \ \)" using valid_path_compose_holomorphic assms by blast moreover have "contour_integral (f \ \) (\w. 1 / (w - z)) = contour_integral \ (\w. deriv f w / (f w - z))" unfolding contour_integral_integral proof (rule integral_spike[rule_format,OF negligible_finite[OF \finite spikes\]]) fix t::real assume t:"t \ {0..1} - spikes" then have "\ differentiable at t" using \_diff unfolding C1_differentiable_on_eq by auto moreover have "f field_differentiable at (\ t)" proof - have "\ t \ s" using \path_image \ \ s\ t unfolding path_image_def by auto thus ?thesis using \open s\ \f holomorphic_on s\ holomorphic_on_imp_differentiable_at by blast qed ultimately show " deriv f (\ t) / (f (\ t) - z) * vector_derivative \ (at t) = 1 / ((f \ \) t - z) * vector_derivative (f \ \) (at t)" - apply (subst vector_derivative_chain_at_general) - by (simp_all add:field_simps) + by (simp add: vector_derivative_chain_at_general) qed moreover note \z \ path_image (f \ \)\ ultimately show ?thesis - apply (subst winding_number_valid_path) - by simp_all + using winding_number_valid_path by presburger qed lemma winding_number_uminus_comp: assumes "valid_path \" "- z \ path_image \" shows "winding_number (uminus \ \) z = winding_number \ (-z)" proof - define c where "c= 2 * pi * \" have "winding_number (uminus \ \) z = 1/c * contour_integral \ (\w. deriv uminus w / (-w-z)) " proof (rule winding_number_comp[of UNIV, folded c_def]) show "open UNIV" "uminus holomorphic_on UNIV" "path_image \ \ UNIV" "valid_path \" using \valid_path \\ by (auto intro:holomorphic_intros) show "z \ path_image (uminus \ \)" unfolding path_image_compose using \- z \ path_image \\ by auto qed also have "\ = 1/c * contour_integral \ (\w. 1 / (w- (-z)))" by (auto intro!:contour_integral_eq simp add:field_simps minus_divide_right) also have "\ = winding_number \ (-z)" using winding_number_valid_path[OF \valid_path \\ \- z \ path_image \\,folded c_def] by simp finally show ?thesis by auto qed lemma winding_number_comp_linear: assumes "c\0" "valid_path \" and not_image: "(z-b)/c \ path_image \" shows "winding_number ((\x. c*x+b) \ \) z = winding_number \ ((z-b)/c)" (is "?L = ?R") proof - define cc where "cc=1 / (complex_of_real (2 * pi) * \)" define zz where "zz=(z-b)/c" have "?L = cc * contour_integral \ (\w. deriv (\x. c * x + b) w / (c * w + b - z))" apply (subst winding_number_comp[of UNIV,simplified]) subgoal by (auto intro:holomorphic_intros) subgoal using \valid_path \\ . subgoal using not_image \c\0\ unfolding path_image_compose by auto subgoal unfolding cc_def by auto done also have "\ = cc * contour_integral \ (\w.1 / (w - zz))" proof - have "deriv (\x. c * x + b) = (\x. c)" by (auto intro:derivative_intros) then show ?thesis unfolding zz_def cc_def using \c\0\ by (auto simp:field_simps) qed also have "\ = winding_number \ zz" using winding_number_valid_path[OF \valid_path \\ not_image,folded zz_def cc_def] by simp finally show "winding_number ((\x. c * x + b) \ \) z = winding_number \ zz" . qed end