how to transform keyword "def" in Isabelle2005 into the corresponding form in Isabelle2020

user_13276122 0
Viewed 53

I am performing a script updating. I encount such a question that :

constdefs is_initiator::"sigma \<Rightarrow>  agent\<Rightarrow> agent \<Rightarrow>nat \<Rightarrow>nat \<Rightarrow>bool" 
  "is_initiator s A B Na Nb == 
  (SP s)=[(+, Crypt (pubK B) {|Nonce Na, Agent A|}), 
  (-,Crypt (pubK A) {|Nonce Na, Nonce Nb, Agent B|}),
  (+, Crypt (pubK B) (Nonce Nb))]"

constdefs is_responder::"sigma \<Rightarrow>  agent\<Rightarrow> agent \<Rightarrow>nat \<Rightarrow>nat \<Rightarrow>bool" 
  "is_responder s A B Na Nb ==
  (SP s)=[(-, Crypt (pubK B) {|Nonce Na, Agent A|}),
  (+,Crypt (pubK A) {|Nonce Na, Nonce Nb, Agent B|}),
  (-, Crypt (pubK B) (Nonce Nb))]"

defs NSL_1:
"\<Sigma> == {s. Is_penetrator_strand s |
          (EX A B Na Nb.  is_initiator s  A B Na Nb) |
          (EX A B Na Nb.  is_responder s A B Na Nb)
       }"

And In Isabelle 2020, I code these phases into

definition is_initiator::"sigma \<Rightarrow>  agent\<Rightarrow> agent \<Rightarrow>nat \<Rightarrow>nat \<Rightarrow>bool" where 
  "is_initiator s A B Na Nb == 
  (SP s)=[(+, Crypt (pubK B) \<lbrace>Nonce Na, Agent A\<rbrace>), 
  (-,Crypt (pubK A) \<lbrace>Nonce Na, Nonce Nb, Agent B\<rbrace>),
  (+, Crypt (pubK B) (Nonce Nb))]"

definition is_responder::"sigma \<Rightarrow>  agent\<Rightarrow> agent \<Rightarrow>nat \<Rightarrow>nat \<Rightarrow>bool" where 
  "is_responder s A B Na Nb ==
  (SP s)=[(-, Crypt (pubK B)  \<lbrace> Nonce Na, Agent A\<rbrace>),
  (+,Crypt (pubK A)  \<lbrace>Nonce Na, Nonce Nb, Agent B\<rbrace>),
  (-, Crypt (pubK B) (Nonce Nb))]"

definition NSL_1:
"NSL_1 == \<Sigma> = {s. Is_penetrator_strand s |
          (EX A B Na Nb.  is_initiator s  A B Na Nb) |
          (EX A B Na Nb.  is_responder s A B Na Nb)
       }"

When i try to unfold the definition NSL_1 in the lemma, find that can not pass in Isabelle2020. How can i transform these codes rightly? Thanks.

The main aim of this is that i wanna unfold the definition NSL_1.

 1. ¬ Is_penetrator_strand (fst m') ⟹
    Key k ⊏  node_term m' ∧
    m' ∈ nodes b ∧
    k ∉ KP ∧
    (∀a ba. (a, ba) ≺⇩b m' ⟶ (a, ba) ∈ nodes b ⟶ Key k ⊏  node_term (a, ba) ⟶ k ∈ KP) ⟹
    b ∈ bundles ⟹
    fst m' ∈ Σ ⟹
    (∃A B Na Nb. is_initiator (fst m') A B Na Nb) ∨
    (∃A B Na Nb. is_responder (fst m') A B Na Nb)

It can be seen that we assume that strand can not be Is_penetrator_strand, so it must be is_initiator and is_responder. Second question that how to apply the definition into lemma prove.

isabelle
1 Answers

I am not familiar with def, but it seems that the constant being defined is Sigma, and the name of the fact that Sigma = ... is NSL_1. So you'd need

definition NSL_1:
"\<Sigma> == {s. Is_penetrator_strand s |
          (EX A B Na Nb.  is_initiator s  A B Na Nb) |
          (EX A B Na Nb.  is_responder s A B Na Nb)
       }"

Then you can do unfolding NSL_1 or apply (unfold NSL_1) or apply (auto simp add: NSL_1), whatever you need.

user_58639870
Related