equal
deleted
inserted
replaced
446 |
446 |
447 |
447 |
448 section {* Substitution Operation on equations *} |
448 section {* Substitution Operation on equations *} |
449 |
449 |
450 text {* |
450 text {* |
451 Suppose and equation @{text "X = xrhs"}, @{text "subst_op"} substitutes |
451 Suppose and equation @{text "X = xrhs"}, @{text "Subst"} substitutes |
452 all occurences of @{text "X"} in @{text "rhs"} by @{text "xrhs"}. |
452 all occurences of @{text "X"} in @{text "rhs"} by @{text "xrhs"}. |
453 *} |
453 *} |
454 |
454 |
455 definition |
455 definition |
456 "Subst rhs X xrhs \<equiv> |
456 "Subst rhs X xrhs \<equiv> |
474 The @{text "Y"}-definition is made non-recursive using Arden's transformation |
474 The @{text "Y"}-definition is made non-recursive using Arden's transformation |
475 @{text "arden_variate Y yrhs"}. |
475 @{text "arden_variate Y yrhs"}. |
476 *} |
476 *} |
477 |
477 |
478 definition |
478 definition |
479 "remove_op ES Y yrhs \<equiv> |
479 "Remove ES Y yrhs \<equiv> |
480 Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)" |
480 Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)" |
481 |
481 |
482 text {* |
482 text {* |
483 The following term @{text "iterm X ES"} represents one iteration in the while loop. |
483 The following term @{text "iterm X ES"} represents one iteration in the while loop. |
484 It arbitrarily chooses a @{text "Y"} different from @{text "X"} to remove. |
484 It arbitrarily chooses a @{text "Y"} different from @{text "X"} to remove. |
485 *} |
485 *} |
486 |
486 |
487 definition |
487 definition |
488 "iter X ES \<equiv> (let (Y, yrhs) = SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> (X \<noteq> Y) |
488 "iter X ES \<equiv> (let (Y, yrhs) = SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> (X \<noteq> Y) |
489 in remove_op ES Y yrhs)" |
489 in Remove ES Y yrhs)" |
490 |
490 |
491 text {* |
491 text {* |
492 The following term @{text "reduce X ES"} repeatedly removes characteriztion equations |
492 The following term @{text "reduce X ES"} repeatedly removes characteriztion equations |
493 for unknowns other than @{text "X"} until one is left. |
493 for unknowns other than @{text "X"} until one is left. |
494 *} |
494 *} |
909 apply (simp only:Subst_def append_rhs_keeps_cls |
909 apply (simp only:Subst_def append_rhs_keeps_cls |
910 classes_of_union_distrib[THEN sym]) |
910 classes_of_union_distrib[THEN sym]) |
911 by (auto simp:classes_of_def) |
911 by (auto simp:classes_of_def) |
912 |
912 |
913 lemma Subst_all_keeps_self_contained: |
913 lemma Subst_all_keeps_self_contained: |
914 fixes Y |
|
915 assumes sc: "self_contained (ES \<union> {(Y, yrhs)})" (is "self_contained ?A") |
914 assumes sc: "self_contained (ES \<union> {(Y, yrhs)})" (is "self_contained ?A") |
916 shows "self_contained (Subst_all ES Y (Arden Y yrhs))" |
915 shows "self_contained (Subst_all ES Y (Arden Y yrhs))" |
917 (is "self_contained ?B") |
916 (is "self_contained ?B") |
918 proof- |
917 proof- |
919 { fix X xrhs' |
918 { fix X xrhs' |
1044 then obtain Y yrhs |
1043 then obtain Y yrhs |
1045 where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" |
1044 where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" |
1046 using not_T X_in_ES by (drule_tac card_noteq_1_has_more, auto) |
1045 using not_T X_in_ES by (drule_tac card_noteq_1_has_more, auto) |
1047 let ?ES' = "iter X ES" |
1046 let ?ES' = "iter X ES" |
1048 show ?thesis |
1047 show ?thesis |
1049 proof(unfold iter_def remove_op_def, rule someI2 [where a = "(Y, yrhs)"], clarsimp) |
1048 proof(unfold iter_def Remove_def, rule someI2 [where a = "(Y, yrhs)"], clarsimp) |
1050 from X_in_ES Y_in_ES and not_eq and Inv_ES |
1049 from X_in_ES Y_in_ES and not_eq and Inv_ES |
1051 show "(Y, yrhs) \<in> ES \<and> X \<noteq> Y" |
1050 show "(Y, yrhs) \<in> ES \<and> X \<noteq> Y" |
1052 by (auto simp: invariant_def distinct_equas_def) |
1051 by (auto simp: invariant_def distinct_equas_def) |
1053 next |
1052 next |
1054 fix x |
1053 fix x |