author immler Thu Jun 28 10:13:54 2018 +0200 (13 months ago) changeset 68524 f5ca4c2157a5 parent 68523 ccacc84e0251 child 68525 e980a0441b61 child 68527 2f4e2aab190a
avoid duplicate facts, the "trick" was copied without deeper motivation
```     1.1 --- a/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy	Wed Jun 27 20:31:22 2018 +0200
1.2 +++ b/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy	Thu Jun 28 10:13:54 2018 +0200
1.3 @@ -100,21 +100,10 @@
1.4      module_hom_on_axioms_def
1.5    by (auto intro!: ext)
1.6
1.7 -locale vector_space_on = \<comment>\<open>here we do the same trick as in \<open>module\<close> vs \<open>vector_space\<close>.\<close>
1.8 -  fixes S and scale :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*s" 75)
1.9 -  assumes scale_right_distrib [algebra_simps]: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> a *s (x + y) = a *s x + a *s y"
1.10 -    and scale_left_distrib [algebra_simps]: "x \<in> S \<Longrightarrow> (a + b) *s x = a *s x + b *s x"
1.11 -    and scale_scale [simp]: "x \<in> S \<Longrightarrow> a *s (b *s x) = (a * b) *s x"
1.12 -    and scale_one [simp]: "x \<in> S \<Longrightarrow> 1 *s x = x"
1.13 -    and mem_add: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x + y \<in> S"
1.14 -    and mem_zero: "0 \<in> S"
1.15 -    and mem_scale: "x \<in> S \<Longrightarrow> a *s x \<in> S"
1.16 +locale vector_space_on = module_on S scale
1.17 +  for S and scale :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*s" 75)
1.18  begin
1.19
1.20 -sublocale module_on S "( *s)"
1.21 -  using vector_space_on_axioms[unfolded vector_space_on_def]
1.22 -  by unfold_locales auto
1.23 -
1.24  definition dim :: "'b set \<Rightarrow> nat"
1.25    where "dim V = (if \<exists>b\<subseteq>S. \<not> dependent b \<and> span b = span V
1.26      then card (SOME b. b \<subseteq> S \<and> \<not> dependent b \<and> span b = span V)
1.27 @@ -230,13 +219,13 @@
1.28  end
1.29
1.30  locale local_typedef_ab_group_add = local_typedef S s for S ::"'b::ab_group_add set" and s::"'s itself" +
1.31 -  assumes mem_zero: "0 \<in> S"
1.32 -  assumes mem_add: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x + y \<in> S"
1.33 -  assumes mem_uminus: "x \<in> S \<Longrightarrow> -x \<in> S"
1.34 +  assumes mem_zero_lt: "0 \<in> S"
1.35 +  assumes mem_add_lt: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x + y \<in> S"
1.36 +  assumes mem_uminus_lt: "x \<in> S \<Longrightarrow> -x \<in> S"
1.37  begin
1.38
1.39 -lemma mem_minus: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x - y \<in> S"
1.40 -  using mem_add[OF _ mem_uminus] by auto
1.41 +lemma mem_minus_lt: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x - y \<in> S"
1.42 +  using mem_add_lt[OF _ mem_uminus_lt] by auto
1.43
1.44  context includes lifting_syntax begin
1.45
1.46 @@ -247,19 +236,19 @@
1.47
1.48  lemma plus_S_transfer[transfer_rule]: "(cr_S ===> cr_S ===> cr_S) plus plus_S"
1.49    unfolding plus_S_def
1.50 -  by (auto simp: cr_S_def mem_add intro!: rel_funI)
1.51 +  by (auto simp: cr_S_def mem_add_lt intro!: rel_funI)
1.52
1.53  lemma minus_S_transfer[transfer_rule]: "(cr_S ===> cr_S ===> cr_S) minus minus_S"
1.54    unfolding minus_S_def
1.55 -  by (auto simp: cr_S_def mem_minus intro!: rel_funI)
1.56 +  by (auto simp: cr_S_def mem_minus_lt intro!: rel_funI)
1.57
1.58  lemma uminus_S_transfer[transfer_rule]: "(cr_S ===> cr_S) uminus uminus_S"
1.59    unfolding uminus_S_def
1.60 -  by (auto simp: cr_S_def mem_uminus intro!: rel_funI)
1.61 +  by (auto simp: cr_S_def mem_uminus_lt intro!: rel_funI)
1.62
1.63  lemma zero_S_transfer[transfer_rule]: "cr_S 0 zero_S"
1.64    unfolding zero_S_def
1.65 -  by (auto simp: cr_S_def mem_zero intro!: rel_funI)
1.66 +  by (auto simp: cr_S_def mem_zero_lt intro!: rel_funI)
1.67
1.68  end
1.69
1.70 @@ -538,11 +527,7 @@
1.72      untransferred,
1.74 -      lt_scale_right_distrib = module.scale_right_distrib
1.75 -  and lt_scale_left_distrib = module.scale_left_distrib
1.76 -  and lt_scale_scale = module.scale_scale
1.77 -  and lt_scale_one = module.scale_one
1.78 -  and lt_scale_left_commute = module.scale_left_commute
1.79 +    lt_scale_left_commute = module.scale_left_commute
1.80    and lt_scale_zero_left = module.scale_zero_left
1.81    and lt_scale_minus_left = module.scale_minus_left
1.82    and lt_scale_left_diff_distrib = module.scale_left_diff_distrib
1.83 @@ -647,11 +632,7 @@
1.84      folded subset_iff',
1.85      simplified pred_fun_def,
1.86      simplified\<comment>\<open>too much?\<close>]:
1.87 -      scale_right_distrib = lt_scale_right_distrib
1.88 -  and scale_left_distrib = lt_scale_left_distrib
1.89 -  and scale_scale = lt_scale_scale
1.90 -  and scale_one = lt_scale_one
1.91 -  and scale_left_commute = lt_scale_left_commute
1.92 +      scale_left_commute = lt_scale_left_commute
1.93    and scale_zero_left = lt_scale_zero_left
1.94    and scale_minus_left = lt_scale_minus_left
1.95    and scale_left_diff_distrib = lt_scale_left_diff_distrib
```