Rename roll_back_to to roll_back

input-output-hk · Sep 22, 2023 · 835363b · 835363b
1 parent 0b5be84
commit 835363b
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/src/Ouroboros-Mini_Protocols-Chain_Sync.thy b/src/Ouroboros-Mini_Protocols-Chain_Sync.thy
@@ -79,8 +79,8 @@ datatype phase =
   is_intersection_finding: IntersectionFinding |
   is_chain_update: ChainUpdate
 
-definition roll_back_to :: "('i \<Rightarrow> 'p) \<Rightarrow> 'i list \<Rightarrow> 'p \<Rightarrow> 'i list" where
-  [simp]: "roll_back_to \<psi> \<C> p = (THE \<C>\<^sub>1. \<exists>\<C>\<^sub>2. \<C> = \<C>\<^sub>1 @ \<C>\<^sub>2 \<and> \<psi> (last \<C>\<^sub>1) = p)"
+definition roll_back :: "('i \<Rightarrow> 'p) \<Rightarrow> 'i list \<Rightarrow> 'p \<Rightarrow> 'i list" where
+  [simp]: "roll_back \<psi> \<C> p = (THE \<C>\<^sub>1. \<exists>\<C>\<^sub>2. \<C> = \<C>\<^sub>1 @ \<C>\<^sub>2 \<and> \<psi> (last \<C>\<^sub>1) = p)"
 
 corec client_program where
   "client_program ph \<kappa> \<psi> \<C> = (
@@ -100,7 +100,7 @@ corec client_program where
           Cont (RollForward i) \<Rightarrow>
             client_program ph \<kappa> \<psi> (\<C> @ [i]) |
           Cont (RollBackward p) \<Rightarrow>
-            client_program ph \<kappa> \<psi> (roll_back_to \<psi> \<C> p) |
+            client_program ph \<kappa> \<psi> (roll_back \<psi> \<C> p) |
           Cont AwaitReply \<Rightarrow> \<comment> \<open>client is up to date\<close>
             \<up> Done;
             \<bottom>