Automate initial version of equivariance proof

Works for all cases except InfFOL and Mazza

Author: jvanbruegge

Tools/binder_inductive.ML

@@ -61,6 +61,10 @@ fun binder_inductive_cmd ((pred_name, binds_opt), perms_supps) no_defs_lthy =
 
     val param_Ts = map (Term.typ_subst_TVars subst) param_Ts;
 
+    val param_sugars = map (fn T => Option.mapPartial (fn s =>
+      MRBNF_Sugar.binder_sugar_of no_defs_lthy s
+    ) (try (fn () => fst (dest_Type T)) ())) param_Ts;
+
     fun collect_binders (Free _) = []
       | collect_binders (Var _) = []
       | collect_binders (Bound _) = []
@@ -230,7 +234,6 @@ fun binder_inductive_cmd ((pred_name, binds_opt), perms_supps) no_defs_lthy =
         val thy = Proof_Context.theory_of no_defs_lthy;
         fun mk_match mk_T ts = map2 (fn t => fn T =>
           let
-            val _ = @{print} (Thm.cterm_of no_defs_lthy t, T, mk_T T)
             val t = Logic.varify_types_global t;
             val tyenv = Sign.typ_match thy (fastype_of t, mk_T T) Vartab.empty;
           in Envir.subst_term (tyenv, Vartab.empty) t end
@@ -361,6 +364,7 @@ fun binder_inductive_cmd ((pred_name, binds_opt), perms_supps) no_defs_lthy =
     val perms_specified = map (fn Inl _ => false | _ => true) raw_perms;
     val supps_specified = map (fn Inl _ => false | _ => true) raw_supps;
     val one_specified = map2 (fn a => fn b => a orelse b) perms_specified supps_specified;
+
     fun keep_perm xs = cond_keep xs perms_specified;
     fun keep_supp xs = cond_keep xs supps_specified;
     fun keep_both xs = cond_keep xs one_specified;
@@ -371,7 +375,7 @@ fun binder_inductive_cmd ((pred_name, binds_opt), perms_supps) no_defs_lthy =
     val goals = map (single o rpair []) (
       keep_perm perm_id0_goals @ keep_perm perm_comp_goals @ keep_both supp_seminat_goals
       @ keep_both perm_support_goals @ keep_supp supp_small_goals @ flat (keep_binders B_small_goals)
-      @ [G_equiv_goal, G_refresh_goal]
+      @ [G_refresh_goal]
     );
     fun after_qed thmss lthy =
       let
@@ -422,14 +426,13 @@ fun binder_inductive_cmd ((pred_name, binds_opt), perms_supps) no_defs_lthy =
         val m2 = length (filter not one_specified);
         val m3 = length (filter not supps_specified);
         val m4 = length (filter not binders_specified);
-        val (((((((perm_id0s, perm_comps), supp_seminats), perm_supports), supp_smalls), B_smalls), G_equiv), G_refresh) = map hd thmss
+        val ((((((perm_id0s, perm_comps), supp_seminats), perm_supports), supp_smalls), B_smalls), G_refresh) = map hd thmss
           |> chop (n - m)
           ||>> chop (n - m)
           ||>> chop (n - m2)
           ||>> chop (n - m2)
           ||>> chop (num_vars * (n - m3))
           ||>> chop (length bind_ts - m4)
-          ||>> apfst hd o chop 1
           ||> hd;
 
         fun map_id0_of_mr_bnf (Inl mrbnf) = [MRBNF_Def.map_id0_of_mrbnf mrbnf]
@@ -578,6 +581,99 @@ fun binder_inductive_cmd ((pred_name, binds_opt), perms_supps) no_defs_lthy =
 
         val perm_ids = map (fn thm => thm RS fun_cong RS @{thm trans[OF _ id_apply]}) perm_id0s;
 
+        val _ = @{print} (map snd perms)
+        val G_equiv =
+          Goal.prove_sorry lthy [] [] G_equiv_goal (fn {context=ctxt, ...} => EVERY1 [
+            K (Local_Defs.unfold0_tac ctxt [snd G]),
+            REPEAT_DETERM o EVERY' [
+              TRY o etac ctxt @{thm disj_forward},
+              SELECT_GOAL (print_tac ctxt "0"),
+              REPEAT_DETERM o eresolve_tac ctxt [exE, conjE],
+              K (print_tac ctxt "0.1"),
+              (*hyp_subst_tac ctxt,*)
+              REPEAT_DETERM_N (length param_Ts + 1) o etac ctxt @{thm subst[OF sym]},
+              K (print_tac ctxt "0.2"),
+              Subgoal.FOCUS_PARAMS (fn {context=ctxt, params, ...} =>
+                let
+                  val (fs, args) = map (Thm.term_of o snd) params
+                    |> drop 2
+                    |> chop 1
+                    ||> drop (length param_Ts);
+                  val (mr_bnfs, ts) = apfst (map snd o flat) (split_list (map (fn x => case find_index (curry (op=) (fastype_of x)) param_Ts of
+                    ~1 => (case find_index (curry (op=) (fastype_of x)) var_Ts of
+                      ~1 => apsnd (fn t => t $ x) (build_permute_for fs var_Ts (fastype_of x))
+                      | n => ([], nth fs n $ x))
+                    | n => ([], Term.list_comb (fst (nth perms n), fs) $ x)
+                  ) args));
+                  val equiv_commute = Named_Theorems.get ctxt "MRBNF_Recursor.equiv_commute";
+                  val equiv = Named_Theorems.get ctxt "MRBNF_Recursor.equiv" @ equiv_commute;
+                  val equiv_simps = Named_Theorems.get ctxt "MRBNF_Recursor.equiv_simps"
+                  val monos = Inductive.get_monos ctxt
+                  val set_maps = maps set_map_of_mr_bnf mr_bnfs;
+                  val _ = @{print} equiv
+                  val _ = @{print} (map (Thm.cterm_of ctxt) ts)
+                  val _ = @{print} set_maps
+                  val _ = @{print} (flat (map_filter (Option.map #permute_simps) param_sugars))
+                in EVERY1 [
+                  K (print_tac ctxt "1"),
+                  EVERY' (map (fn t => rtac ctxt (
+                    infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt t)] exI
+                  )) ts),
+                  K (print_tac ctxt "1.1"),
+                  SELECT_GOAL (Local_Defs.unfold0_tac ctxt (map snd perms)),
+                  rtac ctxt conjI,
+
+                  K (print_tac ctxt "1.2"),
+                  SELECT_GOAL (Local_Defs.unfold0_tac ctxt (@{thms image_Un} @ equiv_simps)),
+                  REPEAT_DETERM o rtac ctxt @{thm arg_cong2[of _ _ _ _ "(\<union>)"]},
+                  REPEAT_DETERM1 o EVERY' [
+                    K (print_tac ctxt "1.3"),
+                    resolve_tac ctxt @{thms image_single[symmetric] image_empty refl} ORELSE' EVERY' [
+                      resolve_tac ctxt (map (fn thm => thm RS sym) (set_maps @ equiv_simps) @ equiv_simps),
+                      REPEAT_DETERM o assume_tac ctxt
+                    ]
+                  ],
+                  K (print_tac ctxt "2"),
+                  K (Local_Defs.unfold0_tac ctxt @{thms id_apply}),
+                  K (Local_Defs.unfold0_tac ctxt @{thms id_def[symmetric]}),
+                  REPEAT_DETERM o EVERY' [
+                    TRY o rtac ctxt conjI,
+                    SELECT_GOAL (EVERY1 [
+                      K (print_tac ctxt "foo"),
+                      REPEAT_DETERM1 o (K (print_tac ctxt "wat") THEN' FIRST' [
+                        assume_tac ctxt,
+                        eresolve_tac ctxt [conjE],
+                        resolve_tac ctxt @{thms conjI refl TrueI bij_imp_bij_inv supp_inv_bound},
+                        rtac ctxt impI THEN' eresolve_tac ctxt @{thms injD[OF bij_is_inj, rotated -1]},
+                        EVERY' [
+                          SELECT_GOAL (Local_Defs.unfold0_tac ctxt (@{print}(map_filter (try (fn thm => thm RS sym)) equiv_commute))),
+                          REPEAT_DETERM1 o EVERY' [
+                            EqSubst.eqsubst_tac ctxt [0] (map (Local_Defs.unfold0 ctxt (map snd perms)) perm_comps),
+                            K (print_tac ctxt "comp"),
+                            REPEAT_DETERM1 o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms supp_inv_bound bij_imp_bij_inv})
+                          ],
+                          K (Local_Defs.unfold0_tac ctxt @{thms inv_o_simp1 inv_o_simp2 inv_simp1 inv_simp2}),
+                          K (Local_Defs.unfold0_tac ctxt (map (Local_Defs.unfold0 ctxt (map snd perms)) perm_ids)),
+                          K (print_tac ctxt "after_comp"),
+                          assume_tac ctxt
+                        ],
+                        eresolve_tac ctxt (map_filter (try (fn thm => Drule.rotate_prems ~1 thm)) equiv),
+                        CHANGED o SELECT_GOAL (Local_Defs.unfold0_tac ctxt (equiv @ equiv_simps @ flat (map_filter (Option.map #permute_simps) param_sugars))),
+                        (*EqSubst.eqsubst_tac ctxt [0] equiv,*)
+                        eresolve_tac ctxt (map (fn thm => Drule.rotate_prems ~1 (thm RS mp)) monos),
+                        resolve_tac ctxt monos,
+                        CHANGED o SELECT_GOAL (Local_Defs.unfold0_tac ctxt (flat (map_filter (Option.map (map (fn thm => thm RS sym) o #permute_simps)) param_sugars)))
+                      ])
+                    ])
+                  ],
+                  K (print_tac ctxt "3")
+                ] end
+              ) ctxt,
+              K (print_tac ctxt "4")
+            ]
+          ]);
+        val _ = @{print} G_equiv
+
         fun mk_induct mono = Drule.rotate_prems ~1 (
           apply_n @{thm le_funD} n (@{thm lfp_induct} OF [mono])
             RS @{thm le_boolD}

Tools/mrbnf_sugar.ML

@@ -427,7 +427,7 @@ fun create_binder_datatype (spec : spec) lthy =
       ])] end
     ) ctors_tys) ctors_tys));
 
-    (* TODO: map_bij (rename simps); injection *)
+    (* TODO: injection *)
 
     (* Term for variable substitution *)
     val x = length replace - #rec_vars spec;

thys/Infinitary_FOL/InfFOL.thy

@@ -231,9 +231,7 @@ unfolding kmember_def map_fun_def id_o o_id map_set\<^sub>k_def
 unfolding comp_def Abs_set\<^sub>k_inverse[OF UNIV_I]
 apply transfer apply transfer by blast
 
-lemma in_k_equiv: "isPerm \<sigma> \<Longrightarrow> rrename_ifol' \<sigma> f \<in>\<^sub>k map_set\<^sub>k (rrename_ifol' \<sigma>) \<Delta> = f \<in>\<^sub>k \<Delta>"
-  unfolding isPerm_def
-  apply (erule conjE)
+lemma in_k_equiv[equiv]: "bij (\<sigma>::'a::var_ifol'_pre \<Rightarrow> 'a) \<Longrightarrow> |supp \<sigma>| <o |UNIV::'a set| \<Longrightarrow> rrename_ifol' \<sigma> f \<in>\<^sub>k map_set\<^sub>k (rrename_ifol' \<sigma>) \<Delta> = f \<in>\<^sub>k \<Delta>"
   apply (rule iffI)
   apply (drule in_k_equiv'[rotated])
   apply (rule bij_imp_bij_inv)
@@ -251,13 +249,11 @@ lemma in_k_equiv: "isPerm \<sigma> \<Longrightarrow> rrename_ifol' \<sigma> f \<
   apply assumption
   done
 
-lemma in_k1_equiv': "bij \<sigma> \<Longrightarrow> f \<in>\<^sub>k\<^sub>1 F \<Longrightarrow> rrename_ifol' \<sigma> f \<in>\<^sub>k\<^sub>1 map_set\<^sub>k\<^sub>1 (rrename_ifol' \<sigma>) F"
+lemma in_k1_equiv'[equiv]: "bij \<sigma> \<Longrightarrow> f \<in>\<^sub>k\<^sub>1 F \<Longrightarrow> rrename_ifol' \<sigma> f \<in>\<^sub>k\<^sub>1 map_set\<^sub>k\<^sub>1 (rrename_ifol' \<sigma>) F"
 apply (unfold k1member_def map_fun_def comp_def id_def map_set\<^sub>k\<^sub>1_def Abs_set\<^sub>k\<^sub>1_inverse[OF UNIV_I])
 apply transfer apply transfer by blast
 
-lemma in_k1_equiv: "isPerm \<sigma> \<Longrightarrow> rrename_ifol' \<sigma> f \<in>\<^sub>k\<^sub>1 map_set\<^sub>k\<^sub>1 (rrename_ifol' \<sigma>) \<Delta> = f \<in>\<^sub>k\<^sub>1 \<Delta>"
-  unfolding isPerm_def
-  apply (erule conjE)
+lemma in_k1_equiv[equiv]: "bij (\<sigma>::'a::var_ifol'_pre \<Rightarrow> 'a) \<Longrightarrow> |supp \<sigma>| <o |UNIV::'a set| \<Longrightarrow> rrename_ifol' \<sigma> f \<in>\<^sub>k\<^sub>1 map_set\<^sub>k\<^sub>1 (rrename_ifol' \<sigma>) \<Delta> = f \<in>\<^sub>k\<^sub>1 \<Delta>"
   apply (rule iffI)
   apply (drule in_k1_equiv'[rotated])
   apply (rule bij_imp_bij_inv)
@@ -340,7 +336,7 @@ inductive deduct :: "ifol set\<^sub>k \<Rightarrow> ifol \<Rightarrow> bool" (in
 | AllE: "\<lbrakk> \<Delta> \<turnstile> All V f ; supp \<rho> \<subseteq> set\<^sub>k\<^sub>2 V \<rbrakk> \<Longrightarrow> \<Delta> \<turnstile> f\<lbrakk>\<rho>\<rbrakk>"
 
 binder_inductive deduct
-  subgoal for R B \<sigma> x1 x2
+(*  subgoal for R B \<sigma> x1 x2
     unfolding induct_rulify_fallback split_beta
     apply (elim disj_forward exE)
           apply (auto simp: ifol'.rrename_comps in_k_equiv in_k_equiv' isPerm_def ifol'.rrename_ids supp_inv_bound)
@@ -412,8 +408,8 @@ binder_inductive deduct
       apply (metis ifol'.rrename_bijs ifol'.rrename_inv_simps inv_simp1 set\<^sub>k.map_ident_strong)
       apply (erule image_mono)
       done
-    done
-  subgoal premises prems for R B \<Delta> x2
+    done*)
+(*  subgoal premises prems for R B \<Delta> x2
     using prems(2-) unfolding induct_rulify_fallback split_beta
     unfolding ex_push_inwards conj_disj_distribL ex_disj_distrib
     apply (elim disj_forward)
@@ -602,7 +598,12 @@ binder_inductive deduct
         by (smt (verit) Int_iff Un_Int_eq(1) X_def \<sigma>_def bij_betw_apply disjoint_iff image_iff)
     qed
     done
-  done
+  done*)
+  sorry
+
+lemma all_mono_bij:
+  "bij f \<Longrightarrow> (\<And>x. P x \<longrightarrow> Q (f x)) \<Longrightarrow> (\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x)"
+  by (metis bij_pointE)
 
 thm deduct.strong_induct
 thm deduct.equiv

thys/Infinitary_Lambda_Calculus/ILC.thy

@@ -71,7 +71,6 @@ lemma inj_embed: "inj embed"
   unfolding embed_def
   by (rule someI_ex[OF ex_inj_infinite_regular_var_iterm_pre[where 'a='a]])
 
-
 (****************************)
 (* DATATYPE-SPECIFIC CUSTOMIZATION  *)
 
@@ -831,11 +830,11 @@ unfolding imkSubst_def by auto
 lemma card_dsset_ivar: "|dsset xs| <o |UNIV::ivar set|"
 using countable_card_ivar countable_card_le_natLeq dsset_natLeq by auto
 
-lemma SSupp_imkSubst[simp,intro]: "|SSupp (imkSubst xs es)| <o |UNIV::ivar set|"
+lemma SSupp_imkSubst[simp,intro]: "|SSupp (imkSubst xs es)| <o |UNIV::'a::var_iterm_pre set|"
 proof-
   have "SSupp (imkSubst xs es) \<subseteq> dsset xs"
   unfolding SSupp_def by auto (metis imkSubst_idle)
-  thus ?thesis by (simp add: card_of_subset_bound card_dsset_ivar)
+  thus ?thesis by (simp add: card_of_subset_bound dsset_card_ls)
 qed
 
 lemma imkSubst_smap_irrename:
@@ -947,7 +946,16 @@ proof-
         imkSubst_idle imkSubst_smap iterm.set(3) not_imageI) . . .
 qed
 
-
+lemma irrename_itvsubst[equiv_commute]:
+  fixes \<sigma>::"ivar \<Rightarrow> ivar"
+  shows "bij \<sigma> \<Longrightarrow> |supp \<sigma>| <o |UNIV::ivar set|
+  \<Longrightarrow> irrename \<sigma> (itvsubst (imkSubst xs es2) e1) = itvsubst (imkSubst (dsmap \<sigma> xs) (smap (irrename \<sigma>) es2)) (irrename \<sigma> e1)"
+  apply (rule trans)
+   apply (rule box_equals[OF iterm.rrename_tvsubst[THEN fun_cong] comp_apply comp_apply])
+     apply assumption+
+   apply (rule SSupp_imkSubst)
+  apply (rule arg_cong2[OF _ refl, of _ _ itvsubst])
+  using imkSubst_smap_irrename[symmetric, of \<sigma>] by auto
 
 (* RECURSOR PREPARATIONS: *)
 

thys/Infinitary_Lambda_Calculus/ILC_Beta.thy

@@ -25,41 +25,6 @@ inductive istep :: "itrm \<Rightarrow> itrm \<Rightarrow> bool" where
 | Xi: "istep e e' \<Longrightarrow> istep (iLam xs e) (iLam xs e')"
 
 binder_inductive istep
-  subgoal for R B \<sigma> x1 x2
-    apply (elim disj_forward exE conjE)
-    subgoal for xs e1 es2
-        apply(rule exI[of _ "dsmap \<sigma> xs"])
-        apply(rule exI[of _ "irrename \<sigma> e1"])
-        apply(rule exI[of _ "smap (irrename \<sigma>) es2"])
-        apply (simp add: iterm.rrename_comps) apply(subst irrename_itvsubst_comp) apply auto
-        apply(subst imkSubst_smap_irrename_inv) unfolding isPerm_def apply auto
-        apply(subst irrename_eq_itvsubst_iVar'[of _ e1]) unfolding isPerm_def apply auto
-        apply(subst itvsubst_comp)
-        subgoal by (metis SSupp_imkSubst imkSubst_smap_irrename_inv)
-        subgoal by (smt (verit, best) SSupp_def VVr_eq_Var card_of_subset_bound mem_Collect_eq not_in_supp_alt o_apply subsetI)
-        subgoal apply(rule itvsubst_cong)
-          subgoal using SSupp_irrename_bound by blast
-          subgoal using card_SSupp_itvsubst_imkSubst_irrename_inv isPerm_def by auto
-          subgoal for x apply simp apply(subst iterm.subst(1))
-            subgoal using card_SSupp_imkSubst_irrename_inv[unfolded isPerm_def] by auto
-            subgoal by simp . . .
-      (* *)
-  subgoal for e1 e1' es2
-      apply(rule exI[of _ "irrename \<sigma> e1"]) apply(rule exI[of _ "irrename \<sigma> e1'"])
-      apply(rule exI[of _ "smap (irrename \<sigma>) es2"])
-      by (simp add: iterm.rrename_comps)
-    (* *)
-  subgoal for es2 i e2' e1
-      apply(rule exI[of _ "smap (irrename \<sigma>) es2"])
-      apply(rule exI[of _ i])
-      apply(rule exI[of _ "irrename \<sigma> e2'"])
-      apply(rule exI[of _ "irrename \<sigma> e1"])
-      apply (simp add: iterm.rrename_comps) .
-    (* *)
-  subgoal for e e' xs
-      apply(rule exI[of _ "irrename \<sigma> e"]) apply(rule exI[of _ "irrename \<sigma> e'"])
-      apply(rule exI[of _ "dsmap \<sigma> xs"])
-      by (simp add: iterm.rrename_comps) .
   subgoal premises prems for R B x1 x2
     using prems(2-) apply safe
     subgoal for xs e1 es2

thys/Infinitary_Lambda_Calculus/ILC_affine.thy

@@ -22,7 +22,8 @@ inductive affine  :: "itrm \<Rightarrow> bool" where
  affine (iApp e1 es2)"
 
 binder_inductive affine
-  unfolding isPerm_def induct_rulify_fallback
+
+  (*unfolding isPerm_def induct_rulify_fallback
   subgoal for R B \<sigma> t
     apply(elim disjE)
     subgoal apply(rule disjI3_1)
@@ -50,7 +51,7 @@ binder_inductive affine
         done
       done
     done
-  done
+  done*)
   subgoal premises prems for R B t
     using prems(2-)
      apply safe

thys/MRBNF_Recursor.thy

@@ -10,6 +10,18 @@ ML_file \<open>../Tools/mrbnf_vvsubst.ML\<close>
 ML_file \<open>../Tools/mrbnf_tvsubst.ML\<close>
 ML_file \<open>../Tools/mrbnf_sugar.ML\<close>
 
+named_theorems equiv
+named_theorems equiv_commute
+named_theorems equiv_simps
+
+declare Un_iff[equiv_simps] de_Morgan_disj[equiv_simps]
+  inj_image_mem_iff[OF bij_is_inj, equiv_simps]
+  singleton_iff[equiv_simps] image_empty[equiv_simps]
+  Int_Un_distrib[equiv_simps] Un_empty[equiv_simps]
+  image_is_empty[equiv_simps] image_Int[OF bij_is_inj, symmetric, equiv_simps]
+  inj_eq[OF bij_is_inj, equiv_simps] inj_eq[OF bij_is_inj, equiv_simps]
+  image_insert[equiv_simps] insert_iff[equiv_simps] notin_empty_eq_True[equiv_simps]
+
 context begin
 ML_file \<open>../Tools/binder_induction.ML\<close>
 end