1(* Title: HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy 2 Author: Fabian Immler, TU M��nchen 3*) 4theory Linear_Algebra_On_With 5 imports 6 Group_On_With 7 Complex_Main 8begin 9 10definition span_with 11 where "span_with pls zero scl b = 12 {sum_with pls zero (\<lambda>a. scl (r a) a) t | t r. finite t \<and> t \<subseteq> b}" 13 14lemma span_with_transfer[transfer_rule]: 15 includes lifting_syntax 16 assumes [transfer_rule]: "right_total A" "bi_unique A" 17 shows "((A ===> A ===> A) ===> A ===> ((=) ===> A ===> A) ===> rel_set A ===> rel_set A) 18 span_with span_with" 19 unfolding span_with_def 20proof (intro rel_funI) 21 fix p p' z z' X X' and s s'::"'c \<Rightarrow> _" 22 assume transfer_rules[transfer_rule]: "(A ===> A ===> A) p p'" "A z z'" "((=) ===> A ===> A) s s'" "rel_set A X X'" 23 have "Domainp A z" using \<open>A z z'\<close> by force 24 have *: "t \<subseteq> X \<Longrightarrow> (\<forall>x\<in>t. Domainp A x)" for t 25 by (meson Domainp.DomainI \<open>rel_set A X X'\<close> rel_setD1 subsetD) 26 note swt=sum_with_transfer[OF assms(1,2,2), THEN rel_funD, THEN rel_funD, THEN rel_funD, THEN rel_funD, OF transfer_rules(1,2)] 27 have DsI: "Domainp A (sum_with p z r t)" if "\<And>x. x \<in> t \<Longrightarrow> Domainp A (r x)" "t \<subseteq> Collect (Domainp A)" for r t 28 proof cases 29 assume ex: "\<exists>C. r ` t \<subseteq> C \<and> comm_monoid_add_on_with C p z" 30 have "Domainp (rel_set A) t" using that by (auto simp: Domainp_set) 31 from ex_comm_monoid_add_around_imageE[OF ex transfer_rules(1,2) this that(1)] 32 obtain C where C: "comm_monoid_add_on_with C p z" "r ` t \<subseteq> C" "Domainp (rel_set A) C" by auto 33 interpret comm_monoid_add_on_with C p z by fact 34 from sum_with_mem[OF C(2)] C(3) 35 show ?thesis 36 by auto (meson C(3) Domainp_set) 37 qed (use \<open>A z _\<close> in \<open>auto simp: sum_with_def\<close>) 38 from Domainp_apply2I[OF transfer_rules(3)] 39 have Domainp_sI: "Domainp A x \<Longrightarrow> Domainp A (s y x)" for x y by auto 40 show "rel_set A 41 {sum_with p z (\<lambda>a. s (r a) a) t |t r. finite t \<and> t \<subseteq> X} 42 {sum_with p' z' (\<lambda>a. s' (r a) a) t |t r. finite t \<and> t \<subseteq> X'}" 43 apply (transfer_prover_start, transfer_step+) 44 using * 45 by (auto simp: intro!: DsI Domainp_sI) 46qed 47 48definition dependent_with 49 where "dependent_with pls zero scl s = 50 (\<exists>t u. finite t \<and> t \<subseteq> s \<and> (sum_with pls zero (\<lambda>v. scl (u v) v) t = zero \<and> (\<exists>v\<in>t. u v \<noteq> 0)))" 51 52lemma dependent_with_transfer[transfer_rule]: 53 includes lifting_syntax 54 assumes [transfer_rule]: "right_total A" "bi_unique A" 55 shows "((A ===> A ===> A) ===> A ===> ((=) ===> A ===> A) ===> rel_set A ===> (=)) 56 dependent_with dependent_with" 57 unfolding dependent_with_def dependent_with_def 58proof (intro rel_funI) 59 fix p p' z z' X X' and s s'::"'c \<Rightarrow> _" 60 assume [transfer_rule]: "(A ===> A ===> A) p p'" "A z z'" "((=) ===> A ===> A) s s'" "rel_set A X X'" 61 have *: "t \<subseteq> X \<Longrightarrow> (\<forall>x\<in>t. Domainp A x)" for t 62 by (meson Domainp.DomainI \<open>rel_set A X X'\<close> rel_setD1 subsetD) 63 show "(\<exists>t u. finite t \<and> t \<subseteq> X \<and> sum_with p z (\<lambda>v. s (u v) v) t = z \<and> (\<exists>v\<in>t. u v \<noteq> 0)) = 64 (\<exists>t u. finite t \<and> t \<subseteq> X' \<and> sum_with p' z' (\<lambda>v. s' (u v) v) t = z' \<and> (\<exists>v\<in>t. u v \<noteq> 0))" 65 apply (transfer_prover_start, transfer_step+) 66 using * 67 by (auto simp: intro!: comm_monoid_add_on_with.sum_with_mem) 68qed 69 70definition subspace_with 71 where "subspace_with pls zero scl S \<longleftrightarrow> zero \<in> S \<and> (\<forall>x\<in>S. \<forall>y\<in>S. pls x y \<in> S) \<and> (\<forall>c. \<forall>x\<in>S. scl c x \<in> S)" 72 73lemma subspace_with_transfer[transfer_rule]: 74 includes lifting_syntax 75 assumes [transfer_rule]: "bi_unique A" 76 shows "((A ===> A ===> A) ===> A ===> ((=) ===> A ===> A) ===> rel_set A ===> (=)) 77 subspace_with subspace_with" 78 unfolding span_with_def subspace_with_def 79 by transfer_prover 80 81definition "module_on_with S pls mns um zero (scl::'a::comm_ring_1\<Rightarrow>_) \<longleftrightarrow> 82 ab_group_add_on_with S pls zero mns um \<and> 83 ((\<forall>a. \<forall>x\<in>S. 84 \<forall>y\<in>S. scl a (pls x y) = pls (scl a x) (scl a y)) \<and> 85 (\<forall>a b. \<forall>x\<in>S. scl (a + b) x = pls (scl a x) (scl b x))) \<and> 86 (\<forall>a b. \<forall>x\<in>S. scl a (scl b x) = scl (a * b) x) \<and> 87 (\<forall>x\<in>S. scl 1 x = x) \<and> 88 (\<forall>a. \<forall>x\<in>S. scl a x \<in> S)" 89 90definition "vector_space_on_with S pls mns um zero (scl::'a::field\<Rightarrow>_) \<longleftrightarrow> 91 module_on_with S pls mns um zero scl" 92 93definition "module_pair_on_with S S' pls mns um zero (scl::'a::comm_ring_1\<Rightarrow>_) pls' mns' um' zero' (scl'::'a::comm_ring_1\<Rightarrow>_) \<longleftrightarrow> 94 module_on_with S pls mns um zero scl \<and> module_on_with S' pls' mns' um' zero' scl'" 95 96definition "vector_space_pair_on_with S S' pls mns um zero (scl::'a::field\<Rightarrow>_) pls' mns' um' zero' (scl'::'a::field\<Rightarrow>_) \<longleftrightarrow> 97 module_pair_on_with S S' pls mns um zero scl pls' mns' um' zero' scl'" 98 99definition "module_hom_on_with S1 S2 plus1 minus1 uminus1 zero1 (scale1::'a::comm_ring_1\<Rightarrow>_) 100 plus2 minus2 uminus2 zero2 (scale2::'a::comm_ring_1\<Rightarrow>_) f \<longleftrightarrow> 101 module_pair_on_with S1 S2 plus1 minus1 uminus1 zero1 scale1 102 plus2 minus2 uminus2 zero2 scale2 \<and> 103 (\<forall>x\<in>S1. \<forall>y\<in>S1. f (plus1 x y) = plus2 (f x) (f y)) \<and> 104 (\<forall>s. \<forall>x\<in>S1. f (scale1 s x) = scale2 s (f x))" 105 106definition "linear_on_with S1 S2 plus1 minus1 uminus1 zero1 (scale1::'a::field\<Rightarrow>_) 107 plus2 minus2 uminus2 zero2 (scale2::'a::field\<Rightarrow>_) f \<longleftrightarrow> 108 module_hom_on_with S1 S2 plus1 minus1 uminus1 zero1 scale1 109 plus2 minus2 uminus2 zero2 scale2 f" 110 111definition dim_on_with 112 where "dim_on_with S pls zero scale V = 113 (if \<exists>b \<subseteq> S. \<not> dependent_with pls zero scale b \<and> span_with pls zero scale b = span_with pls zero scale V 114 then card (SOME b. b \<subseteq> S \<and>\<not> dependent_with pls zero scale b \<and> span_with pls zero scale b = span_with pls zero scale V) 115 else 0)" 116 117definition "finite_dimensional_vector_space_on_with S pls mns um zero (scl::'a::field\<Rightarrow>_) basis \<longleftrightarrow> 118 vector_space_on_with S pls mns um zero scl \<and> 119 finite basis \<and> 120 \<not> dependent_with pls zero scl basis \<and> 121 span_with pls zero scl basis = S" 122 123definition "finite_dimensional_vector_space_pair_1_on_with S S' pls mns um zero (scl::'a::field\<Rightarrow>_) b 124 pls' mns' um' zero' (scl'::'a::field\<Rightarrow>_) \<longleftrightarrow> 125 finite_dimensional_vector_space_on_with S pls mns um zero (scl::'a::field\<Rightarrow>_) b \<and> 126 vector_space_on_with S' pls' mns' um' zero' (scl'::'a::field\<Rightarrow>_)" 127 128definition "finite_dimensional_vector_space_pair_on_with S S' pls mns um zero (scl::'a::field\<Rightarrow>_) b 129 pls' mns' um' zero' (scl'::'a::field\<Rightarrow>_) b' \<longleftrightarrow> 130 finite_dimensional_vector_space_on_with S pls mns um zero (scl::'a::field\<Rightarrow>_) b \<and> 131 finite_dimensional_vector_space_on_with S' pls' mns' um' zero' (scl'::'a::field\<Rightarrow>_) b'" 132 133context module begin 134 135lemma span_with: 136 "span = (\<lambda>X. span_with (+) 0 scale X)" 137 unfolding span_explicit span_with_def sum_with .. 138 139lemma dependent_with: 140 "dependent = (\<lambda>X. dependent_with (+) 0 scale X)" 141 unfolding dependent_explicit dependent_with_def sum_with .. 142 143lemma subspace_with: 144 "subspace = (\<lambda>X. subspace_with (+) 0 scale X)" 145 unfolding subspace_def subspace_with_def .. 146 147end 148 149lemmas [explicit_ab_group_add] = module.span_with module.dependent_with module.subspace_with 150 151lemma module_on_with_transfer[transfer_rule]: 152 includes lifting_syntax 153 assumes [transfer_rule]: "right_total A" "bi_unique A" 154 shows 155 "(rel_set A ===> (A ===> A ===> A) ===> (A ===> A ===> A) ===> (A ===> A) ===> A ===> ((=) ===> A ===> A) ===> (=)) 156 module_on_with module_on_with" 157 unfolding module_on_with_def 158 by transfer_prover 159 160lemma vector_space_on_with_transfer[transfer_rule]: 161 includes lifting_syntax 162 assumes [transfer_rule]: "right_total A" "bi_unique A" 163 shows 164 "(rel_set A ===> (A ===> A ===> A) ===> (A ===> A ===> A) ===> (A ===> A) ===> A ===> ((=) ===> A ===> A) ===> (=)) 165 vector_space_on_with vector_space_on_with" 166 unfolding vector_space_on_with_def 167 by transfer_prover 168 169context vector_space begin 170 171lemma dim_with: "dim = (\<lambda>X. dim_on_with UNIV (+) 0 scale X)" 172 unfolding dim_def dim_on_with_def dependent_with span_with by force 173 174end 175 176lemmas [explicit_ab_group_add] = vector_space.dim_with 177 178lemma module_pair_on_with_transfer[transfer_rule]: 179 includes lifting_syntax 180 assumes [transfer_rule]: "right_total A" "bi_unique A" "right_total C" "bi_unique C" 181 shows 182 "(rel_set A ===> rel_set C ===> 183 (A ===> A ===> A) ===> (A ===> A ===> A) ===> (A ===> A) ===> A ===> ((=) ===> A ===> A) ===> 184 (C ===> C ===> C) ===> (C ===> C ===> C) ===> (C ===> C) ===> C ===> ((=) ===> C ===> C) ===> 185 (=)) module_pair_on_with module_pair_on_with" 186 unfolding module_pair_on_with_def 187 by transfer_prover 188 189lemma module_hom_on_with_transfer[transfer_rule]: 190 includes lifting_syntax 191 assumes [transfer_rule]: "right_total A" "bi_unique A" "right_total C" "bi_unique C" 192 shows 193 "(rel_set A ===> rel_set C ===> 194 (A ===> A ===> A) ===> (A ===> A ===> A) ===> (A ===> A) ===> A ===> ((=) ===> A ===> A) ===> 195 (C ===> C ===> C) ===> (C ===> C ===> C) ===> (C ===> C) ===> C ===> ((=) ===> C ===> C) ===> 196 (A ===> C) ===> (=)) module_hom_on_with module_hom_on_with" 197 unfolding module_hom_on_with_def 198 by transfer_prover 199 200lemma linear_on_with_transfer[transfer_rule]: 201 includes lifting_syntax 202 assumes [transfer_rule]: "right_total A" "bi_unique A" "right_total C" "bi_unique C" 203 shows 204 "(rel_set A ===> rel_set C ===> 205 (A ===> A ===> A) ===> (A ===> A ===> A) ===> (A ===> A) ===> A ===> ((=) ===> A ===> A) ===> 206 (C ===> C ===> C) ===> (C ===> C ===> C) ===> (C ===> C) ===> C ===> ((=) ===> C ===> C) ===> 207 (A ===> C) ===> (=)) linear_on_with linear_on_with" 208 unfolding linear_on_with_def 209 by transfer_prover 210 211subsubsection \<open>Explicit locale formulations\<close> 212 213lemma module_on_with[explicit_ab_group_add]: "module s \<longleftrightarrow> module_on_with UNIV (+) (-) uminus 0 s" 214 and vector_space_on_with[explicit_ab_group_add]: "vector_space t \<longleftrightarrow> vector_space_on_with UNIV (+) (-) uminus 0 t" 215 by (auto simp: module_def module_on_with_def ab_group_add_axioms 216 vector_space_def vector_space_on_with_def) 217 218lemma vector_space_with_imp_module_with[explicit_ab_group_add]: 219 "vector_space_on_with S (+) (-) uminus 0 s \<Longrightarrow> module_on_with S (+) (-) uminus 0 s" 220 by (simp add: vector_space_on_with_def) 221 222lemma finite_dimensional_vector_space_on_with[explicit_ab_group_add]: 223 "finite_dimensional_vector_space t b \<longleftrightarrow> finite_dimensional_vector_space_on_with UNIV (+) (-) uminus 0 t b" 224 by (auto simp: finite_dimensional_vector_space_on_with_def finite_dimensional_vector_space_def 225 finite_dimensional_vector_space_axioms_def explicit_ab_group_add) 226 227lemma vector_space_with_imp_finite_dimensional_vector_space_with[explicit_ab_group_add]: 228 "finite_dimensional_vector_space_on_with S (+) (-) uminus 0 s basis \<Longrightarrow> 229 vector_space_on_with S (+) (-) uminus 0 s" 230 by (auto simp: finite_dimensional_vector_space_on_with_def) 231 232lemma module_hom_on_with[explicit_ab_group_add]: 233 "module_hom s1 s2 f \<longleftrightarrow> module_hom_on_with UNIV UNIV (+) (-) uminus 0 s1 (+) (-) uminus 0 s2 f" 234 and linear_with[explicit_ab_group_add]: 235 "Vector_Spaces.linear t1 t2 f \<longleftrightarrow> linear_on_with UNIV UNIV (+) (-) uminus 0 t1 (+) (-) uminus 0 t2 f" 236 and module_pair_on_with[explicit_ab_group_add]: 237 "module_pair s1 s2 \<longleftrightarrow> module_pair_on_with UNIV UNIV (+) (-) uminus 0 s1 (+) (-) uminus 0 s2" 238 by (auto simp: module_hom_def module_hom_on_with_def module_pair_on_with_def 239 Vector_Spaces.linear_def linear_on_with_def vector_space_on_with 240 module_on_with_def vector_space_on_with_def 241 module_hom_axioms_def module_pair_def module_on_with) 242 243lemma vector_space_pair_with[explicit_ab_group_add]: 244 "vector_space_pair s1 s2 \<longleftrightarrow> vector_space_pair_on_with UNIV UNIV (+) (-) uminus 0 s1 (+) (-) uminus 0 s2" 245 by (auto simp: module_pair_on_with_def explicit_ab_group_add 246 vector_space_pair_on_with_def vector_space_pair_def module_on_with_def vector_space_on_with_def) 247 248lemma finite_dimensional_vector_space_pair_1_with[explicit_ab_group_add]: 249 "finite_dimensional_vector_space_pair_1 s1 b1 s2 \<longleftrightarrow> 250 finite_dimensional_vector_space_pair_1_on_with UNIV UNIV (+) (-) uminus 0 s1 b1 (+) (-) uminus 0 s2" 251 by (auto simp: finite_dimensional_vector_space_pair_1_def 252 finite_dimensional_vector_space_pair_1_on_with_def finite_dimensional_vector_space_on_with 253 vector_space_on_with) 254 255lemma finite_dimensional_vector_space_pair_with[explicit_ab_group_add]: 256 "finite_dimensional_vector_space_pair s1 b1 s2 b2 \<longleftrightarrow> 257 finite_dimensional_vector_space_pair_on_with UNIV UNIV (+) (-) uminus 0 s1 b1 (+) (-) uminus 0 s2 b2" 258 by (auto simp: finite_dimensional_vector_space_pair_def 259 finite_dimensional_vector_space_pair_on_with_def finite_dimensional_vector_space_on_with) 260 261 262lemma module_pair_with_imp_module_with[explicit_ab_group_add]: 263 "module_on_with S (+) (-) uminus 0 s" 264 "module_on_with T (+) (-) uminus 0 t" 265 if "module_pair_on_with S T (+) (-) uminus 0 s (+) (-) uminus 0 t" 266 using that 267 unfolding module_pair_on_with_def 268 by simp_all 269 270lemma vector_space_pair_with_imp_vector_space_with[explicit_ab_group_add]: 271 "vector_space_on_with S (+) (-) uminus 0 s" 272 "vector_space_on_with T (+) (-) uminus 0 t" 273 if "vector_space_pair_on_with S T(+) (-) uminus 0 s (+) (-) uminus 0 t" 274 using that 275 by (auto simp: vector_space_pair_on_with_def module_pair_on_with_def vector_space_on_with_def) 276 277lemma finite_dimensional_vector_space_pair_1_with_imp_with[explicit_ab_group_add]: 278 "vector_space_on_with S (+) (-) uminus 0 s" 279 "finite_dimensional_vector_space_on_with S (+) (-) uminus 0 s b" 280 "vector_space_on_with T (+) (-) uminus 0 t" 281 if "finite_dimensional_vector_space_pair_1_on_with S T (+) (-) uminus 0 s b (+) (-) uminus 0 t" 282 using that 283 unfolding finite_dimensional_vector_space_pair_1_on_with_def 284 by (simp_all add: finite_dimensional_vector_space_on_with_def) 285 286lemma finite_dimensional_vector_space_pair_with_imp_finite_dimensional_vector_space_with[explicit_ab_group_add]: 287 "vector_space_on_with S (+) (-) uminus 0 s" 288 "finite_dimensional_vector_space_on_with T (+) (-) uminus 0 t c" 289 "vector_space_on_with T (+) (-) uminus 0 t" 290 "finite_dimensional_vector_space_on_with T (+) (-) uminus 0 t c" 291 if "finite_dimensional_vector_space_pair_on_with S T (+) (-) uminus 0 s b (+) (-) uminus 0 t c" 292 using that 293 unfolding finite_dimensional_vector_space_pair_on_with_def 294 by (simp_all add: finite_dimensional_vector_space_on_with_def) 295 296lemma finite_dimensional_vector_space_on_with_transfer[transfer_rule]: 297 includes lifting_syntax 298 assumes [transfer_rule]: "right_total A" "bi_unique A" 299 shows 300 "(rel_set A ===> 301 (A ===> A ===> A) ===> (A ===> A ===> A) ===> (A ===> A) ===> A ===> ((=) ===> A ===> A) ===> 302 rel_set A ===> 303 (=)) (finite_dimensional_vector_space_on_with) finite_dimensional_vector_space_on_with" 304 unfolding finite_dimensional_vector_space_on_with_def 305 by transfer_prover 306 307lemma finite_dimensional_vector_space_pair_on_with_transfer[transfer_rule]: 308 includes lifting_syntax 309 assumes [transfer_rule]: "right_total A" "bi_unique A" "right_total C" "bi_unique C" 310 shows 311 "(rel_set A ===> rel_set C ===> 312 (A ===> A ===> A) ===> (A ===> A ===> A) ===> (A ===> A) ===> A ===> ((=) ===> A ===> A) ===> 313 rel_set A ===> 314 (C ===> C ===> C) ===> (C ===> C ===> C) ===> (C ===> C) ===> C ===> ((=) ===> C ===> C) ===> 315 rel_set C ===> 316 (=)) (finite_dimensional_vector_space_pair_on_with) finite_dimensional_vector_space_pair_on_with" 317 unfolding finite_dimensional_vector_space_pair_on_with_def 318 by transfer_prover 319 320end