Cookies disclaimer

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.

Homework 12

This is the task corresponding to homework 12.

Resources

Download Files

Definitions File

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

Template File

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

Check File

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

Terms and Conditions