使用 Isabelle 简化器重写非相等等价关系
Rewriting with non-equality equivalence-relations using Isabelle simplifier
我想用简化器来替换不等式的子项。我将通过一个例子来说明这一点，而不是对我的问题进行通用定义：
假设我有一个简单的编程语言和一个基于它的 Hoare 逻辑。假设我们有 if、while 和序列操作。此外，我们还有 denotation 和 hoare P c Q，它给出了一个程序的表示。下面是 Isabelle/HOL 中的示例签名：
(* A simple language and Hoare logic *)
typedecl program
typedecl memory
consts
seq :: "program ⇒ program ⇒ program" (infixl ";" 10) (* c;d: run c, then run d *)
ifthen :: "(memory ⇒ bool) ⇒ program ⇒ program" (* ifthen e c: run c if e(current_mem)=true *)
while :: "(memory ⇒ bool) ⇒ program ⇒ program" (* while e c: run c while e(current_mem)=true *)
denotation :: "program ⇒ memory ⇒ memory" (* denotation c m: memory after running c, when starting with memory m *)
hoare :: "(memory ⇒ bool) ⇒ program ⇒ (memory ⇒ bool) ⇒ bool"
(* hoare P c Q: if P(current_mem), then after running c, we have Q(current_mem) *)
现在 (a;b);c = a;(b;c) 是不正确的（这些是不同的程序），但它确实认为它们在指称上是等价的，即 denotation ((a;b);c)) = denotation (a;(b;c)).
这意味着，我应该能够在 Hoare 三元组中将 a;(b;c) 重写为 (a;b);c。例如，我希望能够证明
lemma "hoare P (while e (a;b;c)) Q ==> hoare P (while e (a;(b;c))) Q"
只需使用简化器 (by simp)，给定合适的简化规则。
从逻辑上讲，相关规则为：
lemma "denotation (a;(b;c)) = denotation ((a;b);c)"
lemma "denotation a = denotation b ==> hoare P a Q = hoare P b Q"
lemma "denotation a = denotation b ==> denotation (while e a) = denotation (while e b)"
lemma "denotation a = denotation b ==> denotation (ifthen e a) = denotation (ifthen e b)"
lemma "denotation a = denotation a' ==> denotation b = denotation b' ==> denotation (a;b) = denotation (a';b')"
不幸的是，似乎没有直接的方法将这些规则告诉简化者。 （更一般地说，我们想在同余规则中告诉简化器，下面的重写必须完成模块某个等价关系，在本例中为指称等价。）
我已经找到了这个问题的部分解决方案（见下面我自己的回答），但是这个解决方案似乎是一个 hack（我不知道它有多稳定），我想知道是否有好的方法。
我不介意在此过程中使用一些 ML 代码（例如，编写 simproc），但我想避免必须重新实现整个简化器以在 Hoare 元组中重写。
对于似乎可行的方法，请参阅随附的 Isabelle/HOL 理论。这里的想法是使用条件简单规则来模拟从规则。
例如，同余规则
lemma l1 [cong]: "f a = f b ==> g a = g b"
也是一个有效的条件简化规则
lemma l2 [simp]: "f a = f b ==> g a = g b"
并且当 Isabelle 应用简化规则时，b 将被替换为示意图变量，并且简化器将重写 "f a = f ?b"，从而用 b 的简化实例化 ?b。
然而，引理l2 将使简化器循环，因为它可以应用于它自己的 rhs。所以我们可以写一个规则
lemma l3 [simp]: "f_simp a = f_done b ==> g_simp a = g_done b"
其中 g_simp 和 g_done 被定义为等于 g，但会阻止简化器在循环中应用规则。
这个想法的一个完整的工作示例在下面的理论文件中。
问题是：
- 这是一个黑客。我不知道在什么情况下它可能会崩溃或与其他东西不兼容
- apply simp可能会部分重写，所以你必须再次调用它才能完成重写。 （参见理论中的最后一个引理。）
theory Test
imports Main
begin
section "Minimal Hoare logic"
(* A simple language and Hoare logic *)
typedecl program
typedecl memory
consts
seq :: "program ⇒ program ⇒ program" (infixl ";" 10) (* c;d: run c, then run d *)
ifthen :: "(memory ⇒ bool) ⇒ program ⇒ program" (* ifthen e c: run c if e(current_mem)=true *)
while :: "(memory ⇒ bool) ⇒ program ⇒ program" (* while e c: run c while e(current_mem)=true *)
denotation :: "program ⇒ memory ⇒ memory" (* denotation c m: memory after running c, when starting with memory m *)
hoare :: "(memory ⇒ bool) ⇒ program ⇒ (memory ⇒ bool) ⇒ bool"
(* hoare P c Q: if P(current_mem), then after running c, we have Q(current_mem) *)
(* seq is associative modulo denotational equivalence.
Thus we should be able to rewrite "a;(b;c)" to "a;b;c"
within a hoare triple. E.g., the following should be solved with simp: *)
lemma
assumes "hoare P (while e (a;b;c)) Q"
shows "hoare P (while e (a;(b;c))) Q"
using assms
oops (* by simp *)
section "A failed attempt"
experiment begin
(* Here a natural approach first which, however, fails. *)
(* A congruence rule for the simplifier.
To rewrite a hoare triple "hoare P c Q",
we need to rewrite "denotation c". *)
lemma enter [cong]:
assumes "P==P'" and "Q==Q'"
assumes "denotation c == denotation c'"
shows "hoare P c Q == hoare P' c' Q'"
sorry
(* To descend further into subterms, we need a congruence-rule for while. *)
lemma while [cong]:
assumes "e=e'"
and "denotation c == denotation c'"
shows "denotation (while e c) ≡ denotation (while e' c')"
sorry
(* And we give a simplification rule for the associativity of seq *)
lemma assoc [simp]:
"denotation (a;(b;c)) = denotation (a;b;c)"
sorry
(* Now we can simplify the lemma from above *)
lemma
assumes "hoare P (while e (a;b;c)) Q"
shows "hoare P (while e (a;(b;c))) Q"
using assms by simp
(* Unfortunately, this does not work any more once we add more congruence rules. *)
(* To descend further into subterms, we need a congruence-rule for while. *)
lemma ifthen [cong]:
assumes "e=e'"
and "denotation c == denotation c'"
shows "denotation (ifthen e c) ≡ denotation (ifthen e' c')"
sorry
(* Warning: Overwriting congruence rule for "Test.denotation" *)
(* Simplifier doesn't work any more because the congruence rule for while was overwritten *)
lemma
assumes "hoare P (while e (a;b;c)) Q"
shows "hoare P (while e (a;(b;c))) Q"
using assms
oops (* by simp *)
end
section {* A working attempt *}
(* Define copies of the denotation-constant, to control the simplifier *)
definition "denotation_simp == denotation"
definition "denotation_done == denotation"
(* A congruence rule for the simplifier.
To rewrite a hoare triple "hoare P c Q",
we need to rewrite "denotation c".
This means, the congruence rule should have an assumption
"denotation c == denotation c'"
However, to avoid infinite loops with the rewrite rules below,
we use the logically equivalent assumption
"denotation_simp c == denotation_done c'"
This means that we need to configure the rules below rewrite
"denotation_simp c" into "denotation_done c'" where c' is
the simplication of c (module denotational equivalence).
*)
lemma enter [cong]:
assumes "P==P'" and "Q==Q'"
assumes "denotation_simp c == denotation_done c'"
shows "hoare P c Q == hoare P' c' Q'"
sorry
(* A similar congruence rule for simplifying expressions
of the form "denotation c". *)
lemma denot [cong]:
assumes "denotation_simp c == denotation_done c'"
shows "denotation c == denotation c'"
sorry
(* Now we add a congruence-rule for while.
Since we saw above that we cannot use several congruence-rules
with "denotation" as their head,
we simulate a congruence rule using a simp-rule.
To rewrite "denotation_simp (while e c)", we need to rewrite
"denotation_simp c".
We put denotation_done on the rhs instead of denotation_simp
to avoid infinite loops.
*)
lemma while [simp]:
assumes "e=e'"
and "denotation_simp c == denotation_done c'"
shows "denotation_simp (while e c) ≡ denotation_done (while e' c')"
sorry
(* A pseudo-congruence rule for ifthen *)
lemma ifthen [simp]:
assumes "e=e'"
and "denotation_simp c == denotation_done c'"
shows "denotation_simp (ifthen e c) == denotation_done (ifthen e' c')"
sorry
(* A pseudo-congruence rule for seq *)
lemma seq [simp]:
assumes "denotation_simp c == denotation_done c'"
and "denotation_simp d == denotation_done d'"
shows "denotation_simp (c;d) == denotation_done (c';d')"
sorry
(* Finally, we can state associativity of seq. *)
lemma assoc [simp]:
"denotation_simp (a;(b;c)) = denotation_simp (a;b;c)"
sorry
(* Finally, since our congruence-rules expect the rewriting to rewrite
"denotation_simp c" into "denotation_done c'",
we need to translate any non-rewritten "denotation_simp" into
"denotation_done".
However, a rule "denotation_simp c == denotation_done c" does not work,
because it could be triggered too early, and block the pseudo-congruence rules above.
So we only trigger the rule when the current term would not match
any of the pseudo congruence rules *)
lemma finish [simp]:
assumes "NO_MATCH (while e1 c1) a"
assumes "NO_MATCH (ifthen e2 c2) a"
assumes "NO_MATCH (c3;d3) a"
shows "denotation_simp a = denotation_done a"
sorry
(* Testing the simplifier rules *)
lemma
assumes "hoare P (while e (a;b;c)) Q"
shows "hoare P (while e (a;(b;c))) Q"
using assms
by simp
(* Some more complex test *)
lemma iftrue [simp]: "denotation_simp (ifthen (λm. True) c) == denotation_simp c" sorry
lemma
assumes "⋀x. Q x"
assumes "hoare (λm. P x ∧ Q x) (while P (c;(d;e);(f;g);c)) (λm. m=m)"
shows "hoare (λm. P x) (while P (c;(d;e);ifthen (λm. m=m) (f;g;c))) (λm. True)"
using assms
apply simp (* Hmm. Only partially simplified... The assoc rule is not applied to the result of the iftrue rule *)
by simp (* Rerunning simp solves the goal *)
(* By the way: "using assms by auto" solves the goal in one go *)
end
Isabelle 的简化器不支持对任意等价关系的重写。幸运的是，您的重写看起来相当简单，因此在 simproc 中实现重写可能是值得的。想法是这样的：
编写一个根据 hoare P c Q 形式触发的 simproc。调用时，它会设置一个 hoare P c Q == ?rhs 形式的目标，并且
应用一条规则，说明 %c. hoare P c Q 只关心其参数的等价性 class，而不关心具体元素。然后，应用重写规则作为引入规则，直到解决既定目标。这应该将 ?rhs 实例化为 hoare P c' Q 形式的东西。测试 c 和 c' 是否等价于 alpha-beta-eta-...。如果是这样，则 simproc 失败并显示 NONE，否则它 returns 已证明的等式。
这是我将用作开始的一堆引理：
definition fun_equiv :: "('a ⇒ 'b) ⇒ 'a ⇒ 'a ⇒ bool"
where "fun_equiv f x y ⟷ f x = f y"
lemma fun_equiv_refl: "fun_equiv f x x" by(simp add: fun_equiv_def)
lemma hoare_cong_start: (* start rule *)
"fun_equiv denotation c c' ⟹ hoare P c Q == hoare P' c' Q'"
sorry
lemma while_cong: "fun_equiv denotation c c' ⟹ fun_equiv denotation (while b c) (while b c')" sorry
lemma seq_cong: "⟦ fun_equiv denotation a a'; fun_equiv denotation b b' ⟧ ⟹ fun_equiv denotation (a ; b) (a' ; b')" sorry
lemma if_cong: "fun_equiv denotation c c' ⟹ fun_equiv denotation (ifthen b c) (ifthen b c')" sorry
lemma seq_assoc: "fun_equiv denotation (a ; (b ; c)) (a; b; c)" sorry
lemma ifthen_true: "fun_equiv denotation (ifthen (λm. True) c) c" sorry
lemmas hoare_intros =
-- ‹rewrites come first, congruences later, reflexivity last›
ifthen_true seq_assoc
while_cong if_cong seq_cong
fun_equiv_refl
由于这是简化器内部的 simproc，您可以假设调用中的命令已经是正常形式 w.r.t。简单集。在您的示例中，测试 %m. m = m 已简化为 %_. True。因此，simproc 可以专注于实现 hoare 规则的重写。
simproc 调用的单个步骤应该执行类似于以下 Isar 片段的操作：
schematic_lemma "hoare (λm. P x) (while P (c;(d;e);ifthen (λm. True) (f;g;c))) (λm. True) == ?c"
by(rule hoare_cong_start)(rule hoare_intros)+
由于简化器迭代 simproc 直到它不再触发，所以你应该最终得到一个正常的形式。
如果你想支持条件重写规则w.r.t。指称等价，rule hoare_intros 应该替换为检查子目标格式的内容。如果它不是 fun_equiv denotation _ _ 的形式，那么 simproc 应该递归地调用简化器（或您选择的任何其他证明方法），而不是尝试 hoare_intros.
的另一个规则应用程序
下面是我对 的实现。第一部分是一个通用实现（适用于除指称等价之外的其他等价），下面是为我的例子霍尔逻辑实例化。
(* Written by Dominique Unruh *)
theory Test2
imports Main
begin
section "Implementation of modulo-simplifier"
definition fun_equiv :: "('a ⇒ 'b) ⇒ 'a ⇒ 'a ⇒ bool" where "fun_equiv f x y == f x = f y"
lemma fun_equiv_refl: "fun_equiv f x x" by(simp add: fun_equiv_def)
ML {*
(* Call as: hoare_simproc_tac (simplifications@congruences) context/simpset *)
fun fun_equiv_simproc_tac intros ctxt =
SUBGOAL (fn (goal,i) =>
case goal of
Const(@{const_name Trueprop},_) $ (Const(@{const_name fun_equiv},_)$_$_$_) =>
(resolve0_tac intros THEN_ALL_NEW fun_equiv_simproc_tac intros ctxt) i
ORELSE (rtac @{thm fun_equiv_refl} i)
| _ =>
SOLVED' (simp_tac ctxt) i)
fun fun_equiv_simproc start intros _ ctxt (t:cterm) =
let val fresh_var = Var(("x",Term.maxidx_of_term (Thm.term_of t)+1),Thm.typ_of_cterm t)
val goal = Logic.mk_equals (Thm.term_of t,fresh_var)
val thm = Goal.prove ctxt [] [] goal
(fn {context,...} => resolve0_tac start 1 THEN ALLGOALS (fun_equiv_simproc_tac intros context))
in
if (Thm.rhs_of thm) aconvc t then NONE else SOME thm
end
handle ERROR msg => (warning ("fun_equiv_simproc failed\nTerm was:\n"^(@{make_string} t)^"\nError: "^msg); NONE)
fun fun_equiv_simproc_named start cong simp morph ctxt =
fun_equiv_simproc (Named_Theorems.get ctxt start) (Named_Theorems.get ctxt simp @ Named_Theorems.get ctxt cong) morph ctxt
*}
section "Minimal Hoare logic"
(* A simple language and Hoare logic *)
typedecl program
typedecl memory
consts
seq :: "program ⇒ program ⇒ program" (infixl ";" 100) (* c;d: run c, then run d *)
ifthen :: "(memory ⇒ bool) ⇒ program ⇒ program" (* ifthen e c: run c if e(current_mem)=true *)
while :: "(memory ⇒ bool) ⇒ program ⇒ program" (* while e c: run c while e(current_mem)=true *)
denotation :: "program ⇒ memory ⇒ memory" (* denotation c m: memory after running c, when starting with memory m *)
hoare :: "(memory ⇒ bool) ⇒ program ⇒ (memory ⇒ bool) ⇒ bool"
(* hoare P c Q: if P(current_mem), then after running c, we have Q(current_mem) *)
section "Instantiating the simplifier"
named_theorems denot_simp_start
named_theorems denot_simp
named_theorems denot_cong
lemma hoare_cong_start [denot_simp_start]: "fun_equiv denotation c c' ⟹ hoare P c Q == hoare P c' Q" sorry
lemma while_cong [denot_cong]: "fun_equiv denotation c c' ⟹ fun_equiv denotation (while b c) (while b c')" sorry
lemma seq_cong [denot_cong]: "fun_equiv denotation a a' ⟹ fun_equiv denotation b b' ⟹ fun_equiv denotation (a ; b) (a' ; b')" sorry
lemma if_cong [denot_cong]: "fun_equiv denotation c c' ⟹ fun_equiv denotation (ifthen b c) (ifthen b c')" sorry
lemma seq_assoc [denot_simp]: "fun_equiv denotation (a ; (b ; c)) (a; b; c)" sorry
lemma ifthen_true [denot_simp]: "(⋀m. e m) ⟹ fun_equiv denotation (ifthen e c) c" sorry
lemma double_while [denot_simp]: "(⋀m. e m = e' m) ⟹ fun_equiv denotation c d ⟹ fun_equiv denotation (seq (while e c) (while e' d)) (while e c)" sorry
(* -- "If the set of simplification theorems is fixed, we can use the following setup"
lemmas hoare_congruences = while_cong if_cong seq_cong
lemmas hoare_simps = ifthen_true seq_assoc double_while
simproc_setup hoare_simproc ("hoare P c Q") = {* fun_equiv_simproc @{thms hoare_cong_start} @{thms hoare_simps hoare_congruences} *}
*)
(* To make use of dynamic lists of theorems, we use the following setup *)
simproc_setup hoare_simproc ("hoare P c Q") = {*
fun_equiv_simproc_named @{named_theorems denot_simp_start}
@{named_theorems denot_cong}
@{named_theorems denot_simp}
*}
section "Tests"
(* Testing the simplifier rules *)
lemma
assumes "hoare P (while e (a;b;c)) Q"
shows "hoare P (while e (a;(b;c))) Q ∧ True"
using assms
by simp
lemma
assumes "hoare P (while P (c;d;e)) Q"
assumes "⋀x. P x = R x"
shows "hoare P ((while P (c;(d;e))); (while R ((c;d);e))) Q"
using assms by simp
lemma
assumes "⋀x. Q x"
assumes "hoare (λm. P x ∧ Q x) (while P (c;(d;e);(f;g);c)) (λm. m=m)"
shows "hoare (λm. P x) (while P (c;(d;e);ifthen (λm. m=m) (f;g;c))) (λm. True)"
using assms by simp
(* Test: Disabling the simproc *)
lemma
assumes "hoare P (a;(b;c)) Q"
shows "hoare P (a;(b;c)) Q ∧ True"
using[[simproc del: hoare_simproc]] -- "Without this, proof fails"
apply simp
by (fact assms)
end
我想用简化器来替换不等式的子项。我将通过一个例子来说明这一点，而不是对我的问题进行通用定义：
假设我有一个简单的编程语言和一个基于它的 Hoare 逻辑。假设我们有 if、while 和序列操作。此外，我们还有 denotation 和 hoare P c Q，它给出了一个程序的表示。下面是 Isabelle/HOL 中的示例签名：
(* A simple language and Hoare logic *)
typedecl program
typedecl memory
consts
seq :: "program ⇒ program ⇒ program" (infixl ";" 10) (* c;d: run c, then run d *)
ifthen :: "(memory ⇒ bool) ⇒ program ⇒ program" (* ifthen e c: run c if e(current_mem)=true *)
while :: "(memory ⇒ bool) ⇒ program ⇒ program" (* while e c: run c while e(current_mem)=true *)
denotation :: "program ⇒ memory ⇒ memory" (* denotation c m: memory after running c, when starting with memory m *)
hoare :: "(memory ⇒ bool) ⇒ program ⇒ (memory ⇒ bool) ⇒ bool"
(* hoare P c Q: if P(current_mem), then after running c, we have Q(current_mem) *)
现在 (a;b);c = a;(b;c) 是不正确的（这些是不同的程序），但它确实认为它们在指称上是等价的，即 denotation ((a;b);c)) = denotation (a;(b;c)).
这意味着，我应该能够在 Hoare 三元组中将 a;(b;c) 重写为 (a;b);c。例如，我希望能够证明
lemma "hoare P (while e (a;b;c)) Q ==> hoare P (while e (a;(b;c))) Q"
只需使用简化器 (by simp)，给定合适的简化规则。
从逻辑上讲，相关规则为：
lemma "denotation (a;(b;c)) = denotation ((a;b);c)"
lemma "denotation a = denotation b ==> hoare P a Q = hoare P b Q"
lemma "denotation a = denotation b ==> denotation (while e a) = denotation (while e b)"
lemma "denotation a = denotation b ==> denotation (ifthen e a) = denotation (ifthen e b)"
lemma "denotation a = denotation a' ==> denotation b = denotation b' ==> denotation (a;b) = denotation (a';b')"
不幸的是，似乎没有直接的方法将这些规则告诉简化者。 （更一般地说，我们想在同余规则中告诉简化器，下面的重写必须完成模块某个等价关系，在本例中为指称等价。）
我已经找到了这个问题的部分解决方案（见下面我自己的回答），但是这个解决方案似乎是一个 hack（我不知道它有多稳定），我想知道是否有好的方法。
我不介意在此过程中使用一些 ML 代码（例如，编写 simproc），但我想避免必须重新实现整个简化器以在 Hoare 元组中重写。
对于似乎可行的方法，请参阅随附的 Isabelle/HOL 理论。这里的想法是使用条件简单规则来模拟从规则。
例如，同余规则
lemma l1 [cong]: "f a = f b ==> g a = g b"
也是一个有效的条件简化规则
lemma l2 [simp]: "f a = f b ==> g a = g b"
并且当 Isabelle 应用简化规则时，b 将被替换为示意图变量，并且简化器将重写 "f a = f ?b"，从而用 b 的简化实例化 ?b。
然而，引理l2 将使简化器循环，因为它可以应用于它自己的 rhs。所以我们可以写一个规则
lemma l3 [simp]: "f_simp a = f_done b ==> g_simp a = g_done b"
其中 g_simp 和 g_done 被定义为等于 g，但会阻止简化器在循环中应用规则。
这个想法的一个完整的工作示例在下面的理论文件中。
问题是：
- 这是一个黑客。我不知道在什么情况下它可能会崩溃或与其他东西不兼容
- apply simp可能会部分重写，所以你必须再次调用它才能完成重写。 （参见理论中的最后一个引理。）
theory Test
imports Main
begin
section "Minimal Hoare logic"
(* A simple language and Hoare logic *)
typedecl program
typedecl memory
consts
seq :: "program ⇒ program ⇒ program" (infixl ";" 10) (* c;d: run c, then run d *)
ifthen :: "(memory ⇒ bool) ⇒ program ⇒ program" (* ifthen e c: run c if e(current_mem)=true *)
while :: "(memory ⇒ bool) ⇒ program ⇒ program" (* while e c: run c while e(current_mem)=true *)
denotation :: "program ⇒ memory ⇒ memory" (* denotation c m: memory after running c, when starting with memory m *)
hoare :: "(memory ⇒ bool) ⇒ program ⇒ (memory ⇒ bool) ⇒ bool"
(* hoare P c Q: if P(current_mem), then after running c, we have Q(current_mem) *)
(* seq is associative modulo denotational equivalence.
Thus we should be able to rewrite "a;(b;c)" to "a;b;c"
within a hoare triple. E.g., the following should be solved with simp: *)
lemma
assumes "hoare P (while e (a;b;c)) Q"
shows "hoare P (while e (a;(b;c))) Q"
using assms
oops (* by simp *)
section "A failed attempt"
experiment begin
(* Here a natural approach first which, however, fails. *)
(* A congruence rule for the simplifier.
To rewrite a hoare triple "hoare P c Q",
we need to rewrite "denotation c". *)
lemma enter [cong]:
assumes "P==P'" and "Q==Q'"
assumes "denotation c == denotation c'"
shows "hoare P c Q == hoare P' c' Q'"
sorry
(* To descend further into subterms, we need a congruence-rule for while. *)
lemma while [cong]:
assumes "e=e'"
and "denotation c == denotation c'"
shows "denotation (while e c) ≡ denotation (while e' c')"
sorry
(* And we give a simplification rule for the associativity of seq *)
lemma assoc [simp]:
"denotation (a;(b;c)) = denotation (a;b;c)"
sorry
(* Now we can simplify the lemma from above *)
lemma
assumes "hoare P (while e (a;b;c)) Q"
shows "hoare P (while e (a;(b;c))) Q"
using assms by simp
(* Unfortunately, this does not work any more once we add more congruence rules. *)
(* To descend further into subterms, we need a congruence-rule for while. *)
lemma ifthen [cong]:
assumes "e=e'"
and "denotation c == denotation c'"
shows "denotation (ifthen e c) ≡ denotation (ifthen e' c')"
sorry
(* Warning: Overwriting congruence rule for "Test.denotation" *)
(* Simplifier doesn't work any more because the congruence rule for while was overwritten *)
lemma
assumes "hoare P (while e (a;b;c)) Q"
shows "hoare P (while e (a;(b;c))) Q"
using assms
oops (* by simp *)
end
section {* A working attempt *}
(* Define copies of the denotation-constant, to control the simplifier *)
definition "denotation_simp == denotation"
definition "denotation_done == denotation"
(* A congruence rule for the simplifier.
To rewrite a hoare triple "hoare P c Q",
we need to rewrite "denotation c".
This means, the congruence rule should have an assumption
"denotation c == denotation c'"
However, to avoid infinite loops with the rewrite rules below,
we use the logically equivalent assumption
"denotation_simp c == denotation_done c'"
This means that we need to configure the rules below rewrite
"denotation_simp c" into "denotation_done c'" where c' is
the simplication of c (module denotational equivalence).
*)
lemma enter [cong]:
assumes "P==P'" and "Q==Q'"
assumes "denotation_simp c == denotation_done c'"
shows "hoare P c Q == hoare P' c' Q'"
sorry
(* A similar congruence rule for simplifying expressions
of the form "denotation c". *)
lemma denot [cong]:
assumes "denotation_simp c == denotation_done c'"
shows "denotation c == denotation c'"
sorry
(* Now we add a congruence-rule for while.
Since we saw above that we cannot use several congruence-rules
with "denotation" as their head,
we simulate a congruence rule using a simp-rule.
To rewrite "denotation_simp (while e c)", we need to rewrite
"denotation_simp c".
We put denotation_done on the rhs instead of denotation_simp
to avoid infinite loops.
*)
lemma while [simp]:
assumes "e=e'"
and "denotation_simp c == denotation_done c'"
shows "denotation_simp (while e c) ≡ denotation_done (while e' c')"
sorry
(* A pseudo-congruence rule for ifthen *)
lemma ifthen [simp]:
assumes "e=e'"
and "denotation_simp c == denotation_done c'"
shows "denotation_simp (ifthen e c) == denotation_done (ifthen e' c')"
sorry
(* A pseudo-congruence rule for seq *)
lemma seq [simp]:
assumes "denotation_simp c == denotation_done c'"
and "denotation_simp d == denotation_done d'"
shows "denotation_simp (c;d) == denotation_done (c';d')"
sorry
(* Finally, we can state associativity of seq. *)
lemma assoc [simp]:
"denotation_simp (a;(b;c)) = denotation_simp (a;b;c)"
sorry
(* Finally, since our congruence-rules expect the rewriting to rewrite
"denotation_simp c" into "denotation_done c'",
we need to translate any non-rewritten "denotation_simp" into
"denotation_done".
However, a rule "denotation_simp c == denotation_done c" does not work,
because it could be triggered too early, and block the pseudo-congruence rules above.
So we only trigger the rule when the current term would not match
any of the pseudo congruence rules *)
lemma finish [simp]:
assumes "NO_MATCH (while e1 c1) a"
assumes "NO_MATCH (ifthen e2 c2) a"
assumes "NO_MATCH (c3;d3) a"
shows "denotation_simp a = denotation_done a"
sorry
(* Testing the simplifier rules *)
lemma
assumes "hoare P (while e (a;b;c)) Q"
shows "hoare P (while e (a;(b;c))) Q"
using assms
by simp
(* Some more complex test *)
lemma iftrue [simp]: "denotation_simp (ifthen (λm. True) c) == denotation_simp c" sorry
lemma
assumes "⋀x. Q x"
assumes "hoare (λm. P x ∧ Q x) (while P (c;(d;e);(f;g);c)) (λm. m=m)"
shows "hoare (λm. P x) (while P (c;(d;e);ifthen (λm. m=m) (f;g;c))) (λm. True)"
using assms
apply simp (* Hmm. Only partially simplified... The assoc rule is not applied to the result of the iftrue rule *)
by simp (* Rerunning simp solves the goal *)
(* By the way: "using assms by auto" solves the goal in one go *)
end
Isabelle 的简化器不支持对任意等价关系的重写。幸运的是，您的重写看起来相当简单，因此在 simproc 中实现重写可能是值得的。想法是这样的：
编写一个根据 hoare P c Q 形式触发的 simproc。调用时，它会设置一个 hoare P c Q == ?rhs 形式的目标，并且
应用一条规则，说明 %c. hoare P c Q 只关心其参数的等价性 class，而不关心具体元素。然后，应用重写规则作为引入规则，直到解决既定目标。这应该将 ?rhs 实例化为 hoare P c' Q 形式的东西。测试 c 和 c' 是否等价于 alpha-beta-eta-...。如果是这样，则 simproc 失败并显示 NONE，否则它 returns 已证明的等式。
这是我将用作开始的一堆引理：
definition fun_equiv :: "('a ⇒ 'b) ⇒ 'a ⇒ 'a ⇒ bool"
where "fun_equiv f x y ⟷ f x = f y"
lemma fun_equiv_refl: "fun_equiv f x x" by(simp add: fun_equiv_def)
lemma hoare_cong_start: (* start rule *)
"fun_equiv denotation c c' ⟹ hoare P c Q == hoare P' c' Q'"
sorry
lemma while_cong: "fun_equiv denotation c c' ⟹ fun_equiv denotation (while b c) (while b c')" sorry
lemma seq_cong: "⟦ fun_equiv denotation a a'; fun_equiv denotation b b' ⟧ ⟹ fun_equiv denotation (a ; b) (a' ; b')" sorry
lemma if_cong: "fun_equiv denotation c c' ⟹ fun_equiv denotation (ifthen b c) (ifthen b c')" sorry
lemma seq_assoc: "fun_equiv denotation (a ; (b ; c)) (a; b; c)" sorry
lemma ifthen_true: "fun_equiv denotation (ifthen (λm. True) c) c" sorry
lemmas hoare_intros =
-- ‹rewrites come first, congruences later, reflexivity last›
ifthen_true seq_assoc
while_cong if_cong seq_cong
fun_equiv_refl
由于这是简化器内部的 simproc，您可以假设调用中的命令已经是正常形式 w.r.t。简单集。在您的示例中，测试 %m. m = m 已简化为 %_. True。因此，simproc 可以专注于实现 hoare 规则的重写。
simproc 调用的单个步骤应该执行类似于以下 Isar 片段的操作：
schematic_lemma "hoare (λm. P x) (while P (c;(d;e);ifthen (λm. True) (f;g;c))) (λm. True) == ?c"
by(rule hoare_cong_start)(rule hoare_intros)+
由于简化器迭代 simproc 直到它不再触发，所以你应该最终得到一个正常的形式。
如果你想支持条件重写规则w.r.t。指称等价，rule hoare_intros 应该替换为检查子目标格式的内容。如果它不是 fun_equiv denotation _ _ 的形式，那么 simproc 应该递归地调用简化器（或您选择的任何其他证明方法），而不是尝试 hoare_intros.
下面是我对
(* Written by Dominique Unruh *)
theory Test2
imports Main
begin
section "Implementation of modulo-simplifier"
definition fun_equiv :: "('a ⇒ 'b) ⇒ 'a ⇒ 'a ⇒ bool" where "fun_equiv f x y == f x = f y"
lemma fun_equiv_refl: "fun_equiv f x x" by(simp add: fun_equiv_def)
ML {*
(* Call as: hoare_simproc_tac (simplifications@congruences) context/simpset *)
fun fun_equiv_simproc_tac intros ctxt =
SUBGOAL (fn (goal,i) =>
case goal of
Const(@{const_name Trueprop},_) $ (Const(@{const_name fun_equiv},_)$_$_$_) =>
(resolve0_tac intros THEN_ALL_NEW fun_equiv_simproc_tac intros ctxt) i
ORELSE (rtac @{thm fun_equiv_refl} i)
| _ =>
SOLVED' (simp_tac ctxt) i)
fun fun_equiv_simproc start intros _ ctxt (t:cterm) =
let val fresh_var = Var(("x",Term.maxidx_of_term (Thm.term_of t)+1),Thm.typ_of_cterm t)
val goal = Logic.mk_equals (Thm.term_of t,fresh_var)
val thm = Goal.prove ctxt [] [] goal
(fn {context,...} => resolve0_tac start 1 THEN ALLGOALS (fun_equiv_simproc_tac intros context))
in
if (Thm.rhs_of thm) aconvc t then NONE else SOME thm
end
handle ERROR msg => (warning ("fun_equiv_simproc failed\nTerm was:\n"^(@{make_string} t)^"\nError: "^msg); NONE)
fun fun_equiv_simproc_named start cong simp morph ctxt =
fun_equiv_simproc (Named_Theorems.get ctxt start) (Named_Theorems.get ctxt simp @ Named_Theorems.get ctxt cong) morph ctxt
*}
section "Minimal Hoare logic"
(* A simple language and Hoare logic *)
typedecl program
typedecl memory
consts
seq :: "program ⇒ program ⇒ program" (infixl ";" 100) (* c;d: run c, then run d *)
ifthen :: "(memory ⇒ bool) ⇒ program ⇒ program" (* ifthen e c: run c if e(current_mem)=true *)
while :: "(memory ⇒ bool) ⇒ program ⇒ program" (* while e c: run c while e(current_mem)=true *)
denotation :: "program ⇒ memory ⇒ memory" (* denotation c m: memory after running c, when starting with memory m *)
hoare :: "(memory ⇒ bool) ⇒ program ⇒ (memory ⇒ bool) ⇒ bool"
(* hoare P c Q: if P(current_mem), then after running c, we have Q(current_mem) *)
section "Instantiating the simplifier"
named_theorems denot_simp_start
named_theorems denot_simp
named_theorems denot_cong
lemma hoare_cong_start [denot_simp_start]: "fun_equiv denotation c c' ⟹ hoare P c Q == hoare P c' Q" sorry
lemma while_cong [denot_cong]: "fun_equiv denotation c c' ⟹ fun_equiv denotation (while b c) (while b c')" sorry
lemma seq_cong [denot_cong]: "fun_equiv denotation a a' ⟹ fun_equiv denotation b b' ⟹ fun_equiv denotation (a ; b) (a' ; b')" sorry
lemma if_cong [denot_cong]: "fun_equiv denotation c c' ⟹ fun_equiv denotation (ifthen b c) (ifthen b c')" sorry
lemma seq_assoc [denot_simp]: "fun_equiv denotation (a ; (b ; c)) (a; b; c)" sorry
lemma ifthen_true [denot_simp]: "(⋀m. e m) ⟹ fun_equiv denotation (ifthen e c) c" sorry
lemma double_while [denot_simp]: "(⋀m. e m = e' m) ⟹ fun_equiv denotation c d ⟹ fun_equiv denotation (seq (while e c) (while e' d)) (while e c)" sorry
(* -- "If the set of simplification theorems is fixed, we can use the following setup"
lemmas hoare_congruences = while_cong if_cong seq_cong
lemmas hoare_simps = ifthen_true seq_assoc double_while
simproc_setup hoare_simproc ("hoare P c Q") = {* fun_equiv_simproc @{thms hoare_cong_start} @{thms hoare_simps hoare_congruences} *}
*)
(* To make use of dynamic lists of theorems, we use the following setup *)
simproc_setup hoare_simproc ("hoare P c Q") = {*
fun_equiv_simproc_named @{named_theorems denot_simp_start}
@{named_theorems denot_cong}
@{named_theorems denot_simp}
*}
section "Tests"
(* Testing the simplifier rules *)
lemma
assumes "hoare P (while e (a;b;c)) Q"
shows "hoare P (while e (a;(b;c))) Q ∧ True"
using assms
by simp
lemma
assumes "hoare P (while P (c;d;e)) Q"
assumes "⋀x. P x = R x"
shows "hoare P ((while P (c;(d;e))); (while R ((c;d);e))) Q"
using assms by simp
lemma
assumes "⋀x. Q x"
assumes "hoare (λm. P x ∧ Q x) (while P (c;(d;e);(f;g);c)) (λm. m=m)"
shows "hoare (λm. P x) (while P (c;(d;e);ifthen (λm. m=m) (f;g;c))) (λm. True)"
using assms by simp
(* Test: Disabling the simproc *)
lemma
assumes "hoare P (a;(b;c)) Q"
shows "hoare P (a;(b;c)) Q ∧ True"
using[[simproc del: hoare_simproc]] -- "Without this, proof fails"
apply simp
by (fact assms)
end