theory Bug1
imports Main
begin

  named_theorems pw_inits \<open>Simp-Lemmas to start pointwise reasoning\<close>

  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"

  lemma is_res_simps[simp]:
    "is_res FAIL x"
    "is_res (SPEC P) x \<longleftrightarrow> P x"
    unfolding is_res_def by auto

  lemma nres_imp_res[simp]: "is_fail m \<Longrightarrow> is_res m x"
    apply (cases m) 
    by auto
  
    
  definition "ntspec n r \<equiv> if n then FAIL else SPEC (\<lambda>x. r x)"
  lemma ntspec_simps[simp]: 
    "is_fail (ntspec n P) = n"  
    "is_res (ntspec n P) x \<longleftrightarrow> n \<or> P x"
    unfolding ntspec_def
    by auto

          
  lemma pw_nres_eq_iff[pw_inits]: "a=b \<longleftrightarrow> (is_fail a = is_fail b) \<and> (\<forall>x. is_res a x = is_res b x)"  
    by (cases a; cases b; auto)
  
    
  definition "return_nres x \<equiv> SPEC (\<lambda>r. r=x)"
  
  fun bind_nres where
      "bind_nres FAIL _ = FAIL" 
    | "bind_nres (SPEC X) f = ntspec (\<exists>x. X x \<and> is_fail (f x)) (\<lambda>y. \<exists>x. X x \<and> is_res (f x) y)"

    
  lemma return_nres_pw[simp]: "\<not>is_fail (return_nres x)" "is_res (return_nres x) y \<longleftrightarrow> x=y" 
    by (auto simp: return_nres_def) 
    
    
        
  definition "assert_nres P \<equiv> if P then return_nres () else FAIL" 

  lemma assert_nres_pw[simp]: 
    "is_fail (assert_nres P) \<longleftrightarrow> \<not>P"
    "is_res (assert_nres P) x"
    unfolding assert_nres_def    
    by (auto simp: pw_inits)
      

  lemma "undefined" using ntspec_simps
    sledgehammer [provers=vampire]
    (** exception Fail raised (line 558 of "~~/src/HOL/Tools/ATP/atp_problem.ML"): unexpected term in first-order format *)
    oops    

end