1(* Title: HOL/Proofs/Lambda/ListOrder.thy 2 Author: Tobias Nipkow 3 Copyright 1998 TU Muenchen 4*) 5 6section \<open>Lifting an order to lists of elements\<close> 7 8theory ListOrder 9imports Main 10begin 11 12declare [[syntax_ambiguity_warning = false]] 13 14 15text \<open> 16 Lifting an order to lists of elements, relating exactly one 17 element. 18\<close> 19 20definition 21 step1 :: "('a => 'a => bool) => 'a list => 'a list => bool" where 22 "step1 r = 23 (\<lambda>ys xs. \<exists>us z z' vs. xs = us @ z # vs \<and> r z' z \<and> ys = 24 us @ z' # vs)" 25 26 27lemma step1_converse [simp]: "step1 (r\<inverse>\<inverse>) = (step1 r)\<inverse>\<inverse>" 28 apply (unfold step1_def) 29 apply (blast intro!: order_antisym) 30 done 31 32lemma in_step1_converse [iff]: "(step1 (r\<inverse>\<inverse>) x y) = ((step1 r)\<inverse>\<inverse> x y)" 33 apply auto 34 done 35 36lemma not_Nil_step1 [iff]: "\<not> step1 r [] xs" 37 apply (unfold step1_def) 38 apply blast 39 done 40 41lemma not_step1_Nil [iff]: "\<not> step1 r xs []" 42 apply (unfold step1_def) 43 apply blast 44 done 45 46lemma Cons_step1_Cons [iff]: 47 "(step1 r (y # ys) (x # xs)) = 48 (r y x \<and> xs = ys \<or> x = y \<and> step1 r ys xs)" 49 apply (unfold step1_def) 50 apply (rule iffI) 51 apply (erule exE) 52 apply (rename_tac ts) 53 apply (case_tac ts) 54 apply fastforce 55 apply force 56 apply (erule disjE) 57 apply blast 58 apply (blast intro: Cons_eq_appendI) 59 done 60 61lemma append_step1I: 62 "step1 r ys xs \<and> vs = us \<or> ys = xs \<and> step1 r vs us 63 ==> step1 r (ys @ vs) (xs @ us)" 64 apply (unfold step1_def) 65 apply auto 66 apply blast 67 apply (blast intro: append_eq_appendI) 68 done 69 70lemma Cons_step1E [elim!]: 71 assumes "step1 r ys (x # xs)" 72 and "!!y. ys = y # xs \<Longrightarrow> r y x \<Longrightarrow> R" 73 and "!!zs. ys = x # zs \<Longrightarrow> step1 r zs xs \<Longrightarrow> R" 74 shows R 75 using assms 76 apply (cases ys) 77 apply (simp add: step1_def) 78 apply blast 79 done 80 81lemma Snoc_step1_SnocD: 82 "step1 r (ys @ [y]) (xs @ [x]) 83 ==> (step1 r ys xs \<and> y = x \<or> ys = xs \<and> r y x)" 84 apply (unfold step1_def) 85 apply (clarify del: disjCI) 86 apply (rename_tac vs) 87 apply (rule_tac xs = vs in rev_exhaust) 88 apply force 89 apply simp 90 apply blast 91 done 92 93lemma Cons_acc_step1I [intro!]: 94 "Wellfounded.accp r x ==> Wellfounded.accp (step1 r) xs \<Longrightarrow> Wellfounded.accp (step1 r) (x # xs)" 95 apply (induct arbitrary: xs set: Wellfounded.accp) 96 apply (erule thin_rl) 97 apply (erule accp_induct) 98 apply (rule accp.accI) 99 apply blast 100 done 101 102lemma lists_accD: "listsp (Wellfounded.accp r) xs ==> Wellfounded.accp (step1 r) xs" 103 apply (induct set: listsp) 104 apply (rule accp.accI) 105 apply simp 106 apply (rule accp.accI) 107 apply (fast dest: accp_downward) 108 done 109 110lemma ex_step1I: 111 "[| x \<in> set xs; r y x |] 112 ==> \<exists>ys. step1 r ys xs \<and> y \<in> set ys" 113 apply (unfold step1_def) 114 apply (drule in_set_conv_decomp [THEN iffD1]) 115 apply force 116 done 117 118lemma lists_accI: "Wellfounded.accp (step1 r) xs ==> listsp (Wellfounded.accp r) xs" 119 apply (induct set: Wellfounded.accp) 120 apply clarify 121 apply (rule accp.accI) 122 apply (drule_tac r=r in ex_step1I, assumption) 123 apply blast 124 done 125 126end 127