# HG changeset patch
# User immler
# Date 1542223050 18000
# Node ID 4cf8a0432650557ae6ad7fd77c3897cbe7faee2e
# Parent  bc0b0d46599138110f11c1ed8d196552c8f90aff
extract example for ab_group_add_on_with

diff -r bc0b0d465991 -r 4cf8a0432650 src/HOL/Types_To_Sets/Examples/Group_On_With.thy
--- a/src/HOL/Types_To_Sets/Examples/Group_On_With.thy	Wed Nov 14 13:45:09 2018 -0500
+++ b/src/HOL/Types_To_Sets/Examples/Group_On_With.thy	Wed Nov 14 14:17:30 2018 -0500
@@ -4,6 +4,7 @@
 theory Group_On_With
 imports
   Prerequisites
+  Types_To_Sets
 begin
 
 subsection \<open>\<^emph>\<open>on\<close> carrier set \<^emph>\<open>with\<close> explicit group operations\<close>
@@ -13,10 +14,168 @@
   assumes add_assoc: "a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> c \<in> S \<Longrightarrow> pls (pls a b) c = pls a (pls b c)"
   assumes add_mem: "a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> pls a b \<in> S"
 
+locale ab_semigroup_add_on_with = semigroup_add_on_with +
+  assumes add_commute: "a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> pls a b = pls b a"
+
+locale comm_monoid_add_on_with = ab_semigroup_add_on_with +
+  fixes z
+  assumes add_zero: "a \<in> S \<Longrightarrow> pls z a = a"
+  assumes zero_mem: "z \<in> S"
+begin
+
+lemma carrier_ne: "S \<noteq> {}" using zero_mem by auto
+
+end
+
+definition "sum_with pls z f S =
+  (if \<exists>C. f ` S \<subseteq> C \<and> comm_monoid_add_on_with C pls z then
+    Finite_Set.fold (pls o f) z S else z)"
+
+lemma sum_with_empty[simp]: "sum_with pls z f {} = z"
+  by (auto simp: sum_with_def)
+
+lemma sum_with_cases[case_names comm zero]:
+  "P (sum_with pls z f S)"
+  if "\<And>C. f ` S \<subseteq> C \<Longrightarrow> comm_monoid_add_on_with C pls z \<Longrightarrow> P (Finite_Set.fold (pls o f) z S)"
+    "(\<And>C. comm_monoid_add_on_with C pls z \<Longrightarrow> (\<exists>s\<in>S. f s \<notin> C)) \<Longrightarrow> P z"
+  using that
+  by (auto simp: sum_with_def)
+
+context comm_monoid_add_on_with begin
+
+lemma sum_with_infinite: "infinite A \<Longrightarrow> sum_with pls z g A = z"
+  by (induction rule: sum_with_cases) auto
+
+context begin
+
+private abbreviation "pls' \<equiv> \<lambda>x y. pls (if x \<in> S then x else z) (if y \<in> S then y else z)"
+
+lemma fold_pls'_mem: "Finite_Set.fold (pls' \<circ> g) z A \<in> S"
+  if "g ` A \<subseteq> S"
+proof cases
+  assume A: "finite A"
+  interpret comp_fun_commute "pls' o g"
+    using that
+    using add_assoc add_commute add_mem zero_mem
+    by unfold_locales auto
+  from fold_graph_fold[OF A] have "fold_graph (pls' \<circ> g) z A (Finite_Set.fold (pls' \<circ> g) z A)" .
+  from fold_graph_closed_lemma[OF this, of S "pls' \<circ> g"]
+    add_assoc add_commute add_mem zero_mem
+  show ?thesis
+    by auto
+qed (use add_assoc add_commute add_mem zero_mem in simp)
+
+lemma fold_pls'_eq: "Finite_Set.fold (pls' \<circ> g) z A = Finite_Set.fold (pls \<circ> g) z A"
+  if "g ` A \<subseteq> S"
+  using add_assoc add_commute add_mem zero_mem that
+  by (intro fold_closed_eq[where B=S]) auto
+
+lemma sum_with_mem: "sum_with pls z g A \<in> S" if "g ` A \<subseteq> S"
+proof -
+  interpret comp_fun_commute "pls' o g"
+    using add_assoc add_commute add_mem zero_mem that
+    by unfold_locales auto
+  have "\<exists>C. g ` A \<subseteq> C \<and> comm_monoid_add_on_with C pls z"
+    using that comm_monoid_add_on_with_axioms by auto
+  then show ?thesis
+    using fold_pls'_mem[OF that]
+    by (simp add: sum_with_def fold_pls'_eq that)
+qed
+
+lemma sum_with_insert:
+  "sum_with pls z g (insert x A) = pls (g x) (sum_with pls z g A)"
+  if g_into: "g x \<in> S" "g ` A \<subseteq> S"
+    and A: "finite A" and x: "x \<notin> A"
+proof -
+  interpret comp_fun_commute "pls' o g"
+    using add_assoc add_commute add_mem zero_mem g_into
+    by unfold_locales auto
+  have "Finite_Set.fold (pls \<circ> g) z (insert x A) = Finite_Set.fold (pls' \<circ> g) z (insert x A)"
+    using g_into
+    by (subst fold_pls'_eq) auto
+  also have "\<dots> = pls' (g x) (Finite_Set.fold (pls' \<circ> g) z A)"
+    unfolding fold_insert[OF A x]
+    by (auto simp: o_def)
+  also have "\<dots> = pls (g x) (Finite_Set.fold (pls' \<circ> g) z A)"
+  proof -
+    from fold_graph_fold[OF A] have "fold_graph (pls' \<circ> g) z A (Finite_Set.fold (pls' \<circ> g) z A)" .
+    from fold_graph_closed_lemma[OF this, of S "pls' \<circ> g"] add_assoc add_commute add_mem zero_mem
+    have "Finite_Set.fold (pls' \<circ> g) z A \<in> S"
+      by auto
+    then show ?thesis
+      using g_into by auto
+  qed
+  also have "Finite_Set.fold (pls' \<circ> g) z A = Finite_Set.fold (pls \<circ> g) z A"
+    using g_into
+    by (subst fold_pls'_eq) auto
+  finally
+  have "Finite_Set.fold (pls \<circ> g) z (insert x A) = pls (g x) (Finite_Set.fold (pls \<circ> g) z A)" .
+  moreover
+  have "\<exists>C. g ` insert x A \<subseteq> C \<and> comm_monoid_add_on_with C pls z"
+    "\<exists>C. g ` A \<subseteq> C \<and> comm_monoid_add_on_with C pls z"
+    using that (1,2) comm_monoid_add_on_with_axioms by auto
+  ultimately show ?thesis
+    by (simp add: sum_with_def)
+qed
+
+end
+
+end
+
+locale ab_group_add_on_with = comm_monoid_add_on_with +
+  fixes mns um
+  assumes ab_left_minus: "a \<in> S \<Longrightarrow> pls (um a) a = z"
+  assumes ab_diff_conv_add_uminus: "a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> mns a b = pls a (um b)"
+  assumes uminus_mem: "a \<in> S \<Longrightarrow> um a \<in> S"
+
+
+subsection \<open>obvious instances (by type class constraints)\<close>
+
+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 semigroup_add_on_with_Ball_def: "semigroup_add_on_with S pls \<longleftrightarrow>
   (\<forall>a\<in>S. \<forall>b\<in>S. \<forall>c\<in>S. pls (pls a b) c = pls a (pls b c)) \<and> (\<forall>a\<in>S. \<forall>b\<in>S. pls a b \<in> S)"
   by (auto simp: semigroup_add_on_with_def)
 
+lemma ab_semigroup_add_on_with_Ball_def:
+  "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)"
+  by (auto simp: ab_semigroup_add_on_with_def ab_semigroup_add_on_with_axioms_def)
+
+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_Ball_def ac_simps)
+
+lemma comm_monoid_add_on_with_Ball_def:
+  "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"
+  by (auto simp: comm_monoid_add_on_with_def comm_monoid_add_on_with_axioms_def)
+
+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_Ball_def ab_semigroup_add_on_with_Ball_def
+      semigroup_add_on_with_Ball_def ac_simps)
+
+lemma ab_group_add_on_with_Ball_def:
+  "ab_group_add_on_with S pls z mns um \<longleftrightarrow> comm_monoid_add_on_with S pls z \<and>
+    (\<forall>a\<in>S. pls (um a) a = z) \<and> (\<forall>a\<in>S. \<forall>b\<in>S. mns a b = pls a (um b)) \<and> (\<forall>a\<in>S. um a \<in> S)"
+  by (auto simp: ab_group_add_on_with_def ab_group_add_on_with_axioms_def)
+
+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_Ball_def)
+
+lemma sum_with: "sum f S = sum_with (+) 0 f S"
+proof (induction rule: sum_with_cases)
+  case (comm C)
+  then show ?case
+    unfolding sum.eq_fold
+    by simp
+next
+  case zero
+  from zero[OF comm_monoid_add_on_with]
+  show ?case by simp
+qed
+
+
+subsection \<open>transfer rules\<close>
+
 lemma semigroup_add_on_with_transfer[transfer_rule]:
   includes lifting_syntax
   assumes [transfer_rule]: "bi_unique A"
@@ -24,9 +183,6 @@
   unfolding semigroup_add_on_with_Ball_def
   by transfer_prover
 
-lemma semigroup_add_on_with[simp]: "semigroup_add_on_with (UNIV::'a::semigroup_add set) (+)"
-  by (auto simp: semigroup_add_on_with_def ac_simps)
-
 lemma Domainp_applyI:
   includes lifting_syntax
   shows "(A ===> B) f g \<Longrightarrow> A x y \<Longrightarrow> Domainp B (f x)"
@@ -48,13 +204,6 @@
     by transfer (auto intro!: Domainp_apply2I[OF xy])
 qed
 
-locale ab_semigroup_add_on_with = semigroup_add_on_with +
-  assumes add_commute: "a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> pls a b = pls b a"
-
-lemma ab_semigroup_add_on_with_Ball_def:
-  "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)"
-  by (auto simp: ab_semigroup_add_on_with_def ab_semigroup_add_on_with_axioms_def)
-
 lemma ab_semigroup_add_on_with_transfer[transfer_rule]:
   includes lifting_syntax
   assumes [transfer_rule]: "bi_unique A"
@@ -70,18 +219,6 @@
   unfolding class.ab_semigroup_add_def class.ab_semigroup_add_axioms_def ab_semigroup_add_on_with_Ball_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_Ball_def ac_simps)
-
-locale comm_monoid_add_on_with = ab_semigroup_add_on_with +
-  fixes z
-  assumes add_zero: "a \<in> S \<Longrightarrow> pls z a = a"
-  assumes zero_mem: "z \<in> S"
-
-lemma comm_monoid_add_on_with_Ball_def:
-  "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"
-  by (auto simp: comm_monoid_add_on_with_def comm_monoid_add_on_with_axioms_def)
-
 lemma comm_monoid_add_on_with_transfer[transfer_rule]:
   includes lifting_syntax
   assumes [transfer_rule]: "bi_unique A"
@@ -106,21 +243,6 @@
     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_Ball_def ab_semigroup_add_on_with_Ball_def
-      semigroup_add_on_with_Ball_def ac_simps)
-
-locale ab_group_add_on_with = comm_monoid_add_on_with +
-  fixes mns um
-  assumes ab_left_minus: "a \<in> S \<Longrightarrow> pls (um a) a = z"
-  assumes ab_diff_conv_add_uminus: "a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> mns a b = pls a (um b)"
-  assumes uminus_mem: "a \<in> S \<Longrightarrow> um a \<in> S"
-
-lemma ab_group_add_on_with_Ball_def:
-  "ab_group_add_on_with S pls z mns um \<longleftrightarrow> comm_monoid_add_on_with S pls z \<and>
-    (\<forall>a\<in>S. pls (um a) a = z) \<and> (\<forall>a\<in>S. \<forall>b\<in>S. mns a b = pls a (um b)) \<and> (\<forall>a\<in>S. um a \<in> S)"
-  by (auto simp: ab_group_add_on_with_def ab_group_add_on_with_axioms_def)
-
 lemma ab_group_add_transfer[transfer_rule]:
   includes lifting_syntax
   assumes [transfer_rule]: "right_total A" "bi_unique A"
@@ -145,118 +267,6 @@
   unfolding class.ab_group_add_def class.ab_group_add_axioms_def ab_group_add_on_with_Ball_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_Ball_def)
-
-definition "sum_with pls z f S =
-  (if \<exists>C. f ` S \<subseteq> C \<and> comm_monoid_add_on_with C pls z then
-    Finite_Set.fold (pls o f) z S else z)"
-
-lemma sum_with_empty[simp]: "sum_with pls z f {} = z"
-  by (auto simp: sum_with_def)
-
-lemma sum_with_cases[case_names comm zero]:
-  "P (sum_with pls z f S)"
-  if "\<And>C. f ` S \<subseteq> C \<Longrightarrow> comm_monoid_add_on_with C pls z \<Longrightarrow> P (Finite_Set.fold (pls o f) z S)"
-    "(\<And>C. comm_monoid_add_on_with C pls z \<Longrightarrow> (\<exists>s\<in>S. f s \<notin> C)) \<Longrightarrow> P z"
-  using that
-  by (auto simp: sum_with_def)
-
-lemma sum_with: "sum f S = sum_with (+) 0 f S"
-proof (induction rule: sum_with_cases)
-  case (comm C)
-  then show ?case
-    unfolding sum.eq_fold
-    by simp
-next
-  case zero
-  from zero[OF comm_monoid_add_on_with]
-  show ?case by simp
-qed
-
-context comm_monoid_add_on_with begin
-
-lemma sum_with_infinite: "infinite A \<Longrightarrow> sum_with pls z g A = z"
-  by (induction rule: sum_with_cases) auto
-
-lemmas comm_monoid_add_unfolded =
-    comm_monoid_add_on_with_axioms[unfolded
-      comm_monoid_add_on_with_Ball_def ab_semigroup_add_on_with_Ball_def semigroup_add_on_with_Ball_def]
-
-context begin
-
-private abbreviation "pls' \<equiv> \<lambda>x y. pls (if x \<in> S then x else z) (if y \<in> S then y else z)"
-
-lemma fold_pls'_mem: "Finite_Set.fold (pls' \<circ> g) z A \<in> S"
-  if "g ` A \<subseteq> S"
-proof cases
-  assume A: "finite A"
-  interpret comp_fun_commute "pls' o g"
-    using comm_monoid_add_unfolded that
-    by unfold_locales auto
-  from fold_graph_fold[OF A] have "fold_graph (pls' \<circ> g) z A (Finite_Set.fold (pls' \<circ> g) z A)" .
-  from fold_graph_closed_lemma[OF this, of S "pls' \<circ> g"] comm_monoid_add_unfolded
-  show ?thesis
-    by auto
-qed (use comm_monoid_add_unfolded in simp)
-
-lemma fold_pls'_eq: "Finite_Set.fold (pls' \<circ> g) z A = Finite_Set.fold (pls \<circ> g) z A"
-  if "g ` A \<subseteq> S"
-  using comm_monoid_add_unfolded that
-  by (intro fold_closed_eq[where B=S]) auto
-
-lemma sum_with_mem: "sum_with pls z g A \<in> S" if "g ` A \<subseteq> S"
-proof -
-  interpret comp_fun_commute "pls' o g"
-    using comm_monoid_add_unfolded that
-    by unfold_locales auto
-  have "\<exists>C. g ` A \<subseteq> C \<and> comm_monoid_add_on_with C pls z"
-    using that comm_monoid_add_on_with_axioms by auto
-  then show ?thesis
-    using fold_pls'_mem[OF that]
-    by (simp add: sum_with_def fold_pls'_eq that)
-qed
-
-lemma sum_with_insert:
-  "sum_with pls z g (insert x A) = pls (g x) (sum_with pls z g A)"
-  if g_into: "g x \<in> S" "g ` A \<subseteq> S"
-    and A: "finite A" and x: "x \<notin> A"
-proof -
-  interpret comp_fun_commute "pls' o g"
-    using comm_monoid_add_unfolded g_into
-    by unfold_locales auto
-  have "Finite_Set.fold (pls \<circ> g) z (insert x A) = Finite_Set.fold (pls' \<circ> g) z (insert x A)"
-    using g_into
-    by (subst fold_pls'_eq) auto
-  also have "\<dots> = pls' (g x) (Finite_Set.fold (pls' \<circ> g) z A)"
-    unfolding fold_insert[OF A x]
-    by (auto simp: o_def)
-  also have "\<dots> = pls (g x) (Finite_Set.fold (pls' \<circ> g) z A)"
-  proof -
-    from fold_graph_fold[OF A] have "fold_graph (pls' \<circ> g) z A (Finite_Set.fold (pls' \<circ> g) z A)" .
-    from fold_graph_closed_lemma[OF this, of S "pls' \<circ> g"] comm_monoid_add_unfolded
-    have "Finite_Set.fold (pls' \<circ> g) z A \<in> S"
-      by auto
-    then show ?thesis
-      using g_into by auto
-  qed
-  also have "Finite_Set.fold (pls' \<circ> g) z A = Finite_Set.fold (pls \<circ> g) z A"
-    using g_into
-    by (subst fold_pls'_eq) auto
-  finally
-  have "Finite_Set.fold (pls \<circ> g) z (insert x A) = pls (g x) (Finite_Set.fold (pls \<circ> g) z A)" .
-  moreover
-  have "\<exists>C. g ` insert x A \<subseteq> C \<and> comm_monoid_add_on_with C pls z"
-    "\<exists>C. g ` A \<subseteq> C \<and> comm_monoid_add_on_with C pls z"
-    using that (1,2) comm_monoid_add_on_with_axioms by auto
-  ultimately show ?thesis
-    by (simp add: sum_with_def)
-qed
-
-end
-
-end
-
 lemma ex_comm_monoid_add_around_imageE:
   includes lifting_syntax
   assumes ex_comm: "\<exists>C. f ` S \<subseteq> C \<and> comm_monoid_add_on_with C pls zero"
@@ -376,10 +386,142 @@
   qed
 qed
 
+
 subsection \<open>Rewrite rules to make \<open>ab_group_add\<close> operations explicit\<close>
 
 named_theorems explicit_ab_group_add
 
 lemmas [explicit_ab_group_add] = sum_with
 
+
+subsection \<open>Locale defining \<open>ab_group_add\<close>-Operations in a local type\<close>
+
+locale local_typedef_ab_group_add_on_with = local_typedef S s +
+  ab_group_add_on_with S
+  for S ::"'b set" and s::"'s itself"
+begin
+
+lemma mem_minus_lt: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> mns x y \<in> S"
+  using ab_diff_conv_add_uminus[of x y] add_mem[of x "um y"] uminus_mem[of y]
+  by auto
+
+context includes lifting_syntax begin
+
+definition plus_S::"'s \<Rightarrow> 's \<Rightarrow> 's" where "plus_S = (rep ---> rep ---> Abs) pls"
+definition minus_S::"'s \<Rightarrow> 's \<Rightarrow> 's" where "minus_S = (rep ---> rep ---> Abs) mns"
+definition uminus_S::"'s \<Rightarrow> 's" where "uminus_S = (rep ---> Abs) um"
+definition zero_S::"'s" where "zero_S = Abs z"
+
+lemma plus_S_transfer[transfer_rule]: "(cr_S ===> cr_S ===> cr_S) pls plus_S"
+  unfolding plus_S_def
+  by (auto simp: cr_S_def add_mem intro!: rel_funI)
+
+lemma minus_S_transfer[transfer_rule]: "(cr_S ===> cr_S ===> cr_S) mns minus_S"
+  unfolding minus_S_def
+  by (auto simp: cr_S_def mem_minus_lt intro!: rel_funI)
+
+lemma uminus_S_transfer[transfer_rule]: "(cr_S ===> cr_S) um uminus_S"
+  unfolding uminus_S_def
+  by (auto simp: cr_S_def uminus_mem intro!: rel_funI)
+
+lemma zero_S_transfer[transfer_rule]: "cr_S z zero_S"
+  unfolding zero_S_def
+  by (auto simp: cr_S_def zero_mem intro!: rel_funI)
+
+end
+
+sublocale type: ab_group_add plus_S "zero_S::'s" minus_S uminus_S
+  apply unfold_locales
+  subgoal by transfer (rule add_assoc)
+  subgoal by transfer (rule add_commute)
+  subgoal by transfer (rule add_zero)
+  subgoal by transfer (rule ab_left_minus)
+  subgoal by transfer (rule ab_diff_conv_add_uminus)
+  done
+
+context includes lifting_syntax begin
+
+lemma sum_transfer[transfer_rule]:
+  "((A===>cr_S) ===> rel_set A ===> cr_S) (sum_with pls z) type.sum"
+  if [transfer_rule]: "bi_unique A"
+proof (safe intro!: rel_funI)
+  fix f g I J
+  assume fg[transfer_rule]: "(A ===> cr_S) f g" and rel_set: "rel_set A I J"
+  show "cr_S (sum_with pls z f I) (type.sum g J)"
+    using rel_set
+  proof (induction I arbitrary: J rule: infinite_finite_induct)
+    case (infinite I)
+    note [transfer_rule] = infinite.prems
+    from infinite.hyps have "infinite J" by transfer
+    with infinite.hyps show ?case
+      by (simp add: zero_S_transfer sum_with_infinite)
+  next
+    case [transfer_rule]: empty
+    have "J = {}" 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 J"
+      by transfer (simp add: insert.hyps)
+    obtain y where [transfer_rule]: "A x y" and y: "y \<in> J"
+      by (meson insert.prems insertI1 rel_setD1)
+    define J' where "J' = J - {y}"
+    have T_def: "J = insert y J'"
+      by (auto simp: J'_def y)
+    define sF where "sF = sum_with pls z f F"
+    define sT where "sT = type.sum g J'"
+    have [simp]: "y \<notin> J'" "finite J'"
+      by (auto simp: y J'_def)
+    have "rel_set A (insert x F - {x}) J'"
+      unfolding J'_def
+      by transfer_prover
+    then have "rel_set A F J'"
+      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 f_S: "f x \<in> S" "f ` F \<subseteq> S"
+      using \<open>A x y\<close> fg insert.prems
+      by (auto simp: rel_fun_def cr_S_def rel_set_def)
+    have "cr_S (pls (f x) sF) (plus_S (g y) sT)" by transfer_prover
+    then have "cr_S (sum_with pls z f (insert x F)) (type.sum g (insert y J'))"
+      by (simp add: sum_with_insert insert.hyps type.sum.insert_remove sF_def[symmetric]
+          sT_def[symmetric] f_S)
+    then show ?case
+      by (simp add: T_def)
+  qed
+qed
+
+end
+
+end
+
+
+subsection \<open>transfer theorems from \<^term>\<open>class.ab_group_add\<close> to \<^term>\<open>ab_group_add_on_with\<close>\<close>
+
+context ab_group_add_on_with begin
+
+context includes lifting_syntax assumes ltd: "\<exists>(Rep::'s \<Rightarrow> 'a) (Abs::'a \<Rightarrow> 's). type_definition Rep Abs S" begin
+
+interpretation local_typedef_ab_group_add_on_with pls z mns um S "TYPE('s)" by unfold_locales fact
+
+text\<open>Get theorem names:\<close>
+print_locale! ab_group_add
+
+lemmas lt_sum_mono_neutral_cong_left = sum.mono_neutral_cong_left
+  [var_simplified explicit_ab_group_add,
+    unoverload_type 'c,
+    OF type.comm_monoid_add_axioms,
+    untransferred]
+
+end
+
+lemmas sum_mono_neutral_cong_left =
+  lt_sum_mono_neutral_cong_left
+    [cancel_type_definition,
+    OF carrier_ne,
+    simplified pred_fun_def, simplified]
+
+end
+
 end
\ No newline at end of file
diff -r bc0b0d465991 -r 4cf8a0432650 src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy
--- a/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy	Wed Nov 14 13:45:09 2018 -0500
+++ b/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy	Wed Nov 14 14:17:30 2018 -0500
@@ -169,106 +169,6 @@
 
 subsection \<open>Local Typedef for Subspace\<close>
 
-locale local_typedef_ab_group_add = local_typedef S s +
-  ab_group_add_on_with S
-  for S ::"'b set" and s::"'s itself"
-begin
-
-lemma mem_minus_lt: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> mns x y \<in> S"
-  using ab_diff_conv_add_uminus[of x y] add_mem[of x "um y"] uminus_mem[of y]
-  by auto
-
-context includes lifting_syntax begin
-
-definition plus_S::"'s \<Rightarrow> 's \<Rightarrow> 's" where "plus_S = (rep ---> rep ---> Abs) pls"
-definition minus_S::"'s \<Rightarrow> 's \<Rightarrow> 's" where "minus_S = (rep ---> rep ---> Abs) mns"
-definition uminus_S::"'s \<Rightarrow> 's" where "uminus_S = (rep ---> Abs) um"
-definition zero_S::"'s" where "zero_S = Abs z"
-
-lemma plus_S_transfer[transfer_rule]: "(cr_S ===> cr_S ===> cr_S) pls plus_S"
-  unfolding plus_S_def
-  by (auto simp: cr_S_def add_mem intro!: rel_funI)
-
-lemma minus_S_transfer[transfer_rule]: "(cr_S ===> cr_S ===> cr_S) mns minus_S"
-  unfolding minus_S_def
-  by (auto simp: cr_S_def mem_minus_lt intro!: rel_funI)
-
-lemma uminus_S_transfer[transfer_rule]: "(cr_S ===> cr_S) um uminus_S"
-  unfolding uminus_S_def
-  by (auto simp: cr_S_def uminus_mem intro!: rel_funI)
-
-lemma zero_S_transfer[transfer_rule]: "cr_S z zero_S"
-  unfolding zero_S_def
-  by (auto simp: cr_S_def zero_mem intro!: rel_funI)
-
-end
-
-sublocale type: ab_group_add plus_S "zero_S::'s" minus_S uminus_S
-  apply unfold_locales
-  subgoal by transfer (rule add_assoc)
-  subgoal by transfer (rule add_commute)
-  subgoal by transfer (rule add_zero)
-  subgoal by transfer (rule ab_left_minus)
-  subgoal by transfer (rule ab_diff_conv_add_uminus)
-  done
-
-context includes lifting_syntax begin
-
-lemma sum_transfer[transfer_rule]:
-  "((A===>cr_S) ===> rel_set A ===> cr_S) (sum_with pls z) type.sum"
-  if [transfer_rule]: "bi_unique A"
-proof (safe intro!: rel_funI)
-  fix f g I J
-  assume fg[transfer_rule]: "(A ===> cr_S) f g" and rel_set: "rel_set A I J"
-  show "cr_S (sum_with pls z f I) (type.sum g J)"
-    using rel_set
-  proof (induction I arbitrary: J rule: infinite_finite_induct)
-    case (infinite I)
-    note [transfer_rule] = infinite.prems
-    from infinite.hyps have "infinite J" by transfer
-    with infinite.hyps show ?case
-      by (simp add: zero_S_transfer sum_with_infinite)
-  next
-    case [transfer_rule]: empty
-    have "J = {}" 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 J"
-      by transfer (simp add: insert.hyps)
-    obtain y where [transfer_rule]: "A x y" and y: "y \<in> J"
-      by (meson insert.prems insertI1 rel_setD1)
-    define J' where "J' = J - {y}"
-    have T_def: "J = insert y J'"
-      by (auto simp: J'_def y)
-    define sF where "sF = sum_with pls z f F"
-    define sT where "sT = type.sum g J'"
-    have [simp]: "y \<notin> J'" "finite J'"
-      by (auto simp: y J'_def)
-    have "rel_set A (insert x F - {x}) J'"
-      unfolding J'_def
-      by transfer_prover
-    then have "rel_set A F J'"
-      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 f_S: "f x \<in> S" "f ` F \<subseteq> S"
-      using \<open>A x y\<close> fg insert.prems
-      by (auto simp: rel_fun_def cr_S_def rel_set_def)
-    have "cr_S (pls (f x) sF) (plus_S (g y) sT)" by transfer_prover
-    then have "cr_S (sum_with pls z f (insert x F)) (type.sum g (insert y J'))"
-      by (simp add: sum_with_insert insert.hyps type.sum.insert_remove sF_def[symmetric]
-          sT_def[symmetric] f_S)
-    then show ?case
-      by (simp add: T_def)
-  qed
-qed
-
-end
-
-end
-
 locale local_typedef_module_on = module_on S scale
   for S and scale::"'a::comm_ring_1\<Rightarrow>'b\<Rightarrow>'b::ab_group_add" and s::"'s itself" +
   assumes Ex_type_definition_S: "\<exists>(Rep::'s \<Rightarrow> 'b) (Abs::'b \<Rightarrow> 's). type_definition Rep Abs S"
@@ -281,7 +181,7 @@
 sublocale local_typedef S "TYPE('s)"
   using Ex_type_definition_S by unfold_locales
 
-sublocale local_typedef_ab_group_add "(+)::'b\<Rightarrow>'b\<Rightarrow>'b" "0::'b" "(-)" uminus S "TYPE('s)"
+sublocale local_typedef_ab_group_add_on_with "(+)::'b\<Rightarrow>'b\<Rightarrow>'b" "0::'b" "(-)" uminus S "TYPE('s)"
   using mem_zero mem_add mem_scale[of _ "-1"]
   by unfold_locales (auto simp: scale_minus_left_on)