diff --git a/thys/Lambda_Free_EPO/Lambda_Free_EPO.thy b/thys/Lambda_Free_EPO/Lambda_Free_EPO.thy --- a/thys/Lambda_Free_EPO/Lambda_Free_EPO.thy +++ b/thys/Lambda_Free_EPO/Lambda_Free_EPO.thy @@ -1,1232 +1,1232 @@ (* Title: The Embedding Path Order for Lambda-Free Higher-Order Terms Author: Alexander Bentkamp , 2018 Maintainer: Alexander Bentkamp *) section \The Embedding Path Order for Lambda-Free Higher-Order Terms\ theory Lambda_Free_EPO -imports Chop +imports Chop Nested_Multisets_Ordinals.Multiset_More abbrevs ">t" = ">\<^sub>t" and "\t" = "\\<^sub>t" begin text \ This theory defines the embedding path order for \\\-free higher-order terms. \ subsection \Setup\ locale epo = ground_heads "(>\<^sub>s)" arity_sym arity_var for gt_sym :: "'s \ 's \ bool" (infix ">\<^sub>s" 50) and arity_sym :: "'s \ enat" and arity_var :: "'v \ enat" + fixes extf :: "'s \ (('s, 'v) tm \ ('s, 'v) tm \ bool) \ ('s, 'v) tm list \ ('s, 'v) tm list \ bool" assumes extf_ext_trans_before_irrefl: "ext_trans_before_irrefl (extf f)" and extf_ext_compat_list: "ext_compat_list (extf f)" assumes extf_ext_compat_snoc: "ext_compat_snoc (extf f)" assumes extf_ext_compat_cons: "ext_compat_cons (extf f)" assumes extf_ext_snoc: "ext_snoc (extf f)" assumes extf_min_empty: "\ extf f gt [] ss" (* TODO: seperate definition? *) begin lemma extf_ext_trans: "ext_trans (extf f)" by (rule ext_trans_before_irrefl.axioms(1)[OF extf_ext_trans_before_irrefl]) lemma extf_ext: "ext (extf f)" by (rule ext_trans.axioms(1)[OF extf_ext_trans]) lemmas extf_mono_strong = ext.mono_strong[OF extf_ext] lemmas extf_mono = ext.mono[OF extf_ext, mono] lemmas extf_map = ext.map[OF extf_ext] lemmas extf_trans = ext_trans.trans[OF extf_ext_trans] lemmas extf_irrefl_from_trans = ext_trans_before_irrefl.irrefl_from_trans[OF extf_ext_trans_before_irrefl] lemmas extf_compat_list = ext_compat_list.compat_list[OF extf_ext_compat_list] lemmas extf_snoc = ext_snoc.snoc[OF extf_ext_snoc] lemmas extf_compat_append_right = ext_compat_snoc.compat_append_right[OF extf_ext_compat_snoc] lemmas extf_compat_append_left = ext_compat_cons.compat_append_left[OF extf_ext_compat_cons] lemma extf_ext_insert_arg: "extf f gt (xs @ z # ys) (xs @ ys)" using extf_compat_append_left extf_compat_append_right extf_snoc[of f gt Nil z] by fastforce subsection \Inductive Definitions\ definition chkchop :: "(('s, 'v) tm \ ('s, 'v) tm \ bool) \ ('s, 'v) tm \ ('s, 'v) tm \ bool" where [simp]: "chkchop gt t s \ is_Hd s \ gt t (chop s)" definition chkchop_same :: "(('s, 'v) tm \ ('s, 'v) tm \ bool) \ ('s, 'v) tm \ ('s, 'v) tm \ bool" where [simp]: "chkchop_same gt t s \ (if is_Var (head t) then is_Hd t \ chkchop gt (chop t) s else chkchop gt t s)" lemma chkchop_mono[mono]: "gt \ gt' \ chkchop gt \ chkchop gt'" using chkchop_def by blast lemma chkchop_same_mono[mono]: "gt \ gt' \ chkchop_same gt \ chkchop_same gt'" using chkchop_same_def by fastforce inductive gt :: "('s, 'v) tm \ ('s, 'v) tm \ bool" (infix ">\<^sub>t" 50) where gt_chop: "is_App t \ chop t >\<^sub>t s \ chop t = s \ t >\<^sub>t s" | gt_diff: "head t >\<^sub>h\<^sub>d head s \ is_Sym (head s) \ chkchop (>\<^sub>t) t s \ t >\<^sub>t s" | gt_same: "head t = head s \ chkchop_same (>\<^sub>t) t s \ (\f \ ground_heads (head t). extf f (>\<^sub>t) (args t) (args s)) \ t >\<^sub>t s" abbreviation ge :: "('s, 'v) tm \ ('s, 'v) tm \ bool" (infix "\\<^sub>t" 50) where "t \\<^sub>t s \ t >\<^sub>t s \ t = s" inductive gt_chop :: "('s, 'v) tm \ ('s, 'v) tm \ bool" where gt_chopI: "is_App t \ chop t \\<^sub>t s \ gt_chop t s" inductive gt_diff :: "('s, 'v) tm \ ('s, 'v) tm \ bool" where gt_diffI: "head t >\<^sub>h\<^sub>d head s \ is_Sym (head s) \ chkchop (>\<^sub>t) t s \ gt_diff t s" inductive gt_same :: "('s, 'v) tm \ ('s, 'v) tm \ bool" where gt_sameI: "head t = head s \ chkchop_same (>\<^sub>t) t s \ (\f \ ground_heads (head t). extf f (>\<^sub>t) (args t) (args s)) \ gt_same t s" lemma gt_iff_chop_diff_same: "t >\<^sub>t s \ gt_chop t s \ gt_diff t s \ gt_same t s" by (subst gt.simps) (auto simp: gt_chop.simps gt_diff.simps gt_same.simps) subsection \Transitivity\ lemma t_gt_chop_t: "is_App t \ t >\<^sub>t chop t" by (simp add: gt_chop) lemma gt_imp_vars: "t >\<^sub>t s \ vars t \ vars s" proof (simp only: atomize_imp, rule measure_induct_rule[of "\(t, s). hsize t + hsize s" "\(t, s). t >\<^sub>t s \ vars t \ vars s" "(t, s)", simplified prod.case], simp only: split_paired_all prod.case atomize_imp[symmetric]) fix t s assume ih: "\ta sa. hsize ta + hsize sa < hsize t + hsize s \ ta >\<^sub>t sa \ vars ta \ vars sa" and t_gt_s: "t >\<^sub>t s" show "vars t \ vars s" using t_gt_s proof cases case (gt_chop) thus ?thesis using ih by (metis add_mono_thms_linordered_field(1) le_supI1 order_refl hsize_chop_lt vars_chop) next case gt_diff show ?thesis proof (cases s) case Hd thus ?thesis using gt_diff(2) by (metis empty_iff hd.collapse(2) hd.simps(18) subsetI tm.sel(1) tm.simps(17)) next case (App s1 s2) have "vars (chop s) \ vars t" using ih using App chkchop_def local.gt_diff(3) nat_add_left_cancel_less hsize_chop_lt tm.disc(2) by blast thus ?thesis using App le_sup_iff local.gt_diff(2) tm.disc(2) vars_chop by (metis empty_iff hd.collapse(2) hd.simps(18) subsetI) qed next case gt_same thus ?thesis proof (cases "head t") case (Var x) then show ?thesis proof (cases t) case (Hd _) then show ?thesis using gt_same extf_min_empty[of _ "(>\<^sub>t)" "args s"] by simp next case (App t1 t2) then show ?thesis proof (cases s) case (Hd _) then show ?thesis using local.gt_same(1) vars_head_subseteq by fastforce next case (App s1 s2) then have "chop t >\<^sub>t chop s" by (metis Var args.simps(1) chkchop_def chkchop_same_def epo.extf_min_empty epo_axioms gt_hd_def gt_hd_irrefl hd.disc(1) local.gt_same(2) local.gt_same(3) tm.collapse(1) tm.disc(2)) then have "vars (chop s) \ vars (chop t)" using ih[OF _ \chop t >\<^sub>t chop s\] by (metis App add_mono_thms_linordered_field(5) args_Nil_iff_is_Hd extf_min_empty gt_hd_def gt_hd_irrefl local.gt_same(3) hsize_chop_lt tm.disc(2)) then show ?thesis using gt_same(1) vars_chop[of t] vars_chop[of s] by (metis App args_Nil_iff_is_Hd extf_min_empty gt_hd_def gt_hd_irrefl le_sup_iff local.gt_same(3) order_refl sup.coboundedI1 tm.disc(2)) qed qed next case (Sym f) then have "chkchop (>\<^sub>t) t s" using gt_same chkchop_same_def by auto then show ?thesis proof (cases s) case (Hd _) then show ?thesis using local.gt_same(1) vars_head_subseteq by force next case (App s1 s2) then show ?thesis unfolding chkchop_def using vars_chop ih[of t "chop s"] by (metis \chkchop (>\<^sub>t) t s\ chkchop_def le_sup_iff local.gt_same(1) nat_add_left_cancel_less hsize_chop_lt tm.disc(2) vars_head_subseteq) qed qed qed qed lemma gt_trans: "u >\<^sub>t t \ t >\<^sub>t s \ u >\<^sub>t s" proof (simp only: atomize_imp, rule measure_induct_rule[of "\(u, t, s). {#hsize u, hsize t, hsize s#}" "\(u, t, s). u >\<^sub>t t \ t >\<^sub>t s \ u >\<^sub>t s" "(u, t, s)", simplified prod.case], simp only: split_paired_all prod.case atomize_imp[symmetric]) fix u t s assume ih: "\ua ta sa. {#hsize ua, hsize ta, hsize sa#} < {#hsize u, hsize t, hsize s#} \ ua >\<^sub>t ta \ ta >\<^sub>t sa \ ua >\<^sub>t sa" and u_gt_t: "u >\<^sub>t t" and t_gt_s: "t >\<^sub>t s" have u_gt_s_if_ui: "chop u \\<^sub>t t \ u >\<^sub>t s" if ui_in: "is_App u" using ih[of "chop u" t s, simplified] t_gt_s gt_chop hsize_chop_lt ui_in by blast show "u >\<^sub>t s" using t_gt_s proof cases case gt_chop have u_gt_s_if_chk_u_t: ?thesis if chk_u_t: "chkchop (>\<^sub>t) u t" using ih[of u "chop u" s] gt_chop chk_u_t by (metis add_mset_lt_left_lt add_mset_lt_right_lt chkchop_def ih hsize_chop_lt) show ?thesis by (metis args_Nil_iff_is_Hd chkchop_def chkchop_same_def epo.extf_min_empty epo_axioms gt.simps gt_hd_def gt_hd_irrefl u_gt_s_if_chk_u_t u_gt_s_if_ui u_gt_t) next case gt_diff_t_s: gt_diff show ?thesis using u_gt_t proof cases case gt_chop then show ?thesis using u_gt_s_if_ui by blast next case gt_diff_u_t: gt_diff have "head u >\<^sub>h\<^sub>d head s" using gt_diff_u_t(1) gt_diff_t_s(1) by (auto intro: gt_hd_trans) thus ?thesis using add_mset_lt_left_lt add_mset_lt_right_lt chkchop_def gt_diff gt_diff_t_s(3) ih hsize_chop_lt u_gt_t by (metis gt_diff_t_s(2)) next case gt_same_u_t: gt_same have "head u >\<^sub>h\<^sub>d head s" using gt_diff_t_s(1) gt_same_u_t(1) by auto thus ?thesis using add_mset_lt_left_lt add_mset_lt_right_lt chkchop_def gt_diff gt_diff_t_s(3) ih hsize_chop_lt u_gt_t by (metis gt_diff_t_s(2)) qed next case gt_same_t_s: gt_same show ?thesis using u_gt_t proof cases case gt_chop then show ?thesis using u_gt_s_if_ui by linarith next case gt_diff_u_t: gt_diff have "head u >\<^sub>h\<^sub>d head s" using gt_diff_u_t(1) gt_same_t_s(1) by simp thus ?thesis using add_mset_lt_left_lt add_mset_lt_right_lt chkchop_def gt_diff gt_same_t_s ih hsize_chop_lt u_gt_t by (metis chkchop_same_def gt_diff_u_t(2)) next case gt_same_u_t: gt_same have hd_u_s: "head u = head s" using gt_same_u_t(1) gt_same_t_s(1) by simp let ?S = "set (args u) \ set (args t) \ set (args s)" have gt_trans_args: "\ua \ ?S. \ta \ ?S. \sa \ ?S. ua >\<^sub>t ta \ ta >\<^sub>t sa \ ua >\<^sub>t sa" proof clarify fix sa ta ua assume ua_in: "ua \ ?S" and ta_in: "ta \ ?S" and sa_in: "sa \ ?S" and ua_gt_ta: "ua >\<^sub>t ta" and ta_gt_sa: "ta >\<^sub>t sa" show "ua >\<^sub>t sa" by (auto intro!: ih[OF Max_lt_imp_lt_mset ua_gt_ta ta_gt_sa]) (meson ua_in ta_in sa_in Un_iff max.strict_coboundedI1 max.strict_coboundedI2 hsize_in_args)+ qed have "\f \ ground_heads (head u). extf f (>\<^sub>t) (args u) (args s)" proof (clarify, rule extf_trans[OF _ _ _ gt_trans_args]) fix f assume f_in_grounds: "f \ ground_heads (head u)" show "extf f (>\<^sub>t) (args u) (args t)" using f_in_grounds gt_same_u_t(3) by blast show "extf f (>\<^sub>t) (args t) (args s)" using f_in_grounds gt_same_t_s(3) unfolding gt_same_u_t(1) by blast qed auto have "chkchop_same (>\<^sub>t) u s" proof (cases "head u") case (Var x) then show ?thesis proof (cases u) case (Hd _) then show ?thesis using Var by auto next case (App u1 u2) then have "chop u >\<^sub>t chop t" by (metis Var args.simps(1) chkchop_def chkchop_same_def epo.extf_min_empty epo_axioms gt_hd_def gt_hd_irrefl gt_same_t_s(3) gt_same_u_t(2) hd.disc(1) tm.collapse(1) tm.disc(2)) then show ?thesis proof (cases t) case (Hd _) then show ?thesis using extf_min_empty gt_same_t_s(3) by auto next case t_App: (App t1 t2) then have "is_App s \ chop t >\<^sub>t chop s" using gt_same_t_s unfolding chkchop_same_def unfolding chkchop_def using Var hd_u_s by auto then have "chkchop (>\<^sub>t) (chop u) s" unfolding chkchop_def using ih[of "chop u" "chop t" "chop s"] by (metis App \chop u >\<^sub>t chop t\ t_App add_mset_lt_lt_le less_imp_le mset_lt_single_iff hsize_chop_lt tm.disc(2)) then show ?thesis unfolding chkchop_same_def using Var by auto qed qed next case (Sym f) have "chkchop (>\<^sub>t) u s" proof (cases s) case (Hd _) then show ?thesis by simp next case (App s1 s2) then have "t >\<^sub>t chop s" using Sym gt_same_t_s(1) gt_same_t_s(2) hd_u_s by auto then have "u >\<^sub>t chop s" using ih[of u t "chop s"] by (metis App add_mset_lt_right_lt mset_lt_single_iff hsize_chop_lt tm.disc(2) u_gt_t) then show ?thesis unfolding chkchop_def by blast qed then show ?thesis by (simp add: Sym) qed thus ?thesis using \\f\local.ground_heads (head u). extf f (>\<^sub>t) (args u) (args s)\ gt_same hd_u_s by blast qed qed qed subsection \Irreflexivity\ theorem gt_irrefl: "\ s >\<^sub>t s" proof (standard, induct s rule: measure_induct_rule[of hsize]) case (less s) note ih = this(1) and s_gt_s = this(2) show False using s_gt_s proof cases case gt_chop then show False using ih[of "chop s"] by (metis gt.gt_chop gt_trans hsize_chop_lt) next case gt_diff thus False by (cases "head s") (auto simp: gt_hd_irrefl) next case gt_same note in_grounds = this(3) obtain si where si_in_args: "si \ set (args s)" and si_gt_si: "si >\<^sub>t si" using in_grounds by (metis (full_types) all_not_in_conv extf_irrefl_from_trans ground_heads_nonempty gt_trans) have "hsize si < hsize s" by (rule hsize_in_args[OF si_in_args]) thus False by (rule ih[OF _ si_gt_si]) qed qed lemma gt_antisym: "t >\<^sub>t s \ \ s >\<^sub>t t" using gt_irrefl gt_trans by blast subsection "Compatibility with Embedding Relation" (* TODO: move? *) lemma nth_drop_lemma: assumes "length xs = length ys" and "k \ length xs" and "\i. i < length xs \ i \ k \ xs ! i = ys ! i" shows "drop k xs = drop k ys" using assms proof (induct arbitrary:k rule:list_induct2) case Nil then show ?case by simp next case (Cons x xs y ys) then show ?case proof (cases k) case 0 then have "x # xs = y # ys" by (metis Cons.hyps(1) Cons.prems(2) leI length_Cons not_less_zero nth_equalityI) then show ?thesis by blast next case (Suc m) then have "drop m xs = drop m ys" by (metis Cons.hyps(2) Cons.prems(1) Cons.prems(2) Suc_le_mono Suc_mono length_Cons nth_Cons_Suc) then show ?thesis by (simp add: Suc) qed qed lemma gt_embedding_step_property: assumes "t \\<^sub>e\<^sub>m\<^sub>b s" shows "t >\<^sub>t s" using assms apply(simp only: atomize_imp) apply (rule measure_induct_rule[of "\(t, s). hsize t + hsize s" "\(t, s). t \\<^sub>e\<^sub>m\<^sub>b s \ t >\<^sub>t s" "(t, s)", simplified prod.case]) proof(simp only: split_paired_all prod.case atomize_imp[symmetric]) fix s t :: "('s,'v) tm" assume "t \\<^sub>e\<^sub>m\<^sub>b s" and ih: "\tt ss. hsize tt + hsize ss < hsize t + hsize s \ tt \\<^sub>e\<^sub>m\<^sub>b ss \ tt >\<^sub>t ss" have "is_App t" by (metis \t \\<^sub>e\<^sub>m\<^sub>b s\ emb_step_at_is_App emb_step_equiv) obtain p d where "emb_step_at p d t = s" "position_of t (p @ [d])" using \t \\<^sub>e\<^sub>m\<^sub>b s\ emb_step_equiv by (metis position_if_emb_step_at) define q where q_rep_t: "q = replicate (num_args (fun t)) Left" show "t >\<^sub>t s" proof (cases "list_all (\x. x = Left) p") case True show ?thesis proof (cases d) text \Embedding removes an argument i\ case Left define i where "i = num_args t - Suc (length p)" then have " head t = head s" "i < num_args t" "args s = take i (args t) @ drop (Suc i) (args t)" using emb_step_at_remove_arg Left True \emb_step_at p d t = s\ \position_of t (p @ [d])\ by metis+ have "is_App s \ chop t \\<^sub>e\<^sub>m\<^sub>b chop s" proof (cases "p = q") case True assume "is_App s" show ?thesis proof - have "Suc (num_args (fun s)) = num_args (fun t)" by (metis One_nat_def Suc_num_args True \args s = take i (args t) @ drop (Suc i) (args t)\ \is_App s\ \is_App t\ append_self_conv2 cancel_comm_monoid_add_class.diff_cancel diff_Suc_1 i_def length_drop length_replicate q_rep_t take_eq_Nil) have "emb_step_at (replicate (num_args (fun s)) Left) Right (chop t) = emb_step_at (replicate (num_args (fun s)) Left) Right t" using merge_emb_step_at[of "replicate (num_args (fun s)) Left" Right Nil Right t, unfolded append_Nil2 opp_simps(1) replicate_append_same] by (metis \Suc (num_args (fun s)) = num_args (fun t)\ \is_App t\ chop_emb_step_at replicate_Suc) then have "emb_step_at (replicate (num_args (fun s)) dir.Left) dir.Right (chop t) = chop s" unfolding chop_emb_step_at[OF \is_App s\] using merge_emb_step_at[of "replicate (num_args (fun s)) Left" Right Nil Left t, unfolded append_Nil2 opp_simps(1) replicate_append_same] by (metis Left True \Suc (num_args (fun s)) = num_args (fun t)\ \emb_step_at p d t = s\ q_rep_t replicate_Suc) then show "chop t \\<^sub>e\<^sub>m\<^sub>b chop s" by (metis \is_App s\ \is_App t\ \t \\<^sub>e\<^sub>m\<^sub>b s\ emb_step_equiv emb_step_hsize nat_neq_iff hsize_chop) qed next case False assume "is_App s" have p_rep: "p = replicate (length p) Left" by (metis (full_types) \list_all (\x. x = Left) p\ list_all_iff replicate_length_same) have length_p:"length p < num_args t" using no_position_replicate_num_args \position_of t (p @ [d])\ replicate_add[of "num_args t" "length p - num_args t" Left] p_rep q_rep_t by (metis Left add_diff_inverse_nat replicate_app_Cons_same replicate_append_same shallower_pos) then have "length p \ length q" using Suc_num_args \is_App t\ q_rep_t by fastforce then have "length p < length q" using False le_neq_implies_less p_rep q_rep_t by fastforce then have "take (Suc (length p)) q = p @ [Left]" by (metis (no_types, lifting) \length p \ length q\ length_replicate min.orderE nth_replicate p_rep q_rep_t take_Suc_conv_app_nth take_replicate) then obtain q' where "q = p @ [Left] @ q'" by (metis append.assoc append_take_drop_id) have "Suc (num_args (fun s)) = num_args (fun t)" by (metis (no_types, lifting) Cons_nth_drop_Suc Suc_num_args \args s = take i (args t) @ drop (Suc i) (args t)\ \i < num_args t\ \is_App s\ \is_App t\ add_Suc_right append_take_drop_id diff_Suc_1 length_Cons length_append) then have "chop s = emb_step_at p dir.Left (chop t)" using swap_nested_emb_step_at[of p q' Right Left t] chop_emb_step_at[OF \is_App s\] chop_emb_step_at[OF \is_App t\] by (metis (no_types, lifting) Cons_replicate_eq Left \emb_step_at p d t = s\ \q = p @ [dir.Left] @ q'\ append.assoc append_Cons diff_Suc_1 p_rep q_rep_t replicate_append_same) then show "chop t \\<^sub>e\<^sub>m\<^sub>b chop s" by (metis Left \is_App t\ \position_of t (p @ [d])\ \q = p @ [dir.Left] @ q'\ chop_emb_step_at emb_step_at_if_position pos_emb_step_at_nested q_rep_t) qed then have "chkchop_same (>\<^sub>t) t s" proof (cases "is_Var (head t)") case True then show ?thesis unfolding chkchop_same_def chkchop_def using ih[of "chop t" "chop s"] add_less_mono hsize_chop_lt \is_App s \ chop t \\<^sub>e\<^sub>m\<^sub>b chop s\ by metis next case False then show ?thesis unfolding chkchop_same_def chkchop_def using \is_App t\ add_less_mono gt_chop ih hsize_chop_lt \is_App s \ chop t \\<^sub>e\<^sub>m\<^sub>b chop s\ by metis qed have "\f\local.ground_heads (head t). extf f (>\<^sub>t) (args t) (args s)" using extf_ext_insert_arg[of _ _ "take i (args t)" "args t ! i" "drop (Suc i) (args t)"] using \args s = take i (args t) @ drop (Suc i) (args t)\ \i < num_args t\ id_take_nth_drop by fastforce then show ?thesis using gt_same \head t = head s\ \chkchop_same (>\<^sub>t) t s\ by blast next text \Embedding chops and might remove arguments from the left\ case Right show ?thesis using emb_step_at_chop by (metis Right True \emb_step_at p d t = s\ \is_App t\ \position_of t (p @ [d])\ add_Suc gt_chop ih less_Suc_eq hsize_chop) qed next text \Embedding operates under one of the arguments\ case False have "num_args t = num_args s" using emb_step_under_args_num_args[OF False] by (metis (no_types) \\t d. num_args (emb_step_at p d t) = num_args t\ \emb_step_at p d t = s\) then have "is_App s" using \num_args t = num_args s\ by (metis args_Nil_iff_is_Hd length_0_conv \is_App t\) have q_rep_s: "q = replicate (num_args (fun s)) Left" by (metis q_rep_t \is_App s\ \is_App t\ \num_args t = num_args s\ args.simps(2) butlast_snoc length_butlast tm.collapse(2)) have "chop t \\<^sub>e\<^sub>m\<^sub>b chop s" proof (cases "take (num_args (fun t)) p = q") case True have "num_args (fun t) < length p" proof (rule ccontr) assume "\ num_args (fun t) < length p" then have "num_args (fun t) = length p" "q = p" using True q_rep_t by auto then show False using False using list_all_length q_rep_t by fastforce qed have "p ! (num_args (fun t)) = Right" proof (rule ccontr) assume "p ! num_args (fun t) \ Right" then have "p ! num_args (fun t) = Left" using dir.exhaust by blast then have "take (num_args t) p = replicate (num_args t) Left" using True Suc_num_args[OF \is_App t\] q_rep_t take_Suc_conv_app_nth[of "num_args (fun t)" p] by (metis \num_args (fun t) < length p\ replicate_Suc replicate_append_same) then show False by (metis \num_args t = num_args s\ \num_args t = num_args s\ \position_of t (p @ [d])\ append.assoc append_eq_Cons_conv append_take_drop_id no_position_replicate_num_args shallower_pos) qed then obtain q' where "p = q @ [Right] @ q'" by (metis Cons_nth_drop_Suc True \num_args (fun t) < length p\ append_Cons append_Nil append_eq_conv_conj length_replicate q_rep_t) have "emb_step_at (q @ q') d (chop t) = chop s" unfolding chop_emb_step_at[OF \is_App t\] chop_emb_step_at[OF \is_App s\] using swap_nested_emb_step_at[of q q' d Right t, unfolded] \emb_step_at p d t = s\ \p = q @ [Right] @ q'\ q_rep_t q_rep_s by auto moreover have "chop t \ chop s" by (metis \is_App s\ \is_App t\ \t \\<^sub>e\<^sub>m\<^sub>b s\ emb_step_hsize nat_less_le hsize_chop) ultimately show "chop t \\<^sub>e\<^sub>m\<^sub>b chop s" using emb_step_equiv by blast next case False then have takepq: "take (length q) p \ q" using q_rep_t by auto have takeqp: "length p \ length q \ take (length p) q \ p" using \\ list_all (\x. x = Left) p\[unfolded list_all_length] using diff_diff_cancel take_replicate length_replicate nth_replicate q_rep_s by metis have "chop s = emb_step_at p d (chop t)" using swap_disjunct_emb_step_at[of p q Right d t, OF takeqp takepq, unfolded \emb_step_at p d t = s\] using \is_App s\ \is_App t\ chop_emb_step_at q_rep_s q_rep_t by (simp add: chop_emb_step_at) then show ?thesis by (metis False \is_App t\ \position_of t (p @ [d])\ chop_emb_step_at emb_step_at_if_position length_replicate nat_le_linear pos_emb_step_at_disjunct q_rep_t take_all takeqp) qed then have gt1:"chkchop_same (>\<^sub>t) t s" proof (cases "head t") case (Var _) then have "chop t >\<^sub>t chop s" using ih[of "chop t" "chop s"] by (meson \chop t \\<^sub>e\<^sub>m\<^sub>b chop s\ \is_App s\ \is_App t\ add_strict_mono hsize_chop_lt) then show ?thesis unfolding chkchop_same_def by (simp add: Var) next case (Sym _) then show ?thesis unfolding chkchop_same_def using \chop t \\<^sub>e\<^sub>m\<^sub>b chop s\ \is_App t\ add_Suc add_Suc_shift chkchop_def gt_trans ih less_Suc_eq hsize_chop t_gt_chop_t by (metis (no_types, lifting)) qed have gt2:"head t = head s" by (metis emb_step_under_args_head False \emb_step_at p d t = s\) have gt3:"\f\local.ground_heads (head t). extf f (>\<^sub>t) (args t) (args s)" proof (rule ballI) fix f assume "f\local.ground_heads (head t)" obtain i where i_def: "i < num_args t" "args t ! i \\<^sub>e\<^sub>m\<^sub>b args (emb_step_at p d t) ! i" "\j. j < num_args t \ i \ j \ args t ! j = args (emb_step_at p d t) ! j" using emb_step_under_args_emb_step[of p t d] using False \position_of t (p @ [d])\ by blast have compat_list1: "args t ! i >\<^sub>t args s ! i" by (metis \num_args t = num_args s\ \emb_step_at p d t = s\ add_less_mono i_def(1) i_def(2) ih nth_mem hsize_in_args) have compat_list2: "args t ! i \ args s ! i" using emb_step_equiv i_def(2) \emb_step_at p d t = s\ by blast have argst:"args t = take i (args t) @ args t ! i # drop (Suc i) (args t)" by (simp add: Cons_nth_drop_Suc i_def(1)) have argss:"args s = take i (args t) @ args (emb_step_at p d t) ! i # drop (Suc i) (args t)" proof - have "take i (args t) = take i (args s)" apply (rule nth_take_lemma) using \num_args t = num_args s\ i_def(1) i_def(3)[unfolded \emb_step_at p d t = s\] by auto moreover have "drop (Suc i) (args t) = drop (Suc i) (args s)" apply (rule nth_drop_lemma) apply (simp add: \num_args t = num_args s\) apply (simp add: Suc_le_eq i_def(1)) using Suc_n_not_le_n \emb_step_at p d t = s\ i_def(3) by blast ultimately show ?thesis using \emb_step_at p d t = s\ \num_args t = num_args s\ i_def(1) id_take_nth_drop by auto qed show "extf f (>\<^sub>t) (args t) (args s)" using extf_compat_list[of "args t ! i" "args (emb_step_at p d t) ! i" gt f "take i (args t)" "drop (Suc i) (args t)"] using \emb_step_at p d t = s\ argss argst compat_list1 compat_list2 by force qed show ?thesis using gt_same using gt1 gt2 gt3 by blast qed qed lemma gt_embedding_property: assumes "t \\<^sub>e\<^sub>m\<^sub>b s" "t \ s" shows "t >\<^sub>t s" using assms proof (induction) case (refl t) then show ?case by simp next case (step t u s) then show ?case using gt_embedding_step_property gt_trans by blast qed subsection \Subterm Property\ theorem gt_proper_sub: "proper_sub s t \ t >\<^sub>t s" using gt_embedding_property sub_emb by blast lemma gt_emb_fun: "App s t >\<^sub>t s" and gt_emb_arg: "App s t >\<^sub>t t" by (simp_all add: gt_embedding_step_property left right) subsection \Compatibility with Contexts\ lemma gt_fun_imp: "fun t >\<^sub>t s \ t >\<^sub>t s" by (metis emb_step_fun gt_embedding_step_property gt_trans tm.disc(2) tm.exhaust_sel tm.sel(3)) lemma gt_arg_imp: "arg t >\<^sub>t s \ t >\<^sub>t s" by (metis emb_step_arg gt_embedding_step_property gt_trans tm.disc(2) tm.exhaust_sel tm.sel(5)) lemma gt_compat_fun: assumes "t' >\<^sub>t t" shows "App s t' >\<^sub>t App s t" using assms apply (simp only:atomize_imp) proof (induction rule:measure_induct_rule[of "\(t, s). hsize t + hsize s" "\(t, s). t' >\<^sub>t t \ App s t' >\<^sub>t App s t" "(t,s)", simplified prod.case], simp only: split_paired_all prod.case atomize_imp[symmetric]) fix t s ::"('s, 'v) tm" assume ih:"\ta sa. hsize ta + hsize sa < hsize t + hsize s \ t' >\<^sub>t ta \ App sa t' >\<^sub>t App sa ta" and t'_gt_t:"t' >\<^sub>t t" have t'_ne_t: "t' \ t" using gt_antisym t'_gt_t by blast have extf_args_single: "\f \ ground_heads (head s). extf f (>\<^sub>t) (args s @ [t']) (args s @ [t])" by (simp add: extf_compat_list t'_gt_t t'_ne_t) show "App s t' >\<^sub>t App s t" proof (rule gt_same) show "head (App s t') = head (App s t)" by simp show "\f\local.ground_heads (head (App s t')). extf f (>\<^sub>t) (args (App s t')) (args (App s t))" by (simp add: extf_args_single) have 0: "chop (App s t') >\<^sub>t chop (App s t)" proof (cases s) case (Hd _) then show ?thesis using chop_App_Hd by (simp add: chop_App_Hd t'_gt_t) next case (App s1 s2) then show ?thesis using ih[of t "chop s"] chop_fun by (metis nat_add_left_cancel_less hsize_chop_lt t'_gt_t tm.disc(2) tm.sel(4) tm.sel(6)) qed show "chkchop_same (>\<^sub>t) (App s t') (App s t)" proof (cases "is_Var (head (App s t'))") case True then show ?thesis unfolding chkchop_same_def chkchop_def using True 0 by auto next case False have "App s t' >\<^sub>t chop (App s t)" using 0 by (simp add: gt_chop) then show ?thesis unfolding chkchop_same_def chkchop_def using False by auto qed qed qed theorem gt_compat_arg: shows "s' >\<^sub>t s \ t' \\<^sub>t t \ App s' t' >\<^sub>t App s t" proof (simp only:atomize_imp,induction rule:measure_induct[of "\(s',s,t). hsize s' + hsize s + hsize t" "\(s',s,t). s' >\<^sub>t s \ t' \\<^sub>t t \ App s' t' >\<^sub>t App s t" "(s',s,t)", simplified prod.case], simp only: split_paired_all prod.case atomize_imp[symmetric] atomize_all[symmetric]) fix s' s t assume ih:"\ab ac ba. hsize ab + hsize ac + hsize ba < hsize s' + hsize s + hsize t \ ab >\<^sub>t ac \ t' \\<^sub>t ba \ App ab t' >\<^sub>t App ac ba" and "s' >\<^sub>t s" and "t' \\<^sub>t t" { fix s''::"('s,'v) tm" assume hsize_s'':"hsize s'' \ hsize s'" assume chkchop_s'_s: "chkchop (>\<^sub>t) s'' s" then have "chkchop (>\<^sub>t) (App s'' t') (App s t)" proof (cases "is_Hd s") case True then show ?thesis using chkchop_s'_s unfolding chkchop_def by (metis \t' \\<^sub>t t\ chop_App_Hd gt_arg_imp gt_emb_arg tm.sel(6)) next case False then show ?thesis using chkchop_s'_s unfolding chkchop_def using ih[of s'' "chop s" t] hsize_s'' by (metis \t' \\<^sub>t t\ add_less_mono add_mono_thms_linordered_field(1) chop_fun le_eq_less_or_eq nat_add_left_cancel_less hsize_chop_lt tm.sel(4) tm.sel(6)) qed } note chkchop_compat_arg = this show "App s' t' >\<^sub>t App s t " using \s' >\<^sub>t s\ proof (cases rule:gt.cases) case gt_chop then show ?thesis proof (cases "t = t'") case True show ?thesis using True gt.gt_chop[of "App s' t'" "App s t"] gt_chop chkchop_compat_arg[of "chop s'"] by (metis add_strict_right_mono chop_fun ih hsize_chop_lt tm.disc(2) tm.sel(4) tm.sel(6)) next case False then have "t' >\<^sub>t t" using \t' \\<^sub>t t\ by blast have "App s' t' >\<^sub>t App (chop s') t'" by (simp add: context_left emb_step_chop gt_embedding_step_property local.gt_chop(1)) moreover have "... >\<^sub>t App s t" using ih[of "chop s'" s t] using \t' >\<^sub>t t\ gt_compat_fun local.gt_chop(1) local.gt_chop(2) hsize_chop_lt by fastforce ultimately show ?thesis using gt_trans by blast qed next case gt_diff then show ?thesis using chkchop_compat_arg gt.gt_diff by auto next case gt_same have hd_s'_eq_s: "head s' = head s" by (simp add: local.gt_same(1)) { fix f assume f_gh: "f \ ground_heads (head s)" have f_s_args: "extf f (>\<^sub>t) (args s') (args s)" using local.gt_same(3) f_gh by (simp add: hd_s'_eq_s) have f_compat_snoc: "\xs ys x. extf f (>\<^sub>t) ys xs \ extf f (>\<^sub>t) (ys @ [x]) (xs @ [x])" by (simp add: extf_compat_append_right) have f_st_args2: "extf f (>\<^sub>t) (args (App s' t)) (args (App s t))" by (simp add: f_compat_snoc f_s_args) have 0:"\z\UNIV. \y\UNIV. \x\UNIV. z >\<^sub>t y \ y >\<^sub>t x \ z >\<^sub>t x" using gt_trans by blast then have f_trans:"\xs ys zs. extf f (>\<^sub>t) zs ys \ extf f (>\<^sub>t) ys xs \ extf f (>\<^sub>t) zs xs" using extf_trans[of _ UNIV, unfolded lists_UNIV, OF UNIV_I UNIV_I UNIV_I 0] by metis have "extf f (>\<^sub>t) (args (App s' t')) (args (App s t))" proof (cases "t' = t") case True then show ?thesis using f_st_args2 by metis next case False have f_st_args1: "extf f (>\<^sub>t) (args (App s' t')) (args (App s' t))" using extf_compat_list \t' \\<^sub>t t\ False by simp then show ?thesis using f_trans f_st_args1 f_st_args2 by metis qed } note extf_cond = this have "chkchop_same (>\<^sub>t) (App s' t') (App s t)" unfolding chkchop_same_def using args.simps(1) chop_fun chkchop_compat_arg[of "chop s'", unfolded le_eq_less_or_eq] chkchop_compat_arg[of s'] chkchop_def chkchop_same_def hsize_chop_lt epo.extf_min_empty[OF epo_axioms] gt.gt_same gt_antisym hd_s'_eq_s head_App leI less_irrefl_nat local.gt_same(2) local.gt_same(3) tm.collapse(1) tm.sel(4) tm.sel(6) by metis then show ?thesis using extf_cond gt.gt_same hd_s'_eq_s by auto qed qed theorem gt_compat_fun_strong: assumes t'_gt_t: "t' >\<^sub>t t" shows "apps s (t' # us) >\<^sub>t apps s (t # us)" proof (induct us rule: rev_induct) case Nil then show ?case by (simp add: gt_compat_fun t'_gt_t) next case (snoc x xs) then show ?case unfolding App_apps[symmetric] append_Cons[symmetric] using gt_compat_arg by blast qed theorem gt_or_eq_compat_App: "s' \\<^sub>t s \ t' \\<^sub>t t \ App s' t' \\<^sub>t App s t" using gt_compat_fun gt_compat_arg by blast theorem gt_compat_App: shows "s' \\<^sub>t s \ t' >\<^sub>t t \ App s' t' >\<^sub>t App s t" using gt_compat_fun gt_compat_arg by blast subsection "Stability under Substitutions" (* TODO: move *) lemma extf_map2: assumes "\y\set ys \ set xs. \x\set ys \ set xs. y >\<^sub>t x \ (h y) >\<^sub>t (h x)" "extf f (>\<^sub>t) ys xs" shows "extf f (>\<^sub>t) (map h ys) (map h xs)" apply (rule extf_map[of "set ys \ set xs" ys xs "(>\<^sub>t)" h f]) apply simp apply (simp add: in_listsI) apply (simp add: in_listsI) using gt_antisym apply blast using gt_trans apply blast by (simp add: assms)+ theorem gt_sus: assumes \_wary: "wary_subst \" assumes ghd: "\x. ground_heads (Var x) = UNIV" (* This condition is only needed for gt_same, not for gt_diff ! *) shows "t >\<^sub>t s \ subst \ t >\<^sub>t subst \ s" proof (simp only:atomize_imp,induction rule:measure_induct[of "\(t,s). {# hsize t, hsize s #}" "\(t,s). t >\<^sub>t s \ subst \ t >\<^sub>t subst \ s" "(t,s)", simplified prod.case], simp only: split_paired_all prod.case atomize_imp[symmetric] atomize_all[symmetric]) fix t s assume ih:"\tt ss. {# hsize tt, hsize ss #} < {# hsize t, hsize s #} \ tt >\<^sub>t ss \ subst \ tt >\<^sub>t subst \ ss" and "t >\<^sub>t s" show "subst \ t >\<^sub>t subst \ s" using \t >\<^sub>t s\ proof (cases) case t_gt_s_chop: gt_chop then show ?thesis using emb_step_subst emb_step_chop[OF t_gt_s_chop(1)] gt_embedding_step_property emb_step_hsize gt_trans ih[of "chop t" s] by (metis add_mset_lt_left_lt) next case t_gt_s_diff: gt_diff have gt_diff1: "head (subst \ t) >\<^sub>h\<^sub>d head (subst \ s)" by (meson assms gt_hd_def subsetCE t_gt_s_diff(1) wary_subst_ground_heads) have gt_diff2: "is_Sym (head (subst \ s))" by (metis ground_imp_subst_iden hd.collapse(2) hd.simps(18) head_subst t_gt_s_diff(2) tm.sel(1) tm.simps(17)) have gt_diff3: "chkchop (>\<^sub>t) (subst \ t) (subst \ s)" proof (cases s) case (Hd _) then show ?thesis using t_gt_s_diff unfolding chkchop_def by (metis ground_imp_subst_iden hd.collapse(2) hd.simps(18) tm.disc(1) tm.sel(1) tm.simps(17)) next case s_App: (App s1 s2) then show ?thesis using t_gt_s_diff unfolding chkchop_def using ih[of t "chop s"] chop_subst_Sym hsize_chop_lt tm.disc(2) by (metis add_mset_lt_left_lt add_mset_lt_right_lt) qed show ?thesis using gt_diff gt_diff1 gt_diff2 gt_diff3 by blast next case t_gt_s_same: gt_same have gt_same1: "head (subst \ t) = head (subst \ s)" by (simp add: t_gt_s_same(1)) have extf_map_ts:"\f\ground_heads (head t). extf f (>\<^sub>t) (map (subst \) (args t)) (map (subst \) (args s))" proof - have ih_args: "\y\set (args t) \ set (args s). \x\set (args t) \ set (args s). y >\<^sub>t x \ subst \ y >\<^sub>t subst \ x" by (metis Un_iff less_multiset_doubletons hsize_in_args ih) have "\f\ground_heads (head t). extf f (>\<^sub>t) (args t) (args s)" using ghd t_gt_s_same(3) by metis then show ?thesis using extf_map[of "set (args t) \ set (args s)" "args t" "args s" gt "subst \"] using gt_irrefl gt_trans ih_args by blast qed show ?thesis proof (cases "head t") case (Var x1) then have "is_Var (head t)" by simp { fix u :: "('s, 'v) tm" assume "ground_heads (head u) \ ground_heads (head t)" "hsize u \ hsize (subst \ (Hd (head t)))" then have "apps u (map (subst \) (args t)) >\<^sub>t apps u (map (subst \) (args s))" proof (induct "hsize u" arbitrary:u rule:less_induct) case less then show ?case proof (cases u) case u_Hd: (Hd _) then have "args u = []" by simp then show ?thesis proof (cases s) case s_Hd: (Hd _) show ?thesis apply (rule gt_same) using extf_map_ts args_Nil_iff_is_Hd s_Hd u_Hd \args u = []\ less by fastforce+ next case s_App: (App _ _) then have "is_App t" by (metis args_Nil_iff_is_Hd extf_min_empty gt_hd_def gt_hd_irrefl t_gt_s_same(3)) have "chop t >\<^sub>t chop s" using \is_App t\ \is_Var (head t)\ s_App t_gt_s_same(2) by auto then have "subst \ (chop t) >\<^sub>t subst \ (chop s)" using ih by (metis \is_App t\ less_multiset_doubletons s_App hsize_chop_lt tm.disc(2)) define ut where "ut = apps u (map (subst \) (args t))" define us where "us = apps u (map (subst \) (args s))" have 0:"\ss. args (apps u ss) = ss" using \args u = []\ by simp have chop_us: "chop us = subst \ (chop s)" unfolding chop_def subst_apps us_def 0 using hd_map by (metis (no_types, lifting) args_Nil_iff_is_Hd map_tl s_App tm.disc(2)) have chop_ut: "chop ut = subst \ (chop t)" unfolding chop_def subst_apps ut_def 0 using \is_App t\ by (simp add: args_Nil_iff_is_Hd hd_map map_tl) have "head ut = head us" by (simp add: us_def ut_def) moreover have "chkchop_same (>\<^sub>t) ut us" unfolding chkchop_def chkchop_same_def by (metis "0" UNIV_witness \is_Var (head t)\ \subst \ (chop t) >\<^sub>t subst \ (chop s)\ args.simps(1) chop_us chop_ut extf_map_ts extf_min_empty ghd gt_chop is_Var_def tm.collapse(1) ut_def) moreover have "\f\local.ground_heads (head ut). extf f (>\<^sub>t) (args ut) (args us)" using extf_map_ts less us_def ut_def using "0" by auto ultimately show "ut >\<^sub>t us" using gt_same by blast qed next case u_app: (App _ _) let ?ut = "apps u (map (subst \) (args t))" let ?us = "apps u (map (subst \) (args s))" have 1:"head ?ut = head ?ut" by simp have "apps (chop u) (map (subst \) (args t)) >\<^sub>t apps (chop u) (map (subst \) (args s))" using less.hyps[of "chop u"] hsize_chop_lt by (metis Var dual_order.trans ghd less.prems(2) less_or_eq_imp_le subset_UNIV tm.disc(2) u_app) then have "chop ?ut >\<^sub>t chop ?us" by (simp add: chop_apps u_app) then have 2:"chkchop_same (>\<^sub>t) ?ut ?us" unfolding chkchop_same_def chkchop_def by (metis UNIV_I \is_Var (head t)\ args_Nil_iff_is_Hd args_apps extf_compat_append_left extf_map_ts extf_min_empty ghd gt_chop is_Var_def) have 3:"\f\local.ground_heads (head ?ut). extf f (>\<^sub>t) (args ?ut) (args ?us)" using extf_compat_append_left extf_map_ts less.prems(1) by auto show ?thesis using gt_same 1 2 3 by simp qed qed } note inner_induction = this show ?thesis using inner_induction[of "subst \ (Hd (head t))", unfolded subst_apps[symmetric]] by (metis Var ghd order_refl subset_UNIV t_gt_s_same(1) tm_collapse_apps) next case (Sym _) then have "is_Sym (head (subst \ t))" "head (subst \ t) = head t" by simp_all then have "chkchop_same (>\<^sub>t) t s" using t_gt_s_same unfolding chkchop_same_def chkchop_def using Sym by metis then have gt_same2: "chkchop_same (>\<^sub>t) (subst \ t) (subst \ s)" unfolding chkchop_same_def chkchop_def using ih[of t "chop s"] by (metis (no_types, lifting) Sym \head (subst \ t) = head t\ \is_Sym (head (subst \ t))\ add_mset_commute add_mset_lt_left_lt chop_subst_Sym ground_imp_subst_iden hd.simps(18) hsize_chop_lt t_gt_s_same(1) tm.collapse(1) tm.simps(17)) have gt_same3: "\f\local.ground_heads (head (subst \ t)). extf f (>\<^sub>t) (args (subst \ t)) (args (subst \ s))" using \head (subst \ t) = head t\ extf_compat_append_left extf_map_ts t_gt_s_same(1) by auto show ?thesis using gt_same gt_same1 gt_same2 gt_same3 by blast qed qed qed subsection \Totality on Ground Terms\ theorem gt_total_ground: assumes extf_total: "\f. ext_total (extf f)" shows "ground t \ ground s \ t >\<^sub>t s \ s >\<^sub>t t \ t = s" proof (simp only: atomize_imp, rule measure_induct_rule[of "\(t, s). {# hsize t, hsize s #}" "\(t, s). ground t \ ground s \ t >\<^sub>t s \ s >\<^sub>t t \ t = s" "(t, s)", simplified prod.case], simp only: split_paired_all prod.case atomize_imp[symmetric]) fix t s :: "('s, 'v) tm" assume ih: "\ta sa. {# hsize ta, hsize sa #} < {# hsize t, hsize s #} \ ground ta \ ground sa \ ta >\<^sub>t sa \ sa >\<^sub>t ta \ ta = sa" and gr_t: "ground t" and gr_s: "ground s" let ?case = "t >\<^sub>t s \ s >\<^sub>t t \ t = s" have "chkchop (>\<^sub>t) t s \ s >\<^sub>t t" unfolding chkchop_def tm.case_eq_if using ih[of t "chop s"] by (metis (no_types, lifting) add_mset_commute add_mset_lt_left_lt gr_s gr_t ground_chop gt_chop hsize_chop_lt) moreover have "chkchop (>\<^sub>t) s t \ t >\<^sub>t s" unfolding chkchop_def tm.case_eq_if using ih[of "chop t" s] by (metis add_mset_lt_left_lt gr_s gr_t ground_chop gt_chop.intros gt_iff_chop_diff_same hsize_chop_lt) moreover { assume chkembs_t_s: "chkchop (>\<^sub>t) t s" and chkembs_s_t: "chkchop (>\<^sub>t) s t" obtain g where g: "head t = Sym g" using gr_t by (metis ground_head hd.collapse(2)) obtain f where f: "head s = Sym f" using gr_s by (metis ground_head hd.collapse(2)) { assume g_gt_f: "g >\<^sub>s f" have "t >\<^sub>t s" using chkembs_t_s f g g_gt_f gt_diff gt_sym_imp_hd by auto } moreover { assume f_gt_g: "f >\<^sub>s g" have "s >\<^sub>t t" using chkembs_s_t f f_gt_g g gt_diff gt_sym_imp_hd by auto } moreover { assume g_eq_f: "g = f" hence hd_t: "head t = head s" using g f by auto let ?ts = "args t" let ?ss = "args s" have gr_ts: "\ta \ set ?ts. ground ta" using ground_args[OF _ gr_t] by blast have gr_ss: "\sa \ set ?ss. ground sa" using ground_args[OF _ gr_s] by blast { assume ts_eq_ss: "?ts = ?ss" have "t = s" using hd_t ts_eq_ss by (rule tm_expand_apps) } moreover { assume ts_gt_ss: "extf g (>\<^sub>t) ?ts ?ss" have "t >\<^sub>t s" using chkembs_t_s g gt_same hd_t ts_gt_ss by auto } moreover { assume ss_gt_ts: "extf g (>\<^sub>t) ?ss ?ts" have "s >\<^sub>t t" using chkembs_s_t f g_eq_f gt_same hd_t ss_gt_ts by auto } ultimately have ?case using ih gr_ss gr_ts ext_total.total[OF extf_total, rule_format, of "set ?ts \ set ?ss" "(>\<^sub>t)" ?ts ?ss g] using less_multiset_doubletons epo_axioms hsize_in_args in_listsI by (metis Un_iff) } ultimately have ?case using gt_sym_total by blast } ultimately show ?case by fast qed subsection \Well-foundedness\ abbreviation gtg :: "('s, 'v) tm \ ('s, 'v) tm \ bool" (infix ">\<^sub>t\<^sub>g" 50) where "(>\<^sub>t\<^sub>g) \ \t s. ground t \ t >\<^sub>t s" theorem gt_wf: assumes ghd_UNIV: "\x. ground_heads_var x = UNIV" assumes extf_wf: "\f. ext_wf (extf f)" shows "wfP (\s t. t >\<^sub>t s)" proof - have ground_wfP: "wfP (\s t. t >\<^sub>t\<^sub>g s)" unfolding wfP_iff_no_inf_chain proof assume "\f. inf_chain (>\<^sub>t\<^sub>g) f" then obtain t where t_bad: "bad (>\<^sub>t\<^sub>g) t" unfolding inf_chain_def bad_def by blast let ?ff = "worst_chain (>\<^sub>t\<^sub>g) (\t s. hsize t > hsize s)" let ?U_of = "\i. {u. (?ff i) \\<^sub>e\<^sub>m\<^sub>b u}" note wf_sz = wf_app[OF wellorder_class.wf, of hsize, simplified] define U where "U = (\i. ?U_of i)" have gr: "\i. ground (?ff i)" using worst_chain_bad[OF wf_sz t_bad, unfolded inf_chain_def] by fast have gr_u: "\u. u \ U \ ground u" unfolding U_def using gr ground_emb by fastforce have "\ bad (>\<^sub>t\<^sub>g) u" if u_in: "u \ ?U_of i" for u i proof let ?ti = "?ff i" assume u_bad: "bad (>\<^sub>t\<^sub>g) u" have sz_u: "hsize u < hsize ?ti" using emb_hsize_neq u_in by blast show False proof (cases i) case 0 thus False using sz_u min_worst_chain_0[OF wf_sz u_bad] by simp next case Suc hence "?ff (i - 1) >\<^sub>t ?ff i" using worst_chain_pred[OF wf_sz t_bad] by simp moreover have "?ff i >\<^sub>t u" using gt_embedding_property u_in by blast ultimately have "?ff (i - 1) >\<^sub>t u" by (rule gt_trans) thus False using Suc sz_u min_worst_chain_Suc[OF wf_sz u_bad] gr by fastforce qed qed hence u_good: "\u. u \ U \ \ bad (>\<^sub>t\<^sub>g) u" unfolding U_def by blast have bad_diff_same: "inf_chain (\t s. ground t \ (gt_diff t s \ gt_same t s)) ?ff" unfolding inf_chain_def proof (intro allI conjI) fix i show "ground (?ff i)" by (rule gr) have gt: "?ff i >\<^sub>t ?ff (Suc i)" using worst_chain_pred[OF wf_sz t_bad] by blast have "\ gt_chop (?ff i) (?ff (Suc i))" proof assume a: "gt_chop (?ff i) (?ff (Suc i))" then have "chop (?ff i) \ ?U_of i" by (metis (mono_tags, lifting) emb_step_chop emb_step_is_emb gt_chop gt_chop.cases gt_irrefl mem_Collect_eq) then have uij_in:"chop (?ff i) \ U" unfolding U_def by fast have "\n. ?ff n >\<^sub>t ?ff (Suc n)" by (rule worst_chain_pred[OF wf_sz t_bad, THEN conjunct2]) hence uij_gt_i_plus_3: "chop (?ff i) >\<^sub>t ?ff (Suc (Suc i))" using gt_trans by (metis (mono_tags, lifting) a gt_chop.cases) have "inf_chain (>\<^sub>t\<^sub>g) (\j. if j = 0 then chop (?ff i) else ?ff (Suc (i + j)))" unfolding inf_chain_def by (auto intro!: gr gr_u[OF uij_in] uij_gt_i_plus_3 worst_chain_pred[OF wf_sz t_bad]) hence "bad (>\<^sub>t\<^sub>g) (chop (?ff i))" unfolding bad_def by fastforce thus False using u_good[OF uij_in] by sat qed thus "gt_diff (?ff i) (?ff (Suc i)) \ gt_same (?ff i) (?ff (Suc i))" using gt unfolding gt_iff_chop_diff_same by sat qed have "wf {(s, t). ground s \ ground t \ sym (head t) >\<^sub>s sym (head s)}" using gt_sym_wf unfolding wfP_def wf_iff_no_infinite_down_chain by fast moreover have "{(s, t). ground t \ gt_diff t s} \ {(s, t). ground s \ ground t \ sym (head t) >\<^sub>s sym (head s)}" proof (clarsimp, intro conjI) fix s t assume gr_t: "ground t" and gt_diff_t_s: "gt_diff t s" thus gr_s: "ground s" using gt_iff_chop_diff_same gt_imp_vars by fastforce show "sym (head t) >\<^sub>s sym (head s)" using gt_diff_t_s ground_head[OF gr_s] ground_head[OF gr_t] by (cases; cases "head s"; cases "head t") (auto simp: gt_hd_def) qed ultimately have wf_diff: "wf {(s, t). ground t \ gt_diff t s}" by (rule wf_subset) have diff_O_same: "{(s, t). ground t \ gt_diff t s} O {(s, t). ground t \ gt_same t s} \ {(s, t). ground t \ gt_diff t s}" unfolding gt_diff.simps gt_same.simps by clarsimp (metis chkchop_def chkchop_same_def gt_same gt_trans) have diff_same_as_union: "{(s, t). ground t \ (gt_diff t s \ gt_same t s)} = {(s, t). ground t \ gt_diff t s} \ {(s, t). ground t \ gt_same t s}" by auto obtain k where bad_same: "inf_chain (\t s. ground t \ gt_same t s) (\i. ?ff (i + k))" using wf_infinite_down_chain_compatible[OF wf_diff _ diff_O_same, of ?ff] bad_diff_same unfolding inf_chain_def diff_same_as_union[symmetric] by auto hence hd_sym: "\i. is_Sym (head (?ff (i + k)))" unfolding inf_chain_def by (simp add: ground_head) define f where "f = sym (head (?ff k))" have hd_eq_f: "head (?ff (i + k)) = Sym f" for i proof (induct i) case 0 thus ?case by (auto simp: f_def hd.collapse(2)[OF hd_sym, of 0, simplified]) next case (Suc ia) thus ?case using bad_same unfolding inf_chain_def gt_same.simps by simp qed let ?gtu = "\t s. t \ U \ t >\<^sub>t s" thm UnionI CollectI have "t \ set (args (?ff i)) \ t \ U" for t i unfolding U_def apply (rule UnionI[of "?U_of i"]) using arg_emb CollectI arg_emb hsize_in_args by fast+ moreover have "\i. extf f (>\<^sub>t\<^sub>g) (args (?ff (i + k))) (args (?ff (Suc i + k)))" using bad_same hd_eq_f unfolding inf_chain_def gt_same.simps f_def hd.collapse(2)[OF ground_head, OF gr] using extf_mono_strong[of _ _ "(>\<^sub>t)" "(\t s. ground t \ t >\<^sub>t s)" ] ground_hd_in_ground_heads by (metis (no_types, lifting) ground_args) ultimately have "\i. extf f ?gtu (args (?ff (i + k))) (args (?ff (Suc i + k)))" using extf_mono_strong[of _ _ "(\t s. ground t \ t >\<^sub>t s)" "\t s. t \ U \ t >\<^sub>t s"] unfolding U_def by blast hence "inf_chain (extf f ?gtu) (\i. args (?ff (i + k)))" unfolding inf_chain_def by blast hence nwf_ext: "\ wfP (\xs ys. extf f ?gtu ys xs)" unfolding wfP_iff_no_inf_chain by fast have gtu_le_gtg: "?gtu \ (>\<^sub>t\<^sub>g)" by (auto intro!: gr_u) have "wfP (\s t. ?gtu t s)" unfolding wfP_iff_no_inf_chain proof (intro notI, elim exE) fix f assume bad_f: "inf_chain ?gtu f" hence bad_f0: "bad ?gtu (f 0)" by (rule inf_chain_bad) have "f 0 \ U" using bad_f unfolding inf_chain_def by blast hence good_f0: "\ bad ?gtu (f 0)" using u_good bad_f inf_chain_bad inf_chain_subset[OF _ gtu_le_gtg] by blast show False using bad_f0 good_f0 by sat qed hence wf_ext: "wfP (\xs ys. extf f ?gtu ys xs)" by (rule ext_wf.wf[OF extf_wf, rule_format]) show False using nwf_ext wf_ext by blast qed let ?subst = "subst grounding_\" have "wfP (\s t. ?subst t >\<^sub>t\<^sub>g ?subst s)" by (rule wfP_app[OF ground_wfP]) hence "wfP (\s t. ?subst t >\<^sub>t ?subst s)" by (simp add: ground_grounding_\) thus ?thesis using gt_sus ghd_UNIV ground_heads.simps(1) wary_grounding_\ wfP_eq_minimal by (metis (no_types, lifting)) qed end end diff --git a/thys/Lambda_Free_KBOs/Lambda_Free_KBO_Std.thy b/thys/Lambda_Free_KBOs/Lambda_Free_KBO_Std.thy --- a/thys/Lambda_Free_KBOs/Lambda_Free_KBO_Std.thy +++ b/thys/Lambda_Free_KBOs/Lambda_Free_KBO_Std.thy @@ -1,1269 +1,1269 @@ (* Title: The Graceful Standard Knuth-Bendix Order for Lambda-Free Higher-Order Terms Author: Heiko Becker , 2016 Author: Jasmin Blanchette , 2016 Author: Uwe Waldmann , 2016 Author: Daniel Wand , 2016 Maintainer: Jasmin Blanchette *) section \The Graceful Standard Knuth--Bendix Order for Lambda-Free Higher-Order Terms\ theory Lambda_Free_KBO_Std -imports Lambda_Free_KBO_Util +imports Lambda_Free_KBO_Util Nested_Multisets_Ordinals.Multiset_More abbrevs ">t" = ">\<^sub>t" and "\t" = "\\<^sub>t" begin text \ This theory defines the standard version of the graceful Knuth--Bendix order for \\\-free higher-order terms. Standard means that one symbol is allowed to have a weight of 0. \ subsection \Setup\ locale kbo_std = kbo_std_basis _ _ arity_sym arity_var wt_sym for arity_sym :: "'s \ enat" and arity_var :: "'v \ enat" and wt_sym :: "'s \ nat" begin subsection \Weights\ primrec wt :: "('s, 'v) tm \ nat" where "wt (Hd \) = (LEAST w. \f \ ground_heads \. w = wt_sym f + the_enat (\ * arity_sym f))" | "wt (App s t) = (wt s - \) + wt t" lemma wt_Hd_Sym: "wt (Hd (Sym f)) = wt_sym f + the_enat (\ * arity_sym f)" by simp lemma exists_wt_sym: "\f \ ground_heads \. wt (Hd \) = wt_sym f + the_enat (\ * arity_sym f)" by (auto intro: Least_in_nonempty_set_imp_ex) lemma wt_le_wt_sym: "f \ ground_heads \ \ wt (Hd \) \ wt_sym f + the_enat (\ * arity_sym f)" using not_le_imp_less not_less_Least by fastforce lemma enat_the_enat_\_times_arity_sym[simp]: "enat (the_enat (\ * arity_sym f)) = \ * arity_sym f" using arity_sym_ne_infinity_if_\_gt_0 imult_is_infinity zero_enat_def by fastforce lemma wt_arg_le: "wt (arg s) \ wt s" by (cases s) auto lemma wt_ge_\: "wt s \ \" by (induct s, metis exists_wt_sym of_nat_eq_enat le_diff_conv of_nat_id wt_sym_ge, simp add: add_increasing) lemma wt_ge_\: "wt s \ \" by (meson \_le_\ order.trans enat_ord_simps(1) wt_ge_\) lemma wt_gt_\_if_superunary: "arity_hd (head s) > 1 \ wt s > \" proof (induct s) case \: (Hd \) obtain g where g_in_grs: "g \ ground_heads \" and wt_\: "wt (Hd \) = wt_sym g + the_enat (\ * arity_sym g)" using exists_wt_sym by blast have "arity_hd \ > 1" using \ by auto hence ary_g: "arity_sym g > 1" using ground_heads_arity[OF g_in_grs] by simp show ?case proof (cases "\ = 0") case True thus ?thesis by (metis \_gt_0 gr0I leD wt_ge_\) next case \_ne_0: False hence ary_g_ninf: "arity_sym g \ \" using arity_sym_ne_infinity_if_\_gt_0 by blast hence "\ < the_enat (enat \ * arity_sym g)" using \_ne_0 ary_g by (cases "arity_sym g") (auto simp: one_enat_def) thus ?thesis unfolding wt_\ by simp qed next case (App s t) thus ?case using wt_ge_\[of t] by force qed lemma wt_App_\: "wt (App s t) = wt t \ wt s = \" by (simp add: order.antisym wt_ge_\) lemma wt_App_ge_fun: "wt (App s t) \ wt s" by (metis diff_le_mono2 wt_ge_\ le_diff_conv wt.simps(2)) lemma wt_hd_le: "wt (Hd (head s)) \ wt s" by (induct s, simp) (metis head_App leD le_less_trans not_le_imp_less wt_App_ge_fun) lemma wt_\_imp_\_eq_\: "wt s = \ \ \ = \" by (metis \_le_\ le_antisym wt_ge_\) lemma wt_ge_arity_head_if_\_gt_0: assumes \_gt_0: "\ > 0" shows "wt s \ arity_hd (head s)" proof (induct s) case (Hd \) obtain f where f_in_\: "f \ ground_heads \" and wt_\: "wt (Hd \) = wt_sym f + the_enat (\ * arity_sym f)" using exists_wt_sym by blast have "arity_sym f \ arity_hd \" by (rule ground_heads_arity[OF f_in_\]) hence "the_enat (\ * arity_sym f) \ arity_hd \" using \_gt_0 by (metis One_nat_def Suc_ile_eq dual_order.trans enat_ord_simps(2) enat_the_enat_\_times_arity_sym i0_lb mult.commute mult.right_neutral mult_left_mono one_enat_def) thus ?case unfolding wt_\ by (metis add.left_neutral add_mono le_iff_add plus_enat_simps(1) tm.sel(1)) next case App thus ?case by (metis dual_order.trans enat_ord_simps(1) head_App wt_App_ge_fun) qed lemma wt_ge_num_args_if_\_eq_0: assumes \_eq_0: "\ = 0" shows "wt s \ num_args s" by (induct s, simp_all, metis (no_types) \_eq_0 \_gt_0 wt_\_imp_\_eq_\ add_le_same_cancel1 le_0_eq le_trans minus_nat.diff_0 not_gr_zero not_less_eq_eq) lemma wt_ge_num_args: "wary s \ wt s \ num_args s" using wt_ge_arity_head_if_\_gt_0 wt_ge_num_args_if_\_eq_0 by (meson order.trans enat_ord_simps(1) neq0_conv wary_num_args_le_arity_head) subsection \Inductive Definitions\ inductive gt :: "('s, 'v) tm \ ('s, 'v) tm \ bool" (infix ">\<^sub>t" 50) where gt_wt: "vars_mset t \# vars_mset s \ wt t > wt s \ t >\<^sub>t s" | gt_unary: "wt t = wt s \ \ head t \\\<^sub>h\<^sub>d head s \ num_args t = 1 \ (\f \ ground_heads (head t). arity_sym f = 1 \ wt_sym f = 0) \ arg t >\<^sub>t s \ arg t = s \ t >\<^sub>t s" | gt_diff: "vars_mset t \# vars_mset s \ wt t = wt s \ head t >\<^sub>h\<^sub>d head s \ t >\<^sub>t s" | gt_same: "vars_mset t \# vars_mset s \ wt t = wt s \ head t = head s \ (\f \ ground_heads (head t). extf f (>\<^sub>t) (args t) (args s)) \ t >\<^sub>t s" abbreviation ge :: "('s, 'v) tm \ ('s, 'v) tm \ bool" (infix "\\<^sub>t" 50) where "t \\<^sub>t s \ t >\<^sub>t s \ t = s" inductive gt_wt :: "('s, 'v) tm \ ('s, 'v) tm \ bool" where gt_wtI: "vars_mset t \# vars_mset s \ wt t > wt s \ gt_wt t s" inductive gt_diff :: "('s, 'v) tm \ ('s, 'v) tm \ bool" where gt_diffI: "vars_mset t \# vars_mset s \ wt t = wt s \ head t >\<^sub>h\<^sub>d head s \ gt_diff t s" inductive gt_unary :: "('s, 'v) tm \ ('s, 'v) tm \ bool" where gt_unaryI: "wt t = wt s \ \ head t \\\<^sub>h\<^sub>d head s \ num_args t = 1 \ (\f \ ground_heads (head t). arity_sym f = 1 \ wt_sym f = 0) \ arg t \\<^sub>t s \ gt_unary t s" inductive gt_same :: "('s, 'v) tm \ ('s, 'v) tm \ bool" where gt_sameI: "vars_mset t \# vars_mset s \ wt t = wt s \ head t = head s \ (\f \ ground_heads (head t). extf f (>\<^sub>t) (args t) (args s)) \ gt_same t s" lemma gt_iff_wt_unary_diff_same: "t >\<^sub>t s \ gt_wt t s \ gt_unary t s \ gt_diff t s \ gt_same t s" by (subst gt.simps) (auto simp: gt_wt.simps gt_unary.simps gt_diff.simps gt_same.simps) lemma gt_imp_vars_mset: "t >\<^sub>t s \ vars_mset t \# vars_mset s" by (induct rule: gt.induct) (auto intro: subset_mset.order.trans) lemma gt_imp_vars: "t >\<^sub>t s \ vars t \ vars s" using set_mset_mono[OF gt_imp_vars_mset] by simp subsection \Irreflexivity\ theorem gt_irrefl: "wary s \ \ s >\<^sub>t s" proof (induct "size s" arbitrary: s rule: less_induct) case less note ih = this(1) and wary_s = this(2) show ?case proof assume s_gt_s: "s >\<^sub>t s" show False using s_gt_s proof (cases rule: gt.cases) case gt_same then obtain f where f: "extf f (>\<^sub>t) (args s) (args s)" by fastforce thus False using wary_s ih by (metis wary_args extf_irrefl size_in_args) qed (auto simp: comp_hd_def gt_hd_irrefl) qed qed subsection \Transitivity\ lemma gt_imp_wt_ge: "t >\<^sub>t s \ wt t \ wt s" by (induct rule: gt.induct) auto lemma not_extf_gt_nil_singleton_if_\_eq_\: assumes wary_s: "wary s" and \_eq_\: "\ = \" shows "\ extf f (>\<^sub>t) [] [s]" proof assume nil_gt_s: "extf f (>\<^sub>t) [] [s]" note s_gt_nil = extf_singleton_nil_if_\_eq_\[OF \_eq_\, of f gt s] have "\ extf f (>\<^sub>t) [] []" by (rule extf_irrefl) simp moreover have "extf f (>\<^sub>t) [] []" using extf_trans_from_irrefl[of "{s}", OF _ _ _ _ _ _ nil_gt_s s_gt_nil] gt_irrefl[OF wary_s] by fastforce ultimately show False by sat qed lemma gt_sub_arg: "wary (App s t) \ App s t >\<^sub>t t" proof (induct t arbitrary: s rule: measure_induct_rule[of size]) case (less t) note ih = this(1) and wary_st = this(2) { assume wt_st: "wt (App s t) = wt t" hence \_eq_\: "\ = \" using wt_App_\ wt_\_imp_\_eq_\ by metis hence \_gt_0: "\ > 0" using \_gt_0 by simp have wt_s: "wt s = \" by (rule wt_App_\[OF wt_st]) have wary_t: "wary t" and nargs_lt: "num_args s < arity_hd (head s)" using wary_st wary.simps by blast+ have ary_hd_s: "arity_hd (head s) = 1" by (metis One_nat_def arity.wary_AppE dual_order.order_iff_strict eSuc_enat enat_defs(1) enat_defs(2) ileI1 linorder_not_le not_iless0 wary_st wt_gt_\_if_superunary wt_s) hence nargs_s: "num_args s = 0" by (metis enat_ord_simps(2) less_one nargs_lt one_enat_def) have "s = Hd (head s)" by (simp add: Hd_head_id nargs_s) then obtain f where f_in: "f \ ground_heads (head s)" and wt_f_etc: "wt_sym f + the_enat (\ * arity_sym f) = \" using exists_wt_sym wt_s by fastforce have ary_f_1: "arity_sym f = 1" proof - have ary_f_ge_1: "arity_sym f \ 1" using ary_hd_s f_in ground_heads_arity by fastforce hence "enat \ * arity_sym f = \" using wt_f_etc by (metis enat_ord_simps(1) enat_the_enat_\_times_arity_sym le_add2 le_antisym mult.right_neutral mult_left_mono zero_le) thus ?thesis using \_gt_0 by (cases "arity_sym f") (auto simp: one_enat_def) qed hence wt_f_0: "wt_sym f = 0" using wt_f_etc by simp { assume hd_s_ncmp_t: "\ head s \\\<^sub>h\<^sub>d head t" have ?case by (rule gt_unary[OF wt_st]) (auto simp: hd_s_ncmp_t nargs_s intro: f_in ary_f_1 wt_f_0) } moreover { assume hd_s_gt_t: "head s >\<^sub>h\<^sub>d head t" have ?case by (rule gt_diff) (auto simp: hd_s_gt_t wt_s[folded \_eq_\]) } moreover { assume "head t >\<^sub>h\<^sub>d head s" hence False using ary_f_1 exists_wt_sym f_in gt_hd_def gt_sym_antisym unary_wt_sym_0_gt wt_f_0 by blast } moreover { assume hd_t_eq_s: "head t = head s" hence nargs_t_le: "num_args t \ 1" using ary_hd_s wary_num_args_le_arity_head[OF wary_t] by (simp add: one_enat_def) have extf: "extf f (>\<^sub>t) [t] (args t)" for f proof (cases "args t") case Nil thus ?thesis by (simp add: extf_singleton_nil_if_\_eq_\[OF \_eq_\]) next case args_t: (Cons ta ts) hence ts: "ts = []" using ary_hd_s[folded hd_t_eq_s] wary_num_args_le_arity_head[OF wary_t] nargs_t_le by simp have ta: "ta = arg t" by (metis apps.simps(1) apps.simps(2) args_t tm.sel(6) tm_collapse_apps ts) hence t: "t = App (fun t) ta" by (metis args.simps(1) args_t not_Cons_self2 tm.exhaust_sel ts) have "t >\<^sub>t ta" by (rule ih[of ta "fun t", folded t, OF _ wary_t]) (metis ta size_arg_lt t tm.disc(2)) thus ?thesis unfolding args_t ts by (metis extf_singleton gt_irrefl wary_t) qed have ?case by (rule gt_same) (auto simp: hd_t_eq_s wt_s[folded \_eq_\] length_0_conv[THEN iffD1, OF nargs_s] extf) } ultimately have ?case unfolding comp_hd_def by metis } thus ?case using gt_wt by fastforce qed lemma gt_arg: "wary s \ is_App s \ s >\<^sub>t arg s" by (cases s) (auto intro: gt_sub_arg) theorem gt_trans: "wary u \ wary t \ wary s \ u >\<^sub>t t \ t >\<^sub>t s \ u >\<^sub>t s" proof (simp only: atomize_imp, rule measure_induct_rule[of "\(u, t, s). {#size u, size t, size s#}" "\(u, t, s). wary u \ wary t \ wary s \ u >\<^sub>t t \ t >\<^sub>t s \ u >\<^sub>t s" "(u, t, s)", simplified prod.case], simp only: split_paired_all prod.case atomize_imp[symmetric]) fix u t s assume ih: "\ua ta sa. {#size ua, size ta, size sa#} < {#size u, size t, size s#} \ wary ua \ wary ta \ wary sa \ ua >\<^sub>t ta \ ta >\<^sub>t sa \ ua >\<^sub>t sa" and wary_u: "wary u" and wary_t: "wary t" and wary_s: "wary s" and u_gt_t: "u >\<^sub>t t" and t_gt_s: "t >\<^sub>t s" have "vars_mset u \# vars_mset t" and "vars_mset t \# vars_mset s" using u_gt_t t_gt_s by (auto simp: gt_imp_vars_mset) hence vars_u_s: "vars_mset u \# vars_mset s" by auto have wt_u_ge_t: "wt u \ wt t" and wt_t_ge_s: "wt t \ wt s" using gt_imp_wt_ge u_gt_t t_gt_s by auto { assume wt_t_s: "wt t = wt s" and wt_u_t: "wt u = wt t" hence wt_u_s: "wt u = wt s" by simp have wary_arg_u: "wary (arg u)" by (rule wary_arg[OF wary_u]) have wary_arg_t: "wary (arg t)" by (rule wary_arg[OF wary_t]) have wary_arg_s: "wary (arg s)" by (rule wary_arg[OF wary_s]) have "u >\<^sub>t s" using t_gt_s proof cases case gt_unary_t_s: gt_unary have t_app: "is_App t" by (metis args_Nil_iff_is_Hd gt_unary_t_s(3) length_greater_0_conv less_numeral_extra(1)) have \_eq_\: "\ = \" using gt_unary_t_s(4) unary_wt_sym_0_imp_\_eq_\ by blast show ?thesis using u_gt_t proof cases case gt_unary_u_t: gt_unary have u_app: "is_App u" by (metis args_Nil_iff_is_Hd gt_unary_u_t(3) length_greater_0_conv less_numeral_extra(1)) hence arg_u_gt_s: "arg u >\<^sub>t s" using ih[of "arg u" t s] gt_unary_u_t(5) t_gt_s size_arg_lt wary_arg_u wary_s wary_t by force hence arg_u_ge_s: "arg u \\<^sub>t s" by sat { assume "size (arg u) < size t" hence ?thesis using ih[of u "arg u" s] arg_u_gt_s gt_arg by (simp add: u_app wary_arg_u wary_s wary_u) } moreover { assume "size (arg t) < size s" hence "u >\<^sub>t arg t" using ih[of u t "arg t"] args_Nil_iff_is_Hd gt_arg gt_unary_t_s(3) u_gt_t wary_t wary_u by force hence ?thesis using ih[of u "arg t" s] args_Nil_iff_is_Hd gt_unary_t_s(3,5) size_arg_lt wary_arg_t wary_s wary_u by force } moreover { assume sz_u_gt_t: "size u > size t" and sz_t_gt_s: "size t > size s" have wt_fun_u: "wt (fun u) = \" by (metis antisym gt_imp_wt_ge gt_unary_u_t(5) tm.collapse(2) u_app wt_App_\ wt_arg_le wt_t_s wt_u_s) have nargs_fun_u: "num_args (fun u) = 0" by (metis args.simps(1) gt_unary_u_t(3) list.size(3) one_arg_imp_Hd tm.collapse(2) u_app) { assume hd_u_eq_s: "head u = head s" hence ary_hd_s: "arity_hd (head s) = 1" using ground_heads_arity gt_unary_u_t(3,4) hd_u_eq_s one_enat_def wary_num_args_le_arity_head wary_u by fastforce have extf: "extf f (>\<^sub>t) (args u) (args s)" for f proof (cases "args s") case Nil thus ?thesis by (metis Hd_head_id \_eq_\ append_Nil args.simps(2) extf_singleton_nil_if_\_eq_\ gt_unary_u_t(3) head_fun length_greater_0_conv less_irrefl_nat nargs_fun_u tm.exhaust_sel zero_neq_one) next case args_s: (Cons sa ss) hence ss: "ss = []" by (cases s, simp, metis One_nat_def antisym_conv ary_hd_s diff_Suc_1 enat_ord_simps(1) le_add2 length_0_conv length_Cons list.size(4) one_enat_def wary_num_args_le_arity_head wary_s) have sa: "sa = arg s" by (metis apps.simps(1) apps.simps(2) args_s tm.sel(6) tm_collapse_apps ss) have s_app: "is_App s" using args_Nil_iff_is_Hd args_s by force have args_u: "args u = [arg u]" by (metis append_Nil args.simps(2) args_Nil_iff_is_Hd gt_unary_u_t(3) length_0_conv nargs_fun_u tm.collapse(2) zero_neq_one) have max_sz_u_t_s: "Max {size s, size t, size u} = size u" using sz_t_gt_s sz_u_gt_t by auto have max_sz_arg_u_t_arg_t: "Max {size (arg t), size t, size (arg u)} < size u" using size_arg_lt sz_u_gt_t t_app u_app by fastforce have "{#size (arg u), size t, size (arg t)#} < {#size u, size t, size s#}" using max_sz_arg_u_t_arg_t by (simp add: Max_lt_imp_lt_mset insert_commute max_sz_u_t_s) hence arg_u_gt_arg_t: "arg u >\<^sub>t arg t" using ih[OF _ wary_arg_u wary_t wary_arg_t] args_Nil_iff_is_Hd gt_arg gt_unary_t_s(3) gt_unary_u_t(5) wary_t by force have max_sz_arg_s_s_arg_t: "Max {size (arg s), size s, size (arg t)} < size u" using s_app t_app size_arg_lt sz_t_gt_s sz_u_gt_t by force have "{#size (arg t), size s, size (arg s)#} < {#size u, size t, size s#}" by (meson add_mset_lt_lt_lt less_trans mset_lt_single_iff s_app size_arg_lt sz_t_gt_s sz_u_gt_t t_app) hence arg_t_gt_arg_s: "arg t >\<^sub>t arg s" using ih[OF _ wary_arg_t wary_s wary_arg_s] gt_unary_t_s(5) gt_arg args_Nil_iff_is_Hd args_s wary_s by force have "arg u >\<^sub>t arg s" using ih[of "arg u" "arg t" "arg s"] arg_u_gt_arg_t arg_t_gt_arg_s by (simp add: add_mset_lt_le_lt less_imp_le_nat s_app size_arg_lt t_app u_app wary_arg_s wary_arg_t wary_arg_u) thus ?thesis unfolding args_u args_s ss sa by (metis extf_singleton gt_irrefl wary_arg_u) qed have ?thesis by (rule gt_same[OF vars_u_s wt_u_s hd_u_eq_s]) (simp add: extf) } moreover { assume "head u >\<^sub>h\<^sub>d head s" hence ?thesis by (rule gt_diff[OF vars_u_s wt_u_s]) } moreover { assume "head s >\<^sub>h\<^sub>d head u" hence False using gt_hd_def gt_hd_irrefl gt_sym_antisym gt_unary_u_t(4) unary_wt_sym_0_gt by blast } moreover { assume "\ head u \\\<^sub>h\<^sub>d head s" hence ?thesis by (rule gt_unary[OF wt_u_s _ gt_unary_u_t(3,4) arg_u_ge_s]) } ultimately have ?thesis unfolding comp_hd_def by sat } ultimately show ?thesis by (metis args_Nil_iff_is_Hd dual_order.strict_trans2 gt_unary_t_s(3) gt_unary_u_t(3) length_0_conv not_le_imp_less size_arg_lt zero_neq_one) next case gt_diff_u_t: gt_diff have False using gt_diff_u_t(3) gt_hd_def gt_hd_irrefl gt_sym_antisym gt_unary_t_s(4) unary_wt_sym_0_gt by blast thus ?thesis by sat next case gt_same_u_t: gt_same have hd_u_ncomp_s: "\ head u \\\<^sub>h\<^sub>d head s" by (rule gt_unary_t_s(2)[folded gt_same_u_t(3)]) have "num_args u \ 1" by (metis enat_ord_simps(1) ground_heads_arity gt_same_u_t(3) gt_unary_t_s(4) one_enat_def order_trans wary_num_args_le_arity_head wary_u) hence nargs_u: "num_args u = 1" by (cases "args u", metis Hd_head_id \_eq_\ append_Nil args.simps(2) gt_same_u_t(3,4) gt_unary_t_s(3,4) head_fun list.size(3) not_extf_gt_nil_singleton_if_\_eq_\ one_arg_imp_Hd tm.collapse(2)[OF t_app] wary_arg_t, simp) have "arg u >\<^sub>t arg t" by (metis extf_singleton[THEN iffD1] append_Nil args.simps args_Nil_iff_is_Hd comp_hd_def gt_hd_def gt_irrefl gt_same_u_t(3,4) gt_unary_t_s(2,3) head_fun length_0_conv nargs_u one_arg_imp_Hd t_app tm.collapse(2) u_gt_t wary_u) hence "arg u >\<^sub>t s" using ih[OF _ wary_arg_u wary_arg_t wary_s] gt_unary_t_s(5) by (metis add_mset_lt_left_lt add_mset_lt_lt_lt args_Nil_iff_is_Hd list.size(3) nargs_u size_arg_lt t_app zero_neq_one) hence arg_u_ge_s: "arg u \\<^sub>t s" by sat show ?thesis by (rule gt_unary[OF wt_u_s hd_u_ncomp_s nargs_u _ arg_u_ge_s]) (simp add: gt_same_u_t(3) gt_unary_t_s(4)) qed (simp add: wt_u_t) next case gt_diff_t_s: gt_diff show ?thesis using u_gt_t proof cases case gt_unary_u_t: gt_unary have "is_App u" by (metis args_Nil_iff_is_Hd gt_unary_u_t(3) length_greater_0_conv less_numeral_extra(1)) hence "arg u >\<^sub>t s" using ih[of "arg u" t s] gt_unary_u_t(5) t_gt_s size_arg_lt wary_arg_u wary_s wary_t by force hence arg_u_ge_s: "arg u \\<^sub>t s" by sat { assume "head u = head s" hence False using gt_diff_t_s(3) gt_unary_u_t(2) unfolding comp_hd_def by force } moreover { assume "head s >\<^sub>h\<^sub>d head u" hence False using gt_hd_def gt_hd_irrefl gt_sym_antisym gt_unary_u_t(4) unary_wt_sym_0_gt by blast } moreover { assume "head u >\<^sub>h\<^sub>d head s" hence ?thesis by (rule gt_diff[OF vars_u_s wt_u_s]) } moreover { assume "\ head u \\\<^sub>h\<^sub>d head s" hence ?thesis by (rule gt_unary[OF wt_u_s _ gt_unary_u_t(3,4) arg_u_ge_s]) } ultimately show ?thesis unfolding comp_hd_def by sat next case gt_diff_u_t: gt_diff have "head u >\<^sub>h\<^sub>d head s" using gt_diff_u_t(3) gt_diff_t_s(3) gt_hd_trans by blast thus ?thesis by (rule gt_diff[OF vars_u_s wt_u_s]) next case gt_same_u_t: gt_same have "head u >\<^sub>h\<^sub>d head s" using gt_diff_t_s(3) gt_same_u_t(3) by simp thus ?thesis by (rule gt_diff[OF vars_u_s wt_u_s]) qed (simp add: wt_u_t) next case gt_same_t_s: gt_same show ?thesis using u_gt_t proof cases case gt_unary_u_t: gt_unary have "is_App u" by (metis args_Nil_iff_is_Hd gt_unary_u_t(3) length_greater_0_conv less_numeral_extra(1)) hence "arg u >\<^sub>t s" using ih[of "arg u" t s] gt_unary_u_t(5) t_gt_s size_arg_lt wary_arg_u wary_s wary_t by force hence arg_u_ge_s: "arg u \\<^sub>t s" by sat have "\ head u \\\<^sub>h\<^sub>d head s" using gt_same_t_s(3) gt_unary_u_t(2) by simp thus ?thesis by (rule gt_unary[OF wt_u_s _ gt_unary_u_t(3,4) arg_u_ge_s]) next case gt_diff_u_t: gt_diff have "head u >\<^sub>h\<^sub>d head s" using gt_diff_u_t(3) gt_same_t_s(3) by simp thus ?thesis by (rule gt_diff[OF vars_u_s wt_u_s]) next case gt_same_u_t: gt_same have hd_u_s: "head u = head s" by (simp only: gt_same_t_s(3) gt_same_u_t(3)) let ?S = "set (args u) \ set (args t) \ set (args s)" have gt_trans_args: "\ua \ ?S. \ta \ ?S. \sa \ ?S. ua >\<^sub>t ta \ ta >\<^sub>t sa \ ua >\<^sub>t sa" proof clarify fix sa ta ua assume ua_in: "ua \ ?S" and ta_in: "ta \ ?S" and sa_in: "sa \ ?S" and ua_gt_ta: "ua >\<^sub>t ta" and ta_gt_sa: "ta >\<^sub>t sa" have wary_sa: "wary sa" and wary_ta: "wary ta" and wary_ua: "wary ua" using wary_args ua_in ta_in sa_in wary_u wary_t wary_s by blast+ show "ua >\<^sub>t sa" by (auto intro!: ih[OF Max_lt_imp_lt_mset wary_ua wary_ta wary_sa ua_gt_ta ta_gt_sa]) (meson ua_in ta_in sa_in Un_iff max.strict_coboundedI1 max.strict_coboundedI2 size_in_args)+ qed have "\f \ ground_heads (head u). extf f (>\<^sub>t) (args u) (args s)" by (clarify, rule extf_trans_from_irrefl[of ?S _ "args t", OF _ _ _ _ _ gt_trans_args]) (auto simp: gt_same_u_t(3,4) gt_same_t_s(4) wary_args wary_u wary_t wary_s gt_irrefl) thus ?thesis by (rule gt_same[OF vars_u_s wt_u_s hd_u_s]) qed (simp add: wt_u_t) qed (simp add: wt_t_s) } thus "u >\<^sub>t s" using vars_u_s wt_t_ge_s wt_u_ge_t by (force intro: gt_wt) qed lemma gt_antisym: "wary s \ wary t \ t >\<^sub>t s \ \ s >\<^sub>t t" using gt_irrefl gt_trans by blast subsection \Subterm Property\ lemma gt_sub_fun: "App s t >\<^sub>t s" proof (cases "wt (App s t) > wt s") case True thus ?thesis using gt_wt by simp next case False hence wt_st: "wt (App s t) = wt s" by (meson order.antisym not_le_imp_less wt_App_ge_fun) hence \_eq_\: "\ = \" by (metis add_diff_cancel_left' diff_diff_cancel wt_\_imp_\_eq_\ wt_ge_\ wt.simps(2)) have vars_st: "vars_mset (App s t) \# vars_mset s" by auto have hd_st: "head (App s t) = head s" by auto have extf: "\f \ ground_heads (head (App s t)). extf f (>\<^sub>t) (args (App s t)) (args s)" by (simp add: \_eq_\ extf_snoc_if_\_eq_\) show ?thesis by (rule gt_same[OF vars_st wt_st hd_st extf]) qed theorem gt_proper_sub: "wary t \ proper_sub s t \ t >\<^sub>t s" by (induct t) (auto intro: gt_sub_fun gt_sub_arg gt_trans sub.intros wary_sub) subsection \Compatibility with Functions\ theorem gt_compat_fun: assumes wary_t: "wary t" and t'_gt_t: "t' >\<^sub>t t" shows "App s t' >\<^sub>t App s t" proof - have vars_st': "vars_mset (App s t') \# vars_mset (App s t)" by (simp add: t'_gt_t gt_imp_vars_mset) show ?thesis proof (cases "wt t' > wt t") case True hence wt_st': "wt (App s t') > wt (App s t)" by (simp only: wt.simps) show ?thesis by (rule gt_wt[OF vars_st' wt_st']) next case False hence "wt t' = wt t" using t'_gt_t gt_imp_wt_ge order.not_eq_order_implies_strict by fastforce hence wt_st': "wt (App s t') = wt (App s t)" by (simp only: wt.simps) have head_st': "head (App s t') = head (App s t)" by simp have extf: "\f. extf f (>\<^sub>t) (args s @ [t']) (args s @ [t])" using t'_gt_t by (metis extf_compat_list gt_irrefl[OF wary_t]) show ?thesis by (rule gt_same[OF vars_st' wt_st' head_st']) (simp add: extf) qed qed subsection \Compatibility with Arguments\ theorem gt_compat_arg: assumes wary_s't: "wary (App s' t)" and s'_gt_s: "s' >\<^sub>t s" shows "App s' t >\<^sub>t App s t" proof - have vars_s't: "vars_mset (App s' t) \# vars_mset (App s t)" by (simp add: s'_gt_s gt_imp_vars_mset) show ?thesis using s'_gt_s proof cases case gt_wt_s'_s: gt_wt have "wt (App s' t) > wt (App s t)" by (simp add: wt_ge_\) (metis add_diff_assoc add_less_cancel_right gt_wt_s'_s(2) wt_ge_\) thus ?thesis by (rule gt_wt[OF vars_s't]) next case gt_unary_s'_s: gt_unary have False by (metis ground_heads_arity gt_unary_s'_s(3) gt_unary_s'_s(4) leD one_enat_def wary_AppE wary_s't) thus ?thesis by sat next case _: gt_diff thus ?thesis by (simp add: gt_diff) next case gt_same_s'_s: gt_same have wt_s't: "wt (App s' t) = wt (App s t)" by (simp add: gt_same_s'_s(2)) have hd_s't: "head (App s' t) = head (App s t)" by (simp add: gt_same_s'_s(3)) have "\f \ ground_heads (head (App s' t)). extf f (>\<^sub>t) (args (App s' t)) (args (App s t))" using gt_same_s'_s(4) by (auto intro: extf_compat_append_right) thus ?thesis by (rule gt_same[OF vars_s't wt_s't hd_s't]) qed qed subsection \Stability under Substitution\ definition extra_wt :: "('v \ ('s, 'v) tm) \ ('s, 'v) tm \ nat" where "extra_wt \ s = (\x \# vars_mset s. wt (\ x) - wt (Hd (Var x)))" lemma extra_wt_Var[simp]: "extra_wt \ (Hd (Var x)) = wt (\ x) - wt (Hd (Var x))" and extra_wt_Sym[simp]: "extra_wt \ (Hd (Sym f)) = 0" and extra_wt_App[simp]: "extra_wt \ (App s t) = extra_wt \ s + extra_wt \ t" unfolding extra_wt_def by simp+ lemma extra_wt_subseteq: assumes vars_s: "vars_mset t \# vars_mset s" shows "extra_wt \ t \ extra_wt \ s" proof (unfold extra_wt_def) let ?diff = "\v. wt (\ v) - wt (Hd (Var v))" have "vars_mset s + (vars_mset t - vars_mset s) = vars_mset t" using vars_s by (meson subset_mset.add_diff_inverse) hence "{#?diff v. v \# vars_mset t#} = {#?diff v. v \# vars_mset s#} + {#?diff v. v \# vars_mset t - vars_mset s#}" by (metis image_mset_union) thus "(\v \# vars_mset t. ?diff v) \ (\v \# vars_mset s. ?diff v)" by simp qed lemma wt_subst: assumes wary_\: "wary_subst \" and wary_s: "wary s" shows "wt (subst \ s) = wt s + extra_wt \ s" using wary_s proof (induct s rule: tm.induct) case \: (Hd \) show ?case proof (cases \) case x: (Var x) let ?\ = "head (\ x)" obtain g where g_in_grs_\: "g \ ground_heads ?\" and wt_\: "wt (Hd ?\) = wt_sym g + the_enat (\ * arity_sym g)" using exists_wt_sym by blast have "g \ ground_heads \" using x g_in_grs_\ wary_\ wary_subst_def by auto hence wt_\x_ge: "wt (\ x) \ wt (Hd \)" by (metis (full_types) dual_order.trans wt_le_wt_sym wt_\ wt_hd_le) thus ?thesis using x by (simp add: extra_wt_def) qed auto next case (App s t) note ih_s = this(1) and ih_t = this(2) and wary_st = this(3) have "wary s" using wary_st by (meson wary_AppE) hence "\n. extra_wt \ s + (wt s - \ + n) = wt (subst \ s) - \ + n" using ih_s by (metis (full_types) add_diff_assoc2 ab_semigroup_add_class.add_ac(1) add.left_commute wt_ge_\) hence "extra_wt \ s + (wt s + wt t - \ + extra_wt \ t) = wt (subst \ s) + wt (subst \ t) - \" using ih_t wary_st by (metis (no_types) add_diff_assoc2 ab_semigroup_add_class.add_ac(1) wary_AppE wt_ge_\) thus ?case by (simp add: wt_ge_\) qed theorem gt_subst: assumes wary_\: "wary_subst \" shows "wary t \ wary s \ t >\<^sub>t s \ subst \ t >\<^sub>t subst \ s" proof (simp only: atomize_imp, rule measure_induct_rule[of "\(t, s). {#size t, size s#}" "\(t, s). wary t \ wary s \ t >\<^sub>t s \ subst \ t >\<^sub>t subst \ s" "(t, s)", simplified prod.case], simp only: split_paired_all prod.case atomize_imp[symmetric]) fix t s assume ih: "\ta sa. {#size ta, size sa#} < {#size t, size s#} \ wary ta \ wary sa \ ta >\<^sub>t sa \ subst \ ta >\<^sub>t subst \ sa" and wary_t: "wary t" and wary_s: "wary s" and t_gt_s: "t >\<^sub>t s" show "subst \ t >\<^sub>t subst \ s" proof (cases "wt (subst \ t) = wt (subst \ s)") case wt_\t_ne_\s: False have vars_s: "vars_mset t \# vars_mset s" by (simp add: t_gt_s gt_imp_vars_mset) hence vars_\s: "vars_mset (subst \ t) \# vars_mset (subst \ s)" by (rule vars_mset_subst_subseteq) have wt_t_ge_s: "wt t \ wt s" by (simp add: gt_imp_wt_ge t_gt_s) have "wt (subst \ t) > wt (subst \ s)" using wt_\t_ne_\s unfolding wt_subst[OF wary_\ wary_s] wt_subst[OF wary_\ wary_t] by (metis add_le_cancel_left add_less_le_mono extra_wt_subseteq order.not_eq_order_implies_strict vars_s wt_t_ge_s) thus ?thesis by (rule gt_wt[OF vars_\s]) next case wt_\t_eq_\s: True show ?thesis using t_gt_s proof cases case gt_wt hence False using wt_\t_eq_\s wary_s wary_t by (metis add_diff_cancel_right' diff_le_mono2 extra_wt_subseteq wt_subst leD wary_\) thus ?thesis by sat next case gt_unary have wary_\t: "wary (subst \ t)" by (simp add: wary_subst_wary wary_t wary_\) show ?thesis proof (cases t) case Hd hence False using gt_unary(3) by simp thus ?thesis by sat next case t: (App t1 t2) hence t2: "t2 = arg t" by simp hence wary_t2: "wary t2" using wary_t by blast show ?thesis proof (cases "t2 = s") case True moreover have "subst \ t >\<^sub>t subst \ t2" using gt_sub_arg wary_\t unfolding t by simp ultimately show ?thesis by simp next case t2_ne_s: False hence t2_gt_s: "t2 >\<^sub>t s" using gt_unary(5) t2 by blast have "subst \ t2 >\<^sub>t subst \ s" by (rule ih[OF _ wary_t2 wary_s t2_gt_s]) (simp add: t) thus ?thesis by (metis gt_sub_arg gt_trans subst.simps(2) t wary_\ wary_\t wary_s wary_subst_wary wary_t2) qed qed next case _: gt_diff note vars_s = this(1) and hd_t_gt_hd_s = this(3) have vars_\s: "vars_mset (subst \ t) \# vars_mset (subst \ s)" by (rule vars_mset_subst_subseteq[OF vars_s]) have "head (subst \ t) >\<^sub>h\<^sub>d head (subst \ s)" by (meson hd_t_gt_hd_s wary_subst_ground_heads gt_hd_def rev_subsetD wary_\) thus ?thesis by (rule gt_diff[OF vars_\s wt_\t_eq_\s]) next case _: gt_same note vars_s = this(1) and hd_s_eq_hd_t = this(3) and extf = this(4) have vars_\s: "vars_mset (subst \ t) \# vars_mset (subst \ s)" by (rule vars_mset_subst_subseteq[OF vars_s]) have hd_\t: "head (subst \ t) = head (subst \ s)" by (simp add: hd_s_eq_hd_t) { fix f assume f_in_grs: "f \ ground_heads (head (subst \ t))" let ?S = "set (args t) \ set (args s)" have extf_args_s_t: "extf f (>\<^sub>t) (args t) (args s)" using extf f_in_grs wary_subst_ground_heads wary_\ by blast have "extf f (>\<^sub>t) (map (subst \) (args t)) (map (subst \) (args s))" proof (rule extf_map[of ?S, OF _ _ _ _ _ _ extf_args_s_t]) show "\x \ ?S. \ subst \ x >\<^sub>t subst \ x" using gt_irrefl wary_t wary_s wary_args wary_\ wary_subst_wary by fastforce next show "\z \ ?S. \y \ ?S. \x \ ?S. subst \ z >\<^sub>t subst \ y \ subst \ y >\<^sub>t subst \ x \ subst \ z >\<^sub>t subst \ x" using gt_trans wary_t wary_s wary_args wary_\ wary_subst_wary by (metis Un_iff) next have sz_a: "\ta \ ?S. \sa \ ?S. {#size ta, size sa#} < {#size t, size s#}" by (fastforce intro: Max_lt_imp_lt_mset dest: size_in_args) show "\y \ ?S. \x \ ?S. y >\<^sub>t x \ subst \ y >\<^sub>t subst \ x" using ih sz_a size_in_args wary_t wary_s wary_args wary_\ wary_subst_wary by fastforce qed auto hence "extf f (>\<^sub>t) (args (subst \ t)) (args (subst \ s))" by (auto simp: hd_s_eq_hd_t intro: extf_compat_append_left) } hence "\f \ ground_heads (head (subst \ t)). extf f (>\<^sub>t) (args (subst \ t)) (args (subst \ s))" by blast thus ?thesis by (rule gt_same[OF vars_\s wt_\t_eq_\s hd_\t]) qed qed qed subsection \Totality on Ground Terms\ theorem gt_total_ground: assumes extf_total: "\f. ext_total (extf f)" shows "ground t \ ground s \ t >\<^sub>t s \ s >\<^sub>t t \ t = s" proof (simp only: atomize_imp, rule measure_induct_rule[of "\(t, s). {# size t, size s #}" "\(t, s). ground t \ ground s \ t >\<^sub>t s \ s >\<^sub>t t \ t = s" "(t, s)", simplified prod.case], simp only: split_paired_all prod.case atomize_imp[symmetric]) fix t s :: "('s, 'v) tm" assume ih: "\ta sa. {# size ta, size sa #} < {# size t, size s #} \ ground ta \ ground sa \ ta >\<^sub>t sa \ sa >\<^sub>t ta \ ta = sa" and gr_t: "ground t" and gr_s: "ground s" let ?case = "t >\<^sub>t s \ s >\<^sub>t t \ t = s" have vars_t: "vars_mset t \# vars_mset s" and vars_s: "vars_mset s \# vars_mset t" by (simp only: vars_mset_empty_iff[THEN iffD2, OF gr_s] vars_mset_empty_iff[THEN iffD2, OF gr_t])+ show ?case proof (cases "wt t = wt s") case False moreover { assume "wt t > wt s" hence "t >\<^sub>t s" by (rule gt_wt[OF vars_t]) } moreover { assume "wt s > wt t" hence "s >\<^sub>t t" by (rule gt_wt[OF vars_s]) } ultimately show ?thesis by linarith next case wt_t: True note wt_s = wt_t[symmetric] obtain g where \: "head t = Sym g" by (metis ground_head[OF gr_t] hd.collapse(2)) obtain f where \: "head s = Sym f" by (metis ground_head[OF gr_s] hd.collapse(2)) { assume g_gt_f: "g >\<^sub>s f" have "t >\<^sub>t s" by (rule gt_diff[OF vars_t wt_t]) (simp add: \ \ g_gt_f gt_hd_def) } moreover { assume f_gt_g: "f >\<^sub>s g" have "s >\<^sub>t t" by (rule gt_diff[OF vars_s wt_s]) (simp add: \ \ f_gt_g gt_hd_def) } moreover { assume g_eq_f: "g = f" hence hd_t: "head t = head s" using \ \ by force note hd_s = hd_t[symmetric] have gr_ts: "\t \ set (args t). ground t" using gr_t ground_args by auto have gr_ss: "\s \ set (args s). ground s" using gr_s ground_args by auto let ?ts = "args t" let ?ss = "args s" have ?thesis proof (cases "?ts = ?ss") case ts_eq_ss: True show ?thesis using \ \ g_eq_f ts_eq_ss by (simp add: tm_expand_apps) next case False hence "extf g (>\<^sub>t) (args t) ?ss \ extf g (>\<^sub>t) ?ss ?ts" using ih gr_ss gr_ts ext_total.total[OF extf_total, rule_format, of "set ?ts \ set ?ss" "(>\<^sub>t)" ?ts ?ss g] by (metis Un_commute Un_iff in_lists_iff_set less_multiset_doubletons size_in_args sup_ge2) moreover { assume extf: "extf g (>\<^sub>t) ?ts ?ss" have "t >\<^sub>t s" by (rule gt_same[OF vars_t wt_t hd_t]) (simp add: extf \) } moreover { assume extf: "extf g (>\<^sub>t) ?ss ?ts" have "s >\<^sub>t t" by (rule gt_same[OF vars_s wt_s hd_s]) (simp add: extf[unfolded g_eq_f] \) } ultimately show ?thesis by sat qed } ultimately show ?thesis using gt_sym_total by blast qed qed subsection \Well-foundedness\ abbreviation gtw :: "('s, 'v) tm \ ('s, 'v) tm \ bool" (infix ">\<^sub>t\<^sub>w" 50) where "(>\<^sub>t\<^sub>w) \ \t s. wary t \ wary s \ t >\<^sub>t s" abbreviation gtwg :: "('s, 'v) tm \ ('s, 'v) tm \ bool" (infix ">\<^sub>t\<^sub>w\<^sub>g" 50) where "(>\<^sub>t\<^sub>w\<^sub>g) \ \t s. ground t \ t >\<^sub>t\<^sub>w s" lemma ground_gt_unary: assumes gr_t: "ground t" shows "\ gt_unary t s" proof assume gt_unary_t_s: "gt_unary t s" hence "t >\<^sub>t s" using gt_iff_wt_unary_diff_same by blast hence gr_s: "ground s" using gr_t gt_imp_vars by blast have ngr_t_or_s: "\ ground t \ \ ground s" using gt_unary_t_s by cases (blast dest: ground_head not_comp_hd_imp_Var) show False using gr_t gr_s ngr_t_or_s by sat qed theorem gt_wf: "wfP (\s t. t >\<^sub>t\<^sub>w s)" proof - have ground_wfP: "wfP (\s t. t >\<^sub>t\<^sub>w\<^sub>g s)" unfolding wfP_iff_no_inf_chain proof assume "\f. inf_chain (>\<^sub>t\<^sub>w\<^sub>g) f" then obtain t where t_bad: "bad (>\<^sub>t\<^sub>w\<^sub>g) t" unfolding inf_chain_def bad_def by blast let ?ff = "worst_chain (>\<^sub>t\<^sub>w\<^sub>g) (\t s. size t > size s)" note wf_sz = wf_app[OF wellorder_class.wf, of size, simplified] have ffi_ground: "\i. ground (?ff i)" and ffi_wary: "\i. wary (?ff i)" using worst_chain_bad[OF wf_sz t_bad, unfolded inf_chain_def] by fast+ have "inf_chain (>\<^sub>t\<^sub>w\<^sub>g) ?ff" by (rule worst_chain_bad[OF wf_sz t_bad]) hence bad_wt_diff_same: "inf_chain (\t s. ground t \ (gt_wt t s \ gt_diff t s \ gt_same t s)) ?ff" unfolding inf_chain_def using gt_iff_wt_unary_diff_same ground_gt_unary by blast have wf_wt: "wf {(s, t). ground t \ gt_wt t s}" by (rule wf_subset[OF wf_app[of _ wt, OF wf_less]]) (auto simp: gt_wt.simps) have wt_O_diff_same: "{(s, t). ground t \ gt_wt t s} O {(s, t). ground t \ (gt_diff t s \ gt_same t s)} \ {(s, t). ground t \ gt_wt t s}" unfolding gt_wt.simps gt_diff.simps gt_same.simps by auto have wt_diff_same_as_union: "{(s, t). ground t \ (gt_wt t s \ gt_diff t s \ gt_same t s)} = {(s, t). ground t \ gt_wt t s} \ {(s, t). ground t \ (gt_diff t s \ gt_same t s)}" by auto obtain k1 where bad_diff_same: "inf_chain (\t s. ground t \ (gt_diff t s \ gt_same t s)) (\i. ?ff (i + k1))" using wf_infinite_down_chain_compatible[OF wf_wt _ wt_O_diff_same, of ?ff] bad_wt_diff_same unfolding inf_chain_def wt_diff_same_as_union[symmetric] by auto have "wf {(s, t). ground s \ ground t \ sym (head t) >\<^sub>s sym (head s)}" using gt_sym_wf unfolding wfP_def wf_iff_no_infinite_down_chain by fast moreover have "{(s, t). ground t \ gt_diff t s} \ {(s, t). ground s \ ground t \ sym (head t) >\<^sub>s sym (head s)}" proof (clarsimp, intro conjI) fix s t assume gr_t: "ground t" and gt_diff_t_s: "gt_diff t s" thus gr_s: "ground s" using gt_iff_wt_unary_diff_same gt_imp_vars by fastforce show "sym (head t) >\<^sub>s sym (head s)" using gt_diff_t_s by cases (simp add: gt_hd_def gr_s gr_t ground_hd_in_ground_heads) qed ultimately have wf_diff: "wf {(s, t). ground t \ gt_diff t s}" by (rule wf_subset) have diff_O_same: "{(s, t). ground t \ gt_diff t s} O {(s, t). ground t \ gt_same t s} \ {(s, t). ground t \ gt_diff t s}" unfolding gt_diff.simps gt_same.simps by auto have diff_same_as_union: "{(s, t). ground t \ (gt_diff t s \ gt_same t s)} = {(s, t). ground t \ gt_diff t s} \ {(s, t). ground t \ gt_same t s}" by auto obtain k2 where bad_same: "inf_chain (\t s. ground t \ gt_same t s) (\i. ?ff (i + k2))" using wf_infinite_down_chain_compatible[OF wf_diff _ diff_O_same, of "\i. ?ff (i + k1)"] bad_diff_same unfolding inf_chain_def diff_same_as_union[symmetric] by (auto simp: add.assoc) hence hd_sym: "\i. is_Sym (head (?ff (i + k2)))" unfolding inf_chain_def by (simp add: ground_head) define f where "f = sym (head (?ff k2))" have hd_eq_f: "head (?ff (i + k2)) = Sym f" for i unfolding f_def proof (induct i) case 0 thus ?case by (auto simp: hd.collapse(2)[OF hd_sym, of 0, simplified]) next case (Suc ia) thus ?case using bad_same unfolding inf_chain_def gt_same.simps by simp qed define max_args where "max_args = wt (?ff k2)" have wt_eq_max_args: "wt (?ff (i + k2)) = max_args" for i unfolding max_args_def proof (induct i) case (Suc ia) thus ?case using bad_same unfolding inf_chain_def gt_same.simps by simp qed auto have nargs_le_max_args: "num_args (?ff (i + k2)) \ max_args" for i unfolding wt_eq_max_args[of i, symmetric] by (rule wt_ge_num_args[OF ffi_wary]) let ?U_of = "\i. set (args (?ff (i + k2)))" define U where "U = (\i. ?U_of i)" have gr_u: "\u. u \ U \ ground u" unfolding U_def by (blast dest: ground_args[OF _ ffi_ground]) have wary_u: "\u. u \ U \ wary u" unfolding U_def by (blast dest: wary_args[OF _ ffi_wary]) have "\ bad (>\<^sub>t\<^sub>w\<^sub>g) u" if u_in: "u \ ?U_of i" for u i proof assume u_bad: "bad (>\<^sub>t\<^sub>w\<^sub>g) u" have sz_u: "size u < size (?ff (i + k2))" by (rule size_in_args[OF u_in]) show False proof (cases "i + k2") case 0 thus False using sz_u min_worst_chain_0[OF wf_sz u_bad] by simp next case Suc hence gt: "?ff (i + k2 - 1) >\<^sub>t\<^sub>w ?ff (i + k2)" using worst_chain_pred[OF wf_sz t_bad] by auto moreover have "?ff (i + k2) >\<^sub>t\<^sub>w u" using gt gt_proper_sub sub_args sz_u u_in wary_args by auto ultimately have "?ff (i + k2 - 1) >\<^sub>t\<^sub>w u" using gt_trans by blast thus False using Suc sz_u min_worst_chain_Suc[OF wf_sz u_bad] ffi_ground by fastforce qed qed hence u_good: "\u. u \ U \ \ bad (>\<^sub>t\<^sub>w\<^sub>g) u" unfolding U_def by blast let ?gtwu = "\t s. t \ U \ t >\<^sub>t\<^sub>w s" have gtwu_irrefl: "\x. \ ?gtwu x x" using gt_irrefl by auto have "\i j. \t \ set (args (?ff (i + k2))). \s \ set (args (?ff (j + k2))). t >\<^sub>t s \ t \ U \ t >\<^sub>t\<^sub>w s" using wary_u unfolding U_def by blast moreover have "\i. extf f (>\<^sub>t) (args (?ff (i + k2))) (args (?ff (Suc i + k2)))" using bad_same hd_eq_f unfolding inf_chain_def gt_same.simps by auto ultimately have "\i. extf f ?gtwu (args (?ff (i + k2))) (args (?ff (Suc i + k2)))" by (rule extf_mono_strong) hence "inf_chain (extf f ?gtwu) (\i. args (?ff (i + k2)))" unfolding inf_chain_def by blast hence nwf_ext: "\ wfP (\xs ys. length ys \ max_args \ length xs \ max_args \ extf f ?gtwu ys xs)" unfolding inf_chain_def wfP_def wf_iff_no_infinite_down_chain using nargs_le_max_args by fast have gtwu_le_gtwg: "?gtwu \ (>\<^sub>t\<^sub>w\<^sub>g)" by (auto intro!: gr_u) have "wfP (\s t. ?gtwu t s)" unfolding wfP_iff_no_inf_chain proof (intro notI, elim exE) fix f assume bad_f: "inf_chain ?gtwu f" hence bad_f0: "bad ?gtwu (f 0)" by (rule inf_chain_bad) hence "f 0 \ U" using bad_f unfolding inf_chain_def by blast hence "\ bad (>\<^sub>t\<^sub>w\<^sub>g) (f 0)" using u_good by blast hence "\ bad ?gtwu (f 0)" using bad_f inf_chain_bad inf_chain_subset[OF _ gtwu_le_gtwg] by blast thus False using bad_f0 by sat qed hence wf_ext: "wfP (\xs ys. length ys \ max_args \ length xs \ max_args \ extf f ?gtwu ys xs)" using extf_wf_bounded[of ?gtwu] gtwu_irrefl by blast show False using nwf_ext wf_ext by blast qed let ?subst = "subst grounding_\" have "wfP (\s t. ?subst t >\<^sub>t\<^sub>w\<^sub>g ?subst s)" by (rule wfP_app[OF ground_wfP]) hence "wfP (\s t. ?subst t >\<^sub>t\<^sub>w ?subst s)" by (simp add: ground_grounding_\) thus ?thesis by (auto intro: wfP_subset wary_subst_wary[OF wary_grounding_\] gt_subst[OF wary_grounding_\]) qed end end diff --git a/thys/Lambda_Free_RPOs/Lambda_Free_RPO_Std.thy b/thys/Lambda_Free_RPOs/Lambda_Free_RPO_Std.thy --- a/thys/Lambda_Free_RPOs/Lambda_Free_RPO_Std.thy +++ b/thys/Lambda_Free_RPOs/Lambda_Free_RPO_Std.thy @@ -1,826 +1,826 @@ (* Title: The Graceful Recursive Path Order for Lambda-Free Higher-Order Terms Author: Jasmin Blanchette , 2016 Author: Uwe Waldmann , 2016 Author: Daniel Wand , 2016 Maintainer: Jasmin Blanchette *) section \The Graceful Recursive Path Order for Lambda-Free Higher-Order Terms\ theory Lambda_Free_RPO_Std -imports Lambda_Free_Term Extension_Orders +imports Lambda_Free_Term Extension_Orders Nested_Multisets_Ordinals.Multiset_More abbrevs ">t" = ">\<^sub>t" and "\t" = "\\<^sub>t" begin text \ This theory defines the graceful recursive path order (RPO) for \\\-free higher-order terms. \ subsection \Setup\ locale rpo_basis = ground_heads "(>\<^sub>s)" arity_sym arity_var for gt_sym :: "'s \ 's \ bool" (infix ">\<^sub>s" 50) and arity_sym :: "'s \ enat" and arity_var :: "'v \ enat" + fixes extf :: "'s \ (('s, 'v) tm \ ('s, 'v) tm \ bool) \ ('s, 'v) tm list \ ('s, 'v) tm list \ bool" assumes extf_ext_trans_before_irrefl: "ext_trans_before_irrefl (extf f)" and extf_ext_compat_cons: "ext_compat_cons (extf f)" and extf_ext_compat_list: "ext_compat_list (extf f)" begin lemma extf_ext_trans: "ext_trans (extf f)" by (rule ext_trans_before_irrefl.axioms(1)[OF extf_ext_trans_before_irrefl]) lemma extf_ext: "ext (extf f)" by (rule ext_trans.axioms(1)[OF extf_ext_trans]) lemmas extf_mono_strong = ext.mono_strong[OF extf_ext] lemmas extf_mono = ext.mono[OF extf_ext, mono] lemmas extf_map = ext.map[OF extf_ext] lemmas extf_trans = ext_trans.trans[OF extf_ext_trans] lemmas extf_irrefl_from_trans = ext_trans_before_irrefl.irrefl_from_trans[OF extf_ext_trans_before_irrefl] lemmas extf_compat_append_left = ext_compat_cons.compat_append_left[OF extf_ext_compat_cons] lemmas extf_compat_list = ext_compat_list.compat_list[OF extf_ext_compat_list] definition chkvar :: "('s, 'v) tm \ ('s, 'v) tm \ bool" where [simp]: "chkvar t s \ vars_hd (head s) \ vars t" end locale rpo = rpo_basis _ _ arity_sym arity_var for arity_sym :: "'s \ enat" and arity_var :: "'v \ enat" begin subsection \Inductive Definitions\ definition chksubs :: "(('s, 'v) tm \ ('s, 'v) tm \ bool) \ ('s, 'v) tm \ ('s, 'v) tm \ bool" where [simp]: "chksubs gt t s \ (case s of App s1 s2 \ gt t s1 \ gt t s2 | _ \ True)" lemma chksubs_mono[mono]: "gt \ gt' \ chksubs gt \ chksubs gt'" by (auto simp: tm.case_eq_if) force+ inductive gt :: "('s, 'v) tm \ ('s, 'v) tm \ bool" (infix ">\<^sub>t" 50) where gt_sub: "is_App t \ (fun t >\<^sub>t s \ fun t = s) \ (arg t >\<^sub>t s \ arg t = s) \ t >\<^sub>t s" | gt_diff: "head t >\<^sub>h\<^sub>d head s \ chkvar t s \ chksubs (>\<^sub>t) t s \ t >\<^sub>t s" | gt_same: "head t = head s \ chksubs (>\<^sub>t) t s \ (\f \ ground_heads (head t). extf f (>\<^sub>t) (args t) (args s)) \ t >\<^sub>t s" abbreviation ge :: "('s, 'v) tm \ ('s, 'v) tm \ bool" (infix "\\<^sub>t" 50) where "t \\<^sub>t s \ t >\<^sub>t s \ t = s" inductive gt_sub :: "('s, 'v) tm \ ('s, 'v) tm \ bool" where gt_subI: "is_App t \ fun t \\<^sub>t s \ arg t \\<^sub>t s \ gt_sub t s" inductive gt_diff :: "('s, 'v) tm \ ('s, 'v) tm \ bool" where gt_diffI: "head t >\<^sub>h\<^sub>d head s \ chkvar t s \ chksubs (>\<^sub>t) t s \ gt_diff t s" inductive gt_same :: "('s, 'v) tm \ ('s, 'v) tm \ bool" where gt_sameI: "head t = head s \ chksubs (>\<^sub>t) t s \ (\f \ ground_heads (head t). extf f (>\<^sub>t) (args t) (args s)) \ gt_same t s" lemma gt_iff_sub_diff_same: "t >\<^sub>t s \ gt_sub t s \ gt_diff t s \ gt_same t s" by (subst gt.simps) (auto simp: gt_sub.simps gt_diff.simps gt_same.simps) subsection \Transitivity\ lemma gt_fun_imp: "fun t >\<^sub>t s \ t >\<^sub>t s" by (cases t) (auto intro: gt_sub) lemma gt_arg_imp: "arg t >\<^sub>t s \ t >\<^sub>t s" by (cases t) (auto intro: gt_sub) lemma gt_imp_vars: "t >\<^sub>t s \ vars t \ vars s" proof (simp only: atomize_imp, rule measure_induct_rule[of "\(t, s). size t + size s" "\(t, s). t >\<^sub>t s \ vars t \ vars s" "(t, s)", simplified prod.case], simp only: split_paired_all prod.case atomize_imp[symmetric]) fix t s assume ih: "\ta sa. size ta + size sa < size t + size s \ ta >\<^sub>t sa \ vars ta \ vars sa" and t_gt_s: "t >\<^sub>t s" show "vars t \ vars s" using t_gt_s proof cases case gt_sub thus ?thesis using ih[of "fun t" s] ih[of "arg t" s] by (meson add_less_cancel_right subsetD size_arg_lt size_fun_lt subsetI tm.set_sel(5,6)) next case gt_diff show ?thesis proof (cases s) case Hd thus ?thesis using gt_diff(2) by (auto elim: hd.set_cases(2)) next case (App s1 s2) thus ?thesis using gt_diff(3) ih[of t s1] ih[of t s2] by simp qed next case gt_same show ?thesis proof (cases s) case Hd thus ?thesis using gt_same(1) vars_head_subseteq by fastforce next case (App s1 s2) thus ?thesis using gt_same(2) ih[of t s1] ih[of t s2] by simp qed qed qed theorem gt_trans: "u >\<^sub>t t \ t >\<^sub>t s \ u >\<^sub>t s" proof (simp only: atomize_imp, rule measure_induct_rule[of "\(u, t, s). {#size u, size t, size s#}" "\(u, t, s). u >\<^sub>t t \ t >\<^sub>t s \ u >\<^sub>t s" "(u, t, s)", simplified prod.case], simp only: split_paired_all prod.case atomize_imp[symmetric]) fix u t s assume ih: "\ua ta sa. {#size ua, size ta, size sa#} < {#size u, size t, size s#} \ ua >\<^sub>t ta \ ta >\<^sub>t sa \ ua >\<^sub>t sa" and u_gt_t: "u >\<^sub>t t" and t_gt_s: "t >\<^sub>t s" have chkvar: "chkvar u s" by clarsimp (meson u_gt_t t_gt_s gt_imp_vars hd.set_sel(2) vars_head_subseteq subsetCE) have chk_u_s_if: "chksubs (>\<^sub>t) u s" if chk_t_s: "chksubs (>\<^sub>t) t s" proof (cases s) case (App s1 s2) thus ?thesis using chk_t_s by (auto intro: ih[of _ _ s1, OF _ u_gt_t] ih[of _ _ s2, OF _ u_gt_t]) qed auto have fun_u_lt_etc: "is_App u \ {#size (fun u), size t, size s#} < {#size u, size t, size s#}" and arg_u_lt_etc: "is_App u \ {#size (arg u), size t, size s#} < {#size u, size t, size s#}" by (simp_all add: size_fun_lt size_arg_lt) have u_gt_s_if_ui: "is_App u \ fun u \\<^sub>t t \ arg u \\<^sub>t t \ u >\<^sub>t s" using ih[of "fun u" t s, OF fun_u_lt_etc] ih[of "arg u" t s, OF arg_u_lt_etc] gt_arg_imp gt_fun_imp t_gt_s by blast show "u >\<^sub>t s" using t_gt_s proof cases case gt_sub_t_s: gt_sub have u_gt_s_if_chk_u_t: ?thesis if chk_u_t: "chksubs (>\<^sub>t) u t" using gt_sub_t_s(1) proof (cases t) case t: (App t1 t2) show ?thesis using ih[of u t1 s] ih[of u t2 s] gt_sub_t_s(2) chk_u_t unfolding t by auto qed auto show ?thesis using u_gt_t by cases (auto intro: u_gt_s_if_ui u_gt_s_if_chk_u_t) next case gt_diff_t_s: gt_diff show ?thesis using u_gt_t proof cases case gt_diff_u_t: gt_diff have "head u >\<^sub>h\<^sub>d head s" using gt_diff_u_t(1) gt_diff_t_s(1) by (auto intro: gt_hd_trans) thus ?thesis by (rule gt_diff[OF _ chkvar chk_u_s_if[OF gt_diff_t_s(3)]]) next case gt_same_u_t: gt_same have "head u >\<^sub>h\<^sub>d head s" using gt_diff_t_s(1) gt_same_u_t(1) by auto thus ?thesis by (rule gt_diff[OF _ chkvar chk_u_s_if[OF gt_diff_t_s(3)]]) qed (auto intro: u_gt_s_if_ui) next case gt_same_t_s: gt_same show ?thesis using u_gt_t proof cases case gt_diff_u_t: gt_diff have "head u >\<^sub>h\<^sub>d head s" using gt_diff_u_t(1) gt_same_t_s(1) by simp thus ?thesis by (rule gt_diff[OF _ chkvar chk_u_s_if[OF gt_same_t_s(2)]]) next case gt_same_u_t: gt_same have hd_u_s: "head u = head s" using gt_same_u_t(1) gt_same_t_s(1) by simp let ?S = "set (args u) \ set (args t) \ set (args s)" have gt_trans_args: "\ua \ ?S. \ta \ ?S. \sa \ ?S. ua >\<^sub>t ta \ ta >\<^sub>t sa \ ua >\<^sub>t sa" proof clarify fix sa ta ua assume ua_in: "ua \ ?S" and ta_in: "ta \ ?S" and sa_in: "sa \ ?S" and ua_gt_ta: "ua >\<^sub>t ta" and ta_gt_sa: "ta >\<^sub>t sa" show "ua >\<^sub>t sa" by (auto intro!: ih[OF Max_lt_imp_lt_mset ua_gt_ta ta_gt_sa]) (meson ua_in ta_in sa_in Un_iff max.strict_coboundedI1 max.strict_coboundedI2 size_in_args)+ qed have "\f \ ground_heads (head u). extf f (>\<^sub>t) (args u) (args s)" proof (clarify, rule extf_trans[OF _ _ _ gt_trans_args]) fix f assume f_in_grounds: "f \ ground_heads (head u)" show "extf f (>\<^sub>t) (args u) (args t)" using f_in_grounds gt_same_u_t(3) by blast show "extf f (>\<^sub>t) (args t) (args s)" using f_in_grounds gt_same_t_s(3) unfolding gt_same_u_t(1) by blast qed auto thus ?thesis by (rule gt_same[OF hd_u_s chk_u_s_if[OF gt_same_t_s(2)]]) qed (auto intro: u_gt_s_if_ui) qed qed subsection \Irreflexivity\ theorem gt_irrefl: "\ s >\<^sub>t s" proof (standard, induct s rule: measure_induct_rule[of size]) case (less s) note ih = this(1) and s_gt_s = this(2) show False using s_gt_s proof cases case _: gt_sub note is_app = this(1) and si_ge_s = this(2) have s_gt_fun_s: "s >\<^sub>t fun s" and s_gt_arg_s: "s >\<^sub>t arg s" using is_app by (simp_all add: gt_sub) have "fun s >\<^sub>t s \ arg s >\<^sub>t s" using si_ge_s is_app s_gt_arg_s s_gt_fun_s by auto moreover { assume fun_s_gt_s: "fun s >\<^sub>t s" have "fun s >\<^sub>t fun s" by (rule gt_trans[OF fun_s_gt_s s_gt_fun_s]) hence False using ih[of "fun s"] is_app size_fun_lt by blast } moreover { assume arg_s_gt_s: "arg s >\<^sub>t s" have "arg s >\<^sub>t arg s" by (rule gt_trans[OF arg_s_gt_s s_gt_arg_s]) hence False using ih[of "arg s"] is_app size_arg_lt by blast } ultimately show False by sat next case gt_diff thus False by (cases "head s") (auto simp: gt_hd_irrefl) next case gt_same note in_grounds = this(3) obtain si where si_in_args: "si \ set (args s)" and si_gt_si: "si >\<^sub>t si" using in_grounds by (metis (full_types) all_not_in_conv extf_irrefl_from_trans ground_heads_nonempty gt_trans) have "size si < size s" by (rule size_in_args[OF si_in_args]) thus False by (rule ih[OF _ si_gt_si]) qed qed lemma gt_antisym: "t >\<^sub>t s \ \ s >\<^sub>t t" using gt_irrefl gt_trans by blast subsection \Subterm Property\ lemma gt_sub_fun: "App s t >\<^sub>t s" and gt_sub_arg: "App s t >\<^sub>t t" by (auto intro: gt_sub) theorem gt_proper_sub: "proper_sub s t \ t >\<^sub>t s" by (induct t) (auto intro: gt_sub_fun gt_sub_arg gt_trans) subsection \Compatibility with Functions\ lemma gt_compat_fun: assumes t'_gt_t: "t' >\<^sub>t t" shows "App s t' >\<^sub>t App s t" proof - have t'_ne_t: "t' \ t" using gt_antisym t'_gt_t by blast have extf_args_single: "\f \ ground_heads (head s). extf f (>\<^sub>t) (args s @ [t']) (args s @ [t])" by (simp add: extf_compat_list t'_gt_t t'_ne_t) show ?thesis by (rule gt_same) (auto simp: gt_sub gt_sub_fun t'_gt_t intro!: extf_args_single) qed theorem gt_compat_fun_strong: assumes t'_gt_t: "t' >\<^sub>t t" shows "apps s (t' # us) >\<^sub>t apps s (t # us)" proof (induct us rule: rev_induct) case Nil show ?case using t'_gt_t by (auto intro!: gt_compat_fun) next case (snoc u us) note ih = snoc let ?v' = "apps s (t' # us @ [u])" let ?v = "apps s (t # us @ [u])" show ?case proof (rule gt_same) show "chksubs (>\<^sub>t) ?v' ?v" using ih by (auto intro: gt_sub gt_sub_arg) next show "\f \ ground_heads (head ?v'). extf f (>\<^sub>t) (args ?v') (args ?v)" by (metis args_apps extf_compat_list gt_irrefl t'_gt_t) qed simp qed subsection \Compatibility with Arguments\ theorem gt_diff_same_compat_arg: assumes extf_compat_snoc: "\f. ext_compat_snoc (extf f)" and diff_same: "gt_diff s' s \ gt_same s' s" shows "App s' t >\<^sub>t App s t" proof - { assume "s' >\<^sub>t s" hence "App s' t >\<^sub>t s" using gt_sub_fun gt_trans by blast moreover have "App s' t >\<^sub>t t" by (simp add: gt_sub_arg) ultimately have "chksubs (>\<^sub>t) (App s' t) (App s t)" by auto } note chk_s't_st = this show ?thesis using diff_same proof assume "gt_diff s' s" hence s'_gt_s: "s' >\<^sub>t s" and hd_s'_gt_s: "head s' >\<^sub>h\<^sub>d head s" and chkvar_s'_s: "chkvar s' s" and chk_s'_s: "chksubs (>\<^sub>t) s' s" using gt_diff.cases by (auto simp: gt_iff_sub_diff_same) have chkvar_s't_st: "chkvar (App s' t) (App s t)" using chkvar_s'_s by auto show ?thesis by (rule gt_diff[OF _ chkvar_s't_st chk_s't_st[OF s'_gt_s]]) (simp add: hd_s'_gt_s[simplified]) next assume "gt_same s' s" hence s'_gt_s: "s' >\<^sub>t s" and hd_s'_eq_s: "head s' = head s" and chk_s'_s: "chksubs (>\<^sub>t) s' s" and gts_args: "\f \ ground_heads (head s'). extf f (>\<^sub>t) (args s') (args s)" using gt_same.cases by (auto simp: gt_iff_sub_diff_same, metis) have gts_args_t: "\f \ ground_heads (head (App s' t)). extf f (>\<^sub>t) (args (App s' t)) (args (App s t))" using gts_args ext_compat_snoc.compat_append_right[OF extf_compat_snoc] by simp show ?thesis by (rule gt_same[OF _ chk_s't_st[OF s'_gt_s] gts_args_t]) (simp add: hd_s'_eq_s) qed qed subsection \Stability under Substitution\ lemma gt_imp_chksubs_gt: assumes t_gt_s: "t >\<^sub>t s" shows "chksubs (>\<^sub>t) t s" proof - have "is_App s \ t >\<^sub>t fun s \ t >\<^sub>t arg s" using t_gt_s by (meson gt_sub gt_trans) thus ?thesis by (simp add: tm.case_eq_if) qed theorem gt_subst: assumes wary_\: "wary_subst \" shows "t >\<^sub>t s \ subst \ t >\<^sub>t subst \ s" proof (simp only: atomize_imp, rule measure_induct_rule[of "\(t, s). {#size t, size s#}" "\(t, s). t >\<^sub>t s \ subst \ t >\<^sub>t subst \ s" "(t, s)", simplified prod.case], simp only: split_paired_all prod.case atomize_imp[symmetric]) fix t s assume ih: "\ta sa. {#size ta, size sa#} < {#size t, size s#} \ ta >\<^sub>t sa \ subst \ ta >\<^sub>t subst \ sa" and t_gt_s: "t >\<^sub>t s" { assume chk_t_s: "chksubs (>\<^sub>t) t s" have "chksubs (>\<^sub>t) (subst \ t) (subst \ s)" proof (cases s) case s: (Hd \) show ?thesis proof (cases \) case \: (Var x) have psub_x_t: "proper_sub (Hd (Var x)) t" using \ s t_gt_s gt_imp_vars gt_irrefl in_vars_imp_sub by fastforce show ?thesis unfolding \ s by (rule gt_imp_chksubs_gt[OF gt_proper_sub[OF proper_sub_subst]]) (rule psub_x_t) qed (auto simp: s) next case s: (App s1 s2) have "t >\<^sub>t s1" and "t >\<^sub>t s2" using s chk_t_s by auto thus ?thesis using s by (auto intro!: ih[of t s1] ih[of t s2]) qed } note chk_\t_\s_if = this show "subst \ t >\<^sub>t subst \ s" using t_gt_s proof cases case gt_sub_t_s: gt_sub obtain t1 t2 where t: "t = App t1 t2" using gt_sub_t_s(1) by (metis tm.collapse(2)) show ?thesis using gt_sub ih[of t1 s] ih[of t2 s] gt_sub_t_s(2) t by auto next case gt_diff_t_s: gt_diff have "head (subst \ t) >\<^sub>h\<^sub>d head (subst \ s)" by (meson wary_subst_ground_heads gt_diff_t_s(1) gt_hd_def subsetCE wary_\) moreover have "chkvar (subst \ t) (subst \ s)" unfolding chkvar_def using vars_subst_subseteq[OF gt_imp_vars[OF t_gt_s]] vars_head_subseteq by force ultimately show ?thesis by (rule gt_diff[OF _ _ chk_\t_\s_if[OF gt_diff_t_s(3)]]) next case gt_same_t_s: gt_same have hd_\t_eq_\s: "head (subst \ t) = head (subst \ s)" using gt_same_t_s(1) by simp { fix f assume f_in_grounds: "f \ ground_heads (head (subst \ t))" let ?S = "set (args t) \ set (args s)" have extf_args_s_t: "extf f (>\<^sub>t) (args t) (args s)" using gt_same_t_s(3) f_in_grounds wary_\ wary_subst_ground_heads by blast have "extf f (>\<^sub>t) (map (subst \) (args t)) (map (subst \) (args s))" proof (rule extf_map[of ?S, OF _ _ _ _ _ _ extf_args_s_t]) have sz_a: "\ta \ ?S. \sa \ ?S. {#size ta, size sa#} < {#size t, size s#}" by (fastforce intro: Max_lt_imp_lt_mset dest: size_in_args) show "\ta \ ?S. \sa \ ?S. ta >\<^sub>t sa \ subst \ ta >\<^sub>t subst \ sa" using ih sz_a size_in_args by fastforce qed (auto intro!: gt_irrefl elim!: gt_trans) hence "extf f (>\<^sub>t) (args (subst \ t)) (args (subst \ s))" by (auto simp: gt_same_t_s(1) intro: extf_compat_append_left) } hence "\f \ ground_heads (head (subst \ t)). extf f (>\<^sub>t) (args (subst \ t)) (args (subst \ s))" by blast thus ?thesis by (rule gt_same[OF hd_\t_eq_\s chk_\t_\s_if[OF gt_same_t_s(2)]]) qed qed subsection \Totality on Ground Terms\ theorem gt_total_ground: assumes extf_total: "\f. ext_total (extf f)" shows "ground t \ ground s \ t >\<^sub>t s \ s >\<^sub>t t \ t = s" proof (simp only: atomize_imp, rule measure_induct_rule[of "\(t, s). {# size t, size s #}" "\(t, s). ground t \ ground s \ t >\<^sub>t s \ s >\<^sub>t t \ t = s" "(t, s)", simplified prod.case], simp only: split_paired_all prod.case atomize_imp[symmetric]) fix t s :: "('s, 'v) tm" assume ih: "\ta sa. {# size ta, size sa #} < {# size t, size s #} \ ground ta \ ground sa \ ta >\<^sub>t sa \ sa >\<^sub>t ta \ ta = sa" and gr_t: "ground t" and gr_s: "ground s" let ?case = "t >\<^sub>t s \ s >\<^sub>t t \ t = s" have "chksubs (>\<^sub>t) t s \ s >\<^sub>t t" unfolding chksubs_def tm.case_eq_if using ih[of t "fun s"] ih[of t "arg s"] mset_lt_single_iff by (metis add_mset_lt_right_lt gr_s gr_t ground_arg ground_fun gt_sub size_arg_lt size_fun_lt) moreover have "chksubs (>\<^sub>t) s t \ t >\<^sub>t s" unfolding chksubs_def tm.case_eq_if using ih[of "fun t" s] ih[of "arg t" s] by (metis add_mset_lt_left_lt gr_s gr_t ground_arg ground_fun gt_sub size_arg_lt size_fun_lt) moreover { assume chksubs_t_s: "chksubs (>\<^sub>t) t s" and chksubs_s_t: "chksubs (>\<^sub>t) s t" obtain g where g: "head t = Sym g" using gr_t by (metis ground_head hd.collapse(2)) obtain f where f: "head s = Sym f" using gr_s by (metis ground_head hd.collapse(2)) have chkvar_t_s: "chkvar t s" and chkvar_s_t: "chkvar s t" using g f by simp_all { assume g_gt_f: "g >\<^sub>s f" have "t >\<^sub>t s" by (rule gt_diff[OF _ chkvar_t_s chksubs_t_s]) (simp add: g f gt_sym_imp_hd[OF g_gt_f]) } moreover { assume f_gt_g: "f >\<^sub>s g" have "s >\<^sub>t t" by (rule gt_diff[OF _ chkvar_s_t chksubs_s_t]) (simp add: g f gt_sym_imp_hd[OF f_gt_g]) } moreover { assume g_eq_f: "g = f" hence hd_t: "head t = head s" using g f by auto let ?ts = "args t" let ?ss = "args s" have gr_ts: "\ta \ set ?ts. ground ta" using ground_args[OF _ gr_t] by blast have gr_ss: "\sa \ set ?ss. ground sa" using ground_args[OF _ gr_s] by blast { assume ts_eq_ss: "?ts = ?ss" have "t = s" using hd_t ts_eq_ss by (rule tm_expand_apps) } moreover { assume ts_gt_ss: "extf g (>\<^sub>t) ?ts ?ss" have "t >\<^sub>t s" by (rule gt_same[OF hd_t chksubs_t_s]) (auto simp: g ts_gt_ss) } moreover { assume ss_gt_ts: "extf g (>\<^sub>t) ?ss ?ts" have "s >\<^sub>t t" by (rule gt_same[OF hd_t[symmetric] chksubs_s_t]) (auto simp: f[folded g_eq_f] ss_gt_ts) } ultimately have ?case using ih gr_ss gr_ts ext_total.total[OF extf_total, rule_format, of "set ?ts \ set ?ss" "(>\<^sub>t)" ?ts ?ss g] by (metis Un_iff in_listsI less_multiset_doubletons size_in_args) } ultimately have ?case using gt_sym_total by blast } ultimately show ?case by fast qed subsection \Well-foundedness\ abbreviation gtg :: "('s, 'v) tm \ ('s, 'v) tm \ bool" (infix ">\<^sub>t\<^sub>g" 50) where "(>\<^sub>t\<^sub>g) \ \t s. ground t \ t >\<^sub>t s" theorem gt_wf: assumes extf_wf: "\f. ext_wf (extf f)" shows "wfP (\s t. t >\<^sub>t s)" proof - have ground_wfP: "wfP (\s t. t >\<^sub>t\<^sub>g s)" unfolding wfP_iff_no_inf_chain proof assume "\f. inf_chain (>\<^sub>t\<^sub>g) f" then obtain t where t_bad: "bad (>\<^sub>t\<^sub>g) t" unfolding inf_chain_def bad_def by blast let ?ff = "worst_chain (>\<^sub>t\<^sub>g) (\t s. size t > size s)" let ?U_of = "\i. if is_App (?ff i) then {fun (?ff i)} \ set (args (?ff i)) else {}" note wf_sz = wf_app[OF wellorder_class.wf, of size, simplified] define U where "U = (\i. ?U_of i)" have gr: "\i. ground (?ff i)" using worst_chain_bad[OF wf_sz t_bad, unfolded inf_chain_def] by fast have gr_fun: "\i. ground (fun (?ff i))" by (rule ground_fun[OF gr]) have gr_args: "\i s. s \ set (args (?ff i)) \ ground s" by (rule ground_args[OF _ gr]) have gr_u: "\u. u \ U \ ground u" unfolding U_def by (auto dest: gr_args) (metis (lifting) empty_iff gr_fun) have "\ bad (>\<^sub>t\<^sub>g) u" if u_in: "u \ ?U_of i" for u i proof let ?ti = "?ff i" assume u_bad: "bad (>\<^sub>t\<^sub>g) u" have sz_u: "size u < size ?ti" proof (cases "?ff i") case Hd thus ?thesis using u_in size_in_args by fastforce next case App thus ?thesis using u_in size_in_args insert_iff size_fun_lt by fastforce qed show False proof (cases i) case 0 thus False using sz_u min_worst_chain_0[OF wf_sz u_bad] by simp next case Suc hence "?ff (i - 1) >\<^sub>t ?ff i" using worst_chain_pred[OF wf_sz t_bad] by simp moreover have "?ff i >\<^sub>t u" proof - have u_in: "u \ ?U_of i" using u_in by blast have ffi_ne_u: "?ff i \ u" using sz_u by fastforce hence "is_App (?ff i) \ \ sub u (?ff i) \ ?ff i >\<^sub>t u" using u_in gt_sub sub_args by auto thus "?ff i >\<^sub>t u" using ffi_ne_u u_in gt_proper_sub sub_args by fastforce qed ultimately have "?ff (i - 1) >\<^sub>t u" by (rule gt_trans) thus False using Suc sz_u min_worst_chain_Suc[OF wf_sz u_bad] gr by fastforce qed qed hence u_good: "\u. u \ U \ \ bad (>\<^sub>t\<^sub>g) u" unfolding U_def by blast have bad_diff_same: "inf_chain (\t s. ground t \ (gt_diff t s \ gt_same t s)) ?ff" unfolding inf_chain_def proof (intro allI conjI) fix i show "ground (?ff i)" by (rule gr) have gt: "?ff i >\<^sub>t ?ff (Suc i)" using worst_chain_pred[OF wf_sz t_bad] by blast have "\ gt_sub (?ff i) (?ff (Suc i))" proof assume a: "gt_sub (?ff i) (?ff (Suc i))" hence fi_app: "is_App (?ff i)" and fun_or_arg_fi_ge: "fun (?ff i) \\<^sub>t ?ff (Suc i) \ arg (?ff i) \\<^sub>t ?ff (Suc i)" unfolding gt_sub.simps by blast+ have "fun (?ff i) \ ?U_of i" unfolding U_def using fi_app by auto moreover have "arg (?ff i) \ ?U_of i" unfolding U_def using fi_app arg_in_args by force ultimately obtain uij where uij_in: "uij \ U" and uij_cases: "uij \\<^sub>t ?ff (Suc i)" unfolding U_def using fun_or_arg_fi_ge by blast have "\n. ?ff n >\<^sub>t ?ff (Suc n)" by (rule worst_chain_pred[OF wf_sz t_bad, THEN conjunct2]) hence uij_gt_i_plus_3: "uij >\<^sub>t ?ff (Suc (Suc i))" using gt_trans uij_cases by blast have "inf_chain (>\<^sub>t\<^sub>g) (\j. if j = 0 then uij else ?ff (Suc (i + j)))" unfolding inf_chain_def by (auto intro!: gr gr_u[OF uij_in] uij_gt_i_plus_3 worst_chain_pred[OF wf_sz t_bad]) hence "bad (>\<^sub>t\<^sub>g) uij" unfolding bad_def by fastforce thus False using u_good[OF uij_in] by sat qed thus "gt_diff (?ff i) (?ff (Suc i)) \ gt_same (?ff i) (?ff (Suc i))" using gt unfolding gt_iff_sub_diff_same by sat qed have "wf {(s, t). ground s \ ground t \ sym (head t) >\<^sub>s sym (head s)}" using gt_sym_wf unfolding wfP_def wf_iff_no_infinite_down_chain by fast moreover have "{(s, t). ground t \ gt_diff t s} \ {(s, t). ground s \ ground t \ sym (head t) >\<^sub>s sym (head s)}" proof (clarsimp, intro conjI) fix s t assume gr_t: "ground t" and gt_diff_t_s: "gt_diff t s" thus gr_s: "ground s" using gt_iff_sub_diff_same gt_imp_vars by fastforce show "sym (head t) >\<^sub>s sym (head s)" using gt_diff_t_s ground_head[OF gr_s] ground_head[OF gr_t] by (cases; cases "head s"; cases "head t") (auto simp: gt_hd_def) qed ultimately have wf_diff: "wf {(s, t). ground t \ gt_diff t s}" by (rule wf_subset) have diff_O_same: "{(s, t). ground t \ gt_diff t s} O {(s, t). ground t \ gt_same t s} \ {(s, t). ground t \ gt_diff t s}" unfolding gt_diff.simps gt_same.simps by clarsimp (metis chksubs_def empty_subsetI gt_diff[unfolded chkvar_def] gt_imp_chksubs_gt gt_same gt_trans) have diff_same_as_union: "{(s, t). ground t \ (gt_diff t s \ gt_same t s)} = {(s, t). ground t \ gt_diff t s} \ {(s, t). ground t \ gt_same t s}" by auto obtain k where bad_same: "inf_chain (\t s. ground t \ gt_same t s) (\i. ?ff (i + k))" using wf_infinite_down_chain_compatible[OF wf_diff _ diff_O_same, of ?ff] bad_diff_same unfolding inf_chain_def diff_same_as_union[symmetric] by auto hence hd_sym: "\i. is_Sym (head (?ff (i + k)))" unfolding inf_chain_def by (simp add: ground_head) define f where "f = sym (head (?ff k))" have hd_eq_f: "head (?ff (i + k)) = Sym f" for i proof (induct i) case 0 thus ?case by (auto simp: f_def hd.collapse(2)[OF hd_sym, of 0, simplified]) next case (Suc ia) thus ?case using bad_same unfolding inf_chain_def gt_same.simps by simp qed let ?gtu = "\t s. t \ U \ t >\<^sub>t s" have "t \ set (args (?ff i)) \ t \ ?U_of i" for t i unfolding U_def by (cases "is_App (?ff i)", simp_all, metis (lifting) neq_iff size_in_args sub.cases sub_args tm.discI(2)) moreover have "\i. extf f (>\<^sub>t) (args (?ff (i + k))) (args (?ff (Suc i + k)))" using bad_same hd_eq_f unfolding inf_chain_def gt_same.simps by auto ultimately have "\i. extf f ?gtu (args (?ff (i + k))) (args (?ff (Suc i + k)))" using extf_mono_strong[of _ _ "(>\<^sub>t)" "\t s. t \ U \ t >\<^sub>t s"] unfolding U_def by blast hence "inf_chain (extf f ?gtu) (\i. args (?ff (i + k)))" unfolding inf_chain_def by blast hence nwf_ext: "\ wfP (\xs ys. extf f ?gtu ys xs)" unfolding wfP_iff_no_inf_chain by fast have gtu_le_gtg: "?gtu \ (>\<^sub>t\<^sub>g)" by (auto intro!: gr_u) have "wfP (\s t. ?gtu t s)" unfolding wfP_iff_no_inf_chain proof (intro notI, elim exE) fix f assume bad_f: "inf_chain ?gtu f" hence bad_f0: "bad ?gtu (f 0)" by (rule inf_chain_bad) have "f 0 \ U" using bad_f unfolding inf_chain_def by blast hence good_f0: "\ bad ?gtu (f 0)" using u_good bad_f inf_chain_bad inf_chain_subset[OF _ gtu_le_gtg] by blast show False using bad_f0 good_f0 by sat qed hence wf_ext: "wfP (\xs ys. extf f ?gtu ys xs)" by (rule ext_wf.wf[OF extf_wf, rule_format]) show False using nwf_ext wf_ext by blast qed let ?subst = "subst grounding_\" have "wfP (\s t. ?subst t >\<^sub>t\<^sub>g ?subst s)" by (rule wfP_app[OF ground_wfP]) hence "wfP (\s t. ?subst t >\<^sub>t ?subst s)" by (simp add: ground_grounding_\) thus ?thesis by (auto intro: wfP_subset gt_subst[OF wary_grounding_\]) qed end end