Email Gateway (Aug 22 2022 at 18:54): Email Gateway (Aug 22 2022 at 18:54):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
Hello,
I do not understand why lemmas L1, L2, L3, L4, L5, cannot be proved in an
automatic way by using sledgehammer (see below).
Kind Regards,
José M.
theory Q1
imports
Complex_Main
"~~/src/HOL/IMP/AExp"
"~~/src/HOL/IMP/BExp"
"~~/src/HOL/IMP/ASM"
"~~/src/HOL/IMP/Com"
"~~/src/HOL/IMP/Big_Step"
"~~/src/HOL/IMP/Small_Step"
begin
function NextState :: ‹com × state ⇒ state› where
‹NextState (SKIP, s) = s› |
‹NextState (v ::= x, s) = (λ t::vname. (if t = v then aval x s else s
t))›|
‹NextState (c ;; d, s) = NextState (d, NextState (c, s))›|
‹NextState (IF A THEN c ELSE d, s) = (if bval A s then NextState (c, s)
else NextState (d, s) )› |
‹NextState (WHILE A DO b, s) = NextState ((IF A THEN (b ;; WHILE A DO b)
ELSE SKIP), s)›
apply (metis com.exhaust surj_pair)
apply auto
done
function eLength :: ‹com × state ⇒ nat› where
‹eLength (SKIP, s) = 0›|
‹eLength (v ::= x, s) = 0› |
‹eLength (c ;; d, s) = Suc (eLength (c, s) + eLength (d, NextState (c,
s)))› |
‹eLength (IF A THEN c ELSE d, s) = Suc (if bval A s then eLength (c, s)
else eLength (d, s))› |
‹eLength (WHILE A DO b, s) = Suc ( eLength (IF A THEN (b;; (WHILE A DO
b)) ELSE SKIP, s) )›
apply auto
by (meson com.exhaust)
lemma L1: ‹eLength (SKIP, s) = 0›
sorry
lemma L2: ‹eLength (v ::= x, s) = 0›
sorry
lemma L3: ‹eLength (c ;; d, s) = Suc (eLength (c, s) + eLength (d,
NextState (c, s)))›
sorry
lemma L4:‹eLength (IF A THEN c ELSE d, s) = Suc (if bval A s then eLength
(c, s) else eLength (d, s))›
sorry
lemma L5: ‹eLength (WHILE A DO b, s) = Suc ( eLength (IF A THEN (b;; (WHILE
A DO b)) ELSE SKIP, s) )›
sorry
end
Last updated: Apr 30 2024 at 16:19 UTC