--- a/CONTRIBUTORS Wed Jun 27 10:18:03 2018 +0200
+++ b/CONTRIBUTORS Wed Jun 27 11:16:43 2018 +0200
@@ -6,6 +6,9 @@
Contributions to Isabelle2018
-----------------------------
+* June 2018: Fabian Immler
+ More tool support for HOL-Types_To_Sets.
+
* June 2018: Martin Baillon and Paulo Emílio de Vilhena
A variety of contributions to HOL-Algebra.
--- a/NEWS Wed Jun 27 10:18:03 2018 +0200
+++ b/NEWS Wed Jun 27 11:16:43 2018 +0200
@@ -394,6 +394,11 @@
Riemann mapping theorem, the Vitali covering theorem,
change-of-variables results for integration and measures.
+* Session HOL-Types_To_Sets: more tool support
+(unoverload_type combines internalize_sorts and unoverload) and larger
+experimental application (type based linear algebra transferred to linear
+algebra on subspaces).
+
*** ML ***
--- a/src/HOL/ROOT Wed Jun 27 10:18:03 2018 +0200
+++ b/src/HOL/ROOT Wed Jun 27 11:16:43 2018 +0200
@@ -932,6 +932,7 @@
"Examples/Prerequisites"
"Examples/Finite"
"Examples/T2_Spaces"
+ "Examples/Linear_Algebra_On"
session HOLCF (main timing) in HOLCF = HOL +
description {*
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Types_To_Sets/Examples/Group_On_With.thy Wed Jun 27 11:16:43 2018 +0200
@@ -0,0 +1,338 @@
+(* Title: HOL/Types_To_Sets/Examples/Group_On_With.thy
+ Author: Fabian Immler, TU München
+*)
+theory Group_On_With
+imports
+ Main
+begin
+
+subsection \<open>\<^emph>\<open>on\<close> carrier set \<^emph>\<open>with\<close> explicit group operations\<close>
+
+definition "semigroup_add_on_with S pls \<longleftrightarrow>
+ (\<forall>a\<in>S. \<forall>b\<in>S. \<forall>c\<in>S. pls (pls a b) c = pls a (pls b c)) \<and>
+ (\<forall>a\<in>S. \<forall>b\<in>S. pls a b \<in> S)"
+
+lemma semigroup_add_on_with_transfer[transfer_rule]:
+ includes lifting_syntax
+ assumes [transfer_rule]: "bi_unique A"
+ shows "(rel_set A ===> (A ===> A ===> A) ===> (=)) semigroup_add_on_with semigroup_add_on_with"
+ unfolding semigroup_add_on_with_def
+ by transfer_prover
+
+
+lemma semigroup_add_on_with[simp]: "semigroup_add_on_with (UNIV::'a::semigroup_add set) (+)"
+ by (auto simp: semigroup_add_on_with_def ac_simps)
+
+lemma Domainp_applyI:
+ includes lifting_syntax
+ shows "(A ===> B) f g \<Longrightarrow> A x y \<Longrightarrow> Domainp B (f x)"
+ by (auto simp: rel_fun_def)
+
+lemma Domainp_apply2I:
+ includes lifting_syntax
+ shows "(A ===> B ===> C) f g \<Longrightarrow> A x y \<Longrightarrow> B x' y' \<Longrightarrow> Domainp C (f x x')"
+ by (force simp: rel_fun_def)
+
+lemma right_total_semigroup_add_transfer[transfer_rule]:
+ includes lifting_syntax
+ assumes [transfer_rule]: "right_total A" "bi_unique A"
+ shows "((A ===> A ===> A) ===> (=)) (semigroup_add_on_with (Collect (Domainp A))) class.semigroup_add"
+proof (intro rel_funI)
+ fix x y assume xy[transfer_rule]: "(A ===> A ===> A) x y"
+ show "semigroup_add_on_with (Collect (Domainp A)) x = class.semigroup_add y"
+ unfolding semigroup_add_on_with_def class.semigroup_add_def
+ by transfer (auto intro!: Domainp_apply2I[OF xy])
+qed
+
+definition "ab_semigroup_add_on_with S pls \<longleftrightarrow> semigroup_add_on_with S pls \<and> (\<forall>a\<in>S. \<forall>b\<in>S. pls a b = pls b a)"
+
+lemma ab_semigroup_add_on_with_transfer[transfer_rule]:
+ includes lifting_syntax
+ assumes [transfer_rule]: "bi_unique A"
+ shows
+ "(rel_set A ===> (A ===> A ===> A) ===> (=)) ab_semigroup_add_on_with ab_semigroup_add_on_with"
+ unfolding ab_semigroup_add_on_with_def by transfer_prover
+
+lemma right_total_ab_semigroup_add_transfer[transfer_rule]:
+ includes lifting_syntax
+ assumes [transfer_rule]: "right_total A" "bi_unique A"
+ shows
+ "((A ===> A ===> A) ===> (=)) (ab_semigroup_add_on_with (Collect (Domainp A))) class.ab_semigroup_add"
+ unfolding class.ab_semigroup_add_def class.ab_semigroup_add_axioms_def ab_semigroup_add_on_with_def
+ by transfer_prover
+
+lemma ab_semigroup_add_on_with[simp]: "ab_semigroup_add_on_with (UNIV::'a::ab_semigroup_add set) (+)"
+ by (auto simp: ab_semigroup_add_on_with_def ac_simps)
+
+
+definition "comm_monoid_add_on_with S pls z \<longleftrightarrow> ab_semigroup_add_on_with S pls \<and> (\<forall>a\<in>S. pls z a = a) \<and> z \<in> S"
+
+lemma comm_monoid_add_on_with_transfer[transfer_rule]:
+ includes lifting_syntax
+ assumes [transfer_rule]: "bi_unique A"
+ shows
+ "(rel_set A ===> (A ===> A ===> A) ===> A ===> (=)) comm_monoid_add_on_with comm_monoid_add_on_with"
+ unfolding comm_monoid_add_on_with_def
+ by transfer_prover
+
+lemma right_total_comm_monoid_add_transfer[transfer_rule]:
+ includes lifting_syntax
+ assumes [transfer_rule]: "right_total A" "bi_unique A"
+ shows
+ "((A ===> A ===> A) ===> A ===> (=))
+ (comm_monoid_add_on_with (Collect (Domainp A))) class.comm_monoid_add"
+proof (intro rel_funI)
+ fix p p' z z'
+ assume [transfer_rule]: "(A ===> A ===> A) p p'" "A z z'"
+ show "comm_monoid_add_on_with (Collect (Domainp A)) p z = class.comm_monoid_add p' z'"
+ unfolding class.comm_monoid_add_def class.comm_monoid_add_axioms_def comm_monoid_add_on_with_def
+ apply transfer
+ using \<open>A z z'\<close>
+ by auto
+qed
+
+lemma comm_monoid_add_on_with[simp]: "comm_monoid_add_on_with UNIV (+) (0::'a::comm_monoid_add)"
+ by (auto simp: comm_monoid_add_on_with_def ab_semigroup_add_on_with_def
+ semigroup_add_on_with_def ac_simps)
+
+definition "ab_group_add_on_with S pls z mns um \<longleftrightarrow> comm_monoid_add_on_with S pls z \<and>
+ (\<forall>a\<in>S. pls (um a) a = z) \<and> (\<forall>a\<in>S. \<forall>b\<in>S. mns a b = pls a (um b))"
+
+lemma ab_group_add_transfer[transfer_rule]:
+ includes lifting_syntax
+ assumes [transfer_rule]: "right_total A" "bi_unique A"
+ shows
+ "((A ===> A ===> A) ===> A ===> (A ===> A ===> A) ===> (A ===> A)===> (=))
+ (ab_group_add_on_with (Collect (Domainp A))) class.ab_group_add"
+ unfolding class.ab_group_add_def class.ab_group_add_axioms_def ab_group_add_on_with_def
+ by transfer_prover
+
+lemma ab_group_add_on_with_transfer[transfer_rule]:
+ includes lifting_syntax
+ assumes [transfer_rule]: "right_total A" "bi_unique A"
+ shows
+ "(rel_set A ===> (A ===> A ===> A) ===> A ===> (A ===> A ===> A) ===> (A ===> A)===> (=))
+ ab_group_add_on_with ab_group_add_on_with"
+ unfolding class.ab_group_add_def class.ab_group_add_axioms_def ab_group_add_on_with_def
+ by transfer_prover
+
+lemma ab_group_add_on_with[simp]: "ab_group_add_on_with (UNIV::'a::ab_group_add set) (+) 0 (-) uminus"
+ by (auto simp: ab_group_add_on_with_def)
+
+definition "sum_with pls z f S =
+ (if \<exists>C. f ` S \<subseteq> C \<and> comm_monoid_add_on_with C pls z then
+ Finite_Set.fold (pls o f) z S else z)"
+
+lemma sum_with_empty[simp]: "sum_with pls z f {} = z"
+ by (auto simp: sum_with_def)
+
+lemma sum_with: "sum = sum_with (+) 0"
+proof (intro ext)
+ fix f::"'a\<Rightarrow>'b" and X::"'a set"
+ have ex: "\<exists>C. f ` X \<subseteq> C \<and> comm_monoid_add_on_with C (+) 0"
+ by (auto intro!: exI[where x=UNIV] comm_monoid_add_on_with)
+ then show "sum f X = sum_with (+) 0 f X"
+ unfolding sum.eq_fold sum_with_def
+ by simp
+qed
+
+context fixes C pls z assumes comm_monoid_add_on_with: "comm_monoid_add_on_with C pls z" begin
+
+lemmas comm_monoid_add_unfolded =
+ comm_monoid_add_on_with[unfolded
+ comm_monoid_add_on_with_def ab_semigroup_add_on_with_def semigroup_add_on_with_def]
+
+private abbreviation "pls' \<equiv> \<lambda>x y. pls (if x \<in> C then x else z) (if y \<in> C then y else z)"
+
+lemma fold_pls'_mem: "Finite_Set.fold (pls' \<circ> g) z A \<in> C"
+ if "g ` A \<subseteq> C"
+proof cases
+ assume A: "finite A"
+ interpret comp_fun_commute "pls' o g"
+ using comm_monoid_add_unfolded that
+ by unfold_locales auto
+ from fold_graph_fold[OF A] have "fold_graph (pls' \<circ> g) z A (Finite_Set.fold (pls' \<circ> g) z A)" .
+ from fold_graph_closed_lemma[OF this, of C "pls' \<circ> g"] comm_monoid_add_unfolded
+ show ?thesis
+ by auto
+qed (use comm_monoid_add_unfolded in simp)
+
+lemma fold_pls'_eq: "Finite_Set.fold (pls' \<circ> g) z A = Finite_Set.fold (pls \<circ> g) z A"
+ if "g ` A \<subseteq> C"
+ using comm_monoid_add_unfolded that
+ by (intro fold_closed_eq[where B=C]) auto
+
+lemma sum_with_mem: "sum_with pls z g A \<in> C" if "g ` A \<subseteq> C"
+proof -
+ interpret comp_fun_commute "pls' o g"
+ using comm_monoid_add_unfolded that
+ by unfold_locales auto
+ have "\<exists>C. g ` A \<subseteq> C \<and> comm_monoid_add_on_with C pls z" using that comm_monoid_add_on_with by auto
+ then show ?thesis
+ using fold_pls'_mem[OF that]
+ by (simp add: sum_with_def fold_pls'_eq that)
+qed
+
+lemma sum_with_insert:
+ "sum_with pls z g (insert x A) = pls (g x) (sum_with pls z g A)"
+ if g_into: "g x \<in> C" "g ` A \<subseteq> C"
+ and A: "finite A" and x: "x \<notin> A"
+proof -
+ interpret comp_fun_commute "pls' o g"
+ using comm_monoid_add_unfolded g_into
+ by unfold_locales auto
+ have "Finite_Set.fold (pls \<circ> g) z (insert x A) = Finite_Set.fold (pls' \<circ> g) z (insert x A)"
+ using g_into
+ by (subst fold_pls'_eq) auto
+ also have "\<dots> = pls' (g x) (Finite_Set.fold (pls' \<circ> g) z A)"
+ unfolding fold_insert[OF A x]
+ by (auto simp: o_def)
+ also have "\<dots> = pls (g x) (Finite_Set.fold (pls' \<circ> g) z A)"
+ proof -
+ from fold_graph_fold[OF A] have "fold_graph (pls' \<circ> g) z A (Finite_Set.fold (pls' \<circ> g) z A)" .
+ from fold_graph_closed_lemma[OF this, of C "pls' \<circ> g"] comm_monoid_add_unfolded
+ have "Finite_Set.fold (pls' \<circ> g) z A \<in> C"
+ by auto
+ then show ?thesis
+ using g_into by auto
+ qed
+ also have "Finite_Set.fold (pls' \<circ> g) z A = Finite_Set.fold (pls \<circ> g) z A"
+ using g_into
+ by (subst fold_pls'_eq) auto
+ finally
+ have "Finite_Set.fold (pls \<circ> g) z (insert x A) = pls (g x) (Finite_Set.fold (pls \<circ> g) z A)" .
+ moreover
+ have "\<exists>C. g ` insert x A \<subseteq> C \<and> comm_monoid_add_on_with C pls z"
+ "\<exists>C. g ` A \<subseteq> C \<and> comm_monoid_add_on_with C pls z"
+ using that (1,2) comm_monoid_add_on_with by auto
+ ultimately show ?thesis
+ by (simp add: sum_with_def)
+qed
+
+end
+
+lemma ex_comm_monoid_add_around_imageE:
+ includes lifting_syntax
+ assumes ex_comm: "\<exists>C. f ` S \<subseteq> C \<and> comm_monoid_add_on_with C pls zero"
+ assumes transfers: "(A ===> A ===> A) pls pls'" "A zero zero'" "Domainp (rel_set B) S"
+ and in_dom: "\<And>x. x \<in> S \<Longrightarrow> Domainp A (f x)"
+ obtains C where "comm_monoid_add_on_with C pls zero" "f ` S \<subseteq> C" "Domainp (rel_set A) C"
+proof -
+ from ex_comm obtain C0 where C0: "f ` S \<subseteq> C0" and comm: "comm_monoid_add_on_with C0 pls zero"
+ by auto
+ define C where "C = C0 \<inter> Collect (Domainp A)"
+ have "comm_monoid_add_on_with C pls zero"
+ using comm Domainp_apply2I[OF \<open>(A ===> A ===> A) pls pls'\<close>] \<open>A zero zero'\<close>
+ by (auto simp: comm_monoid_add_on_with_def ab_semigroup_add_on_with_def
+ semigroup_add_on_with_def C_def)
+ moreover have "f ` S \<subseteq> C" using C0
+ by (auto simp: C_def in_dom)
+ moreover have "Domainp (rel_set A) C" by (auto simp: C_def Domainp_set)
+ ultimately show ?thesis ..
+qed
+
+lemma sum_with_transfer[transfer_rule]:
+ includes lifting_syntax
+ assumes [transfer_rule]: "right_total A" "bi_unique A" "bi_unique B"
+ shows "((A ===> A ===> A) ===> A ===> (B ===> A) ===> rel_set B ===> A)
+ sum_with sum_with"
+proof (safe intro!: rel_funI)
+ fix pls pls' zero zero' f g S T
+ assume transfer_pls[transfer_rule]: "(A ===> A ===> A) pls pls'"
+ and transfer_zero[transfer_rule]: "A zero zero'"
+ assume transfer_g[transfer_rule]: "(B ===> A) f g"
+ and transfer_T[transfer_rule]: "rel_set B S T"
+ show "A (sum_with pls zero f S) (sum_with pls' zero' g T)"
+ proof cases
+ assume ex_comm: "\<exists>C. f ` S \<subseteq> C \<and> comm_monoid_add_on_with C pls zero"
+ have Domains: "Domainp (rel_set B) S" "(\<And>x. x \<in> S \<Longrightarrow> Domainp A (f x))"
+ using transfer_T transfer_g
+ by auto (meson Domainp_applyI rel_set_def)
+ from ex_comm_monoid_add_around_imageE[OF ex_comm transfer_pls transfer_zero Domains]
+ obtain C where comm: "comm_monoid_add_on_with C pls zero"
+ and C: "f ` S \<subseteq> C"
+ and "Domainp (rel_set A) C"
+ by auto
+ then obtain C' where [transfer_rule]: "rel_set A C C'" by auto
+ have C': "g ` T \<subseteq> C'"
+ by transfer (rule C)
+ have comm': "comm_monoid_add_on_with C' pls' zero'"
+ by transfer (rule comm)
+ from C' comm' have ex_comm': "\<exists>C. g ` T \<subseteq> C \<and> comm_monoid_add_on_with C pls' zero'" by auto
+ show ?thesis
+ using transfer_T C C'
+ proof (induction S arbitrary: T rule: infinite_finite_induct)
+ case (infinite S)
+ note [transfer_rule] = infinite.prems
+ from infinite.hyps have "infinite T" by transfer
+ then show ?case by (simp add: sum_with_def infinite.hyps \<open>A zero zero'\<close>)
+ next
+ case [transfer_rule]: empty
+ have "T = {}" by transfer rule
+ then show ?case by (simp add: sum_with_def \<open>A zero zero'\<close>)
+ next
+ case (insert x F)
+ note [transfer_rule] = insert.prems(1)
+ have [simp]: "finite T"
+ by transfer (simp add: insert.hyps)
+ obtain y where [transfer_rule]: "B x y" and y: "y \<in> T"
+ by (meson insert.prems insertI1 rel_setD1)
+ define T' where "T' = T - {y}"
+ have T_def: "T = insert y T'"
+ by (auto simp: T'_def y)
+ define sF where "sF = sum_with pls zero f F"
+ define sT where "sT = sum_with pls' zero' g T'"
+ have [simp]: "y \<notin> T'" "finite T'"
+ by (auto simp: y T'_def)
+ have "rel_set B (insert x F - {x}) T'"
+ unfolding T'_def
+ by transfer_prover
+ then have transfer_T'[transfer_rule]: "rel_set B F T'"
+ using insert.hyps
+ by simp
+ from insert.prems have "f ` F \<subseteq> C" "g ` T' \<subseteq> C'"
+ by (auto simp: T'_def)
+ from insert.IH[OF transfer_T' this] have [transfer_rule]: "A sF sT" by (auto simp: sF_def sT_def o_def)
+ have rew: "(sum_with pls zero f (insert x F)) = pls (f x) (sum_with pls zero f F)"
+ apply (subst sum_with_insert[OF comm])
+ subgoal using insert.prems by auto
+ subgoal using insert.prems by auto
+ subgoal by fact
+ subgoal by fact
+ subgoal by auto
+ done
+ have rew': "(sum_with pls' zero' g (insert y T')) = pls' (g y) (sum_with pls' zero' g T')"
+ apply (subst sum_with_insert[OF comm'])
+ subgoal
+ apply transfer
+ using insert.prems by auto
+ subgoal
+ apply transfer
+ using insert.prems by auto
+ subgoal by fact
+ subgoal by fact
+ subgoal by auto
+ done
+ have "A (sum_with pls zero f (insert x F)) (sum_with pls' zero' g (insert y T'))"
+ unfolding sT_def[symmetric] sF_def[symmetric] rew rew'
+ by transfer_prover
+ then show ?case
+ by (simp add: T_def)
+ qed
+ next
+ assume *: "\<nexists>C. f ` S \<subseteq> C \<and> comm_monoid_add_on_with C pls zero"
+ then have **: "\<nexists>C'. g ` T \<subseteq> C' \<and> comm_monoid_add_on_with C' pls' zero'"
+ by transfer simp
+ show ?thesis
+ by (simp add: sum_with_def * ** \<open>A zero zero'\<close>)
+ qed
+qed
+
+subsection \<open>Rewrite rules to make \<open>ab_group_add\<close> operations explicit\<close>
+
+named_theorems explicit_ab_group_add
+
+lemmas [explicit_ab_group_add] = sum_with
+
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy Wed Jun 27 11:16:43 2018 +0200
@@ -0,0 +1,1128 @@
+(* Title: HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy
+ Author: Fabian Immler, TU München
+*)
+theory Linear_Algebra_On
+ imports
+ "../Types_To_Sets"
+ "Prerequisites"
+ Linear_Algebra_On_With
+ keywords "lemmas_with"::thy_decl
+begin
+
+subsection \<open>Rewrite rules to make \<open>ab_group_add\<close> operations implicit.\<close>
+
+named_theorems implicit_ab_group_add
+
+lemmas [implicit_ab_group_add] = sum_with[symmetric]
+
+lemma semigroup_add_on_with_eq[implicit_ab_group_add]:
+ "semigroup_add_on_with S ((+)::_::semigroup_add \<Rightarrow> _) \<longleftrightarrow> (\<forall>a\<in>S. \<forall>b\<in>S. a + b \<in> S)"
+ by (simp add: semigroup_add_on_with_def ac_simps)
+
+lemma ab_semigroup_add_on_with_eq[implicit_ab_group_add]:
+ "ab_semigroup_add_on_with S ((+)::_::ab_semigroup_add \<Rightarrow> _) = semigroup_add_on_with S (+)"
+ unfolding ab_semigroup_add_on_with_def
+ by (simp add: semigroup_add_on_with_eq ac_simps)
+
+lemma comm_monoid_add_on_with_eq[implicit_ab_group_add]:
+ "comm_monoid_add_on_with S ((+)::_::comm_monoid_add \<Rightarrow> _) 0 \<longleftrightarrow> semigroup_add_on_with S (+) \<and> 0 \<in> S"
+ unfolding comm_monoid_add_on_with_def
+ by (simp add: ab_semigroup_add_on_with_eq ac_simps)
+
+lemma ab_group_add_on_with[implicit_ab_group_add]:
+ "ab_group_add_on_with S ((+)::_::ab_group_add \<Rightarrow> _) 0 (-) uminus \<longleftrightarrow> comm_monoid_add_on_with S (+) 0"
+ unfolding ab_group_add_on_with_def
+ by simp
+
+subsection \<open>Definitions \<^emph>\<open>on\<close> carrier set\<close>
+
+locale module_on =
+ fixes S and scale :: "'a::comm_ring_1 \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*s" 75)
+ 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"
+ and scale_left_distrib_on [algebra_simps]: "x \<in> S \<Longrightarrow> (a + b) *s x = a *s x + b *s x"
+ and scale_scale_on [simp]: "x \<in> S \<Longrightarrow> a *s (b *s x) = (a * b) *s x"
+ and scale_one_on [simp]: "x \<in> S \<Longrightarrow> 1 *s x = x"
+ and mem_add: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x + y \<in> S"
+ and mem_zero: "0 \<in> S"
+ and mem_scale: "x \<in> S \<Longrightarrow> a *s x \<in> S"
+begin
+
+lemma S_ne: "S \<noteq> {}" using mem_zero by auto
+
+lemma scale_minus_left_on: "scale (- a) x = - scale a x" if "x \<in> S"
+ by (metis add_cancel_right_right scale_left_distrib_on neg_eq_iff_add_eq_0 that)
+
+definition subspace :: "'b set \<Rightarrow> bool"
+ 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)"
+
+definition span :: "'b set \<Rightarrow> 'b set"
+ where span_on_def: "span b = {sum (\<lambda>a. r a *s a) t | t r. finite t \<and> t \<subseteq> b}"
+
+definition dependent :: "'b set \<Rightarrow> bool"
+ 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)))"
+
+lemma implicit_subspace_with[implicit_ab_group_add]: "subspace_with (+) 0 ( *s) = subspace"
+ unfolding subspace_on_def subspace_with_def ..
+
+lemma implicit_dependent_with[implicit_ab_group_add]: "dependent_with (+) 0 ( *s) = dependent"
+ unfolding dependent_on_def dependent_with_def sum_with ..
+
+lemma implicit_span_with[implicit_ab_group_add]: "span_with (+) 0 ( *s) = span"
+ unfolding span_on_def span_with_def sum_with ..
+
+end
+
+lemma implicit_module_on_with[implicit_ab_group_add]:
+ "module_on_with S (+) (-) uminus 0 = module_on S"
+ unfolding module_on_with_def module_on_def implicit_ab_group_add
+ by auto
+
+locale module_pair_on = m1: module_on S1 scale1 +
+ m2: module_on S2 scale2
+ for S1:: "'b::ab_group_add set" and S2::"'c::ab_group_add set"
+ and scale1::"'a::comm_ring_1 \<Rightarrow> _" and scale2::"'a \<Rightarrow> _"
+
+lemma implicit_module_pair_on_with[implicit_ab_group_add]:
+ "module_pair_on_with S1 S2 (+) (-) uminus 0 s1 (+) (-) uminus 0 s2 = module_pair_on S1 S2 s1 s2"
+ unfolding module_pair_on_with_def implicit_module_on_with module_pair_on_def ..
+
+locale module_hom_on = m1: module_on S1 s1 + m2: module_on S2 s2
+ for S1 :: "'b::ab_group_add set" and S2 :: "'c::ab_group_add set"
+ and s1 :: "'a::comm_ring_1 \<Rightarrow> 'b \<Rightarrow> 'b" (infixr "*a" 75)
+ and s2 :: "'a::comm_ring_1 \<Rightarrow> 'c \<Rightarrow> 'c" (infixr "*b" 75) +
+ fixes f :: "'b \<Rightarrow> 'c"
+ assumes add: "\<And>b1 b2. b1 \<in> S1 \<Longrightarrow> b2 \<in> S1 \<Longrightarrow> f (b1 + b2) = f b1 + f b2"
+ and scale: "\<And>b. b \<in> S1 \<Longrightarrow> f (r *a b) = r *b f b"
+
+lemma implicit_module_hom_on_with[implicit_ab_group_add]:
+ "module_hom_on_with S1 S2 (+) (-) uminus 0 s1 (+) (-) uminus 0 s2 = module_hom_on S1 S2 s1 s2"
+ unfolding module_hom_on_with_def implicit_module_pair_on_with module_hom_on_def module_pair_on_def
+ module_hom_on_axioms_def
+ by (auto intro!: ext)
+
+locale vector_space_on = \<comment>\<open>here we do the same trick as in \<open>module\<close> vs \<open>vector_space\<close>.\<close>
+ fixes S and scale :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*s" 75)
+ assumes scale_right_distrib [algebra_simps]: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> a *s (x + y) = a *s x + a *s y"
+ and scale_left_distrib [algebra_simps]: "x \<in> S \<Longrightarrow> (a + b) *s x = a *s x + b *s x"
+ and scale_scale [simp]: "x \<in> S \<Longrightarrow> a *s (b *s x) = (a * b) *s x"
+ and scale_one [simp]: "x \<in> S \<Longrightarrow> 1 *s x = x"
+ and mem_add: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x + y \<in> S"
+ and mem_zero: "0 \<in> S"
+ and mem_scale: "x \<in> S \<Longrightarrow> a *s x \<in> S"
+begin
+
+sublocale module_on S "( *s)"
+ using vector_space_on_axioms[unfolded vector_space_on_def]
+ by unfold_locales auto
+
+definition dim :: "'b set \<Rightarrow> nat"
+ where "dim V = (if \<exists>b\<subseteq>S. \<not> dependent b \<and> span b = span V
+ then card (SOME b. b \<subseteq> S \<and> \<not> dependent b \<and> span b = span V)
+ else 0)"
+
+lemma implicit_dim_with[implicit_ab_group_add]: "dim_on_with S (+) 0 ( *s) = dim"
+ unfolding dim_on_with_def dim_def implicit_ab_group_add ..
+
+end
+
+lemma vector_space_on_alt_def: "vector_space_on S = module_on S"
+ unfolding vector_space_on_def module_on_def
+ by auto
+
+lemma implicit_vector_space_on_with[implicit_ab_group_add]:
+ "vector_space_on_with S (+) (-) uminus 0 = vector_space_on S"
+ unfolding vector_space_on_alt_def vector_space_on_def vector_space_on_with_def implicit_module_on_with ..
+
+locale linear_on = module_hom_on S1 S2 s1 s2 f
+ for S1 S2 and s1::"'a::field \<Rightarrow> 'b \<Rightarrow> 'b::ab_group_add"
+ and s2::"'a::field \<Rightarrow> 'c \<Rightarrow> 'c::ab_group_add"
+ and f
+
+lemma implicit_linear_on_with[implicit_ab_group_add]:
+ "linear_on_with S1 S2 (+) (-) uminus 0 s1 (+) (-) uminus 0 s2 = linear_on S1 S2 s1 s2"
+ unfolding linear_on_with_def linear_on_def implicit_module_hom_on_with ..
+
+locale finite_dimensional_vector_space_on = vector_space_on S scale for S scale +
+ fixes basis :: "'a set"
+ assumes finite_Basis: "finite basis"
+ and independent_Basis: "\<not> dependent basis"
+ and span_Basis: "span basis = S" and basis_subset: "basis \<subseteq> S"
+
+locale vector_space_pair_on = m1: vector_space_on S1 scale1 +
+ m2: vector_space_on S2 scale2
+ for S1:: "'b::ab_group_add set" and S2::"'c::ab_group_add set"
+ and scale1::"'a::field \<Rightarrow> _" and scale2::"'a \<Rightarrow> _"
+
+locale finite_dimensional_vector_space_pair_on =
+ vs1: finite_dimensional_vector_space_on S1 scale1 Basis1 +
+ vs2: finite_dimensional_vector_space_on S2 scale2 Basis2
+ for S1 S2
+ and scale1::"'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b"
+ and scale2::"'a::field \<Rightarrow> 'c::ab_group_add \<Rightarrow> 'c"
+ and Basis1 Basis2
+
+subsection \<open>Tool support\<close>
+
+lemmas subset_iff' = subset_iff[folded Ball_def]
+
+ML \<open>
+structure More_Simplifier =
+struct
+
+fun asm_full_var_simplify ctxt thm =
+ let
+ val ((_, [thm']), ctxt') = Variable.import false [thm] ctxt
+ in
+ Simplifier.asm_full_simplify ctxt' thm'
+ |> singleton (Variable.export ctxt' ctxt)
+ |> Drule.zero_var_indexes
+ end
+
+fun var_simplify_only ctxt ths thm =
+ asm_full_var_simplify (Raw_Simplifier.clear_simpset ctxt addsimps ths) thm
+
+val var_simplified = Attrib.thms >>
+ (fn ths => Thm.rule_attribute ths
+ (fn context => var_simplify_only (Context.proof_of context) ths))
+
+val _ = Theory.setup (Attrib.setup \<^binding>\<open>var_simplified\<close> var_simplified "simplified rule (with vars)")
+
+end
+\<close>
+
+ML \<open>
+val _ = Outer_Syntax.local_theory' \<^command_keyword>\<open>lemmas_with\<close> "note theorems with (the same) attributes"
+ (Parse.attribs --| @{keyword :} -- Parse_Spec.name_facts -- Parse.for_fixes
+ >> (fn (((attrs),facts), fixes) =>
+ #2 oo Specification.theorems_cmd Thm.theoremK
+ (map (apsnd (map (apsnd (fn xs => attrs@xs)))) facts) fixes))
+\<close>
+
+subsection \<open>Local Typedef for Subspace\<close>
+
+lemmas [transfer_rule] = right_total_fun_eq_transfer
+ and [transfer_rule del] = vimage_parametric
+
+locale local_typedef = fixes S ::"'b set" and s::"'s itself"
+ assumes Ex_type_definition_S: "\<exists>(Rep::'s \<Rightarrow> 'b) (Abs::'b \<Rightarrow> 's). type_definition Rep Abs S"
+begin
+
+definition "rep = fst (SOME (Rep::'s \<Rightarrow> 'b, Abs). type_definition Rep Abs S)"
+definition "Abs = snd (SOME (Rep::'s \<Rightarrow> 'b, Abs). type_definition Rep Abs S)"
+
+lemma type_definition_S: "type_definition rep Abs S"
+ unfolding Abs_def rep_def split_beta'
+ by (rule someI_ex) (use Ex_type_definition_S in auto)
+
+lemma rep_in_S[simp]: "rep x \<in> S"
+ and rep_inverse[simp]: "Abs (rep x) = x"
+ and Abs_inverse[simp]: "y \<in> S \<Longrightarrow> rep (Abs y) = y"
+ using type_definition_S
+ unfolding type_definition_def by auto
+
+definition cr_S where "cr_S \<equiv> \<lambda>s b. s = rep b"
+lemmas Domainp_cr_S = type_definition_Domainp[OF type_definition_S cr_S_def, transfer_domain_rule]
+lemmas right_total_cr_S = typedef_right_total[OF type_definition_S cr_S_def, transfer_rule]
+ and bi_unique_cr_S = typedef_bi_unique[OF type_definition_S cr_S_def, transfer_rule]
+ and left_unique_cr_S = typedef_left_unique[OF type_definition_S cr_S_def, transfer_rule]
+ and right_unique_cr_S = typedef_right_unique[OF type_definition_S cr_S_def, transfer_rule]
+
+end
+
+locale local_typedef_ab_group_add = local_typedef S s for S ::"'b::ab_group_add set" and s::"'s itself" +
+ assumes mem_zero: "0 \<in> S"
+ assumes mem_add: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x + y \<in> S"
+ assumes mem_uminus: "x \<in> S \<Longrightarrow> -x \<in> S"
+begin
+
+lemma mem_minus: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x - y \<in> S"
+ using mem_add[OF _ mem_uminus] by auto
+
+context includes lifting_syntax begin
+
+definition plus_S::"'s \<Rightarrow> 's \<Rightarrow> 's" where "plus_S = (rep ---> rep ---> Abs) plus"
+definition minus_S::"'s \<Rightarrow> 's \<Rightarrow> 's" where "minus_S = (rep ---> rep ---> Abs) minus"
+definition uminus_S::"'s \<Rightarrow> 's" where "uminus_S = (rep ---> Abs) uminus"
+definition zero_S::"'s" where "zero_S = Abs 0"
+
+lemma plus_S_transfer[transfer_rule]: "(cr_S ===> cr_S ===> cr_S) plus plus_S"
+ unfolding plus_S_def
+ by (auto simp: cr_S_def mem_add intro!: rel_funI)
+
+lemma minus_S_transfer[transfer_rule]: "(cr_S ===> cr_S ===> cr_S) minus minus_S"
+ unfolding minus_S_def
+ by (auto simp: cr_S_def mem_minus intro!: rel_funI)
+
+lemma uminus_S_transfer[transfer_rule]: "(cr_S ===> cr_S) uminus uminus_S"
+ unfolding uminus_S_def
+ by (auto simp: cr_S_def mem_uminus intro!: rel_funI)
+
+lemma zero_S_transfer[transfer_rule]: "cr_S 0 zero_S"
+ unfolding zero_S_def
+ by (auto simp: cr_S_def mem_zero intro!: rel_funI)
+
+end
+
+sublocale type: ab_group_add plus_S "zero_S::'s" minus_S uminus_S
+ apply unfold_locales
+ subgoal by transfer simp
+ subgoal by transfer simp
+ subgoal by transfer simp
+ subgoal by transfer simp
+ subgoal by transfer simp
+ done
+
+context includes lifting_syntax begin
+
+lemma sum_transfer[transfer_rule]: "((A===>cr_S) ===> rel_set A ===> cr_S) sum type.sum"
+ if [transfer_rule]: "bi_unique A"
+proof (safe intro!: rel_funI)
+ fix f g S T
+ assume [transfer_rule]: "(A ===> cr_S) f g" and rel_set: "rel_set A S T"
+ show "cr_S (sum f S) (type.sum g T)"
+ using rel_set
+ proof (induction S arbitrary: T rule: infinite_finite_induct)
+ case (infinite S)
+ note [transfer_rule] = infinite.prems
+ from infinite.hyps have "infinite T" by transfer
+ then show ?case by (simp add: infinite.hyps zero_S_transfer)
+ next
+ case [transfer_rule]: empty
+ have "T = {}" by transfer rule
+ then show ?case by (simp add: zero_S_transfer)
+ next
+ case (insert x F)
+ note [transfer_rule] = insert.prems
+ have [simp]: "finite T"
+ by transfer (simp add: insert.hyps)
+ obtain y where [transfer_rule]: "A x y" and y: "y \<in> T"
+ by (meson insert.prems insertI1 rel_setD1)
+ define T' where "T' = T - {y}"
+ have T_def: "T = insert y T'"
+ by (auto simp: T'_def y)
+ define sF where "sF = sum f F"
+ define sT where "sT = type.sum g T'"
+ have [simp]: "y \<notin> T'" "finite T'"
+ by (auto simp: y T'_def)
+ have "rel_set A (insert x F - {x}) T'"
+ unfolding T'_def
+ by transfer_prover
+ then have "rel_set A F T'"
+ using insert.hyps
+ by simp
+ from insert.IH[OF this] have [transfer_rule]: "cr_S sF sT" by (auto simp: sF_def sT_def)
+ have "cr_S (sum f (insert x F)) (type.sum g (insert y T'))"
+ apply (simp add: insert.hyps type.sum.insert_remove sF_def[symmetric] sT_def[symmetric])
+ by transfer_prover
+ then show ?case
+ by (simp add: T_def)
+ qed
+qed
+
+end
+
+end
+
+locale local_typedef_module_on = module_on S scale
+ for S and scale::"'a::comm_ring_1\<Rightarrow>'b\<Rightarrow>'b::ab_group_add" and s::"'s itself" +
+ assumes Ex_type_definition_S: "\<exists>(Rep::'s \<Rightarrow> 'b) (Abs::'b \<Rightarrow> 's). type_definition Rep Abs S"
+begin
+
+lemma mem_sum: "sum f X \<in> S" if "\<And>x. x \<in> X \<Longrightarrow> f x \<in> S"
+ using that
+ by (induction X rule: infinite_finite_induct) (auto intro!: mem_zero mem_add)
+
+sublocale local_typedef S "TYPE('s)"
+ using Ex_type_definition_S by unfold_locales
+
+sublocale local_typedef_ab_group_add S "TYPE('s)"
+ using mem_zero mem_add mem_scale[of _ "-1"]
+ by unfold_locales (auto simp: scale_minus_left_on)
+
+context includes lifting_syntax begin
+
+definition scale_S::"'a \<Rightarrow> 's \<Rightarrow> 's" where "scale_S = (id ---> rep ---> Abs) scale"
+
+lemma scale_S_transfer[transfer_rule]: "((=) ===> cr_S ===> cr_S) scale scale_S"
+ unfolding scale_S_def
+ by (auto simp: cr_S_def mem_scale intro!: rel_funI)
+
+end
+
+lemma type_module_on_with: "module_on_with UNIV plus_S minus_S uminus_S (zero_S::'s) scale_S"
+proof -
+ have "module_on_with {x. x \<in> S} (+) (-) uminus 0 scale"
+ using module_on_axioms
+ by (auto simp: module_on_with_def module_on_def ab_group_add_on_with_def comm_monoid_add_on_with_def
+ ab_semigroup_add_on_with_def semigroup_add_on_with_def)
+ then show ?thesis
+ by transfer'
+qed
+
+lemma UNIV_transfer[transfer_rule]: "(rel_set cr_S) S UNIV"
+ by (auto simp: rel_set_def cr_S_def) (metis Abs_inverse)
+
+end
+
+context includes lifting_syntax begin
+
+lemma Eps_unique_transfer_lemma:
+ "f' (Eps (\<lambda>x. Domainp A x \<and> f x)) = g' (Eps g)"
+ if [transfer_rule]: "right_total A" "(A ===> (=)) f g" "(A ===> (=)) f' g'"
+ and holds: "\<exists>x. Domainp A x \<and> f x"
+ and unique_g: "\<And>x y. g x \<Longrightarrow> g y \<Longrightarrow> g' x = g' y"
+proof -
+ define Epsg where "Epsg = Eps g"
+ have "\<exists>x. g x"
+ by transfer (simp add: holds)
+ then have "g Epsg"
+ unfolding Epsg_def
+ by (rule someI_ex)
+ obtain x where x[transfer_rule]: "A x Epsg"
+ by (meson \<open>right_total A\<close> right_totalE)
+ then have "Domainp A x" by auto
+ from \<open>g Epsg\<close>[untransferred] have "f x" .
+ from unique_g have unique:
+ "\<And>x y. Domainp A x \<Longrightarrow> Domainp A y \<Longrightarrow> f x \<Longrightarrow> f y \<Longrightarrow> f' x = f' y"
+ by transfer
+ have "f' (Eps (\<lambda>x. Domainp A x \<and> f x)) = f' x"
+ apply (rule unique[OF _ \<open>Domainp A x\<close> _ \<open>f x\<close>])
+ apply (metis (mono_tags, lifting) local.holds someI_ex)
+ apply (metis (mono_tags, lifting) local.holds someI_ex)
+ done
+ show "f' (SOME x. Domainp A x \<and> f x) = g' (Eps g)"
+ using x \<open>f' (Eps _) = f' x\<close> Epsg_def
+ using rel_funE that(3) by fastforce
+qed
+
+end
+
+locale local_typedef_vector_space_on = local_typedef_module_on S scale s + vector_space_on S scale
+ for S and scale::"'a::field\<Rightarrow>'b\<Rightarrow>'b::ab_group_add" and s::"'s itself"
+begin
+
+lemma type_vector_space_on_with: "vector_space_on_with UNIV plus_S minus_S uminus_S (zero_S::'s) scale_S"
+ using type_module_on_with
+ by (auto simp: vector_space_on_with_def)
+
+context includes lifting_syntax begin
+
+definition dim_S::"'s set \<Rightarrow> nat" where "dim_S = dim_on_with UNIV plus_S zero_S scale_S"
+
+lemma transfer_dim[transfer_rule]: "(rel_set cr_S ===> (=)) dim dim_S"
+proof (rule rel_funI)
+ fix V V'
+ assume [transfer_rule]: "rel_set cr_S V V'"
+ then have subset: "V \<subseteq> S"
+ by (auto simp: rel_set_def cr_S_def)
+ then have "span V \<subseteq> S"
+ by (auto simp: span_on_def intro!: mem_sum mem_scale)
+ note type_dim_eq_card =
+ vector_space.dim_eq_card[var_simplified explicit_ab_group_add, unoverload_type 'd,
+ OF type.ab_group_add_axioms type_vector_space_on_with]
+ 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>
+ (\<exists>b\<subseteq>S. \<not> local.dependent b \<and> local.span b = local.span V)"
+ unfolding subset_iff
+ by transfer (simp add: implicit_ab_group_add Ball_def)
+ have **[symmetric]:
+ "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)) =
+ 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')"
+ if "b \<subseteq> S" "\<not>dependent b" "span b = span V" for b
+ apply (rule Eps_unique_transfer_lemma[where f'=card and g'=card])
+ subgoal by (rule right_total_rel_set) (rule transfer_raw)
+ subgoal by transfer_prover
+ subgoal by transfer_prover
+ subgoal using that by (auto simp: implicit_ab_group_add Domainp_set Domainp_cr_S)
+ subgoal premises prems for b c
+ proof -
+ from type_dim_eq_card[of b V'] type_dim_eq_card[of c V'] prems
+ show ?thesis by simp
+ qed
+ done
+ show "local.dim V = dim_S V'"
+ unfolding dim_def dim_S_def * dim_on_with_def
+ by (auto simp: ** Domainp_set Domainp_cr_S implicit_ab_group_add subset_eq)
+qed
+
+end
+
+
+end
+
+locale local_typedef_finite_dimensional_vector_space_on = local_typedef_vector_space_on S scale s +
+ finite_dimensional_vector_space_on S scale Basis
+ for S and scale::"'a::field\<Rightarrow>'b\<Rightarrow>'b::ab_group_add" and Basis and s::"'s itself"
+begin
+
+definition "Basis_S = Abs ` Basis"
+
+lemma Basis_S_transfer[transfer_rule]: "rel_set cr_S Basis Basis_S"
+ using Abs_inverse rep_inverse basis_subset
+ by (force simp: rel_set_def Basis_S_def cr_S_def)
+
+lemma type_finite_dimensional_vector_space_on_with:
+ "finite_dimensional_vector_space_on_with UNIV plus_S minus_S uminus_S zero_S scale_S Basis_S"
+proof -
+ have "finite Basis_S" by transfer (rule finite_Basis)
+ moreover have "\<not> dependent_with plus_S zero_S scale_S Basis_S"
+ by transfer (simp add: implicit_dependent_with independent_Basis)
+ moreover have "span_with plus_S zero_S scale_S Basis_S = UNIV"
+ by transfer (simp add: implicit_span_with span_Basis)
+ ultimately show ?thesis
+ using type_vector_space_on_with
+ by (auto simp: finite_dimensional_vector_space_on_with_def)
+qed
+
+end
+
+locale local_typedef_module_pair =
+ lt1: local_typedef_module_on S1 scale1 s +
+ lt2: local_typedef_module_on S2 scale2 t
+ for S1::"'b::ab_group_add set" and scale1::"'a::comm_ring_1 \<Rightarrow> 'b \<Rightarrow> 'b" and s::"'s itself"
+ and S2::"'c::ab_group_add set" and scale2::"'a \<Rightarrow> 'c \<Rightarrow> 'c" and t::"'t itself"
+begin
+
+lemma type_module_pair_on_with:
+ "module_pair_on_with UNIV UNIV lt1.plus_S lt1.minus_S lt1.uminus_S (lt1.zero_S::'s) lt1.scale_S
+ lt2.plus_S lt2.minus_S lt2.uminus_S (lt2.zero_S::'t) lt2.scale_S"
+ by (simp add: lt1.type_module_on_with lt2.type_module_on_with module_pair_on_with_def)
+
+end
+
+locale local_typedef_vector_space_pair =
+ local_typedef_module_pair S1 scale1 s S2 scale2 t
+ for S1::"'b::ab_group_add set" and scale1::"'a::field \<Rightarrow> 'b \<Rightarrow> 'b" and s::"'s itself"
+ and S2::"'c::ab_group_add set" and scale2::"'a \<Rightarrow> 'c \<Rightarrow> 'c" and t::"'t itself"
+begin
+
+lemma type_vector_space_pair_on_with:
+ "vector_space_pair_on_with UNIV UNIV lt1.plus_S lt1.minus_S lt1.uminus_S (lt1.zero_S::'s) lt1.scale_S
+ lt2.plus_S lt2.minus_S lt2.uminus_S (lt2.zero_S::'t) lt2.scale_S"
+ by (simp add: type_module_pair_on_with vector_space_pair_on_with_def)
+
+end
+
+locale local_typedef_finite_dimensional_vector_space_pair =
+ lt1: local_typedef_finite_dimensional_vector_space_on S1 scale1 Basis1 s +
+ lt2: local_typedef_finite_dimensional_vector_space_on S2 scale2 Basis2 t
+ for S1::"'b::ab_group_add set" and scale1::"'a::field \<Rightarrow> 'b \<Rightarrow> 'b" and Basis1 and s::"'s itself"
+ and S2::"'c::ab_group_add set" and scale2::"'a \<Rightarrow> 'c \<Rightarrow> 'c" and Basis2 and t::"'t itself"
+begin
+
+lemma type_finite_dimensional_vector_space_pair_on_with:
+ "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
+ lt2.plus_S lt2.minus_S lt2.uminus_S (lt2.zero_S::'t) lt2.scale_S lt2.Basis_S"
+ by (simp add: finite_dimensional_vector_space_pair_on_with_def
+ lt1.type_finite_dimensional_vector_space_on_with
+ lt2.type_finite_dimensional_vector_space_on_with)
+
+end
+
+subsection \<open>Transfer from type-based @{theory HOL.Modules} and @{theory HOL.Vector_Spaces}\<close>
+
+context module_on begin
+
+context includes lifting_syntax assumes ltd: "\<exists>(Rep::'s \<Rightarrow> 'b) (Abs::'b \<Rightarrow> 's). type_definition Rep Abs S" begin
+
+interpretation local_typedef_module_on S scale "TYPE('s)" by unfold_locales fact
+
+text\<open>Get theorem names:\<close>
+print_locale! module
+text\<open>Then replace:
+notes[^"]*"([^"]*).*
+with $1 = module.$1
+\<close>
+text \<open>TODO: automate systematic naming!\<close>
+lemmas_with [var_simplified explicit_ab_group_add,
+ unoverload_type 'd,
+ OF type.ab_group_add_axioms type_module_on_with,
+ untransferred,
+ var_simplified implicit_ab_group_add]:
+ lt_scale_right_distrib = module.scale_right_distrib
+ and lt_scale_left_distrib = module.scale_left_distrib
+ and lt_scale_scale = module.scale_scale
+ and lt_scale_one = module.scale_one
+ and lt_scale_left_commute = module.scale_left_commute
+ and lt_scale_zero_left = module.scale_zero_left
+ and lt_scale_minus_left = module.scale_minus_left
+ and lt_scale_left_diff_distrib = module.scale_left_diff_distrib
+ and lt_scale_sum_left = module.scale_sum_left
+ and lt_scale_zero_right = module.scale_zero_right
+ and lt_scale_minus_right = module.scale_minus_right
+ and lt_scale_right_diff_distrib = module.scale_right_diff_distrib
+ and lt_scale_sum_right = module.scale_sum_right
+ and lt_sum_constant_scale = module.sum_constant_scale
+ and lt_subspace_def = module.subspace_def
+ and lt_subspaceI = module.subspaceI
+ and lt_subspace_single_0 = module.subspace_single_0
+ and lt_subspace_0 = module.subspace_0
+ and lt_subspace_add = module.subspace_add
+ and lt_subspace_scale = module.subspace_scale
+ and lt_subspace_neg = module.subspace_neg
+ and lt_subspace_diff = module.subspace_diff
+ and lt_subspace_sum = module.subspace_sum
+ and lt_subspace_inter = module.subspace_inter
+ and lt_span_explicit = module.span_explicit
+ and lt_span_explicit' = module.span_explicit'
+ and lt_span_finite = module.span_finite
+ and lt_span_induct_alt = module.span_induct_alt
+ and lt_span_mono = module.span_mono
+ and lt_span_base = module.span_base
+ and lt_span_superset = module.span_superset
+ and lt_span_zero = module.span_zero
+ and lt_span_add = module.span_add
+ and lt_span_scale = module.span_scale
+ and lt_subspace_span = module.subspace_span
+ and lt_span_neg = module.span_neg
+ and lt_span_diff = module.span_diff
+ and lt_span_sum = module.span_sum
+ and lt_span_minimal = module.span_minimal
+ and lt_span_unique = module.span_unique
+ and lt_span_subspace_induct = module.span_subspace_induct
+ and lt_span_induct = module.span_induct
+ and lt_span_empty = module.span_empty
+ and lt_span_subspace = module.span_subspace
+ and lt_span_span = module.span_span
+ and lt_span_add_eq = module.span_add_eq
+ and lt_span_add_eq2 = module.span_add_eq2
+ and lt_span_singleton = module.span_singleton
+ and lt_span_Un = module.span_Un
+ and lt_span_insert = module.span_insert
+ and lt_span_breakdown = module.span_breakdown
+ and lt_span_breakdown_eq = module.span_breakdown_eq
+ and lt_span_clauses = module.span_clauses
+ and lt_span_eq_iff = module.span_eq_iff
+ and lt_span_eq = module.span_eq
+ and lt_eq_span_insert_eq = module.eq_span_insert_eq
+ and lt_dependent_explicit = module.dependent_explicit
+ and lt_dependent_mono = module.dependent_mono
+ and lt_independent_mono = module.independent_mono
+ and lt_dependent_zero = module.dependent_zero
+ and lt_independent_empty = module.independent_empty
+ and lt_independent_explicit_module = module.independent_explicit_module
+ and lt_independentD = module.independentD
+ and lt_independent_Union_directed = module.independent_Union_directed
+ and lt_dependent_finite = module.dependent_finite
+ and lt_independentD_alt = module.independentD_alt
+ and lt_independentD_unique = module.independentD_unique
+ and lt_spanning_subset_independent = module.spanning_subset_independent
+ and lt_module_hom_scale_self = module.module_hom_scale_self
+ and lt_module_hom_scale_left = module.module_hom_scale_left
+ and lt_module_hom_id = module.module_hom_id
+ and lt_module_hom_ident = module.module_hom_ident
+ and lt_module_hom_uminus = module.module_hom_uminus
+ and subspace_UNIV = module.subspace_UNIV
+ and span_alt = module.span_alt
+(* should work but don't:
+ and span_def = module.span_def
+ and span_UNIV = module.span_UNIV
+ and dependent_alt = module.dependent_alt
+ and independent_alt = module.independent_alt
+ and unique_representation = module.unique_representation
+ and subspace_Int = module.subspace_Int
+ and subspace_Inter = module.subspace_Inter
+*)
+(* not expected to work:
+and representation_ne_zero = module.representation_ne_zero
+and representation_ne_zero = module.representation_ne_zero
+and finite_representation = module.finite_representation
+and sum_nonzero_representation_eq = module.sum_nonzero_representation_eq
+and sum_representation_eq = module.sum_representation_eq
+and representation_eqI = module.representation_eqI
+and representation_basis = module.representation_basis
+and representation_zero = module.representation_zero
+and representation_diff = module.representation_diff
+and representation_neg = module.representation_neg
+and representation_add = module.representation_add
+and representation_sum = module.representation_sum
+and representation_scale = module.representation_scale
+and representation_extend = module.representation_extend
+end
+*)
+
+end
+
+lemmas_with [cancel_type_definition,
+ OF S_ne,
+ folded subset_iff',
+ simplified pred_fun_def,
+ simplified\<comment>\<open>too much?\<close>]:
+ scale_right_distrib = lt_scale_right_distrib
+ and scale_left_distrib = lt_scale_left_distrib
+ and scale_scale = lt_scale_scale
+ and scale_one = lt_scale_one
+ and scale_left_commute = lt_scale_left_commute
+ and scale_zero_left = lt_scale_zero_left
+ and scale_minus_left = lt_scale_minus_left
+ and scale_left_diff_distrib = lt_scale_left_diff_distrib
+ and scale_sum_left = lt_scale_sum_left
+ and scale_zero_right = lt_scale_zero_right
+ and scale_minus_right = lt_scale_minus_right
+ and scale_right_diff_distrib = lt_scale_right_diff_distrib
+ and scale_sum_right = lt_scale_sum_right
+ and sum_constant_scale = lt_sum_constant_scale
+ and subspace_def = lt_subspace_def
+ and subspaceI = lt_subspaceI
+ and subspace_single_0 = lt_subspace_single_0
+ and subspace_0 = lt_subspace_0
+ and subspace_add = lt_subspace_add
+ and subspace_scale = lt_subspace_scale
+ and subspace_neg = lt_subspace_neg
+ and subspace_diff = lt_subspace_diff
+ and subspace_sum = lt_subspace_sum
+ and subspace_inter = lt_subspace_inter
+ and span_explicit = lt_span_explicit
+ and span_explicit' = lt_span_explicit'
+ and span_finite = lt_span_finite
+ and span_induct_alt[consumes 1, case_names base step, induct set : span] = lt_span_induct_alt
+ and span_mono = lt_span_mono
+ and span_base = lt_span_base
+ and span_superset = lt_span_superset
+ and span_zero = lt_span_zero
+ and span_add = lt_span_add
+ and span_scale = lt_span_scale
+ and subspace_span = lt_subspace_span
+ and span_neg = lt_span_neg
+ and span_diff = lt_span_diff
+ and span_sum = lt_span_sum
+ and span_minimal = lt_span_minimal
+ and span_unique = lt_span_unique
+ and span_subspace_induct[consumes 2] = lt_span_subspace_induct
+ and span_induct[consumes 1, case_names base step, induct set : span] = lt_span_induct
+ and span_empty = lt_span_empty
+ and span_subspace = lt_span_subspace
+ and span_span = lt_span_span
+ and span_add_eq = lt_span_add_eq
+ and span_add_eq2 = lt_span_add_eq2
+ and span_singleton = lt_span_singleton
+ and span_Un = lt_span_Un
+ and span_insert = lt_span_insert
+ and span_breakdown = lt_span_breakdown
+ and span_breakdown_eq = lt_span_breakdown_eq
+ and span_clauses = lt_span_clauses
+ and span_eq_iff = lt_span_eq_iff
+ and span_eq = lt_span_eq
+ and eq_span_insert_eq = lt_eq_span_insert_eq
+ and dependent_explicit = lt_dependent_explicit
+ and dependent_mono = lt_dependent_mono
+ and independent_mono = lt_independent_mono
+ and dependent_zero = lt_dependent_zero
+ and independent_empty = lt_independent_empty
+ and independent_explicit_module = lt_independent_explicit_module
+ and independentD = lt_independentD
+ and independent_Union_directed = lt_independent_Union_directed
+ and dependent_finite = lt_dependent_finite
+ and independentD_alt = lt_independentD_alt
+ and independentD_unique = lt_independentD_unique
+ and spanning_subset_independent = lt_spanning_subset_independent
+ and module_hom_scale_self = lt_module_hom_scale_self
+ and module_hom_scale_left = lt_module_hom_scale_left
+ and module_hom_id = lt_module_hom_id
+ and module_hom_ident = lt_module_hom_ident
+ and module_hom_uminus = lt_module_hom_uminus
+
+end
+
+subsubsection \<open>Vector Spaces\<close>
+
+context vector_space_on begin
+
+context includes lifting_syntax assumes "\<exists>(Rep::'s \<Rightarrow> 'b) (Abs::'b \<Rightarrow> 's). type_definition Rep Abs S" begin
+
+interpretation local_typedef_vector_space_on S scale "TYPE('s)" by unfold_locales fact
+
+lemmas_with [var_simplified explicit_ab_group_add,
+ unoverload_type 'd,
+ OF type.ab_group_add_axioms type_vector_space_on_with,
+ untransferred,
+ var_simplified implicit_ab_group_add]:
+ lt_vector_space_assms = vector_space.vector_space_assms
+and lt_linear_id = vector_space.linear_id
+and lt_linear_ident = vector_space.linear_ident
+and lt_linear_scale_self = vector_space.linear_scale_self
+and lt_linear_scale_left = vector_space.linear_scale_left
+and lt_linear_uminus = vector_space.linear_uminus
+and lt_linear_imp_scale["consumes" - 1, "case_names" "1"] = vector_space.linear_imp_scale
+and lt_scale_eq_0_iff = vector_space.scale_eq_0_iff
+and lt_scale_left_imp_eq = vector_space.scale_left_imp_eq
+and lt_scale_right_imp_eq = vector_space.scale_right_imp_eq
+and lt_scale_cancel_left = vector_space.scale_cancel_left
+and lt_scale_cancel_right = vector_space.scale_cancel_right
+and lt_injective_scale = vector_space.injective_scale
+and lt_dependent_def = vector_space.dependent_def
+and lt_dependent_single = vector_space.dependent_single
+and lt_in_span_insert = vector_space.in_span_insert
+and lt_dependent_insertD = vector_space.dependent_insertD
+and lt_independent_insertI = vector_space.independent_insertI
+and lt_independent_insert = vector_space.independent_insert
+and lt_maximal_independent_subset_extend["consumes" - 1, "case_names" "1"] = vector_space.maximal_independent_subset_extend
+and lt_maximal_independent_subset["consumes" - 1, "case_names" "1"] = vector_space.maximal_independent_subset
+and lt_in_span_delete = vector_space.in_span_delete
+and lt_span_redundant = vector_space.span_redundant
+and lt_span_trans = vector_space.span_trans
+and lt_span_insert_0 = vector_space.span_insert_0
+and lt_span_delete_0 = vector_space.span_delete_0
+and lt_span_image_scale = vector_space.span_image_scale
+and lt_exchange_lemma = vector_space.exchange_lemma
+and lt_independent_span_bound = vector_space.independent_span_bound
+and lt_independent_explicit_finite_subsets = vector_space.independent_explicit_finite_subsets
+and lt_independent_if_scalars_zero = vector_space.independent_if_scalars_zero
+and lt_subspace_sums = vector_space.subspace_sums
+(* should work but don't:
+and lt_injective_scale = vector_space.lt_injective_scale
+and lt_bij_if_span_eq_span_bases = vector_space.bij_if_span_eq_span_bases
+and lt_dim_def = vector_space.dim_def
+and lt_dim_eq_card = vector_space.dim_eq_card
+and lt_basis_card_eq_dim = vector_space.basis_card_eq_dim
+and lt_basis_exists["consumes" - 1, "case_names" "1"] = vector_space.basis_exists
+and lt_dim_eq_card_independent = vector_space.dim_eq_card_independent
+and lt_dim_span = vector_space.dim_span
+and lt_dim_span_eq_card_independent = vector_space.dim_span_eq_card_independent
+and lt_dim_le_card = vector_space.dim_le_card
+and lt_span_eq_dim = vector_space.span_eq_dim
+and lt_dim_le_card' = vector_space.dim_le_card'
+and lt_span_card_ge_dim = vector_space.span_card_ge_dim
+and lt_dim_unique = vector_space.dim_unique
+and lt_dim_with = vector_space.dim_with
+*)
+(* not expected to work:
+and lt_extend_basis_superset = vector_space.extend_basis_superset
+and lt_independent_extend_basis = vector_space.independent_extend_basis
+and lt_span_extend_basis = vector_space.span_extend_basis
+*)
+
+end
+
+lemmas_with [cancel_type_definition,
+ OF S_ne,
+ folded subset_iff',
+ simplified pred_fun_def,
+ simplified\<comment>\<open>too much?\<close>]:
+ vector_space_assms = lt_vector_space_assms
+and linear_id = lt_linear_id
+and linear_ident = lt_linear_ident
+and linear_scale_self = lt_linear_scale_self
+and linear_scale_left = lt_linear_scale_left
+and linear_uminus = lt_linear_uminus
+and linear_imp_scale["consumes" - 1, "case_names" "1"] = lt_linear_imp_scale
+and scale_eq_0_iff = lt_scale_eq_0_iff
+and scale_left_imp_eq = lt_scale_left_imp_eq
+and scale_right_imp_eq = lt_scale_right_imp_eq
+and scale_cancel_left = lt_scale_cancel_left
+and scale_cancel_right = lt_scale_cancel_right
+and dependent_def = lt_dependent_def
+and dependent_single = lt_dependent_single
+and in_span_insert = lt_in_span_insert
+and dependent_insertD = lt_dependent_insertD
+and independent_insertI = lt_independent_insertI
+and independent_insert = lt_independent_insert
+and maximal_independent_subset_extend["consumes" - 1, "case_names" "1"] = lt_maximal_independent_subset_extend
+and maximal_independent_subset["consumes" - 1, "case_names" "1"] = lt_maximal_independent_subset
+and in_span_delete = lt_in_span_delete
+and span_redundant = lt_span_redundant
+and span_trans = lt_span_trans
+and span_insert_0 = lt_span_insert_0
+and span_delete_0 = lt_span_delete_0
+and span_image_scale = lt_span_image_scale
+and exchange_lemma = lt_exchange_lemma
+and independent_span_bound = lt_independent_span_bound
+and independent_explicit_finite_subsets = lt_independent_explicit_finite_subsets
+and independent_if_scalars_zero = lt_independent_if_scalars_zero
+and subspace_sums = lt_subspace_sums
+
+end
+
+subsubsection \<open>Finite Dimensional Vector Spaces\<close>
+
+context finite_dimensional_vector_space_on begin
+
+context includes lifting_syntax assumes "\<exists>(Rep::'s \<Rightarrow> 'a) (Abs::'a \<Rightarrow> 's). type_definition Rep Abs S" begin
+
+interpretation local_typedef_finite_dimensional_vector_space_on S scale basis "TYPE('s)" by unfold_locales fact
+
+lemmas_with [var_simplified explicit_ab_group_add,
+ unoverload_type 'd,
+ OF type.ab_group_add_axioms type_finite_dimensional_vector_space_on_with,
+ folded dim_S_def,
+ untransferred,
+ var_simplified implicit_ab_group_add]:
+ lt_finiteI_independent = finite_dimensional_vector_space.finiteI_independent
+and lt_dim_empty = finite_dimensional_vector_space.dim_empty
+and lt_dim_insert = finite_dimensional_vector_space.dim_insert
+and lt_dim_singleton = finite_dimensional_vector_space.dim_singleton
+and lt_choose_subspace_of_subspace["consumes" - 1, "case_names" "1"] = finite_dimensional_vector_space.choose_subspace_of_subspace
+and lt_basis_subspace_exists["consumes" - 1, "case_names" "1"] = finite_dimensional_vector_space.basis_subspace_exists
+and lt_dim_mono = finite_dimensional_vector_space.dim_mono
+and lt_dim_subset = finite_dimensional_vector_space.dim_subset
+and lt_dim_eq_0 = finite_dimensional_vector_space.dim_eq_0
+and lt_dim_UNIV = finite_dimensional_vector_space.dim_UNIV
+and lt_independent_card_le_dim = finite_dimensional_vector_space.independent_card_le_dim
+and lt_card_ge_dim_independent = finite_dimensional_vector_space.card_ge_dim_independent
+and lt_card_le_dim_spanning = finite_dimensional_vector_space.card_le_dim_spanning
+and lt_card_eq_dim = finite_dimensional_vector_space.card_eq_dim
+and lt_subspace_dim_equal = finite_dimensional_vector_space.subspace_dim_equal
+and lt_dim_eq_span = finite_dimensional_vector_space.dim_eq_span
+and lt_dim_psubset = finite_dimensional_vector_space.dim_psubset
+and lt_indep_card_eq_dim_span = finite_dimensional_vector_space.indep_card_eq_dim_span
+and lt_independent_bound_general = finite_dimensional_vector_space.independent_bound_general
+and lt_independent_explicit = finite_dimensional_vector_space.independent_explicit
+and lt_dim_sums_Int = finite_dimensional_vector_space.dim_sums_Int
+and lt_dependent_biggerset_general = finite_dimensional_vector_space.dependent_biggerset_general
+and lt_subset_le_dim = finite_dimensional_vector_space.subset_le_dim
+and lt_linear_inj_imp_surj = finite_dimensional_vector_space.linear_inj_imp_surj
+and lt_linear_surj_imp_inj = finite_dimensional_vector_space.linear_surj_imp_inj
+and lt_linear_inverse_left = finite_dimensional_vector_space.linear_inverse_left
+and lt_left_inverse_linear = finite_dimensional_vector_space.left_inverse_linear
+and lt_right_inverse_linear = finite_dimensional_vector_space.right_inverse_linear
+(* not expected to work:
+ lt_dimension_def = finite_dimensional_vector_space.dimension_def
+and lt_dim_subset_UNIV = finite_dimensional_vector_space.dim_subset_UNIV
+and lt_dim_eq_full = finite_dimensional_vector_space.dim_eq_full
+and lt_inj_linear_imp_inv_linear = finite_dimensional_vector_space.inj_linear_imp_inv_linear
+*)
+
+end
+
+lemmas_with [cancel_type_definition,
+ OF S_ne,
+ folded subset_iff',
+ simplified pred_fun_def,
+ simplified\<comment>\<open>too much?\<close>]:
+ vector_space_assms = lt_vector_space_assms
+and linear_id = lt_linear_id
+and linear_ident = lt_linear_ident
+and linear_scale_self = lt_linear_scale_self
+and linear_scale_left = lt_linear_scale_left
+and linear_uminus = lt_linear_uminus
+and linear_imp_scale["consumes" - 1, "case_names" "1"] = lt_linear_imp_scale
+and scale_eq_0_iff = lt_scale_eq_0_iff
+and scale_left_imp_eq = lt_scale_left_imp_eq
+and scale_right_imp_eq = lt_scale_right_imp_eq
+and scale_cancel_left = lt_scale_cancel_left
+and scale_cancel_right = lt_scale_cancel_right
+and dependent_def = lt_dependent_def
+and dependent_single = lt_dependent_single
+and in_span_insert = lt_in_span_insert
+and dependent_insertD = lt_dependent_insertD
+and independent_insertI = lt_independent_insertI
+and independent_insert = lt_independent_insert
+and maximal_independent_subset_extend["consumes" - 1, "case_names" "1"] = lt_maximal_independent_subset_extend
+and maximal_independent_subset["consumes" - 1, "case_names" "1"] = lt_maximal_independent_subset
+and in_span_delete = lt_in_span_delete
+and span_redundant = lt_span_redundant
+and span_trans = lt_span_trans
+and span_insert_0 = lt_span_insert_0
+and span_delete_0 = lt_span_delete_0
+and span_image_scale = lt_span_image_scale
+and exchange_lemma = lt_exchange_lemma
+and independent_span_bound = lt_independent_span_bound
+and independent_explicit_finite_subsets = lt_independent_explicit_finite_subsets
+and independent_if_scalars_zero = lt_independent_if_scalars_zero
+and subspace_sums = lt_subspace_sums
+
+end
+
+context module_pair_on begin
+
+context includes lifting_syntax
+ assumes
+ "\<exists>(Rep::'s \<Rightarrow> 'b) (Abs::'b \<Rightarrow> 's). type_definition Rep Abs S1"
+ "\<exists>(Rep::'t \<Rightarrow> 'c) (Abs::'c \<Rightarrow> 't). type_definition Rep Abs S2" begin
+
+interpretation local_typedef_module_pair S1 scale1 "TYPE('s)" S2 scale2 "TYPE('t)" by unfold_locales fact+
+
+lemmas_with [var_simplified explicit_ab_group_add,
+ unoverload_type 'e 'b,
+ OF lt2.type.ab_group_add_axioms lt1.type.ab_group_add_axioms type_module_pair_on_with,
+ untransferred,
+ var_simplified implicit_ab_group_add]:
+ lt_module_hom_zero = module_pair.module_hom_zero
+and lt_module_hom_add = module_pair.module_hom_add
+and lt_module_hom_sub = module_pair.module_hom_sub
+and lt_module_hom_neg = module_pair.module_hom_neg
+and lt_module_hom_scale = module_pair.module_hom_scale
+and lt_module_hom_compose_scale = module_pair.module_hom_compose_scale
+and lt_module_hom_sum = module_pair.module_hom_sum
+and lt_module_hom_eq_on_span = module_pair.module_hom_eq_on_span
+(* should work, but doesnt
+and lt_bij_module_hom_imp_inv_module_hom = module_pair.bij_module_hom_imp_inv_module_hom[of scale1 scale2]
+*)
+
+end
+
+lemmas_with [cancel_type_definition, OF m1.S_ne,
+ cancel_type_definition, OF m2.S_ne,
+ folded subset_iff' top_set_def,
+ simplified pred_fun_def,
+ simplified\<comment>\<open>too much?\<close>]:
+ module_hom_zero = lt_module_hom_zero
+and module_hom_add = lt_module_hom_add
+and module_hom_sub = lt_module_hom_sub
+and module_hom_neg = lt_module_hom_neg
+and module_hom_scale = lt_module_hom_scale
+and module_hom_compose_scale = lt_module_hom_compose_scale
+and module_hom_sum = lt_module_hom_sum
+and module_hom_eq_on_span = lt_module_hom_eq_on_span
+
+end
+
+context vector_space_pair_on begin
+
+context includes lifting_syntax
+ notes [transfer_rule del] = Collect_transfer
+ assumes
+ "\<exists>(Rep::'s \<Rightarrow> 'b) (Abs::'b \<Rightarrow> 's). type_definition Rep Abs S1"
+ "\<exists>(Rep::'t \<Rightarrow> 'c) (Abs::'c \<Rightarrow> 't). type_definition Rep Abs S2" begin
+
+interpretation local_typedef_vector_space_pair S1 scale1 "TYPE('s)" S2 scale2 "TYPE('t)" by unfold_locales fact+
+
+lemmas_with [var_simplified explicit_ab_group_add,
+ unoverload_type 'e 'b,
+ OF lt2.type.ab_group_add_axioms lt1.type.ab_group_add_axioms type_vector_space_pair_on_with,
+ untransferred,
+ var_simplified implicit_ab_group_add]:
+ lt_linear_0 = vector_space_pair.linear_0
+and lt_linear_add = vector_space_pair.linear_add
+and lt_linear_scale = vector_space_pair.linear_scale
+and lt_linear_neg = vector_space_pair.linear_neg
+and lt_linear_diff = vector_space_pair.linear_diff
+and lt_linear_sum = vector_space_pair.linear_sum
+and lt_linear_inj_on_iff_eq_0 = vector_space_pair.linear_inj_on_iff_eq_0
+and lt_linear_inj_iff_eq_0 = vector_space_pair.linear_inj_iff_eq_0
+and lt_linear_subspace_image = vector_space_pair.linear_subspace_image
+and lt_linear_subspace_vimage = vector_space_pair.linear_subspace_vimage
+and lt_linear_subspace_kernel = vector_space_pair.linear_subspace_kernel
+and lt_linear_span_image = vector_space_pair.linear_span_image
+and lt_linear_dependent_inj_imageD = vector_space_pair.linear_dependent_inj_imageD
+and lt_linear_eq_0_on_span = vector_space_pair.linear_eq_0_on_span
+and lt_linear_independent_injective_image = vector_space_pair.linear_independent_injective_image
+and lt_linear_inj_on_span_independent_image = vector_space_pair.linear_inj_on_span_independent_image
+and lt_linear_inj_on_span_iff_independent_image = vector_space_pair.linear_inj_on_span_iff_independent_image
+and lt_linear_subspace_linear_preimage = vector_space_pair.linear_subspace_linear_preimage
+and lt_linear_spans_image = vector_space_pair.linear_spans_image
+and lt_linear_spanning_surjective_image = vector_space_pair.linear_spanning_surjective_image
+and lt_linear_eq_on_span = vector_space_pair.linear_eq_on_span
+and lt_linear_compose_scale_right = vector_space_pair.linear_compose_scale_right
+and lt_linear_compose_add = vector_space_pair.linear_compose_add
+and lt_linear_zero = vector_space_pair.linear_zero
+and lt_linear_compose_sub = vector_space_pair.linear_compose_sub
+and lt_linear_compose_neg = vector_space_pair.linear_compose_neg
+and lt_linear_compose_scale = vector_space_pair.linear_compose_scale
+and lt_linear_indep_image_lemma = vector_space_pair.linear_indep_image_lemma
+and lt_linear_eq_on = vector_space_pair.linear_eq_on
+and lt_linear_compose_sum = vector_space_pair.linear_compose_sum
+and lt_linear_independent_extend_subspace = vector_space_pair.linear_independent_extend_subspace
+and lt_linear_independent_extend = vector_space_pair.linear_independent_extend
+and lt_linear_exists_left_inverse_on = vector_space_pair.linear_exists_left_inverse_on
+and lt_linear_exists_right_inverse_on = vector_space_pair.linear_exists_right_inverse_on
+and lt_linear_inj_on_left_inverse = vector_space_pair.linear_inj_on_left_inverse
+and lt_linear_injective_left_inverse = vector_space_pair.linear_injective_left_inverse
+and lt_linear_surj_right_inverse = vector_space_pair.linear_surj_right_inverse
+and lt_linear_surjective_right_inverse = vector_space_pair.linear_surjective_right_inverse
+(* should work, but doesnt
+*)
+(* not expected to work:
+ lt_construct_def = vector_space_pair.construct_def
+ lt_construct_cong = vector_space_pair.construct_cong
+ lt_linear_construct = vector_space_pair.linear_construct
+ lt_construct_basis = vector_space_pair.construct_basis
+ lt_construct_outside = vector_space_pair.construct_outside
+ lt_construct_add = vector_space_pair.construct_add
+ lt_construct_scale = vector_space_pair.construct_scale
+ lt_construct_in_span = vector_space_pair.construct_in_span
+ lt_in_span_in_range_construct = vector_space_pair.in_span_in_range_construct
+ lt_range_construct_eq_span = vector_space_pair.range_construct_eq_span
+*)
+
+end
+
+lemmas_with [cancel_type_definition, OF m1.S_ne,
+ cancel_type_definition, OF m2.S_ne,
+ folded subset_iff' top_set_def,
+ simplified pred_fun_def,
+ simplified\<comment>\<open>too much?\<close>]:
+ linear_0 = lt_linear_0
+ and linear_add = lt_linear_add
+ and linear_scale = lt_linear_scale
+ and linear_neg = lt_linear_neg
+ and linear_diff = lt_linear_diff
+ and linear_sum = lt_linear_sum
+ and linear_inj_on_iff_eq_0 = lt_linear_inj_on_iff_eq_0
+ and linear_inj_iff_eq_0 = lt_linear_inj_iff_eq_0
+ and linear_subspace_image = lt_linear_subspace_image
+ and linear_subspace_vimage = lt_linear_subspace_vimage
+ and linear_subspace_kernel = lt_linear_subspace_kernel
+ and linear_span_image = lt_linear_span_image
+ and linear_dependent_inj_imageD = lt_linear_dependent_inj_imageD
+ and linear_eq_0_on_span = lt_linear_eq_0_on_span
+ and linear_independent_injective_image = lt_linear_independent_injective_image
+ and linear_inj_on_span_independent_image = lt_linear_inj_on_span_independent_image
+ and linear_inj_on_span_iff_independent_image = lt_linear_inj_on_span_iff_independent_image
+ and linear_subspace_linear_preimage = lt_linear_subspace_linear_preimage
+ and linear_spans_image = lt_linear_spans_image
+ and linear_spanning_surjective_image = lt_linear_spanning_surjective_image
+ and linear_eq_on_span = lt_linear_eq_on_span
+ and linear_compose_scale_right = lt_linear_compose_scale_right
+ and linear_compose_add = lt_linear_compose_add
+ and linear_zero = lt_linear_zero
+ and linear_compose_sub = lt_linear_compose_sub
+ and linear_compose_neg = lt_linear_compose_neg
+ and linear_compose_scale = lt_linear_compose_scale
+ and linear_indep_image_lemma = lt_linear_indep_image_lemma
+ and linear_eq_on = lt_linear_eq_on
+ and linear_compose_sum = lt_linear_compose_sum
+ and linear_independent_extend_subspace = lt_linear_independent_extend_subspace
+ and linear_independent_extend = lt_linear_independent_extend
+ and linear_exists_left_inverse_on = lt_linear_exists_left_inverse_on
+ and linear_exists_right_inverse_on = lt_linear_exists_right_inverse_on
+ and linear_inj_on_left_inverse = lt_linear_inj_on_left_inverse
+ and linear_injective_left_inverse = lt_linear_injective_left_inverse
+ and linear_surj_right_inverse = lt_linear_surj_right_inverse
+ and linear_surjective_right_inverse = lt_linear_surjective_right_inverse
+
+end
+
+context finite_dimensional_vector_space_pair_on begin
+
+context includes lifting_syntax
+ notes [transfer_rule del] = Collect_transfer
+ assumes
+ "\<exists>(Rep::'s \<Rightarrow> 'b) (Abs::'b \<Rightarrow> 's). type_definition Rep Abs S1"
+ "\<exists>(Rep::'t \<Rightarrow> 'c) (Abs::'c \<Rightarrow> 't). type_definition Rep Abs S2" begin
+
+interpretation local_typedef_finite_dimensional_vector_space_pair S1 scale1 Basis1 "TYPE('s)" S2 scale2 Basis2 "TYPE('t)" by unfold_locales fact+
+
+lemmas_with [var_simplified explicit_ab_group_add,
+ unoverload_type 'e 'b,
+ OF lt2.type.ab_group_add_axioms lt1.type.ab_group_add_axioms type_finite_dimensional_vector_space_pair_on_with,
+ folded lt1.dim_S_def lt2.dim_S_def,
+ untransferred,
+ var_simplified implicit_ab_group_add]:
+lt_linear_surjective_imp_injective = finite_dimensional_vector_space_pair.linear_surjective_imp_injective
+and lt_linear_injective_imp_surjective = finite_dimensional_vector_space_pair.linear_injective_imp_surjective
+and lt_linear_injective_isomorphism = finite_dimensional_vector_space_pair.linear_injective_isomorphism
+and lt_linear_surjective_isomorphism = finite_dimensional_vector_space_pair.linear_surjective_isomorphism
+and lt_dim_image_eq = finite_dimensional_vector_space_pair.dim_image_eq
+and lt_basis_to_basis_subspace_isomorphism = finite_dimensional_vector_space_pair.basis_to_basis_subspace_isomorphism
+and lt_dim_image_le = finite_dimensional_vector_space_pair.dim_image_le
+and lt_subspace_isomorphism = finite_dimensional_vector_space_pair.subspace_isomorphism
+
+end
+
+lemmas_with [cancel_type_definition, OF vs1.S_ne,
+ cancel_type_definition, OF vs2.S_ne,
+ folded subset_iff' top_set_def,
+ simplified pred_fun_def,
+ simplified\<comment>\<open>too much?\<close>]:
+linear_surjective_imp_injective = lt_linear_surjective_imp_injective
+and linear_injective_imp_surjective = lt_linear_injective_imp_surjective
+and linear_injective_isomorphism = lt_linear_injective_isomorphism
+and linear_surjective_isomorphism = lt_linear_surjective_isomorphism
+and dim_image_eq = lt_dim_image_eq
+and basis_to_basis_subspace_isomorphism = lt_basis_to_basis_subspace_isomorphism
+and dim_image_le = lt_dim_image_le
+and subspace_isomorphism = lt_subspace_isomorphism
+
+end
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy Wed Jun 27 11:16:43 2018 +0200
@@ -0,0 +1,304 @@
+(* Title: HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy
+ Author: Fabian Immler, TU München
+*)
+theory Linear_Algebra_On_With
+ imports
+ Group_On_With
+ Complex_Main
+begin
+
+definition span_with
+ where "span_with pls zero scl b =
+ {sum_with pls zero (\<lambda>a. scl (r a) a) t | t r. finite t \<and> t \<subseteq> b}"
+
+lemma span_with_transfer[transfer_rule]:
+ includes lifting_syntax
+ assumes [transfer_rule]: "right_total A" "bi_unique A"
+ shows "((A ===> A ===> A) ===> A ===> ((=) ===> A ===> A) ===> rel_set A ===> rel_set A)
+ span_with span_with"
+ unfolding span_with_def
+proof (intro rel_funI)
+ fix p p' z z' X X' and s s'::"'c \<Rightarrow> _"
+ assume transfer_rules[transfer_rule]: "(A ===> A ===> A) p p'" "A z z'" "((=) ===> A ===> A) s s'" "rel_set A X X'"
+ have "Domainp A z" using \<open>A z z'\<close> by force
+ have *: "t \<subseteq> X \<Longrightarrow> (\<forall>x\<in>t. Domainp A x)" for t
+ by (meson Domainp.DomainI \<open>rel_set A X X'\<close> rel_setD1 set_mp)
+ 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)]
+ 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
+ proof cases
+ assume ex: "\<exists>C. r ` t \<subseteq> C \<and> comm_monoid_add_on_with C p z"
+ have "Domainp (rel_set A) t" using that by (auto simp: Domainp_set)
+ from ex_comm_monoid_add_around_imageE[OF ex transfer_rules(1,2) this that(1)]
+ obtain C where C: "comm_monoid_add_on_with C p z" "r ` t \<subseteq> C" "Domainp (rel_set A) C" by auto
+ from sum_with_mem[OF C(1,2)] C(3)
+ show ?thesis
+ by auto (meson C(3) Domainp_set)
+ qed (use \<open>A z _\<close> in \<open>auto simp: sum_with_def\<close>)
+ from Domainp_apply2I[OF transfer_rules(3)]
+ have Domainp_sI: "Domainp A x \<Longrightarrow> Domainp A (s y x)" for x y by auto
+ show "rel_set A
+ {sum_with p z (\<lambda>a. s (r a) a) t |t r. finite t \<and> t \<subseteq> X}
+ {sum_with p' z' (\<lambda>a. s' (r a) a) t |t r. finite t \<and> t \<subseteq> X'}"
+ apply (transfer_prover_start, transfer_step+)
+ using *
+ by (auto simp: intro!: DsI Domainp_sI)
+qed
+
+definition dependent_with
+ where "dependent_with pls zero scl s =
+ (\<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)))"
+
+lemma dependent_with_transfer[transfer_rule]:
+ includes lifting_syntax
+ assumes [transfer_rule]: "right_total A" "bi_unique A"
+ shows "((A ===> A ===> A) ===> A ===> ((=) ===> A ===> A) ===> rel_set A ===> (=))
+ dependent_with dependent_with"
+ unfolding dependent_with_def dependent_with_def
+proof (intro rel_funI)
+ fix p p' z z' X X' and s s'::"'c \<Rightarrow> _"
+ assume [transfer_rule]: "(A ===> A ===> A) p p'" "A z z'" "((=) ===> A ===> A) s s'" "rel_set A X X'"
+ have *: "t \<subseteq> X \<Longrightarrow> (\<forall>x\<in>t. Domainp A x)" for t
+ by (meson Domainp.DomainI \<open>rel_set A X X'\<close> rel_setD1 set_mp)
+ 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)) =
+ (\<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))"
+ apply (transfer_prover_start, transfer_step+)
+ using *
+ by (auto simp: intro!: sum_with_mem)
+qed
+
+definition subspace_with
+ 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)"
+
+lemma subspace_with_transfer[transfer_rule]:
+ includes lifting_syntax
+ assumes [transfer_rule]: "bi_unique A"
+ shows "((A ===> A ===> A) ===> A ===> ((=) ===> A ===> A) ===> rel_set A ===> (=))
+ subspace_with subspace_with"
+ unfolding span_with_def subspace_with_def
+ by transfer_prover
+
+definition "module_on_with S pls mns um zero (scl::'a::comm_ring_1\<Rightarrow>_) \<longleftrightarrow>
+ ab_group_add_on_with S pls zero mns um \<and>
+ ((\<forall>a. \<forall>x\<in>S.
+ \<forall>y\<in>S. scl a (pls x y) = pls (scl a x) (scl a y)) \<and>
+ (\<forall>a b. \<forall>x\<in>S. scl (a + b) x = pls (scl a x) (scl b x))) \<and>
+ (\<forall>a b. \<forall>x\<in>S. scl a (scl b x) = scl (a * b) x) \<and>
+ (\<forall>x\<in>S. scl 1 x = x) \<and>
+ (\<forall>a. \<forall>x\<in>S. scl a x \<in> S)"
+
+definition "vector_space_on_with S pls mns um zero (scl::'a::field\<Rightarrow>_) \<longleftrightarrow>
+ module_on_with S pls mns um zero scl"
+
+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>
+ module_on_with S pls mns um zero scl \<and> module_on_with S' pls' mns' um' zero' scl'"
+
+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>
+ module_pair_on_with S S' pls mns um zero scl pls' mns' um' zero' scl'"
+
+definition "module_hom_on_with S1 S2 plus1 minus1 uminus1 zero1 (scale1::'a::comm_ring_1\<Rightarrow>_)
+ plus2 minus2 uminus2 zero2 (scale2::'a::comm_ring_1\<Rightarrow>_) f \<longleftrightarrow>
+ module_pair_on_with S1 S2 plus1 minus1 uminus1 zero1 scale1
+ plus2 minus2 uminus2 zero2 scale2 \<and>
+ (\<forall>x\<in>S1. \<forall>y\<in>S1. f (plus1 x y) = plus2 (f x) (f y)) \<and>
+ (\<forall>s. \<forall>x\<in>S1. f (scale1 s x) = scale2 s (f x))"
+
+definition "linear_on_with S1 S2 plus1 minus1 uminus1 zero1 (scale1::'a::field\<Rightarrow>_)
+ plus2 minus2 uminus2 zero2 (scale2::'a::field\<Rightarrow>_) f \<longleftrightarrow>
+ module_hom_on_with S1 S2 plus1 minus1 uminus1 zero1 scale1
+ plus2 minus2 uminus2 zero2 scale2 f"
+
+definition dim_on_with
+ where "dim_on_with S pls zero scale V =
+ (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
+ 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)
+ else 0)"
+
+definition "finite_dimensional_vector_space_on_with S pls mns um zero (scl::'a::field\<Rightarrow>_) basis \<longleftrightarrow>
+ vector_space_on_with S pls mns um zero scl \<and>
+ finite basis \<and>
+ \<not> dependent_with pls zero scl basis \<and>
+ span_with pls zero scl basis = S"
+
+definition "finite_dimensional_vector_space_pair_on_with S S' pls mns um zero (scl::'a::field\<Rightarrow>_) b
+ pls' mns' um' zero' (scl'::'a::field\<Rightarrow>_) b' \<longleftrightarrow>
+ finite_dimensional_vector_space_on_with S pls mns um zero (scl::'a::field\<Rightarrow>_) b \<and>
+ finite_dimensional_vector_space_on_with S' pls' mns' um' zero' (scl'::'a::field\<Rightarrow>_) b'"
+
+context module begin
+
+lemma span_with:
+ "span = (\<lambda>X. span_with (+) 0 scale X)"
+ unfolding span_explicit span_with_def sum_with ..
+
+lemma dependent_with:
+ "dependent = (\<lambda>X. dependent_with (+) 0 scale X)"
+ unfolding dependent_explicit dependent_with_def sum_with ..
+
+lemma subspace_with:
+ "subspace = (\<lambda>X. subspace_with (+) 0 scale X)"
+ unfolding subspace_def subspace_with_def ..
+
+end
+
+lemmas [explicit_ab_group_add] = module.span_with module.dependent_with module.subspace_with
+
+lemma module_on_with_transfer[transfer_rule]:
+ includes lifting_syntax
+ assumes [transfer_rule]: "right_total A" "bi_unique A"
+ shows
+ "(rel_set A ===> (A ===> A ===> A) ===> (A ===> A ===> A) ===> (A ===> A) ===> A ===> ((=) ===> A ===> A) ===> (=))
+ module_on_with module_on_with"
+ unfolding module_on_with_def
+ by transfer_prover
+
+lemma vector_space_on_with_transfer[transfer_rule]:
+ includes lifting_syntax
+ assumes [transfer_rule]: "right_total A" "bi_unique A"
+ shows
+ "(rel_set A ===> (A ===> A ===> A) ===> (A ===> A ===> A) ===> (A ===> A) ===> A ===> ((=) ===> A ===> A) ===> (=))
+ vector_space_on_with vector_space_on_with"
+ unfolding vector_space_on_with_def
+ by transfer_prover
+
+context vector_space begin
+
+lemma dim_with: "dim = (\<lambda>X. dim_on_with UNIV (+) 0 scale X)"
+ unfolding dim_def dim_on_with_def dependent_with span_with by force
+
+end
+
+lemmas [explicit_ab_group_add] = vector_space.dim_with
+
+lemma module_pair_on_with_transfer[transfer_rule]:
+ includes lifting_syntax
+ assumes [transfer_rule]: "right_total A" "bi_unique A" "right_total C" "bi_unique C"
+ shows
+ "(rel_set A ===> rel_set C ===>
+ (A ===> A ===> A) ===> (A ===> A ===> A) ===> (A ===> A) ===> A ===> ((=) ===> A ===> A) ===>
+ (C ===> C ===> C) ===> (C ===> C ===> C) ===> (C ===> C) ===> C ===> ((=) ===> C ===> C) ===>
+ (=)) module_pair_on_with module_pair_on_with"
+ unfolding module_pair_on_with_def
+ by transfer_prover
+
+lemma module_hom_on_with_transfer[transfer_rule]:
+ includes lifting_syntax
+ assumes [transfer_rule]: "right_total A" "bi_unique A" "right_total C" "bi_unique C"
+ shows
+ "(rel_set A ===> rel_set C ===>
+ (A ===> A ===> A) ===> (A ===> A ===> A) ===> (A ===> A) ===> A ===> ((=) ===> A ===> A) ===>
+ (C ===> C ===> C) ===> (C ===> C ===> C) ===> (C ===> C) ===> C ===> ((=) ===> C ===> C) ===>
+ (A ===> C) ===> (=)) module_hom_on_with module_hom_on_with"
+ unfolding module_hom_on_with_def
+ by transfer_prover
+
+lemma linear_on_with_transfer[transfer_rule]:
+ includes lifting_syntax
+ assumes [transfer_rule]: "right_total A" "bi_unique A" "right_total C" "bi_unique C"
+ shows
+ "(rel_set A ===> rel_set C ===>
+ (A ===> A ===> A) ===> (A ===> A ===> A) ===> (A ===> A) ===> A ===> ((=) ===> A ===> A) ===>
+ (C ===> C ===> C) ===> (C ===> C ===> C) ===> (C ===> C) ===> C ===> ((=) ===> C ===> C) ===>
+ (A ===> C) ===> (=)) linear_on_with linear_on_with"
+ unfolding linear_on_with_def
+ by transfer_prover
+
+subsubsection \<open>Explicit locale formulations\<close>
+
+lemma module_on_with[explicit_ab_group_add]: "module s \<longleftrightarrow> module_on_with UNIV (+) (-) uminus 0 s"
+ and vector_space_on_with[explicit_ab_group_add]: "vector_space t \<longleftrightarrow> vector_space_on_with UNIV (+) (-) uminus 0 t"
+ by (auto simp: module_def module_on_with_def ab_group_add_axioms
+ vector_space_def vector_space_on_with_def)
+
+lemma vector_space_with_imp_module_with[explicit_ab_group_add]:
+ "vector_space_on_with S (+) (-) uminus 0 s \<Longrightarrow> module_on_with S (+) (-) uminus 0 s"
+ by (simp add: vector_space_on_with_def)
+
+lemma finite_dimensional_vector_space_on_with[explicit_ab_group_add]:
+ "finite_dimensional_vector_space t b \<longleftrightarrow> finite_dimensional_vector_space_on_with UNIV (+) (-) uminus 0 t b"
+ by (auto simp: finite_dimensional_vector_space_on_with_def finite_dimensional_vector_space_def
+ finite_dimensional_vector_space_axioms_def explicit_ab_group_add)
+
+lemma vector_space_with_imp_finite_dimensional_vector_space_with[explicit_ab_group_add]:
+ "finite_dimensional_vector_space_on_with S (+) (-) uminus 0 s basis \<Longrightarrow>
+ vector_space_on_with S (+) (-) uminus 0 s"
+ by (auto simp: finite_dimensional_vector_space_on_with_def)
+
+lemma module_hom_on_with[explicit_ab_group_add]:
+ "module_hom s1 s2 f \<longleftrightarrow> module_hom_on_with UNIV UNIV (+) (-) uminus 0 s1 (+) (-) uminus 0 s2 f"
+ and linear_with[explicit_ab_group_add]:
+ "Vector_Spaces.linear t1 t2 f \<longleftrightarrow> linear_on_with UNIV UNIV (+) (-) uminus 0 t1 (+) (-) uminus 0 t2 f"
+ and module_pair_on_with[explicit_ab_group_add]:
+ "module_pair s1 s2 \<longleftrightarrow> module_pair_on_with UNIV UNIV (+) (-) uminus 0 s1 (+) (-) uminus 0 s2"
+ by (auto simp: module_hom_def module_hom_on_with_def module_pair_on_with_def
+ Vector_Spaces.linear_def linear_on_with_def vector_space_on_with
+ module_on_with_def vector_space_on_with_def
+ module_hom_axioms_def module_pair_def module_on_with)
+
+lemma vector_space_pair_with[explicit_ab_group_add]:
+ "vector_space_pair s1 s2 \<longleftrightarrow> vector_space_pair_on_with UNIV UNIV (+) (-) uminus 0 s1 (+) (-) uminus 0 s2"
+ by (auto simp: module_pair_on_with_def explicit_ab_group_add
+ vector_space_pair_on_with_def vector_space_pair_def module_on_with_def vector_space_on_with_def)
+
+lemma finite_dimensional_vector_space_pair_with[explicit_ab_group_add]:
+ "finite_dimensional_vector_space_pair s1 b1 s2 b2 \<longleftrightarrow>
+ finite_dimensional_vector_space_pair_on_with UNIV UNIV (+) (-) uminus 0 s1 b1 (+) (-) uminus 0 s2 b2"
+ by (auto simp: finite_dimensional_vector_space_pair_def
+ finite_dimensional_vector_space_pair_on_with_def finite_dimensional_vector_space_on_with)
+
+
+lemma module_pair_with_imp_module_with[explicit_ab_group_add]:
+ "module_on_with S (+) (-) uminus 0 s"
+ "module_on_with T (+) (-) uminus 0 t"
+ if "module_pair_on_with S T (+) (-) uminus 0 s (+) (-) uminus 0 t"
+ using that
+ unfolding module_pair_on_with_def
+ by simp_all
+
+lemma vector_space_pair_with_imp_vector_space_with[explicit_ab_group_add]:
+ "vector_space_on_with S (+) (-) uminus 0 s"
+ "vector_space_on_with T (+) (-) uminus 0 t"
+ if "vector_space_pair_on_with S T(+) (-) uminus 0 s (+) (-) uminus 0 t"
+ using that
+ by (auto simp: vector_space_pair_on_with_def module_pair_on_with_def vector_space_on_with_def)
+
+lemma finite_dimensional_vector_space_pair_with_imp_finite_dimensional_vector_space_with[explicit_ab_group_add]:
+ "finite_dimensional_vector_space_on_with S (+) (-) uminus 0 s b"
+ "finite_dimensional_vector_space_on_with T (+) (-) uminus 0 t c"
+ if "finite_dimensional_vector_space_pair_on_with S T (+) (-) uminus 0 s b (+) (-) uminus 0 t c"
+ using that
+ unfolding finite_dimensional_vector_space_pair_on_with_def
+ by simp_all
+
+lemma finite_dimensional_vector_space_pair_with_imp_vector_space_with[explicit_ab_group_add]:
+ \<comment>\<open>this rule is strange: why is it needed, but not the one with \<open>module_with\<close> as conclusions?\<close>
+ "vector_space_on_with S (+) (-) uminus 0 s"
+ "vector_space_on_with T (+) (-) uminus 0 t"
+ if "finite_dimensional_vector_space_pair_on_with S T (+) (-) uminus 0 s b (+) (-) uminus 0 t c"
+ using that
+ by (auto simp: finite_dimensional_vector_space_pair_on_with_def finite_dimensional_vector_space_on_with_def)
+
+lemma finite_dimensional_vector_space_on_with_transfer[transfer_rule]:
+ includes lifting_syntax
+ assumes [transfer_rule]: "right_total A" "bi_unique A"
+ shows
+ "(rel_set A ===>
+ (A ===> A ===> A) ===> (A ===> A ===> A) ===> (A ===> A) ===> A ===> ((=) ===> A ===> A) ===>
+ rel_set A ===>
+ (=)) (finite_dimensional_vector_space_on_with) finite_dimensional_vector_space_on_with"
+ unfolding finite_dimensional_vector_space_on_with_def
+ by transfer_prover
+
+lemma finite_dimensional_vector_space_pair_on_with_transfer[transfer_rule]:
+ includes lifting_syntax
+ assumes [transfer_rule]: "right_total A" "bi_unique A" "right_total C" "bi_unique C"
+ shows
+ "(rel_set A ===> rel_set C ===>
+ (A ===> A ===> A) ===> (A ===> A ===> A) ===> (A ===> A) ===> A ===> ((=) ===> A ===> A) ===>
+ rel_set A ===>
+ (C ===> C ===> C) ===> (C ===> C ===> C) ===> (C ===> C) ===> C ===> ((=) ===> C ===> C) ===>
+ rel_set C ===>
+ (=)) (finite_dimensional_vector_space_pair_on_with) finite_dimensional_vector_space_pair_on_with"
+ unfolding finite_dimensional_vector_space_pair_on_with_def
+ by transfer_prover
+
+end
\ No newline at end of file