# HG changeset patch # User traytel # Date 1691502541 -7200 # Node ID da437a9f2823a4b81c6d8ce7b1c5ccc2cbce7243 # Parent e72f8009a4f0b719d3c1a4cf62eb2ef60e5bfca3 made another two tactics more robust in presence of BNFs nesting live variables (reported by Wolfgang Jeltsch) diff -r e72f8009a4f0 -r da437a9f2823 src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML --- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML Mon Aug 07 23:43:19 2023 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML Tue Aug 08 15:49:01 2023 +0200 @@ -136,7 +136,7 @@ fun mk_abs_transfer ctxt fpT_name = let - val SOME {pre_bnf, absT_info = {absT, repT, abs, type_definition, ...}, ...} = + val SOME {pre_bnf, absT_info = {absT, repT, abs, type_definition, ...}, live_nesting_bnfs,...} = fp_sugar_of ctxt fpT_name; in if absT = repT then @@ -144,6 +144,7 @@ else let val rel_def = rel_def_of_bnf pre_bnf; + val live_nesting_rel_eqs = map rel_eq_of_bnf live_nesting_bnfs; val absT = T_of_bnf pre_bnf |> singleton (freeze_types ctxt (map dest_TVar (lives_of_bnf pre_bnf))); @@ -152,7 +153,7 @@ in Variable.add_free_names ctxt goal [] |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} => - unfold_thms_tac ctxt [rel_def] THEN + unfold_thms_tac ctxt (rel_def :: live_nesting_rel_eqs) THEN HEADGOAL (rtac ctxt refl ORELSE' rtac ctxt (@{thm Abs_transfer} OF [type_definition, type_definition])))) end @@ -160,13 +161,15 @@ fun mk_rep_transfer ctxt fpT_name = let - val SOME {pre_bnf, absT_info = {absT, repT, rep, ...}, ...} = fp_sugar_of ctxt fpT_name; + val SOME {pre_bnf, absT_info = {absT, repT, rep, ...}, live_nesting_bnfs, ...} = + fp_sugar_of ctxt fpT_name; in if absT = repT then raise Fail "no abs/rep" else let val rel_def = rel_def_of_bnf pre_bnf; + val live_nesting_rel_eqs = map rel_eq_of_bnf live_nesting_bnfs; val absT = T_of_bnf pre_bnf |> singleton (freeze_types ctxt (map dest_TVar (lives_of_bnf pre_bnf))); @@ -175,7 +178,7 @@ in Variable.add_free_names ctxt goal [] |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} => - unfold_thms_tac ctxt [rel_def] THEN + unfold_thms_tac ctxt (rel_def :: live_nesting_rel_eqs) THEN HEADGOAL (rtac ctxt refl ORELSE' rtac ctxt @{thm vimage2p_rel_fun}))) end end;