Removed unused lemmas

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"

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")

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)"

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)