Myhill_1.thy
changeset 103 f460d5f75cb5
parent 101 d3fe0597080a
child 104 5bd73aa805a7
equal deleted inserted replaced
102:5fed809d0fc1 103:f460d5f75cb5
   526 *}
   526 *}
   527 
   527 
   528 definition 
   528 definition 
   529   "ardenable ES \<equiv> \<forall>(X, rhs) \<in> ES. rhs_nonempty rhs"
   529   "ardenable ES \<equiv> \<forall>(X, rhs) \<in> ES. rhs_nonempty rhs"
   530 
   530 
       
   531 
   531 text {* 
   532 text {* 
   532   @{text "finite_rhs ES"} requires every equation in @{text "rhs"} 
   533   @{text "finite_rhs ES"} requires every equation in @{text "rhs"} 
   533   be finite.
   534   be finite.
   534 *}
   535 *}
   535 definition
   536 definition
   536   "finite_rhs ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> finite rhs"
   537   "finite_rhs ES \<equiv> \<forall>(X, rhs) \<in> ES. finite rhs"
       
   538 
       
   539 lemma finite_rhs_def2:
       
   540   "finite_rhs ES = (\<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> finite rhs)"
       
   541 unfolding finite_rhs_def by auto
   537 
   542 
   538 text {*
   543 text {*
   539   @{text "classes_of rhs"} returns all variables (or equivalent classes)
   544   @{text "classes_of rhs"} returns all variables (or equivalent classes)
   540   occuring in @{text "rhs"}.
   545   occuring in @{text "rhs"}.
   541   *}
   546   *}
   546 text {*
   551 text {*
   547   @{text "lefts_of ES"} returns all variables defined by an 
   552   @{text "lefts_of ES"} returns all variables defined by an 
   548   equational system @{text "ES"}.
   553   equational system @{text "ES"}.
   549 *}
   554 *}
   550 definition
   555 definition
   551   "lefts_of ES \<equiv> {Y | Y yrhs. (Y, yrhs) \<in> ES}"
   556   "lhss ES \<equiv> {Y | Y yrhs. (Y, yrhs) \<in> ES}"
   552 
   557 
   553 text {*
   558 text {*
   554   The following @{text "self_contained ES"} requires that every variable occuring 
   559   The following @{text "self_contained ES"} requires that every variable occuring 
   555   on the right hand side of equations is already defined by some equation in @{text "ES"}.
   560   on the right hand side of equations is already defined by some equation in @{text "ES"}.
   556 *}
   561 *}
   557 definition 
   562 definition 
   558   "self_contained ES \<equiv> \<forall>(X, xrhs) \<in> ES. classes_of xrhs \<subseteq> lefts_of ES"
   563   "self_contained ES \<equiv> \<forall>(X, xrhs) \<in> ES. classes_of xrhs \<subseteq> lhss ES"
   559 
   564 
   560 
   565 
   561 text {*
   566 text {*
   562   The invariant @{text "invariant(ES)"} is a conjunction of all the previously defined constaints.
   567   The invariant @{text "invariant(ES)"} is a conjunction of all the previously defined constaints.
   563   *}
   568   *}
   564 definition 
   569 definition 
   565   "invariant ES \<equiv> valid_eqns ES \<and> finite ES \<and> distinct_equas ES \<and> ardenable ES \<and> 
   570   "invariant ES \<equiv> finite ES
   566                   finite_rhs ES \<and> self_contained ES"
   571                 \<and> finite_rhs ES
       
   572                 \<and> valid_eqns ES 
       
   573                 \<and> distinct_equas ES 
       
   574                 \<and> ardenable ES 
       
   575                 \<and> self_contained ES"
   567 
   576 
   568 
   577 
   569 lemma invariantI:
   578 lemma invariantI:
   570   assumes "valid_eqns ES" "finite ES" "distinct_equas ES" "ardenable ES" 
   579   assumes "valid_eqns ES" "finite ES" "distinct_equas ES" "ardenable ES" 
   571           "finite_rhs ES" "self_contained ES"
   580           "finite_rhs ES" "self_contained ES"
   643 
   652 
   644 lemma classes_of_union_distrib:
   653 lemma classes_of_union_distrib:
   645   shows "classes_of (A \<union> B) = classes_of A \<union> classes_of B"
   654   shows "classes_of (A \<union> B) = classes_of A \<union> classes_of B"
   646 by (auto simp add: classes_of_def)
   655 by (auto simp add: classes_of_def)
   647 
   656 
   648 lemma lefts_of_union_distrib:
   657 lemma lhss_union_distrib:
   649   shows "lefts_of (A \<union> B) = lefts_of A \<union> lefts_of B"
   658   shows "lhss (A \<union> B) = lhss A \<union> lhss B"
   650 by (auto simp add: lefts_of_def)
   659 by (auto simp add: lhss_def)
   651 
   660 
   652 
   661 
   653 subsubsection {* Intialization *}
   662 subsubsection {* Intialization *}
   654 
   663 
   655 text {*
   664 text {*
   758     unfolding Init_def by simp
   767     unfolding Init_def by simp
   759   show "distinct_equas (Init (UNIV // \<approx>A))"     
   768   show "distinct_equas (Init (UNIV // \<approx>A))"     
   760     unfolding distinct_equas_def Init_def by simp
   769     unfolding distinct_equas_def Init_def by simp
   761   show "ardenable (Init (UNIV // \<approx>A))"
   770   show "ardenable (Init (UNIV // \<approx>A))"
   762     unfolding ardenable_def Init_def Init_rhs_def rhs_nonempty_def
   771     unfolding ardenable_def Init_def Init_rhs_def rhs_nonempty_def
   763     by auto
   772    by auto 
   764   show "finite_rhs (Init (UNIV // \<approx>A))"
   773   show "finite_rhs (Init (UNIV // \<approx>A))"
   765     using finite_Init_rhs[OF finite_CS]
   774     using finite_Init_rhs[OF finite_CS]
   766     unfolding finite_rhs_def Init_def by auto
   775     unfolding finite_rhs_def Init_def by auto
   767   show "self_contained (Init (UNIV // \<approx>A))"
   776   show "self_contained (Init (UNIV // \<approx>A))"
   768     unfolding self_contained_def Init_def Init_rhs_def classes_of_def lefts_of_def
   777     unfolding self_contained_def Init_def Init_rhs_def classes_of_def lhss_def
   769     by auto
   778     by auto
   770 qed
   779 qed
   771 
   780 
   772 subsubsection {* Interation step *}
   781 subsubsection {* Interation step *}
   773 
   782 
   890 lemma Arden_removes_cl:
   899 lemma Arden_removes_cl:
   891   "classes_of (Arden Y yrhs) = classes_of yrhs - {Y}"
   900   "classes_of (Arden Y yrhs) = classes_of yrhs - {Y}"
   892 apply (simp add:Arden_def append_rhs_keeps_cls)
   901 apply (simp add:Arden_def append_rhs_keeps_cls)
   893 by (auto simp:classes_of_def)
   902 by (auto simp:classes_of_def)
   894 
   903 
   895 lemma lefts_of_keeps_cls:
   904 lemma lhss_keeps_cls:
   896   "lefts_of (Subst_all ES Y yrhs) = lefts_of ES"
   905   "lhss (Subst_all ES Y yrhs) = lhss ES"
   897 by (auto simp:lefts_of_def Subst_all_def)
   906 by (auto simp:lhss_def Subst_all_def)
   898 
   907 
   899 lemma Subst_updates_cls:
   908 lemma Subst_updates_cls:
   900   "X \<notin> classes_of xrhs \<Longrightarrow> 
   909   "X \<notin> classes_of xrhs \<Longrightarrow> 
   901       classes_of (Subst rhs X xrhs) = classes_of rhs \<union> classes_of xrhs - {X}"
   910       classes_of (Subst rhs X xrhs) = classes_of rhs \<union> classes_of xrhs - {X}"
   902 apply (simp only:Subst_def append_rhs_keeps_cls classes_of_union_distrib)
   911 apply (simp only:Subst_def append_rhs_keeps_cls classes_of_union_distrib)
   910   { fix X xrhs'
   919   { fix X xrhs'
   911     assume "(X, xrhs') \<in> ?B"
   920     assume "(X, xrhs') \<in> ?B"
   912     then obtain xrhs 
   921     then obtain xrhs 
   913       where xrhs_xrhs': "xrhs' = Subst xrhs Y (Arden Y yrhs)"
   922       where xrhs_xrhs': "xrhs' = Subst xrhs Y (Arden Y yrhs)"
   914       and X_in: "(X, xrhs) \<in> ES" by (simp add:Subst_all_def, blast)    
   923       and X_in: "(X, xrhs) \<in> ES" by (simp add:Subst_all_def, blast)    
   915     have "classes_of xrhs' \<subseteq> lefts_of ?B"
   924     have "classes_of xrhs' \<subseteq> lhss ?B"
   916     proof-
   925     proof-
   917       have "lefts_of ?B = lefts_of ES" by (auto simp add:lefts_of_def Subst_all_def)
   926       have "lhss ?B = lhss ES" by (auto simp add:lhss_def Subst_all_def)
   918       moreover have "classes_of xrhs' \<subseteq> lefts_of ES"
   927       moreover have "classes_of xrhs' \<subseteq> lhss ES"
   919       proof-
   928       proof-
   920         have "classes_of xrhs' \<subseteq> 
   929         have "classes_of xrhs' \<subseteq> 
   921                         classes_of xrhs \<union> classes_of (Arden Y yrhs) - {Y}"
   930                         classes_of xrhs \<union> classes_of (Arden Y yrhs) - {Y}"
   922         proof-
   931         proof-
   923           have "Y \<notin> classes_of (Arden Y yrhs)" 
   932           have "Y \<notin> classes_of (Arden Y yrhs)" 
   924             using Arden_removes_cl by simp
   933             using Arden_removes_cl by simp
   925           thus ?thesis using xrhs_xrhs' by (auto simp:Subst_updates_cls)
   934           thus ?thesis using xrhs_xrhs' by (auto simp:Subst_updates_cls)
   926         qed
   935         qed
   927         moreover have "classes_of xrhs \<subseteq> lefts_of ES \<union> {Y}" using X_in sc
   936         moreover have "classes_of xrhs \<subseteq> lhss ES \<union> {Y}" using X_in sc
   928           apply (simp only:self_contained_def lefts_of_union_distrib)
   937           apply (simp only:self_contained_def lhss_union_distrib)
   929           by (drule_tac x = "(X, xrhs)" in bspec, auto simp:lefts_of_def)
   938           by (drule_tac x = "(X, xrhs)" in bspec, auto simp:lhss_def)
   930         moreover have "classes_of (Arden Y yrhs) \<subseteq> lefts_of ES \<union> {Y}" 
   939         moreover have "classes_of (Arden Y yrhs) \<subseteq> lhss ES \<union> {Y}" 
   931           using sc 
   940           using sc 
   932           by (auto simp add:Arden_removes_cl self_contained_def lefts_of_def)
   941           by (auto simp add:Arden_removes_cl self_contained_def lhss_def)
   933         ultimately show ?thesis by auto
   942         ultimately show ?thesis by auto
   934       qed
   943       qed
   935       ultimately show ?thesis by simp
   944       ultimately show ?thesis by simp
   936     qed
   945     qed
   937   } thus ?thesis by (auto simp only:Subst_all_def self_contained_def)
   946   } thus ?thesis by (auto simp only:Subst_all_def self_contained_def)
   948   have nonempty_yrhs: "rhs_nonempty yrhs" 
   957   have nonempty_yrhs: "rhs_nonempty yrhs" 
   949     using invariant_ES by (auto simp:invariant_def ardenable_def)
   958     using invariant_ES by (auto simp:invariant_def ardenable_def)
   950   show "valid_eqns (Subst_all ES Y (Arden Y yrhs))"
   959   show "valid_eqns (Subst_all ES Y (Arden Y yrhs))"
   951   proof-
   960   proof-
   952     have "Y = L (Arden Y yrhs)" 
   961     have "Y = L (Arden Y yrhs)" 
   953       using Y_eq_yrhs invariant_ES finite_yrhs nonempty_yrhs
   962       using Y_eq_yrhs invariant_ES finite_yrhs
   954       by (rule_tac Arden_keeps_eq, (simp add:rexp_of_empty)+)
   963       using finite_Trn[OF finite_yrhs]
   955     thus ?thesis using invariant_ES 
   964       apply(rule_tac Arden_keeps_eq)
   956       by (auto simp add:valid_eqns_def 
   965       apply(simp_all)
   957         Subst_all_def Subst_keeps_eq invariant_def finite_rhs_def
   966       unfolding invariant_def ardenable_def rhs_nonempty_def
   958         simp del:L_rhs.simps)
   967       apply(auto)
       
   968       done
       
   969     thus ?thesis using invariant_ES
       
   970       unfolding  invariant_def finite_rhs_def2 valid_eqns_def Subst_all_def
       
   971       by (auto simp add: Subst_keeps_eq simp del: L_rhs.simps)
   959   qed
   972   qed
   960   show "finite (Subst_all ES Y (Arden Y yrhs))" 
   973   show "finite (Subst_all ES Y (Arden Y yrhs))" 
   961     using invariant_ES by (simp add:invariant_def Subst_all_keeps_finite)
   974     using invariant_ES by (simp add:invariant_def Subst_all_keeps_finite)
   962   show "distinct_equas (Subst_all ES Y (Arden Y yrhs))" 
   975   show "distinct_equas (Subst_all ES Y (Arden Y yrhs))" 
   963     using invariant_ES
   976     using invariant_ES
  1013 lemma Subst_all_cls_remains: 
  1026 lemma Subst_all_cls_remains: 
  1014   "(X, xrhs) \<in> ES \<Longrightarrow> \<exists> xrhs'. (X, xrhs') \<in> (Subst_all ES Y yrhs)"
  1027   "(X, xrhs) \<in> ES \<Longrightarrow> \<exists> xrhs'. (X, xrhs') \<in> (Subst_all ES Y yrhs)"
  1015 by (auto simp: Subst_all_def)
  1028 by (auto simp: Subst_all_def)
  1016 
  1029 
  1017 lemma card_noteq_1_has_more:
  1030 lemma card_noteq_1_has_more:
  1018   assumes card:"card S \<noteq> 1"
  1031   assumes card:"Cond ES"
  1019   and e_in: "e \<in> S"
  1032   and e_in: "(X, xrhs) \<in> ES"
  1020   and finite: "finite S"
  1033   and finite: "finite ES"
  1021   obtains e' where "e' \<in> S \<and> e \<noteq> e'"
  1034   shows "\<exists>(Y, yrhs) \<in> ES. (X, xrhs) \<noteq> (Y, yrhs)"
  1022 proof-
  1035 proof-
  1023   have "card (S - {e}) > 0"
  1036   have "card ES > 1" using card e_in finite 
  1024   proof -
  1037     by (cases "card ES") (auto) 
  1025     have "card S > 1" using card e_in finite 
  1038   then have "card (ES - {(X, xrhs)}) > 0"
  1026       by (cases "card S") (auto) 
  1039     using finite e_in by auto
  1027     thus ?thesis using finite e_in by auto
  1040   then have "(ES - {(X, xrhs)}) \<noteq> {}" using finite by (rule_tac notI, simp)
  1028   qed
  1041   then show "\<exists>(Y, yrhs) \<in> ES. (X, xrhs) \<noteq> (Y, yrhs)"
  1029   hence "S - {e} \<noteq> {}" using finite by (rule_tac notI, simp)
  1042     by auto
  1030   thus "(\<And>e'. e' \<in> S \<and> e \<noteq> e' \<Longrightarrow> thesis) \<Longrightarrow> thesis" by auto
  1043 qed
  1031 qed
       
  1032 
       
  1033 
       
  1034 
  1044 
  1035 lemma iteration_step_measure:
  1045 lemma iteration_step_measure:
  1036   assumes Inv_ES: "invariant ES"
  1046   assumes Inv_ES: "invariant ES"
  1037   and    X_in_ES: "(X, xrhs) \<in> ES"
  1047   and    X_in_ES: "(X, xrhs) \<in> ES"
  1038   and    not_T: "card ES \<noteq> 1"
  1048   and    not_T: "Cond ES "
  1039   shows "(Iter X ES, ES) \<in> measure card"
  1049   shows "(Iter X ES, ES) \<in> measure card"
  1040 proof -
  1050 proof -
  1041   have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def)
  1051   have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def)
  1042   then obtain Y yrhs 
  1052   then obtain Y yrhs 
  1043     where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" 
  1053     where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" 
  1044     using not_T X_in_ES by (drule_tac card_noteq_1_has_more) (auto)
  1054     using not_T X_in_ES by (drule_tac card_noteq_1_has_more) (auto)
  1045   then have "(Y, yrhs) \<in> ES " "X \<noteq> Y"  
  1055   then have "(Y, yrhs) \<in> ES " "X \<noteq> Y"  
  1046     using X_in_ES Inv_ES 
  1056     using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def
  1047     by (auto simp: invariant_def distinct_equas_def)
  1057     by auto
  1048   then show "(Iter X ES, ES) \<in> measure card" 
  1058   then show "(Iter X ES, ES) \<in> measure card" 
  1049   apply(rule IterI2)
  1059   apply(rule IterI2)
  1050   apply(rule Remove_in_card_measure)
  1060   apply(rule Remove_in_card_measure)
  1051   apply(simp_all add: finite_ES)
  1061   apply(simp_all add: finite_ES)
  1052   done
  1062   done
  1053 qed
  1063 qed
  1054 
  1064 
  1055 lemma iteration_step_invariant:
  1065 lemma iteration_step_invariant:
  1056   assumes Inv_ES: "invariant ES"
  1066   assumes Inv_ES: "invariant ES"
  1057   and    X_in_ES: "(X, xrhs) \<in> ES"
  1067   and    X_in_ES: "(X, xrhs) \<in> ES"
  1058   and    not_T: "card ES \<noteq> 1"
  1068   and    not_T: "Cond ES"
  1059   shows "invariant (Iter X ES)"
  1069   shows "invariant (Iter X ES)"
  1060 proof -
  1070 proof -
  1061   have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def)
  1071   have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def)
  1062   then obtain Y yrhs 
  1072   then obtain Y yrhs 
  1063     where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" 
  1073     where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" 
  1064     using not_T X_in_ES by (drule_tac card_noteq_1_has_more) (auto)
  1074     using not_T X_in_ES by (drule_tac card_noteq_1_has_more) (auto)
  1065   then have "(Y, yrhs) \<in> ES " "X \<noteq> Y"  
  1075   then have "(Y, yrhs) \<in> ES" "X \<noteq> Y" 
  1066     using X_in_ES Inv_ES 
  1076     using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def
  1067     by (auto simp: invariant_def distinct_equas_def)
  1077     by auto
  1068   then show "invariant (Iter X ES)" 
  1078   then show "invariant (Iter X ES)" 
  1069   proof(rule IterI2)
  1079   proof(rule IterI2)
  1070     fix Y yrhs
  1080     fix Y yrhs
  1071     assume h: "(Y, yrhs) \<in> ES" "X \<noteq> Y"
  1081     assume h: "(Y, yrhs) \<in> ES" "X \<noteq> Y"
  1072     then have "ES - {(Y, yrhs)} \<union> {(Y, yrhs)} = ES" by auto
  1082     then have "ES - {(Y, yrhs)} \<union> {(Y, yrhs)} = ES" by auto
  1076 qed
  1086 qed
  1077 
  1087 
  1078 lemma iteration_step_ex:
  1088 lemma iteration_step_ex:
  1079   assumes Inv_ES: "invariant ES"
  1089   assumes Inv_ES: "invariant ES"
  1080   and    X_in_ES: "(X, xrhs) \<in> ES"
  1090   and    X_in_ES: "(X, xrhs) \<in> ES"
  1081   and    not_T: "card ES \<noteq> 1"
  1091   and    not_T: "Cond ES"
  1082   shows "\<exists>xrhs'. (X, xrhs') \<in> (Iter X ES)"
  1092   shows "\<exists>xrhs'. (X, xrhs') \<in> (Iter X ES)"
  1083 proof -
  1093 proof -
  1084   have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def)
  1094   have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def)
  1085   then obtain Y yrhs 
  1095   then obtain Y yrhs 
  1086     where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" 
  1096     where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" 
  1087     using not_T X_in_ES by (drule_tac card_noteq_1_has_more) (auto)
  1097     using not_T X_in_ES by (drule_tac card_noteq_1_has_more) (auto)
  1088   then have "(Y, yrhs) \<in> ES " "X \<noteq> Y"  
  1098   then have "(Y, yrhs) \<in> ES " "X \<noteq> Y"  
  1089     using X_in_ES Inv_ES 
  1099     using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def
  1090     by (auto simp: invariant_def distinct_equas_def)
  1100     by auto
  1091   then show "\<exists>xrhs'. (X, xrhs') \<in> (Iter X ES)" 
  1101   then show "\<exists>xrhs'. (X, xrhs') \<in> (Iter X ES)" 
  1092   apply(rule IterI2)
  1102   apply(rule IterI2)
  1093   unfolding Remove_def
  1103   unfolding Remove_def
  1094   apply(rule Subst_all_cls_remains)
  1104   apply(rule Subst_all_cls_remains)
  1095   using X_in_ES
  1105   using X_in_ES
  1098 qed
  1108 qed
  1099 
  1109 
  1100 
  1110 
  1101 subsubsection {* Conclusion of the proof *}
  1111 subsubsection {* Conclusion of the proof *}
  1102 
  1112 
  1103 text {*
  1113 lemma Solve:
  1104   From this point until @{text "hard_direction"}, the hard direction is proved
  1114   assumes fin: "finite (UNIV // \<approx>A)"
  1105   through a simple application of the iteration principle.
  1115   and     X_in: "X \<in> (UNIV // \<approx>A)"
  1106 *}
  1116   shows "\<exists>xrhs. Solve X (Init (UNIV // \<approx>A)) = {(X, xrhs)} \<and> invariant {(X, xrhs)}"
  1107 
  1117 proof -
  1108 
  1118   def Inv \<equiv> "\<lambda>ES. invariant ES \<and> (\<exists>xrhs. (X, xrhs) \<in> ES)"
  1109 lemma reduce_x:
  1119   have "Inv (Init (UNIV // \<approx>A))" unfolding Inv_def
  1110   assumes inv: "invariant ES"
  1120       using fin X_in by (simp add: Init_ES_satisfies_invariant, simp add: Init_def)
  1111   and contain_x: "(X, xrhs) \<in> ES" 
  1121   moreover
  1112   shows "\<exists> xrhs'. Solve X ES = {(X, xrhs')} \<and> invariant(Solve X ES)"
  1122   { fix ES
  1113 proof -
  1123     assume inv: "Inv ES" and crd: "Cond ES"
  1114   let ?Inv = "\<lambda> ES. (invariant ES \<and> (\<exists> xrhs. (X, xrhs) \<in> ES))"
  1124     then have "Inv (Iter X ES)"
  1115   show ?thesis unfolding Solve_def
  1125       unfolding Inv_def
  1116   proof (rule while_rule [where P = ?Inv and r = "measure card"])
  1126       by (auto simp add: iteration_step_invariant iteration_step_ex) }
  1117     from inv and contain_x show "?Inv ES" by auto
  1127   moreover
  1118   next
  1128   { fix ES
  1119     show "wf (measure card)" by simp
  1129     assume "Inv ES" and "\<not> Cond ES"
  1120   next
  1130     then have "\<exists>xrhs'. ES = {(X, xrhs')} \<and> invariant ES"
  1121     fix ES
  1131       unfolding Inv_def invariant_def
  1122     assume inv: "?Inv ES" and crd: "card ES \<noteq> 1"
  1132       apply (auto, rule_tac x = xrhs in exI)
  1123     then show "(Iter X ES, ES) \<in> measure card"
  1133       apply (auto dest!: card_Suc_Diff1 simp: card_eq_0_iff) 
       
  1134       done
       
  1135     then have "\<exists>xrhs'. ES = {(X, xrhs')} \<and> invariant {(X, xrhs')}"
       
  1136       by auto }
       
  1137   moreover
       
  1138     have "wf (measure card)" by simp
       
  1139   moreover
       
  1140   { fix ES
       
  1141     assume inv: "Inv ES" and crd: "Cond ES"
       
  1142     then have "(Iter X ES, ES) \<in> measure card"
       
  1143       unfolding Inv_def
  1124       apply(clarify)
  1144       apply(clarify)
  1125       apply(rule iteration_step_measure)
  1145       apply(rule_tac iteration_step_measure)
  1126       apply(auto)
  1146       apply(auto)
  1127       done
  1147       done }
  1128   next
  1148   ultimately 
  1129     fix ES
  1149   show "\<exists>xrhs. Solve X (Init (UNIV // \<approx>A)) = {(X, xrhs)} \<and> invariant {(X, xrhs)}" 
  1130     assume inv: "?Inv ES" and crd: "card ES \<noteq> 1"
  1150     unfolding Solve_def by (rule while_rule)
  1131     then show "?Inv (Iter X ES)"
       
  1132       apply -
       
  1133       apply(auto)
       
  1134       apply(rule iteration_step_invariant)
       
  1135       apply(auto)
       
  1136       apply(rule iteration_step_ex)
       
  1137       apply(auto)
       
  1138       done
       
  1139   next
       
  1140     fix ES
       
  1141     assume "?Inv ES" and "\<not> card ES \<noteq> 1"
       
  1142     thus "\<exists>xrhs'. ES = {(X, xrhs')} \<and> invariant ES"
       
  1143       apply (auto, rule_tac x = xrhs in exI)
       
  1144       by (auto simp: invariant_def dest!:card_Suc_Diff1 simp:card_eq_0_iff) 
       
  1145   qed
       
  1146 qed
  1151 qed
  1147 
  1152 
  1148 lemma last_cl_exists_rexp:
  1153 lemma last_cl_exists_rexp:
  1149   assumes Inv_ES: "invariant {(X, xrhs)}"
  1154   assumes Inv_ES: "invariant {(X, xrhs)}"
  1150   shows "\<exists>r::rexp. L r = X" 
  1155   shows "\<exists>r::rexp. L r = X" 
  1151 proof-
  1156 proof-
  1152   def A \<equiv> "Arden X xrhs"
  1157   def A \<equiv> "Arden X xrhs"
  1153   have eq: "{Lam r | r. Lam r \<in> A} = A"
  1158   have eq: "{Lam r | r. Lam r \<in> A} = A"
  1154   proof -
  1159   proof -
  1155     have "classes_of A = {}" using Inv_ES 
  1160     have "classes_of A = {}" using Inv_ES 
  1156       unfolding A_def self_contained_def invariant_def lefts_of_def
  1161       unfolding A_def self_contained_def invariant_def lhss_def
  1157       by (simp add: Arden_removes_cl) 
  1162       by (simp add: Arden_removes_cl) 
  1158     thus ?thesis unfolding A_def classes_of_def
  1163     thus ?thesis unfolding A_def classes_of_def
  1159       apply(auto simp only:)
  1164       apply(auto simp only:)
  1160       apply(case_tac x)
  1165       apply(case_tac x)
  1161       apply(auto)
  1166       apply(auto)
  1188 lemma every_eqcl_has_reg: 
  1193 lemma every_eqcl_has_reg: 
  1189   assumes finite_CS: "finite (UNIV // \<approx>A)"
  1194   assumes finite_CS: "finite (UNIV // \<approx>A)"
  1190   and X_in_CS: "X \<in> (UNIV // \<approx>A)"
  1195   and X_in_CS: "X \<in> (UNIV // \<approx>A)"
  1191   shows "\<exists>r::rexp. L r = X"
  1196   shows "\<exists>r::rexp. L r = X"
  1192 proof -
  1197 proof -
  1193   def ES \<equiv> "Init (UNIV // \<approx>A)"
  1198   from finite_CS X_in_CS 
  1194   have "invariant ES" using finite_CS unfolding ES_def
  1199   obtain xrhs where "invariant {(X, xrhs)}"
  1195     by (rule Init_ES_satisfies_invariant)
  1200     using Solve by metis
  1196   moreover
       
  1197   from X_in_CS obtain xrhs where "(X, xrhs) \<in> ES" unfolding ES_def
       
  1198     unfolding Init_def Init_rhs_def by auto
       
  1199   ultimately
       
  1200   obtain xrhs' where "Solve X ES = {(X, xrhs')}" "invariant (Solve X ES)"
       
  1201     using reduce_x by blast
       
  1202   then show "\<exists>r::rexp. L r = X"
  1201   then show "\<exists>r::rexp. L r = X"
  1203   using last_cl_exists_rexp by auto
  1202     using last_cl_exists_rexp by auto
  1204 qed
  1203 qed
  1205 
       
  1206 
  1204 
  1207 lemma bchoice_finite_set:
  1205 lemma bchoice_finite_set:
  1208   assumes a: "\<forall>x \<in> S. \<exists>y. x = f y" 
  1206   assumes a: "\<forall>x \<in> S. \<exists>y. x = f y" 
  1209   and     b: "finite S"
  1207   and     b: "finite S"
  1210   shows "\<exists>ys. (\<Union> S) = \<Union>(f ` ys) \<and> finite ys"
  1208   shows "\<exists>ys. (\<Union> S) = \<Union>(f ` ys) \<and> finite ys"