[isabelle-dev] Let and tuple case expressions
Florian Haftmann
florian.haftmann at informatik.tu-muenchen.de
Thu Oct 2 18:13:28 CEST 2014
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
-------------- next part --------------
# 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 *)
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20141002/cda0daa6/attachment.asc>
More information about the isabelle-dev
mailing list