Fix ILC proof

Author: jvanbruegge

Tools/bmv_monad_def.ML

@@ -945,7 +945,7 @@ fun mk_bmv_monad const_policy fact_policy qualify bmv_b_opt (model: thm bmv_mona
             rtac ctxt @{thm UN_mono},
             resolve_tac ctxt (the SSupp_Map_subsets),
             K (Local_Defs.unfold0_tac ctxt (@{thms comp_apply} @ #Vrs_Map (the params))),
-            rtac ctxt subset_refl
+            rtac ctxt @{thm subset_refl}
           ]) end
         ) (RVrs @ Vrs))) Injs rhos) (Option.map #Map param_consts);
 
@@ -2061,8 +2061,8 @@ fun compose_bmv_monad qualify (outer : bmv_monad) (inners : (bmv_monad, typ) eit
                 assume_tac ctxt,
                 REPEAT_DETERM o FIRST' [
                   assume_tac ctxt,
-                  eresolve_tac ctxt [UnI1, UnI2],
-                  rtac ctxt UnI1
+                  eresolve_tac ctxt @{thms UnI1 UnI2},
+                  rtac ctxt @{thm UnI1}
                 ]
               ]
             ]) inners),
@@ -2072,8 +2072,8 @@ fun compose_bmv_monad qualify (outer : bmv_monad) (inners : (bmv_monad, typ) eit
               REPEAT_DETERM o FIRST' [
                 assume_tac ctxt,
                 resolve_tac ctxt (refl :: @{thms SSupp_Inj_bound IImsupp_Inj_bound} @ prems),
-                eresolve_tac ctxt [UnI1, UnI2],
-                rtac ctxt UnI1
+                eresolve_tac ctxt @{thms UnI1 UnI2},
+                rtac ctxt @{thm UnI1}
               ]
             ]
           ]) ctxt

case_studies/Infinitary_Lambda_Calculus/ILC.thy

@@ -653,7 +653,7 @@ assumes \<sigma>: "bij \<sigma>" "|supp \<sigma>| <o |UNIV::ivar set|"
 shows "irrename \<sigma> (usub t u (x::ivar)) = usub (irrename \<sigma> t) (\<sigma> u) (\<sigma> x)"
 using assms
 apply(induct t rule: iterm.fresh_induct[where A = "{x,u} \<union> supp \<sigma>"])
-  subgoal using assms by simp (meson le_UNIV_insert)
+  subgoal using assms by simp
   subgoal by (auto simp: sb_def bij_implies_inject)
   subgoal using assms apply simp unfolding stream.map_comp apply(rule stream.map_cong0) by auto
   subgoal using assms apply(subst usub_iLam) apply auto apply(subst usub_iLam) by (auto simp: bij_implies_inject) .