New HOL simproc 'datatype_no_proper_subterm'
authorManuel Eberl <eberlm@in.tum.de>
Mon, 04 May 2020 17:35:29 +0200
changeset 72059 c095d3143047
parent 72058 455b010d8436
child 72060 96fa0f8072f9
child 72062 dca11678c495
New HOL simproc 'datatype_no_proper_subterm'
NEWS
src/HOL/BNF_Least_Fixpoint.thy
src/HOL/Datatype_Examples/Datatype_Simproc_Tests.thy
src/HOL/Hoare_Parallel/RG_Hoare.thy
src/HOL/Nat.thy
src/HOL/ROOT
src/HOL/Tools/datatype_simprocs.ML
--- 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