# HG changeset patch # User Manuel Eberl # Date 1588606529 -7200 # Node ID c095d31430478ab058509b99e08f720e50085eef # Parent 455b010d8436693331256747c00fc42f0e55c254 New HOL simproc 'datatype_no_proper_subterm' diff -r 455b010d8436 -r c095d3143047 NEWS --- 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 diff -r 455b010d8436 -r c095d3143047 src/HOL/BNF_Least_Fixpoint.thy --- 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 \Tools/BNF/bnf_lfp_rec_sugar_more.ML\ ML_file \Tools/BNF/bnf_lfp_size.ML\ +ML_file \Tools/datatype_simprocs.ML\ + +simproc_setup datatype_no_proper_subterm + ("(x :: 'a :: size) = y") = \K Datatype_Simprocs.no_proper_subterm_simproc\ + end diff -r 455b010d8436 -r c095d3143047 src/HOL/Datatype_Examples/Datatype_Simproc_Tests.thy --- /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 \Tests of datatype-specific simprocs\ + +theory Datatype_Simproc_Tests +imports Main +begin + +(* datatype without parameters *) + +datatype foo = X | Y foo foo + +lemma "x \ Y x y" "x \ Y y x" "Y x y \ x" "Y y x \ x" + by simp_all + + +(* datatype with parameters *) + +datatype 'a mytree = A 'a | B "'a mytree" "'a mytree" + +lemma "B l r \ l" and "B l r \ r" and "l \ B l r" and "r \ 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 "\x\{a,b,c,d,e,f}. t \ x" + by simp + have "\x\{a,b,c,d,e,f}. x \ 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) \ a" and "B1 a (B2 b c) \ c" + by simp_all + +lemma "B2 a (B1 b c) \ a" and "B2 a (B1 b c) \ c" + by simp_all + +end diff -r 455b010d8436 -r c095d3143047 src/HOL/Hoare_Parallel/RG_Hoare.thy --- 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) \ \WhileOne\ -apply(thin_tac "P = While b P \ 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 \ \WhileMore\ -apply(thin_tac "P = While b P \ Q" for Q) apply(rule ctran_in_comm,simp del:last.simps) \ \metiendo la hipotesis antes de dividir la conclusion.\ apply(subgoal_tac "(Some (While b P), snd (last ((Some P, sa) # xs))) # ys \ assum (pre, rely)") diff -r 455b010d8436 -r c095d3143047 src/HOL/Nat.thy --- 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 \ size y \ x \ y" + by (erule contrapos_nn) (rule arg_cong) + subsection \Code module namespace\ diff -r 455b010d8436 -r c095d3143047 src/HOL/ROOT --- 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 " diff -r 455b010d8436 -r c095d3143047 src/HOL/Tools/datatype_simprocs.ML --- /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 \ '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