author nipkow Fri, 16 Oct 2020 15:09:41 +0200 changeset 72485 a0066948e7df parent 72484 32ac6d3d1623 child 72486 e4d707eb7d1b
renamed constant
```--- a/src/HOL/Data_Structures/Queue_2Lists.thy	Fri Oct 16 11:38:55 2020 +0200
+++ b/src/HOL/Data_Structures/Queue_2Lists.thy	Fri Oct 16 15:09:41 2020 +0200
@@ -19,8 +19,8 @@
fun deq :: "'a queue \<Rightarrow> 'a queue" where
"deq (os,is) = (if os = [] then (os,is) else norm(tl os,is))"

-fun front :: "'a queue \<Rightarrow> 'a" where
-"front (a # os,is) = a"
+fun first :: "'a queue \<Rightarrow> 'a" where
+"first (a # os,is) = a"

fun is_empty :: "'a queue \<Rightarrow> bool" where
"is_empty (os,is) = (os = [])"
@@ -35,7 +35,7 @@
text \<open>Implementation correctness:\<close>

interpretation Queue
-where empty = "([],[])" and enq = enq and deq = deq and front = front
+where empty = "([],[])" and enq = enq and deq = deq and first = first
and is_empty = is_empty and list = list and invar = invar
proof (standard, goal_cases)
case 1 show ?case by (simp)
@@ -66,8 +66,8 @@
fun t_deq :: "'a queue \<Rightarrow> nat" where
"t_deq (os,is) = (if os = [] then 0 else t_norm(tl os,is)) + 1"

-fun t_front :: "'a queue \<Rightarrow> nat" where
-"t_front (a # os,is) = 1"
+fun t_first :: "'a queue \<Rightarrow> nat" where
+"t_first (a # os,is) = 1"

fun t_is_empty :: "'a queue \<Rightarrow> nat" where
"t_is_empty (os,is) = 1"```
```--- a/src/HOL/Data_Structures/Queue_Spec.thy	Fri Oct 16 11:38:55 2020 +0200
+++ b/src/HOL/Data_Structures/Queue_Spec.thy	Fri Oct 16 15:09:41 2020 +0200
@@ -11,7 +11,7 @@
locale Queue =
fixes empty :: "'q"
fixes enq :: "'a \<Rightarrow> 'q \<Rightarrow> 'q"
-fixes front :: "'q \<Rightarrow> 'a"
+fixes first :: "'q \<Rightarrow> 'a"
fixes deq :: "'q \<Rightarrow> 'q"
fixes is_empty :: "'q \<Rightarrow> bool"
fixes list :: "'q \<Rightarrow> 'a list"
@@ -19,7 +19,7 @@
assumes list_empty:    "list empty = []"
assumes list_enq:      "invar q \<Longrightarrow> list(enq x q) = list q @ [x]"
assumes list_deq:      "invar q \<Longrightarrow> list(deq q) = tl(list q)"
-assumes list_front:    "invar q \<Longrightarrow> \<not> list q = [] \<Longrightarrow> front q = hd(list q)"
+assumes list_first:    "invar q \<Longrightarrow> \<not> list q = [] \<Longrightarrow> first q = hd(list q)"
assumes list_is_empty: "invar q \<Longrightarrow> is_empty q = (list q = [])"
assumes invar_empty:   "invar empty"
assumes invar_enq:     "invar q \<Longrightarrow> invar(enq x q)"```