In a private discussion, there had been a question what can be done against
let (a, b) = p in t being simplified by default to case p of (a, b) => t I did one attempt (see attached patch) to suppress this. However after realizing that proofs now tend to become more complicated, I spent a second thought on this. In short, I have come to the conclusion that let (a, b) = p in t case p of (a, b) => t at the moment being logically distinct, should be one and the same. In other words, I suggest that any case expression on tuples should be printed using »let« rather than »case«. The constant »Let« would turn into a degenerate case combinator with no actual pattern match. This is very much the same way as the code generator translates let- and case expression to target languages. Opinions? Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
# HG changeset patch # Parent 685fb5d8343432ca4547a8ef9a790c3d4099d417 consider let expressions over with product tuple bindings as non-trivial: do not unfold by default diff -r 685fb5d83434 NEWS --- a/NEWS Sun Sep 28 19:40:36 2014 +0200 +++ b/NEWS Sun Sep 28 20:43:36 2014 +0200 @@ -32,6 +32,11 @@ *** HOL *** +* Tupled let bindings "let (…, …) = t in …" are always considered non-trivial +and never unfolded by default. INCOMPATIBILITY, use rule collection +"tuple_binding_unfold" to rewrite tuple bindings via "let" or "case" +to projections with "fst" / "snd". + * Bootstrap of listsum as special case of abstract product over lists. Fact rename: listsum_def ~> listsum.eq_foldr diff -r 685fb5d83434 src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Sun Sep 28 19:40:36 2014 +0200 +++ b/src/HOL/Code_Numeral.thy Sun Sep 28 20:43:36 2014 +0200 @@ -384,7 +384,7 @@ by (auto simp add: sgn_if) have aux2: "\<And>q::int. - int_of_integer k = int_of_integer l * q \<longleftrightarrow> int_of_integer k = int_of_integer l * - q" by auto show ?thesis - by (simp add: prod_eq_iff integer_eq_iff case_prod_beta aux1) + by (simp add: prod_eq_iff integer_eq_iff aux1 tuple_binding_unfold) (auto simp add: zdiv_zminus1_eq_if zmod_zminus1_eq_if div_minus_right mod_minus_right aux2) qed diff -r 685fb5d83434 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Sun Sep 28 19:40:36 2014 +0200 +++ b/src/HOL/HOL.thy Sun Sep 28 20:43:36 2014 +0200 @@ -1226,10 +1226,10 @@ | count_loose (s $ t) k = count_loose s k + count_loose t k | count_loose (Abs (_, _, t)) k = count_loose t (k + 1) | count_loose _ _ = 0; - fun is_trivial_let (Const (@{const_name Let}, _) $ x $ t) = + fun is_trivial_let (Const (@{const_name Let}, _) $ _ $ t) = case t of Abs (_, _, t') => count_loose t' 0 <= 1 - | _ => true; + | _ => not (HOLogic.is_tuple_abs t); in fn _ => fn ctxt => fn ct => if is_trivial_let (Thm.term_of ct) then SOME @{thm Let_def} (*no or one ocurrence of bound variable*) else let (*Norbert Schirmer's case*) diff -r 685fb5d83434 src/HOL/IMP/Abs_Int2.thy --- a/src/HOL/IMP/Abs_Int2.thy Sun Sep 28 19:40:36 2014 +0200 +++ b/src/HOL/IMP/Abs_Int2.thy Sun Sep 28 20:43:36 2014 +0200 @@ -119,8 +119,8 @@ next case (Plus e1 e2) thus ?case using inv_plus'[OF _ aval''_correct aval''_correct] - by (auto split: prod.split) -qed + by (auto simp add: Let_def split: prod.split) + qed lemma inv_bval'_correct: "s : \<gamma>\<^sub>o S \<Longrightarrow> bv = bval b s \<Longrightarrow> s : \<gamma>\<^sub>o(inv_bval' b bv S)" proof(induction b arbitrary: S bv) @@ -133,7 +133,7 @@ next case (Less e1 e2) thus ?case apply hypsubst_thin - apply (auto split: prod.split) + apply (auto simp add: Let_def split: prod.split) apply (metis (lifting) inv_aval'_correct aval''_correct inv_less') done qed @@ -152,7 +152,7 @@ by(induction e arbitrary: a S) (auto simp: Let_def split: option.splits prod.split) lemma top_on_inv_bval': "\<lbrakk>top_on_opt S X; vars b \<subseteq> -X\<rbrakk> \<Longrightarrow> top_on_opt (inv_bval' b r S) X" -by(induction b arbitrary: r S) (auto simp: top_on_inv_aval' top_on_sup split: prod.split) +by(induction b arbitrary: r S) (auto simp: top_on_inv_aval' top_on_sup Let_def split: prod.split) lemma top_on_step': "top_on_acom C (- vars C) \<Longrightarrow> top_on_acom (step' \<top> C) (- vars C)" unfolding step'_def @@ -221,7 +221,7 @@ apply(simp) apply simp apply(metis order_trans[OF _ sup_ge1] order_trans[OF _ sup_ge2]) -apply (simp split: prod.splits) +apply (simp add: Let_def split: prod.splits) apply(metis mono_aval'' mono_inv_aval' mono_inv_less'[simplified less_eq_prod_def] fst_conv snd_conv) done diff -r 685fb5d83434 src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy Sun Sep 28 19:40:36 2014 +0200 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy Sun Sep 28 20:43:36 2014 +0200 @@ -154,7 +154,7 @@ next case (Plus e1 e2) thus ?case using filter_plus'[OF _ aval'_sound[OF Plus(3)] aval'_sound[OF Plus(3)]] - by (auto split: prod.split) + by (auto simp add: Let_def split: prod.split) qed lemma bfilter_sound: "s <:: S \<Longrightarrow> bv = bval b s \<Longrightarrow> s <:: bfilter b bv S" @@ -167,7 +167,7 @@ next case (Less e1 e2) thus ?case apply hypsubst_thin - apply (auto split: prod.split) + apply (auto simp add: Let_def split: prod.split) apply (metis afilter_sound filter_less' aval'_sound Less) done qed diff -r 685fb5d83434 src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy Sun Sep 28 19:40:36 2014 +0200 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy Sun Sep 28 20:43:36 2014 +0200 @@ -126,7 +126,7 @@ next case (Plus e1 e2) thus ?case using filter_plus'[OF _ aval''_sound[OF Plus(3)] aval''_sound[OF Plus(3)]] - by (auto split: prod.split) + by (auto simp add: Let_def split: prod.split) qed lemma bfilter_sound: "s : \<gamma>\<^sub>o S \<Longrightarrow> bv = bval b s \<Longrightarrow> s : \<gamma>\<^sub>o(bfilter b bv S)" @@ -142,7 +142,7 @@ next case (Less e1 e2) thus ?case apply hypsubst_thin - apply (auto split: prod.split) + apply (auto simp add: Let_def split: prod.split) apply (metis afilter_sound filter_less' aval''_sound Less) done qed @@ -256,7 +256,7 @@ apply(simp add: domo_def) apply(simp add: domo_def Let_def update_def lookup_def split: option.splits) apply blast -apply(simp split: prod.split) +apply(simp add: Let_def split: prod.split) done lemma domo_bfilter: "vars b \<subseteq> X \<Longrightarrow> domo S \<subseteq> X \<Longrightarrow> domo(bfilter b bv S) \<subseteq> X" @@ -266,7 +266,7 @@ apply(simp) apply rule apply (metis le_sup_iff subset_trans[OF domo_join]) -apply(simp split: prod.split) +apply(simp add: Let_def split: prod.split) by (metis domo_afilter) lemma step'_Com: @@ -322,7 +322,7 @@ lemma mono_bfilter: "S \<sqsubseteq> S' \<Longrightarrow> bfilter b r S \<sqsubseteq> bfilter b r S'" apply(induction b arbitrary: r S S') -apply(auto simp: le_trans[OF _ join_ge1] le_trans[OF _ join_ge2] split: prod.splits) +apply(auto simp: le_trans[OF _ join_ge1] le_trans[OF _ join_ge2] Let_def split: prod.splits) apply(metis mono_aval'' mono_afilter mono_filter_less'[simplified le_prod_def] fst_conv snd_conv) done diff -r 685fb5d83434 src/HOL/Library/Tree.thy --- a/src/HOL/Library/Tree.thy Sun Sep 28 19:40:36 2014 +0200 +++ b/src/HOL/Library/Tree.thy Sun Sep 28 20:43:36 2014 +0200 @@ -77,13 +77,13 @@ "\<lbrakk> del_rightmost t = (t',x); bst t; t \<noteq> Leaf \<rbrakk> \<Longrightarrow> x \<in> set_tree t \<and> set_tree t' = set_tree t - {x}" apply(induction t arbitrary: t' rule: del_rightmost.induct) - apply (fastforce simp: ball_Un split: prod.splits)+ + apply (fastforce simp: ball_Un Let_def split: prod.splits)+ done lemma del_rightmost_set_tree: "\<lbrakk> del_rightmost t = (t',x); t \<noteq> \<langle>\<rangle> \<rbrakk> \<Longrightarrow> set_tree t = insert x (set_tree t')" apply(induction t arbitrary: t' rule: del_rightmost.induct) -by (auto split: prod.splits) auto +by (auto simp add: Let_def split: prod.splits) auto lemma del_rightmost_bst: "\<lbrakk> del_rightmost t = (t',x); bst t; t \<noteq> \<langle>\<rangle> \<rbrakk> \<Longrightarrow> bst t'" @@ -91,7 +91,7 @@ case (2 l a rl b rr) let ?r = "Node rl b rr" from "2.prems"(1) obtain r' where 1: "del_rightmost ?r = (r',x)" and [simp]: "t' = Node l a r'" - by(simp split: prod.splits) + by(simp add: Let_def split: prod.splits) from "2.prems"(2) 1 del_rightmost_set_tree[OF 1] show ?case by(auto)(simp add: "2.IH") qed auto @@ -102,7 +102,7 @@ case (2 l a rl b rr) from "2.prems"(1) obtain r' where dm: "del_rightmost (Node rl b rr) = (r',x)" and [simp]: "t' = Node l a r'" - by(simp split: prod.splits) + by(simp add: Let_def split: prod.splits) show ?case using "2.prems"(2) "2.IH"[OF dm] del_rightmost_set_tree_if_bst[OF dm] by (fastforce simp add: ball_Un) qed simp_all diff -r 685fb5d83434 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Sun Sep 28 19:40:36 2014 +0200 +++ b/src/HOL/Product_Type.thy Sun Sep 28 20:43:36 2014 +0200 @@ -601,6 +601,12 @@ lemmas split_split_asm [no_atp] = prod.split_asm +lemma Let_pair_split: + "(let (x, y) = t in f x y) = f (fst t) (snd t)" + by (simp add: prod.case_eq_if) + +lemmas tuple_binding_unfold = prod.case_eq_if Let_pair_split + text {* \medskip @{term split} used as a logical connective or set former. diff -r 685fb5d83434 src/HOL/Tools/hologic.ML --- a/src/HOL/Tools/hologic.ML Sun Sep 28 19:40:36 2014 +0200 +++ b/src/HOL/Tools/hologic.ML Sun Sep 28 20:43:36 2014 +0200 @@ -83,6 +83,7 @@ val flat_tuple_paths: term -> int list list val mk_psplits: int list list -> typ -> typ -> term -> term val strip_psplits: term -> term * typ list * int list list + val is_tuple_abs: term -> bool val natT: typ val zero: term val is_zero: term -> bool @@ -478,6 +479,9 @@ (incr_boundvars 1 t $ Bound 0) in strip [[]] [] [] end; +fun is_tuple_abs t = + case try strip_psplits t of SOME (_, _ :: _ :: _, _) => true | _ => false; + (* nat *)
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev