diff --git a/thys/First_Order_Clause/Typed_Tiebreakers.thy b/thys/First_Order_Clause/Typed_Tiebreakers.thy index b1a333d9a68522e71b3c9cfabe97b8cccf8b648c_dGh5cy9GaXJzdF9PcmRlcl9DbGF1c2UvVHlwZWRfVGllYnJlYWtlcnMudGh5..59c3a4dddc8b2edde390137e4053366cb11c5367_dGh5cy9GaXJzdF9PcmRlcl9DbGF1c2UvVHlwZWRfVGllYnJlYWtlcnMudGh5 100644 --- a/thys/First_Order_Clause/Typed_Tiebreakers.thy +++ b/thys/First_Order_Clause/Typed_Tiebreakers.thy @@ -9,6 +9,8 @@ locale typed_tiebreakers = fixes tiebreakers :: "('f, 'v) tiebreakers" - assumes tiebreakers: "\<And>C\<^sub>G. wellfounded_strict_order (tiebreakers C\<^sub>G)" + assumes + wfp_tiebreakers: "\<And>C\<^sub>G. wfp (tiebreakers C\<^sub>G)" and + transp_tiebreakers: "\<And>C\<^sub>G. transp (tiebreakers C\<^sub>G)" begin @@ -13,9 +15,6 @@ begin -sublocale tiebreakers: wellfounded_strict_order "tiebreakers C\<^sub>G" - by (rule tiebreakers) - abbreviation typed_tiebreakers :: "'f gatom clause \<Rightarrow> ('f, 'v, 'ty) typed_clause \<Rightarrow> ('f, 'v, 'ty) typed_clause \<Rightarrow> bool" where "typed_tiebreakers C\<^sub>G C\<^sub>1 C\<^sub>2 \<equiv> tiebreakers C\<^sub>G (fst C\<^sub>1) (fst C\<^sub>2)" @@ -18,13 +17,9 @@ abbreviation typed_tiebreakers :: "'f gatom clause \<Rightarrow> ('f, 'v, 'ty) typed_clause \<Rightarrow> ('f, 'v, 'ty) typed_clause \<Rightarrow> bool" where "typed_tiebreakers C\<^sub>G C\<^sub>1 C\<^sub>2 \<equiv> tiebreakers C\<^sub>G (fst C\<^sub>1) (fst C\<^sub>2)" -sublocale typed_tiebreakers: wellfounded_strict_order "typed_tiebreakers C\<^sub>G" -proof unfold_locales - - show "transp (typed_tiebreakers C\<^sub>G)" - using tiebreakers.transp - unfolding transp_def - by blast -next +lemma transp_typed_tiebreakers[iff]: "transp (typed_tiebreakers C\<^sub>G)" + using transp_tiebreakers + unfolding transp_def + by blast @@ -30,9 +25,4 @@ - show "asymp (typed_tiebreakers C\<^sub>G)" - using tiebreakers.asymp - by (meson asympD asympI) -next - - show "wfp (typed_tiebreakers C\<^sub>G)" - using tiebreakers.wfp +lemma wfp_typed_tiebreakers[iff]: "wfp (typed_tiebreakers C\<^sub>G)" + using wfp_tiebreakers by (meson wfp_if_convertible_to_wfp) @@ -38,5 +28,4 @@ by (meson wfp_if_convertible_to_wfp) -qed end diff --git a/thys/Superposition_Calculus/Grounded_Superposition.thy b/thys/Superposition_Calculus/Grounded_Superposition.thy index b1a333d9a68522e71b3c9cfabe97b8cccf8b648c_dGh5cy9TdXBlcnBvc2l0aW9uX0NhbGN1bHVzL0dyb3VuZGVkX1N1cGVycG9zaXRpb24udGh5..59c3a4dddc8b2edde390137e4053366cb11c5367_dGh5cy9TdXBlcnBvc2l0aW9uX0NhbGN1bHVzL0dyb3VuZGVkX1N1cGVycG9zaXRpb24udGh5 100644 --- a/thys/Superposition_Calculus/Grounded_Superposition.thy +++ b/thys/Superposition_Calculus/Grounded_Superposition.thy @@ -129,7 +129,7 @@ clause.welltyped_ground_instances "Some \<circ> inference_ground_instances" typed_tiebreakers -proof(unfold_locales; (intro impI typed_tiebreakers.wfp typed_tiebreakers.transp)?) +proof(unfold_locales; (intro impI wfp_typed_tiebreakers transp_typed_tiebreakers)?) show "\<bottom>\<^sub>F \<noteq> {}" using obtain_infinite_variables_per_type_on''[of "{}"] diff --git a/thys/Superposition_Calculus/Grounded_Untyped_Superposition.thy b/thys/Superposition_Calculus/Grounded_Untyped_Superposition.thy index b1a333d9a68522e71b3c9cfabe97b8cccf8b648c_dGh5cy9TdXBlcnBvc2l0aW9uX0NhbGN1bHVzL0dyb3VuZGVkX1VudHlwZWRfU3VwZXJwb3NpdGlvbi50aHk=..59c3a4dddc8b2edde390137e4053366cb11c5367_dGh5cy9TdXBlcnBvc2l0aW9uX0NhbGN1bHVzL0dyb3VuZGVkX1VudHlwZWRfU3VwZXJwb3NpdGlvbi50aHk= 100644 --- a/thys/Superposition_Calculus/Grounded_Untyped_Superposition.thy +++ b/thys/Superposition_Calculus/Grounded_Untyped_Superposition.thy @@ -9,7 +9,7 @@ proof unfold_locales show "\<And>\<tau>. \<exists>f. (replicate 0 (), ()) = ([], \<tau>)" by simp -qed +qed simp_all lemma all_welltyped [intro]: "typed.welltyped \<V> t ()" proof (induction t) diff --git a/thys/Superposition_Calculus/Superposition.thy b/thys/Superposition_Calculus/Superposition.thy index b1a333d9a68522e71b3c9cfabe97b8cccf8b648c_dGh5cy9TdXBlcnBvc2l0aW9uX0NhbGN1bHVzL1N1cGVycG9zaXRpb24udGh5..59c3a4dddc8b2edde390137e4053366cb11c5367_dGh5cy9TdXBlcnBvc2l0aW9uX0NhbGN1bHVzL1N1cGVycG9zaXRpb24udGh5 100644 --- a/thys/Superposition_Calculus/Superposition.thy +++ b/thys/Superposition_Calculus/Superposition.thy @@ -16,9 +16,8 @@ nonground_inhabited_typing \<F> + nonground_equality_order less\<^sub>t + nonground_selection_function select + - typed_tiebreakers tiebreakers + ground_critical_pair_theorem "TYPE('f)" for select :: "('f, 'v :: infinite) select" and less\<^sub>t :: "('f, 'v) term \<Rightarrow> ('f, 'v) term \<Rightarrow> bool" and \<F> :: "('f, 'ty) fun_types" and @@ -20,8 +19,11 @@ ground_critical_pair_theorem "TYPE('f)" for select :: "('f, 'v :: infinite) select" and less\<^sub>t :: "('f, 'v) term \<Rightarrow> ('f, 'v) term \<Rightarrow> bool" and \<F> :: "('f, 'ty) fun_types" and - tiebreakers :: "('f, 'v) tiebreakers" + tiebreakers :: "('f, 'v) tiebreakers" + + assumes + wfp_tiebreakers[iff]: "\<And>C\<^sub>G. wfp (tiebreakers C\<^sub>G)" and + transp_tiebreakers[iff]: "\<And>C\<^sub>G. transp (tiebreakers C\<^sub>G)" begin @@ -26,5 +28,8 @@ begin +sublocale typed_tiebreakers tiebreakers + by unfold_locales simp_all + interpretation term_order_notation. inductive eq_resolution :: "('f, 'v, 'ty) typed_clause \<Rightarrow> ('f, 'v, 'ty) typed_clause \<Rightarrow> bool" where diff --git a/thys/Superposition_Calculus/Superposition_Example.thy b/thys/Superposition_Calculus/Superposition_Example.thy index b1a333d9a68522e71b3c9cfabe97b8cccf8b648c_dGh5cy9TdXBlcnBvc2l0aW9uX0NhbGN1bHVzL1N1cGVycG9zaXRpb25fRXhhbXBsZS50aHk=..59c3a4dddc8b2edde390137e4053366cb11c5367_dGh5cy9TdXBlcnBvc2l0aW9uX0NhbGN1bHVzL1N1cGVycG9zaXRpb25fRXhhbXBsZS50aHk= 100644 --- a/thys/Superposition_Calculus/Superposition_Example.thy +++ b/thys/Superposition_Calculus/Superposition_Example.thy @@ -5,6 +5,15 @@ VeriComp.Well_founded begin +lemma asymp_bot[iff]: "asymp \<bottom>" + by (simp add: asymp_on_def) + +lemma transp_bot[iff]: "transp \<bottom>" + by (simp add: transp_def) + +lemma wfp_bot[iff]: "wfp \<bottom>" + by (simp add: wfp_def) + sublocale nonground_term_with_context \<subseteq> nonground_term_order "less_kbo :: ('f :: weighted,'v) term \<Rightarrow> ('f,'v) term \<Rightarrow> bool" proof unfold_locales @@ -55,10 +64,7 @@ (* TODO: use strictly_generalizes *) abbreviation trivial_tiebreakers :: "'f gatom clause \<Rightarrow> ('f,'v) atom clause \<Rightarrow> ('f,'v) atom clause \<Rightarrow> bool" where - "trivial_tiebreakers _ _ _ \<equiv> False" - -lemma trivial_tiebreakers: "wellfounded_strict_order (trivial_tiebreakers C\<^sub>G)" - by unfold_locales auto + "trivial_tiebreakers \<equiv> \<bottom>" (* TODO: We have to get the ground_critical_pair_theorem into the afp *) locale trivial_superposition_example = @@ -200,9 +206,6 @@ ground_critical_pair_theorem "TYPE(nat)" begin -sublocale wellfounded_strict_order "trivial_tiebreakers C\<^sub>G" - using trivial_tiebreakers . - sublocale nonground_term_with_context . sublocale nonground_equality_order less_kbo @@ -218,7 +221,7 @@ fix \<tau> show "\<exists>f. types f 0 = ([], \<tau>)" using types_inhabited . -qed +qed simp_all end diff --git a/thys/Superposition_Calculus/Untyped_Superposition.thy b/thys/Superposition_Calculus/Untyped_Superposition.thy index b1a333d9a68522e71b3c9cfabe97b8cccf8b648c_dGh5cy9TdXBlcnBvc2l0aW9uX0NhbGN1bHVzL1VudHlwZWRfU3VwZXJwb3NpdGlvbi50aHk=..59c3a4dddc8b2edde390137e4053366cb11c5367_dGh5cy9TdXBlcnBvc2l0aW9uX0NhbGN1bHVzL1VudHlwZWRfU3VwZXJwb3NpdGlvbi50aHk= 100644 --- a/thys/Superposition_Calculus/Untyped_Superposition.thy +++ b/thys/Superposition_Calculus/Untyped_Superposition.thy @@ -5,8 +5,7 @@ locale untyped_superposition_calculus = nonground_equality_order less\<^sub>t + nonground_selection_function select + - typed_tiebreakers tiebreakers + ground_critical_pair_theorem "TYPE('f)" for select :: "('f, 'v :: infinite) select" and less\<^sub>t :: "('f, 'v) term \<Rightarrow> ('f, 'v) term \<Rightarrow> bool" and @@ -9,8 +8,11 @@ ground_critical_pair_theorem "TYPE('f)" for select :: "('f, 'v :: infinite) select" and less\<^sub>t :: "('f, 'v) term \<Rightarrow> ('f, 'v) term \<Rightarrow> bool" and - tiebreakers :: "('f, 'v) tiebreakers" + tiebreakers :: "('f, 'v) tiebreakers" + + assumes + wfp_tiebreakers[iff]: "\<And>C\<^sub>G. wfp (tiebreakers C\<^sub>G)" and + transp_tiebreakers[iff]: "\<And>C\<^sub>G. transp (tiebreakers C\<^sub>G)" begin interpretation term_order_notation.