1(* Title: HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy 2 Author: Fabian Immler, TU M��nchen 3*) 4theory Linear_Algebra_On 5 imports 6 "Prerequisites" 7 "../Types_To_Sets" 8 Linear_Algebra_On_With 9begin 10 11subsection \<open>Rewrite rules to make \<open>ab_group_add\<close> operations implicit.\<close> 12 13named_theorems implicit_ab_group_add 14 15lemmas [implicit_ab_group_add] = sum_with[symmetric] 16 17lemma semigroup_add_on_with_eq[implicit_ab_group_add]: 18 "semigroup_add_on_with S ((+)::_::semigroup_add \<Rightarrow> _) \<longleftrightarrow> (\<forall>a\<in>S. \<forall>b\<in>S. a + b \<in> S)" 19 by (simp add: semigroup_add_on_with_Ball_def ac_simps) 20 21lemma ab_semigroup_add_on_with_eq[implicit_ab_group_add]: 22 "ab_semigroup_add_on_with S ((+)::_::ab_semigroup_add \<Rightarrow> _) = semigroup_add_on_with S (+)" 23 unfolding ab_semigroup_add_on_with_Ball_def 24 by (simp add: semigroup_add_on_with_eq ac_simps) 25 26lemma comm_monoid_add_on_with_eq[implicit_ab_group_add]: 27 "comm_monoid_add_on_with S ((+)::_::comm_monoid_add \<Rightarrow> _) 0 \<longleftrightarrow> semigroup_add_on_with S (+) \<and> 0 \<in> S" 28 unfolding comm_monoid_add_on_with_Ball_def 29 by (simp add: ab_semigroup_add_on_with_eq ac_simps) 30 31lemma ab_group_add_on_with[implicit_ab_group_add]: 32 "ab_group_add_on_with S ((+)::_::ab_group_add \<Rightarrow> _) 0 (-) uminus \<longleftrightarrow> 33 comm_monoid_add_on_with S (+) 0 \<and> (\<forall>a\<in>S. -a\<in>S)" 34 unfolding ab_group_add_on_with_Ball_def 35 by simp 36 37subsection \<open>Definitions \<^emph>\<open>on\<close> carrier set\<close> 38 39locale module_on = 40 fixes S and scale :: "'a::comm_ring_1 \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*s" 75) 41 assumes scale_right_distrib_on [algebra_simps]: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> a *s (x + y) = a *s x + a *s y" 42 and scale_left_distrib_on [algebra_simps]: "x \<in> S \<Longrightarrow> (a + b) *s x = a *s x + b *s x" 43 and scale_scale_on [simp]: "x \<in> S \<Longrightarrow> a *s (b *s x) = (a * b) *s x" 44 and scale_one_on [simp]: "x \<in> S \<Longrightarrow> 1 *s x = x" 45 and mem_add: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x + y \<in> S" 46 and mem_zero: "0 \<in> S" 47 and mem_scale: "x \<in> S \<Longrightarrow> a *s x \<in> S" 48begin 49 50lemma S_ne: "S \<noteq> {}" using mem_zero by auto 51 52lemma scale_minus_left_on: "scale (- a) x = - scale a x" if "x \<in> S" 53 by (metis add_cancel_right_right scale_left_distrib_on neg_eq_iff_add_eq_0 that) 54 55lemma mem_uminus: "x \<in> S \<Longrightarrow> -x \<in> S" 56 by (metis mem_scale scale_minus_left_on scale_one_on) 57 58definition subspace :: "'b set \<Rightarrow> bool" 59 where subspace_on_def: "subspace T \<longleftrightarrow> 0 \<in> T \<and> (\<forall>x\<in>T. \<forall>y\<in>T. x + y \<in> T) \<and> (\<forall>c. \<forall>x\<in>T. c *s x \<in> T)" 60 61definition span :: "'b set \<Rightarrow> 'b set" 62 where span_on_def: "span b = {sum (\<lambda>a. r a *s a) t | t r. finite t \<and> t \<subseteq> b}" 63 64definition dependent :: "'b set \<Rightarrow> bool" 65 where dependent_on_def: "dependent s \<longleftrightarrow> (\<exists>t u. finite t \<and> t \<subseteq> s \<and> (sum (\<lambda>v. u v *s v) t = 0 \<and> (\<exists>v\<in>t. u v \<noteq> 0)))" 66 67lemma implicit_subspace_with[implicit_ab_group_add]: "subspace_with (+) 0 (*s) = subspace" 68 unfolding subspace_on_def subspace_with_def .. 69 70lemma implicit_dependent_with[implicit_ab_group_add]: "dependent_with (+) 0 (*s) = dependent" 71 unfolding dependent_on_def dependent_with_def sum_with .. 72 73lemma implicit_span_with[implicit_ab_group_add]: "span_with (+) 0 (*s) = span" 74 unfolding span_on_def span_with_def sum_with .. 75 76end 77 78lemma implicit_module_on_with[implicit_ab_group_add]: 79 "module_on_with S (+) (-) uminus 0 = module_on S" 80proof (intro ext iffI) 81 fix s::"'a\<Rightarrow>'b\<Rightarrow>'b" assume "module_on S s" 82 then interpret module_on S s . 83 show "module_on_with S (+) (-) uminus 0 s" 84 by (auto simp: module_on_with_def implicit_ab_group_add 85 mem_add mem_zero mem_uminus scale_right_distrib_on scale_left_distrib_on mem_scale) 86qed (auto simp: module_on_with_def module_on_def implicit_ab_group_add) 87 88locale module_pair_on = m1: module_on S1 scale1 + 89 m2: module_on S2 scale2 90 for S1:: "'b::ab_group_add set" and S2::"'c::ab_group_add set" 91 and scale1::"'a::comm_ring_1 \<Rightarrow> _" and scale2::"'a \<Rightarrow> _" 92 93lemma implicit_module_pair_on_with[implicit_ab_group_add]: 94 "module_pair_on_with S1 S2 (+) (-) uminus 0 s1 (+) (-) uminus 0 s2 = module_pair_on S1 S2 s1 s2" 95 unfolding module_pair_on_with_def implicit_module_on_with module_pair_on_def .. 96 97locale module_hom_on = m1: module_on S1 s1 + m2: module_on S2 s2 98 for S1 :: "'b::ab_group_add set" and S2 :: "'c::ab_group_add set" 99 and s1 :: "'a::comm_ring_1 \<Rightarrow> 'b \<Rightarrow> 'b" (infixr "*a" 75) 100 and s2 :: "'a::comm_ring_1 \<Rightarrow> 'c \<Rightarrow> 'c" (infixr "*b" 75) + 101 fixes f :: "'b \<Rightarrow> 'c" 102 assumes add: "\<And>b1 b2. b1 \<in> S1 \<Longrightarrow> b2 \<in> S1 \<Longrightarrow> f (b1 + b2) = f b1 + f b2" 103 and scale: "\<And>b. b \<in> S1 \<Longrightarrow> f (r *a b) = r *b f b" 104 105lemma implicit_module_hom_on_with[implicit_ab_group_add]: 106 "module_hom_on_with S1 S2 (+) (-) uminus 0 s1 (+) (-) uminus 0 s2 = module_hom_on S1 S2 s1 s2" 107 unfolding module_hom_on_with_def implicit_module_pair_on_with module_hom_on_def module_pair_on_def 108 module_hom_on_axioms_def 109 by (auto intro!: ext) 110 111locale vector_space_on = module_on S scale 112 for S and scale :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*s" 75) 113begin 114 115definition dim :: "'b set \<Rightarrow> nat" 116 where "dim V = (if \<exists>b\<subseteq>S. \<not> dependent b \<and> span b = span V 117 then card (SOME b. b \<subseteq> S \<and> \<not> dependent b \<and> span b = span V) 118 else 0)" 119 120lemma implicit_dim_with[implicit_ab_group_add]: "dim_on_with S (+) 0 (*s) = dim" 121 unfolding dim_on_with_def dim_def implicit_ab_group_add .. 122 123end 124 125lemma vector_space_on_alt_def: "vector_space_on S = module_on S" 126 unfolding vector_space_on_def module_on_def 127 by auto 128 129lemma implicit_vector_space_on_with[implicit_ab_group_add]: 130 "vector_space_on_with S (+) (-) uminus 0 = vector_space_on S" 131 unfolding vector_space_on_alt_def vector_space_on_def vector_space_on_with_def implicit_module_on_with .. 132 133locale linear_on = module_hom_on S1 S2 s1 s2 f 134 for S1 S2 and s1::"'a::field \<Rightarrow> 'b \<Rightarrow> 'b::ab_group_add" 135 and s2::"'a::field \<Rightarrow> 'c \<Rightarrow> 'c::ab_group_add" 136 and f 137 138lemma implicit_linear_on_with[implicit_ab_group_add]: 139 "linear_on_with S1 S2 (+) (-) uminus 0 s1 (+) (-) uminus 0 s2 = linear_on S1 S2 s1 s2" 140 unfolding linear_on_with_def linear_on_def implicit_module_hom_on_with .. 141 142locale finite_dimensional_vector_space_on = vector_space_on S scale for S scale + 143 fixes basis :: "'a set" 144 assumes finite_Basis: "finite basis" 145 and independent_Basis: "\<not> dependent basis" 146 and span_Basis: "span basis = S" and basis_subset: "basis \<subseteq> S" 147 148locale vector_space_pair_on = m1: vector_space_on S1 scale1 + 149 m2: vector_space_on S2 scale2 150 for S1:: "'b::ab_group_add set" and S2::"'c::ab_group_add set" 151 and scale1::"'a::field \<Rightarrow> _" and scale2::"'a \<Rightarrow> _" 152 153locale finite_dimensional_vector_space_pair_1_on = 154 vs1: finite_dimensional_vector_space_on S1 scale1 Basis1 + 155 vs2: vector_space_on S2 scale2 156 for S1 S2 157 and scale1::"'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" 158 and scale2::"'a::field \<Rightarrow> 'c::ab_group_add \<Rightarrow> 'c" 159 and Basis1 160 161locale finite_dimensional_vector_space_pair_on = 162 vs1: finite_dimensional_vector_space_on S1 scale1 Basis1 + 163 vs2: finite_dimensional_vector_space_on S2 scale2 Basis2 164 for S1 S2 165 and scale1::"'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" 166 and scale2::"'a::field \<Rightarrow> 'c::ab_group_add \<Rightarrow> 'c" 167 and Basis1 Basis2 168 169 170subsection \<open>Local Typedef for Subspace\<close> 171 172locale local_typedef_module_on = module_on S scale 173 for S and scale::"'a::comm_ring_1\<Rightarrow>'b\<Rightarrow>'b::ab_group_add" and s::"'s itself" + 174 assumes Ex_type_definition_S: "\<exists>(Rep::'s \<Rightarrow> 'b) (Abs::'b \<Rightarrow> 's). type_definition Rep Abs S" 175begin 176 177lemma mem_sum: "sum f X \<in> S" if "\<And>x. x \<in> X \<Longrightarrow> f x \<in> S" 178 using that 179 by (induction X rule: infinite_finite_induct) (auto intro!: mem_zero mem_add) 180 181sublocale local_typedef S "TYPE('s)" 182 using Ex_type_definition_S by unfold_locales 183 184sublocale local_typedef_ab_group_add_on_with "(+)::'b\<Rightarrow>'b\<Rightarrow>'b" "0::'b" "(-)" uminus S "TYPE('s)" 185 using mem_zero mem_add mem_scale[of _ "-1"] 186 by unfold_locales (auto simp: scale_minus_left_on) 187 188context includes lifting_syntax begin 189 190definition scale_S::"'a \<Rightarrow> 's \<Rightarrow> 's" where "scale_S = (id ---> rep ---> Abs) scale" 191 192lemma scale_S_transfer[transfer_rule]: "((=) ===> cr_S ===> cr_S) scale scale_S" 193 unfolding scale_S_def 194 by (auto simp: cr_S_def mem_scale intro!: rel_funI) 195 196end 197 198lemma type_module_on_with: "module_on_with UNIV plus_S minus_S uminus_S (zero_S::'s) scale_S" 199proof - 200 have "module_on_with {x. x \<in> S} (+) (-) uminus 0 scale" 201 using module_on_axioms 202 by (auto simp: module_on_with_def module_on_def ab_group_add_on_with_Ball_def 203 comm_monoid_add_on_with_Ball_def mem_uminus 204 ab_semigroup_add_on_with_Ball_def semigroup_add_on_with_def) 205 then show ?thesis 206 by transfer' 207qed 208 209lemma UNIV_transfer[transfer_rule]: "(rel_set cr_S) S UNIV" 210 by (auto simp: rel_set_def cr_S_def) (metis Abs_inverse) 211 212end 213 214context includes lifting_syntax begin 215 216lemma Eps_unique_transfer_lemma: 217 "f' (Eps (\<lambda>x. Domainp A x \<and> f x)) = g' (Eps g)" 218 if [transfer_rule]: "right_total A" "(A ===> (=)) f g" "(A ===> (=)) f' g'" 219 and holds: "\<exists>x. Domainp A x \<and> f x" 220 and unique_g: "\<And>x y. g x \<Longrightarrow> g y \<Longrightarrow> g' x = g' y" 221proof - 222 define Epsg where "Epsg = Eps g" 223 have "\<exists>x. g x" 224 by transfer (simp add: holds) 225 then have "g Epsg" 226 unfolding Epsg_def 227 by (rule someI_ex) 228 obtain x where x[transfer_rule]: "A x Epsg" 229 by (meson \<open>right_total A\<close> right_totalE) 230 then have "Domainp A x" by auto 231 from \<open>g Epsg\<close>[untransferred] have "f x" . 232 from unique_g have unique: 233 "\<And>x y. Domainp A x \<Longrightarrow> Domainp A y \<Longrightarrow> f x \<Longrightarrow> f y \<Longrightarrow> f' x = f' y" 234 by transfer 235 have "f' (Eps (\<lambda>x. Domainp A x \<and> f x)) = f' x" 236 apply (rule unique[OF _ \<open>Domainp A x\<close> _ \<open>f x\<close>]) 237 apply (metis (mono_tags, lifting) local.holds someI_ex) 238 apply (metis (mono_tags, lifting) local.holds someI_ex) 239 done 240 show "f' (SOME x. Domainp A x \<and> f x) = g' (Eps g)" 241 using x \<open>f' (Eps _) = f' x\<close> Epsg_def 242 using rel_funE that(3) by fastforce 243qed 244 245end 246 247locale local_typedef_vector_space_on = local_typedef_module_on S scale s + vector_space_on S scale 248 for S and scale::"'a::field\<Rightarrow>'b\<Rightarrow>'b::ab_group_add" and s::"'s itself" 249begin 250 251lemma type_vector_space_on_with: "vector_space_on_with UNIV plus_S minus_S uminus_S (zero_S::'s) scale_S" 252 using type_module_on_with 253 by (auto simp: vector_space_on_with_def) 254 255context includes lifting_syntax begin 256 257definition dim_S::"'s set \<Rightarrow> nat" where "dim_S = dim_on_with UNIV plus_S zero_S scale_S" 258 259lemma transfer_dim[transfer_rule]: "(rel_set cr_S ===> (=)) dim dim_S" 260proof (rule rel_funI) 261 fix V V' 262 assume [transfer_rule]: "rel_set cr_S V V'" 263 then have subset: "V \<subseteq> S" 264 by (auto simp: rel_set_def cr_S_def) 265 then have "span V \<subseteq> S" 266 by (auto simp: span_on_def intro!: mem_sum mem_scale) 267 note type_dim_eq_card = 268 vector_space.dim_eq_card[var_simplified explicit_ab_group_add, unoverload_type 'd, 269 OF type.ab_group_add_axioms type_vector_space_on_with] 270 have *: "(\<exists>b\<subseteq>UNIV. \<not> dependent_with plus_S zero_S scale_S b \<and> span_with plus_S zero_S scale_S b = span_with plus_S zero_S scale_S V') \<longleftrightarrow> 271 (\<exists>b\<subseteq>S. \<not> local.dependent b \<and> local.span b = local.span V)" 272 unfolding subset_iff 273 by transfer (simp add: implicit_ab_group_add Ball_def) 274 have **[symmetric]: 275 "card (SOME b. Domainp (rel_set cr_S) b \<and> (\<not> dependent_with (+) 0 scale b \<and> span_with (+) 0 scale b = span_with (+) 0 scale V)) = 276 card (SOME b. \<not> dependent_with plus_S zero_S scale_S b \<and> span_with plus_S zero_S scale_S b = span_with plus_S zero_S scale_S V')" 277 if "b \<subseteq> S" "\<not>dependent b" "span b = span V" for b 278 apply (rule Eps_unique_transfer_lemma[where f'=card and g'=card]) 279 subgoal by (rule right_total_rel_set) (rule transfer_raw) 280 subgoal by transfer_prover 281 subgoal by transfer_prover 282 subgoal using that by (auto simp: implicit_ab_group_add Domainp_set Domainp_cr_S) 283 subgoal premises prems for b c 284 proof - 285 from type_dim_eq_card[of b V'] type_dim_eq_card[of c V'] prems 286 show ?thesis by simp 287 qed 288 done 289 show "local.dim V = dim_S V'" 290 unfolding dim_def dim_S_def * dim_on_with_def 291 by (auto simp: ** Domainp_set Domainp_cr_S implicit_ab_group_add subset_eq) 292qed 293 294end 295 296 297end 298 299locale local_typedef_finite_dimensional_vector_space_on = local_typedef_vector_space_on S scale s + 300 finite_dimensional_vector_space_on S scale Basis 301 for S and scale::"'a::field\<Rightarrow>'b\<Rightarrow>'b::ab_group_add" and Basis and s::"'s itself" 302begin 303 304definition "Basis_S = Abs ` Basis" 305 306lemma Basis_S_transfer[transfer_rule]: "rel_set cr_S Basis Basis_S" 307 using Abs_inverse rep_inverse basis_subset 308 by (force simp: rel_set_def Basis_S_def cr_S_def) 309 310lemma type_finite_dimensional_vector_space_on_with: 311 "finite_dimensional_vector_space_on_with UNIV plus_S minus_S uminus_S zero_S scale_S Basis_S" 312proof - 313 have "finite Basis_S" by transfer (rule finite_Basis) 314 moreover have "\<not> dependent_with plus_S zero_S scale_S Basis_S" 315 by transfer (simp add: implicit_dependent_with independent_Basis) 316 moreover have "span_with plus_S zero_S scale_S Basis_S = UNIV" 317 by transfer (simp add: implicit_span_with span_Basis) 318 ultimately show ?thesis 319 using type_vector_space_on_with 320 by (auto simp: finite_dimensional_vector_space_on_with_def) 321qed 322 323end 324 325locale local_typedef_module_pair = 326 lt1: local_typedef_module_on S1 scale1 s + 327 lt2: local_typedef_module_on S2 scale2 t 328 for S1::"'b::ab_group_add set" and scale1::"'a::comm_ring_1 \<Rightarrow> 'b \<Rightarrow> 'b" and s::"'s itself" 329 and S2::"'c::ab_group_add set" and scale2::"'a \<Rightarrow> 'c \<Rightarrow> 'c" and t::"'t itself" 330begin 331 332lemma type_module_pair_on_with: 333 "module_pair_on_with UNIV UNIV lt1.plus_S lt1.minus_S lt1.uminus_S (lt1.zero_S::'s) lt1.scale_S 334 lt2.plus_S lt2.minus_S lt2.uminus_S (lt2.zero_S::'t) lt2.scale_S" 335 by (simp add: lt1.type_module_on_with lt2.type_module_on_with module_pair_on_with_def) 336 337end 338 339locale local_typedef_vector_space_pair = 340 local_typedef_module_pair S1 scale1 s S2 scale2 t 341 for S1::"'b::ab_group_add set" and scale1::"'a::field \<Rightarrow> 'b \<Rightarrow> 'b" and s::"'s itself" 342 and S2::"'c::ab_group_add set" and scale2::"'a \<Rightarrow> 'c \<Rightarrow> 'c" and t::"'t itself" 343begin 344 345lemma type_vector_space_pair_on_with: 346 "vector_space_pair_on_with UNIV UNIV lt1.plus_S lt1.minus_S lt1.uminus_S (lt1.zero_S::'s) lt1.scale_S 347 lt2.plus_S lt2.minus_S lt2.uminus_S (lt2.zero_S::'t) lt2.scale_S" 348 by (simp add: type_module_pair_on_with vector_space_pair_on_with_def) 349 350sublocale lt1: local_typedef_vector_space_on S1 scale1 s by unfold_locales 351sublocale lt2: local_typedef_vector_space_on S2 scale2 t by unfold_locales 352 353end 354 355locale local_typedef_finite_dimensional_vector_space_pair_1 = 356 lt1: local_typedef_finite_dimensional_vector_space_on S1 scale1 Basis1 s + 357 lt2: local_typedef_vector_space_on S2 scale2 t 358 for S1::"'b::ab_group_add set" and scale1::"'a::field \<Rightarrow> 'b \<Rightarrow> 'b" and Basis1 and s::"'s itself" 359 and S2::"'c::ab_group_add set" and scale2::"'a \<Rightarrow> 'c \<Rightarrow> 'c" and t::"'t itself" 360begin 361 362lemma type_finite_dimensional_vector_space_pair_1_on_with: 363 "finite_dimensional_vector_space_pair_1_on_with UNIV UNIV lt1.plus_S lt1.minus_S lt1.uminus_S (lt1.zero_S::'s) lt1.scale_S lt1.Basis_S 364 lt2.plus_S lt2.minus_S lt2.uminus_S (lt2.zero_S::'t) lt2.scale_S" 365 by (simp add: finite_dimensional_vector_space_pair_1_on_with_def 366 lt1.type_finite_dimensional_vector_space_on_with lt2.type_vector_space_on_with) 367 368end 369 370locale local_typedef_finite_dimensional_vector_space_pair = 371 lt1: local_typedef_finite_dimensional_vector_space_on S1 scale1 Basis1 s + 372 lt2: local_typedef_finite_dimensional_vector_space_on S2 scale2 Basis2 t 373 for S1::"'b::ab_group_add set" and scale1::"'a::field \<Rightarrow> 'b \<Rightarrow> 'b" and Basis1 and s::"'s itself" 374 and S2::"'c::ab_group_add set" and scale2::"'a \<Rightarrow> 'c \<Rightarrow> 'c" and Basis2 and t::"'t itself" 375begin 376 377lemma type_finite_dimensional_vector_space_pair_on_with: 378 "finite_dimensional_vector_space_pair_on_with UNIV UNIV lt1.plus_S lt1.minus_S lt1.uminus_S (lt1.zero_S::'s) lt1.scale_S lt1.Basis_S 379 lt2.plus_S lt2.minus_S lt2.uminus_S (lt2.zero_S::'t) lt2.scale_S lt2.Basis_S" 380 by (simp add: finite_dimensional_vector_space_pair_on_with_def 381 lt1.type_finite_dimensional_vector_space_on_with 382 lt2.type_finite_dimensional_vector_space_on_with) 383 384end 385 386 387subsection \<open>Transfer from type-based \<^theory>\<open>HOL.Modules\<close> and \<^theory>\<open>HOL.Vector_Spaces\<close>\<close> 388 389lemmas [transfer_rule] = right_total_fun_eq_transfer 390 and [transfer_rule del] = vimage_parametric 391 392subsubsection \<open>Modules\<close> 393 394context module_on begin 395 396context includes lifting_syntax assumes ltd: "\<exists>(Rep::'s \<Rightarrow> 'b) (Abs::'b \<Rightarrow> 's). type_definition Rep Abs S" begin 397 398interpretation local_typedef_module_on S scale "TYPE('s)" by unfold_locales fact 399 400text\<open>Get theorem names:\<close> 401print_locale! module 402text\<open>Then replace: 403\<^verbatim>\<open>notes[^"]*"([^"]*).*\<close> 404with 405\<^verbatim>\<open>$1 = module.$1\<close> 406\<close> 407text \<open>TODO: automate systematic naming!\<close> 408lemmas_with [var_simplified explicit_ab_group_add, 409 unoverload_type 'd, 410 OF type.ab_group_add_axioms type_module_on_with, 411 untransferred, 412 var_simplified implicit_ab_group_add]: 413 lt_scale_left_commute = module.scale_left_commute 414 and lt_scale_zero_left = module.scale_zero_left 415 and lt_scale_minus_left = module.scale_minus_left 416 and lt_scale_left_diff_distrib = module.scale_left_diff_distrib 417 and lt_scale_sum_left = module.scale_sum_left 418 and lt_scale_zero_right = module.scale_zero_right 419 and lt_scale_minus_right = module.scale_minus_right 420 and lt_scale_right_diff_distrib = module.scale_right_diff_distrib 421 and lt_scale_sum_right = module.scale_sum_right 422 and lt_sum_constant_scale = module.sum_constant_scale 423 and lt_subspace_def = module.subspace_def 424 and lt_subspaceI = module.subspaceI 425 and lt_subspace_single_0 = module.subspace_single_0 426 and lt_subspace_0 = module.subspace_0 427 and lt_subspace_add = module.subspace_add 428 and lt_subspace_scale = module.subspace_scale 429 and lt_subspace_neg = module.subspace_neg 430 and lt_subspace_diff = module.subspace_diff 431 and lt_subspace_sum = module.subspace_sum 432 and lt_subspace_inter = module.subspace_inter 433 and lt_span_explicit = module.span_explicit 434 and lt_span_explicit' = module.span_explicit' 435 and lt_span_finite = module.span_finite 436 and lt_span_induct_alt = module.span_induct_alt 437 and lt_span_mono = module.span_mono 438 and lt_span_base = module.span_base 439 and lt_span_superset = module.span_superset 440 and lt_span_zero = module.span_zero 441 and lt_span_add = module.span_add 442 and lt_span_scale = module.span_scale 443 and lt_subspace_span = module.subspace_span 444 and lt_span_neg = module.span_neg 445 and lt_span_diff = module.span_diff 446 and lt_span_sum = module.span_sum 447 and lt_span_minimal = module.span_minimal 448 and lt_span_unique = module.span_unique 449 and lt_span_subspace_induct = module.span_subspace_induct 450 and lt_span_induct = module.span_induct 451 and lt_span_empty = module.span_empty 452 and lt_span_subspace = module.span_subspace 453 and lt_span_span = module.span_span 454 and lt_span_add_eq = module.span_add_eq 455 and lt_span_add_eq2 = module.span_add_eq2 456 and lt_span_singleton = module.span_singleton 457 and lt_span_Un = module.span_Un 458 and lt_span_insert = module.span_insert 459 and lt_span_breakdown = module.span_breakdown 460 and lt_span_breakdown_eq = module.span_breakdown_eq 461 and lt_span_clauses = module.span_clauses 462 and lt_span_eq_iff = module.span_eq_iff 463 and lt_span_eq = module.span_eq 464 and lt_eq_span_insert_eq = module.eq_span_insert_eq 465 and lt_dependent_explicit = module.dependent_explicit 466 and lt_dependent_mono = module.dependent_mono 467 and lt_independent_mono = module.independent_mono 468 and lt_dependent_zero = module.dependent_zero 469 and lt_independent_empty = module.independent_empty 470 and lt_independent_explicit_module = module.independent_explicit_module 471 and lt_independentD = module.independentD 472 and lt_independent_Union_directed = module.independent_Union_directed 473 and lt_dependent_finite = module.dependent_finite 474 and lt_independentD_alt = module.independentD_alt 475 and lt_independentD_unique = module.independentD_unique 476 and lt_spanning_subset_independent = module.spanning_subset_independent 477 and lt_module_hom_scale_self = module.module_hom_scale_self 478 and lt_module_hom_scale_left = module.module_hom_scale_left 479 and lt_module_hom_id = module.module_hom_id 480 and lt_module_hom_ident = module.module_hom_ident 481 and lt_module_hom_uminus = module.module_hom_uminus 482 and lt_subspace_UNIV = module.subspace_UNIV 483(* should work but don't: 484 and span_def = module.span_def 485 and span_UNIV = module.span_UNIV 486 and lt_span_alt = module.span_alt 487 and dependent_alt = module.dependent_alt 488 and independent_alt = module.independent_alt 489 and unique_representation = module.unique_representation 490 and subspace_Int = module.subspace_Int 491 and subspace_Inter = module.subspace_Inter 492*) 493(* not expected to work: 494and representation_ne_zero = module.representation_ne_zero 495and representation_ne_zero = module.representation_ne_zero 496and finite_representation = module.finite_representation 497and sum_nonzero_representation_eq = module.sum_nonzero_representation_eq 498and sum_representation_eq = module.sum_representation_eq 499and representation_eqI = module.representation_eqI 500and representation_basis = module.representation_basis 501and representation_zero = module.representation_zero 502and representation_diff = module.representation_diff 503and representation_neg = module.representation_neg 504and representation_add = module.representation_add 505and representation_sum = module.representation_sum 506and representation_scale = module.representation_scale 507and representation_extend = module.representation_extend 508end 509*) 510 511end 512 513lemmas_with [cancel_type_definition, 514 OF S_ne, 515 folded subset_iff', 516 simplified pred_fun_def, 517 simplified\<comment>\<open>too much?\<close>]: 518 scale_left_commute = lt_scale_left_commute 519 and scale_zero_left = lt_scale_zero_left 520 and scale_minus_left = lt_scale_minus_left 521 and scale_left_diff_distrib = lt_scale_left_diff_distrib 522 and scale_sum_left = lt_scale_sum_left 523 and scale_zero_right = lt_scale_zero_right 524 and scale_minus_right = lt_scale_minus_right 525 and scale_right_diff_distrib = lt_scale_right_diff_distrib 526 and scale_sum_right = lt_scale_sum_right 527 and sum_constant_scale = lt_sum_constant_scale 528 and subspace_def = lt_subspace_def 529 and subspaceI = lt_subspaceI 530 and subspace_single_0 = lt_subspace_single_0 531 and subspace_0 = lt_subspace_0 532 and subspace_add = lt_subspace_add 533 and subspace_scale = lt_subspace_scale 534 and subspace_neg = lt_subspace_neg 535 and subspace_diff = lt_subspace_diff 536 and subspace_sum = lt_subspace_sum 537 and subspace_inter = lt_subspace_inter 538 and span_explicit = lt_span_explicit 539 and span_explicit' = lt_span_explicit' 540 and span_finite = lt_span_finite 541 and span_induct_alt[consumes 1, case_names base step, induct set : span] = lt_span_induct_alt 542 and span_mono = lt_span_mono 543 and span_base = lt_span_base 544 and span_superset = lt_span_superset 545 and span_zero = lt_span_zero 546 and span_add = lt_span_add 547 and span_scale = lt_span_scale 548 and subspace_span = lt_subspace_span 549 and span_neg = lt_span_neg 550 and span_diff = lt_span_diff 551 and span_sum = lt_span_sum 552 and span_minimal = lt_span_minimal 553 and span_unique = lt_span_unique 554 and span_subspace_induct[consumes 2] = lt_span_subspace_induct 555 and span_induct[consumes 1, case_names base step, induct set : span] = lt_span_induct 556 and span_empty = lt_span_empty 557 and span_subspace = lt_span_subspace 558 and span_span = lt_span_span 559 and span_add_eq = lt_span_add_eq 560 and span_add_eq2 = lt_span_add_eq2 561 and span_singleton = lt_span_singleton 562 and span_Un = lt_span_Un 563 and span_insert = lt_span_insert 564 and span_breakdown = lt_span_breakdown 565 and span_breakdown_eq = lt_span_breakdown_eq 566 and span_clauses = lt_span_clauses 567 and span_eq_iff = lt_span_eq_iff 568 and span_eq = lt_span_eq 569 and eq_span_insert_eq = lt_eq_span_insert_eq 570 and dependent_explicit = lt_dependent_explicit 571 and dependent_mono = lt_dependent_mono 572 and independent_mono = lt_independent_mono 573 and dependent_zero = lt_dependent_zero 574 and independent_empty = lt_independent_empty 575 and independent_explicit_module = lt_independent_explicit_module 576 and independentD = lt_independentD 577 and independent_Union_directed = lt_independent_Union_directed 578 and dependent_finite = lt_dependent_finite 579 and independentD_alt = lt_independentD_alt 580 and independentD_unique = lt_independentD_unique 581 and spanning_subset_independent = lt_spanning_subset_independent 582 and module_hom_scale_self = lt_module_hom_scale_self 583 and module_hom_scale_left = lt_module_hom_scale_left 584 and module_hom_id = lt_module_hom_id 585 and module_hom_ident = lt_module_hom_ident 586 and module_hom_uminus = lt_module_hom_uminus 587 and subspace_UNIV = lt_subspace_UNIV 588end 589 590subsubsection \<open>Vector Spaces\<close> 591 592context vector_space_on begin 593 594context includes lifting_syntax assumes "\<exists>(Rep::'s \<Rightarrow> 'b) (Abs::'b \<Rightarrow> 's). type_definition Rep Abs S" begin 595 596interpretation local_typedef_vector_space_on S scale "TYPE('s)" by unfold_locales fact 597 598lemmas_with [var_simplified explicit_ab_group_add, 599 unoverload_type 'd, 600 OF type.ab_group_add_axioms type_vector_space_on_with, 601 folded dim_S_def, 602 untransferred, 603 var_simplified implicit_ab_group_add]: 604 lt_linear_id = vector_space.linear_id 605and lt_linear_ident = vector_space.linear_ident 606and lt_linear_scale_self = vector_space.linear_scale_self 607and lt_linear_scale_left = vector_space.linear_scale_left 608and lt_linear_uminus = vector_space.linear_uminus 609and lt_linear_imp_scale["consumes" - 1, "case_names" "1"] = vector_space.linear_imp_scale 610and lt_scale_eq_0_iff = vector_space.scale_eq_0_iff 611and lt_scale_left_imp_eq = vector_space.scale_left_imp_eq 612and lt_scale_right_imp_eq = vector_space.scale_right_imp_eq 613and lt_scale_cancel_left = vector_space.scale_cancel_left 614and lt_scale_cancel_right = vector_space.scale_cancel_right 615and lt_injective_scale = vector_space.injective_scale 616and lt_dependent_def = vector_space.dependent_def 617and lt_dependent_single = vector_space.dependent_single 618and lt_in_span_insert = vector_space.in_span_insert 619and lt_dependent_insertD = vector_space.dependent_insertD 620and lt_independent_insertI = vector_space.independent_insertI 621and lt_independent_insert = vector_space.independent_insert 622and lt_maximal_independent_subset_extend["consumes" - 1, "case_names" "1"] = vector_space.maximal_independent_subset_extend 623and lt_maximal_independent_subset["consumes" - 1, "case_names" "1"] = vector_space.maximal_independent_subset 624and lt_in_span_delete = vector_space.in_span_delete 625and lt_span_redundant = vector_space.span_redundant 626and lt_span_trans = vector_space.span_trans 627and lt_span_insert_0 = vector_space.span_insert_0 628and lt_span_delete_0 = vector_space.span_delete_0 629and lt_span_image_scale = vector_space.span_image_scale 630and lt_exchange_lemma = vector_space.exchange_lemma 631and lt_independent_span_bound = vector_space.independent_span_bound 632and lt_independent_explicit_finite_subsets = vector_space.independent_explicit_finite_subsets 633and lt_independent_if_scalars_zero = vector_space.independent_if_scalars_zero 634and lt_subspace_sums = vector_space.subspace_sums 635and lt_dim_unique = vector_space.dim_unique 636and lt_dim_eq_card = vector_space.dim_eq_card 637and lt_basis_card_eq_dim = vector_space.basis_card_eq_dim 638and lt_basis_exists = vector_space.basis_exists 639and lt_dim_eq_card_independent = vector_space.dim_eq_card_independent 640and lt_dim_span = vector_space.dim_span 641and lt_dim_span_eq_card_independent = vector_space.dim_span_eq_card_independent 642and lt_dim_le_card = vector_space.dim_le_card 643and lt_span_eq_dim = vector_space.span_eq_dim 644and lt_dim_le_card' = vector_space.dim_le_card' 645and lt_span_card_ge_dim = vector_space.span_card_ge_dim 646and lt_dim_with = vector_space.dim_with 647(* should work but don't:v 648 649and lt_bij_if_span_eq_span_bases = vector_space.bij_if_span_eq_span_bases 650*) 651(* not expected to work: 652and lt_dim_def = vector_space.dim_def 653and lt_extend_basis_superset = vector_space.extend_basis_superset 654and lt_independent_extend_basis = vector_space.independent_extend_basis 655and lt_span_extend_basis = vector_space.span_extend_basis 656*) 657 658end 659 660lemmas_with [cancel_type_definition, 661 OF S_ne, 662 folded subset_iff', 663 simplified pred_fun_def, 664 simplified\<comment>\<open>too much?\<close>]: 665 linear_id = lt_linear_id 666and linear_ident = lt_linear_ident 667and linear_scale_self = lt_linear_scale_self 668and linear_scale_left = lt_linear_scale_left 669and linear_uminus = lt_linear_uminus 670and linear_imp_scale["consumes" - 1, "case_names" "1"] = lt_linear_imp_scale 671and scale_eq_0_iff = lt_scale_eq_0_iff 672and scale_left_imp_eq = lt_scale_left_imp_eq 673and scale_right_imp_eq = lt_scale_right_imp_eq 674and scale_cancel_left = lt_scale_cancel_left 675and scale_cancel_right = lt_scale_cancel_right 676and dependent_def = lt_dependent_def 677and dependent_single = lt_dependent_single 678and in_span_insert = lt_in_span_insert 679and dependent_insertD = lt_dependent_insertD 680and independent_insertI = lt_independent_insertI 681and independent_insert = lt_independent_insert 682and maximal_independent_subset_extend["consumes" - 1, "case_names" "1"] = lt_maximal_independent_subset_extend 683and maximal_independent_subset["consumes" - 1, "case_names" "1"] = lt_maximal_independent_subset 684and in_span_delete = lt_in_span_delete 685and span_redundant = lt_span_redundant 686and span_trans = lt_span_trans 687and span_insert_0 = lt_span_insert_0 688and span_delete_0 = lt_span_delete_0 689and span_image_scale = lt_span_image_scale 690and exchange_lemma = lt_exchange_lemma 691and independent_span_bound = lt_independent_span_bound 692and independent_explicit_finite_subsets = lt_independent_explicit_finite_subsets 693and independent_if_scalars_zero = lt_independent_if_scalars_zero 694and subspace_sums = lt_subspace_sums 695and dim_unique = lt_dim_unique 696and dim_eq_card = lt_dim_eq_card 697and basis_card_eq_dim = lt_basis_card_eq_dim 698and basis_exists["consumes" - 1, "case_names" "1"] = lt_basis_exists 699and dim_eq_card_independent = lt_dim_eq_card_independent 700and dim_span = lt_dim_span 701and dim_span_eq_card_independent = lt_dim_span_eq_card_independent 702and dim_le_card = lt_dim_le_card 703and span_eq_dim = lt_span_eq_dim 704and dim_le_card' = lt_dim_le_card' 705and span_card_ge_dim = lt_span_card_ge_dim 706and dim_with = lt_dim_with 707 708end 709 710subsubsection \<open>Finite Dimensional Vector Spaces\<close> 711 712context finite_dimensional_vector_space_on begin 713 714context includes lifting_syntax assumes "\<exists>(Rep::'s \<Rightarrow> 'a) (Abs::'a \<Rightarrow> 's). type_definition Rep Abs S" begin 715 716interpretation local_typedef_finite_dimensional_vector_space_on S scale basis "TYPE('s)" by unfold_locales fact 717 718lemmas_with [var_simplified explicit_ab_group_add, 719 unoverload_type 'd, 720 OF type.ab_group_add_axioms type_finite_dimensional_vector_space_on_with, 721 folded dim_S_def, 722 untransferred, 723 var_simplified implicit_ab_group_add]: 724 lt_finiteI_independent = finite_dimensional_vector_space.finiteI_independent 725and lt_dim_empty = finite_dimensional_vector_space.dim_empty 726and lt_dim_insert = finite_dimensional_vector_space.dim_insert 727and lt_dim_singleton = finite_dimensional_vector_space.dim_singleton 728and lt_choose_subspace_of_subspace["consumes" - 1, "case_names" "1"] = finite_dimensional_vector_space.choose_subspace_of_subspace 729and lt_basis_subspace_exists["consumes" - 1, "case_names" "1"] = finite_dimensional_vector_space.basis_subspace_exists 730and lt_dim_mono = finite_dimensional_vector_space.dim_mono 731and lt_dim_subset = finite_dimensional_vector_space.dim_subset 732and lt_dim_eq_0 = finite_dimensional_vector_space.dim_eq_0 733and lt_dim_UNIV = finite_dimensional_vector_space.dim_UNIV 734and lt_independent_card_le_dim = finite_dimensional_vector_space.independent_card_le_dim 735and lt_card_ge_dim_independent = finite_dimensional_vector_space.card_ge_dim_independent 736and lt_card_le_dim_spanning = finite_dimensional_vector_space.card_le_dim_spanning 737and lt_card_eq_dim = finite_dimensional_vector_space.card_eq_dim 738and lt_subspace_dim_equal = finite_dimensional_vector_space.subspace_dim_equal 739and lt_dim_eq_span = finite_dimensional_vector_space.dim_eq_span 740and lt_dim_psubset = finite_dimensional_vector_space.dim_psubset 741and lt_indep_card_eq_dim_span = finite_dimensional_vector_space.indep_card_eq_dim_span 742and lt_independent_bound_general = finite_dimensional_vector_space.independent_bound_general 743and lt_independent_explicit = finite_dimensional_vector_space.independent_explicit 744and lt_dim_sums_Int = finite_dimensional_vector_space.dim_sums_Int 745and lt_dependent_biggerset_general = finite_dimensional_vector_space.dependent_biggerset_general 746and lt_subset_le_dim = finite_dimensional_vector_space.subset_le_dim 747and lt_linear_inj_imp_surj = finite_dimensional_vector_space.linear_inj_imp_surj 748and lt_linear_surj_imp_inj = finite_dimensional_vector_space.linear_surj_imp_inj 749and lt_linear_inverse_left = finite_dimensional_vector_space.linear_inverse_left 750and lt_left_inverse_linear = finite_dimensional_vector_space.left_inverse_linear 751and lt_right_inverse_linear = finite_dimensional_vector_space.right_inverse_linear 752(* not expected to work: 753 lt_dimension_def = finite_dimensional_vector_space.dimension_def 754and lt_dim_subset_UNIV = finite_dimensional_vector_space.dim_subset_UNIV 755and lt_dim_eq_full = finite_dimensional_vector_space.dim_eq_full 756and lt_inj_linear_imp_inv_linear = finite_dimensional_vector_space.inj_linear_imp_inv_linear 757*) 758 759end 760 761lemmas_with [cancel_type_definition, 762 OF S_ne, 763 folded subset_iff', 764 simplified pred_fun_def, 765 simplified\<comment>\<open>too much?\<close>]: 766 finiteI_independent = lt_finiteI_independent 767and dim_empty = lt_dim_empty 768and dim_insert = lt_dim_insert 769and dim_singleton = lt_dim_singleton 770and choose_subspace_of_subspace["consumes" - 1, "case_names" "1"] = lt_choose_subspace_of_subspace 771and basis_subspace_exists["consumes" - 1, "case_names" "1"] = lt_basis_subspace_exists 772and dim_mono = lt_dim_mono 773and dim_subset = lt_dim_subset 774and dim_eq_0 = lt_dim_eq_0 775and dim_UNIV = lt_dim_UNIV 776and independent_card_le_dim = lt_independent_card_le_dim 777and card_ge_dim_independent = lt_card_ge_dim_independent 778and card_le_dim_spanning = lt_card_le_dim_spanning 779and card_eq_dim = lt_card_eq_dim 780and subspace_dim_equal = lt_subspace_dim_equal 781and dim_eq_span = lt_dim_eq_span 782and dim_psubset = lt_dim_psubset 783and indep_card_eq_dim_span = lt_indep_card_eq_dim_span 784and independent_bound_general = lt_independent_bound_general 785and independent_explicit = lt_independent_explicit 786and dim_sums_Int = lt_dim_sums_Int 787and dependent_biggerset_general = lt_dependent_biggerset_general 788and subset_le_dim = lt_subset_le_dim 789and linear_inj_imp_surj = lt_linear_inj_imp_surj 790and linear_surj_imp_inj = lt_linear_surj_imp_inj 791and linear_inverse_left = lt_linear_inverse_left 792and left_inverse_linear = lt_left_inverse_linear 793and right_inverse_linear = lt_right_inverse_linear 794 795end 796 797context module_pair_on begin 798 799context includes lifting_syntax 800 assumes 801 "\<exists>(Rep::'s \<Rightarrow> 'b) (Abs::'b \<Rightarrow> 's). type_definition Rep Abs S1" 802 "\<exists>(Rep::'t \<Rightarrow> 'c) (Abs::'c \<Rightarrow> 't). type_definition Rep Abs S2" begin 803 804interpretation local_typedef_module_pair S1 scale1 "TYPE('s)" S2 scale2 "TYPE('t)" by unfold_locales fact+ 805 806lemmas_with [var_simplified explicit_ab_group_add, 807 unoverload_type 'e 'f, 808 OF lt2.type.ab_group_add_axioms lt1.type.ab_group_add_axioms type_module_pair_on_with, 809 untransferred, 810 var_simplified implicit_ab_group_add]: 811 lt_module_hom_zero = module_pair.module_hom_zero 812and lt_module_hom_add = module_pair.module_hom_add 813and lt_module_hom_sub = module_pair.module_hom_sub 814and lt_module_hom_neg = module_pair.module_hom_neg 815and lt_module_hom_scale = module_pair.module_hom_scale 816and lt_module_hom_compose_scale = module_pair.module_hom_compose_scale 817and lt_module_hom_sum = module_pair.module_hom_sum 818and lt_module_hom_eq_on_span = module_pair.module_hom_eq_on_span 819(* should work, but doesnt 820and lt_bij_module_hom_imp_inv_module_hom = module_pair.bij_module_hom_imp_inv_module_hom[of scale1 scale2] 821*) 822 823end 824 825lemmas_with [cancel_type_definition, OF m1.S_ne, 826 cancel_type_definition, OF m2.S_ne, 827 folded subset_iff' top_set_def, 828 simplified pred_fun_def, 829 simplified\<comment>\<open>too much?\<close>]: 830 module_hom_zero = lt_module_hom_zero 831and module_hom_add = lt_module_hom_add 832and module_hom_sub = lt_module_hom_sub 833and module_hom_neg = lt_module_hom_neg 834and module_hom_scale = lt_module_hom_scale 835and module_hom_compose_scale = lt_module_hom_compose_scale 836and module_hom_sum = lt_module_hom_sum 837and module_hom_eq_on_span = lt_module_hom_eq_on_span 838 839end 840 841context vector_space_pair_on begin 842 843context includes lifting_syntax 844 notes [transfer_rule del] = Collect_transfer 845 assumes 846 "\<exists>(Rep::'s \<Rightarrow> 'b) (Abs::'b \<Rightarrow> 's). type_definition Rep Abs S1" 847 "\<exists>(Rep::'t \<Rightarrow> 'c) (Abs::'c \<Rightarrow> 't). type_definition Rep Abs S2" begin 848 849interpretation local_typedef_vector_space_pair S1 scale1 "TYPE('s)" S2 scale2 "TYPE('t)" by unfold_locales fact+ 850 851lemmas_with [var_simplified explicit_ab_group_add, 852 unoverload_type 'e 'f, 853 OF lt2.type.ab_group_add_axioms lt1.type.ab_group_add_axioms type_vector_space_pair_on_with, 854 folded lt1.dim_S_def lt2.dim_S_def, 855 untransferred, 856 var_simplified implicit_ab_group_add]: 857 lt_linear_0 = vector_space_pair.linear_0 858and lt_linear_add = vector_space_pair.linear_add 859and lt_linear_scale = vector_space_pair.linear_scale 860and lt_linear_neg = vector_space_pair.linear_neg 861and lt_linear_diff = vector_space_pair.linear_diff 862and lt_linear_sum = vector_space_pair.linear_sum 863and lt_linear_inj_on_iff_eq_0 = vector_space_pair.linear_inj_on_iff_eq_0 864and lt_linear_inj_iff_eq_0 = vector_space_pair.linear_inj_iff_eq_0 865and lt_linear_subspace_image = vector_space_pair.linear_subspace_image 866and lt_linear_subspace_vimage = vector_space_pair.linear_subspace_vimage 867and lt_linear_subspace_kernel = vector_space_pair.linear_subspace_kernel 868and lt_linear_span_image = vector_space_pair.linear_span_image 869and lt_linear_dependent_inj_imageD = vector_space_pair.linear_dependent_inj_imageD 870and lt_linear_eq_0_on_span = vector_space_pair.linear_eq_0_on_span 871and lt_linear_independent_injective_image = vector_space_pair.linear_independent_injective_image 872and lt_linear_inj_on_span_independent_image = vector_space_pair.linear_inj_on_span_independent_image 873and lt_linear_inj_on_span_iff_independent_image = vector_space_pair.linear_inj_on_span_iff_independent_image 874and lt_linear_subspace_linear_preimage = vector_space_pair.linear_subspace_linear_preimage 875and lt_linear_spans_image = vector_space_pair.linear_spans_image 876and lt_linear_spanning_surjective_image = vector_space_pair.linear_spanning_surjective_image 877and lt_linear_eq_on_span = vector_space_pair.linear_eq_on_span 878and lt_linear_compose_scale_right = vector_space_pair.linear_compose_scale_right 879and lt_linear_compose_add = vector_space_pair.linear_compose_add 880and lt_linear_zero = vector_space_pair.linear_zero 881and lt_linear_compose_sub = vector_space_pair.linear_compose_sub 882and lt_linear_compose_neg = vector_space_pair.linear_compose_neg 883and lt_linear_compose_scale = vector_space_pair.linear_compose_scale 884and lt_linear_indep_image_lemma = vector_space_pair.linear_indep_image_lemma 885and lt_linear_eq_on = vector_space_pair.linear_eq_on 886and lt_linear_compose_sum = vector_space_pair.linear_compose_sum 887and lt_linear_independent_extend_subspace = vector_space_pair.linear_independent_extend_subspace 888and lt_linear_independent_extend = vector_space_pair.linear_independent_extend 889and lt_linear_exists_left_inverse_on = vector_space_pair.linear_exists_left_inverse_on 890and lt_linear_exists_right_inverse_on = vector_space_pair.linear_exists_right_inverse_on 891and lt_linear_inj_on_left_inverse = vector_space_pair.linear_inj_on_left_inverse 892and lt_linear_injective_left_inverse = vector_space_pair.linear_injective_left_inverse 893and lt_linear_surj_right_inverse = vector_space_pair.linear_surj_right_inverse 894and lt_linear_surjective_right_inverse = vector_space_pair.linear_surjective_right_inverse 895and lt_finite_basis_to_basis_subspace_isomorphism = vector_space_pair.finite_basis_to_basis_subspace_isomorphism 896(* should work, but doesnt 897*) 898(* not expected to work: 899 lt_construct_def = vector_space_pair.construct_def 900 lt_construct_cong = vector_space_pair.construct_cong 901 lt_linear_construct = vector_space_pair.linear_construct 902 lt_construct_basis = vector_space_pair.construct_basis 903 lt_construct_outside = vector_space_pair.construct_outside 904 lt_construct_add = vector_space_pair.construct_add 905 lt_construct_scale = vector_space_pair.construct_scale 906 lt_construct_in_span = vector_space_pair.construct_in_span 907 lt_in_span_in_range_construct = vector_space_pair.in_span_in_range_construct 908 lt_range_construct_eq_span = vector_space_pair.range_construct_eq_span 909*) 910end 911 912lemmas_with [cancel_type_definition, OF m1.S_ne, 913 cancel_type_definition, OF m2.S_ne, 914 folded subset_iff' top_set_def, 915 simplified pred_fun_def, 916 simplified\<comment>\<open>too much?\<close>]: 917 linear_0 = lt_linear_0 918 and linear_add = lt_linear_add 919 and linear_scale = lt_linear_scale 920 and linear_neg = lt_linear_neg 921 and linear_diff = lt_linear_diff 922 and linear_sum = lt_linear_sum 923 and linear_inj_on_iff_eq_0 = lt_linear_inj_on_iff_eq_0 924 and linear_inj_iff_eq_0 = lt_linear_inj_iff_eq_0 925 and linear_subspace_image = lt_linear_subspace_image 926 and linear_subspace_vimage = lt_linear_subspace_vimage 927 and linear_subspace_kernel = lt_linear_subspace_kernel 928 and linear_span_image = lt_linear_span_image 929 and linear_dependent_inj_imageD = lt_linear_dependent_inj_imageD 930 and linear_eq_0_on_span = lt_linear_eq_0_on_span 931 and linear_independent_injective_image = lt_linear_independent_injective_image 932 and linear_inj_on_span_independent_image = lt_linear_inj_on_span_independent_image 933 and linear_inj_on_span_iff_independent_image = lt_linear_inj_on_span_iff_independent_image 934 and linear_subspace_linear_preimage = lt_linear_subspace_linear_preimage 935 and linear_spans_image = lt_linear_spans_image 936 and linear_spanning_surjective_image = lt_linear_spanning_surjective_image 937 and linear_eq_on_span = lt_linear_eq_on_span 938 and linear_compose_scale_right = lt_linear_compose_scale_right 939 and linear_compose_add = lt_linear_compose_add 940 and linear_zero = lt_linear_zero 941 and linear_compose_sub = lt_linear_compose_sub 942 and linear_compose_neg = lt_linear_compose_neg 943 and linear_compose_scale = lt_linear_compose_scale 944 and linear_indep_image_lemma = lt_linear_indep_image_lemma 945 and linear_eq_on = lt_linear_eq_on 946 and linear_compose_sum = lt_linear_compose_sum 947 and linear_independent_extend_subspace = lt_linear_independent_extend_subspace 948 and linear_independent_extend = lt_linear_independent_extend 949 and linear_exists_left_inverse_on = lt_linear_exists_left_inverse_on 950 and linear_exists_right_inverse_on = lt_linear_exists_right_inverse_on 951 and linear_inj_on_left_inverse = lt_linear_inj_on_left_inverse 952 and linear_injective_left_inverse = lt_linear_injective_left_inverse 953 and linear_surj_right_inverse = lt_linear_surj_right_inverse 954 and linear_surjective_right_inverse = lt_linear_surjective_right_inverse 955 and finite_basis_to_basis_subspace_isomorphism = lt_finite_basis_to_basis_subspace_isomorphism 956 957end 958 959context finite_dimensional_vector_space_pair_1_on begin 960 961context includes lifting_syntax 962 notes [transfer_rule del] = Collect_transfer 963 assumes 964 "\<exists>(Rep::'s \<Rightarrow> 'b) (Abs::'b \<Rightarrow> 's). type_definition Rep Abs S1" 965 "\<exists>(Rep::'t \<Rightarrow> 'c) (Abs::'c \<Rightarrow> 't). type_definition Rep Abs S2" begin 966 967interpretation local_typedef_finite_dimensional_vector_space_pair_1 S1 scale1 Basis1 "TYPE('s)" S2 scale2 "TYPE('t)" by unfold_locales fact+ 968 969lemmas_with [var_simplified explicit_ab_group_add, 970 unoverload_type 'e 'f, 971 OF lt2.type.ab_group_add_axioms lt1.type.ab_group_add_axioms type_finite_dimensional_vector_space_pair_1_on_with, 972 folded lt1.dim_S_def lt2.dim_S_def, 973 untransferred, 974 var_simplified implicit_ab_group_add]: 975 lt_dim_image_eq = finite_dimensional_vector_space_pair_1.dim_image_eq 976and lt_dim_image_le = finite_dimensional_vector_space_pair_1.dim_image_le 977 978end 979 980lemmas_with [cancel_type_definition, OF vs1.S_ne, 981 cancel_type_definition, OF vs2.S_ne, 982 folded subset_iff' top_set_def, 983 simplified pred_fun_def, 984 simplified\<comment>\<open>too much?\<close>]: 985 dim_image_eq = lt_dim_image_eq 986and dim_image_le = lt_dim_image_le 987 988end 989 990 991context finite_dimensional_vector_space_pair_on begin 992 993context includes lifting_syntax 994 notes [transfer_rule del] = Collect_transfer 995 assumes 996 "\<exists>(Rep::'s \<Rightarrow> 'b) (Abs::'b \<Rightarrow> 's). type_definition Rep Abs S1" 997 "\<exists>(Rep::'t \<Rightarrow> 'c) (Abs::'c \<Rightarrow> 't). type_definition Rep Abs S2" begin 998 999interpretation local_typedef_finite_dimensional_vector_space_pair S1 scale1 Basis1 "TYPE('s)" S2 scale2 Basis2 "TYPE('t)" by unfold_locales fact+ 1000 1001lemmas_with [var_simplified explicit_ab_group_add, 1002 unoverload_type 'e 'f, 1003 OF lt2.type.ab_group_add_axioms lt1.type.ab_group_add_axioms type_finite_dimensional_vector_space_pair_on_with, 1004 folded lt1.dim_S_def lt2.dim_S_def, 1005 untransferred, 1006 var_simplified implicit_ab_group_add]: 1007lt_linear_surjective_imp_injective = finite_dimensional_vector_space_pair.linear_surjective_imp_injective 1008and lt_linear_injective_imp_surjective = finite_dimensional_vector_space_pair.linear_injective_imp_surjective 1009and lt_linear_injective_isomorphism = finite_dimensional_vector_space_pair.linear_injective_isomorphism 1010and lt_linear_surjective_isomorphism = finite_dimensional_vector_space_pair.linear_surjective_isomorphism 1011and lt_basis_to_basis_subspace_isomorphism = finite_dimensional_vector_space_pair.basis_to_basis_subspace_isomorphism 1012and lt_subspace_isomorphism = finite_dimensional_vector_space_pair.subspace_isomorphism 1013 1014end 1015 1016lemmas_with [cancel_type_definition, OF vs1.S_ne, 1017 cancel_type_definition, OF vs2.S_ne, 1018 folded subset_iff' top_set_def, 1019 simplified pred_fun_def, 1020 simplified\<comment>\<open>too much?\<close>]: 1021linear_surjective_imp_injective = lt_linear_surjective_imp_injective 1022and linear_injective_imp_surjective = lt_linear_injective_imp_surjective 1023and linear_injective_isomorphism = lt_linear_injective_isomorphism 1024and linear_surjective_isomorphism = lt_linear_surjective_isomorphism 1025and basis_to_basis_subspace_isomorphism = lt_basis_to_basis_subspace_isomorphism 1026and subspace_isomorphism = lt_subspace_isomorphism 1027 1028end 1029 1030end 1031