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