lib/monads: use experiment for demo lemmas

Use the experiment context to discard demo lemmas from the theory in the
Monad session. Some of these demo lemmas confuse sledgehammer.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

lib/Monads/wp/Datatype_Schematic.thy

@@ -263,7 +263,7 @@ declare option.sel[datatype_schematic]
 declare list.sel(1,3)[datatype_schematic]
 declare sum.sel[datatype_schematic]
 
-locale datatype_schem_demo begin
+experiment begin
 
 lemma handles_nested_constructors:
   "\<exists>f. \<forall>y. f True (Some [x, (y, z)]) = y"

lib/Monads/wp/WPBang.thy

@@ -53,6 +53,9 @@ method_setup wpe = \<open>WP_Safe.wpe_args\<close>
 
 text \<open>Testing.\<close>
 
+experiment
+begin
+
 lemma
   assumes x: "\<lbrace> P \<rbrace> f \<lbrace> \<lambda>rv. Q \<rbrace>"
        and y: "\<lbrace> P \<rbrace> f \<lbrace> \<lambda>rv. R \<rbrace>"
@@ -71,3 +74,5 @@ lemma
   done
 
 end
+
+end

lib/Monads/wp/WPFix.thy

@@ -217,6 +217,9 @@ end
 
 method_setup wpfix = \<open>WPFix.method\<close>
 
+experiment
+begin
+
 lemma demo1:
   "(\<exists>Ia Ib Ic Id Ra.
     (Ia (Suc 0) \<longrightarrow> Qa)
@@ -267,3 +270,5 @@ lemma (in datatype_schem_demo) demo3:
   by (rule refl)
 
 end
+
+end

lib/Monads/wp/WP_Pre.thy

@@ -102,6 +102,9 @@ named_theorems wp_pre
 method wp_pre0 = pre_tac wp_pre
 method wp_pre = wp_pre0?
 
+experiment
+begin
+
 definition
   test_wp_pre :: "bool \<Rightarrow> bool \<Rightarrow> bool"
 where
@@ -121,3 +124,5 @@ lemma demo:
   done
 
 end
+
+end