# HG changeset patch # User immler # Date 1542159115 0 # Node ID b8b33ef47f400e96f3b0d468ee09bf7af6d5f915 # Parent 085f31ae902d8b52f80efdc0db8d70c8feed21df use locales in Group_On_With diff -r 085f31ae902d -r b8b33ef47f40 src/HOL/Types_To_Sets/Examples/Group_On_With.thy --- 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 \\<^emph>\on\ carrier set \<^emph>\with\ explicit group operations\ -definition "semigroup_add_on_with S pls \ - (\a\S. \b\S. \c\S. pls (pls a b) c = pls a (pls b c)) \ - (\a\S. \b\S. pls a b \ S)" +locale semigroup_add_on_with = + fixes S::"'a set" and pls::"'a\'a\'a" + assumes add_assoc: "a \ S \ b \ S \ c \ S \ pls (pls a b) c = pls a (pls b c)" + assumes add_mem: "a \ S \ b \ S \ pls a b \ S" + +lemma semigroup_add_on_with_Ball_def: "semigroup_add_on_with S pls \ + (\a\S. \b\S. \c\S. pls (pls a b) c = pls a (pls b c)) \ (\a\S. \b\S. pls a b \ 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 \ semigroup_add_on_with S pls \ (\a\S. \b\S. pls a b = pls b a)" +locale ab_semigroup_add_on_with = semigroup_add_on_with + + assumes add_commute: "a \ S \ b \ S \ pls a b = pls b a" + +lemma ab_semigroup_add_on_with_Ball_def: + "ab_semigroup_add_on_with S pls \ semigroup_add_on_with S pls \ (\a\S. \b\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 \ S \ pls z a = a" + assumes zero_mem: "z \ S" -definition "comm_monoid_add_on_with S pls z \ ab_semigroup_add_on_with S pls \ (\a\S. pls z a = a) \ z \ S" +lemma comm_monoid_add_on_with_Ball_def: + "comm_monoid_add_on_with S pls z \ ab_semigroup_add_on_with S pls \ (\a\S. pls z a = a) \ z \ 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 \A z z'\ 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 \ comm_monoid_add_on_with S pls z \ - (\a\S. pls (um a) a = z) \ (\a\S. \b\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 \ S \ pls (um a) a = z" + assumes ab_diff_conv_add_uminus: "a \ S \ b \ S \ 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 \ comm_monoid_add_on_with S pls z \ + (\a\S. pls (um a) a = z) \ (\a\S. \b\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 \C. f ` S \ C \ 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' \ \x y. pls (if x \ C then x else z) (if y \ C then y else z)" @@ -223,7 +245,7 @@ define C where "C = C0 \ Collect (Domainp A)" have "comm_monoid_add_on_with C pls zero" using comm Domainp_apply2I[OF \(A ===> A ===> A) pls pls'\] \A zero zero'\ - 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 \ 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 diff -r 085f31ae902d -r b8b33ef47f40 src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy --- 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 \ _) \ (\a\S. \b\S. a + b \ 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 \ _) = 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 \ _) 0 \ semigroup_add_on_with S (+) \ 0 \ 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 \ _) 0 (-) uminus \ 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 \Definitions \<^emph>\on\ carrier set\ @@ -197,35 +197,6 @@ subsection \Local Typedef for Subspace\ -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: "\(Rep::'s \ 'b) (Abs::'b \ 's). type_definition Rep Abs S" -begin - -definition "rep = fst (SOME (Rep::'s \ 'b, Abs). type_definition Rep Abs S)" -definition "Abs = snd (SOME (Rep::'s \ '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 \ S" - and rep_inverse[simp]: "Abs (rep x) = x" - and Abs_inverse[simp]: "y \ S \ rep (Abs y) = y" - using type_definition_S - unfolding type_definition_def by auto - -definition cr_S where "cr_S \ \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 \ S" assumes mem_add_lt: "x \ S \ y \ S \ x + y \ S" @@ -350,8 +321,9 @@ proof - have "module_on_with {x. x \ 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 \Transfer from type-based @{theory HOL.Modules} and @{theory HOL.Vector_Spaces}\ +lemmas [transfer_rule] = right_total_fun_eq_transfer + and [transfer_rule del] = vimage_parametric + +subsubsection \Modules\ + context module_on begin context includes lifting_syntax assumes ltd: "\(Rep::'s \ 'b) (Abs::'b \ '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, diff -r 085f31ae902d -r b8b33ef47f40 src/HOL/Types_To_Sets/Examples/Prerequisites.thy --- 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 \setting up transfer for local typedef\ + +lemmas [transfer_rule] = \ \prefer right-total rules\ + 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: "\(Rep::'s \ 'b) (Abs::'b \ 's). type_definition Rep Abs S" +begin + +definition "rep = fst (SOME (Rep::'s \ 'b, Abs). type_definition Rep Abs S)" +definition "Abs = snd (SOME (Rep::'s \ '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 \ S" + and rep_inverse[simp]: "Abs (rep x) = x" + and Abs_inverse[simp]: "y \ S \ rep (Abs y) = y" + using type_definition_S + unfolding type_definition_def by auto + +definition cr_S where "cr_S \ \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\S \ cr_S a (Abs a)" by (simp add: cr_S_def) + end + +end