From fd2fb82a734381a7ec8673419fe6bcebdcb1e8fe Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Tue, 5 Nov 2024 15:28:38 -0500
Subject: [PATCH] checkpoint

---
 SampCert/Foundations/While.lean | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/SampCert/Foundations/While.lean b/SampCert/Foundations/While.lean
index 380d0e0b..b9548be5 100644
--- a/SampCert/Foundations/While.lean
+++ b/SampCert/Foundations/While.lean
@@ -58,4 +58,19 @@ theorem probWhile_apply (cond : T → Bool) (body : T → SLang T) (init : T) (x
   · apply probWhileCut_monotonic
   · apply H
 
+
+-- A version of probWhile that proves normalization, when its arguments are all normal
+def SPMF_while (cond : T → Bool) (body : T → SPMF T) (init : T) : SPMF T :=
+  ⟨ probWhile cond (fun x => body x) init,
+    by
+      unfold probWhile
+      sorry ⟩
+
+lemma SPMF_while_eq (cond : T → Bool) (body : T → SPMF T) (init : T) :
+    ((SPMF_while cond body init) : SLang T) = (probWhile cond (fun x => body x) init) := by
+  simp [SPMF_while]
+
+
+
+
 end SLang