Mercurial Mercurial > hg > afl-material / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
progs/Matcher2.thy
changeset 1011 31e011ce66e3
parent 1010 ae9ffbf979ff 
--- a/progs/Matcher2.thy	Fri Oct 17 11:20:49 2025 +0100
+++ b/progs/Matcher2.thy	Sun Oct 19 09:44:04 2025 +0200
@@ -2,30 +2,24 @@
   imports "Main" 
 begin
 
-lemma Suc_Union:
-  "(\<Union> x\<le>Suc m. B x) = (B (Suc m) \<union> (\<Union> x\<le>m. B x))"
-by (metis UN_insert atMost_Suc)
-
-lemma Suc_reduce_Union:
-  "(\<Union>x\<in>{Suc n..Suc m}. B x) = (\<Union>x\<in>{n..m}. B (Suc x))"
-by (metis UN_extend_simps(10) image_Suc_atLeastAtMost)
 
 
 section \<open>Regular Expressions\<close>
 
 datatype rexp =
-  NULL
-| EMPTY
+  ZERO
+| ONE
 | CH char
 | SEQ rexp rexp
 | ALT rexp rexp
 | STAR rexp
+
 | NOT rexp
 | PLUS rexp
 | OPT rexp
 | NTIMES rexp nat
-| NMTIMES rexp nat nat
-| UPNTIMES rexp nat
+| BETWEEN rexp nat nat
+| UPTO rexp nat
 
 
 section \<open>Sequential Composition of Sets\<close>
@@ -136,8 +130,8 @@
 fun
   L :: "rexp \<Rightarrow> string set"
 where
-  "L (NULL) = {}"
-| "L (EMPTY) = {[]}"
+  "L (ZERO) = {}"
+| "L (ONE) = {[]}"
 | "L (CH c) = {[c]}"
 | "L (SEQ r1 r2) = (L r1) ;; (L r2)"
 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"
@@ -146,10 +140,10 @@
 | "L (PLUS r) = (L r) ;; ((L r)\<star>)"
 | "L (OPT r) = (L r) \<union> {[]}"
 | "L (NTIMES r n) = (L r) \<up> n"
-| "L (NMTIMES r n m) = (\<Union>i\<in> {n..m} . ((L r) \<up> i))" 
-| "L (UPNTIMES r n) = (\<Union>i\<in> {..n} . ((L r) \<up> i))"
+| "L (BETWEEN r n m) = (\<Union>i\<in> {n..m} . ((L r) \<up> i))" 
+| "L (UPTO r n) = (\<Union>i\<in> {..n} . ((L r) \<up> i))"
 
-lemma "L (NOT NULL) = UNIV"
+lemma "L (NOT ZERO) = UNIV"
 apply(simp)
 done
 
@@ -158,8 +152,8 @@
 fun
  nullable :: "rexp \<Rightarrow> bool"
 where
-  "nullable (NULL) = False"
-| "nullable (EMPTY) = True"
+  "nullable (ZERO) = False"
+| "nullable (ONE) = True"
 | "nullable (CH c) = False"
 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
@@ -168,41 +162,27 @@
 | "nullable (PLUS r) = (nullable r)"
 | "nullable (OPT r) = True"
 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)"
-| "nullable (NMTIMES r n m) = (if m < n then False else (if n = 0 then True else nullable r))"
-| "nullable (UPNTIMES r n) = True"
+| "nullable (BETWEEN r n m) = (if m < n then False else (if n = 0 then True else nullable r))"
+| "nullable (UPTO r n) = True"
 
-fun M :: "rexp \<Rightarrow> nat"
-where
-  "M (NULL) = 0"
-| "M (EMPTY) = 0"
-| "M (CH char) = 0"
-| "M (SEQ r1 r2) = Suc ((M r1) + (M r2))"
-| "M (ALT r1 r2) = Suc ((M r1) + (M r2))"
-| "M (STAR r) = Suc (M r)"
-| "M (NOT r) = Suc (M r)"
-| "M (PLUS r) = Suc (M r)"
-| "M (OPT r) = Suc (M r)"
-| "M (NTIMES r n) = Suc (M r) * 2 * (Suc n)"
-| "M (NMTIMES r n m) = Suc (Suc (M r)) * 2 * (Suc m) * (Suc (Suc m) - Suc n)"
-| "M (UPNTIMES r n) = Suc (M r) * 2 * (Suc n)"
 
 fun der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
 where
-  "der c (NULL) = NULL"
-| "der c (EMPTY) = NULL"
-| "der c (CH d) = (if c = d then EMPTY else NULL)"
+  "der c (ZERO) = ZERO"
+| "der c (ONE) = ZERO"
+| "der c (CH d) = (if c = d then ONE else ZERO)"
 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"
-| "der c (SEQ r1 r2) = ALT (SEQ (der c r1) r2) (if nullable r1 then der c r2 else NULL)"
+| "der c (SEQ r1 r2) = ALT (SEQ (der c r1) r2) (if nullable r1 then der c r2 else ZERO)"
 | "der c (STAR r) = SEQ (der c r) (STAR r)"
 | "der c (NOT r) = NOT(der c r)"
 | "der c (PLUS r) = SEQ (der c r) (STAR r)"
 | "der c (OPT r) = der c r"
-| "der c (NTIMES r n) = (if n = 0 then NULL else (SEQ (der c r) (NTIMES r (n - 1))))"
-| "der c (NMTIMES r n m) = 
-        (if m = 0 then NULL else 
-        (if n = 0 then SEQ (der c r) (UPNTIMES r (m - 1))
-         else SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))"
-| "der c (UPNTIMES r n) = (if n = 0 then NULL else SEQ (der c r) (UPNTIMES r (n - 1)))"
+| "der c (NTIMES r n) = (if n = 0 then ZERO else (SEQ (der c r) (NTIMES r (n - 1))))"
+| "der c (BETWEEN r n m) = 
+        (if m = 0 then ZERO else 
+        (if n = 0 then SEQ (der c r) (UPTO r (m - 1))
+         else SEQ (der c r) (BETWEEN r (n - 1) (m - 1))))"
+| "der c (UPTO r n) = (if n = 0 then ZERO else SEQ (der c r) (UPTO r (n - 1)))"
 
 fun 
  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
@@ -287,6 +267,7 @@
   apply blast
   by force
 
+
 lemma Der_ntimes [simp]:
   shows "Der c (A  \<up> (Suc n)) = (Der c A) ;; (A \<up> n)"
 proof -    
@@ -311,6 +292,14 @@
 unfolding Der_def 
 by(auto simp add: Cons_eq_append_conv Seq_def)
 
+lemma concI_if_Nil2: "[] \<in> B \<Longrightarrow> xs \<in> A \<Longrightarrow> xs \<in> A ;; B"
+  using Matcher2.Seq_def by auto
+
+lemma Der_pow2:
+  shows "Der c (A \<up> n) = (if n = 0 then {} else (Der c A) ;; (A \<up> (n - 1)))"
+  apply(induct n arbitrary: A)
+  using Der_ntimes by auto
+
 
 lemma Der_UNION [simp]: 
   shows "Der c (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. Der c (B x))"
@@ -324,10 +313,10 @@
 lemma der_correctness:
   shows "L (der c r) = Der c (L r)"
 proof(induct r)
-  case NULL
+  case ZERO
   then show ?case by simp
 next
-  case EMPTY
+  case ONE
   then show ?case by simp
 next
   case (CH x)
@@ -359,99 +348,34 @@
     using Der_ntimes Matcher2.Seq_def less_iff_Suc_add apply fastforce
     using Der_ntimes Matcher2.Seq_def less_iff_Suc_add by auto
 next
-  case (NMTIMES r n m)
+  case (BETWEEN r n m)
   then show ?case 
     apply(auto simp add: Seq_def)
-    sledgeham mer[timeout=1000]
-    apply(case_tac n)
-    sorry
+    apply (metis (mono_tags, lifting) Der_ntimes Matcher2.Seq_def Suc_pred atLeast0AtMost atMost_iff diff_Suc_Suc
+        diff_is_0_eq mem_Collect_eq)
+      apply(subst (asm) Der_pow2)
+      apply(case_tac xa)
+       apply(simp)
+      apply(auto simp add: Seq_def)[1]
+    apply (metis atMost_iff diff_Suc_1' diff_le_mono)
+    apply (metis (mono_tags, lifting) Der_ntimes Matcher2.Seq_def Suc_le_mono Suc_pred atLeastAtMost_iff
+        mem_Collect_eq)
+    apply(subst (asm) Der_pow2)
+      apply(case_tac xa)
+       apply(simp)
+    apply(auto simp add: Seq_def)[1]
+    by force
 next
-  case (UPNTIMES r x2)
+  case (UPTO r x2)
   then show ?case 
     apply(auto simp add: Seq_def)
     apply (metis (mono_tags, lifting) Der_ntimes Matcher2.Seq_def Suc_le_mono Suc_pred atMost_iff
         mem_Collect_eq)
-sledgehammer[timeout=1000]
-    sorry
-qed
-
-
-
-
-lemma der_correctness:
-  shows "L (der c r) = Der c (L r)"
-apply(induct rule: der.induct) 
-apply(simp_all add: nullable_correctness 
-    Suc_Union Suc_reduce_Union seq_Union atLeast0AtMost)
-apply(rule impI)+
-apply(subgoal_tac "{n..m} = {n} \<union> {Suc n..m}")
-apply(auto simp add: Seq_def)
-done
-
-lemma L_der_NTIMES:
-  shows "L(der c (NTIMES r n)) = L (if n = 0 then NULL else if nullable r then 
-         SEQ (der c r) (UPNTIMES r (n - 1)) else SEQ (der c r) (NTIMES r (n - 1)))"
-apply(induct n)
-apply(simp)
-apply(simp)
-apply(auto)
-apply(auto simp add: Seq_def)
-apply(rule_tac x="s1" in exI)
-apply(simp)
-apply(rule_tac x="xa" in bexI)
-apply(simp)
-apply(simp)
-apply(rule_tac x="s1" in exI)
-apply(simp)
-by (metis Suc_pred atMost_iff le_Suc_eq)
-
-lemma "L(der c (UPNTIMES r 0)) = {}"
-by simp
-
-lemma "L(der c (UPNTIMES r (Suc n))) = L(SEQ (der c r) (UPNTIMES r n))"
-proof(induct n)
-  case 0 show ?case by simp
-next
-  case (Suc n)
-  have IH: "L (der c (UPNTIMES r (Suc n))) = L (SEQ (der c r) (UPNTIMES r n))" by fact
-  { assume a: "nullable r"
-    have "L (der c (UPNTIMES r (Suc (Suc n)))) = Der c (L (UPNTIMES r (Suc (Suc n))))"
-    by (simp only: der_correctness)
-    also have "... = Der c (L (ALT (NTIMES r (Suc (Suc n))) (UPNTIMES r (Suc n))))"
-    by(simp only: L.simps Suc_Union)
-    also have "... = L (der c (ALT (NTIMES r (Suc (Suc n))) (UPNTIMES r (Suc n))))"
-    by (simp only: der_correctness)
-    also have "... = L (der c (NTIMES r (Suc (Suc n)))) \<union> L (der c (UPNTIMES r (Suc n)))"
-    by(auto simp add: Seq_def)
-    also have "... = L (der c (NTIMES r (Suc (Suc n)))) \<union> L (SEQ (der c r) (UPNTIMES r n))"
-    using IH by simp
-    also have "... = L (SEQ (der c r) (UPNTIMES r (Suc n))) \<union> L (SEQ (der c r) (UPNTIMES r n))"
-    using a unfolding L_der_NTIMES by simp
-    also have "... =  L (SEQ (der c r) (UPNTIMES r (Suc n)))"
-    by (auto, metis Suc_Union Un_iff seq_Union)
-    finally have "L (der c (UPNTIMES r (Suc (Suc n)))) = L (SEQ (der c r) (UPNTIMES r (Suc n)))" .
-    } 
-  moreover
-  { assume a: "\<not>nullable r"
-    have "L (der c (UPNTIMES r (Suc (Suc n)))) = Der c (L (UPNTIMES r (Suc (Suc n))))"
-    by (simp only: der_correctness)
-    also have "... = Der c (L (ALT (NTIMES r (Suc (Suc n))) (UPNTIMES r (Suc n))))"
-    by(simp only: L.simps Suc_Union)
-    also have "... = L (der c (ALT (NTIMES r (Suc (Suc n))) (UPNTIMES r (Suc n))))"
-    by (simp only: der_correctness)
-    also have "... = L (der c (NTIMES r (Suc (Suc n)))) \<union> L (der c (UPNTIMES r (Suc n)))"
-    by(auto simp add: Seq_def)
-    also have "... = L (der c (NTIMES r (Suc (Suc n)))) \<union> L (SEQ (der c r) (UPNTIMES r n))"
-    using IH by simp
-    also have "... = L (SEQ (der c r) (NTIMES r (Suc n))) \<union> L (SEQ (der c r) (UPNTIMES r n))"
-    using a unfolding L_der_NTIMES by simp
-    also have "... =  L (SEQ (der c r) (UPNTIMES r (Suc n)))"
-    by (simp add: Suc_Union seq_union(1))
-    finally have "L (der c (UPNTIMES r (Suc (Suc n)))) = L (SEQ (der c r) (UPNTIMES r (Suc n)))" .
-  }
-  ultimately  
-  show "L (der c (UPNTIMES r (Suc (Suc n)))) = L (SEQ (der c r) (UPNTIMES r (Suc n)))"
-  by blast
+    apply(subst (asm) Der_pow2)
+    apply(case_tac xa)
+     apply(simp)
+    apply(auto simp add: Seq_def)
+    by (metis atMost_iff diff_Suc_1' diff_le_mono)
 qed
 
 lemma matcher_correctness:
afl-material