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