How to solve the proof state about Isar text

Question

I'm writing a lemma according to the Proof state and isar text, and meet some difficult. There is a proof state that

(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

According to the tip, I try to write down below code:

(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"

But it mentions me that Failed to refine any pending goal Local statement fails to refine any pending goal Failed attempt to solve goal by exported rule:

 ((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

I see that there are extra brackets here, how to solve it. Thank you.

definition:

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

After I add the declare [[show_sorts]], I see that the output becomes:

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

I think there is no wrong, how to fix it.

Answer 1

Let me give some idea how to debug such cases. Assume

fix x
assume A
assume B
assume C
show D

First comment out all assumptions and remove all unused fixed variables.

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

If you still have the error, then your error is in the conclusion or the type of the fixes.

If it works, great, the error comes from one of the assumptions. Add them with the fixed variables one by one until you find the faulty one. So something like:

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

show D