List now contains some lexicographic orderings.
authornipkow
Sat Aug 08 14:00:56 1998 +0200 (1998-08-08)
changeset 5281f4d16517b360
parent 5280 6055775a151b
child 5282 80c75c862a8f
List now contains some lexicographic orderings.
src/HOL/List.ML
src/HOL/List.thy
src/HOL/Trancl.ML
src/HOL/WF.ML
src/HOL/equalities.ML
     1.1 --- a/src/HOL/List.ML	Thu Aug 06 18:21:14 1998 +0200
     1.2 +++ b/src/HOL/List.ML	Sat Aug 08 14:00:56 1998 +0200
     1.3 @@ -848,6 +848,73 @@
     1.4  Addsimps [set_replicate];
     1.5  
     1.6  
     1.7 +(*** Lexcicographic orderings on lists ***)
     1.8 +section"Lexcicographic orderings on lists";
     1.9 +
    1.10 +Goal "wf r ==> wf(lexn r n)";
    1.11 +by(induct_tac "n" 1);
    1.12 +by(Simp_tac 1);
    1.13 +by(Simp_tac 1);
    1.14 +br wf_subset 1;
    1.15 +br Int_lower1 2;
    1.16 +br wf_prod_fun_image 1;
    1.17 +br injI 2;
    1.18 +by(Auto_tac);
    1.19 +qed "wf_lexn";
    1.20 +
    1.21 +Goal "!xs ys. (xs,ys) : lexn r n --> length xs = n & length ys = n";
    1.22 +by(induct_tac "n" 1);
    1.23 +by(Auto_tac);
    1.24 +qed_spec_mp "lexn_length";
    1.25 +
    1.26 +Goalw [lex_def] "wf r ==> wf(lex r)";
    1.27 +br wf_UN 1;
    1.28 +by(blast_tac (claset() addIs [wf_lexn]) 1);
    1.29 +by(Clarify_tac 1);
    1.30 +by(rename_tac "m n" 1);
    1.31 +by(subgoal_tac "m ~= n" 1);
    1.32 + by(Blast_tac 2);
    1.33 +by(blast_tac (claset() addDs [lexn_length,not_sym]) 1);
    1.34 +qed "wf_lex";
    1.35 +AddSIs [wf_lex];
    1.36 +
    1.37 +Goal
    1.38 + "lexn r n = \
    1.39 +\ {(xs,ys). length xs = n & length ys = n & \
    1.40 +\           (? xys x y xs' ys'. xs= xys @ x#xs' & ys= xys @ y#ys' & (x,y):r)}";
    1.41 +by(induct_tac "n" 1);
    1.42 + by(Simp_tac 1);
    1.43 + by(Blast_tac 1);
    1.44 +by(asm_full_simp_tac (simpset() addsimps [lex_prod_def]) 1);
    1.45 +by(Auto_tac);
    1.46 +  by(Blast_tac 1);
    1.47 + by(rename_tac "a xys x xs' y ys'" 1);
    1.48 + by(res_inst_tac [("x","a#xys")] exI 1);
    1.49 + by(Simp_tac 1);
    1.50 +by(exhaust_tac "xys" 1);
    1.51 + by(ALLGOALS Asm_full_simp_tac);
    1.52 +by(Blast_tac 1);
    1.53 +qed "lexn_conv";
    1.54 +
    1.55 +Goalw [lex_def]
    1.56 + "lex r = \
    1.57 +\ {(xs,ys). length xs = length ys & \
    1.58 +\           (? xys x y xs' ys'. xs= xys @ x#xs' & ys= xys @ y#ys' & (x,y):r)}";
    1.59 +by(force_tac (claset(), simpset() addsimps [lexn_conv]) 1);
    1.60 +qed "lex_conv";
    1.61 +
    1.62 +Goalw [lexico_def] "wf r ==> wf(lexico r)";
    1.63 +by(Blast_tac 1);
    1.64 +qed "wf_lexico";
    1.65 +AddSIs [wf_lexico];
    1.66 +
    1.67 +Goalw
    1.68 + [lexico_def,diag_def,lex_prod_def,measure_def,inv_image_def]
    1.69 +"lexico r = {(xs,ys). length xs < length ys | \
    1.70 +\                     length xs = length ys & (xs,ys) : lex r}";
    1.71 +by(Simp_tac 1);
    1.72 +qed "lexico_conv";
    1.73 +
    1.74  (***
    1.75  Simplification procedure for all list equalities.
    1.76  Currently only tries to rearranges @ to see if
     2.1 --- a/src/HOL/List.thy	Thu Aug 06 18:21:14 1998 +0200
     2.2 +++ b/src/HOL/List.thy	Sat Aug 08 14:00:56 1998 +0200
     2.3 @@ -145,6 +145,22 @@
     2.4    replicate_0   "replicate 0 x       = []"
     2.5    replicate_Suc "replicate (Suc n) x = x # replicate n x"
     2.6  
     2.7 +(** Lexcicographic orderings on lists **)
     2.8 +
     2.9 +consts
    2.10 + lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"
    2.11 +primrec
    2.12 +"lexn r 0       = {}"
    2.13 +"lexn r (Suc n) = (prod_fun (split op#) (split op#) `` (r ** lexn r n)) Int
    2.14 +                  {(xs,ys). length xs = Suc n & length ys = Suc n}"
    2.15 +
    2.16 +constdefs
    2.17 + lex :: "('a * 'a)set => ('a list * 'a list)set"
    2.18 +"lex r == UN n. lexn r n"
    2.19 +
    2.20 + lexico :: "('a * 'a)set => ('a list * 'a list)set"
    2.21 +"lexico r == inv_image (less_than ** lex r) (%xs. (length xs, xs))"
    2.22 +
    2.23  end
    2.24  
    2.25  ML
     3.1 --- a/src/HOL/Trancl.ML	Thu Aug 06 18:21:14 1998 +0200
     3.2 +++ b/src/HOL/Trancl.ML	Sat Aug 08 14:00:56 1998 +0200
     3.3 @@ -138,8 +138,7 @@
     3.4  qed "rtrancl_Un_rtrancl";
     3.5  
     3.6  Goal "(R^=)^* = R^*";
     3.7 -by (blast_tac (claset() addSIs [rtrancl_subset]
     3.8 -                       addIs  [rtrancl_refl, r_into_rtrancl]) 1);
     3.9 +by (blast_tac (claset() addSIs [rtrancl_subset] addIs [r_into_rtrancl]) 1);
    3.10  qed "rtrancl_reflcl";
    3.11  Addsimps [rtrancl_reflcl];
    3.12  
     4.1 --- a/src/HOL/WF.ML	Thu Aug 06 18:21:14 1998 +0200
     4.2 +++ b/src/HOL/WF.ML	Sat Aug 08 14:00:56 1998 +0200
     4.3 @@ -105,7 +105,7 @@
     4.4  Goal "wf({})";
     4.5  by (simp_tac (simpset() addsimps [wf_def]) 1);
     4.6  qed "wf_empty";
     4.7 -AddSIs [wf_empty];
     4.8 +AddIffs [wf_empty];
     4.9  
    4.10  (*---------------------------------------------------------------------------
    4.11   * Wellfoundedness of `insert'
    4.12 @@ -134,6 +134,74 @@
    4.13  qed "wf_insert";
    4.14  AddIffs [wf_insert];
    4.15  
    4.16 +(*---------------------------------------------------------------------------
    4.17 + * Wellfoundedness of `disjoint union'
    4.18 + *---------------------------------------------------------------------------*)
    4.19 +
    4.20 +Goal
    4.21 + "[| !i:I. wf(r i); \
    4.22 +\    !i:I.!j:I. r i ~= r j --> Domain(r i) Int Range(r j) = {} & \
    4.23 +\                              Domain(r j) Int Range(r i) = {} \
    4.24 +\ |] ==> wf(UN i:I. r i)";
    4.25 +by(asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1);
    4.26 +by(Clarify_tac 1);
    4.27 +by(rename_tac "A a" 1);
    4.28 +by(case_tac "? i:I. ? a:A. ? b:A. (b,a) : r i" 1);
    4.29 + by(Clarify_tac 1);
    4.30 + by(EVERY1[dtac bspec, atac,
    4.31 +           eres_inst_tac[("x","{a. a:A & (? b:A. (b,a) : r i)}")]allE]);
    4.32 + by(EVERY1[etac allE,etac impE]);
    4.33 +  by(Blast_tac 1);
    4.34 + by(Clarify_tac 1);
    4.35 + by(rename_tac "z'" 1);
    4.36 + by(res_inst_tac [("x","z'")] bexI 1);
    4.37 +  ba 2;
    4.38 + by(Clarify_tac 1);
    4.39 + by(rename_tac "j" 1);
    4.40 + by(case_tac "r j = r i" 1);
    4.41 +  by(EVERY1[etac allE,etac impE,atac]);
    4.42 +  by(Asm_full_simp_tac 1);
    4.43 +  by(Blast_tac 1);
    4.44 + by(blast_tac (claset() addEs [equalityE]) 1);
    4.45 +by(Asm_full_simp_tac 1);
    4.46 +by(case_tac "? i. i:I" 1);
    4.47 + by(Clarify_tac 1);
    4.48 + by(EVERY1[dtac bspec, atac, eres_inst_tac[("x","A")]allE]);
    4.49 + by(Blast_tac 1);
    4.50 +by(Blast_tac 1);
    4.51 +qed "wf_UN";
    4.52 +
    4.53 +Goalw [Union_def]
    4.54 + "[| !r:R. wf r; \
    4.55 +\    !r:R.!s:R. r ~= s --> Domain r Int Range s = {} & \
    4.56 +\                          Domain s Int Range r = {} \
    4.57 +\ |] ==> wf(Union R)";
    4.58 +br wf_UN 1;
    4.59 +by(Blast_tac 1);
    4.60 +by(Blast_tac 1);
    4.61 +qed "wf_Union";
    4.62 +
    4.63 +Goal
    4.64 + "[| wf r; wf s; Domain r Int Range s = {}; Domain s Int Range r = {} \
    4.65 +\ |] ==> wf(r Un s)";
    4.66 +br(simplify (simpset()) (read_instantiate[("R","{r,s}")]wf_Union)) 1;
    4.67 +by(Blast_tac 1);
    4.68 +by(Blast_tac 1);
    4.69 +qed "wf_Un";
    4.70 +
    4.71 +(*---------------------------------------------------------------------------
    4.72 + * Wellfoundedness of `image'
    4.73 + *---------------------------------------------------------------------------*)
    4.74 +
    4.75 +Goal "[| wf r; inj f |] ==> wf(prod_fun f f `` r)";
    4.76 +by(asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1);
    4.77 +by(Clarify_tac 1);
    4.78 +by(case_tac "? p. f p : Q" 1);
    4.79 +by(eres_inst_tac [("x","{p. f p : Q}")]allE 1);
    4.80 +by(fast_tac (claset() addDs [injD]) 1);
    4.81 +by(Blast_tac 1);
    4.82 +qed "wf_prod_fun_image";
    4.83 +
    4.84  (*** acyclic ***)
    4.85  
    4.86  val acyclicI = prove_goalw WF.thy [acyclic_def] 
     5.1 --- a/src/HOL/equalities.ML	Thu Aug 06 18:21:14 1998 +0200
     5.2 +++ b/src/HOL/equalities.ML	Sat Aug 08 14:00:56 1998 +0200
     5.3 @@ -123,6 +123,11 @@
     5.4  qed "image_is_empty";
     5.5  AddIffs [image_is_empty];
     5.6  
     5.7 +Goal "f `` {x. P x} = {f x | x. P x}";
     5.8 +by(Blast_tac 1);
     5.9 +qed "image_Collect";
    5.10 +Addsimps [image_Collect];
    5.11 +
    5.12  Goalw [image_def]
    5.13  "(%x. if P x then f x else g x) `` S                    \
    5.14  \ = (f `` (S Int {x. P x})) Un (g `` (S Int {x. ~(P x)}))";