--- a/NEWS Tue May 12 16:53:13 2020 +0100
+++ b/NEWS Mon May 04 17:35:29 2020 +0200
@@ -451,6 +451,10 @@
*** HOL ***
+* Simproc 'datatype_no_proper_subterm' rewrites equalities 'lhs = rhs'
+on datatypes to 'False' if either side is a proper subexpression of the
+other (for any datatype with a reasonable size function).
+
* Command 'export_code' produces output as logical files within the
theory context, as well as formal session exports that can be
materialized via command-line tools "isabelle export" or "isabelle build
--- a/src/HOL/BNF_Least_Fixpoint.thy Tue May 12 16:53:13 2020 +0100
+++ b/src/HOL/BNF_Least_Fixpoint.thy Mon May 04 17:35:29 2020 +0200
@@ -203,4 +203,9 @@
ML_file \<open>Tools/BNF/bnf_lfp_rec_sugar_more.ML\<close>
ML_file \<open>Tools/BNF/bnf_lfp_size.ML\<close>
+ML_file \<open>Tools/datatype_simprocs.ML\<close>
+
+simproc_setup datatype_no_proper_subterm
+ ("(x :: 'a :: size) = y") = \<open>K Datatype_Simprocs.no_proper_subterm_simproc\<close>
+
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Datatype_Examples/Datatype_Simproc_Tests.thy Mon May 04 17:35:29 2020 +0200
@@ -0,0 +1,48 @@
+(* Title: HOL/Datatype_Examples/Simproc_Tests.thy
+ Author: Manuel Eberl, TU München
+*)
+
+section \<open>Tests of datatype-specific simprocs\<close>
+
+theory Datatype_Simproc_Tests
+imports Main
+begin
+
+(* datatype without parameters *)
+
+datatype foo = X | Y foo foo
+
+lemma "x \<noteq> Y x y" "x \<noteq> Y y x" "Y x y \<noteq> x" "Y y x \<noteq> x"
+ by simp_all
+
+
+(* datatype with parameters *)
+
+datatype 'a mytree = A 'a | B "'a mytree" "'a mytree"
+
+lemma "B l r \<noteq> l" and "B l r \<noteq> r" and "l \<noteq> B l r" and "r \<noteq> B l r"
+ by simp_all
+
+notepad
+begin
+ fix a b c d e f :: "nat mytree"
+ define t where [simp]: "t = B (B (B a b) (B c d)) (B e f)"
+ have "\<forall>x\<in>{a,b,c,d,e,f}. t \<noteq> x"
+ by simp
+ have "\<forall>x\<in>{a,b,c,d,e,f}. x \<noteq> t"
+ by simp
+end
+
+
+(* mutual recursion *)
+
+datatype 'a myty1 = A1 'a | B1 "'a myty1" "'a myty2"
+ and 'a myty2 = A2 'a | B2 "'a myty2" "'a myty1"
+
+lemma "B1 a (B2 b c) \<noteq> a" and "B1 a (B2 b c) \<noteq> c"
+ by simp_all
+
+lemma "B2 a (B1 b c) \<noteq> a" and "B2 a (B1 b c) \<noteq> c"
+ by simp_all
+
+end
--- a/src/HOL/Hoare_Parallel/RG_Hoare.thy Tue May 12 16:53:13 2020 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy Mon May 04 17:35:29 2020 +0200
@@ -914,7 +914,6 @@
apply clarify
apply (simp add:last_length)
\<comment> \<open>WhileOne\<close>
-apply(thin_tac "P = While b P \<longrightarrow> Q" for Q)
apply(rule ctran_in_comm,simp)
apply(simp add:Cons_lift del:list.map)
apply(simp add:comm_def del:list.map)
@@ -957,7 +956,6 @@
apply(simp only:last_lift_not_None)
apply simp
\<comment> \<open>WhileMore\<close>
-apply(thin_tac "P = While b P \<longrightarrow> Q" for Q)
apply(rule ctran_in_comm,simp del:last.simps)
\<comment> \<open>metiendo la hipotesis antes de dividir la conclusion.\<close>
apply(subgoal_tac "(Some (While b P), snd (last ((Some P, sa) # xs))) # ys \<in> assum (pre, rely)")
--- a/src/HOL/Nat.thy Tue May 12 16:53:13 2020 +0100
+++ b/src/HOL/Nat.thy Mon May 04 17:35:29 2020 +0200
@@ -2528,6 +2528,9 @@
lemmas size_nat = size_nat_def
+lemma size_neq_size_imp_neq: "size x \<noteq> size y \<Longrightarrow> x \<noteq> y"
+ by (erule contrapos_nn) (rule arg_cong)
+
subsection \<open>Code module namespace\<close>
--- a/src/HOL/ROOT Tue May 12 16:53:13 2020 +0100
+++ b/src/HOL/ROOT Mon May 04 17:35:29 2020 +0200
@@ -851,6 +851,7 @@
Misc_Datatype
Misc_Primcorec
Misc_Primrec
+ Datatype_Simproc_Tests
session "HOL-Corec_Examples" (timing) in Corec_Examples = "HOL-Library" +
description "
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/datatype_simprocs.ML Mon May 04 17:35:29 2020 +0200
@@ -0,0 +1,133 @@
+(* Title: HOL/Tools/datatype_simprocs.ML
+ Author: Manuel Eberl, TU München
+
+Simproc to automatically rewrite equalities of datatype values "lhs = rhs" to "False" if
+either side is a proper subterm of the other.
+*)
+
+signature DATATYPE_SIMPROCS = sig
+ val no_proper_subterm_simproc : Proof.context -> cterm -> thm option
+end
+
+structure Datatype_Simprocs : DATATYPE_SIMPROCS = struct
+
+exception NOT_APPLICABLE
+
+val size_neq_imp_neq_thm = @{thm HOL.Eq_FalseI[OF size_neq_size_imp_neq]}
+
+fun get_bnf_sugar ctxt s =
+ case BNF_FP_Def_Sugar.fp_sugar_of ctxt s of
+ SOME sugar => sugar
+ | NONE => raise NOT_APPLICABLE
+
+(*
+ Checks if the given type contains any of the given datatypes (with only type variables
+ as arguments). This allows discovering which arguments of a datatype constructor are
+ recursive and which are not.
+*)
+fun contains_datatypes T_names =
+ let
+ fun go (Type (s, Ts)) =
+ (member op= T_names s andalso forall is_TVar Ts)
+ orelse exists go Ts
+ | go _ = false
+ in
+ go
+ end
+
+fun mk_ctor T_names t =
+ let
+ val name = t |> dest_Const |> fst
+ val (argTs, _) = strip_type (fastype_of t)
+ val active_poss = map (contains_datatypes T_names) argTs
+ in
+ (name, active_poss)
+ end
+
+(*
+ Returns a pair of constructor name and a boolean list indicating whether each
+ constructor argument is or is recursive. E.g. the first parameter of "Cons" for lists is
+ non-recursive and the second one is.
+*)
+fun get_ctors T_names (sugar : BNF_FP_Def_Sugar.fp_sugar) =
+ sugar
+ |> #fp_ctr_sugar
+ |> #ctr_defs
+ |> map (Thm.concl_of #> Logic.dest_equals #> fst #> mk_ctor T_names)
+
+fun get_mutuals (sugar : BNF_FP_Def_Sugar.fp_sugar) =
+ sugar
+ |> #fp_res
+ |> #Ts
+ |> map (dest_Type #> fst)
+
+fun get_ctors_mutuals ctxt sugar =
+ let
+ val mutuals = sugar |> get_mutuals
+ in
+ mutuals |> map (get_bnf_sugar ctxt #> get_ctors mutuals) |> flat
+ end
+
+fun get_size_info ctxt s =
+ case BNF_LFP_Size.size_of ctxt s of
+ SOME info => info
+ | NONE => raise NOT_APPLICABLE
+
+fun is_comb (_ $ _) = true
+ | is_comb _ = false
+
+(* simproc will not be used for these types *)
+val forbidden_types =
+ ([@{typ "bool"}, @{typ "nat"}, @{typ "'a \<times> 'b"}, @{typ "'a + 'b"}]
+ |> map (dest_Type #> fst))
+ @ ["List.list", "Option.option"]
+
+(* FIXME: possible improvements:
+ - support for nested datatypes
+ - replace size-based proof with proper subexpression relation
+*)
+fun no_proper_subterm_simproc ctxt ct =
+ let
+ val (clhs, crhs) = ct |> Thm.dest_comb |> apfst (Thm.dest_comb #> snd)
+ val (lhs, rhs) = apply2 Thm.term_of (clhs, crhs)
+ val cT = Thm.ctyp_of_cterm clhs
+ val T = Thm.typ_of cT
+ val (T_name, T_args) = T |> dest_Type
+
+ val _ = if member op= forbidden_types T_name then raise NOT_APPLICABLE else ()
+ val _ = if lhs aconv rhs then raise NOT_APPLICABLE else ()
+
+ val sugar = get_bnf_sugar ctxt T_name
+ val (_, (_, size_eq_thms, _)) = get_size_info ctxt T_name
+ val ctors = get_ctors_mutuals ctxt sugar
+
+ (* Descend into the term t along datatype constructors, but only along those constructor
+ arguments that are actually recursive *)
+ fun is_subterm s t =
+ let
+ fun go t =
+ s aconv t orelse (is_comb t andalso go' (strip_comb t))
+ and go' (Const (c, _), ts) = (
+ case AList.lookup op= ctors c of
+ NONE => false
+ | SOME poss => exists (fn (b, t) => b andalso go t) (poss ~~ ts))
+ | go' _ = false
+ in
+ go t
+ end
+ val _ = if not (is_subterm lhs rhs) andalso not (is_subterm rhs lhs) then
+ raise NOT_APPLICABLE else ()
+ in
+ size_neq_imp_neq_thm
+ |> Drule.instantiate'_normalize [SOME cT] [SOME clhs, SOME crhs]
+ |> rewrite_goals_rule ctxt (map (fn thm => thm RS @{thm eq_reflection}) size_eq_thms)
+ |> Tactic.rule_by_tactic ctxt (HEADGOAL (Lin_Arith.simple_tac ctxt))
+ |> SOME
+ end
+ handle NOT_APPLICABLE => NONE
+ | CTERM _ => NONE
+ | TERM _ => NONE
+ | TYPE _ => NONE
+ | THM _ => NONE
+
+end