# HG changeset patch
# User nipkow
# Date 1603344685 -7200
# Node ID 7d7fa4e35053e50a0715965b886c2e094e2640b6
# Parent  d59242549b7fa67192ae2cd9932a40a491e2b583# Parent  f3ec4c151ab1ec3c77ffeb1a1c8ee7b2355a7ac1
merged

diff -r d59242549b7f -r 7d7fa4e35053 src/HOL/Data_Structures/Queue_2Lists.thy
--- a/src/HOL/Data_Structures/Queue_2Lists.thy	Wed Oct 21 21:59:20 2020 +0200
+++ b/src/HOL/Data_Structures/Queue_2Lists.thy	Thu Oct 22 07:31:25 2020 +0200
@@ -11,25 +11,25 @@
 type_synonym 'a queue = "'a list \<times> 'a list"
 
 fun norm :: "'a queue \<Rightarrow> 'a queue" where
-"norm (os,is) = (if os = [] then (rev is, []) else (os,is))"
+"norm (fs,rs) = (if fs = [] then (rev rs, []) else (fs,rs))"
 
 fun enq :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where
-"enq a (os,is) = norm(os, a # is)"
+"enq a (fs,rs) = norm(fs, a # rs)"
 
 fun deq :: "'a queue \<Rightarrow> 'a queue" where
-"deq (os,is) = (if os = [] then (os,is) else norm(tl os,is))"
+"deq (fs,rs) = (if fs = [] then (fs,rs) else norm(tl fs,rs))"
 
 fun first :: "'a queue \<Rightarrow> 'a" where
-"first (a # os,is) = a"
+"first (a # fs,rs) = a"
 
 fun is_empty :: "'a queue \<Rightarrow> bool" where
-"is_empty (os,is) = (os = [])"
+"is_empty (fs,rs) = (fs = [])"
 
 fun list :: "'a queue \<Rightarrow> 'a list" where
-"list (os,is) = os @ rev is"
+"list (fs,rs) = fs @ rev rs"
 
 fun invar :: "'a queue \<Rightarrow> bool" where
-"invar (os,is) = (os = [] \<longrightarrow> is = [])"
+"invar (fs,rs) = (fs = [] \<longrightarrow> rs = [])"
 
 
 text \<open>Implementation correctness:\<close>
@@ -58,29 +58,29 @@
 text \<open>Running times:\<close>
 
 fun t_norm :: "'a queue \<Rightarrow> nat" where
-"t_norm (os,is) = (if os = [] then length is else 0) + 1"
+"t_norm (fs,rs) = (if fs = [] then length rs else 0) + 1"
 
 fun t_enq :: "'a \<Rightarrow> 'a queue \<Rightarrow> nat" where
-"t_enq a (os,is) = t_norm(os, a # is)"
+"t_enq a (fs,rs) = t_norm(fs, a # rs)"
 
 fun t_deq :: "'a queue \<Rightarrow> nat" where
-"t_deq (os,is) = (if os = [] then 0 else t_norm(tl os,is)) + 1"
+"t_deq (fs,rs) = (if fs = [] then 0 else t_norm(tl fs,rs)) + 1"
 
 fun t_first :: "'a queue \<Rightarrow> nat" where
-"t_first (a # os,is) = 1"
+"t_first (a # fs,rs) = 1"
 
 fun t_is_empty :: "'a queue \<Rightarrow> nat" where
-"t_is_empty (os,is) = 1"
+"t_is_empty (fs,rs) = 1"
 
 text \<open>Amortized running times:\<close>
 
 fun \<Phi> :: "'a queue \<Rightarrow> nat" where
-"\<Phi>(os,is) = length is"
+"\<Phi>(fs,rs) = length rs"
 
-lemma a_enq: "t_enq a (os,is) + \<Phi>(enq a (os,is)) - \<Phi>(os,is) \<le> 2"
+lemma a_enq: "t_enq a (fs,rs) + \<Phi>(enq a (fs,rs)) - \<Phi>(fs,rs) \<le> 2"
 by(auto)
 
-lemma a_deq: "t_deq (os,is) + \<Phi>(deq (os,is)) - \<Phi>(os,is) \<le> 2"
+lemma a_deq: "t_deq (fs,rs) + \<Phi>(deq (fs,rs)) - \<Phi>(fs,rs) \<le> 2"
 by(auto)
 
 end