# HG changeset patch # User immler # Date 1542221109 18000 # Node ID bc0b0d46599138110f11c1ed8d196552c8f90aff # Parent b8b33ef47f400e96f3b0d468ee09bf7af6d5f915 generalized local_typedef_ab_group_add diff -r b8b33ef47f40 -r bc0b0d465991 src/HOL/Types_To_Sets/Examples/Group_On_With.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 \ S \ pls (um a) a = z" assumes ab_diff_conv_add_uminus: "a \ S \ b \ S \ mns a b = pls a (um b)" + assumes uminus_mem: "a \ S \ um a \ S" 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))" + (\a\S. pls (um a) a = z) \ (\a\S. \b\S. mns a b = pls a (um b)) \ (\a\S. um a \ 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 \auto simp: rel_fun_def\) +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\'b" and X::"'a set" - have ex: "\C. f ` X \ C \ 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 "\C. f ` S \ C \ comm_monoid_add_on_with C pls z \ P (Finite_Set.fold (pls o f) z S)" + "(\C. comm_monoid_add_on_with C pls z \ (\s\S. f s \ C)) \ 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 \ 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' \ \x y. pls (if x \ C then x else z) (if y \ C then y else z)" +context begin -lemma fold_pls'_mem: "Finite_Set.fold (pls' \ g) z A \ C" - if "g ` A \ C" +private abbreviation "pls' \ \x y. pls (if x \ S then x else z) (if y \ S then y else z)" + +lemma fold_pls'_mem: "Finite_Set.fold (pls' \ g) z A \ S" + if "g ` A \ 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' \ g) z A (Finite_Set.fold (pls' \ g) z A)" . - from fold_graph_closed_lemma[OF this, of C "pls' \ g"] comm_monoid_add_unfolded + from fold_graph_closed_lemma[OF this, of S "pls' \ 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' \ g) z A = Finite_Set.fold (pls \ g) z A" - if "g ` A \ C" + if "g ` A \ 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 \ C" if "g ` A \ C" +lemma sum_with_mem: "sum_with pls z g A \ S" if "g ` A \ S" proof - interpret comp_fun_commute "pls' o g" using comm_monoid_add_unfolded that by unfold_locales auto - have "\C. g ` A \ C \ comm_monoid_add_on_with C pls z" using that comm_monoid_add_on_with by auto + have "\C. g ` A \ C \ 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 \ C" "g ` A \ C" + if g_into: "g x \ S" "g ` A \ S" and A: "finite A" and x: "x \ A" proof - interpret comp_fun_commute "pls' o g" @@ -212,8 +234,8 @@ also have "\ = pls (g x) (Finite_Set.fold (pls' \ g) z A)" proof - from fold_graph_fold[OF A] have "fold_graph (pls' \ g) z A (Finite_Set.fold (pls' \ g) z A)" . - from fold_graph_closed_lemma[OF this, of C "pls' \ g"] comm_monoid_add_unfolded - have "Finite_Set.fold (pls' \ g) z A \ C" + from fold_graph_closed_lemma[OF this, of S "pls' \ g"] comm_monoid_add_unfolded + have "Finite_Set.fold (pls' \ g) z A \ S" by auto then show ?thesis using g_into by auto @@ -226,13 +248,15 @@ moreover have "\C. g ` insert x A \ C \ comm_monoid_add_on_with C pls z" "\C. g ` A \ C \ 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: "\C. f ` S \ C \ 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 \ 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': "\C. g ` T \ C \ 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 diff -r b8b33ef47f40 -r bc0b0d465991 src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy --- 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 \Rewrite rules to make \ab_group_add\ operations implicit.\ @@ -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 \ _) 0 (-) uminus \ comm_monoid_add_on_with S (+) 0" + "ab_group_add_on_with S ((+)::_::ab_group_add \ _) 0 (-) uminus \ + comm_monoid_add_on_with S (+) 0 \ (\a\S. -a\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 \ S" by (metis add_cancel_right_right scale_left_distrib_on neg_eq_iff_add_eq_0 that) +lemma mem_uminus: "x \ S \ -x \ S" + by (metis mem_scale scale_minus_left_on scale_one_on) + definition subspace :: "'b set \ bool" where subspace_on_def: "subspace T \ 0 \ T \ (\x\T. \y\T. x + y \ T) \ (\c. \x\T. c *s x \ 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\'b\'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 \ 'c::ab_group_add \ 'c" and Basis1 Basis2 -subsection \Tool support\ - -lemmas subset_iff' = subset_iff[folded Ball_def] - -ML \ -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>\var_simplified\ var_simplified "simplified rule (with vars)") - -end -\ - -ML \ -val _ = Outer_Syntax.local_theory' \<^command_keyword>\lemmas_with\ "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)) -\ subsection \Local Typedef for Subspace\ -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" - assumes mem_uminus_lt: "x \ S \ -x \ 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 \ S \ y \ S \ x - y \ S" - using mem_add_lt[OF _ mem_uminus_lt] by auto +lemma mem_minus_lt: "x \ S \ y \ S \ mns x y \ 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 \ 's \ 's" where "plus_S = (rep ---> rep ---> Abs) plus" -definition minus_S::"'s \ 's \ 's" where "minus_S = (rep ---> rep ---> Abs) minus" -definition uminus_S::"'s \ 's" where "uminus_S = (rep ---> Abs) uminus" -definition zero_S::"'s" where "zero_S = Abs 0" +definition plus_S::"'s \ 's \ 's" where "plus_S = (rep ---> rep ---> Abs) pls" +definition minus_S::"'s \ 's \ 's" where "minus_S = (rep ---> rep ---> Abs) mns" +definition uminus_S::"'s \ '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 \ T" + obtain y where [transfer_rule]: "A x y" and y: "y \ 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 \ 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 \ 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 \ S" "f ` F \ S" + using \A x y\ 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\'b\'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 \ 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' diff -r b8b33ef47f40 -r bc0b0d465991 src/HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy --- 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 \ 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 \A z _\ in \auto simp: sum_with_def\) @@ -63,7 +64,7 @@ (\t u. finite t \ t \ X' \ sum_with p' z' (\v. s' (u v) v) t = z' \ (\v\t. u v \ 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 diff -r b8b33ef47f40 -r bc0b0d465991 src/HOL/Types_To_Sets/Examples/Prerequisites.thy --- 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 \some \ + +subsection \Tool support\ + +lemmas subset_iff' = subset_iff[folded Ball_def] + +ML \ +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>\var_simplified\ var_simplified "simplified rule (with vars)") + end +\ + +ML \ +val _ = Outer_Syntax.local_theory' \<^command_keyword>\lemmas_with\ "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)) +\ + +end