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)
@@ -260,10 +263,14 @@ lemma demo2:
 \<comment> \<open>
   Shows how to use @{attribute datatype_schematic} rules as "accessors".
 \<close>
-lemma (in datatype_schem_demo) demo3:
+datatype foo = basic (a:nat) (b:int) | another nat
+
+lemma demo3:
   "\<exists>x. \<forall>a b. x (basic a b) = a"
   apply (rule exI, (rule allI)+)
-  apply (wpfix add: get_basic_0.simps) \<comment> \<open>Only exposes `a` to the schematic.\<close>
+  apply (wpfix add: foo.sel(1)) \<comment> \<open>Only exposes `a` to the schematic.\<close>
   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