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 13

This is the task corresponding to homework 13.

Resources

Definitions File

```theory Defs
imports "HOL-Library.Extended_Real"
begin

type_synonym val = "ereal option"

datatype bound = NegInf ("\<infinity>\<^sup>-") | PosInf ("\<infinity>\<^sup>+") | NaN | Real

lemma UNIV_bound: "UNIV = {\<infinity>\<^sup>-,\<infinity>\<^sup>+,NaN,Real}"
by (smt (verit, best) UNIV_eq_I bound.exhaust insert_iff)

instantiation bound :: enum
begin

definition "enum_bound = [\<infinity>\<^sup>-,\<infinity>\<^sup>+,NaN,Real]"
definition "enum_all_bound P \<equiv> P \<infinity>\<^sup>- \<and> P \<infinity>\<^sup>+ \<and> P NaN \<and> P Real"
definition "enum_ex_bound P \<equiv> P \<infinity>\<^sup>- \<or> P \<infinity>\<^sup>+ \<or> P NaN \<or> P Real"

instance
by standard (auto simp: enum_bound_def enum_all_bound_def enum_ex_bound_def UNIV_bound)

end

datatype bounds = B "bound set"

fun \<gamma>_bound :: "bound \<Rightarrow> val set" where
"\<gamma>_bound \<infinity>\<^sup>- = {Some (- \<infinity>)}" |
"\<gamma>_bound \<infinity>\<^sup>+ = {Some \<infinity>}" |
"\<gamma>_bound NaN = {None}" |
"\<gamma>_bound Real = {Some r|r. r\<in>\<real>}"

fun \<gamma>_bounds :: "bounds \<Rightarrow> val set" where
"\<gamma>_bounds (B bnds) = \<Union> (\<gamma>_bound ` bnds)"

fun num_bound :: "ereal \<Rightarrow> bound" where
"num_bound PInfty = \<infinity>\<^sup>+" |
"num_bound MInfty = \<infinity>\<^sup>-" |
"num_bound (ereal r) = Real"

definition num_bounds :: "ereal \<Rightarrow> bounds" where
"num_bounds v = B {num_bound v}"

fun plus_bound :: "bound \<Rightarrow> bound \<Rightarrow> bound" where
"plus_bound NaN _ = NaN" |
"plus_bound _ NaN = NaN" |
"plus_bound \<infinity>\<^sup>- \<infinity>\<^sup>+ = NaN" |
"plus_bound \<infinity>\<^sup>+ \<infinity>\<^sup>- = NaN" |
"plus_bound \<infinity>\<^sup>- _ = \<infinity>\<^sup>-" |
"plus_bound _ \<infinity>\<^sup>- = \<infinity>\<^sup>-" |
"plus_bound _ \<infinity>\<^sup>+ = \<infinity>\<^sup>+" |
"plus_bound \<infinity>\<^sup>+ _ = \<infinity>\<^sup>+" |
"plus_bound Real Real = Real"

fun plus_bounds :: "bounds \<Rightarrow> bounds \<Rightarrow> bounds" where
"plus_bounds (B X) (B Y) = B {plus_bound a b | a b. a \<in> X \<and> b \<in> Y}"

lemma minfty_bound[simp]: "Some (- \<infinity>) \<in> \<gamma>_bound bd \<longleftrightarrow> bd = \<infinity>\<^sup>-"
by (cases bd; auto)

lemma pinfty_bound[simp]: "Some (\<infinity>) \<in> \<gamma>_bound bd \<longleftrightarrow> bd = \<infinity>\<^sup>+"
by (cases bd; auto)

lemma NaN_bound[simp]: "None \<in> \<gamma>_bound bd \<longleftrightarrow> bd = NaN"
by (cases bd; auto)

lemma Real_bound[simp]: "Some (ereal r) \<in> \<gamma>_bound bd \<longleftrightarrow> bd = Real"
by (cases bd; auto simp: Reals_def)

consts inv_plus' :: "bounds \<Rightarrow> bounds \<Rightarrow> bounds \<Rightarrow> (bounds * bounds)"

consts inv_less' :: "bool option \<Rightarrow> bounds \<Rightarrow> bounds \<Rightarrow> (bounds * bounds)"

end```

Template File

```theory Submission
imports Defs
begin

fun inv_plus' :: "bounds \<Rightarrow> bounds \<Rightarrow> bounds \<Rightarrow> (bounds * bounds)"  where
"inv_plus' _ = undefined"

fun inv_less' :: "bool option \<Rightarrow> bounds \<Rightarrow> bounds \<Rightarrow> (bounds * bounds)"  where
"inv_less' _ = undefined"

value "inv_plus' (B {NaN}) (B {\<infinity>\<^sup>+}) (B {\<infinity>\<^sup>-, Real}) = (B {\<infinity>\<^sup>+}, B {\<infinity>\<^sup>-})"
value "inv_plus' (B {\<infinity>\<^sup>+,\<infinity>\<^sup>-}) (B {\<infinity>\<^sup>+, NaN}) (B {\<infinity>\<^sup>-, Real, \<infinity>\<^sup>+}) = (B {\<infinity>\<^sup>+}, B {\<infinity>\<^sup>+, Real})"
value "inv_less' (Some True) (B {\<infinity>\<^sup>+, \<infinity>\<^sup>-}) (B {\<infinity>\<^sup>+}) = (B {\<infinity>\<^sup>-}, B {\<infinity>\<^sup>+})"

lemma inv_plus'_sound:
assumes "inv_plus' (B A) (B A1) (B A2) = (B A1', B A2')"
and "i1 \<in> \<gamma>_bounds (B A1)"
and "i2 \<in> \<gamma>_bounds (B A2)"
and "(case (i1,i2) of
(None, _) \<Rightarrow> None \<in> \<gamma>_bounds (B A)
| (_, None) \<Rightarrow> None \<in> \<gamma>_bounds (B A)
| (Some PInfty, Some MInfty) \<Rightarrow> None \<in> \<gamma>_bounds (B A)
| (Some MInfty, Some PInfty) \<Rightarrow> None \<in> \<gamma>_bounds (B A)
| (Some i1, Some i2) \<Rightarrow> Some (i1+i2) \<in> \<gamma>_bounds (B A))"
shows "i1 \<in> \<gamma>_bounds (B A1') \<and> i2 \<in> \<gamma>_bounds (B A2')"
sorry

lemma inv_less'_sound:
assumes "inv_less' bv (B A1) (B A2) = (B A1',B A2')"
and "i1 \<in> \<gamma>_bounds (B A1)"
and "i2 \<in> \<gamma>_bounds (B A2)"
and "(case (i1,i2) of
(None, _) \<Rightarrow> None = bv
| (_, None) \<Rightarrow> None = bv
| (Some i1, Some i2) \<Rightarrow> Some (i1<i2) = bv)"
shows "i1 \<in> \<gamma>_bounds (B A1') \<and> i2 \<in> \<gamma>_bounds (B A2')"
sorry

end```

Check File

```theory Check
imports Submission
begin

lemma inv_plus'_sound: "(inv_plus' (B A) (B A1) (B A2) = (B A1', B A2')) \<Longrightarrow> (i1 \<in> \<gamma>_bounds (B A1)) \<Longrightarrow> (i2 \<in> \<gamma>_bounds (B A2)) \<Longrightarrow> ((case (i1,i2) of
(None, _) \<Rightarrow> None \<in> \<gamma>_bounds (B A)
| (_, None) \<Rightarrow> None \<in> \<gamma>_bounds (B A)
| (Some PInfty, Some MInfty) \<Rightarrow> None \<in> \<gamma>_bounds (B A)
| (Some MInfty, Some PInfty) \<Rightarrow> None \<in> \<gamma>_bounds (B A)
| (Some i1, Some i2) \<Rightarrow> Some (i1+i2) \<in> \<gamma>_bounds (B A))) \<Longrightarrow> i1 \<in> \<gamma>_bounds (B A1') \<and> i2 \<in> \<gamma>_bounds (B A2')"
by (rule Submission.inv_plus'_sound)

lemma inv_less'_sound: "(inv_less' bv (B A1) (B A2) = (B A1',B A2')) \<Longrightarrow> (i1 \<in> \<gamma>_bounds (B A1)) \<Longrightarrow> (i2 \<in> \<gamma>_bounds (B A2)) \<Longrightarrow> ((case (i1,i2) of
(None, _) \<Rightarrow> None = bv
| (_, None) \<Rightarrow> None = bv
| (Some i1, Some i2) \<Rightarrow> Some (i1<i2) = bv)) \<Longrightarrow> i1 \<in> \<gamma>_bounds (B A1') \<and> i2 \<in> \<gamma>_bounds (B A2')"
by (rule Submission.inv_less'_sound)

end```

Terms and Conditions