From 7c34190f56bd6029d61d717a7038604b54538b2e Mon Sep 17 00:00:00 2001
From: Hernan Rajchert <hrajchert@gmail.com>
Date: Fri, 17 Mar 2023 10:47:09 -0300
Subject: [PATCH] Removed unused assumptions

---
 isabelle/Core/QuiescentResult.thy |  3 +--
 isabelle/Core/TimeRange.thy       |  2 +-
 isabelle/Core/Timeout.thy         | 18 +++++++++---------
 isabelle/Core/ValidState.thy      |  3 +--
 4 files changed, 12 insertions(+), 14 deletions(-)

diff --git a/isabelle/Core/QuiescentResult.thy b/isabelle/Core/QuiescentResult.thy
index 65fadf54..51c9c162 100644
--- a/isabelle/Core/QuiescentResult.thy
+++ b/isabelle/Core/QuiescentResult.thy
@@ -13,8 +13,7 @@ lemma reduceContractStepPayIsQuiescent :
                     warning = if paidMoney < moneyToPay then ReducePartialPay x21 x22 tok paidMoney moneyToPay else ReduceNoWarning;
                     (payment, finalAccs) = giveMoney x21 x22 tok paidMoney newAccs
                 in Reduced warning payment (sta\<lparr>accounts := finalAccs\<rparr>) x24) =
-       NotReduced \<Longrightarrow>
-       cont = Pay x21 x22 tok x23 x24 \<Longrightarrow> False"
+       NotReduced \<Longrightarrow> False"
   apply (cases "evalValue env sta x23 \<le> 0")
   apply simp
   apply (cases "min (moneyInAccount x21 tok (accounts sta)) (evalValue env sta x23) < (evalValue env sta x23)")
diff --git a/isabelle/Core/TimeRange.thy b/isabelle/Core/TimeRange.thy
index af2b07b9..82c9fe9a 100644
--- a/isabelle/Core/TimeRange.thy
+++ b/isabelle/Core/TimeRange.thy
@@ -214,7 +214,7 @@ lemma geIfNone_redListSize :
 
 
 lemma reduceStep_ifCaseLtCt_aux : "inInterval (a, b) (calculateNonAmbiguousInterval n ct (When x41 x42 x43)) \<Longrightarrow>
-                                   a \<le> b \<Longrightarrow> env = \<lparr>timeInterval = (a, b)\<rparr> \<Longrightarrow> b < x42 \<Longrightarrow> ct < x42"
+                                   a \<le> b \<Longrightarrow> b < x42 \<Longrightarrow> ct < x42"
   apply (induction x41)
    apply simp
    apply (smt (verit, best) OptBoundTimeInterval.inInterval.simps(3) inIntervalIdempotency1)
diff --git a/isabelle/Core/Timeout.thy b/isabelle/Core/Timeout.thy
index a9bb3ab7..820b1bda 100644
--- a/isabelle/Core/Timeout.thy
+++ b/isabelle/Core/Timeout.thy
@@ -40,8 +40,7 @@ lemma reduceClose_is_Close : "reduceContractUntilQuiescent env sta Close = Contr
   using reductionLoopClose_is_Close by blast
 
 lemma timedOutReduce_only_quiescent_in_close_When :
-  "minTime sta \<le> iniTime \<Longrightarrow>
-   maxTimeContract (When x41 x42 x43) \<le> iniTime \<Longrightarrow>
+  "maxTimeContract (When x41 x42 x43) \<le> iniTime \<Longrightarrow>
    iniTime \<le> endTime \<Longrightarrow>
    reduceContractStep \<lparr>timeInterval = (iniTime, endTime)\<rparr> (sta\<lparr>minTime := iniTime\<rparr>) (When x41 x42 x43) \<noteq> NotReduced"
   apply (induction x41)
@@ -119,7 +118,7 @@ lemma maxTimeNotAmbiguous : "maxTimeContract cont \<le> iniTime \<Longrightarrow
 
 
 lemma timedOutReduce_only_quiescent_in_close :
-  "minTime sta \<le> iniTime \<Longrightarrow>
+  "
    maxTimeContract c \<le> iniTime \<Longrightarrow>
    iniTime \<le> endTime \<Longrightarrow>
    reduceContractStep \<lparr>timeInterval = (iniTime, endTime)\<rparr> (sta\<lparr>minTime := iniTime\<rparr>) c = NotReduced \<Longrightarrow> c = Close"
@@ -167,7 +166,7 @@ lemma timedOutReduceStep_does_not_modify_minTime :
     apply (smt ReduceStepResult.inject State.ext_inject State.surjective State.update_convs(3) State.update_convs(4) reduceContractStep.simps(5))
     by simp
 
-lemma timedOutReduceContractLoop_closes_contract : "minTime sta \<le> iniTime \<Longrightarrow>
+lemma timedOutReduceContractLoop_closes_contract : "
     maxTimeContract cont \<le> iniTime \<Longrightarrow>
     iniTime \<le> endTime \<Longrightarrow>
     minTime sta = iniTime \<Longrightarrow>
@@ -187,13 +186,14 @@ lemma timedOutReduceContractLoop_closes_contract : "minTime sta \<le> iniTime \<
         apply simp
         apply simp
         apply simp
+
+        using facts maxTimeOnlyDecreases_reduceStep apply fastforce
         apply simp
-        using facts(3) facts(7) maxTimeOnlyDecreases_reduceStep apply fastforce
-        apply simp
-        using facts(5) facts(7) timedOutReduceStep_does_not_modify_minTime apply blast
-        by (metis (no_types, lifting) ReduceStepResult.simps(8) facts(6) facts(7) reductionLoop.simps)
+        using facts timedOutReduceStep_does_not_modify_minTime apply meson
+        using facts by (metis (no_types, lifting) ReduceStepResult.simps(8)  reductionLoop.simps)
       done
-    using timedOutReduce_only_quiescent_in_close apply fastforce
+    using timedOutReduce_only_quiescent_in_close
+    apply (metis SemanticsTypes.State.cases SemanticsTypes.State.select_convs(4) SemanticsTypes.State.update_convs(4) reductionLoopClose_is_Close)
     using maxTimeNotAmbiguous_reduceStep by blast
   done
 
diff --git a/isabelle/Core/ValidState.thy b/isabelle/Core/ValidState.thy
index 0d689df8..8db6439a 100644
--- a/isabelle/Core/ValidState.thy
+++ b/isabelle/Core/ValidState.thy
@@ -25,8 +25,7 @@ lemma refundOne_preserves_valid_map_accounts :
 lemma reductionStep_preserves_valid_state_Refund :
   "valid_state state \<Longrightarrow>
    reduceContractStep env state Close = Reduced wa ef newState newCont \<Longrightarrow>
-   state = \<lparr>accounts = oldAccounts, choices = oldChoices, boundValues = oldBoundValues, minTime = oldMinTime\<rparr> \<Longrightarrow>
-   newState = \<lparr>accounts = newAccounts, choices = newChoices, boundValues = newBoundValues, minTime = newMinTime\<rparr> \<Longrightarrow>
+   state = \<lparr>accounts = oldAccounts, choices = oldChoices, boundValues = oldBoundValues, minTime = oldMinTime\<rparr> \<Longrightarrow>   
    valid_state newState"
   apply (cases "refundOne oldAccounts")
   using refundOne_preserves_valid_map_accounts by auto