equal
deleted
inserted
replaced
510 *} |
510 *} |
511 |
511 |
512 definition |
512 definition |
513 "ardenable ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> rhs_nonempty rhs" |
513 "ardenable ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> rhs_nonempty rhs" |
514 |
514 |
515 (* The following non_empty seems useless. *) |
|
516 definition |
|
517 "non_empty ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> X \<noteq> {}" |
|
518 |
|
519 text {* |
515 text {* |
520 @{text "finite_rhs ES"} requires every equation in @{text "rhs"} |
516 @{text "finite_rhs ES"} requires every equation in @{text "rhs"} |
521 be finite. |
517 be finite. |
522 *} |
518 *} |
523 definition |
519 definition |
549 text {* |
545 text {* |
550 The invariant @{text "invariant(ES)"} is a conjunction of all the previously defined constaints. |
546 The invariant @{text "invariant(ES)"} is a conjunction of all the previously defined constaints. |
551 *} |
547 *} |
552 definition |
548 definition |
553 "invariant ES \<equiv> valid_eqns ES \<and> finite ES \<and> distinct_equas ES \<and> ardenable ES \<and> |
549 "invariant ES \<equiv> valid_eqns ES \<and> finite ES \<and> distinct_equas ES \<and> ardenable ES \<and> |
554 non_empty ES \<and> finite_rhs ES \<and> self_contained ES" |
550 finite_rhs ES \<and> self_contained ES" |
555 |
551 |
556 subsection {* The proof of this direction *} |
552 subsection {* The proof of this direction *} |
557 |
553 |
558 subsubsection {* Basic properties *} |
554 subsubsection {* Basic properties *} |
559 |
555 |
746 by (simp add:distinct_equas_def eqs_def) |
742 by (simp add:distinct_equas_def eqs_def) |
747 moreover have "ardenable (eqs (UNIV // (\<approx>Lang)))" |
743 moreover have "ardenable (eqs (UNIV // (\<approx>Lang)))" |
748 by (auto simp add:ardenable_def eqs_def init_rhs_def rhs_nonempty_def del:L_rhs.simps) |
744 by (auto simp add:ardenable_def eqs_def init_rhs_def rhs_nonempty_def del:L_rhs.simps) |
749 moreover have "valid_eqns (eqs (UNIV // (\<approx>Lang)))" |
745 moreover have "valid_eqns (eqs (UNIV // (\<approx>Lang)))" |
750 using l_eq_r_in_eqs by (simp add:valid_eqns_def) |
746 using l_eq_r_in_eqs by (simp add:valid_eqns_def) |
751 moreover have "non_empty (eqs (UNIV // (\<approx>Lang)))" |
|
752 by (auto simp:non_empty_def eqs_def quotient_def Image_def str_eq_rel_def) |
|
753 moreover have "finite_rhs (eqs (UNIV // (\<approx>Lang)))" |
747 moreover have "finite_rhs (eqs (UNIV // (\<approx>Lang)))" |
754 using finite_init_rhs[OF finite_CS] |
748 using finite_init_rhs[OF finite_CS] |
755 by (auto simp:finite_rhs_def eqs_def) |
749 by (auto simp:finite_rhs_def eqs_def) |
756 moreover have "self_contained (eqs (UNIV // (\<approx>Lang)))" |
750 moreover have "self_contained (eqs (UNIV // (\<approx>Lang)))" |
757 by (auto simp:self_contained_def eqs_def init_rhs_def classes_of_def lefts_of_def) |
751 by (auto simp:self_contained_def eqs_def init_rhs_def classes_of_def lefts_of_def) |
981 thus ?thesis using invariant_ES |
975 thus ?thesis using invariant_ES |
982 by (clarsimp simp add:valid_eqns_def |
976 by (clarsimp simp add:valid_eqns_def |
983 subst_op_all_def subst_op_keeps_eq invariant_def finite_rhs_def |
977 subst_op_all_def subst_op_keeps_eq invariant_def finite_rhs_def |
984 simp del:L_rhs.simps) |
978 simp del:L_rhs.simps) |
985 qed |
979 qed |
986 moreover have |
|
987 non_empty_subst: "non_empty (subst_op_all ES Y (arden_op Y yrhs))" |
|
988 using invariant_ES by (auto simp:invariant_def non_empty_def subst_op_all_def) |
|
989 moreover |
980 moreover |
990 have self_subst: "self_contained (subst_op_all ES Y (arden_op Y yrhs))" |
981 have self_subst: "self_contained (subst_op_all ES Y (arden_op Y yrhs))" |
991 using invariant_ES subst_op_all_keeps_self_contained by (simp add:invariant_def) |
982 using invariant_ES subst_op_all_keeps_self_contained by (simp add:invariant_def) |
992 ultimately show ?thesis using invariant_ES by (simp add:invariant_def) |
983 ultimately show ?thesis using invariant_ES by (simp add:invariant_def) |
993 qed |
984 qed |