theory i131214a__isaU_Trueprop_False_meta_eq_auto_hangs_PIDE
imports Complex_Main 
begin

declare[[show_sorts=true]]
declare[[show_brackets=true]]
declare[[show_question_marks=true]]
notation Trueprop ("_\<Colon>\<^sub>T" [1000] 1000)

(*With "Auto Methods" off, auto goes off and doesn't come back, if it's allowed
  to run very long.*)
  
lemma "Trueprop False == (!!f. !!a. f = (%a. a | f a) ==> (f a = a))"
apply(rule equal_intr_rule)
(*apply(auto)*)
oops


(*This direction with auto is the problem. I need to terminate it within less
  than about 5 seconds when I have "show_sorts=true".*)

lemma "(!!f. !!a. f = (%a. a | f a) ==> (f a = a)) ==> False"
(*apply(auto)*)
oops


(*No problem with blast to prove ==, instead of auto.*)

lemma "Trueprop False == (!!f. !!a. f = (%a. a | f a) ==> (f a = a))"
apply(rule equal_intr_rule)
apply(blast)
apply(blast) (*Failure messages here.*)
done


(*This direction with blast is okay, though there are failure messages.*)

lemma "(!!f. !!a. f = (%a. a | f a) ==> (f a = a)) ==> False"
apply(blast) (*Failure messages here.*)
done


(*The other direction with auto is okay.*)

lemma "False ==> (!!f. !!a. f = (%a. a | f a) ==> (f a = a))"
apply(auto)
done

end