Add basic automation for injection theorems

Tools/mrbnf_sugar.ML

@@ -21,6 +21,7 @@ type binder_sugar = {
   mrbnf: MRBNF_Def.mrbnf,
   strong_induct: thm option,
   distinct: thm list,
+  inject: thm list,
   ctors: (term * thm) list
 };
 
@@ -63,11 +64,12 @@ type binder_sugar = {
   mrbnf: MRBNF_Def.mrbnf,
   strong_induct: thm option,
   distinct: thm list,
+  inject: thm list,
   ctors: (term * thm) list
 };
 
 fun morph_binder_sugar phi { map_simps, permute_simps, set_simpss, subst_simps, mrbnf,
-  strong_induct, distinct, ctors, bsetss, bset_bounds } = {
+  strong_induct, distinct, inject, ctors, bsetss, bset_bounds } = {
   map_simps = map (Morphism.thm phi) map_simps,
   permute_simps = map (Morphism.thm phi) permute_simps,
   set_simpss = map (map (Morphism.thm phi)) set_simpss,
@@ -77,6 +79,7 @@ fun morph_binder_sugar phi { map_simps, permute_simps, set_simpss, subst_simps,
   mrbnf = MRBNF_Def.morph_mrbnf phi mrbnf,
   strong_induct = Option.map (Morphism.thm phi) strong_induct,
   distinct = map (Morphism.thm phi) distinct,
+  inject = map (Morphism.thm phi) inject,
   ctors = map (map_prod (Morphism.term phi) (Morphism.thm phi)) ctors
 } : binder_sugar;
 
@@ -451,7 +454,69 @@ fun create_binder_datatype (spec : spec) lthy =
       ])] end
     ) ctors_tys) ctors_tys));
 
-    (* TODO: map_bij (rename simps); injection *)
+    val inject = map_filter (fn ((ctor, ctor_def), tys) => if null tys then NONE else try (fn () =>
+      let
+        val tys' = map (Term.typ_subst_atomic replace) tys;
+        val ((xs, ys), _) = names_lthy
+          |> mk_Frees "x" tys'
+          ||>> mk_Frees "y" tys';
+        val ys' = @{map 3} (fn ty => fn x => fn y =>
+          if exists (member (op=) bounds o TFree) (Term.add_tfreesT ty []) then 
+            (if member (op=) bounds ty then x else raise TYPE ("typ contains binder", [ty], [])) else y
+        ) tys xs ys;
+        val xs_ys' = @{map_filter 2} (fn x => fn y' => if x = y' then NONE else SOME (x, y')) xs ys';
+
+        val goal = mk_Trueprop_eq (
+          HOLogic.mk_eq (Term.list_comb (ctor, xs), Term.list_comb (ctor, ys')),
+          foldr1 HOLogic.mk_conj (map HOLogic.mk_eq xs_ys')
+        );
+      in Goal.prove_sorry lthy (names (xs @ map snd xs_ys')) [] goal (fn {context=ctxt, ...} => EVERY1 [
+        K (Local_Defs.unfold0_tac ctxt [ctor_def, #inject quotient]),
+        K (Local_Defs.unfold0_tac ctxt (
+          @{thms map_sum.simps map_prod_simp comp_def sum_set_simps cSup_singleton Union_empty
+            Un_empty_left Un_empty_right Diff_empty UN_empty id_apply sum.inject prod.inject
+            prod_set_simps UN_single id_def[symmetric] UN_single UN_singleton
+          }
+          @ maps MRBNF_Def.set_map_of_mrbnf fp_nesting_mrbnfs
+          @ map MRBNF_Def.map_id_of_mrbnf fp_nesting_mrbnfs
+          @ MRBNF_Def.set_defs_of_mrbnf pre_mrbnf
+          @ [#Abs_inverse (snd info) OF @{thms UNIV_I}, #Abs_inject (snd info) OF @{thms UNIV_I UNIV_I},
+            MRBNF_Def.map_def_of_mrbnf pre_mrbnf
+          ]
+        )),
+        rtac ctxt iffI,
+        SELECT_GOAL (EVERY1 [
+          REPEAT_DETERM o eresolve_tac ctxt [exE, conjE],
+          REPEAT_DETERM o (TRY o rtac ctxt conjI THEN' assume_tac ctxt),
+          IF_UNSOLVED o EVERY' [
+            rotate_tac ~1,
+            dtac ctxt @{thm trans[rotated]},
+            rtac ctxt sym,
+            resolve_tac ctxt (#permute_cong_id (#inner quotient) :: map (fn mrbnf =>
+              trans OF [MRBNF_Def.map_cong_of_mrbnf mrbnf, MRBNF_Def.map_id_of_mrbnf mrbnf]
+            ) fp_nesting_mrbnfs),
+            REPEAT_DETERM o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms supp_id_bound bij_id}),
+            TRY o rtac ctxt refl,
+            K (Local_Defs.unfold0_tac ctxt @{thms id_apply}),
+            REPEAT_DETERM o EVERY' [
+              dtac ctxt @{thm id_on_Diff},
+              rtac ctxt @{thm id_onI},
+              dtac ctxt @{thm singletonD},
+              hyp_subst_tac ctxt,
+              assume_tac ctxt,
+              etac ctxt @{thm id_onD},
+              REPEAT_DETERM o assume_tac ctxt
+            ]
+          ]
+        ]),
+        REPEAT_DETERM o rtac ctxt @{thm exI[of _ id]},
+        REPEAT_DETERM o etac ctxt conjE,
+        REPEAT_DETERM o (resolve_tac ctxt (
+          (trans OF [#permute_id quotient]) :: @{thms id_apply conjI supp_id_bound bij_id id_on_id}
+          @ map (fn mrbnf => trans OF [MRBNF_Def.map_id_of_mrbnf mrbnf]) fp_nesting_mrbnfs
+        ) ORELSE' assume_tac ctxt)
+      ]) end) ()
+    ) ctors_tys;
 
     (* Term for variable substitution *)
     val x = length replace - #rec_vars spec;
@@ -778,6 +843,7 @@ fun create_binder_datatype (spec : spec) lthy =
       bset_bounds = [],
       mrbnf = mrbnf,
       distinct = distinct,
+      inject = inject,
       ctors = ctors
     } : binder_sugar;
 
@@ -793,7 +859,8 @@ fun create_binder_datatype (spec : spec) lthy =
       @ [("set", flat set_simpss, simp),
         ("map", map_simps, simp),
         ("permute", permute_simps, simp),
-        ("distinct", distinct, simp)
+        ("distinct", distinct, simp),
+        ("inject", inject, simp)
       ] @ the_default [] (Option.map (fn (_, tvsubst_simps) => [("subst", tvsubst_simps, simp)]) tvsubst_opt)
       ) |> (map (fn (thmN, thms, attrs) =>
         ((Binding.qualify true (Binding.name_of (#fp_b spec)) (Binding.name thmN), attrs), [(thms, [])])

operations/BMV_Monad.thy

@@ -0,0 +1,96 @@
+theory BMV_Monad
+  imports "Binders.MRBNF_Recursor"
+begin
+
+declare [[mrbnf_internals]]
+binder_datatype 'a FType
+  = TyVar 'a
+  | TyApp "'a FType" "'a FType"
+  | TyAll a::'a t::"'a FType" binds a in t
+
+(*
+SOps = { 'a FType }
+L = 'a FType
+m = 1
+*)
+abbreviation Inj_FType_1 :: "'tyvar::var \<Rightarrow> 'tyvar FType" where "Inj_FType_1 \<equiv> TyVar"
+abbreviation Sb_FType :: "('tyvar::var \<Rightarrow> 'tyvar FType) \<Rightarrow> 'tyvar FType \<Rightarrow> 'tyvar FType" where "Sb_FType \<equiv> tvsubst_FType"
+abbreviation Vrs_FType_1 :: "'tyvar::var FType \<Rightarrow> 'tyvar set" where "Vrs_FType_1 \<equiv> FVars_FType"
+
+lemma SSupp_Inj_FType[simp]: "SSupp_FType Inj_FType_1 = {}" unfolding SSupp_FType_def tvVVr_tvsubst_FType_def TyVar_def tv\<eta>_FType_tvsubst_FType_def by simp
+lemma IImsupp_Inj_FType[simp]: "IImsupp_FType Inj_FType_1 = {}" unfolding IImsupp_FType_def by simp
+lemma SSupp_IImsupp_bound[simp]:
+  fixes \<rho>::"'tyvar::var \<Rightarrow> 'tyvar FType"
+  assumes "|SSupp_FType \<rho>| <o |UNIV::'tyvar set|"
+  shows "|IImsupp_FType \<rho>| <o |UNIV::'tyvar set|"
+  unfolding IImsupp_FType_def using assms by (auto simp: FType.Un_bound FType.UN_bound FType.set_bd_UNIV)
+
+lemma SSupp_comp_subset:
+  fixes \<rho> \<rho>'::"'tyvar::var \<Rightarrow> 'tyvar FType"
+  assumes "|SSupp_FType \<rho>| <o |UNIV::'tyvar set|"
+  shows "SSupp_FType (tvsubst_FType \<rho> \<circ> \<rho>') \<subseteq> SSupp_FType \<rho> \<union> SSupp_FType \<rho>'"
+  unfolding SSupp_FType_def tvVVr_tvsubst_FType_def tv\<eta>_FType_tvsubst_FType_def comp_def
+  apply (unfold TyVar_def[symmetric])
+  apply (rule subsetI)
+  apply (unfold mem_Collect_eq)
+  apply simp
+  using assms(1) by force
+lemma SSupp_comp_bound[simp]:
+  fixes \<rho> \<rho>'::"'tyvar::var \<Rightarrow> 'tyvar FType"
+  assumes "|SSupp_FType \<rho>| <o |UNIV::'tyvar set|" "|SSupp_FType \<rho>'| <o |UNIV::'tyvar set|"
+  shows "|SSupp_FType (tvsubst_FType \<rho> \<circ> \<rho>')| <o |UNIV::'tyvar set|"
+  using assms SSupp_comp_subset by (metis card_of_subset_bound var_class.Un_bound)
+
+lemma Sb_Inj_FType: "Sb_FType Inj_FType_1 = id"
+  apply (rule ext)
+  subgoal for x
+    apply (induction x)
+    by auto
+  done
+lemma Sb_comp_Inj_FType:
+  fixes \<rho>::"'tyvar::var \<Rightarrow> 'tyvar FType"
+  assumes "|SSupp_FType \<rho>| <o |UNIV::'tyvar set|"
+  shows "Sb_FType \<rho> \<circ> Inj_FType_1 = \<rho>"
+  using assms by auto
+
+lemma Sb_comp_FType:
+  fixes \<rho> \<rho>'::"'tyvar::var \<Rightarrow> 'tyvar FType"
+  assumes "|SSupp_FType \<rho>| <o |UNIV::'tyvar set|" "|SSupp_FType \<rho>'| <o |UNIV::'tyvar set|"
+  shows "Sb_FType \<rho> \<circ> Sb_FType \<rho>' = Sb_FType (Sb_FType \<rho> \<circ> \<rho>')"
+  apply (rule ext)
+  apply (rule trans[OF comp_apply])
+  subgoal for x
+    apply (binder_induction x avoiding: "IImsupp_FType \<rho>" "IImsupp_FType \<rho>'" "IImsupp_FType (Sb_FType \<rho> \<circ> \<rho>')" rule: FType.strong_induct)
+    using assms by (auto simp: IImsupp_FType_def FType.Un_bound FType.UN_bound FType.set_bd_UNIV)
+  done
+
+lemma Vrs_Inj_FType: "Vrs_FType_1 (Inj_FType_1 a) = {a}"
+  by simp
+
+lemma Vrs_Sb_FType:
+  fixes \<rho>::"'tyvar::var \<Rightarrow> 'tyvar FType"
+  assumes "|SSupp_FType \<rho>| <o |UNIV::'tyvar set|"
+  shows "Vrs_FType_1 (Sb_FType \<rho> x) = (\<Union>a\<in>Vrs_FType_1 x. Vrs_FType_1 (\<rho> a))"
+proof (binder_induction x avoiding: "IImsupp_FType \<rho>" rule: FType.strong_induct)
+  case (TyAll x1 x2)
+  then show ?case using assms by (auto intro!: FType.IImsupp_Diff[symmetric])
+qed (auto simp: assms)
+
+lemma Sb_cong_FType:
+  fixes \<rho> \<rho>'::"'tyvar::var \<Rightarrow> 'tyvar FType"
+  assumes "|SSupp_FType \<rho>| <o |UNIV::'tyvar set|" "|SSupp_FType \<rho>'| <o |UNIV::'tyvar set|"
+  and "\<And>a. a \<in> Vrs_FType_1 t \<Longrightarrow> \<rho> a = \<rho>' a"
+  shows "Sb_FType \<rho> t = Sb_FType \<rho>' t"
+using assms(3) proof (binder_induction t avoiding: "IImsupp_FType \<rho>" "IImsupp_FType \<rho>'" rule: FType.strong_induct)
+  case (TyAll x1 x2)
+  then show ?case using assms apply auto
+    by (smt (verit, ccfv_threshold) CollectI IImsupp_FType_def SSupp_FType_def Un_iff)
+qed (auto simp: assms(1-2))
+
+(* *)
+
+type_synonym ('var, 'tyvar, 'bvar, 'btyvar, 'rec, 'brec) FTerm_pre' = "('var + 'rec * 'rec + 'btyvar * 'brec) + ('bvar * 'tyvar FType * 'brec + 'rec * 'tyvar FType)"
+
+
+
+end

operations/Sugar.thy

@@ -521,6 +521,140 @@ lemma T2_distinct[simp]:
                       apply (rule notI, (erule exE conjE sum.distinct[THEN notE])+)+
   done
 
+lemmas map_id0_nesting = list.map_id0 prod.map_id0
+lemmas set_map_nesting = list.set_map prod.set_map
+
+lemma T1_inject[simp]:
+  "(Var_T1 x = Var_T1 y) = (x = y)"
+  "(TyVar_T1 x2 = TyVar_T1 y2) = (x2 = y2)"
+  "(App_T1 x3 x4 = App_T1 y3 y4) = (x3 = y3 \<and> x4 = y4)"
+  "(BFree_T1 x xs = BFree_T1 x ys) = (xs = ys)"
+  "(Lam_T1 x x3 = Lam_T1 x y3) = (x3 = y3)"
+  "(TyLam_T1 x2 x3 = TyLam_T1 x2 y3) = (x3 = y3)"
+  "(Ext_T1 x5 = Ext_T1 y5) = (x5 = y5)"
+        apply (unfold T1_ctors_defs TT_inject0s)
+        apply (unfold map_T1_pre_def comp_def map_sum.simps map_prod_simp Abs_T1_pre_inverse[OF UNIV_I]
+      set_simp_thms T1_pre_set_defs id_apply Abs_T1_pre_inject[OF UNIV_I UNIV_I] sum.inject prod.inject
+      set_map_nesting
+      )
+        apply (unfold id_def[symmetric])
+    (* REPEAT_DETERM *)
+        apply (rule iffI)
+         apply (erule exE conjE)+
+         apply ((rule conjI)?, assumption)+
+        apply (rule exI[of _ id])+
+        apply ((erule conjE)+)?
+        apply (rule conjI bij_id supp_id_bound id_on_id | assumption)+
+    (* repeated *)
+       apply (rule iffI)
+        apply (erule exE conjE)+
+        apply ((rule conjI)?, assumption)+
+       apply (rule exI[of _ id])+
+       apply ((erule conjE)+)?
+       apply (rule conjI bij_id supp_id_bound id_on_id | assumption)+
+    (* repeated *)
+      apply (rule iffI)
+       apply (erule exE conjE)+
+       apply ((rule conjI)?, assumption)+
+      apply (rule exI[of _ id])+
+      apply (erule conjE)+
+      apply (rule conjI bij_id supp_id_bound id_on_id | assumption)+
+    (* repeated *)
+     apply (rule iffI)
+      apply (erule exE conjE)+
+      apply hypsubst_thin
+      apply (rule sym)
+      apply ((rule trans[OF list.map_cong[OF refl] list.map_id] trans[OF prod.map_cong[OF refl] prod.map_id], rule trans[rotated, OF id_apply[symmetric]])+)?
+       apply (drule id_on_Diff)
+        apply (rule id_onI)
+        apply (drule singletonD)
+        apply hypsubst
+        apply assumption
+       apply (erule id_onD)
+       apply (rule UN_I)
+        apply assumption+
+      apply (rule refl)
+     apply (rule exI[of _ id])+
+     apply ((erule conjE)+)?
+     apply (unfold list.map_id0 prod.map_id0)
+     apply (rule conjI bij_id supp_id_bound id_on_id trans[OF id_apply] refl | assumption)+
+    (* repeated *)
+    apply (rule iffI)
+     apply (erule exE conjE)+
+     apply hypsubst_thin
+     apply (rule sym)
+     apply ((rule trans[OF list.map_cong[OF refl] list.map_id] trans[OF prod.map_cong[OF refl] prod.map_id], rule trans[rotated, OF id_apply[symmetric]])+)?
+     apply (rule permute_cong_ids)
+          apply assumption+
+    (* REPEAT_DETERM *)
+      apply (drule id_on_Diff)
+       apply (rule id_onI)
+       apply (drule singletonD)
+       apply hypsubst
+       apply assumption
+      apply (erule id_onD)
+      apply (rule UN_I)?
+      apply assumption+
+    (* repeated *)
+     apply (drule id_on_Diff)
+      apply (rule id_onI)
+      apply (drule singletonD)
+      apply hypsubst
+      apply assumption
+     apply (erule id_onD)
+     apply (rule UN_I)?
+     apply assumption+
+    (* END REPEAT_DETERM *)
+    apply (rule exI[of _ id])+
+    apply ((erule conjE)+)?
+    apply (unfold list.map_id0 prod.map_id0 permute_id0s)?
+    apply (rule conjI bij_id supp_id_bound id_on_id trans[OF id_apply] refl | assumption)+
+    (* repeated *)
+   apply (rule iffI)
+    apply (erule exE conjE)+
+    apply hypsubst_thin
+    apply (rule sym)
+    apply ((rule trans[OF list.map_cong[OF refl] list.map_id] trans[OF prod.map_cong[OF refl] prod.map_id], rule trans[rotated, OF id_apply[symmetric]])+)?
+    apply (rule permute_cong_ids)
+         apply assumption+
+    (* REPEAT_DETERM *)
+     apply (drule id_on_Diff)
+      apply (rule id_onI)
+      apply (drule singletonD)
+      apply hypsubst
+      apply assumption
+     apply (erule id_onD)
+     apply (rule UN_I)?
+     apply assumption+
+    (* repeated *)
+    apply (drule id_on_Diff)
+     apply (rule id_onI)
+     apply (drule singletonD)
+     apply hypsubst
+     apply assumption
+    apply (erule id_onD)
+    apply (rule UN_I)?
+    apply assumption+
+    (* END REPEAT_DETERM *)
+   apply (rule exI[of _ id])+
+   apply ((erule conjE)+)?
+   apply (unfold list.map_id0 prod.map_id0 permute_id0s)?
+   apply (rule conjI bij_id supp_id_bound id_on_id trans[OF id_apply] refl | assumption)+
+    (* repeated *)
+  apply (rule iffI)
+   apply (erule exE conjE)+
+   apply hypsubst_thin
+   apply (rule sym)
+   apply ((rule trans[OF list.map_cong[OF refl] list.map_id] trans[OF prod.map_cong[OF refl] prod.map_id], rule trans[rotated, OF id_apply[symmetric]])+)?
+   apply (rule permute_cong_ids, assumption+)?
+   apply (rule refl)?
+  apply (rule exI[of _ id])+
+  apply ((erule conjE)+)?
+  apply (unfold list.map_id0 prod.map_id0 permute_id0s)?
+  apply (rule conjI bij_id supp_id_bound id_on_id trans[OF id_apply] refl | assumption)+
+    (* END REPEAT_DETERM *)
+  done
+
 abbreviation eta11 :: "'a \<Rightarrow> ('a::var, 'b::var, 'c::var, 'd, 'e::var, 'f::var, 'g::var, 'h, 'i, 'j, 'k) T1_pre" where
   "eta11 x \<equiv> Abs_T1_pre (Inl (Inl (Inl x)))"
 abbreviation eta12 :: "'b \<Rightarrow> ('a::var, 'b::var, 'c::var, 'd, 'e::var, 'f::var, 'g::var, 'h, 'i, 'j, 'k) T1_pre" where
@@ -664,8 +798,6 @@ print_theorems
 
 lemmas prod_sum_simps = prod.set_map sum.set_map prod_set_simps sum_set_simps UN_empty UN_empty2
   Un_empty_left Un_empty_right UN_singleton comp_def map_sum.simps map_prod_simp UN_single
-lemmas map_id0_nesting = list.map_id0 prod.map_id0
-lemmas set_map_nesting = list.set_map prod.set_map
 
 lemma map_simps[simp]:
   fixes f1::"'a::var \<Rightarrow> 'a" and f2::"'b::var \<Rightarrow> 'b" and f3::"'c::var \<Rightarrow> 'c" and f4::"'d \<Rightarrow> 'e"

thys/Infinitary_FOL/InfFOL.thy

@@ -339,10 +339,6 @@ binder_inductive deduct
     unfolding induct_rulify_fallback split_beta
     apply (elim disj_forward exE)
           apply (auto simp: ifol'.permute_comp in_k_equiv in_k_equiv' isPerm_def ifol'.permute_id supp_inv_bound)
-         apply (rule exI)
-         apply (rule conjI)
-          apply (rule refl)
-         apply (rule allI impI)+
          apply (unfold set\<^sub>k.map_comp)
          apply (subst ifol'.permute_comp0)
              apply (assumption | rule bij_imp_bij_inv supp_inv_bound)+