# HG changeset patch # User paulson # Date 1597845482 -3600 # Node ID 7075fe8ffd76c80302cff513c98f27285d9317a6 # Parent 7fa9605b226cdd2b0bc605d99d2fd98c9ab018f0 more lex fixes diff -r 7fa9605b226c -r 7075fe8ffd76 src/HOL/Datatype_Examples/Stream_Processor.thy --- a/src/HOL/Datatype_Examples/Stream_Processor.thy Wed Aug 19 12:58:28 2020 +0100 +++ b/src/HOL/Datatype_Examples/Stream_Processor.thy Wed Aug 19 14:58:02 2020 +0100 @@ -55,6 +55,10 @@ show "P x" by (induct x) (auto intro: I) qed +lemma neq_Get [simp]: "f b \ Get f" + by (metis subI wf_asym wf_sub) + + function sp\<^sub>\_comp :: "('a, 'b, 'c) sp\<^sub>\ \ ('d, 'a, ('d, 'a) sp\<^sub>\) sp\<^sub>\ \ ('d, 'b, 'c \ ('d, 'a) sp\<^sub>\) sp\<^sub>\" (infixl "o\<^sub>\" 65) @@ -63,7 +67,8 @@ | "Get f o\<^sub>\ Put b sp = f b o\<^sub>\ out sp" | "Get f o\<^sub>\ Get g = Get (\a. Get f o\<^sub>\ g a)" by pat_completeness auto -termination by (relation "lex_prod sub sub") auto +termination + by (relation "lex_prod sub sub") auto primcorec sp\<^sub>\_comp (infixl "o\<^sub>\" 65) where "out (sp o\<^sub>\ sp') = map_sp\<^sub>\ id (\(sp, sp'). sp o\<^sub>\ sp') (out sp o\<^sub>\ out sp')"