theory Bug2
imports Main
begin
  datatype 'a M_nres = is_fail: FAIL | SPEC "'a \<Rightarrow> bool"

  definition "is_res m x \<equiv> case m of FAIL \<Rightarrow> True | SPEC P \<Rightarrow> P x"
  
  datatype ('a,'s) M_state = M_STATE (run: "'s \<Rightarrow> ('a\<times>'s) M_nres")
  
  lemma "\<lbrakk>\<forall>x y. (\<forall>xa s. is_fail (run (x xa) s) \<or>
                   is_fail (run (y xa) s) = is_fail (run (x xa) s) \<and>
                   (\<forall>a b. is_res (run (y xa) s) (a, b) = is_res (run (x xa) s) (a, b))) \<longrightarrow>
           (\<forall>s. is_fail (run (B x) s) \<or>
                is_fail (run (B y) s) = is_fail (run (B x) s) \<and>
                (\<forall>a b. is_res (run (B y) s) (a, b) = is_res (run (B x) s) (a, b)));
     \<And>y. \<forall>x ya. (\<forall>xa s. is_fail (run (x xa) s) \<or>
                         is_fail (run (ya xa) s) = is_fail (run (x xa) s) \<and>
                         (\<forall>a b. is_res (run (ya xa) s) (a, b) = is_res (run (x xa) s) (a, b))) \<longrightarrow>
                 (\<forall>s. is_fail (run (C y x) s) \<or>
                      is_fail (run (C y ya) s) = is_fail (run (C y x) s) \<and>
                      (\<forall>a b. is_res (run (C y ya) s) (a, b) = is_res (run (C y x) s) (a, b)))\<rbrakk>
    \<Longrightarrow> \<forall>x y. (\<forall>xa s.
                  is_fail (run (x xa) s) \<or>
                  is_fail (run (y xa) s) = is_fail (run (x xa) s) \<and>
                  (\<forall>a b. is_res (run (y xa) s) (a, b) = is_res (run (x xa) s) (a, b))) \<longrightarrow>
              (\<forall>s. is_fail (run (B x) s) \<or>
                   (\<exists>a b. is_res (run (B x) s) (a, b) \<and> is_fail (run (C a x) b)) \<or>
                   (is_fail (run (B y) s) \<or> (\<exists>a b. is_res (run (B y) s) (a, b) \<and> is_fail (run (C a y) b))) =
                   (is_fail (run (B x) s) \<or> (\<exists>a b. is_res (run (B x) s) (a, b) \<and> is_fail (run (C a x) b))) \<and>
                   (\<forall>a b. (is_fail (run (B y) s) \<or>
                           (\<exists>aa ba. is_res (run (B y) s) (aa, ba) \<and> is_res (run (C aa y) ba) (a, b))) =
                          (is_fail (run (B x) s) \<or>
                           (\<exists>aa ba. is_res (run (B x) s) (aa, ba) \<and> is_res (run (C aa x) ba) (a, b)))))"  
    apply (smt (z3))
    (** exception Fail raised (line 222 of "~~/src/HOL/Tools/SMT/z3_proof.ML"): Replaying the proof trace produced by Z3 failed: the bound "?2" is undeclared; this indicates a bug in Z3 *)    
  oops
    
end