Add/generate Isabelle lemmas about the monad lifting

Architecture-specific lemmas about concrete registers and types are generated
and written to a file <prefix>_lemmas.thy, generic lemmas are in the
theories *_extras.thy in lib/isabelle.  In particular, State_extras contains
simplification lemmas about the lifting from prompt to state monad.

1 files changed, 15 insertions, 58 deletions

diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 756bb699..728014eb 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -10,81 +10,38 @@ let rec iter_aux i f xs = match xs with
   | [] -> return ()
   end
 
+declare {isabelle} termination_argument iter_aux = automatic
+
 val iteri : forall 'rv 'a 'e. (integer -> 'a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e
 let iteri f xs = iter_aux 0 f xs
 
 val iter : forall 'rv 'a 'e. ('a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e
 let iter f xs = iteri (fun _ x -> f x) xs
 
+val foreachM : forall 'a 'rv 'vars 'e.
+  list 'a -> 'vars -> ('a -> 'vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
+let rec foreachM [] vars _ = return vars
+and foreachM (x :: xs) vars body =
+  body x vars >>= fun vars ->
+  foreachM xs vars body
 
-val foreachM_inc : forall 'rv 'vars 'e. (integer * integer * integer) -> 'vars ->
-                  (integer -> 'vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
-let rec foreachM_inc (i,stop,by) vars body =
-  if (by > 0 && i <= stop) || (by < 0 && stop <= i)
-  then
-    body i vars >>= fun vars ->
-    foreachM_inc (i + by,stop,by) vars body
-  else return vars
-
-
-val foreachM_dec : forall 'rv 'vars 'e. (integer * integer * integer) -> 'vars ->
-                  (integer -> 'vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
-let rec foreachM_dec (i,stop,by) vars body =
-  if (by > 0 && i >= stop) || (by < 0 && stop >= i)
-  then
-    body i vars >>= fun vars ->
-    foreachM_dec (i - by,stop,by) vars body
-  else return vars
-
-val while_PP : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
-let rec while_PP vars cond body =
-  if cond vars then while_PP (body vars) cond body else vars
-
-val while_PM : forall 'rv 'vars 'e. 'vars -> ('vars -> bool) ->
-                ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
-let rec while_PM vars cond body =
-  if cond vars then
-    body vars >>= fun vars -> while_PM vars cond body
-  else return vars
+declare {isabelle} termination_argument foreachM = automatic
 
-val while_MP : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
-                ('vars -> 'vars) -> monad 'rv 'vars 'e
-let rec while_MP vars cond body =
-  cond vars >>= fun cond_val ->
-  if cond_val then while_MP (body vars) cond body else return vars
 
-val while_MM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
+val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
                 ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
-let rec while_MM vars cond body =
+let rec whileM vars cond body =
   cond vars >>= fun cond_val ->
   if cond_val then
-    body vars >>= fun vars -> while_MM vars cond body
+    body vars >>= fun vars -> whileM vars cond body
   else return vars
 
-val until_PP : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
-let rec until_PP vars cond body =
-  let vars = body vars in
-  if (cond vars) then vars else until_PP (body vars) cond body
-
-val until_PM : forall 'rv 'vars 'e. 'vars -> ('vars -> bool) ->
-                ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
-let rec until_PM vars cond body =
-  body vars >>= fun vars ->
-  if (cond vars) then return vars else until_PM vars cond body
-
-val until_MP : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
-                ('vars -> 'vars) -> monad 'rv 'vars 'e
-let rec until_MP vars cond body =
-  let vars = body vars in
-  cond vars >>= fun cond_val ->
-  if cond_val then return vars else until_MP vars cond body
-
-val until_MM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
+val untilM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
                 ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
-let rec until_MM vars cond body =
+let rec untilM vars cond body =
   body vars >>= fun vars ->
   cond vars >>= fun cond_val ->
-  if cond_val then return vars else until_MM vars cond body
+  if cond_val then return vars else untilM vars cond body
 
 (*let write_two_regs r1 r2 vec =
   let is_inc =