如何解决Isar文本的证明状态

Question

我正在根据证明状态和isar文本写一个引理，并且遇到了一些困难。有证据表明

(y, z) ∈ (edges b)⇧+ ∪ {(a, n2). a ≼⇩b n1} ⟹
    n1 ∈ nodes b ⟹ n2 ∉ nodes b ⟹ y ≺⇩b z ⟶ y ≠ z ⟹ z = n2 ⟹ b ∈ bundles ⟹ y ≠ z

根据提示，我试着写下下面的代码：

(y, z) \<in> (edges b)\<^sup>+ \<union> {(a, n2). (a, n1) \<in> (edges b)\<^sup>*} \<Longrightarrow> n1 \<in> nodes b\<Longrightarrow>
               n2 \<notin> nodes b\<Longrightarrow> (y, z) \<in> (edges b)\<^sup>+ \<longrightarrow> y \<noteq> z\<Longrightarrow> z = n2\<Longrightarrow> b \<in> bundles\<Longrightarrow> y \<noteq> z"

但它提到，未能细化任何挂起的目标本地语句，无法细化任何挂起的目标，试图通过导出规则解决目标的尝试失败：

 ((y, z) ∈ (edges b)⇧+ ∪ {(a, n2). a ≼⇩b n1}) ⟹
  (n1 ∈ nodes b) ⟹
  (n2 ∉ nodes b) ⟹ (y ≺⇩b z ⟶ y ≠ z) ⟹ (z = n2) ⟹ (b ∈ bundles) ⟹ y ≠ z

我看到这里有额外的括号，如何解决它。谢谢。

定义：

datatype
  Sign=positive  ("+"  100)
  |negative ("-" 100)



typedecl sigma

type_synonym signed_msg="Sign\<times>  msg"
type_synonym node=" sigma \<times> nat"

type_synonym strand_space="sigma \<Rightarrow> signed_msg  list "


consts
  Sigma_set::"sigma set" ("\<Sigma>")

  SP::"strand_space"

definition Domain::"node set" where
  "Domain == {(n1,i). n1 \<in>  \<Sigma>  \<and> i < length (SP n1)}"

definition strand::"node \<Rightarrow> sigma" where
  "strand n==fst n"

definition index ::"node \<Rightarrow> nat" where
  "index n == snd n"

definition node_sign ::"node \<Rightarrow> Sign" where
   "node_sign n ==fst (nth (SP(fst(n))) (snd(n)) )"



definition 
  node_term ::"node\<Rightarrow>msg" where
  "node_term n==  snd (nth (SP(fst(n))) (snd(n)) )"

definition  casual1:: "( node  \<times> node ) set "  where
  "casual1 == { (n1,n2) . n1 \<in>  Domain \<and> n2 \<in>  Domain \<and>
  node_sign n1= +  \<and>
  node_sign n2= -
  \<and>  node_term n1= node_term n2 
  \<and>  strand n1 \<noteq> strand n2    
  } "

syntax
  "_casual1"::" node \<Rightarrow>node\<Rightarrow>bool" (infix "\<rightarrow>" 100)
translations
  "n1\<rightarrow>n2 "=="(n1 ,n2) \<in> CONST casual1"

 


definition  casual2::"(node  \<times> node) set" where
  "casual2 ==  { (n1,n2) . n1 \<in>  Domain \<and> n2 \<in>  Domain  \<and>
   (strand n1)=   (strand n2 ) \<and> Suc (index n1)=index n2} "

syntax
  "_casual2"::" node \<Rightarrow>node\<Rightarrow>bool" (infix "\<Rightarrow>" 50)
translations
  "n1\<Rightarrow>n2 "=="(n1 ,n2):CONST casual2"

syntax
  "_casual2Trans"::" node \<Rightarrow>node\<Rightarrow>bool" (infix "\<Rightarrow>\<^sup>+" 50)

translations
  "n1\<Rightarrow>\<^sup>+ n2 "=="(n1 ,n2):CONST casual2⇧+"

syntax
  "_casual2TransReflex"::" node \<Rightarrow>node\<Rightarrow>bool" (infix "\<Rightarrow>\<^sup>*" 50)
translations
  "n1\<Rightarrow>\<^sup>*n2 "=="(n1 ,n2):CONST casual2^*"

definition  casual3::"(node  \<times> node) set" where
  "casual3 ==  { (n1,n2) . n1\<rightarrow>n2 \<or>(n1, n2):(casual2⇧+) }"

syntax
  "_casual3"::" node \<Rightarrow>node\<Rightarrow>bool" (infix "\<mapsto> " 50)
translations
  "n1\<mapsto> n2 "=="(n1 ,n2): CONST casual3"


type_synonym  edge="node  \<times> node"
type_synonym  graph="node set \<times> edge set"

 




definition  Atoms::"msg set" where
  "Atoms=={a. (\<exists> ag. a=Agent ag) \<or>  (\<exists> n. a=Number n) 
  \<or>(\<exists> n. a=Nonce n) | (\<exists> k. a=Key k)}"
syntax
  Is_atom::"msg \<Rightarrow>  bool"
translations
  "Is_atom m"=="m  \<in> CONST Atoms"

definition KP::"key set" where
"KP=={k. \<exists> A. (k=pubK A)|(A \<in> bad \<and>(k=priK A |k=shrK A))}"

definition T:: "msg set" where
"T== {t. t: Atoms\<and> (\<forall> k. t \<noteq>   Key k)}"


definition  Is_K_strand::"sigma \<Rightarrow> bool " where
  "Is_K_strand KS ==   (\<exists> k.  k\<in> KP \<and> (SP KS)=[(+, Key k)])"


definition
  Is_T_strand::"sigma \<Rightarrow> bool" where
  "Is_T_strand KS==   (\<exists> t. t \<in> T  \<and>  (SP KS)=[(+,  t)]) "


definition
  Is_E_strand ::"sigma \<Rightarrow> bool " where
  "Is_E_strand KS ==   (\<exists> k. \<exists> h.  (SP KS)=[(-, (Key k)),(-,h),(+, (Crypt k h))])"

definition
  Is_D_strand::"sigma \<Rightarrow>bool" where
  "Is_D_strand KS==  (\<exists> k. \<exists> k'. \<exists> h. k'=invKey k\<and> (SP KS)=[(-, (Key k')),(-, (Crypt k h)),(+,h)])"

definition
  Is_Cat_strand::"sigma \<Rightarrow>bool" where
  "Is_Cat_strand KS==  (\<exists> g. \<exists> h.  (SP KS)=[(-, g),(-,  h),(+, MPair g h)])"  

definition
  Is_Sep_strand::"sigma \<Rightarrow>bool" where
  "Is_Sep_strand KS==  (\<exists> g. \<exists> h.  (SP KS)=[(-, MPair g h),(+,  g),(+,  h)])"


definition
  Is_Flush_strand::"sigma \<Rightarrow>bool" where
  "Is_Flush_strand KS==  (\<exists> g.   (SP KS)=[(-, g )])"

definition
  Is_Tee_strand::"sigma \<Rightarrow>bool" where
  "Is_Tee_strand KS==  (\<exists> g.  (SP KS)=[(-, g),(+,  g),(+,  g )])"  

definition Is_penetrator_strand:: "sigma \<Rightarrow> bool" where
"Is_penetrator_strand s==
     (  Is_Tee_strand s | Is_Flush_strand s | Is_Cat_strand s |
        Is_Sep_strand s |  Is_E_strand s | Is_D_strand s |
        Is_T_strand s | Is_K_strand s)"

definition Is_regular_strand :: "sigma \<Rightarrow>bool" where
  "Is_regular_strand s==\<not> ( Is_penetrator_strand s)"



definition nodes::"graph \<Rightarrow> node set" where
  "nodes b== fst b"

definition edges::"graph \<Rightarrow> edge set" where
  "edges  b == snd b"


inductive_set bundles :: "graph set" where
  Nil[intro!] : "({},{}):bundles" |
  Add_positive1[intro!]: "\<lbrakk> b \<in> bundles; 
      (node_sign n2) = +;
      n2 \<in> Domain;
      n2 \<notin> (nodes b);
      0 < index n2 ;
      n1 \<in>  nodes  b;
      n1\<Rightarrow> n2
      \<rbrakk>\<Longrightarrow>
      ({n2} \<union> (nodes b), {(n1, n2)} \<union> (edges b)) \<in> bundles" |

  Add_positive2[intro!]: "\<lbrakk> b \<in>   bundles; 
      node_sign n2=+;
      n2 \<notin> (nodes b);
      n2 \<in> Domain;
      index n2=0 
      \<rbrakk>
      \<Longrightarrow>
  ({n2} \<union> nodes b,  edges b) \<in> bundles" |

  Add_negtive1[intro!]: "\<lbrakk> b \<in>   bundles; 
      node_sign n2=-; 
      n2 \<notin> nodes b;               
      ((strand  n1 \<noteq> strand n2)\<and> (n1 \<rightarrow> n2) \<and> (n1  \<in>  nodes b) \<and> (\<forall> n3. ( (n3  \<in>  nodes b)\<longrightarrow> (n1,n3) \<notin>   edges b)) );
      0 < index n2 ;
      n1' \<in>  nodes b;
      n1'\<Rightarrow>n2
      \<rbrakk> \<Longrightarrow>
  ({n2} \<union> nodes b,  {(n1, n2), (n1' , n2)} \<union> edges b) \<in> bundles" |

  Add_negtive2: "\<lbrakk> b \<in>   bundles; 
      node_sign n2= -;
      n2 \<notin> nodes b;               
      ((strand  n1 \<noteq> strand n2)\<and> (n1 \<rightarrow> n2) \<and> (n1  \<in>  nodes b) \<and> (\<forall> n3. ( (n3  \<in>  nodes b)\<longrightarrow> (n1,n3) \<notin>   edges b)) );
      index n2=0
      \<rbrakk> \<Longrightarrow>
    ({n2} \<union> nodes b, {(n1, n2)} \<union> edges b) \<in> bundles"  

lemma bundle_edge_is_anti2:
  assumes A:"b \<in> bundles" 
  shows "y \<prec>\<^sub>b z\<longrightarrow> y\<noteq>z"
  using A
  proof induct
  case Nil show ?case 
    by(unfold edges_def, auto)
  next
    fix b n1 n2
    assume a1:"b \<in> bundles" 
      and IH:" (y, z) \<in> (edges b)\<^sup>+ \<longrightarrow> y \<noteq> z"
      and a2:" node_sign n2 = +" 
      and a3:" n2 \<in> Domain" 
      and a4:" n2 \<notin> nodes b"
      and a5:" 0 < index n2" 
      and a6:" n1 \<in> nodes b" 
      and a7:" n1 \<Rightarrow> n2"
    show "(y, z) \<in> (edges ({n2} \<union> nodes b, {(n1, n2)} \<union> edges b))\<^sup>+ \<longrightarrow> y\<noteq>z"
    proof
      assume a8:"(y, z) \<in> (edges ({n2} \<union> nodes b, {(n1, n2)} \<union> edges b))\<^sup>+"
      show "y\<noteq>z"
      proof(cases "z=n2")
        case True
        from this 
        have casehyp:"z=n2" .
        from a8 
        have a9:"(y,z):({(n1, n2)} \<union> edges b)\<^sup>+" 
        by(unfold edges_def, simp)
        from a9 
        have a10:"(y,z) \<in>  ((edges b)^+ Un {(a,c). (a,n1) \<in>  (edges b)^* \<and>  ((n2,c) \<in> (edges b)^*)})" 
        by (simp add:trancl_insert)
        from a10  
        have a12:"(y,z) \<in>  (edges b)^+ Un {(a,n2). (a,n1) \<in>  (edges b)^* }"   
        proof - 
        show "(y, z) \<in> (edges b)\<^sup>+ \<union> {(a, c). (a, n1) \<in> (edges b)\<^sup>* \<and> (n2, c) \<in> (edges b)\<^sup>*} 
          \<Longrightarrow> 
          (y, z) \<in> (edges b)\<^sup>+ \<union> {(a, n2). (a, n1) \<in> (edges b)\<^sup>*}"
          apply simp
          apply(erule disjE) 
          apply simp 
          by simp
        qed
        from a12 and a6 and a4 and IH and casehyp and A  
        show ?thesis
          by (metis (no_types, lifting) Un_insert_left a1 a2 a3 a5 a7 a8 bundle_is_closed bundle_is_closed1 bundles.Add_positive1 edges_def insert_iff snd_conv sup_bot.left_neutral tranclD)
      next
      case False
      from this have casehyp:"z\<noteq>n2" .
      from  a8 have a9:"(y,z) \<in> ({(n1, n2)} \<union> edges b)\<^sup>+" 
    by (unfold edges_def,simp)
      from A and  a8 and casehyp and a4 
      have a10: "(y,z) \<in>  (edges b)\<^sup>+" 
      proof -

        show "\<lbrakk>b \<in> bundles; (y, z) \<in> (edges ({n2} \<union> nodes b, {(n1, n2)} \<union> edges b))\<^sup>+; z \<noteq> n2;
           n2 \<notin> nodes b\<rbrakk> \<Longrightarrow> (y, z) \<in> (edges b)\<^sup>+ " 
          apply (simp add:edges_def trancl_insert)
          apply(erule disjE) 
          apply simp
          apply(erule conjE)
          apply(drule_tac a="n2" and b="z" in rtranclD)
          apply(fold edges_def)
          apply(auto dest:bundle_is_trans_closed22)
          done
      from a10 and IH show ?thesis by simp
    qed
  qed

在添加了声明[show_sorts]之后，我看到输出变成：

proof (state)
goal (1 subgoal):
 1. b ∈ bundles ⟹ y ≺⇩({n2} ∪ nodes b, {(n1, n2)} ∪ edges b) z ⟹ z ≠ n2 ⟹ n2 ∉ nodes b ⟹ y ≺⇩b z
variables:
  n1, n2, y, z :: sigma × nat
  b, b :: (sigma × nat) set × ((sigma × nat) × sigma × nat) set 
Failed to refine any pending goal 
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
  ((b::(sigma × nat) set × ((sigma × nat) × sigma × nat) set) ∈ bundles) ⟹
  ((y::sigma ×
       nat) ≺⇩({n2::sigma × nat} ∪ nodes b, {(n1::sigma × nat, n2)} ∪ edges b) (z::sigma × nat)) ⟹
  (z ≠ n2) ⟹ (n2 ∉ nodes b) ⟹ y ≺⇩b z

我认为没有错，如何解决它。

Answer 1

让我给出一些如何调试这种情况的方法。假设

fix x
assume A
assume B
assume C
show D

首先，注释掉所有假设，删除所有未使用的固定变量。

fix x
(*
assume A
assume B
assume C
*)
show D

如果您仍然有错误，那么您的错误在结论或修复的类型中。

如果它有效的话，很好，错误来自其中一个假设。把它们一个接一个地加入固定的变量，直到你发现有问题的变量为止。所以，就像：

fix x
(*
assume A
assume B
*)
assume C

show D