aboutsummaryrefslogtreecommitdiff
path: root/spartan/lib
diff options
context:
space:
mode:
Diffstat (limited to 'spartan/lib')
-rw-r--r--spartan/lib/List.thy6
-rw-r--r--spartan/lib/Maybe.thy4
-rw-r--r--spartan/lib/Prelude.thy6
3 files changed, 8 insertions, 8 deletions
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