generalized local_typedef_ab_group_add draft
authorimmler <immler@in.tum.de>
Wed, 14 Nov 2018 13:45:09 -0500
changeset 69302 983ec54f9b60
parent 69301 0fd23badd749
child 69303 98bd0da01e76
generalized local_typedef_ab_group_add
src/HOL/Types_To_Sets/Examples/Group_On_With.thy
src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy
src/HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy
src/HOL/Types_To_Sets/Examples/Prerequisites.thy
--- a/src/HOL/Types_To_Sets/Examples/Group_On_With.thy	Wed Nov 14 01:31:55 2018 +0000
+++ b/src/HOL/Types_To_Sets/Examples/Group_On_With.thy	Wed Nov 14 13:45:09 2018 -0500
@@ -114,20 +114,27 @@
   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))"
+    (\<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"
-  shows
-    "((A ===> A ===> A) ===> A  ===> (A ===> A ===> A) ===> (A ===> 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_Ball_def
-  by transfer_prover
+proof (intro rel_funI)
+  fix p p' z z' m m' um um'
+  assume [transfer_rule]:
+    "(A ===> A ===> A) p p'" "A z z'" "(A ===> A ===> A) m m'"
+    and um[transfer_rule]: "(A ===> A) um um'"
+  show "ab_group_add_on_with (Collect (Domainp A)) p z m um = class.ab_group_add p' z' m' um'"
+    unfolding class.ab_group_add_def class.ab_group_add_axioms_def ab_group_add_on_with_Ball_def
+    by transfer (use um in \<open>auto simp: rel_fun_def\<close>)
+qed
 
 lemma ab_group_add_on_with_transfer[transfer_rule]:
   includes lifting_syntax
@@ -148,48 +155,63 @@
 lemma sum_with_empty[simp]: "sum_with pls z f {} = z"
   by (auto simp: sum_with_def)
 
-lemma sum_with: "sum = sum_with (+) 0"
-proof (intro ext)
-  fix f::"'a\<Rightarrow>'b" and X::"'a set"
-  have ex: "\<exists>C. f ` X \<subseteq> C \<and> comm_monoid_add_on_with C (+) 0"
-    by (auto intro!: exI[where x=UNIV] comm_monoid_add_on_with)
-  then show "sum f X = sum_with (+) 0 f X"
-    unfolding sum.eq_fold sum_with_def
+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 fixes C pls z assumes comm_monoid_add_on_with: "comm_monoid_add_on_with C pls z" begin
+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[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]
 
-private abbreviation "pls' \<equiv> \<lambda>x y. pls (if x \<in> C then x else z) (if y \<in> C then y else z)"
+context begin
 
-lemma fold_pls'_mem: "Finite_Set.fold (pls' \<circ> g) z A \<in> C"
-  if "g ` A \<subseteq> C"
+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 C "pls' \<circ> g"] comm_monoid_add_unfolded
+  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> C"
+  if "g ` A \<subseteq> S"
   using comm_monoid_add_unfolded that
-  by (intro fold_closed_eq[where B=C]) auto
+  by (intro fold_closed_eq[where B=S]) auto
 
-lemma sum_with_mem: "sum_with pls z g A \<in> C" if "g ` A \<subseteq> C"
+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 by 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)
@@ -197,7 +219,7 @@
 
 lemma sum_with_insert:
   "sum_with pls z g (insert x A) = pls (g x) (sum_with pls z g A)"
-  if g_into: "g x \<in> C" "g ` A \<subseteq> C"
+  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"
@@ -212,8 +234,8 @@
   also have "\<dots> = pls (g x) (Finite_Set.fold (pls' \<circ> g) z A)"
   proof -
     from fold_graph_fold[OF A] have "fold_graph (pls' \<circ> g) z A (Finite_Set.fold (pls' \<circ> g) z A)" .
-    from fold_graph_closed_lemma[OF this, of C "pls' \<circ> g"] comm_monoid_add_unfolded
-    have "Finite_Set.fold (pls' \<circ> g) z A \<in> C"
+    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
@@ -226,13 +248,15 @@
   moreover
   have "\<exists>C. g ` insert x A \<subseteq> C \<and> comm_monoid_add_on_with C pls z"
     "\<exists>C. g ` A \<subseteq> C \<and> comm_monoid_add_on_with C pls z"
-    using that (1,2) comm_monoid_add_on_with by auto
+    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"
@@ -276,10 +300,12 @@
       and "Domainp (rel_set A) C"
       by auto
     then obtain C' where [transfer_rule]: "rel_set A C C'" by auto
+    interpret comm: comm_monoid_add_on_with C pls zero by fact
     have C': "g ` T \<subseteq> C'"
       by transfer (rule C)
     have comm': "comm_monoid_add_on_with C' pls' zero'"
       by transfer (rule comm)
+    then interpret comm': comm_monoid_add_on_with C' pls' zero' .
     from C' comm' have ex_comm': "\<exists>C. g ` T \<subseteq> C \<and> comm_monoid_add_on_with C pls' zero'" by auto
     show ?thesis
       using transfer_T C C'
@@ -316,7 +342,7 @@
         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])
+        apply (subst comm.sum_with_insert)
         subgoal using insert.prems by auto
         subgoal using insert.prems by auto
         subgoal by fact
@@ -324,7 +350,7 @@
         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'])
+        apply (subst comm'.sum_with_insert)
         subgoal
           apply transfer
           using insert.prems by auto
--- a/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy	Wed Nov 14 01:31:55 2018 +0000
+++ b/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy	Wed Nov 14 13:45:09 2018 -0500
@@ -6,7 +6,6 @@
     "Prerequisites"
     "../Types_To_Sets"
     Linear_Algebra_On_With
-  keywords "lemmas_with"::thy_decl
 begin
 
 subsection \<open>Rewrite rules to make \<open>ab_group_add\<close> operations implicit.\<close>
@@ -30,7 +29,8 @@
   by (simp add: ab_semigroup_add_on_with_eq ac_simps)
 
 lemma ab_group_add_on_with[implicit_ab_group_add]:
-  "ab_group_add_on_with S ((+)::_::ab_group_add \<Rightarrow> _) 0 (-) uminus \<longleftrightarrow> comm_monoid_add_on_with S (+) 0"
+  "ab_group_add_on_with S ((+)::_::ab_group_add \<Rightarrow> _) 0 (-) uminus \<longleftrightarrow>
+    comm_monoid_add_on_with S (+) 0 \<and> (\<forall>a\<in>S. -a\<in>S)"
   unfolding ab_group_add_on_with_Ball_def
   by simp
 
@@ -52,6 +52,9 @@
 lemma scale_minus_left_on: "scale (- a) x = - scale a x" if "x \<in> S"
   by (metis add_cancel_right_right scale_left_distrib_on neg_eq_iff_add_eq_0 that)
 
+lemma mem_uminus: "x \<in> S \<Longrightarrow> -x \<in> S"
+  by (metis mem_scale scale_minus_left_on scale_one_on)
+
 definition subspace :: "'b set \<Rightarrow> bool"
   where subspace_on_def: "subspace T \<longleftrightarrow> 0 \<in> T \<and> (\<forall>x\<in>T. \<forall>y\<in>T. x + y \<in> T) \<and> (\<forall>c. \<forall>x\<in>T. c *s x \<in> T)"
 
@@ -74,8 +77,13 @@
 
 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
+proof (intro ext iffI)
+  fix s::"'a\<Rightarrow>'b\<Rightarrow>'b" assume "module_on S s"
+  then interpret module_on S s .
+  show "module_on_with S (+) (-) uminus 0 s"
+    by (auto simp: module_on_with_def implicit_ab_group_add
+        mem_add mem_zero mem_uminus scale_right_distrib_on scale_left_distrib_on mem_scale)
+qed (auto simp: module_on_with_def module_on_def implicit_ab_group_add)
 
 locale module_pair_on = m1: module_on S1 scale1 +
                         m2: module_on S2 scale2
@@ -158,130 +166,100 @@
     and scale2::"'a::field \<Rightarrow> 'c::ab_group_add \<Rightarrow> 'c"
     and Basis1 Basis2
 
-subsection \<open>Tool support\<close>
-
-lemmas subset_iff' = subset_iff[folded Ball_def]
-
-ML \<open>
-structure More_Simplifier =
-struct
-
-fun asm_full_var_simplify ctxt thm =
-  let
-    val ((_, [thm']), ctxt') = Variable.import false [thm] ctxt
-  in
-    Simplifier.asm_full_simplify ctxt' thm'
-    |> singleton (Variable.export ctxt' ctxt)
-    |> Drule.zero_var_indexes
-  end
-
-fun var_simplify_only ctxt ths thm =
-  asm_full_var_simplify (Raw_Simplifier.clear_simpset ctxt addsimps ths) thm
-
-val var_simplified = Attrib.thms >>
-  (fn ths => Thm.rule_attribute ths
-    (fn context => var_simplify_only (Context.proof_of context) ths))
-
-val _ = Theory.setup (Attrib.setup \<^binding>\<open>var_simplified\<close> var_simplified "simplified rule (with vars)")
-
-end
-\<close>
-
-ML \<open>
-val _ = Outer_Syntax.local_theory' \<^command_keyword>\<open>lemmas_with\<close> "note theorems with (the same) attributes"
-    (Parse.attribs --| @{keyword :} -- Parse_Spec.name_facts -- Parse.for_fixes
-     >> (fn (((attrs),facts), fixes) =>
-      #2 oo Specification.theorems_cmd Thm.theoremK
-        (map (apsnd (map (apsnd (fn xs => attrs@xs)))) facts) fixes))
-\<close>
 
 subsection \<open>Local Typedef for Subspace\<close>
 
-locale local_typedef_ab_group_add = local_typedef S s for S ::"'b::ab_group_add set" and s::"'s itself" +
-  assumes mem_zero_lt: "0 \<in> S"
-  assumes mem_add_lt: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x + y \<in> S"
-  assumes mem_uminus_lt: "x \<in> S \<Longrightarrow> -x \<in> S"
+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> x - y \<in> S"
-  using mem_add_lt[OF _ mem_uminus_lt] by auto
+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) plus"
-definition minus_S::"'s \<Rightarrow> 's \<Rightarrow> 's" where "minus_S = (rep ---> rep ---> Abs) minus"
-definition uminus_S::"'s \<Rightarrow> 's" where "uminus_S = (rep ---> Abs) uminus"
-definition zero_S::"'s" where "zero_S = Abs 0"
+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) plus plus_S"
+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 mem_add_lt intro!: rel_funI)
+  by (auto simp: cr_S_def add_mem intro!: rel_funI)
 
-lemma minus_S_transfer[transfer_rule]: "(cr_S ===> cr_S ===> cr_S) minus minus_S"
+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) uminus uminus_S"
+lemma uminus_S_transfer[transfer_rule]: "(cr_S ===> cr_S) um uminus_S"
   unfolding uminus_S_def
-  by (auto simp: cr_S_def mem_uminus_lt intro!: rel_funI)
+  by (auto simp: cr_S_def uminus_mem intro!: rel_funI)
 
-lemma zero_S_transfer[transfer_rule]: "cr_S 0 zero_S"
+lemma zero_S_transfer[transfer_rule]: "cr_S z zero_S"
   unfolding zero_S_def
-  by (auto simp: cr_S_def mem_zero_lt intro!: rel_funI)
+  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 simp
-  subgoal by transfer simp
-  subgoal by transfer simp
-  subgoal by transfer simp
-  subgoal by transfer simp
+  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 type.sum"
+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 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)"
+  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 S arbitrary: T rule: infinite_finite_induct)
-    case (infinite S)
+  proof (induction I arbitrary: J rule: infinite_finite_induct)
+    case (infinite I)
     note [transfer_rule] = infinite.prems
-    from infinite.hyps have "infinite T" by transfer
-    then show ?case by (simp add: infinite.hyps zero_S_transfer)
+    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 "T = {}" by transfer rule
+    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 T"
+    have [simp]: "finite J"
       by transfer (simp add: insert.hyps)
-    obtain y where [transfer_rule]: "A x y" and y: "y \<in> T"
+    obtain y where [transfer_rule]: "A x y" and y: "y \<in> J"
       by (meson insert.prems insertI1 rel_setD1)
-    define T' where "T' = T - {y}"
-    have T_def: "T = insert y T'"
-      by (auto simp: T'_def y)
-    define sF where "sF = sum f F"
-    define sT where "sT = type.sum g T'"
-    have [simp]: "y \<notin> T'" "finite T'"
-      by (auto simp: y T'_def)
-    have "rel_set A (insert x F - {x}) T'"
-      unfolding T'_def
+    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 T'"
+    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 "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
+    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
@@ -303,7 +281,7 @@
 sublocale local_typedef S "TYPE('s)"
   using Ex_type_definition_S by unfold_locales
 
-sublocale local_typedef_ab_group_add S "TYPE('s)"
+sublocale local_typedef_ab_group_add "(+)::'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)
 
@@ -322,7 +300,7 @@
   have "module_on_with {x. x \<in> S} (+) (-) uminus 0 scale"
     using module_on_axioms
     by (auto simp: module_on_with_def module_on_def ab_group_add_on_with_Ball_def
-        comm_monoid_add_on_with_Ball_def
+        comm_monoid_add_on_with_Ball_def mem_uminus
         ab_semigroup_add_on_with_Ball_def semigroup_add_on_with_def)
   then show ?thesis
     by transfer'
--- a/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy	Wed Nov 14 01:31:55 2018 +0000
+++ b/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy	Wed Nov 14 13:45:09 2018 -0500
@@ -30,7 +30,8 @@
     have "Domainp (rel_set A) t" using that by (auto simp: Domainp_set)
     from ex_comm_monoid_add_around_imageE[OF ex transfer_rules(1,2) this that(1)]
     obtain C where C: "comm_monoid_add_on_with C p z" "r ` t \<subseteq> C" "Domainp (rel_set A) C" by auto
-    from sum_with_mem[OF C(1,2)] C(3)
+    interpret comm_monoid_add_on_with C p z by fact
+    from sum_with_mem[OF C(2)] C(3)
     show ?thesis
       by auto (meson C(3) Domainp_set)
   qed (use \<open>A z _\<close> in \<open>auto simp: sum_with_def\<close>)
@@ -63,7 +64,7 @@
     (\<exists>t u. finite t \<and> t \<subseteq> X' \<and> sum_with p' z' (\<lambda>v. s' (u v) v) t = z' \<and> (\<exists>v\<in>t. u v \<noteq> 0))"
     apply (transfer_prover_start, transfer_step+)
     using *
-    by (auto simp: intro!: sum_with_mem)
+    by (auto simp: intro!: comm_monoid_add_on_with.sum_with_mem)
 qed
 
 definition subspace_with
--- a/src/HOL/Types_To_Sets/Examples/Prerequisites.thy	Wed Nov 14 01:31:55 2018 +0000
+++ b/src/HOL/Types_To_Sets/Examples/Prerequisites.thy	Wed Nov 14 13:45:09 2018 -0500
@@ -4,6 +4,7 @@
 
 theory Prerequisites
   imports Main
+  keywords "lemmas_with"::thy_decl
 begin
 
 context
@@ -58,4 +59,43 @@
 
 end
 
+subsection \<open>some \<close>
+
+subsection \<open>Tool support\<close>
+
+lemmas subset_iff' = subset_iff[folded Ball_def]
+
+ML \<open>
+structure More_Simplifier =
+struct
+
+fun asm_full_var_simplify ctxt thm =
+  let
+    val ((_, [thm']), ctxt') = Variable.import false [thm] ctxt
+  in
+    Simplifier.asm_full_simplify ctxt' thm'
+    |> singleton (Variable.export ctxt' ctxt)
+    |> Drule.zero_var_indexes
+  end
+
+fun var_simplify_only ctxt ths thm =
+  asm_full_var_simplify (Raw_Simplifier.clear_simpset ctxt addsimps ths) thm
+
+val var_simplified = Attrib.thms >>
+  (fn ths => Thm.rule_attribute ths
+    (fn context => var_simplify_only (Context.proof_of context) ths))
+
+val _ = Theory.setup (Attrib.setup \<^binding>\<open>var_simplified\<close> var_simplified "simplified rule (with vars)")
+
 end
+\<close>
+
+ML \<open>
+val _ = Outer_Syntax.local_theory' \<^command_keyword>\<open>lemmas_with\<close> "note theorems with (the same) attributes"
+    (Parse.attribs --| @{keyword :} -- Parse_Spec.name_facts -- Parse.for_fixes
+     >> (fn (((attrs),facts), fixes) =>
+      #2 oo Specification.theorems_cmd Thm.theoremK
+        (map (apsnd (map (apsnd (fn xs => attrs@xs)))) facts) fixes))
+\<close>
+
+end