From 85c61dfbec8c20cb0cd3d478e85580e20f806df5 Mon Sep 17 00:00:00 2001
From: Hernan Rajchert <hrajchert@gmail.com>
Date: Fri, 17 Mar 2023 11:44:49 -0300
Subject: [PATCH] Removed unused lemmas

---
 isabelle/Core/PositiveAccounts.thy        | 8 --------
 isabelle/Core/QuiescentResult.thy         | 6 ++----
 isabelle/Core/SingleInputTransactions.thy | 8 --------
 isabelle/Core/ValidState.thy              | 8 --------
 4 files changed, 2 insertions(+), 28 deletions(-)

diff --git a/isabelle/Core/PositiveAccounts.thy b/isabelle/Core/PositiveAccounts.thy
index 8447b4d0..afdca0e2 100644
--- a/isabelle/Core/PositiveAccounts.thy
+++ b/isabelle/Core/PositiveAccounts.thy
@@ -61,14 +61,6 @@ lemma positiveMoneyInAccountOrNoAccount_sublist_gtZero_different :
   apply (simp only:positiveMoneyInAccountOrNoAccount.simps findWithDefault.simps)
   by (metis MList.delete.simps(2) MList.different_delete_lookup)
 
-lemma positiveMoneyInAccountOrNoAccount_sublist_gtZero :
-    "valid_map ((accIdTok, money) # rest) \<Longrightarrow>
-     money > 0 \<Longrightarrow>
-    (\<forall>x tok. positiveMoneyInAccountOrNoAccount x tok ((accIdTok, money) # rest)) \<Longrightarrow> positiveMoneyInAccountOrNoAccount y tok2 rest"
-  apply (cases "accIdTok = (y, tok2)")
-  using positiveMoneyInAccountOrNoAccount_valid_zero apply auto[1]
-  using positiveMoneyInAccountOrNoAccount_sublist_gtZero_different by blast
-
 lemma positiveMoneyInAccountOrNoAccount_gtZero_preservation :
   "valid_map ((accIdTok, money) # rest) \<Longrightarrow>
    (\<forall>x tok. positiveMoneyInAccountOrNoAccount x tok ((accIdTok, money) # rest)) \<Longrightarrow> positiveMoneyInAccountOrNoAccount y tok2 rest"
diff --git a/isabelle/Core/QuiescentResult.thy b/isabelle/Core/QuiescentResult.thy
index 51c9c162..c8bd6f0e 100644
--- a/isabelle/Core/QuiescentResult.thy
+++ b/isabelle/Core/QuiescentResult.thy
@@ -2,9 +2,6 @@ theory QuiescentResult
 imports Semantics PositiveAccounts
 begin
 
-lemma reduceOne_onlyIfNonEmptyState : "refundOne acc = Some c \<Longrightarrow> acc \<noteq> []"
-  by auto
-
 lemma reduceContractStepPayIsQuiescent :
       "(let moneyToPay = evalValue env sta x23
         in if moneyToPay \<le> 0 then Reduced (ReduceNonPositivePay x21 x22 tok moneyToPay) ReduceNoPayment sta x24
@@ -149,7 +146,8 @@ lemma reductionLoop_reduce_monotonic : "reductionLoop True env sta cont wa ef =
     by simp
   done
 
-lemma reduceContractUntilQuiescent_ifDifferentReduced : "reduceContractUntilQuiescent si sta cont = ContractQuiescent reduce wa ef sta newCont \<Longrightarrow> cont \<noteq> newCont \<Longrightarrow> reduce"
+text "If we reduce the contract and the continuation has changed, then the reduced flag should be true"
+theorem reduceContractUntilQuiescent_ifDifferentReduced : "reduceContractUntilQuiescent si sta cont = ContractQuiescent reduce wa ef sta newCont \<Longrightarrow> cont \<noteq> newCont \<Longrightarrow> reduce"
   apply (simp only:reduceContractUntilQuiescent.simps)
   apply (simp only:reductionLoop.simps)
   apply (cases "reduceContractStep si sta cont")
diff --git a/isabelle/Core/SingleInputTransactions.thy b/isabelle/Core/SingleInputTransactions.thy
index b51d85f2..c4100d22 100644
--- a/isabelle/Core/SingleInputTransactions.thy
+++ b/isabelle/Core/SingleInputTransactions.thy
@@ -1211,14 +1211,6 @@ lemma transactionPrefixForSingleInput : "h # t = traceListToSingleInput nt \<Lon
   done
 
 
-lemma traceListToSingleInput_isSingleInput : "\<lparr>interval = inte, inputs = inp_h # inp_t\<rparr> # t = traceListToSingleInput t2 \<Longrightarrow> inp_t \<noteq> [] \<Longrightarrow> False"
-  apply (induction t2 rule:traceListToSingleInput.induct)
-  apply simp_all
-  subgoal for si inps rest
-    apply (induction si inps rule:inputsToTransactions.induct)
-    by simp_all
-  done
-
 fun isSingleInput :: "Transaction list \<Rightarrow> bool" where
 "isSingleInput [] = True" |
 "isSingleInput (h # t) = (length (inputs h) \<le> 1 \<and> isSingleInput t)"
diff --git a/isabelle/Core/ValidState.thy b/isabelle/Core/ValidState.thy
index 8db6439a..c3cc45e5 100644
--- a/isabelle/Core/ValidState.thy
+++ b/isabelle/Core/ValidState.thy
@@ -6,14 +6,6 @@ lemma valid_state_valid_accounts : "valid_state state \<Longrightarrow> valid_ma
   apply (cases state)
   by simp
 
-lemma valid_state_valid_choices : "valid_state state \<Longrightarrow> valid_map (choices state)"
-  apply (cases state)
-  by simp
-
-lemma valid_state_valid_boundValues : "valid_state state \<Longrightarrow> valid_map (boundValues state)"
-  apply (cases state)
-  by simp
-
 lemma refundOne_preserves_valid_map_accounts :
   "valid_map oldAccounts \<Longrightarrow>
    refundOne oldAccounts = Some ((party, money), newAccounts)