# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1597838308 -3600
# Node ID 7fa9605b226cdd2b0bc605d99d2fd98c9ab018f0
# Parent  2d7619fc0e1afd710423703bba7f966574c33724
Another go with lex: now lexordp back in class ord

diff -r 2d7619fc0e1a -r 7fa9605b226c src/HOL/Corec_Examples/Stream_Processor.thy
--- a/src/HOL/Corec_Examples/Stream_Processor.thy	Tue Aug 18 21:45:24 2020 +0100
+++ b/src/HOL/Corec_Examples/Stream_Processor.thy	Wed Aug 19 12:58:28 2020 +0100
@@ -33,6 +33,9 @@
   show "P x" by (induct x) (auto intro: I)
 qed
 
+lemma Get_neq: "Get f \<noteq> f a"
+  by (metis subI wf_not_sym wf_sub)
+
 definition get where
   "get f = In (Get (\<lambda>a. out (f a)))"
 
@@ -40,8 +43,8 @@
   "run sp s = (case out sp of
      Get f \<Rightarrow> run (In (f (shd s))) (stl s)
    | Put b sp \<Rightarrow> b ## run sp s)"
-  by (relation "map_prod In In ` sub <*lex*> {}")
-    (auto simp: inj_on_def out_def split: sp\<^sub>\<nu>.splits intro: wf_map_prod_image)
+  by (relation "inv_image (map_prod In In ` sub) fst")
+     (auto simp: inj_on_def out_def split: sp\<^sub>\<nu>.splits intro: wf_map_prod_image)
 
 corec copy where
   "copy = In (Get (\<lambda>a. Put a copy))"
@@ -58,20 +61,26 @@
 lemma copy_sel[simp]: "out copy = Get (\<lambda>a. Put a copy)"
   by (subst copy.code; simp)
 
+lemma wf_imp_irrefl:
+  assumes "wf r" shows "irrefl r" 
+  using wf_irrefl [OF assms] by (auto simp add: irrefl_def)
+
+
 corecursive sp_comp (infixl "oo" 65) where
   "sp oo sp' = (case (out sp, out sp') of
       (Put b sp, _) \<Rightarrow> In (Put b (sp oo sp'))
     | (Get f, Put b sp) \<Rightarrow> In (f b) oo sp
     | (_, Get g) \<Rightarrow> get (\<lambda>a. (sp oo In (g a))))"
-  by (relation "map_prod In In ` sub <*lex*> map_prod In In ` sub")
-    (auto simp: inj_on_def out_def split: sp\<^sub>\<nu>.splits intro: wf_map_prod_image)
+  apply(relation "map_prod In In ` sub <*lex*> map_prod In In ` sub")
+    apply(auto simp: inj_on_def out_def split: sp\<^sub>\<nu>.splits intro: wf_map_prod_image)
+  by (metis Get_neq)
 
 lemma run_copy_unique:
-    "(\<And>s. h s = shd s ## h (stl s)) \<Longrightarrow> h = run copy"
-apply corec_unique
-apply(rule ext)
-apply(subst copy.code)
-apply simp
-done
+  "(\<And>s. h s = shd s ## h (stl s)) \<Longrightarrow> h = run copy"
+  apply corec_unique
+  apply(rule ext)
+  apply(subst copy.code)
+  apply simp
+  done
 
 end
diff -r 2d7619fc0e1a -r 7fa9605b226c src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Aug 18 21:45:24 2020 +0100
+++ b/src/HOL/List.thy	Wed Aug 19 12:58:28 2020 +0100
@@ -6748,7 +6748,7 @@
   Author: Andreas Lochbihler
 \<close>
 
-context order
+context ord
 begin
 
 context
@@ -6812,8 +6812,8 @@
 
 end
 
-declare order.lexordp_simps [simp, code]
-declare order.lexordp_eq_simps [code, simp]
+declare ord.lexordp_simps [simp, code]
+declare ord.lexordp_eq_simps [code, simp]
 
 context order
 begin
diff -r 2d7619fc0e1a -r 7fa9605b226c src/HOL/String.thy
--- a/src/HOL/String.thy	Tue Aug 18 21:45:24 2020 +0100
+++ b/src/HOL/String.thy	Wed Aug 19 12:58:28 2020 +0100
@@ -158,7 +158,7 @@
 proof -
   have "range (of_char :: char \<Rightarrow> nat) = of_char ` char_of ` {0::nat..<256}"
     by (auto simp add: range_nat_of_char intro!: image_eqI)
-  with inj_of_char [where ?'a = nat] show ?thesis 
+  with inj_of_char [where ?'a = nat] show ?thesis
     by (simp add: inj_image_eq_iff)
 qed
 
@@ -523,16 +523,16 @@
 begin
 
 qualified lift_definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
-  is "order.lexordp_eq (\<lambda>c d. of_char c < (of_char d :: nat))"
+  is "ord.lexordp_eq (\<lambda>c d. of_char c < (of_char d :: nat))"
   .
 
 qualified lift_definition less_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
-  is "order.lexordp (\<lambda>c d. of_char c < (of_char d :: nat))"
+  is "ord.lexordp (\<lambda>c d. of_char c < (of_char d :: nat))"
   .
 
 instance proof -
-  from linorder_char interpret linorder "order.lexordp_eq (\<lambda>c d. of_char c < (of_char d :: nat))"
-    "order.lexordp (\<lambda>c d. of_char c < (of_char d :: nat)) :: string \<Rightarrow> string \<Rightarrow> bool"
+  from linorder_char interpret linorder "ord.lexordp_eq (\<lambda>c d. of_char c < (of_char d :: nat))"
+    "ord.lexordp (\<lambda>c d. of_char c < (of_char d :: nat)) :: string \<Rightarrow> string \<Rightarrow> bool"
     by (rule linorder.lexordp_linorder)
   show "PROP ?thesis"
     by (standard; transfer) (simp_all add: less_le_not_le linear)
@@ -602,7 +602,7 @@
   fix cs
   assume "\<forall>c\<in>set cs. \<not> digit7 c"
   then show "map (String.ascii_of \<circ> char_of) (map of_char cs) = cs"
-    by (induction cs) (simp_all add: String.ascii_of_idem) 
+    by (induction cs) (simp_all add: String.ascii_of_idem)
 qed
 
 qualified lemma explode_code [code]:
@@ -628,7 +628,7 @@
 text \<open>Alternative constructor for generated computations\<close>
 
 context
-begin  
+begin
 
 qualified definition Literal' :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> String.literal \<Rightarrow> String.literal"
   where [simp]: "Literal' = String.Literal"
diff -r 2d7619fc0e1a -r 7fa9605b226c src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Tue Aug 18 21:45:24 2020 +0100
+++ b/src/HOL/Wellfounded.thy	Wed Aug 19 12:58:28 2020 +0100
@@ -64,6 +64,10 @@
   obtains "(a, a) \<notin> r"
   by (drule wf_not_refl[OF assms])
 
+lemma wf_imp_irrefl:
+  assumes "wf r" shows "irrefl r" 
+  using wf_irrefl [OF assms] by (auto simp add: irrefl_def)
+
 lemma wf_wellorderI:
   assumes wf: "wf {(x::'a::ord, y). x < y}"
     and lin: "OFCLASS('a::ord, linorder_class)"