summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Lex/Prefix.ML

author | paulson |

Wed, 07 Oct 1998 10:31:30 +0200 | |

changeset 5619 | 76a8c72e3fd4 |

parent 5609 | 03d74c85a818 |

child 6675 | 63e53327f5e5 |

permissions | -rw-r--r-- |

new theorems

(* Title: HOL/Lex/Prefix.thy ID: $Id$ Author: Richard Mayr & Tobias Nipkow Copyright 1995 TUM *) (** <= is a partial order: **) Goalw [prefix_def] "xs <= (xs::'a list)"; by (Simp_tac 1); qed "prefix_refl"; AddIffs[prefix_refl]; Goalw [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= zs |] ==> xs <= zs"; by (Clarify_tac 1); by (Simp_tac 1); qed "prefix_trans"; Goalw [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= xs |] ==> xs = ys"; by (Clarify_tac 1); by (Asm_full_simp_tac 1); qed "prefix_antisym"; (** recursion equations **) Goalw [prefix_def] "[] <= xs"; by (simp_tac (simpset() addsimps [eq_sym_conv]) 1); qed "Nil_prefix"; AddIffs[Nil_prefix]; Goalw [prefix_def] "(xs <= []) = (xs = [])"; by (induct_tac "xs" 1); by (Simp_tac 1); by (Simp_tac 1); qed "prefix_Nil"; Addsimps [prefix_Nil]; Goalw [prefix_def] "(xs <= ys@[y]) = (xs = ys@[y] | xs <= ys)"; by (rtac iffI 1); by (etac exE 1); by (rename_tac "zs" 1); by (res_inst_tac [("xs","zs")] rev_exhaust 1); by (Asm_full_simp_tac 1); by (hyp_subst_tac 1); by (asm_full_simp_tac (simpset() delsimps [append_assoc] addsimps [append_assoc RS sym])1); by (etac disjE 1); by (Asm_simp_tac 1); by (Clarify_tac 1); by (Simp_tac 1); qed "prefix_snoc"; Addsimps [prefix_snoc]; Goalw [prefix_def] "(x#xs <= y#ys) = (x=y & xs<=ys)"; by (Simp_tac 1); by (Fast_tac 1); qed"Cons_prefix_Cons"; Addsimps [Cons_prefix_Cons]; Goal "(xs@ys <= xs@zs) = (ys <= zs)"; by (induct_tac "xs" 1); by (ALLGOALS Asm_simp_tac); qed "same_prefix_prefix"; Addsimps [same_prefix_prefix]; AddIffs (* (xs@ys <= xs) = (ys <= []) *) [simplify (simpset()) (read_instantiate [("zs","[]")] same_prefix_prefix)]; Goalw [prefix_def] "xs <= ys ==> xs <= ys@zs"; by (Clarify_tac 1); by (Simp_tac 1); qed "prefix_prefix"; Addsimps [prefix_prefix]; Goalw [prefix_def] "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))"; by (exhaust_tac "xs" 1); by Auto_tac; qed "prefix_Cons"; Goal "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))"; by (res_inst_tac [("xs","zs")] rev_induct 1); by (Simp_tac 1); by (Blast_tac 1); by (asm_full_simp_tac (simpset() delsimps [append_assoc] addsimps [append_assoc RS sym])1); by (Simp_tac 1); by (Blast_tac 1); qed "prefix_append"; Goalw [prefix_def] "[| xs <= ys; length xs < length ys |] ==> xs @ [ys ! length xs] <= ys"; by (auto_tac(claset(), simpset() addsimps [nth_append])); by (exhaust_tac "ys" 1); by Auto_tac; qed "append_one_prefix"; Goalw [prefix_def] "xs <= ys ==> length xs <= length ys"; by Auto_tac; qed "prefix_length_le";