--- a/src/HOL/Types_To_Sets/Examples/Group_On_With.thy Tue Nov 13 20:57:54 2018 +0100
+++ b/src/HOL/Types_To_Sets/Examples/Group_On_With.thy Wed Nov 14 01:31:55 2018 +0000
@@ -3,23 +3,27 @@
*)
theory Group_On_With
imports
- Main
+ Prerequisites
begin
subsection \<open>\<^emph>\<open>on\<close> carrier set \<^emph>\<open>with\<close> explicit group operations\<close>
-definition "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)"
+locale semigroup_add_on_with =
+ fixes S::"'a set" and pls::"'a\<Rightarrow>'a\<Rightarrow>'a"
+ 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"
+
+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 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
+ 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)
@@ -44,35 +48,46 @@
by transfer (auto intro!: Domainp_apply2I[OF xy])
qed
-definition "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)"
+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"
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
+ unfolding ab_semigroup_add_on_with_Ball_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
+ 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_def ac_simps)
+ 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"
-definition "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"
+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"
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
+ unfolding comm_monoid_add_on_with_Ball_def
by transfer_prover
lemma right_total_comm_monoid_add_transfer[transfer_rule]:
@@ -85,18 +100,25 @@
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
+ unfolding class.comm_monoid_add_def class.comm_monoid_add_axioms_def comm_monoid_add_on_with_Ball_def
apply transfer
using \<open>A z z'\<close>
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)
+ 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)
-definition "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))"
+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)"
+
+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))"
+ 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
@@ -104,7 +126,7 @@
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
+ 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_transfer[transfer_rule]:
@@ -113,11 +135,11 @@
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
+ 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_def)
+ 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
@@ -140,7 +162,7 @@
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]
+ 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)"
@@ -223,7 +245,7 @@
define C where "C = C0 \<inter> Collect (Domainp A)"
have "comm_monoid_add_on_with C pls zero"
using comm Domainp_apply2I[OF \<open>(A ===> A ===> A) pls pls'\<close>] \<open>A zero zero'\<close>
- by (auto simp: comm_monoid_add_on_with_def ab_semigroup_add_on_with_def
+ by (auto simp: comm_monoid_add_on_with_Ball_def ab_semigroup_add_on_with_Ball_def
semigroup_add_on_with_def C_def)
moreover have "f ` S \<subseteq> C" using C0
by (auto simp: C_def in_dom)
@@ -334,5 +356,4 @@
lemmas [explicit_ab_group_add] = sum_with
-
end
\ No newline at end of file
--- a/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy Tue Nov 13 20:57:54 2018 +0100
+++ b/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy Wed Nov 14 01:31:55 2018 +0000
@@ -3,8 +3,8 @@
*)
theory Linear_Algebra_On
imports
+ "Prerequisites"
"../Types_To_Sets"
- "Prerequisites"
Linear_Algebra_On_With
keywords "lemmas_with"::thy_decl
begin
@@ -17,21 +17,21 @@
lemma semigroup_add_on_with_eq[implicit_ab_group_add]:
"semigroup_add_on_with S ((+)::_::semigroup_add \<Rightarrow> _) \<longleftrightarrow> (\<forall>a\<in>S. \<forall>b\<in>S. a + b \<in> S)"
- by (simp add: semigroup_add_on_with_def ac_simps)
+ by (simp add: semigroup_add_on_with_Ball_def ac_simps)
lemma ab_semigroup_add_on_with_eq[implicit_ab_group_add]:
"ab_semigroup_add_on_with S ((+)::_::ab_semigroup_add \<Rightarrow> _) = semigroup_add_on_with S (+)"
- unfolding ab_semigroup_add_on_with_def
+ unfolding ab_semigroup_add_on_with_Ball_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 \<Rightarrow> _) 0 \<longleftrightarrow> semigroup_add_on_with S (+) \<and> 0 \<in> S"
- unfolding comm_monoid_add_on_with_def
+ unfolding comm_monoid_add_on_with_Ball_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 \<Rightarrow> _) 0 (-) uminus \<longleftrightarrow> comm_monoid_add_on_with S (+) 0"
- unfolding ab_group_add_on_with_def
+ unfolding ab_group_add_on_with_Ball_def
by simp
subsection \<open>Definitions \<^emph>\<open>on\<close> carrier set\<close>
@@ -197,35 +197,6 @@
subsection \<open>Local Typedef for Subspace\<close>
-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: "\<exists>(Rep::'s \<Rightarrow> 'b) (Abs::'b \<Rightarrow> 's). type_definition Rep Abs S"
-begin
-
-definition "rep = fst (SOME (Rep::'s \<Rightarrow> 'b, Abs). type_definition Rep Abs S)"
-definition "Abs = snd (SOME (Rep::'s \<Rightarrow> '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 \<in> S"
- and rep_inverse[simp]: "Abs (rep x) = x"
- and Abs_inverse[simp]: "y \<in> S \<Longrightarrow> rep (Abs y) = y"
- using type_definition_S
- unfolding type_definition_def by auto
-
-definition cr_S where "cr_S \<equiv> \<lambda>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_lt: "0 \<in> S"
assumes mem_add_lt: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x + y \<in> S"
@@ -350,8 +321,9 @@
proof -
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_def comm_monoid_add_on_with_def
- ab_semigroup_add_on_with_def semigroup_add_on_with_def)
+ by (auto simp: module_on_with_def module_on_def ab_group_add_on_with_Ball_def
+ comm_monoid_add_on_with_Ball_def
+ ab_semigroup_add_on_with_Ball_def semigroup_add_on_with_def)
then show ?thesis
by transfer'
qed
@@ -536,6 +508,11 @@
subsection \<open>Transfer from type-based @{theory HOL.Modules} and @{theory HOL.Vector_Spaces}\<close>
+lemmas [transfer_rule] = right_total_fun_eq_transfer
+ and [transfer_rule del] = vimage_parametric
+
+subsubsection \<open>Modules\<close>
+
context module_on begin
context includes lifting_syntax assumes ltd: "\<exists>(Rep::'s \<Rightarrow> 'b) (Abs::'b \<Rightarrow> 's). type_definition Rep Abs S" begin
@@ -789,7 +766,8 @@
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_with = vector_space.dim_with
-(* should work but don't:
+(* should work but don't:v
+
and lt_bij_if_span_eq_span_bases = vector_space.bij_if_span_eq_span_bases
*)
(* not expected to work:
@@ -992,8 +970,6 @@
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,
@@ -1053,7 +1029,6 @@
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,
--- a/src/HOL/Types_To_Sets/Examples/Prerequisites.thy Tue Nov 13 20:57:54 2018 +0100
+++ b/src/HOL/Types_To_Sets/Examples/Prerequisites.thy Wed Nov 14 01:31:55 2018 +0000
@@ -22,4 +22,40 @@
end
+subsection \<open>setting up transfer for local typedef\<close>
+
+lemmas [transfer_rule] = \<comment> \<open>prefer right-total rules\<close>
+ right_total_All_transfer
+ right_total_UNIV_transfer
+ right_total_Ex_transfer
+
+locale local_typedef = fixes S ::"'b set" and s::"'s itself"
+ assumes Ex_type_definition_S: "\<exists>(Rep::'s \<Rightarrow> 'b) (Abs::'b \<Rightarrow> 's). type_definition Rep Abs S"
+begin
+
+definition "rep = fst (SOME (Rep::'s \<Rightarrow> 'b, Abs). type_definition Rep Abs S)"
+definition "Abs = snd (SOME (Rep::'s \<Rightarrow> '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 \<in> S"
+ and rep_inverse[simp]: "Abs (rep x) = x"
+ and Abs_inverse[simp]: "y \<in> S \<Longrightarrow> rep (Abs y) = y"
+ using type_definition_S
+ unfolding type_definition_def by auto
+
+definition cr_S where "cr_S \<equiv> \<lambda>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]
+
+lemma cr_S_rep[intro, simp]: "cr_S (rep a) a" by (simp add: cr_S_def)
+lemma cr_S_Abs[intro, simp]: "a\<in>S \<Longrightarrow> cr_S a (Abs a)" by (simp add: cr_S_def)
+
end
+
+end