(* Title: HOL/Lambda/ListOrder.thy ID: $Id: ListOrder.thy,v 1.10 2005/06/17 14:13:08 haftmann Exp $ Author: Tobias Nipkow Copyright 1998 TU Muenchen *) header {* Lifting an order to lists of elements *} theory ListOrder imports Accessible_Part begin text {* Lifting an order to lists of elements, relating exactly one element. *} constdefs step1 :: "('a × 'a) set => ('a list × 'a list) set" "step1 r == {(ys, xs). ∃us z z' vs. xs = us @ z # vs ∧ (z', z) ∈ r ∧ ys = us @ z' # vs}" lemma step1_converse [simp]: "step1 (r^-1) = (step1 r)^-1" apply (unfold step1_def) apply blast done lemma in_step1_converse [iff]: "(p ∈ step1 (r^-1)) = (p ∈ (step1 r)^-1)" apply auto done lemma not_Nil_step1 [iff]: "([], xs) ∉ step1 r" apply (unfold step1_def) apply blast done lemma not_step1_Nil [iff]: "(xs, []) ∉ step1 r" apply (unfold step1_def) apply blast done lemma Cons_step1_Cons [iff]: "((y # ys, x # xs) ∈ step1 r) = ((y, x) ∈ r ∧ xs = ys ∨ x = y ∧ (ys, xs) ∈ step1 r)" apply (unfold step1_def) apply simp apply (rule iffI) apply (erule exE) apply (rename_tac ts) apply (case_tac ts) apply fastsimp apply force apply (erule disjE) apply blast apply (blast intro: Cons_eq_appendI) done lemma append_step1I: "(ys, xs) ∈ step1 r ∧ vs = us ∨ ys = xs ∧ (vs, us) ∈ step1 r ==> (ys @ vs, xs @ us) : step1 r" apply (unfold step1_def) apply auto apply blast apply (blast intro: append_eq_appendI) done lemma Cons_step1E [rule_format, elim!]: "[| (ys, x # xs) ∈ step1 r; ∀y. ys = y # xs --> (y, x) ∈ r --> R; ∀zs. ys = x # zs --> (zs, xs) ∈ step1 r --> R |] ==> R" apply (case_tac ys) apply (simp add: step1_def) apply blast done lemma Snoc_step1_SnocD: "(ys @ [y], xs @ [x]) ∈ step1 r ==> ((ys, xs) ∈ step1 r ∧ y = x ∨ ys = xs ∧ (y, x) ∈ r)" apply (unfold step1_def) apply simp apply (clarify del: disjCI) apply (rename_tac vs) apply (rule_tac xs = vs in rev_exhaust) apply force apply simp apply blast done lemma Cons_acc_step1I [rule_format, intro!]: "x ∈ acc r ==> ∀xs. xs ∈ acc (step1 r) --> x # xs ∈ acc (step1 r)" apply (erule acc_induct) apply (erule thin_rl) apply clarify apply (erule acc_induct) apply (rule accI) apply blast done lemma lists_accD: "xs ∈ lists (acc r) ==> xs ∈ acc (step1 r)" apply (erule lists.induct) apply (rule accI) apply simp apply (rule accI) apply (fast dest: acc_downward) done lemma ex_step1I: "[| x ∈ set xs; (y, x) ∈ r |] ==> ∃ys. (ys, xs) ∈ step1 r ∧ y ∈ set ys" apply (unfold step1_def) apply (drule in_set_conv_decomp [THEN iffD1]) apply force done lemma lists_accI: "xs ∈ acc (step1 r) ==> xs ∈ lists (acc r)" apply (erule acc_induct) apply clarify apply (rule accI) apply (drule ex_step1I, assumption) apply blast done end
lemma step1_converse:
step1 (r^-1) = (step1 r)^-1
lemma in_step1_converse:
(p ∈ step1 (r^-1)) = (p ∈ (step1 r)^-1)
lemma not_Nil_step1:
([], xs) ∉ step1 r
lemma not_step1_Nil:
(xs, []) ∉ step1 r
lemma Cons_step1_Cons:
((y # ys, x # xs) ∈ step1 r) = ((y, x) ∈ r ∧ xs = ys ∨ x = y ∧ (ys, xs) ∈ step1 r)
lemma append_step1I:
(ys, xs) ∈ step1 r ∧ vs = us ∨ ys = xs ∧ (vs, us) ∈ step1 r ==> (ys @ vs, xs @ us) ∈ step1 r
lemma Cons_step1E:
[| (ys, x # xs) ∈ step1 r; !!y. [| ys = y # xs; (y, x) ∈ r |] ==> R; !!zs. [| ys = x # zs; (zs, xs) ∈ step1 r |] ==> R |] ==> R
lemma Snoc_step1_SnocD:
(ys @ [y], xs @ [x]) ∈ step1 r ==> (ys, xs) ∈ step1 r ∧ y = x ∨ ys = xs ∧ (y, x) ∈ r
lemma Cons_acc_step1I:
[| x ∈ acc r; xs ∈ acc (step1 r) |] ==> x # xs ∈ acc (step1 r)
lemma lists_accD:
xs ∈ lists (acc r) ==> xs ∈ acc (step1 r)
lemma ex_step1I:
[| x ∈ set xs; (y, x) ∈ r |] ==> ∃ys. (ys, xs) ∈ step1 r ∧ y ∈ set ys
lemma lists_accI:
xs ∈ acc (step1 r) ==> xs ∈ lists (acc r)