Another attempt to fix the tactic closure-solver
authorLukas Stevens <mail@lukas-stevens.de>
Thu, 23 Sep 2021 12:03:29 +0000
branchclosure-solver
changeset 74716 a744e9a22655
parent 74715 f7a8c4470e32
child 74717 e0cbf224a970
Another attempt to fix the tactic
src/HOL/Tools/closure_tac.ML
src/HOL/Transitive_Closure.thy
--- a/src/HOL/Tools/closure_tac.ML	Thu Sep 23 11:26:15 2021 +0200
+++ b/src/HOL/Tools/closure_tac.ML	Thu Sep 23 12:03:29 2021 +0000
@@ -41,10 +41,6 @@
 
 fun dereify_closure_fm r reifytab t =
   let
-    val field_ty = field_type_of (Term.fastype_of r)
-    fun mk_eq (x, y) =
-      Term.Const (@{const_name HOL.eq}, field_ty --> field_ty --> HOLogic.boolT) $ x $ y
-
     fun dereify_term' (App (App (Const "in", t1), t2)) =
           in_pat (dereify_term' t1) (dereify_term' t2) r
       | dereify_term' (App (App (Const "in_trancl", t1), t2)) =
@@ -56,7 +52,7 @@
       | dereify_term' (App (App (Const "in_converse", t1), t2)) =
           in_converse_pat (dereify_term' t1) (dereify_term' t2) r
       | dereify_term' (App (App (Const "eq", t1), t2)) =
-          mk_eq (dereify_term' t1, dereify_term' t2)
+          HOLogic.mk_eq (dereify_term' t1, dereify_term' t2)
       | dereify_term' (App (t1, t2)) = dereify_term' t1 $ dereify_term' t2
       | dereify_term' (Const "Not") = HOLogic.Not
       | dereify_term' (Const "conj") = HOLogic.conj
@@ -178,25 +174,34 @@
     replay_prf_trm (replay_conv convs) dereify ctxt thmtab assmtab
   end
 
-  fun closure_tac simp_prems r = Subgoal.FOCUS (fn {prems=prems, context=ctxt, ...} =>
+  fun closure_tac simp_prems = Subgoal.FOCUS (fn {prems=prems, context=ctxt, ...} =>
     let
+      val prems = filter (fn p => null (Term.add_vars (Thm.prop_of p) [])) (simp_prems @ prems)
+
+      (* Extract the negated form of the original concl to determine the relation *)
+      val concl' = split_last prems |> snd
+      val SOME (_, (x, y), (_, r)) = decomp (Thm.prop_of concl')
+
+      val (x_ty, y_ty) = apply2 Term.fastype_of (x, y)
+      val _ = if x_ty <> y_ty
+                then raise TYPE ("Field type mismatch", [x_ty, y_ty], [])
+                else ()
+
       fun these' _ [] = []
         | these' f (x :: xs) = case f x of NONE => these' f xs | SOME y => (x, y) :: these' f xs
+      val decomp_prems = these' (decomp o Thm.prop_of) prems
+                         |> filter (fn (_, (_, _, (_, r'))) => r aconv r')
 
       val field_ty = field_type_of (Term.fastype_of r)
 
-      fun decomp_eq' (@{const Not} $ t) =
+      fun decomp_eq' (\<^Const_>\<open>Not for t\<close>) =
             Option.map (fn (b, t') => (not b, t')) (decomp_eq' t)
-        | decomp_eq' ((Term.Const (@{const_name HOL.eq}, ty) $ x $ y)) =
+        | decomp_eq' (\<^Const_>\<open>HOL.eq ty for x y\<close>) =
             if ty = field_ty --> field_ty --> @{typ bool} then SOME (true, (x, y)) else NONE
         | decomp_eq' _ = NONE
-      fun decomp_eq (@{const Trueprop} $ t) = decomp_eq' t
+      fun decomp_eq (\<^Const_>\<open>Trueprop for t\<close>) = decomp_eq' t
         | decomp_eq _ = NONE
 
-      val prems = filter (fn p => null (Term.add_vars (Thm.prop_of p) [])) (simp_prems @ prems)
-
-      val decomp_prems = these' (decomp o Thm.prop_of) prems
-                         |> filter (fn (_, (_, _, (_, r'))) => r aconv r')
       val decomp_eq_prems = these' (decomp_eq o Thm.prop_of) prems
 
       fun reify (_, (b, (x, y), (ctor, _))) (ps, reifytab) =
@@ -230,24 +235,21 @@
       closure_procedure (map fst decomp_prems @ map fst decomp_eq_prems)
                         (reified_prems @ reified_eq_prems)
                         reifytab
-    end)
+    end handle TYPE ("Field type mismatch", _, _) => no_tac)
  
   val ad_absurdum_tac = SUBGOAL (fn (A, i) =>
       case try (HOLogic.dest_Trueprop o Logic.strip_assums_concl) A of
-        SOME (nt $ _) =>
-          if nt = HOLogic.Not
-            then resolve0_tac [@{thm notI}] i
-            else resolve0_tac [@{thm ccontr}] i
+        SOME (@{const Not} $ _) => resolve0_tac [@{thm notI}] i
       | _ => resolve0_tac [@{thm ccontr}] i)
 
   fun tac simp_prems ctxt = SUBGOAL (fn (A, i) =>
-    let val goal = Logic.strip_assums_concl A
+    let val concl = Logic.strip_assums_concl A
     in
-      if null (Term.add_vars goal []) then
-        case decomp goal of
+      if null (Term.add_vars concl []) then
+        case decomp (Envir.beta_eta_contract concl) of
           NONE => no_tac
-        | SOME (_, _, (_, r)) => EVERY' [ ad_absurdum_tac, CONVERSION Thm.eta_conversion
-                                        , closure_tac simp_prems r ctxt ] i
+        | SOME _ => EVERY' [ ad_absurdum_tac, CONVERSION Thm.eta_conversion
+                           , closure_tac simp_prems ctxt ] i
       else no_tac
     end)
 
--- a/src/HOL/Transitive_Closure.thy	Thu Sep 23 11:26:15 2021 +0200
+++ b/src/HOL/Transitive_Closure.thy	Thu Sep 23 12:03:29 2021 +0000
@@ -1277,7 +1277,7 @@
 
 ML_file \<open>~~/src/HOL/Tools/closure_procedure.ML\<close>
 ML_file \<open>~~/src/HOL/Tools/closure_tac.ML\<close>
-
+                              
 lemma not_rtrancl_into_not_trancl: "(x, y) \<notin> r\<^sup>* \<Longrightarrow> (x, y) \<notin> r\<^sup>+"
   using trancl_into_rtrancl by fast
 
@@ -1306,121 +1306,100 @@
   using conversep_iff by blast
 
 ML \<open>
- local
-    fun mk_closure_type r = Term.fastype_of r --> Term.fastype_of r
-
-    fun mk_Id ty = Const (@{const_name Id}, ty)
-    fun mk_eq ty = Const (@{const_name HOL.eq}, ty)
-    fun mk_reflcl mk_Id r =
+  structure Closure_Tac_Rel = Closure_Tac(
+    val field_type_of = fst o HOLogic.dest_prodT o HOLogic.dest_setT
+    val field_type_of_rel = field_type_of o Term.fastype_of
+  
+    fun in_pat x y r = HOLogic.mk_mem (HOLogic.mk_prod (x, y), r)
+    fun in_trancl_pat x y r = in_pat x y (\<^Const>\<open>trancl \<open>field_type_of_rel r\<close>\<close> $ r)
+    fun in_rtrancl_pat x y r = in_pat x y (\<^Const>\<open>rtrancl \<open>field_type_of_rel r\<close>\<close> $ r)
+    fun in_reflcl_pat x y r =
       let val r_ty = Term.fastype_of r
-      in Const (@{const_name sup}, r_ty --> r_ty --> r_ty) $ r $ mk_Id r_ty end
-  in
-    structure Closure_Tac_Rel = Closure_Tac(
-        val field_type_of = fst o HOLogic.dest_prodT o HOLogic.dest_setT
+      in in_pat x y (\<^Const>\<open>sup r_ty\<close> $ r $ \<^Const>\<open>Id r_ty\<close>) end
+    fun in_converse_pat x y r =
+      in_pat x y (\<^Const>\<open>converse \<open>field_type_of_rel r\<close> \<open>field_type_of_rel r\<close>\<close> $ r)
   
-        fun in_pat x y r =
-          let
-            val r_ty = Term.fastype_of r
-            val prod_ty = HOLogic.dest_setT r_ty
-            val field_ty = fst (HOLogic.dest_prodT prod_ty)
-            val member = Const (@{const_name Set.member}, prod_ty --> r_ty --> HOLogic.boolT)
-            val pair = Const (@{const_name Pair}, field_ty --> field_ty --> prod_ty)
-          in
-            member $ (pair $ x $ y) $ r
-          end
-        fun in_trancl_pat x y r = in_pat x y (Const (@{const_name trancl}, mk_closure_type r) $ r)
-        fun in_rtrancl_pat x y r = in_pat x y (Const (@{const_name rtrancl}, mk_closure_type r) $ r)
-        fun in_reflcl_pat x y r = in_pat x y (mk_reflcl mk_Id r)
-        fun in_converse_pat x y r = in_pat x y (Const (@{const_name converse}, Term.fastype_of r))
+    val r_into_trancl_thm = @{thm r_into_trancl}
+    val trancl_trans_thm = @{thm trancl_trans}
+    val eq_in_thm = @{lemma \<open>v = x \<Longrightarrow> w = y \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (v, w) \<in> r\<close> by simp}
+    val eq_in_trancl_thm = @{lemma \<open>v = x \<Longrightarrow> w = y \<Longrightarrow> (x, y) \<in> r\<^sup>+ \<Longrightarrow> (v, w) \<in> r\<^sup>+\<close> by simp}
+    val rtrancl_refl_thm = @{lemma \<open>x = y \<Longrightarrow> (x, y) \<in> r\<^sup>*\<close> by simp}
+    val not_rtrancl_into_not_trancl_thm = @{thm not_rtrancl_into_not_trancl}
   
-        val r_into_trancl_thm = @{thm r_into_trancl}
-        val trancl_trans_thm = @{thm trancl_trans}
-        val eq_in_thm = @{lemma \<open>v = x \<Longrightarrow> w = y \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (v, w) \<in> r\<close> by simp}
-        val eq_in_trancl_thm = @{lemma \<open>v = x \<Longrightarrow> w = y \<Longrightarrow> (x, y) \<in> r\<^sup>+ \<Longrightarrow> (v, w) \<in> r\<^sup>+\<close> by simp}
-        val rtrancl_refl_thm = @{lemma \<open>x = y \<Longrightarrow> (x, y) \<in> r\<^sup>*\<close> by simp}
-        val not_rtrancl_into_not_trancl_thm = @{thm not_rtrancl_into_not_trancl}
-  
-        val rtrancl_eq_or_trancl_conv = Conv.rewr_conv @{thm eq_reflection[OF rtrancl_eq_or_trancl]}
-        val reflcl_eq_or_in_conv = Conv.rewr_conv @{thm eq_reflection[OF reflcl_eq_or_in]}
-        val not_reflcl_eq_and_in_conv = Conv.rewr_conv @{thm eq_reflection[OF not_reflcl_eq_and_in]}
-        val in_converse_conv = Conv.rewr_conv @{thm eq_reflection[OF converse_iff]}
-        val not_in_converse_conv = Conv.rewr_conv @{thm eq_reflection[OF not_in_converse]}
+    val rtrancl_eq_or_trancl_conv = Conv.rewr_conv @{thm eq_reflection[OF rtrancl_eq_or_trancl]}
+    val reflcl_eq_or_in_conv = Conv.rewr_conv @{thm eq_reflection[OF reflcl_eq_or_in]}
+    val not_reflcl_eq_and_in_conv = Conv.rewr_conv @{thm eq_reflection[OF not_reflcl_eq_and_in]}
+    val in_converse_conv = Conv.rewr_conv @{thm eq_reflection[OF converse_iff]}
+    val not_in_converse_conv = Conv.rewr_conv @{thm eq_reflection[OF not_in_converse]}
   
-        fun decomp' (@{const Not} $ t) =
-              Option.map (fn (b, p, t') => (not b, p, t')) (decomp' t)
-          | decomp' t =
-            let
-              local open Closure_Procedure
-              in
-                fun decomp_rel (Term.Const (@{const_name rtrancl}, _) $ r) = (InRtcl, r)
-                  | decomp_rel (Term.Const (@{const_name trancl}, _) $ r) = (InTcl, r)
-                  | decomp_rel (Term.Const (@{const_name converse}, _) $ r) = (InConv, r)
-                  | decomp_rel (Term.Const (@{const_name sup}, _) $ r $ Term.Const (@{const_name Id}, _)) =
-                      (InReflcl, r)
-                  | decomp_rel r = (In, r)
-              end
-            in
-              case try (HOLogic.dest_mem #>> HOLogic.dest_prod) (Envir.beta_eta_contract t) of
-                SOME ((x, y), r) =>
-                  try Term.fastype_of r
-                  |> Option.mapPartial (fn r_ty =>
-                       if HOLogic.dest_setT r_ty |> HOLogic.dest_prodT |> op =
-                         then SOME (true, (x, y), decomp_rel r)
-                         else NONE)
-              | NONE => NONE
-            end
-        fun decomp (@{const Trueprop} $ t) = decomp' t
-          | decomp _ = NONE
-      );
+    fun decomp' (\<^Const_>\<open>Not for t\<close>) =
+          Option.map (fn (b, p, t') => (not b, p, t')) (decomp' t)
+      | decomp' t =
+        let
+          local open Closure_Procedure
+          in
+            fun decomp_rel (\<^Const_>\<open>rtrancl _ for r\<close>) = (InRtcl, r)
+              | decomp_rel (\<^Const_>\<open>trancl _ for r\<close>) = (InTcl, r)
+              | decomp_rel (\<^Const_>\<open>converse _ _ for r\<close>) = (InConv, r)
+              | decomp_rel (\<^Const_>\<open>sup _ for r \<open>\<^Const_>\<open>Id _\<close>\<close>\<close>) = (InReflcl, r)
+              | decomp_rel r = (In, r)
+          end
+        in
+          case t of
+            \<^Const_>\<open>Set.member _ for \<open>\<^Const_>\<open>Pair _ _ for x y\<close>\<close> r\<close> =>
+              SOME (true, (x, y), decomp_rel r)
+          | _ => NONE
+        end
+    fun decomp \<^Const_>\<open>Trueprop for t\<close> = decomp' t
+      | decomp _ = NONE
+    );
 
-    structure Closure_Tac_Pred = Closure_Tac(
-      val field_type_of = Term.domain_type
-
-      fun in_pat x y r = r $ x $ y
-      fun in_trancl_pat x y r = in_pat x y (Const (@{const_name tranclp}, mk_closure_type r) $ r)
-      fun in_rtrancl_pat x y r = in_pat x y (Const (@{const_name rtranclp}, mk_closure_type r) $ r)
-      fun in_reflcl_pat x y r = in_pat x y (mk_reflcl mk_eq r)
-      fun in_converse_pat x y r = in_pat x y (Const (@{const_name conversep}, mk_closure_type r) $ r)
+  structure Closure_Tac_Pred = Closure_Tac(
+    val field_type_of = Term.domain_type
+    val field_type_of_rel = field_type_of o Term.fastype_of
   
-      val r_into_trancl_thm = @{thm tranclp.r_into_trancl}
-      val trancl_trans_thm = @{thm tranclp_trans}
-      val eq_in_thm = @{lemma \<open>v = x \<Longrightarrow> w = y \<Longrightarrow> r x y \<Longrightarrow> r v w\<close> by simp}
-      val eq_in_trancl_thm = @{lemma \<open>v = x \<Longrightarrow> w = y \<Longrightarrow> r\<^sup>+\<^sup>+ x y \<Longrightarrow> r\<^sup>+\<^sup>+ v w\<close> by simp}
-      val rtrancl_refl_thm = @{lemma \<open>x = y \<Longrightarrow> r\<^sup>*\<^sup>* x y\<close> by simp}
-      val not_rtrancl_into_not_trancl_thm = @{thm not_rtranclp_into_not_tranclp}
-
-      val rtrancl_eq_or_trancl_conv = Conv.rewr_conv @{thm eq_reflection[OF rtranclp_eq_or_tranclp]}
-      val reflcl_eq_or_in_conv = Conv.rewr_conv @{thm eq_reflection[OF reflclp_eq_or_in]}
-      val not_reflcl_eq_and_in_conv = Conv.rewr_conv @{thm eq_reflection[OF not_reflclp_eq_and_in]}
-      val in_converse_conv = Conv.rewr_conv @{thm eq_reflection[OF conversep_iff]}
-      val not_in_converse_conv = Conv.rewr_conv @{thm eq_reflection[OF not_in_conversep]}
-
-      fun decomp' (@{const Not} $ t) =
-            Option.map (fn (b, p, t') => (not b, p, t')) (decomp' t)
-        | decomp' t =
-          let
-            local open Closure_Procedure
-            in
-              fun decomp_rel (Term.Const (@{const_name rtranclp}, _) $ r) = (InRtcl, r)
-                | decomp_rel (Term.Const (@{const_name tranclp}, _) $ r) = (InTcl, r)
-                | decomp_rel (Term.Const (@{const_name conversep}, _) $ r) = (InConv, r)
-                | decomp_rel (Term.Const (@{const_name sup}, _) $ r $ Term.Const (@{const_name HOL.eq}, _)) =
-                    (InReflcl, r)
-                | decomp_rel r = (In, r)
-            end
+    fun in_pat x y r = r $ x $ y
+    fun in_trancl_pat x y r = in_pat x y (\<^Const>\<open>tranclp \<open>field_type_of_rel r\<close>\<close> $ r)
+    fun in_rtrancl_pat x y r = in_pat x y (\<^Const>\<open>rtranclp \<open>field_type_of_rel r\<close>\<close> $ r)
+    fun in_reflcl_pat x y r =
+      let val r_ty = Term.fastype_of r
+      in in_pat x y (\<^Const>\<open>sup r_ty\<close> $ r $ \<^Const>\<open>HOL.eq r_ty\<close>) end
+    fun in_converse_pat x y r =
+      in_pat x y (\<^Const>\<open>conversep \<open>field_type_of_rel r\<close> \<open>field_type_of_rel r\<close>\<close> $ r)
+  
+    val r_into_trancl_thm = @{thm tranclp.r_into_trancl}
+    val trancl_trans_thm = @{thm tranclp_trans}
+    val eq_in_thm = @{lemma \<open>v = x \<Longrightarrow> w = y \<Longrightarrow> r x y \<Longrightarrow> r v w\<close> by simp}
+    val eq_in_trancl_thm = @{lemma \<open>v = x \<Longrightarrow> w = y \<Longrightarrow> r\<^sup>+\<^sup>+ x y \<Longrightarrow> r\<^sup>+\<^sup>+ v w\<close> by simp}
+    val rtrancl_refl_thm = @{lemma \<open>x = y \<Longrightarrow> r\<^sup>*\<^sup>* x y\<close> by simp}
+    val not_rtrancl_into_not_trancl_thm = @{thm not_rtranclp_into_not_tranclp}
+  
+    val rtrancl_eq_or_trancl_conv = Conv.rewr_conv @{thm eq_reflection[OF rtranclp_eq_or_tranclp]}
+    val reflcl_eq_or_in_conv = Conv.rewr_conv @{thm eq_reflection[OF reflclp_eq_or_in]}
+    val not_reflcl_eq_and_in_conv = Conv.rewr_conv @{thm eq_reflection[OF not_reflclp_eq_and_in]}
+    val in_converse_conv = Conv.rewr_conv @{thm eq_reflection[OF conversep_iff]}
+    val not_in_converse_conv = Conv.rewr_conv @{thm eq_reflection[OF not_in_conversep]}
+  
+    fun decomp' (\<^Const_>\<open>Not for t\<close>) =
+          Option.map (fn (b, p, t') => (not b, p, t')) (decomp' t)
+      | decomp' t =
+        let
+          local open Closure_Procedure
           in
-            case Envir.beta_eta_contract t of
-              r $ x $ y =>
-                try Term.fastype_of r
-                |> Option.mapPartial (fn r_ty =>
-                     if r_ty = field_type_of r_ty --> field_type_of r_ty --> @{typ bool}
-                       then SOME (true, (x, y), decomp_rel r) else NONE)
+            fun decomp_rel (\<^Const_>\<open>rtranclp _ for r\<close>) = (InRtcl, r)
+              | decomp_rel (\<^Const_>\<open>tranclp _ for r\<close>) = (InTcl, r)
+              | decomp_rel (\<^Const_>\<open>conversep _ _ for r\<close>) = (InConv, r)
+              | decomp_rel (\<^Const_>\<open>sup _ for r \<open>\<^Const_>\<open>HOL.eq _\<close>\<close>\<close>) = (InReflcl, r)
+              | decomp_rel r = (In, r)
+          end
+        in
+          case t of
+            r $ x $ y => SOME (true, (x, y), decomp_rel r)
             | _ => NONE
-          end
-      fun decomp (@{const Trueprop} $ t) = decomp' t
-        | decomp _ = NONE
-    );
-  end 
+        end
+    fun decomp \<^Const_>\<open>Trueprop for t\<close> = decomp' t
+      | decomp _ = NONE
+  );
 \<close>
 
 setup \<open>