Isaac Freund (Sep 21 2022 at 13:46): Isaac Freund (Sep 21 2022 at 13:46):How does one obtain the set of all members of a datatype? For example {True, False} for type bool or {0, 1, 2, ...} for type nat?
Lukas Stevens (Sep 21 2022 at 13:56):UNIV :: 'a
Isaac Freund (Sep 21 2022 at 14:03):I assume you mean UNIV :: 'a set? UNIV :: bool set for example gives what I want, Thanks!
Ryan13 (Sep 23 2022 at 02:26):I'm using isabelle to proof security boot of device. lemma AF1_aux fail to pass the proof.
When I change if event_enabled s be to if false, it pass. I can't move forward.
Any guidance would be very helpful!
Here is the simple code
section ‹boot security›
theory boot_sec
imports Main
begin
locale M_HLR =
(* declare the initial state *)
fixes Initial_State :: 's
(* next state function *)
fixes next_state :: "'s ⇒ 'be ⇒ 's"
(* Auxiliary function for present Stable State *)
fixes success :: "'s ⇒ bool"
(* Security Requirements *)
assumes AF1: "∃s. ∀b. next_state s b = s"
datatype Status = INIT | READ_ROM | END
record State =
status :: Status
datatype Behavior = Read_ROM |
Gen_SessionKey
definition read_rom :: "State ⇒ State" where
"read_rom s ≡ s ⦇status := READ_ROM ⦈"
definition gen_sessionkey :: "State ⇒ State" where
"gen_sessionkey s ≡ s ⦇status := END ⦈"
definition event_enabled :: "State ⇒ Behavior ⇒ bool" where
"event_enabled s be ≡ if status s = END then False else True"
definition exec_be :: "State ⇒ Behavior ⇒ State" where
"exec_be s be ≡
if event_enabled s be
then
( case be of
Read_ROM ⇒ read_rom s |
Gen_SessionKey ⇒ gen_sessionkey s )
else s"
lemma AF1_aux: "status s = END ⟹ ∀be. exec_be s be = s"
by(simp add: exec_be_def)
theorem AF1: "∃s. ∀be. exec_be s be = s"
by (meson AF1_aux State.select_convs(1))
end
The output is
theorem AF1_aux: status ?s = END ⟹ ∀be. exec_be ?s be = ?s
Failed to finish proof⌂:
goal (1 subgoal):
1. status s = END ⟹ ∀be. event_enabled s be ⟶ (case be of Read_ROM ⇒ read_rom s | Gen_SessionKey ⇒ gen_sessionkey s) = s
You need to also add event_enabled_def in addition to exec_be_def. Thus by (simp add: exec_be_def event_enabled_def) should work.
Robert Soeldner (Sep 29 2022 at 09:45):(deleted)
Last updated: Apr 20 2024 at 08:16 UTC