# HG changeset patch # User nipkow # Date 1636291571 -3600 # Node ID f05c73bf5968df6168a9b72f64d7b996fcaa86f7 # Parent 15beb1ef5ad1accda53328eb8f44cc40db2ffd13 Preserve variable name z in VAR {z = t} diff -r 15beb1ef5ad1 -r f05c73bf5968 src/HOL/Hoare/Hoare_Logic.thy --- a/src/HOL/Hoare/Hoare_Logic.thy Sun Nov 07 10:07:09 2021 +0100 +++ b/src/HOL/Hoare/Hoare_Logic.thy Sun Nov 07 14:26:11 2021 +0100 @@ -134,8 +134,8 @@ assumes "p \ i" and "\n::nat . ValidTC (i \ b \ {s . v s = n}) c (A n) (i \ {s . v s < n})" and "i \ uminus b \ q" - shows "ValidTC p (While b c) (Awhile i v A) q" -proof - + shows "ValidTC p (While b c) (Awhile i v (\n. A n)) q" +proof - { fix s n have "s \ i \ v s = n \ (\t . Sem (While b c) s t \ t \ q)" diff -r 15beb1ef5ad1 -r f05c73bf5968 src/HOL/Hoare/hoare_syntax.ML --- a/src/HOL/Hoare/hoare_syntax.ML Sun Nov 07 10:07:09 2021 +0100 +++ b/src/HOL/Hoare/hoare_syntax.ML Sun Nov 07 14:26:11 2021 +0100 @@ -99,7 +99,7 @@ let val (c',a) = tr c xs val (v',A) = case v of Const (\<^const_syntax>\HOL.eq\, _) $ z $ t => (t, Syntax_Trans.abs_tr [z, a]) | - t => (t, absdummy dummyT a) + t => (t, Abs ("n", dummyT, a)) in (syntax_const ctxt #While $ bexp_tr b xs $ c', Syntax.const \<^const_syntax>\Awhile\ $ assn_tr i xs $ var_tr v' xs $ A)