avoid duplicate facts, the "trick" was copied without deeper motivation
authorimmler
Thu Jun 28 10:13:54 2018 +0200 (13 months ago)
changeset 68524f5ca4c2157a5
parent 68523 ccacc84e0251
child 68525 e980a0441b61
child 68527 2f4e2aab190a
avoid duplicate facts, the "trick" was copied without deeper motivation
src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy
     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.71      OF type.ab_group_add_axioms type_module_on_with,
    1.72      untransferred,
    1.73      var_simplified implicit_ab_group_add]:
    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