example for Types_To_Sets: transfer from type-based linear algebra to subspaces
authorimmler
Wed Jun 27 11:16:43 2018 +0200 (11 months ago)
changeset 68522d9cbc1e8644d
parent 68521 1bad08165162
child 68523 ccacc84e0251
example for Types_To_Sets: transfer from type-based linear algebra to subspaces
CONTRIBUTORS
NEWS
src/HOL/ROOT
src/HOL/Types_To_Sets/Examples/Group_On_With.thy
src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy
src/HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy
     1.1 --- a/CONTRIBUTORS	Wed Jun 27 10:18:03 2018 +0200
     1.2 +++ b/CONTRIBUTORS	Wed Jun 27 11:16:43 2018 +0200
     1.3 @@ -6,6 +6,9 @@
     1.4  Contributions to Isabelle2018
     1.5  -----------------------------
     1.6  
     1.7 +* June 2018: Fabian Immler
     1.8 +  More tool support for HOL-Types_To_Sets.
     1.9 +
    1.10  * June 2018: Martin Baillon and Paulo Emílio de Vilhena
    1.11    A variety of contributions to HOL-Algebra.
    1.12  
     2.1 --- a/NEWS	Wed Jun 27 10:18:03 2018 +0200
     2.2 +++ b/NEWS	Wed Jun 27 11:16:43 2018 +0200
     2.3 @@ -394,6 +394,11 @@
     2.4  Riemann mapping theorem, the Vitali covering theorem,
     2.5  change-of-variables results for integration and measures.
     2.6  
     2.7 +* Session HOL-Types_To_Sets: more tool support
     2.8 +(unoverload_type combines internalize_sorts and unoverload) and larger
     2.9 +experimental application (type based linear algebra transferred to linear
    2.10 +algebra on subspaces).
    2.11 +
    2.12  
    2.13  *** ML ***
    2.14  
     3.1 --- a/src/HOL/ROOT	Wed Jun 27 10:18:03 2018 +0200
     3.2 +++ b/src/HOL/ROOT	Wed Jun 27 11:16:43 2018 +0200
     3.3 @@ -932,6 +932,7 @@
     3.4      "Examples/Prerequisites"
     3.5      "Examples/Finite"
     3.6      "Examples/T2_Spaces"
     3.7 +    "Examples/Linear_Algebra_On"
     3.8  
     3.9  session HOLCF (main timing) in HOLCF = HOL +
    3.10    description {*
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Types_To_Sets/Examples/Group_On_With.thy	Wed Jun 27 11:16:43 2018 +0200
     4.3 @@ -0,0 +1,338 @@
     4.4 +(*  Title:      HOL/Types_To_Sets/Examples/Group_On_With.thy
     4.5 +    Author:     Fabian Immler, TU München
     4.6 +*)
     4.7 +theory Group_On_With
     4.8 +imports
     4.9 +  Main
    4.10 +begin
    4.11 +
    4.12 +subsection \<open>\<^emph>\<open>on\<close> carrier set \<^emph>\<open>with\<close> explicit group operations\<close>
    4.13 +
    4.14 +definition "semigroup_add_on_with S pls \<longleftrightarrow>
    4.15 +  (\<forall>a\<in>S. \<forall>b\<in>S. \<forall>c\<in>S. pls (pls a b) c = pls a (pls b c)) \<and>
    4.16 +  (\<forall>a\<in>S. \<forall>b\<in>S. pls a b \<in> S)"
    4.17 +
    4.18 +lemma semigroup_add_on_with_transfer[transfer_rule]:
    4.19 +  includes lifting_syntax
    4.20 +  assumes [transfer_rule]: "bi_unique A"
    4.21 +  shows "(rel_set A ===> (A ===> A ===> A) ===> (=)) semigroup_add_on_with semigroup_add_on_with"
    4.22 +  unfolding semigroup_add_on_with_def
    4.23 +  by transfer_prover
    4.24 +
    4.25 +
    4.26 +lemma semigroup_add_on_with[simp]: "semigroup_add_on_with (UNIV::'a::semigroup_add set) (+)"
    4.27 +  by (auto simp: semigroup_add_on_with_def ac_simps)
    4.28 +
    4.29 +lemma Domainp_applyI:
    4.30 +  includes lifting_syntax
    4.31 +  shows "(A ===> B) f g \<Longrightarrow> A x y \<Longrightarrow> Domainp B (f x)"
    4.32 +  by (auto simp: rel_fun_def)
    4.33 +
    4.34 +lemma Domainp_apply2I:
    4.35 +  includes lifting_syntax
    4.36 +  shows "(A ===> B ===> C) f g \<Longrightarrow> A x y \<Longrightarrow> B x' y' \<Longrightarrow> Domainp C (f x x')"
    4.37 +  by (force simp: rel_fun_def)
    4.38 +
    4.39 +lemma right_total_semigroup_add_transfer[transfer_rule]:
    4.40 +  includes lifting_syntax
    4.41 +  assumes [transfer_rule]: "right_total A" "bi_unique A"
    4.42 +  shows "((A ===> A ===> A) ===> (=)) (semigroup_add_on_with (Collect (Domainp A))) class.semigroup_add"
    4.43 +proof (intro rel_funI)
    4.44 +  fix x y assume xy[transfer_rule]: "(A ===> A ===> A) x y"
    4.45 +  show "semigroup_add_on_with (Collect (Domainp A)) x = class.semigroup_add y"
    4.46 +    unfolding semigroup_add_on_with_def class.semigroup_add_def
    4.47 +    by transfer (auto intro!: Domainp_apply2I[OF xy])
    4.48 +qed
    4.49 +
    4.50 +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)"
    4.51 +
    4.52 +lemma ab_semigroup_add_on_with_transfer[transfer_rule]:
    4.53 +  includes lifting_syntax
    4.54 +  assumes [transfer_rule]: "bi_unique A"
    4.55 +  shows
    4.56 +    "(rel_set A ===> (A ===> A ===> A) ===> (=)) ab_semigroup_add_on_with ab_semigroup_add_on_with"
    4.57 +  unfolding ab_semigroup_add_on_with_def by transfer_prover
    4.58 +
    4.59 +lemma right_total_ab_semigroup_add_transfer[transfer_rule]:
    4.60 +  includes lifting_syntax
    4.61 +  assumes [transfer_rule]: "right_total A" "bi_unique A"
    4.62 +  shows
    4.63 +    "((A ===> A ===> A) ===> (=)) (ab_semigroup_add_on_with (Collect (Domainp A))) class.ab_semigroup_add"
    4.64 +  unfolding class.ab_semigroup_add_def class.ab_semigroup_add_axioms_def ab_semigroup_add_on_with_def
    4.65 +  by transfer_prover
    4.66 +
    4.67 +lemma ab_semigroup_add_on_with[simp]: "ab_semigroup_add_on_with (UNIV::'a::ab_semigroup_add set) (+)"
    4.68 +  by (auto simp: ab_semigroup_add_on_with_def ac_simps)
    4.69 +
    4.70 +
    4.71 +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"
    4.72 +
    4.73 +lemma comm_monoid_add_on_with_transfer[transfer_rule]:
    4.74 +  includes lifting_syntax
    4.75 +  assumes [transfer_rule]: "bi_unique A"
    4.76 +  shows
    4.77 +    "(rel_set A ===> (A ===> A ===> A) ===> A ===> (=)) comm_monoid_add_on_with comm_monoid_add_on_with"
    4.78 +  unfolding comm_monoid_add_on_with_def
    4.79 +  by transfer_prover
    4.80 +
    4.81 +lemma right_total_comm_monoid_add_transfer[transfer_rule]:
    4.82 +  includes lifting_syntax
    4.83 +  assumes [transfer_rule]: "right_total A" "bi_unique A"
    4.84 +  shows
    4.85 +    "((A ===> A ===> A) ===> A ===> (=))
    4.86 +      (comm_monoid_add_on_with (Collect (Domainp A))) class.comm_monoid_add"
    4.87 +proof (intro rel_funI)
    4.88 +  fix p p' z z'
    4.89 +  assume [transfer_rule]: "(A ===> A ===> A) p p'" "A z z'"
    4.90 +  show "comm_monoid_add_on_with (Collect (Domainp A)) p z = class.comm_monoid_add p' z'"
    4.91 +    unfolding class.comm_monoid_add_def class.comm_monoid_add_axioms_def comm_monoid_add_on_with_def
    4.92 +    apply transfer
    4.93 +    using \<open>A z z'\<close>
    4.94 +    by auto
    4.95 +qed
    4.96 +
    4.97 +lemma comm_monoid_add_on_with[simp]: "comm_monoid_add_on_with UNIV (+) (0::'a::comm_monoid_add)"
    4.98 +  by (auto simp: comm_monoid_add_on_with_def ab_semigroup_add_on_with_def
    4.99 +      semigroup_add_on_with_def ac_simps)
   4.100 +
   4.101 +definition "ab_group_add_on_with S pls z mns um \<longleftrightarrow> comm_monoid_add_on_with S pls z \<and>
   4.102 +  (\<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))"
   4.103 +
   4.104 +lemma ab_group_add_transfer[transfer_rule]:
   4.105 +  includes lifting_syntax
   4.106 +  assumes [transfer_rule]: "right_total A" "bi_unique A"
   4.107 +  shows
   4.108 +    "((A ===> A ===> A) ===> A  ===> (A ===> A ===> A) ===> (A ===> A)===> (=))
   4.109 +      (ab_group_add_on_with (Collect (Domainp A))) class.ab_group_add"
   4.110 +  unfolding class.ab_group_add_def class.ab_group_add_axioms_def ab_group_add_on_with_def
   4.111 +  by transfer_prover
   4.112 +
   4.113 +lemma ab_group_add_on_with_transfer[transfer_rule]:
   4.114 +  includes lifting_syntax
   4.115 +  assumes [transfer_rule]: "right_total A" "bi_unique A"
   4.116 +  shows
   4.117 +    "(rel_set A ===> (A ===> A ===> A) ===> A  ===> (A ===> A ===> A) ===> (A ===> A)===> (=))
   4.118 +      ab_group_add_on_with ab_group_add_on_with"
   4.119 +  unfolding class.ab_group_add_def class.ab_group_add_axioms_def ab_group_add_on_with_def
   4.120 +  by transfer_prover
   4.121 +
   4.122 +lemma ab_group_add_on_with[simp]: "ab_group_add_on_with (UNIV::'a::ab_group_add set) (+) 0 (-) uminus"
   4.123 +  by (auto simp: ab_group_add_on_with_def)
   4.124 +
   4.125 +definition "sum_with pls z f S =
   4.126 +  (if \<exists>C. f ` S \<subseteq> C \<and> comm_monoid_add_on_with C pls z then
   4.127 +    Finite_Set.fold (pls o f) z S else z)"
   4.128 +
   4.129 +lemma sum_with_empty[simp]: "sum_with pls z f {} = z"
   4.130 +  by (auto simp: sum_with_def)
   4.131 +
   4.132 +lemma sum_with: "sum = sum_with (+) 0"
   4.133 +proof (intro ext)
   4.134 +  fix f::"'a\<Rightarrow>'b" and X::"'a set"
   4.135 +  have ex: "\<exists>C. f ` X \<subseteq> C \<and> comm_monoid_add_on_with C (+) 0"
   4.136 +    by (auto intro!: exI[where x=UNIV] comm_monoid_add_on_with)
   4.137 +  then show "sum f X = sum_with (+) 0 f X"
   4.138 +    unfolding sum.eq_fold sum_with_def
   4.139 +    by simp
   4.140 +qed
   4.141 +
   4.142 +context fixes C pls z assumes comm_monoid_add_on_with: "comm_monoid_add_on_with C pls z" begin
   4.143 +
   4.144 +lemmas comm_monoid_add_unfolded =
   4.145 +    comm_monoid_add_on_with[unfolded
   4.146 +      comm_monoid_add_on_with_def ab_semigroup_add_on_with_def semigroup_add_on_with_def]
   4.147 +
   4.148 +private abbreviation "pls' \<equiv> \<lambda>x y. pls (if x \<in> C then x else z) (if y \<in> C then y else z)"
   4.149 +
   4.150 +lemma fold_pls'_mem: "Finite_Set.fold (pls' \<circ> g) z A \<in> C"
   4.151 +  if "g ` A \<subseteq> C"
   4.152 +proof cases
   4.153 +  assume A: "finite A"
   4.154 +  interpret comp_fun_commute "pls' o g"
   4.155 +    using comm_monoid_add_unfolded that
   4.156 +    by unfold_locales auto
   4.157 +  from fold_graph_fold[OF A] have "fold_graph (pls' \<circ> g) z A (Finite_Set.fold (pls' \<circ> g) z A)" .
   4.158 +  from fold_graph_closed_lemma[OF this, of C "pls' \<circ> g"] comm_monoid_add_unfolded
   4.159 +  show ?thesis
   4.160 +    by auto
   4.161 +qed (use comm_monoid_add_unfolded in simp)
   4.162 +
   4.163 +lemma fold_pls'_eq: "Finite_Set.fold (pls' \<circ> g) z A = Finite_Set.fold (pls \<circ> g) z A"
   4.164 +  if "g ` A \<subseteq> C"
   4.165 +  using comm_monoid_add_unfolded that
   4.166 +  by (intro fold_closed_eq[where B=C]) auto
   4.167 +
   4.168 +lemma sum_with_mem: "sum_with pls z g A \<in> C" if "g ` A \<subseteq> C"
   4.169 +proof -
   4.170 +  interpret comp_fun_commute "pls' o g"
   4.171 +    using comm_monoid_add_unfolded that
   4.172 +    by unfold_locales auto
   4.173 +  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
   4.174 +  then show ?thesis
   4.175 +    using fold_pls'_mem[OF that]
   4.176 +    by (simp add: sum_with_def fold_pls'_eq that)
   4.177 +qed
   4.178 +
   4.179 +lemma sum_with_insert:
   4.180 +  "sum_with pls z g (insert x A) = pls (g x) (sum_with pls z g A)"
   4.181 +  if g_into: "g x \<in> C" "g ` A \<subseteq> C"
   4.182 +    and A: "finite A" and x: "x \<notin> A"
   4.183 +proof -
   4.184 +  interpret comp_fun_commute "pls' o g"
   4.185 +    using comm_monoid_add_unfolded g_into
   4.186 +    by unfold_locales auto
   4.187 +  have "Finite_Set.fold (pls \<circ> g) z (insert x A) = Finite_Set.fold (pls' \<circ> g) z (insert x A)"
   4.188 +    using g_into
   4.189 +    by (subst fold_pls'_eq) auto
   4.190 +  also have "\<dots> = pls' (g x) (Finite_Set.fold (pls' \<circ> g) z A)"
   4.191 +    unfolding fold_insert[OF A x]
   4.192 +    by (auto simp: o_def)
   4.193 +  also have "\<dots> = pls (g x) (Finite_Set.fold (pls' \<circ> g) z A)"
   4.194 +  proof -
   4.195 +    from fold_graph_fold[OF A] have "fold_graph (pls' \<circ> g) z A (Finite_Set.fold (pls' \<circ> g) z A)" .
   4.196 +    from fold_graph_closed_lemma[OF this, of C "pls' \<circ> g"] comm_monoid_add_unfolded
   4.197 +    have "Finite_Set.fold (pls' \<circ> g) z A \<in> C"
   4.198 +      by auto
   4.199 +    then show ?thesis
   4.200 +      using g_into by auto
   4.201 +  qed
   4.202 +  also have "Finite_Set.fold (pls' \<circ> g) z A = Finite_Set.fold (pls \<circ> g) z A"
   4.203 +    using g_into
   4.204 +    by (subst fold_pls'_eq) auto
   4.205 +  finally
   4.206 +  have "Finite_Set.fold (pls \<circ> g) z (insert x A) = pls (g x) (Finite_Set.fold (pls \<circ> g) z A)" .
   4.207 +  moreover
   4.208 +  have "\<exists>C. g ` insert x A \<subseteq> C \<and> comm_monoid_add_on_with C pls z"
   4.209 +    "\<exists>C. g ` A \<subseteq> C \<and> comm_monoid_add_on_with C pls z"
   4.210 +    using that (1,2) comm_monoid_add_on_with by auto
   4.211 +  ultimately show ?thesis
   4.212 +    by (simp add: sum_with_def)
   4.213 +qed
   4.214 +
   4.215 +end
   4.216 +
   4.217 +lemma ex_comm_monoid_add_around_imageE:
   4.218 +  includes lifting_syntax
   4.219 +  assumes ex_comm: "\<exists>C. f ` S \<subseteq> C \<and> comm_monoid_add_on_with C pls zero"
   4.220 +  assumes transfers: "(A ===> A ===> A) pls pls'" "A zero zero'" "Domainp (rel_set B) S"
   4.221 +    and in_dom: "\<And>x. x \<in> S \<Longrightarrow> Domainp A (f x)"
   4.222 +  obtains C where "comm_monoid_add_on_with C pls zero" "f ` S \<subseteq> C" "Domainp (rel_set A) C"
   4.223 +proof -
   4.224 +  from ex_comm obtain C0 where C0: "f ` S \<subseteq> C0" and comm: "comm_monoid_add_on_with C0 pls zero"
   4.225 +    by auto
   4.226 +  define C where "C = C0 \<inter> Collect (Domainp A)"
   4.227 +  have "comm_monoid_add_on_with C pls zero"
   4.228 +    using comm Domainp_apply2I[OF \<open>(A ===> A ===> A) pls pls'\<close>] \<open>A zero zero'\<close>
   4.229 +    by (auto simp: comm_monoid_add_on_with_def ab_semigroup_add_on_with_def
   4.230 +        semigroup_add_on_with_def C_def)
   4.231 +  moreover have "f ` S \<subseteq> C" using C0
   4.232 +    by (auto simp: C_def in_dom)
   4.233 +  moreover have "Domainp (rel_set A) C" by (auto simp: C_def Domainp_set)
   4.234 +  ultimately show ?thesis ..
   4.235 +qed
   4.236 +
   4.237 +lemma sum_with_transfer[transfer_rule]:
   4.238 +  includes lifting_syntax
   4.239 +  assumes [transfer_rule]: "right_total A" "bi_unique A" "bi_unique B"
   4.240 +  shows "((A ===> A ===> A) ===> A ===> (B ===> A) ===> rel_set B ===> A)
   4.241 +    sum_with sum_with"
   4.242 +proof (safe intro!: rel_funI)
   4.243 +  fix pls pls' zero zero' f g S T
   4.244 +  assume transfer_pls[transfer_rule]: "(A ===> A ===> A) pls pls'"
   4.245 +    and transfer_zero[transfer_rule]: "A zero zero'"
   4.246 +  assume transfer_g[transfer_rule]: "(B ===> A) f g"
   4.247 +    and transfer_T[transfer_rule]: "rel_set B S T"
   4.248 +  show "A (sum_with pls zero f S) (sum_with pls' zero' g T)"
   4.249 +  proof cases
   4.250 +    assume ex_comm: "\<exists>C. f ` S \<subseteq> C \<and> comm_monoid_add_on_with C pls zero"
   4.251 +    have Domains: "Domainp (rel_set B) S" "(\<And>x. x \<in> S \<Longrightarrow> Domainp A (f x))"
   4.252 +      using transfer_T transfer_g
   4.253 +      by auto (meson Domainp_applyI rel_set_def)
   4.254 +    from ex_comm_monoid_add_around_imageE[OF ex_comm transfer_pls transfer_zero Domains]
   4.255 +    obtain C where comm: "comm_monoid_add_on_with C pls zero"
   4.256 +      and C: "f ` S \<subseteq> C"
   4.257 +      and "Domainp (rel_set A) C"
   4.258 +      by auto
   4.259 +    then obtain C' where [transfer_rule]: "rel_set A C C'" by auto
   4.260 +    have C': "g ` T \<subseteq> C'"
   4.261 +      by transfer (rule C)
   4.262 +    have comm': "comm_monoid_add_on_with C' pls' zero'"
   4.263 +      by transfer (rule comm)
   4.264 +    from C' comm' have ex_comm': "\<exists>C. g ` T \<subseteq> C \<and> comm_monoid_add_on_with C pls' zero'" by auto
   4.265 +    show ?thesis
   4.266 +      using transfer_T C C'
   4.267 +    proof (induction S arbitrary: T rule: infinite_finite_induct)
   4.268 +      case (infinite S)
   4.269 +      note [transfer_rule] = infinite.prems
   4.270 +      from infinite.hyps have "infinite T" by transfer
   4.271 +      then show ?case by (simp add: sum_with_def infinite.hyps \<open>A zero zero'\<close>)
   4.272 +    next
   4.273 +      case [transfer_rule]: empty
   4.274 +      have "T = {}" by transfer rule
   4.275 +      then show ?case by (simp add: sum_with_def \<open>A zero zero'\<close>)
   4.276 +    next
   4.277 +      case (insert x F)
   4.278 +      note [transfer_rule] = insert.prems(1)
   4.279 +      have [simp]: "finite T"
   4.280 +        by transfer (simp add: insert.hyps)
   4.281 +      obtain y where [transfer_rule]: "B x y" and y: "y \<in> T"
   4.282 +        by (meson insert.prems insertI1 rel_setD1)
   4.283 +      define T' where "T' = T - {y}"
   4.284 +      have T_def: "T = insert y T'"
   4.285 +        by (auto simp: T'_def y)
   4.286 +      define sF where "sF = sum_with pls zero f F"
   4.287 +      define sT where "sT = sum_with pls' zero' g T'"
   4.288 +      have [simp]: "y \<notin> T'" "finite T'"
   4.289 +        by (auto simp: y T'_def)
   4.290 +      have "rel_set B (insert x F - {x}) T'"
   4.291 +        unfolding T'_def
   4.292 +        by transfer_prover
   4.293 +      then have transfer_T'[transfer_rule]: "rel_set B F T'"
   4.294 +        using insert.hyps
   4.295 +        by simp
   4.296 +      from insert.prems have "f ` F \<subseteq> C" "g ` T' \<subseteq> C'"
   4.297 +        by (auto simp: T'_def)
   4.298 +      from insert.IH[OF transfer_T' this] have [transfer_rule]: "A sF sT" by (auto simp: sF_def sT_def o_def)
   4.299 +      have rew: "(sum_with pls zero f (insert x F)) = pls (f x) (sum_with pls zero f F)"
   4.300 +        apply (subst sum_with_insert[OF comm])
   4.301 +        subgoal using insert.prems by auto
   4.302 +        subgoal using insert.prems by auto
   4.303 +        subgoal by fact
   4.304 +        subgoal by fact
   4.305 +        subgoal by auto
   4.306 +        done
   4.307 +      have rew': "(sum_with pls' zero' g (insert y T')) = pls' (g y) (sum_with pls' zero' g T')"
   4.308 +        apply (subst sum_with_insert[OF comm'])
   4.309 +        subgoal
   4.310 +          apply transfer
   4.311 +          using insert.prems by auto
   4.312 +        subgoal
   4.313 +          apply transfer
   4.314 +          using insert.prems by auto
   4.315 +        subgoal by fact
   4.316 +        subgoal by fact
   4.317 +        subgoal by auto
   4.318 +        done
   4.319 +      have "A (sum_with pls zero f (insert x F)) (sum_with pls' zero' g (insert y T'))"
   4.320 +        unfolding sT_def[symmetric] sF_def[symmetric] rew rew'
   4.321 +        by transfer_prover
   4.322 +      then show ?case
   4.323 +        by (simp add: T_def)
   4.324 +    qed
   4.325 +  next
   4.326 +    assume *: "\<nexists>C. f ` S \<subseteq> C \<and> comm_monoid_add_on_with C pls zero"
   4.327 +    then have **: "\<nexists>C'. g ` T \<subseteq> C' \<and> comm_monoid_add_on_with C' pls' zero'"
   4.328 +      by transfer simp
   4.329 +    show ?thesis
   4.330 +      by (simp add: sum_with_def * ** \<open>A zero zero'\<close>)
   4.331 +  qed
   4.332 +qed
   4.333 +
   4.334 +subsection \<open>Rewrite rules to make \<open>ab_group_add\<close> operations explicit\<close>
   4.335 +
   4.336 +named_theorems explicit_ab_group_add
   4.337 +
   4.338 +lemmas [explicit_ab_group_add] = sum_with
   4.339 +
   4.340 +
   4.341 +end
   4.342 \ No newline at end of file
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy	Wed Jun 27 11:16:43 2018 +0200
     5.3 @@ -0,0 +1,1128 @@
     5.4 +(*  Title:      HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy
     5.5 +    Author:     Fabian Immler, TU München
     5.6 +*)
     5.7 +theory Linear_Algebra_On
     5.8 +  imports
     5.9 +    "../Types_To_Sets"
    5.10 +    "Prerequisites"
    5.11 +    Linear_Algebra_On_With
    5.12 +  keywords "lemmas_with"::thy_decl
    5.13 +begin
    5.14 +
    5.15 +subsection \<open>Rewrite rules to make \<open>ab_group_add\<close> operations implicit.\<close>
    5.16 +
    5.17 +named_theorems implicit_ab_group_add
    5.18 +
    5.19 +lemmas [implicit_ab_group_add] = sum_with[symmetric]
    5.20 +
    5.21 +lemma semigroup_add_on_with_eq[implicit_ab_group_add]:
    5.22 +  "semigroup_add_on_with S ((+)::_::semigroup_add \<Rightarrow> _) \<longleftrightarrow> (\<forall>a\<in>S. \<forall>b\<in>S. a + b \<in> S)"
    5.23 +  by (simp add: semigroup_add_on_with_def ac_simps)
    5.24 +
    5.25 +lemma ab_semigroup_add_on_with_eq[implicit_ab_group_add]:
    5.26 +  "ab_semigroup_add_on_with S ((+)::_::ab_semigroup_add \<Rightarrow> _) = semigroup_add_on_with S (+)"
    5.27 +  unfolding ab_semigroup_add_on_with_def
    5.28 +  by (simp add: semigroup_add_on_with_eq ac_simps)
    5.29 +
    5.30 +lemma comm_monoid_add_on_with_eq[implicit_ab_group_add]:
    5.31 +  "comm_monoid_add_on_with S ((+)::_::comm_monoid_add \<Rightarrow> _) 0 \<longleftrightarrow> semigroup_add_on_with S (+) \<and> 0 \<in> S"
    5.32 +  unfolding comm_monoid_add_on_with_def
    5.33 +  by (simp add: ab_semigroup_add_on_with_eq ac_simps)
    5.34 +
    5.35 +lemma ab_group_add_on_with[implicit_ab_group_add]:
    5.36 +  "ab_group_add_on_with S ((+)::_::ab_group_add \<Rightarrow> _) 0 (-) uminus \<longleftrightarrow> comm_monoid_add_on_with S (+) 0"
    5.37 +  unfolding ab_group_add_on_with_def
    5.38 +  by simp
    5.39 +
    5.40 +subsection \<open>Definitions \<^emph>\<open>on\<close> carrier set\<close>
    5.41 +
    5.42 +locale module_on =
    5.43 +  fixes S and scale :: "'a::comm_ring_1 \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*s" 75)
    5.44 +  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"
    5.45 +    and scale_left_distrib_on [algebra_simps]: "x \<in> S \<Longrightarrow> (a + b) *s x = a *s x + b *s x"
    5.46 +    and scale_scale_on [simp]: "x \<in> S \<Longrightarrow> a *s (b *s x) = (a * b) *s x"
    5.47 +    and scale_one_on [simp]: "x \<in> S \<Longrightarrow> 1 *s x = x"
    5.48 +    and mem_add: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x + y \<in> S"
    5.49 +    and mem_zero: "0 \<in> S"
    5.50 +    and mem_scale: "x \<in> S \<Longrightarrow> a *s x \<in> S"
    5.51 +begin
    5.52 +
    5.53 +lemma S_ne: "S \<noteq> {}" using mem_zero by auto
    5.54 +
    5.55 +lemma scale_minus_left_on: "scale (- a) x = - scale a x" if "x \<in> S"
    5.56 +  by (metis add_cancel_right_right scale_left_distrib_on neg_eq_iff_add_eq_0 that)
    5.57 +
    5.58 +definition subspace :: "'b set \<Rightarrow> bool"
    5.59 +  where subspace_on_def: "subspace T \<longleftrightarrow> 0 \<in> T \<and> (\<forall>x\<in>T. \<forall>y\<in>T. x + y \<in> T) \<and> (\<forall>c. \<forall>x\<in>T. c *s x \<in> T)"
    5.60 +
    5.61 +definition span :: "'b set \<Rightarrow> 'b set"
    5.62 +  where span_on_def: "span b = {sum (\<lambda>a. r a *s  a) t | t r. finite t \<and> t \<subseteq> b}"
    5.63 +
    5.64 +definition dependent :: "'b set \<Rightarrow> bool"
    5.65 +  where dependent_on_def: "dependent s \<longleftrightarrow> (\<exists>t u. finite t \<and> t \<subseteq> s \<and> (sum (\<lambda>v. u v *s v) t = 0 \<and> (\<exists>v\<in>t. u v \<noteq> 0)))"
    5.66 +
    5.67 +lemma implicit_subspace_with[implicit_ab_group_add]: "subspace_with (+) 0 ( *s) = subspace"
    5.68 +  unfolding subspace_on_def subspace_with_def ..
    5.69 +
    5.70 +lemma implicit_dependent_with[implicit_ab_group_add]: "dependent_with (+) 0 ( *s) = dependent"
    5.71 +  unfolding dependent_on_def dependent_with_def sum_with ..
    5.72 +
    5.73 +lemma implicit_span_with[implicit_ab_group_add]: "span_with (+) 0 ( *s) = span"
    5.74 +  unfolding span_on_def span_with_def sum_with ..
    5.75 +
    5.76 +end
    5.77 +
    5.78 +lemma implicit_module_on_with[implicit_ab_group_add]:
    5.79 +  "module_on_with S (+) (-) uminus 0 = module_on S"
    5.80 +  unfolding module_on_with_def module_on_def implicit_ab_group_add
    5.81 +  by auto
    5.82 +
    5.83 +locale module_pair_on = m1: module_on S1 scale1 +
    5.84 +                        m2: module_on S2 scale2
    5.85 +                        for S1:: "'b::ab_group_add set" and S2::"'c::ab_group_add set"
    5.86 +                          and scale1::"'a::comm_ring_1 \<Rightarrow> _" and scale2::"'a \<Rightarrow> _"
    5.87 +
    5.88 +lemma implicit_module_pair_on_with[implicit_ab_group_add]:
    5.89 +  "module_pair_on_with S1 S2 (+) (-) uminus 0 s1 (+) (-) uminus 0 s2 = module_pair_on S1 S2 s1 s2"
    5.90 +  unfolding module_pair_on_with_def implicit_module_on_with module_pair_on_def ..
    5.91 +
    5.92 +locale module_hom_on = m1: module_on S1 s1 + m2: module_on S2 s2
    5.93 +  for S1 :: "'b::ab_group_add set" and S2 :: "'c::ab_group_add set"
    5.94 +    and s1 :: "'a::comm_ring_1 \<Rightarrow> 'b \<Rightarrow> 'b" (infixr "*a" 75)
    5.95 +    and s2 :: "'a::comm_ring_1 \<Rightarrow> 'c \<Rightarrow> 'c" (infixr "*b" 75) +
    5.96 +  fixes f :: "'b \<Rightarrow> 'c"
    5.97 +  assumes add: "\<And>b1 b2. b1 \<in> S1 \<Longrightarrow> b2 \<in> S1 \<Longrightarrow> f (b1 + b2) = f b1 + f b2"
    5.98 +    and scale: "\<And>b. b \<in> S1 \<Longrightarrow> f (r *a b) = r *b f b"
    5.99 +
   5.100 +lemma implicit_module_hom_on_with[implicit_ab_group_add]:
   5.101 +  "module_hom_on_with S1 S2 (+) (-) uminus 0 s1 (+) (-) uminus 0 s2 = module_hom_on S1 S2 s1 s2"
   5.102 +  unfolding module_hom_on_with_def implicit_module_pair_on_with module_hom_on_def module_pair_on_def
   5.103 +    module_hom_on_axioms_def
   5.104 +  by (auto intro!: ext)
   5.105 +
   5.106 +locale vector_space_on = \<comment>\<open>here we do the same trick as in \<open>module\<close> vs \<open>vector_space\<close>.\<close>
   5.107 +  fixes S and scale :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*s" 75)
   5.108 +  assumes scale_right_distrib [algebra_simps]: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> a *s (x + y) = a *s x + a *s y"
   5.109 +    and scale_left_distrib [algebra_simps]: "x \<in> S \<Longrightarrow> (a + b) *s x = a *s x + b *s x"
   5.110 +    and scale_scale [simp]: "x \<in> S \<Longrightarrow> a *s (b *s x) = (a * b) *s x"
   5.111 +    and scale_one [simp]: "x \<in> S \<Longrightarrow> 1 *s x = x"
   5.112 +    and mem_add: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x + y \<in> S"
   5.113 +    and mem_zero: "0 \<in> S"
   5.114 +    and mem_scale: "x \<in> S \<Longrightarrow> a *s x \<in> S"
   5.115 +begin
   5.116 +
   5.117 +sublocale module_on S "( *s)"
   5.118 +  using vector_space_on_axioms[unfolded vector_space_on_def]
   5.119 +  by unfold_locales auto
   5.120 +
   5.121 +definition dim :: "'b set \<Rightarrow> nat"
   5.122 +  where "dim V = (if \<exists>b\<subseteq>S. \<not> dependent b \<and> span b = span V
   5.123 +    then card (SOME b. b \<subseteq> S \<and> \<not> dependent b \<and> span b = span V)
   5.124 +    else 0)"
   5.125 +
   5.126 +lemma implicit_dim_with[implicit_ab_group_add]: "dim_on_with S (+) 0 ( *s) = dim"
   5.127 +  unfolding dim_on_with_def dim_def implicit_ab_group_add ..
   5.128 +
   5.129 +end
   5.130 +
   5.131 +lemma vector_space_on_alt_def: "vector_space_on S = module_on S"
   5.132 +  unfolding vector_space_on_def module_on_def
   5.133 +  by auto
   5.134 +
   5.135 +lemma implicit_vector_space_on_with[implicit_ab_group_add]:
   5.136 +  "vector_space_on_with S (+) (-) uminus 0 = vector_space_on S"
   5.137 +  unfolding vector_space_on_alt_def vector_space_on_def vector_space_on_with_def implicit_module_on_with ..
   5.138 +
   5.139 +locale linear_on = module_hom_on S1 S2 s1 s2 f
   5.140 +  for S1 S2 and s1::"'a::field \<Rightarrow> 'b \<Rightarrow> 'b::ab_group_add"
   5.141 +    and s2::"'a::field \<Rightarrow> 'c \<Rightarrow> 'c::ab_group_add"
   5.142 +    and f
   5.143 +
   5.144 +lemma implicit_linear_on_with[implicit_ab_group_add]:
   5.145 +  "linear_on_with S1 S2 (+) (-) uminus 0 s1 (+) (-) uminus 0 s2 = linear_on S1 S2 s1 s2"
   5.146 +  unfolding linear_on_with_def linear_on_def implicit_module_hom_on_with ..
   5.147 +
   5.148 +locale finite_dimensional_vector_space_on = vector_space_on S scale for S scale +
   5.149 +  fixes basis :: "'a set"
   5.150 +  assumes finite_Basis: "finite basis"
   5.151 +  and independent_Basis: "\<not> dependent basis"
   5.152 +  and span_Basis: "span basis = S" and basis_subset: "basis \<subseteq> S"
   5.153 +
   5.154 +locale vector_space_pair_on = m1: vector_space_on S1 scale1 +
   5.155 +  m2: vector_space_on S2 scale2
   5.156 +  for S1:: "'b::ab_group_add set" and S2::"'c::ab_group_add set"
   5.157 +    and scale1::"'a::field \<Rightarrow> _" and scale2::"'a \<Rightarrow> _"
   5.158 +
   5.159 +locale finite_dimensional_vector_space_pair_on =
   5.160 +  vs1: finite_dimensional_vector_space_on S1 scale1 Basis1 +
   5.161 +  vs2: finite_dimensional_vector_space_on S2 scale2 Basis2
   5.162 +  for S1 S2
   5.163 +    and scale1::"'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b"
   5.164 +    and scale2::"'a::field \<Rightarrow> 'c::ab_group_add \<Rightarrow> 'c"
   5.165 +    and Basis1 Basis2
   5.166 +
   5.167 +subsection \<open>Tool support\<close>
   5.168 +
   5.169 +lemmas subset_iff' = subset_iff[folded Ball_def]
   5.170 +
   5.171 +ML \<open>
   5.172 +structure More_Simplifier =
   5.173 +struct
   5.174 +
   5.175 +fun asm_full_var_simplify ctxt thm =
   5.176 +  let
   5.177 +    val ((_, [thm']), ctxt') = Variable.import false [thm] ctxt
   5.178 +  in
   5.179 +    Simplifier.asm_full_simplify ctxt' thm'
   5.180 +    |> singleton (Variable.export ctxt' ctxt)
   5.181 +    |> Drule.zero_var_indexes
   5.182 +  end
   5.183 +
   5.184 +fun var_simplify_only ctxt ths thm =
   5.185 +  asm_full_var_simplify (Raw_Simplifier.clear_simpset ctxt addsimps ths) thm
   5.186 +
   5.187 +val var_simplified = Attrib.thms >>
   5.188 +  (fn ths => Thm.rule_attribute ths
   5.189 +    (fn context => var_simplify_only (Context.proof_of context) ths))
   5.190 +
   5.191 +val _ = Theory.setup (Attrib.setup \<^binding>\<open>var_simplified\<close> var_simplified "simplified rule (with vars)")
   5.192 +
   5.193 +end
   5.194 +\<close>
   5.195 +
   5.196 +ML \<open>
   5.197 +val _ = Outer_Syntax.local_theory' \<^command_keyword>\<open>lemmas_with\<close> "note theorems with (the same) attributes"
   5.198 +    (Parse.attribs --| @{keyword :} -- Parse_Spec.name_facts -- Parse.for_fixes
   5.199 +     >> (fn (((attrs),facts), fixes) =>
   5.200 +      #2 oo Specification.theorems_cmd Thm.theoremK
   5.201 +        (map (apsnd (map (apsnd (fn xs => attrs@xs)))) facts) fixes))
   5.202 +\<close>
   5.203 +
   5.204 +subsection \<open>Local Typedef for Subspace\<close>
   5.205 +
   5.206 +lemmas [transfer_rule] = right_total_fun_eq_transfer
   5.207 +  and [transfer_rule del] = vimage_parametric
   5.208 +
   5.209 +locale local_typedef = fixes S ::"'b set" and s::"'s itself"
   5.210 +  assumes Ex_type_definition_S: "\<exists>(Rep::'s \<Rightarrow> 'b) (Abs::'b \<Rightarrow> 's). type_definition Rep Abs S"
   5.211 +begin
   5.212 +
   5.213 +definition "rep = fst (SOME (Rep::'s \<Rightarrow> 'b, Abs). type_definition Rep Abs S)"
   5.214 +definition "Abs = snd (SOME (Rep::'s \<Rightarrow> 'b, Abs). type_definition Rep Abs S)"
   5.215 +
   5.216 +lemma type_definition_S: "type_definition rep Abs S"
   5.217 +  unfolding Abs_def rep_def split_beta'
   5.218 +  by (rule someI_ex) (use Ex_type_definition_S in auto)
   5.219 +
   5.220 +lemma rep_in_S[simp]: "rep x \<in> S"
   5.221 +  and rep_inverse[simp]: "Abs (rep x) = x"
   5.222 +  and Abs_inverse[simp]: "y \<in> S \<Longrightarrow> rep (Abs y) = y"
   5.223 +  using type_definition_S
   5.224 +  unfolding type_definition_def by auto
   5.225 +
   5.226 +definition cr_S where "cr_S \<equiv> \<lambda>s b. s = rep b"
   5.227 +lemmas Domainp_cr_S = type_definition_Domainp[OF type_definition_S cr_S_def, transfer_domain_rule]
   5.228 +lemmas right_total_cr_S = typedef_right_total[OF type_definition_S cr_S_def, transfer_rule]
   5.229 +  and bi_unique_cr_S = typedef_bi_unique[OF type_definition_S cr_S_def, transfer_rule]
   5.230 +  and left_unique_cr_S = typedef_left_unique[OF type_definition_S cr_S_def, transfer_rule]
   5.231 +  and right_unique_cr_S = typedef_right_unique[OF type_definition_S cr_S_def, transfer_rule]
   5.232 +
   5.233 +end
   5.234 +
   5.235 +locale local_typedef_ab_group_add = local_typedef S s for S ::"'b::ab_group_add set" and s::"'s itself" +
   5.236 +  assumes mem_zero: "0 \<in> S"
   5.237 +  assumes mem_add: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x + y \<in> S"
   5.238 +  assumes mem_uminus: "x \<in> S \<Longrightarrow> -x \<in> S"
   5.239 +begin
   5.240 +
   5.241 +lemma mem_minus: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x - y \<in> S"
   5.242 +  using mem_add[OF _ mem_uminus] by auto
   5.243 +
   5.244 +context includes lifting_syntax begin
   5.245 +
   5.246 +definition plus_S::"'s \<Rightarrow> 's \<Rightarrow> 's" where "plus_S = (rep ---> rep ---> Abs) plus"
   5.247 +definition minus_S::"'s \<Rightarrow> 's \<Rightarrow> 's" where "minus_S = (rep ---> rep ---> Abs) minus"
   5.248 +definition uminus_S::"'s \<Rightarrow> 's" where "uminus_S = (rep ---> Abs) uminus"
   5.249 +definition zero_S::"'s" where "zero_S = Abs 0"
   5.250 +
   5.251 +lemma plus_S_transfer[transfer_rule]: "(cr_S ===> cr_S ===> cr_S) plus plus_S"
   5.252 +  unfolding plus_S_def
   5.253 +  by (auto simp: cr_S_def mem_add intro!: rel_funI)
   5.254 +
   5.255 +lemma minus_S_transfer[transfer_rule]: "(cr_S ===> cr_S ===> cr_S) minus minus_S"
   5.256 +  unfolding minus_S_def
   5.257 +  by (auto simp: cr_S_def mem_minus intro!: rel_funI)
   5.258 +
   5.259 +lemma uminus_S_transfer[transfer_rule]: "(cr_S ===> cr_S) uminus uminus_S"
   5.260 +  unfolding uminus_S_def
   5.261 +  by (auto simp: cr_S_def mem_uminus intro!: rel_funI)
   5.262 +
   5.263 +lemma zero_S_transfer[transfer_rule]: "cr_S 0 zero_S"
   5.264 +  unfolding zero_S_def
   5.265 +  by (auto simp: cr_S_def mem_zero intro!: rel_funI)
   5.266 +
   5.267 +end
   5.268 +
   5.269 +sublocale type: ab_group_add plus_S "zero_S::'s" minus_S uminus_S
   5.270 +  apply unfold_locales
   5.271 +  subgoal by transfer simp
   5.272 +  subgoal by transfer simp
   5.273 +  subgoal by transfer simp
   5.274 +  subgoal by transfer simp
   5.275 +  subgoal by transfer simp
   5.276 +  done
   5.277 +
   5.278 +context includes lifting_syntax begin
   5.279 +
   5.280 +lemma sum_transfer[transfer_rule]: "((A===>cr_S) ===> rel_set A ===> cr_S) sum type.sum"
   5.281 +  if [transfer_rule]: "bi_unique A"
   5.282 +proof (safe intro!: rel_funI)
   5.283 +  fix f g S T
   5.284 +  assume [transfer_rule]: "(A ===> cr_S) f g" and rel_set: "rel_set A S T"
   5.285 +  show "cr_S (sum f S) (type.sum g T)"
   5.286 +    using rel_set
   5.287 +  proof (induction S arbitrary: T rule: infinite_finite_induct)
   5.288 +    case (infinite S)
   5.289 +    note [transfer_rule] = infinite.prems
   5.290 +    from infinite.hyps have "infinite T" by transfer
   5.291 +    then show ?case by (simp add: infinite.hyps zero_S_transfer)
   5.292 +  next
   5.293 +    case [transfer_rule]: empty
   5.294 +    have "T = {}" by transfer rule
   5.295 +    then show ?case by (simp add: zero_S_transfer)
   5.296 +  next
   5.297 +    case (insert x F)
   5.298 +    note [transfer_rule] = insert.prems
   5.299 +    have [simp]: "finite T"
   5.300 +      by transfer (simp add: insert.hyps)
   5.301 +    obtain y where [transfer_rule]: "A x y" and y: "y \<in> T"
   5.302 +      by (meson insert.prems insertI1 rel_setD1)
   5.303 +    define T' where "T' = T - {y}"
   5.304 +    have T_def: "T = insert y T'"
   5.305 +      by (auto simp: T'_def y)
   5.306 +    define sF where "sF = sum f F"
   5.307 +    define sT where "sT = type.sum g T'"
   5.308 +    have [simp]: "y \<notin> T'" "finite T'"
   5.309 +      by (auto simp: y T'_def)
   5.310 +    have "rel_set A (insert x F - {x}) T'"
   5.311 +      unfolding T'_def
   5.312 +      by transfer_prover
   5.313 +    then have "rel_set A F T'"
   5.314 +      using insert.hyps
   5.315 +      by simp
   5.316 +    from insert.IH[OF this] have [transfer_rule]: "cr_S sF sT" by (auto simp: sF_def sT_def)
   5.317 +    have "cr_S (sum f (insert x F)) (type.sum g (insert y T'))"
   5.318 +      apply (simp add: insert.hyps type.sum.insert_remove sF_def[symmetric] sT_def[symmetric])
   5.319 +      by transfer_prover
   5.320 +    then show ?case
   5.321 +      by (simp add: T_def)
   5.322 +  qed
   5.323 +qed
   5.324 +
   5.325 +end
   5.326 +
   5.327 +end
   5.328 +
   5.329 +locale local_typedef_module_on = module_on S scale
   5.330 +  for S and scale::"'a::comm_ring_1\<Rightarrow>'b\<Rightarrow>'b::ab_group_add" and s::"'s itself" +
   5.331 +  assumes Ex_type_definition_S: "\<exists>(Rep::'s \<Rightarrow> 'b) (Abs::'b \<Rightarrow> 's). type_definition Rep Abs S"
   5.332 +begin
   5.333 +
   5.334 +lemma mem_sum: "sum f X \<in> S" if "\<And>x. x \<in> X \<Longrightarrow> f x \<in> S"
   5.335 +  using that
   5.336 +  by (induction X rule: infinite_finite_induct) (auto intro!: mem_zero mem_add)
   5.337 +
   5.338 +sublocale local_typedef S "TYPE('s)"
   5.339 +  using Ex_type_definition_S by unfold_locales
   5.340 +
   5.341 +sublocale local_typedef_ab_group_add S "TYPE('s)"
   5.342 +  using mem_zero mem_add mem_scale[of _ "-1"]
   5.343 +  by unfold_locales (auto simp: scale_minus_left_on)
   5.344 +
   5.345 +context includes lifting_syntax begin
   5.346 +
   5.347 +definition scale_S::"'a \<Rightarrow> 's \<Rightarrow> 's" where "scale_S = (id ---> rep ---> Abs) scale"
   5.348 +
   5.349 +lemma scale_S_transfer[transfer_rule]: "((=) ===> cr_S ===> cr_S) scale scale_S"
   5.350 +  unfolding scale_S_def
   5.351 +  by (auto simp: cr_S_def mem_scale intro!: rel_funI)
   5.352 +
   5.353 +end
   5.354 +
   5.355 +lemma type_module_on_with: "module_on_with UNIV plus_S minus_S uminus_S (zero_S::'s) scale_S"
   5.356 +proof -
   5.357 +  have "module_on_with {x. x \<in> S} (+) (-) uminus 0 scale"
   5.358 +    using module_on_axioms
   5.359 +    by (auto simp: module_on_with_def module_on_def ab_group_add_on_with_def comm_monoid_add_on_with_def
   5.360 +        ab_semigroup_add_on_with_def semigroup_add_on_with_def)
   5.361 +  then show ?thesis
   5.362 +    by transfer'
   5.363 +qed
   5.364 +
   5.365 +lemma UNIV_transfer[transfer_rule]: "(rel_set cr_S) S UNIV"
   5.366 +  by (auto simp: rel_set_def cr_S_def) (metis Abs_inverse)
   5.367 +
   5.368 +end
   5.369 +
   5.370 +context includes lifting_syntax begin
   5.371 +
   5.372 +lemma Eps_unique_transfer_lemma:
   5.373 +  "f' (Eps (\<lambda>x. Domainp A x \<and> f x)) = g' (Eps g)"
   5.374 +  if [transfer_rule]: "right_total A" "(A ===> (=)) f g" "(A ===> (=)) f' g'"
   5.375 +    and holds: "\<exists>x. Domainp A x \<and> f x"
   5.376 +    and unique_g: "\<And>x y. g x \<Longrightarrow> g y \<Longrightarrow> g' x = g' y"
   5.377 +proof -
   5.378 +  define Epsg where "Epsg = Eps g"
   5.379 +  have "\<exists>x. g x"
   5.380 +    by transfer (simp add: holds)
   5.381 +  then have "g Epsg"
   5.382 +    unfolding Epsg_def
   5.383 +    by (rule someI_ex)
   5.384 +  obtain x where x[transfer_rule]: "A x Epsg"
   5.385 +    by (meson \<open>right_total A\<close> right_totalE)
   5.386 +  then have "Domainp A x" by auto
   5.387 +  from \<open>g Epsg\<close>[untransferred] have "f x" .
   5.388 +  from unique_g have unique:
   5.389 +    "\<And>x y. Domainp A x \<Longrightarrow> Domainp A y \<Longrightarrow> f x \<Longrightarrow> f y \<Longrightarrow> f' x = f' y"
   5.390 +    by transfer
   5.391 +  have "f' (Eps (\<lambda>x. Domainp A x \<and> f x)) = f' x"
   5.392 +    apply (rule unique[OF _ \<open>Domainp A x\<close> _ \<open>f x\<close>])
   5.393 +    apply (metis (mono_tags, lifting) local.holds someI_ex)
   5.394 +    apply (metis (mono_tags, lifting) local.holds someI_ex)
   5.395 +    done
   5.396 +  show "f' (SOME x. Domainp A x \<and> f x) = g' (Eps g)"
   5.397 +    using x \<open>f' (Eps _) = f' x\<close> Epsg_def
   5.398 +    using rel_funE that(3) by fastforce
   5.399 +qed
   5.400 +
   5.401 +end
   5.402 +
   5.403 +locale local_typedef_vector_space_on = local_typedef_module_on S scale s + vector_space_on S scale
   5.404 +  for S and scale::"'a::field\<Rightarrow>'b\<Rightarrow>'b::ab_group_add" and s::"'s itself"
   5.405 +begin
   5.406 +
   5.407 +lemma type_vector_space_on_with: "vector_space_on_with UNIV plus_S minus_S uminus_S (zero_S::'s) scale_S"
   5.408 +  using type_module_on_with
   5.409 +  by (auto simp: vector_space_on_with_def)
   5.410 +
   5.411 +context includes lifting_syntax begin
   5.412 +
   5.413 +definition dim_S::"'s set \<Rightarrow> nat" where "dim_S = dim_on_with UNIV plus_S zero_S scale_S"
   5.414 +
   5.415 +lemma transfer_dim[transfer_rule]: "(rel_set cr_S ===> (=)) dim dim_S"
   5.416 +proof (rule rel_funI)
   5.417 +  fix V V'
   5.418 +  assume [transfer_rule]: "rel_set cr_S V V'"
   5.419 +  then have subset: "V \<subseteq> S"
   5.420 +    by (auto simp: rel_set_def cr_S_def)
   5.421 +  then have "span V \<subseteq> S"
   5.422 +    by (auto simp: span_on_def intro!: mem_sum mem_scale)
   5.423 +  note type_dim_eq_card =
   5.424 +    vector_space.dim_eq_card[var_simplified explicit_ab_group_add, unoverload_type 'd,
   5.425 +      OF type.ab_group_add_axioms type_vector_space_on_with]
   5.426 +  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>
   5.427 +    (\<exists>b\<subseteq>S. \<not> local.dependent b \<and> local.span b = local.span V)"
   5.428 +    unfolding subset_iff
   5.429 +    by transfer (simp add: implicit_ab_group_add Ball_def)
   5.430 +  have **[symmetric]:
   5.431 +    "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)) =
   5.432 +      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')"
   5.433 +    if "b \<subseteq> S" "\<not>dependent b" "span b = span V" for b
   5.434 +    apply (rule Eps_unique_transfer_lemma[where f'=card and g'=card])
   5.435 +    subgoal by (rule right_total_rel_set) (rule transfer_raw)
   5.436 +    subgoal by transfer_prover
   5.437 +    subgoal by transfer_prover
   5.438 +    subgoal using that by (auto simp: implicit_ab_group_add Domainp_set Domainp_cr_S)
   5.439 +    subgoal premises prems for b c
   5.440 +    proof -
   5.441 +      from type_dim_eq_card[of b V'] type_dim_eq_card[of c V'] prems
   5.442 +      show ?thesis by simp
   5.443 +    qed
   5.444 +    done
   5.445 +  show "local.dim V = dim_S V'"
   5.446 +    unfolding dim_def dim_S_def * dim_on_with_def
   5.447 +    by (auto simp: ** Domainp_set Domainp_cr_S implicit_ab_group_add subset_eq)
   5.448 +qed
   5.449 +
   5.450 +end
   5.451 +
   5.452 +
   5.453 +end
   5.454 +
   5.455 +locale local_typedef_finite_dimensional_vector_space_on = local_typedef_vector_space_on S scale s +
   5.456 +  finite_dimensional_vector_space_on S scale Basis
   5.457 +  for S and scale::"'a::field\<Rightarrow>'b\<Rightarrow>'b::ab_group_add" and Basis and s::"'s itself"
   5.458 +begin
   5.459 +
   5.460 +definition "Basis_S = Abs ` Basis"
   5.461 +
   5.462 +lemma Basis_S_transfer[transfer_rule]: "rel_set cr_S Basis Basis_S"
   5.463 +  using Abs_inverse rep_inverse basis_subset
   5.464 +  by (force simp: rel_set_def Basis_S_def cr_S_def)
   5.465 +
   5.466 +lemma type_finite_dimensional_vector_space_on_with:
   5.467 +  "finite_dimensional_vector_space_on_with UNIV plus_S minus_S uminus_S zero_S scale_S Basis_S"
   5.468 +proof -
   5.469 +  have "finite Basis_S" by transfer (rule finite_Basis)
   5.470 +  moreover have "\<not> dependent_with plus_S zero_S scale_S Basis_S"
   5.471 +    by transfer (simp add: implicit_dependent_with independent_Basis)
   5.472 +  moreover have "span_with plus_S zero_S scale_S Basis_S = UNIV"
   5.473 +    by transfer (simp add: implicit_span_with span_Basis)
   5.474 +  ultimately show ?thesis
   5.475 +    using type_vector_space_on_with
   5.476 +    by (auto simp: finite_dimensional_vector_space_on_with_def)
   5.477 +qed
   5.478 +
   5.479 +end
   5.480 +
   5.481 +locale local_typedef_module_pair =
   5.482 +  lt1: local_typedef_module_on S1 scale1 s +
   5.483 +  lt2: local_typedef_module_on S2 scale2 t
   5.484 +  for S1::"'b::ab_group_add set" and scale1::"'a::comm_ring_1 \<Rightarrow> 'b \<Rightarrow> 'b" and s::"'s itself"
   5.485 +    and S2::"'c::ab_group_add set" and scale2::"'a \<Rightarrow> 'c \<Rightarrow> 'c" and t::"'t itself"
   5.486 +begin
   5.487 +
   5.488 +lemma type_module_pair_on_with:
   5.489 +  "module_pair_on_with UNIV UNIV lt1.plus_S lt1.minus_S lt1.uminus_S (lt1.zero_S::'s) lt1.scale_S
   5.490 +  lt2.plus_S lt2.minus_S lt2.uminus_S (lt2.zero_S::'t) lt2.scale_S"
   5.491 +  by (simp add: lt1.type_module_on_with lt2.type_module_on_with module_pair_on_with_def)
   5.492 +
   5.493 +end
   5.494 +
   5.495 +locale local_typedef_vector_space_pair =
   5.496 +  local_typedef_module_pair S1 scale1 s S2 scale2 t
   5.497 +  for S1::"'b::ab_group_add set" and scale1::"'a::field \<Rightarrow> 'b \<Rightarrow> 'b" and s::"'s itself"
   5.498 +    and S2::"'c::ab_group_add set" and scale2::"'a \<Rightarrow> 'c \<Rightarrow> 'c" and t::"'t itself"
   5.499 +begin
   5.500 +
   5.501 +lemma type_vector_space_pair_on_with:
   5.502 +  "vector_space_pair_on_with UNIV UNIV lt1.plus_S lt1.minus_S lt1.uminus_S (lt1.zero_S::'s) lt1.scale_S
   5.503 +  lt2.plus_S lt2.minus_S lt2.uminus_S (lt2.zero_S::'t) lt2.scale_S"
   5.504 +  by (simp add: type_module_pair_on_with vector_space_pair_on_with_def)
   5.505 +
   5.506 +end
   5.507 +
   5.508 +locale local_typedef_finite_dimensional_vector_space_pair =
   5.509 +  lt1: local_typedef_finite_dimensional_vector_space_on S1 scale1 Basis1 s +
   5.510 +  lt2: local_typedef_finite_dimensional_vector_space_on S2 scale2 Basis2 t
   5.511 +  for S1::"'b::ab_group_add set" and scale1::"'a::field \<Rightarrow> 'b \<Rightarrow> 'b" and Basis1 and s::"'s itself"
   5.512 +    and S2::"'c::ab_group_add set" and scale2::"'a \<Rightarrow> 'c \<Rightarrow> 'c" and Basis2 and t::"'t itself"
   5.513 +begin
   5.514 +
   5.515 +lemma type_finite_dimensional_vector_space_pair_on_with:
   5.516 +  "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
   5.517 +  lt2.plus_S lt2.minus_S lt2.uminus_S (lt2.zero_S::'t) lt2.scale_S lt2.Basis_S"
   5.518 +  by (simp add: finite_dimensional_vector_space_pair_on_with_def
   5.519 +      lt1.type_finite_dimensional_vector_space_on_with
   5.520 +      lt2.type_finite_dimensional_vector_space_on_with)
   5.521 +
   5.522 +end
   5.523 +
   5.524 +subsection \<open>Transfer from type-based @{theory HOL.Modules} and @{theory HOL.Vector_Spaces}\<close>
   5.525 +
   5.526 +context module_on begin
   5.527 +
   5.528 +context includes lifting_syntax assumes ltd: "\<exists>(Rep::'s \<Rightarrow> 'b) (Abs::'b \<Rightarrow> 's). type_definition Rep Abs S" begin
   5.529 +
   5.530 +interpretation local_typedef_module_on S scale "TYPE('s)" by unfold_locales fact
   5.531 +
   5.532 +text\<open>Get theorem names:\<close>
   5.533 +print_locale! module
   5.534 +text\<open>Then replace:
   5.535 +notes[^"]*"([^"]*).*
   5.536 +with $1 = module.$1
   5.537 +\<close>
   5.538 +text \<open>TODO: automate systematic naming!\<close>
   5.539 +lemmas_with [var_simplified explicit_ab_group_add,
   5.540 +    unoverload_type 'd,
   5.541 +    OF type.ab_group_add_axioms type_module_on_with,
   5.542 +    untransferred,
   5.543 +    var_simplified implicit_ab_group_add]:
   5.544 +      lt_scale_right_distrib = module.scale_right_distrib
   5.545 +  and lt_scale_left_distrib = module.scale_left_distrib
   5.546 +  and lt_scale_scale = module.scale_scale
   5.547 +  and lt_scale_one = module.scale_one
   5.548 +  and lt_scale_left_commute = module.scale_left_commute
   5.549 +  and lt_scale_zero_left = module.scale_zero_left
   5.550 +  and lt_scale_minus_left = module.scale_minus_left
   5.551 +  and lt_scale_left_diff_distrib = module.scale_left_diff_distrib
   5.552 +  and lt_scale_sum_left = module.scale_sum_left
   5.553 +  and lt_scale_zero_right = module.scale_zero_right
   5.554 +  and lt_scale_minus_right = module.scale_minus_right
   5.555 +  and lt_scale_right_diff_distrib = module.scale_right_diff_distrib
   5.556 +  and lt_scale_sum_right = module.scale_sum_right
   5.557 +  and lt_sum_constant_scale = module.sum_constant_scale
   5.558 +  and lt_subspace_def = module.subspace_def
   5.559 +  and lt_subspaceI = module.subspaceI
   5.560 +  and lt_subspace_single_0 = module.subspace_single_0
   5.561 +  and lt_subspace_0 = module.subspace_0
   5.562 +  and lt_subspace_add = module.subspace_add
   5.563 +  and lt_subspace_scale = module.subspace_scale
   5.564 +  and lt_subspace_neg = module.subspace_neg
   5.565 +  and lt_subspace_diff = module.subspace_diff
   5.566 +  and lt_subspace_sum = module.subspace_sum
   5.567 +  and lt_subspace_inter = module.subspace_inter
   5.568 +  and lt_span_explicit = module.span_explicit
   5.569 +  and lt_span_explicit' = module.span_explicit'
   5.570 +  and lt_span_finite = module.span_finite
   5.571 +  and lt_span_induct_alt = module.span_induct_alt
   5.572 +  and lt_span_mono = module.span_mono
   5.573 +  and lt_span_base = module.span_base
   5.574 +  and lt_span_superset = module.span_superset
   5.575 +  and lt_span_zero = module.span_zero
   5.576 +  and lt_span_add = module.span_add
   5.577 +  and lt_span_scale = module.span_scale
   5.578 +  and lt_subspace_span = module.subspace_span
   5.579 +  and lt_span_neg = module.span_neg
   5.580 +  and lt_span_diff = module.span_diff
   5.581 +  and lt_span_sum = module.span_sum
   5.582 +  and lt_span_minimal = module.span_minimal
   5.583 +  and lt_span_unique = module.span_unique
   5.584 +  and lt_span_subspace_induct = module.span_subspace_induct
   5.585 +  and lt_span_induct = module.span_induct
   5.586 +  and lt_span_empty = module.span_empty
   5.587 +  and lt_span_subspace = module.span_subspace
   5.588 +  and lt_span_span = module.span_span
   5.589 +  and lt_span_add_eq = module.span_add_eq
   5.590 +  and lt_span_add_eq2 = module.span_add_eq2
   5.591 +  and lt_span_singleton = module.span_singleton
   5.592 +  and lt_span_Un = module.span_Un
   5.593 +  and lt_span_insert = module.span_insert
   5.594 +  and lt_span_breakdown = module.span_breakdown
   5.595 +  and lt_span_breakdown_eq = module.span_breakdown_eq
   5.596 +  and lt_span_clauses = module.span_clauses
   5.597 +  and lt_span_eq_iff = module.span_eq_iff
   5.598 +  and lt_span_eq = module.span_eq
   5.599 +  and lt_eq_span_insert_eq = module.eq_span_insert_eq
   5.600 +  and lt_dependent_explicit = module.dependent_explicit
   5.601 +  and lt_dependent_mono = module.dependent_mono
   5.602 +  and lt_independent_mono = module.independent_mono
   5.603 +  and lt_dependent_zero = module.dependent_zero
   5.604 +  and lt_independent_empty = module.independent_empty
   5.605 +  and lt_independent_explicit_module = module.independent_explicit_module
   5.606 +  and lt_independentD = module.independentD
   5.607 +  and lt_independent_Union_directed = module.independent_Union_directed
   5.608 +  and lt_dependent_finite = module.dependent_finite
   5.609 +  and lt_independentD_alt = module.independentD_alt
   5.610 +  and lt_independentD_unique = module.independentD_unique
   5.611 +  and lt_spanning_subset_independent = module.spanning_subset_independent
   5.612 +  and lt_module_hom_scale_self = module.module_hom_scale_self
   5.613 +  and lt_module_hom_scale_left = module.module_hom_scale_left
   5.614 +  and lt_module_hom_id = module.module_hom_id
   5.615 +  and lt_module_hom_ident = module.module_hom_ident
   5.616 +  and lt_module_hom_uminus = module.module_hom_uminus
   5.617 +  and subspace_UNIV = module.subspace_UNIV
   5.618 +  and span_alt = module.span_alt
   5.619 +(* should work but don't:
   5.620 +  and span_def = module.span_def
   5.621 +  and span_UNIV = module.span_UNIV
   5.622 +  and dependent_alt = module.dependent_alt
   5.623 +  and independent_alt = module.independent_alt
   5.624 +  and unique_representation = module.unique_representation
   5.625 +  and subspace_Int = module.subspace_Int
   5.626 +  and subspace_Inter = module.subspace_Inter
   5.627 +*)
   5.628 +(* not expected to work:
   5.629 +and representation_ne_zero = module.representation_ne_zero
   5.630 +and representation_ne_zero = module.representation_ne_zero
   5.631 +and finite_representation = module.finite_representation
   5.632 +and sum_nonzero_representation_eq = module.sum_nonzero_representation_eq
   5.633 +and sum_representation_eq = module.sum_representation_eq
   5.634 +and representation_eqI = module.representation_eqI
   5.635 +and representation_basis = module.representation_basis
   5.636 +and representation_zero = module.representation_zero
   5.637 +and representation_diff = module.representation_diff
   5.638 +and representation_neg = module.representation_neg
   5.639 +and representation_add = module.representation_add
   5.640 +and representation_sum = module.representation_sum
   5.641 +and representation_scale = module.representation_scale
   5.642 +and representation_extend = module.representation_extend
   5.643 +end
   5.644 +*)
   5.645 +
   5.646 +end
   5.647 +
   5.648 +lemmas_with [cancel_type_definition,
   5.649 +    OF S_ne,
   5.650 +    folded subset_iff',
   5.651 +    simplified pred_fun_def,
   5.652 +    simplified\<comment>\<open>too much?\<close>]:
   5.653 +      scale_right_distrib = lt_scale_right_distrib
   5.654 +  and scale_left_distrib = lt_scale_left_distrib
   5.655 +  and scale_scale = lt_scale_scale
   5.656 +  and scale_one = lt_scale_one
   5.657 +  and scale_left_commute = lt_scale_left_commute
   5.658 +  and scale_zero_left = lt_scale_zero_left
   5.659 +  and scale_minus_left = lt_scale_minus_left
   5.660 +  and scale_left_diff_distrib = lt_scale_left_diff_distrib
   5.661 +  and scale_sum_left = lt_scale_sum_left
   5.662 +  and scale_zero_right = lt_scale_zero_right
   5.663 +  and scale_minus_right = lt_scale_minus_right
   5.664 +  and scale_right_diff_distrib = lt_scale_right_diff_distrib
   5.665 +  and scale_sum_right = lt_scale_sum_right
   5.666 +  and sum_constant_scale = lt_sum_constant_scale
   5.667 +  and subspace_def = lt_subspace_def
   5.668 +  and subspaceI = lt_subspaceI
   5.669 +  and subspace_single_0 = lt_subspace_single_0
   5.670 +  and subspace_0 = lt_subspace_0
   5.671 +  and subspace_add = lt_subspace_add
   5.672 +  and subspace_scale = lt_subspace_scale
   5.673 +  and subspace_neg = lt_subspace_neg
   5.674 +  and subspace_diff = lt_subspace_diff
   5.675 +  and subspace_sum = lt_subspace_sum
   5.676 +  and subspace_inter = lt_subspace_inter
   5.677 +  and span_explicit = lt_span_explicit
   5.678 +  and span_explicit' = lt_span_explicit'
   5.679 +  and span_finite = lt_span_finite
   5.680 +  and span_induct_alt[consumes 1, case_names base step, induct set : span] = lt_span_induct_alt
   5.681 +  and span_mono = lt_span_mono
   5.682 +  and span_base = lt_span_base
   5.683 +  and span_superset = lt_span_superset
   5.684 +  and span_zero = lt_span_zero
   5.685 +  and span_add = lt_span_add
   5.686 +  and span_scale = lt_span_scale
   5.687 +  and subspace_span = lt_subspace_span
   5.688 +  and span_neg = lt_span_neg
   5.689 +  and span_diff = lt_span_diff
   5.690 +  and span_sum = lt_span_sum
   5.691 +  and span_minimal = lt_span_minimal
   5.692 +  and span_unique = lt_span_unique
   5.693 +  and span_subspace_induct[consumes 2] = lt_span_subspace_induct
   5.694 +  and span_induct[consumes 1, case_names base step, induct set : span] = lt_span_induct
   5.695 +  and span_empty = lt_span_empty
   5.696 +  and span_subspace = lt_span_subspace
   5.697 +  and span_span = lt_span_span
   5.698 +  and span_add_eq = lt_span_add_eq
   5.699 +  and span_add_eq2 = lt_span_add_eq2
   5.700 +  and span_singleton = lt_span_singleton
   5.701 +  and span_Un = lt_span_Un
   5.702 +  and span_insert = lt_span_insert
   5.703 +  and span_breakdown = lt_span_breakdown
   5.704 +  and span_breakdown_eq = lt_span_breakdown_eq
   5.705 +  and span_clauses = lt_span_clauses
   5.706 +  and span_eq_iff = lt_span_eq_iff
   5.707 +  and span_eq = lt_span_eq
   5.708 +  and eq_span_insert_eq = lt_eq_span_insert_eq
   5.709 +  and dependent_explicit = lt_dependent_explicit
   5.710 +  and dependent_mono = lt_dependent_mono
   5.711 +  and independent_mono = lt_independent_mono
   5.712 +  and dependent_zero = lt_dependent_zero
   5.713 +  and independent_empty = lt_independent_empty
   5.714 +  and independent_explicit_module = lt_independent_explicit_module
   5.715 +  and independentD = lt_independentD
   5.716 +  and independent_Union_directed = lt_independent_Union_directed
   5.717 +  and dependent_finite = lt_dependent_finite
   5.718 +  and independentD_alt = lt_independentD_alt
   5.719 +  and independentD_unique = lt_independentD_unique
   5.720 +  and spanning_subset_independent = lt_spanning_subset_independent
   5.721 +  and module_hom_scale_self = lt_module_hom_scale_self
   5.722 +  and module_hom_scale_left = lt_module_hom_scale_left
   5.723 +  and module_hom_id = lt_module_hom_id
   5.724 +  and module_hom_ident = lt_module_hom_ident
   5.725 +  and module_hom_uminus = lt_module_hom_uminus
   5.726 +
   5.727 +end
   5.728 +
   5.729 +subsubsection \<open>Vector Spaces\<close>
   5.730 +
   5.731 +context vector_space_on begin
   5.732 +
   5.733 +context includes lifting_syntax assumes "\<exists>(Rep::'s \<Rightarrow> 'b) (Abs::'b \<Rightarrow> 's). type_definition Rep Abs S" begin
   5.734 +
   5.735 +interpretation local_typedef_vector_space_on S scale "TYPE('s)" by unfold_locales fact
   5.736 +
   5.737 +lemmas_with [var_simplified explicit_ab_group_add,
   5.738 +    unoverload_type 'd,
   5.739 +    OF type.ab_group_add_axioms type_vector_space_on_with,
   5.740 +    untransferred,
   5.741 +    var_simplified implicit_ab_group_add]:
   5.742 + lt_vector_space_assms = vector_space.vector_space_assms
   5.743 +and lt_linear_id = vector_space.linear_id
   5.744 +and lt_linear_ident = vector_space.linear_ident
   5.745 +and lt_linear_scale_self = vector_space.linear_scale_self
   5.746 +and lt_linear_scale_left = vector_space.linear_scale_left
   5.747 +and lt_linear_uminus = vector_space.linear_uminus
   5.748 +and lt_linear_imp_scale["consumes" - 1, "case_names" "1"] = vector_space.linear_imp_scale
   5.749 +and lt_scale_eq_0_iff = vector_space.scale_eq_0_iff
   5.750 +and lt_scale_left_imp_eq = vector_space.scale_left_imp_eq
   5.751 +and lt_scale_right_imp_eq = vector_space.scale_right_imp_eq
   5.752 +and lt_scale_cancel_left = vector_space.scale_cancel_left
   5.753 +and lt_scale_cancel_right = vector_space.scale_cancel_right
   5.754 +and lt_injective_scale = vector_space.injective_scale
   5.755 +and lt_dependent_def = vector_space.dependent_def
   5.756 +and lt_dependent_single = vector_space.dependent_single
   5.757 +and lt_in_span_insert = vector_space.in_span_insert
   5.758 +and lt_dependent_insertD = vector_space.dependent_insertD
   5.759 +and lt_independent_insertI = vector_space.independent_insertI
   5.760 +and lt_independent_insert = vector_space.independent_insert
   5.761 +and lt_maximal_independent_subset_extend["consumes" - 1, "case_names" "1"] = vector_space.maximal_independent_subset_extend
   5.762 +and lt_maximal_independent_subset["consumes" - 1, "case_names" "1"] = vector_space.maximal_independent_subset
   5.763 +and lt_in_span_delete = vector_space.in_span_delete
   5.764 +and lt_span_redundant = vector_space.span_redundant
   5.765 +and lt_span_trans = vector_space.span_trans
   5.766 +and lt_span_insert_0 = vector_space.span_insert_0
   5.767 +and lt_span_delete_0 = vector_space.span_delete_0
   5.768 +and lt_span_image_scale = vector_space.span_image_scale
   5.769 +and lt_exchange_lemma = vector_space.exchange_lemma
   5.770 +and lt_independent_span_bound = vector_space.independent_span_bound
   5.771 +and lt_independent_explicit_finite_subsets = vector_space.independent_explicit_finite_subsets
   5.772 +and lt_independent_if_scalars_zero = vector_space.independent_if_scalars_zero
   5.773 +and lt_subspace_sums = vector_space.subspace_sums
   5.774 +(* should work but don't:
   5.775 +and lt_injective_scale = vector_space.lt_injective_scale
   5.776 +and lt_bij_if_span_eq_span_bases = vector_space.bij_if_span_eq_span_bases
   5.777 +and lt_dim_def = vector_space.dim_def
   5.778 +and lt_dim_eq_card = vector_space.dim_eq_card
   5.779 +and lt_basis_card_eq_dim = vector_space.basis_card_eq_dim
   5.780 +and lt_basis_exists["consumes" - 1, "case_names" "1"] = vector_space.basis_exists
   5.781 +and lt_dim_eq_card_independent = vector_space.dim_eq_card_independent
   5.782 +and lt_dim_span = vector_space.dim_span
   5.783 +and lt_dim_span_eq_card_independent = vector_space.dim_span_eq_card_independent
   5.784 +and lt_dim_le_card = vector_space.dim_le_card
   5.785 +and lt_span_eq_dim = vector_space.span_eq_dim
   5.786 +and lt_dim_le_card' = vector_space.dim_le_card'
   5.787 +and lt_span_card_ge_dim = vector_space.span_card_ge_dim
   5.788 +and lt_dim_unique = vector_space.dim_unique
   5.789 +and     lt_dim_with = vector_space.dim_with
   5.790 +*)
   5.791 +(* not expected to work:
   5.792 +and lt_extend_basis_superset = vector_space.extend_basis_superset
   5.793 +and lt_independent_extend_basis = vector_space.independent_extend_basis
   5.794 +and lt_span_extend_basis = vector_space.span_extend_basis
   5.795 +*)
   5.796 +
   5.797 +end
   5.798 +
   5.799 +lemmas_with [cancel_type_definition,
   5.800 +    OF S_ne,
   5.801 +    folded subset_iff',
   5.802 +    simplified pred_fun_def,
   5.803 +    simplified\<comment>\<open>too much?\<close>]:
   5.804 + vector_space_assms = lt_vector_space_assms
   5.805 +and linear_id = lt_linear_id
   5.806 +and linear_ident = lt_linear_ident
   5.807 +and linear_scale_self = lt_linear_scale_self
   5.808 +and linear_scale_left = lt_linear_scale_left
   5.809 +and linear_uminus = lt_linear_uminus
   5.810 +and linear_imp_scale["consumes" - 1, "case_names" "1"] = lt_linear_imp_scale
   5.811 +and scale_eq_0_iff = lt_scale_eq_0_iff
   5.812 +and scale_left_imp_eq = lt_scale_left_imp_eq
   5.813 +and scale_right_imp_eq = lt_scale_right_imp_eq
   5.814 +and scale_cancel_left = lt_scale_cancel_left
   5.815 +and scale_cancel_right = lt_scale_cancel_right
   5.816 +and dependent_def = lt_dependent_def
   5.817 +and dependent_single = lt_dependent_single
   5.818 +and in_span_insert = lt_in_span_insert
   5.819 +and dependent_insertD = lt_dependent_insertD
   5.820 +and independent_insertI = lt_independent_insertI
   5.821 +and independent_insert = lt_independent_insert
   5.822 +and maximal_independent_subset_extend["consumes" - 1, "case_names" "1"] = lt_maximal_independent_subset_extend
   5.823 +and maximal_independent_subset["consumes" - 1, "case_names" "1"] = lt_maximal_independent_subset
   5.824 +and in_span_delete = lt_in_span_delete
   5.825 +and span_redundant = lt_span_redundant
   5.826 +and span_trans = lt_span_trans
   5.827 +and span_insert_0 = lt_span_insert_0
   5.828 +and span_delete_0 = lt_span_delete_0
   5.829 +and span_image_scale = lt_span_image_scale
   5.830 +and exchange_lemma = lt_exchange_lemma
   5.831 +and independent_span_bound = lt_independent_span_bound
   5.832 +and independent_explicit_finite_subsets = lt_independent_explicit_finite_subsets
   5.833 +and independent_if_scalars_zero = lt_independent_if_scalars_zero
   5.834 +and subspace_sums = lt_subspace_sums
   5.835 +
   5.836 +end
   5.837 +
   5.838 +subsubsection \<open>Finite Dimensional Vector Spaces\<close>
   5.839 +
   5.840 +context finite_dimensional_vector_space_on begin
   5.841 +
   5.842 +context includes lifting_syntax assumes "\<exists>(Rep::'s \<Rightarrow> 'a) (Abs::'a \<Rightarrow> 's). type_definition Rep Abs S" begin
   5.843 +
   5.844 +interpretation local_typedef_finite_dimensional_vector_space_on S scale basis "TYPE('s)" by unfold_locales fact
   5.845 +
   5.846 +lemmas_with [var_simplified explicit_ab_group_add,
   5.847 +    unoverload_type 'd,
   5.848 +    OF type.ab_group_add_axioms type_finite_dimensional_vector_space_on_with,
   5.849 +    folded dim_S_def,
   5.850 +    untransferred,
   5.851 +    var_simplified implicit_ab_group_add]:
   5.852 +     lt_finiteI_independent = finite_dimensional_vector_space.finiteI_independent
   5.853 +and  lt_dim_empty = finite_dimensional_vector_space.dim_empty
   5.854 +and  lt_dim_insert = finite_dimensional_vector_space.dim_insert
   5.855 +and  lt_dim_singleton = finite_dimensional_vector_space.dim_singleton
   5.856 +and  lt_choose_subspace_of_subspace["consumes" - 1, "case_names" "1"] = finite_dimensional_vector_space.choose_subspace_of_subspace
   5.857 +and  lt_basis_subspace_exists["consumes" - 1, "case_names" "1"] = finite_dimensional_vector_space.basis_subspace_exists
   5.858 +and  lt_dim_mono = finite_dimensional_vector_space.dim_mono
   5.859 +and  lt_dim_subset = finite_dimensional_vector_space.dim_subset
   5.860 +and  lt_dim_eq_0 = finite_dimensional_vector_space.dim_eq_0
   5.861 +and  lt_dim_UNIV = finite_dimensional_vector_space.dim_UNIV
   5.862 +and  lt_independent_card_le_dim = finite_dimensional_vector_space.independent_card_le_dim
   5.863 +and  lt_card_ge_dim_independent = finite_dimensional_vector_space.card_ge_dim_independent
   5.864 +and  lt_card_le_dim_spanning = finite_dimensional_vector_space.card_le_dim_spanning
   5.865 +and  lt_card_eq_dim = finite_dimensional_vector_space.card_eq_dim
   5.866 +and  lt_subspace_dim_equal = finite_dimensional_vector_space.subspace_dim_equal
   5.867 +and  lt_dim_eq_span = finite_dimensional_vector_space.dim_eq_span
   5.868 +and  lt_dim_psubset = finite_dimensional_vector_space.dim_psubset
   5.869 +and  lt_indep_card_eq_dim_span = finite_dimensional_vector_space.indep_card_eq_dim_span
   5.870 +and  lt_independent_bound_general = finite_dimensional_vector_space.independent_bound_general
   5.871 +and  lt_independent_explicit = finite_dimensional_vector_space.independent_explicit
   5.872 +and  lt_dim_sums_Int = finite_dimensional_vector_space.dim_sums_Int
   5.873 +and  lt_dependent_biggerset_general = finite_dimensional_vector_space.dependent_biggerset_general
   5.874 +and  lt_subset_le_dim = finite_dimensional_vector_space.subset_le_dim
   5.875 +and  lt_linear_inj_imp_surj = finite_dimensional_vector_space.linear_inj_imp_surj
   5.876 +and  lt_linear_surj_imp_inj = finite_dimensional_vector_space.linear_surj_imp_inj
   5.877 +and  lt_linear_inverse_left = finite_dimensional_vector_space.linear_inverse_left
   5.878 +and  lt_left_inverse_linear = finite_dimensional_vector_space.left_inverse_linear
   5.879 +and  lt_right_inverse_linear = finite_dimensional_vector_space.right_inverse_linear
   5.880 +(* not expected to work:
   5.881 +     lt_dimension_def = finite_dimensional_vector_space.dimension_def
   5.882 +and  lt_dim_subset_UNIV = finite_dimensional_vector_space.dim_subset_UNIV
   5.883 +and  lt_dim_eq_full = finite_dimensional_vector_space.dim_eq_full
   5.884 +and  lt_inj_linear_imp_inv_linear = finite_dimensional_vector_space.inj_linear_imp_inv_linear
   5.885 +*)
   5.886 +
   5.887 +end
   5.888 +
   5.889 +lemmas_with [cancel_type_definition,
   5.890 +    OF S_ne,
   5.891 +    folded subset_iff',
   5.892 +    simplified pred_fun_def,
   5.893 +    simplified\<comment>\<open>too much?\<close>]:
   5.894 + vector_space_assms = lt_vector_space_assms
   5.895 +and linear_id = lt_linear_id
   5.896 +and linear_ident = lt_linear_ident
   5.897 +and linear_scale_self = lt_linear_scale_self
   5.898 +and linear_scale_left = lt_linear_scale_left
   5.899 +and linear_uminus = lt_linear_uminus
   5.900 +and linear_imp_scale["consumes" - 1, "case_names" "1"] = lt_linear_imp_scale
   5.901 +and scale_eq_0_iff = lt_scale_eq_0_iff
   5.902 +and scale_left_imp_eq = lt_scale_left_imp_eq
   5.903 +and scale_right_imp_eq = lt_scale_right_imp_eq
   5.904 +and scale_cancel_left = lt_scale_cancel_left
   5.905 +and scale_cancel_right = lt_scale_cancel_right
   5.906 +and dependent_def = lt_dependent_def
   5.907 +and dependent_single = lt_dependent_single
   5.908 +and in_span_insert = lt_in_span_insert
   5.909 +and dependent_insertD = lt_dependent_insertD
   5.910 +and independent_insertI = lt_independent_insertI
   5.911 +and independent_insert = lt_independent_insert
   5.912 +and maximal_independent_subset_extend["consumes" - 1, "case_names" "1"] = lt_maximal_independent_subset_extend
   5.913 +and maximal_independent_subset["consumes" - 1, "case_names" "1"] = lt_maximal_independent_subset
   5.914 +and in_span_delete = lt_in_span_delete
   5.915 +and span_redundant = lt_span_redundant
   5.916 +and span_trans = lt_span_trans
   5.917 +and span_insert_0 = lt_span_insert_0
   5.918 +and span_delete_0 = lt_span_delete_0
   5.919 +and span_image_scale = lt_span_image_scale
   5.920 +and exchange_lemma = lt_exchange_lemma
   5.921 +and independent_span_bound = lt_independent_span_bound
   5.922 +and independent_explicit_finite_subsets = lt_independent_explicit_finite_subsets
   5.923 +and independent_if_scalars_zero = lt_independent_if_scalars_zero
   5.924 +and subspace_sums = lt_subspace_sums
   5.925 +
   5.926 +end
   5.927 +
   5.928 +context module_pair_on begin
   5.929 +
   5.930 +context includes lifting_syntax
   5.931 +  assumes
   5.932 +    "\<exists>(Rep::'s \<Rightarrow> 'b) (Abs::'b \<Rightarrow> 's). type_definition Rep Abs S1"
   5.933 +    "\<exists>(Rep::'t \<Rightarrow> 'c) (Abs::'c \<Rightarrow> 't). type_definition Rep Abs S2" begin
   5.934 +
   5.935 +interpretation local_typedef_module_pair S1 scale1 "TYPE('s)" S2 scale2 "TYPE('t)" by unfold_locales fact+
   5.936 +
   5.937 +lemmas_with [var_simplified explicit_ab_group_add,
   5.938 +  unoverload_type 'e 'b,
   5.939 +  OF lt2.type.ab_group_add_axioms lt1.type.ab_group_add_axioms type_module_pair_on_with,
   5.940 +  untransferred,
   5.941 +  var_simplified implicit_ab_group_add]:
   5.942 +  lt_module_hom_zero = module_pair.module_hom_zero
   5.943 +and lt_module_hom_add = module_pair.module_hom_add
   5.944 +and lt_module_hom_sub = module_pair.module_hom_sub
   5.945 +and lt_module_hom_neg = module_pair.module_hom_neg
   5.946 +and lt_module_hom_scale = module_pair.module_hom_scale
   5.947 +and lt_module_hom_compose_scale = module_pair.module_hom_compose_scale
   5.948 +and lt_module_hom_sum = module_pair.module_hom_sum
   5.949 +and lt_module_hom_eq_on_span = module_pair.module_hom_eq_on_span
   5.950 +(* should work, but doesnt
   5.951 +and lt_bij_module_hom_imp_inv_module_hom = module_pair.bij_module_hom_imp_inv_module_hom[of scale1 scale2]
   5.952 +*)
   5.953 +
   5.954 +end
   5.955 +
   5.956 +lemmas_with [cancel_type_definition, OF m1.S_ne,
   5.957 +  cancel_type_definition, OF m2.S_ne,
   5.958 +    folded subset_iff' top_set_def,
   5.959 +    simplified pred_fun_def,
   5.960 +    simplified\<comment>\<open>too much?\<close>]:
   5.961 +  module_hom_zero = lt_module_hom_zero
   5.962 +and module_hom_add = lt_module_hom_add
   5.963 +and module_hom_sub = lt_module_hom_sub
   5.964 +and module_hom_neg = lt_module_hom_neg
   5.965 +and module_hom_scale = lt_module_hom_scale
   5.966 +and module_hom_compose_scale = lt_module_hom_compose_scale
   5.967 +and module_hom_sum = lt_module_hom_sum
   5.968 +and module_hom_eq_on_span = lt_module_hom_eq_on_span
   5.969 +
   5.970 +end
   5.971 +
   5.972 +context vector_space_pair_on begin
   5.973 +
   5.974 +context includes lifting_syntax
   5.975 +  notes [transfer_rule del] = Collect_transfer
   5.976 +  assumes
   5.977 +    "\<exists>(Rep::'s \<Rightarrow> 'b) (Abs::'b \<Rightarrow> 's). type_definition Rep Abs S1"
   5.978 +    "\<exists>(Rep::'t \<Rightarrow> 'c) (Abs::'c \<Rightarrow> 't). type_definition Rep Abs S2" begin
   5.979 +
   5.980 +interpretation local_typedef_vector_space_pair S1 scale1 "TYPE('s)" S2 scale2 "TYPE('t)" by unfold_locales fact+
   5.981 +
   5.982 +lemmas_with [var_simplified explicit_ab_group_add,
   5.983 +    unoverload_type 'e 'b,
   5.984 +  OF lt2.type.ab_group_add_axioms lt1.type.ab_group_add_axioms type_vector_space_pair_on_with,
   5.985 +  untransferred,
   5.986 +  var_simplified implicit_ab_group_add]:
   5.987 +  lt_linear_0 = vector_space_pair.linear_0
   5.988 +and lt_linear_add = vector_space_pair.linear_add
   5.989 +and lt_linear_scale = vector_space_pair.linear_scale
   5.990 +and lt_linear_neg = vector_space_pair.linear_neg
   5.991 +and lt_linear_diff = vector_space_pair.linear_diff
   5.992 +and lt_linear_sum = vector_space_pair.linear_sum
   5.993 +and lt_linear_inj_on_iff_eq_0 = vector_space_pair.linear_inj_on_iff_eq_0
   5.994 +and lt_linear_inj_iff_eq_0 = vector_space_pair.linear_inj_iff_eq_0
   5.995 +and lt_linear_subspace_image = vector_space_pair.linear_subspace_image
   5.996 +and lt_linear_subspace_vimage = vector_space_pair.linear_subspace_vimage
   5.997 +and lt_linear_subspace_kernel = vector_space_pair.linear_subspace_kernel
   5.998 +and lt_linear_span_image = vector_space_pair.linear_span_image
   5.999 +and lt_linear_dependent_inj_imageD = vector_space_pair.linear_dependent_inj_imageD
  5.1000 +and lt_linear_eq_0_on_span = vector_space_pair.linear_eq_0_on_span
  5.1001 +and lt_linear_independent_injective_image = vector_space_pair.linear_independent_injective_image
  5.1002 +and lt_linear_inj_on_span_independent_image = vector_space_pair.linear_inj_on_span_independent_image
  5.1003 +and lt_linear_inj_on_span_iff_independent_image = vector_space_pair.linear_inj_on_span_iff_independent_image
  5.1004 +and lt_linear_subspace_linear_preimage = vector_space_pair.linear_subspace_linear_preimage
  5.1005 +and lt_linear_spans_image = vector_space_pair.linear_spans_image
  5.1006 +and lt_linear_spanning_surjective_image = vector_space_pair.linear_spanning_surjective_image
  5.1007 +and lt_linear_eq_on_span = vector_space_pair.linear_eq_on_span
  5.1008 +and lt_linear_compose_scale_right = vector_space_pair.linear_compose_scale_right
  5.1009 +and lt_linear_compose_add = vector_space_pair.linear_compose_add
  5.1010 +and lt_linear_zero = vector_space_pair.linear_zero
  5.1011 +and lt_linear_compose_sub = vector_space_pair.linear_compose_sub
  5.1012 +and lt_linear_compose_neg = vector_space_pair.linear_compose_neg
  5.1013 +and lt_linear_compose_scale = vector_space_pair.linear_compose_scale
  5.1014 +and lt_linear_indep_image_lemma = vector_space_pair.linear_indep_image_lemma
  5.1015 +and lt_linear_eq_on = vector_space_pair.linear_eq_on
  5.1016 +and lt_linear_compose_sum = vector_space_pair.linear_compose_sum
  5.1017 +and lt_linear_independent_extend_subspace = vector_space_pair.linear_independent_extend_subspace
  5.1018 +and lt_linear_independent_extend = vector_space_pair.linear_independent_extend
  5.1019 +and lt_linear_exists_left_inverse_on = vector_space_pair.linear_exists_left_inverse_on
  5.1020 +and lt_linear_exists_right_inverse_on = vector_space_pair.linear_exists_right_inverse_on
  5.1021 +and lt_linear_inj_on_left_inverse = vector_space_pair.linear_inj_on_left_inverse
  5.1022 +and lt_linear_injective_left_inverse = vector_space_pair.linear_injective_left_inverse
  5.1023 +and lt_linear_surj_right_inverse = vector_space_pair.linear_surj_right_inverse
  5.1024 +and lt_linear_surjective_right_inverse = vector_space_pair.linear_surjective_right_inverse
  5.1025 +(* should work, but doesnt
  5.1026 +*)
  5.1027 +(* not expected to work:
  5.1028 +  lt_construct_def = vector_space_pair.construct_def
  5.1029 +  lt_construct_cong = vector_space_pair.construct_cong
  5.1030 +  lt_linear_construct = vector_space_pair.linear_construct
  5.1031 +  lt_construct_basis = vector_space_pair.construct_basis
  5.1032 +  lt_construct_outside = vector_space_pair.construct_outside
  5.1033 +  lt_construct_add = vector_space_pair.construct_add
  5.1034 +  lt_construct_scale = vector_space_pair.construct_scale
  5.1035 +  lt_construct_in_span = vector_space_pair.construct_in_span
  5.1036 +  lt_in_span_in_range_construct = vector_space_pair.in_span_in_range_construct
  5.1037 +  lt_range_construct_eq_span = vector_space_pair.range_construct_eq_span
  5.1038 +*)
  5.1039 +
  5.1040 +end
  5.1041 +
  5.1042 +lemmas_with [cancel_type_definition, OF m1.S_ne,
  5.1043 +    cancel_type_definition, OF m2.S_ne,
  5.1044 +    folded subset_iff' top_set_def,
  5.1045 +    simplified pred_fun_def,
  5.1046 +    simplified\<comment>\<open>too much?\<close>]:
  5.1047 +  linear_0 = lt_linear_0
  5.1048 +  and linear_add = lt_linear_add
  5.1049 +  and linear_scale = lt_linear_scale
  5.1050 +  and linear_neg = lt_linear_neg
  5.1051 +  and linear_diff = lt_linear_diff
  5.1052 +  and linear_sum = lt_linear_sum
  5.1053 +  and linear_inj_on_iff_eq_0 = lt_linear_inj_on_iff_eq_0
  5.1054 +  and linear_inj_iff_eq_0 = lt_linear_inj_iff_eq_0
  5.1055 +  and linear_subspace_image = lt_linear_subspace_image
  5.1056 +  and linear_subspace_vimage = lt_linear_subspace_vimage
  5.1057 +  and linear_subspace_kernel = lt_linear_subspace_kernel
  5.1058 +  and linear_span_image = lt_linear_span_image
  5.1059 +  and linear_dependent_inj_imageD = lt_linear_dependent_inj_imageD
  5.1060 +  and linear_eq_0_on_span = lt_linear_eq_0_on_span
  5.1061 +  and linear_independent_injective_image = lt_linear_independent_injective_image
  5.1062 +  and linear_inj_on_span_independent_image = lt_linear_inj_on_span_independent_image
  5.1063 +  and linear_inj_on_span_iff_independent_image = lt_linear_inj_on_span_iff_independent_image
  5.1064 +  and linear_subspace_linear_preimage = lt_linear_subspace_linear_preimage
  5.1065 +  and linear_spans_image = lt_linear_spans_image
  5.1066 +  and linear_spanning_surjective_image = lt_linear_spanning_surjective_image
  5.1067 +  and linear_eq_on_span = lt_linear_eq_on_span
  5.1068 +  and linear_compose_scale_right = lt_linear_compose_scale_right
  5.1069 +  and linear_compose_add = lt_linear_compose_add
  5.1070 +  and linear_zero = lt_linear_zero
  5.1071 +  and linear_compose_sub = lt_linear_compose_sub
  5.1072 +  and linear_compose_neg = lt_linear_compose_neg
  5.1073 +  and linear_compose_scale = lt_linear_compose_scale
  5.1074 +  and linear_indep_image_lemma = lt_linear_indep_image_lemma
  5.1075 +  and linear_eq_on = lt_linear_eq_on
  5.1076 +  and linear_compose_sum = lt_linear_compose_sum
  5.1077 +  and linear_independent_extend_subspace = lt_linear_independent_extend_subspace
  5.1078 +  and linear_independent_extend = lt_linear_independent_extend
  5.1079 +  and linear_exists_left_inverse_on = lt_linear_exists_left_inverse_on
  5.1080 +  and linear_exists_right_inverse_on = lt_linear_exists_right_inverse_on
  5.1081 +  and linear_inj_on_left_inverse = lt_linear_inj_on_left_inverse
  5.1082 +  and linear_injective_left_inverse = lt_linear_injective_left_inverse
  5.1083 +  and linear_surj_right_inverse = lt_linear_surj_right_inverse
  5.1084 +  and linear_surjective_right_inverse = lt_linear_surjective_right_inverse
  5.1085 +
  5.1086 +end
  5.1087 +
  5.1088 +context finite_dimensional_vector_space_pair_on begin
  5.1089 +
  5.1090 +context includes lifting_syntax
  5.1091 +  notes [transfer_rule del] = Collect_transfer
  5.1092 +  assumes
  5.1093 +    "\<exists>(Rep::'s \<Rightarrow> 'b) (Abs::'b \<Rightarrow> 's). type_definition Rep Abs S1"
  5.1094 +    "\<exists>(Rep::'t \<Rightarrow> 'c) (Abs::'c \<Rightarrow> 't). type_definition Rep Abs S2" begin
  5.1095 +
  5.1096 +interpretation local_typedef_finite_dimensional_vector_space_pair S1 scale1 Basis1 "TYPE('s)" S2 scale2 Basis2 "TYPE('t)" by unfold_locales fact+
  5.1097 +
  5.1098 +lemmas_with [var_simplified explicit_ab_group_add,
  5.1099 +    unoverload_type 'e 'b,
  5.1100 +  OF lt2.type.ab_group_add_axioms lt1.type.ab_group_add_axioms type_finite_dimensional_vector_space_pair_on_with,
  5.1101 +  folded lt1.dim_S_def lt2.dim_S_def,
  5.1102 +  untransferred,
  5.1103 +  var_simplified implicit_ab_group_add]:
  5.1104 +lt_linear_surjective_imp_injective = finite_dimensional_vector_space_pair.linear_surjective_imp_injective
  5.1105 +and lt_linear_injective_imp_surjective = finite_dimensional_vector_space_pair.linear_injective_imp_surjective
  5.1106 +and lt_linear_injective_isomorphism = finite_dimensional_vector_space_pair.linear_injective_isomorphism
  5.1107 +and lt_linear_surjective_isomorphism = finite_dimensional_vector_space_pair.linear_surjective_isomorphism
  5.1108 +and lt_dim_image_eq = finite_dimensional_vector_space_pair.dim_image_eq
  5.1109 +and lt_basis_to_basis_subspace_isomorphism = finite_dimensional_vector_space_pair.basis_to_basis_subspace_isomorphism
  5.1110 +and lt_dim_image_le = finite_dimensional_vector_space_pair.dim_image_le
  5.1111 +and lt_subspace_isomorphism = finite_dimensional_vector_space_pair.subspace_isomorphism
  5.1112 +
  5.1113 +end
  5.1114 +
  5.1115 +lemmas_with [cancel_type_definition, OF vs1.S_ne,
  5.1116 +    cancel_type_definition, OF vs2.S_ne,
  5.1117 +    folded subset_iff' top_set_def,
  5.1118 +    simplified pred_fun_def,
  5.1119 +    simplified\<comment>\<open>too much?\<close>]:
  5.1120 +linear_surjective_imp_injective = lt_linear_surjective_imp_injective
  5.1121 +and linear_injective_imp_surjective = lt_linear_injective_imp_surjective
  5.1122 +and linear_injective_isomorphism = lt_linear_injective_isomorphism
  5.1123 +and linear_surjective_isomorphism = lt_linear_surjective_isomorphism
  5.1124 +and dim_image_eq = lt_dim_image_eq
  5.1125 +and basis_to_basis_subspace_isomorphism = lt_basis_to_basis_subspace_isomorphism
  5.1126 +and dim_image_le = lt_dim_image_le
  5.1127 +and subspace_isomorphism = lt_subspace_isomorphism
  5.1128 +
  5.1129 +end
  5.1130 +
  5.1131 +end
  5.1132 \ No newline at end of file
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy	Wed Jun 27 11:16:43 2018 +0200
     6.3 @@ -0,0 +1,304 @@
     6.4 +(*  Title:      HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy
     6.5 +    Author:     Fabian Immler, TU München
     6.6 +*)
     6.7 +theory Linear_Algebra_On_With
     6.8 +  imports
     6.9 +    Group_On_With
    6.10 +    Complex_Main
    6.11 +begin
    6.12 +
    6.13 +definition span_with
    6.14 +  where "span_with pls zero scl b =
    6.15 +    {sum_with pls zero (\<lambda>a. scl (r a) a) t | t r. finite t \<and> t \<subseteq> b}"
    6.16 +
    6.17 +lemma span_with_transfer[transfer_rule]:
    6.18 +  includes lifting_syntax
    6.19 +  assumes [transfer_rule]: "right_total A" "bi_unique A"
    6.20 +  shows "((A ===> A ===> A) ===> A ===> ((=) ===> A ===> A) ===> rel_set A ===> rel_set A)
    6.21 +    span_with span_with"
    6.22 +  unfolding span_with_def
    6.23 +proof (intro rel_funI)
    6.24 +  fix p p' z z' X X' and s s'::"'c \<Rightarrow> _"
    6.25 +  assume transfer_rules[transfer_rule]: "(A ===> A ===> A) p p'" "A z z'" "((=) ===> A ===> A) s s'" "rel_set A X X'"
    6.26 +  have "Domainp A z" using \<open>A z z'\<close> by force
    6.27 +  have *: "t \<subseteq> X \<Longrightarrow> (\<forall>x\<in>t. Domainp A x)" for t
    6.28 +    by (meson Domainp.DomainI \<open>rel_set A X X'\<close> rel_setD1 set_mp)
    6.29 +  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)]
    6.30 +  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
    6.31 +  proof cases
    6.32 +    assume ex: "\<exists>C. r ` t \<subseteq> C \<and> comm_monoid_add_on_with C p z"
    6.33 +    have "Domainp (rel_set A) t" using that by (auto simp: Domainp_set)
    6.34 +    from ex_comm_monoid_add_around_imageE[OF ex transfer_rules(1,2) this that(1)]
    6.35 +    obtain C where C: "comm_monoid_add_on_with C p z" "r ` t \<subseteq> C" "Domainp (rel_set A) C" by auto
    6.36 +    from sum_with_mem[OF C(1,2)] C(3)
    6.37 +    show ?thesis
    6.38 +      by auto (meson C(3) Domainp_set)
    6.39 +  qed (use \<open>A z _\<close> in \<open>auto simp: sum_with_def\<close>)
    6.40 +  from Domainp_apply2I[OF transfer_rules(3)]
    6.41 +  have Domainp_sI: "Domainp A x \<Longrightarrow> Domainp A (s y x)" for x y by auto
    6.42 +  show "rel_set A
    6.43 +    {sum_with p z (\<lambda>a. s (r a) a) t |t r. finite t \<and> t \<subseteq> X}
    6.44 +        {sum_with p' z' (\<lambda>a. s' (r a) a) t |t r. finite t \<and> t \<subseteq> X'}"
    6.45 +    apply (transfer_prover_start, transfer_step+)
    6.46 +    using *
    6.47 +    by (auto simp: intro!: DsI Domainp_sI)
    6.48 +qed
    6.49 +
    6.50 +definition dependent_with
    6.51 +  where "dependent_with pls zero scl s =
    6.52 +    (\<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)))"
    6.53 +
    6.54 +lemma dependent_with_transfer[transfer_rule]:
    6.55 +  includes lifting_syntax
    6.56 +  assumes [transfer_rule]: "right_total A" "bi_unique A"
    6.57 +  shows "((A ===> A ===> A) ===> A ===> ((=) ===> A ===> A) ===> rel_set A ===> (=))
    6.58 +    dependent_with dependent_with"
    6.59 +  unfolding dependent_with_def dependent_with_def
    6.60 +proof (intro rel_funI)
    6.61 +  fix p p' z z' X X' and s s'::"'c \<Rightarrow> _"
    6.62 +  assume [transfer_rule]: "(A ===> A ===> A) p p'" "A z z'" "((=) ===> A ===> A) s s'" "rel_set A X X'"
    6.63 +  have *: "t \<subseteq> X \<Longrightarrow> (\<forall>x\<in>t. Domainp A x)" for t
    6.64 +    by (meson Domainp.DomainI \<open>rel_set A X X'\<close> rel_setD1 set_mp)
    6.65 +  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)) =
    6.66 +    (\<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))"
    6.67 +    apply (transfer_prover_start, transfer_step+)
    6.68 +    using *
    6.69 +    by (auto simp: intro!: sum_with_mem)
    6.70 +qed
    6.71 +
    6.72 +definition subspace_with
    6.73 +  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)"
    6.74 +
    6.75 +lemma subspace_with_transfer[transfer_rule]:
    6.76 +  includes lifting_syntax
    6.77 +  assumes [transfer_rule]: "bi_unique A"
    6.78 +  shows "((A ===> A ===> A) ===> A ===> ((=) ===> A ===> A) ===> rel_set A ===> (=))
    6.79 +    subspace_with subspace_with"
    6.80 +  unfolding span_with_def subspace_with_def
    6.81 +  by transfer_prover
    6.82 +
    6.83 +definition "module_on_with S pls mns um zero (scl::'a::comm_ring_1\<Rightarrow>_) \<longleftrightarrow>
    6.84 +  ab_group_add_on_with S pls zero mns um \<and>
    6.85 +        ((\<forall>a. \<forall>x\<in>S.
    6.86 +                 \<forall>y\<in>S. scl a (pls x y) = pls (scl a x) (scl a y)) \<and>
    6.87 +         (\<forall>a b. \<forall>x\<in>S. scl (a + b) x = pls (scl a x) (scl b x))) \<and>
    6.88 +        (\<forall>a b. \<forall>x\<in>S. scl a (scl b x) = scl (a * b) x) \<and>
    6.89 +        (\<forall>x\<in>S. scl 1 x = x) \<and>
    6.90 +        (\<forall>a. \<forall>x\<in>S. scl a x \<in> S)"
    6.91 +
    6.92 +definition "vector_space_on_with S pls mns um zero (scl::'a::field\<Rightarrow>_) \<longleftrightarrow>
    6.93 +  module_on_with S pls mns um zero scl"
    6.94 +
    6.95 +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>
    6.96 +  module_on_with S pls mns um zero scl \<and> module_on_with S' pls' mns' um' zero' scl'"
    6.97 +
    6.98 +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>
    6.99 +  module_pair_on_with S S' pls mns um zero scl pls' mns' um' zero' scl'"
   6.100 +
   6.101 +definition "module_hom_on_with S1 S2 plus1 minus1 uminus1 zero1 (scale1::'a::comm_ring_1\<Rightarrow>_)
   6.102 +  plus2 minus2 uminus2 zero2 (scale2::'a::comm_ring_1\<Rightarrow>_) f \<longleftrightarrow>
   6.103 +        module_pair_on_with S1 S2 plus1 minus1 uminus1 zero1 scale1
   6.104 +         plus2 minus2 uminus2 zero2 scale2 \<and>
   6.105 +        (\<forall>x\<in>S1. \<forall>y\<in>S1. f (plus1 x y) = plus2 (f x) (f y)) \<and>
   6.106 +        (\<forall>s. \<forall>x\<in>S1. f (scale1 s x) = scale2 s (f x))"
   6.107 +
   6.108 +definition "linear_on_with S1 S2 plus1 minus1 uminus1 zero1 (scale1::'a::field\<Rightarrow>_)
   6.109 +  plus2 minus2 uminus2 zero2 (scale2::'a::field\<Rightarrow>_) f \<longleftrightarrow>
   6.110 +  module_hom_on_with S1 S2 plus1 minus1 uminus1 zero1 scale1
   6.111 +  plus2 minus2 uminus2 zero2 scale2 f"
   6.112 +
   6.113 +definition dim_on_with
   6.114 +  where "dim_on_with S pls zero scale V =
   6.115 +    (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
   6.116 +      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)
   6.117 +      else 0)"
   6.118 +
   6.119 +definition "finite_dimensional_vector_space_on_with S pls mns um zero (scl::'a::field\<Rightarrow>_) basis \<longleftrightarrow>
   6.120 +  vector_space_on_with S pls mns um zero scl \<and>
   6.121 +    finite basis \<and>
   6.122 +    \<not> dependent_with pls zero scl basis \<and>
   6.123 +    span_with pls zero scl basis = S"
   6.124 +
   6.125 +definition "finite_dimensional_vector_space_pair_on_with S S' pls mns um zero (scl::'a::field\<Rightarrow>_) b
   6.126 +  pls' mns' um' zero' (scl'::'a::field\<Rightarrow>_) b' \<longleftrightarrow>
   6.127 +  finite_dimensional_vector_space_on_with S pls mns um zero (scl::'a::field\<Rightarrow>_) b \<and>
   6.128 +  finite_dimensional_vector_space_on_with S' pls' mns' um' zero' (scl'::'a::field\<Rightarrow>_) b'"
   6.129 +
   6.130 +context module begin
   6.131 +
   6.132 +lemma span_with:
   6.133 +  "span = (\<lambda>X. span_with (+) 0 scale X)"
   6.134 +  unfolding span_explicit span_with_def sum_with ..
   6.135 +
   6.136 +lemma dependent_with:
   6.137 +  "dependent = (\<lambda>X. dependent_with (+) 0 scale X)"
   6.138 +  unfolding dependent_explicit dependent_with_def sum_with ..
   6.139 +
   6.140 +lemma subspace_with:
   6.141 +  "subspace = (\<lambda>X. subspace_with (+) 0 scale X)"
   6.142 +  unfolding subspace_def subspace_with_def ..
   6.143 +
   6.144 +end
   6.145 +
   6.146 +lemmas [explicit_ab_group_add] = module.span_with module.dependent_with module.subspace_with
   6.147 +
   6.148 +lemma module_on_with_transfer[transfer_rule]:
   6.149 +  includes lifting_syntax
   6.150 +  assumes [transfer_rule]: "right_total A" "bi_unique A"
   6.151 +  shows
   6.152 +    "(rel_set A ===> (A ===> A ===> A) ===> (A ===> A ===> A) ===> (A ===> A) ===> A ===> ((=) ===> A ===> A) ===> (=))
   6.153 +      module_on_with module_on_with"
   6.154 +  unfolding module_on_with_def
   6.155 +  by transfer_prover
   6.156 +
   6.157 +lemma vector_space_on_with_transfer[transfer_rule]:
   6.158 +  includes lifting_syntax
   6.159 +  assumes [transfer_rule]: "right_total A" "bi_unique A"
   6.160 +  shows
   6.161 +    "(rel_set A ===> (A ===> A ===> A) ===> (A ===> A ===> A) ===> (A ===> A) ===> A ===> ((=) ===> A ===> A) ===> (=))
   6.162 +      vector_space_on_with vector_space_on_with"
   6.163 +  unfolding vector_space_on_with_def
   6.164 +  by transfer_prover
   6.165 +
   6.166 +context vector_space begin
   6.167 +
   6.168 +lemma dim_with: "dim = (\<lambda>X. dim_on_with UNIV (+) 0 scale X)"
   6.169 +  unfolding dim_def dim_on_with_def dependent_with span_with by force
   6.170 +
   6.171 +end
   6.172 +
   6.173 +lemmas [explicit_ab_group_add] = vector_space.dim_with
   6.174 +
   6.175 +lemma module_pair_on_with_transfer[transfer_rule]:
   6.176 +  includes lifting_syntax
   6.177 +  assumes [transfer_rule]: "right_total A" "bi_unique A" "right_total C" "bi_unique C"
   6.178 +  shows
   6.179 +    "(rel_set A ===> rel_set C ===>
   6.180 +    (A ===> A ===> A) ===> (A ===> A ===> A) ===> (A ===> A) ===> A ===> ((=) ===> A ===> A) ===>
   6.181 +    (C ===> C ===> C) ===> (C ===> C ===> C) ===> (C ===> C) ===> C ===> ((=) ===> C ===> C) ===>
   6.182 +    (=)) module_pair_on_with module_pair_on_with"
   6.183 +  unfolding module_pair_on_with_def
   6.184 +  by transfer_prover
   6.185 +
   6.186 +lemma module_hom_on_with_transfer[transfer_rule]:
   6.187 +  includes lifting_syntax
   6.188 +  assumes [transfer_rule]: "right_total A" "bi_unique A" "right_total C" "bi_unique C"
   6.189 +  shows
   6.190 +    "(rel_set A ===> rel_set C ===>
   6.191 +    (A ===> A ===> A) ===> (A ===> A ===> A) ===> (A ===> A) ===> A ===> ((=) ===> A ===> A) ===>
   6.192 +    (C ===> C ===> C) ===> (C ===> C ===> C) ===> (C ===> C) ===> C ===> ((=) ===> C ===> C) ===>
   6.193 +    (A ===> C) ===> (=)) module_hom_on_with module_hom_on_with"
   6.194 +  unfolding module_hom_on_with_def
   6.195 +  by transfer_prover
   6.196 +
   6.197 +lemma linear_on_with_transfer[transfer_rule]:
   6.198 +  includes lifting_syntax
   6.199 +  assumes [transfer_rule]: "right_total A" "bi_unique A" "right_total C" "bi_unique C"
   6.200 +  shows
   6.201 +    "(rel_set A ===> rel_set C ===>
   6.202 +    (A ===> A ===> A) ===> (A ===> A ===> A) ===> (A ===> A) ===> A ===> ((=) ===> A ===> A) ===>
   6.203 +    (C ===> C ===> C) ===> (C ===> C ===> C) ===> (C ===> C) ===> C ===> ((=) ===> C ===> C) ===>
   6.204 +    (A ===> C) ===> (=)) linear_on_with linear_on_with"
   6.205 +  unfolding linear_on_with_def
   6.206 +  by transfer_prover
   6.207 +
   6.208 +subsubsection \<open>Explicit locale formulations\<close>
   6.209 +
   6.210 +lemma module_on_with[explicit_ab_group_add]: "module s \<longleftrightarrow> module_on_with UNIV (+) (-) uminus 0 s"
   6.211 +  and vector_space_on_with[explicit_ab_group_add]: "vector_space t \<longleftrightarrow> vector_space_on_with UNIV (+) (-) uminus 0 t"
   6.212 +  by (auto simp: module_def module_on_with_def ab_group_add_axioms
   6.213 +      vector_space_def vector_space_on_with_def)
   6.214 +
   6.215 +lemma vector_space_with_imp_module_with[explicit_ab_group_add]:
   6.216 +  "vector_space_on_with S (+) (-) uminus 0 s \<Longrightarrow> module_on_with S (+) (-) uminus 0 s"
   6.217 +  by (simp add: vector_space_on_with_def)
   6.218 +
   6.219 +lemma finite_dimensional_vector_space_on_with[explicit_ab_group_add]:
   6.220 +    "finite_dimensional_vector_space t b \<longleftrightarrow> finite_dimensional_vector_space_on_with UNIV (+) (-) uminus 0 t b"
   6.221 +  by (auto simp: finite_dimensional_vector_space_on_with_def finite_dimensional_vector_space_def
   6.222 +    finite_dimensional_vector_space_axioms_def explicit_ab_group_add)
   6.223 +
   6.224 +lemma vector_space_with_imp_finite_dimensional_vector_space_with[explicit_ab_group_add]:
   6.225 +  "finite_dimensional_vector_space_on_with S (+) (-) uminus 0 s basis \<Longrightarrow>
   6.226 +  vector_space_on_with S  (+) (-) uminus 0 s"
   6.227 +  by (auto simp: finite_dimensional_vector_space_on_with_def)
   6.228 +
   6.229 +lemma module_hom_on_with[explicit_ab_group_add]:
   6.230 +  "module_hom s1 s2 f \<longleftrightarrow> module_hom_on_with UNIV UNIV (+) (-) uminus 0 s1 (+) (-) uminus 0 s2 f"
   6.231 +  and linear_with[explicit_ab_group_add]:
   6.232 +  "Vector_Spaces.linear t1 t2 f \<longleftrightarrow> linear_on_with UNIV UNIV (+) (-) uminus 0 t1 (+) (-) uminus 0 t2 f"
   6.233 +  and module_pair_on_with[explicit_ab_group_add]:
   6.234 +  "module_pair s1 s2 \<longleftrightarrow> module_pair_on_with UNIV UNIV (+) (-) uminus 0 s1 (+) (-) uminus 0 s2"
   6.235 +  by (auto simp: module_hom_def module_hom_on_with_def module_pair_on_with_def
   6.236 +      Vector_Spaces.linear_def linear_on_with_def vector_space_on_with
   6.237 +      module_on_with_def vector_space_on_with_def
   6.238 +      module_hom_axioms_def module_pair_def module_on_with)
   6.239 +
   6.240 +lemma vector_space_pair_with[explicit_ab_group_add]:
   6.241 +  "vector_space_pair s1 s2 \<longleftrightarrow> vector_space_pair_on_with UNIV UNIV (+) (-) uminus 0 s1  (+) (-) uminus 0 s2"
   6.242 +  by (auto simp: module_pair_on_with_def explicit_ab_group_add
   6.243 +      vector_space_pair_on_with_def vector_space_pair_def module_on_with_def vector_space_on_with_def)
   6.244 +
   6.245 +lemma finite_dimensional_vector_space_pair_with[explicit_ab_group_add]:
   6.246 +  "finite_dimensional_vector_space_pair s1 b1 s2 b2 \<longleftrightarrow>
   6.247 +    finite_dimensional_vector_space_pair_on_with UNIV UNIV (+) (-) uminus 0 s1 b1 (+) (-) uminus 0 s2 b2"
   6.248 +  by (auto simp: finite_dimensional_vector_space_pair_def
   6.249 +      finite_dimensional_vector_space_pair_on_with_def finite_dimensional_vector_space_on_with)
   6.250 +
   6.251 +
   6.252 +lemma module_pair_with_imp_module_with[explicit_ab_group_add]:
   6.253 +  "module_on_with S (+) (-) uminus 0 s"
   6.254 +  "module_on_with T (+) (-) uminus 0 t"
   6.255 +  if "module_pair_on_with S T (+) (-) uminus 0 s (+) (-) uminus 0 t"
   6.256 +  using that
   6.257 +  unfolding module_pair_on_with_def
   6.258 +  by simp_all
   6.259 +
   6.260 +lemma vector_space_pair_with_imp_vector_space_with[explicit_ab_group_add]:
   6.261 +  "vector_space_on_with S (+) (-) uminus 0 s"
   6.262 +  "vector_space_on_with T (+) (-) uminus 0 t"
   6.263 +  if "vector_space_pair_on_with S T(+) (-) uminus 0 s (+) (-) uminus 0 t"
   6.264 +  using that
   6.265 +  by (auto simp: vector_space_pair_on_with_def module_pair_on_with_def vector_space_on_with_def)
   6.266 +
   6.267 +lemma finite_dimensional_vector_space_pair_with_imp_finite_dimensional_vector_space_with[explicit_ab_group_add]:
   6.268 +  "finite_dimensional_vector_space_on_with S (+) (-) uminus 0 s b"
   6.269 +  "finite_dimensional_vector_space_on_with T (+) (-) uminus 0 t c"
   6.270 +  if "finite_dimensional_vector_space_pair_on_with S T (+) (-) uminus 0 s b (+) (-) uminus 0 t c"
   6.271 +  using that
   6.272 +  unfolding finite_dimensional_vector_space_pair_on_with_def
   6.273 +  by simp_all
   6.274 +
   6.275 +lemma finite_dimensional_vector_space_pair_with_imp_vector_space_with[explicit_ab_group_add]:
   6.276 +  \<comment>\<open>this rule is strange: why is it needed, but not the one with \<open>module_with\<close> as conclusions?\<close>
   6.277 +  "vector_space_on_with S (+) (-) uminus 0 s"
   6.278 +  "vector_space_on_with T (+) (-) uminus 0 t"
   6.279 +  if "finite_dimensional_vector_space_pair_on_with S T (+) (-) uminus 0 s b (+) (-) uminus 0 t c"
   6.280 +  using that
   6.281 +  by (auto simp: finite_dimensional_vector_space_pair_on_with_def finite_dimensional_vector_space_on_with_def)
   6.282 +
   6.283 +lemma finite_dimensional_vector_space_on_with_transfer[transfer_rule]:
   6.284 +  includes lifting_syntax
   6.285 +  assumes [transfer_rule]: "right_total A" "bi_unique A"
   6.286 +  shows
   6.287 +    "(rel_set A ===>
   6.288 +    (A ===> A ===> A) ===> (A ===> A ===> A) ===> (A ===> A) ===> A ===> ((=) ===> A ===> A) ===>
   6.289 +    rel_set A ===>
   6.290 +    (=)) (finite_dimensional_vector_space_on_with) finite_dimensional_vector_space_on_with"
   6.291 +  unfolding finite_dimensional_vector_space_on_with_def
   6.292 +  by transfer_prover
   6.293 +
   6.294 +lemma finite_dimensional_vector_space_pair_on_with_transfer[transfer_rule]:
   6.295 +  includes lifting_syntax
   6.296 +  assumes [transfer_rule]: "right_total A" "bi_unique A" "right_total C" "bi_unique C"
   6.297 +  shows
   6.298 +    "(rel_set A ===> rel_set C ===>
   6.299 +    (A ===> A ===> A) ===> (A ===> A ===> A) ===> (A ===> A) ===> A ===> ((=) ===> A ===> A) ===>
   6.300 +    rel_set A ===>
   6.301 +    (C ===> C ===> C) ===> (C ===> C ===> C) ===> (C ===> C) ===> C ===> ((=) ===> C ===> C) ===>
   6.302 +    rel_set C ===>
   6.303 +    (=)) (finite_dimensional_vector_space_pair_on_with) finite_dimensional_vector_space_pair_on_with"
   6.304 +  unfolding finite_dimensional_vector_space_pair_on_with_def
   6.305 +  by transfer_prover
   6.306 +
   6.307 +end
   6.308 \ No newline at end of file