Add snapshot of generated Isabelle theories

Currently contains Lem and Sail libraries, and RISC-V and CHERI-MIPS specs.

1 files changed, 75 insertions, 0 deletions

diff --git a/snapshots/isabelle/lib/lem/Lem_bool.thy b/snapshots/isabelle/lib/lem/Lem_bool.thy
new file mode 100644
index 00000000..75142160
--- /dev/null
+++ b/snapshots/isabelle/lib/lem/Lem_bool.thy
@@ -0,0 +1,75 @@
+chapter \<open>Generated by Lem from bool.lem.\<close>
+
+theory "Lem_bool" 
+
+imports 
+ 	 Main
+
+begin 
+
+ 
+
+(* The type bool is hard-coded, so are true and false *)
+
+(* ----------------------- *)
+(* not                     *)
+(* ----------------------- *)
+
+(*val not : bool -> bool*)
+(*let not b=  match b with
+  | true -> false
+  | false -> true
+end*)
+
+(* ----------------------- *)
+(* and                     *)
+(* ----------------------- *)
+
+(*val && [and] : bool -> bool -> bool*)
+(*let && b1 b2=  match (b1, b2) with
+  | (true, true) -> true
+  | _ -> false
+end*)
+
+
+(* ----------------------- *)
+(* or                      *)
+(* ----------------------- *)
+
+(*val || [or] : bool -> bool -> bool*)
+(*let || b1 b2=  match (b1, b2) with
+  | (false, false) -> false
+  | _ -> true
+end*)
+
+
+(* ----------------------- *)
+(* implication             *)
+(* ----------------------- *)
+
+(*val --> [imp] : bool -> bool -> bool*)
+(*let --> b1 b2=  match (b1, b2) with
+  | (true, false) -> false
+  | _ -> true
+end*)
+
+
+(* ----------------------- *)
+(* equivalence             *)
+(* ----------------------- *)
+
+(*val <-> [equiv] : bool -> bool -> bool*)
+(*let <-> b1 b2=  match (b1, b2) with
+  | (true, true) -> true
+  | (false, false) -> true
+  | _ -> false
+end*)
+
+
+(* ----------------------- *)
+(* xor                     *)
+(* ----------------------- *)
+
+(*val xor : bool -> bool -> bool*)
+
+end