# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1498853620 -3600
# Node ID 78dd6bca5627e4028cdb5fc4c2ddff2ed5b9b184
# Parent  6670f2cb5741b4e73268fbec1417313b6cbb1ec5
updated

diff -r 6670f2cb5741 -r 78dd6bca5627 thys/Exercises.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/Exercises.thy	Fri Jun 30 21:13:40 2017 +0100
@@ -0,0 +1,216 @@
+theory Exercises
+  imports Lexer "~~/src/HOL/Library/Infinite_Set"
+begin
+
+section {* some fun tests *}
+
+fun
+ zeroable :: "rexp \<Rightarrow> bool"
+where
+  "zeroable (ZERO) \<longleftrightarrow> True"
+| "zeroable (ONE) \<longleftrightarrow> False"
+| "zeroable (CHAR c) \<longleftrightarrow> False"
+| "zeroable (ALT r1 r2) \<longleftrightarrow> zeroable r1 \<and> zeroable r2"
+| "zeroable (SEQ r1 r2) \<longleftrightarrow> zeroable r1 \<or> zeroable r2"
+| "zeroable (STAR r) \<longleftrightarrow> False"
+
+lemma zeroable_correctness:
+  shows "zeroable r \<longleftrightarrow> L r = {}"
+apply(induct r rule: zeroable.induct)
+apply(auto simp add: Sequ_def)
+done
+
+fun
+ atmostempty :: "rexp \<Rightarrow> bool"
+where
+  "atmostempty (ZERO) \<longleftrightarrow> True"
+| "atmostempty (ONE) \<longleftrightarrow> True"
+| "atmostempty (CHAR c) \<longleftrightarrow> False"
+| "atmostempty (ALT r1 r2) \<longleftrightarrow> atmostempty r1 \<and> atmostempty r2"
+| "atmostempty (SEQ r1 r2) \<longleftrightarrow> 
+     zeroable r1 \<or> zeroable r2 \<or> (atmostempty r1 \<and> atmostempty r2)"
+| "atmostempty (STAR r) = atmostempty r"
+
+fun
+ somechars :: "rexp \<Rightarrow> bool"
+where
+  "somechars (ZERO) \<longleftrightarrow> False"
+| "somechars (ONE) \<longleftrightarrow> False"
+| "somechars (CHAR c) \<longleftrightarrow> True"
+| "somechars (ALT r1 r2) \<longleftrightarrow> somechars r1 \<or> somechars r2"
+| "somechars (SEQ r1 r2) \<longleftrightarrow> 
+      (\<not> zeroable r1 \<and> somechars r2) \<or> (\<not> zeroable r2 \<and> somechars r1) \<or> 
+      (somechars r1 \<and> nullable r2) \<or> (somechars r2 \<and> nullable r1)"
+| "somechars (STAR r) \<longleftrightarrow> somechars r"
+
+lemma somechars_correctness:
+  shows "somechars r \<longleftrightarrow> (\<exists>s. s \<noteq> [] \<and> s \<in> L r)"
+apply(induct r rule: somechars.induct)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(auto)[1]
+prefer 2
+apply(simp)
+apply(rule iffI)
+apply(auto)[1]
+apply (metis Star_decomp neq_Nil_conv)
+apply(rule iffI)
+apply(simp add: Sequ_def zeroable_correctness nullable_correctness)
+apply(auto)[1]
+apply(simp add: Sequ_def zeroable_correctness nullable_correctness)
+apply(auto)[1]
+done
+
+lemma atmostempty_correctness_aux:
+  shows "atmostempty r \<longleftrightarrow> \<not> somechars r"
+apply(induct r)
+apply(simp_all)
+apply(auto simp add: zeroable_correctness nullable_correctness somechars_correctness)
+done
+
+lemma atmostempty_correctness:
+  shows "atmostempty r \<longleftrightarrow> L r \<subseteq> {[]}"
+by(auto simp add: atmostempty_correctness_aux somechars_correctness)
+
+fun
+ infinitestrings :: "rexp \<Rightarrow> bool"
+where
+  "infinitestrings (ZERO) = False"
+| "infinitestrings (ONE) = False"
+| "infinitestrings (CHAR c) = False"
+| "infinitestrings (ALT r1 r2) = (infinitestrings r1 \<or> infinitestrings r2)"
+| "infinitestrings (SEQ r1 r2) \<longleftrightarrow> 
+      (\<not> zeroable r1 \<and> infinitestrings r2) \<or> (\<not> zeroable r2 \<and> infinitestrings r1)"
+| "infinitestrings (STAR r) = (\<not> atmostempty r)"
+
+lemma Star_atmostempty:
+  assumes "A \<subseteq> {[]}"
+  shows "A\<star> \<subseteq> {[]}"
+using assms
+using Star_string concat_eq_Nil_conv empty_iff insert_iff subsetI subset_singletonD by fastforce
+
+lemma Star_empty_string_finite:
+  shows "finite ({[]}\<star>)"
+using Star_atmostempty infinite_super by auto
+
+lemma Star_empty_finite:
+  shows "finite ({}\<star>)"
+using Star_atmostempty infinite_super by auto
+
+lemma Star_concat_replicate:
+  assumes "s \<in> A"
+  shows "concat (replicate n s) \<in> A\<star>"
+using assms
+by (induct n) (auto)
+
+
+lemma concat_replicate_inj:
+  assumes "concat (replicate n s) = concat (replicate m s)" "s \<noteq> []"
+  shows "n = m"
+using assms
+apply(induct n arbitrary: m)
+apply(auto)[1]
+apply(auto)
+apply(case_tac m)
+apply(clarify)
+apply(simp only: replicate.simps concat.simps)
+apply blast
+by simp
+
+lemma A0:
+  assumes "finite (A ;; B)" "B \<noteq> {}"
+  shows "finite A"
+apply(subgoal_tac "\<exists>s. s \<in> B")
+apply(erule exE)
+apply(subgoal_tac "finite {s1 @ s |s1. s1 \<in> A}")
+apply(rule_tac f="\<lambda>s1. s1 @ s" in finite_imageD)
+apply(simp add: image_def)
+apply(smt Collect_cong)
+apply(simp add: inj_on_def)
+apply(rule_tac B="A ;; B" in finite_subset)
+apply(auto simp add: Sequ_def)[1]
+apply(rule assms(1))
+using assms(2) by auto
+
+lemma A1:
+  assumes "finite (A ;; B)" "A \<noteq> {}"
+  shows "finite B"
+apply(subgoal_tac "\<exists>s. s \<in> A")
+apply(erule exE)
+apply(subgoal_tac "finite {s @ s1 |s1. s1 \<in> B}")
+apply(rule_tac f="\<lambda>s1. s @ s1" in finite_imageD)
+apply(simp add: image_def)
+apply(smt Collect_cong)
+apply(simp add: inj_on_def)
+apply(rule_tac B="A ;; B" in finite_subset)
+apply(auto simp add: Sequ_def)[1]
+apply(rule assms(1))
+using assms(2) by auto
+
+lemma Sequ_Prod_finite:
+  assumes "A \<noteq> {}" "B \<noteq> {}"
+  shows "finite (A ;; B) \<longleftrightarrow> (finite (A \<times> B))"
+apply(rule iffI)
+apply(rule finite_cartesian_product)
+apply(erule A0)
+apply(rule assms(2))
+apply(erule A1)
+apply(rule assms(1))
+apply(simp add: Sequ_def)
+apply(rule finite_image_set2)
+apply(drule finite_cartesian_productD1)
+apply(rule assms(2))
+apply(simp)
+apply(drule finite_cartesian_productD2)
+apply(rule assms(1))
+apply(simp)
+done
+
+
+lemma Star_non_empty_string_infinite:
+  assumes "s \<in> A" " s \<noteq> []"
+  shows "infinite (A\<star>)"
+proof -
+  have "inj (\<lambda>n. concat (replicate n s))" 
+  using assms(2) concat_replicate_inj
+    by(auto simp add: inj_on_def)
+  moreover
+  have "infinite (UNIV::nat set)" by simp
+  ultimately
+  have "infinite ((\<lambda>n. concat (replicate n s)) ` UNIV)"
+   by (simp add: range_inj_infinite)
+  moreover
+  have "((\<lambda>n. concat (replicate n s)) ` UNIV) \<subseteq> (A\<star>)"
+    using Star_concat_replicate assms(1) by auto
+  ultimately show "infinite (A\<star>)" 
+  using infinite_super by auto
+qed
+
+lemma infinitestrings_correctness:
+  shows "infinitestrings r \<longleftrightarrow> infinite (L r)"
+apply(induct r)
+apply(simp_all)
+apply(simp add: zeroable_correctness)
+apply(rule iffI)
+apply(erule disjE)
+apply(subst Sequ_Prod_finite)
+apply(auto)[2]
+using finite_cartesian_productD2 apply blast
+apply(subst Sequ_Prod_finite)
+apply(auto)[2]
+using finite_cartesian_productD1 apply blast
+apply(subgoal_tac "L r1 \<noteq> {} \<and> L r2 \<noteq> {}")
+prefer 2
+apply(auto simp add: Sequ_def)[1]
+apply(subst (asm) Sequ_Prod_finite)
+apply(auto)[2]
+apply(auto)[1]
+apply(simp add: atmostempty_correctness)
+apply(rule iffI)
+apply (metis Star_empty_finite Star_empty_string_finite subset_singletonD)
+using Star_non_empty_string_infinite apply blast
+done
+
+
+end
\ No newline at end of file
diff -r 6670f2cb5741 -r 78dd6bca5627 thys/Fun.thy
--- a/thys/Fun.thy	Fri Jun 30 17:41:59 2017 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,213 +0,0 @@
-theory Fun
-  imports Lexer "~~/src/HOL/Library/Infinite_Set"
-begin
-
-section {* some fun tests *}
-
-fun
- zeroable :: "rexp ⇒ bool"
-where
-  "zeroable (ZERO) = True"
-| "zeroable (ONE) = False"
-| "zeroable (CHAR c) = False"
-| "zeroable (ALT r1 r2) = (zeroable r1 ∧ zeroable r2)"
-| "zeroable (SEQ r1 r2) = (zeroable r1 ∨ zeroable r2)"
-| "zeroable (STAR r) = False"
-
-lemma zeroable_correctness:
-  shows "zeroable r ⟷ L r = {}"
-apply(induct r rule: zeroable.induct)
-apply(auto simp add: Sequ_def)
-done
-
-fun
- atmostempty :: "rexp ⇒ bool"
-where
-  "atmostempty (ZERO) = True"
-| "atmostempty (ONE) = True"
-| "atmostempty (CHAR c) = False"
-| "atmostempty (ALT r1 r2) = (atmostempty r1 ∧ atmostempty r2)"
-| "atmostempty (SEQ r1 r2) = ((zeroable r1) ∨ (zeroable r2) ∨ (atmostempty r1 ∧ atmostempty r2))"
-| "atmostempty (STAR r) = atmostempty r"
-
-fun
- somechars :: "rexp ⇒ bool"
-where
-  "somechars (ZERO) = False"
-| "somechars (ONE) = False"
-| "somechars (CHAR c) = True"
-| "somechars (ALT r1 r2) = (somechars r1 ∨ somechars r2)"
-| "somechars (SEQ r1 r2) = ((¬zeroable r1 ∧ somechars r2) ∨ (¬zeroable r2 ∧ somechars r1) ∨ 
-                           (somechars r1 ∧ nullable r2) ∨ (somechars r2 ∧ nullable r1))"
-| "somechars (STAR r) = somechars r"
-
-lemma somechars_correctness:
-  shows "somechars r ⟷ (∃s. s ≠ [] ∧ s ∈ L r)"
-apply(induct r rule: somechars.induct)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(auto)[1]
-prefer 2
-apply(simp)
-apply(rule iffI)
-apply(auto)[1]
-apply (metis Star_decomp neq_Nil_conv)
-apply(rule iffI)
-apply(simp add: Sequ_def zeroable_correctness nullable_correctness)
-apply(auto)[1]
-apply(simp add: Sequ_def zeroable_correctness nullable_correctness)
-apply(auto)[1]
-done
-
-lemma atmostempty_correctness_aux:
-  shows "atmostempty r ⟷ ¬somechars r"
-apply(induct r)
-apply(simp_all)
-apply(auto simp add: zeroable_correctness nullable_correctness somechars_correctness)
-done
-
-lemma atmostempty_correctness:
-  shows "atmostempty r ⟷ L r ⊆ {[]}"
-by(auto simp add: atmostempty_correctness_aux somechars_correctness)
-
-fun
- infinitestrings :: "rexp ⇒ bool"
-where
-  "infinitestrings (ZERO) = False"
-| "infinitestrings (ONE) = False"
-| "infinitestrings (CHAR c) = False"
-| "infinitestrings (ALT r1 r2) = (infinitestrings r1 ∨ infinitestrings r2)"
-| "infinitestrings (SEQ r1 r2) = ((¬zeroable r1 ∧ infinitestrings r2) ∨ (¬zeroable r2 ∧ infinitestrings r1))"
-| "infinitestrings (STAR r) = (¬atmostempty r)"
-
-lemma Star_atmostempty:
-  assumes "A ⊆ {[]}"
-  shows "A⋆ ⊆ {[]}"
-using assms
-using Star_string concat_eq_Nil_conv empty_iff insert_iff subsetI subset_singletonD by fastforce
-
-lemma Star_empty_string_finite:
-  shows "finite ({[]}⋆)"
-using Star_atmostempty infinite_super by auto
-
-lemma Star_empty_finite:
-  shows "finite ({}⋆)"
-using Star_atmostempty infinite_super by auto
-
-lemma Star_concat_replicate:
-  assumes "s ∈ A"
-  shows "concat (replicate n s) ∈ A⋆"
-using assms
-by (induct n) (auto)
-
-
-lemma concat_replicate_inj:
-  assumes "concat (replicate n s) = concat (replicate m s)" "s ≠ []"
-  shows "n = m"
-using assms
-apply(induct n arbitrary: m)
-apply(auto)[1]
-apply(auto)
-apply(case_tac m)
-apply(clarify)
-apply(simp only: replicate.simps concat.simps)
-apply blast
-by simp
-
-lemma A0:
-  assumes "finite (A ;; B)" "B ≠ {}"
-  shows "finite A"
-apply(subgoal_tac "∃s. s ∈ B")
-apply(erule exE)
-apply(subgoal_tac "finite {s1 @ s |s1. s1 ∈ A}")
-apply(rule_tac f="λs1. s1 @ s" in finite_imageD)
-apply(simp add: image_def)
-apply(smt Collect_cong)
-apply(simp add: inj_on_def)
-apply(rule_tac B="A ;; B" in finite_subset)
-apply(auto simp add: Sequ_def)[1]
-apply(rule assms(1))
-using assms(2) by auto
-
-lemma A1:
-  assumes "finite (A ;; B)" "A ≠ {}"
-  shows "finite B"
-apply(subgoal_tac "∃s. s ∈ A")
-apply(erule exE)
-apply(subgoal_tac "finite {s @ s1 |s1. s1 ∈ B}")
-apply(rule_tac f="λs1. s @ s1" in finite_imageD)
-apply(simp add: image_def)
-apply(smt Collect_cong)
-apply(simp add: inj_on_def)
-apply(rule_tac B="A ;; B" in finite_subset)
-apply(auto simp add: Sequ_def)[1]
-apply(rule assms(1))
-using assms(2) by auto
-
-lemma Sequ_Prod_finite:
-  assumes "A ≠ {}" "B ≠ {}"
-  shows "finite (A ;; B) ⟷ (finite (A × B))"
-apply(rule iffI)
-apply(rule finite_cartesian_product)
-apply(erule A0)
-apply(rule assms(2))
-apply(erule A1)
-apply(rule assms(1))
-apply(simp add: Sequ_def)
-apply(rule finite_image_set2)
-apply(drule finite_cartesian_productD1)
-apply(rule assms(2))
-apply(simp)
-apply(drule finite_cartesian_productD2)
-apply(rule assms(1))
-apply(simp)
-done
-
-
-lemma Star_non_empty_string_infinite:
-  assumes "s ∈ A" " s ≠ []"
-  shows "infinite (A⋆)"
-proof -
-  have "inj (λn. concat (replicate n s))" 
-  using assms(2) concat_replicate_inj
-    by(auto simp add: inj_on_def)
-  moreover
-  have "infinite (UNIV::nat set)" by simp
-  ultimately
-  have "infinite ((λn. concat (replicate n s)) ` UNIV)"
-   by (simp add: range_inj_infinite)
-  moreover
-  have "((λn. concat (replicate n s)) ` UNIV) ⊆ (A⋆)"
-    using Star_concat_replicate assms(1) by auto
-  ultimately show "infinite (A⋆)" 
-  using infinite_super by auto
-qed
-
-lemma infinitestrings_correctness:
-  shows "infinitestrings r ⟷ infinite (L r)"
-apply(induct r)
-apply(simp_all)
-apply(simp add: zeroable_correctness)
-apply(rule iffI)
-apply(erule disjE)
-apply(subst Sequ_Prod_finite)
-apply(auto)[2]
-using finite_cartesian_productD2 apply blast
-apply(subst Sequ_Prod_finite)
-apply(auto)[2]
-using finite_cartesian_productD1 apply blast
-apply(subgoal_tac "L r1 ≠ {} ∧ L r2 ≠ {}")
-prefer 2
-apply(auto simp add: Sequ_def)[1]
-apply(subst (asm) Sequ_Prod_finite)
-apply(auto)[2]
-apply(auto)[1]
-apply(simp add: atmostempty_correctness)
-apply(rule iffI)
-apply (metis Star_empty_finite Star_empty_string_finite subset_singletonD)
-using Star_non_empty_string_infinite apply blast
-done
-
-
-end
\ No newline at end of file
diff -r 6670f2cb5741 -r 78dd6bca5627 thys/ROOT
--- a/thys/ROOT	Fri Jun 30 17:41:59 2017 +0100
+++ b/thys/ROOT	Fri Jun 30 21:13:40 2017 +0100
@@ -5,7 +5,7 @@
         "Simplifying"
         (*"Sulzmann"*) 
         "Positions"
-        "Fun"
+        "Exercises"
 
 session Paper in "Paper" = Lex +
   options [document = pdf, document_output = "..", document_variants="paper"]