# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# 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 \<noteq> Get f"
+  by (metis subI wf_asym wf_sub)
+
+
 function
   sp\<^sub>\<mu>_comp :: "('a, 'b, 'c) sp\<^sub>\<mu> \<Rightarrow> ('d, 'a, ('d, 'a) sp\<^sub>\<nu>) sp\<^sub>\<mu> \<Rightarrow> ('d, 'b, 'c \<times> ('d, 'a) sp\<^sub>\<nu>) sp\<^sub>\<mu>"
   (infixl "o\<^sub>\<mu>" 65)
@@ -63,7 +67,8 @@
 | "Get f o\<^sub>\<mu> Put b sp = f b o\<^sub>\<mu> out sp"
 | "Get f o\<^sub>\<mu> Get g = Get (\<lambda>a. Get f o\<^sub>\<mu> 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>\<nu>_comp (infixl "o\<^sub>\<nu>" 65) where
   "out (sp o\<^sub>\<nu> sp') = map_sp\<^sub>\<mu> id (\<lambda>(sp, sp'). sp o\<^sub>\<nu> sp') (out sp o\<^sub>\<mu> out sp')"