Mercurial Mercurial > hg > regexp / comparison
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.
Myhill_1.thy
changeset 97 70485955c934
parent 96 3b9deda4f459
child 98 36f9d19be0e6
equal deleted inserted replaced
96:3b9deda4f459 97:70485955c934 
   247   then have "X \<subseteq> B ;; A\<star>" by auto
 
   247   then have "X \<subseteq> B ;; A\<star>" by auto
 
   248   ultimately 
   248   ultimately 
   249   show "X = B ;; A\<star>" by simp
 
   249   show "X = B ;; A\<star>" by simp
 
   250 qed
 
   250 qed
 
   251 
   251 
   252 (*
 
       
   253 corollary arden_eq:
 
       
   254   assumes nemp: "[] \<notin> A"
 
       
   255   shows "(X ;; A \<union> B) = (B ;; A\<star>)"
 
       
   256 proof -
 
       
   257   { assume "X = X ;; A \<union> B"
 
       
   258     then have "X = B ;; A\<star>"
 
       
   259     then have ?thesis
 
       
   260       thm arden[THEN iffD1]
 
       
   261 apply(rule set_eqI)
 
       
   262 thm arden[THEN iffD1]
 
       
   263 apply(rule iffI)
 
       
   264 apply(rule trans)
 
       
   265 apply(rule arden[THEN iffD2, symmetric])
 
       
   266 apply(rule arden[OF iffD1, symmetric])
 
       
   267 thm trans
 
       
   268 proof -
 
       
   269   { assume "X = X ;; A \<union> B"
 
       
   270     then have "X = B ;; A\<star>" using arden[OF nemp] by blast
 
       
   271     moreover 
       
   272   
       
   273     
       
   274 using arden[of "A" "X" "B", OF nemp]
 
       
   275 apply(erule_tac iffE)
 
       
   276 apply(blast)
 
       
   277 *)
 
       
   278 
       
   279 
   252 
   280 section {* Regular Expressions *}
 
   253 section {* Regular Expressions *}
 
   281 
   254 
   282 datatype rexp =
 
   255 datatype rexp =
 
   283   NULL
 
   256   NULL
 
   466 text {*
 
   439 text {*
 
   467   @{text "eqs_subst ES X xrhs"} substitutes @{text xrhs} into every 
   440   @{text "eqs_subst ES X xrhs"} substitutes @{text xrhs} into every 
   468   equation of the equational system @{text ES}.
 
   441   equation of the equational system @{text ES}.
 
   469 *}
 
   442 *}
 
   470 
   443 
       
   444 types esystem = "(lang \<times> rhs_item set) set"
 
       
   445 
   471 definition
 
   446 definition
 
       
   447   Subst_all :: "esystem \<Rightarrow> lang \<Rightarrow> rhs_item set \<Rightarrow> esystem"
 
       
   448 where
 
   472   "Subst_all ES X xrhs \<equiv> {(Y, Subst yrhs X xrhs) | Y yrhs. (Y, yrhs) \<in> ES}"
 
   449   "Subst_all ES X xrhs \<equiv> {(Y, Subst yrhs X xrhs) | Y yrhs. (Y, yrhs) \<in> ES}"
 
   473 
   450 
   474 text {*
 
   451 text {*
 
   475   The following term @{text "remove ES Y yrhs"} removes the equation
 
   452   The following term @{text "remove ES Y yrhs"} removes the equation
 
   476   @{text "Y = yrhs"} from equational system @{text "ES"} by replacing
 
   453   @{text "Y = yrhs"} from equational system @{text "ES"} by replacing
 
   493 
   470 
   494 definition 
   471 definition 
   495   "Iter X ES \<equiv> (let (Y, yrhs) = SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> X \<noteq> Y
 
   472   "Iter X ES \<equiv> (let (Y, yrhs) = SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> X \<noteq> Y
 
   496                 in Remove ES Y yrhs)"
 
   473                 in Remove ES Y yrhs)"
 
   497 
   474 
       
   475 lemma IterI2:
 
       
   476   assumes "(Y, yrhs) \<in> ES"
 
       
   477   and     "X \<noteq> Y"
 
       
   478   and     "\<And>Y yrhs. \<lbrakk>(Y, yrhs) \<in> ES; X \<noteq> Y\<rbrakk> \<Longrightarrow> Q (Remove ES Y yrhs)"
 
       
   479   shows "Q (Iter X ES)"
 
       
   480 unfolding Iter_def using assms
 
       
   481 by (rule_tac a="(Y, yrhs)" in someI2) (auto)
 
       
   482 
       
   483 
   498 text {*
 
   484 text {*
 
   499   The following term @{text "Reduce X ES"} repeatedly removes characteriztion equations
 
   485   The following term @{text "Reduce X ES"} repeatedly removes characteriztion equations
 
   500   for unknowns other than @{text "X"} until one is left.
 
   486   for unknowns other than @{text "X"} until one is left.
 
   501 *}
 
   487 *}
 
   502 
   488 
   503 definition 
   489 abbreviation
 
   504   "Reduce X ES \<equiv> while (\<lambda> ES. card ES \<noteq> 1) (Iter X) ES"
 
   490   "Test ES \<equiv> card ES \<noteq> 1"
 
   505 
   491 
   506 text {*
 
   492 definition 
   507   Since the @{text "while"} combinator from HOL library is used to implement @{text "Reduce X ES"},
 
   493   "Solve X ES \<equiv> while Test (Iter X) ES"
 
       
   494 
       
   495 
       
   496 (* test *)
 
       
   497 partial_function (tailrec)
 
       
   498   solve
 
       
   499 where
 
       
   500   "solve X ES = (if (card ES = 1) then ES else solve X (Iter X ES))"
 
       
   501 
       
   502 
       
   503 text {*
 
       
   504   Since the @{text "while"} combinator from HOL library is used to implement @{text "Solve X ES"},
 
   508   the induction principle @{thm [source] while_rule} is used to proved the desired properties
 
   505   the induction principle @{thm [source] while_rule} is used to proved the desired properties
 
   509   of @{text "Reduce X ES"}. For this purpose, an invariant predicate @{text "invariant"} is defined
 
   506   of @{text "Solve X ES"}. For this purpose, an invariant predicate @{text "invariant"} is defined
 
   510   in terms of a series of auxilliary predicates:
 
   507   in terms of a series of auxilliary predicates:
 
   511 *}
 
   508 *}
 
   512 
   509 
   513 section {* Invariants *}
 
   510 section {* Invariants *}
 
   514 
   511 
   515 text {* Every variable is defined at most onece in @{text ES}. *}
 
   512 text {* Every variable is defined at most once in @{text ES}. *}
 
   516 
   513 
   517 definition 
   514 definition 
   518   "distinct_equas ES \<equiv> 
   515   "distinct_equas ES \<equiv> 
   519      \<forall> X rhs rhs'. (X, rhs) \<in> ES \<and> (X, rhs') \<in> ES \<longrightarrow> rhs = rhs'"
 
   516      \<forall> X rhs rhs'. (X, rhs) \<in> ES \<and> (X, rhs') \<in> ES \<longrightarrow> rhs = rhs'"
 
   520 
   517 
       
   518 
   521 text {* 
   519 text {* 
   522   Every equation in @{text ES} (represented by @{text "(X, rhs)"}) 
   520   Every equation in @{text ES} (represented by @{text "(X, rhs)"}) 
   523   is valid, i.e. @{text "(X = L rhs)"}.
 
   521   is valid, i.e. @{text "X = L rhs"}.
 
   524 *}
 
   522 *}
 
   525 
   523 
   526 definition 
   524 definition 
   527   "valid_eqns ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> (X = L rhs)"
 
   525   "valid_eqns ES \<equiv> \<forall>(X, rhs) \<in> ES. X = L rhs"
 
   528 
   526 
   529 text {*
 
   527 text {*
 
   530   @{text "rhs_nonempty rhs"} requires regular expressions occuring in 
   528   @{text "rhs_nonempty rhs"} requires regular expressions occuring in 
   531   transitional items of @{text "rhs"} do not contain empty string. This is 
   529   transitional items of @{text "rhs"} do not contain empty string. This is 
   532   necessary for the application of Arden's transformation to @{text "rhs"}.
 
   530   necessary for the application of Arden's transformation to @{text "rhs"}.
 
   539   The following @{text "ardenable ES"} requires that Arden's transformation 
   537   The following @{text "ardenable ES"} requires that Arden's transformation 
   540   is applicable to every equation of equational system @{text "ES"}.
 
   538   is applicable to every equation of equational system @{text "ES"}.
 
   541 *}
 
   539 *}
 
   542 
   540 
   543 definition 
   541 definition 
   544   "ardenable ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> rhs_nonempty rhs"
 
   542   "ardenable ES \<equiv> \<forall>(X, rhs) \<in> ES. rhs_nonempty rhs"
 
   545 
   543 
   546 text {* 
   544 text {* 
   547   @{text "finite_rhs ES"} requires every equation in @{text "rhs"} 
   545   @{text "finite_rhs ES"} requires every equation in @{text "rhs"} 
   548   be finite.
 
   546   be finite.
 
   549 *}
 
   547 *}
 
   554   @{text "classes_of rhs"} returns all variables (or equivalent classes)
 
   552   @{text "classes_of rhs"} returns all variables (or equivalent classes)
 
   555   occuring in @{text "rhs"}.
 
   553   occuring in @{text "rhs"}.
 
   556   *}
 
   554   *}
 
   557 
   555 
   558 definition 
   556 definition 
   559   "classes_of rhs \<equiv> {X. \<exists> r. Trn X r \<in> rhs}"
 
   557   "classes_of rhs \<equiv> {X | X r. Trn X r \<in> rhs}"
 
   560 
   558 
   561 text {*
 
   559 text {*
 
   562   @{text "lefts_of ES"} returns all variables defined by an 
   560   @{text "lefts_of ES"} returns all variables defined by an 
   563   equational system @{text "ES"}.
 
   561   equational system @{text "ES"}.
 
   564 *}
 
   562 *}
 
   568 text {*
 
   566 text {*
 
   569   The following @{text "self_contained ES"} requires that every variable occuring 
   567   The following @{text "self_contained ES"} requires that every variable occuring 
   570   on the right hand side of equations is already defined by some equation in @{text "ES"}.
 
   568   on the right hand side of equations is already defined by some equation in @{text "ES"}.
 
   571 *}
 
   569 *}
 
   572 definition 
   570 definition 
   573   "self_contained ES \<equiv> \<forall> (X, xrhs) \<in> ES. classes_of xrhs \<subseteq> lefts_of ES"
 
   571   "self_contained ES \<equiv> \<forall>(X, xrhs) \<in> ES. classes_of xrhs \<subseteq> lefts_of ES"
 
   574 
   572 
   575 
   573 
   576 text {*
 
   574 text {*
 
   577   The invariant @{text "invariant(ES)"} is a conjunction of all the previously defined constaints.
 
   575   The invariant @{text "invariant(ES)"} is a conjunction of all the previously defined constaints.
 
   578   *}
 
   576   *}
 
   627   assumes finite: "finite rhs"
 
   625   assumes finite: "finite rhs"
 
   628   and nonempty: "rhs_nonempty rhs"
 
   626   and nonempty: "rhs_nonempty rhs"
 
   629   shows "[] \<notin> L (\<Uplus> {r. Trn X r \<in> rhs})"
 
   627   shows "[] \<notin> L (\<Uplus> {r. Trn X r \<in> rhs})"
 
   630 using finite nonempty rhs_nonempty_def
 
   628 using finite nonempty rhs_nonempty_def
 
   631 using finite_Trn[OF finite]
 
   629 using finite_Trn[OF finite]
 
   632 by (auto)
 
   630 by auto
 
   633 
   631 
   634 lemma lang_of_rexp_of:
 
   632 lemma lang_of_rexp_of:
 
   635   assumes finite:"finite rhs"
 
   633   assumes finite:"finite rhs"
 
   636   shows "L ({Trn X r| r. Trn X r \<in> rhs}) = X ;; (L (\<Uplus>{r. Trn X r \<in> rhs}))"
 
   634   shows "L ({Trn X r| r. Trn X r \<in> rhs}) = X ;; (L (\<Uplus>{r. Trn X r \<in> rhs}))"
 
   637 proof -
 
   635 proof -
 
   756   assumes finite_CS: "finite (UNIV // \<approx>A)"
 
   754   assumes finite_CS: "finite (UNIV // \<approx>A)"
 
   757   shows "invariant (Init (UNIV // \<approx>A))"
 
   755   shows "invariant (Init (UNIV // \<approx>A))"
 
   758 proof (rule invariantI)
 
   756 proof (rule invariantI)
 
   759   show "valid_eqns (Init (UNIV // \<approx>A))"
 
   757   show "valid_eqns (Init (UNIV // \<approx>A))"
 
   760     unfolding valid_eqns_def 
   758     unfolding valid_eqns_def 
   761     using l_eq_r_in_eqs by simp
 
   759     using l_eq_r_in_eqs by auto
 
   762   show "finite (Init (UNIV // \<approx>A))" using finite_CS
 
   760   show "finite (Init (UNIV // \<approx>A))" using finite_CS
 
   763     unfolding Init_def by simp
 
   761     unfolding Init_def by simp
 
   764   show "distinct_equas (Init (UNIV // \<approx>A))"     
   762   show "distinct_equas (Init (UNIV // \<approx>A))"     
   765     unfolding distinct_equas_def Init_def by simp
 
   763     unfolding distinct_equas_def Init_def by simp
 
   766   show "ardenable (Init (UNIV // \<approx>A))"
 
   764   show "ardenable (Init (UNIV // \<approx>A))"
 
   871   shows "finite (Subst_all ES Y yrhs)"
 
   869   shows "finite (Subst_all ES Y yrhs)"
 
   872 proof -
 
   870 proof -
 
   873   have "finite {(Ya, Subst yrhsa Y yrhs) |Ya yrhsa. (Ya, yrhsa) \<in> ES}" 
   871   have "finite {(Ya, Subst yrhsa Y yrhs) |Ya yrhsa. (Ya, yrhsa) \<in> ES}" 
   874                                                                   (is "finite ?A")
 
   872                                                                   (is "finite ?A")
 
   875   proof-
 
   873   proof-
 
   876     def eqns' \<equiv> "{((Ya::string set), yrhsa)| Ya yrhsa. (Ya, yrhsa) \<in> ES}"
 
   874     def eqns' \<equiv> "{(Ya::lang, yrhsa) | Ya yrhsa. (Ya, yrhsa) \<in> ES}"
 
   877     def h \<equiv> "\<lambda> ((Ya::string set), yrhsa). (Ya, Subst yrhsa Y yrhs)"
 
   875     def h \<equiv> "\<lambda>(Ya::lang, yrhsa). (Ya, Subst yrhsa Y yrhs)"
 
   878     have "finite (h ` eqns')" using finite h_def eqns'_def by auto
 
   876     have "finite (h ` eqns')" using finite h_def eqns'_def by auto
 
   879     moreover have "?A = h ` eqns'" by (auto simp:h_def eqns'_def)
 
   877     moreover have "?A = h ` eqns'" by (auto simp:h_def eqns'_def)
 
   880     ultimately show ?thesis by auto      
   878     ultimately show ?thesis by auto      
   881   qed
 
   879   qed
 
   882   thus ?thesis by (simp add:Subst_all_def)
 
   880   thus ?thesis by (simp add:Subst_all_def)
 
   956   proof-
 
   954   proof-
 
   957     have "Y = L (Arden Y yrhs)" 
   955     have "Y = L (Arden Y yrhs)" 
   958       using Y_eq_yrhs invariant_ES finite_yrhs nonempty_yrhs
 
   956       using Y_eq_yrhs invariant_ES finite_yrhs nonempty_yrhs
 
   959       by (rule_tac Arden_keeps_eq, (simp add:rexp_of_empty)+)
 
   957       by (rule_tac Arden_keeps_eq, (simp add:rexp_of_empty)+)
 
   960     thus ?thesis using invariant_ES 
   958     thus ?thesis using invariant_ES 
   961       by (clarsimp simp add:valid_eqns_def 
   959       by (auto simp add:valid_eqns_def 
   962         Subst_all_def Subst_keeps_eq invariant_def finite_rhs_def
 
   960         Subst_all_def Subst_keeps_eq invariant_def finite_rhs_def
 
   963         simp del:L_rhs.simps)
 
   961         simp del:L_rhs.simps)
 
   964   qed
 
   962   qed
 
   965   show "finite (Subst_all ES Y (Arden Y yrhs))" 
   963   show "finite (Subst_all ES Y (Arden Y yrhs))" 
   966     using invariant_ES by (simp add:invariant_def Subst_all_keeps_finite)
 
   964     using invariant_ES by (simp add:invariant_def Subst_all_keeps_finite)
 
   970   show "ardenable (Subst_all ES Y (Arden Y yrhs))"
 
   968   show "ardenable (Subst_all ES Y (Arden Y yrhs))"
 
   971   proof - 
   969   proof - 
   972     { fix X rhs
 
   970     { fix X rhs
 
   973       assume "(X, rhs) \<in> ES"
 
   971       assume "(X, rhs) \<in> ES"
 
   974       hence "rhs_nonempty rhs"  using prems invariant_ES  
   972       hence "rhs_nonempty rhs"  using prems invariant_ES  
   975         by (simp add:invariant_def ardenable_def)
 
   973         by (auto simp add:invariant_def ardenable_def)
 
   976       with nonempty_yrhs 
   974       with nonempty_yrhs 
   977       have "rhs_nonempty (Subst rhs Y (Arden Y yrhs))"
 
   975       have "rhs_nonempty (Subst rhs Y (Arden Y yrhs))"
 
   978         by (simp add:nonempty_yrhs 
   976         by (simp add:nonempty_yrhs 
   979                Subst_keeps_nonempty Arden_keeps_nonempty)
 
   977                Subst_keeps_nonempty Arden_keeps_nonempty)
 
   980     } thus ?thesis by (auto simp add:ardenable_def Subst_all_def)
 
   978     } thus ?thesis by (auto simp add:ardenable_def Subst_all_def)
 
   994   qed
 
   992   qed
 
   995   show "self_contained (Subst_all ES Y (Arden Y yrhs))"
 
   993   show "self_contained (Subst_all ES Y (Arden Y yrhs))"
 
   996     using invariant_ES Subst_all_keeps_self_contained by (simp add:invariant_def)
 
   994     using invariant_ES Subst_all_keeps_self_contained by (simp add:invariant_def)
 
   997 qed
 
   995 qed
 
   998 
   996 
   999 lemma Subst_all_card_le: 
   997 lemma Remove_in_card_measure:
 
  1000   assumes finite: "finite (ES::(string set \<times> rhs_item set) set)"
 
   998   assumes finite: "finite ES"
 
  1001   shows "card (Subst_all ES Y yrhs) <= card ES"
 
   999   and     in_ES: "(X, rhs) \<in> ES"
 
  1002 proof-
 
  1000   shows "(Remove ES X rhs, ES) \<in> measure card"
 
  1003   def f \<equiv> "\<lambda> x. ((fst x)::string set, Subst (snd x) Y yrhs)"
 
  1001 proof -
 
  1004   have "Subst_all ES Y yrhs = f ` ES" 
  1002   def f \<equiv> "\<lambda> x. ((fst x)::lang, Subst (snd x) X (Arden X rhs))"
 
  1005     apply (auto simp:Subst_all_def f_def image_def)
 
  1003   def ES' \<equiv> "ES - {(X, rhs)}"
 
  1006     by (rule_tac x = "(Ya, yrhsa)" in bexI, simp+)
 
  1004   have "Subst_all ES' X (Arden X rhs) = f ` ES'" 
  1007   thus ?thesis using finite by (auto intro:card_image_le)
 
  1005     apply (auto simp: Subst_all_def f_def image_def)
 
  1008 qed
 
  1006     by (rule_tac x = "(Y, yrhs)" in bexI, simp+)
 
       
  1007   then have "card (Subst_all ES' X (Arden X rhs)) \<le> card ES'"
 
       
  1008     unfolding ES'_def using finite by (auto intro: card_image_le)
 
       
  1009   also have "\<dots> < card ES" unfolding ES'_def 
       
  1010     using in_ES finite by (rule_tac card_Diff1_less)
 
       
  1011   finally show "(Remove ES X rhs, ES) \<in> measure card" 
       
  1012     unfolding Remove_def ES'_def by simp
 
       
  1013 qed
 
       
  1014     
  1009 
  1015 
  1010 lemma Subst_all_cls_remains: 
  1016 lemma Subst_all_cls_remains: 
  1011   "(X, xrhs) \<in> ES \<Longrightarrow> \<exists> xrhs'. (X, xrhs') \<in> (Subst_all ES Y yrhs)"
 
  1017   "(X, xrhs) \<in> ES \<Longrightarrow> \<exists> xrhs'. (X, xrhs') \<in> (Subst_all ES Y yrhs)"
 
  1012 by (auto simp:Subst_all_def)
 
  1018 by (auto simp: Subst_all_def)
 
  1013 
  1019 
  1014 lemma card_noteq_1_has_more:
 
  1020 lemma card_noteq_1_has_more:
 
  1015   assumes card:"card S \<noteq> 1"
 
  1021   assumes card:"card S \<noteq> 1"
 
  1016   and e_in: "e \<in> S"
 
  1022   and e_in: "e \<in> S"
 
  1017   and finite: "finite S"
 
  1023   and finite: "finite S"
 
  1018   obtains e' where "e' \<in> S \<and> e \<noteq> e'" 
  1024   obtains e' where "e' \<in> S \<and> e \<noteq> e'"
 
  1019 proof-
 
  1025 proof-
 
  1020   have "card (S - {e}) > 0"
 
  1026   have "card (S - {e}) > 0"
 
  1021   proof -
 
  1027   proof -
 
  1022     have "card S > 1" using card e_in finite  
  1028     have "card S > 1" using card e_in finite 
  1023       by (case_tac "card S", auto) 
  1029       by (cases "card S") (auto) 
  1024     thus ?thesis using finite e_in by auto
 
  1030     thus ?thesis using finite e_in by auto
 
  1025   qed
 
  1031   qed
 
  1026   hence "S - {e} \<noteq> {}" using finite by (rule_tac notI, simp)
 
  1032   hence "S - {e} \<noteq> {}" using finite by (rule_tac notI, simp)
 
  1027   thus "(\<And>e'. e' \<in> S \<and> e \<noteq> e' \<Longrightarrow> thesis) \<Longrightarrow> thesis" by auto
 
  1033   thus "(\<And>e'. e' \<in> S \<and> e \<noteq> e' \<Longrightarrow> thesis) \<Longrightarrow> thesis" by auto
 
  1028 qed
 
  1034 qed
 
  1029 
  1035 
  1030 lemma iteration_step:
 
  1036 
       
  1037 
       
  1038 lemma iteration_step_measure:
 
  1031   assumes Inv_ES: "invariant ES"
 
  1039   assumes Inv_ES: "invariant ES"
 
  1032   and    X_in_ES: "(X, xrhs) \<in> ES"
 
  1040   and    X_in_ES: "(X, xrhs) \<in> ES"
 
  1033   and    not_T: "card ES \<noteq> 1"
 
  1041   and    not_T: "card ES \<noteq> 1"
 
  1034   shows "(invariant (Iter X ES) \<and> (\<exists> xrhs'.(X, xrhs') \<in> (Iter X ES)) \<and> 
  1042   shows "(Iter X ES, ES) \<in> measure card"
 
  1035                 (Iter X ES, ES) \<in> measure card)"
 
       
  1036 proof -
 
  1043 proof -
 
  1037   have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def)
 
  1044   have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def)
 
  1038   then obtain Y yrhs 
  1045   then obtain Y yrhs 
  1039     where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" 
  1046     where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" 
  1040     using not_T X_in_ES by (drule_tac card_noteq_1_has_more, auto)
 
  1047     using not_T X_in_ES by (drule_tac card_noteq_1_has_more) (auto)
 
  1041   let ?ES' = "Iter X ES"
 
  1048   then have "(Y, yrhs) \<in> ES " "X \<noteq> Y"  
  1042   show ?thesis
 
  1049     using X_in_ES Inv_ES 
  1043   proof(unfold Iter_def Remove_def, rule someI2 [where a = "(Y, yrhs)"], clarsimp)
 
  1050     by (auto simp: invariant_def distinct_equas_def)
 
  1044     from X_in_ES Y_in_ES and not_eq and Inv_ES
 
  1051   then show "(Iter X ES, ES) \<in> measure card" 
  1045     show "(Y, yrhs) \<in> ES \<and> X \<noteq> Y"
 
  1052   apply(rule IterI2)
 
  1046       by (auto simp: invariant_def distinct_equas_def)
 
  1053   apply(rule Remove_in_card_measure)
 
  1047   next
 
  1054   apply(simp_all add: finite_ES)
 
  1048     fix x
 
  1055   done
 
  1049     let ?ES' = "let (Y, yrhs) = x in Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)"
 
  1056 qed
 
  1050     assume prem: "case x of (Y, yrhs) \<Rightarrow> (Y, yrhs) \<in> ES \<and> (X \<noteq> Y)"
 
  1057 
  1051     thus "invariant (?ES') \<and> (\<exists>xrhs'. (X, xrhs') \<in> ?ES') \<and> (?ES', ES) \<in> measure card"
 
  1058 lemma iteration_step_invariant:
 
  1052     proof(cases "x", simp)
 
  1059   assumes Inv_ES: "invariant ES"
 
  1053       fix Y yrhs
 
  1060   and    X_in_ES: "(X, xrhs) \<in> ES"
 
  1054       assume h: "(Y, yrhs) \<in> ES \<and>  X \<noteq> Y" 
  1061   and    not_T: "card ES \<noteq> 1"
 
  1055       show "invariant (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) \<and>
 
  1062   shows "invariant (Iter X ES)"
 
  1056              (\<exists>xrhs'. (X, xrhs') \<in> Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) \<and>
 
  1063 proof -
 
  1057              card (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) < card ES"
 
  1064   have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def)
 
  1058       proof -
 
  1065   then obtain Y yrhs 
  1059         have "invariant (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs))" 
  1066     where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" 
  1060         proof(rule Subst_all_satisfies_invariant)
 
  1067     using not_T X_in_ES by (drule_tac card_noteq_1_has_more) (auto)
 
  1061           from h have "(Y, yrhs) \<in> ES" by simp
 
  1068   then have "(Y, yrhs) \<in> ES " "X \<noteq> Y"  
  1062           hence "ES - {(Y, yrhs)} \<union> {(Y, yrhs)} = ES" by auto
 
  1069     using X_in_ES Inv_ES 
  1063           with Inv_ES show "invariant (ES - {(Y, yrhs)} \<union> {(Y, yrhs)})" by auto
 
  1070     by (auto simp: invariant_def distinct_equas_def)
 
  1064         qed
 
  1071   then show "invariant (Iter X ES)" 
  1065         moreover have 
  1072   proof(rule IterI2)
 
  1066           "(\<exists>xrhs'. (X, xrhs') \<in> Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs))"
 
  1073     fix Y yrhs
 
  1067         proof(rule Subst_all_cls_remains)
 
  1074     assume h: "(Y, yrhs) \<in> ES" "X \<noteq> Y"
 
  1068           from X_in_ES and h
 
  1075     then have "ES - {(Y, yrhs)} \<union> {(Y, yrhs)} = ES" by auto
 
  1069           show "(X, xrhs) \<in> ES - {(Y, yrhs)}" by auto
 
  1076     then show "invariant (Remove ES Y yrhs)" unfolding Remove_def
 
  1070         qed
 
  1077       using Inv_ES by (rule_tac Subst_all_satisfies_invariant) (simp) 
  1071         moreover have 
       
  1072           "card (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) < card ES"
 
       
  1073         proof(rule le_less_trans)
 
       
  1074           show 
       
  1075             "card (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) \<le> 
       
  1076                                                                 card (ES - {(Y, yrhs)})"
 
       
  1077           proof(rule Subst_all_card_le)
 
       
  1078             show "finite (ES - {(Y, yrhs)})" using finite_ES by auto
 
       
  1079           qed
 
       
  1080         next
 
       
  1081           show "card (ES - {(Y, yrhs)}) < card ES" using finite_ES h
 
       
  1082             by (auto simp:card_gt_0_iff intro:diff_Suc_less)
 
       
  1083         qed
 
       
  1084         ultimately show ?thesis 
       
  1085           by (auto dest: Subst_all_card_le elim:le_less_trans)
 
       
  1086       qed
 
       
  1087     qed
 
       
  1088   qed
 
  1078   qed
 
       
  1079 qed
 
       
  1080 
       
  1081 lemma iteration_step_ex:
 
       
  1082   assumes Inv_ES: "invariant ES"
 
       
  1083   and    X_in_ES: "(X, xrhs) \<in> ES"
 
       
  1084   and    not_T: "card ES \<noteq> 1"
 
       
  1085   shows "\<exists>xrhs'. (X, xrhs') \<in> (Iter X ES)"
 
       
  1086 proof -
 
       
  1087   have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def)
 
       
  1088   then obtain Y yrhs 
       
  1089     where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" 
       
  1090     using not_T X_in_ES by (drule_tac card_noteq_1_has_more) (auto)
 
       
  1091   then have "(Y, yrhs) \<in> ES " "X \<noteq> Y"  
       
  1092     using X_in_ES Inv_ES 
       
  1093     by (auto simp: invariant_def distinct_equas_def)
 
       
  1094   then show "\<exists>xrhs'. (X, xrhs') \<in> (Iter X ES)" 
       
  1095   apply(rule IterI2)
 
       
  1096   unfolding Remove_def
 
       
  1097   apply(rule Subst_all_cls_remains)
 
       
  1098   using X_in_ES
 
       
  1099   apply(auto)
 
       
  1100   done
 
  1089 qed
 
  1101 qed
 
  1090 
  1102 
  1091 
  1103 
  1092 subsubsection {* Conclusion of the proof *}
 
  1104 subsubsection {* Conclusion of the proof *}
 
  1093 
  1105 
  1094 text {*
 
  1106 text {*
 
  1095   From this point until @{text "hard_direction"}, the hard direction is proved
 
  1107   From this point until @{text "hard_direction"}, the hard direction is proved
 
  1096   through a simple application of the iteration principle.
 
  1108   through a simple application of the iteration principle.
 
  1097 *}
 
  1109 *}
 
       
  1110 
  1098 
  1111 
  1099 lemma reduce_x:
 
  1112 lemma reduce_x:
 
  1100   assumes inv: "invariant ES"
 
  1113   assumes inv: "invariant ES"
 
  1101   and contain_x: "(X, xrhs) \<in> ES" 
  1114   and contain_x: "(X, xrhs) \<in> ES" 
  1102   shows "\<exists> xrhs'. Reduce X ES = {(X, xrhs')} \<and> invariant(Reduce X ES)"
 
  1115   shows "\<exists> xrhs'. Solve X ES = {(X, xrhs')} \<and> invariant(Solve X ES)"
 
  1103 proof -
 
  1116 proof -
 
  1104   let ?Inv = "\<lambda> ES. (invariant ES \<and> (\<exists> xrhs. (X, xrhs) \<in> ES))"
 
  1117   let ?Inv = "\<lambda> ES. (invariant ES \<and> (\<exists> xrhs. (X, xrhs) \<in> ES))"
 
  1105   show ?thesis
 
  1118   show ?thesis unfolding Solve_def
 
  1106   proof (unfold Reduce_def, 
  1119   proof (rule while_rule [where P = ?Inv and r = "measure card"])
 
  1107          rule while_rule [where P = ?Inv and r = "measure card"])
 
       
  1108     from inv and contain_x show "?Inv ES" by auto
 
  1120     from inv and contain_x show "?Inv ES" by auto
 
  1109   next
 
  1121   next
 
  1110     show "wf (measure card)" by simp
 
  1122     show "wf (measure card)" by simp
 
  1111   next
 
  1123   next
 
  1112     fix ES
 
  1124     fix ES
 
  1113     assume inv: "?Inv ES" and crd: "card ES \<noteq> 1"
 
  1125     assume inv: "?Inv ES" and crd: "card ES \<noteq> 1"
 
  1114     show "(Iter X ES, ES) \<in> measure card"
 
  1126     then show "(Iter X ES, ES) \<in> measure card"
 
  1115     proof -
 
  1127       apply(clarify)
 
  1116       from inv obtain xrhs where x_in: "(X, xrhs) \<in> ES" by auto
 
  1128       apply(rule iteration_step_measure)
 
  1117       from inv have "invariant ES" by simp
 
  1129       apply(auto)
 
  1118       from iteration_step [OF this x_in crd]
 
  1130       done
 
  1119       show ?thesis by auto
 
       
  1120     qed
 
       
  1121   next
 
  1131   next
 
  1122     fix ES
 
  1132     fix ES
 
  1123     assume inv: "?Inv ES" and crd: "card ES \<noteq> 1"
 
  1133     assume inv: "?Inv ES" and crd: "card ES \<noteq> 1"
 
  1124     thus "?Inv (Iter X ES)" 
  1134     then show "?Inv (Iter X ES)"
 
  1125     proof -
 
  1135       apply -
 
  1126       from inv obtain xrhs where x_in: "(X, xrhs) \<in> ES" by auto
 
  1136       apply(auto)
 
  1127       from inv have "invariant ES" by simp
 
  1137       apply(rule iteration_step_invariant)
 
  1128       from iteration_step [OF this x_in crd]
 
  1138       apply(auto)
 
  1129       show ?thesis by auto
 
  1139       apply(rule iteration_step_ex)
 
  1130     qed
 
  1140       apply(auto)
 
       
  1141       done
 
  1131   next
 
  1142   next
 
  1132     fix ES
 
  1143     fix ES
 
  1133     assume "?Inv ES" and "\<not> card ES \<noteq> 1"
 
  1144     assume "?Inv ES" and "\<not> card ES \<noteq> 1"
 
  1134     thus "\<exists>xrhs'. ES = {(X, xrhs')} \<and> invariant ES"
 
  1145     thus "\<exists>xrhs'. ES = {(X, xrhs')} \<and> invariant ES"
 
  1135       apply (auto, rule_tac x = xrhs in exI)
 
  1146       apply (auto, rule_tac x = xrhs in exI)
 
  1187     by (rule Init_ES_satisfies_invariant)
 
  1198     by (rule Init_ES_satisfies_invariant)
 
  1188   moreover
 
  1199   moreover
 
  1189   from X_in_CS obtain xrhs where "(X, xrhs) \<in> ES" unfolding ES_def
 
  1200   from X_in_CS obtain xrhs where "(X, xrhs) \<in> ES" unfolding ES_def
 
  1190     unfolding Init_def Init_rhs_def by auto
 
  1201     unfolding Init_def Init_rhs_def by auto
 
  1191   ultimately
 
  1202   ultimately
 
  1192   obtain xrhs' where "Reduce X ES = {(X, xrhs')}" "invariant (Reduce X ES)"
 
  1203   obtain xrhs' where "Solve X ES = {(X, xrhs')}" "invariant (Solve X ES)"
 
  1193     using reduce_x by blast
 
  1204     using reduce_x by blast
 
  1194   then show "\<exists>r::rexp. L r = X"
 
  1205   then show "\<exists>r::rexp. L r = X"
 
  1195   using last_cl_exists_rexp by auto
 
  1206   using last_cl_exists_rexp by auto
 
  1196 qed
 
  1207 qed
 
  1197 
  1208
regexp