New induction schemas for lists (length and snoc).

--- a/src/HOL/Lex/Prefix.ML	Fri Feb 20 17:57:16 1998 +0100
+++ b/src/HOL/Lex/Prefix.ML	Sun Feb 22 14:12:23 1998 +0100
@@ -4,8 +4,7 @@
     Copyright   1995 TUM
 *)
 
-open Prefix;
-
+(* Junk: *)
 val [maj,min] = goal Prefix.thy "[| Q([]); !! y ys. Q(y#ys) |] ==> ! l. Q(l)";
 by (rtac allI 1);
 by (list.induct_tac "l" 1);
@@ -13,6 +12,25 @@
 by (rtac min 1);
 val list_cases = result();
 
+(** <= is a partial order: **)
+
+goalw thy [prefix_def] "xs <= (xs::'a list)";
+by(Simp_tac 1);
+qed "prefix_refl";
+Addsimps[prefix_refl];
+
+goalw thy [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= zs |] ==> xs <= zs";
+by(Clarify_tac 1);
+by(Simp_tac 1);
+qed "prefix_trans";
+
+goalw thy [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.thy [prefix_def] "[] <= xs";
 by (simp_tac (simpset() addsimps [eq_sym_conv]) 1);
 qed "Nil_prefix";
@@ -25,6 +43,34 @@
 qed "prefix_Nil";
 Addsimps [prefix_Nil];
 
+goalw thy [prefix_def] "(xs <= ys@[y]) = (xs = ys@[y] | xs <= ys)";
+br iffI 1;
+ be exE 1;
+ by(rename_tac "zs" 1);
+ by(res_inst_tac [("xs","zs")] snoc_eq_cases 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);
+be disjE 1;
+ by(Asm_simp_tac 1);
+by(Clarify_tac 1);
+by (Simp_tac 1);
+qed "prefix_snoc";
+Addsimps [prefix_snoc];
+
+goalw Prefix.thy [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];
+
+goalw thy [prefix_def] "!!xs. xs <= ys ==> xs <= ys@zs";
+by(Clarify_tac 1);
+by (Simp_tac 1);
+qed "prefix_prefix";
+Addsimps [prefix_prefix];
+
 (* nicht sehr elegant bewiesen - Induktion eigentlich ueberfluessig *)
 goalw Prefix.thy [prefix_def]
    "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))";
@@ -33,9 +79,3 @@
 by (Simp_tac 1);
 by (Fast_tac 1);
 qed "prefix_Cons";
-
-goalw Prefix.thy [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];

--- a/src/HOL/List.ML	Fri Feb 20 17:57:16 1998 +0100
+++ b/src/HOL/List.ML	Sun Feb 22 14:12:23 1998 +0100
@@ -6,8 +6,6 @@
 List lemmas
 *)
 
-open List;
-
 goal thy "!x. xs ~= x#xs";
 by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
@@ -46,7 +44,8 @@
 Addsimps [lists_Int_eq];
 
 
-(** list_case **)
+(**  Case analysis **)
+section "Case analysis";
 
 val prems = goal thy "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)";
 by (induct_tac "xs" 1);
@@ -60,7 +59,6 @@
 bind_thm("list_eq_cases",
   impI RSN (2,allI RSN (2,allI RSN (2,impI RS (conjI RS (result() RS mp))))));
 
-
 (** length **)
 (* needs to come before "@" because of thm append_eq_append_conv *)
 
@@ -509,6 +507,51 @@
 qed_spec_mp "nth_mem";
 Addsimps [nth_mem];
 
+(**  More case analysis and induction **)
+section "More case analysis and induction";
+
+val [prem] = goal thy
+  "(!!xs. (!ys. length ys < length xs --> P ys) ==> P xs) ==> P(xs)";
+by(rtac measure_induct 1 THEN etac prem 1);
+qed "length_induct";
+
+goal thy "xs ~= [] --> (? ys y. xs = ys@[y])";
+by(res_inst_tac [("xs","xs")] length_induct 1);
+by(Clarify_tac 1);
+bd (neq_Nil_conv RS iffD1) 1;
+by(Clarify_tac 1);
+by(rename_tac "ys" 1);
+by(case_tac "ys = []" 1);
+ by(res_inst_tac [("x","[]")] exI 1);
+ by(Asm_full_simp_tac 1);
+by(eres_inst_tac [("x","ys")] allE 1);
+by(Asm_full_simp_tac 1);
+by(REPEAT(etac exE 1));
+by(rename_tac "zs z" 1);
+by(hyp_subst_tac 1);
+by(res_inst_tac [("x","y#zs")] exI 1);
+by(Simp_tac 1);
+qed_spec_mp "neq_Nil_snocD";
+
+val prems = goal thy
+  "[| xs=[] ==> P []; !!ys y. xs=ys@[y] ==> P(ys@[y]) |] ==> P xs";
+by(case_tac "xs = []" 1);
+ by(Asm_simp_tac 1);
+ bes prems 1;
+bd neq_Nil_snocD 1;
+by(REPEAT(etac exE 1));
+by(Asm_simp_tac 1);
+bes prems 1;
+qed "snoc_eq_cases";
+
+val prems = goal thy
+  "[| P []; !!x xs. P xs ==> P(xs@[x]) |] ==> P(xs)";
+by(res_inst_tac [("xs","xs")] length_induct 1);
+by(res_inst_tac [("xs","xs")] snoc_eq_cases 1);
+ brs prems 1;
+by(fast_tac (claset() addIs prems addss simpset()) 1);
+qed "snoc_induct";
+
 (** last & butlast **)
 
 goal thy "last(xs@[x]) = x";
@@ -523,6 +566,12 @@
 qed "butlast_snoc";
 Addsimps [butlast_snoc];
 
+goal thy "length(butlast xs) = length xs - 1";
+by(res_inst_tac [("xs","xs")] snoc_induct 1);
+by(ALLGOALS Asm_simp_tac);
+qed "length_butlast";
+Addsimps [length_butlast];
+
 goal thy
   "!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)";
 by (induct_tac "xs" 1);

--- a/src/HOL/List.thy	Fri Feb 20 17:57:16 1998 +0100
+++ b/src/HOL/List.thy	Sun Feb 22 14:12:23 1998 +0100
@@ -6,7 +6,7 @@
 The datatype of finite lists.
 *)
 
-List = Divides +
+List = WF_Rel +
 
 datatype 'a list = "[]" ("[]") | "#" 'a ('a list) (infixr 65)
 

--- a/src/HOL/WF_Rel.ML	Fri Feb 20 17:57:16 1998 +0100
+++ b/src/HOL/WF_Rel.ML	Sun Feb 22 14:12:23 1998 +0100
@@ -59,6 +59,11 @@
 qed "wf_measure";
 AddIffs [wf_measure];
 
+val measure_induct = standard
+    (asm_full_simplify (simpset() addsimps [measure_def,inv_image_def])
+      (wf_measure RS wf_induct));
+store_thm("measure_induct",measure_induct);
+
 (*----------------------------------------------------------------------------
  * Wellfoundedness of lexicographic combinations
  *---------------------------------------------------------------------------*)