I agree Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.
theory Defs
imports "HOL-IMP.Big_Step" Complex_Main
begin
datatype entry = Unchanged ("'_'_'_'_'_'_'_'_") | V "(int\<times>int) set"
unbundle lattice_syntax
definition chain :: "(nat \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool"
where "chain C \<longleftrightarrow> (\<forall>n. C n \<le> C (Suc n))"
definition continuous :: "('a::complete_lattice \<Rightarrow> 'b::complete_lattice) \<Rightarrow> bool"
where "continuous f \<longleftrightarrow> (\<forall>C. chain C \<longrightarrow> f (\<Squnion> (range C)) = \<Squnion> (f ` range C))"
lemma continuousD: "\<lbrakk>continuous f; chain C\<rbrakk> \<Longrightarrow> f (\<Squnion> (range C)) = \<Squnion> (f ` range C)"
unfolding continuous_def by auto
paragraph \<open>Galois\<close>
lemma preorder_onI [intro]:
assumes "refl_on A R"
and "trans R"
shows "preorder_on A R"
using assms unfolding preorder_on_def by auto
declare refl_onI[intro] transI[intro]
lemma preorder_onE [elim]:
assumes "preorder_on A R"
obtains "refl_on A R" "trans R"
using assms unfolding preorder_on_def by auto
declare refl_onD[dest] transD[dest]
definition "fun_rel R S \<equiv> {(f, g). \<forall>x y. (x, y) \<in> R \<longrightarrow> (f x, g y) \<in> S}"
notation "fun_rel" ("(_ \<Rrightarrow> _)" [80,80] 81)
lemma fun_relI [intro]:
assumes "\<And>x y. (x, y) \<in> R \<Longrightarrow> (f x, g y) \<in> S"
shows "(f, g) \<in> (R \<Rrightarrow> S)"
using assms unfolding fun_rel_def by auto
lemma fun_relE [elim]:
assumes "(f, g) \<in> (R \<Rrightarrow> S)"
obtains "\<And>x y. (x, y) \<in> R \<Longrightarrow> (f x, g y) \<in> S"
using assms unfolding fun_rel_def by auto
definition "mono_fun R S f \<equiv> (f, f) \<in> (R \<Rrightarrow> S)"
notation "mono_fun" ("(_ \<Rrightarrow>m _)" [50,50] 51)
lemma mono_funI [intro]:
assumes "\<And>x y. (x, y) \<in> R \<Longrightarrow> (f x, f y) \<in> S"
shows "(R \<Rrightarrow>m S) f"
using assms unfolding mono_fun_def fun_rel_def by auto
lemma mono_funE [elim]:
assumes "(R \<Rrightarrow>m S) f"
obtains "\<And>x y. (x, y) \<in> R \<Longrightarrow> (f x, f y) \<in> S"
using assms unfolding mono_fun_def fun_rel_def by auto
definition "sound_rel x L R r y \<equiv> y \<in> Domain R \<and> (x, r y) \<in> L"
notation sound_rel ("(_ \<^bsub>_\<^esub>\<lessapprox>\<^bsub>_ _\<^esub> _)" [50,50,50,50,50] 51)
lemma sound_relI [intro]:
assumes "y \<in> Domain R" "(x, r y) \<in> L"
shows "x \<^bsub>L\<^esub>\<lessapprox>\<^bsub>R r\<^esub> y"
using assms unfolding sound_rel_def by auto
lemma sound_relE [elim]:
assumes "x \<^bsub>L\<^esub>\<lessapprox>\<^bsub>R r\<^esub> y"
obtains "y \<in> Domain R" "(x, r y) \<in> L"
using assms unfolding sound_rel_def by auto
corollary sound_rel_iff: "(x \<^bsub>L\<^esub>\<lessapprox>\<^bsub>R r\<^esub> y) \<longleftrightarrow> y \<in> Domain R \<and> (x, r y) \<in> L" by blast
definition "galois_con L R l r \<equiv>
preorder_on (Domain L) L \<and> preorder_on (Domain R) R
\<and> (L \<Rrightarrow>m R) l \<and> (R \<Rrightarrow>m L) r
\<and> (\<forall>x y. x \<in> Domain L \<and> y \<in> Domain R \<longrightarrow> (x, r y) \<in> L \<longleftrightarrow> (l x, y) \<in> R)"
notation "galois_con" ("(_ \<stileturn> _)" 50)
lemma galois_conI [intro]:
assumes "preorder_on (Domain L) L" "preorder_on (Domain R) R"
and "(L \<Rrightarrow>m R) l" "(R \<Rrightarrow>m L) r"
and "\<And>x y. y \<in> Domain R \<Longrightarrow> (x, r y) \<in> L \<Longrightarrow> (l x, y) \<in> R"
and "\<And>x y. x \<in> Domain L \<Longrightarrow> (l x, y) \<in> R \<Longrightarrow> (x, r y) \<in> L"
shows "(L \<stileturn> R) l r"
using assms unfolding galois_con_def by fastforce
lemma galois_conE [elim]:
assumes "(L \<stileturn> R) l r"
obtains "preorder_on (Domain L) L" "preorder_on (Domain R) R"
"(L \<Rrightarrow>m R) l" "(R \<Rrightarrow>m L) r"
"\<And>x y. y \<in> Domain R \<Longrightarrow> (x, r y) \<in> L \<Longrightarrow> (l x, y) \<in> R"
"\<And>x y. x \<in> Domain L \<Longrightarrow> (l x, y) \<in> R \<Longrightarrow> (x, r y) \<in> L"
using assms unfolding galois_con_def by fastforce
definition "rel_eq x R y \<equiv> (x, y) \<in> R \<and> (y, x) \<in> R"
notation "rel_eq" ("(_ \<equiv>\<^bsub>_\<^esub> _)" [50,50,50] 51)
lemma rel_eqI [intro]:
assumes "(x, y) \<in> R" "(y, x) \<in> R"
shows "x \<equiv>\<^bsub>R\<^esub> y"
using assms unfolding rel_eq_def by auto
lemma rel_eqE [elim]:
assumes "x \<equiv>\<^bsub>R\<^esub> y"
obtains "(x, y) \<in> R" "(y, x) \<in> R"
using assms unfolding rel_eq_def by auto
definition "refl_rel R \<equiv> {(x, y). (x, x) \<in> R \<and> (y, y) \<in> R \<and> (x, y) \<in> R}"
notation "refl_rel" ("_\<^sup>\<oplus>" [1000])
lemma refl_relI [intro]:
assumes "(x, x) \<in> R"
and "(y, y) \<in> R"
and "(x, y) \<in> R"
shows "(x, y) \<in> R\<^sup>\<oplus>"
using assms unfolding refl_rel_def by auto
lemma refl_relE [elim]:
assumes "(x, y) \<in> R\<^sup>\<oplus>"
obtains "(x, x) \<in> R" "(y, y) \<in> R" "(x, y) \<in> R"
using assms unfolding refl_rel_def by auto
definition "fun_map f g h \<equiv> g o h o f"
notation "fun_map" ("'(_ \<rightarrow> _')")
lemma fun_map_eq [simp]: "(f \<rightarrow> g) h x = g (h (f x))"
unfolding fun_map_def by simp
abbreviation (input) "rel_of R \<equiv> {(x, y). R x y}"
consts A\<^sub>1 :: "entry list"
consts A\<^sub>2 :: "entry list"
consts A\<^sub>3 :: "entry list"
consts A\<^sub>4 :: "entry list"
consts A\<^sub>5 :: "entry list"
consts A\<^sub>6 :: "entry list"
end
theory Submission
imports Defs
begin
definition A\<^sub>0 :: "entry list" where "A\<^sub>0 = [V{},V{(9,0)},________,________,________ ,________ ,________ , ________ , ________ , ________ , ________ , ________, ________ ]"
definition A\<^sub>1 :: "entry list" where "A\<^sub>1 = []"
definition A\<^sub>2 :: "entry list" where "A\<^sub>2 = []"
definition A\<^sub>3 :: "entry list" where "A\<^sub>3 = []"
definition A\<^sub>4 :: "entry list" where "A\<^sub>4 = []"
definition A\<^sub>5 :: "entry list" where "A\<^sub>5 = []"
definition A\<^sub>6 :: "entry list" where "A\<^sub>6 = []"
lemma galois_con_sound_selfI:
assumes "(L \<stileturn> R) l r"
and "x \<in> Domain L"
shows "x \<^bsub>L\<^esub>\<lessapprox>\<^bsub>R r\<^esub> l x"
sorry
lemma galois_con_counit_underapproxI:
assumes "(L \<stileturn> R) l r"
and "y \<in> Domain R"
shows "(l (r y), y) \<in> R"
sorry
lemma galois_con_right_counit_rel_eqI:
assumes "(L \<stileturn> R) l r"
and "y \<in> Domain R"
shows "r (l (r y)) \<equiv>\<^bsub>L\<^esub> r y"
sorry
lemma galois_con_left_unit_rel_eqI:
assumes "(L \<stileturn> R) l r"
and "x \<in> Domain L"
shows "l (r (l x)) \<equiv>\<^bsub>R\<^esub> l x"
sorry
lemma galois_con_unique_left:
assumes "(L \<stileturn> R) l r" "(L \<stileturn> R) l' r"
and "x \<in> Domain L"
shows "l x \<equiv>\<^bsub>R\<^esub> l' x"
sorry
lemma galois_con_if_unique_left_if_galois_con:
assumes "(L \<stileturn> R) l r"
and "\<And>x. x \<in> Domain L \<Longrightarrow> l x \<equiv>\<^bsub>R\<^esub> l' x"
shows "(L \<stileturn> R) l' r"
sorry
lemma real_int_galois: "(rel_of (\<le>) \<stileturn> rel_of (\<le>)) ceiling real_of_int"
sorry
lemma galois_compI:
assumes "(L \<stileturn> M) l1 r1"
and "(M \<stileturn> R) l2 r2"
shows "(L \<stileturn> R) (l2 o l1) (r1 o r2)"
sorry
context
fixes L1 R1 l1 r1 L2 R2 l2 r2 L R l r
assumes gal_cons: "(L1 \<stileturn> R1) l1 r1" "(L2 \<stileturn> R2) l2 r2"
defines L_def [simp]: "L \<equiv> (L1 \<Rrightarrow> L2)\<^sup>\<oplus>"
and R_def [simp]: "R \<equiv> (R1 \<Rrightarrow> R2)\<^sup>\<oplus>"
and l_def [simp]: "l \<equiv> (r1 \<rightarrow> l2)"
and r_def [simp]: "r \<equiv> (l1 \<rightarrow> r2)"
begin
lemma refl_fun_rel_galois_propI1:
assumes "g \<in> Domain R"
and "(f, r g) \<in> L"
shows "(l f, g) \<in> R"
sorry
lemma refl_fun_rel_galois_propI2:
assumes "f \<in> Domain L"
and "(l f, g) \<in> R"
shows "(f, r g) \<in> L"
sorry
theorem galois_refl_fun_relI: "(L \<stileturn> R) l r"
sorry
end
schematic_goal real_int_galois2:
"(?L \<stileturn> ?R) (?l :: (real \<Rightarrow> real) \<Rightarrow> int \<Rightarrow> int) ?r"
by (rule galois_refl_fun_relI real_int_galois)+
schematic_goal real_int_galois3:
"(?L \<stileturn> ?R) (?l :: (real \<Rightarrow> real \<Rightarrow> real) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int) ?r"
by (rule galois_refl_fun_relI real_int_galois)+
print_statement real_int_galois3
lemma "(real_of_int \<rightarrow> (real_of_int \<rightarrow> ceiling)) (+) i1 i2 = \<lceil>real_of_int i1 + real_of_int i2\<rceil>"
unfolding fun_map_eq by (rule refl)
lemma galois_fun_sound:
assumes gal_cons: "(L1 \<stileturn> R1) l1 r1" "(L2 \<stileturn> R2) l2 r2"
and f_mono: "(L1 \<Rrightarrow>m L2) f"
and ysound: "x \<^bsub>L1\<^esub>\<lessapprox>\<^bsub>R1 r1\<^esub> y"
shows "f x \<^bsub>L2\<^esub>\<lessapprox>\<^bsub>R2 r2\<^esub> (r1 \<rightarrow> l2) f y"
sorry
context
fixes L :: "'a rel" and R :: "'b rel" and l r
and lbound :: "'b set \<Rightarrow> 'b"
assumes lbound_lower: "\<And>Y y. Y \<subseteq> Domain R \<Longrightarrow> y \<in> Y \<Longrightarrow> (lbound Y, y) \<in> R"
defines [simp]: "l \<equiv> \<lambda>x. lbound {y \<in> Domain R. (x, r y) \<in> L}"
begin
lemma galois_fun_optimal:
assumes refl_onR: "refl_on (Domain R) R"
and rmono: "(R \<Rrightarrow>m L) r"
and f'sound: "\<And>x y. x \<^bsub>L\<^esub>\<lessapprox>\<^bsub>R r\<^esub> y \<Longrightarrow> f x \<^bsub>L\<^esub>\<lessapprox>\<^bsub>R r\<^esub> f' y"
and f'mono: "(R \<Rrightarrow>m R) f'"
shows "((r \<rightarrow> l) f, f') \<in> R \<Rrightarrow> R"
sorry
lemma galois_fun_canonical:
assumes galcon: "(L \<stileturn> R) l' r"
and lbound_least: "\<And>Y y'. Y \<subseteq> Domain R \<Longrightarrow> (\<And>y. y \<in> Y \<Longrightarrow> (y', y) \<in> R) \<Longrightarrow> (y', lbound Y) \<in> R"
shows "(L \<stileturn> R) l r"
sorry
end
end
theory Check
imports Submission
begin
lemma galois_con_sound_selfI: "((L \<stileturn> R) l r) \<Longrightarrow> (x \<in> Domain L) \<Longrightarrow> x \<^bsub>L\<^esub>\<lessapprox>\<^bsub>R r\<^esub> l x"
by (rule Submission.galois_con_sound_selfI)
lemma galois_con_counit_underapproxI: "((L \<stileturn> R) l r) \<Longrightarrow> (y \<in> Domain R) \<Longrightarrow> (l (r y), y) \<in> R"
by (rule Submission.galois_con_counit_underapproxI)
lemma galois_con_right_counit_rel_eqI: "((L \<stileturn> R) l r) \<Longrightarrow> (y \<in> Domain R) \<Longrightarrow> r (l (r y)) \<equiv>\<^bsub>L\<^esub> r y"
by (rule Submission.galois_con_right_counit_rel_eqI)
lemma galois_con_left_unit_rel_eqI: "((L \<stileturn> R) l r) \<Longrightarrow> (x \<in> Domain L) \<Longrightarrow> l (r (l x)) \<equiv>\<^bsub>R\<^esub> l x"
by (rule Submission.galois_con_left_unit_rel_eqI)
lemma galois_con_if_unique_left_if_galois_con: "((L \<stileturn> R) l r) \<Longrightarrow> (\<And>x. x \<in> Domain L \<Longrightarrow> l x \<equiv>\<^bsub>R\<^esub> l' x) \<Longrightarrow> (L \<stileturn> R) l' r"
by (rule Submission.galois_con_if_unique_left_if_galois_con)
lemma real_int_galois: "(rel_of (\<le>) \<stileturn> rel_of (\<le>)) ceiling real_of_int"
by (rule Submission.real_int_galois)
lemma galois_compI: "((L \<stileturn> M) l1 r1) \<Longrightarrow> ((M \<stileturn> R) l2 r2) \<Longrightarrow> (L \<stileturn> R) (l2 o l1) (r1 o r2)"
by (rule Submission.galois_compI)
lemma refl_fun_rel_galois_propI1: "(L1 \<stileturn> R1) l1 r1 \<Longrightarrow> (L2 \<stileturn> R2) l2 r2 \<Longrightarrow> g \<in> Domain (R1 \<Rrightarrow> R2)\<^sup>\<oplus> \<Longrightarrow> (f, (l1 \<rightarrow> r2) g) \<in> (L1 \<Rrightarrow> L2)\<^sup>\<oplus> \<Longrightarrow> ((r1 \<rightarrow> l2) f, g) \<in> (R1 \<Rrightarrow> R2)\<^sup>\<oplus>"
by (rule Submission.refl_fun_rel_galois_propI1)
lemma refl_fun_rel_galois_propI2: "(L1 \<stileturn> R1) l1 r1 \<Longrightarrow> (L2 \<stileturn> R2) l2 r2 \<Longrightarrow> f \<in> Domain (L1 \<Rrightarrow> L2)\<^sup>\<oplus> \<Longrightarrow> ((r1 \<rightarrow> l2) f, g) \<in> (R1 \<Rrightarrow> R2)\<^sup>\<oplus> \<Longrightarrow> (f, (l1 \<rightarrow> r2) g) \<in> (L1 \<Rrightarrow> L2)\<^sup>\<oplus>"
by (rule Submission.refl_fun_rel_galois_propI2)
theorem galois_refl_fun_relI: "(L1 \<stileturn> R1) l1 r1 \<Longrightarrow> (L2 \<stileturn> R2) l2 r2 \<Longrightarrow> ((L1 \<Rrightarrow> L2)\<^sup>\<oplus> \<stileturn> (R1 \<Rrightarrow> R2)\<^sup>\<oplus>) (r1 \<rightarrow> l2) (l1 \<rightarrow> r2)"
by (rule Submission.galois_refl_fun_relI)
lemma galois_fun_optimal: "(\<And>Y y. Y \<subseteq> Domain R \<Longrightarrow> y \<in> Y \<Longrightarrow> (lbound Y, y) \<in> R) \<Longrightarrow>
refl_on (Domain R) R \<Longrightarrow>
(R \<Rrightarrow>m L) r \<Longrightarrow> (\<And>x y. x \<^bsub>L\<^esub>\<lessapprox>\<^bsub>R r\<^esub> y \<Longrightarrow> f x \<^bsub>L\<^esub>\<lessapprox>\<^bsub>R r\<^esub> f' y) \<Longrightarrow> (R \<Rrightarrow>m R) f' \<Longrightarrow> ((r \<rightarrow> \<lambda>x. lbound {y \<in> Domain R. (x, r y) \<in> L}) f, f') \<in> R \<Rrightarrow> R"
by (rule Submission.galois_fun_optimal)
end