From aff3d43d9865e7b8d082f0c239d2c73eee1fb291 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Thu, 21 Jan 2021 00:52:13 +0000
Subject: renamings

---
 spartan/lib/List.thy    | 6 +++---
 spartan/lib/Maybe.thy   | 4 ++--
 spartan/lib/Prelude.thy | 6 +++---
 3 files changed, 8 insertions(+), 8 deletions(-)

(limited to 'spartan/lib')

diff --git a/spartan/lib/List.thy b/spartan/lib/List.thy
index 1501221..4beb9b6 100644
--- a/spartan/lib/List.thy
+++ b/spartan/lib/List.thy
@@ -114,7 +114,7 @@ Lemma head_type [type]:
 Lemma head_of_cons [comp]:
   assumes "A: U i" "x: A" "xs: List A"
   shows "head (x # xs) \<equiv> some x"
-  unfolding head_def by reduce
+  unfolding head_def by compute
 
 Lemma tail_type [type]:
   assumes "A: U i" "xs: List A"
@@ -124,7 +124,7 @@ Lemma tail_type [type]:
 Lemma tail_of_cons [comp]:
   assumes "A: U i" "x: A" "xs: List A"
   shows "tail (x # xs) \<equiv> xs"
-  unfolding tail_def by reduce
+  unfolding tail_def by compute
 
 subsection \<open>Append\<close>
 
@@ -185,7 +185,7 @@ Lemma rev_type [type]:
 Lemma rev_nil [comp]:
   assumes "A: U i"
   shows "rev (nil A) \<equiv> nil A"
-  unfolding rev_def by reduce
+  unfolding rev_def by compute
 
 
 end
diff --git a/spartan/lib/Maybe.thy b/spartan/lib/Maybe.thy
index e06a07b..452acc2 100644
--- a/spartan/lib/Maybe.thy
+++ b/spartan/lib/Maybe.thy
@@ -40,7 +40,7 @@ Lemma Maybe_comp_none:
   shows "MaybeInd A C c\<^sub>0 f (none A) \<equiv> c\<^sub>0"
   using assms
   unfolding Maybe_def MaybeInd_def none_def some_def
-  by reduce
+  by compute
 
 Lemma Maybe_comp_some:
   assumes
@@ -52,7 +52,7 @@ Lemma Maybe_comp_some:
   shows "MaybeInd A C c\<^sub>0 f (some A a) \<equiv> f a"
   using assms
   unfolding Maybe_def MaybeInd_def none_def some_def
-  by reduce
+  by compute
 
 lemmas
   [form] = MaybeF and
diff --git a/spartan/lib/Prelude.thy b/spartan/lib/Prelude.thy
index 0043c1e..56adbfc 100644
--- a/spartan/lib/Prelude.thy
+++ b/spartan/lib/Prelude.thy
@@ -116,7 +116,7 @@ Lemma if_true:
   shows "ifelse C true a b \<equiv> a"
   unfolding ifelse_def true_def
   using assms unfolding Bool_def true_def false_def
-  by reduce
+  by compute
 
 Lemma if_false:
   assumes
@@ -126,7 +126,7 @@ Lemma if_false:
   shows "ifelse C false a b \<equiv> b"
   unfolding ifelse_def false_def
   using assms unfolding Bool_def true_def false_def
-  by reduce
+  by compute
 
 lemmas
   [form] = BoolF and
@@ -145,7 +145,7 @@ translations "if x then a else b" \<leftharpoondown> "CONST ifelse C x a b"
 
 subsection \<open>Logical connectives\<close>
 
-definition not ("!_") where "not x \<equiv> ifelse (K Bool) x false true"
+definition not ("!_") where "!x \<equiv> ifelse (K Bool) x false true"
 
 
 end
-- 
cgit v1.2.3