--- 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
--- 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
--- 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"
--- 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)"