# HG changeset patch
# User nipkow
# Date 902577656 -7200
# Node ID f4d16517b3604903ff49fde13bf99f00641df22b
# Parent  6055775a151bae863ae6f988b20e1eadfead6943
List now contains some lexicographic orderings.

diff -r 6055775a151b -r f4d16517b360 src/HOL/List.ML
--- a/src/HOL/List.ML	Thu Aug 06 18:21:14 1998 +0200
+++ b/src/HOL/List.ML	Sat Aug 08 14:00:56 1998 +0200
@@ -848,6 +848,73 @@
 Addsimps [set_replicate];
 
 
+(*** Lexcicographic orderings on lists ***)
+section"Lexcicographic orderings on lists";
+
+Goal "wf r ==> wf(lexn r n)";
+by(induct_tac "n" 1);
+by(Simp_tac 1);
+by(Simp_tac 1);
+br wf_subset 1;
+br Int_lower1 2;
+br wf_prod_fun_image 1;
+br injI 2;
+by(Auto_tac);
+qed "wf_lexn";
+
+Goal "!xs ys. (xs,ys) : lexn r n --> length xs = n & length ys = n";
+by(induct_tac "n" 1);
+by(Auto_tac);
+qed_spec_mp "lexn_length";
+
+Goalw [lex_def] "wf r ==> wf(lex r)";
+br wf_UN 1;
+by(blast_tac (claset() addIs [wf_lexn]) 1);
+by(Clarify_tac 1);
+by(rename_tac "m n" 1);
+by(subgoal_tac "m ~= n" 1);
+ by(Blast_tac 2);
+by(blast_tac (claset() addDs [lexn_length,not_sym]) 1);
+qed "wf_lex";
+AddSIs [wf_lex];
+
+Goal
+ "lexn r n = \
+\ {(xs,ys). length xs = n & length ys = n & \
+\           (? xys x y xs' ys'. xs= xys @ x#xs' & ys= xys @ y#ys' & (x,y):r)}";
+by(induct_tac "n" 1);
+ by(Simp_tac 1);
+ by(Blast_tac 1);
+by(asm_full_simp_tac (simpset() addsimps [lex_prod_def]) 1);
+by(Auto_tac);
+  by(Blast_tac 1);
+ by(rename_tac "a xys x xs' y ys'" 1);
+ by(res_inst_tac [("x","a#xys")] exI 1);
+ by(Simp_tac 1);
+by(exhaust_tac "xys" 1);
+ by(ALLGOALS Asm_full_simp_tac);
+by(Blast_tac 1);
+qed "lexn_conv";
+
+Goalw [lex_def]
+ "lex r = \
+\ {(xs,ys). length xs = length ys & \
+\           (? xys x y xs' ys'. xs= xys @ x#xs' & ys= xys @ y#ys' & (x,y):r)}";
+by(force_tac (claset(), simpset() addsimps [lexn_conv]) 1);
+qed "lex_conv";
+
+Goalw [lexico_def] "wf r ==> wf(lexico r)";
+by(Blast_tac 1);
+qed "wf_lexico";
+AddSIs [wf_lexico];
+
+Goalw
+ [lexico_def,diag_def,lex_prod_def,measure_def,inv_image_def]
+"lexico r = {(xs,ys). length xs < length ys | \
+\                     length xs = length ys & (xs,ys) : lex r}";
+by(Simp_tac 1);
+qed "lexico_conv";
+
 (***
 Simplification procedure for all list equalities.
 Currently only tries to rearranges @ to see if
diff -r 6055775a151b -r f4d16517b360 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Aug 06 18:21:14 1998 +0200
+++ b/src/HOL/List.thy	Sat Aug 08 14:00:56 1998 +0200
@@ -145,6 +145,22 @@
   replicate_0   "replicate 0 x       = []"
   replicate_Suc "replicate (Suc n) x = x # replicate n x"
 
+(** Lexcicographic orderings on lists **)
+
+consts
+ lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"
+primrec
+"lexn r 0       = {}"
+"lexn r (Suc n) = (prod_fun (split op#) (split op#) `` (r ** lexn r n)) Int
+                  {(xs,ys). length xs = Suc n & length ys = Suc n}"
+
+constdefs
+ lex :: "('a * 'a)set => ('a list * 'a list)set"
+"lex r == UN n. lexn r n"
+
+ lexico :: "('a * 'a)set => ('a list * 'a list)set"
+"lexico r == inv_image (less_than ** lex r) (%xs. (length xs, xs))"
+
 end
 
 ML
diff -r 6055775a151b -r f4d16517b360 src/HOL/Trancl.ML
--- a/src/HOL/Trancl.ML	Thu Aug 06 18:21:14 1998 +0200
+++ b/src/HOL/Trancl.ML	Sat Aug 08 14:00:56 1998 +0200
@@ -138,8 +138,7 @@
 qed "rtrancl_Un_rtrancl";
 
 Goal "(R^=)^* = R^*";
-by (blast_tac (claset() addSIs [rtrancl_subset]
-                       addIs  [rtrancl_refl, r_into_rtrancl]) 1);
+by (blast_tac (claset() addSIs [rtrancl_subset] addIs [r_into_rtrancl]) 1);
 qed "rtrancl_reflcl";
 Addsimps [rtrancl_reflcl];
 
diff -r 6055775a151b -r f4d16517b360 src/HOL/WF.ML
--- a/src/HOL/WF.ML	Thu Aug 06 18:21:14 1998 +0200
+++ b/src/HOL/WF.ML	Sat Aug 08 14:00:56 1998 +0200
@@ -105,7 +105,7 @@
 Goal "wf({})";
 by (simp_tac (simpset() addsimps [wf_def]) 1);
 qed "wf_empty";
-AddSIs [wf_empty];
+AddIffs [wf_empty];
 
 (*---------------------------------------------------------------------------
  * Wellfoundedness of `insert'
@@ -134,6 +134,74 @@
 qed "wf_insert";
 AddIffs [wf_insert];
 
+(*---------------------------------------------------------------------------
+ * Wellfoundedness of `disjoint union'
+ *---------------------------------------------------------------------------*)
+
+Goal
+ "[| !i:I. wf(r i); \
+\    !i:I.!j:I. r i ~= r j --> Domain(r i) Int Range(r j) = {} & \
+\                              Domain(r j) Int Range(r i) = {} \
+\ |] ==> wf(UN i:I. r i)";
+by(asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1);
+by(Clarify_tac 1);
+by(rename_tac "A a" 1);
+by(case_tac "? i:I. ? a:A. ? b:A. (b,a) : r i" 1);
+ by(Clarify_tac 1);
+ by(EVERY1[dtac bspec, atac,
+           eres_inst_tac[("x","{a. a:A & (? b:A. (b,a) : r i)}")]allE]);
+ by(EVERY1[etac allE,etac impE]);
+  by(Blast_tac 1);
+ by(Clarify_tac 1);
+ by(rename_tac "z'" 1);
+ by(res_inst_tac [("x","z'")] bexI 1);
+  ba 2;
+ by(Clarify_tac 1);
+ by(rename_tac "j" 1);
+ by(case_tac "r j = r i" 1);
+  by(EVERY1[etac allE,etac impE,atac]);
+  by(Asm_full_simp_tac 1);
+  by(Blast_tac 1);
+ by(blast_tac (claset() addEs [equalityE]) 1);
+by(Asm_full_simp_tac 1);
+by(case_tac "? i. i:I" 1);
+ by(Clarify_tac 1);
+ by(EVERY1[dtac bspec, atac, eres_inst_tac[("x","A")]allE]);
+ by(Blast_tac 1);
+by(Blast_tac 1);
+qed "wf_UN";
+
+Goalw [Union_def]
+ "[| !r:R. wf r; \
+\    !r:R.!s:R. r ~= s --> Domain r Int Range s = {} & \
+\                          Domain s Int Range r = {} \
+\ |] ==> wf(Union R)";
+br wf_UN 1;
+by(Blast_tac 1);
+by(Blast_tac 1);
+qed "wf_Union";
+
+Goal
+ "[| wf r; wf s; Domain r Int Range s = {}; Domain s Int Range r = {} \
+\ |] ==> wf(r Un s)";
+br(simplify (simpset()) (read_instantiate[("R","{r,s}")]wf_Union)) 1;
+by(Blast_tac 1);
+by(Blast_tac 1);
+qed "wf_Un";
+
+(*---------------------------------------------------------------------------
+ * Wellfoundedness of `image'
+ *---------------------------------------------------------------------------*)
+
+Goal "[| wf r; inj f |] ==> wf(prod_fun f f `` r)";
+by(asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1);
+by(Clarify_tac 1);
+by(case_tac "? p. f p : Q" 1);
+by(eres_inst_tac [("x","{p. f p : Q}")]allE 1);
+by(fast_tac (claset() addDs [injD]) 1);
+by(Blast_tac 1);
+qed "wf_prod_fun_image";
+
 (*** acyclic ***)
 
 val acyclicI = prove_goalw WF.thy [acyclic_def] 
diff -r 6055775a151b -r f4d16517b360 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Thu Aug 06 18:21:14 1998 +0200
+++ b/src/HOL/equalities.ML	Sat Aug 08 14:00:56 1998 +0200
@@ -123,6 +123,11 @@
 qed "image_is_empty";
 AddIffs [image_is_empty];
 
+Goal "f `` {x. P x} = {f x | x. P x}";
+by(Blast_tac 1);
+qed "image_Collect";
+Addsimps [image_Collect];
+
 Goalw [image_def]
 "(%x. if P x then f x else g x) `` S                    \
 \ = (f `` (S Int {x. P x})) Un (g `` (S Int {x. ~(P x)}))";