From 33ba3043e776c9dd67204ff996e26a8d4bc4188c Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Mon, 2 Dec 2024 18:46:00 +1100
Subject: [PATCH] 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 |  2 +-
 lib/Monads/wp/WPBang.thy             |  5 +++++
 lib/Monads/wp/WPFix.thy              | 11 +++++++++--
 lib/Monads/wp/WP_Pre.thy             |  5 +++++
 4 files changed, 20 insertions(+), 3 deletions(-)

diff --git a/lib/Monads/wp/Datatype_Schematic.thy b/lib/Monads/wp/Datatype_Schematic.thy
index 9701c97e0b..9396a7fb94 100644
--- a/lib/Monads/wp/Datatype_Schematic.thy
+++ b/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"
diff --git a/lib/Monads/wp/WPBang.thy b/lib/Monads/wp/WPBang.thy
index e7f21e2d3a..0d845cb3dd 100644
--- a/lib/Monads/wp/WPBang.thy
+++ b/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
diff --git a/lib/Monads/wp/WPFix.thy b/lib/Monads/wp/WPFix.thy
index 619d43a0b9..c008cbdd2e 100644
--- a/lib/Monads/wp/WPFix.thy
+++ b/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
diff --git a/lib/Monads/wp/WP_Pre.thy b/lib/Monads/wp/WP_Pre.thy
index 82879d7d68..836435343f 100644
--- a/lib/Monads/wp/WP_Pre.thy
+++ b/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